Let being an isomorphism be a property

src/category-theory/isomorphisms-in-precategories.lagda.md

@@ -8,6 +8,8 @@ module category-theory.isomorphisms-in-precategories where
 
 ```agda
 open import category-theory.precategories
+open import category-theory.retractions-in-precategories
+open import category-theory.sections-in-precategories
 
 open import foundation.action-on-identifications-functions
 open import foundation.cartesian-product-types
@@ -22,56 +24,119 @@ open import foundation.retractions
 open import foundation.sections
 open import foundation.sets
 open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 
 </details>
 
 ## Idea
 
-An **isomorphism** in a [precategory](category-theory.precategories.md) `C` is a
-morphism `f : x → y` in `C` for which there exists a morphism `g : y → x` such
-that `f ∘ g ＝ id` and `g ∘ f ＝ id`.
+An {{#concept "isomorphism" Disambiguation="precategory" Agda=iso-Precategory}}
+in a [precategory](category-theory.precategories.md) `C` is a
+morphism `f : x → y` in `C` which has a [section](category-theory.sections-in-precategories.md) and a [retraction](category-theory.retractions-in-precategories.md). In other words, an isomorphism is a morphism `f : x → y` for which there is a morphism `g : y → x` equipped with an identification
+
+```text
+  f ∘ g ＝ id,
+```
+
+and a morphism `h : y → x` equipped with an identification
+
+```text
+  h ∘ f ＝ id.
+```
+
+This definition of isomorphisms follows a general pattern in agda-unimath, where we will always define isomorphisms in this manner.
 
 ## Definitions
 
 ### The predicate of being an isomorphism in a precategory
 
 ```agda
-is-iso-Precategory :
-  {l1 l2 : Level}
-  (C : Precategory l1 l2)
-  {x y : obj-Precategory C}
-  (f : hom-Precategory C x y) →
-  UU l2
-is-iso-Precategory C {x} {y} f =
-  Σ ( hom-Precategory C y x)
-    ( λ g →
-      ( comp-hom-Precategory C f g ＝ id-hom-Precategory C) ×
-      ( comp-hom-Precategory C g f ＝ id-hom-Precategory C))
+module _
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C} (f : hom-Precategory C x y)
+  where
+
+  is-iso-Precategory : UU l2
+  is-iso-Precategory =
+    section-hom-Precategory C f × retraction-hom-Precategory C f
 
 module _
-  {l1 l2 : Level}
-  (C : Precategory l1 l2)
-  {x y : obj-Precategory C}
-  {f : hom-Precategory C x y}
+  {l1 l2 : Level} (C : Precategory l1 l2)
+  {x y : obj-Precategory C} {f : hom-Precategory C x y}
+  (H : is-iso-Precategory C f)
   where
 
-  hom-inv-is-iso-Precategory :
-    is-iso-Precategory C f → hom-Precategory C y x
-  hom-inv-is-iso-Precategory = pr1
+  section-is-iso-Precategory : section-hom-Precategory C f
+  section-is-iso-Precategory = pr1 H
+
+  hom-section-is-iso-Precategory : hom-Precategory C y x
+  hom-section-is-iso-Precategory =
+    hom-section-hom-Precategory C f section-is-iso-Precategory
+
+  is-section-section-is-iso-Precategory :
+    is-section-hom-Precategory C f hom-section-is-iso-Precategory
+  is-section-section-is-iso-Precategory =
+    is-section-section-hom-Precategory C f section-is-iso-Precategory
+
+  retraction-is-iso-Precategory : retraction-hom-Precategory C f
+  retraction-is-iso-Precategory = pr2 H
+
+  hom-retraction-is-iso-Precategory : hom-Precategory C y x
+  hom-retraction-is-iso-Precategory =
+    hom-retraction-hom-Precategory C f retraction-is-iso-Precategory
+
+  is-retraction-retraction-is-iso-Precategory :
+    is-retraction-hom-Precategory C f hom-retraction-is-iso-Precategory
+  is-retraction-retraction-is-iso-Precategory =
+    is-retraction-retraction-hom-Precategory C f retraction-is-iso-Precategory
+
+  hom-inv-is-iso-Precategory : hom-Precategory C y x
+  hom-inv-is-iso-Precategory = hom-section-is-iso-Precategory
 
   is-section-hom-inv-is-iso-Precategory :
-    (H : is-iso-Precategory C f) →
-    comp-hom-Precategory C f (hom-inv-is-iso-Precategory H) ＝
-    id-hom-Precategory C
-  is-section-hom-inv-is-iso-Precategory = pr1 ∘ pr2
+    is-section-hom-Precategory C f hom-inv-is-iso-Precategory
+  is-section-hom-inv-is-iso-Precategory = is-section-section-is-iso-Precategory
+
+  eq-hom-retraction-hom-section-is-iso-Precategory :
+    hom-section-is-iso-Precategory ＝ hom-retraction-is-iso-Precategory
+  eq-hom-retraction-hom-section-is-iso-Precategory =
+    equational-reasoning
+      hom-section-is-iso-Precategory
+      ＝ comp-hom-Precategory C
+          ( id-hom-Precategory C)
+          ( hom-section-is-iso-Precategory)
+        by
+        inv (left-unit-law-comp-hom-Precategory C _)
+      ＝ comp-hom-Precategory C
+          ( comp-hom-Precategory C hom-retraction-is-iso-Precategory f)
+          ( hom-section-is-iso-Precategory)
+        by
+        inv
+          ( ap
+            ( λ g → comp-hom-Precategory C g _)
+            ( is-retraction-retraction-is-iso-Precategory))
+      ＝ comp-hom-Precategory C
+          ( hom-retraction-is-iso-Precategory)
+          ( comp-hom-Precategory C f hom-section-is-iso-Precategory)
+        by associative-comp-hom-Precategory C _ _ _
+      ＝ comp-hom-Precategory C
+          ( hom-retraction-is-iso-Precategory)
+          ( id-hom-Precategory C)
+        by
+        ap (comp-hom-Precategory C _) is-section-section-is-iso-Precategory
+      ＝ hom-retraction-is-iso-Precategory
+        by
+        right-unit-law-comp-hom-Precategory C _
 
   is-retraction-hom-inv-is-iso-Precategory :
-    (H : is-iso-Precategory C f) →
-    comp-hom-Precategory C (hom-inv-is-iso-Precategory H) f ＝
-    id-hom-Precategory C
-  is-retraction-hom-inv-is-iso-Precategory = pr2 ∘ pr2
+    is-retraction-hom-Precategory C f hom-inv-is-iso-Precategory
+  is-retraction-hom-inv-is-iso-Precategory =
+    tr
+      ( is-retraction-hom-Precategory C f)
+      ( inv eq-hom-retraction-hom-section-is-iso-Precategory)
+      ( is-retraction-retraction-is-iso-Precategory)
 ```
 
 ### Isomorphisms in a precategory
@@ -138,11 +203,13 @@ module _
   {x : obj-Precategory C}
   where
 
-  is-iso-id-hom-Precategory :
-    is-iso-Precategory C (id-hom-Precategory C {x})
-  pr1 is-iso-id-hom-Precategory = id-hom-Precategory C
+  is-iso-id-hom-Precategory : is-iso-Precategory C (id-hom-Precategory C {x})
+  pr1 (pr1 is-iso-id-hom-Precategory) =
+    id-hom-Precategory C
+  pr2 (pr1 is-iso-id-hom-Precategory) =
+    right-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
   pr1 (pr2 is-iso-id-hom-Precategory) =
-    left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
+    id-hom-Precategory C
   pr2 (pr2 is-iso-id-hom-Precategory) =
     left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)
 
@@ -198,7 +265,7 @@ module _
     (f : hom-Precategory C x y)
     (H K : is-iso-Precategory C f) → H ＝ K
   all-elements-equal-is-iso-Precategory f
-    (g , p , q) (g' , p' , q') =
+    ((g , p) , (h , q)) ((g' , p') , (h' , q')) =
     eq-type-subtype
       ( λ g →
         product-Prop

src/category-theory/retractions-in-categories.lagda.md

@@ -0,0 +1,67 @@
+# Retractions in categories
+
+```agda
+module category-theory.retractions-in-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.retractions-in-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [category](category-theory.categories.md) `𝒞`. A {{#concept "retraction" Disambiguation="morphism in a category" Agda=retraction-hom-Category}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  g ∘ f ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a category of being a retraction
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Category l1 l2)
+  {A B : obj-Category 𝒞} (f : hom-Category 𝒞 A B)
+  where
+
+  is-retraction-hom-Category : hom-Category 𝒞 B A → UU l2
+  is-retraction-hom-Category =
+    is-retraction-hom-Precategory (precategory-Category 𝒞) f
+```
+
+### Retractions of a morphism in a category
+
+```agda
+module _
+  {l1 l2 : Level} (𝒞 : Category l1 l2)
+  {A B : obj-Category 𝒞} (f : hom-Category 𝒞 A B)
+  where
+
+  retraction-hom-Category : UU l2
+  retraction-hom-Category =
+    retraction-hom-Precategory (precategory-Category 𝒞) f
+
+  module _
+    (r : retraction-hom-Category)
+    where
+
+    hom-retraction-hom-Category : hom-Category 𝒞 B A
+    hom-retraction-hom-Category =
+      hom-retraction-hom-Precategory (precategory-Category 𝒞) f r
+
+    is-retraction-retraction-hom-Category :
+      is-retraction-hom-Category 𝒞 f hom-retraction-hom-Category
+    is-retraction-retraction-hom-Category =
+      is-retraction-retraction-hom-Precategory (precategory-Category 𝒞) f r
+```

src/category-theory/retractions-in-large-categories.lagda.md

@@ -0,0 +1,78 @@
+# Retractions in large categories
+
+```agda
+module category-theory.retractions-in-large-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.large-categories
+open import category-theory.retractions-in-large-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a morphism `f : A → B` in a [large category](category-theory.large-categories.md) `𝒞`. A {{#concept "retraction" Disambiguation="morphism in a large category" Agda=retraction-hom-Large-Category}} of `f` consists of a morphism `g : B → A` equipped with an [identification](foundation-core.identifications.md)
+
+```text
+  g ∘ f ＝ id.
+```
+
+## Definitions
+
+### The predicate on morphisms in a large category of being a retraction
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Category α β)
+  {l1 l2 : Level} {A : obj-Large-Category 𝒞 l1}
+  {B : obj-Large-Category 𝒞 l2} (f : hom-Large-Category 𝒞 A B)
+  where
+
+  is-retraction-hom-Large-Category :
+    hom-Large-Category 𝒞 B A → UU (β l1 l1)
+  is-retraction-hom-Large-Category =
+    is-retraction-hom-Large-Precategory (large-precategory-Large-Category 𝒞) f
+```
+
+### Retractions of a morphism in a large category
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level} (𝒞 : Large-Category α β)
+  {l1 l2 : Level} {A : obj-Large-Category 𝒞 l1}
+  {B : obj-Large-Category 𝒞 l2} (f : hom-Large-Category 𝒞 A B)
+  where
+
+  retraction-hom-Large-Category : UU (β l1 l1 ⊔ β l2 l1)
+  retraction-hom-Large-Category =
+    retraction-hom-Large-Precategory (large-precategory-Large-Category 𝒞) f
+
+  module _
+    (r : retraction-hom-Large-Category)
+    where
+
+    hom-retraction-hom-Large-Category : hom-Large-Category 𝒞 B A
+    hom-retraction-hom-Large-Category =
+      hom-retraction-hom-Large-Precategory
+        ( large-precategory-Large-Category 𝒞)
+        ( f)
+        ( r)
+
+    is-retraction-retraction-hom-Large-Category :
+      is-retraction-hom-Large-Category 𝒞 f
+        ( hom-retraction-hom-Large-Category)
+    is-retraction-retraction-hom-Large-Category =
+      is-retraction-retraction-hom-Large-Precategory
+        ( large-precategory-Large-Category 𝒞)
+        ( f)
+        ( r)
+```
+