Removed temporary definitions, adjusted definitions

Coproduct.agda

@@ -1,47 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Categories.Category hiding (_[_,_])
-open import Level
-open import Function using (_$_)
-
-module Coproduct {o ℓ e} (𝒞 : Category o ℓ e) where
-
-open Category 𝒞
-
-open import Categories.Morphism.Reasoning 𝒞
-open import Categories.Morphism 𝒞
-
-open HomReasoning
-open import Categories.Object.Coproduct
-
-private
-  variable
-    A B C D : Obj
-    f g h : A ⇒ B
-
-module _ {A B : Obj} where
-  open Coproduct {𝒞 = 𝒞} {A = A} {B = B} renaming ([_,_] to _[_,_])
-
-  repack : (p₁ p₂ : Coproduct 𝒞 A B) → A+B p₁ ⇒ A+B p₂
-  repack p₁ p₂ = p₁ [ i₁ p₂ , i₂ p₂ ]
-
-  repack∘ : (p₁ p₂ p₃ : Coproduct 𝒞 A B) → repack p₂ p₃ ∘ repack p₁ p₂ ≈ repack p₁ p₃
-  repack∘ p₁ p₂ p₃ = ⟺ $ unique p₁ 
-    (glueTrianglesˡ (inject₁ p₂) (inject₁ p₁)) 
-    (glueTrianglesˡ (inject₂ p₂) (inject₂ p₁))
-
-  repack≡id : (p : Coproduct 𝒞 A B) → repack p p ≈ id
-  repack≡id = η
-
-  repack-cancel : (p₁ p₂ : Coproduct 𝒞 A B) → repack p₁ p₂ ∘ repack p₂ p₁ ≈ id
-  repack-cancel p₁ p₂ = repack∘ p₂ p₁ p₂ ○ repack≡id p₂
-
-up-to-iso : ∀ (p₁ p₂ : Coproduct 𝒞 A B) → Coproduct.A+B p₁ ≅ Coproduct.A+B p₂
-up-to-iso p₁ p₂ = record
-  { from = repack p₁ p₂
-  ; to   = repack p₂ p₁
-  ; iso  = record
-    { isoˡ = repack-cancel p₂ p₁
-    ; isoʳ = repack-cancel p₁ p₂
-    }
-  }

Distributive/Bundle.agda

@@ -1,22 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Categories.Category
-open import Categories.Category.Cartesian
-open import Categories.Category.BinaryProducts
-open import Categories.Category.Cocartesian
-open import Distributive.Core using (Distributive)
-import Categories.Morphism as M
-
-module Distributive.Bundle where
-
-open import Level
-
-record DistributiveCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
-    field
-        U : Category o ℓ e
-        cartesian : Cartesian U
-        cocartesian : Cocartesian U
-        distributive : Distributive U cartesian cocartesian
-
-    open Category U public
-    open Distributive distributive public

Distributive/Core.agda

@@ -1,57 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Categories.Category
-open import Categories.Category.Cartesian
-open import Categories.Category.BinaryProducts
-open import Categories.Category.Cocartesian
-import Categories.Morphism as M
-import Categories.Morphism.Reasoning as MR
-
-module Distributive.Core {o ℓ e} (𝒞 : Category o ℓ e) where
-
-open import Level
-open Category 𝒞
-open M 𝒞
-
-private
-    variable
-        A B C : Obj
-
-record Distributive (cartesian : Cartesian 𝒞) (cocartesian : Cocartesian 𝒞) : Set (levelOfTerm 𝒞) where
-    open Cartesian cartesian
-    open BinaryProducts products
-    open Cocartesian cocartesian
-
-    field
-        distributeˡ : (A × B + A × C) ≅ (A × (B + C))
-
-    distributeʳ : ∀ {A B C : Obj} → (B × A + C × A) ≅ (B + C) × A
-    distributeʳ {A} {B} {C} = record 
-        { from = (swap ∘ from) ∘ (swap +₁ swap)
-        ; to = ((swap +₁ swap) ∘ to) ∘ swap 
-        ; iso = record 
-            { isoˡ = begin 
-                (((swap +₁ swap) ∘ to) ∘ swap) ∘ (swap ∘ from) ∘ (swap +₁ swap) ≈⟨ pullˡ (pullˡ (pullʳ swap∘swap)) ⟩ 
-                ((((swap +₁ swap) ∘ to) ∘ id) ∘ from) ∘ (swap +₁ swap)          ≈⟨ identityʳ ⟩∘⟨refl ⟩∘⟨refl ⟩
-                (((swap +₁ swap) ∘ to) ∘ from) ∘ (swap +₁ swap)                 ≈⟨ pullʳ isoˡ ⟩∘⟨refl ⟩
-                ((swap +₁ swap) ∘ id) ∘ (swap +₁ swap)                          ≈⟨ identityʳ ⟩∘⟨refl ⟩
-                (swap +₁ swap) ∘ (swap +₁ swap)                                 ≈⟨ +₁∘+₁ ⟩
-                ((swap ∘ swap) +₁ (swap ∘ swap))                                ≈⟨ +₁-cong₂ swap∘swap swap∘swap ⟩
-                (id +₁ id)                                                      ≈⟨ +-unique id-comm-sym id-comm-sym ⟩
-                id                                                              ∎ 
-            ; isoʳ = begin 
-                ((swap ∘ from) ∘ (swap +₁ swap)) ∘ ((swap +₁ swap) ∘ to) ∘ swap  ≈⟨ pullˡ (pullˡ (pullʳ +₁∘+₁)) ⟩ 
-                (((swap ∘ from) ∘ ((swap ∘ swap) +₁ (swap ∘ swap))) ∘ to) ∘ swap ≈⟨ (((refl⟩∘⟨ +₁-cong₂ swap∘swap swap∘swap) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
-                (((swap ∘ from) ∘ (id +₁ id)) ∘ to) ∘ swap                       ≈⟨ (((refl⟩∘⟨ +-unique id-comm-sym id-comm-sym) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
-                (((swap ∘ from) ∘ id) ∘ to) ∘ swap                               ≈⟨ ((identityʳ ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
-                ((swap ∘ from) ∘ to) ∘ swap                                      ≈⟨ (pullʳ isoʳ ⟩∘⟨refl) ⟩ 
-                (swap ∘ id) ∘ swap                                               ≈⟨ (identityʳ ⟩∘⟨refl) ⟩ 
-                swap ∘ swap                                                      ≈⟨ swap∘swap ⟩ 
-                id                                                               ∎ 
-            }
-        }
-        where 
-            open _≅_ (distributeˡ {A} {B} {C})
-            open HomReasoning
-            open Equiv
-            open MR 𝒞

ElgotAlgebra.agda

@@ -6,7 +6,8 @@ open import Categories.Category
 open import Categories.Category.Cartesian
 open import Categories.Category.BinaryProducts
 open import Categories.Category.Cocartesian
-open import Extensive.Bundle
+open import Categories.Category.Extensive.Bundle
+open import Categories.Category.Extensive
 import Categories.Morphism.Reasoning as MR
 
 private
@@ -16,8 +17,8 @@ private
 
 module _ (D : ExtensiveDistributiveCategory o ℓ e) where
   open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
-  open Cocartesian cocartesian
-  open Cartesian cartesian
+  open Cocartesian (Extensive.cocartesian extensive)
+  open Cartesian (ExtensiveDistributiveCategory.cartesian D)
   open MR C
 
   --*

ElgotAlgebras.agda

@@ -14,10 +14,9 @@ open import Categories.Object.Coproduct
 open import Categories.Category.BinaryProducts
 open import Categories.Category
 open import ElgotAlgebra
-open import Distributive.Bundle
-open import Distributive.Core
-open import Extensive.Bundle
-open import Extensive.Core
+open import Categories.Category.Distributive
+open import Categories.Category.Extensive.Bundle
+open import Categories.Category.Extensive
 open import Categories.Morphism
 
 module ElgotAlgebras where
@@ -28,8 +27,8 @@ private
 
 module _ (D : ExtensiveDistributiveCategory o ℓ e) where
   open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
-  open Cocartesian cocartesian
-  open Cartesian cartesian
+  open Cocartesian (Extensive.cocartesian extensive)
+  open Cartesian (ExtensiveDistributiveCategory.cartesian D)
   open BinaryProducts products
 
   --*
@@ -258,5 +257,5 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
     where
     open Exponential exp renaming (B^A to A^X; product to product')
     open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
-    dstr = λ {X Y Z} → _≅_.to (distributeˡ {X} {Y} {Z})
-    dstl = λ {X Y Z} → _≅_.to (distributeʳ {X} {Y} {Z})
+    dstr = λ {X Y Z} → IsIso.inv (isIsoˡ {X} {Y} {Z})
+    dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z})

Extensive/Bundle.agda

@@ -1,31 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Categories.Category
-open import Categories.Category.Cartesian
-open import Categories.Category.BinaryProducts
-open import Categories.Category.Cocartesian
-open import Distributive.Core
-open import Extensive.Core
-import Categories.Morphism as M
-
-module Extensive.Bundle where
-
-open import Level
-
-record ExtensiveCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
-    field
-        U : Category o ℓ e
-        extensive : Extensive U
-
-    open Category U public
-    open Extensive extensive public
-
-record ExtensiveDistributiveCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
-    field
-        U : Category o ℓ e
-        cartesian : Cartesian U
-        extensive : Extensive U
-    
-    open Category U public
-    open Extensive extensive public
-    open Distributive (Extensive⇒Distributive cartesian extensive) public

Extensive/Core.agda

@@ -1,99 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-module Extensive.Core where
-
--- https://ncatlab.org/nlab/show/extensive+category
-
-open import Level
-
-open import Categories.Category.Core
-open import Distributive.Core
-open import Categories.Diagram.Pullback
-open import Categories.Category.Cocartesian
-open import Categories.Category.Cartesian
-open import Categories.Category.BinaryProducts
-open import Categories.Object.Coproduct
-open import Categories.Morphism
-open import Function using (_$_)
-open import Coproduct
-
-
-private
-    variable
-        o ℓ e : Level
-
-record Extensive (𝒞 : Category o ℓ e) : Set (suc (o ⊔ ℓ ⊔ e)) where
-  open Category 𝒞
-  open Pullback
-
-  field
-    cocartesian : Cocartesian 𝒞
-  
-  module CC = Cocartesian cocartesian
-  open CC using (_+_; i₁; i₂; ¡)
-
-  field
-    -- top-row is coproduct ⇒ pullback
-    cp⇒pullback₁ : {A B C D : Obj} (cp : Coproduct 𝒞 A B) (p₂ : A ⇒ C) (f : Coproduct.A+B cp ⇒ C + D) → IsPullback 𝒞 (Coproduct.i₁ cp) p₂ f i₁
-    cp⇒pullback₂ : {A B C D : Obj} (cp : Coproduct 𝒞 A B) (p₂ : B ⇒ D) (f : Coproduct.A+B cp ⇒ C + D) → IsPullback 𝒞 (Coproduct.i₂ cp) p₂ f i₂
-
-    -- pullbacks ⇒ top-row is coproduct
-    pullbacks⇒cp : {A B C : Obj} {f : A ⇒ B + C} (P₁ : Pullback 𝒞 f i₁) (P₂ : Pullback 𝒞 f i₂) → IsCoproduct 𝒞 (Pullback.p₁ P₁) (Pullback.p₁ P₂)
-
-Extensive⇒Distributive : ∀ {𝒞 : Category o ℓ e} → (cartesian : Cartesian 𝒞) → (E : Extensive 𝒞) → Distributive 𝒞 cartesian (Extensive.cocartesian E)
-Extensive⇒Distributive {𝒞 = 𝒞} cartesian E = record 
-  { distributeˡ = λ {A} {B} {C} → ≅-sym 𝒞 $ iso {A} {B} {C} 
-  }
-  where
-    open Category 𝒞
-    open Extensive E
-    open Cocartesian cocartesian
-    open Cartesian cartesian
-    open BinaryProducts products
-    open HomReasoning
-    open Equiv
-    open ≅ using () renaming (sym to ≅-sym)
-    pb₁ : ∀ {A B C} → Pullback 𝒞 (π₂ {A = A} {B = B + C}) i₁
-    pb₁ {A} {B} {C} = record { P = A × B ; p₁ = id ⁂ i₁ ; p₂ = π₂ ; isPullback = record
-      { commute = π₂∘⁂
-      ; universal = λ {X} {h₁} {h₂} H → ⟨ π₁ ∘ h₁ , h₂ ⟩
-      ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (unique (sym $
-          begin 
-            π₁ ∘ h₁ ≈⟨ ∘-resp-≈ʳ (sym H1) ⟩ 
-            (π₁ ∘ (id ⁂ i₁) ∘ i) ≈⟨ sym-assoc ⟩
-            ((π₁ ∘ (id ⁂ i₁)) ∘ i) ≈⟨ ∘-resp-≈ˡ π₁∘⁂ ⟩
-            ((id ∘ π₁) ∘ i) ≈⟨ ∘-resp-≈ˡ identityˡ ⟩
-            π₁ ∘ i ∎) H2)
-      ; p₁∘universal≈h₁ = λ {X} {h₁} {h₂} {eq} → 
-          begin 
-            (id ⁂ i₁) ∘ ⟨ π₁ ∘ h₁ , h₂ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩
-            ⟨ id ∘ π₁ ∘ h₁ , i₁ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congʳ identityˡ ⟩
-            ⟨ π₁ ∘ h₁ , i₁ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congˡ (sym eq) ⟩
-            ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩ ≈⟨ g-η ⟩
-            h₁ ∎
-      ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → project₂
-      } }
-    pb₂ : ∀ {A B C} → Pullback 𝒞 (π₂ {A = A} {B = B + C}) i₂
-    pb₂ {A} {B} {C} = record { P = A × C ; p₁ = id ⁂ i₂ ; p₂ = π₂ ; isPullback = record
-      { commute = π₂∘⁂
-      ; universal = λ {X} {h₁} {h₂} H → ⟨ π₁ ∘ h₁ , h₂ ⟩
-      ; unique = λ {X} {h₁} {h₂} {i} {eq} H1 H2 → sym (unique (sym $
-          begin 
-            π₁ ∘ h₁ ≈⟨ ∘-resp-≈ʳ (sym H1) ⟩ 
-            (π₁ ∘ (id ⁂ i₂) ∘ i) ≈⟨ sym-assoc ⟩
-            ((π₁ ∘ (id ⁂ i₂)) ∘ i) ≈⟨ ∘-resp-≈ˡ π₁∘⁂ ⟩
-            ((id ∘ π₁) ∘ i) ≈⟨ ∘-resp-≈ˡ identityˡ ⟩
-            π₁ ∘ i ∎) H2)
-      ; p₁∘universal≈h₁ = λ {X} {h₁} {h₂} {eq} → 
-          begin 
-            (id ⁂ i₂) ∘ ⟨ π₁ ∘ h₁ , h₂ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩
-            ⟨ id ∘ π₁ ∘ h₁ , i₂ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congʳ identityˡ ⟩
-            ⟨ π₁ ∘ h₁ , i₂ ∘ h₂ ⟩ ≈⟨ ⟨⟩-congˡ (sym eq) ⟩
-            ⟨ π₁ ∘ h₁ , π₂ ∘ h₁ ⟩ ≈⟨ g-η ⟩
-            h₁ ∎
-      ; p₂∘universal≈h₂ = λ {X} {h₁} {h₂} {eq} → project₂
-      } }
-    cp₁ : ∀ {A B C : Obj} → IsCoproduct 𝒞 {A+B = A × (B + C)} (id ⁂ i₁) (id ⁂ i₂)
-    cp₁ {A} {B} {C} = pullbacks⇒cp pb₁ pb₂
-    cp₂ = λ {A B C : Obj} → coproduct {A × B} {A × C}
-    iso = λ {A B C : Obj} → Coproduct.up-to-iso 𝒞 (IsCoproduct⇒Coproduct 𝒞 (cp₁ {A} {B} {C})) cp₂