From 4fd67ee7ee559d5b98555985eff8fb91710c3c0c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Mon, 27 Jan 2025 12:15:32 +0100
Subject: [PATCH] Add functors between (co)cone categories
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This adds three functors between cone categories (and cocone categories,
respectively). All F₀ and F₁ fields are maps that already have been
defined in Categories.Diagram.Co(co)ne.Properties, and thus the Functor
definition is places there as well. Unfortunately, using the definition
of Cones (and Cocones) requires the import of
Categories.Category.Construction.Cones (and Cocones) in the
Cones.Properties module.

For `F : Functor J C`, the new functors are:

  - Every `G : Functor C D` lifts to a `Functor (Cones F) (Cones (G ∘F F))`
    and `Functor (Cocones F) (Cocones (G ∘F F))`
  - Every `G : Functor J′ J` lifts to a `Functor (Cones F) (Cones (F ∘F G))`
    and `Functor (Cocones F) (Cocones (F ∘F G))`
  - Every `G : Functor J C` and `α : NaturalTransformation F G` extends
    to a `Functor (Cones F) (Cones G)` and `Functor (Cocones G) (Cocones F)`

In Cocones.Properties, I've restricted the import of Cone.Properties to
the four maps that are actually used.
---
 src/Categories/Diagram/Cocone/Properties.agda | 32 ++++++++++++++++++-
 src/Categories/Diagram/Cone/Properties.agda   | 28 ++++++++++++++++
 2 files changed, 59 insertions(+), 1 deletion(-)

diff --git a/src/Categories/Diagram/Cocone/Properties.agda b/src/Categories/Diagram/Cocone/Properties.agda
index dba9f4708..1ffec06c7 100644
--- a/src/Categories/Diagram/Cocone/Properties.agda
+++ b/src/Categories/Diagram/Cocone/Properties.agda
@@ -8,8 +8,9 @@ open import Categories.Category
 open import Categories.Functor
 open import Categories.Functor.Properties
 open import Categories.NaturalTransformation
-open import Categories.Diagram.Cone.Properties
+open import Categories.Diagram.Cone.Properties using (F-map-Coneʳ; F-map-Cone⇒ʳ; nat-map-Cone; nat-map-Cone⇒)
 open import Categories.Diagram.Duality
+open import Categories.Category.Construction.Cocones using (Cocones)
 
 import Categories.Diagram.Cocone as Coc
 import Categories.Morphism.Reasoning as MR
@@ -45,6 +46,15 @@ module _ {F : Functor J C} (G : Functor C D) where
     }
     where open CF.Cocone⇒ f
 
+  mapˡ : Functor (Cocones F) (Cocones (G ∘F F))
+  mapˡ = record
+    { F₀ = F-map-Coconeˡ
+    ; F₁ =  F-map-Cocone⇒ˡ
+    ; identity = G.identity
+    ; homomorphism = G.homomorphism
+    ; F-resp-≈ = G.F-resp-≈
+    }
+
 module _ {F : Functor J C} (G : Functor J′ J) where
   private
     module C   = Category C
@@ -61,8 +71,19 @@ module _ {F : Functor J C} (G : Functor J′ J) where
   F-map-Cocone⇒ʳ : ∀ {K K′} (f : CF.Cocone⇒ K K′) → CFG.Cocone⇒ (F-map-Coconeʳ K) (F-map-Coconeʳ K′)
   F-map-Cocone⇒ʳ f = coCone⇒⇒Cocone⇒ C (F-map-Cone⇒ʳ G.op (Cocone⇒⇒coCone⇒ C f))
 
+  mapʳ : Functor (Cocones F) (Cocones (F ∘F G))
+  mapʳ = record
+    { F₀ = F-map-Coconeʳ
+    ; F₁ = F-map-Cocone⇒ʳ
+    ; identity = C.Equiv.refl
+    ; homomorphism = C.Equiv.refl
+    ; F-resp-≈ = λ f≈g → f≈g
+    }
+
+
 module _ {F G : Functor J C} (α : NaturalTransformation F G) where
   private
+    module C  = Category C
     module α  = NaturalTransformation α
     module CF = Coc F
     module CG = Coc G
@@ -72,3 +93,12 @@ module _ {F G : Functor J C} (α : NaturalTransformation F G) where
 
   nat-map-Cocone⇒ : ∀ {K K′} (f : CG.Cocone⇒ K K′) → CF.Cocone⇒ (nat-map-Cocone K) (nat-map-Cocone K′)
   nat-map-Cocone⇒ f = coCone⇒⇒Cocone⇒ C (nat-map-Cone⇒ α.op (Cocone⇒⇒coCone⇒ C f))
+
+  nat-map : Functor (Cocones G) (Cocones F)
+  nat-map = record
+    { F₀ = nat-map-Cocone
+    ; F₁ = nat-map-Cocone⇒
+    ; identity = C.Equiv.refl
+    ; homomorphism = C.Equiv.refl
+    ; F-resp-≈ = λ f≈g → f≈g
+    }
diff --git a/src/Categories/Diagram/Cone/Properties.agda b/src/Categories/Diagram/Cone/Properties.agda
index 34891b350..fe6158e99 100644
--- a/src/Categories/Diagram/Cone/Properties.agda
+++ b/src/Categories/Diagram/Cone/Properties.agda
@@ -10,6 +10,7 @@ open import Categories.Functor.Properties
 open import Categories.NaturalTransformation
 import Categories.Diagram.Cone as Con
 import Categories.Morphism.Reasoning as MR
+open import Categories.Category.Construction.Cones using (Cones)
 
 private
   variable
@@ -42,6 +43,15 @@ module _ {F : Functor J C} (G : Functor C D) where
     }
     where open CF.Cone⇒ f
 
+  mapˡ : Functor (Cones F) (Cones (G ∘F F))
+  mapˡ = record
+    { F₀ = F-map-Coneˡ
+    ; F₁ =  F-map-Cone⇒ˡ
+    ; identity = G.identity
+    ; homomorphism = G.homomorphism
+    ; F-resp-≈ = G.F-resp-≈
+    }
+
 module _ {F : Functor J C} (G : Functor J′ J) where
   private
     module C   = Category C
@@ -68,6 +78,15 @@ module _ {F : Functor J C} (G : Functor J′ J) where
     }
     where open CF.Cone⇒ f
 
+  mapʳ : Functor (Cones F) (Cones (F ∘F G))
+  mapʳ = record
+    { F₀ = F-map-Coneʳ
+    ; F₁ = F-map-Cone⇒ʳ
+    ; identity = C.Equiv.refl
+    ; homomorphism = C.Equiv.refl
+    ; F-resp-≈ = λ f≈g → f≈g
+    }
+
 module _ {F G : Functor J C} (α : NaturalTransformation F G) where
   private
     module C  = Category C
@@ -99,3 +118,12 @@ module _ {F G : Functor J C} (α : NaturalTransformation F G) where
     ; commute = pullʳ commute
     }
     where open CF.Cone⇒ f
+
+  nat-map : Functor (Cones F) (Cones G)
+  nat-map = record
+    { F₀ = nat-map-Cone
+    ; F₁ = nat-map-Cone⇒
+    ; identity = C.Equiv.refl
+    ; homomorphism = C.Equiv.refl
+    ; F-resp-≈ = λ f≈g → f≈g
+    }