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

Descent and induction principle of identity types of coequalizers #1140

Draft
wants to merge 10 commits into
base: master
Choose a base branch
from
Prev Previous commit
Next Next commit
Transport in a family of equivalence types
VojtechStep committed May 19, 2024
commit ea3636fd209c1f8fdc37aab910f9d728c0eed1b3
14 changes: 14 additions & 0 deletions src/foundation/equivalences.lagda.md
Original file line number Diff line number Diff line change
@@ -16,6 +16,7 @@ open import foundation.equivalence-extensionality
open import foundation.function-extensionality
open import foundation.functoriality-fibers-of-maps
open import foundation.logical-equivalences
open import foundation.transport-along-identifications
open import foundation.transposition-identifications-along-equivalences
open import foundation.truncated-maps
open import foundation.universal-property-equivalences
@@ -572,6 +573,19 @@ pr1 (equiv-precomp-equiv e C) = _∘e e
pr2 (equiv-precomp-equiv e C) = is-equiv-precomp-equiv-equiv e
```

### Computing transport in a family of equivalence types

```agda
module _
{l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
where

tr-equiv-type :
{x y : A} (p : x = y) (e : B x ≃ C x) →
tr (λ x → B x ≃ C x) p e = equiv-tr C p ∘e e ∘e equiv-tr B (inv p)
tr-equiv-type refl e = eq-htpy-equiv refl-htpy
```

### A cospan in which one of the legs is an equivalence is a pullback if and only if the corresponding map on the cone is an equivalence

```agda