Univalent type families
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.
Created on 2022-03-03.
Last modified on 2023-09-11.
module foundation.univalent-type-families where
Imports
open import foundation.transport-along-identifications open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.identity-types
Idea
A type family B
over A
is said to be univalent if the map
equiv-tr : (Id x y) → (B x ≃ B y)
is an equivalence for every x y : A
.
Definition
is-univalent : {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2) is-univalent {A = A} B = (x y : A) → is-equiv (λ (p : x = y) → equiv-tr B p)
Recent changes
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622).