{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Cubical.Id where

  open import Agda.Primitive.Cubical
  open import Agda.Builtin.Cubical.Path
  open import Agda.Builtin.Cubical.Sub renaming (primSubOut to ouc; Sub to _[_↦_])

  postulate
    Id :  {} {A : Set }  A  A  Set 

  {-# BUILTIN ID           Id       #-}
  {-# BUILTIN CONID        conid    #-}

  -- Id x y is treated as a pair of I and x ≡ y, using "i" for the
  -- first component and "p" for the second.
  {-# COMPILE JS conid =
      _ => _ => _ => _ => i => p => { return { "i" : i, "p" : p } }
    #-}

  primitive
    primDepIMin : _
    primIdFace :  {} {A : Set } {x y : A}  Id x y  I
    primIdPath :  {} {A : Set } {x y : A}  Id x y  x  y

  primitive
    primIdJ :  { ℓ'} {A : Set } {x : A} (P :  y  Id x y  Set ℓ') 
                P x (conid i1  i  x))   {y} (p : Id x y)  P y p


  primitive
    primIdElim :  {a c} {A : Set a} {x : A}
                   (C : (y : A)  Id x y  Set c) 
                   ((φ : I) (y : A [ φ   _  x) ])
                    (w : (x  ouc y) [ φ   { (φ = i1)  \ _  x}) ]) 
                    C (ouc y) (conid φ (ouc w))) 
                   {y : A} (p : Id x y)  C y p