### Properties of the Subalgebra Inclusion Relation

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

open import Overture using (π ; π₯ ; Signature )

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

-- Imports from Agda and the Agda Standard Library -------------------------------
open import Data.Product     using ( _,_ ) renaming ( projβ to fst ; projβ to snd )
open import Function         using ( _β_ ; id ; flip ; Injection )
open import Level            using ( Level; _β_ )
open import Relation.Unary   using ( Pred ; _β_ )
open import Relation.Binary  using ( _RespectsΚ³_ ; _RespectsΛ‘_ )

open  import Relation.Binary.PropositionalEquality as β‘
using ( _β‘_ ; module β‘-Reasoning )

-- Imports from the Agda Universal Algebra Library --------------------
open  import Overture        using ( β£_β£ ; β₯_β₯ ; _β»ΒΉ )
open  import Base.Functions  using ( id-is-injective ; IsInjective ; β-injective )

open  import Base.Algebras       {π = π}  using ( Algebra ; Lift-Alg ; ov )
open  import Base.Homomorphisms  {π = π}  using ( is-homomorphism ; β-hom )
using ( β-is-hom ; _β_ ; βtoInjective )
using ( βfromInjective ; β-refl ; β-sym )
using ( β-trans ; Lift-β ; mkiso )
open  import Base.Subalgebras.Subalgebras
{π = π}  using  ( _β€_ ; _β₯_ ; _IsSubalgebraOfClass_ )

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

-- The subalgebra relation is a *preorder* (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