Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Representable isos #141

Merged
merged 24 commits into from
Dec 15, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/simplicial-hott/07-discrete.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ This is a literate `rzk` file:
- `hott/01-paths.rzk.md` - We require basic path algebra.
- `hott/04-equivalences.rzk.md` - We require the notion of equivalence between
types.
- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
their subshapes.
- `04-extension-types.rzk.md` — We use extension extensionality.
- `03-extension-types.rzk.md` — We use extension extensionality.
- `05-segal-types.rzk.md` - We use the notion of hom types.

Some of the definitions in this file rely on function extensionality and
Expand Down
380 changes: 380 additions & 0 deletions src/simplicial-hott/10-rezk-types.rzk.md
Original file line number Diff line number Diff line change
Expand Up @@ -941,3 +941,383 @@ In particular, every contractible type is Rezk
: is-rezk Unit
:= is-rezk-is-contr Unit (is-contr-Unit)
```

## Representable isomorphisms.

We prove [RS17, Proposition 10.11]. We first need to access the fiberwise
equivalence with no extra data, and then define some helpers.

```rzk
#section representable-isomorphisms

#variable A : U
#variable is-segal-A : is-segal A
#variables a a' : A
#variable ψ : (x : A) → (Equiv (hom A a x) (hom A a' x))

#def map-representable-equiv
: ( x : A) → (hom A a x) → (hom A a' x)
:= \ x → first (ψ x)

#def inverse-representable-equiv
: ( x : A) → (has-inverse (hom A a x) (hom A a' x) (first (ψ x)))
:=
\ x →
has-inverse-is-equiv
( hom A a x)
( hom A a' x)
( first (ψ x))
( second (ψ x))

#def inv-map-representable-equiv uses (A a a' ψ)
: ( x : A) → (hom A a' x) → (hom A a x)
:= \ x → first (inverse-representable-equiv x)

#def arr-map-representable-equiv
: hom A a' a
:= evid A a (hom A a') (map-representable-equiv)

#def arr-inv-map-representable-equiv
: hom A a a'
:= evid A a' (hom A a) (inv-map-representable-equiv)
```

We now show that `#!rzk arrow-map-representable-equiv` has section
`#!rzk arrow-inv-map-representable-equiv`.

```rzk
#def htpy-inv-map-fib-equiv-map-fib-equiv-id uses (A a a' ψ)
: ( x : A)
→ ( homotopy
( hom A a x)
( hom A a x)
( comp
( hom A a x)
( hom A a' x)
( hom A a x)
( inv-map-representable-equiv x)
( map-representable-equiv x))
( identity (hom A a x)))
:= \ x → first (second (inverse-representable-equiv x))
```

We compute the required paths for the section of
`#!rzk arrow-map-representable-equiv`.

```rzk
#def rev-comp-id-comp-arr-inv-map-arr-map-id-a uses (A is-segal-A a a' ψ)
: comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv
=_{ hom A a a}
comp-is-segal A is-segal-A a a a
( comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv)
( id-hom A a)
:=
rev
( hom A a a)
( comp-is-segal A is-segal-A a a a
( comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv)
( id-hom A a))
( comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv)
( comp-id-is-segal A is-segal-A a a
( comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv))

#def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a
uses (A is-segal-A a a' ψ)
: comp-is-segal A is-segal-A a a a
( comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv)
( id-hom A a)
=_{ hom A a a}
comp-is-segal A is-segal-A a a' a
( arr-inv-map-representable-equiv)
( comp-is-segal A is-segal-A a' a a
( arr-map-representable-equiv)
( id-hom A a))
:=
associative-is-segal extext A is-segal-A a a' a a
( arr-inv-map-representable-equiv)
( arr-map-representable-equiv)
( id-hom A a)

#def rev-eq-compute-precomposition-evid-arr-inv-map-representable-equiv
uses (A is-segal-A a a' ψ)
: comp-is-segal A is-segal-A a a' a
( arr-inv-map-representable-equiv)
( comp-is-segal A is-segal-A a' a a
( arr-map-representable-equiv)
( id-hom A a))
=_{ hom A a a}
inv-map-representable-equiv a
( comp-is-segal A is-segal-A a' a a
( arr-map-representable-equiv)
( id-hom A a))
:=
rev
( hom A a a)
( inv-map-representable-equiv a
( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a)))
( comp-is-segal A is-segal-A a a' a
( arr-inv-map-representable-equiv)
( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a)))
( eq-compute-precomposition-evid funext A is-segal-A a' a
( inv-map-representable-equiv)
( a)
( comp-is-segal A is-segal-A a' a a
( arr-map-representable-equiv)
( id-hom A a)))

#def rev-ap-inv-map-representable-equiv uses (A is-segal-A a a' ψ)
: inv-map-representable-equiv a
( comp-is-segal A is-segal-A a' a a
( arr-map-representable-equiv)
( id-hom A a))
=_{ hom A a a}
inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))
:=
ap
( hom A a' a)
( hom A a a)
( comp-is-segal A is-segal-A a' a a
( arr-map-representable-equiv)
( id-hom A a))
( map-representable-equiv a (id-hom A a))
( inv-map-representable-equiv a)
( rev (hom A a' a)
( map-representable-equiv a (id-hom A a))
( comp-is-segal A is-segal-A a' a a
( arr-map-representable-equiv)
( id-hom A a))
( eq-compute-precomposition-evid funext A is-segal-A a a'
( map-representable-equiv)
( a)
( id-hom A a)))

#def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id
: inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))
=_{ hom A a a}
id-hom A a
:= htpy-inv-map-fib-equiv-map-fib-equiv-id a (id-hom A a)
```

Concatenate all the paths above.

```rzk
#def eq-comp-arrow-inv-map-arrow-map-equiv-id-a
uses (extext funext A is-segal-A a a' ψ)
: comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv
=_{ hom A a a}
id-hom A a
:=
quintuple-concat
( hom A a a)
( comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv)
( comp-is-segal A is-segal-A a a a
( comp-is-segal A is-segal-A a a' a
arr-inv-map-representable-equiv
arr-map-representable-equiv)
( id-hom A a))
( comp-is-segal A is-segal-A a a' a
( arr-inv-map-representable-equiv)
( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a)))
( inv-map-representable-equiv a
( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a)))
( inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)))
( id-hom A a)
( rev-comp-id-comp-arr-inv-map-arr-map-id-a)
( assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a)
( rev-eq-compute-precomposition-evid-arr-inv-map-representable-equiv)
( rev-ap-inv-map-representable-equiv)
( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id)
```

Now we give the section of `#!rzk arrow-map-representable-equiv`.

```rzk
#def section-arrow-map-representable-equiv uses (extext funext A is-segal-A a a' ψ)
: Section-arrow A is-segal-A a' a arr-map-representable-equiv
:=
( arr-inv-map-representable-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a)
```

We see that `#!rzk arrow-map-representable-equiv` has retraction
`#!rzk arrow-inv-map-representable-equiv`.

```rzk
#def htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ)
: ( x : A)
→ ( homotopy
( hom A a' x)
( hom A a' x)
( comp
( hom A a' x)
( hom A a x)
( hom A a' x)
( map-representable-equiv x)
( inv-map-representable-equiv x))
( identity (hom A a' x)))
:= \ x → second (second (inverse-representable-equiv x))
```

We compute the required paths for the retraction of
`#!rzk arrow-map-iso-representable`.

```rzk
#def rev-eq-compute-precomposition-evid-map-representable-equiv
uses (A is-segal-A a a' ψ)
: comp-is-segal A is-segal-A a' a a'
arr-map-representable-equiv
arr-inv-map-representable-equiv
=_{ hom A a' a'}
map-representable-equiv a' arr-inv-map-representable-equiv
:=
rev
( hom A a' a')
( map-representable-equiv a' arr-inv-map-representable-equiv)
( comp-is-segal A is-segal-A a' a a'
arr-map-representable-equiv
arr-inv-map-representable-equiv)
( eq-compute-precomposition-evid funext A is-segal-A a a'
map-representable-equiv
a'
arr-inv-map-representable-equiv)

#def rev-ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map
uses (A is-segal-A a a' ψ)
: map-representable-equiv a' arr-inv-map-representable-equiv
=_{ hom A a' a'}
map-representable-equiv a'
( comp-is-segal A is-segal-A a a' a'
( arr-inv-map-representable-equiv)
( id-hom A a'))
:=
ap
( hom A a a')
( hom A a' a')
( arr-inv-map-representable-equiv)
( comp-is-segal A is-segal-A a a' a'
( arr-inv-map-representable-equiv)
( id-hom A a'))
( map-representable-equiv a')
( rev
( hom A a a')
( comp-is-segal A is-segal-A a a' a'
( arr-inv-map-representable-equiv)
( id-hom A a'))
( arr-inv-map-representable-equiv)
( comp-id-is-segal A is-segal-A a a' arr-inv-map-representable-equiv))

#def rev-ap-map-representable-equiv uses (A is-segal-A a a' ψ)
: map-representable-equiv a'
( comp-is-segal A is-segal-A a a' a'
( arr-inv-map-representable-equiv)
( id-hom A a'))
=_{ hom A a' a'}
map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a'))
:=
ap
( hom A a a')
( hom A a' a')
( comp-is-segal A is-segal-A a a' a'
( arr-inv-map-representable-equiv)
( id-hom A a'))
( inv-map-representable-equiv a' (id-hom A a'))
( map-representable-equiv a')
( rev
( hom A a a')
( inv-map-representable-equiv a' (id-hom A a'))
( comp-is-segal A is-segal-A a a' a'
( arr-inv-map-representable-equiv)
( id-hom A a'))
( eq-compute-precomposition-evid funext A is-segal-A a' a
( inv-map-representable-equiv)
( a')
( id-hom A a')))

#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ)
: map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a'))
=_{ hom A a' a'}
id-hom A a'
:= htpy-comp-map-fib-equiv-inv-map-fib-equiv a' (id-hom A a')
```

Concatenate all the paths above.

```rzk
#def eq-comp-arr-map-representable-arr-inv-map-representable-id-a'
uses (funext A is-segal-A a a' ψ)
: comp-is-segal A is-segal-A a' a a'
arr-map-representable-equiv
arr-inv-map-representable-equiv
=_{ hom A a' a'}
id-hom A a'
:=
quadruple-concat
( hom A a' a')
( comp-is-segal A is-segal-A a' a a'
arr-map-representable-equiv
arr-inv-map-representable-equiv)
( map-representable-equiv a' arr-inv-map-representable-equiv)
( map-representable-equiv a'
( comp-is-segal A is-segal-A a a' a'
( arr-inv-map-representable-equiv)
( id-hom A a')))
( map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a')))
( id-hom A a')
( rev-eq-compute-precomposition-evid-map-representable-equiv)
( rev-ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map)
( rev-ap-map-representable-equiv)
( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv)
```

Now we give the retraction of `#!rzk arrow-map-representable-equiv`.

```rzk
#def retraction-arrow-map-representable-equiv uses (funext A is-segal-A a a' ψ)
: Retraction-arrow A is-segal-A a' a arr-map-representable-equiv
:=
( arr-inv-map-representable-equiv
, eq-comp-arr-map-representable-arr-inv-map-representable-id-a')
```

We show that arrows from representable equivalences are isomorphisms, i.e. that
`#!rzk arr-map-representable-equiv` is an isomorphism.

```rzk title="RS17, Proposition 10.11 (i)"
#def representable-isomorphism uses (extext funext A is-segal-A a a' ψ)
: is-iso-arrow A is-segal-A a' a arr-map-representable-equiv
:=
( retraction-arrow-map-representable-equiv
, section-arrow-map-representable-equiv)

#end representable-isomorphisms
```

The second part of Proposition 10.11.

```rzk title="RS17, Proposition 10.11 (ii)"
#def eq-representable-isomorphism uses (extext funext)
( A : U)
( is-rezk-A : is-rezk A)
( a a' : A)
( ψ : (x : A) → (Equiv (hom A a x) (hom A a' x)))
: a' = a
:=
eq-iso-is-rezk A is-rezk-A a' a
( arr-map-representable-equiv A a a' ψ
, representable-isomorphism A (first is-rezk-A) a a' ψ)
```