diff --git a/src/category-theory/groupoids.lagda.md b/src/category-theory/groupoids.lagda.md index de26e339b3..7028c7da72 100644 --- a/src/category-theory/groupoids.lagda.md +++ b/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) diff --git a/src/category-theory/isomorphisms-in-categories.lagda.md b/src/category-theory/isomorphisms-in-categories.lagda.md index b80829fa85..5efbcdb841 100644 --- a/src/category-theory/isomorphisms-in-categories.lagda.md +++ b/src/category-theory/isomorphisms-in-categories.lagda.md @@ -743,7 +743,7 @@ 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) @@ -751,7 +751,7 @@ module _ 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` diff --git a/src/category-theory/isomorphisms-in-large-categories.lagda.md b/src/category-theory/isomorphisms-in-large-categories.lagda.md index cfa72bca82..e6f13cb68a 100644 --- a/src/category-theory/isomorphisms-in-large-categories.lagda.md +++ b/src/category-theory/isomorphisms-in-large-categories.lagda.md @@ -199,7 +199,7 @@ 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) @@ -207,7 +207,7 @@ module _ 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 diff --git a/src/category-theory/slice-precategories.lagda.md b/src/category-theory/slice-precategories.lagda.md index 2e0eb5f494..101b4b7712 100644 --- a/src/category-theory/slice-precategories.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/universal-property-integers.lagda.md b/src/elementary-number-theory/universal-property-integers.lagda.md index 3602311b47..a8689cf3e8 100644 --- a/src/elementary-number-theory/universal-property-integers.lagda.md +++ b/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))) diff --git a/src/elementary-number-theory/universal-property-natural-numbers.lagda.md b/src/elementary-number-theory/universal-property-natural-numbers.lagda.md index 9044063f8b..5edeebe5cc 100644 --- a/src/elementary-number-theory/universal-property-natural-numbers.lagda.md +++ b/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)))) diff --git a/src/foundation-core/contractible-maps.lagda.md b/src/foundation-core/contractible-maps.lagda.md index 4016cecbd3..46a3cecce5 100644 --- a/src/foundation-core/contractible-maps.lagda.md +++ b/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). diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md index 3d2821c664..afb4ad31b8 100644 --- a/src/foundation-core/contractible-types.lagda.md +++ b/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 diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md index 4fdf05534e..2010a4a555 100644 --- a/src/foundation-core/equivalences.lagda.md +++ b/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). diff --git a/src/foundation-core/path-split-maps.lagda.md b/src/foundation-core/path-split-maps.lagda.md index 66ae437fa4..c2b94a4453 100644 --- a/src/foundation-core/path-split-maps.lagda.md +++ b/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). diff --git a/src/foundation-core/sets.lagda.md b/src/foundation-core/sets.lagda.md index cecd9e33de..603e8413ec 100644 --- a/src/foundation-core/sets.lagda.md +++ b/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) ``` diff --git a/src/foundation-core/transport-along-identifications.lagda.md b/src/foundation-core/transport-along-identifications.lagda.md index 67ef4e293d..968011e96f 100644 --- a/src/foundation-core/transport-along-identifications.lagda.md +++ 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 ``` diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 1adc44d8a8..1badf21b0d 100644 --- a/src/foundation.lagda.md +++ b/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 diff --git a/src/foundation/category-of-sets.lagda.md b/src/foundation/category-of-sets.lagda.md index be56947a17..803e007a6a 100644 --- a/src/foundation/category-of-sets.lagda.md +++ b/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) diff --git a/src/foundation/contractible-maps.lagda.md b/src/foundation/contractible-maps.lagda.md index df0d7ac4bc..15c5bb6786 100644 --- a/src/foundation/contractible-maps.lagda.md +++ b/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). diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md index d231edfd31..49b66be7e3 100644 --- a/src/foundation/embeddings.lagda.md +++ b/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 diff --git a/src/foundation/equality-coproduct-types.lagda.md b/src/foundation/equality-coproduct-types.lagda.md index 6252418e66..ea0ad0ca29 100644 --- a/src/foundation/equality-coproduct-types.lagda.md +++ b/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) diff --git a/src/foundation/equivalences-maybe.lagda.md b/src/foundation/equivalences-maybe.lagda.md index 5a38bc210b..47f52136b4 100644 --- a/src/foundation/equivalences-maybe.lagda.md +++ 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 diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md index e3e695b440..59256d5b1e 100644 --- a/src/foundation/equivalences.lagda.md +++ b/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). diff --git a/src/foundation/families-of-maps.lagda.md b/src/foundation/families-of-maps.lagda.md index 94ab9ec72e..79070bc5ac 100644 --- a/src/foundation/families-of-maps.lagda.md +++ b/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 , _) → diff --git a/src/foundation/functional-correspondences.lagda.md b/src/foundation/functional-correspondences.lagda.md index dcc17b0b4b..7bf1fe2d0c 100644 --- a/src/foundation/functional-correspondences.lagda.md +++ b/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) diff --git a/src/foundation/fundamental-theorem-of-identity-types.lagda.md b/src/foundation/fundamental-theorem-of-identity-types.lagda.md index 5090cca6f8..9614810977 100644 --- a/src/foundation/fundamental-theorem-of-identity-types.lagda.md +++ b/src/foundation/fundamental-theorem-of-identity-types.lagda.md @@ -8,11 +8,13 @@ module foundation.fundamental-theorem-of-identity-types where ```agda open import foundation.dependent-pair-types +open import foundation.retracts-of-types open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.families-of-equivalences +open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types @@ -59,7 +61,7 @@ module _ is-torsorial B → (f : (x : A) → a ＝ x → B x) → is-fiberwise-equiv f fundamental-theorem-id is-contr-AB f = is-fiberwise-equiv-is-equiv-tot - ( is-equiv-is-contr (tot f) (is-torsorial-path a) is-contr-AB) + ( is-equiv-is-contr (tot f) (is-torsorial-Id a) is-contr-AB) abstract fundamental-theorem-id' : @@ -69,7 +71,7 @@ module _ ( Σ A (Id a)) ( tot f) ( is-equiv-tot-is-fiberwise-equiv is-fiberwise-equiv-f) - ( is-torsorial-path a) + ( is-torsorial-Id a) ``` ## Corollaries @@ -87,13 +89,13 @@ module _ abstract fundamental-theorem-id-J' : - (is-fiberwise-equiv (ind-Id a (λ x p → B x) b)) → is-torsorial B + is-fiberwise-equiv (ind-Id a (λ x p → B x) b) → is-torsorial B fundamental-theorem-id-J' H = is-contr-is-equiv' ( Σ A (Id a)) ( tot (ind-Id a (λ x p → B x) b)) ( is-equiv-tot-is-fiberwise-equiv H) - ( is-torsorial-path a) + ( is-torsorial-Id a) ``` ### Retracts of the identity type are equivalent to the identity type @@ -105,18 +107,29 @@ module _ abstract fundamental-theorem-id-retraction : - (i : (x : A) → B x → a ＝ x) → (R : (x : A) → retraction (i x)) → + (i : (x : A) → B x → a ＝ x) → + ((x : A) → retraction (i x)) → is-fiberwise-equiv i fundamental-theorem-id-retraction i R = is-fiberwise-equiv-is-equiv-tot ( is-equiv-is-contr (tot i) - ( is-contr-retract-of (Σ _ (λ y → a ＝ y)) - ( pair (tot i) - ( pair (tot λ x → pr1 (R x)) - ( ( inv-htpy (preserves-comp-tot i (λ x → pr1 (R x)))) ∙h - ( ( tot-htpy λ x → pr2 (R x)) ∙h (tot-id B))))) - ( is-torsorial-path a)) - ( is-torsorial-path a)) + ( is-contr-retract-of + ( Σ _ (λ y → a ＝ y)) + ( ( tot i) , + ( tot (λ x → pr1 (R x))) , + ( ( inv-htpy (preserves-comp-tot i (pr1 ∘ R))) ∙h + ( tot-htpy (pr2 ∘ R)) ∙h + ( tot-id B))) + ( is-torsorial-Id a)) + ( is-torsorial-Id a)) + + fundamental-theorem-id-retract : + (R : (x : A) → (B x) retract-of (a ＝ x)) → + is-fiberwise-equiv (inclusion-retract ∘ R) + fundamental-theorem-id-retract R = + fundamental-theorem-id-retraction + ( inclusion-retract ∘ R) + ( retraction-retract ∘ R) ``` ### The fundamental theorem of identity types, using sections @@ -128,19 +141,18 @@ module _ abstract fundamental-theorem-id-section : - (f : (x : A) → a ＝ x → B x) → ((x : A) → section (f x)) → + (f : (x : A) → a ＝ x → B x) → + ((x : A) → section (f x)) → is-fiberwise-equiv f fundamental-theorem-id-section f section-f x = - is-equiv-section-is-equiv (f x) (section-f x) (is-fiberwise-equiv-i x) - where - i : (x : A) → B x → a ＝ x - i = λ x → pr1 (section-f x) - retraction-i : (x : A) → retraction (i x) - pr1 (retraction-i x) = f x - pr2 (retraction-i x) = pr2 (section-f x) - is-fiberwise-equiv-i : is-fiberwise-equiv i - is-fiberwise-equiv-i = - fundamental-theorem-id-retraction a i retraction-i + is-equiv-section-is-equiv + ( f x) + ( section-f x) + ( fundamental-theorem-id-retraction + ( a) + ( λ x → map-section (f x) (section-f x)) + ( λ x → (f x , is-section-map-section (f x) (section-f x))) + ( x)) ``` ## See also diff --git a/src/foundation/homotopy-induction.lagda.md b/src/foundation/homotopy-induction.lagda.md index 4c35f92ee6..da645df1f2 100644 --- a/src/foundation/homotopy-induction.lagda.md +++ b/src/foundation/homotopy-induction.lagda.md @@ -90,7 +90,7 @@ module _ is-contr-equiv' ( Σ ((x : A) → B x) (Id f)) ( equiv-tot (λ g → equiv-funext)) - ( is-torsorial-path f) + ( is-torsorial-Id f) abstract is-torsorial-htpy' : is-torsorial (λ g → g ~ f) @@ -98,7 +98,7 @@ module _ is-contr-equiv' ( Σ ((x : A) → B x) (λ g → g ＝ f)) ( equiv-tot (λ g → equiv-funext)) - ( is-torsorial-path' f) + ( is-torsorial-Id' f) ``` ### Homotopy induction is equivalent to function extensionality diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md index 4829557c6b..44e04f05f9 100644 --- a/src/foundation/identity-systems.lagda.md +++ b/src/foundation/identity-systems.lagda.md @@ -15,6 +15,7 @@ open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.families-of-equivalences open import foundation-core.identity-types +open import foundation-core.propositions open import foundation-core.sections open import foundation-core.torsorial-type-families open import foundation-core.transport-along-identifications @@ -59,11 +60,11 @@ module _ ```agda module _ - {l1 l2 : Level} {A : UU l1} (B : A → UU l2) (a : A) (b : B a) - where + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) (a : A) (b : B a) + where - is-identity-system : UUω - is-identity-system = {l : Level} → is-identity-system-Level l B a b + is-identity-system : UUω + is-identity-system = {l : Level} → is-identity-system-Level l B a b ``` ## Properties diff --git a/src/foundation/images.lagda.md b/src/foundation/images.lagda.md index ac7b172c3c..f678e73231 100644 --- a/src/foundation/images.lagda.md +++ b/src/foundation/images.lagda.md @@ -94,7 +94,7 @@ module _ (x : im f) → is-torsorial (Eq-im x) is-torsorial-Eq-im x = is-torsorial-Eq-subtype - ( is-torsorial-path (pr1 x)) + ( is-torsorial-Id (pr1 x)) ( λ x → is-prop-type-trunc-Prop) ( pr1 x) ( refl) diff --git a/src/foundation/isomorphisms-of-sets.lagda.md b/src/foundation/isomorphisms-of-sets.lagda.md index f13a4ac68e..c1f3c53125 100644 --- a/src/foundation/isomorphisms-of-sets.lagda.md +++ b/src/foundation/isomorphisms-of-sets.lagda.md @@ -73,15 +73,15 @@ module _ ( htpy-eq (pr1 (pr2 H))) ( htpy-eq (pr2 (pr2 H))) - iso-equiv-Set : type-equiv-Set A B → iso-Set + iso-equiv-Set : equiv-Set A B → iso-Set pr1 (iso-equiv-Set e) = map-equiv e pr2 (iso-equiv-Set e) = is-iso-is-equiv-Set (is-equiv-map-equiv e) - equiv-iso-Set : iso-Set → type-equiv-Set A B + equiv-iso-Set : iso-Set → equiv-Set A B pr1 (equiv-iso-Set f) = map-iso-Set f pr2 (equiv-iso-Set f) = is-equiv-is-iso-Set (is-iso-map-iso-Set f) - equiv-iso-equiv-Set : type-equiv-Set A B ≃ iso-Set + equiv-iso-equiv-Set : equiv-Set A B ≃ iso-Set equiv-iso-equiv-Set = equiv-type-subtype ( is-property-is-equiv) diff --git a/src/foundation/logical-equivalences.lagda.md b/src/foundation/logical-equivalences.lagda.md index 4df5fd6e56..b6cbf82ad8 100644 --- a/src/foundation/logical-equivalences.lagda.md +++ b/src/foundation/logical-equivalences.lagda.md @@ -165,7 +165,7 @@ compute-fiber-iff-equiv : fiber (iff-equiv) (f , g) ≃ Σ (is-equiv f) (λ f' → map-inv-is-equiv f' ~ g) compute-fiber-iff-equiv {A = A} {B} (f , g) = ( equiv-tot (λ _ → equiv-funext)) ∘e - ( left-unit-law-Σ-is-contr (is-torsorial-path' f) (f , refl)) ∘e + ( left-unit-law-Σ-is-contr (is-torsorial-Id' f) (f , refl)) ∘e ( inv-associative-Σ (A → B) (_＝ f) _) ∘e ( equiv-tot (λ _ → equiv-left-swap-Σ)) ∘e ( associative-Σ (A → B) _ _) ∘e diff --git a/src/foundation/multivariable-homotopies.lagda.md b/src/foundation/multivariable-homotopies.lagda.md index 48783bc3f8..49f9ff4882 100644 --- a/src/foundation/multivariable-homotopies.lagda.md +++ b/src/foundation/multivariable-homotopies.lagda.md @@ -194,7 +194,7 @@ abstract is-torsorial-multivariable-htpy : {l : Level} (n : ℕ) {{A : telescope l n}} (f : iterated-Π A) → is-torsorial (multivariable-htpy {{A}} f) - is-torsorial-multivariable-htpy .0 {{base-telescope A}} = is-torsorial-path + is-torsorial-multivariable-htpy .0 {{base-telescope A}} = is-torsorial-Id is-torsorial-multivariable-htpy ._ {{cons-telescope A}} f = is-torsorial-Eq-Π (λ x → is-torsorial-multivariable-htpy _ {{A x}} (f x)) @@ -206,7 +206,7 @@ abstract is-contr-equiv' ( Σ (iterated-implicit-Π A) (Id {A = iterated-implicit-Π A} f)) ( equiv-tot (λ _ → equiv-iterated-funext-implicit _ {{A}})) - ( is-torsorial-path {A = iterated-implicit-Π A} f) + ( is-torsorial-Id {A = iterated-implicit-Π A} f) abstract is-torsorial-multivariable-implicit-htpy : diff --git a/src/foundation/pairs-of-distinct-elements.lagda.md b/src/foundation/pairs-of-distinct-elements.lagda.md index 92ad06dd75..8b152f6408 100644 --- a/src/foundation/pairs-of-distinct-elements.lagda.md +++ b/src/foundation/pairs-of-distinct-elements.lagda.md @@ -84,10 +84,10 @@ module _ is-torsorial (Eq-pair-of-distinct-elements p) is-torsorial-Eq-pair-of-distinct-elements p = is-torsorial-Eq-structure - ( is-torsorial-path (first-pair-of-distinct-elements p)) + ( is-torsorial-Id (first-pair-of-distinct-elements p)) ( pair (first-pair-of-distinct-elements p) refl) ( is-torsorial-Eq-subtype - ( is-torsorial-path (second-pair-of-distinct-elements p)) + ( is-torsorial-Id (second-pair-of-distinct-elements p)) ( λ x → is-prop-neg) ( second-pair-of-distinct-elements p) ( refl) diff --git a/src/foundation/partitions.lagda.md b/src/foundation/partitions.lagda.md index 220e28ce32..9f37022516 100644 --- a/src/foundation/partitions.lagda.md +++ b/src/foundation/partitions.lagda.md @@ -641,7 +641,7 @@ module _ ( subtype-inhabited-subtype Q x)) ∘e ( equiv-inv-equiv))) ∘e ( left-unit-law-Σ-is-contr - ( is-torsorial-path (index-Set-Indexed-Σ-Decomposition D a)) + ( is-torsorial-Id (index-Set-Indexed-Σ-Decomposition D a)) ( pair ( index-Set-Indexed-Σ-Decomposition D a) ( refl)))) ∘e diff --git a/src/foundation/path-split-maps.lagda.md b/src/foundation/path-split-maps.lagda.md index a55bbed9d3..57d49b87c3 100644 --- a/src/foundation/path-split-maps.lagda.md +++ b/src/foundation/path-split-maps.lagda.md @@ -74,8 +74,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). diff --git a/src/foundation/preunivalence.lagda.md b/src/foundation/preunivalence.lagda.md index be874acfdd..298f482891 100644 --- a/src/foundation/preunivalence.lagda.md +++ b/src/foundation/preunivalence.lagda.md @@ -107,4 +107,5 @@ preunivalence = preunivalence-axiom-univalence-axiom univalence - Preunivalence is sufficient to prove that `Id : A → (A → 𝒰)` is an embedding. This fact is proven in [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md) +- [Preunivalent type families](foundation.preunivalent-type-families.md) - [Preunivalent categories](category-theory.preunivalent-categories.md) diff --git a/src/foundation/preunivalent-type-families.lagda.md b/src/foundation/preunivalent-type-families.lagda.md new file mode 100644 index 0000000000..5d647dfedd --- /dev/null +++ b/src/foundation/preunivalent-type-families.lagda.md @@ -0,0 +1,177 @@ +# Preunivalent type families + +```agda +module foundation.preunivalent-type-families where +``` + +
Imports + +```agda +open import foundation.0-maps +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.embeddings +open import foundation.equivalence-injective-type-families +open import foundation.faithful-maps +open import foundation.function-types +open import foundation.preunivalence +open import foundation.retractions +open import foundation.subuniverses +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import foundation-core.equivalences +open import foundation-core.identity-types +open import foundation-core.injective-maps +open import foundation-core.sets +open import foundation-core.univalence +``` + +
+ +## Idea + +A type family `B` over `A` is said to be +{{#concept "preunivalent" Disambiguation="type family" Agda=is-preunivalent}} if +the map + +```text + equiv-tr B : x ＝ y → B x ≃ B y +``` + +is an [embedding](foundation-core.embeddings.md) for every `x y : A`. + +## Definition + +```agda +is-preunivalent : + {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2) +is-preunivalent {A = A} B = (x y : A) → is-emb (λ (p : x ＝ y) → equiv-tr B p) +``` + +## Properties + +### Assuming the preunivalence axiom, type families are preunivalent if and only if they are faithful as maps + +**Proof:** We have the +[commuting triangle of maps](foundation-core.commuting-triangles-of-maps.md) + +```text + ap B + (x ＝ y) -----> (B x ＝ B y) + \ / + \ / + equiv-tr B \ / equiv-eq + v v + (B x ≃ B y) +``` + +where the right edge is an embedding by the +[preunivalence axiom](foundation.preunivalence.md). Hence, the top map is an +embedding if and only if the left map is. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + abstract + is-faithful-is-preunivalent : + is-preunivalent B → is-faithful B + is-faithful-is-preunivalent U x y = + is-emb-top-map-triangle + ( equiv-tr B) + ( equiv-eq) + ( ap B) + ( λ where refl → refl) + ( preunivalence (B x) (B y)) + ( U x y) + + is-preunivalent-is-faithful : + is-faithful B → is-preunivalent B + is-preunivalent-is-faithful is-faithful-B x y = + is-emb-left-map-triangle + ( equiv-tr B) + ( equiv-eq) + ( ap B) + ( λ where refl → refl) + ( preunivalence (B x) (B y)) + ( is-faithful-B x y) + + is-0-map-is-preunivalent : + is-preunivalent B → is-0-map B + is-0-map-is-preunivalent U = + is-0-map-is-faithful (is-faithful-is-preunivalent U) + + is-preunivalent-is-0-map : + is-0-map B → is-preunivalent B + is-preunivalent-is-0-map H = + is-preunivalent-is-faithful (is-faithful-is-0-map H) +``` + +### Families of sets are preunivalent if `equiv-tr` is fiberwise injective + +```agda +module _ + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) + (is-set-B : (x : A) → is-set (B x)) + where + + is-preunivalent-is-injective-equiv-tr-is-set : + ((x y : A) → is-injective (equiv-tr B {x} {y})) → + is-preunivalent B + is-preunivalent-is-injective-equiv-tr-is-set is-inj-B x y = + is-emb-is-injective + ( is-set-equiv-is-set (is-set-B x) (is-set-B y)) + ( is-inj-B x y) + + is-preunivalent-retraction-equiv-tr-is-set : + ((x y : A) → retraction (equiv-tr B {x} {y})) → + is-preunivalent B + is-preunivalent-retraction-equiv-tr-is-set R = + is-preunivalent-is-injective-equiv-tr-is-set + ( λ x y → is-injective-retraction (equiv-tr B) (R x y)) + +module _ + {l1 l2 : Level} {A : UU l1} (B : A → Set l2) + where + + is-preunivalent-is-injective-equiv-tr-Set : + ((x y : A) → is-injective (equiv-tr (type-Set ∘ B) {x} {y})) → + is-preunivalent (type-Set ∘ B) + is-preunivalent-is-injective-equiv-tr-Set = + is-preunivalent-is-injective-equiv-tr-is-set + ( type-Set ∘ B) + ( is-set-type-Set ∘ B) + + is-preunivalent-retraction-equiv-tr-Set : + ((x y : A) → retraction (equiv-tr (type-Set ∘ B) {x} {y})) → + is-preunivalent (type-Set ∘ B) + is-preunivalent-retraction-equiv-tr-Set = + is-preunivalent-retraction-equiv-tr-is-set + ( type-Set ∘ B) + ( is-set-type-Set ∘ B) +``` + +### Inclusions of subuniverses into the universe are preunivalent + +**Note.** These proofs rely on essential use of the preunivalence axiom. + +```agda +is-preunivalent-projection-Type-With-Set-Element : + {l1 l2 : Level} (S : UU l1 → Set l2) → + is-preunivalent (pr1 {A = UU l1} {B = type-Set ∘ S}) +is-preunivalent-projection-Type-With-Set-Element S = + is-preunivalent-is-0-map (is-0-map-pr1 (is-set-type-Set ∘ S)) + +is-preunivalent-inclusion-subuniverse : + {l1 l2 : Level} (S : subuniverse l1 l2) → + is-preunivalent (inclusion-subuniverse S) +is-preunivalent-inclusion-subuniverse S = + is-preunivalent-projection-Type-With-Set-Element (set-Prop ∘ S) +``` + +## See also + +- [Univalent type families](foundation.univalent-type-families.md) +- [Transport-split type families](foundation.transport-split-type-families.md) diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md index 64af30d769..2f4d48bdf0 100644 --- a/src/foundation/pullbacks.lagda.md +++ b/src/foundation/pullbacks.lagda.md @@ -1145,11 +1145,11 @@ module _ ( c) ( cone-ap' c1)) ( is-equiv-is-contr _ - ( is-torsorial-path (horizontal-map-cone f g c c1)) - ( is-torsorial-path (f (vertical-map-cone f g c c1)))) + ( is-torsorial-Id (horizontal-map-cone f g c c1)) + ( is-torsorial-Id (f (vertical-map-cone f g c c1)))) ( is-equiv-is-contr _ - ( is-torsorial-path c1) - ( is-torsorial-path (vertical-map-cone f g c c1)))) + ( is-torsorial-Id c1) + ( is-torsorial-Id (vertical-map-cone f g c c1)))) ( c2)) ``` diff --git a/src/foundation/russells-paradox.lagda.md b/src/foundation/russells-paradox.lagda.md index a3552d5d08..d4ac4625c8 100644 --- a/src/foundation/russells-paradox.lagda.md +++ b/src/foundation/russells-paradox.lagda.md @@ -129,7 +129,7 @@ paradox-Russell {l} H = β = ( equiv-precomp α empty) ∘e ( ( left-unit-law-Σ-is-contr { B = λ t → (pr1 t) ∉-𝕍 (pr1 t)} - ( is-torsorial-path' R') + ( is-torsorial-Id' R') ( pair R' refl)) ∘e ( ( inv-associative-Σ (𝕍 l) (_＝ R') (λ t → (pr1 t) ∉-𝕍 (pr1 t))) ∘e ( ( equiv-tot diff --git a/src/foundation/sections.lagda.md b/src/foundation/sections.lagda.md index 7854512e21..86de6b12bb 100644 --- a/src/foundation/sections.lagda.md +++ b/src/foundation/sections.lagda.md @@ -139,7 +139,7 @@ module _ ( is-contr-equiv ( Π-total-fam (λ x y → y ＝ x)) ( inv-distributive-Π-Σ) - ( is-contr-Π is-torsorial-path')) + ( is-contr-Π is-torsorial-Id')) ( id , refl-htpy)) ∘e ( equiv-right-swap-Σ) ∘e ( equiv-Σ-equiv-base ( λ s → pr1 s ~ id) ( distributive-Π-Σ)) diff --git a/src/foundation/sequential-limits.lagda.md b/src/foundation/sequential-limits.lagda.md index 3910a4a89b..c01524227e 100644 --- a/src/foundation/sequential-limits.lagda.md +++ b/src/foundation/sequential-limits.lagda.md @@ -193,7 +193,7 @@ module _ is-torsorial-Eq-structure ( is-torsorial-htpy (pr1 s)) ( pr1 s , refl-htpy) - ( is-torsorial-Eq-Π (λ n → is-torsorial-path (pr2 s n ∙ refl))) + ( is-torsorial-Eq-Π (λ n → is-torsorial-Id (pr2 s n ∙ refl))) is-equiv-Eq-eq-standard-sequential-limit : (s t : standard-sequential-limit A) → diff --git a/src/foundation/set-truncations.lagda.md b/src/foundation/set-truncations.lagda.md index 8e4f26493e..c5080bce61 100644 --- a/src/foundation/set-truncations.lagda.md +++ b/src/foundation/set-truncations.lagda.md @@ -423,7 +423,7 @@ module _ abstract distributive-trunc-coprod-Set : is-contr - ( Σ ( type-equiv-Set + ( Σ ( equiv-Set ( trunc-Set (A + B)) ( coprod-Set (trunc-Set A) (trunc-Set B))) ( λ e → @@ -451,7 +451,7 @@ module _ ( is-set-truncation-trunc-Set B C)))) equiv-distributive-trunc-coprod-Set : - type-equiv-Set (trunc-Set (A + B)) (coprod-Set (trunc-Set A) (trunc-Set B)) + equiv-Set (trunc-Set (A + B)) (coprod-Set (trunc-Set A) (trunc-Set B)) equiv-distributive-trunc-coprod-Set = pr1 (center distributive-trunc-coprod-Set) diff --git a/src/foundation/sets.lagda.md b/src/foundation/sets.lagda.md index 8799c286aa..862fb3d31a 100644 --- a/src/foundation/sets.lagda.md +++ b/src/foundation/sets.lagda.md @@ -13,6 +13,7 @@ open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.subuniverses open import foundation.truncated-types +open import foundation.univalent-type-families open import foundation.universe-levels open import foundation-core.1-types @@ -23,6 +24,7 @@ open import foundation-core.identity-types open import foundation-core.precomposition-functions open import foundation-core.propositional-maps open import foundation-core.propositions +open import foundation-core.subtypes open import foundation-core.torsorial-type-families open import foundation-core.truncation-levels ``` @@ -173,28 +175,6 @@ precomp-Set : precomp-Set f C = precomp f (type-Set C) ``` -### The type of equivalences between sets is a set - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} - where - - is-set-equiv-is-set : 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 - - type-equiv-Set : UU (l1 ⊔ l2) - type-equiv-Set = type-Set A ≃ type-Set B - - equiv-Set : Set (l1 ⊔ l2) - pr1 equiv-Set = type-equiv-Set - pr2 equiv-Set = is-set-equiv-is-set (is-set-type-Set A) (is-set-type-Set B) -``` - ### Extensionality of sets ```agda @@ -202,11 +182,11 @@ module _ {l : Level} (X : Set l) where - equiv-eq-Set : (Y : Set l) → X ＝ Y → type-equiv-Set X Y + equiv-eq-Set : (Y : Set l) → X ＝ Y → equiv-Set X Y equiv-eq-Set = equiv-eq-subuniverse is-set-Prop X abstract - is-torsorial-equiv-Set : is-torsorial (λ (Y : Set l) → type-equiv-Set X Y) + is-torsorial-equiv-Set : is-torsorial (λ (Y : Set l) → equiv-Set X Y) is-torsorial-equiv-Set = is-torsorial-equiv-subuniverse is-set-Prop X @@ -214,10 +194,10 @@ module _ is-equiv-equiv-eq-Set : (Y : Set l) → is-equiv (equiv-eq-Set Y) is-equiv-equiv-eq-Set = is-equiv-equiv-eq-subuniverse is-set-Prop X - eq-equiv-Set : (Y : Set l) → type-equiv-Set X Y → X ＝ Y + eq-equiv-Set : (Y : Set l) → equiv-Set X Y → X ＝ Y eq-equiv-Set Y = eq-equiv-subuniverse is-set-Prop - extensionality-Set : (Y : Set l) → (X ＝ Y) ≃ type-equiv-Set X Y + extensionality-Set : (Y : Set l) → (X ＝ Y) ≃ equiv-Set X Y pr1 (extensionality-Set Y) = equiv-eq-Set Y pr2 (extensionality-Set Y) = is-equiv-equiv-eq-Set Y ``` @@ -263,3 +243,23 @@ set-Truncated-Type : pr1 (set-Truncated-Type k A) = type-Set A pr2 (set-Truncated-Type k A) = is-trunc-is-set k (is-set-type-Set A) ``` + +### The type of equivalences is a set if the domain or codomain is a set + +```agda +abstract + is-set-equiv-is-set-codomain : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-set B → is-set (A ≃ B) + is-set-equiv-is-set-codomain = is-trunc-equiv-is-trunc-codomain neg-one-𝕋 + + is-set-equiv-is-set-domain : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → is-set A → is-set (A ≃ B) + is-set-equiv-is-set-domain = is-trunc-equiv-is-trunc-domain neg-one-𝕋 +``` + +### The canonical type family over `Set` is univalent + +```agda +is-univalent-type-Set : {l : Level} → is-univalent (type-Set {l}) +is-univalent-type-Set = is-univalent-inclusion-subuniverse is-set-Prop +``` diff --git a/src/foundation/singleton-subtypes.lagda.md b/src/foundation/singleton-subtypes.lagda.md index c8d010b9ae..ed53f6dc71 100644 --- a/src/foundation/singleton-subtypes.lagda.md +++ b/src/foundation/singleton-subtypes.lagda.md @@ -105,7 +105,7 @@ module _ standard-singleton-subtype : singleton-subtype l (type-Set X) pr1 standard-singleton-subtype = subtype-standard-singleton-subtype - pr2 standard-singleton-subtype = is-torsorial-path x + pr2 standard-singleton-subtype = is-torsorial-Id x inhabited-subtype-standard-singleton-subtype : inhabited-subtype l (type-Set X) @@ -248,8 +248,8 @@ module _ ( λ y → ( inv-equiv (equiv-unit-trunc-Prop (Id-Prop Y (f x) y))) ∘e ( equiv-trunc-Prop - ( left-unit-law-Σ-is-contr (is-torsorial-path x) (x , refl))))) - ( is-torsorial-path (f x)) + ( left-unit-law-Σ-is-contr (is-torsorial-Id x) (x , refl))))) + ( is-torsorial-Id (f x)) compute-im-singleton-subtype : has-same-elements-subtype @@ -261,7 +261,7 @@ module _ ( im-subtype f (subtype-standard-singleton-subtype X x)) ( refl) ( unit-trunc-Prop ((x , refl) , refl)) - ( is-torsorial-path (f x)) + ( is-torsorial-Id (f x)) ( is-singleton-im-singleton-subtype) ``` diff --git a/src/foundation/symmetric-identity-types.lagda.md b/src/foundation/symmetric-identity-types.lagda.md index 0f1282b7e5..4390404734 100644 --- a/src/foundation/symmetric-identity-types.lagda.md +++ b/src/foundation/symmetric-identity-types.lagda.md @@ -67,7 +67,7 @@ module _ (p : symmetric-Id a) → is-torsorial (Eq-symmetric-Id p) is-torsorial-Eq-symmetric-Id (x , H) = is-torsorial-Eq-structure - ( is-torsorial-path x) + ( is-torsorial-Id x) ( x , refl) ( is-torsorial-htpy H) diff --git a/src/foundation/transport-along-identifications.lagda.md b/src/foundation/transport-along-identifications.lagda.md index 35d9f29985..0edb4f76e6 100644 --- a/src/foundation/transport-along-identifications.lagda.md +++ b/src/foundation/transport-along-identifications.lagda.md @@ -56,7 +56,7 @@ module _ ( is-section-inv-tr p) ( is-retraction-inv-tr p) - equiv-tr : x ＝ y → (B x) ≃ (B y) + equiv-tr : x ＝ y → B x ≃ B y pr1 (equiv-tr p) = tr B p pr2 (equiv-tr p) = is-equiv-tr p ``` diff --git a/src/foundation/transport-split-type-families.lagda.md b/src/foundation/transport-split-type-families.lagda.md new file mode 100644 index 0000000000..f4fc0dad2f --- /dev/null +++ b/src/foundation/transport-split-type-families.lagda.md @@ -0,0 +1,158 @@ +# Transport-split type families + +```agda +module foundation.transport-split-type-families where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-equivalences-functions +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.equivalence-extensionality +open import foundation.equivalence-injective-type-families +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.fundamental-theorem-of-identity-types +open import foundation.iterated-dependent-product-types +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.univalent-type-families +open import foundation.universal-property-identity-systems +open import foundation.universe-levels + +open import foundation-core.embeddings +open import foundation-core.identity-types +open import foundation-core.propositions +open import foundation-core.sections +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +A type family `B` over `A` is said to be +{{#concept "transport-split" Disambiguation="type family" Agda=is-transport-split}} +if the map + +```text + equiv-tr B : x ＝ y → B x ≃ B y +``` + +admits a [section](foundation-core.sections.md) for every `x y : A`. By a +corollary of +[the fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md) +every transport-split type family is +[univalent](foundation.univalent-type-families.md), meaning that `equiv-tr B` is +in fact an [equivalence](foundation-core.equivalences.md) for all `x y : A`. + +## Definition + +### Transport-split type families + +```agda +is-transport-split : + {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2) +is-transport-split {A = A} B = + (x y : A) → section (λ (p : x ＝ y) → equiv-tr B p) +``` + +## Properties + +### Transport-split type families are equivalence injective + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + is-equivalence-injective-is-transport-split : + is-transport-split B → is-equivalence-injective B + is-equivalence-injective-is-transport-split s {x} {y} = + map-section (equiv-tr B) (s x y) +``` + +### Transport-split type families are univalent + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + is-transport-split-is-univalent : + is-univalent B → is-transport-split B + is-transport-split-is-univalent U x y = section-is-equiv (U x y) + + is-univalent-is-transport-split : + is-transport-split B → is-univalent B + is-univalent-is-transport-split s x = + fundamental-theorem-id-section x (λ y → equiv-tr B) (s x) +``` + +### The type `is-transport-split` is a proposition + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + is-proof-irrelevant-is-transport-split : + is-proof-irrelevant (is-transport-split B) + is-proof-irrelevant-is-transport-split s = + is-contr-iterated-Π 2 + ( λ x y → + is-contr-section-is-equiv (is-univalent-is-transport-split s x y)) + + is-prop-is-transport-split : + is-prop (is-transport-split B) + is-prop-is-transport-split = + is-prop-is-proof-irrelevant is-proof-irrelevant-is-transport-split +``` + +### Assuming the univalence axiom, type families are transport-split if and only if they are embeddings as maps + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + is-emb-is-transport-split : is-transport-split B → is-emb B + is-emb-is-transport-split s = + is-emb-is-univalent (is-univalent-is-transport-split s) + + is-transport-split-is-emb : is-emb B → is-transport-split B + is-transport-split-is-emb H = + is-transport-split-is-univalent (is-univalent-is-emb H) +``` + +### Transport-split type families satisfy equivalence induction + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + (s : is-transport-split B) + where + + is-torsorial-fam-equiv-is-transport-split : + {x : A} → is-torsorial (λ y → B x ≃ B y) + is-torsorial-fam-equiv-is-transport-split = + is-torsorial-fam-equiv-is-univalent (is-univalent-is-transport-split s) + + dependent-universal-property-identity-system-fam-equiv-is-transport-split : + {x : A} → + dependent-universal-property-identity-system (λ y → B x ≃ B y) id-equiv + dependent-universal-property-identity-system-fam-equiv-is-transport-split = + dependent-universal-property-identity-system-is-torsorial + ( id-equiv) + ( is-torsorial-fam-equiv-is-transport-split) +``` + +## See also + +- [Univalent type families](foundation.univalent-type-families.md) +- [Preunivalent type families](foundation.preunivalent-type-families.md) diff --git a/src/foundation/truncated-types.lagda.md b/src/foundation/truncated-types.lagda.md index 33d95d4812..3adb80b12a 100644 --- a/src/foundation/truncated-types.lagda.md +++ b/src/foundation/truncated-types.lagda.md @@ -12,13 +12,13 @@ open import foundation-core.truncated-types public open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types +open import foundation.equivalences open import foundation.subtype-identity-principle open import foundation.truncation-levels open import foundation.univalence open import foundation.universe-levels open import foundation-core.embeddings -open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.subtypes @@ -110,3 +110,32 @@ module _ ( is-trunc-equiv' k A e) ( is-trunc-equiv k B e) ``` + +### If the domain or codomain is `k+1`-truncated, then the type of equivalences is `k+1`-truncated + +```agda +module _ + {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} + where + + is-trunc-equiv-is-trunc-codomain : + is-trunc (succ-𝕋 k) B → is-trunc (succ-𝕋 k) (A ≃ B) + is-trunc-equiv-is-trunc-codomain is-trunc-B = + is-trunc-type-subtype + ( k) + ( is-equiv-Prop) + ( is-trunc-function-type (succ-𝕋 k) is-trunc-B) + +module _ + {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : UU l2} + where + + is-trunc-equiv-is-trunc-domain : + is-trunc (succ-𝕋 k) A → is-trunc (succ-𝕋 k) (A ≃ B) + is-trunc-equiv-is-trunc-domain is-trunc-A = + is-trunc-equiv + ( succ-𝕋 k) + ( B ≃ A) + ( equiv-inv-equiv) + ( is-trunc-equiv-is-trunc-codomain k is-trunc-A) +``` diff --git a/src/foundation/type-duality.lagda.md b/src/foundation/type-duality.lagda.md index 9010140341..bf363dbedf 100644 --- a/src/foundation/type-duality.lagda.md +++ b/src/foundation/type-duality.lagda.md @@ -119,7 +119,7 @@ is-emb-map-type-duality {l} {l1} {A} H (X , f) = ( Σ Y (λ y → type-is-small (H (g y) a)))) ∘e ( equiv-univalence))) ∘e ( equiv-funext))) - ( is-torsorial-path (X , f))) + ( is-torsorial-Id (X , f))) ( λ Y → ap (map-type-duality H)) emb-type-duality : diff --git a/src/foundation/univalence.lagda.md b/src/foundation/univalence.lagda.md index 1df7bab84c..1e7f3190b7 100644 --- a/src/foundation/univalence.lagda.md +++ b/src/foundation/univalence.lagda.md @@ -112,7 +112,7 @@ module _ is-contr-equiv' ( Σ (UU l) (λ X → X ＝ A)) ( equiv-tot (λ X → equiv-univalence)) - ( is-torsorial-path' A) + ( is-torsorial-Id' A) ``` ### Univalence for type families diff --git a/src/foundation/univalent-type-families.lagda.md b/src/foundation/univalent-type-families.lagda.md index 8297c1c7a7..d68a061924 100644 --- a/src/foundation/univalent-type-families.lagda.md +++ b/src/foundation/univalent-type-families.lagda.md @@ -7,29 +7,164 @@ module foundation.univalent-type-families where
Imports ```agda +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.fundamental-theorem-of-identity-types +open import foundation.identity-systems +open import foundation.iterated-dependent-product-types +open import foundation.propositions +open import foundation.subuniverses open import foundation.transport-along-identifications +open import foundation.univalence +open import foundation.universal-property-identity-systems open import foundation.universe-levels -open import foundation-core.equivalences +open import foundation-core.embeddings open import foundation-core.identity-types +open import foundation-core.sections +open import foundation-core.torsorial-type-families ```
## Idea -A type family `B` over `A` is said to be univalent if the map +A type family `B` over `A` is said to be +{{#concept "univalent" Disambiguation="type family" Agda=is-univalent}} if the +map ```text - equiv-tr : (Id x y) → (B x ≃ B y) + equiv-tr B : x ＝ y → B x ≃ B y ``` -is an equivalence for every `x y : A`. +is an [equivalence](foundation-core.equivalences.md) for every `x y : A`. By +[the univalence axiom](foundation-core.univalence.md), this is equivalent to the +type family `B` being an [embedding](foundation-core.embeddings.md) considered +as a map. ## Definition +### The predicate on type families of being univalent + ```agda is-univalent : {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2) is-univalent {A = A} B = (x y : A) → is-equiv (λ (p : x ＝ y) → equiv-tr B p) + +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + is-prop-is-univalent : is-prop (is-univalent B) + is-prop-is-univalent = + is-prop-iterated-Π 2 (λ x y → is-property-is-equiv (equiv-tr B)) + + is-univalent-Prop : Prop (l1 ⊔ l2) + pr1 is-univalent-Prop = is-univalent B + pr2 is-univalent-Prop = is-prop-is-univalent +``` + +### Univalent type families + +```agda +univalent-type-family : + {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2) +univalent-type-family l2 A = Σ (A → UU l2) is-univalent +``` + +## Properties + +### Assuming the univalence axiom, type families are univalent if and only if they are embeddings as maps + +**Proof:** We have the +[commuting triangle of maps](foundation-core.commuting-triangles-of-maps.md) + +```text + ap B + (x ＝ y) -----> (B x ＝ B y) + \ / + \ / + equiv-tr B \ / equiv-eq + v v + (B x ≃ B y) +``` + +where the right edge is an equivalence by the univalence axiom. Hence, the top +map is an equivalence if and only if the left map is. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + where + + abstract + is-emb-is-univalent : + is-univalent B → is-emb B + is-emb-is-univalent U x y = + is-equiv-top-map-triangle + ( equiv-tr B) + ( equiv-eq) + ( ap B) + ( λ where refl → refl) + ( univalence (B x) (B y)) + ( U x y) + + is-univalent-is-emb : + is-emb B → is-univalent B + is-univalent-is-emb is-emb-B x y = + is-equiv-left-map-triangle + ( equiv-tr B) + ( equiv-eq) + ( ap B) + ( λ where refl → refl) + ( is-emb-B x y) + ( univalence (B x) (B y)) +``` + +### Univalent type families satisfy equivalence induction + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : A → UU l2} + (U : is-univalent B) + where + + is-torsorial-fam-equiv-is-univalent : + {x : A} → is-torsorial (λ y → B x ≃ B y) + is-torsorial-fam-equiv-is-univalent {x} = + fundamental-theorem-id' (λ y → equiv-tr B) (U x) + + dependent-universal-property-identity-system-fam-equiv-is-univalent : + {x : A} → + dependent-universal-property-identity-system (λ y → B x ≃ B y) id-equiv + dependent-universal-property-identity-system-fam-equiv-is-univalent {x} = + dependent-universal-property-identity-system-is-torsorial + ( id-equiv) + ( is-torsorial-fam-equiv-is-univalent {x}) ``` + +### Inclusions of subuniverses into the universe are univalent + +**Note.** This proof relies on essential use of the univalence axiom. + +```agda +module _ + {l1 l2 : Level} (S : subuniverse l1 l2) + where + + is-univalent-inclusion-subuniverse : is-univalent (inclusion-subuniverse S) + is-univalent-inclusion-subuniverse = + is-univalent-is-emb (is-emb-inclusion-subuniverse S) +``` + +## See also + +- [Preunivalent type families](foundation.preunivalent-type-families.md) +- [Transport-split type families](foundation.transport-split-type-families.md): + By a corollary of + [the fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md), + `equiv-tr B` is a + [fiberwise equivalence](foundation-core.families-of-equivalences.md) as soon + as it admits a fiberwise [section](foundation-core.sections.md). diff --git a/src/foundation/universal-property-identity-systems.lagda.md b/src/foundation/universal-property-identity-systems.lagda.md index 8748ea89d0..a29595fa9d 100644 --- a/src/foundation/universal-property-identity-systems.lagda.md +++ b/src/foundation/universal-property-identity-systems.lagda.md @@ -36,8 +36,8 @@ also follows for identity systems. ```agda dependent-universal-property-identity-system : - {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {a : A} (b : B a) → UUω -dependent-universal-property-identity-system {A = A} {B} b = + {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {a : A} (b : B a) → UUω +dependent-universal-property-identity-system {A = A} B b = {l3 : Level} (P : (x : A) (y : B x) → UU l3) → is-equiv (ev-refl-identity-system b {P}) ``` @@ -53,7 +53,7 @@ module _ dependent-universal-property-identity-system-is-torsorial : is-torsorial B → - dependent-universal-property-identity-system {B = B} b + dependent-universal-property-identity-system B b dependent-universal-property-identity-system-is-torsorial H P = is-equiv-left-factor @@ -75,7 +75,7 @@ module _ dependent-universal-property-identity-system-is-torsorial H _ is-torsorial-dependent-universal-property-identity-system : - dependent-universal-property-identity-system {B = B} b → + dependent-universal-property-identity-system B b → is-torsorial B pr1 (is-torsorial-dependent-universal-property-identity-system H) = (a , b) pr2 (is-torsorial-dependent-universal-property-identity-system H) u = @@ -95,13 +95,13 @@ module _ dependent-universal-property-identity-system-is-identity-system : is-identity-system B a b → - dependent-universal-property-identity-system {B = B} b + dependent-universal-property-identity-system B b dependent-universal-property-identity-system-is-identity-system H = dependent-universal-property-identity-system-is-torsorial b ( is-torsorial-is-identity-system a b H) is-identity-system-dependent-universal-property-identity-system : - dependent-universal-property-identity-system {B = B} b → + dependent-universal-property-identity-system B b → is-identity-system B a b is-identity-system-dependent-universal-property-identity-system H P = section-is-equiv (H P) diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md index af544782f6..74679cffd1 100644 --- a/src/foundation/universal-property-identity-types.lagda.md +++ b/src/foundation/universal-property-identity-types.lagda.md @@ -129,7 +129,7 @@ module _ ( equiv-ev-refl x) ∘e ( equiv-inclusion-is-full-subtype ( Π-Prop A ∘ (is-equiv-Prop ∘_)) - ( fundamental-theorem-id (is-torsorial-path a))) ∘e + ( fundamental-theorem-id (is-torsorial-Id a))) ∘e ( distributive-Π-Σ)))) ( emb-tot ( λ x → @@ -145,7 +145,7 @@ module _ ( λ _ → is-injective-emb ( emb-fiber-Id-preunivalent-Id a) - ( eq-is-contr (is-torsorial-path a)))) + ( eq-is-contr (is-torsorial-Id a)))) ( λ _ → ap Id) module _ diff --git a/src/foundation/universal-property-truncation.lagda.md b/src/foundation/universal-property-truncation.lagda.md index 2df1545015..80dec71320 100644 --- a/src/foundation/universal-property-truncation.lagda.md +++ b/src/foundation/universal-property-truncation.lagda.md @@ -68,7 +68,7 @@ module _ ( K x' x) ( Id-Truncated-Type C (g x') z)))) ∘e ( equiv-ev-pair))) - ( is-torsorial-path (g x))) + ( is-torsorial-Id (g x))) is-truncation-is-truncation-ap : is-truncation B f diff --git a/src/foundation/weak-function-extensionality.lagda.md b/src/foundation/weak-function-extensionality.lagda.md index cfd66c65ae..c445141e12 100644 --- a/src/foundation/weak-function-extensionality.lagda.md +++ b/src/foundation/weak-function-extensionality.lagda.md @@ -101,7 +101,7 @@ abstract ( λ t → eq-pair-Σ refl refl)) ( weak-funext A ( λ x → Σ (B x) (λ b → f x ＝ b)) - ( λ x → is-torsorial-path (f x)))) + ( λ x → is-torsorial-Id (f x)))) ( λ g → htpy-eq {g = g}) ``` diff --git a/src/graph-theory/equivalences-directed-graphs.lagda.md b/src/graph-theory/equivalences-directed-graphs.lagda.md index 726b7fb471..ec10cf5c03 100644 --- a/src/graph-theory/equivalences-directed-graphs.lagda.md +++ b/src/graph-theory/equivalences-directed-graphs.lagda.md @@ -335,7 +335,7 @@ module _ is-contr-equiv' ( Σ (Directed-Graph l1 l2) (λ H → G ＝ H)) ( equiv-tot extensionality-Directed-Graph) - ( is-torsorial-path G) + ( is-torsorial-Id G) ``` ### The inverse of an equivalence of directed trees diff --git a/src/graph-theory/fibers-directed-graphs.lagda.md b/src/graph-theory/fibers-directed-graphs.lagda.md index cf20c1a1bf..7f0d16753a 100644 --- a/src/graph-theory/fibers-directed-graphs.lagda.md +++ b/src/graph-theory/fibers-directed-graphs.lagda.md @@ -200,7 +200,7 @@ module _ direct-predecessor-Directed-Graph G ( node-inclusion-fiber-Directed-Graph G x y) compute-direct-predecessor-fiber-Directed-Graph y = - ( right-unit-law-Σ-is-contr (λ (u , e) → is-torsorial-path' _)) ∘e + ( right-unit-law-Σ-is-contr (λ (u , e) → is-torsorial-Id' _)) ∘e ( interchange-Σ-Σ _) map-compute-direct-predecessor-fiber-Directed-Graph : diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md index cd6f407532..822b9d4c23 100644 --- a/src/graph-theory/walks-directed-graphs.lagda.md +++ b/src/graph-theory/walks-directed-graphs.lagda.md @@ -407,7 +407,7 @@ module _ is-contr-equiv' ( Σ (vertex-Directed-Graph G) (λ y → y ＝ x)) ( equiv-tot (λ y → compute-raise l2 (y ＝ x))) - ( is-torsorial-path' x) + ( is-torsorial-Id' x) ``` ### `cons-walk e w ≠ refl-walk` diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md index 0377bd1cc9..52490662e6 100644 --- a/src/graph-theory/walks-undirected-graphs.lagda.md +++ b/src/graph-theory/walks-undirected-graphs.lagda.md @@ -169,7 +169,7 @@ module _ is-contr ( vertex-on-walk-Undirected-Graph G (refl-walk-Undirected-Graph {x = x})) is-contr-vertex-on-walk-refl-walk-Undirected-Graph = - is-torsorial-path x + is-torsorial-Id x ``` ### The type of vertices on a walk is equivalent to `Fin (n + 1)` where `n` is the length of the walk @@ -192,7 +192,7 @@ module _ ( equiv-coprod ( compute-vertex-on-walk-Undirected-Graph w) ( equiv-is-contr - ( is-torsorial-path (other-element-unordered-pair p y)) + ( is-torsorial-Id (other-element-unordered-pair p y)) ( is-contr-unit))) ∘e ( left-distributive-Σ-coprod ( vertex-Undirected-Graph G) @@ -231,7 +231,7 @@ module _ ( equiv-coprod ( compute-edge-on-walk-Undirected-Graph w) ( equiv-is-contr - ( is-torsorial-path (pair p e)) + ( is-torsorial-Id (pair p e)) ( is-contr-unit))) ∘e ( left-distributive-Σ-coprod ( total-edge-Undirected-Graph G) diff --git a/src/group-theory/automorphism-groups.lagda.md b/src/group-theory/automorphism-groups.lagda.md index 66a609eded..aa5a4f79ff 100644 --- a/src/group-theory/automorphism-groups.lagda.md +++ b/src/group-theory/automorphism-groups.lagda.md @@ -120,7 +120,7 @@ module _ is-torsorial (Eq-classifying-type-Automorphism-∞-Group X) is-torsorial-Eq-classifying-type-Automorphism-∞-Group X = is-torsorial-Eq-subtype - ( is-torsorial-path (pr1 X)) + ( is-torsorial-Id (pr1 X)) ( λ a → is-prop-type-trunc-Prop) ( pr1 X) ( refl) diff --git a/src/group-theory/equivalences-concrete-group-actions.lagda.md b/src/group-theory/equivalences-concrete-group-actions.lagda.md index a631706793..27c37431a5 100644 --- a/src/group-theory/equivalences-concrete-group-actions.lagda.md +++ b/src/group-theory/equivalences-concrete-group-actions.lagda.md @@ -41,7 +41,7 @@ module _ equiv-action-Concrete-Group : {l3 : Level} (Y : action-Concrete-Group l3 G) → UU (l1 ⊔ l2 ⊔ l3) equiv-action-Concrete-Group Y = - (u : classifying-type-Concrete-Group G) → type-equiv-Set (X u) (Y u) + (u : classifying-type-Concrete-Group G) → equiv-Set (X u) (Y u) id-equiv-action-Concrete-Group : equiv-action-Concrete-Group X id-equiv-action-Concrete-Group u = id-equiv @@ -50,7 +50,7 @@ module _ (Y : action-Concrete-Group l2 G) → (X ＝ Y) ≃ equiv-action-Concrete-Group Y extensionality-action-Concrete-Group = extensionality-Π X - ( λ u → type-equiv-Set (X u)) + ( λ u → equiv-Set (X u)) ( λ u → extensionality-Set (X u)) equiv-eq-action-Concrete-Group : diff --git a/src/group-theory/isomorphisms-abelian-groups.lagda.md b/src/group-theory/isomorphisms-abelian-groups.lagda.md index 7d636cd570..9d7b07d36e 100644 --- a/src/group-theory/isomorphisms-abelian-groups.lagda.md +++ b/src/group-theory/isomorphisms-abelian-groups.lagda.md @@ -196,7 +196,7 @@ abstract is-contr-equiv' ( Σ (Ab l) (Id A)) ( equiv-tot (equiv-iso-eq-Ab' A)) - ( is-torsorial-path A) + ( is-torsorial-Id A) is-equiv-iso-eq-Ab : {l : Level} (A B : Ab l) → is-equiv (iso-eq-Ab A B) diff --git a/src/group-theory/isomorphisms-groups.lagda.md b/src/group-theory/isomorphisms-groups.lagda.md index a176295cd3..0ab46ae767 100644 --- a/src/group-theory/isomorphisms-groups.lagda.md +++ b/src/group-theory/isomorphisms-groups.lagda.md @@ -242,7 +242,7 @@ module _ is-contr-equiv' ( Σ (Group l) (Id G)) ( equiv-tot extensionality-Group') - ( is-torsorial-path G) + ( is-torsorial-Id G) ``` ### Group isomorphisms are stable by composition diff --git a/src/group-theory/orbits-monoid-actions.lagda.md b/src/group-theory/orbits-monoid-actions.lagda.md index 3238837f89..a6766ac596 100644 --- a/src/group-theory/orbits-monoid-actions.lagda.md +++ b/src/group-theory/orbits-monoid-actions.lagda.md @@ -81,7 +81,7 @@ module _ is-torsorial (htpy-hom-orbit-action-Monoid f) is-torsorial-htpy-hom-orbit-action-Monoid {x} {y} f = is-torsorial-Eq-subtype - ( is-torsorial-path (element-hom-orbit-action-Monoid f)) + ( is-torsorial-Id (element-hom-orbit-action-Monoid f)) ( λ u → is-set-type-action-Monoid M X (mul-action-Monoid M X u x) y) ( element-hom-orbit-action-Monoid f) diff --git a/src/group-theory/symmetric-concrete-groups.lagda.md b/src/group-theory/symmetric-concrete-groups.lagda.md index b329c223a9..006ef44e03 100644 --- a/src/group-theory/symmetric-concrete-groups.lagda.md +++ b/src/group-theory/symmetric-concrete-groups.lagda.md @@ -57,7 +57,7 @@ module _ equiv-classifying-type-symmetric-Concrete-Group : (X Y : classifying-type-symmetric-Concrete-Group A) → UU l equiv-classifying-type-symmetric-Concrete-Group X Y = - type-equiv-Set (pr1 X) (pr1 Y) + equiv-Set (pr1 X) (pr1 Y) type-symmetric-Concrete-Group : UU l type-symmetric-Concrete-Group = diff --git a/src/lists/lists.lagda.md b/src/lists/lists.lagda.md index 82634d6451..70c2f61bc6 100644 --- a/src/lists/lists.lagda.md +++ b/src/lists/lists.lagda.md @@ -220,7 +220,7 @@ is-torsorial-Eq-list {A = A} l = is-contr-equiv' ( Σ (list A) (Id l)) ( equiv-tot (equiv-Eq-list l)) - ( is-torsorial-path l) + ( is-torsorial-Id l) is-trunc-Eq-list : (k : 𝕋) {l : Level} {A : UU l} → is-trunc (succ-𝕋 (succ-𝕋 k)) A → diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md index 7c79d77436..bdbd345410 100644 --- a/src/orthogonal-factorization-systems/closed-modalities.lagda.md +++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md @@ -90,7 +90,7 @@ module _ ( f' a) ( center (is-modal-B q))))) ∘e ( equiv-up-join B))) - ( is-torsorial-path' f)) + ( is-torsorial-Id' f)) reflective-subuniverse-closed-modality : reflective-subuniverse (l ⊔ lQ) (l ⊔ lQ) diff --git a/src/ring-theory/isomorphisms-rings.lagda.md b/src/ring-theory/isomorphisms-rings.lagda.md index b8575bd7c4..3b76b3ef97 100644 --- a/src/ring-theory/isomorphisms-rings.lagda.md +++ b/src/ring-theory/isomorphisms-rings.lagda.md @@ -491,7 +491,7 @@ module _ ( (mul-Ring R , associative-mul-Ring R) , λ {x} {y} → refl) ( is-torsorial-Eq-subtype ( is-torsorial-Eq-subtype - ( is-torsorial-path (one-Ring R)) + ( is-torsorial-Id (one-Ring R)) ( λ x → is-prop-prod ( is-prop-Π (λ y → is-set-type-Ring R (mul-Ring R x y) y)) diff --git a/src/structured-types/pointed-equivalences.lagda.md b/src/structured-types/pointed-equivalences.lagda.md index 0c24aaae98..80c212d416 100644 --- a/src/structured-types/pointed-equivalences.lagda.md +++ b/src/structured-types/pointed-equivalences.lagda.md @@ -165,7 +165,7 @@ module _ is-torsorial-Eq-structure ( is-torsorial-equiv (type-Pointed-Type A)) ( pair (type-Pointed-Type A) id-equiv) - ( is-torsorial-path (point-Pointed-Type A)) + ( is-torsorial-Id (point-Pointed-Type A)) extensionality-Pointed-Type : (B : Pointed-Type l1) → Id A B ≃ (A ≃∗ B) extensionality-Pointed-Type = diff --git a/src/structured-types/pointed-types-equipped-with-automorphisms.lagda.md b/src/structured-types/pointed-types-equipped-with-automorphisms.lagda.md index c4e36e99ce..83f24fc993 100644 --- a/src/structured-types/pointed-types-equipped-with-automorphisms.lagda.md +++ b/src/structured-types/pointed-types-equipped-with-automorphisms.lagda.md @@ -159,7 +159,7 @@ is-torsorial-htpy-hom-Pointed-Type-With-Aut X Y h1 = ( is-torsorial-htpy (map-hom-Pointed-Type-With-Aut X Y h1)) ( pair (map-hom-Pointed-Type-With-Aut X Y h1) refl-htpy) ( is-torsorial-Eq-structure - ( is-torsorial-path + ( is-torsorial-Id ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h1)) ( pair (preserves-point-map-hom-Pointed-Type-With-Aut X Y h1) refl) ( is-contr-equiv' diff --git a/src/structured-types/pointed-universal-property-contractible-types.lagda.md b/src/structured-types/pointed-universal-property-contractible-types.lagda.md index 3c595d66c6..93bb61ec11 100644 --- a/src/structured-types/pointed-universal-property-contractible-types.lagda.md +++ b/src/structured-types/pointed-universal-property-contractible-types.lagda.md @@ -73,7 +73,7 @@ module _ is-contr-equiv ( Σ X (λ y → y ＝ x)) ( equiv-Σ-equiv-base _ (equiv-universal-property-contr a c X)) - ( is-torsorial-path' x) + ( is-torsorial-Id' x) module _ {l1 : Level} {A : UU l1} @@ -101,7 +101,7 @@ module _ ( equivalence-reasoning (A → X) ≃ Σ (A → X) (λ f → Σ X (λ x → f a ＝ x)) - by inv-right-unit-law-Σ-is-contr (λ f → is-torsorial-path (f a)) + by inv-right-unit-law-Σ-is-contr (λ f → is-torsorial-Id (f a)) ≃ Σ X (λ x → (A , a) →∗ (X , x)) by equiv-left-swap-Σ ≃ X @@ -110,7 +110,7 @@ module _ ap ( pr1) ( inv - ( contraction (is-torsorial-path (f a)) (pair (f a) refl))))) + ( contraction (is-torsorial-Id (f a)) (pair (f a) refl))))) module _ {l1 : Level} (A : Pointed-Type l1) diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md index 2d2b34123b..b09342fe44 100644 --- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md @@ -376,7 +376,7 @@ module _ equiv-left-swap-Σ ≃ (C → X) by - equiv-pr1 (λ v → is-torsorial-path' (v ∘ horizontal-map-cocone f g c)) + equiv-pr1 (λ v → is-torsorial-Id' (v ∘ horizontal-map-cocone f g c)) is-acyclic-map-vertical-map-cocone-is-pushout : is-pushout f g c → diff --git a/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md b/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md index ba96029837..40f331bb0d 100644 --- a/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md +++ b/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md @@ -104,15 +104,15 @@ module _ ( unit) ( inv-equiv ( terminal-map (fiber id b) , - ( is-equiv-terminal-map-is-contr (is-torsorial-path' b)))) + ( is-equiv-terminal-map-is-contr (is-torsorial-Id' b)))) ( inv-equiv ( terminal-map (fiber id b) , - ( is-equiv-terminal-map-is-contr (is-torsorial-path' b)))) + ( is-equiv-terminal-map-is-contr (is-torsorial-Id' b)))) ( id-equiv) ( terminal-map (fiber f b)) ( terminal-map (fiber f b)) - ( λ _ → eq-is-contr (is-torsorial-path' b)) - ( λ _ → eq-is-contr (is-torsorial-path' b)) + ( λ _ → eq-is-contr (is-torsorial-Id' b)) + ( λ _ → eq-is-contr (is-torsorial-Id' b)) suspension-cocone-fiber : suspension-cocone (fiber f b) (fiber (codiagonal-map f) b) diff --git a/src/synthetic-homotopy-theory/free-loops.lagda.md b/src/synthetic-homotopy-theory/free-loops.lagda.md index 179b0d76fa..9abf11b695 100644 --- a/src/synthetic-homotopy-theory/free-loops.lagda.md +++ b/src/synthetic-homotopy-theory/free-loops.lagda.md @@ -95,14 +95,14 @@ module _ (α : free-loop X) → is-torsorial (Eq-free-loop α) is-torsorial-Eq-free-loop (pair x α) = is-torsorial-Eq-structure - ( is-torsorial-path x) + ( is-torsorial-Id x) ( pair x refl) ( is-contr-is-equiv' ( Σ (Id x x) (λ α' → Id α α')) ( tot (λ α' α → right-unit ∙ α)) ( is-equiv-tot-is-fiberwise-equiv ( λ α' → is-equiv-concat right-unit α')) - ( is-torsorial-path α)) + ( is-torsorial-Id α)) abstract is-equiv-Eq-eq-free-loop : @@ -142,14 +142,14 @@ module _ ( p : free-dependent-loop α P) → is-torsorial (Eq-free-dependent-loop p) is-torsorial-Eq-free-dependent-loop (pair y p) = is-torsorial-Eq-structure - ( is-torsorial-path y) + ( is-torsorial-Id y) ( pair y refl) ( is-contr-is-equiv' ( Σ (Id (tr P (loop-free-loop α) y) y) (λ p' → Id p p')) ( tot (λ p' α → right-unit ∙ α)) ( is-equiv-tot-is-fiberwise-equiv ( λ p' → is-equiv-concat right-unit p')) - ( is-torsorial-path p)) + ( is-torsorial-Id p)) abstract is-equiv-Eq-free-dependent-loop-eq : diff --git a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md index 7c4a10756d..4f8238af04 100644 --- a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md +++ b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md @@ -153,15 +153,15 @@ module _ is-torsorial Eq-structure-Hatcher-Acyclic-Type is-torsorial-Eq-structure-Hatcher-Acyclic-Type = is-torsorial-Eq-structure - ( is-torsorial-path (pr1 s)) + ( is-torsorial-Id (pr1 s)) ( pr1 s , refl) ( is-torsorial-Eq-structure - ( is-torsorial-path (pr1 (pr2 s))) + ( is-torsorial-Id (pr1 (pr2 s))) ( pr1 (pr2 s) , refl) ( is-torsorial-Eq-structure - ( is-torsorial-path (pr1 (pr2 (pr2 s)) ∙ refl)) + ( is-torsorial-Id (pr1 (pr2 (pr2 s)) ∙ refl)) ( pr1 (pr2 (pr2 s)) , right-unit) - ( is-torsorial-path (pr2 (pr2 (pr2 s)) ∙ refl)))) + ( is-torsorial-Id (pr2 (pr2 (pr2 s)) ∙ refl)))) Eq-eq-structure-Hatcher-Acyclic-Type : (t : structure-Hatcher-Acyclic-Type A) → @@ -216,7 +216,7 @@ module _ ( ( inv (power-nat-mul-Ω 3 2 (Ω A) a)) ∙ ( power-nat-succ-Ω' 5 (Ω A) a)))) ∘e ( ( ( left-unit-law-Σ-is-contr - ( is-torsorial-path' (a ∙ a)) + ( is-torsorial-Id' (a ∙ a)) ( a ∙ a , refl)) ∘e ( inv-associative-Σ ( type-Ω (Ω A)) @@ -239,7 +239,7 @@ module _ ( equiv-concat' ( power-nat-Ω 3 (Ω A) b) ( interchange-concat-Ω² a b a b))))))))) - ( is-torsorial-path refl) + ( is-torsorial-Id refl) ``` ### For a fixed pointed map, the `is-hom-pointed-map-algebra-Hatcher-Acyclic-Type` family is torsorial @@ -309,13 +309,13 @@ module _ is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' (A , σ) (B , τ) f) is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' = is-torsorial-Eq-structure - ( is-torsorial-path (map-Ω f a1)) ((map-Ω f a1) , refl) + ( is-torsorial-Id (map-Ω f a1)) ((map-Ω f a1) , refl) ( is-torsorial-Eq-structure - ( is-torsorial-path (map-Ω f a2)) ((map-Ω f a2) , refl) + ( is-torsorial-Id (map-Ω f a2)) ((map-Ω f a2) , refl) ( is-torsorial-Eq-structure - ( is-torsorial-path _) + ( is-torsorial-Id _) ( _ , refl) - ( is-torsorial-path _))) + ( is-torsorial-Id _))) abstract is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type : diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md index 6a3e59877e..90522d9f5d 100644 --- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md +++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md @@ -268,7 +268,7 @@ module _ ( Σ (suspension-structure X Z) (λ c' → c ＝ c')) ( inv-equiv ( equiv-tot (extensionality-suspension-structure c))) - ( is-torsorial-path c)) + ( is-torsorial-Id c)) ( P)) ``` diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md index ac4e4cb5b7..77461197bb 100644 --- a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md +++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md @@ -607,7 +607,7 @@ module _ equiv-left-swap-Σ ≃ (C → type-Truncated-Type X) by - equiv-pr1 (λ v → is-torsorial-path' (v ∘ horizontal-map-cocone f g c)) + equiv-pr1 (λ v → is-torsorial-Id' (v ∘ horizontal-map-cocone f g c)) is-truncated-acyclic-map-vertical-map-cocone-is-pushout : is-pushout f g c → diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md index a638e4ea4b..1ed990b712 100644 --- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md @@ -143,7 +143,7 @@ module _ (suspension-Pointed-Type X →∗ Y) ≃ (X →∗ Ω Y) equiv-transpose-suspension-loop-adjunction = ( left-unit-law-Σ-is-contr - ( is-torsorial-path (point-Pointed-Type Y)) + ( is-torsorial-Id (point-Pointed-Type Y)) ( point-Pointed-Type Y , refl)) ∘e ( inv-associative-Σ ( type-Pointed-Type Y) @@ -159,9 +159,9 @@ module _ Σ ( point-Pointed-Type Y ＝ pr1 z) ( λ x → pr2 z (point-Pointed-Type X) ＝ x))) ∘e ( inv-right-unit-law-Σ-is-contr - ( λ z → is-torsorial-path (pr2 z (point-Pointed-Type X)))) ∘e + ( λ z → is-torsorial-Id (pr2 z (point-Pointed-Type X)))) ∘e ( left-unit-law-Σ-is-contr - ( is-torsorial-path' (point-Pointed-Type Y)) + ( is-torsorial-Id' (point-Pointed-Type Y)) ( point-Pointed-Type Y , refl)) ∘e ( equiv-right-swap-Σ) ∘e ( equiv-Σ-equiv-base diff --git a/src/trees/equivalences-directed-trees.lagda.md b/src/trees/equivalences-directed-trees.lagda.md index 3d53b85582..4b3dbd9ecb 100644 --- a/src/trees/equivalences-directed-trees.lagda.md +++ b/src/trees/equivalences-directed-trees.lagda.md @@ -443,7 +443,7 @@ module _ is-contr-equiv' ( Σ (Directed-Tree l1 l2) (λ S → T ＝ S)) ( equiv-tot extensionality-Directed-Tree) - ( is-torsorial-path T) + ( is-torsorial-Id T) ``` ### A morphism of directed trees is an equivalence if it is an equivalence on the nodes diff --git a/src/trees/equivalences-enriched-directed-trees.lagda.md b/src/trees/equivalences-enriched-directed-trees.lagda.md index 435594dd57..b4ee4e1da9 100644 --- a/src/trees/equivalences-enriched-directed-trees.lagda.md +++ b/src/trees/equivalences-enriched-directed-trees.lagda.md @@ -506,7 +506,7 @@ module _ is-contr-equiv' ( Σ (Enriched-Directed-Tree l3 l4 A B) (λ S → T ＝ S)) ( equiv-tot extensionality-Enriched-Directed-Tree) - ( is-torsorial-path T) + ( is-torsorial-Id T) ``` ### A morphism of enriched directed trees is an equivalence if it is an equivalence on the nodes diff --git a/src/trees/fibers-enriched-directed-trees.lagda.md b/src/trees/fibers-enriched-directed-trees.lagda.md index c4b4fcaa4a..f546f1acf3 100644 --- a/src/trees/fibers-enriched-directed-trees.lagda.md +++ b/src/trees/fibers-enriched-directed-trees.lagda.md @@ -99,7 +99,7 @@ module _ ( interchange-Σ-Σ (λ u e v → v ＝ cons-walk-Directed-Graph e w)) ∘e ( ( inv-right-unit-law-Σ-is-contr ( λ i → - is-torsorial-path' (cons-walk-Directed-Graph (pr2 i) w))) ∘e + is-torsorial-Id' (cons-walk-Directed-Graph (pr2 i) w))) ∘e ( enrichment-Enriched-Directed-Tree A B T y)) fiber-Enriched-Directed-Tree : Enriched-Directed-Tree (l3 ⊔ l4) (l3 ⊔ l4) A B @@ -157,7 +157,7 @@ module _ map-enrichment-fiber-Enriched-Directed-Tree y b eq-map-enrichment-fiber-Enriched-Directed-Tree y b w p = eq-interchange-Σ-Σ-is-contr _ - ( is-torsorial-path' + ( is-torsorial-Id' ( cons-walk-Directed-Graph ( edge-enrichment-Enriched-Directed-Tree A B T ( node-inclusion-fiber-Enriched-Directed-Tree y) diff --git a/src/trees/polynomial-endofunctors.lagda.md b/src/trees/polynomial-endofunctors.lagda.md index 6962ec19ac..398d54325a 100644 --- a/src/trees/polynomial-endofunctors.lagda.md +++ b/src/trees/polynomial-endofunctors.lagda.md @@ -71,7 +71,7 @@ module _ is-torsorial (Eq-type-polynomial-endofunctor x) is-torsorial-Eq-type-polynomial-endofunctor (pair x α) = is-torsorial-Eq-structure - ( is-torsorial-path x) + ( is-torsorial-Id x) ( pair x refl) ( is-torsorial-htpy α) diff --git a/src/trees/rooted-morphisms-directed-trees.lagda.md b/src/trees/rooted-morphisms-directed-trees.lagda.md index fb82443c30..81c9d5fc01 100644 --- a/src/trees/rooted-morphisms-directed-trees.lagda.md +++ b/src/trees/rooted-morphisms-directed-trees.lagda.md @@ -256,5 +256,5 @@ module _ is-contr-equiv' ( Σ (rooted-hom-Directed-Tree S T) (λ g → f ＝ g)) ( equiv-tot extensionality-rooted-hom-Directed-Tree) - ( is-torsorial-path f) + ( is-torsorial-Id f) ``` diff --git a/src/univalent-combinatorics/2-element-subtypes.lagda.md b/src/univalent-combinatorics/2-element-subtypes.lagda.md index efafaa64f8..16f26a1213 100644 --- a/src/univalent-combinatorics/2-element-subtypes.lagda.md +++ b/src/univalent-combinatorics/2-element-subtypes.lagda.md @@ -129,10 +129,10 @@ module _ ( equiv-coprod ( equiv-is-contr ( is-contr-Fin-one-ℕ) - ( is-torsorial-path x)) + ( is-torsorial-Id x)) ( equiv-is-contr ( is-contr-unit) - ( is-torsorial-path y))) + ( is-torsorial-Id y))) has-two-elements-type-standard-2-Element-Subtype : has-two-elements type-standard-2-Element-Subtype diff --git a/src/univalent-combinatorics/2-element-types.lagda.md b/src/univalent-combinatorics/2-element-types.lagda.md index b15edfc919..01e0347945 100644 --- a/src/univalent-combinatorics/2-element-types.lagda.md +++ b/src/univalent-combinatorics/2-element-types.lagda.md @@ -410,7 +410,7 @@ is-identity-system-type-2-Element-Type X x = dependent-universal-property-identity-system-type-2-Element-Type : {l1 : Level} (X : 2-Element-Type l1) (x : type-2-Element-Type X) → dependent-universal-property-identity-system - { B = type-2-Element-Type {l1}} + ( type-2-Element-Type {l1}) { a = X} ( x) dependent-universal-property-identity-system-type-2-Element-Type X x = diff --git a/src/univalent-combinatorics/cartesian-product-types.lagda.md b/src/univalent-combinatorics/cartesian-product-types.lagda.md index 0ef51f58d3..fa9ee2a64b 100644 --- a/src/univalent-combinatorics/cartesian-product-types.lagda.md +++ b/src/univalent-combinatorics/cartesian-product-types.lagda.md @@ -85,7 +85,7 @@ equiv-left-factor : equiv-left-factor {l1} {l2} {X} {Y} y = ( ( right-unit-law-prod) ∘e ( equiv-tot - ( λ x → equiv-is-contr (is-torsorial-path' y) is-contr-unit))) ∘e + ( λ x → equiv-is-contr (is-torsorial-Id' y) is-contr-unit))) ∘e ( associative-Σ X (λ x → Y) (λ t → Id (pr2 t) y)) count-left-factor : diff --git a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md index 99211c837f..8e1578953e 100644 --- a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md +++ b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md @@ -149,7 +149,7 @@ count-fiber-map-section-family : count-fiber-map-section-family {l1} {l2} {A} {B} b e f (pair y z) = count-equiv' ( ( ( left-unit-law-Σ-is-contr - ( is-torsorial-path' y) + ( is-torsorial-Id' y) ( pair y refl)) ∘e ( inv-associative-Σ A ( λ x → Id x y) diff --git a/src/univalent-combinatorics/dependent-pair-types.lagda.md b/src/univalent-combinatorics/dependent-pair-types.lagda.md index 54170fb6ef..288b6e4881 100644 --- a/src/univalent-combinatorics/dependent-pair-types.lagda.md +++ b/src/univalent-combinatorics/dependent-pair-types.lagda.md @@ -106,7 +106,7 @@ abstract ( λ (x : A) → Id x (pr1 t)) ( λ s → Id (tr B (pr2 s) (b (pr1 s))) (pr2 t))) ∘e ( inv-left-unit-law-Σ-is-contr - ( is-torsorial-path' (pr1 t)) + ( is-torsorial-Id' (pr1 t)) ( pair (pr1 t) refl)))))) ( count-Σ e ( λ t → diff --git a/src/univalent-combinatorics/fibers-of-maps.lagda.md b/src/univalent-combinatorics/fibers-of-maps.lagda.md index 5e5eff6376..434a444727 100644 --- a/src/univalent-combinatorics/fibers-of-maps.lagda.md +++ b/src/univalent-combinatorics/fibers-of-maps.lagda.md @@ -113,7 +113,7 @@ abstract is-finite-fiber-map-section-family {l1} {l2} {A} {B} b f g (pair y z) = is-finite-equiv' ( ( ( left-unit-law-Σ-is-contr - ( is-torsorial-path' y) + ( is-torsorial-Id' y) ( pair y refl)) ∘e ( inv-associative-Σ A ( λ x → Id x y) diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md index 8fdc0f7f01..7ae5f6ef72 100644 --- a/src/univalent-combinatorics/finite-types.lagda.md +++ b/src/univalent-combinatorics/finite-types.lagda.md @@ -585,7 +585,7 @@ is-torsorial-equiv-𝔽 {l} X = is-contr-equiv' ( Σ (𝔽 l) (Id X)) ( equiv-tot (extensionality-𝔽 X)) - ( is-torsorial-path X) + ( is-torsorial-Id X) equiv-eq-𝔽 : {l : Level} → (X Y : 𝔽 l) → Id X Y → equiv-𝔽 X Y equiv-eq-𝔽 X Y = map-equiv (extensionality-𝔽 X Y) diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md index aec18df6b8..9103b85ba3 100644 --- a/src/univalent-combinatorics/standard-finite-types.lagda.md +++ b/src/univalent-combinatorics/standard-finite-types.lagda.md @@ -30,8 +30,13 @@ open import foundation.injective-maps open import foundation.negated-equality open import foundation.negation open import foundation.noncontractible-types +open import foundation.path-algebra +open import foundation.preunivalent-type-families open import foundation.raising-universe-levels +open import foundation.retractions +open import foundation.sections open import foundation.sets +open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels @@ -427,22 +432,55 @@ leq-nat-succ-Fin (succ-ℕ k) (inr star) = ( leq-zero-ℕ (succ-ℕ (nat-Fin (succ-ℕ k) (inr star)))) ``` -### Fin is injective +### `Fin` is injective ```agda -abstract - is-equivalence-injective-Fin : is-equivalence-injective Fin - is-equivalence-injective-Fin {zero-ℕ} {zero-ℕ} e = - refl - is-equivalence-injective-Fin {zero-ℕ} {succ-ℕ l} e = - ex-falso (map-inv-equiv e (zero-Fin l)) - is-equivalence-injective-Fin {succ-ℕ k} {zero-ℕ} e = - ex-falso (map-equiv e (zero-Fin k)) - is-equivalence-injective-Fin {succ-ℕ k} {succ-ℕ l} e = - ap succ-ℕ (is-equivalence-injective-Fin (equiv-equiv-Maybe e)) +is-equivalence-injective-Fin : is-equivalence-injective Fin +is-equivalence-injective-Fin {zero-ℕ} {zero-ℕ} e = + refl +is-equivalence-injective-Fin {zero-ℕ} {succ-ℕ l} e = + ex-falso (map-inv-equiv e (zero-Fin l)) +is-equivalence-injective-Fin {succ-ℕ k} {zero-ℕ} e = + ex-falso (map-equiv e (zero-Fin k)) +is-equivalence-injective-Fin {succ-ℕ k} {succ-ℕ l} e = + ap succ-ℕ (is-equivalence-injective-Fin (equiv-equiv-Maybe e)) abstract is-injective-Fin : is-injective Fin is-injective-Fin = is-injective-is-equivalence-injective is-equivalence-injective-Fin + +compute-is-equivalence-injective-Fin-id-equiv : + {n : ℕ} → is-equivalence-injective-Fin {n} {n} id-equiv ＝ refl +compute-is-equivalence-injective-Fin-id-equiv {zero-ℕ} = refl +compute-is-equivalence-injective-Fin-id-equiv {succ-ℕ n} = + ap² succ-ℕ + ( ( ap is-equivalence-injective-Fin compute-equiv-equiv-Maybe-id-equiv) ∙ + ( compute-is-equivalence-injective-Fin-id-equiv {n})) +``` + +### `Fin` is a preunivalent type family + +The proof does not rely on the (pre-)univalence axiom. + +```agda +is-section-on-diagonal-is-equivalence-injective-Fin : + {n : ℕ} → + equiv-tr Fin (is-equivalence-injective-Fin {n} {n} id-equiv) ＝ id-equiv +is-section-on-diagonal-is-equivalence-injective-Fin = + ap (equiv-tr Fin) compute-is-equivalence-injective-Fin-id-equiv + +is-retraction-is-equivalence-injective-Fin : + {n m : ℕ} → + is-retraction (equiv-tr Fin) (is-equivalence-injective-Fin {n} {m}) +is-retraction-is-equivalence-injective-Fin refl = + compute-is-equivalence-injective-Fin-id-equiv + +retraction-equiv-tr-Fin : (n m : ℕ) → retraction (equiv-tr Fin {n} {m}) +pr1 (retraction-equiv-tr-Fin n m) = is-equivalence-injective-Fin +pr2 (retraction-equiv-tr-Fin n m) = is-retraction-is-equivalence-injective-Fin + +is-preunivalent-Fin : is-preunivalent Fin +is-preunivalent-Fin = + is-preunivalent-retraction-equiv-tr-Set Fin-Set retraction-equiv-tr-Fin ```