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:

  :  {} {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)
discrete-id :  {} {A : Type } {x y : A}  Dec (x  y)  Dec (x ≡ᵢ y)
discrete-id {x = x} {y} (yes p) = yes (subst (x ≡ᵢ_) p reflᵢ)
discrete-id {x = x} {y} (no ¬p) = no λ { reflᵢ  absurd (¬p refl) }

  _≡ᵢ?_ :  {} {A : Type }  _ : Discrete A  (x y : A)  Dec (x ≡ᵢ y)
  x ≡ᵢ? y = discrete-id (x ≡? y)

  ≡ᵢ?-default :  {} {A : Type } {x y : A} {d : Discrete A}  (_≡ᵢ?_  d  x y) ≡rw discrete-id d
  ≡ᵢ?-default = make-rewrite refl

  ≡ᵢ?-yes :  {} {A : Type } {x : A} {d : Discrete A}  (_≡ᵢ?_  d  x x) ≡rw yes reflᵢ
  ≡ᵢ?-yes {d = d} = make-rewrite (case d return  d  discrete-id d  yes reflᵢ) of λ where
    (yes a)  ap yes (is-set→is-setᵢ (Discrete→is-set d) _ _ _ _)
    (no ¬a)  absurd (¬a refl))

{-# REWRITE ≡ᵢ?-default ≡ᵢ?-yes #-}

  :  { ℓ'} {A : Type } {B : Type ℓ'} (f : A  B)
   (∀ {x y}  f x ≡ᵢ f y  x ≡ᵢ y)
    _ : Discrete B 
   Discrete A
Discrete-inj' f inj {x} {y} =
  Dec-map  p  Id≃ (inj p))  x  Id≃path.from (ap f x)) (f x ≡ᵢ? f y)

    :  { ℓ'} {A : Type } {B : A  Type ℓ'}
      _ : Discrete A 
      _ :  {x}  Discrete (B x) 
     Discrete (Σ A B)
  Discrete-Σ {B = B} {x = a , b} {a' , b'} = case a ≡ᵢ? a' of λ where
    (yes reflᵢ)  case b ≡? b' of λ where
      (yes q)  yes (ap₂ _,_ refl q)
      (no ¬q)  no λ p  ¬q (Σ-inj-set (Discrete→is-set auto) p)
    (no ¬p)  no λ p  ¬p (Id≃path.from (ap fst p))

abstract instance
    :  { n} {S : Type }  s : H-Level S (suc n)  {x y : S}
     H-Level (x ≡ᵢ y) n
  H-Level-Id {n = n} = hlevel-instance (Equiv→is-hlevel n Id≃path (hlevel n))

  :  { ℓ'} {A : Type } (P : A  Type ℓ')
   is-set A
   {a : A}
   (p : a ≡ᵢ a)
    x  x  substᵢ P p x
substᵢ-filler-set P is-set-A p x = subst  q  x  substᵢ P q x) (is-set→is-setᵢ is-set-A _ _ reflᵢ p) refl

record Recallᵢ
  {a b} {A : Type a} {B : A  Type b}
  (f : (x : A)  B x) (x : A) (y : B x)
  : Type (a  b)
    constructor ⟪_⟫ᵢ
      eq : f x ≡ᵢ y

  :  {a b} {A : Type a} {B : A  Type b}
   (f : (x : A)  B x) (x : A)
   Recallᵢ f x (f x)
recallᵢ f x =  reflᵢ ⟫ᵢ

symᵢ :  {a} {A : Type a} {x y : A}  x ≡ᵢ y  y ≡ᵢ x
symᵢ reflᵢ = reflᵢ

_∙ᵢ_ :  {a} {A : Type a} {x y z : A}  x ≡ᵢ y  y ≡ᵢ z  x ≡ᵢ z
reflᵢ ∙ᵢ q = q

  :  { ℓ'} {A : Type } {x : A} (P : (y : A)  x ≡ᵢ y  Type ℓ')
   P x reflᵢ
    {y} (p : x ≡ᵢ y)
   P y p
Jᵢ P prefl reflᵢ = prefl