From 4a5c79d076d5bc6f3ca97b3950ab3b86e86b24c5 Mon Sep 17 00:00:00 2001 From: JacquesCarette Date: Sat, 30 Dec 2023 14:23:33 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/agd?= =?UTF-8?q?a-categories@e5fef742f6f9b250876ffbbb71edb368b8b96c98=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Categories.Adjoint.AFT.html | 8 +- Categories.Adjoint.Instance.BaseChange.html | 23 + Categories.Adjoint.Instance.Slice.html | 48 + Categories.Adjoint.Properties.html | 6 +- ...ry.CartesianClosed.Locally.Properties.html | 4 +- Categories.Category.Construction.Comma.html | 188 ++-- ...ategory.Construction.Properties.Comma.html | 28 +- Categories.Diagram.Limit.Ran.html | 18 +- Categories.Functor.Slice.BaseChange.html | 26 + Categories.Functor.Slice.html | 256 ++--- Categories.Morphism.Universal.html | 2 +- Everything.html | 887 +++++++++--------- index.html | 887 +++++++++--------- 13 files changed, 1210 insertions(+), 1171 deletions(-) create mode 100644 Categories.Adjoint.Instance.BaseChange.html create mode 100644 Categories.Adjoint.Instance.Slice.html create mode 100644 Categories.Functor.Slice.BaseChange.html diff --git a/Categories.Adjoint.AFT.html b/Categories.Adjoint.AFT.html index 8fa5dec63..9903d350a 100644 --- a/Categories.Adjoint.AFT.html +++ b/Categories.Adjoint.AFT.html @@ -72,7 +72,7 @@ private module _ X where X↙R : Category (C.o-level ⊔ D.ℓ-level) (C.ℓ-level ⊔ D.e-level) C.e-level - X↙R = X ↙ R + X↙R = X ↙ R module X↙R = Category X↙R s′ : SolutionSet X↙R @@ -99,7 +99,7 @@ module F = Functor F F′ : Functor J C - F′ = Cod _ _ ∘F F + F′ = Cod _ _ ∘F F LimF′ : Limit F′ LimF′ = Com F′ @@ -149,7 +149,7 @@ } K-conv : Cone F → Cone F′ - K-conv = F-map-Coneˡ (Cod _ _) + K-conv = F-map-Coneˡ (Cod _ _) K-conv′ : Cone F → Cone (R ∘F F′) K-conv′ K = F-map-Coneˡ R (K-conv K) @@ -195,7 +195,7 @@ solutionSet′⇒universalMorphism : UniversalMorphism X R solutionSet′⇒universalMorphism = record - { initial = SolutionSet⇒Initial {o′ = 0ℓ} {0ℓ} {0ℓ} {C = X ↙ R} complete s′ + { initial = SolutionSet⇒Initial {o′ = 0ℓ} {0ℓ} {0ℓ} {C = X ↙ R} complete s′ } solutionSet⇒adjoint : Σ (Functor D C) (λ L → L ⊣ R) diff --git a/Categories.Adjoint.Instance.BaseChange.html b/Categories.Adjoint.Instance.BaseChange.html new file mode 100644 index 000000000..cfeb1cb6d --- /dev/null +++ b/Categories.Adjoint.Instance.BaseChange.html @@ -0,0 +1,23 @@ + +Categories.Adjoint.Instance.BaseChange
{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+
+module Categories.Adjoint.Instance.BaseChange {o ℓ e} (C : Category o ℓ e) where
+
+open import Categories.Adjoint using (_⊣_)
+open import Categories.Adjoint.Compose using (_∘⊣_)
+open import Categories.Adjoint.Instance.Slice using (Forgetful⊣Free)
+open import Categories.Category.Slice C using (Slice)
+open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice≃slice)
+open import Categories.Category.Equivalence.Properties using (module C≅D)
+open import Categories.Diagram.Pullback C using (Pullback)
+open import Categories.Functor.Slice.BaseChange C using (BaseChange!; BaseChange*)
+
+open Category C
+
+module _ {A B : Obj} (f : B ⇒ A) (pullback : ∀ {C} {h : C ⇒ A} → Pullback f h) where
+
+  !⊣* : BaseChange! f ⊣ BaseChange* f pullback
+  !⊣* = C≅D.L⊣R (slice-slice≃slice f) ∘⊣ Forgetful⊣Free (Slice A) (pullback⇒product pullback)
+
\ No newline at end of file diff --git a/Categories.Adjoint.Instance.Slice.html b/Categories.Adjoint.Instance.Slice.html new file mode 100644 index 000000000..57d3eec6f --- /dev/null +++ b/Categories.Adjoint.Instance.Slice.html @@ -0,0 +1,48 @@ + +Categories.Adjoint.Instance.Slice
{-# OPTIONS --safe --without-K #-}
+
+open import Categories.Category using (Category)
+
+module Categories.Adjoint.Instance.Slice {o ℓ e} (C : Category o ℓ e) where
+
+open import Categories.Adjoint using (_⊣_)
+open import Categories.Category.Slice C using (SliceObj; Slice⇒; slicearr)
+open import Categories.Functor.Slice C using (Forgetful; Free)
+open import Categories.NaturalTransformation using (ntHelper)
+open import Categories.Object.Product C
+
+open Category C
+open HomReasoning
+
+open SliceObj
+open Slice⇒
+
+module _ {A : Obj} (product : ∀ {X} → Product A X) where
+
+  private
+    module product {X} = Product (product {X})
+    open product
+
+  Forgetful⊣Free : Forgetful ⊣ Free product
+  Forgetful⊣Free = record
+    { unit = ntHelper record
+      { η = λ _ → slicearr project₁
+      ; commute = λ {X} {Y} f → begin
+        ⟨ arr Y , id ⟩ ∘ h f                            ≈⟨ ∘-distribʳ-⟨⟩ ⟩
+        ⟨ arr Y ∘ h f , id ∘ h f ⟩                      ≈⟨ ⟨⟩-cong₂ (△ f) identityˡ ⟩
+        ⟨ arr X , h f ⟩                                 ≈˘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩
+        ⟨ id ∘ arr X , h f ∘ id ⟩                       ≈˘⟨ [ product ⇒ product ]×∘⟨⟩ ⟩
+        [ product ⇒ product ] id × h f ∘ ⟨ arr X , id ⟩ ∎
+      }
+    ; counit = ntHelper record
+      { η = λ _ → π₂
+      ; commute = λ _ → project₂
+      }
+    ; zig = project₂
+    ; zag = begin
+      [ product ⇒ product ]id× π₂ ∘ ⟨ π₁ , id ⟩ ≈⟨ [ product ⇒ product ]×∘⟨⟩ ⟩
+      ⟨ id ∘ π₁ , π₂ ∘ id ⟩                     ≈⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩
+      ⟨ π₁ , π₂ ⟩                               ≈⟨ η ⟩
+      id                                        ∎
+    }
+
\ No newline at end of file diff --git a/Categories.Adjoint.Properties.html b/Categories.Adjoint.Properties.html index dfd4bf341..9e698574e 100644 --- a/Categories.Adjoint.Properties.html +++ b/Categories.Adjoint.Properties.html @@ -12,7 +12,7 @@ open import Categories.Adjoint.RAPL using (rapl) open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) open import Categories.Category.Product using (_⁂_; _⁂ⁿⁱ_) -open import Categories.Category.Construction.Comma using (CommaObj; Comma⇒; _↙_) +open import Categories.Category.Construction.Comma using (CommaObj; Comma⇒; _↙_) open import Categories.Diagram.Limit using (Limit) open import Categories.Diagram.Colimit using (Colimit) open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) @@ -300,7 +300,7 @@ commaObj∘g : ∀ {X Y} → X C.⇒ Y → CommaObj (const! X) R commaObj∘g {X} {Y} g = record { f = f (umors.⊥ Y) C.∘ g } - ⊥X⇒⊥Y : ∀ {X Y} (g : X C.⇒ Y) → (X ↙ R) [ umors.⊥ X , commaObj∘g g ] + ⊥X⇒⊥Y : ∀ {X Y} (g : X C.⇒ Y) → (X ↙ R) [ umors.⊥ X , commaObj∘g g ] ⊥X⇒⊥Y {X} {Y} g = umors.! X {commaObj∘g g} L₀ : ∀ X → D.Obj @@ -337,7 +337,7 @@ ⊥Rd : (d : D.Obj) → CommaObj (const! (R.F₀ d)) R ⊥Rd d = umors.⊥ (R.F₀ d) - ⊥Rd⇒id : (d : D.Obj) → (R.F₀ d ↙ R) [ ⊥Rd d , record { f = C.id } ] + ⊥Rd⇒id : (d : D.Obj) → (R.F₀ d ↙ R) [ ⊥Rd d , record { f = C.id } ] ⊥Rd⇒id d = umors.! (R.F₀ d) {record { f = C.id }} ε : ∀ d → L₀ (R.F₀ d) D.⇒ d ε d = h (⊥Rd⇒id d) diff --git a/Categories.Category.CartesianClosed.Locally.Properties.html b/Categories.Category.CartesianClosed.Locally.Properties.html index 36fb7c759..9d7ac736b 100644 --- a/Categories.Category.CartesianClosed.Locally.Properties.html +++ b/Categories.Category.CartesianClosed.Locally.Properties.html @@ -38,10 +38,10 @@ J = slice⇒slice-slice C f I : Functor (Slice C/B (fObj ^ fObj)) C/B - I = pullback-functorial C/B slice-pullbacks i + I = pullback-functorial C/B slice-pullbacks i K : Functor C/B/f (Slice C/B (fObj ^ fObj)) - K = Base-F C/B (fObj ⇨-) + K = Base-F C/B (fObj ⇨-) -- this functor should be the right adjoint functor of (BaseChange* C pullbacks f). BaseChange⁎ : Functor C/A C/B diff --git a/Categories.Category.Construction.Comma.html b/Categories.Category.Construction.Comma.html index ae0475a38..9f7ad9648 100644 --- a/Categories.Category.Construction.Comma.html +++ b/Categories.Category.Construction.Comma.html @@ -44,98 +44,98 @@ h : B [ β₁ , β₂ ] commute : CommutativeSquare f₁ (T₁ g) (S₁ h) f₂ - Comma : Functor A C → Functor B C → Category _ _ _ - Comma T S = record - { Obj = CommaObj T S - ; _⇒_ = Comma⇒ - ; _≈_ = λ a₁ a₂ → g a₁ A.≈ g a₂ × h a₁ B.≈ h a₂ - ; _∘_ = _∘′_ - ; id = record { g = A.id ; h = B.id ; commute = id-comm } - ; assoc = A.assoc , B.assoc - ; sym-assoc = A.sym-assoc , B.sym-assoc - ; identityˡ = A.identityˡ , B.identityˡ - ; identityʳ = A.identityʳ , B.identityʳ - ; identity² = A.identity² , B.identity² - ; equiv = record - { refl = A.Equiv.refl , B.Equiv.refl - ; sym = map A.Equiv.sym B.Equiv.sym - ; trans = zip A.Equiv.trans B.Equiv.trans - } - ; ∘-resp-≈ = zip A.∘-resp-≈ B.∘-resp-≈ - } module Comma - where - module T = Functor T - module S = Functor S - - open T using () renaming (F₀ to T₀; F₁ to T₁) - open S using () renaming (F₀ to S₀; F₁ to S₁) - open Comma⇒ - id-comm : {E : CommaObj T S} → let open CommaObj E in - S₁ B.id C.∘ f C.≈ f C.∘ T₁ A.id - id-comm {E} = begin - S₁ B.id C.∘ f ≈⟨ elimˡ S.identity ⟩ - f ≈⟨ introʳ T.identity ⟩ - f C.∘ T₁ A.id ∎ - where - open C.HomReasoning - open CommaObj E - open MR C - - _∘′_ : ∀ {X₁ X₂ X₃} → Comma⇒ X₂ X₃ → Comma⇒ X₁ X₂ → Comma⇒ X₁ X₃ - _∘′_ {X₁} {X₂} {X₃} a₁ a₂ = record - { g = A [ g₁ ∘ g₂ ] - ; h = B [ h₁ ∘ h₂ ] - ; commute = begin - S₁ (h₁ B.∘ h₂) C.∘ f₁ ≈⟨ S.homomorphism ⟩∘⟨refl ⟩ - (S₁ h₁ C.∘ S₁ h₂) C.∘ f₁ ≈⟨ glue commutes₁ commutes₂ ⟩ - f₃ C.∘ (T₁ g₁ C.∘ T₁ g₂) ≈˘⟨ refl⟩∘⟨ T.homomorphism ⟩ - f₃ C.∘ T₁ (g₁ A.∘ g₂) ∎ - } - where - open C.HomReasoning - open MR C - open Comma⇒ a₁ renaming (g to g₁; h to h₁; commute to commutes₁) - open Comma⇒ a₂ renaming (g to g₂; h to h₂; commute to commutes₂) - open CommaObj X₁ renaming (f to f₁) - open CommaObj X₂ renaming (f to f₂) - open CommaObj X₃ renaming (f to f₃) - - infix 4 _↓_ - _↓_ : (S : Functor A C) (T : Functor B C) → Category _ _ _ - S ↓ T = Comma S T - - Dom : (T : Functor A C) → (S : Functor B C) → Functor (Comma T S) A - Dom T S = record - { F₀ = CommaObj.α - ; F₁ = Comma⇒.g - ; identity = refl - ; homomorphism = refl - ; F-resp-≈ = proj₁ - } - where - open Comma T S - open A.Equiv - - Cod : (T : Functor A C) → (S : Functor B C) → Functor (Comma T S) B - Cod T S = record - { F₀ = CommaObj.β - ; F₁ = Comma⇒.h - ; identity = refl - ; homomorphism = refl - ; F-resp-≈ = proj₂ - } - where - open Comma T S - open B.Equiv - -module _ {C : Category o₁ ℓ₁ e₁} {D : Category o₂ ℓ₂ e₂} where - private - module C = Category C - - infix 4 _↙_ _↘_ - _↙_ : (X : C.Obj) (T : Functor D C) → Category _ _ _ - X ↙ T = const! X ↓ T - - _↘_ : (S : Functor D C) (X : C.Obj) → Category _ _ _ - S ↘ X = S ↓ const! X + Comma : Functor A C → Functor B C → Category (o₁ ⊔ o₂ ⊔ ℓ₃) (ℓ₁ ⊔ ℓ₂ ⊔ e₃) (e₁ ⊔ e₂) + Comma T S = record + { Obj = CommaObj T S + ; _⇒_ = Comma⇒ + ; _≈_ = λ a₁ a₂ → g a₁ A.≈ g a₂ × h a₁ B.≈ h a₂ + ; _∘_ = _∘′_ + ; id = record { g = A.id ; h = B.id ; commute = id-comm } + ; assoc = A.assoc , B.assoc + ; sym-assoc = A.sym-assoc , B.sym-assoc + ; identityˡ = A.identityˡ , B.identityˡ + ; identityʳ = A.identityʳ , B.identityʳ + ; identity² = A.identity² , B.identity² + ; equiv = record + { refl = A.Equiv.refl , B.Equiv.refl + ; sym = map A.Equiv.sym B.Equiv.sym + ; trans = zip A.Equiv.trans B.Equiv.trans + } + ; ∘-resp-≈ = zip A.∘-resp-≈ B.∘-resp-≈ + } module Comma + where + module T = Functor T + module S = Functor S + + open T using () renaming (F₀ to T₀; F₁ to T₁) + open S using () renaming (F₀ to S₀; F₁ to S₁) + open Comma⇒ + id-comm : {E : CommaObj T S} → let open CommaObj E in + S₁ B.id C.∘ f C.≈ f C.∘ T₁ A.id + id-comm {E} = begin + S₁ B.id C.∘ f ≈⟨ elimˡ S.identity ⟩ + f ≈⟨ introʳ T.identity ⟩ + f C.∘ T₁ A.id ∎ + where + open C.HomReasoning + open CommaObj E + open MR C + + _∘′_ : ∀ {X₁ X₂ X₃} → Comma⇒ X₂ X₃ → Comma⇒ X₁ X₂ → Comma⇒ X₁ X₃ + _∘′_ {X₁} {X₂} {X₃} a₁ a₂ = record + { g = A [ g₁ ∘ g₂ ] + ; h = B [ h₁ ∘ h₂ ] + ; commute = begin + S₁ (h₁ B.∘ h₂) C.∘ f₁ ≈⟨ S.homomorphism ⟩∘⟨refl ⟩ + (S₁ h₁ C.∘ S₁ h₂) C.∘ f₁ ≈⟨ glue commutes₁ commutes₂ ⟩ + f₃ C.∘ (T₁ g₁ C.∘ T₁ g₂) ≈˘⟨ refl⟩∘⟨ T.homomorphism ⟩ + f₃ C.∘ T₁ (g₁ A.∘ g₂) ∎ + } + where + open C.HomReasoning + open MR C + open Comma⇒ a₁ renaming (g to g₁; h to h₁; commute to commutes₁) + open Comma⇒ a₂ renaming (g to g₂; h to h₂; commute to commutes₂) + open CommaObj X₁ renaming (f to f₁) + open CommaObj X₂ renaming (f to f₂) + open CommaObj X₃ renaming (f to f₃) + + infix 4 _↓_ + _↓_ : (S : Functor A C) (T : Functor B C) → Category _ _ _ + S ↓ T = Comma S T + + Dom : (T : Functor A C) → (S : Functor B C) → Functor (Comma T S) A + Dom T S = record + { F₀ = CommaObj.α + ; F₁ = Comma⇒.g + ; identity = refl + ; homomorphism = refl + ; F-resp-≈ = proj₁ + } + where + open Comma T S + open A.Equiv + + Cod : (T : Functor A C) → (S : Functor B C) → Functor (Comma T S) B + Cod T S = record + { F₀ = CommaObj.β + ; F₁ = Comma⇒.h + ; identity = refl + ; homomorphism = refl + ; F-resp-≈ = proj₂ + } + where + open Comma T S + open B.Equiv + +module _ {C : Category o₁ ℓ₁ e₁} {D : Category o₂ ℓ₂ e₂} where + private + module C = Category C + + infix 4 _↙_ _↘_ + _↙_ : (X : C.Obj) (T : Functor D C) → Category (o₂ ⊔ ℓ₁) (ℓ₂ ⊔ e₁) e₂ + X ↙ T = const! X ↓ T + + _↘_ : (S : Functor D C) (X : C.Obj) → Category (o₂ ⊔ ℓ₁) (ℓ₂ ⊔ e₁) e₂ + S ↘ X = S ↓ const! X \ No newline at end of file diff --git a/Categories.Category.Construction.Properties.Comma.html b/Categories.Category.Construction.Properties.Comma.html index 8319d2dad..5b47ab6be 100644 --- a/Categories.Category.Construction.Properties.Comma.html +++ b/Categories.Category.Construction.Properties.Comma.html @@ -40,7 +40,7 @@ module S = Functor S module T = Functor T - S↓T⇒A×B : Functor (S ↓ T) (A × B) + S↓T⇒A×B : Functor (S ↓ T) (A × B) S↓T⇒A×B = record { F₀ = < β , α > ; F₁ = < h , g > @@ -49,7 +49,7 @@ ; F-resp-≈ = swap } - induced-nat : NaturalTransformation (S ∘F Dom S T) (T ∘F Cod S T) + induced-nat : NaturalTransformation (S ∘F Dom S T) (T ∘F Cod S T) induced-nat = record { η = f ; commute = λ i → C.Equiv.sym (commute i) @@ -61,7 +61,7 @@ module S′ = Functor S′ module T′ = Functor T′ - compose-F : Functor (S ∘F S′ ↓ T ∘F T′) (S ↓ T) + compose-F : Functor (S ∘F S′ ↓ T ∘F T′) (S ↓ T) compose-F = record { F₀ = λ X → record { f = f X @@ -80,7 +80,7 @@ private module S′ = Functor S′ - compose-Fˡ : Functor (S ∘F S′ ↓ T) (S ↓ T) + compose-Fˡ : Functor (S ∘F S′ ↓ T) (S ↓ T) compose-Fˡ = record { F₀ = λ X → record { f = f X @@ -99,7 +99,7 @@ private module T′ = Functor T′ - compose-Fʳ : Functor (S ↓ T ∘F T′) (S ↓ T) + compose-Fʳ : Functor (S ↓ T ∘F T′) (S ↓ T) compose-Fʳ = record { F₀ = λ X → record { f = f X @@ -128,7 +128,7 @@ open Reas C -- functors between Comma categories along natural transformations - along-nat : Functor (S ↓ T) (S′ ↓ T′) + along-nat : Functor (S ↓ T) (S′ ↓ T′) along-nat = record { F₀ = λ X → record { f = δ.η (β X) ∘ f X ∘ γ.η (α X) @@ -148,10 +148,10 @@ ; F-resp-≈ = λ eq → eq } - along-natʳ : ∀ {T T′ : Functor A C} (S : Functor B C) (δ : NaturalTransformation T T′) → Functor (S ↓ T) (S ↓ T′) + along-natʳ : ∀ {T T′ : Functor A C} (S : Functor B C) (δ : NaturalTransformation T T′) → Functor (S ↓ T) (S ↓ T′) along-natʳ S = along-nat idN - along-natˡ : ∀ {S S′ : Functor B C} (γ : NaturalTransformation S′ S) (T : Functor A C) → Functor (S ↓ T) (S′ ↓ T) + along-natˡ : ∀ {S S′ : Functor B C} (γ : NaturalTransformation S′ S) (T : Functor A C) → Functor (S ↓ T) (S′ ↓ T) along-natˡ γ T = along-nat γ idN -- There's an induced functor from Functors category to Functors over Comma categories @@ -164,7 +164,7 @@ open Reas C induced : {s₁ d₁ : Functor A C} {s₂ d₂ : Functor B C} → - ((Category.op [ A ⇒ C ] × [ B ⇒ C ]) [ (s₁ , s₂) , (d₁ , d₂) ]) → Functor (s₁ ↓ s₂) (d₁ ↓ d₂) + ((Category.op [ A ⇒ C ] × [ B ⇒ C ]) [ (s₁ , s₂) , (d₁ , d₂) ]) → Functor (s₁ ↓ s₂) (d₁ ↓ d₂) induced {s₁ = s₁} {d₁ = d₁} {s₂} {d₂} (m₁ , m₂) = record { F₀ = λ o → record { α = α o @@ -194,10 +194,10 @@ private module D = Category D - along-natˡ′ : ∀ {A B} (f : A D.⇒ B) → Functor (B ↙ F) (A ↙ F) + along-natˡ′ : ∀ {A B} (f : A D.⇒ B) → Functor (B ↙ F) (A ↙ F) along-natˡ′ f = along-natˡ (constNat f) F - along-natʳ′ : ∀ {A B} (f : A D.⇒ B) → Functor (F ↘ A) (F ↘ B) + along-natʳ′ : ∀ {A B} (f : A D.⇒ B) → Functor (F ↘ A) (F ↘ B) along-natʳ′ f = along-natʳ F (constNat f) module _ {C : Category o ℓ e} where @@ -211,7 +211,7 @@ open Comma⇒ open Reas C - slice⇒comma : ∀ X → Functor (Slice X) (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X) + slice⇒comma : ∀ X → Functor (Slice X) (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X) slice⇒comma X = record { F₀ = λ X → record { f = arr X } ; F₁ = λ f → record { commute = identityˡ ○ ⟺ (△ f) } @@ -220,7 +220,7 @@ ; F-resp-≈ = λ eq → eq , _ } - comma⇒slice : ∀ X → Functor (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X) (Slice X) + comma⇒slice : ∀ X → Functor (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X) (Slice X) comma⇒slice X = record { F₀ = λ X → Sl.sliceobj (f X) ; F₁ = λ g → Sl.slicearr (⟺ (commute g) ○ identityˡ) @@ -229,7 +229,7 @@ ; F-resp-≈ = proj₁ } - comma-slice-equiv : ∀ X → StrongEquivalence (Slice X) (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X) + comma-slice-equiv : ∀ X → StrongEquivalence (Slice X) (idF {C = C} ↓ const {C = One {o} {ℓ} {e}} X) comma-slice-equiv X = record { F = slice⇒comma X ; G = comma⇒slice X diff --git a/Categories.Diagram.Limit.Ran.html b/Categories.Diagram.Limit.Ran.html index c95dd50d5..ace5adeb0 100644 --- a/Categories.Diagram.Limit.Ran.html +++ b/Categories.Diagram.Limit.Ran.html @@ -42,14 +42,14 @@ open ConesCat.Cone⇒ using (arr) renaming (commute to ⇒-commute) open Mor E using (_≅_) - G : (d : D.Obj) → Functor (d ↙ F) E - G d = X ∘F Cod {A = One} {B = C} {C = D} (const! d) F + G : (d : D.Obj) → Functor (d ↙ F) E + G d = X ∘F Cod {A = One} {B = C} {C = D} (const! d) F ⊤Gd : (d : D.Obj) → Limit (G d) ⊤Gd d = Com (G d) module ⊤Gd d = Limit (⊤Gd d) using (proj; limit; rep; rep-cone; apex; module terminal) - f↙F : {Y Z : D.Obj} (f : Y D.⇒ Z) → Functor (Z ↙ F) (Y ↙ F) + f↙F : {Y Z : D.Obj} (f : Y D.⇒ Z) → Functor (Z ↙ F) (Y ↙ F) f↙F = along-natˡ′ F Gf≃ : {Y Z : D.Obj} (f : Y D.⇒ Z) → G Z ≃ G Y ∘F f↙F f @@ -132,7 +132,7 @@ } ConesGd : {d : D.Obj} → Functor (Comma {A = One} (const d) F) E - ConesGd {d} = X ∘F Cod {A = One} {B = C} {C = D} (const d) F + ConesGd {d} = X ∘F Cod {A = One} {B = C} {C = D} (const d) F R-identity : {d : D.Obj} → R₁ {d} D.id E.≈ E.id R-identity {d} = G.terminal.⊤-id ConeArr @@ -154,7 +154,7 @@ module ⊤GY = Cone (⊤Gd.limit Y) module H = Functor (f↙F (g D.∘ f)) using (₀; ₁) open E - cc : Cone (X ∘F Cod (const W) F) + cc : Cone (X ∘F Cod (const W) F) cc = record { N = ⊤GY.N; apex = record { ψ = λ K → ⊤GY.ψ (H.₀ K) ; commute = λ h → ⊤GY.commute (H.₁ h) @@ -180,12 +180,12 @@ open E module ⊤GY = Cone (⊤Gd.limit Y) module H = Functor (f↙F f) - cc : Cone (X ∘F Cod (const Z) F) + cc : Cone (X ∘F Cod (const Z) F) cc = record { apex = record { ψ = λ K → ⊤GY.ψ (H.F₀ K) ; commute = λ h → ⊤GY.commute (H.F₁ h) } } - F-resp-≈-commute : ∀ {Y Z} {K : Category.Obj (Z ↙ F)} {f g : Y D.⇒ Z} → f D.≈ g → + F-resp-≈-commute : ∀ {Y Z} {K : Category.Obj (Z ↙ F)} {f g : Y D.⇒ Z} → f D.≈ g → ⊤Gd.proj Z K ∘ R₁ f ≈ ⊤Gd.proj Y (↙⇒ K g) F-resp-≈-commute {Y} {Z} {K} {f} {g} eq = begin ⊤Gd.proj Z K ∘ R₁ f ≈⟨ proj-red K f ⟩ @@ -271,7 +271,7 @@ module γ = NaturalTransformation γ module δ-Cone d = Cone (δ-Cone d M γ) open CommaObj - cc : {Y Z : D.Obj} → Y D.⇒ Z → Cone (X ∘F Cod (const Z) F) + cc : {Y Z : D.Obj} → Y D.⇒ Z → Cone (X ∘F Cod (const Z) F) cc {_} {Z} f = record { apex = record { ψ = λ W → δ-Cone.ψ Z W E.∘ M.F₁ f @@ -302,7 +302,7 @@ module γ = NaturalTransformation γ using (η) module δ = NaturalTransformation δ′ using (η; commute) open CommaObj - C⇒ : Cone⇒ (X ∘F Cod (const d) F) (δ-Cone d M γ) (terminal.⊤ (⊤Gd d)) + C⇒ : Cone⇒ (X ∘F Cod (const d) F) (δ-Cone d M γ) (terminal.⊤ (⊤Gd d)) C⇒ = record { arr = δ.η d ; commute = λ {W} → begin diff --git a/Categories.Functor.Slice.BaseChange.html b/Categories.Functor.Slice.BaseChange.html new file mode 100644 index 000000000..b331799c5 --- /dev/null +++ b/Categories.Functor.Slice.BaseChange.html @@ -0,0 +1,26 @@ + +Categories.Functor.Slice.BaseChange
{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+
+module Categories.Functor.Slice.BaseChange {o ℓ e} (C : Category o ℓ e) where
+
+open import Categories.Category.Slice C using (Slice)
+open import Categories.Category.Slice.Properties C using (pullback⇒product; slice-slice⇒slice; slice⇒slice-slice)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Slice using (Forgetful; Free)
+open import Categories.Diagram.Pullback C using (Pullback)
+
+open Category C
+
+module _ {A B : Obj} (f : B ⇒ A) where
+
+  -- Any morphism induces a functor between slices.
+  BaseChange! : Functor (Slice B) (Slice A)
+  BaseChange! = Forgetful (Slice A) ∘F slice⇒slice-slice f
+
+  -- Any morphism which admits pullbacks induces a functor the other way between slices.
+  -- This is adjoint to BaseChange!: see Categories.Adjoint.Instance.BaseChange.
+  BaseChange* : (∀ {C} {h : C ⇒ A} → Pullback f h) → Functor (Slice A) (Slice B)
+  BaseChange* pullback = slice-slice⇒slice f ∘F Free (Slice A) (pullback⇒product pullback)
+
\ No newline at end of file diff --git a/Categories.Functor.Slice.html b/Categories.Functor.Slice.html index b99dadc2a..44e20e383 100644 --- a/Categories.Functor.Slice.html +++ b/Categories.Functor.Slice.html @@ -1,164 +1,100 @@ Categories.Functor.Slice
{-# OPTIONS --without-K --safe #-}
 
-open import Categories.Category
-
-module Categories.Functor.Slice {o ℓ e} (C : Category o ℓ e) where
-
-open import Data.Product using (_,_)
-
-open import Categories.Adjoint
-open import Categories.Category.CartesianClosed
-open import Categories.Category.CartesianClosed.Locally
-open import Categories.Functor hiding (id)
-open import Categories.Functor.Properties
-open import Categories.Morphism.Reasoning C
-open import Categories.NaturalTransformation hiding (id)
-open import Categories.Object.Product C
-
-import Categories.Category.Slice as S
-import Categories.Diagram.Pullback as P
-import Categories.Category.Construction.Pullbacks as Pbs
-
-open Category C
-open HomReasoning
-open Equiv
-
-module _ {A : Obj} where
-  open S.SliceObj
-  open S.Slice⇒
-
-  Base-F : ∀ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} (F : Functor C D) → Functor (S.Slice C A) (S.Slice D (Functor.F₀ F A))
-  Base-F {D = D} F = record
-    { F₀           = λ { (S.sliceobj arr) → S.sliceobj (F₁ arr) }
-    ; F₁           = λ { (S.slicearr △) → S.slicearr ([ F ]-resp-∘ △) }
-    ; identity     = identity
-    ; homomorphism = homomorphism
-    ; F-resp-≈     = F-resp-≈
-    }
-    where module D = Category D
-          open Functor F
-
-  open S C
-
-  Forgetful : Functor (Slice A) C
-  Forgetful = record
-    { F₀           = λ X → Y X
-    ; F₁           = λ f → h f
-    ; identity     = refl
-    ; homomorphism = refl
-    ; F-resp-≈     = λ eq → eq
-    }
-
-  BaseChange! : ∀ {B} (f : B ⇒ A) → Functor (Slice B) (Slice A)
-  BaseChange! f = record
-    { F₀           = λ X → sliceobj (f ∘ arr X)
-    ; F₁           = λ g → slicearr (pullʳ (△ g))
-    ; identity     = refl
-    ; homomorphism = refl
-    ; F-resp-≈     = λ eq → eq
-    }
-
-
-  module _ (pullbacks : ∀ {X Y Z} (h : X ⇒ Z) (i : Y ⇒ Z) → P.Pullback C h i) where
-    private
-      open P C
-      module pullbacks {X Y Z} h i = Pullback (pullbacks {X} {Y} {Z} h i)
-      open pullbacks
-
-    BaseChange* : ∀ {B} (f : B ⇒ A) → Functor (Slice A) (Slice B)
-    BaseChange* f = record
-      { F₀           = λ X → sliceobj (p₂ (arr X) f)
-      ; F₁           = λ {X Y} g → slicearr {h = Pullback.p₂ (unglue (pullbacks (arr Y) f)
-                                                                     (Pullback-resp-≈ (pullbacks (arr X) f) (△ g) refl))}
-                                            (p₂∘universal≈h₂ (arr Y) f)
-      ; identity     = λ {X} → ⟺ (unique (arr X) f id-comm identityʳ)
-      ; homomorphism = λ {X Y Z} {h i} → unique-diagram (arr Z) f (p₁∘universal≈h₁ (arr Z) f ○ assoc ○ ⟺ (pullʳ (p₁∘universal≈h₁ (arr Y) f)) ○ ⟺ (pullˡ (p₁∘universal≈h₁ (arr Z) f)))
-                                                                  (p₂∘universal≈h₂ (arr Z) f ○ ⟺ (p₂∘universal≈h₂ (arr Y) f) ○ ⟺ (pullˡ (p₂∘universal≈h₂ (arr Z) f)))
-      ; F-resp-≈     = λ {X Y} eq″ → unique (arr Y) f (p₁∘universal≈h₁ (arr Y) f ○ ∘-resp-≈ˡ eq″) (p₂∘universal≈h₂ (arr Y) f)
-      }
-
-
-    !⊣* : ∀ {B} (f : B ⇒ A) →  BaseChange! f ⊣ BaseChange* f
-    !⊣* f = record
-      { unit   = ntHelper record
-        { η       = λ X → slicearr (p₂∘universal≈h₂ (f ∘ arr X) f {eq = identityʳ})
-        ; commute = λ {X Y} g → unique-diagram (f ∘ arr Y) f
-                                               (cancelˡ (p₁∘universal≈h₁ (f ∘ arr Y) f) ○ ⟺ (cancelʳ (p₁∘universal≈h₁ (f ∘ arr X) f)) ○ pushˡ (⟺ (p₁∘universal≈h₁ (f ∘ arr Y) f)))
-                                               (pullˡ (p₂∘universal≈h₂ (f ∘ arr Y) f) ○ △ g ○ ⟺ (p₂∘universal≈h₂ (f ∘ arr X) f) ○ pushˡ (⟺ (p₂∘universal≈h₂ (f ∘ arr Y) f)))
-        }
-      ; counit = ntHelper record
-        { η       = λ X → slicearr (pullbacks.commute (arr X) f)
-        ; commute = λ {X Y} g → p₁∘universal≈h₁ (arr Y) f
-        }
-      ; zig    = λ {X} → p₁∘universal≈h₁ (f ∘ arr X) f
-      ; zag    = λ {Y} → unique-diagram (arr Y) f
-                                        (pullˡ (p₁∘universal≈h₁ (arr Y) f) ○ pullʳ (p₁∘universal≈h₁ (f ∘ pullbacks.p₂ (arr Y) f) f))
-                                        (pullˡ (p₂∘universal≈h₂ (arr Y) f) ○ p₂∘universal≈h₂ (f ∘ pullbacks.p₂ (arr Y) f) f ○ ⟺ identityʳ)
-      }
-
-    pullback-functorial : ∀ {B} (f : B ⇒ A) → Functor (Slice A) C
-    pullback-functorial f = record
-      { F₀           = λ X → p.P X
-      ; F₁           = λ f → p⇒ _ _ f
-      ; identity     = λ {X} → sym (p.unique X id-comm id-comm)
-      ; homomorphism = λ {_ Y Z} →
-        p.unique-diagram Z (p.p₁∘universal≈h₁ Z ○ ⟺ identityˡ ○ ⟺ (pullʳ (p.p₁∘universal≈h₁ Y)) ○ ⟺ (pullˡ (p.p₁∘universal≈h₁ Z)))
-                           (p.p₂∘universal≈h₂ Z ○ assoc ○ ⟺ (pullʳ (p.p₂∘universal≈h₂ Y)) ○ ⟺ (pullˡ (p.p₂∘universal≈h₂ Z)))
-      ; F-resp-≈     = λ {_ B} {h i} eq →
-        p.unique-diagram B (p.p₁∘universal≈h₁ B ○ ⟺ (p.p₁∘universal≈h₁ B))
-                           (p.p₂∘universal≈h₂ B ○ ∘-resp-≈ˡ eq ○ ⟺ (p.p₂∘universal≈h₂ B))
-      }
-      where p : ∀ X → Pullback f (arr X)
-            p X        = pullbacks f (arr X)
-            module p X = Pullback (p X)
-
-            p⇒ : ∀ X Y (g : Slice⇒ X Y) → p.P X ⇒ p.P Y
-            p⇒ X Y g = Pbs.Pullback⇒.pbarr pX⇒pY
-              where pX : Pbs.PullbackObj C A
-                    pX = record { pullback = p X }
-                    pY : Pbs.PullbackObj C A
-                    pY = record { pullback = p Y }
-                    pX⇒pY : Pbs.Pullback⇒ C A pX pY
-                    pX⇒pY = record
-                      { mor₁     = Category.id C
-                      ; mor₂     = h g
-                      ; commute₁ = identityʳ
-                      ; commute₂ = △ g
-                      }
-
-  module _ (product : {X : Obj} → Product A X) where
-
-    -- this is adapted from proposition 1.33 of Aspects of Topoi (Freyd, 1972)
-    Free : Functor C (Slice A)
-    Free = record
-      { F₀ = λ _ → sliceobj [ product ]π₁
-      ; F₁ = λ f → slicearr ([ product ⇒ product ]π₁∘× ○ identityˡ)
-      ; identity = id×id product
-      ; homomorphism = sym [ product ⇒ product ⇒ product ]id×∘id×
-      ; F-resp-≈ = λ f≈g → Product.⟨⟩-cong₂ product refl (∘-resp-≈ˡ f≈g)
-      }
-
-    Forgetful⊣Free : Forgetful ⊣ Free
-    Forgetful⊣Free = record
-      { unit = ntHelper record
-        { η = λ _ → slicearr (Product.project₁ product)
-        ; commute = λ {X} {Y} f → begin
-          [ product ]⟨ arr Y , id ⟩ ∘ h f                            ≈⟨ [ product ]⟨⟩∘ ⟩
-          [ product ]⟨ arr Y ∘ h f , id ∘ h f ⟩                      ≈⟨ Product.⟨⟩-cong₂ product (△ f) identityˡ ⟩
-          [ product ]⟨ arr X , h f ⟩                                 ≈˘⟨ Product.⟨⟩-cong₂ product identityˡ identityʳ ⟩
-          [ product ]⟨ id ∘ arr X , h f ∘ id ⟩                       ≈˘⟨ [ product ⇒ product ]×∘⟨⟩ ⟩
-          [ product ⇒ product ] id × h f ∘ [ product ]⟨ arr X , id ⟩ ∎
-        }
-      ; counit = ntHelper record
-        { η = λ _ → Product.π₂ product
-        ; commute = λ _ → Product.project₂ product
-        }
-      ; zig = Product.project₂ product
-      ; zag = begin
-        [ product ⇒ product ]id× [ product ]π₂ ∘ [ product ]⟨ [ product ]π₁ , id ⟩ ≈⟨ [ product ⇒ product ]×∘⟨⟩ ⟩
-        [ product ]⟨ id ∘ [ product ]π₁ , [ product ]π₂ ∘ id ⟩                     ≈⟨ Product.⟨⟩-cong₂ product identityˡ identityʳ ⟩
-        [ product ]⟨ [ product ]π₁ , [ product ]π₂ ⟩                               ≈⟨ Product.η product ⟩
-        id                                                                         ∎
-      }
+open import Categories.Category using (Category)
+
+module Categories.Functor.Slice {o ℓ e} (C : Category o ℓ e) where
+
+open import Function using () renaming (id to id→)
+
+open import Categories.Diagram.Pullback C using (Pullback; unglue; Pullback-resp-≈)
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Properties using ([_]-resp-∘)
+open import Categories.Morphism.Reasoning C
+open import Categories.Object.Product C
+
+import Categories.Category.Slice as S
+import Categories.Category.Construction.Pullbacks as Pbs
+
+open Category C
+open HomReasoning
+open Equiv
+
+module _ {A : Obj} where
+  open S.SliceObj
+  open S.Slice⇒
+
+  -- A functor between categories induces one between the corresponding slices at a given object of C.
+  Base-F : ∀ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} (F : Functor C D) → Functor (S.Slice C A) (S.Slice D (Functor.F₀ F A))
+  Base-F F = record
+    { F₀           = λ s → S.sliceobj (F₁ (arr s))
+    ; F₁           = λ s⇒ → S.slicearr ([ F ]-resp-∘ (△ s⇒))
+    ; identity     = identity
+    ; homomorphism = homomorphism
+    ; F-resp-≈     = F-resp-≈
+    }
+    where open Functor F
+
+  open S C
+
+  Forgetful : Functor (Slice A) C
+  Forgetful = record
+    { F₀           = Y
+    ; F₁           = h
+    ; identity     = refl
+    ; homomorphism = refl
+    ; F-resp-≈     = id→
+    }
+
+  module _ (pullback : ∀ {X} {Y} {Z} (h : X ⇒ Z) (i : Y ⇒ Z) → Pullback h i) where
+    private
+      module pullbacks {X Y Z} h i = Pullback (pullback {X} {Y} {Z} h i)
+      open pullbacks using (p₂; p₂∘universal≈h₂; unique; unique-diagram; p₁∘universal≈h₁)
+
+    pullback-functorial : ∀ {B} (f : B ⇒ A) → Functor (Slice A) C
+    pullback-functorial f = record
+      { F₀           = λ X → p.P X
+      ; F₁           = λ f → p⇒ _ _ f
+      ; identity     = λ {X} → sym (p.unique X id-comm id-comm)
+      ; homomorphism = λ {_ Y Z} →
+        p.unique-diagram Z (p.p₁∘universal≈h₁ Z ○ ⟺ identityˡ ○ ⟺ (pullʳ (p.p₁∘universal≈h₁ Y)) ○ ⟺ (pullˡ (p.p₁∘universal≈h₁ Z)))
+                           (p.p₂∘universal≈h₂ Z ○ assoc ○ ⟺ (pullʳ (p.p₂∘universal≈h₂ Y)) ○ ⟺ (pullˡ (p.p₂∘universal≈h₂ Z)))
+      ; F-resp-≈     = λ {_ B} {h i} eq →
+        p.unique-diagram B (p.p₁∘universal≈h₁ B ○ ⟺ (p.p₁∘universal≈h₁ B))
+                           (p.p₂∘universal≈h₂ B ○ ∘-resp-≈ˡ eq ○ ⟺ (p.p₂∘universal≈h₂ B))
+      }
+      where p : ∀ X → Pullback f (arr X)
+            p X        = pullback f (arr X)
+            module p X = Pullback (p X)
+
+            p⇒ : ∀ X Y (g : Slice⇒ X Y) → p.P X ⇒ p.P Y
+            p⇒ X Y g = Pbs.Pullback⇒.pbarr pX⇒pY
+              where pX : Pbs.PullbackObj C A
+                    pX = record { pullback = p X }
+                    pY : Pbs.PullbackObj C A
+                    pY = record { pullback = p Y }
+                    pX⇒pY : Pbs.Pullback⇒ C A pX pY
+                    pX⇒pY = record
+                      { mor₁     = Category.id C
+                      ; mor₂     = h g
+                      ; commute₁ = identityʳ
+                      ; commute₂ = △ g
+                      }
+
+  module _ (product : {X : Obj} → Product A X) where
+
+    private
+      module product {X} = Product (product {X})
+      open product
+
+    -- this is adapted from proposition 1.33 of Aspects of Topoi (Freyd, 1972)
+    Free : Functor C (Slice A)
+    Free = record
+      { F₀ = λ _ → sliceobj π₁
+      ; F₁ = λ f → slicearr ([ product ⇒ product ]π₁∘× ○ identityˡ)
+      ; identity = id×id product
+      ; homomorphism = sym [ product ⇒ product ⇒ product ]id×∘id×
+      ; F-resp-≈ = λ f≈g → ⟨⟩-cong₂ refl (∘-resp-≈ˡ f≈g)
+      }
+
\ No newline at end of file diff --git a/Categories.Morphism.Universal.html b/Categories.Morphism.Universal.html index 177743ea2..17f58c156 100644 --- a/Categories.Morphism.Universal.html +++ b/Categories.Morphism.Universal.html @@ -12,7 +12,7 @@ record UniversalMorphism {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (X : Category.Obj C) (F : Functor D C) : Set (e ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′) where X↙F : Category _ _ _ - X↙F = X ↙ F + X↙F = X ↙ F private module X↙F = Category X↙F diff --git a/Everything.html b/Everything.html index 5dca025c4..c453864c7 100644 --- a/Everything.html +++ b/Everything.html @@ -15,446 +15,449 @@ import Categories.Adjoint.Equivalents import Categories.Adjoint.Instance.0-Truncation import Categories.Adjoint.Instance.01-Truncation -import Categories.Adjoint.Instance.Core -import Categories.Adjoint.Instance.PathsOf -import Categories.Adjoint.Instance.PosetCore -import Categories.Adjoint.Instance.StrictCore -import Categories.Adjoint.Instance.StrictDiscrete -import Categories.Adjoint.Mate -import Categories.Adjoint.Monadic -import Categories.Adjoint.Monadic.Crude -import Categories.Adjoint.Monadic.Properties -import Categories.Adjoint.Parametric -import Categories.Adjoint.Properties -import Categories.Adjoint.RAPL -import Categories.Adjoint.Relative -import Categories.Adjoint.TwoSided -import Categories.Adjoint.TwoSided.Compose -import Categories.Bicategory -import Categories.Bicategory.Bigroupoid -import Categories.Bicategory.Construction.1-Category -import Categories.Bicategory.Construction.LaxSlice -import Categories.Bicategory.Construction.Spans -import Categories.Bicategory.Construction.Spans.Properties -import Categories.Bicategory.Extras -import Categories.Bicategory.Instance.Cats -import Categories.Bicategory.Instance.EnrichedCats -import Categories.Bicategory.Monad -import Categories.Bicategory.Monad.Properties -import Categories.Bicategory.Object.Product -import Categories.Bicategory.Object.Terminal -import Categories.Bicategory.Opposite -import Categories.Category -import Categories.Category.BicartesianClosed -import Categories.Category.BinaryProducts -import Categories.Category.CMonoidEnriched -import Categories.Category.Cartesian -import Categories.Category.Cartesian.Bundle -import Categories.Category.Cartesian.Monoidal -import Categories.Category.Cartesian.Properties -import Categories.Category.Cartesian.SymmetricMonoidal -import Categories.Category.CartesianClosed -import Categories.Category.CartesianClosed.Bundle -import Categories.Category.CartesianClosed.Canonical -import Categories.Category.CartesianClosed.Locally -import Categories.Category.CartesianClosed.Locally.Properties -import Categories.Category.CartesianClosed.Properties -import Categories.Category.Closed -import Categories.Category.Cocartesian -import Categories.Category.Cocartesian.Bundle -import Categories.Category.Cocomplete -import Categories.Category.Cocomplete.Finitely -import Categories.Category.Cocomplete.Finitely.Properties -import Categories.Category.Cocomplete.Properties -import Categories.Category.Complete -import Categories.Category.Complete.Finitely -import Categories.Category.Complete.Finitely.Properties -import Categories.Category.Complete.Properties -import Categories.Category.Complete.Properties.Construction -import Categories.Category.Complete.Properties.SolutionSet -import Categories.Category.Concrete -import Categories.Category.Concrete.Properties -import Categories.Category.Construction.0-Groupoid -import Categories.Category.Construction.Adjoints -import Categories.Category.Construction.Arrow -import Categories.Category.Construction.CoEilenbergMoore -import Categories.Category.Construction.CoKleisli -import Categories.Category.Construction.Cocones -import Categories.Category.Construction.Comma -import Categories.Category.Construction.Cones -import Categories.Category.Construction.Coproduct -import Categories.Category.Construction.Core -import Categories.Category.Construction.Cowedges -import Categories.Category.Construction.EilenbergMoore -import Categories.Category.Construction.Elements -import Categories.Category.Construction.EnrichedFunctors -import Categories.Category.Construction.F-Algebras -import Categories.Category.Construction.F-Coalgebras -import Categories.Category.Construction.Fin -import Categories.Category.Construction.Functors -import Categories.Category.Construction.Grothendieck -import Categories.Category.Construction.GroupAsCategory -import Categories.Category.Construction.Groups -import Categories.Category.Construction.KanComplex -import Categories.Category.Construction.KaroubiEnvelope -import Categories.Category.Construction.KaroubiEnvelope.Properties -import Categories.Category.Construction.Kleisli -import Categories.Category.Construction.LT-Models -import Categories.Category.Construction.MonoidAsCategory -import Categories.Category.Construction.MonoidalFunctors -import Categories.Category.Construction.Monoids -import Categories.Category.Construction.ObjectRestriction -import Categories.Category.Construction.Path -import Categories.Category.Construction.PathCategory -import Categories.Category.Construction.Presheaves -import Categories.Category.Construction.Properties.CoEilenbergMoore -import Categories.Category.Construction.Properties.CoKleisli -import Categories.Category.Construction.Properties.Comma -import Categories.Category.Construction.Properties.EilenbergMoore -import Categories.Category.Construction.Properties.Functors -import Categories.Category.Construction.Properties.Kleisli -import Categories.Category.Construction.Properties.Presheaves -import Categories.Category.Construction.Properties.Presheaves.Cartesian -import Categories.Category.Construction.Properties.Presheaves.CartesianClosed -import Categories.Category.Construction.Properties.Presheaves.Complete -import Categories.Category.Construction.Properties.Presheaves.FromCartesianCCC -import Categories.Category.Construction.Pullbacks -import Categories.Category.Construction.SetoidDiscrete -import Categories.Category.Construction.Spans -import Categories.Category.Construction.StrictDiscrete -import Categories.Category.Construction.SymmetricMonoidalFunctors -import Categories.Category.Construction.Thin -import Categories.Category.Construction.TwistedArrow -import Categories.Category.Construction.Wedges -import Categories.Category.Construction.mu-Bialgebras -import Categories.Category.Core -import Categories.Category.Dagger -import Categories.Category.Dagger.Construction.Discrete -import Categories.Category.Dagger.Instance.Rels -import Categories.Category.Diagram.Span -import Categories.Category.Discrete -import Categories.Category.Distributive -import Categories.Category.Duality -import Categories.Category.Equivalence -import Categories.Category.Equivalence.Preserves -import Categories.Category.Equivalence.Properties -import Categories.Category.Exact -import Categories.Category.Extensive -import Categories.Category.Extensive.Bundle -import Categories.Category.Extensive.Properties.Distributive -import Categories.Category.Finite -import Categories.Category.Finite.Fin -import Categories.Category.Finite.Fin.Construction.Discrete -import Categories.Category.Finite.Fin.Construction.Poset -import Categories.Category.Finite.Fin.Instance.Parallel -import Categories.Category.Finite.Fin.Instance.Span -import Categories.Category.Finite.Fin.Instance.Triangle -import Categories.Category.Groupoid -import Categories.Category.Groupoid.Properties -import Categories.Category.Helper -import Categories.Category.Indiscrete -import Categories.Category.Instance.Cartesians -import Categories.Category.Instance.Cats -import Categories.Category.Instance.EmptySet -import Categories.Category.Instance.FamilyOfSetoids -import Categories.Category.Instance.FinCatShapes -import Categories.Category.Instance.FinSetoids -import Categories.Category.Instance.Globe -import Categories.Category.Instance.Groupoids -import Categories.Category.Instance.KanComplexes -import Categories.Category.Instance.LawvereTheories -import Categories.Category.Instance.Monoidals -import Categories.Category.Instance.Nat -import Categories.Category.Instance.One -import Categories.Category.Instance.PartialFunctions -import Categories.Category.Instance.PointedSets -import Categories.Category.Instance.Posets -import Categories.Category.Instance.Preds -import Categories.Category.Instance.Properties.Cats -import Categories.Category.Instance.Properties.Posets -import Categories.Category.Instance.Properties.Setoids -import Categories.Category.Instance.Properties.Setoids.CCC -import Categories.Category.Instance.Properties.Setoids.Choice -import Categories.Category.Instance.Properties.Setoids.Cocomplete -import Categories.Category.Instance.Properties.Setoids.Complete -import Categories.Category.Instance.Properties.Setoids.Exact -import Categories.Category.Instance.Properties.Setoids.Extensive -import Categories.Category.Instance.Properties.Setoids.LCCC -import Categories.Category.Instance.Properties.Setoids.Limits.Canonical -import Categories.Category.Instance.Quivers -import Categories.Category.Instance.Rels -import Categories.Category.Instance.Setoids -import Categories.Category.Instance.Sets -import Categories.Category.Instance.Simplex -import Categories.Category.Instance.SimplicialSet -import Categories.Category.Instance.SimplicialSet.Properties -import Categories.Category.Instance.SingletonSet -import Categories.Category.Instance.Span -import Categories.Category.Instance.StrictCats -import Categories.Category.Instance.StrictGroupoids -import Categories.Category.Instance.Zero -import Categories.Category.Inverse -import Categories.Category.Lift -import Categories.Category.Monoidal -import Categories.Category.Monoidal.Braided -import Categories.Category.Monoidal.Braided.Properties -import Categories.Category.Monoidal.Bundle -import Categories.Category.Monoidal.Closed -import Categories.Category.Monoidal.Closed.IsClosed -import Categories.Category.Monoidal.Closed.IsClosed.Diagonal -import Categories.Category.Monoidal.Closed.IsClosed.Dinatural -import Categories.Category.Monoidal.Closed.IsClosed.Identity -import Categories.Category.Monoidal.Closed.IsClosed.L -import Categories.Category.Monoidal.Closed.IsClosed.Pentagon -import Categories.Category.Monoidal.CompactClosed -import Categories.Category.Monoidal.Construction.Endofunctors -import Categories.Category.Monoidal.Construction.Minus2 -import Categories.Category.Monoidal.Construction.Product -import Categories.Category.Monoidal.Core -import Categories.Category.Monoidal.Instance.Cats -import Categories.Category.Monoidal.Instance.One -import Categories.Category.Monoidal.Instance.Rels -import Categories.Category.Monoidal.Instance.Setoids -import Categories.Category.Monoidal.Instance.Sets -import Categories.Category.Monoidal.Instance.StrictCats -import Categories.Category.Monoidal.Interchange -import Categories.Category.Monoidal.Interchange.Braided -import Categories.Category.Monoidal.Interchange.Symmetric -import Categories.Category.Monoidal.Properties -import Categories.Category.Monoidal.Reasoning -import Categories.Category.Monoidal.Rigid -import Categories.Category.Monoidal.Star-Autonomous -import Categories.Category.Monoidal.Symmetric -import Categories.Category.Monoidal.Traced -import Categories.Category.Monoidal.Utilities -import Categories.Category.Product -import Categories.Category.Product.Properties -import Categories.Category.Regular -import Categories.Category.Restriction -import Categories.Category.Restriction.Construction.Trivial -import Categories.Category.Restriction.Instance.PartialFunctions -import Categories.Category.Restriction.Properties -import Categories.Category.RigCategory -import Categories.Category.Site -import Categories.Category.Slice -import Categories.Category.Slice.Properties -import Categories.Category.Species -import Categories.Category.Species.Constructions -import Categories.Category.SubCategory -import Categories.Category.Topos -import Categories.Category.Unbundled -import Categories.Category.Unbundled.Properties -import Categories.Category.Unbundled.Utilities -import Categories.CoYoneda -import Categories.Comonad -import Categories.Comonad.Construction.CoKleisli -import Categories.Comonad.Relative -import Categories.Diagram.Cocone -import Categories.Diagram.Cocone.Properties -import Categories.Diagram.Coend -import Categories.Diagram.Coend.Properties -import Categories.Diagram.Coequalizer -import Categories.Diagram.Coequalizer.Properties -import Categories.Diagram.Colimit -import Categories.Diagram.Colimit.DualProperties -import Categories.Diagram.Colimit.Lan -import Categories.Diagram.Colimit.Properties -import Categories.Diagram.Cone -import Categories.Diagram.Cone.Properties -import Categories.Diagram.Cowedge -import Categories.Diagram.Cowedge.Properties -import Categories.Diagram.Duality -import Categories.Diagram.End -import Categories.Diagram.End.Properties -import Categories.Diagram.Equalizer -import Categories.Diagram.Equalizer.Indexed -import Categories.Diagram.Equalizer.Limit -import Categories.Diagram.Equalizer.Properties -import Categories.Diagram.Finite -import Categories.Diagram.KernelPair -import Categories.Diagram.Limit -import Categories.Diagram.Limit.Properties -import Categories.Diagram.Limit.Ran -import Categories.Diagram.Pullback -import Categories.Diagram.Pullback.Limit -import Categories.Diagram.Pullback.Properties -import Categories.Diagram.Pushout -import Categories.Diagram.Pushout.Properties -import Categories.Diagram.ReflexivePair -import Categories.Diagram.SubobjectClassifier -import Categories.Diagram.Wedge -import Categories.Diagram.Wedge.Properties -import Categories.Double -import Categories.Double.Core -import Categories.Enriched.Category -import Categories.Enriched.Category.Opposite -import Categories.Enriched.Category.Underlying -import Categories.Enriched.Functor -import Categories.Enriched.NaturalTransformation -import Categories.Enriched.NaturalTransformation.NaturalIsomorphism -import Categories.Enriched.Over.One -import Categories.Enriched.Over.Setoids -import Categories.FreeObjects.Free -import Categories.Functor -import Categories.Functor.Algebra -import Categories.Functor.Bialgebra -import Categories.Functor.Bifunctor -import Categories.Functor.Bifunctor.Properties -import Categories.Functor.Cartesian -import Categories.Functor.Cartesian.Properties -import Categories.Functor.CartesianClosed -import Categories.Functor.Coalgebra -import Categories.Functor.Construction.Constant -import Categories.Functor.Construction.Diagonal -import Categories.Functor.Construction.FromDiscrete -import Categories.Functor.Construction.LiftAlgebras -import Categories.Functor.Construction.LiftCoalgebras -import Categories.Functor.Construction.LiftSetoids -import Categories.Functor.Construction.Limit -import Categories.Functor.Construction.ObjectRestriction -import Categories.Functor.Construction.PathsOf -import Categories.Functor.Construction.SubCategory -import Categories.Functor.Construction.SubCategory.Properties -import Categories.Functor.Construction.Zero -import Categories.Functor.Core -import Categories.Functor.DistributiveLaw -import Categories.Functor.Duality -import Categories.Functor.Equivalence -import Categories.Functor.Fibration -import Categories.Functor.Groupoid -import Categories.Functor.Hom -import Categories.Functor.Hom.Properties -import Categories.Functor.Hom.Properties.Contra -import Categories.Functor.Hom.Properties.Covariant -import Categories.Functor.IdentityOnObjects -import Categories.Functor.Instance.0-Truncation -import Categories.Functor.Instance.01-Truncation -import Categories.Functor.Instance.ConnectedComponents -import Categories.Functor.Instance.Core -import Categories.Functor.Instance.Discrete -import Categories.Functor.Instance.SetoidDiscrete -import Categories.Functor.Instance.StrictCore -import Categories.Functor.Instance.Twisted -import Categories.Functor.Instance.UnderlyingQuiver -import Categories.Functor.Limits -import Categories.Functor.Monoidal -import Categories.Functor.Monoidal.Braided -import Categories.Functor.Monoidal.Construction.Product -import Categories.Functor.Monoidal.PointwiseTensor -import Categories.Functor.Monoidal.Properties -import Categories.Functor.Monoidal.Symmetric -import Categories.Functor.Monoidal.Tensor -import Categories.Functor.Power -import Categories.Functor.Power.Functorial -import Categories.Functor.Power.NaturalTransformation -import Categories.Functor.Presheaf -import Categories.Functor.Profunctor -import Categories.Functor.Profunctor.Cograph -import Categories.Functor.Profunctor.FormalComposite -import Categories.Functor.Properties -import Categories.Functor.Representable -import Categories.Functor.Restriction -import Categories.Functor.Slice -import Categories.GlobularSet -import Categories.Kan -import Categories.Kan.Duality -import Categories.Minus2-Category -import Categories.Minus2-Category.Construction.Indiscrete -import Categories.Minus2-Category.Instance.One -import Categories.Minus2-Category.Properties -import Categories.Monad -import Categories.Monad.Construction.Kleisli -import Categories.Monad.Duality -import Categories.Monad.Graded -import Categories.Monad.Idempotent -import Categories.Monad.Morphism -import Categories.Monad.Relative -import Categories.Monad.Strong -import Categories.Morphism -import Categories.Morphism.Cartesian -import Categories.Morphism.Duality -import Categories.Morphism.Extremal -import Categories.Morphism.Extremal.Properties -import Categories.Morphism.HeterogeneousEquality -import Categories.Morphism.HeterogeneousIdentity -import Categories.Morphism.HeterogeneousIdentity.Properties -import Categories.Morphism.Idempotent -import Categories.Morphism.Idempotent.Bundles -import Categories.Morphism.IsoEquiv -import Categories.Morphism.Isomorphism -import Categories.Morphism.Lifts -import Categories.Morphism.Lifts.Properties -import Categories.Morphism.Normal -import Categories.Morphism.Notation -import Categories.Morphism.Properties -import Categories.Morphism.Reasoning -import Categories.Morphism.Reasoning.Core -import Categories.Morphism.Reasoning.Iso -import Categories.Morphism.Regular -import Categories.Morphism.Regular.Properties -import Categories.Morphism.Universal -import Categories.Multi.Category.Indexed -import Categories.NaturalTransformation -import Categories.NaturalTransformation.Core -import Categories.NaturalTransformation.Dinatural -import Categories.NaturalTransformation.Equivalence -import Categories.NaturalTransformation.Extranatural -import Categories.NaturalTransformation.Hom -import Categories.NaturalTransformation.Monoidal -import Categories.NaturalTransformation.Monoidal.Braided -import Categories.NaturalTransformation.Monoidal.Symmetric -import Categories.NaturalTransformation.NaturalIsomorphism -import Categories.NaturalTransformation.NaturalIsomorphism.Equivalence -import Categories.NaturalTransformation.NaturalIsomorphism.Functors -import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal -import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Braided -import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric -import Categories.NaturalTransformation.NaturalIsomorphism.Properties -import Categories.NaturalTransformation.Properties -import Categories.Object.Biproduct -import Categories.Object.Cokernel -import Categories.Object.Coproduct -import Categories.Object.Duality -import Categories.Object.Exponential -import Categories.Object.Group -import Categories.Object.Initial -import Categories.Object.InternalRelation -import Categories.Object.Kernel -import Categories.Object.Kernel.Properties -import Categories.Object.Monoid -import Categories.Object.NaturalNumbers -import Categories.Object.NaturalNumbers.Parametrized -import Categories.Object.NaturalNumbers.Properties.F-Algebras -import Categories.Object.NaturalNumbers.Properties.Parametrized -import Categories.Object.Product -import Categories.Object.Product.Construction -import Categories.Object.Product.Core -import Categories.Object.Product.Indexed -import Categories.Object.Product.Indexed.Properties -import Categories.Object.Product.Limit -import Categories.Object.Product.Morphisms -import Categories.Object.Subobject -import Categories.Object.Subobject.Properties -import Categories.Object.Terminal -import Categories.Object.Terminal.Limit -import Categories.Object.Zero -import Categories.Pseudofunctor -import Categories.Pseudofunctor.Composition -import Categories.Pseudofunctor.Hom -import Categories.Pseudofunctor.Identity -import Categories.Pseudofunctor.Instance.EnrichedUnderlying -import Categories.Tactic.Category -import Categories.Theory.Lawvere -import Categories.Theory.Lawvere.Instance.Identity -import Categories.Theory.Lawvere.Instance.Triv -import Categories.Utils.EqReasoning -import Categories.Utils.Product -import Categories.Yoneda -import Categories.Yoneda.Continuous -import Categories.Yoneda.Properties -import Data.Quiver -import Data.Quiver.Morphism -import Data.Quiver.Paths -import Function.Construct.Setoid -import Relation.Binary.PropositionalEquality.Subst.Properties +import Categories.Adjoint.Instance.BaseChange +import Categories.Adjoint.Instance.Core +import Categories.Adjoint.Instance.PathsOf +import Categories.Adjoint.Instance.PosetCore +import Categories.Adjoint.Instance.Slice +import Categories.Adjoint.Instance.StrictCore +import Categories.Adjoint.Instance.StrictDiscrete +import Categories.Adjoint.Mate +import Categories.Adjoint.Monadic +import Categories.Adjoint.Monadic.Crude +import Categories.Adjoint.Monadic.Properties +import Categories.Adjoint.Parametric +import Categories.Adjoint.Properties +import Categories.Adjoint.RAPL +import Categories.Adjoint.Relative +import Categories.Adjoint.TwoSided +import Categories.Adjoint.TwoSided.Compose +import Categories.Bicategory +import Categories.Bicategory.Bigroupoid +import Categories.Bicategory.Construction.1-Category +import Categories.Bicategory.Construction.LaxSlice +import Categories.Bicategory.Construction.Spans +import Categories.Bicategory.Construction.Spans.Properties +import Categories.Bicategory.Extras +import Categories.Bicategory.Instance.Cats +import Categories.Bicategory.Instance.EnrichedCats +import Categories.Bicategory.Monad +import Categories.Bicategory.Monad.Properties +import Categories.Bicategory.Object.Product +import Categories.Bicategory.Object.Terminal +import Categories.Bicategory.Opposite +import Categories.Category +import Categories.Category.BicartesianClosed +import Categories.Category.BinaryProducts +import Categories.Category.CMonoidEnriched +import Categories.Category.Cartesian +import Categories.Category.Cartesian.Bundle +import Categories.Category.Cartesian.Monoidal +import Categories.Category.Cartesian.Properties +import Categories.Category.Cartesian.SymmetricMonoidal +import Categories.Category.CartesianClosed +import Categories.Category.CartesianClosed.Bundle +import Categories.Category.CartesianClosed.Canonical +import Categories.Category.CartesianClosed.Locally +import Categories.Category.CartesianClosed.Locally.Properties +import Categories.Category.CartesianClosed.Properties +import Categories.Category.Closed +import Categories.Category.Cocartesian +import Categories.Category.Cocartesian.Bundle +import Categories.Category.Cocomplete +import Categories.Category.Cocomplete.Finitely +import Categories.Category.Cocomplete.Finitely.Properties +import Categories.Category.Cocomplete.Properties +import Categories.Category.Complete +import Categories.Category.Complete.Finitely +import Categories.Category.Complete.Finitely.Properties +import Categories.Category.Complete.Properties +import Categories.Category.Complete.Properties.Construction +import Categories.Category.Complete.Properties.SolutionSet +import Categories.Category.Concrete +import Categories.Category.Concrete.Properties +import Categories.Category.Construction.0-Groupoid +import Categories.Category.Construction.Adjoints +import Categories.Category.Construction.Arrow +import Categories.Category.Construction.CoEilenbergMoore +import Categories.Category.Construction.CoKleisli +import Categories.Category.Construction.Cocones +import Categories.Category.Construction.Comma +import Categories.Category.Construction.Cones +import Categories.Category.Construction.Coproduct +import Categories.Category.Construction.Core +import Categories.Category.Construction.Cowedges +import Categories.Category.Construction.EilenbergMoore +import Categories.Category.Construction.Elements +import Categories.Category.Construction.EnrichedFunctors +import Categories.Category.Construction.F-Algebras +import Categories.Category.Construction.F-Coalgebras +import Categories.Category.Construction.Fin +import Categories.Category.Construction.Functors +import Categories.Category.Construction.Grothendieck +import Categories.Category.Construction.GroupAsCategory +import Categories.Category.Construction.Groups +import Categories.Category.Construction.KanComplex +import Categories.Category.Construction.KaroubiEnvelope +import Categories.Category.Construction.KaroubiEnvelope.Properties +import Categories.Category.Construction.Kleisli +import Categories.Category.Construction.LT-Models +import Categories.Category.Construction.MonoidAsCategory +import Categories.Category.Construction.MonoidalFunctors +import Categories.Category.Construction.Monoids +import Categories.Category.Construction.ObjectRestriction +import Categories.Category.Construction.Path +import Categories.Category.Construction.PathCategory +import Categories.Category.Construction.Presheaves +import Categories.Category.Construction.Properties.CoEilenbergMoore +import Categories.Category.Construction.Properties.CoKleisli +import Categories.Category.Construction.Properties.Comma +import Categories.Category.Construction.Properties.EilenbergMoore +import Categories.Category.Construction.Properties.Functors +import Categories.Category.Construction.Properties.Kleisli +import Categories.Category.Construction.Properties.Presheaves +import Categories.Category.Construction.Properties.Presheaves.Cartesian +import Categories.Category.Construction.Properties.Presheaves.CartesianClosed +import Categories.Category.Construction.Properties.Presheaves.Complete +import Categories.Category.Construction.Properties.Presheaves.FromCartesianCCC +import Categories.Category.Construction.Pullbacks +import Categories.Category.Construction.SetoidDiscrete +import Categories.Category.Construction.Spans +import Categories.Category.Construction.StrictDiscrete +import Categories.Category.Construction.SymmetricMonoidalFunctors +import Categories.Category.Construction.Thin +import Categories.Category.Construction.TwistedArrow +import Categories.Category.Construction.Wedges +import Categories.Category.Construction.mu-Bialgebras +import Categories.Category.Core +import Categories.Category.Dagger +import Categories.Category.Dagger.Construction.Discrete +import Categories.Category.Dagger.Instance.Rels +import Categories.Category.Diagram.Span +import Categories.Category.Discrete +import Categories.Category.Distributive +import Categories.Category.Duality +import Categories.Category.Equivalence +import Categories.Category.Equivalence.Preserves +import Categories.Category.Equivalence.Properties +import Categories.Category.Exact +import Categories.Category.Extensive +import Categories.Category.Extensive.Bundle +import Categories.Category.Extensive.Properties.Distributive +import Categories.Category.Finite +import Categories.Category.Finite.Fin +import Categories.Category.Finite.Fin.Construction.Discrete +import Categories.Category.Finite.Fin.Construction.Poset +import Categories.Category.Finite.Fin.Instance.Parallel +import Categories.Category.Finite.Fin.Instance.Span +import Categories.Category.Finite.Fin.Instance.Triangle +import Categories.Category.Groupoid +import Categories.Category.Groupoid.Properties +import Categories.Category.Helper +import Categories.Category.Indiscrete +import Categories.Category.Instance.Cartesians +import Categories.Category.Instance.Cats +import Categories.Category.Instance.EmptySet +import Categories.Category.Instance.FamilyOfSetoids +import Categories.Category.Instance.FinCatShapes +import Categories.Category.Instance.FinSetoids +import Categories.Category.Instance.Globe +import Categories.Category.Instance.Groupoids +import Categories.Category.Instance.KanComplexes +import Categories.Category.Instance.LawvereTheories +import Categories.Category.Instance.Monoidals +import Categories.Category.Instance.Nat +import Categories.Category.Instance.One +import Categories.Category.Instance.PartialFunctions +import Categories.Category.Instance.PointedSets +import Categories.Category.Instance.Posets +import Categories.Category.Instance.Preds +import Categories.Category.Instance.Properties.Cats +import Categories.Category.Instance.Properties.Posets +import Categories.Category.Instance.Properties.Setoids +import Categories.Category.Instance.Properties.Setoids.CCC +import Categories.Category.Instance.Properties.Setoids.Choice +import Categories.Category.Instance.Properties.Setoids.Cocomplete +import Categories.Category.Instance.Properties.Setoids.Complete +import Categories.Category.Instance.Properties.Setoids.Exact +import Categories.Category.Instance.Properties.Setoids.Extensive +import Categories.Category.Instance.Properties.Setoids.LCCC +import Categories.Category.Instance.Properties.Setoids.Limits.Canonical +import Categories.Category.Instance.Quivers +import Categories.Category.Instance.Rels +import Categories.Category.Instance.Setoids +import Categories.Category.Instance.Sets +import Categories.Category.Instance.Simplex +import Categories.Category.Instance.SimplicialSet +import Categories.Category.Instance.SimplicialSet.Properties +import Categories.Category.Instance.SingletonSet +import Categories.Category.Instance.Span +import Categories.Category.Instance.StrictCats +import Categories.Category.Instance.StrictGroupoids +import Categories.Category.Instance.Zero +import Categories.Category.Inverse +import Categories.Category.Lift +import Categories.Category.Monoidal +import Categories.Category.Monoidal.Braided +import Categories.Category.Monoidal.Braided.Properties +import Categories.Category.Monoidal.Bundle +import Categories.Category.Monoidal.Closed +import Categories.Category.Monoidal.Closed.IsClosed +import Categories.Category.Monoidal.Closed.IsClosed.Diagonal +import Categories.Category.Monoidal.Closed.IsClosed.Dinatural +import Categories.Category.Monoidal.Closed.IsClosed.Identity +import Categories.Category.Monoidal.Closed.IsClosed.L +import Categories.Category.Monoidal.Closed.IsClosed.Pentagon +import Categories.Category.Monoidal.CompactClosed +import Categories.Category.Monoidal.Construction.Endofunctors +import Categories.Category.Monoidal.Construction.Minus2 +import Categories.Category.Monoidal.Construction.Product +import Categories.Category.Monoidal.Core +import Categories.Category.Monoidal.Instance.Cats +import Categories.Category.Monoidal.Instance.One +import Categories.Category.Monoidal.Instance.Rels +import Categories.Category.Monoidal.Instance.Setoids +import Categories.Category.Monoidal.Instance.Sets +import Categories.Category.Monoidal.Instance.StrictCats +import Categories.Category.Monoidal.Interchange +import Categories.Category.Monoidal.Interchange.Braided +import Categories.Category.Monoidal.Interchange.Symmetric +import Categories.Category.Monoidal.Properties +import Categories.Category.Monoidal.Reasoning +import Categories.Category.Monoidal.Rigid +import Categories.Category.Monoidal.Star-Autonomous +import Categories.Category.Monoidal.Symmetric +import Categories.Category.Monoidal.Traced +import Categories.Category.Monoidal.Utilities +import Categories.Category.Product +import Categories.Category.Product.Properties +import Categories.Category.Regular +import Categories.Category.Restriction +import Categories.Category.Restriction.Construction.Trivial +import Categories.Category.Restriction.Instance.PartialFunctions +import Categories.Category.Restriction.Properties +import Categories.Category.RigCategory +import Categories.Category.Site +import Categories.Category.Slice +import Categories.Category.Slice.Properties +import Categories.Category.Species +import Categories.Category.Species.Constructions +import Categories.Category.SubCategory +import Categories.Category.Topos +import Categories.Category.Unbundled +import Categories.Category.Unbundled.Properties +import Categories.Category.Unbundled.Utilities +import Categories.CoYoneda +import Categories.Comonad +import Categories.Comonad.Construction.CoKleisli +import Categories.Comonad.Relative +import Categories.Diagram.Cocone +import Categories.Diagram.Cocone.Properties +import Categories.Diagram.Coend +import Categories.Diagram.Coend.Properties +import Categories.Diagram.Coequalizer +import Categories.Diagram.Coequalizer.Properties +import Categories.Diagram.Colimit +import Categories.Diagram.Colimit.DualProperties +import Categories.Diagram.Colimit.Lan +import Categories.Diagram.Colimit.Properties +import Categories.Diagram.Cone +import Categories.Diagram.Cone.Properties +import Categories.Diagram.Cowedge +import Categories.Diagram.Cowedge.Properties +import Categories.Diagram.Duality +import Categories.Diagram.End +import Categories.Diagram.End.Properties +import Categories.Diagram.Equalizer +import Categories.Diagram.Equalizer.Indexed +import Categories.Diagram.Equalizer.Limit +import Categories.Diagram.Equalizer.Properties +import Categories.Diagram.Finite +import Categories.Diagram.KernelPair +import Categories.Diagram.Limit +import Categories.Diagram.Limit.Properties +import Categories.Diagram.Limit.Ran +import Categories.Diagram.Pullback +import Categories.Diagram.Pullback.Limit +import Categories.Diagram.Pullback.Properties +import Categories.Diagram.Pushout +import Categories.Diagram.Pushout.Properties +import Categories.Diagram.ReflexivePair +import Categories.Diagram.SubobjectClassifier +import Categories.Diagram.Wedge +import Categories.Diagram.Wedge.Properties +import Categories.Double +import Categories.Double.Core +import Categories.Enriched.Category +import Categories.Enriched.Category.Opposite +import Categories.Enriched.Category.Underlying +import Categories.Enriched.Functor +import Categories.Enriched.NaturalTransformation +import Categories.Enriched.NaturalTransformation.NaturalIsomorphism +import Categories.Enriched.Over.One +import Categories.Enriched.Over.Setoids +import Categories.FreeObjects.Free +import Categories.Functor +import Categories.Functor.Algebra +import Categories.Functor.Bialgebra +import Categories.Functor.Bifunctor +import Categories.Functor.Bifunctor.Properties +import Categories.Functor.Cartesian +import Categories.Functor.Cartesian.Properties +import Categories.Functor.CartesianClosed +import Categories.Functor.Coalgebra +import Categories.Functor.Construction.Constant +import Categories.Functor.Construction.Diagonal +import Categories.Functor.Construction.FromDiscrete +import Categories.Functor.Construction.LiftAlgebras +import Categories.Functor.Construction.LiftCoalgebras +import Categories.Functor.Construction.LiftSetoids +import Categories.Functor.Construction.Limit +import Categories.Functor.Construction.ObjectRestriction +import Categories.Functor.Construction.PathsOf +import Categories.Functor.Construction.SubCategory +import Categories.Functor.Construction.SubCategory.Properties +import Categories.Functor.Construction.Zero +import Categories.Functor.Core +import Categories.Functor.DistributiveLaw +import Categories.Functor.Duality +import Categories.Functor.Equivalence +import Categories.Functor.Fibration +import Categories.Functor.Groupoid +import Categories.Functor.Hom +import Categories.Functor.Hom.Properties +import Categories.Functor.Hom.Properties.Contra +import Categories.Functor.Hom.Properties.Covariant +import Categories.Functor.IdentityOnObjects +import Categories.Functor.Instance.0-Truncation +import Categories.Functor.Instance.01-Truncation +import Categories.Functor.Instance.ConnectedComponents +import Categories.Functor.Instance.Core +import Categories.Functor.Instance.Discrete +import Categories.Functor.Instance.SetoidDiscrete +import Categories.Functor.Instance.StrictCore +import Categories.Functor.Instance.Twisted +import Categories.Functor.Instance.UnderlyingQuiver +import Categories.Functor.Limits +import Categories.Functor.Monoidal +import Categories.Functor.Monoidal.Braided +import Categories.Functor.Monoidal.Construction.Product +import Categories.Functor.Monoidal.PointwiseTensor +import Categories.Functor.Monoidal.Properties +import Categories.Functor.Monoidal.Symmetric +import Categories.Functor.Monoidal.Tensor +import Categories.Functor.Power +import Categories.Functor.Power.Functorial +import Categories.Functor.Power.NaturalTransformation +import Categories.Functor.Presheaf +import Categories.Functor.Profunctor +import Categories.Functor.Profunctor.Cograph +import Categories.Functor.Profunctor.FormalComposite +import Categories.Functor.Properties +import Categories.Functor.Representable +import Categories.Functor.Restriction +import Categories.Functor.Slice +import Categories.Functor.Slice.BaseChange +import Categories.GlobularSet +import Categories.Kan +import Categories.Kan.Duality +import Categories.Minus2-Category +import Categories.Minus2-Category.Construction.Indiscrete +import Categories.Minus2-Category.Instance.One +import Categories.Minus2-Category.Properties +import Categories.Monad +import Categories.Monad.Construction.Kleisli +import Categories.Monad.Duality +import Categories.Monad.Graded +import Categories.Monad.Idempotent +import Categories.Monad.Morphism +import Categories.Monad.Relative +import Categories.Monad.Strong +import Categories.Morphism +import Categories.Morphism.Cartesian +import Categories.Morphism.Duality +import Categories.Morphism.Extremal +import Categories.Morphism.Extremal.Properties +import Categories.Morphism.HeterogeneousEquality +import Categories.Morphism.HeterogeneousIdentity +import Categories.Morphism.HeterogeneousIdentity.Properties +import Categories.Morphism.Idempotent +import Categories.Morphism.Idempotent.Bundles +import Categories.Morphism.IsoEquiv +import Categories.Morphism.Isomorphism +import Categories.Morphism.Lifts +import Categories.Morphism.Lifts.Properties +import Categories.Morphism.Normal +import Categories.Morphism.Notation +import Categories.Morphism.Properties +import Categories.Morphism.Reasoning +import Categories.Morphism.Reasoning.Core +import Categories.Morphism.Reasoning.Iso +import Categories.Morphism.Regular +import Categories.Morphism.Regular.Properties +import Categories.Morphism.Universal +import Categories.Multi.Category.Indexed +import Categories.NaturalTransformation +import Categories.NaturalTransformation.Core +import Categories.NaturalTransformation.Dinatural +import Categories.NaturalTransformation.Equivalence +import Categories.NaturalTransformation.Extranatural +import Categories.NaturalTransformation.Hom +import Categories.NaturalTransformation.Monoidal +import Categories.NaturalTransformation.Monoidal.Braided +import Categories.NaturalTransformation.Monoidal.Symmetric +import Categories.NaturalTransformation.NaturalIsomorphism +import Categories.NaturalTransformation.NaturalIsomorphism.Equivalence +import Categories.NaturalTransformation.NaturalIsomorphism.Functors +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Braided +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric +import Categories.NaturalTransformation.NaturalIsomorphism.Properties +import Categories.NaturalTransformation.Properties +import Categories.Object.Biproduct +import Categories.Object.Cokernel +import Categories.Object.Coproduct +import Categories.Object.Duality +import Categories.Object.Exponential +import Categories.Object.Group +import Categories.Object.Initial +import Categories.Object.InternalRelation +import Categories.Object.Kernel +import Categories.Object.Kernel.Properties +import Categories.Object.Monoid +import Categories.Object.NaturalNumbers +import Categories.Object.NaturalNumbers.Parametrized +import Categories.Object.NaturalNumbers.Properties.F-Algebras +import Categories.Object.NaturalNumbers.Properties.Parametrized +import Categories.Object.Product +import Categories.Object.Product.Construction +import Categories.Object.Product.Core +import Categories.Object.Product.Indexed +import Categories.Object.Product.Indexed.Properties +import Categories.Object.Product.Limit +import Categories.Object.Product.Morphisms +import Categories.Object.Subobject +import Categories.Object.Subobject.Properties +import Categories.Object.Terminal +import Categories.Object.Terminal.Limit +import Categories.Object.Zero +import Categories.Pseudofunctor +import Categories.Pseudofunctor.Composition +import Categories.Pseudofunctor.Hom +import Categories.Pseudofunctor.Identity +import Categories.Pseudofunctor.Instance.EnrichedUnderlying +import Categories.Tactic.Category +import Categories.Theory.Lawvere +import Categories.Theory.Lawvere.Instance.Identity +import Categories.Theory.Lawvere.Instance.Triv +import Categories.Utils.EqReasoning +import Categories.Utils.Product +import Categories.Yoneda +import Categories.Yoneda.Continuous +import Categories.Yoneda.Properties +import Data.Quiver +import Data.Quiver.Morphism +import Data.Quiver.Paths +import Function.Construct.Setoid +import Relation.Binary.PropositionalEquality.Subst.Properties \ No newline at end of file diff --git a/index.html b/index.html index 34774b4a6..200e0387e 100644 --- a/index.html +++ b/index.html @@ -21,446 +21,449 @@ import Categories.Adjoint.Equivalents import Categories.Adjoint.Instance.0-Truncation import Categories.Adjoint.Instance.01-Truncation -import Categories.Adjoint.Instance.Core -import Categories.Adjoint.Instance.PathsOf -import Categories.Adjoint.Instance.PosetCore -import Categories.Adjoint.Instance.StrictCore -import Categories.Adjoint.Instance.StrictDiscrete -import Categories.Adjoint.Mate -import Categories.Adjoint.Monadic -import Categories.Adjoint.Monadic.Crude -import Categories.Adjoint.Monadic.Properties -import Categories.Adjoint.Parametric -import Categories.Adjoint.Properties -import Categories.Adjoint.RAPL -import Categories.Adjoint.Relative -import Categories.Adjoint.TwoSided -import Categories.Adjoint.TwoSided.Compose -import Categories.Bicategory -import Categories.Bicategory.Bigroupoid -import Categories.Bicategory.Construction.1-Category -import Categories.Bicategory.Construction.LaxSlice -import Categories.Bicategory.Construction.Spans -import Categories.Bicategory.Construction.Spans.Properties -import Categories.Bicategory.Extras -import Categories.Bicategory.Instance.Cats -import Categories.Bicategory.Instance.EnrichedCats -import Categories.Bicategory.Monad -import Categories.Bicategory.Monad.Properties -import Categories.Bicategory.Object.Product -import Categories.Bicategory.Object.Terminal -import Categories.Bicategory.Opposite -import Categories.Category -import Categories.Category.BicartesianClosed -import Categories.Category.BinaryProducts -import Categories.Category.CMonoidEnriched -import Categories.Category.Cartesian -import Categories.Category.Cartesian.Bundle -import Categories.Category.Cartesian.Monoidal -import Categories.Category.Cartesian.Properties -import Categories.Category.Cartesian.SymmetricMonoidal -import Categories.Category.CartesianClosed -import Categories.Category.CartesianClosed.Bundle -import Categories.Category.CartesianClosed.Canonical -import Categories.Category.CartesianClosed.Locally -import Categories.Category.CartesianClosed.Locally.Properties -import Categories.Category.CartesianClosed.Properties -import Categories.Category.Closed -import Categories.Category.Cocartesian -import Categories.Category.Cocartesian.Bundle -import Categories.Category.Cocomplete -import Categories.Category.Cocomplete.Finitely -import Categories.Category.Cocomplete.Finitely.Properties -import Categories.Category.Cocomplete.Properties -import Categories.Category.Complete -import Categories.Category.Complete.Finitely -import Categories.Category.Complete.Finitely.Properties -import Categories.Category.Complete.Properties -import Categories.Category.Complete.Properties.Construction -import Categories.Category.Complete.Properties.SolutionSet -import Categories.Category.Concrete -import Categories.Category.Concrete.Properties -import Categories.Category.Construction.0-Groupoid -import Categories.Category.Construction.Adjoints -import Categories.Category.Construction.Arrow -import Categories.Category.Construction.CoEilenbergMoore -import Categories.Category.Construction.CoKleisli -import Categories.Category.Construction.Cocones -import Categories.Category.Construction.Comma -import Categories.Category.Construction.Cones -import Categories.Category.Construction.Coproduct -import Categories.Category.Construction.Core -import Categories.Category.Construction.Cowedges -import Categories.Category.Construction.EilenbergMoore -import Categories.Category.Construction.Elements -import Categories.Category.Construction.EnrichedFunctors -import Categories.Category.Construction.F-Algebras -import Categories.Category.Construction.F-Coalgebras -import Categories.Category.Construction.Fin -import Categories.Category.Construction.Functors -import Categories.Category.Construction.Grothendieck -import Categories.Category.Construction.GroupAsCategory -import Categories.Category.Construction.Groups -import Categories.Category.Construction.KanComplex -import Categories.Category.Construction.KaroubiEnvelope -import Categories.Category.Construction.KaroubiEnvelope.Properties -import Categories.Category.Construction.Kleisli -import Categories.Category.Construction.LT-Models -import Categories.Category.Construction.MonoidAsCategory -import Categories.Category.Construction.MonoidalFunctors -import Categories.Category.Construction.Monoids -import Categories.Category.Construction.ObjectRestriction -import Categories.Category.Construction.Path -import Categories.Category.Construction.PathCategory -import Categories.Category.Construction.Presheaves -import Categories.Category.Construction.Properties.CoEilenbergMoore -import Categories.Category.Construction.Properties.CoKleisli -import Categories.Category.Construction.Properties.Comma -import Categories.Category.Construction.Properties.EilenbergMoore -import Categories.Category.Construction.Properties.Functors -import Categories.Category.Construction.Properties.Kleisli -import Categories.Category.Construction.Properties.Presheaves -import Categories.Category.Construction.Properties.Presheaves.Cartesian -import Categories.Category.Construction.Properties.Presheaves.CartesianClosed -import Categories.Category.Construction.Properties.Presheaves.Complete -import Categories.Category.Construction.Properties.Presheaves.FromCartesianCCC -import Categories.Category.Construction.Pullbacks -import Categories.Category.Construction.SetoidDiscrete -import Categories.Category.Construction.Spans -import Categories.Category.Construction.StrictDiscrete -import Categories.Category.Construction.SymmetricMonoidalFunctors -import Categories.Category.Construction.Thin -import Categories.Category.Construction.TwistedArrow -import Categories.Category.Construction.Wedges -import Categories.Category.Construction.mu-Bialgebras -import Categories.Category.Core -import Categories.Category.Dagger -import Categories.Category.Dagger.Construction.Discrete -import Categories.Category.Dagger.Instance.Rels -import Categories.Category.Diagram.Span -import Categories.Category.Discrete -import Categories.Category.Distributive -import Categories.Category.Duality -import Categories.Category.Equivalence -import Categories.Category.Equivalence.Preserves -import Categories.Category.Equivalence.Properties -import Categories.Category.Exact -import Categories.Category.Extensive -import Categories.Category.Extensive.Bundle -import Categories.Category.Extensive.Properties.Distributive -import Categories.Category.Finite -import Categories.Category.Finite.Fin -import Categories.Category.Finite.Fin.Construction.Discrete -import Categories.Category.Finite.Fin.Construction.Poset -import Categories.Category.Finite.Fin.Instance.Parallel -import Categories.Category.Finite.Fin.Instance.Span -import Categories.Category.Finite.Fin.Instance.Triangle -import Categories.Category.Groupoid -import Categories.Category.Groupoid.Properties -import Categories.Category.Helper -import Categories.Category.Indiscrete -import Categories.Category.Instance.Cartesians -import Categories.Category.Instance.Cats -import Categories.Category.Instance.EmptySet -import Categories.Category.Instance.FamilyOfSetoids -import Categories.Category.Instance.FinCatShapes -import Categories.Category.Instance.FinSetoids -import Categories.Category.Instance.Globe -import Categories.Category.Instance.Groupoids -import Categories.Category.Instance.KanComplexes -import Categories.Category.Instance.LawvereTheories -import Categories.Category.Instance.Monoidals -import Categories.Category.Instance.Nat -import Categories.Category.Instance.One -import Categories.Category.Instance.PartialFunctions -import Categories.Category.Instance.PointedSets -import Categories.Category.Instance.Posets -import Categories.Category.Instance.Preds -import Categories.Category.Instance.Properties.Cats -import Categories.Category.Instance.Properties.Posets -import Categories.Category.Instance.Properties.Setoids -import Categories.Category.Instance.Properties.Setoids.CCC -import Categories.Category.Instance.Properties.Setoids.Choice -import Categories.Category.Instance.Properties.Setoids.Cocomplete -import Categories.Category.Instance.Properties.Setoids.Complete -import Categories.Category.Instance.Properties.Setoids.Exact -import Categories.Category.Instance.Properties.Setoids.Extensive -import Categories.Category.Instance.Properties.Setoids.LCCC -import Categories.Category.Instance.Properties.Setoids.Limits.Canonical -import Categories.Category.Instance.Quivers -import Categories.Category.Instance.Rels -import Categories.Category.Instance.Setoids -import Categories.Category.Instance.Sets -import Categories.Category.Instance.Simplex -import Categories.Category.Instance.SimplicialSet -import Categories.Category.Instance.SimplicialSet.Properties -import Categories.Category.Instance.SingletonSet -import Categories.Category.Instance.Span -import Categories.Category.Instance.StrictCats -import Categories.Category.Instance.StrictGroupoids -import Categories.Category.Instance.Zero -import Categories.Category.Inverse -import Categories.Category.Lift -import Categories.Category.Monoidal -import Categories.Category.Monoidal.Braided -import Categories.Category.Monoidal.Braided.Properties -import Categories.Category.Monoidal.Bundle -import Categories.Category.Monoidal.Closed -import Categories.Category.Monoidal.Closed.IsClosed -import Categories.Category.Monoidal.Closed.IsClosed.Diagonal -import Categories.Category.Monoidal.Closed.IsClosed.Dinatural -import Categories.Category.Monoidal.Closed.IsClosed.Identity -import Categories.Category.Monoidal.Closed.IsClosed.L -import Categories.Category.Monoidal.Closed.IsClosed.Pentagon -import Categories.Category.Monoidal.CompactClosed -import Categories.Category.Monoidal.Construction.Endofunctors -import Categories.Category.Monoidal.Construction.Minus2 -import Categories.Category.Monoidal.Construction.Product -import Categories.Category.Monoidal.Core -import Categories.Category.Monoidal.Instance.Cats -import Categories.Category.Monoidal.Instance.One -import Categories.Category.Monoidal.Instance.Rels -import Categories.Category.Monoidal.Instance.Setoids -import Categories.Category.Monoidal.Instance.Sets -import Categories.Category.Monoidal.Instance.StrictCats -import Categories.Category.Monoidal.Interchange -import Categories.Category.Monoidal.Interchange.Braided -import Categories.Category.Monoidal.Interchange.Symmetric -import Categories.Category.Monoidal.Properties -import Categories.Category.Monoidal.Reasoning -import Categories.Category.Monoidal.Rigid -import Categories.Category.Monoidal.Star-Autonomous -import Categories.Category.Monoidal.Symmetric -import Categories.Category.Monoidal.Traced -import Categories.Category.Monoidal.Utilities -import Categories.Category.Product -import Categories.Category.Product.Properties -import Categories.Category.Regular -import Categories.Category.Restriction -import Categories.Category.Restriction.Construction.Trivial -import Categories.Category.Restriction.Instance.PartialFunctions -import Categories.Category.Restriction.Properties -import Categories.Category.RigCategory -import Categories.Category.Site -import Categories.Category.Slice -import Categories.Category.Slice.Properties -import Categories.Category.Species -import Categories.Category.Species.Constructions -import Categories.Category.SubCategory -import Categories.Category.Topos -import Categories.Category.Unbundled -import Categories.Category.Unbundled.Properties -import Categories.Category.Unbundled.Utilities -import Categories.CoYoneda -import Categories.Comonad -import Categories.Comonad.Construction.CoKleisli -import Categories.Comonad.Relative -import Categories.Diagram.Cocone -import Categories.Diagram.Cocone.Properties -import Categories.Diagram.Coend -import Categories.Diagram.Coend.Properties -import Categories.Diagram.Coequalizer -import Categories.Diagram.Coequalizer.Properties -import Categories.Diagram.Colimit -import Categories.Diagram.Colimit.DualProperties -import Categories.Diagram.Colimit.Lan -import Categories.Diagram.Colimit.Properties -import Categories.Diagram.Cone -import Categories.Diagram.Cone.Properties -import Categories.Diagram.Cowedge -import Categories.Diagram.Cowedge.Properties -import Categories.Diagram.Duality -import Categories.Diagram.End -import Categories.Diagram.End.Properties -import Categories.Diagram.Equalizer -import Categories.Diagram.Equalizer.Indexed -import Categories.Diagram.Equalizer.Limit -import Categories.Diagram.Equalizer.Properties -import Categories.Diagram.Finite -import Categories.Diagram.KernelPair -import Categories.Diagram.Limit -import Categories.Diagram.Limit.Properties -import Categories.Diagram.Limit.Ran -import Categories.Diagram.Pullback -import Categories.Diagram.Pullback.Limit -import Categories.Diagram.Pullback.Properties -import Categories.Diagram.Pushout -import Categories.Diagram.Pushout.Properties -import Categories.Diagram.ReflexivePair -import Categories.Diagram.SubobjectClassifier -import Categories.Diagram.Wedge -import Categories.Diagram.Wedge.Properties -import Categories.Double -import Categories.Double.Core -import Categories.Enriched.Category -import Categories.Enriched.Category.Opposite -import Categories.Enriched.Category.Underlying -import Categories.Enriched.Functor -import Categories.Enriched.NaturalTransformation -import Categories.Enriched.NaturalTransformation.NaturalIsomorphism -import Categories.Enriched.Over.One -import Categories.Enriched.Over.Setoids -import Categories.FreeObjects.Free -import Categories.Functor -import Categories.Functor.Algebra -import Categories.Functor.Bialgebra -import Categories.Functor.Bifunctor -import Categories.Functor.Bifunctor.Properties -import Categories.Functor.Cartesian -import Categories.Functor.Cartesian.Properties -import Categories.Functor.CartesianClosed -import Categories.Functor.Coalgebra -import Categories.Functor.Construction.Constant -import Categories.Functor.Construction.Diagonal -import Categories.Functor.Construction.FromDiscrete -import Categories.Functor.Construction.LiftAlgebras -import Categories.Functor.Construction.LiftCoalgebras -import Categories.Functor.Construction.LiftSetoids -import Categories.Functor.Construction.Limit -import Categories.Functor.Construction.ObjectRestriction -import Categories.Functor.Construction.PathsOf -import Categories.Functor.Construction.SubCategory -import Categories.Functor.Construction.SubCategory.Properties -import Categories.Functor.Construction.Zero -import Categories.Functor.Core -import Categories.Functor.DistributiveLaw -import Categories.Functor.Duality -import Categories.Functor.Equivalence -import Categories.Functor.Fibration -import Categories.Functor.Groupoid -import Categories.Functor.Hom -import Categories.Functor.Hom.Properties -import Categories.Functor.Hom.Properties.Contra -import Categories.Functor.Hom.Properties.Covariant -import Categories.Functor.IdentityOnObjects -import Categories.Functor.Instance.0-Truncation -import Categories.Functor.Instance.01-Truncation -import Categories.Functor.Instance.ConnectedComponents -import Categories.Functor.Instance.Core -import Categories.Functor.Instance.Discrete -import Categories.Functor.Instance.SetoidDiscrete -import Categories.Functor.Instance.StrictCore -import Categories.Functor.Instance.Twisted -import Categories.Functor.Instance.UnderlyingQuiver -import Categories.Functor.Limits -import Categories.Functor.Monoidal -import Categories.Functor.Monoidal.Braided -import Categories.Functor.Monoidal.Construction.Product -import Categories.Functor.Monoidal.PointwiseTensor -import Categories.Functor.Monoidal.Properties -import Categories.Functor.Monoidal.Symmetric -import Categories.Functor.Monoidal.Tensor -import Categories.Functor.Power -import Categories.Functor.Power.Functorial -import Categories.Functor.Power.NaturalTransformation -import Categories.Functor.Presheaf -import Categories.Functor.Profunctor -import Categories.Functor.Profunctor.Cograph -import Categories.Functor.Profunctor.FormalComposite -import Categories.Functor.Properties -import Categories.Functor.Representable -import Categories.Functor.Restriction -import Categories.Functor.Slice -import Categories.GlobularSet -import Categories.Kan -import Categories.Kan.Duality -import Categories.Minus2-Category -import Categories.Minus2-Category.Construction.Indiscrete -import Categories.Minus2-Category.Instance.One -import Categories.Minus2-Category.Properties -import Categories.Monad -import Categories.Monad.Construction.Kleisli -import Categories.Monad.Duality -import Categories.Monad.Graded -import Categories.Monad.Idempotent -import Categories.Monad.Morphism -import Categories.Monad.Relative -import Categories.Monad.Strong -import Categories.Morphism -import Categories.Morphism.Cartesian -import Categories.Morphism.Duality -import Categories.Morphism.Extremal -import Categories.Morphism.Extremal.Properties -import Categories.Morphism.HeterogeneousEquality -import Categories.Morphism.HeterogeneousIdentity -import Categories.Morphism.HeterogeneousIdentity.Properties -import Categories.Morphism.Idempotent -import Categories.Morphism.Idempotent.Bundles -import Categories.Morphism.IsoEquiv -import Categories.Morphism.Isomorphism -import Categories.Morphism.Lifts -import Categories.Morphism.Lifts.Properties -import Categories.Morphism.Normal -import Categories.Morphism.Notation -import Categories.Morphism.Properties -import Categories.Morphism.Reasoning -import Categories.Morphism.Reasoning.Core -import Categories.Morphism.Reasoning.Iso -import Categories.Morphism.Regular -import Categories.Morphism.Regular.Properties -import Categories.Morphism.Universal -import Categories.Multi.Category.Indexed -import Categories.NaturalTransformation -import Categories.NaturalTransformation.Core -import Categories.NaturalTransformation.Dinatural -import Categories.NaturalTransformation.Equivalence -import Categories.NaturalTransformation.Extranatural -import Categories.NaturalTransformation.Hom -import Categories.NaturalTransformation.Monoidal -import Categories.NaturalTransformation.Monoidal.Braided -import Categories.NaturalTransformation.Monoidal.Symmetric -import Categories.NaturalTransformation.NaturalIsomorphism -import Categories.NaturalTransformation.NaturalIsomorphism.Equivalence -import Categories.NaturalTransformation.NaturalIsomorphism.Functors -import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal -import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Braided -import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric -import Categories.NaturalTransformation.NaturalIsomorphism.Properties -import Categories.NaturalTransformation.Properties -import Categories.Object.Biproduct -import Categories.Object.Cokernel -import Categories.Object.Coproduct -import Categories.Object.Duality -import Categories.Object.Exponential -import Categories.Object.Group -import Categories.Object.Initial -import Categories.Object.InternalRelation -import Categories.Object.Kernel -import Categories.Object.Kernel.Properties -import Categories.Object.Monoid -import Categories.Object.NaturalNumbers -import Categories.Object.NaturalNumbers.Parametrized -import Categories.Object.NaturalNumbers.Properties.F-Algebras -import Categories.Object.NaturalNumbers.Properties.Parametrized -import Categories.Object.Product -import Categories.Object.Product.Construction -import Categories.Object.Product.Core -import Categories.Object.Product.Indexed -import Categories.Object.Product.Indexed.Properties -import Categories.Object.Product.Limit -import Categories.Object.Product.Morphisms -import Categories.Object.Subobject -import Categories.Object.Subobject.Properties -import Categories.Object.Terminal -import Categories.Object.Terminal.Limit -import Categories.Object.Zero -import Categories.Pseudofunctor -import Categories.Pseudofunctor.Composition -import Categories.Pseudofunctor.Hom -import Categories.Pseudofunctor.Identity -import Categories.Pseudofunctor.Instance.EnrichedUnderlying -import Categories.Tactic.Category -import Categories.Theory.Lawvere -import Categories.Theory.Lawvere.Instance.Identity -import Categories.Theory.Lawvere.Instance.Triv -import Categories.Utils.EqReasoning -import Categories.Utils.Product -import Categories.Yoneda -import Categories.Yoneda.Continuous -import Categories.Yoneda.Properties -import Data.Quiver -import Data.Quiver.Morphism -import Data.Quiver.Paths -import Function.Construct.Setoid -import Relation.Binary.PropositionalEquality.Subst.Properties +import Categories.Adjoint.Instance.BaseChange +import Categories.Adjoint.Instance.Core +import Categories.Adjoint.Instance.PathsOf +import Categories.Adjoint.Instance.PosetCore +import Categories.Adjoint.Instance.Slice +import Categories.Adjoint.Instance.StrictCore +import Categories.Adjoint.Instance.StrictDiscrete +import Categories.Adjoint.Mate +import Categories.Adjoint.Monadic +import Categories.Adjoint.Monadic.Crude +import Categories.Adjoint.Monadic.Properties +import Categories.Adjoint.Parametric +import Categories.Adjoint.Properties +import Categories.Adjoint.RAPL +import Categories.Adjoint.Relative +import Categories.Adjoint.TwoSided +import Categories.Adjoint.TwoSided.Compose +import Categories.Bicategory +import Categories.Bicategory.Bigroupoid +import Categories.Bicategory.Construction.1-Category +import Categories.Bicategory.Construction.LaxSlice +import Categories.Bicategory.Construction.Spans +import Categories.Bicategory.Construction.Spans.Properties +import Categories.Bicategory.Extras +import Categories.Bicategory.Instance.Cats +import Categories.Bicategory.Instance.EnrichedCats +import Categories.Bicategory.Monad +import Categories.Bicategory.Monad.Properties +import Categories.Bicategory.Object.Product +import Categories.Bicategory.Object.Terminal +import Categories.Bicategory.Opposite +import Categories.Category +import Categories.Category.BicartesianClosed +import Categories.Category.BinaryProducts +import Categories.Category.CMonoidEnriched +import Categories.Category.Cartesian +import Categories.Category.Cartesian.Bundle +import Categories.Category.Cartesian.Monoidal +import Categories.Category.Cartesian.Properties +import Categories.Category.Cartesian.SymmetricMonoidal +import Categories.Category.CartesianClosed +import Categories.Category.CartesianClosed.Bundle +import Categories.Category.CartesianClosed.Canonical +import Categories.Category.CartesianClosed.Locally +import Categories.Category.CartesianClosed.Locally.Properties +import Categories.Category.CartesianClosed.Properties +import Categories.Category.Closed +import Categories.Category.Cocartesian +import Categories.Category.Cocartesian.Bundle +import Categories.Category.Cocomplete +import Categories.Category.Cocomplete.Finitely +import Categories.Category.Cocomplete.Finitely.Properties +import Categories.Category.Cocomplete.Properties +import Categories.Category.Complete +import Categories.Category.Complete.Finitely +import Categories.Category.Complete.Finitely.Properties +import Categories.Category.Complete.Properties +import Categories.Category.Complete.Properties.Construction +import Categories.Category.Complete.Properties.SolutionSet +import Categories.Category.Concrete +import Categories.Category.Concrete.Properties +import Categories.Category.Construction.0-Groupoid +import Categories.Category.Construction.Adjoints +import Categories.Category.Construction.Arrow +import Categories.Category.Construction.CoEilenbergMoore +import Categories.Category.Construction.CoKleisli +import Categories.Category.Construction.Cocones +import Categories.Category.Construction.Comma +import Categories.Category.Construction.Cones +import Categories.Category.Construction.Coproduct +import Categories.Category.Construction.Core +import Categories.Category.Construction.Cowedges +import Categories.Category.Construction.EilenbergMoore +import Categories.Category.Construction.Elements +import Categories.Category.Construction.EnrichedFunctors +import Categories.Category.Construction.F-Algebras +import Categories.Category.Construction.F-Coalgebras +import Categories.Category.Construction.Fin +import Categories.Category.Construction.Functors +import Categories.Category.Construction.Grothendieck +import Categories.Category.Construction.GroupAsCategory +import Categories.Category.Construction.Groups +import Categories.Category.Construction.KanComplex +import Categories.Category.Construction.KaroubiEnvelope +import Categories.Category.Construction.KaroubiEnvelope.Properties +import Categories.Category.Construction.Kleisli +import Categories.Category.Construction.LT-Models +import Categories.Category.Construction.MonoidAsCategory +import Categories.Category.Construction.MonoidalFunctors +import Categories.Category.Construction.Monoids +import Categories.Category.Construction.ObjectRestriction +import Categories.Category.Construction.Path +import Categories.Category.Construction.PathCategory +import Categories.Category.Construction.Presheaves +import Categories.Category.Construction.Properties.CoEilenbergMoore +import Categories.Category.Construction.Properties.CoKleisli +import Categories.Category.Construction.Properties.Comma +import Categories.Category.Construction.Properties.EilenbergMoore +import Categories.Category.Construction.Properties.Functors +import Categories.Category.Construction.Properties.Kleisli +import Categories.Category.Construction.Properties.Presheaves +import Categories.Category.Construction.Properties.Presheaves.Cartesian +import Categories.Category.Construction.Properties.Presheaves.CartesianClosed +import Categories.Category.Construction.Properties.Presheaves.Complete +import Categories.Category.Construction.Properties.Presheaves.FromCartesianCCC +import Categories.Category.Construction.Pullbacks +import Categories.Category.Construction.SetoidDiscrete +import Categories.Category.Construction.Spans +import Categories.Category.Construction.StrictDiscrete +import Categories.Category.Construction.SymmetricMonoidalFunctors +import Categories.Category.Construction.Thin +import Categories.Category.Construction.TwistedArrow +import Categories.Category.Construction.Wedges +import Categories.Category.Construction.mu-Bialgebras +import Categories.Category.Core +import Categories.Category.Dagger +import Categories.Category.Dagger.Construction.Discrete +import Categories.Category.Dagger.Instance.Rels +import Categories.Category.Diagram.Span +import Categories.Category.Discrete +import Categories.Category.Distributive +import Categories.Category.Duality +import Categories.Category.Equivalence +import Categories.Category.Equivalence.Preserves +import Categories.Category.Equivalence.Properties +import Categories.Category.Exact +import Categories.Category.Extensive +import Categories.Category.Extensive.Bundle +import Categories.Category.Extensive.Properties.Distributive +import Categories.Category.Finite +import Categories.Category.Finite.Fin +import Categories.Category.Finite.Fin.Construction.Discrete +import Categories.Category.Finite.Fin.Construction.Poset +import Categories.Category.Finite.Fin.Instance.Parallel +import Categories.Category.Finite.Fin.Instance.Span +import Categories.Category.Finite.Fin.Instance.Triangle +import Categories.Category.Groupoid +import Categories.Category.Groupoid.Properties +import Categories.Category.Helper +import Categories.Category.Indiscrete +import Categories.Category.Instance.Cartesians +import Categories.Category.Instance.Cats +import Categories.Category.Instance.EmptySet +import Categories.Category.Instance.FamilyOfSetoids +import Categories.Category.Instance.FinCatShapes +import Categories.Category.Instance.FinSetoids +import Categories.Category.Instance.Globe +import Categories.Category.Instance.Groupoids +import Categories.Category.Instance.KanComplexes +import Categories.Category.Instance.LawvereTheories +import Categories.Category.Instance.Monoidals +import Categories.Category.Instance.Nat +import Categories.Category.Instance.One +import Categories.Category.Instance.PartialFunctions +import Categories.Category.Instance.PointedSets +import Categories.Category.Instance.Posets +import Categories.Category.Instance.Preds +import Categories.Category.Instance.Properties.Cats +import Categories.Category.Instance.Properties.Posets +import Categories.Category.Instance.Properties.Setoids +import Categories.Category.Instance.Properties.Setoids.CCC +import Categories.Category.Instance.Properties.Setoids.Choice +import Categories.Category.Instance.Properties.Setoids.Cocomplete +import Categories.Category.Instance.Properties.Setoids.Complete +import Categories.Category.Instance.Properties.Setoids.Exact +import Categories.Category.Instance.Properties.Setoids.Extensive +import Categories.Category.Instance.Properties.Setoids.LCCC +import Categories.Category.Instance.Properties.Setoids.Limits.Canonical +import Categories.Category.Instance.Quivers +import Categories.Category.Instance.Rels +import Categories.Category.Instance.Setoids +import Categories.Category.Instance.Sets +import Categories.Category.Instance.Simplex +import Categories.Category.Instance.SimplicialSet +import Categories.Category.Instance.SimplicialSet.Properties +import Categories.Category.Instance.SingletonSet +import Categories.Category.Instance.Span +import Categories.Category.Instance.StrictCats +import Categories.Category.Instance.StrictGroupoids +import Categories.Category.Instance.Zero +import Categories.Category.Inverse +import Categories.Category.Lift +import Categories.Category.Monoidal +import Categories.Category.Monoidal.Braided +import Categories.Category.Monoidal.Braided.Properties +import Categories.Category.Monoidal.Bundle +import Categories.Category.Monoidal.Closed +import Categories.Category.Monoidal.Closed.IsClosed +import Categories.Category.Monoidal.Closed.IsClosed.Diagonal +import Categories.Category.Monoidal.Closed.IsClosed.Dinatural +import Categories.Category.Monoidal.Closed.IsClosed.Identity +import Categories.Category.Monoidal.Closed.IsClosed.L +import Categories.Category.Monoidal.Closed.IsClosed.Pentagon +import Categories.Category.Monoidal.CompactClosed +import Categories.Category.Monoidal.Construction.Endofunctors +import Categories.Category.Monoidal.Construction.Minus2 +import Categories.Category.Monoidal.Construction.Product +import Categories.Category.Monoidal.Core +import Categories.Category.Monoidal.Instance.Cats +import Categories.Category.Monoidal.Instance.One +import Categories.Category.Monoidal.Instance.Rels +import Categories.Category.Monoidal.Instance.Setoids +import Categories.Category.Monoidal.Instance.Sets +import Categories.Category.Monoidal.Instance.StrictCats +import Categories.Category.Monoidal.Interchange +import Categories.Category.Monoidal.Interchange.Braided +import Categories.Category.Monoidal.Interchange.Symmetric +import Categories.Category.Monoidal.Properties +import Categories.Category.Monoidal.Reasoning +import Categories.Category.Monoidal.Rigid +import Categories.Category.Monoidal.Star-Autonomous +import Categories.Category.Monoidal.Symmetric +import Categories.Category.Monoidal.Traced +import Categories.Category.Monoidal.Utilities +import Categories.Category.Product +import Categories.Category.Product.Properties +import Categories.Category.Regular +import Categories.Category.Restriction +import Categories.Category.Restriction.Construction.Trivial +import Categories.Category.Restriction.Instance.PartialFunctions +import Categories.Category.Restriction.Properties +import Categories.Category.RigCategory +import Categories.Category.Site +import Categories.Category.Slice +import Categories.Category.Slice.Properties +import Categories.Category.Species +import Categories.Category.Species.Constructions +import Categories.Category.SubCategory +import Categories.Category.Topos +import Categories.Category.Unbundled +import Categories.Category.Unbundled.Properties +import Categories.Category.Unbundled.Utilities +import Categories.CoYoneda +import Categories.Comonad +import Categories.Comonad.Construction.CoKleisli +import Categories.Comonad.Relative +import Categories.Diagram.Cocone +import Categories.Diagram.Cocone.Properties +import Categories.Diagram.Coend +import Categories.Diagram.Coend.Properties +import Categories.Diagram.Coequalizer +import Categories.Diagram.Coequalizer.Properties +import Categories.Diagram.Colimit +import Categories.Diagram.Colimit.DualProperties +import Categories.Diagram.Colimit.Lan +import Categories.Diagram.Colimit.Properties +import Categories.Diagram.Cone +import Categories.Diagram.Cone.Properties +import Categories.Diagram.Cowedge +import Categories.Diagram.Cowedge.Properties +import Categories.Diagram.Duality +import Categories.Diagram.End +import Categories.Diagram.End.Properties +import Categories.Diagram.Equalizer +import Categories.Diagram.Equalizer.Indexed +import Categories.Diagram.Equalizer.Limit +import Categories.Diagram.Equalizer.Properties +import Categories.Diagram.Finite +import Categories.Diagram.KernelPair +import Categories.Diagram.Limit +import Categories.Diagram.Limit.Properties +import Categories.Diagram.Limit.Ran +import Categories.Diagram.Pullback +import Categories.Diagram.Pullback.Limit +import Categories.Diagram.Pullback.Properties +import Categories.Diagram.Pushout +import Categories.Diagram.Pushout.Properties +import Categories.Diagram.ReflexivePair +import Categories.Diagram.SubobjectClassifier +import Categories.Diagram.Wedge +import Categories.Diagram.Wedge.Properties +import Categories.Double +import Categories.Double.Core +import Categories.Enriched.Category +import Categories.Enriched.Category.Opposite +import Categories.Enriched.Category.Underlying +import Categories.Enriched.Functor +import Categories.Enriched.NaturalTransformation +import Categories.Enriched.NaturalTransformation.NaturalIsomorphism +import Categories.Enriched.Over.One +import Categories.Enriched.Over.Setoids +import Categories.FreeObjects.Free +import Categories.Functor +import Categories.Functor.Algebra +import Categories.Functor.Bialgebra +import Categories.Functor.Bifunctor +import Categories.Functor.Bifunctor.Properties +import Categories.Functor.Cartesian +import Categories.Functor.Cartesian.Properties +import Categories.Functor.CartesianClosed +import Categories.Functor.Coalgebra +import Categories.Functor.Construction.Constant +import Categories.Functor.Construction.Diagonal +import Categories.Functor.Construction.FromDiscrete +import Categories.Functor.Construction.LiftAlgebras +import Categories.Functor.Construction.LiftCoalgebras +import Categories.Functor.Construction.LiftSetoids +import Categories.Functor.Construction.Limit +import Categories.Functor.Construction.ObjectRestriction +import Categories.Functor.Construction.PathsOf +import Categories.Functor.Construction.SubCategory +import Categories.Functor.Construction.SubCategory.Properties +import Categories.Functor.Construction.Zero +import Categories.Functor.Core +import Categories.Functor.DistributiveLaw +import Categories.Functor.Duality +import Categories.Functor.Equivalence +import Categories.Functor.Fibration +import Categories.Functor.Groupoid +import Categories.Functor.Hom +import Categories.Functor.Hom.Properties +import Categories.Functor.Hom.Properties.Contra +import Categories.Functor.Hom.Properties.Covariant +import Categories.Functor.IdentityOnObjects +import Categories.Functor.Instance.0-Truncation +import Categories.Functor.Instance.01-Truncation +import Categories.Functor.Instance.ConnectedComponents +import Categories.Functor.Instance.Core +import Categories.Functor.Instance.Discrete +import Categories.Functor.Instance.SetoidDiscrete +import Categories.Functor.Instance.StrictCore +import Categories.Functor.Instance.Twisted +import Categories.Functor.Instance.UnderlyingQuiver +import Categories.Functor.Limits +import Categories.Functor.Monoidal +import Categories.Functor.Monoidal.Braided +import Categories.Functor.Monoidal.Construction.Product +import Categories.Functor.Monoidal.PointwiseTensor +import Categories.Functor.Monoidal.Properties +import Categories.Functor.Monoidal.Symmetric +import Categories.Functor.Monoidal.Tensor +import Categories.Functor.Power +import Categories.Functor.Power.Functorial +import Categories.Functor.Power.NaturalTransformation +import Categories.Functor.Presheaf +import Categories.Functor.Profunctor +import Categories.Functor.Profunctor.Cograph +import Categories.Functor.Profunctor.FormalComposite +import Categories.Functor.Properties +import Categories.Functor.Representable +import Categories.Functor.Restriction +import Categories.Functor.Slice +import Categories.Functor.Slice.BaseChange +import Categories.GlobularSet +import Categories.Kan +import Categories.Kan.Duality +import Categories.Minus2-Category +import Categories.Minus2-Category.Construction.Indiscrete +import Categories.Minus2-Category.Instance.One +import Categories.Minus2-Category.Properties +import Categories.Monad +import Categories.Monad.Construction.Kleisli +import Categories.Monad.Duality +import Categories.Monad.Graded +import Categories.Monad.Idempotent +import Categories.Monad.Morphism +import Categories.Monad.Relative +import Categories.Monad.Strong +import Categories.Morphism +import Categories.Morphism.Cartesian +import Categories.Morphism.Duality +import Categories.Morphism.Extremal +import Categories.Morphism.Extremal.Properties +import Categories.Morphism.HeterogeneousEquality +import Categories.Morphism.HeterogeneousIdentity +import Categories.Morphism.HeterogeneousIdentity.Properties +import Categories.Morphism.Idempotent +import Categories.Morphism.Idempotent.Bundles +import Categories.Morphism.IsoEquiv +import Categories.Morphism.Isomorphism +import Categories.Morphism.Lifts +import Categories.Morphism.Lifts.Properties +import Categories.Morphism.Normal +import Categories.Morphism.Notation +import Categories.Morphism.Properties +import Categories.Morphism.Reasoning +import Categories.Morphism.Reasoning.Core +import Categories.Morphism.Reasoning.Iso +import Categories.Morphism.Regular +import Categories.Morphism.Regular.Properties +import Categories.Morphism.Universal +import Categories.Multi.Category.Indexed +import Categories.NaturalTransformation +import Categories.NaturalTransformation.Core +import Categories.NaturalTransformation.Dinatural +import Categories.NaturalTransformation.Equivalence +import Categories.NaturalTransformation.Extranatural +import Categories.NaturalTransformation.Hom +import Categories.NaturalTransformation.Monoidal +import Categories.NaturalTransformation.Monoidal.Braided +import Categories.NaturalTransformation.Monoidal.Symmetric +import Categories.NaturalTransformation.NaturalIsomorphism +import Categories.NaturalTransformation.NaturalIsomorphism.Equivalence +import Categories.NaturalTransformation.NaturalIsomorphism.Functors +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Braided +import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric +import Categories.NaturalTransformation.NaturalIsomorphism.Properties +import Categories.NaturalTransformation.Properties +import Categories.Object.Biproduct +import Categories.Object.Cokernel +import Categories.Object.Coproduct +import Categories.Object.Duality +import Categories.Object.Exponential +import Categories.Object.Group +import Categories.Object.Initial +import Categories.Object.InternalRelation +import Categories.Object.Kernel +import Categories.Object.Kernel.Properties +import Categories.Object.Monoid +import Categories.Object.NaturalNumbers +import Categories.Object.NaturalNumbers.Parametrized +import Categories.Object.NaturalNumbers.Properties.F-Algebras +import Categories.Object.NaturalNumbers.Properties.Parametrized +import Categories.Object.Product +import Categories.Object.Product.Construction +import Categories.Object.Product.Core +import Categories.Object.Product.Indexed +import Categories.Object.Product.Indexed.Properties +import Categories.Object.Product.Limit +import Categories.Object.Product.Morphisms +import Categories.Object.Subobject +import Categories.Object.Subobject.Properties +import Categories.Object.Terminal +import Categories.Object.Terminal.Limit +import Categories.Object.Zero +import Categories.Pseudofunctor +import Categories.Pseudofunctor.Composition +import Categories.Pseudofunctor.Hom +import Categories.Pseudofunctor.Identity +import Categories.Pseudofunctor.Instance.EnrichedUnderlying +import Categories.Tactic.Category +import Categories.Theory.Lawvere +import Categories.Theory.Lawvere.Instance.Identity +import Categories.Theory.Lawvere.Instance.Triv +import Categories.Utils.EqReasoning +import Categories.Utils.Product +import Categories.Yoneda +import Categories.Yoneda.Continuous +import Categories.Yoneda.Properties +import Data.Quiver +import Data.Quiver.Morphism +import Data.Quiver.Paths +import Function.Construct.Setoid +import Relation.Binary.PropositionalEquality.Subst.Properties \ No newline at end of file