{-# 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         _≡_     #-}