⚠️ Archived site. This is the pre-3.0 Agda Universal Algebra Library, preserved for reference. Its current home is agda-algebras.universalalgebra.org (as of July 2026).

{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness --no-subtyping #-} module Agda.Builtin.Cubical.Path where open import Agda.Primitive.Cubical postulate PathP : ∀ {ℓ } (A : I → Set ℓ ) → A i0 → A i1 → Set ℓ {-# BUILTIN PATHP PathP #-} infix 4 _≡_ -- We have a variable name in `(λ i → A)` as a hint for case -- splitting. _≡_ : ∀ {ℓ } {A : Set ℓ } → A → A → Set ℓ _≡_ {A = A } = PathP (λ i → A ) {-# BUILTIN PATH _≡_ #-}