Merge branch 'master' into preunivalence

src/category-theory/categories.lagda.md

@@ -156,42 +156,36 @@ module _
     is-emb-is-equiv (is-category-Category C x y)
 ```
 
-### Precomposition by a morphism
+### Equalities induce morphisms
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2) (x y : obj-Category C)
+  where
+
+  hom-eq-Category : x ＝ y → hom-Category C x y
+  hom-eq-Category = hom-eq-Precategory (precategory-Category C) x y
+
+  hom-inv-eq-Category : x ＝ y → hom-Category C y x
+  hom-inv-eq-Category = hom-inv-eq-Precategory (precategory-Category C) x y
+```
+
+### Pre- and postcomposition by a morphism
 
 ```agda
 precomp-hom-Category :
   {l1 l2 : Level} (C : Category l1 l2) {x y : obj-Category C}
   (f : hom-Category C x y) (z : obj-Category C) →
   hom-Category C y z → hom-Category C x z
 precomp-hom-Category C = precomp-hom-Precategory (precategory-Category C)
-```
-
-### Postcomposition by a morphism
 
-```agda
 postcomp-hom-Category :
   {l1 l2 : Level} (C : Category l1 l2) {x y : obj-Category C}
   (f : hom-Category C x y) (z : obj-Category C) →
   hom-Category C z x → hom-Category C z y
 postcomp-hom-Category C = postcomp-hom-Precategory (precategory-Category C)
 ```
 
-### Equalities induce morphisms
-
-```agda
-module _
-  {l1 l2 : Level} (C : Category l1 l2)
-  where
-
-  hom-eq-Category :
-    (x y : obj-Category C) → x ＝ y → hom-Category C x y
-  hom-eq-Category = hom-eq-Precategory (precategory-Category C)
-
-  hom-inv-eq-Category :
-    (x y : obj-Category C) → x ＝ y → hom-Category C y x
-  hom-inv-eq-Category = hom-inv-eq-Precategory (precategory-Category C)
-```
-
 ## Properties
 
 ### The objects in a category form a 1-type

src/category-theory/isomorphism-induction-categories.lagda.md

@@ -20,6 +20,7 @@ open import foundation.function-types
 open import foundation.identity-systems
 open import foundation.identity-types
 open import foundation.sections
+open import foundation.torsorial-type-families
 open import foundation.universal-property-identity-systems
 open import foundation.universe-levels
 ```
@@ -78,39 +79,6 @@ module _
 
 ## Properties
 
-### Contractibility of the total space of isomorphisms implies isomorphism induction
-
-```agda
-module _
-  {l1 l2 : Level} (C : Category l1 l2) {A : obj-Category C}
-  where
-
-  abstract
-    is-identity-system-iso-is-torsorial-iso-Category :
-      is-contr (Σ (obj-Category C) (iso-Category C A)) →
-      {l : Level} →
-      is-identity-system l (iso-Category C A) A (id-iso-Category C)
-    is-identity-system-iso-is-torsorial-iso-Category =
-      is-identity-system-iso-is-torsorial-iso-Precategory
-        ( precategory-Category C)
-```
-
-### Isomorphism induction implies contractibility of the total space of isomorphisms
-
-```agda
-module _
-  {l1 l2 : Level} (C : Category l1 l2) {A : obj-Category C}
-  where
-
-  is-torsorial-equiv-induction-principle-iso-Category :
-    ( {l : Level} →
-      is-identity-system l (iso-Category C A) A (id-iso-Category C)) →
-    is-contr (Σ (obj-Category C) (iso-Category C A))
-  is-torsorial-equiv-induction-principle-iso-Category =
-    is-torsorial-equiv-induction-principle-iso-Precategory
-      ( precategory-Category C)
-```
-
 ### Isomorphism induction in a category
 
 ```agda
@@ -122,8 +90,10 @@ module _
   abstract
     is-identity-system-iso-Category : section (ev-id-iso-Category C P)
     is-identity-system-iso-Category =
-      is-identity-system-iso-is-torsorial-iso-Category C
-        ( is-torsorial-iso-Category C A) P
+      is-identity-system-is-torsorial-iso-Precategory
+        ( precategory-Category C)
+        ( is-torsorial-iso-Category C A)
+        ( P)
 
   ind-iso-Category :
     P A (id-iso-Category C) →

src/category-theory/isomorphism-induction-precategories.lagda.md

@@ -17,6 +17,7 @@ open import foundation.function-types
 open import foundation.identity-systems
 open import foundation.identity-types
 open import foundation.sections
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -81,11 +82,10 @@ module _
   where
 
   abstract
-    is-identity-system-iso-is-torsorial-iso-Precategory :
-      is-contr (Σ (obj-Precategory C) (iso-Precategory C A)) →
-      {l : Level} →
-      is-identity-system l (iso-Precategory C A) A (id-iso-Precategory C)
-    is-identity-system-iso-is-torsorial-iso-Precategory =
+    is-identity-system-is-torsorial-iso-Precategory :
+      is-torsorial (iso-Precategory C A) →
+      is-identity-system (iso-Precategory C A) A (id-iso-Precategory C)
+    is-identity-system-is-torsorial-iso-Precategory =
       is-identity-system-is-torsorial A (id-iso-Precategory C)
 ```
 
@@ -97,9 +97,8 @@ module _
   where
 
   is-torsorial-equiv-induction-principle-iso-Precategory :
-    ( {l : Level} →
-      is-identity-system l (iso-Precategory C A) A (id-iso-Precategory C)) →
-    is-contr (Σ (obj-Precategory C) (iso-Precategory C A))
+    is-identity-system (iso-Precategory C A) A (id-iso-Precategory C) →
+    is-torsorial (iso-Precategory C A)
   is-torsorial-equiv-induction-principle-iso-Precategory =
     is-torsorial-is-identity-system A (id-iso-Precategory C)
 ```

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

@@ -19,6 +19,7 @@ open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -658,15 +659,15 @@ module _
   where
 
   is-torsorial-iso-Category :
-    is-contr (Σ (obj-Category C) (iso-Category C X))
+    is-torsorial (iso-Category C X)
   is-torsorial-iso-Category =
     is-contr-equiv'
       ( Σ (obj-Category C) (X ＝_))
       ( equiv-tot (extensionality-obj-Category C X))
       ( is-torsorial-path X)
 
   is-torsorial-iso-Category' :
-    is-contr (Σ (obj-Category C) (λ Y → iso-Category C Y X))
+    is-torsorial (λ Y → iso-Category C Y X)
   is-torsorial-iso-Category' =
     is-contr-equiv'
       ( Σ (obj-Category C) (_＝ X))

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

@@ -19,6 +19,7 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -176,7 +177,8 @@ module _
   compute-iso-eq-Large-Category :
     iso-eq-Category (category-Large-Category C l1) X Y ~
     iso-eq-Large-Category
-  compute-iso-eq-Large-Category refl = refl
+  compute-iso-eq-Large-Category =
+    compute-iso-eq-Large-Precategory (large-precategory-Large-Category C) X Y
 
   extensionality-obj-Large-Category :
     (X ＝ Y) ≃ iso-Large-Category C X Y
@@ -192,15 +194,15 @@ module _
   where
 
   is-torsorial-iso-Large-Category :
-    is-contr (Σ (obj-Large-Category C l1) (iso-Large-Category C X))
+    is-torsorial (iso-Large-Category C X)
   is-torsorial-iso-Large-Category =
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (X ＝_))
       ( equiv-tot (extensionality-obj-Large-Category C X))
       ( is-torsorial-path X)
 
   is-torsorial-iso-Large-Category' :
-    is-contr (Σ (obj-Large-Category C l1) (λ Y → iso-Large-Category C Y X))
+    is-torsorial (λ Y → iso-Large-Category C Y X)
   is-torsorial-iso-Large-Category' =
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (_＝ X))

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

@@ -140,30 +140,6 @@ module _
   pr2 id-iso-Large-Precategory = is-iso-id-hom-Large-Precategory
 ```
 
-### Equalities induce isomorphisms
-
-An equality between objects `X Y : A` gives rise to an isomorphism between them.
-This is because, by the J-rule, it is enough to construct an isomorphism given
-`refl : X ＝ X`, from `X` to itself. We take the identity morphism as such an
-isomorphism.
-
-```agda
-iso-eq-Large-Precategory :
-  {α : Level → Level} {β : Level → Level → Level} →
-  (C : Large-Precategory α β) {l1 : Level}
-  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l1) →
-  X ＝ Y → iso-Large-Precategory C X Y
-iso-eq-Large-Precategory C X .X refl = id-iso-Large-Precategory C
-
-compute-iso-eq-Large-Precategory :
-  {α : Level → Level} {β : Level → Level → Level} →
-  (C : Large-Precategory α β) {l1 : Level}
-  (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l1) →
-  iso-eq-Precategory (precategory-Large-Precategory C l1) X Y ~
-  iso-eq-Large-Precategory C X Y
-compute-iso-eq-Large-Precategory C X .X refl = refl
-```
-
 ## Properties
 
 ### Being an isomorphism is a proposition
@@ -255,6 +231,35 @@ module _
   pr2 iso-set-Large-Precategory = is-set-iso-Large-Precategory
 ```
 
+### Equalities induce isomorphisms
+
+An equality between objects `X Y : A` gives rise to an isomorphism between them.
+This is because, by the J-rule, it is enough to construct an isomorphism given
+`refl : X ＝ X`, from `X` to itself. We take the identity morphism as such an
+isomorphism.
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  (C : Large-Precategory α β) {l1 : Level}
+  where
+
+  iso-eq-Large-Precategory :
+    (X Y : obj-Large-Precategory C l1) → X ＝ Y → iso-Large-Precategory C X Y
+  pr1 (iso-eq-Large-Precategory X Y p) = hom-eq-Large-Precategory C X Y p
+  pr2 (iso-eq-Large-Precategory X .X refl) = is-iso-id-hom-Large-Precategory C
+
+  compute-iso-eq-Large-Precategory :
+    (X Y : obj-Large-Precategory C l1) →
+    iso-eq-Precategory (precategory-Large-Precategory C l1) X Y ~
+    iso-eq-Large-Precategory X Y
+  compute-iso-eq-Large-Precategory X Y p =
+    eq-iso-eq-hom-Large-Precategory C
+      ( iso-eq-Precategory (precategory-Large-Precategory C l1) X Y p)
+      ( iso-eq-Large-Precategory X Y p)
+      ( compute-hom-eq-Large-Precategory C X Y p)
+```
+
 ### Isomorphisms are closed under composition
 
 ```agda

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

@@ -164,7 +164,8 @@ module _
   iso-eq-Precategory :
     (x y : obj-Precategory C) →
     x ＝ y → iso-Precategory C x y
-  iso-eq-Precategory x .x refl = id-iso-Precategory C
+  pr1 (iso-eq-Precategory x y p) = hom-eq-Precategory C x y p
+  pr2 (iso-eq-Precategory x .x refl) = is-iso-id-hom-Precategory C
 
   compute-hom-iso-eq-Precategory :
     {x y : obj-Precategory C} →