define representing arrow category

src/category-theory.lagda.md

@@ -79,6 +79,7 @@ open import category-theory.products-of-precategories public
 open import category-theory.pullbacks-in-precategories public
 open import category-theory.representable-functors-categories public
 open import category-theory.representable-functors-precategories public
+open import category-theory.representing-arrow-category public
 open import category-theory.sieves-in-categories public
 open import category-theory.slice-precategories public
 open import category-theory.terminal-objects-in-precategories public

src/category-theory/functors-large-precategories.lagda.md

@@ -19,7 +19,8 @@ open import foundation.universe-levels
 
 ## Idea
 
-A functor from a large precategory `C` to a large precategory `D` consists of:
+A **functor** from a [large precategory](category-theory.large-precategories.md)
+`C` to a large precategory `D` consists of:
 
 - a map `F : C → D` on objects,
 - a map `Fmap : hom x y → hom (F x) (F y)` on morphisms, such that the following

src/category-theory/large-precategories.lagda.md

@@ -42,7 +42,8 @@ record
 
     comp-hom-Large-Precategory :
       {l1 l2 l3 : Level}
-      {X : obj-Large-Precategory l1} {Y : obj-Large-Precategory l2}
+      {X : obj-Large-Precategory l1}
+      {Y : obj-Large-Precategory l2}
       {Z : obj-Large-Precategory l3} →
       type-Set (hom-Large-Precategory Y Z) →
       type-Set (hom-Large-Precategory X Y) →

src/category-theory/precategories.lagda.md

@@ -93,13 +93,15 @@ module _
 
   comp-hom-Precategory :
     {x y z : obj-Precategory} →
-    type-hom-Precategory y z → type-hom-Precategory x y →
+    type-hom-Precategory y z →
+    type-hom-Precategory x y →
     type-hom-Precategory x z
   comp-hom-Precategory = pr1 associative-composition-structure-Precategory
 
   comp-hom-Precategory' :
     {x y z : obj-Precategory} →
-    type-hom-Precategory x y → type-hom-Precategory y z →
+    type-hom-Precategory x y →
+    type-hom-Precategory y z →
     type-hom-Precategory x z
   comp-hom-Precategory' f g = comp-hom-Precategory g f
 

src/category-theory/representing-arrow-category.lagda.md

@@ -0,0 +1,167 @@
+# The representing arrow category
+
+```agda
+module category-theory.representing-arrow-category where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.functors-precategories
+open import category-theory.precategories
+open import category-theory.categories
+open import category-theory.isomorphisms-in-precategories
+open import category-theory.yoneda-lemma-precategories
+open import category-theory.yoneda-lemma-categories
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.contractible-types
+open import foundation.unit-type
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.injective-maps
+open import foundation.empty-types
+open import foundation.booleans
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+The **representing arrow** is the [category](category-theory.categories.md) that
+[represents](category-theory.representable-functors-categories.md) arrows in a
+([pre-](category-theory.precategories.md))category. We model it after
+implication on the [booleans](foundation.booleans.md).
+
+## Definition
+
+### The objects and hom-sets of the representing arrow
+
+```agda
+obj-representing-arrow : UU lzero
+obj-representing-arrow = bool
+
+hom-representing-arrow :
+  obj-representing-arrow → obj-representing-arrow → Set lzero
+hom-representing-arrow true true = unit-Set
+hom-representing-arrow true false = empty-Set
+hom-representing-arrow false _ = unit-Set
+
+type-hom-representing-arrow :
+  obj-representing-arrow → obj-representing-arrow → UU lzero
+type-hom-representing-arrow x y = type-Set (hom-representing-arrow x y)
+```
+
+### The precategory structure of the representing arrow
+
+```agda
+comp-hom-representing-arrow :
+  {x y z : obj-representing-arrow} →
+  type-hom-representing-arrow y z →
+  type-hom-representing-arrow x y →
+  type-hom-representing-arrow x z
+comp-hom-representing-arrow {true} {true} {true} _ _ = star
+comp-hom-representing-arrow {false} _ _ = star
+
+associative-comp-hom-representing-arrow :
+  {x y z w : obj-representing-arrow} →
+  (h : type-hom-representing-arrow z w)
+  (g : type-hom-representing-arrow y z)
+  (f : type-hom-representing-arrow x y) →
+  comp-hom-representing-arrow {x} (comp-hom-representing-arrow {y} h g) f ＝
+  comp-hom-representing-arrow {x} h (comp-hom-representing-arrow {x} g f)
+associative-comp-hom-representing-arrow {true} {true} {true} {true} h g f = refl
+associative-comp-hom-representing-arrow {false} h g f = refl
+
+associative-composition-structure-representing-arrow :
+  associative-composition-structure-Set hom-representing-arrow
+pr1 associative-composition-structure-representing-arrow {x} =
+  comp-hom-representing-arrow {x}
+pr2 associative-composition-structure-representing-arrow =
+  associative-comp-hom-representing-arrow
+
+id-hom-representing-arrow :
+  {x : obj-representing-arrow} → type-hom-representing-arrow x x
+id-hom-representing-arrow {true} = star
+id-hom-representing-arrow {false} = star
+
+left-unit-law-comp-hom-representing-arrow :
+  {x y : obj-representing-arrow} →
+  (f : type-hom-representing-arrow x y) →
+  comp-hom-representing-arrow {x} (id-hom-representing-arrow {y}) f ＝ f
+left-unit-law-comp-hom-representing-arrow {true} {true} f = refl
+left-unit-law-comp-hom-representing-arrow {false} f = refl
+
+right-unit-law-comp-hom-representing-arrow :
+  {x y : obj-representing-arrow} →
+  (f : type-hom-representing-arrow x y) →
+  comp-hom-representing-arrow {x} f (id-hom-representing-arrow {x}) ＝ f
+right-unit-law-comp-hom-representing-arrow {true} {true} f = refl
+right-unit-law-comp-hom-representing-arrow {false} f = refl
+
+is-unital-composition-structure-representing-arrow :
+  is-unital-composition-structure-Set
+    ( hom-representing-arrow)
+    ( associative-composition-structure-representing-arrow)
+pr1 is-unital-composition-structure-representing-arrow x =
+  id-hom-representing-arrow {x}
+pr1 (pr2 is-unital-composition-structure-representing-arrow) =
+  left-unit-law-comp-hom-representing-arrow
+pr2 (pr2 is-unital-composition-structure-representing-arrow) =
+  right-unit-law-comp-hom-representing-arrow
+
+representing-arrow-Precategory : Precategory lzero lzero
+pr1 representing-arrow-Precategory = obj-representing-arrow
+pr1 (pr2 representing-arrow-Precategory) = hom-representing-arrow
+pr1 (pr2 (pr2 representing-arrow-Precategory)) =
+  associative-composition-structure-representing-arrow
+pr2 (pr2 (pr2 representing-arrow-Precategory)) =
+  is-unital-composition-structure-representing-arrow
+```
+
+### The representing arrow category
+
+```agda
+is-category-representing-arrow :
+  is-category-Precategory representing-arrow-Precategory
+is-category-representing-arrow true true =
+    is-equiv-is-prop
+    ( is-set-bool true true)
+    ( is-prop-type-subtype
+      ( is-iso-Precategory-Prop representing-arrow-Precategory {true} {true})
+      ( is-prop-unit))
+    ( λ _ → refl)
+is-category-representing-arrow true false =
+  is-equiv-is-empty
+    ( iso-eq-Precategory representing-arrow-Precategory true false)
+    ( hom-iso-Precategory representing-arrow-Precategory)
+is-category-representing-arrow false true =
+  is-equiv-is-empty
+    ( iso-eq-Precategory representing-arrow-Precategory false true)
+    ( hom-inv-iso-Precategory representing-arrow-Precategory)
+is-category-representing-arrow false false =
+  is-equiv-is-prop
+    ( is-set-bool false false)
+    ( is-prop-type-subtype
+      ( is-iso-Precategory-Prop representing-arrow-Precategory {false} {false})
+      ( is-prop-unit))
+    ( λ _ → refl)
+
+representing-arrow-Category : Category lzero lzero
+pr1 representing-arrow-Category = representing-arrow-Precategory
+pr2 representing-arrow-Category = is-category-representing-arrow
+```
+
+## Properties
+
+### The representing arrow represents arrows in a category
+
+Use the Yoneda lemma.

src/foundation-core/empty-types.lagda.md

@@ -23,7 +23,7 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-An empty type is a type with no elements. The (standard) empty type is
+An **empty type** is a type with no elements. The (standard) empty type is
 introduced as an inductive type with no constructors. With the standard empty
 type available, we will say that a type is empty if it maps into the standard
 empty type.

src/foundation-core/subtypes.lagda.md

@@ -31,8 +31,10 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-A subtype of a type `A` is a family of propositions over `A`. The underlying
-type of a subtype `P` of `A` is the total space `Σ A B`.
+A **subtype** of a type `A` is a family of
+[propositions](foundation-core.propositions.md) over `A`. The underlying type of
+a subtype `P` of `A` is the [total space](foundation.dependent-pair-types.md)
+`Σ A B`.
 
 ## Definitions
 

src/foundation/booleans.lagda.md

@@ -32,8 +32,10 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The type of booleans is a 2-element type with elements `true false : bool`,
-which is used for reasoning with decidable propositions.
+The type of **booleans** is a
+[2-element type](univalent-combinatorics.2-element-types.md) with elements
+`true false : bool`, which is used for reasoning with
+[decidable propositions](foundation-core.decidable-propositions.md).
 
 ## Definition
 
@@ -64,6 +66,17 @@ compute-raise-bool : (l : Level) → bool ≃ raise-bool l
 compute-raise-bool l = compute-raise l bool
 ```
 
+### The representing propositions of bool
+
+```agda
+prop-bool : bool → Prop lzero
+prop-bool true = unit-Prop
+prop-bool false = empty-Prop
+
+type-prop-bool : bool → UU lzero
+type-prop-bool = type-Prop ∘ prop-bool
+```
+
 ### Equality on the booleans
 
 ```agda
@@ -100,17 +113,23 @@ neg-bool : bool → bool
 neg-bool true = false
 neg-bool false = true
 
-conjunction-bool : bool → (bool → bool)
+conjunction-bool : bool → bool → bool
 conjunction-bool true true = true
 conjunction-bool true false = false
 conjunction-bool false true = false
 conjunction-bool false false = false
 
-disjunction-bool : bool → (bool → bool)
+disjunction-bool : bool → bool → bool
 disjunction-bool true true = true
 disjunction-bool true false = true
 disjunction-bool false true = true
 disjunction-bool false false = false
+
+implication-bool : bool → bool → bool
+implication-bool true true = true
+implication-bool true false = false
+implication-bool false true = true
+implication-bool false false = true
 ```
 
 ## Properties