From dad4f852c59fad3a734f39a8c0b9dbc778ea4bb2 Mon Sep 17 00:00:00 2001 From: JacquesCarette Date: Sun, 26 May 2024 15:21:42 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/agd?= =?UTF-8?q?a-categories@429cd39440c9015c47cde7b7d3a608d9b17ce9fa=20?= =?UTF-8?q?=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...Category.Restriction.Properties.Poset.html | 48 ++ ...ories.Category.Restriction.Properties.html | 188 ++++---- Everything.html | 455 +++++++++--------- index.html | 455 +++++++++--------- 4 files changed, 597 insertions(+), 549 deletions(-) create mode 100644 Categories.Category.Restriction.Properties.Poset.html diff --git a/Categories.Category.Restriction.Properties.Poset.html b/Categories.Category.Restriction.Properties.Poset.html new file mode 100644 index 00000000..100bd4f1 --- /dev/null +++ b/Categories.Category.Restriction.Properties.Poset.html @@ -0,0 +1,48 @@ + +Categories.Category.Restriction.Properties.Poset
{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Restriction using (Restriction)
+open import Relation.Binary.Bundles using (Poset)
+open import Relation.Binary.Structures using (IsPartialOrder)
+
+import Categories.Morphism.Reasoning as MR
+
+-- Every restriction category induces a partial order (the restriction order) on hom-sets
+
+module Categories.Category.Restriction.Properties.Poset {o β„“ e} {π’ž : Category o β„“ e} (R : Restriction π’ž) where  
+  open Category π’ž
+  open Restriction R
+  open Equiv
+  open HomReasoning
+  open MR π’ž using (pullΚ³; pullΛ‘)
+
+  poset : (A B : Obj) β†’ Poset β„“ e e
+  poset A B = record 
+    { Carrier = A β‡’ B 
+    ; _β‰ˆ_ = _β‰ˆ_ 
+    ; _≀_ = Ξ» f g β†’ f β‰ˆ g ∘ f ↓
+    ; isPartialOrder = record 
+      { isPreorder = record 
+        { isEquivalence = equiv
+        ; reflexive = Ξ» {x} {y} xβ‰ˆy β†’ begin 
+          x       β‰ˆΛ˜βŸ¨ pidΚ³ ⟩ 
+          x ∘ x ↓ β‰ˆβŸ¨ xβ‰ˆy ⟩∘⟨refl ⟩
+          y ∘ x ↓ ∎
+        ; trans = Ξ» {i} {j} {k} iβ‰ˆj∘i↓ jβ‰ˆk∘j↓ β†’ begin 
+          i               β‰ˆβŸ¨ iβ‰ˆj∘i↓ ⟩ 
+          j ∘ i ↓         β‰ˆβŸ¨ jβ‰ˆk∘j↓ ⟩∘⟨refl ⟩ 
+          (k ∘ j ↓) ∘ i ↓ β‰ˆβŸ¨ pullΚ³ (sym ↓-denestΚ³) ⟩ 
+          k ∘ (j ∘ i ↓) ↓ β‰ˆβŸ¨ refl⟩∘⟨ ↓-cong (sym iβ‰ˆj∘i↓) ⟩ 
+          k ∘ i ↓         ∎ 
+        } 
+      ; antisym = Ξ» {i} {j} iβ‰ˆj∘i↓ jβ‰ˆi∘j↓ β†’ begin 
+        i               β‰ˆβŸ¨ iβ‰ˆj∘i↓ ⟩ 
+        j ∘ i ↓         β‰ˆβŸ¨ jβ‰ˆi∘j↓ ⟩∘⟨refl ⟩ 
+        (i ∘ j ↓) ∘ i ↓ β‰ˆβŸ¨ pullΚ³ ↓-comm ⟩ 
+        i ∘ i ↓ ∘ j ↓   β‰ˆβŸ¨ pullΛ‘ pidΚ³ ⟩
+        i ∘ j ↓         β‰ˆΛ˜βŸ¨ jβ‰ˆi∘j↓ ⟩
+        j               ∎ 
+      } 
+    }
+
\ No newline at end of file diff --git a/Categories.Category.Restriction.Properties.html b/Categories.Category.Restriction.Properties.html index 9f5d73e3..bcd417ab 100644 --- a/Categories.Category.Restriction.Properties.html +++ b/Categories.Category.Restriction.Properties.html @@ -1,99 +1,97 @@ Categories.Category.Restriction.Properties
{-# OPTIONS --without-K --safe #-}
 
--- Some properties of Restriction Categories
-
--- The first few lemmas are from Cocket & Lack, Lemma 2.1 and 2.2
-module Categories.Category.Restriction.Properties where
-
-open import Data.Product using (Ξ£; _,_)
-open import Level using (Level; _βŠ”_)
-
-open import Categories.Category.Core using (Category)
-open import Categories.Category.Restriction using (Restriction)
-open import Categories.Category.SubCategory
-open import Categories.Morphism using (Mono)
-open import Categories.Morphism.Idempotent using (Idempotent)
-open import Categories.Morphism.Properties using (Mono-id)
-import Categories.Morphism.Reasoning as MR
-
-module _ {o β„“ e : Level} {π’ž : Category o β„“ e} (R : Restriction π’ž) where
-  open Category π’ž
-  open Restriction R
-  open HomReasoning
-  open MR π’ž using (elimΛ‘; introΚ³)
-
-  private
-    variable
-      A B C : Obj
-      f : A β‡’ B
-      g : B β‡’ C
-
-  ↓f-idempotent : (A β‡’ B) β†’ Idempotent π’ž A
-  ↓f-idempotent f = record { idem = f ↓ ; idempotent = ⟺ ↓-denestΚ³ β—‹ ↓-cong pidΚ³ }
-
-  -- a special version of ↓ being a partial left identity
-  ↓-pidΛ‘-gf : f ↓ ∘ (g ∘ f) ↓ β‰ˆ (g ∘ f) ↓
-  ↓-pidΛ‘-gf {f = f} {g = g} = begin
-    f ↓ ∘ (g ∘ f) ↓   β‰ˆβŸ¨ ↓-comm ⟩
-    (g ∘ f) ↓ ∘ f ↓   β‰ˆΛ˜βŸ¨ ↓-denestΚ³ ⟩
-    ((g ∘ f) ∘ f ↓) ↓ β‰ˆβŸ¨ ↓-cong assoc ⟩
-    (g ∘ (f ∘ f ↓)) ↓ β‰ˆβŸ¨ ↓-cong (∘-resp-β‰ˆΚ³ pidΚ³) ⟩
-    (g ∘ f) ↓ ∎
-
-  -- left denesting looks different in its conclusion
-  ↓-denestΛ‘ : (g ↓ ∘ f) ↓ β‰ˆ (g ∘ f) ↓
-  ↓-denestΛ‘ {g = g} {f = f} = begin
-    (g ↓ ∘ f) ↓       β‰ˆβŸ¨ ↓-cong ↓-skew-comm ⟩
-    (f ∘ (g ∘ f) ↓) ↓ β‰ˆβŸ¨ ↓-denestΚ³ ⟩
-    f ↓ ∘ (g ∘ f) ↓   β‰ˆβŸ¨ ↓-pidΛ‘-gf ⟩
-    (g ∘ f) ↓         ∎
-
-  ↓-idempotent : f ↓ ↓ β‰ˆ f ↓
-  ↓-idempotent {f = f} = begin
-    f ↓ ↓        β‰ˆΛ˜βŸ¨ ↓-cong identityΚ³ ⟩
-    (f ↓ ∘ id) ↓ β‰ˆβŸ¨ ↓-denestΛ‘ ⟩
-    (f ∘ id) ↓   β‰ˆβŸ¨ ↓-cong identityΚ³ ⟩
-    f ↓ ∎
-
-  ↓↓denest : (g ↓ ∘ f ↓) ↓ β‰ˆ g ↓ ∘ f ↓
-  ↓↓denest {g = g} {f = f} = begin
-    (g ↓ ∘ f ↓) ↓ β‰ˆβŸ¨ ↓-denestΚ³ ⟩
-    g ↓ ↓ ∘ f ↓   β‰ˆβŸ¨ (↓-idempotent ⟩∘⟨refl) ⟩
-    g ↓ ∘ f ↓ ∎
-
-  Monoβ‡’fβ†“β‰ˆid : Mono π’ž f β†’ f ↓ β‰ˆ id
-  Monoβ‡’fβ†“β‰ˆid {f = f} mono = mono (f ↓) id (pidΚ³ β—‹ ⟺ identityΚ³)
-
-  -- if the domain of g is at least that of f, then the restriction coincides
-  β†“βŠƒβ‡’β‰ˆ : f ∘ g ↓ β‰ˆ f β†’ f ↓ β‰ˆ f ↓ ∘ g ↓
-  β†“βŠƒβ‡’β‰ˆ {f = f} {g = g} fgβ†“β‰ˆf = ⟺ (↓-cong fgβ†“β‰ˆf) β—‹ ↓-denestΚ³
-
-  Monoβ‡’Total : Mono π’ž f β†’ total f
-  Monoβ‡’Total = Monoβ‡’fβ†“β‰ˆid
-
-  ∘-pres-total : {A B C : Obj} {f : B β‡’ C} {g : A β‡’ B} β†’ total f β†’ total g β†’ total (f ∘ g)
-  ∘-pres-total {f = f} {g = g} tf tg = begin
-    (f ∘ g) ↓   β‰ˆΛ˜βŸ¨ ↓-denestΛ‘ ⟩
-    (f ↓ ∘ g) ↓ β‰ˆβŸ¨ ↓-cong (elimΛ‘ tf) ⟩
-    g ↓         β‰ˆβŸ¨ tg ⟩
-    id ∎
-
-  total-gfβ‡’total-f : total (g ∘ f) β†’ total f
-  total-gf⇒total-f {g = g} {f = f} tgf = begin
-    f ↓             β‰ˆβŸ¨ introΚ³ tgf ⟩
-    f ↓ ∘ (g ∘ f) ↓ β‰ˆβŸ¨ ↓-pidΛ‘-gf ⟩
-    (g ∘ f) ↓       β‰ˆβŸ¨ tgf ⟩
-    id              ∎
-
-  total-SubCat : SubCat π’ž Obj
-  total-SubCat = record
-    { U = Ξ» x β†’ x
-    ; R = total
-    ; Rid = Monoβ‡’Total (Mono-id π’ž)
-    ; _∘R_ = ∘-pres-total
-    }
-
-  Total : Category o (β„“ βŠ” e) e
-  Total = SubCategory π’ž total-SubCat
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Restriction using (Restriction)
+open import Data.Product using (Ξ£; _,_)
+open import Level using (Level; _βŠ”_)
+
+open import Categories.Category.SubCategory
+open import Categories.Morphism using (Mono)
+open import Categories.Morphism.Idempotent using (Idempotent)
+open import Categories.Morphism.Properties using (Mono-id)
+import Categories.Morphism.Reasoning as MR
+
+-- Some properties of Restriction Categories
+
+-- The first few lemmas are from Cocket & Lack, Lemma 2.1 and 2.2
+module Categories.Category.Restriction.Properties {o β„“ e} {π’ž : Category o β„“ e} (R : Restriction π’ž) where
+  open Category π’ž
+  open Restriction R
+  open HomReasoning
+  open MR π’ž using (elimΛ‘; introΚ³)
+
+  private
+    variable
+      A B C : Obj
+      f : A β‡’ B
+      g : B β‡’ C
+
+  ↓f-idempotent : (A β‡’ B) β†’ Idempotent π’ž A
+  ↓f-idempotent f = record { idem = f ↓ ; idempotent = ⟺ ↓-denestΚ³ β—‹ ↓-cong pidΚ³ }
+
+  -- a special version of ↓ being a partial left identity
+  ↓-pidΛ‘-gf : f ↓ ∘ (g ∘ f) ↓ β‰ˆ (g ∘ f) ↓
+  ↓-pidΛ‘-gf {f = f} {g = g} = begin
+    f ↓ ∘ (g ∘ f) ↓   β‰ˆβŸ¨ ↓-comm ⟩
+    (g ∘ f) ↓ ∘ f ↓   β‰ˆΛ˜βŸ¨ ↓-denestΚ³ ⟩
+    ((g ∘ f) ∘ f ↓) ↓ β‰ˆβŸ¨ ↓-cong assoc ⟩
+    (g ∘ (f ∘ f ↓)) ↓ β‰ˆβŸ¨ ↓-cong (∘-resp-β‰ˆΚ³ pidΚ³) ⟩
+    (g ∘ f) ↓ ∎
+
+  -- left denesting looks different in its conclusion
+  ↓-denestΛ‘ : (g ↓ ∘ f) ↓ β‰ˆ (g ∘ f) ↓
+  ↓-denestΛ‘ {g = g} {f = f} = begin
+    (g ↓ ∘ f) ↓       β‰ˆβŸ¨ ↓-cong ↓-skew-comm ⟩
+    (f ∘ (g ∘ f) ↓) ↓ β‰ˆβŸ¨ ↓-denestΚ³ ⟩
+    f ↓ ∘ (g ∘ f) ↓   β‰ˆβŸ¨ ↓-pidΛ‘-gf ⟩
+    (g ∘ f) ↓         ∎
+
+  ↓-idempotent : f ↓ ↓ β‰ˆ f ↓
+  ↓-idempotent {f = f} = begin
+    f ↓ ↓        β‰ˆΛ˜βŸ¨ ↓-cong identityΚ³ ⟩
+    (f ↓ ∘ id) ↓ β‰ˆβŸ¨ ↓-denestΛ‘ ⟩
+    (f ∘ id) ↓   β‰ˆβŸ¨ ↓-cong identityΚ³ ⟩
+    f ↓ ∎
+
+  ↓↓denest : (g ↓ ∘ f ↓) ↓ β‰ˆ g ↓ ∘ f ↓
+  ↓↓denest {g = g} {f = f} = begin
+    (g ↓ ∘ f ↓) ↓ β‰ˆβŸ¨ ↓-denestΚ³ ⟩
+    g ↓ ↓ ∘ f ↓   β‰ˆβŸ¨ (↓-idempotent ⟩∘⟨refl) ⟩
+    g ↓ ∘ f ↓ ∎
+
+  Monoβ‡’fβ†“β‰ˆid : Mono π’ž f β†’ f ↓ β‰ˆ id
+  Monoβ‡’fβ†“β‰ˆid {f = f} mono = mono (f ↓) id (pidΚ³ β—‹ ⟺ identityΚ³)
+
+  -- if the domain of g is at least that of f, then the restriction coincides
+  β†“βŠƒβ‡’β‰ˆ : f ∘ g ↓ β‰ˆ f β†’ f ↓ β‰ˆ f ↓ ∘ g ↓
+  β†“βŠƒβ‡’β‰ˆ {f = f} {g = g} fgβ†“β‰ˆf = ⟺ (↓-cong fgβ†“β‰ˆf) β—‹ ↓-denestΚ³
+
+  Monoβ‡’Total : Mono π’ž f β†’ total f
+  Monoβ‡’Total = Monoβ‡’fβ†“β‰ˆid
+
+  ∘-pres-total : {A B C : Obj} {f : B β‡’ C} {g : A β‡’ B} β†’ total f β†’ total g β†’ total (f ∘ g)
+  ∘-pres-total {f = f} {g = g} tf tg = begin
+    (f ∘ g) ↓   β‰ˆΛ˜βŸ¨ ↓-denestΛ‘ ⟩
+    (f ↓ ∘ g) ↓ β‰ˆβŸ¨ ↓-cong (elimΛ‘ tf) ⟩
+    g ↓         β‰ˆβŸ¨ tg ⟩
+    id ∎
+
+  total-gfβ‡’total-f : total (g ∘ f) β†’ total f
+  total-gf⇒total-f {g = g} {f = f} tgf = begin
+    f ↓             β‰ˆβŸ¨ introΚ³ tgf ⟩
+    f ↓ ∘ (g ∘ f) ↓ β‰ˆβŸ¨ ↓-pidΛ‘-gf ⟩
+    (g ∘ f) ↓       β‰ˆβŸ¨ tgf ⟩
+    id              ∎
+
+  total-SubCat : SubCat π’ž Obj
+  total-SubCat = record
+    { U = Ξ» x β†’ x
+    ; R = total
+    ; Rid = Monoβ‡’Total (Mono-id π’ž)
+    ; _∘R_ = ∘-pres-total
+    }
+
+  Total : Category o (β„“ βŠ” e) e
+  Total = SubCategory π’ž total-SubCat
\ No newline at end of file diff --git a/Everything.html b/Everything.html index a9b82773..4df07b7e 100644 --- a/Everything.html +++ b/Everything.html @@ -239,231 +239,232 @@ 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.Morphism -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.Commutative -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.Monad.Strong.Properties -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.Category.Restriction.Properties.Poset +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.Morphism +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.Commutative +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.Monad.Strong.Properties +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 c2e7a482..dae24faa 100644 --- a/index.html +++ b/index.html @@ -245,231 +245,232 @@ 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.Morphism -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.Commutative -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.Monad.Strong.Properties -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.Category.Restriction.Properties.Poset +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.Morphism +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.Commutative +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.Monad.Strong.Properties +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