diff --git a/Categories.Category.Monoidal.Braided.Properties.html b/Categories.Category.Monoidal.Braided.Properties.html index 3af9ff746..0599f8801 100644 --- a/Categories.Category.Monoidal.Braided.Properties.html +++ b/Categories.Category.Monoidal.Braided.Properties.html @@ -157,4 +157,24 @@ ≈ λ⇒ ⟩ inv-braiding-coherence = ⟺ (switch-fromtoʳ σ braiding-coherence) + +-- Reversing a ternary product via braiding commutes with the associator. + +assoc-reverse : [ X ⊗₀ (Y ⊗₀ Z) ⇒ (X ⊗₀ Y) ⊗₀ Z ]⟨ + id ⊗₁ σ⇒ ⇒⟨ X ⊗₀ (Z ⊗₀ Y) ⟩ + σ⇒ ⇒⟨ (Z ⊗₀ Y) ⊗₀ X ⟩ + α⇒ ⇒⟨ Z ⊗₀ (Y ⊗₀ X) ⟩ + id ⊗₁ σ⇐ ⇒⟨ Z ⊗₀ (X ⊗₀ Y) ⟩ + σ⇐ + ≈ α⇐ + ⟩ +assoc-reverse = begin + σ⇐ ∘ id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒ ∘ id ⊗₁ σ⇒ ≈˘⟨ refl⟩∘⟨ assoc²' ⟩ + σ⇐ ∘ (id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒) ∘ id ⊗₁ σ⇒ ≈⟨ refl⟩∘⟨ pushˡ hex₁' ⟩ + σ⇐ ∘ (α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ σ⇒ ≈⟨ refl⟩∘⟨ pullʳ (sym-assoc ○ hexagon₂) ⟩ + σ⇐ ∘ α⇒ ∘ (α⇐ ∘ σ⇒) ∘ α⇐ ≈⟨ refl⟩∘⟨ pullˡ (cancelˡ associator.isoʳ) ⟩ + σ⇐ ∘ σ⇒ ∘ α⇐ ≈⟨ cancelˡ (braiding.iso.isoˡ _) ⟩ + α⇐ ∎ + where + hex₁' = conjugate-from associator (idᵢ ⊗ᵢ σ) (⟺ (hexagon₁ ○ sym-assoc)) \ No newline at end of file diff --git a/Categories.Category.Monoidal.Construction.Reverse.html b/Categories.Category.Monoidal.Construction.Reverse.html new file mode 100644 index 000000000..92216c923 --- /dev/null +++ b/Categories.Category.Monoidal.Construction.Reverse.html @@ -0,0 +1,128 @@ + +Categories.Category.Monoidal.Construction.Reverse
{-# OPTIONS --without-K --safe #-}
+
+module Categories.Category.Monoidal.Construction.Reverse where
+
+-- The reverse monoidal category of a monoidal category V has the same
+-- underlying category and unit as V but reversed monoidal product,
+-- and similarly for tensors of morphisms.
+--
+-- https://ncatlab.org/nlab/show/reverse+monoidal+category
+
+open import Level using (_⊔_)
+open import Data.Product using (_,_; swap)
+import Function
+
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal
+open import Categories.Category.Monoidal.Braided using (Braided)
+import Categories.Category.Monoidal.Braided.Properties as BraidedProperties
+import Categories.Category.Monoidal.Symmetric.Properties as SymmetricProperties
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+import Categories.Category.Monoidal.Utilities as MonoidalUtils
+import Categories.Morphism as Morphism
+import Categories.Morphism.Reasoning as MorphismReasoning
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
+
+open Category using (Obj)
+
+module _ {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where
+
+  private module M = Monoidal M
+
+  open Function using (_∘_)
+  open Category C using (sym-assoc)
+  open Category.HomReasoning C using (⟺; _○_)
+  open Morphism C using (module ≅)
+  open MorphismReasoning C using (switch-fromtoʳ)
+  open MonoidalUtils M using (pentagon-inv)
+
+  ⊗ : Bifunctor C C C
+  ⊗ = record
+    { F₀           = M.⊗.₀ ∘ swap
+    ; F₁           = M.⊗.₁ ∘ swap
+    ; identity     = M.⊗.identity
+    ; homomorphism = M.⊗.homomorphism
+    ; F-resp-≈     = M.⊗.F-resp-≈ ∘ swap
+    }
+
+  Reverse-Monoidal : Monoidal C
+  Reverse-Monoidal = record
+    { ⊗                    = ⊗
+    ; unit                 = M.unit
+    ; unitorˡ              = M.unitorʳ
+    ; unitorʳ              = M.unitorˡ
+    ; associator           = ≅.sym M.associator
+    ; unitorˡ-commute-from = M.unitorʳ-commute-from
+    ; unitorˡ-commute-to   = M.unitorʳ-commute-to
+    ; unitorʳ-commute-from = M.unitorˡ-commute-from
+    ; unitorʳ-commute-to   = M.unitorˡ-commute-to
+    ; assoc-commute-from   = M.assoc-commute-to
+    ; assoc-commute-to     = M.assoc-commute-from
+    ; triangle             = ⟺ (switch-fromtoʳ M.associator M.triangle)
+    ; pentagon             = sym-assoc ○ pentagon-inv
+    }
+
+module _ {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} where
+
+  open Category C using (assoc; sym-assoc)
+  open Category.HomReasoning C using (_○_)
+
+  -- The reverse of a braided category is again braided.
+
+  Reverse-Braided : Braided M → Braided (Reverse-Monoidal M)
+  Reverse-Braided BM = record
+    { braiding  = niHelper (record
+      { η       = braiding.⇐.η
+      ; η⁻¹     = braiding.⇒.η
+      ; commute = braiding.⇐.commute
+      ; iso     = λ XY → record
+        { isoˡ  = braiding.iso.isoʳ XY
+        ; isoʳ  = braiding.iso.isoˡ XY }
+      })
+    ; hexagon₁  = sym-assoc ○ hexagon₁-inv ○ assoc
+    ; hexagon₂  = assoc ○ hexagon₂-inv ○ sym-assoc
+    }
+    where
+      open Braided BM
+      open BraidedProperties BM using (hexagon₁-inv; hexagon₂-inv)
+
+  -- The reverse of a symmetric category is again symmetric.
+
+  Reverse-Symmetric : Symmetric M → Symmetric (Reverse-Monoidal M)
+  Reverse-Symmetric SM = record
+    { braided     = Reverse-Braided braided
+    ; commutative = inv-commutative
+    }
+    where
+      open Symmetric SM using (braided)
+      open SymmetricProperties SM using (inv-commutative)
+
+-- Bundled versions of the above
+
+Reverse-MonoidalCategory : ∀ {o ℓ e} → MonoidalCategory o ℓ e → MonoidalCategory o ℓ e
+Reverse-MonoidalCategory C = record
+  { U        = U
+  ; monoidal = Reverse-Monoidal monoidal
+  }
+  where open MonoidalCategory C
+
+Reverse-BraidedMonoidalCategory : ∀ {o ℓ e} →
+  BraidedMonoidalCategory o ℓ e → BraidedMonoidalCategory o ℓ e
+Reverse-BraidedMonoidalCategory C = record
+  { U        = U
+  ; monoidal = Reverse-Monoidal monoidal
+  ; braided  = Reverse-Braided braided
+  }
+  where open BraidedMonoidalCategory C
+
+Reverse-SymmetricMonoidalCategory : ∀ {o ℓ e} →
+  SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalCategory o ℓ e
+Reverse-SymmetricMonoidalCategory C = record
+  { U         = U
+  ; monoidal  = Reverse-Monoidal monoidal
+  ; symmetric = Reverse-Symmetric symmetric
+  }
+  where open SymmetricMonoidalCategory C
+
\ No newline at end of file diff --git a/Categories.Category.Monoidal.Symmetric.Properties.html b/Categories.Category.Monoidal.Symmetric.Properties.html new file mode 100644 index 000000000..8b76e3bc0 --- /dev/null +++ b/Categories.Category.Monoidal.Symmetric.Properties.html @@ -0,0 +1,31 @@ + +Categories.Category.Monoidal.Symmetric.Properties
{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+
+module Categories.Category.Monoidal.Symmetric.Properties
+  {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (SM : Symmetric M) where
+
+open import Data.Product using (_,_)
+
+import Categories.Category.Monoidal.Braided.Properties as BraidedProperties
+open import Categories.Morphism.Reasoning C
+
+open Category C
+open HomReasoning
+open Symmetric SM
+
+-- Shorthands for the braiding
+
+open BraidedProperties braided public using (module Shorthands)
+
+-- Extra properties of the braiding in a symmetric monoidal category
+
+braiding-selfInverse : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X)
+braiding-selfInverse = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _)
+
+inv-commutative : ∀ {X Y} → braiding.⇐.η (X , Y) ∘ braiding.⇐.η (Y , X) ≈ id
+inv-commutative = ∘-resp-≈ braiding-selfInverse braiding-selfInverse ○ commutative
+
\ No newline at end of file diff --git a/Categories.Monad.Commutative.html b/Categories.Monad.Commutative.html new file mode 100644 index 000000000..1dcf9c2ca --- /dev/null +++ b/Categories.Monad.Commutative.html @@ -0,0 +1,46 @@ + +Categories.Monad.Commutative
{-# OPTIONS --without-K --safe #-}
+
+-- Commutative Monad on a braided monoidal category
+-- https://ncatlab.org/nlab/show/commutative+monad
+
+module Categories.Monad.Commutative where
+
+open import Level
+open import Data.Product using (_,_)
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Monad using (Monad)
+open import Categories.Monad.Strong using (StrongMonad; RightStrength; Strength)
+import Categories.Monad.Strong.Properties as StrongProps
+
+private
+  variable
+    o ℓ e : Level
+
+module _ {C : Category o ℓ e} {V : Monoidal C} (B : Braided V) where
+  record Commutative (LSM : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where
+    open Category C using (_⇒_; _∘_; _≈_)
+    open Braided B using (_⊗₀_)
+    open StrongMonad LSM using (M; strength)
+    open StrongProps.Left.Shorthands strength
+
+    rightStrength : RightStrength V M
+    rightStrength = StrongProps.Strength⇒RightStrength B strength
+
+    open StrongProps.Right.Shorthands rightStrength
+
+    field
+      commutes : ∀ {X Y} → M.μ.η (X ⊗₀ Y) ∘ M.F.₁ τ ∘ σ ≈ M.μ.η (X ⊗₀ Y) ∘ M.F.₁ σ ∘ τ
+
+  record CommutativeMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      strongMonad : StrongMonad V
+      commutative : Commutative strongMonad
+
+    open StrongMonad strongMonad public
+    open Commutative commutative public
+
+
\ No newline at end of file diff --git a/Categories.Monad.Strong.Properties.html b/Categories.Monad.Strong.Properties.html new file mode 100644 index 000000000..42518e78a --- /dev/null +++ b/Categories.Monad.Strong.Properties.html @@ -0,0 +1,269 @@ + +Categories.Monad.Strong.Properties
{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category; module Commutation)
+
+module Categories.Monad.Strong.Properties {o ℓ e} {C : Category o ℓ e} where
+
+open import Level
+open import Data.Product using (_,_; _×_)
+
+import Categories.Category.Construction.Core as Core
+open import Categories.Category.Product
+open import Categories.Functor renaming (id to idF)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Category.Monoidal.Construction.Reverse
+  using (Reverse-Monoidal; Reverse-Braided)
+import Categories.Category.Monoidal.Braided.Properties as BraidedProps
+import Categories.Category.Monoidal.Reasoning as MonoidalReasoning
+import Categories.Category.Monoidal.Utilities as MonoidalUtils
+open import Categories.Monad using (Monad)
+open import Categories.Monad.Strong using (Strength; RightStrength; StrongMonad; RightStrongMonad)
+import Categories.Morphism.Reasoning as MR
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+
+-- A left strength is a right strength in the reversed category.
+
+rightInReversed : {V : Monoidal C} {M : Monad C} →
+                  Strength V M → RightStrength (Reverse-Monoidal V) M
+rightInReversed left = record
+  { strengthen     = ntHelper (record
+    { η            = λ{ (X , Y) → strengthen.η (Y , X)       }
+    ; commute      = λ{ (f , g) → strengthen.commute (g , f) }
+    })
+  ; identityˡ      = identityˡ
+  ; η-comm         = η-comm
+  ; μ-η-comm       = μ-η-comm
+  ; strength-assoc = strength-assoc
+  }
+  where open Strength left
+
+-- A right strength is a left strength in the reversed category.
+
+leftInReversed : {V : Monoidal C} {M : Monad C} →
+                 RightStrength V M → Strength (Reverse-Monoidal V) M
+leftInReversed right = record
+  { strengthen     = ntHelper (record
+    { η            = λ{ (X , Y) → strengthen.η (Y , X)       }
+    ; commute      = λ{ (f , g) → strengthen.commute (g , f) }
+    })
+  ; identityˡ      = identityˡ
+  ; η-comm         = η-comm
+  ; μ-η-comm       = μ-η-comm
+  ; strength-assoc = strength-assoc
+  }
+  where open RightStrength right
+
+open Category C hiding (identityˡ)
+open MR C
+open Commutation C
+
+module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where
+  open Category C using (identityˡ)
+  open Monoidal V using (_⊗₀_)
+  open MonoidalUtils V using (_⊗ᵢ_)
+  open Core.Shorthands C             -- for idᵢ, _∘ᵢ_, ...
+  open MonoidalUtils.Shorthands V    -- for λ⇒, ρ⇒, α⇒, ...
+  open MonoidalReasoning V
+  open Monad M using (F; μ; η)
+
+  private
+    module left = Strength left
+    variable
+      X Y Z W : Obj
+
+  module Shorthands where
+    module σ = left.strengthen
+
+    σ : ∀ {X Y} → X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊗₀ Y)
+    σ {X} {Y} = σ.η (X , Y)
+
+  open Shorthands
+
+  -- In a braided monoidal category, a left strength induces a right strength.
+
+  module _ (BV : Braided V) where
+    open Braided BV hiding (_⊗₀_)
+    open BraidedProps BV using (braiding-coherence; inv-braiding-coherence; assoc-reverse)
+    open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐)
+
+    private
+      τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y)
+      τ {X} {Y} = F.₁ B⇐ ∘ σ ∘ B⇒
+
+      τ-commute : (f : X ⇒ Z) (g : Y ⇒ W) → τ ∘ (F.₁ f ⊗₁ g) ≈ F.₁ (f ⊗₁ g) ∘ τ
+      τ-commute f g = begin
+        (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ (F.₁ f ⊗₁ g)   ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩
+        F.₁ B⇐ ∘ σ ∘ ((g ⊗₁ F.₁ f) ∘ B⇒)   ≈⟨ refl⟩∘⟨ pullˡ (σ.commute (g , f)) ⟩
+        F.₁ B⇐ ∘ (F.₁ (g ⊗₁ f) ∘ σ) ∘ B⇒   ≈˘⟨ pushˡ (pushˡ (F.homomorphism)) ⟩
+        (F.₁ (B⇐ ∘ (g ⊗₁ f)) ∘ σ) ∘ B⇒     ≈⟨ pushˡ (F.F-resp-≈ (braiding.⇐.commute (f , g)) ⟩∘⟨refl) ⟩
+        F.₁ ((f ⊗₁ g) ∘ B⇐) ∘ σ ∘ B⇒       ≈⟨ pushˡ F.homomorphism ⟩
+        F.₁ (f ⊗₁ g) ∘ F.₁ B⇐ ∘ σ ∘ B⇒     ∎
+
+    right-strengthen : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗)
+    right-strengthen = ntHelper (record
+      { η = λ _ → τ
+      ; commute = λ (f , g) → τ-commute f g
+      })
+
+    private module τ = NaturalTransformation right-strengthen
+
+    -- The strengths commute with braiding.
+
+    left-right-braiding-comm : ∀ {X Y} → F.₁ B⇐ ∘ σ {X} {Y} ≈ τ ∘ B⇐
+    left-right-braiding-comm = begin
+      F.₁ B⇐ ∘ σ               ≈˘⟨ pullʳ (cancelʳ (braiding.iso.isoʳ _)) ⟩
+      (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ B⇐   ∎
+
+    right-left-braiding-comm : ∀ {X Y} → F.₁ B⇒ ∘ τ {X} {Y} ≈ σ ∘ B⇒
+    right-left-braiding-comm = begin
+      F.₁ B⇒ ∘ (F.₁ B⇐ ∘ σ ∘ B⇒)   ≈˘⟨ pushˡ F.homomorphism ⟩
+      F.₁ (B⇒ ∘ B⇐) ∘ σ ∘ B⇒       ≈⟨ F.F-resp-≈ (braiding.iso.isoʳ _) ⟩∘⟨refl ⟩
+      F.₁ id ∘ σ ∘ B⇒              ≈⟨ elimˡ F.identity ⟩
+      σ ∘ B⇒                       ∎
+
+    right-identityˡ : ∀ {X} → F.₁ ρ⇒ ∘ τ {X} {unit} ≈ ρ⇒
+    right-identityˡ = begin
+      F.₁ ρ⇒ ∘ F.₁ B⇐ ∘ σ ∘ B⇒  ≈⟨ pullˡ (⟺ F.homomorphism) ⟩
+      F.₁ (ρ⇒ ∘ B⇐) ∘ σ ∘ B⇒    ≈⟨ F.F-resp-≈ (inv-braiding-coherence) ⟩∘⟨refl ⟩
+      F.₁ λ⇒ ∘ σ ∘ B⇒           ≈⟨ pullˡ left.identityˡ ⟩
+      λ⇒ ∘ B⇒                   ≈⟨ braiding-coherence ⟩
+      ρ⇒                        ∎
+
+    -- The induced right strength commutes with the monad unit.
+
+    right-η-comm : ∀ {X Y} → τ ∘ η.η X ⊗₁ id ≈ η.η (X ⊗₀ Y)
+    right-η-comm {X} {Y} = begin
+      (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ (η.η X ⊗₁ id)  ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩
+      F.₁ B⇐ ∘ σ ∘ (id ⊗₁ η.η X) ∘ B⇒  ≈⟨ refl⟩∘⟨ pullˡ left.η-comm ⟩
+      F.₁ B⇐ ∘ η.η (Y ⊗₀ X) ∘ B⇒       ≈⟨ pullˡ (⟺ (η.commute B⇐)) ⟩
+      (η.η (X ⊗₀ Y) ∘ B⇐) ∘ B⇒         ≈⟨ cancelʳ (braiding.iso.isoˡ _) ⟩
+      η.η (X ⊗₀ Y)                     ∎
+
+    -- The induced right strength commutes with the monad multiplication.
+
+    right-μ-η-comm : ∀ {X Y} → μ.η (X ⊗₀ Y) ∘ F.₁ τ ∘ τ ≈ τ ∘ μ.η X ⊗₁ id
+    right-μ-η-comm {X} {Y} = begin
+      μ.η (X ⊗₀ Y) ∘ F.₁ τ ∘ F.₁ B⇐ ∘ σ ∘ B⇒           ≈⟨ refl⟩∘⟨ pullˡ (⟺ F.homomorphism) ⟩
+      μ.η (X ⊗₀ Y) ∘ F.₁ (τ ∘ B⇐) ∘ σ ∘ B⇒             ≈⟨ refl⟩∘⟨ (F.F-resp-≈ (pullʳ (cancelʳ (braiding.iso.isoʳ _))) ⟩∘⟨refl) ⟩
+      μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ B⇐ ∘ σ) ∘ σ ∘ B⇒         ≈⟨ refl⟩∘⟨ F.homomorphism ⟩∘⟨refl ⟩
+      μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ B⇐) ∘ F.₁ σ) ∘ σ ∘ B⇒   ≈⟨ pullˡ (pullˡ (μ.commute B⇐)) ⟩
+      ((F.₁ B⇐ ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ σ) ∘ σ ∘ B⇒       ≈⟨ assoc² ○ (refl⟩∘⟨ ⟺ assoc²') ⟩
+      F.₁ B⇐ ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ σ ∘ σ) ∘ B⇒         ≈⟨ refl⟩∘⟨ pushˡ left.μ-η-comm ⟩
+      F.₁ B⇐ ∘ σ ∘ (id ⊗₁ μ.η X) ∘ B⇒                  ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩
+      τ ∘ μ.η X ⊗₁ id ∎
+
+    -- The induced right strength commutes with the associator
+
+    right-strength-assoc : [ F.₀ X ⊗₀ (Y ⊗₀ Z)  ⇒  F.₀ ((X ⊗₀ Y) ⊗₀ Z) ]⟨
+                             τ                  ⇒⟨ F.₀ (X ⊗₀ (Y ⊗₀ Z)) ⟩
+                             F.₁ α⇐
+                           ≈ α⇐                 ⇒⟨ (F.₀ X ⊗₀ Y) ⊗₀ Z ⟩
+                             τ ⊗₁ id            ⇒⟨ F.₀ (X ⊗₀ Y) ⊗₀ Z ⟩
+                             τ
+                           ⟩
+    right-strength-assoc = begin
+        F.₁ α⇐ ∘ τ
+      ≈˘⟨ F.F-resp-≈ assoc-reverse ⟩∘⟨refl ⟩
+        F.₁ (B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ
+      ≈⟨ pushˡ F.homomorphism ⟩
+        F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ
+      ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
+        F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ (α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ
+      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
+        F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ (B⇒ ∘ id ⊗₁ B⇒) ∘ τ
+      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
+        F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ τ
+      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ τ.commute (id , B⇒) ⟩
+        F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ τ ∘ F.₁ id ⊗₁ B⇒
+      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ right-left-braiding-comm ⟩
+        F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ σ ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒
+      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ left.strength-assoc ⟩
+        F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ σ ∘ (id ⊗₁ σ ∘ α⇒) ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒
+      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ (refl⟩∘⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl) ⟩
+        F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ σ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒
+      ≈˘⟨ refl⟩∘⟨ extendʳ (σ.commute (id , B⇐)) ⟩
+        F.₁ B⇐ ∘ σ ∘ id ⊗₁ F.₁ B⇐ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒
+      ≈⟨ extendʳ left-right-braiding-comm ⟩
+        τ ∘ B⇐ ∘ id ⊗₁ F.₁ B⇐ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒
+      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (parallel Equiv.refl left-right-braiding-comm) ⟩
+        τ ∘ B⇐ ∘ id ⊗₁ τ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒
+      ≈⟨ refl⟩∘⟨ extendʳ (braiding.⇐.commute (τ , id)) ⟩
+        τ ∘ τ ⊗₁ id ∘ B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒
+      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Equiv.refl ⟩∘⟨ (refl⟩⊗⟨ Equiv.refl) ⟩∘⟨refl ⟩
+        τ ∘ τ ⊗₁ id ∘ B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒
+      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-reverse ⟩
+        τ ∘ τ ⊗₁ id ∘ α⇐
+      ∎
+
+    -- The induced right strength
+
+    right : RightStrength V M
+    right = record
+      { strengthen     = right-strengthen
+      ; identityˡ      = right-identityˡ
+      ; η-comm         = right-η-comm
+      ; μ-η-comm       = right-μ-η-comm
+      ; strength-assoc = right-strength-assoc
+      }
+
+Strength⇒RightStrength : {V : Monoidal C} {M : Monad C} →
+                         Braided V → Strength V M → RightStrength V M
+Strength⇒RightStrength BV left = Left.right left BV
+
+StrongMonad⇒RightStrongMonad : {V : Monoidal C} →
+                               Braided V → StrongMonad V → RightStrongMonad V
+StrongMonad⇒RightStrongMonad BV SM = record
+  { M             = M
+  ; rightStrength = Strength⇒RightStrength BV strength
+  }
+  where open StrongMonad SM
+
+module Right {V : Monoidal C} {M : Monad C} (right : RightStrength V M) where
+  open Monoidal V using (_⊗₀_)
+  open Monad M using (F)
+
+  module Shorthands where
+    module τ = RightStrength.strengthen right
+
+    τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y)
+    τ {X} {Y} = τ.η (X , Y)
+
+-- In a braided monoidal category, a right strength induces a left strength.
+
+RightStrength⇒Strength : {V : Monoidal C} {M : Monad C} →
+                         Braided V → RightStrength V M → Strength V M
+RightStrength⇒Strength {V} {M} BV right = record
+  { strengthen     = strengthen
+  ; identityˡ      = identityˡ
+  ; η-comm         = η-comm
+  ; μ-η-comm       = μ-η-comm
+  ; strength-assoc = strength-assoc
+  }
+  where
+    left₁ : Strength (Reverse-Monoidal V) M
+    left₁ = leftInReversed right
+
+    right₂ : RightStrength (Reverse-Monoidal V) M
+    right₂ = Strength⇒RightStrength (Reverse-Braided BV) left₁
+
+    -- Note: this is almost what we need, but Reverse-Monoidal is
+    -- not a strict involution (some of the coherence laws are
+    -- have proofs that are not strictly identical to their
+    -- original counterparts). But this does not matter
+    -- structurally, so we can just re-package the components we
+    -- need.
+    left₂ : Strength (Reverse-Monoidal (Reverse-Monoidal V)) M
+    left₂ = leftInReversed right₂
+
+    open Strength left₂
+
+RightStrongMonad⇒StrongMonad : {V : Monoidal C} →
+                               Braided V → RightStrongMonad V → StrongMonad V
+RightStrongMonad⇒StrongMonad BV RSM = record
+  { M        = M
+  ; strength = RightStrength⇒Strength BV rightStrength
+  }
+  where open RightStrongMonad RSM
+
\ No newline at end of file diff --git a/Categories.Monad.Strong.html b/Categories.Monad.Strong.html index 7801f0047..a9bada844 100644 --- a/Categories.Monad.Strong.html +++ b/Categories.Monad.Strong.html @@ -23,39 +23,78 @@ variable o ℓ e : Level -record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where - open Category C - open Monoidal V - private - module M = Monad M - open M using (F) - open NaturalTransformation M.η using (η) - open NaturalTransformation M.μ renaming (η to μ) - open Functor F - field - strengthen : NaturalTransformation (⊗ ∘F (idF ⁂ F)) (F ∘F ⊗) - - module strengthen = NaturalTransformation strengthen - private - module t = strengthen - - field - -- strengthening with 1 is irrelevant - identityˡ : {A : Obj} → F₁ (unitorˡ.from) ∘ t.η (unit , A) ≈ unitorˡ.from - -- commutes with unit (of monad) - η-comm : {A B : Obj} → t.η (A , B) ∘ (id ⊗₁ η B) ≈ η (A ⊗₀ B) - -- strength commutes with multiplication - μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (t.η (A , B)) ∘ t.η (A , F₀ B) - ≈ t.η (A , B) ∘ id ⊗₁ μ B - -- consecutive applications of strength commute (i.e. strength is associative) - strength-assoc : {A B C : Obj} → F₁ associator.from ∘ t.η (A ⊗₀ B , C) - ≈ t.η (A , B ⊗₀ C) ∘ id ⊗₁ t.η (B , C) ∘ associator.from - -record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where - field - M : Monad C - strength : Strength V M - - module M = Monad M - open Strength strength public - \ No newline at end of file +-- (left) strength on a monad + +record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where + open Category C + open Monoidal V + private + module M = Monad M + open M using (F) + open NaturalTransformation M.η using (η) + open NaturalTransformation M.μ renaming (η to μ) + open Functor F + field + strengthen : NaturalTransformation (⊗ ∘F (idF ⁂ F)) (F ∘F ⊗) + + module strengthen = NaturalTransformation strengthen + private + module t = strengthen + + field + -- strengthening with 1 is irrelevant + identityˡ : {A : Obj} → F₁ (unitorˡ.from) ∘ t.η (unit , A) ≈ unitorˡ.from + -- commutes with unit (of monad) + η-comm : {A B : Obj} → t.η (A , B) ∘ (id ⊗₁ η B) ≈ η (A ⊗₀ B) + -- strength commutes with multiplication + μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (t.η (A , B)) ∘ t.η (A , F₀ B) + ≈ t.η (A , B) ∘ (id ⊗₁ μ B) + -- consecutive applications of strength commute (i.e. strength is associative) + strength-assoc : {A B C : Obj} → F₁ associator.from ∘ t.η (A ⊗₀ B , C) + ≈ t.η (A , B ⊗₀ C) ∘ (id ⊗₁ t.η (B , C)) ∘ associator.from + +record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where + field + M : Monad C + strength : Strength V M + + module M = Monad M + open Strength strength public + +-- right strength + +record RightStrength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where + open Category C + open Monoidal V + private + module M = Monad M + open M using (F) + open NaturalTransformation M.η using (η) + open NaturalTransformation M.μ renaming (η to μ) + open Functor F + field + strengthen : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗) + + module strengthen = NaturalTransformation strengthen + private + module u = strengthen + + field + -- strengthening with 1 is irrelevant + identityˡ : {A : Obj} → F₁ (unitorʳ.from) ∘ u.η (A , unit) ≈ unitorʳ.from + -- commutes with unit (of monad) + η-comm : {A B : Obj} → u.η (A , B) ∘ (η A ⊗₁ id) ≈ η (A ⊗₀ B) + -- strength commutes with multiplication + μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (u.η (A , B)) ∘ u.η (F₀ A , B) + ≈ u.η (A , B) ∘ (μ A ⊗₁ id) + -- consecutive applications of strength commute (i.e. strength is associative) + strength-assoc : {A B C : Obj} → F₁ associator.to ∘ u.η (A , B ⊗₀ C) + ≈ u.η (A ⊗₀ B , C) ∘ (u.η (A , B) ⊗₁ id) ∘ associator.to + +record RightStrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where + field + M : Monad C + rightStrength : RightStrength V M + + module M = Monad M + open RightStrength rightStrength public \ No newline at end of file diff --git a/Everything.html b/Everything.html index c453864c7..231643639 100644 --- a/Everything.html +++ b/Everything.html @@ -212,252 +212,256 @@ 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 +import Categories.Category.Monoidal.Construction.Reverse +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.Symmetric.Properties +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.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 200e0387e..c568e6406 100644 --- a/index.html +++ b/index.html @@ -218,252 +218,256 @@ 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 +import Categories.Category.Monoidal.Construction.Reverse +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.Symmetric.Properties +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.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