preliminary extensionality of functors

src/category-theory/functors-categories.lagda.md

@@ -10,8 +10,11 @@ module category-theory.functors-categories where
 open import category-theory.categories
 open import category-theory.functors-precategories
 
+open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.equivalences
 open import foundation.identity-types
+open import foundation.propositions
 open import foundation.universe-levels
 ```
 
@@ -25,6 +28,85 @@ A **functor** between two categories is a
 
 ## Definition
 
+### Maps between categories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Category l1 l2)
+  (D : Category l3 l4)
+  where
+
+  map-Category : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  map-Category =
+    map-Precategory (precategory-Category C) (precategory-Category D)
+
+  map-obj-map-Category :
+    (F : map-Category) → obj-Category C → obj-Category D
+  map-obj-map-Category =
+    map-obj-map-Precategory (precategory-Category C) (precategory-Category D)
+
+  map-hom-map-Category :
+    (F : map-Category)
+    {x y : obj-Category C} →
+    type-hom-Category C x y →
+    type-hom-Category D
+      ( map-obj-map-Category F x)
+      ( map-obj-map-Category F y)
+  map-hom-map-Category =
+    map-hom-map-Precategory (precategory-Category C) (precategory-Category D)
+```
+
+### The predicate of being a functor on maps between Categories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Category l1 l2)
+  (D : Category l3 l4)
+  (F : map-Category C D)
+  where
+
+  preserves-comp-hom-map-Category : UU (l1 ⊔ l2 ⊔ l4)
+  preserves-comp-hom-map-Category =
+    preserves-comp-hom-map-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  preserves-id-hom-map-Category : UU (l1 ⊔ l4)
+  preserves-id-hom-map-Category =
+    preserves-id-hom-map-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  is-functor-map-Category : UU (l1 ⊔ l2 ⊔ l4)
+  is-functor-map-Category =
+    is-functor-map-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  preserves-comp-hom-is-functor-map-Category :
+    is-functor-map-Category → preserves-comp-hom-map-Category
+  preserves-comp-hom-is-functor-map-Category =
+    preserves-comp-hom-is-functor-map-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  preserves-id-hom-is-functor-map-Category :
+    is-functor-map-Category → preserves-id-hom-map-Category
+  preserves-id-hom-is-functor-map-Category =
+    preserves-id-hom-is-functor-map-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+```
+
+### Functors between categories
+
 ```agda
 module _
   {l1 l2 l3 l4 : Level}
@@ -37,7 +119,8 @@ module _
     functor-Precategory (precategory-Category C) (precategory-Category D)
 
   map-obj-functor-Category : functor-Category → obj-Category C → obj-Category D
-  map-obj-functor-Category = pr1
+  map-obj-functor-Category =
+    map-obj-functor-Precategory (precategory-Category C) (precategory-Category D)
 
   map-hom-functor-Category :
     (F : functor-Category) →
@@ -46,7 +129,14 @@ module _
     type-hom-Category D
       ( map-obj-functor-Category F x)
       ( map-obj-functor-Category F y)
-  map-hom-functor-Category F = pr1 (pr2 F)
+  map-hom-functor-Category =
+    map-hom-functor-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+
+  map-functor-Category : functor-Category → map-Category C D
+  map-functor-Category =
+    map-functor-Precategory (precategory-Category C) (precategory-Category D)
 
   preserves-comp-functor-Category :
     ( F : functor-Category) {x y z : obj-Category C}
@@ -55,19 +145,19 @@ module _
     ( comp-hom-Category D
       ( map-hom-functor-Category F g)
       ( map-hom-functor-Category F f))
-  preserves-comp-functor-Category F =
+  preserves-comp-functor-Category =
     preserves-comp-functor-Precategory
       ( precategory-Category C)
-      ( precategory-Category D) F
+      ( precategory-Category D)
 
   preserves-id-functor-Category :
     (F : functor-Category) (x : obj-Category C) →
     map-hom-functor-Category F (id-hom-Category C {x}) ＝
     id-hom-Category D {map-obj-functor-Category F x}
-  preserves-id-functor-Category F =
+  preserves-id-functor-Category =
     preserves-id-functor-Precategory
       ( precategory-Category C)
-      ( precategory-Category D) F
+      ( precategory-Category D)
 ```
 
 ## Examples
@@ -91,11 +181,90 @@ comp-functor-Category :
   {l1 l2 l3 l4 l5 l6 : Level}
   (C : Category l1 l2) (D : Category l3 l4) (E : Category l5 l6) →
   functor-Category D E → functor-Category C D → functor-Category C E
-comp-functor-Category C D E G F =
+comp-functor-Category C D E =
   comp-functor-Precategory
     ( precategory-Category C)
     ( precategory-Category D)
     ( precategory-Category E)
-    ( G)
-    ( F)
 ```
+
+## Properties
+
+### Respecting identities and compositions are propositions
+
+This follows from the fact that the hom-types are
+[sets](foundation-core.sets.md).
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Category l1 l2)
+  (D : Category l3 l4)
+  (F : map-Category C D)
+  where
+
+  is-prop-preserves-comp-hom-map-Category :
+    is-prop (preserves-comp-hom-map-Category C D F)
+  is-prop-preserves-comp-hom-map-Category =
+    is-prop-preserves-comp-hom-map-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  preserves-comp-hom-map-Category-Prop : Prop (l1 ⊔ l2 ⊔ l4)
+  preserves-comp-hom-map-Category-Prop =
+    preserves-comp-hom-map-Precategory-Prop
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  is-prop-preserves-id-hom-map-Category :
+    is-prop (preserves-id-hom-map-Category C D F)
+  is-prop-preserves-id-hom-map-Category =
+    is-prop-preserves-id-hom-map-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  preserves-id-hom-map-Category-Prop : Prop (l1 ⊔ l4)
+  preserves-id-hom-map-Category-Prop =
+    preserves-id-hom-map-Precategory-Prop
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  is-prop-is-functor-map-Category :
+    is-prop (is-functor-map-Category C D F)
+  is-prop-is-functor-map-Category =
+    is-prop-is-functor-map-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  is-functor-map-Category-Prop : Prop (l1 ⊔ l2 ⊔ l4)
+  is-functor-map-Category-Prop =
+    is-functor-map-Precategory-Prop
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+```
+
+### Extensionality of functors between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Category l1 l2)
+  (D : Category l3 l4)
+  where
+
+  extensionality-functor-Category' :
+    (F G : functor-Category C D) →
+    (F ＝ G) ≃ (map-functor-Category C D F ＝ map-functor-Category C D G)
+  extensionality-functor-Category' =
+    extensionality-functor-Precategory'
+      ( precategory-Category C)
+      ( precategory-Category D)
+```
+
+It remains to characterize equality of maps between categories.