Add functors between (co)cone categories

[t-wissmann]

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)) (from Contribution of lemmas about colimits #417)
• 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.

[t-wissmann]

Beside the location of the above functors, I also wasn't to certain about the naming scheme for them. I simply took the existing names and replaced Coneˡ and Coconeˡ⇒ etc by Functor, obtaining:

• F-map-Functorˡ : Functor (Cocones F) (Cocones (G ∘F F))
• F-map-Functorʳ : Functor (Cocones F) (Cocones (F ∘F G))
• nat-map-Functor : Functor (Cocones G) (Cocones F)

[JacquesCarette]

one nitpick, and this is good to go, at least code-wise.

[JacquesCarette]

here (and everywhere in this PR), can you delete implicits if/when they are not needed please?

[t-wissmann]

Sure! I've removed all implicit arguments from the lambdas in my commit.

[JacquesCarette]

On names: I wonder if mapˡ and nat-map would be sufficient? Certainly the F- prefix seems redundant, no?

[t-wissmann]

On names: I wonder if mapˡ and nat-map would be sufficient? Certainly the F- prefix seems redundant, no?

I agree; maybe it would still be preferrable to include Cones etc in the name such that no name conflict arises (so far, Cocones.Properties and Cones.Properties don't have any conflicting names). So maybe: map-Conesˡ, map-Coconesˡ, nat-map-Cones?

[JacquesCarette]

I admit that I was thinking of the usage as having open import Categories.Diagram.Cones as Cones in the header, so that having Cones in the function name doubles things up.

[t-wissmann]

I admit that I was thinking of the usage as having open import Categories.Diagram.Cones as Cones in the header, so that having Cones in the function name doubles things up.

Fine for me, too. This would have the advantage of making the order of words canonical (Cones.mapˡ instead of having the dilemma between Cones-mapˡ, map-Conesˡ, mapˡ-Cones).

Edit: so if you want me to rename things to mapˡ etc, just let me know.

[t-wissmann]

I've just renamed the functions to mapˡ, nat-map etc. :-)

[t-wissmann]

Thanks for approving this PR! Is there anything left that I can (or need to) do?

[JacquesCarette]

No, I just needed to let the checks run to completion before I could merge (and then I got insanely busy). Merging now.