{-# OPTIONS -WUnsupportedIndexedMatch #-} open import 1Lab.Path.IdentitySystem.Interface open import 1Lab.Path.IdentitySystem open import 1Lab.Univalence open import 1Lab.HLevel open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type open import Data.Dec.Base module Data.Id.Base where
Inductive identity🔗
In cubical type theory, we generally use the path types to represent identifications. But in cubical type theory with indexed inductive types, we have a different — but equivalent — choice: the inductive identity type.
data _≡ᵢ_ {ℓ} {A : Type ℓ} (x : A) : A → Type ℓ where reflᵢ : x ≡ᵢ x
To show that
is equivalent to
for every type
,
we’ll show that _≡ᵢ_ and reflᵢ form an identity system regardless of
the underlying type. Since Id
is an
inductive type, we can do so by pattern matching, which results in a
very slick definition:
Id-identity-system : ∀ {ℓ} {A : Type ℓ} → is-identity-system (_≡ᵢ_ {A = A}) (λ _ → reflᵢ) Id-identity-system .to-path reflᵢ = refl Id-identity-system .to-path-over reflᵢ = refl
Paths are, in many ways, more convenient than the inductive identity type: as a (silly) example, for paths, we have definitionally. But the inductive identity type has one property which sets it apart from paths: regularity. Transport along the reflexivity path is definitionally the identity:
substᵢ : ∀ {ℓ ℓ′} {A : Type ℓ} (P : A → Type ℓ′) {x y : A} → x ≡ᵢ y → P x → P y substᵢ P reflᵢ x = x _ : ∀ {ℓ} {A : Type ℓ} {x : A} → substᵢ (λ x → x) reflᵢ x ≡ x _ = refl
In the 1Lab, we prefer _≡_ over
_≡ᵢ_ — which is why there is no
comprehensive toolkit for working with the latter. But it can still be
used when we want to avoid transport along reflexivity, for
example, when working with decidable equality of concrete (indexed)
types like Fin
.
Discreteᵢ : ∀ {ℓ} → Type ℓ → Type ℓ Discreteᵢ A = (x y : A) → Dec (x ≡ᵢ y) Discreteᵢ→discrete : ∀ {ℓ} {A : Type ℓ} → Discreteᵢ A → Discrete A Discreteᵢ→discrete d x y with d x y ... | yes reflᵢ = yes refl ... | no ¬x=y = no λ p → ¬x=y (Id≃path.from p) is-set→is-setᵢ : ∀ {ℓ} {A : Type ℓ} → is-set A → (x y : A) (p q : x ≡ᵢ y) → p ≡ q is-set→is-setᵢ A-set x y p q = Id≃path.injective (A-set _ _ _ _) ≡ᵢ-is-hlevel' : ∀ {ℓ} {A : Type ℓ} {n} → is-hlevel A (suc n) → (x y : A) → is-hlevel (x ≡ᵢ y) n ≡ᵢ-is-hlevel' {n = n} ahl x y = subst (λ e → is-hlevel e n) (sym (ua Id≃path)) (Path-is-hlevel' n ahl x y)