{- This file exports the primitives of cubical Id types -} {-# OPTIONS --cubical --no-import-sorts --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