### Properties of the Subalgebra Inclusion Relation

```{-# OPTIONS --without-K --exact-split --safe #-}

open import Algebras.Basic using (π ; π₯ ; Signature )

module Subalgebras.Properties {π : Signature π π₯} where

-- Imports from Agda and the Agda Standard Library -------------------------------
open import Agda.Primitive   using ( _β_ ; lsuc ; Level ) renaming ( Set to Type )
open import Data.Product     using ( _,_ ) renaming ( projβ to fst ; projβ to snd )
open import Function.Base    using ( _β_ ; id ; flip )
open import Function.Bundles using ( Injection )
open import Relation.Unary   using ( Pred ; _β_ )
open import Relation.Binary.Definitions
using ( _RespectsΚ³_ ; _RespectsΛ‘_ )
open import Relation.Binary.PropositionalEquality
using ( _β‘_ ; refl ; module β‘-Reasoning ; cong )

-- Imports from the Agda Universal Algebra Library --------------------
open import Overture.Preliminaries             using ( β£_β£ ; β₯_β₯ ; _β»ΒΉ )
open import Overture.Injective                 using (  id-is-injective ; IsInjective ; β-injective )
open import Algebras.Basic                     using ( Algebra ; Lift-Alg )
open import Algebras.Products          {π = π} using ( ov )
open import Homomorphisms.Basic        {π = π} using ( is-homomorphism )
open import Homomorphisms.Properties   {π = π} using ( β-hom ; β-is-hom )
open import Homomorphisms.Isomorphisms {π = π} using ( _β_ ; βtoInjective ; βfromInjective ; β-refl
; β-sym ; β-trans ; Lift-β ; mkiso )
open import Subalgebras.Subalgebras    {π = π} using ( _β€_ ; _β₯_ ; _IsSubalgebraOfClass_ )

private variable Ξ± Ξ² Ξ³ π§ : Level

-- The subalgebra relation is a *preorder*, i.e., a reflexive transitive binary relation.

open _β_

β€-refl : {π¨ : Algebra Ξ± π}{π© : Algebra Ξ² π} β π¨ β π© β π¨ β€ π©
β€-refl Ο = (to Ο) , βtoInjective Ο

β₯-refl : {π¨ : Algebra Ξ± π}{π© : Algebra Ξ² π} β π¨ β π© β π¨ β₯ π©
β₯-refl Ο = (from Ο) , βfromInjective Ο

β€-reflexive : (π¨ : Algebra Ξ± π) β π¨ β€ π¨
β€-reflexive π¨ = (id , Ξ» π π β refl) , Injection.injective id-is-injective

β€-trans : (π¨ : Algebra Ξ± π){π© : Algebra Ξ² π}(πͺ : Algebra Ξ³ π)
β        π¨ β€ π© β π© β€ πͺ β π¨ β€ πͺ
β€-trans π¨ πͺ Aβ€B Bβ€C = (β-hom π¨ πͺ β£ Aβ€B β£ β£ Bβ€C β£) , β-injective β₯ Aβ€B β₯ β₯ Bβ€C β₯

β₯-trans : (π¨ : Algebra Ξ± π){π© : Algebra Ξ² π}(πͺ : Algebra Ξ³ π)
β        π¨ β₯ π© β π© β₯ πͺ β π¨ β₯ πͺ
β₯-trans π¨ πͺ Aβ₯B Bβ₯C = β€-trans πͺ π¨ Bβ₯C Aβ₯B

```

#### Relations between β€, β₯, and β

In case all algebras live in the same universe level, we can use some of the definitions in the standard library. However, to obtain more general versions, we need to either extend the standard libraryβs Binary.Structures module to be universe polymorphic, or just implement what we need here. For now we do the latter (below).

```module _ {Ξ± : Level} where

open import Relation.Binary.Structures {a = (ov Ξ±)}{β = (π β π₯ β Ξ±)} (_β_ {Ξ±}{Ξ±})

open IsPreorder

β€-preorder : IsPreorder _β€_
isEquivalence β€-preorder = record { refl = β-refl ; sym = β-sym ; trans = β-trans }
reflexive β€-preorder = β€-refl
trans β€-preorder {π¨}{π©}{πͺ} Aβ€B Bβ€C = β€-trans π¨ πͺ Aβ€B Bβ€C

β₯-preorder : IsPreorder _β₯_
isEquivalence β₯-preorder = record { refl = β-refl ; sym = β-sym ; trans = β-trans }
reflexive β₯-preorder = β₯-refl
trans β₯-preorder {π¨}{π©}{πͺ} Aβ₯B Bβ₯C = β₯-trans π¨ πͺ Aβ₯B Bβ₯C

```

Here are some consequences of the fact that `_β€_` and `_β₯_` are preorders relative to `_β_`. These are essentially equivalent variations on the following obvious fact: If two algebras are isomorphic and one of them is a subalgebra, then so is the other.

``` -- 1a. If π¨ β€ π©  and  π© β πͺ, then  π¨ β€ πͺ
β€-resp-β : _β€_ RespectsΚ³ _β_     -- usage: (note the argument order)
β€-resp-β = βΌ-respΛ‘-β β₯-preorder  -- (p : π© β πͺ) (q : π¨ β€ π©) β (β€-resp-β p q) : π¨ β€ πͺ

-- 2a. If π¨ β₯ π©  and  π© β πͺ,   then π¨ β₯ πͺ
β₯-resp-β : _β₯_ RespectsΚ³ _β_
β₯-resp-β {π¨} = βΌ-respΛ‘-β β€-preorder {π¨}

-- 1b. If π© β πͺ   and π© β₯ π¨, then  πͺ β₯ π¨
β-resp-β₯ : _β₯_ RespectsΛ‘ _β_
β-resp-β₯ = β€-resp-β

-- 2b. If π© β πͺ  and π© β€ π¨, then  πͺ β€ π¨
β-resp-β€ : _β€_ RespectsΛ‘ _β_
β-resp-β€ {π¨} = β₯-resp-β {π¨}

```

#### Relations between β€, β₯, and β (universe-polymorphic versions)

```module _ {π¨ : Algebra Ξ± π}{π© : Algebra Ξ² π}{πͺ : Algebra Ξ³ π} where
β€-RESP-β : π¨ β€ π© β π© β πͺ β π¨ β€ πͺ
β€-RESP-β a<b bc = β€-trans π¨ πͺ a<b (β€-refl bc)

β₯-RESP-β : π¨ β₯ π© β π© β πͺ β π¨ β₯ πͺ
β₯-RESP-β a<b ac = β€-trans πͺ π¨ (β€-refl (β-sym ac)) a<b

module _ {π¨ : Algebra Ξ± π}{π© : Algebra Ξ² π}{πͺ : Algebra Ξ³ π} where

β-RESP-β€ : π¨ β π© β π© β€ πͺ β π¨ β€ πͺ
β-RESP-β€ ab b<c = β₯-RESP-β{π¨ = πͺ} b<c (β-sym ab)

β-RESP-β₯ : π¨ β π© β π© β₯ πͺ β π¨ β₯ πͺ
β-RESP-β₯ ab b<c = β€-RESP-β b<c (β-sym ab)

open β‘-Reasoning
isoβinjective : {π¨ : Algebra Ξ± π}{π© : Algebra Ξ² π}
β              (Ο : π¨ β π©) β IsInjective β£ to Ο β£
isoβinjective {π¨ = π¨} (mkiso f g fβΌg gβΌf) {x} {y} fxfy =
(β£ g β£ β β£ f β£) x  β‘β¨ cong β£ g β£ fxfy β©
(β£ g β£ β β£ f β£) y  β‘β¨ gβΌf y β©
y                  β

β€-mono : (π© : Algebra Ξ² π){π¦ π¦' : Pred (Algebra Ξ± π) Ξ³}
β       π¦ β π¦' β π© IsSubalgebraOfClass π¦ β π© IsSubalgebraOfClass π¦'

β€-mono π© KK' KB = β£ KB β£ , fst β₯ KB β₯ , KK' (β£ snd β₯ KB β₯ β£) , β₯ (snd β₯ KB β₯) β₯

```

#### Lifts of subalgebras

```module _ {π¦ : Pred (Algebra Ξ± π)(ov Ξ±)}{π© : Algebra Ξ± π} where

Lift-is-sub (π¨ , (sa , (KA , Bβsa))) = π¨ , sa , KA , β-trans (β-sym Lift-β) Bβsa

β€-Lift : {π¨ : Algebra Ξ± π}(π© : Algebra Ξ² π){β : Level} β π¨ β€ π© β π¨ β€ Lift-Alg π© β