Add functors between (co)cone categories

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

@@ -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
+    }

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
+    }