Merge branch 'master' into monad

src/category-theory/groupoids.lagda.md

@@ -165,12 +165,12 @@ module _
               Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl))
                 ( λ (q , l) → p ∙ q ＝ refl))))
         ( is-contr-iterated-Σ 2
-          ( is-torsorial-path x ,
+          ( is-torsorial-Id x ,
             ( x , refl) ,
             ( is-contr-equiv
               ( Σ (x ＝ x) (λ q → q ＝ refl))
               ( equiv-tot (λ q → equiv-concat (inv right-unit) refl))
-              ( is-torsorial-path' refl)) ,
+              ( is-torsorial-Id' refl)) ,
             ( refl , refl) ,
             ( is-proof-irrelevant-is-prop
               ( is-1-type-type-1-Type X x x refl refl)

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

@@ -743,15 +743,15 @@ module _
     is-contr-equiv'
       ( Σ (obj-Category C) (X ＝_))
       ( equiv-tot (extensionality-obj-Category C X))
-      ( is-torsorial-path X)
+      ( is-torsorial-Id X)
 
   is-torsorial-iso-Category' :
     is-torsorial (λ Y → iso-Category C Y X)
   is-torsorial-iso-Category' =
     is-contr-equiv'
       ( Σ (obj-Category C) (_＝ X))
       ( equiv-tot (λ Y → extensionality-obj-Category C Y X))
-      ( is-torsorial-path' X)
+      ( is-torsorial-Id' X)
 ```
 
 ### Functoriality of `eq-iso`

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

@@ -199,15 +199,15 @@ module _
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (X ＝_))
       ( equiv-tot (extensionality-obj-Large-Category C X))
-      ( is-torsorial-path X)
+      ( is-torsorial-Id X)
 
   is-torsorial-iso-Large-Category' :
     is-torsorial (λ Y → iso-Large-Category C Y X)
   is-torsorial-iso-Large-Category' =
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (_＝ X))
       ( equiv-tot (λ Y → extensionality-obj-Large-Category C Y X))
-      ( is-torsorial-path' X)
+      ( is-torsorial-Id' X)
 ```
 
 ## Properties

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

@@ -212,7 +212,7 @@ module _
       ( Σ (hom-Precategory C A X) (λ g → f ＝ g))
       ( equiv-tot
         ( λ g → equiv-concat' f (left-unit-law-comp-hom-Precategory C g)))
-      ( is-torsorial-path f)
+      ( is-torsorial-Id f)
 ```
 
 ### Products in slice precategories are pullbacks in the original category

src/elementary-number-theory/universal-property-integers.lagda.md

@@ -161,7 +161,7 @@ abstract
           ( tot (λ α → right-transpose-eq-concat refl α (pr1 (pr2 s))))
           ( is-equiv-tot-is-fiberwise-equiv
             ( λ α → is-equiv-right-transpose-eq-concat refl α (pr1 (pr2 s))))
-          ( is-torsorial-path' (pr1 (pr2 s))))
+          ( is-torsorial-Id' (pr1 (pr2 s))))
         ( pair (pr1 (pr2 s)) (inv (right-inv (pr1 (pr2 s)))))
         ( is-contr-is-equiv'
           ( Σ ( ( k : ℤ) → Id (pr1 s (succ-ℤ k)) (pr1 (pS k) (pr1 s k)))

src/elementary-number-theory/universal-property-natural-numbers.lagda.md

@@ -69,7 +69,7 @@ module _
       ( is-torsorial-htpy (pr1 h))
       ( pair (pr1 h) refl-htpy)
       ( is-torsorial-Eq-structure
-        ( is-torsorial-path (pr1 (pr2 h)))
+        ( is-torsorial-Id (pr1 (pr2 h)))
         ( pair (pr1 (pr2 h)) refl)
         ( is-torsorial-htpy (λ n → (pr2 (pr2 h) n ∙ refl))))
 

src/foundation-core/contractible-maps.lagda.md

@@ -129,8 +129,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of path-split maps see
   [`foundation.path-split-maps`](foundation.path-split-maps.md).

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

@@ -82,16 +82,16 @@ module _
   where
 
   abstract
-    is-torsorial-path : (a : A) → is-contr (Σ A (λ x → a ＝ x))
-    pr1 (pr1 (is-torsorial-path a)) = a
-    pr2 (pr1 (is-torsorial-path a)) = refl
-    pr2 (is-torsorial-path a) (pair .a refl) = refl
+    is-torsorial-Id : (a : A) → is-contr (Σ A (λ x → a ＝ x))
+    pr1 (pr1 (is-torsorial-Id a)) = a
+    pr2 (pr1 (is-torsorial-Id a)) = refl
+    pr2 (is-torsorial-Id a) (pair .a refl) = refl
 
   abstract
-    is-torsorial-path' : (a : A) → is-contr (Σ A (λ x → x ＝ a))
-    pr1 (pr1 (is-torsorial-path' a)) = a
-    pr2 (pr1 (is-torsorial-path' a)) = refl
-    pr2 (is-torsorial-path' a) (pair .a refl) = refl
+    is-torsorial-Id' : (a : A) → is-contr (Σ A (λ x → x ＝ a))
+    pr1 (pr1 (is-torsorial-Id' a)) = a
+    pr2 (pr1 (is-torsorial-Id' a)) = refl
+    pr2 (is-torsorial-Id' a) (pair .a refl) = refl
 ```
 
 ## Properties

src/foundation-core/equivalences.lagda.md

@@ -749,8 +749,8 @@ syntax step-equivalence-reasoning e Z f = e ≃ Z by f
 
 ## See also
 
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).

src/foundation-core/path-split-maps.lagda.md

@@ -24,9 +24,9 @@ open import foundation-core.sections
 ## Idea
 
 A map `f : A → B` is said to be **path split** if it has a
-[section](foundation-core.sections.md) and its action on
-[identity types](foundation-core.identity-types.md) `Id x y → Id (f x) (f y)`
-has a section for each `x y : A`. By the
+[section](foundation-core.sections.md) and its
+[action on identifications](foundation.action-on-identifications-functions.md)
+`x ＝ y → f x ＝ f y` has a section for each `x y : A`. By the
 [fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md),
 it follows that a map is path-split if and only if it is an
 [equivalence](foundation-core.equivalences.md).
@@ -80,8 +80,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).

src/foundation-core/sets.lagda.md

@@ -147,4 +147,22 @@ abstract
     {l1 l2 : Level} (A : UU l1) {B : UU l2} (e : A ≃ B) →
     is-set A → is-set B
   is-set-equiv' = is-trunc-equiv' zero-𝕋
+
+abstract
+  is-set-equiv-is-set :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
+    is-set A → is-set B → is-set (A ≃ B)
+  is-set-equiv-is-set = is-trunc-equiv-is-trunc zero-𝕋
+
+module _
+  {l1 l2 : Level} (A : Set l1) (B : Set l2)
+  where
+
+  equiv-Set : UU (l1 ⊔ l2)
+  equiv-Set = type-Set A ≃ type-Set B
+
+  equiv-set-Set : Set (l1 ⊔ l2)
+  pr1 equiv-set-Set = equiv-Set
+  pr2 equiv-set-Set =
+    is-set-equiv-is-set (is-set-type-Set A) (is-set-type-Set B)
 ```

src/foundation-core/transport-along-identifications.lagda.md

@@ -110,7 +110,7 @@ module _
 ```agda
 tr-Id-left :
   {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : b ＝ a) →
-  tr (_＝ a) q p ＝ ((inv q) ∙ p)
+  tr (_＝ a) q p ＝ (inv q ∙ p)
 tr-Id-left refl p = refl
 ```
 

src/foundation.lagda.md

@@ -270,6 +270,7 @@ open import foundation.precomposition-type-families public
 open import foundation.preidempotent-maps public
 open import foundation.preimages-of-subtypes public
 open import foundation.preunivalence public
+open import foundation.preunivalent-type-families public
 open import foundation.principle-of-omniscience public
 open import foundation.product-decompositions public
 open import foundation.product-decompositions-subuniverse public
@@ -352,6 +353,7 @@ open import foundation.transport-along-equivalences public
 open import foundation.transport-along-higher-identifications public
 open import foundation.transport-along-homotopies public
 open import foundation.transport-along-identifications public
+open import foundation.transport-split-type-families public
 open import foundation.transposition-span-diagrams public
 open import foundation.trivial-relaxed-sigma-decompositions public
 open import foundation.trivial-sigma-decompositions public

src/foundation/category-of-sets.lagda.md

@@ -68,7 +68,7 @@ is-large-category-Set-Large-Precategory :
 is-large-category-Set-Large-Precategory {l} X =
   fundamental-theorem-id
     ( is-contr-equiv'
-      ( Σ (Set l) (type-equiv-Set X))
+      ( Σ (Set l) (equiv-Set X))
       ( equiv-tot (equiv-iso-equiv-Set X))
       ( is-torsorial-equiv-Set X))
     ( iso-eq-Set X)

src/foundation/contractible-maps.lagda.md

@@ -133,8 +133,8 @@ module _
 
 - For the notion of biinvertible maps see
   [`foundation.equivalences`](foundation.equivalences.md).
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of path-split maps see
   [`foundation.path-split-maps`](foundation.path-split-maps.md).

src/foundation/embeddings.lagda.md

@@ -279,7 +279,7 @@ module _
   is-section-inv-map-Σ-emb-base (b , c) =
     ap
       ( λ s → (pr1 s , inv-tr C (pr2 s) c))
-      ( eq-is-contr (is-torsorial-path' b))
+      ( eq-is-contr (is-torsorial-Id' b))
 
   is-retraction-inv-map-Σ-emb-base :
     is-retraction (map-Σ-map-base (map-emb f) C) inv-map-Σ-emb-base
@@ -322,9 +322,9 @@ module _
 
   abstract
     is-emb-section-ap :
-      ((x y : A) → section (ap f {x = x} {y = y})) → is-emb f
-    is-emb-section-ap section-ap-f x y =
-      fundamental-theorem-id-section x (λ y → ap f {y = y}) (section-ap-f x) y
+      ((x y : A) → section (ap f {x} {y})) → is-emb f
+    is-emb-section-ap section-ap-f x =
+      fundamental-theorem-id-section x (λ y → ap f) (section-ap-f x)
 ```
 
 ### If there is an equivalence `(f x = f y) ≃ (x = y)` that sends `refl` to `refl`, then f is an embedding

src/foundation/equality-coproduct-types.lagda.md

@@ -230,7 +230,7 @@ module _
         ( is-contr-equiv
           ( Σ A (Id x))
           ( equiv-tot (compute-eq-coprod-inl-inl x))
-          ( is-torsorial-path x))
+          ( is-torsorial-Id x))
         ( λ y → ap inl)
 
   emb-inl : A ↪ (A + B)
@@ -244,7 +244,7 @@ module _
         ( is-contr-equiv
           ( Σ B (Id x))
           ( equiv-tot (compute-eq-coprod-inr-inr x))
-          ( is-torsorial-path x))
+          ( is-torsorial-Id x))
         ( λ y → ap inr)
 
   emb-inr : B ↪ (A + B)

src/foundation/equivalences-maybe.lagda.md

@@ -380,6 +380,11 @@ equiv-equiv-Maybe :
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} → (Maybe X ≃ Maybe Y) → (X ≃ Y)
 pr1 (equiv-equiv-Maybe e) = map-equiv-equiv-Maybe e
 pr2 (equiv-equiv-Maybe e) = is-equiv-map-equiv-equiv-Maybe e
+
+compute-equiv-equiv-Maybe-id-equiv :
+  {l1 : Level} {X : UU l1} →
+  equiv-equiv-Maybe id-equiv ＝ id-equiv {A = X}
+compute-equiv-equiv-Maybe-id-equiv = eq-htpy-equiv refl-htpy
 ```
 
 ### For any set `X`, the type of automorphisms on `X` is equivalent to the type of automorphisms on `Maybe X` that fix the exception

src/foundation/equivalences.lagda.md

@@ -805,8 +805,8 @@ module _
 
 ## See also
 
-- For the notions of inverses and coherently invertible maps, also known as
-  half-adjoint equivalences, see
+- For the notion of coherently invertible maps, also known as half-adjoint
+  equivalences, see
   [`foundation.coherently-invertible-maps`](foundation.coherently-invertible-maps.md).
 - For the notion of maps with contractible fibers see
   [`foundation.contractible-maps`](foundation.contractible-maps.md).

src/foundation/families-of-maps.lagda.md

@@ -56,7 +56,7 @@ module _
       ≃ (((x , _) : Σ A B) →
           Σ (Σ A (x ＝_)) λ (x' , _) → C x') by equiv-Π-equiv-family (λ (x , _) →
                                                   inv-left-unit-law-Σ-is-contr
-                                                    (is-torsorial-path x)
+                                                    (is-torsorial-Id x)
                                                     (x , refl))
       ≃ (((x , _) : Σ A B) →
           Σ (Σ A C) λ (x' , _) → x ＝ x') by equiv-Π-equiv-family (λ (x , _) →

src/foundation/functional-correspondences.lagda.md

@@ -155,7 +155,7 @@ module _
     ((x : A) → B x) → functional-correspondence l2 A B
   pr1 (functional-correspondence-function f) x y = f x ＝ y
   pr2 (functional-correspondence-function f) x =
-    is-torsorial-path (f x)
+    is-torsorial-Id (f x)
 
   function-functional-correspondence :
     {l3 : Level} → functional-correspondence l3 A B → ((x : A) → B x)