Skip to content
Permalink
master
Switch branches/tags
Go to file
 
 
Cannot retrieve contributors at this time
{- This file exports the primitives of cubical Id types -}
{-# OPTIONS --safe #-}
module Cubical.Core.Id where
open import Cubical.Core.Primitives hiding ( _≡_ )
open import Agda.Builtin.Cubical.Id public
renaming ( conid to ⟨_,_⟩
-- TODO: should the user really be able to access these two?
; primIdFace to faceId -- ∀ {ℓ} {A : Type ℓ} {x y : A} → Id x y → I
; primIdPath to pathId -- ∀ {ℓ} {A : Type ℓ} {x y : A} → Id x y → Path A x y
; primIdElim to elimId -- ∀ {ℓ ℓ'} {A : Type ℓ} {x : A}
-- (P : ∀ (y : A) → x ≡ y → Type ℓ')
-- (h : ∀ (φ : I) (y : A [ φ ↦ (λ _ → x) ])
-- (w : (Path _ x (outS y)) [ φ ↦ (λ { (φ = i1) → λ _ → x}) ] ) →
-- P (outS y) ⟨ φ , outS w ⟩) →
-- {y : A} (w' : x ≡ y) → P y w'
)
hiding ( primIdJ ) -- this should not be used as it is using compCCHM
{- BUILTIN ID Id -}
_≡_ : {ℓ} {A : Type ℓ} A A Type ℓ
_≡_ = Id