Skip to content

Commit

Permalink
Merge branch 'main' into right-orthogonal-calculus-2
Browse files Browse the repository at this point in the history
  • Loading branch information
Tashi Walde committed Oct 13, 2023
2 parents 65cfff1 + 1a07223 commit 4582eaa
Show file tree
Hide file tree
Showing 9 changed files with 521 additions and 221 deletions.
179 changes: 177 additions & 2 deletions src/hott/03-equivalences.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -421,8 +421,8 @@ 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))
Expand Down Expand Up @@ -551,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.
Expand Down
55 changes: 23 additions & 32 deletions src/hott/06-contractible.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -175,65 +175,56 @@ A type is contractible if and only if its terminal map is an equivalence.

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 section-is-retract-of
: A → B
:= first is-retract-of-A-B
#def retraction-is-retract-of
: B → A
:= first (second is-retract-of-A-B)
#variable is-retr-of-A-B : is-retract-of A B
#def homotopy-is-retract-of
: homotopy A A (comp A B A retraction-is-retract-of section-is-retract-of) (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-inhabited-is-contr-is-retract-of 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
:= retraction-is-retract-of (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 has-homotopy-is-contr-is-retract-of 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-inhabited-is-contr-is-retract-of is-contr-B) = a
:=
concat
( A)
( is-inhabited-is-contr-is-retract-of is-contr-B)
( (comp A B A retraction-is-retract-of section-is-retract-of) a)
( 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) (section-is-retract-of a)
( retraction-is-retract-of)
( homotopy-contraction B is-contr-B (section-is-retract-of a)))
( homotopy-is-retract-of 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-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
Expand Down
43 changes: 42 additions & 1 deletion src/hott/08-families-of-maps.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -287,7 +287,9 @@ equivalence.
:= (family-of-equiv-total-equiv A B C f , total-equiv-family-of-equiv 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
Expand All @@ -308,6 +310,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
Expand Down
Loading

0 comments on commit 4582eaa

Please sign in to comment.