↑ Top

---

Isomorphisms of setoid algebras

This is the Setoid.Homomorphisms.Factor module of the Agda Universal Algebra Library.

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

open import Overture using (𝓞 ; 𝓥 ; Signature)

module Setoid.Homomorphisms.Isomorphisms {𝑆 : Signature 𝓞 𝓥}  where

-- Imports from Agda (builtin/primitive) and the Agda Standard Library ---------------------
open import Agda.Primitive              using ()      renaming ( Set to Type )
open import Data.Product                using ( _,_ )
open import Data.Unit.Polymorphic.Base  using ()      renaming ( ⊤ to 𝟙 ; tt to ∗ )
open import Data.Unit.Base              using ( ⊤ ; tt )
open import Function                    using ( id )  renaming ( Func to _⟶_ )
open import Level                       using ( Level ; Lift ; lift ; lower ; _⊔_ )
open import Relation.Binary             using ( Setoid ; Reflexive ; Sym ; Trans )

open import Relation.Binary.PropositionalEquality as ≡ using ()

-- Imports from the Agda Universal Algebra Library -----------------------------------------
open import Overture          using ( ∣_∣ ; ∥_∥ )
open import Setoid.Functions  using ( _∘_ ; eq ; IsInjective ; IsSurjective )

open import Setoid.Algebras {𝑆 = 𝑆}  using ( Algebra ; Lift-Alg ; _̂_ )
                                     using ( Lift-Algˡ ; Lift-Algʳ ; ⨅ )

open import Setoid.Homomorphisms.Basic       {𝑆 = 𝑆} using  ( hom ; IsHom )
open import Setoid.Homomorphisms.Properties  {𝑆 = 𝑆} using
 ( 𝒾𝒹 ; ∘-hom ; ToLiftˡ ; FromLiftˡ ; ToFromLiftˡ ; FromToLiftˡ
 ; ToLiftʳ ; FromLiftʳ ; ToFromLiftʳ ; FromToLiftʳ )

open _⟶_      using ( cong ) renaming ( f to _⟨$⟩_ )
open Algebra  using ( Domain )

private variable  α ρᵃ β ρᵇ γ ρᶜ ι : Level

Recall, f ~ g means f and g are extensionally (or pointwise) equal; i.e., ∀ x, f x ≡ g x. We use this notion of equality of functions in the following definition of isomorphism.

We could define this using Sigma types, like this.

_≅_ : {α β : Level}(𝑨 : Algebra α 𝑆)(𝑩 : Algebra β ρᵇ) → Type(𝓞 ⊔ 𝓥 ⊔ α ⊔ β)
𝑨 ≅ 𝑩 =  Σ[ f ∈ (hom 𝑨 𝑩)] Σ[ g ∈ hom 𝑩 𝑨 ] ((∣ f ∣ ∘ ∣ g ∣ ≈ ∣ 𝒾𝒹 𝑩 ∣) × (∣ g ∣ ∘ ∣ f ∣ ≈ ∣ 𝒾𝒹 𝑨 ∣))

However, with four components, an equivalent record type is easier to work with.

module _ (𝑨 : Algebra α ρᵃ) (𝑩 : Algebra β ρᵇ) where
 open Setoid (Domain 𝑨) using ( sym ; trans ) renaming ( _≈_ to _≈₁_ )
 open Setoid (Domain 𝑩) using () renaming ( _≈_ to _≈₂_ ; sym to sym₂ ; trans to trans₂)

 record _≅_ : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ β ⊔ ρᵃ ⊔ ρᵇ ) where
  constructor mkiso
  field
   to : hom 𝑨 𝑩
   from : hom 𝑩 𝑨
   to∼from : ∀ b → (∣ to ∣ ⟨$⟩ (∣ from ∣ ⟨$⟩ b)) ≈₂ b
   from∼to : ∀ a → (∣ from ∣ ⟨$⟩ (∣ to ∣ ⟨$⟩ a)) ≈₁ a

  toIsSurjective : IsSurjective ∣ to ∣
  toIsSurjective {y} = eq (∣ from ∣ ⟨$⟩ y) (sym₂ (to∼from y))

  toIsInjective : IsInjective ∣ to ∣
  toIsInjective {x} {y} xy = Goal
   where
   ξ : ∣ from ∣ ⟨$⟩ (∣ to ∣ ⟨$⟩ x) ≈₁ ∣ from ∣ ⟨$⟩ (∣ to ∣ ⟨$⟩ y)
   ξ = cong ∣ from ∣ xy
   Goal : x ≈₁ y
   Goal = trans (sym (from∼to x)) (trans ξ (from∼to y))


  fromIsSurjective : IsSurjective ∣ from ∣
  fromIsSurjective {y} = eq (∣ to ∣ ⟨$⟩ y) (sym (from∼to y))

  fromIsInjective : IsInjective ∣ from ∣
  fromIsInjective {x} {y} xy = Goal
   where
   ξ : ∣ to ∣ ⟨$⟩ (∣ from ∣ ⟨$⟩ x) ≈₂ ∣ to ∣ ⟨$⟩ (∣ from ∣ ⟨$⟩ y)
   ξ = cong ∣ to ∣ xy
   Goal : x ≈₂ y
   Goal = trans₂ (sym₂ (to∼from x)) (trans₂ ξ (to∼from y))

That is, two structures are isomorphic provided there are homomorphisms going back and forth between them which compose to the identity map.

Properties of isomorphism of setoid algebras

open _≅_

≅-refl : Reflexive (_≅_ {α}{ρᵃ})
≅-refl {α}{ρᵃ}{𝑨} = mkiso 𝒾𝒹 𝒾𝒹 (λ b → refl) λ a → refl
 where open Setoid (Domain 𝑨) using ( refl )

≅-sym : Sym (_≅_{β}{ρᵇ}) (_≅_{α}{ρᵃ})
≅-sym φ = mkiso (from φ) (to φ) (from∼to φ) (to∼from φ)

≅-trans : Trans (_≅_ {α}{ρᵃ})(_≅_{β}{ρᵇ})(_≅_{α}{ρᵃ}{γ}{ρᶜ})
≅-trans {ρᶜ = ρᶜ}{𝑨}{𝑩}{𝑪} ab bc = mkiso f g τ ν
  where
  open Setoid (Domain 𝑨) using () renaming ( _≈_ to _≈₁_ ; trans to trans₁ )
  open Setoid (Domain 𝑪) using () renaming ( _≈_ to _≈₃_ ; trans to trans₃ )
  f : hom 𝑨 𝑪
  f = ∘-hom (to ab) (to bc)

  g : hom 𝑪 𝑨
  g = ∘-hom (from bc) (from ab)

  τ : ∀ b → (∣ f ∣ ⟨$⟩ (∣ g ∣ ⟨$⟩ b)) ≈₃ b
  τ b = trans₃ (cong ∣ to bc ∣ (to∼from ab (∣ from bc ∣ ⟨$⟩ b))) (to∼from bc b)

  ν : ∀ a → (∣ g ∣ ⟨$⟩ (∣ f ∣ ⟨$⟩ a)) ≈₁ a
  ν a = trans₁ (cong ∣ from ab ∣ (from∼to bc (∣ to ab ∣ ⟨$⟩ a))) (from∼to ab a)

module _ {𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ} where
 open Setoid (Domain 𝑨) using ( _≈_ ; sym ; trans )

 -- The "to" map of an isomorphism is injective.
 ≅toInjective : (φ : 𝑨 ≅ 𝑩) → IsInjective ∣ to φ ∣
 ≅toInjective (mkiso (f , _) (g , _) _ g∼f){a₀}{a₁} fafb = Goal
  where
  lem1 : a₀ ≈ (g ⟨$⟩ (f ⟨$⟩ a₀))
  lem1 = sym (g∼f a₀)
  lem2 : (g ⟨$⟩ (f ⟨$⟩ a₀)) ≈ (g ⟨$⟩ (f ⟨$⟩ a₁))
  lem2 = cong g fafb
  lem3 : (g ⟨$⟩ (f ⟨$⟩ a₁)) ≈ a₁
  lem3 = g∼f a₁
  Goal : a₀ ≈ a₁
  Goal = trans lem1 (trans lem2 lem3)

 -- The "from" map of an isomorphism is injective.
≅fromInjective :  {𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ}
                  (φ : 𝑨 ≅ 𝑩) → IsInjective ∣ from φ ∣

≅fromInjective φ = ≅toInjective (≅-sym φ)

Fortunately, the lift operation preserves isomorphism (i.e., it’s an algebraic invariant). As our focus is universal algebra, this is important and is what makes the lift operation a workable solution to the technical problems that arise from the noncumulativity of Agda’s universe hierarchy.

module _ {𝑨 : Algebra α ρᵃ}{ℓ : Level} where
 Lift-≅ˡ : 𝑨 ≅ (Lift-Algˡ 𝑨 ℓ)
 Lift-≅ˡ = mkiso ToLiftˡ FromLiftˡ (ToFromLiftˡ{𝑨 = 𝑨}) (FromToLiftˡ{𝑨 = 𝑨}{ℓ})

 Lift-≅ʳ : 𝑨 ≅ (Lift-Algʳ 𝑨 ℓ)
 Lift-≅ʳ = mkiso ToLiftʳ FromLiftʳ (ToFromLiftʳ{𝑨 = 𝑨}) (FromToLiftʳ{𝑨 = 𝑨}{ℓ})

Lift-≅ : {𝑨 : Algebra α ρᵃ}{ℓ ρ : Level} → 𝑨 ≅ (Lift-Alg 𝑨 ℓ ρ)
Lift-≅ = ≅-trans Lift-≅ˡ Lift-≅ʳ


module _ {𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ}{ℓᵃ ℓᵇ : Level} where

 Lift-Alg-isoˡ : 𝑨 ≅ 𝑩 → Lift-Algˡ 𝑨 ℓᵃ ≅ Lift-Algˡ 𝑩 ℓᵇ
 Lift-Alg-isoˡ A≅B = ≅-trans (≅-trans (≅-sym Lift-≅ˡ ) A≅B) Lift-≅ˡ

 Lift-Alg-isoʳ : 𝑨 ≅ 𝑩 →  Lift-Algʳ 𝑨 ℓᵃ ≅ Lift-Algʳ 𝑩 ℓᵇ
 Lift-Alg-isoʳ A≅B = ≅-trans (≅-trans (≅-sym Lift-≅ʳ ) A≅B) Lift-≅ʳ


Lift-Alg-iso :  {𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ}{ℓᵃ rᵃ ℓᵇ rᵇ : Level}
 →              𝑨 ≅ 𝑩 → Lift-Alg 𝑨 ℓᵃ rᵃ ≅ Lift-Alg 𝑩 ℓᵇ rᵇ
Lift-Alg-iso {ℓᵇ = ℓᵇ} A≅B =
  ≅-trans  (Lift-Alg-isoʳ{ℓᵇ = ℓᵇ}(≅-trans (Lift-Alg-isoˡ{ℓᵇ = ℓᵇ} A≅B) (≅-sym Lift-≅ˡ)))
           (Lift-Alg-isoʳ Lift-≅ˡ)

The lift is also associative, up to isomorphism at least.

module _ {𝑨 : Algebra α ρᵃ}{ℓ₁ ℓ₂ : Level} where

 Lift-assocˡ : Lift-Algˡ 𝑨 (ℓ₁ ⊔ ℓ₂) ≅  Lift-Algˡ (Lift-Algˡ 𝑨 ℓ₁) ℓ₂
 Lift-assocˡ = ≅-trans (≅-trans (≅-sym Lift-≅ˡ) Lift-≅ˡ) Lift-≅ˡ

 Lift-assocʳ : Lift-Algʳ 𝑨 (ℓ₁ ⊔ ℓ₂) ≅  Lift-Algʳ (Lift-Algʳ 𝑨 ℓ₁) ℓ₂
 Lift-assocʳ = ≅-trans (≅-trans (≅-sym Lift-≅ʳ) Lift-≅ʳ) Lift-≅ʳ

Lift-assoc :  {𝑨 : Algebra α ρᵃ}{ℓ ρ : Level}
 →            Lift-Alg 𝑨 ℓ ρ ≅  Lift-Algʳ (Lift-Algˡ 𝑨 ℓ) ρ
Lift-assoc {𝑨 = 𝑨}{ℓ}{ρ} = ≅-trans (≅-sym Lift-≅) (≅-trans Lift-≅ˡ Lift-≅ʳ)

Lift-assoc' :  {𝑨 : Algebra α α}{β γ : Level}
 →             Lift-Alg 𝑨 (β ⊔ γ) (β ⊔ γ) ≅ Lift-Alg (Lift-Alg 𝑨 β β) γ γ
Lift-assoc'{𝑨 = 𝑨}{β}{γ} = ≅-trans (≅-sym Lift-≅) (≅-trans Lift-≅ Lift-≅)

Products of isomorphic families of algebras are themselves isomorphic. The proof looks a bit technical, but it is as straightforward as it ought to be.

module _ {𝓘 : Level}{I : Type 𝓘} {𝒜 : I → Algebra α ρᵃ} {ℬ : I → Algebra β ρᵇ} where
 open Algebra (⨅ 𝒜)  using () renaming (Domain to ⨅A )
 open Setoid ⨅A      using () renaming ( _≈_ to _≈₁_ )
 open Algebra (⨅ ℬ)  using () renaming (Domain to ⨅B )
 open Setoid ⨅B      using () renaming ( _≈_ to _≈₂_ )
 open IsHom

 ⨅≅ : (∀ (i : I) → 𝒜 i ≅ ℬ i) → ⨅ 𝒜 ≅ ⨅ ℬ
 ⨅≅ AB = mkiso (ϕ , ϕhom) (ψ , ψhom) ϕ∼ψ ψ∼ϕ
  where
   ϕ : ⨅A ⟶ ⨅B
   ϕ = record  { f = λ a i → ∣ to (AB i) ∣ ⟨$⟩ (a i)
               ; cong = λ a i → cong ∣ to (AB i) ∣ (a i)
               }

   ϕhom : IsHom (⨅ 𝒜) (⨅ ℬ) ϕ
   ϕhom = record { compatible = λ i → compatible ∥ to (AB i) ∥ }

   ψ : ⨅B ⟶ ⨅A
   ψ = record  { f = λ b i → ∣ from (AB i) ∣ ⟨$⟩ (b i)
               ; cong = λ b i → cong ∣ from (AB i) ∣ (b i)
               }

   ψhom : IsHom (⨅ ℬ) (⨅ 𝒜) ψ
   ψhom = record { compatible = λ i → compatible ∥ from (AB i) ∥ }

   ϕ∼ψ : ∀ b → (ϕ ⟨$⟩ (ψ ⟨$⟩ b)) ≈₂ b
   ϕ∼ψ b = λ i → to∼from (AB i) (b i)

   ψ∼ϕ : ∀ a → (ψ ⟨$⟩ (ϕ ⟨$⟩ a)) ≈₁ a
   ψ∼ϕ a = λ i → from∼to (AB i)(a i)

A nearly identical proof goes through for isomorphisms of lifted products.

module _  {𝓘 : Level}{I : Type 𝓘}
          {𝒜 : I → Algebra α ρᵃ}
          {ℬ : (Lift γ I) → Algebra β ρᵇ} where

 open Algebra (⨅ 𝒜)  using () renaming (Domain to ⨅A )
 open Setoid ⨅A      using () renaming ( _≈_ to _≈₁_ )
 open Algebra (⨅ ℬ)  using () renaming (Domain to ⨅B )
 open Setoid ⨅B      using () renaming ( _≈_ to _≈₂_ )
 open IsHom

 Lift-Alg-⨅≅ˡ : (∀ i → 𝒜 i ≅ ℬ (lift i)) → Lift-Algˡ (⨅ 𝒜) γ ≅ ⨅ ℬ
 Lift-Alg-⨅≅ˡ AB = ≅-trans (≅-sym Lift-≅ˡ) A≅B
  where
   ϕ : ⨅A ⟶ ⨅B
   ϕ = record  { f = λ a i → ∣ to (AB (lower i)) ∣ ⟨$⟩ (a (lower i))
               ; cong = λ a i → cong ∣ to (AB (lower i)) ∣ (a (lower i))
               }

   ϕhom : IsHom (⨅ 𝒜) (⨅ ℬ) ϕ
   ϕhom = record { compatible = λ i → compatible ∥ to (AB (lower i)) ∥ }

   ψ : ⨅B ⟶ ⨅A
   ψ = record  { f = λ b i → ∣ from (AB i) ∣ ⟨$⟩ (b (lift i))
               ; cong = λ b i → cong ∣ from (AB i) ∣ (b (lift i))
               }

   ψhom : IsHom (⨅ ℬ) (⨅ 𝒜) ψ
   ψhom = record { compatible = λ i → compatible ∥ from (AB i) ∥ }

   ϕ∼ψ : ∀ b → (ϕ ⟨$⟩ (ψ ⟨$⟩ b)) ≈₂ b
   ϕ∼ψ b = λ i → to∼from (AB (lower i)) (b i)

   ψ∼ϕ : ∀ a → (ψ ⟨$⟩ (ϕ ⟨$⟩ a)) ≈₁ a
   ψ∼ϕ a = λ i → from∼to (AB i)(a i)

   A≅B : ⨅ 𝒜 ≅ ⨅ ℬ
   A≅B = mkiso (ϕ , ϕhom) (ψ , ψhom) ϕ∼ψ ψ∼ϕ

module _ {𝓘 : Level}{I : Type 𝓘} {𝒜 : I → Algebra α ρᵃ} where
 open IsHom
 open Algebra  using (Domain)
 open Setoid   using (_≈_ )

 ⨅≅⨅ℓ : ∀ {ℓ} → ⨅ 𝒜 ≅ ⨅ (λ i → Lift-Alg (𝒜 (lower{ℓ = ℓ} i)) ℓ ℓ)
 ⨅≅⨅ℓ {ℓ} = mkiso (φ , φhom) (ψ , ψhom) φ∼ψ ψ∼φ
  where
  open Algebra (⨅ 𝒜)  using () renaming (Domain to ⨅A )
  open Setoid ⨅A      using () renaming ( _≈_ to _≈₁_ )

  ⨅ℓ𝒜 : Algebra _ _
  ⨅ℓ𝒜 = ⨅ (λ i → Lift-Alg (𝒜 (lower{ℓ = ℓ} i)) ℓ ℓ)

  open Algebra ⨅ℓ𝒜 using () renaming (Domain to ⨅ℓA)

  φ : ⨅A ⟶ ⨅ℓA
  (φ ⟨$⟩ x) i = lift (x (lower i))
  cong φ x i = lift (x (lower i))
  φhom : IsHom (⨅ 𝒜) ⨅ℓ𝒜  φ
  compatible φhom i = lift refl
   where open Setoid (Domain (𝒜 (lower i))) using ( refl )

  ψ : ⨅ℓA ⟶ ⨅A
  (ψ ⟨$⟩ x) i = lower (x (lift i))
  cong ψ x i = lower (x (lift i))
  ψhom : IsHom ⨅ℓ𝒜 (⨅ 𝒜) ψ
  compatible ψhom i = refl
   where open Setoid (Domain (𝒜 i)) using ( refl )

  φ∼ψ : ∀ b i → (Domain (Lift-Alg (𝒜 (lower i)) ℓ ℓ)) ._≈_ ((φ ⟨$⟩ (ψ ⟨$⟩ b)) i) (b i)
  φ∼ψ _ i = lift (reflexive ≡.refl)
   where open Setoid (Domain (𝒜 (lower i))) using ( reflexive )

  ψ∼φ : ∀ a i → (Domain (𝒜 i)) ._≈_ ((ψ ⟨$⟩ (φ ⟨$⟩ a)) i) (a i)
  ψ∼φ _ i = (reflexive ≡.refl)
   where open Setoid (Domain (𝒜  i)) using ( reflexive )

module _ {ι : Level}{I : Type ι}{𝒜 : I → Algebra α ρᵃ} where
 open IsHom
 open Algebra  using (Domain)
 open Setoid   using (_≈_ )

 ⨅≅⨅ℓρ : ∀ {ℓ ρ} → ⨅ 𝒜 ≅ ⨅ (λ i → Lift-Alg (𝒜 i) ℓ ρ)
 ⨅≅⨅ℓρ {ℓ}{ρ} = mkiso φ ψ φ∼ψ ψ∼φ
  where
  open Algebra (⨅ 𝒜)                         using () renaming ( Domain to ⨅A )
  open Setoid ⨅A                             using () renaming ( _≈_ to _≈⨅A≈_ )
  open Algebra (⨅ λ i → Lift-Alg (𝒜 i) ℓ ρ)  using () renaming ( Domain to ⨅lA )
  open Setoid ⨅lA                            using () renaming ( _≈_ to _≈⨅lA≈_ )

  φfunc : ⨅A ⟶ ⨅lA
  (φfunc ⟨$⟩ x) i = lift (x i)
  cong φfunc x i = lift (x i)

  φhom : IsHom (⨅ 𝒜) (⨅ λ i → Lift-Alg (𝒜 i) ℓ ρ) φfunc
  compatible φhom i = refl
   where open Setoid (Domain (Lift-Alg (𝒜 i) ℓ ρ)) using ( refl )

  φ : hom (⨅ 𝒜) (⨅ λ i → Lift-Alg (𝒜 i) ℓ ρ)
  φ = φfunc , φhom

  ψfunc : ⨅lA ⟶ ⨅A
  (ψfunc ⟨$⟩ x) i = lower (x i)
  cong ψfunc x i = lower (x i)

  ψhom : IsHom (⨅ λ i → Lift-Alg (𝒜 i) ℓ ρ) (⨅ 𝒜) ψfunc
  compatible ψhom i = refl
   where open Setoid (Domain (𝒜 i)) using (refl)

  ψ : hom (⨅ λ i → Lift-Alg (𝒜 i) ℓ ρ) (⨅ 𝒜)
  ψ = ψfunc , ψhom

  φ∼ψ : ∀ b → ∣ φ ∣ ⟨$⟩ (∣ ψ ∣ ⟨$⟩ b) ≈⨅lA≈ b
  φ∼ψ _ i = reflexive ≡.refl
   where open Setoid (Domain (Lift-Alg (𝒜 i) ℓ ρ)) using ( reflexive )

  ψ∼φ : ∀ a → ∣ ψ ∣ ⟨$⟩ (∣ φ ∣ ⟨$⟩ a) ≈⨅A≈ a
  ψ∼φ _ = reflexive ≡.refl
   where open Setoid (Domain (⨅ 𝒜)) using ( reflexive )


module _ {ℓᵃ : Level}{I : Type ℓᵃ}{𝒜 : I → Algebra α ρᵃ}where
 open IsHom
 open Algebra  using (Domain)
 open Setoid   using (_≈_ )

 ⨅≅⨅lowerℓρ : ∀ {ℓ ρ} → ⨅ 𝒜 ≅ ⨅ λ i → Lift-Alg (𝒜 (lower{ℓ = α ⊔ ρᵃ} i)) ℓ ρ
 ⨅≅⨅lowerℓρ {ℓ}{ρ} = mkiso φ ψ φ∼ψ ψ∼φ
  where
  open Algebra (⨅ 𝒜)                               using() renaming ( Domain to ⨅A )
  open Setoid ⨅A                                   using() renaming ( _≈_ to _≈⨅A≈_ )
  open Algebra(⨅ λ i → Lift-Alg(𝒜 (lower i)) ℓ ρ)  using() renaming ( Domain to ⨅lA )
  open Setoid ⨅lA                                  using() renaming ( _≈_ to _≈⨅lA≈_ )

  φfunc : ⨅A ⟶ ⨅lA
  (φfunc ⟨$⟩ x) i = lift (x (lower i))
  cong φfunc x i = lift (x (lower i))

  φhom : IsHom (⨅ 𝒜) (⨅ λ i → Lift-Alg (𝒜 (lower i)) ℓ ρ) φfunc
  compatible φhom i = refl
   where open Setoid (Domain (Lift-Alg (𝒜 (lower i)) ℓ ρ)) using ( refl )

  φ : hom (⨅ 𝒜) (⨅ λ i → Lift-Alg (𝒜 (lower i)) ℓ ρ)
  φ = φfunc , φhom

  ψfunc : ⨅lA ⟶ ⨅A
  (ψfunc ⟨$⟩ x) i = lower (x (lift i))
  cong ψfunc x i = lower (x (lift i))

  ψhom : IsHom (⨅ λ i → Lift-Alg (𝒜 (lower i)) ℓ ρ) (⨅ 𝒜) ψfunc
  compatible ψhom i = refl
   where open Setoid (Domain (𝒜 i)) using (refl)

  ψ : hom (⨅ λ i → Lift-Alg (𝒜 (lower i)) ℓ ρ) (⨅ 𝒜)
  ψ = ψfunc , ψhom

  φ∼ψ : ∀ b → ∣ φ ∣ ⟨$⟩ (∣ ψ ∣ ⟨$⟩ b) ≈⨅lA≈ b
  φ∼ψ _ i = reflexive ≡.refl
   where open Setoid (Domain (Lift-Alg (𝒜 (lower i)) ℓ ρ)) using (reflexive)

  ψ∼φ : ∀ a → ∣ ψ ∣ ⟨$⟩ (∣ φ ∣ ⟨$⟩ a) ≈⨅A≈ a
  ψ∼φ _ = reflexive ≡.refl
   where open Setoid (Domain (⨅ 𝒜)) using (reflexive)

 ℓ⨅≅⨅ℓ : ∀ {ℓ} → Lift-Alg (⨅ 𝒜) ℓ ℓ ≅ ⨅ λ i → Lift-Alg (𝒜 (lower{ℓ = ℓ} i)) ℓ ℓ
 ℓ⨅≅⨅ℓ {ℓ} = mkiso (φ , φhom) (ψ , ψhom) φ∼ψ ψ∼φ -- φ∼ψ ψ∼φ
  where
  ℓ⨅𝒜 : Algebra _ _
  ℓ⨅𝒜 = Lift-Alg (⨅ 𝒜) ℓ ℓ
  ⨅ℓ𝒜 : Algebra _ _
  ⨅ℓ𝒜 = ⨅ (λ i → Lift-Alg (𝒜 (lower{ℓ = ℓ} i)) ℓ ℓ)

  open Algebra ℓ⨅𝒜  using() renaming (Domain to ℓ⨅A )
  open Setoid ℓ⨅A   using() renaming ( _≈_ to _≈₁_ )
  open Algebra ⨅ℓ𝒜  using() renaming (Domain to ⨅ℓA)
  open Setoid ⨅ℓA   using() renaming ( _≈_ to _≈₂_ )

  φ : ℓ⨅A ⟶ ⨅ℓA
  (φ ⟨$⟩ x) i = lift ((lower x)(lower i))
  cong φ x i = lift ((lower x)(lower i))
  φhom : IsHom ℓ⨅𝒜 ⨅ℓ𝒜  φ
  compatible φhom i = lift refl
   where open Setoid (Domain (𝒜 (lower i))) using ( refl )

  ψ : ⨅ℓA ⟶ ℓ⨅A
  (ψ ⟨$⟩ x) = lift λ i → lower (x (lift i))
  cong ψ x = lift λ i → lower (x (lift i))
  ψhom : IsHom ⨅ℓ𝒜 ℓ⨅𝒜 ψ
  lower (compatible ψhom) i = refl
   where open Setoid (Domain (𝒜 i)) using ( refl )

  φ∼ψ : ∀ b → (φ ⟨$⟩ (ψ ⟨$⟩ b)) ≈₂ b
  lower (φ∼ψ _ i) = reflexive ≡.refl
   where open Setoid (Domain (𝒜 (lower i))) using ( reflexive )

  ψ∼φ : ∀ a → (ψ ⟨$⟩ (φ ⟨$⟩ a)) ≈₁ a
  lower (ψ∼φ _) i = reflexive ≡.refl
   where open Setoid (Domain (𝒜  i)) using ( reflexive )

module _ {ι : Level}{𝑨 : Algebra α ρᵃ} where
 open Algebra 𝑨                     using() renaming ( Domain to A )
 open Algebra (⨅ λ (i : 𝟙{ι}) → 𝑨)  using() renaming ( Domain to ⨅A )
 open Setoid A                      using ( refl )
 open _≅_
 open IsHom

 private
  to𝟙 : A ⟶ ⨅A
  (to𝟙 ⟨$⟩ x) ∗ = x
  cong to𝟙 xy ∗ = xy
  from𝟙 : ⨅A ⟶ A
  from𝟙 ⟨$⟩ x = x ∗
  cong from𝟙 xy = xy ∗

  to𝟙IsHom : IsHom 𝑨 (⨅ (λ _ → 𝑨)) to𝟙
  compatible to𝟙IsHom = λ _ → refl
  from𝟙IsHom : IsHom (⨅ (λ _ → 𝑨)) 𝑨 from𝟙
  compatible from𝟙IsHom = refl

 ≅⨅⁺-refl : 𝑨 ≅ ⨅ (λ (i : 𝟙) → 𝑨)
 to ≅⨅⁺-refl = to𝟙 , to𝟙IsHom
 from ≅⨅⁺-refl = from𝟙 , from𝟙IsHom
 to∼from ≅⨅⁺-refl = λ _ _ → refl
 from∼to ≅⨅⁺-refl = λ _ → refl

module _ {𝑨 : Algebra α ρᵃ} where
 open Algebra 𝑨                  using () renaming ( Domain to A )
 open Algebra (⨅ λ (i : ⊤) → 𝑨)  using () renaming ( Domain to ⨅A )
 open Setoid A                   using ( refl )
 open _≅_
 open IsHom

 private
  to⊤ : A ⟶ ⨅A
  (to⊤ ⟨$⟩ x) = λ _ → x
  cong to⊤ xy = λ _ → xy
  from⊤ : ⨅A ⟶ A
  from⊤ ⟨$⟩ x = x tt
  cong from⊤ xy = xy tt

  to⊤IsHom : IsHom 𝑨 (⨅ λ _ → 𝑨) to⊤
  compatible to⊤IsHom = λ _ → refl
  from⊤IsHom : IsHom (⨅ λ _ → 𝑨) 𝑨 from⊤
  compatible from⊤IsHom = refl

 ≅⨅-refl : 𝑨 ≅ ⨅ (λ (i : ⊤) → 𝑨)
 to ≅⨅-refl = to⊤ , to⊤IsHom
 from ≅⨅-refl = from⊤ , from⊤IsHom
 to∼from ≅⨅-refl = λ _ _ → refl
 from∼to ≅⨅-refl = λ _ → refl

---

← Setoid.Homomorphisms.Factor Setoid.Homomorphisms.HomomorphicImages →