Crisp identity types
Content created by Fredrik Bakke.
Created on 2023-11-24.
Last modified on 2023-11-24.
{-# OPTIONS --cohesion --flat-split #-} module modal-type-theory.crisp-identity-types where
Idea
We record here some basic facts about identity types in crisp contexts.
Properties
ind-path-crisp : {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {@♭ a : A} → (C : (@♭ y : A) (p : a = y) → UU l2) → C a refl → (@♭ y : A) (@♭ p : a = y) → C y p ind-path-crisp C b _ refl = b ap-crisp : {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {B : UU l2} {@♭ x y : A} (f : (@♭ x : A) → B) → @♭ (x = y) → (f x) = (f y) ap-crisp f refl = refl
Recent changes
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).