End calculus

src/Categories/Category/CartesianClosed/Properties.agda

@@ -1,53 +1,99 @@
 {-# OPTIONS --without-K --safe #-}
 
-module Categories.Category.CartesianClosed.Properties where
 
 open import Level
 open import Data.Product using (Σ; _,_; Σ-syntax; proj₁; proj₂)
 
 open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.CartesianClosed using (CartesianClosed)
+open import Categories.Category.CartesianClosed using (CartesianClosed; module CartesianMonoidalClosed)
+open import Categories.Category.Monoidal.Closed using (Closed)
 open import Categories.Category.Core using (Category)
 open import Categories.Object.Terminal
+open import Categories.Diagram.Colimit
+open import Categories.Adjoint.Properties using (lapc)
 
 import Categories.Morphism.Reasoning as MR
 
-module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝓥 : CartesianClosed 𝒞) where
-  open Category 𝒞
-  open CartesianClosed 𝓥 using (_^_; eval′; cartesian)
-  open Cartesian cartesian using (products; terminal)
-  open BinaryProducts products
-  open Terminal terminal using (⊤)
-  open HomReasoning
-  open MR 𝒞
-
-  PointSurjective : ∀ {A X Y : Obj} → (X ⇒ Y ^ A) → Set (ℓ ⊔ e)
-  PointSurjective {A = A} {X = X} {Y = Y} ϕ =
-    ∀ (f : A ⇒ Y) → Σ[ x ∈ ⊤ ⇒ X ] (∀ (a : ⊤ ⇒ A) → eval′ ∘ first ϕ ∘ ⟨ x , a ⟩  ≈ f ∘ a)
-
-  lawvere-fixed-point : ∀ {A B : Obj} → (ϕ : A ⇒ B ^ A) → PointSurjective ϕ → (f : B ⇒ B) → Σ[ s ∈ ⊤ ⇒ B ] f ∘ s ≈ s
-  lawvere-fixed-point {A = A} {B = B} ϕ surjective f = g ∘ x , g-fixed-point
-    where
-      g : A ⇒ B
-      g = f ∘ eval′ ∘ ⟨ ϕ , id ⟩
-
-      x : ⊤ ⇒ A
-      x = proj₁ (surjective  g)
-
-      g-surjective : eval′ ∘ first ϕ ∘ ⟨ x , x ⟩ ≈ g ∘ x
-      g-surjective = proj₂ (surjective g) x
-
-      lemma : ∀ {A B C D} → (f : B ⇒ C) → (g : B ⇒ D) → (h : A ⇒ B) → (f ⁂ g) ∘ ⟨ h , h ⟩ ≈ ⟨ f , g ⟩ ∘ h
-      lemma f g h = begin
-        (f ⁂ g) ∘ ⟨ h , h ⟩ ≈⟨  ⁂∘⟨⟩ ⟩
-        ⟨ f ∘ h , g ∘ h ⟩   ≈˘⟨ ⟨⟩∘ ⟩
-        ⟨ f , g ⟩ ∘ h       ∎
-
-      g-fixed-point : f ∘ (g ∘ x) ≈ g ∘ x
-      g-fixed-point = begin
-        f ∘ g ∘ x                       ≈˘⟨  refl⟩∘⟨ g-surjective ⟩
-        f ∘ eval′ ∘ first ϕ ∘ ⟨ x , x ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ lemma ϕ id x ⟩
-        f ∘ eval′ ∘ ⟨ ϕ , id ⟩ ∘ x       ≈⟨ ∘-resp-≈ʳ sym-assoc ○ sym-assoc ⟩
-        (f ∘ eval′ ∘ ⟨ ϕ , id ⟩) ∘ x     ≡⟨⟩
-        g ∘ x                            ∎
+open import Categories.Functor using (Functor; _∘F_)
+
+module Categories.Category.CartesianClosed.Properties {o ℓ e} {𝒞 : Category o ℓ e} (𝓥 : CartesianClosed 𝒞) where
+
+open import Categories.Diagram.Empty 𝒞
+
+open Category 𝒞
+open CartesianClosed 𝓥 using (_^_; eval′; cartesian)
+open Cartesian cartesian using (products; terminal)
+open BinaryProducts products
+open Terminal terminal using (⊤)
+open HomReasoning
+open MR 𝒞
+
+open CartesianMonoidalClosed 𝒞 𝓥 using (closedMonoidal)
+private
+  module closedMonoidal = Closed closedMonoidal
+
+open import Categories.Object.Initial 𝒞
+open import Categories.Object.StrictInitial 𝒞
+open import Categories.Object.Initial.Colimit 𝒞
+
+
+PointSurjective : ∀ {A X Y : Obj} → (X ⇒ Y ^ A) → Set (ℓ ⊔ e)
+PointSurjective {A = A} {X = X} {Y = Y} ϕ =
+  ∀ (f : A ⇒ Y) → Σ[ x ∈ ⊤ ⇒ X ] (∀ (a : ⊤ ⇒ A) → eval′ ∘ first ϕ ∘ ⟨ x , a ⟩  ≈ f ∘ a)
+
+lawvere-fixed-point : ∀ {A B : Obj} → (ϕ : A ⇒ B ^ A) → PointSurjective ϕ → (f : B ⇒ B) → Σ[ s ∈ ⊤ ⇒ B ] f ∘ s ≈ s
+lawvere-fixed-point {A = A} {B = B} ϕ surjective f = g ∘ x , g-fixed-point
+  where
+    g : A ⇒ B
+    g = f ∘ eval′ ∘ ⟨ ϕ , id ⟩
+
+    x : ⊤ ⇒ A
+    x = proj₁ (surjective  g)
+
+    g-surjective : eval′ ∘ first ϕ ∘ ⟨ x , x ⟩ ≈ g ∘ x
+    g-surjective = proj₂ (surjective g) x
+
+    lemma : ∀ {A B C D} → (f : B ⇒ C) → (g : B ⇒ D) → (h : A ⇒ B) → (f ⁂ g) ∘ ⟨ h , h ⟩ ≈ ⟨ f , g ⟩ ∘ h
+    lemma f g h = begin
+      (f ⁂ g) ∘ ⟨ h , h ⟩ ≈⟨  ⁂∘⟨⟩ ⟩
+      ⟨ f ∘ h , g ∘ h ⟩   ≈˘⟨ ⟨⟩∘ ⟩
+      ⟨ f , g ⟩ ∘ h       ∎
+
+    g-fixed-point : f ∘ (g ∘ x) ≈ g ∘ x
+    g-fixed-point = begin
+      f ∘ g ∘ x                       ≈˘⟨  refl⟩∘⟨ g-surjective ⟩
+      f ∘ eval′ ∘ first ϕ ∘ ⟨ x , x ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ lemma ϕ id x ⟩
+      f ∘ eval′ ∘ ⟨ ϕ , id ⟩ ∘ x       ≈⟨ ∘-resp-≈ʳ sym-assoc ○ sym-assoc ⟩
+      (f ∘ eval′ ∘ ⟨ ϕ , id ⟩) ∘ x     ≡⟨⟩
+      g ∘ x                            ∎
+
+initial→product-initial : ∀ {⊥ A} → IsInitial ⊥ → IsInitial (⊥ × A)
+initial→product-initial {⊥} {A} i = initial.⊥-is-initial
+  where colim : Colimit (empty o ℓ e)
+        colim = ⊥⇒colimit record { ⊥ = ⊥ ; ⊥-is-initial = i }
+        colim' : Colimit (-× A ∘F (empty o ℓ e))
+        colim' = lapc closedMonoidal.adjoint (empty o ℓ e) colim
+        initial : Initial
+        initial = colimit⇒⊥ colim'
+        module initial = Initial initial
+
+open IsStrictInitial using (is-initial; is-strict)
+initial→strict-initial : ∀ {⊥} → IsInitial ⊥ → IsStrictInitial ⊥
+initial→strict-initial i .is-initial = i
+initial→strict-initial {⊥} i .is-strict f = record 
+  { from = f
+  ; to = !
+  ; iso = record
+    { isoˡ = begin
+      ! ∘ f                ≈˘⟨ refl⟩∘⟨ project₁ ⟩
+      ! ∘ π₁ ∘ ⟨ f , id ⟩   ≈⟨ pullˡ (initial-product.!-unique₂ (! ∘ π₁) π₂)  ⟩
+      π₂ ∘ ⟨ f , id ⟩       ≈⟨ project₂ ⟩
+      id                    ∎
+    ; isoʳ = !-unique₂ (f ∘ !) id
+    }
+  }
+  where open IsInitial i
+        module initial-product {A} =
+          IsInitial (initial→product-initial {⊥} {A} i)
+

src/Categories/Category/Complete/Properties.agda

@@ -18,6 +18,7 @@ open import Categories.Diagram.Cone.Properties
 open import Categories.Object.Terminal
 open import Categories.Object.Product.Limit C
 open import Categories.Object.Terminal.Limit C
+open import Categories.Diagram.Empty C
 open import Categories.Functor
 open import Categories.Functor.Limits
 open import Categories.Functor.Properties
@@ -43,7 +44,7 @@ module _ (Com : Complete o′ ℓ′ e′ C) where
   Complete⇒FinitelyComplete : FinitelyComplete C
   Complete⇒FinitelyComplete = record
     { cartesian = record
-      { terminal = limit⇒⊤ (Com (⊤⇒limit-F _ _ _))
+      { terminal = limit⇒⊤ (Com (empty _ _ _))
       ; products = record
         { product = λ {A B} → limit⇒product (Com (product⇒limit-F _ _ _ A B))
         }

src/Categories/Category/Construction/Functors.agda

@@ -130,6 +130,8 @@ module curry {o₁ e₁ ℓ₁} {C₁ : Category o₁ e₁ ℓ₁}
   open Category
   open NaturalIsomorphism
 
+  module ₀ (F : Bifunctor C₁ C₂ D) = Functor (Functor.F₀ curry F)
+
   -- Currying preserves natural isos.
   -- This makes |curry.F₀| a map between the hom-setoids of Cats.
 

src/Categories/Category/Construction/TwistedArrow.agda

@@ -1,20 +1,26 @@
 {-# OPTIONS --without-K --safe #-}
+open import Data.Product using (_,_; _×_; map; zip)
+open import Function.Base using (_$_; flip)
+open import Level
+open import Relation.Binary.Core using (Rel)
+
 open import Categories.Category using (Category; module Definitions)
+open import Categories.Category.Product renaming (Product to _×ᶜ_)
+open import Categories.Functor
+
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
 
 -- Definition of the "Twisted Arrow" Category of a Category 𝒞
 module Categories.Category.Construction.TwistedArrow {o ℓ e} (𝒞 : Category o ℓ e) where
 
-open import Level
-open import Data.Product using (_,_; _×_; map; zip)
-open import Function.Base using (_$_; flip)
-open import Relation.Binary.Core using (Rel)
+private
+  open module 𝒞 = Category 𝒞
 
-import Categories.Morphism as M
-open M 𝒞
-open import Categories.Morphism.Reasoning 𝒞
 
-open Category 𝒞
+open M 𝒞
 open Definitions 𝒞
+open MR 𝒞
 open HomReasoning
 
 private
@@ -68,3 +74,18 @@ TwistedArrow = record
     cod⇒ m₁ ∘ (cod⇒ m₂ ∘ Morphism.arr A) ∘ (dom⇐ m₂ ∘ dom⇐ m₁) ≈⟨ refl⟩∘⟨ (pullˡ assoc) ⟩
     cod⇒ m₁ ∘ (cod⇒ m₂ ∘ Morphism.arr A ∘ dom⇐ m₂) ∘ dom⇐ m₁   ≈⟨ (refl⟩∘⟨ square m₂ ⟩∘⟨refl) ⟩
     cod⇒ m₁ ∘ Morphism.arr B ∘ dom⇐ m₁ ∎
+
+
+-- Consider TwistedArrow as the comma category * / Hom[C][-,-]
+-- We have the codomain functor TwistedArrow → C.op × C
+
+module _ where
+  open Morphism
+  open Morphism⇒
+  open Functor
+  Forget : Functor TwistedArrow (𝒞.op ×ᶜ 𝒞)
+  Forget .F₀ x = dom x , cod x
+  Forget .F₁ f = dom⇐ f , cod⇒ f
+  Forget .identity = Equiv.refl , Equiv.refl
+  Forget .homomorphism = Equiv.refl , Equiv.refl
+  Forget .F-resp-≈ e = e

src/Categories/Comonad/Morphism.agda

@@ -112,8 +112,7 @@ module _ {S R T : Comonad C} where
     R.δ.η U ∘ σ .α.η U ∘ τ .α.η U
       ≈⟨ pullˡ (σ .comult-comp) ⟩
     (σ .α.η (R.F.₀ U) ∘ T.F.₁ (σ .α.η U) ∘ T.δ.η U) ∘ τ .α.η U
-      -- there is no approx² that witnesses (a ∘ (b ∘ c)) ∘ d ≈ (a ∘ b) ∘ (c ∘ d)
-      ≈⟨ pushˡ C.sym-assoc ⟩
+      ≈⟨ assoc²βγ ⟩
     (σ .α.η (R.F.₀ U) ∘ T.F.₁ (σ .α.η U)) ∘ (T.δ.η U ∘ τ .α.η U)
       ≈⟨ refl⟩∘⟨ τ .comult-comp ⟩
     (σ .α.η (R.F.₀ U) ∘ T.F.₁ (σ .α.η U)) ∘ (τ .α.η (T.F.₀ U) ∘ S.F.₁ (τ .α.η U) ∘ S.δ.η U)

src/Categories/Diagram/Empty.agda

@@ -0,0 +1,18 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+open import Categories.Category.Lift
+open import Categories.Category.Finite.Fin.Construction.Discrete
+open import Categories.Functor.Core
+
+module Categories.Diagram.Empty {o ℓ e} (C : Category o ℓ e) where
+
+-- maybe (liftC o′ ℓ′ e′ (Discrete 0)) should be Categories.Category.Empty so this does not depend on liftC
+empty : ∀ o′ ℓ′ e′ → Functor (liftC o′ ℓ′ e′ (Discrete 0)) C
+empty _ _ _ = record
+  { F₀           = λ ()
+  ; F₁           = λ { {()} }
+  ; identity     = λ { {()} }
+  ; homomorphism = λ { {()} }
+  ; F-resp-≈     = λ { {()} }
+  }