diff --git a/.github/workflows/format.yml b/.github/workflows/format.yml index 8ae7b8f3..8850e099 100644 --- a/.github/workflows/format.yml +++ b/.github/workflows/format.yml @@ -1,30 +1,22 @@ -name: Code autoformatting +name: File formatting on: push: branches: - main + pull_request: + branches: + - main jobs: format: runs-on: ubuntu-latest - permissions: - contents: write steps: - name: Checkout code uses: actions/checkout@v3 - with: - # Make sure the actual branch is checked out when running on pull requests - ref: ${{ github.head_ref }} - # This is important to fetch the changes to the previous commit - fetch-depth: 0 - - name: Run Prettier + - name: Prettier uses: creyD/prettier_action@v4.3 with: - prettier_options: --write **/*.{md,json,yaml,yml} - commit_options: --allow-empty - # Update the current commit instead of creating a new one. Only works if checkout fetch depth is set to `0` - same_commit: true - # Prettify changed files. Only works if checkout fetch depth is set to `0` - only_changed: true + dry: true + prettier_options: --check **/*.{md,json,yaml,yml} diff --git a/.vscode/extensions.json b/.vscode/extensions.json index e62e4397..771db0e3 100644 --- a/.vscode/extensions.json +++ b/.vscode/extensions.json @@ -1,6 +1,6 @@ { - "recommendations": [ - "nikolaikudasovfizruk.rzk-1-experimental-highlighting", - "esbenp.prettier-vscode" - ] + "recommendations": [ + "nikolaikudasovfizruk.rzk-1-experimental-highlighting", + "esbenp.prettier-vscode" + ] } diff --git a/README.md b/README.md index 6352fe2d..dca683fc 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ results from the following papers: - "[Limits and colimits of synthetic ∞-categories](https://arxiv.org/abs/2202.12386)" [3] -This formalization project follows the philosophy layed out in the article +This formalization project follows the philosophy laid out in the article "[Could ∞-category theory be taught to undergraduates?](https://www.ams.org/journals/notices/202305/noti2692/noti2692.html)" [4]. diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md index a1f238ef..52291225 100644 --- a/src/hott/03-equivalences.rzk.md +++ b/src/hott/03-equivalences.rzk.md @@ -24,18 +24,6 @@ This is a literate `rzk` file: := Σ (r : B → A) , (homotopy A A (comp A B A r f) (identity A)) ``` -```rzk -#def ind-has-section - ( f : A → B) - ( ( sec-f , ε-f) : has-section f) - ( C : B → U) - ( s : ( a : A) → C ( f a)) - ( b : B) - : C b - := - transport B C ( f (sec-f b)) b ( ε-f b) ( s (sec-f b)) -``` - We define equivalences to be bi-invertible maps. ```rzk @@ -70,9 +58,17 @@ We define equivalences to be bi-invertible maps. : B → A := first (second is-equiv-f) +#def has-section-is-equiv + : has-section A B f + := second is-equiv-f + #def retraction-is-equiv uses (f) : B → A := first (first is-equiv-f) + +#def has-retraction-is-equiv + : has-retraction A B f + := first is-equiv-f ``` ```rzk title="The homotopy between the section and retraction of an equivalence" @@ -214,7 +210,7 @@ The inverse of an invertible map has an inverse. first ( second has-inverse-f))) ``` -## Composing equivalences +## The type of equivalences The type of equivalences between types uses `#!rzk is-equiv` rather than `#!rzk has-inverse`. @@ -226,6 +222,32 @@ The type of equivalences between types uses `#!rzk is-equiv` rather than := Σ (f : A → B) , (is-equiv A B f) ``` +## Induction with section + +```rzk +#def ind-has-section + ( A B : U) + ( f : A → B) + ( ( sec-f , ε-f) : has-section A B f) + ( C : B → U) + ( s : (a : A) → C (f a)) + ( b : B) + : C b + := transport B C (f (sec-f b)) b (ε-f b) (s (sec-f b)) +``` + +It is convenient to have available the special case where `f` is an equivalence. + +```rzk +#def ind-has-section-equiv + ( A B : U) + ( (f, is-equiv-f) : Equiv A B) + : ( C : B → U) → ((a : A) → C (f a)) → (b : B) → C b + := ind-has-section A B f (second is-equiv-f) +``` + +## Composing equivalences + The data of an equivalence is not symmetric so we promote an equivalence to an invertible map to prove symmetry: @@ -382,14 +404,12 @@ retraction the first map is an equivalence, and dually. ( ( (retr-gf, η-gf), (sec-gf, ε-gf)) : is-equiv A C (comp A B C g f)) : is-equiv A B f := - ( ( comp B C A retr-gf g, η-gf) , - ( comp B C A sec-gf g , - \ b → + ( ( comp B C A retr-gf g, η-gf) + , ( comp B C A sec-gf g + , \ b → ap-cancel-has-retraction B C g has-retraction-g (f (sec-gf (g b))) b - ( ε-gf (g b)) - ) - ) + ( ε-gf (g b)))) ``` ```rzk title="Left cancellation of equivalence property in diagrammatic order" @@ -401,13 +421,11 @@ retraction the first map is an equivalence, and dually. ( ( ( retr-gf, η-gf), (sec-gf, ε-gf)) : is-equiv A C (comp A B C g f)) : is-equiv B C g := - ( ( comp C A B f retr-gf , - ind-has-section A B f has-section-f + ( ( comp C A B f retr-gf + , ind-has-section A B f has-section-f ( \ b → f (retr-gf (g b)) = b) - ( \ a → ap A B (retr-gf (g ( f a))) a f (η-gf a)) - ) , - ( comp C A B f sec-gf, ε-gf) - ) + ( \ a → ap A B (retr-gf (g (f a))) a f (η-gf a))) + , ( comp C A B f sec-gf, ε-gf)) ``` We typically apply the cancelation property in a setting where the composite and @@ -474,16 +492,16 @@ If a map is homotopic to an equivalence it is an equivalence. ( is-equiv-g : is-equiv A B g) : is-equiv A B f := - ( ( ( first (first is-equiv-g)) , - ( \ a → + ( ( ( first (first is-equiv-g)) + , ( \ a → concat A ( first (first is-equiv-g) (f a)) ( first (first is-equiv-g) (g a)) ( a) ( ap B A (f a) (g a) (first (first is-equiv-g)) (H a)) - ( second (first is-equiv-g) a))) , - ( ( first (second is-equiv-g)) , - ( \ b → + ( second (first is-equiv-g) a))) + , ( ( first (second is-equiv-g)) + , ( \ b → concat B ( f (first (second is-equiv-g) b)) ( g (first (second is-equiv-g) b)) @@ -533,6 +551,181 @@ The retraction associated with an equivalence is an equivalence. ( is-equiv-section-is-equiv A B f is-equiv-f) ``` +## Section-retraction pairs + +A pair of maps `s : A → B` and `r : B → A'` is a **section-retraction pair** if +the composite `A → A'` is an equivalence. + +```rzk +#def is-section-retraction-pair + ( A B A' : U) + ( s : A → B) + ( r : B → A') + : U + := is-equiv A A' (comp A B A' r s) +``` + +When we have such a section-retraction pair `(s, r)`, we say that `r` is an +**external retraction** of `s` and `s` is an **external section** of `r`. + +```rzk +#def has-external-retraction + ( A B : U) + ( s : A → B) + : U + := + Σ ((A', r) : ( Σ (A' : U) , B → A')) + , ( is-section-retraction-pair A B A' s r) + +#def has-external-section + ( B A' : U) + ( r : B → A') + : U + := + Σ ((A, s) : ( Σ (A : U) , A → B)) + , ( is-section-retraction-pair A B A' s r) +``` + +Note that exactly like `has-section` and `has-retraction` these are not +_properties_ of `s` or `r`, but structure. + +Without univalence, we cannot yet show that the types `has-external-retraction` +and `has-retraction` (and their section counterparts, respectively) are +equivalent, so we content ourselves in showing that there is a logical +biimplication between them. + +```rzk +#def has-retraction-externalize + ( A B : U) + ( s : A → B) + ( (r , η) : has-retraction A B s) + : has-external-retraction A B s + := + ( ( A , r) + , is-equiv-homotopy A A (\ a → r (s (a))) (identity A) + ( η) ( is-equiv-identity A)) + +#def has-section-externalize + ( B A' : U) + ( r : B → A') + ( (s , ε) : has-section B A' r) + : has-external-section B A' r + := + ( ( A' , s) + , is-equiv-homotopy A' A' (\ a' → r (s (a'))) (identity A') + ( ε) ( is-equiv-identity A')) + +#def has-retraction-internalize + ( A B : U) + ( s : A → B) + ( ((A' , r) , ( (rec-rs , η-rs) , _)) + : has-external-retraction A B s) + : has-retraction A B s + := ( comp B A' A rec-rs r , η-rs) + +#def has-section-internalize + ( B A' : U) + ( r : B → A') + ( ((A , s) , (_ , (sec-rs , ε-rs))) + : has-external-section B A' r) + : has-section B A' r + := ( comp A' A B s sec-rs , ε-rs) +``` + +A consequence of the above is that in a section-retraction pair `(s, r)`, the +map `s` is a section and the map `r` is a retraction. Note that not every +composable pair `(s, r)` of such maps is a section-retraction pair; they have to +(up to composition with an equivalence) be section and retraction _of each +other_. + +In a section-retraction pair, if one of `s : A → B` and `r : B → A'` is an +equivalence, then so is the other. + +This is just a rephrasing of `is-equiv-left-factor` and `is-equiv-right-factor`. + +```rzk +#section is-equiv-is-section-retraction-pair + +#variables A B A' : U +#variable s : A → B +#variable r : B → A' + +#variable is-sec-rec-pair : is-section-retraction-pair A B A' s r + +#def is-equiv-section-is-equiv-retraction-is-section-retraction-pair + ( is-equiv-r : is-equiv B A' r) + : is-equiv A B s + := + is-equiv-right-factor A B A' s r + ( is-equiv-r) ( is-sec-rec-pair) + +#def is-equiv-retraction-is-equiv-section-is-section-retraction-pair + ( is-equiv-s : is-equiv A B s) + : is-equiv B A' r + := + is-equiv-left-factor A B A' + ( s) ( is-equiv-s) + ( r) ( is-sec-rec-pair) + +#end is-equiv-is-section-retraction-pair +``` + +## Retracts + +We say that a type `A` is a retract of a type `B` if we have a map `s : A → B` +which has a retraction. + +```rzk title="The type of proofs that A is a retract of B" +#def is-retract-of + ( A B : U) + : U + := Σ ( s : A → B) , has-retraction A B s + +#def section-is-retract-of + ( A B : U) + ( (s , (_ , _)) : is-retract-of A B) + : A → B + := s + +#def retraction-is-retract-of + ( A B : U) + ( (_ , (r , _)) : is-retract-of A B) + : B → A + := r + +#def homotopy-is-retract-of + ( A B : U) + ( (s , (r , η)) : is-retract-of A B) + : homotopy A A ( \ a → r ( s a)) ( identity A) + := η +``` + +Section-retraction pairs `A → B → A'` are a convenient way to exhibit both `A` +and `A'` as retracts of `B`. + +```rzk +#def is-retract-of-left-section-retraction-pair + ( A B A' : U) + ( s : A → B) + ( r : B → A') + ( is-sr-pair-sr : is-section-retraction-pair A B A' s r) + : is-retract-of A B + := + ( ( s) + , ( has-retraction-internalize A B s ((A' , r) , is-sr-pair-sr))) + +#def is-retract-of-right-section-retraction-pair + ( A B A' : U) + ( s : A → B) + ( r : B → A') + ( is-sr-pair-sr : is-section-retraction-pair A B A' s r) + : is-retract-of A' B + := + ( first ( has-section-internalize B A' r ((A , s) , is-sr-pair-sr)) + , ( r + , second ( has-section-internalize B A' r ((A , s) , is-sr-pair-sr)))) +``` + ## Function extensionality By path induction, an identification between functions defines a homotopy. @@ -611,8 +804,8 @@ dependent function types. ( famisequiv : (x : X) → is-equiv (A x) (B x) (f x)) : is-equiv ((x : X) → A x) ((x : X) → B x) ( \ a x → f x (a x)) := - ( ( ( \ b x → first (first (famisequiv x)) (b x)) , - ( \ a → + ( ( ( \ b x → first (first (famisequiv x)) (b x)) + , ( \ a → eq-htpy X A ( \ x → @@ -620,13 +813,12 @@ dependent function types. ( first (famisequiv x)) ( f x (a x))) ( a) - ( \ x → second (first (famisequiv x)) (a x)))) , - ( ( \ b x → first (second (famisequiv x)) (b x)) , - ( \ b → + ( \ x → second (first (famisequiv x)) (a x)))) + , ( ( \ b x → first (second (famisequiv x)) (b x)) + , ( \ b → eq-htpy X B - ( \ x → - f x (first (second (famisequiv x)) (b x))) + ( \ x → f x (first (second (famisequiv x)) (b x))) ( b) ( \ x → second (second (famisequiv x)) (b x))))) ``` @@ -638,8 +830,8 @@ dependent function types. ( famequiv : (x : X) → Equiv (A x) (B x)) : Equiv ((x : X) → A x) ((x : X) → B x) := - ( ( \ a x → (first (famequiv x)) (a x)) , - ( is-equiv-function-is-equiv-family + ( ( \ a x → (first (famequiv x)) (a x)) + , ( is-equiv-function-is-equiv-family ( X) ( A) ( B) @@ -688,6 +880,16 @@ dependent function types. := (rev A x y , ((rev A y x , rev-rev A x y) , (rev A y x , rev-rev A y x))) ``` +```rzk +#def ind-rev + ( A : U) + ( x y : A) + ( B : (x = y) → U) + : ((p : y = x) → B (rev A y x p)) → ( q : x = y) → B q + := + ind-has-section-equiv (y = x) (x = y) (equiv-rev A y x) ( B) +``` + ## Concatenation with a fixed path is an equivalence ```rzk @@ -697,20 +899,20 @@ dependent function types. ( p : x = y) : Equiv (y = z) (x = z) := - ( concat A x y z p, - ( ( concat A y x z (rev A x y p), retraction-preconcat A x y z p), - ( concat A y x z (rev A x y p), section-preconcat A x y z p))) + ( concat A x y z p + , ( ( concat A y x z (rev A x y p), retraction-preconcat A x y z p) + , ( concat A y x z (rev A x y p), section-preconcat A x y z p))) #def equiv-postconcat ( A : U) ( x y z : A) ( q : y = z) : Equiv (x = y) (x = z) := - ( \ p → concat A x y z p q, - ( ( \ r → concat A x z y r (rev A y z q), - retraction-postconcat A x y z q), - ( \ r → concat A x z y r (rev A y z q), - section-postconcat A x y z q))) + ( \ p → concat A x y z p q + , ( ( \ r → concat A x z y r (rev A y z q) + , retraction-postconcat A x y z q) + , ( \ r → concat A x z y r (rev A y z q) + , section-postconcat A x y z q))) ``` ## Transport along a path is an equivalence @@ -736,8 +938,8 @@ dependent function types. ( β : B' → B) : U := - Σ ( ( s',s) : product ( A' → B' ) ( A → B)), - ( ( a' : A') → β ( s' a') = s ( α a')) + Σ ( ( s',s) : product ( A' → B' ) ( A → B)) + , ( ( a' : A') → β ( s' a') = s ( α a')) #def Equiv-of-maps ( A' A : U) @@ -746,11 +948,10 @@ dependent function types. ( β : B' → B) : U := - Σ ( ((s', s), _) : map-of-maps A' A α B' B β), - ( product - ( is-equiv A' B' s') - ( is-equiv A B s) - ) + Σ ( ((s', s), _) : map-of-maps A' A α B' B β) + , ( product + ( is-equiv A' B' s') + ( is-equiv A B s)) #def is-equiv-equiv-is-equiv ( A' A : U) @@ -765,11 +966,10 @@ dependent function types. := is-equiv-right-factor A' A B α s is-equiv-s ( is-equiv-rev-homotopy A' B - ( comp A' B' B β s') - ( comp A' A B s α) - ( η ) - ( is-equiv-comp A' B' B s' is-equiv-s' β is-equiv-β) - ) + ( comp A' B' B β s') + ( comp A' A B s α) + ( η ) + ( is-equiv-comp A' B' B s' is-equiv-s' β is-equiv-β)) #def is-equiv-Equiv-is-equiv ( A' A : U) @@ -778,8 +978,7 @@ dependent function types. ( β : B' → B) ( ( S, (is-equiv-s',is-equiv-s)) : Equiv-of-maps A' A α B' B β ) : is-equiv B' B β → is-equiv A' A α - := - is-equiv-equiv-is-equiv A' A α B' B β S is-equiv-s' is-equiv-s + := is-equiv-equiv-is-equiv A' A α B' B β S is-equiv-s' is-equiv-s #def is-equiv-equiv-is-equiv' ( A' A : U) @@ -797,8 +996,7 @@ dependent function types. ( comp A' B' B β s') ( comp A' A B s α) ( η) - ( is-equiv-comp A' A B α is-equiv-α s is-equiv-s) - ) + ( is-equiv-comp A' A B α is-equiv-α s is-equiv-s)) #def is-equiv-Equiv-is-equiv' ( A' A : U) @@ -807,6 +1005,5 @@ dependent function types. ( β : B' → B) ( ( S, (is-equiv-s',is-equiv-s)) : Equiv-of-maps A' A α B' B β ) : is-equiv A' A α → is-equiv B' B β - := - is-equiv-equiv-is-equiv' A' A α B' B β S is-equiv-s' is-equiv-s + := is-equiv-equiv-is-equiv' A' A α B' B β S is-equiv-s' is-equiv-s ``` diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md index 04aa5c54..42f890a1 100644 --- a/src/hott/06-contractible.rzk.md +++ b/src/hott/06-contractible.rzk.md @@ -48,7 +48,7 @@ This is a literate `rzk` file: ``` ```rzk title="A path between any pair of terms in a contractible type" -#def eq-is-contr uses (is-contr-A) +#def all-elements-equal-is-contr uses (is-contr-A) (x y : A) : x = y := @@ -70,10 +70,9 @@ The prototypical contractible type is the unit type, which is built-in to rzk. : C x := C-unit -#def is-prop-unit - ( x y : Unit) - : x = y - := refl +#def is-contr-Unit + : is-contr Unit + := (unit, \ _ → refl) ``` ```rzk title="The terminal projection as a constant map" @@ -86,24 +85,24 @@ The prototypical contractible type is the unit type, which is built-in to rzk. ## Identity types of unit types ```rzk -#def terminal-map-of-path-types-of-Unit-has-retr +#def has-retraction-terminal-map-path-types-Unit ( x y : Unit) : has-retraction (x = y) Unit (terminal-map (x = y)) := ( \ a → refl , \ p → ind-path (Unit) (x) (\ y' p' → refl =_{x = y'} p') (refl) (y) (p)) -#def terminal-map-of-path-types-of-Unit-has-sec +#def has-section-terminal-map-path-types-Unit ( x y : Unit) : has-section (x = y) Unit (terminal-map (x = y)) := ( \ a → refl , \ a → refl) -#def terminal-map-of-path-types-of-Unit-is-equiv +#def is-equiv-terminal-map-path-types-Unit ( x y : Unit) : is-equiv (x = y) Unit (terminal-map (x = y)) := - ( terminal-map-of-path-types-of-Unit-has-retr x y , - terminal-map-of-path-types-of-Unit-has-sec x y) + ( has-retraction-terminal-map-path-types-Unit x y , + has-section-terminal-map-path-types-Unit x y) ``` ## Characterization of contractibility @@ -116,7 +115,7 @@ A type is contractible if and only if its terminal map is an equivalence. : U := is-equiv A Unit (terminal-map A) -#def contr-implies-terminal-map-is-equiv-retr +#def has-retraction-terminal-map-is-contr ( A : U) ( is-contr-A : is-contr A) : has-retraction A Unit (terminal-map A) @@ -124,32 +123,32 @@ A type is contractible if and only if its terminal map is an equivalence. ( constant Unit A (center-contraction A is-contr-A) , \ y → (homotopy-contraction A is-contr-A) y) -#def contr-implies-terminal-map-is-equiv-sec +#def has-section-terminal-map-is-contr ( A : U) ( is-contr-A : is-contr A) : has-section A Unit (terminal-map A) := ( constant Unit A (center-contraction A is-contr-A) , \ z → refl) -#def contr-implies-terminal-map-is-equiv +#def is-equiv-terminal-map-is-contr ( A : U) ( is-contr-A : is-contr A) : is-equiv A Unit (terminal-map A) := - ( contr-implies-terminal-map-is-equiv-retr A is-contr-A , - contr-implies-terminal-map-is-equiv-sec A is-contr-A) + ( has-retraction-terminal-map-is-contr A is-contr-A , + has-section-terminal-map-is-contr A is-contr-A) -#def terminal-map-is-equiv-implies-contr +#def is-contr-is-equiv-terminal-map ( A : U) (e : terminal-map-is-equiv A) : is-contr A := ( (first (first e)) unit , (second (first e))) -#def contr-iff-terminal-map-is-equiv +#def is-equiv-terminal-map-iff-is-contr ( A : U) : iff (is-contr A) (terminal-map-is-equiv A) := - ( ( contr-implies-terminal-map-is-equiv A) , - ( terminal-map-is-equiv-implies-contr A)) + ( ( is-equiv-terminal-map-is-contr A) , + ( is-contr-is-equiv-terminal-map A)) #def equiv-with-contractible-domain-implies-contractible-codomain ( A B : U) @@ -157,105 +156,75 @@ A type is contractible if and only if its terminal map is an equivalence. ( is-contr-A : is-contr A) : is-contr B := - ( terminal-map-is-equiv-implies-contr B + ( is-contr-is-equiv-terminal-map B ( second ( equiv-comp B A Unit ( inv-equiv A B f) ( ( terminal-map A) , - ( contr-implies-terminal-map-is-equiv A is-contr-A))))) - -#def equiv-with-contractible-codomain-implies-contractible-domain - ( A B : U) - ( f : Equiv A B) - ( is-contr-B : is-contr B) - : is-contr A - := - ( equiv-with-contractible-domain-implies-contractible-codomain B A - ( inv-equiv A B f) is-contr-B) + ( is-equiv-terminal-map-is-contr A is-contr-A))))) -#def equiv-then-domain-contractible-iff-codomain-contractible - ( A B : U) - ( f : Equiv A B) - : ( iff (is-contr A) (is-contr B)) - := - ( \ is-contr-A → - ( equiv-with-contractible-domain-implies-contractible-codomain - A B f is-contr-A) , - \ is-contr-B → - ( equiv-with-contractible-codomain-implies-contractible-domain - A B f is-contr-B)) - -#def path-types-of-Unit-are-contractible +#def is-contr-path-types-Unit ( x y : Unit) : is-contr (x = y) := - ( terminal-map-is-equiv-implies-contr - ( x = y) (terminal-map-of-path-types-of-Unit-is-equiv x y)) + ( is-contr-is-equiv-terminal-map + ( x = y) (is-equiv-terminal-map-path-types-Unit x y)) ``` ## Retracts of contractible types A retract of contractible types is contractible. -```rzk title="The type of proofs that A is a retract of B" -#def is-retract-of - ( A B : U) - : U - := Σ ( s : A → B) , has-retraction A B s - -#section retraction-data +```rzk title="If A is a retract of a contractible type it has a term" +#section is-contr-is-retract-of-is-contr #variables A B : U -#variable is-retract-of-A-B : is-retract-of A B - -#def is-retract-of-section - : A → B - := first is-retract-of-A-B +#variable is-retr-of-A-B : is-retract-of A B -#def is-retract-of-retraction - : B → A - := first (second is-retract-of-A-B) - -#def is-retract-of-homotopy - : homotopy A A (comp A B A is-retract-of-retraction is-retract-of-section) (identity A) - := second (second is-retract-of-A-B) -``` - -```rzk title="If A is a retract of a contractible type it has a term" -#def is-retract-of-is-contr-isInhabited uses (is-retract-of-A-B) +#def is-inhabited-is-contr-is-retract-of uses (is-retr-of-A-B) ( is-contr-B : is-contr B) : A - := is-retract-of-retraction (center-contraction B is-contr-B) + := + retraction-is-retract-of A B is-retr-of-A-B + ( center-contraction B is-contr-B) ``` ```rzk title="If A is a retract of a contractible type it has a contracting homotopy" -#def is-retract-of-is-contr-hasHtpy uses (is-retract-of-A-B) +#def has-homotopy-is-contr-is-retract-of uses (is-retr-of-A-B) ( is-contr-B : is-contr B) ( a : A) - : ( is-retract-of-is-contr-isInhabited is-contr-B) = a + : ( is-inhabited-is-contr-is-retract-of is-contr-B) = a := concat ( A) - ( is-retract-of-is-contr-isInhabited is-contr-B) - ( (comp A B A is-retract-of-retraction is-retract-of-section) a) + ( is-inhabited-is-contr-is-retract-of is-contr-B) + ( comp A B A + ( retraction-is-retract-of A B is-retr-of-A-B) + ( section-is-retract-of A B is-retr-of-A-B) + ( a)) ( a) - ( ap B A (center-contraction B is-contr-B) (is-retract-of-section a) - ( is-retract-of-retraction) - ( homotopy-contraction B is-contr-B (is-retract-of-section a))) - ( is-retract-of-homotopy a) + ( ap B A + ( center-contraction B is-contr-B) + ( section-is-retract-of A B is-retr-of-A-B a) + ( retraction-is-retract-of A B is-retr-of-A-B) + ( homotopy-contraction B is-contr-B + ( section-is-retract-of A B is-retr-of-A-B a))) + ( homotopy-is-retract-of A B is-retr-of-A-B a) ``` ```rzk title="If A is a retract of a contractible type it is contractible" -#def is-contr-is-retract-of-is-contr uses (is-retract-of-A-B) +#def is-contr-is-retract-of-is-contr uses (is-retr-of-A-B) ( is-contr-B : is-contr B) : is-contr A := - ( is-retract-of-is-contr-isInhabited is-contr-B , - is-retract-of-is-contr-hasHtpy is-contr-B) + ( is-inhabited-is-contr-is-retract-of is-contr-B , + has-homotopy-is-contr-is-retract-of is-contr-B) + +#end is-contr-is-retract-of-is-contr ``` ```rzk -#end retraction-data + ``` ## Functions between contractible types @@ -271,7 +240,7 @@ A retract of contractible types is contractible. ( ( \ b → center-contraction A is-contr-A , \ a → homotopy-contraction A is-contr-A a) , ( \ b → center-contraction A is-contr-A , - \ b → eq-is-contr B is-contr-B + \ b → all-elements-equal-is-contr B is-contr-B (f (center-contraction A is-contr-A)) b)) ``` @@ -533,48 +502,52 @@ A type is contractible if and only if it has singleton induction. ## Identity types of contractible types -We show that any two paths between the same endpoints in a contractible type are the same. +We show that any two paths between the same endpoints in a contractible type are +the same. + +In a contractible type any path $p : x = y$ is equal to the path constructed in +`all-elements-equal-is-contr`. -In a contractible type any path $p : x = y$ is equal to the path constructed in `eq-is-contr`. ```rzk #define path-eq-path-through-center-is-contr ( A : U) ( is-contr-A : is-contr A) ( x y : A) ( p : x = y) - : ((eq-is-contr A is-contr-A x y) = p) - := + : ((all-elements-equal-is-contr A is-contr-A x y) = p) + := ind-path ( A) ( x) - ( \ y' p' → (eq-is-contr A is-contr-A x y') = p') - ( left-inverse-concat A (center-contraction A is-contr-A) x (homotopy-contraction A is-contr-A x)) - ( y) - ( p) + ( \ y' p' → (all-elements-equal-is-contr A is-contr-A x y') = p') + ( left-inverse-concat A (center-contraction A is-contr-A) x (homotopy-contraction A is-contr-A x)) + ( y) + ( p) ``` -Finally, in a contractible type any two paths between the same end points are equal. There are many possible proofs of this (e.g. identifying contractible types with the unit type where it is more transparent), but we proceed by gluing together the two identifications to the out and back path. +Finally, in a contractible type any two paths between the same end points are +equal. There are many possible proofs of this (e.g. identifying contractible +types with the unit type where it is more transparent), but we proceed by gluing +together the two identifications to the out and back path. ```rzk -#define all-paths-eq-is-contr +#define all-paths-equal-is-contr ( A : U) ( is-contr-A : is-contr A) ( x y : A) - ( p q : x = y) + ( p q : x = y) : (p = q) - := + := concat ( x = y) ( p) - ( eq-is-contr A is-contr-A x y) + ( all-elements-equal-is-contr A is-contr-A x y) ( q) ( rev - (x = y) - ( eq-is-contr A is-contr-A x y) - ( p) + (x = y) + ( all-elements-equal-is-contr A is-contr-A x y) + ( p) ( path-eq-path-through-center-is-contr A is-contr-A x y p)) ( path-eq-path-through-center-is-contr A is-contr-A x y q) ``` - - diff --git a/src/hott/07-fibers.rzk.md b/src/hott/07-fibers.rzk.md index 581adcf7..c868a218 100644 --- a/src/hott/07-fibers.rzk.md +++ b/src/hott/07-fibers.rzk.md @@ -117,7 +117,7 @@ Contractible maps are equivalences: (a : A) : (is-contr-map-data-in-fiber a) =_{fib A B f (f a)} (a , refl) := - eq-is-contr + all-elements-equal-is-contr ( fib A B f (f a)) ( is-contr-f (f a)) ( is-contr-map-data-in-fiber a) diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md index cee81ef3..becae7a8 100644 --- a/src/hott/08-families-of-maps.rzk.md +++ b/src/hott/08-families-of-maps.rzk.md @@ -16,109 +16,98 @@ maps. ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - : ( Σ (x : A) , B x) → (Σ (x : A) , C x) - := \ z → (first z , f (first z) (second z)) + : ( total-type A B) → (total-type A C) + := \ (a , b) → (a , f a b) -#def total-map-to-fiber +#def fib-total-map-fib-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( w : (Σ (x : A) , C x)) - : fib (B (first w)) (C (first w)) (f (first w)) (second w) → - ( fib (Σ (x : A) , B x) (Σ (x : A) , C x) (total-map A B C f) w) - := - \ (b , p) → - ( (first w , b) , - eq-eq-fiber-Σ A C (first w) (f (first w) b) (second w) p) + ( (a , c) : total-type A C) + : fib (B a) (C a) (f a) (c) + → fib (total-type A B) (total-type A C) (total-map A B C f) (a , c) + := \ (b , p) → ((a , b) , eq-eq-fiber-Σ A C a (f a b) c p) -#def total-map-from-fiber +#def fib-fiberwise-fib-total-map ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( w : (Σ (x : A) , C x)) - : fib (Σ (x : A) , B x) (Σ (x : A) , C x) (total-map A B C f) w → - fib (B (first w)) (C (first w)) (f (first w)) (second w) + : ( (a , c) : total-type A C) + → fib (total-type A B) (total-type A C) (total-map A B C f) (a , c) + → fib (B a) (C a) (f a) (c) := - \ (z , p) → - ind-path - ( Σ (x : A) , C x) - ( total-map A B C f z) - ( \ w' p' → fib (B (first w')) (C (first w')) (f (first w')) (second w')) - ( second z , refl) - ( w) - ( p) + ind-fib (total-type A B) (total-type A C) (total-map A B C f) + ( \ (a' , c') _ → fib (B a') (C a') (f a') c') + ( \ (_ , b') → (b' , refl)) -#def total-map-to-fiber-retraction +#def has-retraction-fib-total-map-fib-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( w : (Σ (x : A) , C x)) + ( (a , c) : total-type A C) : has-retraction - ( fib (B (first w)) (C (first w)) (f (first w)) (second w)) - ( fib (Σ (x : A) , B x) (Σ (x : A) , C x) (total-map A B C f) w) - ( total-map-to-fiber A B C f w) + ( fib (B a) (C a) (f a) (c)) + ( fib (total-type A B) (total-type A C) (total-map A B C f) (a , c)) + ( fib-total-map-fib-fiberwise A B C f (a , c)) := - ( ( total-map-from-fiber A B C f w) , - ( \ (b , p) → - ind-path - ( C (first w)) - ( f (first w) b) - ( \ w1 p' → - ( ( total-map-from-fiber A B C f ((first w , w1))) - ( (total-map-to-fiber A B C f (first w , w1)) (b , p'))) - =_{(fib (B (first w)) (C (first w)) (f (first w)) (w1))} - ( b , p')) - ( refl) - ( second w) - ( p))) + ( ( fib-fiberwise-fib-total-map A B C f (a , c)) + , ( \ (b , p) → + ind-path ( C a) ( f a b) + ( \ c' p' → + ( ( fib-fiberwise-fib-total-map A B C f ((a , c'))) + ( (fib-total-map-fib-fiberwise A B C f (a , c')) (b , p')) + = ( b , p'))) + ( refl) + ( c) + ( p))) -#def total-map-to-fiber-section +#def has-section-fib-total-map-fib-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( w : (Σ (x : A) , C x)) + ( (a , c) : (Σ (x : A) , C x)) : has-section - ( fib (B (first w)) (C (first w)) (f (first w)) (second w)) - ( fib (Σ (x : A) , B x) (Σ (x : A) , C x) (total-map A B C f) w) - ( total-map-to-fiber A B C f w) + ( fib (B a) (C a) (f a) c) + ( fib (total-type A B) (total-type A C) (total-map A B C f) (a , c)) + ( fib-total-map-fib-fiberwise A B C f (a , c)) := - ( ( total-map-from-fiber A B C f w) , - ( \ (z , p) → + ( ( fib-fiberwise-fib-total-map A B C f (a , c)) + , ( \ ((a', b') , p) → ind-path - ( Σ (x : A) , C x) - ( first z , f (first z) (second z)) + ( total-type A C) + ( a' , f a' b') ( \ w' p' → - ( ( total-map-to-fiber A B C f w') - ( ( total-map-from-fiber A B C f w') (z , p'))) = - ( z , p')) + ( ( fib-total-map-fib-fiberwise A B C f w') + ( ( fib-fiberwise-fib-total-map A B C f w') ((a' , b') , p')) + = ( (a' , b') , p'))) ( refl) - ( w) + ( a , c) ( p))) -#def total-map-to-fiber-is-equiv +#def is-equiv-fib-total-map-fib-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( w : (Σ (x : A) , C x)) + ( (a , c) : total-type A C) : is-equiv - ( fib (B (first w)) (C (first w)) (f (first w)) (second w)) - ( fib (Σ (x : A) , B x) (Σ (x : A) , C x) - ( total-map A B C f) w) - ( total-map-to-fiber A B C f w) + ( fib (B a) (C a) (f a) c) + ( fib (total-type A B) (total-type A C) ( total-map A B C f) (a , c)) + ( fib-total-map-fib-fiberwise A B C f (a , c)) := - ( total-map-to-fiber-retraction A B C f w , - total-map-to-fiber-section A B C f w) + ( has-retraction-fib-total-map-fib-fiberwise A B C f (a , c) + , has-section-fib-total-map-fib-fiberwise A B C f (a , c)) -#def total-map-fiber-equiv +#def equiv-fib-total-map-fib-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( w : (Σ (x : A) , C x)) + ( (a , c) : total-type A C) : Equiv - ( fib (B (first w)) (C (first w)) (f (first w)) (second w)) - ( fib (Σ (x : A) , B x) (Σ (x : A) , C x) - ( total-map A B C f) w) - := (total-map-to-fiber A B C f w , total-map-to-fiber-is-equiv A B C f w) + ( fib (B a) (C a) (f a) c) + ( fib (total-type A B) (total-type A C) ( total-map A B C f) (a , c)) + := + ( fib-total-map-fib-fiberwise A B C f (a , c) + , is-equiv-fib-total-map-fib-fiberwise A B C f (a, c)) ``` ## Families of equivalences @@ -127,156 +116,143 @@ A family of equivalences induces an equivalence on total spaces and conversely. It will be easiest to work with the incoherent notion of two-sided-inverses. ```rzk -#def invertible-family-total-inverse +#def map-inverse-total-has-inverse-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) ( invfamily : (a : A) → has-inverse (B a) (C a) (f a)) - : ( Σ (x : A) , C x) → (Σ (x : A) , B x) - := \ (a , c) → (a , (map-inverse-has-inverse (B a) (C a) (f a) (invfamily a)) c) + : (total-type A C) → (total-type A B) + := + \ (a , c) → + (a , (map-inverse-has-inverse (B a) (C a) (f a) (invfamily a)) c) -#def invertible-family-total-retraction +#def has-retraction-total-has-inverse-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) ( invfamily : (a : A) → has-inverse (B a) (C a) (f a)) - : has-retraction - ( Σ (x : A) , B x) - ( Σ (x : A) , C x) - ( total-map A B C f) + : has-retraction (total-type A B) (total-type A C) (total-map A B C f) := - ( invertible-family-total-inverse A B C f invfamily , + ( map-inverse-total-has-inverse-fiberwise A B C f invfamily , \ (a , b) → (eq-eq-fiber-Σ A B a ( (map-inverse-has-inverse (B a) (C a) (f a) (invfamily a)) (f a b)) b ( (first (second (invfamily a))) b))) -#def invertible-family-total-section +#def has-section-total-has-inverse-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) ( invfamily : (a : A) → has-inverse (B a) (C a) (f a)) - : has-section (Σ (x : A) , B x) (Σ (x : A) , C x) (total-map A B C f) + : has-section (total-type A B) (total-type A C) (total-map A B C f) := - ( invertible-family-total-inverse A B C f invfamily , + ( map-inverse-total-has-inverse-fiberwise A B C f invfamily , \ (a , c) → ( eq-eq-fiber-Σ A C a ( f a ((map-inverse-has-inverse (B a) (C a) (f a) (invfamily a)) c)) c ( (second (second (invfamily a))) c))) -#def invertible-family-total-invertible +#def has-inverse-total-has-inverse-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) ( invfamily : (a : A) → has-inverse (B a) (C a) (f a)) - : has-inverse - ( Σ (x : A) , B x) - ( Σ (x : A) , C x) - ( total-map A B C f) + : has-inverse (total-type A B) (total-type A C) (total-map A B C f) := - ( invertible-family-total-inverse A B C f invfamily , - ( second (invertible-family-total-retraction A B C f invfamily) , - second (invertible-family-total-section A B C f invfamily))) + ( map-inverse-total-has-inverse-fiberwise A B C f invfamily , + ( second (has-retraction-total-has-inverse-fiberwise A B C f invfamily) , + second (has-section-total-has-inverse-fiberwise A B C f invfamily))) +``` -#def family-of-equiv-total-equiv +The one-way result: that a family of equivalence gives an invertible map (and +thus an equivalence) on total spaces. + +```rzk +#def has-inverse-total-is-equiv-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) ( familyequiv : (a : A) → is-equiv (B a) (C a) (f a)) - : is-equiv - ( Σ (x : A) , B x) (Σ (x : A) , C x) (total-map A B C f) + : has-inverse (total-type A B) ( total-type A C) ( total-map A B C f) := - is-equiv-has-inverse - ( Σ (x : A) , B x) (Σ (x : A) , C x) (total-map A B C f) - ( invertible-family-total-invertible A B C f - ( \ a → has-inverse-is-equiv (B a) (C a) (f a) (familyequiv a))) + has-inverse-total-has-inverse-fiberwise A B C f + ( \ a → has-inverse-is-equiv (B a) (C a) (f a) (familyequiv a)) -#def total-equiv-family-equiv +#def is-equiv-total-is-equiv-fiberwise ( A : U) ( B C : A → U) - ( familyeq : (a : A) → Equiv (B a) (C a)) - : Equiv (Σ (x : A) , B x) (Σ (x : A) , C x) + ( f : (a : A) → (B a) → (C a)) + ( familyequiv : (a : A) → is-equiv (B a) (C a) (f a)) + : is-equiv ( total-type A B) (total-type A C) (total-map A B C f) := - ( total-map A B C (\ a → first (familyeq a)) , - family-of-equiv-total-equiv A B C - ( \ a → first (familyeq a)) - ( \ a → second (familyeq a))) -``` - -The one-way result: that a family of equivalence gives an invertible map (and -thus an equivalence) on total spaces. + is-equiv-has-inverse + ( total-type A B) ( total-type A C) ( total-map A B C f) + ( has-inverse-total-is-equiv-fiberwise A B C f familyequiv) -```rzk -#def total-has-inverse-family-equiv +#def total-equiv-family-of-equiv ( A : U) ( B C : A → U) - ( f : (a : A) → (B a) → (C a)) - ( familyequiv : (a : A) → is-equiv (B a) (C a) (f a)) - : has-inverse (Σ (x : A) , B x) (Σ (x : A) , C x) (total-map A B C f) + ( familyeq : (a : A) → Equiv (B a) (C a)) + : Equiv (total-type A B) (total-type A C) := - invertible-family-total-invertible A B C f - ( \ a → has-inverse-is-equiv (B a) (C a) (f a) (familyequiv a)) + ( total-map A B C (\ a → first (familyeq a)) + , is-equiv-total-is-equiv-fiberwise A B C + ( \ a → first (familyeq a)) + ( \ a → second (familyeq a))) ``` For the converse, we make use of our calculation on fibers. The first implication could be proven similarly. ```rzk -#def total-contr-map-family-of-contr-maps +#def is-contr-map-total-is-contr-map-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( totalcontrmap : - is-contr-map - ( Σ (x : A) , B x) - ( Σ (x : A) , C x) - ( total-map A B C f)) + ( totalcontrmap + : is-contr-map (total-type A B) ( total-type A C) ( total-map A B C f)) ( a : A) : is-contr-map (B a) (C a) (f a) := \ c → is-contr-equiv-is-contr' - ( fib (B a) (C a) (f a) c) - ( fib (Σ (x : A) , B x) (Σ (x : A) , C x) - ( total-map A B C f) ((a , c))) - ( total-map-fiber-equiv A B C f ((a , c))) - ( totalcontrmap ((a , c))) + ( fib (B a) (C a) (f a) c) + ( fib ( total-type A B) ( total-type A C) ( total-map A B C f) (a , c)) + ( equiv-fib-total-map-fib-fiberwise A B C f (a , c)) + ( totalcontrmap (a , c)) -#def total-equiv-family-of-equiv +#def is-equiv-fiberwise-is-equiv-total ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( totalequiv : is-equiv - ( Σ (x : A) , B x) - ( Σ (x : A) , C x) - ( total-map A B C f)) + ( totalequiv + : is-equiv (total-type A B) (total-type A C) ( total-map A B C f)) (a : A) : is-equiv (B a) (C a) (f a) := is-equiv-is-contr-map (B a) (C a) (f a) - ( total-contr-map-family-of-contr-maps A B C f + ( is-contr-map-total-is-contr-map-fiberwise A B C f ( is-contr-map-is-equiv - ( Σ (x : A) , B x) (Σ (x : A) , C x) - ( total-map A B C f) totalequiv) a) + ( total-type A B) (total-type A C) (total-map A B C f) + ( totalequiv)) + ( a)) -#def family-equiv-total-equiv +#def family-of-equiv-is-equiv-total ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) - ( totalequiv : is-equiv - ( Σ (x : A) , B x) - ( Σ (x : A) , C x) - ( total-map A B C f)) + ( totalequiv + : is-equiv (total-type A B) (total-type A C) ( total-map A B C f)) ( a : A) : Equiv (B a) (C a) - := ( f a , total-equiv-family-of-equiv A B C f totalequiv a) + := ( f a , is-equiv-fiberwise-is-equiv-total A B C f totalequiv a) ``` In summary, a family of maps is an equivalence iff the map on total spaces is an equivalence. ```rzk -#def total-equiv-iff-family-of-equiv +#def is-equiv-total-iff-is-equiv-fiberwise ( A : U) ( B C : A → U) ( f : (a : A) → (B a) → (C a)) @@ -284,17 +260,21 @@ equivalence. ( (a : A) → is-equiv (B a) (C a) (f a)) ( is-equiv (Σ (x : A) , B x) (Σ (x : A) , C x) ( total-map A B C f)) - := (family-of-equiv-total-equiv A B C f , total-equiv-family-of-equiv A B C f) + := + ( is-equiv-total-is-equiv-fiberwise A B C f + , is-equiv-fiberwise-is-equiv-total A B C f) ``` -## Endpoint based path spaces +## Path spaces + +### Based path spaces ```rzk title="An equivalence between the based path spaces" #def equiv-based-paths ( A : U) ( a : A) : Equiv (Σ (x : A) , x = a) (Σ (x : A) , a = x) - := total-equiv-family-equiv A (\ x → x = a) (\ x → a = x) (\ x → equiv-rev A x a) + := total-equiv-family-of-equiv A (\ x → x = a) (\ x → a = x) (\ x → equiv-rev A x a) ``` ```rzk title="Endpoint based path spaces are contractible" @@ -308,6 +288,45 @@ equivalence. ( is-contr-based-paths A a) ``` +### Free path spaces + +The canonical map from a type to its the free path type is an equivalence. + +```rzk +#def free-paths + ( A : U) + : U + := Σ ( (x , y) : product A A) , (x = y) + +#def constant-free-path + ( A : U) + ( a : A) + : free-paths A + := ((a , a) , refl) + +#def is-constant-free-path + ( A : U) + ( ((a , y) , p) : free-paths A) + : constant-free-path A a = ((a , y), p) + := + ind-path A a + ( \ x p' → constant-free-path A a = ((a , x) , p')) + ( refl) + ( y) ( p) + +#def start-free-path + ( A : U) + : free-paths A → A + := \ ((a , _) , _) → a + +#def is-equiv-constant-free-path + ( A : U) + : is-equiv A (free-paths A) (constant-free-path A) + := + ( ( start-free-path A , \ _ → refl) + , ( start-free-path A , is-constant-free-path A)) +``` + ## Pullback of a type family A family of types over B pulls back along any function f : A → B to define a @@ -347,8 +366,8 @@ The pullback of a family along homotopic maps is equivalent. ( pullback A B g C a) ( pullback-homotopy) := - ( map-inverse-pullback-homotopy , - \ c → + ( map-inverse-pullback-homotopy + , \ c → concat ( pullback A B f C a) ( transport B C (g a) (f a) @@ -367,8 +386,8 @@ The pullback of a family along homotopic maps is equivalent. : has-section (pullback A B f C a) (pullback A B g C a) ( pullback-homotopy) := - ( map-inverse-pullback-homotopy , - \ c → + ( map-inverse-pullback-homotopy + , \ c → concat ( pullback A B g C a) ( transport B C (f a) (g a) (α a) @@ -545,7 +564,7 @@ As a corollary, we show that pullback along an equivalence induces an equivalence of total spaces. ```rzk -#def total-equiv-pullback-is-equiv +#def equiv-total-pullback-is-equiv ( A B : U) ( f : A → B) ( is-equiv-f : is-equiv A B f) @@ -567,6 +586,13 @@ equivalence of total spaces. ## Fundamental theorem of identity types +The fundamental theorem of identity types concerns the following question: Given +a type family `B : A → U`, when is `B` equivalent to `\ x → a x` for some +`a : A`? + +We start by fixing `a : A` and investigating when a map of families +`x : A → (a = x) → B x` is a (fiberwise) equivalence. + ```rzk #section fundamental-thm-id-types @@ -575,25 +601,26 @@ equivalence of total spaces. #variable B : A → U #variable f : (x : A) → (a = x) → B x -#def fund-id-fam-of-eqs-implies-sum-over-codomain-contr - : ((x : A) → (is-equiv (a = x) (B x) (f x))) → (is-contr (Σ (x : A) , B x)) +#def is-contr-total-are-equiv-from-paths + : ( (x : A) → (is-equiv (a = x) (B x) (f x))) + → ( is-contr (Σ (x : A) , B x)) := ( \ familyequiv → ( equiv-with-contractible-domain-implies-contractible-codomain ( Σ (x : A) , a = x) (Σ (x : A) , B x) - ( ( total-map A ( \ x → (a = x)) B f) , - ( is-equiv-has-inverse (Σ (x : A) , a = x) (Σ (x : A) , B x) + ( ( total-map A ( \ x → (a = x)) B f) + , ( is-equiv-has-inverse (Σ (x : A) , a = x) (Σ (x : A) , B x) ( total-map A ( \ x → (a = x)) B f) - ( total-has-inverse-family-equiv A + ( has-inverse-total-is-equiv-fiberwise A ( \ x → (a = x)) B f familyequiv))) ( is-contr-based-paths A a))) -#def fund-id-sum-over-codomain-contr-implies-fam-of-eqs - : ( is-contr (Σ (x : A) , B x)) → - ( (x : A) → (is-equiv (a = x) (B x) (f x))) +#def are-equiv-from-paths-is-contr-total + : ( is-contr (Σ (x : A) , B x)) + → ( (x : A) → (is-equiv (a = x) (B x) (f x))) := ( \ is-contr-Σ-A-B x → - total-equiv-family-of-equiv A + is-equiv-fiberwise-is-equiv-total A ( \ x' → (a = x')) ( B) ( f) @@ -625,7 +652,7 @@ fundamental theorem: ( \ (u' , p') → P u' p') ( contr-implies-singleton-induction-pointed ( Σ (z : A) , B z) - ( fund-id-fam-of-eqs-implies-sum-over-codomain-contr familyequiv) + ( is-contr-total-are-equiv-from-paths familyequiv) ( \ (x' , p') → P x' p')) ( p0) ( u , p) @@ -633,6 +660,40 @@ fundamental theorem: #end fundamental-thm-id-types ``` +We can now answer the original question. A type family `B : A → U` is equivalent +to the family of based paths at a point if and only if its total space is +contractible. + +```rzk +#def map-from-paths-inhabited-total + ( A : U) + ( B : A → U) + ( (a , b) : total-type A B) + ( x : A) + : (a = x) → B x + := ind-path A a ( \ y _ → B y) b x + +#def fundamental-theorem-of-identity-types + ( A : U) + ( B : A → U) + : iff + ( is-contr (total-type A B)) + ( Σ (a : A) , ((x : A) → Equiv (a = x) (B x))) + := + ( ( \ ((a , b) , h) → + ( a + , \ x → + ( map-from-paths-inhabited-total A B (a , b) x + , are-equiv-from-paths-is-contr-total A a B + ( map-from-paths-inhabited-total A B (a , b)) + ( (a , b) , h) + ( x)))) + , ( \ (a , familyequiv) → + is-contr-total-are-equiv-from-paths A a B + ( \ x → first (familyequiv x)) + ( \ x → second (familyequiv x)))) +``` + ## Maps over product types For later use, we specialize the previous results to the case of a family of @@ -646,23 +707,24 @@ types over a product type. #variable C' : A' → B' → U #variable f : A → A' #variable g : B → B' -#variable h : (a : A) → (b : B) → (c : C a b) → C' (f a) (g b) +#variable h : (a : A) → (b : B) → (C a b) → C' (f a) (g b) #def total-map-fibered-map-over-product - : (Σ (a : A) , (Σ (b : B) , C a b)) → (Σ (a' : A') , (Σ (b' : B') , C' a' b')) + : ( Σ (a : A) , (Σ (b : B) , C a b)) + → ( Σ (a' : A') , (Σ (b' : B') , C' a' b')) := \ (a , (b , c)) → (f a , (g b , h a b c)) #def pullback-is-equiv-base-is-equiv-total-is-equiv - ( is-equiv-total : - is-equiv + ( is-equiv-total + : is-equiv ( Σ (a : A) , (Σ (b : B) , C a b)) ( Σ (a' : A') , (Σ (b' : B') , C' a' b')) ( total-map-fibered-map-over-product)) ( is-equiv-f : is-equiv A A' f) : is-equiv - ( Σ (a : A) , (Σ (b : B) , C a b)) - ( Σ (a : A) , (Σ (b' : B') , C' (f a) b')) - ( \ (a , (b , c)) → (a , (g b , h a b c))) + ( Σ (a : A) , (Σ (b : B) , C a b)) + ( Σ (a : A) , (Σ (b' : B') , C' (f a) b')) + ( \ (a , (b , c)) → (a , (g b , h a b c))) := is-equiv-right-factor ( Σ (a : A) , (Σ (b : B) , C a b)) @@ -671,24 +733,24 @@ types over a product type. ( \ (a , (b , c)) → (a , (g b , h a b c))) ( \ (a , (b' , c')) → (f a , (b' , c'))) ( second - ( total-equiv-pullback-is-equiv + ( equiv-total-pullback-is-equiv ( A) (A') ( f) (is-equiv-f) ( \ a' → (Σ (b' : B') , C' a' b')))) ( is-equiv-total) #def pullback-is-equiv-bases-are-equiv-total-is-equiv - ( is-equiv-total : - is-equiv - ( Σ (a : A) , (Σ (b : B) , C a b)) - ( Σ (a' : A') , (Σ (b' : B') , C' a' b')) - ( total-map-fibered-map-over-product)) + ( is-equiv-total + : is-equiv + ( Σ (a : A) , (Σ (b : B) , C a b)) + ( Σ (a' : A') , (Σ (b' : B') , C' a' b')) + ( total-map-fibered-map-over-product)) ( is-equiv-f : is-equiv A A' f) ( is-equiv-g : is-equiv B B' g) : is-equiv - ( Σ (a : A) , (Σ (b : B) , C a b)) - ( Σ (a : A) , (Σ (b : B) , C' (f a) (g b))) - ( \ (a , (b , c)) → (a , (b , h a b c))) + ( Σ (a : A) , (Σ (b : B) , C a b)) + ( Σ (a : A) , (Σ (b : B) , C' (f a) (g b))) + ( \ (a , (b , c)) → (a , (b , h a b c))) := is-equiv-right-factor ( Σ (a : A) , (Σ (b : B) , C a b)) @@ -696,35 +758,35 @@ types over a product type. ( Σ (a : A) , (Σ (b' : B') , C' (f a) b')) ( \ (a , (b , c)) → (a , (b , h a b c))) ( \ (a , (b , c)) → (a , (g b , c))) - ( family-of-equiv-total-equiv A + ( is-equiv-total-is-equiv-fiberwise A ( \ a → (Σ (b : B) , C' (f a) (g b))) ( \ a → (Σ (b' : B') , C' (f a) b')) ( \ a (b , c) → (g b , c)) ( \ a → ( second - ( total-equiv-pullback-is-equiv + ( equiv-total-pullback-is-equiv ( B) (B') ( g) (is-equiv-g) ( \ b' → C' (f a) b'))))) ( pullback-is-equiv-base-is-equiv-total-is-equiv is-equiv-total is-equiv-f) #def fibered-map-is-equiv-bases-are-equiv-total-map-is-equiv - ( is-equiv-total : - is-equiv - ( Σ (a : A) , (Σ (b : B) , C a b)) - ( Σ (a' : A') , (Σ (b' : B') , C' a' b')) - ( total-map-fibered-map-over-product)) + ( is-equiv-total + : is-equiv + ( Σ (a : A) , (Σ (b : B) , C a b)) + ( Σ (a' : A') , (Σ (b' : B') , C' a' b')) + ( total-map-fibered-map-over-product)) ( is-equiv-f : is-equiv A A' f) ( is-equiv-g : is-equiv B B' g) ( a0 : A) ( b0 : B) : is-equiv (C a0 b0) (C' (f a0) (g b0)) (h a0 b0) := - total-equiv-family-of-equiv B + is-equiv-fiberwise-is-equiv-total B ( \ b → C a0 b) ( \ b → C' (f a0) (g b)) ( \ b c → h a0 b c) - ( total-equiv-family-of-equiv + ( is-equiv-fiberwise-is-equiv-total ( A) ( \ a → (Σ (b : B) , C a b)) ( \ a → (Σ (b : B) , C' (f a) (g b))) diff --git a/src/hott/09-propositions.rzk.md b/src/hott/09-propositions.rzk.md index dfca6345..781602ec 100644 --- a/src/hott/09-propositions.rzk.md +++ b/src/hott/09-propositions.rzk.md @@ -23,10 +23,15 @@ A type is a proposition when its identity types are contractible. (A : U) : U := (a : A) → (b : A) → is-contr (a = b) +``` + +For example, the type `Unit` is a proposition. In fact we will show below that +this is true for every contractible type. +```rzk #def is-prop-Unit : is-prop Unit - := \ x y → (path-types-of-Unit-are-contractible x y) + := \ x y → (is-contr-path-types-Unit x y) ``` ## Alternative characterizations: definitions @@ -77,7 +82,7 @@ A type is a proposition when its identity types are contractible. := \ x → ( is-emb-is-equiv A Unit (terminal-map A) - ( contr-implies-terminal-map-is-equiv A (c x))) + ( is-equiv-terminal-map-is-contr A (c x))) #def terminal-map-is-emb-is-contr-is-inhabited ( A : U) @@ -95,7 +100,7 @@ A type is a proposition when its identity types are contractible. \ x y → ( is-contr-equiv-is-contr' (x = y) (unit = unit) ( (ap A Unit x y (terminal-map A)) , (f x y)) - ( path-types-of-Unit-are-contractible unit unit)) + ( is-contr-path-types-Unit unit unit)) #def is-prop-is-contr-is-inhabited ( A : U) @@ -116,7 +121,6 @@ A type is a proposition when its identity types are contractible. ## Properties of propositions - If two propositions are logically equivalent, then they are equivalent: ```rzk @@ -183,8 +187,8 @@ All parallel paths in a proposition are equal. transport A B a x (first (is-prop-A a x)) b ``` -It is convenient to able to apply this to contractible types -without explicitly invoking `is-prop-is-contr`. +It is convenient to able to apply this to contractible types without explicitly +invoking `is-prop-is-contr`. ```rzk #def ind-prop-is-contr @@ -251,7 +255,6 @@ dependent functions `#!rzk (x : A) → B x` is a proposition. ( weakfunext A (\ x → f x = g x) (\ x → fiberwise-prop-B x (f x) (g x))) ``` - ### Sum types over a propositions We consider a type family `C : A → U` over a proposition `A`. @@ -280,8 +283,8 @@ If each `C a` is a proposition, then so is the total type `total-type A C`. ( c')))) ``` -Conversely, if the total type `total-type A C` is a proposition, -then so is every fiber `C a`. +Conversely, if the total type `total-type A C` is a proposition, then so is +every fiber `C a`. ```rzk #def is-fiberwise-prop-is-prop-total-type-is-prop-base uses (is-prop-A) diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md index 972814f4..3a2839af 100644 --- a/src/hott/11-homotopy-pullbacks.rzk.md +++ b/src/hott/11-homotopy-pullbacks.rzk.md @@ -8,8 +8,9 @@ This is a literate `rzk` file: ## Homotopy cartesian squares -We start by fixing the data of a map between two type families -`A' → U` and `A → U`, which we think of as a commutative square +We start by fixing the data of a map between two type families `A' → U` and +`A → U`, which we think of as a commutative square + ``` Σ A' → Σ A ↓ ↓ @@ -35,8 +36,8 @@ We start by fixing the data of a map between two type families := \ (a', c') → (α a', γ a' c') ``` -We say that such a square is homotopy cartesian -just if it induces an equivalence componentwise. +We say that such a square is homotopy cartesian just if it induces an +equivalence componentwise. ```rzk #def is-homotopy-cartesian uses (A) @@ -80,18 +81,13 @@ cartesian square, then so is the upper one `Σαγ : Σ C' → Σ C`. ( Σ (a' : A'), C (α a')) ( total-type A C) ( total-map A' C' (\ a' → C (α a')) γ) - ( family-of-equiv-total-equiv - ( A' ) - ( C' ) + ( is-equiv-total-is-equiv-fiberwise A' C' ( \ a' → C (α a') ) ( γ) ( \ a' → is-hc-α-γ a')) ( \ (a', c) → (α a', c) ) ( second - ( total-equiv-pullback-is-equiv - ( A') - ( A ) - ( α ) + ( equiv-total-pullback-is-equiv A' A α ( is-equiv-α ) ( C )))) ``` @@ -107,15 +103,15 @@ square is homotopy-cartesian. ) : is-homotopy-cartesian := - total-equiv-family-of-equiv - A' C' ( \ x → C (α x) ) γ -- use x instead of a' to avoid shadowing + is-equiv-fiberwise-is-equiv-total + A' C' ( \ x → C (α x) ) γ ( is-equiv-right-factor ( total-type A' C') ( Σ (x : A'), C (α x)) ( total-type A C) ( total-map A' C' (\ x → C (α x)) γ) ( \ (x, c) → (α x, c) ) - ( second ( total-equiv-pullback-is-equiv A' A α is-equiv-α C)) + ( second ( equiv-total-pullback-is-equiv A' A α is-equiv-α C)) ( is-equiv-homotopy ( total-type A' C') ( total-type A C ) @@ -216,8 +212,8 @@ always do this (whether the square is homotopy-cartesian or not). ### Invariance under pullbacks -We can pullback a homotopy cartesian square over `α : A' → A` -along any map of maps `β → α` and obtain another homotopy cartesian square. +We can pullback a homotopy cartesian square over `α : A' → A` along any map of +maps `β → α` and obtain another homotopy cartesian square. ```rzk #def is-homotopy-cartesian-pullback @@ -246,16 +242,15 @@ along any map of maps `β → α` and obtain another homotopy cartesian square. ## Pasting calculus for homotopy cartesian squares -Currently our notion of squares is not symmetric, -since the vertical maps are given by type families, -i.e. they are _display maps_, -while the horizontal maps are arbitrary. -Therefore we distinquish between the vertical and the horizontal pasting calculus. +Currently our notion of squares is not symmetric, since the vertical maps are +given by type families, i.e. they are _display maps_, while the horizontal maps +are arbitrary. Therefore we distinquish between the vertical and the horizontal +pasting calculus. ### Vertical calculus -The following vertical composition and cancellation laws follow easily from -the corresponding statements about equivalences established above. +The following vertical composition and cancellation laws follow easily from the +corresponding statements about equivalences established above. ```rzk #section homotopy-cartesian-vertical-calculus @@ -409,5 +404,216 @@ from composition and cancelling laws for equivalences. ( ihc (f' a'')) ( ihc'' a'') +``` + +We can cancel the left homotopy cartesian square if its lower map +`f' : A'' → A'` has a section. + +```rzk +#def is-homotopy-cartesian-left-cancel-with-lower-section + ( has-section-f' : has-section A'' A' f') + ( ihc' : is-homotopy-cartesian A'' C'' A' C' f' F') + ( ihc'' : is-homotopy-cartesian A'' C'' A C + ( comp A'' A' A f f') + ( \ a'' → + comp (C'' a'') (C' (f' a'')) (C (f (f' a''))) + (F (f' a'')) (F' a''))) + : is-homotopy-cartesian A' C' A C f F + := + ind-has-section A'' A' f' has-section-f' + ( \ a' → is-equiv (C' a') (C (f a')) (F a')) + ( \ a'' → + is-equiv-left-factor (C'' a'') (C' (f' a'')) (C (f (f' a''))) + ( F' a'') (ihc' a'') + ( F (f' a'')) ( ihc'' a'')) +``` + +In fact, it suffices to assume that the left square has horizontal sections. + +```rzk +#def is-homotopy-cartesian-left-cancel-with-section + ( has-section-f' : has-section A'' A' f') + ( has-sections-F' : (a'' : A'') → has-section (C'' a'') (C' (f' a'')) (F' a'')) + ( ihc'' : is-homotopy-cartesian A'' C'' A C + ( comp A'' A' A f f') + ( \ a'' → + comp (C'' a'') (C' (f' a'')) (C (f (f' a''))) + (F (f' a'')) (F' a''))) + : is-homotopy-cartesian A' C' A C f F + := + ind-has-section A'' A' f' has-section-f' + ( \ a' → is-equiv (C' a') (C (f a')) (F a')) + ( \ a'' → + is-equiv-left-cancel (C'' a'') (C' (f' a'')) (C (f (f' a''))) + ( F' a'') ( has-sections-F' a'') + ( F (f' a'')) ( ihc'' a'')) + #end homotopy-cartesian-horizontal-calculus ``` + +## Fiber products + +Given two type families `B C : A → U`, we can form their **fiberwise product**. + +```rzk +#def fiberwise-product + ( A : U) + ( B C : A → U) + : A → U + := + \ a → product (B a) (C a) + +#def first-fiberwise-product + ( A : U) + ( B C : A → U) + ( a : A) + : fiberwise-product A B C a → B a + := \ (b,_) → b + +#def second-fiberwise-product + ( A : U) + ( B C : A → U) + ( a : A) + : fiberwise-product A B C a → C a + := \ (_,c) → c +``` + +Given two maps `B → A` and `C → A`, we can form the **relative product** over +`A`. + +```rzk +#section relative-product + +#variable A : U +#variable B : U +#variable β : B → A +#variable C : U +#variable γ : C → A + +#def relative-product + : U + := Σ ( (b, c) : product B C) , (β b = γ c) + +#def first-relative-product uses (A B β C γ) + : relative-product → B + := \ ((b , _), _) → b + +#def second-relative-product uses (A B β C γ) + : relative-product → C + := \ ((_ , c), _) → c + +#def homotopy-relative-product uses (A B C) + ( (bc, p) : relative-product ) + : β (first-relative-product (bc,p)) = γ (second-relative-product (bc,p)) + := p +``` + +This relative product agrees with the fiber product obtained by summing over the +product of all fibers. + +```rzk +#def fiber-product + : U + := total-type A (fiberwise-product A (fib B A β) (fib C A γ)) + +#def unpack-fiber-product + : fiber-product + = ( Σ (a : A), (product (fib B A β a) (fib C A γ a))) + := refl + +#def first-fiber-product uses (A B β C γ) + : fiber-product → B + := \ (_, ((b, _), _ )) → b + +#def second-fiber-product uses (A B β C γ) + : fiber-product → C + := \ (_, (_, (c, _))) → c + +#def homotopy-fiber-product uses (A B C) + : ( abpcq : fiber-product ) + → β (first-fiber-product abpcq) = γ (second-fiber-product abpcq) + := + \ ( a, ((b, p), (c,q))) → + zig-zag-concat A (β b) a (γ c) p q + +#def relative-fiber-product uses (B C) + ( (a, ((b, p), (c,q))) : fiber-product ) + : relative-product + := ( ( b , c) , zig-zag-concat A (β b) a (γ c) p q) + +#def fiber-relative-product uses ( A B β C) + ( ((b,c), e) : relative-product) + : fiber-product + := ( γ c , ( (b , e) , (c , refl))) + +#def is-id-relative-fiber-relative-product + ( bce : relative-product) + : relative-fiber-product (fiber-relative-product bce) = bce + := refl + +#def is-id-fiber-relative-fiber-product + : ( abpcq : fiber-product) + → ( fiber-relative-product (relative-fiber-product abpcq)) = abpcq + := + \ (a', (bq', cq')) → + ind-fib C A γ + ( \ a cq → + ( ( bq : fib B A β a) + → ( fiber-relative-product (relative-fiber-product (a, (bq, cq))) + = ( a, (bq, cq))))) + ( \ c bq → refl) + ( a') + ( cq') + ( bq') + +#def is-equiv-relative-fiber-product uses (A B β C γ) + : is-equiv fiber-product relative-product relative-fiber-product + := + ( ( fiber-relative-product + , is-id-fiber-relative-fiber-product) + , ( fiber-relative-product + , is-id-relative-fiber-relative-product)) + +#def equiv-relative-product-fiber-product uses (A B β C γ) + : Equiv fiber-product relative-product + := + ( relative-fiber-product + , is-equiv-relative-fiber-product) + +#end relative-product +``` + +### Fiber product with singleton type + +The relative product of `f : B → A` with a map `Unit → A` corresponding to +`a : A` is nothing but the fiber `fib B A f a`. + +```rzk +#def compute-pullback-to-Unit + ( B A : U) + ( f : B → A) + ( a : A) + : Equiv (fib B A f a) (relative-product A B f Unit (\ unit → a)) + := + ( ( \ (b , p) → ((b , unit) , p)) + , ( ( ( ( \ ((b , unit) , p) → (b, p)) + , ( \ _ → refl)) + , ( ( \ ((b , unit) , p) → (b, p)) + , ( \ _ → refl))))) + +#def compute-map-pullback-to-Unit + ( B A : U) + ( f : B → A) + ( a : A) + : Equiv-of-maps + ( fib B A f a) (Unit) (\ _ → unit) + ( relative-product A B f Unit (\ unit → a)) + ( Unit) ( second-relative-product A B f Unit (\ unit → a)) + := + ( ( ( ( \ (b , p) → ((b , unit) , p)) + , ( identity Unit)) + , \ _ → refl) + , ( second (compute-pullback-to-Unit B A f a) + , is-equiv-identity Unit)) + +``` diff --git a/src/index.md b/src/index.md index 3a94a1bb..efbf6449 100644 --- a/src/index.md +++ b/src/index.md @@ -15,7 +15,7 @@ results from the following papers: - "[Limits and colimits of synthetic ∞-categories](https://arxiv.org/abs/2202.12386)" [^3] -This formalization project follows the philosophy layed out in the article +This formalization project follows the philosophy laid out in the article "[Could ∞-category theory be taught to undergraduates?](https://www.ams.org/journals/notices/202305/noti2692/noti2692.html)" [^4]. diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md index 51e75625..fbd71d2b 100644 --- a/src/simplicial-hott/03-extension-types.rzk.md +++ b/src/simplicial-hott/03-extension-types.rzk.md @@ -17,13 +17,12 @@ This is a literate `rzk` file: ## Extension up to homotopy -For a shape inclusion `ϕ ⊂ ψ` and any type `A`, -we have the inbuilt extension types `(t : ψ) → A [ϕ t ↦ σ t]` -(for every `σ : ϕ → A`). +For a shape inclusion `ϕ ⊂ ψ` and any type `A`, we have the inbuilt extension +types `(t : ψ) → A [ϕ t ↦ σ t]` (for every `σ : ϕ → A`). -We show that these extension types are equivalent to the fibers -of the canonical restriction map `(ψ → A) → (ϕ → A)`, -which we can view as the types of "extension up to homotopy". +We show that these extension types are equivalent to the fibers of the canonical +restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of +"extension up to homotopy". ```rzk #section extensions-up-to-homotopy @@ -49,7 +48,7 @@ which we can view as the types of "extension up to homotopy". := \ τ → ( τ, refl) -#def extension-type-weakening-section +#def section-extension-type-weakening' : ( σ : (t : ϕ) → A t) → ( th : homotopy-extension-type σ) → Σ (τ : extension-type σ), (( τ, refl) =_{homotopy-extension-type σ} th) @@ -64,17 +63,24 @@ which we can view as the types of "extension up to homotopy". ( σ : (t : ϕ) → A t) : (homotopy-extension-type σ) → (extension-type σ) := - \ th → first (extension-type-weakening-section σ th) + \ th → first (section-extension-type-weakening' σ th) + +#def has-section-extension-type-weakening + ( σ : (t : ϕ) → A t) + : has-section (extension-type σ) (homotopy-extension-type σ) + (extension-type-weakening-map σ) + := + ( extension-strictification σ + , \ th → ( second (section-extension-type-weakening' σ th))) + #def is-equiv-extension-type-weakening ( σ : (t : ϕ) → A t) : is-equiv (extension-type σ) (homotopy-extension-type σ) (extension-type-weakening-map σ) := - ( ( extension-strictification σ , - \ _ → refl), - ( extension-strictification σ, - \ th → ( second (extension-type-weakening-section σ th)))) + ( ( extension-strictification σ, \ _ → refl) + , has-section-extension-type-weakening σ) #def extension-type-weakening ( σ : (t : ϕ) → A t) @@ -114,10 +120,7 @@ This equivalence is functorial in the following sense: , \ _ → refl ) , ( is-equiv-extension-type-weakening I ψ ϕ A' σ' - , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t)) - ) - ) - + , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t)))) ``` ## Commutation of arguments and currying @@ -448,9 +451,10 @@ fact, sometimes only this weaker form of the axiom is needed. ( first (first (extext I ψ ϕ A a f g))) ``` -We show that naive extension extensionality implies weak extension extensionality. -On the way, we obtain another useful version of extension extensionality, -stating that all extension types in a proposition are propositions. +We show that naive extension extensionality implies weak extension +extensionality. On the way, we obtain another useful version of extension +extensionality, stating that all extension types in a proposition are +propositions. ```rzk #section weakextext-naiveextext @@ -488,8 +492,8 @@ stating that all extension types in a proposition are propositions. ( is-prop-shape-type-is-locally-prop I ψ A is-locally-prop-A)) ``` -Still using `naiveextext`, -in a fiberwise contractible family, every extension type is always inhabited. +Still using `naiveextext`, in a fiberwise contractible family, every extension +type is always inhabited. ```rzk #def is-inhabited-extension-type-is-locally-contr uses (naiveextext) @@ -511,8 +515,8 @@ in a fiberwise contractible family, every extension type is always inhabited. #end weakextext-naiveextext ``` -We conclude that naive extension extensionality implies -weak extension extensionality. +We conclude that naive extension extensionality implies weak extension +extensionality. ```rzk #def weakextext-naiveextext @@ -529,8 +533,8 @@ weak extension extensionality. ( is-locally-contr-A) ( a))) ``` -For convenience we also provide the composite implication -from extension extensionality to weak extension extensionality: +For convenience we also provide the composite implication from extension +extensionality to weak extension extensionality: ```rzk #def weakextext-extext @@ -676,7 +680,7 @@ extensionality. The following is statement the as proved in RS17. ( f = g) ( (t : ψ ) → (f t = g t) [ϕ t ↦ refl]) ( ext-htpy-eq I ψ ϕ A a f g) - := total-equiv-family-of-equiv + := is-equiv-fiberwise-is-equiv-total ( (t : ψ ) → A t [ϕ t ↦ a t] ) ( \ g → (f = g) ) ( \ g → (t : ψ ) → (f t = g t) [ϕ t ↦ refl]) @@ -700,6 +704,7 @@ We now assume extension extensionality and derive a few consequences. ```rzk #assume extext : ExtExt +#assume naiveextext : NaiveExtExt ``` In particular, extension extensionality implies that homotopies give rise to @@ -718,43 +723,7 @@ retraction to `#!rzk ext-htpy-eq`. := first (first (extext I ψ ϕ A a f g)) ``` -By extension extensionality, fiberwise equivalences of extension types define -equivalences of extension types. For simplicity, we extend from `#!rzk BOT`. - -```rzk -#def equiv-extension-equiv-family uses (extext) - ( I : CUBE) - ( ψ : I → TOPE) - ( A B : ψ → U) - ( famequiv : (t : ψ) → (Equiv (A t) (B t))) - : Equiv ((t : ψ) → A t) ((t : ψ) → B t) - := - ( ( \ a t → (first (famequiv t)) (a t)) , - ( ( ( \ b t → (first (first (second (famequiv t)))) (b t)) , - ( \ a → - eq-ext-htpy - ( I) - ( ψ) - ( \ t → BOT) - ( A) - ( \ u → recBOT) - ( \ t → - first (first (second (famequiv t))) (first (famequiv t) (a t))) - ( a) - ( \ t → second (first (second (famequiv t))) (a t)))) , - ( ( \ b t → first (second (second (famequiv t))) (b t)) , - ( \ b → - eq-ext-htpy - ( I) - ( ψ) - ( \ t → BOT) - ( B) - ( \ u → recBOT) - ( \ t → - first (famequiv t) (first (second (second (famequiv t))) (b t))) - ( b) - ( \ t → second (second (second (famequiv t))) (b t)))))) -``` +### Homotopy extension property We have a homotopy extension property. @@ -945,7 +914,7 @@ generality is needed. ( f : (t : ψ ) → A t [ϕ t ↦ a t]) (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t)) : (t : ψ ) → f t = (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t - := \ t → eq-is-contr + := \ t → all-elements-equal-is-contr ( A t) ( is-contr-fiberwise-A t) ( f t ) @@ -968,7 +937,7 @@ slightly more general statement. ( c : (t : ψ ) → (f t = a' t)) : (t : ϕ ) → (refl =_{f t = a' t} c t) := \ t → - all-paths-eq-is-contr + all-paths-equal-is-contr ( A t) ( is-fiberwise-contr t) ( f t) @@ -1057,3 +1026,314 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r ( a) ( f)))) ``` + +### Pointwise homotopy extension types + +Using `ExtExt` we can write the homotopy in the homotopy extension type +pointwise. + +```rzk +#section pointwise-homotopy-extension-type + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variable A : ψ → U + +#def pointwise-homotopy-extension-type + ( σ : (t : ϕ) → A t) + : U + := + Σ ( τ : (t : ψ) → A t) , ( (t : ϕ) → (τ t =_{ A t} σ t)) + +#def equiv-pointwise-homotopy-extension-type uses (extext) + ( σ : (t : ϕ) → A t) + : Equiv + ( homotopy-extension-type I ψ ϕ A σ) + ( pointwise-homotopy-extension-type σ) + := + total-equiv-family-of-equiv + ( (t : ψ) → A t) + ( \ τ → (\ t → τ t) =_{ (t : ϕ) → A t} σ) + ( \ τ → (t : ϕ) → (τ t = σ t)) + ( \ τ → + equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t) + ( \ _ → recBOT) (\ t → τ t) σ) + +#def extension-type-pointwise-weakening uses (extext) + ( σ : (t : ϕ) → A t) + : Equiv + ( extension-type I ψ ϕ A σ) + ( pointwise-homotopy-extension-type σ) + := equiv-comp + ( extension-type I ψ ϕ A σ) + ( homotopy-extension-type I ψ ϕ A σ) + ( pointwise-homotopy-extension-type σ) + ( extension-type-weakening I ψ ϕ A σ) + ( equiv-pointwise-homotopy-extension-type σ) + + +#end pointwise-homotopy-extension-type +``` + +## Relative extension types + +Given a map `α : A' → A`, there is also a notion of relative extension types. + +```rzk +#section relative-extension-types + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : ψ → U +#variable α : (t : ψ) → A' t → A t +#variable σ' : (t : ϕ) → A' t +#variable τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)] + +#def relative-extension-type + : U + := + Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) + , ( ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]) + +#def relative-extension-type' + : U + := + fib + ( (t : ψ) → A' t [ϕ t ↦ σ' t]) + ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) + ( \ τ' t → α t (τ' t)) + ( τ) + +#def equiv-relative-extension-type-fib uses (extext) + : Equiv + ( relative-extension-type') + ( relative-extension-type) + := + total-equiv-family-of-equiv + ( (t : ψ) → A' t [ϕ t ↦ σ' t]) + ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ) + ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]) + ( \ τ' → + equiv-ExtExt extext I ψ ϕ A (\ t → α t (σ' t)) + ( \ t → α t (τ' t)) ( τ)) +#end relative-extension-types +``` + +### Generalized relative extension types + +We will also need to allow more general relative extension types, where we start +with a `τ : ψ → A` that does not strictly restrict to `\ t → α (σ' t)`. + +```rzk +#section general-extension-types + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : ψ → U +#variable α : (t : ψ) → A' t → A t + +#def general-relative-extension-type + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t) + ( h : (t : ϕ) → α t (σ' t) = τ t) + : U + := + Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) + , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t] +``` + +If all ordinary relative extension types are contractible, then all generalized +extension types are also contractible. + +```rzk +#def has-contr-relative-extension-types + : U + := + ( ( σ' : (t : ϕ) → A' t) + → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) + → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ))) + +#def has-contr-general-relative-extension-types + : U + := + ( ( σ' : (t : ϕ) → A' t) + → ( τ : (t : ψ) → A t) + → ( h : (t : ϕ) → α t (σ' t) = τ t) + → ( is-contr ( general-relative-extension-type σ' τ h))) + +#def has-contr-relative-extension-types-generalize' uses (extext) + ( has-contr-relext-α : has-contr-relative-extension-types) + ( σ' : (t : ϕ) → A' t) + ( τ : (t : ψ) → A t) + ( h : (t : ϕ) → α t (σ' t) = τ t) + : is-contr + ( general-relative-extension-type σ' τ + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t)))) + := + ind-has-section-equiv + ( extension-type I ψ ϕ A (\ t → α t (σ' t))) + ( pointwise-homotopy-extension-type I ψ ϕ A (\ t → α t (σ' t))) + ( extension-type-pointwise-weakening I ψ ϕ A (\ t → α t (σ' t))) + ( \ (τ̂ , ĥ) → + is-contr + ( general-relative-extension-type σ' τ̂ + ( \ t → rev (A t) (τ̂ t) (α t (σ' t)) (ĥ t)))) + ( \ τ → has-contr-relext-α σ' τ) + ( τ , \ t → (rev (A t) (α t (σ' t)) (τ t) (h t))) + +#def has-contr-relative-extension-types-generalize uses (extext) + ( has-contr-relext-α : has-contr-relative-extension-types) + : has-contr-general-relative-extension-types + := + \ σ' τ h → + transport + ( (t : ϕ) → α t (σ' t) = τ t) + ( \ ĥ → is-contr ( general-relative-extension-type σ' τ ĥ)) + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))) + ( h) + ( naiveextext-extext extext + ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → α t (σ' t ) = τ t) (\ _ → recBOT) + ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))) + ( h) + ( \ t → rev-rev (A t) (α t (σ' t)) (τ t) (h t))) + ( has-contr-relative-extension-types-generalize' + has-contr-relext-α σ' τ h) +``` + +The converse is of course trivial. + +```rzk +#def has-contr-relative-extension-types-specialize + ( has-contr-gen-relext-α : has-contr-general-relative-extension-types) + : has-contr-relative-extension-types + := + \ σ' τ → has-contr-gen-relext-α σ' τ (\ _ → refl) + +#end general-extension-types +``` + +## Functoriality of extension types + +For simplicity, we only consider extesions of `#!rzk BOT`. + +For each map `f : A → B` and each shape inclusion `ϕ ⊂ ψ`, we have a commutative +square. + +``` +(ψ → A') → (ψ → A) + + ↓ ↓ + +(ϕ → A') → (ϕ → A) +``` + +We can view it as a map of maps either vertically or horizontally. + +```rzk +#def map-of-restriction-maps + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( f : (t : ψ) → A t → B t) + : map-of-maps + ( (t : ψ) → A t) ( (t : ϕ) → A t) (\ a t → a t) + ( (t : ψ) → B t) ( (t : ϕ) → B t) (\ b t → b t) + := + ( ( ( \ a t → f t (a t)) + , ( \ a t → f t (a t))) + , \ _ → refl) + +#def map-of-map-extension-type + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( f : (t : ψ) → A t → B t) + : map-of-maps + ( (t : ψ) → A t) ( (t : ψ) → B t) (\ a t → f t (a t)) + ( (t : ϕ) → A t) ( (t : ϕ) → B t) (\ a t → f t (a t)) + := + ( ( ( \ a t → a t) + , ( \ b t → b t)) + , \ _ → refl) +``` + +It follows from extension extensionality that if `f : A → B` is an equivalence, +then so is the map of maps `map-of-restriction-maps`. + +```rzk +#def is-equiv-extension-is-equiv-family uses (extext) + ( I : CUBE) + ( ψ : I → TOPE) + ( A B : ψ → U) + ( f : (t : ψ) → (A t) → (B t)) + ( is-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t)) + : is-equiv ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t)) + := ( ( ( \ b t → (first (first (is-equiv-f t))) (b t)) + , ( \ a → + eq-ext-htpy I ψ ( \ t → BOT) + ( A) + ( \ u → recBOT) + ( \ t → first (first (is-equiv-f t)) (f t (a t))) + ( a) + ( \ t → second (first (is-equiv-f t)) (a t)))) + , ( ( \ b t → first (second (is-equiv-f t)) (b t)) + , ( \ b → + eq-ext-htpy I ψ ( \ t → BOT) + ( B) + ( \ u → recBOT) + ( \ t → f t (first (second (is-equiv-f t)) (b t))) + ( b) + ( \ t → second (second (is-equiv-f t)) (b t))))) + +#def equiv-extension-equiv-family uses (extext) + ( I : CUBE) + ( ψ : I → TOPE) + ( A B : ψ → U) + ( famequiv : (t : ψ) → (Equiv (A t) (B t))) + : Equiv ((t : ψ) → A t) ((t : ψ) → B t) + := + ( ( \ a t → first ( famequiv t) (a t)) + , is-equiv-extension-is-equiv-family I ψ A B + ( \ t → first (famequiv t)) + ( \ t → second (famequiv t))) + +#def equiv-of-restriction-maps-equiv-family uses (extext) + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A B : ψ → U) + ( famequiv : (t : ψ) → (Equiv (A t) (B t))) + : Equiv-of-maps + ( (t : ψ) → A t) ( (t : ϕ) → A t) (\ a t → a t) + ( (t : ψ) → B t) ( (t : ϕ) → B t) (\ b t → b t) + := + ( map-of-restriction-maps I ψ ϕ A B (\ t → first (famequiv t)) + , ( second (equiv-extension-equiv-family I ψ A B famequiv) + , second ( equiv-extension-equiv-family I + (\ t → ϕ t) (\ t → A t) (\ t → B t) (\ t → famequiv t)))) +``` + +Similarly, a fiberwise section of a map `(t : ψ) → A t → B t` induces a section +on extension types. + +```rzk +#def has-section-extension-has-section-family uses (naiveextext) + ( I : CUBE) + ( ψ : I → TOPE) + ( A B : ψ → U) + ( f : ( t : ψ) → A t → B t) + ( has-fiberwise-section-f : (t : ψ) → has-section (A t ) (B t) (f t)) + : has-section ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t)) + := + ( ( \ b t → first (has-fiberwise-section-f t) (b t)) + , \ b → + ( naiveextext I ψ (\ _ → BOT) B (\ _ → recBOT) + ( \ t → f t (first (has-fiberwise-section-f t) (b t))) + ( \ t → b t) + ( \ t → second (has-fiberwise-section-f t) (b t)))) +``` diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md index 802fb1a4..12154ce0 100644 --- a/src/simplicial-hott/04-right-orthogonal.rzk.md +++ b/src/simplicial-hott/04-right-orthogonal.rzk.md @@ -8,21 +8,25 @@ This is a literate `rzk` file: ## Prerequisites -Some of the definitions in this file rely on naive extension extensionality: +Some of the definitions in this file rely on extension extensionality or +function extensionality: ```rzk #assume naiveextext : NaiveExtExt +#assume extext : ExtExt +#assume funext : FunExt +#assume weakextext : WeakExtExt ``` ## Right orthogonal maps with respect to shapes -For every shape inclusion `ϕ ⊂ ψ`, -we obtain a fibrancy condition for a map `α : A' → A` -in terms of unique extension along `ϕ ⊂ ψ`. -This is a relative version of unique extension along `ϕ ⊂ ψ`. +For every shape inclusion `ϕ ⊂ ψ`, we obtain a fibrancy condition for a map +`α : A' → A` in terms of unique extension along `ϕ ⊂ ψ`. This is a relative +version of unique extension along `ϕ ⊂ ψ`. -We say that `α : A' → A` is _right orthogonal_ to the shape inclusion `ϕ ⊂ ψ`, +We say that `α : A' → A` is **right orthogonal** to the shape inclusion `ϕ ⊂ ψ`, if the square + ``` (ψ → A') → (ψ → A) @@ -30,17 +34,17 @@ if the square (ϕ → A') → (ϕ → A) ``` + is homotopy cartesian. -Equivalently, we can interpret this orthogonality -as a cofibrancy condition on the shape inclusion. -We say that the shape inclusion `ϕ ⊂ ψ` is _left orthogonal_ to the map `α`, -if `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`. +Equivalently, we can interpret this orthogonality as a cofibrancy condition on +the shape inclusion. We say that the shape inclusion `ϕ ⊂ ψ` is **left +orthogonal** to the map `α`, if `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`. ```rzk title="BW23, Section 3" #def is-right-orthogonal-to-shape ( I : CUBE) - ( ψ : I → TOPE ) + ( ψ : I → TOPE) ( ϕ : ψ → TOPE) ( A' A : U) ( α : A' → A) @@ -52,6 +56,80 @@ if `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`. ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) ) ``` +## Contractible relative extension types + +Using `ExtExt`, we can characterize right orthogonal maps in terms of the +contractibility of relative extension types or, equivalently, generalized +extension types. + +```rzk +#section has-contr-relative-extension-types-iff-is-right-orthogonal + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : U +#variable α : A' → A + +#def is-right-orthogonal-to-shape-has-contr-relative-extension-types uses (extext) + ( are-contr-relext-α + : has-contr-relative-extension-types I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α)) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + \ σ' → + is-equiv-is-contr-map + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( \ τ → + is-contr-equiv-is-contr' + ( fib + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( τ)) + ( relative-extension-type I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( equiv-relative-extension-type-fib extext I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( are-contr-relext-α σ' τ)) + +#def has-contr-relative-extension-types-is-right-orthogonal-to-shape uses (extext) + ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : has-contr-relative-extension-types I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + := + \ σ' τ → + is-contr-equiv-is-contr + ( fib + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( τ)) + ( relative-extension-type I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( equiv-relative-extension-type-fib extext I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ) + ( is-contr-map-is-equiv + ( (t : ψ) → A' [ϕ t ↦ σ' t]) + ( (t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t)) + ( is-orth-α σ') + ( τ)) + +#def has-contr-general-relative-extension-types-is-right-orthogonal-to-shape + uses (extext) + ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : has-contr-general-relative-extension-types I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) + := + has-contr-relative-extension-types-generalize extext I ψ ϕ + ( \ _ → A') (\ _ → A) (\ _ → α) + ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α) + +#end has-contr-relative-extension-types-iff-is-right-orthogonal +``` + ## Stability properties of left orthogonal shape inclusions We fix a map `α : A' → A`. @@ -62,8 +140,9 @@ We fix a map `α : A' → A`. #variables A' A : U #variable α : A' → A ``` -Consider nested shapes `ϕ ⊂ χ ⊂ ψ` -and the three possible right orthogonality conditions. + +Consider nested shapes `ϕ ⊂ χ ⊂ ψ` and the three possible right orthogonality +conditions. ```rzk #variable I : CUBE @@ -74,22 +153,20 @@ and the three possible right orthogonality conditions. #variable is-orth-χ-ϕ : is-right-orthogonal-to-shape I ( \ t → χ t) ( \ t → ϕ t) A' A α #variable is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α - -- rzk does not accept these terms after η-reduction ``` -Using the vertical pasting calculus for homotopy cartesian squares, -it is not hard to deduce the corresponding composition and cancellation properties -for left orthogonality of shape inclusion with respect to `α : A' → A`. +Using the vertical pasting calculus for homotopy cartesian squares, it is not +hard to deduce the corresponding composition and cancellation properties for +left orthogonality of shape inclusion with respect to `α : A' → A`. ### Σ over an intermediate shape -The only fact that stops some of these laws from being a direct corollary -is that the `Σ`-types appearing in the vertical pasting of the relevant squares -(such as `Σ (\ σ : ϕ → A), ( (t : χ) → A [ϕ t ↦ σ t])`) -are not literally equal to the corresponding extension types -(such as `τ → A `). -Therefore we have to occasionally go back or forth along the -functorial equivalence `cofibration-composition-functorial`. +The only fact that stops some of these laws from being a direct corollary is +that the `Σ`-types appearing in the vertical pasting of the relevant squares +(such as `Σ (\ σ : ϕ → A), ( (t : χ) → A [ϕ t ↦ σ t])`) are not literally equal +to the corresponding extension types (such as `τ → A `). Therefore we have to +occasionally go back or forth along the functorial equivalence +`cofibration-composition-functorial`. ```rzk #def is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape uses (is-orth-ψ-ϕ) @@ -106,10 +183,10 @@ functorial equivalence `cofibration-composition-functorial`. ( ( t : ψ) → A' [ϕ t ↦ σ' t]) ( ( t : ψ) → A [ϕ t ↦ α (σ' t)]) ( \ υ' t → α ( υ' t)) - ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]), - ( ( t : ψ) → A' [χ t ↦ τ' t])) - ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]), - ( ( t : ψ) → A [χ t ↦ τ t])) + ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]) + , ( ( t : ψ) → A' [χ t ↦ τ' t])) + ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]) + , ( ( t : ψ) → A [χ t ↦ τ t])) ( \ (τ', υ') → ( \ t → α (τ' t), \t → α (υ' t))) ( cofibration-composition-functorial I ψ χ ϕ ( \ _ → A') ( \ _ → A) ( \ _ → α) σ') @@ -130,10 +207,10 @@ Left orthogonal shape inclusions are preserved under composition. ( ( t : ψ) → A' [ϕ t ↦ σ' t]) ( ( t : ψ) → A [ϕ t ↦ α (σ' t)]) ( \ υ' t → α ( υ' t)) - ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]), - ( ( t : ψ) → A' [χ t ↦ τ' t])) - ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]), - ( ( t : ψ) → A [χ t ↦ τ t])) + ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]) + , ( ( t : ψ) → A' [χ t ↦ τ' t])) + ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]) + , ( ( t : ψ) → A [χ t ↦ τ t])) ( \ (τ', υ') → ( \ t → α (τ' t), \t → α (υ' t))) ( cofibration-composition-functorial I ψ χ ϕ ( \ _ → A') ( \ _ → A) ( \ _ → α) σ') @@ -174,12 +251,11 @@ If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so i ( is-orth-χ-ϕ ) (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape) ( \ ( t : ϕ) → τ' t) - τ' + ( τ') ``` -If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` -and `χ ⊂ ψ` is a (functorial) shape retract, -then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`. +If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` and `χ ⊂ ψ` is a (functorial) +shape retract, then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`. ```rzk #def is-right-orthogonal-to-shape-right-cancel-retract uses (is-orth-ψ-ϕ) @@ -197,18 +273,18 @@ then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`. ( \ _ τ' x → α (τ' x) ) ( \ _ _ υ' x → α (υ' x) ) ( relativize-is-functorial-shape-retract I ψ χ is-fretract-ψ-χ ϕ A' A α) - (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape) + ( is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape) #end left-orthogonal-calculus-1 ``` ### Stability under exponentiation -If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` -then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`. +If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` then so is `χ × ϕ ⊂ χ × ψ` for +every other shape `χ`. -The following proof uses a lot of currying and uncurrying -and relies on (the naive form of) extension extensionality. +The following proof uses a lot of currying and uncurrying and relies on (the +naive form of) extension extensionality. ```rzk #def is-right-orthogonal-to-shape-× uses (naiveextext) @@ -225,12 +301,10 @@ and relies on (the naive form of) extension extensionality. ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) A' A α := \ ( σ' : ( (t,s) : J × I | χ t ∧ ϕ s) → A') → - ( - ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))]) + ( ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))]) ( t, s) → ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s - , - \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) → + , \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) → naiveextext ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) ( \ _ → A') @@ -246,15 +320,11 @@ and relies on (the naive form of) extension extensionality. ( \ s' → τ' (t, s') ) ( ( second (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ' (t, s'))) - ( s) - ) - ) - , - ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) + ( s))) + , ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) ( t, s) → ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s - , - \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) → + , \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) → naiveextext ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) ( \ _ → A) @@ -268,20 +338,17 @@ and relies on (the naive form of) extension extensionality. ( \ s'' → α ( ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) - (s''))) + ( s''))) ( \ s' → τ (t, s') ) ( ( second ( second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s'))) - ( s) - ) - ) - ) + ( s)))) ``` ### Stability under exact pushouts -For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to `α : A' → A`, -then so is `ψ ⊂ ϕ ∪ ψ`. +For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to +`α : A' → A`, then so is `ψ ⊂ ϕ ∪ ψ`. ```rzk #def is-right-orthogonal-to-shape-pushout @@ -303,79 +370,396 @@ then so is `ψ ⊂ ϕ ∪ ψ`. ( is-orth-ϕ-ψ∧ϕ ( \ t → τ' t)) ``` -## Types with unique extension +## Stability properties of right orthogonal maps -We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`, -if for each `σ : ϕ → A` the type of `ψ`-extensions is contractible. +Now we change perspective. We fix a shape inclusion `ϕ ⊂ ψ` and investigate +stability properties of maps right orthogonal to it. ```rzk -#def has-unique-extensions - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) - ( A : U) - : U - := - ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t]) +#section right-orthogonal-calculus +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE ``` -The property of having unique extension -can be pulled back along any right orthogonal map. +### Equivalences are right orthogonal + +Every equivalence `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`. ```rzk -#def has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) +#def is-right-orthogonal-is-equiv-to-shape uses (extext) ( A' A : U) ( α : A' → A) + ( is-equiv-α : is-equiv A' A α) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + is-homotopy-cartesian-is-horizontal-equiv + ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t]) + ( ϕ → A) (\ σ → (t : ψ) → A [ϕ t ↦ σ t]) + ( \ σ' t → α (σ' t)) + ( \ _ τ' t → α (τ' t)) + ( second + ( equiv-extension-equiv-family extext I ( \ t → ϕ t) + ( \ _ → A') ( \ _ → A) ( \ _ → (α , is-equiv-α)))) + ( is-equiv-Equiv-is-equiv' + ( ψ → A') ( ψ → A) ( \ τ' t → α (τ' t)) + ( Σ (σ' : ϕ → A') , (t : ψ) → A' [ϕ t ↦ σ' t]) + ( Σ (σ : ϕ → A) , (t : ψ) → A [ϕ t ↦ σ t]) + ( \ (σ' , τ') → ( \ t → α (σ' t) , \ t → α (τ' t))) + ( cofibration-composition-functorial I ψ ϕ ( \ _ → BOT) + ( \ _ → A') ( \ _ → A) ( \ _ → α) ( \ _ → recBOT)) + ( second + ( equiv-extension-equiv-family extext I ( \ t → ψ t) + ( \ _ → A') ( \ _ → A) ( \ _ → (α , is-equiv-α))))) +``` + +Right orthogonality is closed under homotopy. + +```rzk +#def is-right-orthogonal-homotopy-to-shape uses (funext) + ( A' A : U) + ( α β : A' → A) + ( h : homotopy A' A α β) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + → is-right-orthogonal-to-shape I ψ ϕ A' A β + := + transport (A' → A) ( is-right-orthogonal-to-shape I ψ ϕ A' A) α β + ( first (first (funext A' (\ _ → A) α β)) h) +``` + +### Stability under composition + +```rzk +#variables A'' A' A : U +#variable α' : A'' → A' +#variable α : A' → A + +#variable is-orth-ψ-ϕ-α' : is-right-orthogonal-to-shape I ψ ϕ A'' A' α' +#variable is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α +#variable is-orth-ψ-ϕ-αα' : is-right-orthogonal-to-shape I ψ ϕ A'' A + ( comp A'' A' A α α') + +#def is-right-orthogonal-comp-to-shape + uses (is-orth-ψ-ϕ-α' is-orth-ψ-ϕ-α) + : is-right-orthogonal-to-shape I ψ ϕ A'' A (comp A'' A' A α α') + := + \ σ'' → + is-equiv-comp + ( extension-type I ψ ϕ (\ _ → A'') σ'') + ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t))) + ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t)))) + ( \ τ'' t → α' (τ'' t)) + ( is-orth-ψ-ϕ-α' σ'') + ( \ τ' t → α (τ' t)) + ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t))) +``` + +### Right cancellation + +```rzk +#def is-right-orthogonal-right-cancel-to-shape + uses (is-orth-ψ-ϕ-α is-orth-ψ-ϕ-αα') + : is-right-orthogonal-to-shape I ψ ϕ A'' A' α' + := + \ σ'' → + is-equiv-right-factor + ( extension-type I ψ ϕ (\ _ → A'') σ'') + ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t))) + ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t)))) + ( \ τ'' t → α' (τ'' t)) + ( \ τ' t → α (τ' t)) + ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t))) + ( is-orth-ψ-ϕ-αα' σ'') +``` + +### Left cancellation with section (weak version) + +This should hold even without assuming `is-orth-ψ-ϕ-α'`. + +```rzk +#def is-right-orthogonal-weak-left-cancel-with-section-to-shape + uses (naiveextext is-orth-ψ-ϕ-α' is-orth-ψ-ϕ-αα') + ( has-section-α' : has-section A'' A' α') + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + is-homotopy-cartesian-left-cancel-with-lower-section + ( ϕ → A'' ) ( \ σ'' → (t : ψ) → A'' [ϕ t ↦ σ'' t]) + ( ϕ → A' ) ( \ σ' → (t : ψ) → A' [ϕ t ↦ σ' t]) + ( ϕ → A ) ( \ σ → (t : ψ) → A [ϕ t ↦ σ t]) + ( \ σ'' t → α' (σ'' t)) ( \ _ τ'' x → α' (τ'' x) ) + ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) ) + ( has-section-extension-has-section-family naiveextext I (\ t → ϕ t) + ( \ _ → A'') (\ _ → A') (\ _ → α') + ( \ _ → has-section-α')) + ( is-orth-ψ-ϕ-α') + ( is-orth-ψ-ϕ-αα') +``` + +### Stability under pullback + +Right orthogonal maps are stable under pullback. More precisely: If `α : A' → A` +is right orthogonal, then so is the second projection +`relative-product A A' α B f → B` for every `f : B → A`. + +To prove this, we first show that each relative extension type of +`relative-product A A' α B f → B`, is a retract of a generalized extension type +for `A' → A`. Since the latter are all contractible by assumption, the same +follows for the former. + +```rzk +#variable B : U +#variable f : B → A + +#def relative-extension-type-pullback-general-relative-extension-type + ( σB' : ϕ → relative-product A A' α B f) + ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) + ( (τA', hA) + : general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t))) + : relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB) + := + ( \ t → ( (τA' t, τB t) , hA t) + , \ t → refl) + +#def general-relative-extension-type-relative-extension-type-pullback + ( σB' : ϕ → relative-product A A' α B f) + ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) + ( (τB', hB) + : relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + : general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t)) + := + ( \ t → first-relative-product A A' α B f (τB' t) + , \ t → + concat A + ( α (first-relative-product A A' α B f (τB' t))) + ( f (second-relative-product A A' α B f (τB' t))) + ( f (τB t)) + ( homotopy-relative-product A A' α B f (τB' t)) + ( ap B A + ( second-relative-product A A' α B f (τB' t)) + ( τB t) + ( f) ( hB t))) + +#def is-id-rel-ext-type-pb-gen-rel-ext-type-rel-ext-type-pb uses (extext) + ( σB' : ϕ → relative-product A A' α B f) + ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) + : ( τhB + : relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + → ( relative-extension-type-pullback-general-relative-extension-type σB' τB + ( general-relative-extension-type-relative-extension-type-pullback σB' τB τhB) + = τhB) + := + ind-has-section-equiv + ( relative-extension-type' I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( equiv-relative-extension-type-fib extext I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( \ τhB → + ( relative-extension-type-pullback-general-relative-extension-type σB' τB + ( general-relative-extension-type-relative-extension-type-pullback σB' τB τhB) + = τhB)) + ( ind-fib + ( (t : ψ) → relative-product A A' α B f [ϕ t ↦ σB' t]) + ( (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) + ( \ τB' t → second-relative-product A A' α B f (τB' t)) + ( \ τB₁ (τB'₁, h₁) → + ( relative-extension-type-pullback-general-relative-extension-type σB' τB₁ + ( general-relative-extension-type-relative-extension-type-pullback σB' τB₁ + ( τB'₁ + , ext-htpy-eq I ψ ϕ (\ _ → B) + ( \ t → second-relative-product A A' α B f (σB' t)) + ( \ t → second-relative-product A A' α B f (τB'₁ t)) + ( τB₁) ( h₁))) + = ( τB'₁ + , ext-htpy-eq I ψ ϕ (\ _ → B) + ( \ t → second-relative-product A A' α B f (σB' t)) + ( \ t → second-relative-product A A' α B f (τB'₁ t)) + ( τB₁) ( h₁)))) + ( \ τB' → refl) + ( τB)) + +#def is-retract-of-rel-ext-type-pb-gen-rel-ext-type uses (extext) + ( σB' : ϕ → relative-product A A' α B f) + ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)]) + : is-retract-of + ( relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t))) + := + ( general-relative-extension-type-relative-extension-type-pullback σB' τB + , ( relative-extension-type-pullback-general-relative-extension-type σB' τB + , is-id-rel-ext-type-pb-gen-rel-ext-type-rel-ext-type-pb σB' τB)) +``` + +Then we can deduce that right orthogonal maps are preserved under pullback: + +```rzk +#def is-right-orthogonal-pullback-to-shape uses (extext is-orth-ψ-ϕ-α B f) + : is-right-orthogonal-to-shape I ψ ϕ + ( relative-product A A' α B f) ( B) + ( second-relative-product A A' α B f) + := + is-right-orthogonal-to-shape-has-contr-relative-extension-types I ψ ϕ + ( relative-product A A' α B f) ( B) + ( second-relative-product A A' α B f) + ( \ σB' τB → + is-contr-is-retract-of-is-contr + ( relative-extension-type I ψ ϕ + ( \ _ → relative-product A A' α B f) ( \ _ → B) + ( \ _ → second-relative-product A A' α B f) + ( σB') ( τB)) + ( general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α) + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t))) + ( is-retract-of-rel-ext-type-pb-gen-rel-ext-type σB' τB) + ( has-contr-general-relative-extension-types-is-right-orthogonal-to-shape + I ψ ϕ A' A α + ( is-orth-ψ-ϕ-α) + ( \ t → first-relative-product A A' α B f (σB' t)) + ( \ t → f (τB t)) + ( \ t → homotopy-relative-product A A' α B f (σB' t)))) + +#end right-orthogonal-calculus +``` + +### Right orthogonal maps are closed under equivalence + +If two maps `α : A' → A` and `β : B' → B` are equivalent, then if one is right +orthogonal to `ϕ ⊂ ψ`, then so is the other. + +```rzk +#section is-right-orthogonal-equiv-to-shape + +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variables A' A : U +#variable α : A' → A +#variables B' B : U +#variable β : B' → B + +#def is-right-orthogonal-equiv-to-shape uses (funext extext) + ( (((s', s), η), (is-equiv-s', is-equiv-s)) : Equiv-of-maps A' A α B' B β) + ( is-orth-ψ-ϕ-β : is-right-orthogonal-to-shape I ψ ϕ B' B β) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + is-right-orthogonal-right-cancel-to-shape I ψ ϕ A' A B α s + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A B s is-equiv-s) + ( is-right-orthogonal-homotopy-to-shape I ψ ϕ A' B + ( \ a' → β (s' a')) ( \ a' → s (α a')) ( η) + ( is-right-orthogonal-comp-to-shape I ψ ϕ A' B' B s' β + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A' B' s' is-equiv-s') + ( is-orth-ψ-ϕ-β))) + +#def is-right-orthogonal-equiv-to-shape' + uses (funext extext naiveextext) + ( (((s', s), η), (is-equiv-s', is-equiv-s)) : Equiv-of-maps A' A α B' B β) ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) - : has-unique-extensions I ψ ϕ A → has-unique-extensions I ψ ϕ A' + : is-right-orthogonal-to-shape I ψ ϕ B' B β := - \ has-ue-A ( σ' : ϕ → A') → - is-contr-equiv-is-contr' - ( ( t : ψ) → A' [ϕ t ↦ σ' t]) - ( ( t : ψ) → A [ϕ t ↦ α (σ' t)]) - ( \ τ' t → α (τ' t) , is-orth-ψ-ϕ-α σ') - ( has-ue-A (\ t → α (σ' t))) + is-right-orthogonal-weak-left-cancel-with-section-to-shape + I ψ ϕ A' B' B s' β + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A' B' s' is-equiv-s') + ( is-right-orthogonal-homotopy-to-shape I ψ ϕ A' B + ( \ a' → s (α a')) ( \ a' → β (s' a')) + ( rev-homotopy A' B ( \ a' → β (s' a')) ( \ a' → s (α a')) ( η)) + ( is-right-orthogonal-comp-to-shape I ψ ϕ A' A B α s + ( is-orth-ψ-ϕ-α) + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A B s is-equiv-s))) + ( second is-equiv-s') + +#end is-right-orthogonal-equiv-to-shape ``` -Alternatively, we can ask that the canonical restriction map `(ψ → A) → (ϕ → A)` -is an equivalence. +## Types with unique extension + +We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`, if +for each `σ : ϕ → A` the type of `ψ`-extensions is contractible. ```rzk -#section is-local-type +#section has-unique-extensions #variable I : CUBE #variable ψ : I → TOPE #variable ϕ : ψ → TOPE #variable A : U +#def has-unique-extensions + : U + := ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t]) +``` + +There are other equivalent characterizations which we shall prove below: + +We can ask that the canonical restriction map `(ψ → A) → (ϕ → A)` is an +equivalence. + +```rzk #def is-local-type : U := is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t) ``` -This follows straightforwardly from the fact that for every `σ : ϕ → A` -we have an equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]` -and the fiber of the restriction map `(ψ → A) → (ϕ → A)`. +We can ask that the terminal map `A → Unit` is right orthogonal to `ϕ ⊂ ψ`. + +```rzk +#def is-right-orthogonal-terminal-map + : U + := + is-right-orthogonal-to-shape I ψ ϕ A Unit (terminal-map A) +``` + +### Unique extensions types are local types + +The equivalence between `is-local-type` and `has-unique-extensions` follows +straightforwardly from the fact that for every `σ : ϕ → A` we have an +equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]` and the fiber +of the restriction map `(ψ → A) → (ϕ → A)`. ```rzk #def is-local-type-has-unique-extensions - ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A) + ( has-ue-ψ-ϕ-A : has-unique-extensions) : is-local-type := is-equiv-is-contr-map (ψ → A) (ϕ → A) ( \ τ t → τ t) ( \ ( σ : ϕ → A) → - is-contr-equiv-is-contr - ( extension-type I ψ ϕ ( \ t → A) σ) - ( homotopy-extension-type I ψ ϕ ( \ t → A) σ) - ( extension-type-weakening I ψ ϕ ( \ t → A) σ) - ( has-ue-ψ-ϕ-A σ)) + is-contr-equiv-is-contr + ( extension-type I ψ ϕ ( \ t → A) σ) + ( homotopy-extension-type I ψ ϕ ( \ t → A) σ) + ( extension-type-weakening I ψ ϕ ( \ t → A) σ) + ( has-ue-ψ-ϕ-A σ)) #def has-unique-extensions-is-local-type ( is-lt-ψ-ϕ-A : is-local-type) - : has-unique-extensions I ψ ϕ A + : has-unique-extensions := \ σ → is-contr-equiv-is-contr' @@ -386,17 +770,70 @@ and the fiber of the restriction map `(ψ → A) → (ϕ → A)`. ( ψ → A) (ϕ → A) ( \ τ t → τ t) ( is-lt-ψ-ϕ-A) ( σ)) -#end is-local-type + +#end has-unique-extensions ``` -Since the property of having unique extensions passes from the codomain to the domain -of a right orthogonal map, the same is true for locality of types. +### Properties of local types / unique extension types + +We fix a shape inclusion `ϕ ⊂ ψ`. ```rzk -#def is-local-type-domain-right-orthogonal-is-local-type-codomain - ( I : CUBE) - ( ψ : I → TOPE) - ( ϕ : ψ → TOPE) +#section stability-properties-local-types +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +``` + +Every map between types with unique extensions / local types is right +orthogonal. + +```rzk +#def is-right-orthogonal-have-unique-extensions + ( A' A : U) + ( has-ue-ψ-ϕ-A' : has-unique-extensions I ψ ϕ A') + ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A) + ( α : A' → A) + : is-right-orthogonal-to-shape I ψ ϕ A' A α + := + \ σ → + is-equiv-are-contr + ( extension-type I ψ ϕ (\ _ → A') (σ)) + ( extension-type I ψ ϕ (\ _ → A) (\ t → α (σ t))) + ( has-ue-ψ-ϕ-A' σ) + ( has-ue-ψ-ϕ-A (\ t → α (σ t))) + ( \ τ t → α (τ t)) + +#def is-right-orthogonal-are-local-types + ( A' A : U) + ( is-lt-ψ-ϕ-A' : is-local-type I ψ ϕ A') + ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A) + : ( α : A' → A) + → is-right-orthogonal-to-shape I ψ ϕ A' A α + := + is-right-orthogonal-have-unique-extensions A' A + ( has-unique-extensions-is-local-type I ψ ϕ A' is-lt-ψ-ϕ-A') + ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A) +``` + +Conversely, the property of having unique extension can be pulled back along any +right orthogonal map. + +```rzk +#def has-unique-extensions-right-orthogonal-has-unique-extensions + ( A' A : U) + ( α : A' → A) + ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + : has-unique-extensions I ψ ϕ A → has-unique-extensions I ψ ϕ A' + := + \ has-ue-A ( σ' : ϕ → A') → + is-contr-equiv-is-contr' + ( ( t : ψ) → A' [ϕ t ↦ σ' t]) + ( ( t : ψ) → A [ϕ t ↦ α (σ' t)]) + ( \ τ' t → α (τ' t) , is-orth-ψ-ϕ-α σ') + ( has-ue-A (\ t → α (σ' t))) + +#def is-local-type-right-orthogonal-is-local-type ( A' A : U) ( α : A' → A) ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) @@ -404,8 +841,162 @@ of a right orthogonal map, the same is true for locality of types. : is-local-type I ψ ϕ A' := is-local-type-has-unique-extensions I ψ ϕ A' - ( has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain - I ψ ϕ A' A α is-orth-α + ( has-unique-extensions-right-orthogonal-has-unique-extensions + ( A') ( A) ( α) ( is-orth-α) ( has-unique-extensions-is-local-type I ψ ϕ A is-local-A)) +``` + +Weak extension extensionality says that every contractible type has unique +extensions for every shape inclusion `ϕ ⊂ ψ`. + +```rzk +#def has-unique-extensions-is-contr uses (weakextext) + ( C : U) + ( is-contr-C : is-contr C) + : has-unique-extensions I ψ ϕ C + := + weakextext I ψ ϕ + ( \ _ → C) ( \ _ → is-contr-C) + +#def has-unique-extensions-Unit uses (weakextext) + : has-unique-extensions I ψ ϕ Unit + := has-unique-extensions-is-contr Unit is-contr-Unit + +``` + +Unique extension types are closed under equivalence. + +```rzk +#def is-local-type-equiv-is-local-type uses (extext) + ( A' A : U) + ( A'≃A : Equiv A' A) + : is-local-type I ψ ϕ A → is-local-type I ψ ϕ A' + := + is-equiv-Equiv-is-equiv + ( ψ → A') ( ϕ → A') ( \ τ' t → τ' t) + ( ψ → A) ( ϕ → A) ( \ τ t → τ t) + ( equiv-of-restriction-maps-equiv-family extext I ψ ϕ + ( \ _ → A') ( \ _ → A) ( \ _ → A'≃A)) + +#def has-unique-extensions-equiv-has-unique-extensions uses (extext) + ( A' A : U) + ( (α , is-equiv-α) : Equiv A' A) + : has-unique-extensions I ψ ϕ A → has-unique-extensions I ψ ϕ A' + := + has-unique-extensions-right-orthogonal-has-unique-extensions A' A α + ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A' A α is-equiv-α) + +#end stability-properties-local-types +``` + +### Unique extension types are types with right orthogonal terminal map + +Next we prove the logical equivalence between `has-unique-extensions` and +`is-right-orthogonal-terminal-map`. This follows directly from the fact that +`Unit` has unique extensions (using `weakextext : WeakExtExt`). + +```rzk +#section is-right-orthogonal-terminal-map +#variable I : CUBE +#variable ψ : I → TOPE +#variable ϕ : ψ → TOPE +#variable A : U + +#def has-unique-extensions-is-right-orthogonal-terminal-map + uses (weakextext) + ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A) + : has-unique-extensions I ψ ϕ A + := + has-unique-extensions-right-orthogonal-has-unique-extensions + I ψ ϕ A Unit (terminal-map A) + ( is-orth-ψ-ϕ-tm-A) + ( has-unique-extensions-Unit I ψ ϕ) + +#def has-unique-extensions-is-right-orthogonal-a-terminal-map + uses (weakextext) + ( tm : A → Unit) + ( is-orth-ψ-ϕ-tm : is-right-orthogonal-to-shape I ψ ϕ A Unit tm) + : has-unique-extensions I ψ ϕ A + := + has-unique-extensions-right-orthogonal-has-unique-extensions + I ψ ϕ A Unit tm + ( is-orth-ψ-ϕ-tm) + ( has-unique-extensions-Unit I ψ ϕ) + +#def is-right-orthogonal-terminal-map-has-unique-extensions + uses (weakextext) + ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A) + : is-right-orthogonal-terminal-map I ψ ϕ A + := + is-right-orthogonal-have-unique-extensions I ψ ϕ A Unit + ( has-ue-ψ-ϕ-A) ( has-unique-extensions-Unit I ψ ϕ) + ( terminal-map A) + +#def is-right-orthogonal-terminal-map-is-local-type + uses (weakextext) + ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A) + : is-right-orthogonal-terminal-map I ψ ϕ A + := + is-right-orthogonal-terminal-map-has-unique-extensions + ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A) + +#def is-local-type-is-right-orthogonal-terminal-map + uses (weakextext) + ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A) + : is-local-type I ψ ϕ A + := + is-local-type-has-unique-extensions I ψ ϕ A + ( has-unique-extensions-is-right-orthogonal-terminal-map + ( is-orth-ψ-ϕ-tm-A)) + +#end is-right-orthogonal-terminal-map +``` + +## Fibers of right orthogonal maps +Let `α : A' → A` be right orthogonal to `ϕ ⊂ ψ`. Then every fiber of `α` has +unique extensions along `ϕ ⊂ ψ`. This follows immediately since the fibers of +`α` are just the relative products of `α : A' → A` with the maps `a : Unit → A` +from the unit type. + +```rzk +#def has-fiberwise-unique-extensions-is-right-orthogonal-to-shape + uses (extext weakextext) + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A' A : U) + ( α : A' → A) + ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α) + ( a : A) + : has-unique-extensions I ψ ϕ (fib A' A α a) + := + has-unique-extensions-equiv-has-unique-extensions I ψ ϕ + ( fib A' A α a) + ( relative-product A A' α Unit (\ unit → a)) + ( compute-pullback-to-Unit A' A α a) + ( has-unique-extensions-is-right-orthogonal-terminal-map I ψ ϕ + ( relative-product A A' α Unit (\ unit → a)) + ( is-right-orthogonal-pullback-to-shape I ψ ϕ A' A α + ( is-orth-ψ-ϕ-α) ( Unit) (\ unit → a))) +``` + +Corollary: Given two types `A'` and `A` with unique extensions w.r.t. `ϕ ⊂ ψ`, +every fiber of every map `α : A' → A` also has unique extensions. + +```rzk +#def has-fiberwise-unique-extensions-have-unique-extensions + uses (extext weakextext) + ( I : CUBE) + ( ψ : I → TOPE) + ( ϕ : ψ → TOPE) + ( A' A : U) + ( α : A' → A) + ( has-ue-ψ-ϕ-A' : has-unique-extensions I ψ ϕ A') + ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A) + : (a : A) → has-unique-extensions I ψ ϕ (fib A' A α a) + := + has-fiberwise-unique-extensions-is-right-orthogonal-to-shape I ψ ϕ A' A α + ( is-right-orthogonal-have-unique-extensions I ψ ϕ A' A + ( has-ue-ψ-ϕ-A') ( has-ue-ψ-ϕ-A) ( α)) ``` diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md index c3ad152c..6a0b1166 100644 --- a/src/simplicial-hott/05-segal-types.rzk.md +++ b/src/simplicial-hott/05-segal-types.rzk.md @@ -16,8 +16,8 @@ This is a literate `rzk` file: - `hott/total-space.md` — We rely on `#!rzk is-equiv-projection-contractible-fibers` and `#!rzk projection-total-type` in the proof of Theorem 5.5. -- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and their - subshapes. +- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and + their subshapes. - `03-extension-types.rzk.md` — We use the fubini theorem and extension extensionality. @@ -216,6 +216,66 @@ Extension types are also used to define the type of commutative triangles: t₂ ≡ t₁ ↦ h t₂] -- the diagonal is exactly `h` ``` +## Arrow types + +We define the arrow type: + +```rzk +#def arr + ( A : U) + : U + := Δ¹ → A +``` + +For later convenience we give an alternative characterizations of the arrow +type. + +```rzk +#def fibered-arr + ( A : U) + : U + := Σ (x : A) , (Σ (y : A) , hom A x y) + +#def fibered-arr-free-arr + ( A : U) + : arr A → fibered-arr A + := \ k → (k 0₂ , (k 1₂ , k)) + +#def is-equiv-fibered-arr-free-arr + ( A : U) + : is-equiv (arr A) (fibered-arr A) (fibered-arr-free-arr A) + := + ( ( (\ (_ , (_ , f)) → f) , (\ _ → refl)) + , ( (\ (_ , (_ , f)) → f) , (\ _ → refl))) + +#def equiv-fibered-arr-free-arr + ( A : U) + : Equiv (arr A) (fibered-arr A) + := (fibered-arr-free-arr A , is-equiv-fibered-arr-free-arr A) +``` + +And the corresponding uncurried version. + +```rzk +#def fibered-arr' + ( A : U) + : U + := + Σ ((a,b) : product A A), hom A a b + +#def fibered-arr-free-arr' + ( A : U) + : arr A → fibered-arr' A + := \ σ → ((σ 0₂ , σ 1₂) , σ) + +#def is-equiv-fibered-arr-free-arr' + ( A : U) + : is-equiv (arr A) (fibered-arr' A) (fibered-arr-free-arr' A) + := + ( ( (\ ((_ , _) , σ) → σ) , (\ _ → refl)) + , ( (\ ((_ , _) , σ) → σ) , (\ _ → refl))) +``` + ## The Segal condition A type is **Segal** if every composable pair of arrows has a unique composite. @@ -624,36 +684,7 @@ then $(x : X) → A x$ is a Segal type. ( \ s → is-local-horn-inclusion-is-segal (A s)(fiberwise-is-segal-A s))) ``` -In particular, the arrow type of a Segal type is Segal. First, we define the -arrow type: - -```rzk -#def arr - ( A : U) - : U - := Δ¹ → A -``` - -For later use, an equivalent characterization of the arrow type. - -```rzk -#def arr-Σ-hom - ( A : U) - : ( arr A) → (Σ (x : A) , (Σ (y : A) , hom A x y)) - := \ f → (f 0₂ , (f 1₂ , f)) - -#def is-equiv-arr-Σ-hom - ( A : U) - : is-equiv (arr A) (Σ (x : A) , (Σ (y : A) , hom A x y)) (arr-Σ-hom A) - := - ( ( \ (x , (y , f)) → f , \ f → refl) , - ( \ (x , (y , f)) → f , \ xyf → refl)) - -#def equiv-arr-Σ-hom - ( A : U) - : Equiv (arr A) (Σ (x : A) , (Σ (y : A) , hom A x y)) - := ( arr-Σ-hom A , is-equiv-arr-Σ-hom A) -``` +In particular, the arrow type of a Segal type is Segal. ```rzk title="RS17, Corollary 5.6(ii), special case for locality at the horn inclusion" #def is-local-horn-inclusion-arr uses (extext) @@ -912,17 +943,16 @@ The `#!rzk witness-square-comp-is-segal` as an arrow in the arrow type: ( g : hom A x y) ( h : hom A y z) : hom2 (arr A) f g h - (arr-in-arr-is-segal A is-segal-A w x y f g) - (arr-in-arr-is-segal A is-segal-A x y z g h) - (comp-is-segal (arr A) (is-segal-arr A is-segal-A) - f g h - (arr-in-arr-is-segal A is-segal-A w x y f g) - (arr-in-arr-is-segal A is-segal-A x y z g h)) + ( arr-in-arr-is-segal A is-segal-A w x y f g) + ( arr-in-arr-is-segal A is-segal-A x y z g h) + ( comp-is-segal (arr A) (is-segal-arr A is-segal-A) f g h + ( arr-in-arr-is-segal A is-segal-A w x y f g) + ( arr-in-arr-is-segal A is-segal-A x y z g h)) := witness-comp-is-segal ( arr A) ( is-segal-arr A is-segal-A) - f g h + ( f) ( g) ( h) ( arr-in-arr-is-segal A is-segal-A w x y f g) ( arr-in-arr-is-segal A is-segal-A x y z g h) ``` @@ -1203,7 +1233,7 @@ arrow. : Equiv (f = h) (hom2 A x x y (id-hom A x) f h) := ( ( map-hom2-homotopy A x y f h) , - ( total-equiv-family-of-equiv + ( is-equiv-fiberwise-is-equiv-total ( hom A x y) ( \ k → (f = k)) ( \ k → (hom2 A x x y (id-hom A x) f k)) @@ -1265,7 +1295,7 @@ A dual notion of homotopy can be defined similarly. : Equiv (f = h) (hom2 A x y y f (id-hom A y) h) := ( ( map-hom2-homotopy' A x y f h) , - ( total-equiv-family-of-equiv + ( is-equiv-fiberwise-is-equiv-total ( hom A x y) ( \ k → (f = k)) ( \ k → (hom2 A x y y f (id-hom A y) k)) @@ -1336,7 +1366,7 @@ the data provided by a commutative triangle with that boundary. : Equiv ((comp-is-segal A is-segal-A x y z f g) = k) (hom2 A x y z f g k) := ( ( map-hom2-eq-is-segal A is-segal-A x y z f g k) , - ( total-equiv-family-of-equiv + ( is-equiv-fiberwise-is-equiv-total ( hom A x z) ( \ m → (comp-is-segal A is-segal-A x y z f g) = m) ( hom2 A x y z f g) @@ -1455,8 +1485,6 @@ As a special case of the above: #section is-segal-Unit -#def is-contr-Unit : is-contr Unit := (unit , \ _ → refl) - #def is-contr-Δ²→Unit uses (extext) : is-contr (Δ² → Unit) := @@ -1624,7 +1652,7 @@ The cofibration Λ²₁ → Δ² is inner anodyne #def is-inner-anodyne-Λ²₁ : is-inner-anodyne (2 × 2) Δ² Λ²₁ := \ A is-segal-A h' → - equiv-with-contractible-domain-implies-contractible-codomain + is-contr-equiv-is-contr ( Σ (h : hom A (h' (0₂,0₂)) (h' (1₂,1₂))) , (hom2 A (h' (0₂,0₂)) (h' (1₂,0₂)) (h' (1₂,1₂)) (\ t → h' (t,0₂)) (\ s → h' (1₂,s)) h)) @@ -1648,7 +1676,7 @@ The cofibration Λ²₁ → Δ² is inner anodyne (\ (t,s) → ψ t ∧ ζ s) (\ (t,s) → (Φ t ∧ ζ s) ∨ (ψ t ∧ χ s)) := \ A is-segal-A h → - equiv-with-contractible-codomain-implies-contractible-domain + is-contr-equiv-is-contr' (((t,s) : I × J | ψ t ∧ ζ s) → A[(Φ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ h (t,s)]) ( (s : ζ) → ((t : ψ) → A[ Φ t ↦ h (t,s)])[ χ s ↦ \ t → h (t, s)]) (uncurry-opcurry I J ψ Φ ζ χ (\ s t → A) h) @@ -1671,7 +1699,7 @@ The cofibration Λ²₁ → Δ² is inner anodyne (\ (t,s) → ψ t ∧ ζ s) (\ (t,s) → (Φ t ∧ ζ s) ∨ (ψ t ∧ χ s)) := \ A is-segal-A h → - equiv-with-contractible-domain-implies-contractible-codomain + is-contr-equiv-is-contr ( (t : ψ) → ((s : ζ) → A[ χ s ↦ h (t,s)])[ Φ t ↦ \ s → h (t, s)]) (((t,s) : I × J | ψ t ∧ ζ s) → A[(Φ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ h (t,s)]) (curry-uncurry I J ψ Φ ζ χ (\ s t → A) h) @@ -1779,8 +1807,8 @@ The cofibration Λ²₁ → Δ² is inner anodyne ## Inner fibrations -An inner fibration is a map `α : A' → A` which is right orthogonal -to `Λ ⊂ Δ²`. This is the relative notion of a Segal type. +An inner fibration is a map `α : A' → A` which is right orthogonal to `Λ ⊂ Δ²`. +This is the relative notion of a Segal type. ```rzk #def is-inner-fibration diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md index 89aee5d3..5b2be0b3 100644 --- a/src/simplicial-hott/07-discrete.rzk.md +++ b/src/simplicial-hott/07-discrete.rzk.md @@ -44,6 +44,144 @@ identity types. := (x : A) → (y : A) → is-equiv (x = y) (hom A x y) (hom-eq A x y) ``` +## Alternative definitions + +One can characterize discrete types in various other equivalent: + +```rzk +#section discrete-types-alternative + +#variable A : U + +#def is-Δ¹-local + : U + := is-equiv A (Δ¹ → A) (\ a _ → a) +``` + +```rzk +#def is-left-local + : U + := is-local-type 2 Δ¹ (\ t → t ≡ 0₂) A + +#def is-right-local + : U + := is-local-type 2 Δ¹ (\ t → t ≡ 1₂) A +``` + +### Alternative definitions : proofs + +First ot all, note that we have two section-retraction pairs + +```rzk +#def is-section-retraction-0-Δ¹-0 + : is-section-retraction-pair + ( A) ( Δ¹ → A) ( (t : 2 | Δ¹ t ∧ t ≡ 0₂) → A) + ( \ a _ → a) (\ τ t → τ t) + := + ( ( \ σ → σ 0₂ , \ _ → refl) + , ( \ σ → σ 0₂ , \ _ → refl)) + +#def is-section-retraction-1-Δ¹-1 + : is-section-retraction-pair + ( A) ( Δ¹ → A) ( (t : 2 | Δ¹ t ∧ t ≡ 1₂) → A) + ( \ a _ → a) (\ τ t → τ t) + := + ( ( \ σ → σ 1₂ , \ _ → refl) + , ( \ σ → σ 1₂ , \ _ → refl)) +``` + +From this it follows that the three alternative definitions are all equivalent +to each other. + +```rzk +#def is-left-local-is-Δ¹-local + : is-Δ¹-local → is-left-local + := + is-equiv-retraction-is-equiv-section-is-section-retraction-pair + ( A) ( Δ¹ → A) ( (t : 2 | Δ¹ t ∧ t ≡ 0₂) → A) + ( \ a _ → a) (\ τ t → τ t) + ( is-section-retraction-0-Δ¹-0) + +#def is-Δ¹-local-is-left-local + : is-left-local → is-Δ¹-local + := + is-equiv-section-is-equiv-retraction-is-section-retraction-pair + ( A) ( Δ¹ → A) ( (t : 2 | Δ¹ t ∧ t ≡ 0₂) → A) + ( \ a _ → a) (\ τ t → τ t) + ( is-section-retraction-0-Δ¹-0) + +#def is-right-local-is-Δ¹-local + : is-Δ¹-local → is-right-local + := + is-equiv-retraction-is-equiv-section-is-section-retraction-pair + ( A) ( Δ¹ → A) ( (t : 2 | Δ¹ t ∧ t ≡ 1₂) → A) + ( \ a _ → a) (\ τ t → τ t) + ( is-section-retraction-1-Δ¹-1) + +#def is-Δ¹-local-is-right-local + : is-right-local → is-Δ¹-local + := + is-equiv-section-is-equiv-retraction-is-section-retraction-pair + ( A) ( Δ¹ → A) ( (t : 2 | Δ¹ t ∧ t ≡ 1₂) → A) + ( \ a _ → a) (\ τ t → τ t) + ( is-section-retraction-1-Δ¹-1) +``` + +Next, we aim to compare the original `is-discrete` with `is-Δ¹-local`. + +To do this, we note that we have an equivalence of maps between `A → (Δ¹ → A)` +and the total map of the family `\ (a, b) → hom-eq a b : a = b → hom A a b` . + +```rzk +#def equiv-of-maps-total-map-hom-eq-const-Δ¹ + : Equiv-of-maps + ( A) ( Δ¹ → A) + ( \ a _ → a) + ( free-paths A) ( fibered-arr' A) + ( \ ((a,b), p) → ((a,b), hom-eq A a b p)) + := + ( ( ( constant-free-path A + , fibered-arr-free-arr' A) + , \ _ → refl) + , ( is-equiv-constant-free-path A + , is-equiv-fibered-arr-free-arr' A)) +``` + +The rest is just logical bookkeeping using that equivalences are preserved under +equivalences of maps and when passing to/from total types. + +```rzk +#def is-Δ¹-local-is-discrete + ( is-discrete-A : is-discrete A) + : is-Δ¹-local + := + is-equiv-Equiv-is-equiv ( A) ( Δ¹ → A) ( \ a _ → a) + ( free-paths A) ( fibered-arr' A) + ( \ ((a,b), p) → ((a,b), hom-eq A a b p)) + ( equiv-of-maps-total-map-hom-eq-const-Δ¹) + ( is-equiv-total-is-equiv-fiberwise + ( product A A) ( \ (a,b) → a = b) ( \ (a,b) → hom A a b) + ( \ (a,b) → hom-eq A a b) + ( \ (a,b) → is-discrete-A a b)) + +#def is-discrete-is-Δ¹-local + ( is-Δ¹-local-A : is-Δ¹-local) + : is-discrete A + := + \ a b → + ( is-equiv-fiberwise-is-equiv-total ( product A A) ( \ (a,b) → a = b) + ( \ (a,b) → hom A a b) + ( \ (a,b) → hom-eq A a b) + ( is-equiv-Equiv-is-equiv' ( A) ( Δ¹ → A) ( \ a _ → a) + ( free-paths A) ( fibered-arr' A) + ( \ ((a,b), p) → ((a,b), hom-eq A a b p)) + ( equiv-of-maps-total-map-hom-eq-const-Δ¹) + (is-Δ¹-local-A))) + ( a, b) + +#end discrete-types-alternative +``` + ## Families of discrete types By function extensionality, the dependent function type associated to a family @@ -237,50 +375,40 @@ Discrete types are automatically Segal types. ( ( \ σ t s → (second (second σ)) (t , s)) , (\ σ → refl)))) ``` -The equivalence underlying `#!rzk equiv-arr-Σ-hom`: - ```rzk -#def fibered-arr-free-arr - : (arr A) → (Σ (u : A) , (Σ (v : A) , hom A u v)) - := \ k → (k 0₂ , (k 1₂ , k)) - -#def is-equiv-fibered-arr-free-arr - : is-equiv (arr A) (Σ (u : A) , (Σ (v : A) , hom A u v)) (fibered-arr-free-arr) - := is-equiv-arr-Σ-hom A - #def is-equiv-ap-fibered-arr-free-arr uses (w x y z) : is-equiv ( f =_{Δ¹ → A} g) - ( fibered-arr-free-arr f = fibered-arr-free-arr g) + ( fibered-arr-free-arr A f = fibered-arr-free-arr A g) ( ap ( arr A) ( Σ (u : A) , (Σ (v : A) , (hom A u v))) ( f) ( g) - ( fibered-arr-free-arr)) + ( fibered-arr-free-arr A)) := is-emb-is-equiv ( arr A) ( Σ (u : A) , (Σ (v : A) , (hom A u v))) - ( fibered-arr-free-arr) - ( is-equiv-fibered-arr-free-arr) + ( fibered-arr-free-arr A) + ( is-equiv-fibered-arr-free-arr A) ( f) ( g) #def equiv-eq-fibered-arr-eq-free-arr uses (w x y z) - : Equiv (f =_{Δ¹ → A} g) (fibered-arr-free-arr f = fibered-arr-free-arr g) + : Equiv (f =_{Δ¹ → A} g) (fibered-arr-free-arr A f = fibered-arr-free-arr A g) := equiv-ap-is-equiv ( arr A) ( Σ (u : A) , (Σ (v : A) , (hom A u v))) - ( fibered-arr-free-arr) - ( is-equiv-fibered-arr-free-arr) + ( fibered-arr-free-arr A) + ( is-equiv-fibered-arr-free-arr A) ( f) ( g) #def equiv-sigma-over-product-hom-eq : Equiv - ( fibered-arr-free-arr f = fibered-arr-free-arr g) + ( fibered-arr-free-arr A f = fibered-arr-free-arr A g) ( Σ ( p : x = z) , ( Σ ( q : y = w) , ( product-transport A A (hom A) x z y w p q f = g))) @@ -288,8 +416,8 @@ The equivalence underlying `#!rzk equiv-arr-Σ-hom`: extensionality-Σ-over-product ( A) (A) ( hom A) - ( fibered-arr-free-arr f) - ( fibered-arr-free-arr g) + ( fibered-arr-free-arr A f) + ( fibered-arr-free-arr A g) #def equiv-square-sigma-over-product uses (extext is-discrete-A) : Equiv @@ -318,7 +446,7 @@ The equivalence underlying `#!rzk equiv-arr-Σ-hom`: (Δ¹ t) ∧ (s ≡ 1₂) ↦ k t]))) ( equiv-comp ( f =_{Δ¹ → A} g) - ( fibered-arr-free-arr f = fibered-arr-free-arr g) + ( fibered-arr-free-arr A f = fibered-arr-free-arr A g) ( Σ ( p : x = z) , ( Σ ( q : y = w) , ( product-transport A A (hom A) x z y w p q f = g))) @@ -625,7 +753,7 @@ The previous calculations allow us to establish a family of equivalences: ( fibered-map-square-sigma-over-product A x y x y f refl refl)) := - family-of-equiv-total-equiv + is-equiv-total-is-equiv-fiberwise ( hom A x y) ( \ g → f = g) ( \ g → diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md index c369dda1..5647968d 100644 --- a/src/simplicial-hott/08-covariant.rzk.md +++ b/src/simplicial-hott/08-covariant.rzk.md @@ -415,7 +415,7 @@ type, then so is `A'`. : is-segal A' := is-segal-is-local-horn-inclusion A' - ( is-local-type-domain-right-orthogonal-is-local-type-codomain + ( is-local-type-right-orthogonal-is-local-type ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α ( is-inner-fibration-is-left-fibration A' A α is-left-fib-α) ( is-local-horn-inclusion-is-segal A is-segal-A)) @@ -593,12 +593,6 @@ Finally, we deduce the theorem by some straightforward logical bookkeeping. ## Total type of a covariant family over a Segal type -We prove that the total type of a covariant family over a Segal type is a Segal -type. We split the proof into intermediate steps. Let `A` be a type and a type -family `#!rzk C : A → U`. - -### Category theoretic proof - For every covariant family `C : A → U`, the projection `Σ A, C → A` is an left fibration, hence an inner fibration. It immediately follows that if `A` is Segal, then so is `Σ A, C`. @@ -617,63 +611,6 @@ Segal, then so is `Σ A, C`. ( is-naive-left-fibration-is-covariant A C is-covariant-C)) ``` -### Type theoretic proof - -We examine the fibers of the horn restriction on the total type of `C`. First -note we have the equivalences: - -```rzk -#def apply-4-3 - ( A : U ) - ( C : A → U ) - : Equiv - ( Λ → (Σ ( a : A ), C a ) ) - ( Σ ( f : Λ → A ), ( t : Λ ) → ( C ( f t ) ) ) - := - axiom-choice ( 2 × 2 ) Λ ( \ t → BOT ) ( \ t → A ) - ( \ t a → C a ) ( \ t → recBOT ) ( \ t → recBOT ) - -#def apply-4-3-again - ( A : U ) - ( C : A → U ) - : Equiv - ( Δ² → (Σ ( a : A ), C a ) ) - ( Σ ( f : Δ² → A ), ( t : Δ² ) → ( C ( f t ) ) ) - := - axiom-choice ( 2 × 2 ) Δ² ( \ t → BOT ) ( \ t → A ) - ( \ t a → C a ) ( \ t → recBOT ) ( \ t → recBOT ) -``` - -We show that the induced map between this types is an equivalence. First we -exhibit the map: - -```rzk -#def total-inner-horn-restriction - ( A : U ) - ( C : A → U ) - : ( Σ ( f : Δ² → A ), ( t : Δ² ) → ( C ( f t ) ) ) → - ( Σ ( g : Λ → A ), ( t : Λ ) → ( C ( g t ) ) ) - := \ ( f, μ ) → ( \ t → f t , \ t → μ t) -``` - -Next we compute the fibers of this map by showing the equivalence as claimed in -the proof of Theorem 8.8 in RS17. The following maps will be packed into some -`#!rzk Equiv`. - -```rzk -#def map-to-total-inner-horn-restriction-fiber - ( A : U ) - ( C : A → U ) - ( (g , φ) : ( Σ ( k : Λ → A ), ( t : Λ ) → C ( k t ) ) ) - : ( Σ (h : (t : Δ²) → A [ Λ t ↦ g t ] ) , - (( t : Δ² ) → C (h t) [ Λ t ↦ φ t])) → - ( fib ( Σ ( l : Δ² → A ), ( t : Δ² ) → ( C ( l t ) )) - ( Σ ( k : Λ → A ), ( t : Λ ) → ( C ( k t ) )) - ( total-inner-horn-restriction A C ) - ( g, φ) ) - := \ ( f,μ ) → ( ( \ t → f t, \ t → μ t ), refl ) -``` - ## Representable covariant families If `A` is a Segal type and `a : A` is any term, then `hom A a` defines a @@ -743,7 +680,7 @@ By uncurrying (RS 4.2) we have an equivalence: (Δ¹ t) ∧ (s ≡ 0₂) ↦ a , (Δ¹ t) ∧ (s ≡ 1₂) ↦ f t])) := - total-equiv-family-equiv + total-equiv-family-of-equiv ( hom A a y) ( \ v → dhom-representable A a x y f u v) ( \ v → @@ -826,7 +763,7 @@ By uncurrying (RS 4.2) we have an equivalence: ( Σ ( d : hom A a y) , ( product (hom2 A a x y u f d) (hom2 A a a y (id-hom A a) v d)))) := - total-equiv-family-equiv + total-equiv-family-of-equiv ( hom A a y) ( \ v → ( ( (t , s) : Δ¹×Δ¹) → @@ -891,7 +828,7 @@ By uncurrying (RS 4.2) we have an equivalence: ( Σ ( v : hom A a y) , ( product (hom2 A a x y u f d) (hom2 A a a y (id-hom A a) v d)))) ( representable-dhom-from-hom2 A a x y f u) - ( total-equiv-family-equiv + ( total-equiv-family-of-equiv ( hom A a y) ( \ d → ( product @@ -930,7 +867,7 @@ Now we introduce the hypothesis that A is Segal type. ( hom2 A a x y u f d) ( Σ (v : hom A a y) , hom2 A a a y (id-hom A a) v d))) ( representable-dhom-from-hom2-dist A a x y f u) - ( total-equiv-family-equiv + ( total-equiv-family-of-equiv ( hom A a y) ( \ d → product (hom2 A a x y u f d) (Σ (v : hom A a y) , (v = d))) ( \ d → @@ -938,12 +875,12 @@ Now we introduce the hypothesis that A is Segal type. ( hom2 A a x y u f d) ( Σ (v : hom A a y) , hom2 A a a y (id-hom A a) v d))) ( \ d → - ( total-equiv-family-equiv + ( total-equiv-family-of-equiv ( hom2 A a x y u f d) ( \ α → (Σ (v : hom A a y) , (v = d))) ( \ α → (Σ (v : hom A a y) , hom2 A a a y (id-hom A a) v d)) ( \ α → - ( total-equiv-family-equiv + ( total-equiv-family-of-equiv ( hom A a y) ( \ v → (v = d)) ( \ v → hom2 A a a y (id-hom A a) v d) @@ -981,7 +918,7 @@ Now we introduce the hypothesis that A is Segal type. ( product (hom2 A a x y u f d) (Σ (v : hom A a y) , (v = d)))) ( Σ (d : hom A a y) , (hom2 A a x y u f d)) ( representable-dhom-from-path-space-is-segal A is-segal-A a x y f u) - ( total-equiv-family-equiv + ( total-equiv-family-of-equiv ( hom A a y) ( \ d → product (hom2 A a x y u f d) (Σ (v : hom A a y) , (v = d))) ( \ d → hom2 A a x y u f d) @@ -1146,7 +1083,7 @@ types as follows. (Δ¹ t) ∧ (s ≡ 0₂) ↦ a , (Δ¹ t) ∧ (s ≡ 1₂) ↦ f t])) := - total-equiv-pullback-is-equiv + equiv-total-pullback-is-equiv ( ( (t , s) : ∂□) → A [ (t ≡ 0₂) ∧ (Δ¹ s) ↦ u s , (Δ¹ t) ∧ (s ≡ 0₂) ↦ a , @@ -1389,7 +1326,7 @@ equivalence. This follows from the fact that the total types (summed over (covariant-uniqueness-curried A x y f C is-covariant-C u v) := - total-equiv-family-of-equiv + is-equiv-fiberwise-is-equiv-total (C y) (dhom A x y f C u) (\ v' → covariant-transport A x y f C is-covariant-C u = v') @@ -1527,7 +1464,7 @@ domain are equivalent: ( Σ (i : B x) , ((t : Δ¹) → C (f t) [t ≡ 0₂ ↦ (first (equiv-BC x)) i])) ( Σ (u : C x) , ((t : Δ¹) → C (f t) [t ≡ 0₂ ↦ u])) := - total-equiv-pullback-is-equiv + equiv-total-pullback-is-equiv ( B x) ( C x) ( first (equiv-BC x)) @@ -1563,7 +1500,7 @@ domain are equivalent: ( (t : Δ¹) → B (f t) [t ≡ 0₂ ↦ i]) ( (t : Δ¹) → C (f t) [t ≡ 0₂ ↦ (first (equiv-BC x)) i]) := - family-equiv-total-equiv + family-of-equiv-is-equiv-total ( B x) ( \ ii → ((t : Δ¹) → B (f t) [t ≡ 0₂ ↦ ii])) ( \ ii → ((t : Δ¹) → C (f t) [t ≡ 0₂ ↦ (first (equiv-BC x)) ii])) @@ -1795,7 +1732,7 @@ By uncurrying (RS 4.2) we have an equivalence: (Δ¹ t) ∧ (s ≡ 0₂) ↦ f t , (Δ¹ t) ∧ (s ≡ 1₂) ↦ a])) := - total-equiv-family-equiv + total-equiv-family-of-equiv ( hom A x a) ( \ u → dhom-contra-representable A a x y f u v) ( \ u → @@ -1822,7 +1759,7 @@ By uncurrying (RS 4.2) we have an equivalence: (Σ (d : hom A x a) , product (hom2 A x a a u (id-hom A a) d) (hom2 A x y a f v d))) := - total-equiv-family-equiv (hom A x a) + total-equiv-family-of-equiv (hom A x a) ( \ u → ( ( (t , s) : Δ¹×Δ¹) → A [ (t ≡ 0₂) ∧ (Δ¹ s) ↦ u s , @@ -1884,14 +1821,14 @@ By uncurrying (RS 4.2) we have an equivalence: ( Σ ( u : hom A x a) , ( product (hom2 A x y a f v d) (hom2 A x a a u (id-hom A a) d)))) ( representable-dhom-to-hom2 A a x y f v) - ( total-equiv-family-equiv (hom A x a) + ( total-equiv-family-of-equiv (hom A x a) (\ d → Σ ( u : hom A x a) , ( product (hom2 A x a a u (id-hom A a) d) (hom2 A x y a f v d))) ( \ d → Σ ( u : hom A x a) , ( product (hom2 A x y a f v d) (hom2 A x a a u (id-hom A a) d))) - ( \ d → total-equiv-family-equiv (hom A x a) + ( \ d → total-equiv-family-of-equiv (hom A x a) ( \ u → product (hom2 A x a a u (id-hom A a) d) (hom2 A x y a f v d)) ( \ u → product (hom2 A x y a f v d) (hom2 A x a a u (id-hom A a) d)) ( \ u → @@ -1921,7 +1858,7 @@ By uncurrying (RS 4.2) we have an equivalence: ( hom2 A x y a f v d) ( hom2 A x a a u (id-hom A a) d))) ( representable-dhom-to-hom2-swap A a x y f v) - ( total-equiv-family-equiv (hom A x a) + ( total-equiv-family-of-equiv (hom A x a) ( \ d → ( product ( hom2 A x y a f v d) @@ -1959,19 +1896,19 @@ Now we introduce the hypothesis that A is Segal type. ( hom2 A x y a f v d) ( Σ (u : hom A x a) , (hom2 A x a a u (id-hom A a) d)))) ( representable-dhom-to-hom2-dist A a x y f v) - ( total-equiv-family-equiv (hom A x a) + ( total-equiv-family-of-equiv (hom A x a) ( \ d → product (hom2 A x y a f v d) (Σ (u : hom A x a) , (u = d))) ( \ d → product ( hom2 A x y a f v d) ( Σ (u : hom A x a) , hom2 A x a a u (id-hom A a) d)) ( \ d → - total-equiv-family-equiv + total-equiv-family-of-equiv ( hom2 A x y a f v d) ( \ α → (Σ (u : hom A x a) , (u = d))) ( \ α → (Σ (u : hom A x a) , hom2 A x a a u (id-hom A a) d)) ( \ α → - ( total-equiv-family-equiv + ( total-equiv-family-of-equiv ( hom A x a) ( \ u → (u = d)) ( \ u → hom2 A x a a u (id-hom A a) d) @@ -1993,7 +1930,7 @@ Now we introduce the hypothesis that A is Segal type. ( product (hom2 A x y a f v d) (Σ (u : hom A x a) , (u = d)))) ( Σ (d : hom A x a) , (hom2 A x y a f v d)) ( representable-dhom-to-path-space-is-segal A is-segal-A a x y f v) - ( total-equiv-family-equiv + ( total-equiv-family-of-equiv ( hom A x a) ( \ d → product (hom2 A x y a f v d) (Σ (u : hom A x a) , (u = d))) ( \ d → hom2 A x y a f v d) @@ -2213,7 +2150,7 @@ commuting with the contravariant lifts. ( A) ( \ a → ( b : B ) → (C a b) ) ( \ x y f g → - equiv-with-contractible-codomain-implies-contractible-domain + is-contr-equiv-is-contr' ( (t : Δ¹) → ((b : B) → C (f t) b) [ t ≡ 0₂ ↦ g ]) ( (b : B) → (t : Δ¹) → C (f t) b [ t ≡ 0₂ ↦ g b]) ( flip-ext-fun 2 Δ¹ (\ t → t ≡ 0₂) B ( \ t → C (f t)) ( \ t → g)) @@ -2242,7 +2179,7 @@ The fibers of a covariant fibration over a Segal type are discrete types. : is-discrete (C x) := ( \ u v → - total-equiv-family-of-equiv + is-equiv-fiberwise-is-equiv-total ( C x) ( \ v' → (u = v')) ( hom (C x) u) diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md index 38033774..ea9f382c 100644 --- a/src/simplicial-hott/10-rezk-types.rzk.md +++ b/src/simplicial-hott/10-rezk-types.rzk.md @@ -662,7 +662,7 @@ The predicate `#!rzk is-iso-arrow` is a proposition. ( Σ ( α' : nat-trans-components X A f g) , ( x : X) → is-iso-arrow (A x) (is-segal-A x) (f x) (g x) (α' x)) ( (x : X) → Iso (A x) (is-segal-A x) (f x) (g x)) - ( total-equiv-family-equiv + ( total-equiv-family-of-equiv ( nat-trans X A f g) ( \ α → ( is-iso-arrow @@ -674,7 +674,7 @@ The predicate `#!rzk is-iso-arrow` is a proposition. ( is-iso-arrow (A x) (is-segal-A x) (f x) (g x) ( ev-components-nat-trans X A f g α x))) ( \ α → equiv-is-iso-pointwise-is-iso X A is-segal-A f g α)) - ( total-equiv-pullback-is-equiv + ( equiv-total-pullback-is-equiv ( nat-trans X A f g) ( nat-trans-components X A f g) ( ev-components-nat-trans X A f g) diff --git a/src/simplicial-hott/12-cocartesian.rzk.md b/src/simplicial-hott/12-cocartesian.rzk.md index 5b056eb2..18a207cc 100644 --- a/src/simplicial-hott/12-cocartesian.rzk.md +++ b/src/simplicial-hott/12-cocartesian.rzk.md @@ -94,8 +94,8 @@ a given starting point in the fiber. ## Cocartesian family -A family over cocartesian if it is isoinner and any arrow in -the has a cocartesian lift, given a point in the fiber over the domain. +A family over cocartesian if it is isoinner and any arrow in the has a +cocartesian lift, given a point in the fiber over the domain. ```rzk title="BW23, Definition 5.2.1" #def has-cocartesian-lifts diff --git a/src/simplicial-hott/13-limits.rzk.md b/src/simplicial-hott/13-limits.rzk.md index 7161bf99..7b42b546 100644 --- a/src/simplicial-hott/13-limits.rzk.md +++ b/src/simplicial-hott/13-limits.rzk.md @@ -31,6 +31,7 @@ under `#!rzk f`. : U := Σ (b : B), hom ( A → B) f (constant A B b) ``` + We define a colimit for `#!rzk f : A → B` as an initial cocone under `#!rzk f`. ```rzk @@ -50,8 +51,9 @@ We define a limit of `#!rzk f : A → B` as a terminal cone over `#!rzk f`. : U := Σ ( x : cone A B f ) , is-final (cone A B f) x ``` -We give a second definition of limits, we eventually want to prove both definitions coincide. -Define cone as a family. + +We give a second definition of limits, we eventually want to prove both +definitions coincide. Define cone as a family. ```rzk #def cone2 @@ -59,6 +61,7 @@ Define cone as a family. : (A → B) → (B) → U := \ f → \ b → (hom (A → B) (constant A B b) f) ``` + ```rzk #def constant-nat-trans (A B : U) @@ -86,6 +89,7 @@ Define cone as a family. ( constant-nat-trans A B b x k ) ( α) ``` + Another definition of limit. ```rzk @@ -100,8 +104,8 @@ Another definition of limit. → is-equiv (cone2 A B f x) (cone2 A B f b) (cone-precomposition A B is-segal-B f b x k ) ``` -We give a second definition of colimits, we eventually want to prove both definitions coincide. -Define cocone as a family. +We give a second definition of colimits, we eventually want to prove both +definitions coincide. Define cocone as a family. ```rzk #def cocone2 @@ -128,6 +132,7 @@ Define cocone as a family. ( α) ( constant-nat-trans A B x b k ) ``` + Another definition of colimit. ```rzk @@ -141,8 +146,9 @@ Another definition of colimit. ( x : B) → ( k : hom B x b) → is-equiv (cocone2 A B f x) (cocone2 A B f b) (cocone-postcomposition A B is-segal-B f x b k ) ``` -The following alternative definition does not require a Segalness condition. When -`#!rzk is-segal B` then definitions 1 and 3 coincide. + +The following alternative definition does not require a Segalness condition. +When `#!rzk is-segal B` then definitions 1 and 3 coincide. ```rzk #def limit3 @@ -151,6 +157,7 @@ The following alternative definition does not require a Segalness condition. Whe : U := Σ ( b : B),(x : B) → Equiv (hom B b x ) (cone2 A B f x) ``` + ```rzk #def colimit3 ( A B : U) @@ -174,7 +181,7 @@ In a Segal type, initial objects are isomorphic. := ( first (is-initial-a b) , ( ( first (is-initial-b a) , - eq-is-contr + all-elements-equal-is-contr ( hom A a a) ( is-initial-a a) ( comp-is-segal A is-segal-A a b a @@ -182,7 +189,7 @@ In a Segal type, initial objects are isomorphic. ( first (is-initial-b a))) ( id-hom A a)) , ( first (is-initial-b a) , - eq-is-contr + all-elements-equal-is-contr ( hom A b b) ( is-initial-b b) ( comp-is-segal A is-segal-A b a b @@ -205,7 +212,7 @@ In a Segal type, final objects are isomorphic. := ( first (is-final-b a) , ( ( first (is-final-a b) , - eq-is-contr + all-elements-equal-is-contr ( hom A a a) ( is-final-a a) ( comp-is-segal A is-segal-A a b a @@ -213,7 +220,7 @@ In a Segal type, final objects are isomorphic. ( first (is-final-a b))) ( id-hom A a)) , ( first (is-final-a b) , - eq-is-contr + all-elements-equal-is-contr ( hom A b b) ( is-final-b b) ( comp-is-segal A is-segal-A b a b