Skip to content

Commit

Permalink
Redefine equiv-eq as equiv-tr id (#1020)
Browse files Browse the repository at this point in the history
Hopefully, this gives us some computational benefits.
  • Loading branch information
fredrik-bakke authored Feb 6, 2024
1 parent 9b1707d commit 518f41e
Show file tree
Hide file tree
Showing 6 changed files with 100 additions and 17 deletions.
89 changes: 77 additions & 12 deletions src/foundation-core/univalence.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,44 +9,89 @@ module foundation-core.univalence where
```agda
open import foundation.action-on-identifications-functions
open import foundation.fundamental-theorem-of-identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families
open import foundation-core.transport-along-identifications
```

</details>

## Idea

The univalence axiom characterizes the identity types of universes. It asserts
that the map `Id A B A ≃ B` is an equivalence.
The {{#concept "univalence axiom" Disambiguation="types" Agda=univalence-axiom}}
characterizes the [identity types](foundation-core.identity-types.md) of
universes. It asserts that the map `(A = B) (A ≃ B)` is an equivalence.

In this file, we define the statement of the axiom. The axiom itself is
postulated in [`foundation.univalence`](foundation.univalence.md) as
`univalence`.

## Statement
Univalence is postulated by stating that the canonical comparison map

```text
equiv-eq : A = B A ≃ B
```

from identifications between two types to equivalences between them is an
equivalence. Although we could define `equiv-eq` by pattern matching, due to
computational considerations, we define it as

```text
equiv-eq := equiv-tr (id_𝒰).
```

It follows from this definition that `equiv-eq refl ≐ id-equiv`, as expected.

## Definitions

### Equalities induce equivalences

```agda
equiv-eq : {l : Level} {A : UU l} {B : UU l} A = B A ≃ B
equiv-eq refl = id-equiv
module _
{l : Level}
where

equiv-eq : {A B : UU l} A = B A ≃ B
equiv-eq = equiv-tr id

map-eq : {l : Level} {A : UU l} {B : UU l} A = B A B
map-eq = map-equiv ∘ equiv-eq
map-eq : {A B : UU l} A = B A B
map-eq = map-equiv ∘ equiv-eq

compute-equiv-eq-refl :
{A : UU l} equiv-eq (refl {x = A}) = id-equiv
compute-equiv-eq-refl = refl
```

### The statement of the univalence axiom

#### An instance of univalence

```agda
instance-univalence : {l : Level} (A B : UU l) UU (lsuc l)
instance-univalence A B = is-equiv (equiv-eq {A = A} {B = B})
```

#### Based univalence

```agda
based-univalence-axiom : {l : Level} (A : UU l) UU (lsuc l)
based-univalence-axiom {l} A = (B : UU l) instance-univalence A B
```

#### The univalence axiom with respect to a universe level

```agda
univalence-axiom-Level : (l : Level) UU (lsuc l)
univalence-axiom-Level l = (A B : UU l) instance-univalence A B
```

#### The univalence axiom

```agda
univalence-axiom : UUω
univalence-axiom = {l : Level} univalence-axiom-Level l
```
Expand Down Expand Up @@ -75,11 +120,31 @@ abstract
fundamental-theorem-id c (λ B equiv-eq)
```

### Computing transport
### The underlying map of `equiv-eq` evaluated at `ap B` is the same as transport in the family `B`

For any type family `B` and identification `p : x = y` in the base, we have a
commuting diagram

```text
equiv-eq
(B x = B y) ---------> (B x ≃ B y)
∧ |
ap B p | | map-equiv
| ∨
(x = y) -----------> (B x → B y).
tr B p
```

```agda
compute-equiv-eq-ap :
module _
{l1 l2 : Level} {A : UU l1} {B : A UU l2} {x y : A}
(p : x = y) map-equiv (equiv-eq (ap B p)) = tr B p
compute-equiv-eq-ap refl = refl
where

compute-equiv-eq-ap :
(p : x = y) equiv-eq (ap B p) = equiv-tr B p
compute-equiv-eq-ap refl = refl

compute-map-eq-ap :
(p : x = y) map-eq (ap B p) = tr B p
compute-map-eq-ap p = ap map-equiv (compute-equiv-eq-ap p)
```
8 changes: 8 additions & 0 deletions src/foundation/preunivalent-type-families.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,14 @@ is-preunivalent {A = A} B = (x y : A) → is-emb (λ (p : x = y) → equiv-tr

## Properties

### The preunivalence axiom states that the identity family `id : 𝒰 𝒰` is preunivalent

```agda
is-preunivalent-UU :
(l : Level) is-preunivalent (id {A = UU l})
is-preunivalent-UU l = preunivalence
```

### Assuming the preunivalence axiom, type families are preunivalent if and only if they are faithful as maps

**Proof:** We have the
Expand Down
5 changes: 3 additions & 2 deletions src/foundation/transport-along-identifications.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ open import foundation-core.transport-along-identifications public
<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels

Expand Down Expand Up @@ -43,10 +44,10 @@ module _
inv-tr : x = y B y B x
inv-tr p = tr B (inv p)

is-retraction-inv-tr : (p : x = y) (inv-tr p ∘ tr B p) ~ id
is-retraction-inv-tr : (p : x = y) inv-tr p ∘ tr B p ~ id
is-retraction-inv-tr refl b = refl

is-section-inv-tr : (p : x = y) (tr B p ∘ inv-tr p) ~ id
is-section-inv-tr : (p : x = y) tr B p ∘ inv-tr p ~ id
is-section-inv-tr refl b = refl

is-equiv-tr : (p : x = y) is-equiv (tr B p)
Expand Down
4 changes: 2 additions & 2 deletions src/foundation/univalence.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -181,10 +181,10 @@ compute-eq-equiv-comp-equiv f g =
( λ e map-equiv e (g ∘e f))
( inv (right-inverse-law-equiv equiv-univalence))))))

compute-equiv-eq-ap-inv :
compute-map-eq-ap-inv :
{l1 l2 : Level} {A : UU l1} {B : A UU l2} {x y : A} (p : x = y)
map-eq (ap B (inv p)) ∘ map-eq (ap B p) ~ id
compute-equiv-eq-ap-inv refl = refl-htpy
compute-map-eq-ap-inv refl = refl-htpy

commutativity-inv-equiv-eq :
{l : Level} {A B : UU l} (p : A = B)
Expand Down
9 changes: 9 additions & 0 deletions src/foundation/univalent-type-families.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ open import foundation.universal-property-identity-systems
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.sections
open import foundation-core.torsorial-type-families
Expand Down Expand Up @@ -76,6 +77,14 @@ univalent-type-family l2 A = Σ (A → UU l2) is-univalent

## Properties

### The univalence axiom states that the identity family `id : 𝒰 𝒰` is univalent

```agda
is-univalent-UU :
(l : Level) is-univalent (id {A = UU l})
is-univalent-UU l = univalence
```

### Assuming the univalence axiom, type families are univalent if and only if they are embeddings as maps

**Proof:** We have the
Expand Down
2 changes: 1 addition & 1 deletion src/synthetic-homotopy-theory/descent-circle.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -330,7 +330,7 @@ module _
eq-equiv-descent-data-circle
( descent-data-family-circle l A)
( comparison-descent-data-circle l2 (ev-free-loop l (UU l2) A))
( id-equiv , (htpy-eq (inv (compute-equiv-eq-ap (loop-free-loop l)))))
( id-equiv , (htpy-eq (inv (compute-map-eq-ap (loop-free-loop l)))))

is-equiv-descent-data-family-circle-universal-property-circle :
( up-circle : universal-property-circle (lsuc l2) l)
Expand Down

0 comments on commit 518f41e

Please sign in to comment.