{-# OPTIONS --cubical --safe #-}

module Path where

open import Cubical.Foundations.Everything
  using ( _≡_
        ; sym
        ; refl
        ; subst
        ; transport
        ; Path
        ; PathP
        ; I
        ; i0
        ; i1
        ; funExt
        ; cong
        ; toPathP
        ; cong₂
        ; ~_
        ; _∧_
        ; _∨_
        ; hcomp
        ; transp
        ; J
        )
  renaming
    ( subst2 to subst₂
    ; congS to cong′
    )
  public

open import Data.Empty using (¬_)
open import Level

infixr 2 _;_
_;_ : {x y z : A}  x  y  y  z  x  z
_;_ = Cubical.Foundations.Everything._∙_

infix 4 _≢_
_≢_ : {A : Type a}  A  A  Type a
x  y = ¬ (x  y)

infix 4 PathP-syntax
PathP-syntax = PathP
{-# DISPLAY PathP-syntax = PathP #-}

syntax PathP-syntax  i  Ty) lhs rhs = lhs ≡[ i  Ty ]≡ rhs

cong₃ :  {d} {D : Type d}
       (f : A  B  C  D)
       {x x′ : A}
       {y y′ : B}
       {z z′ : C}
       x  x′
       y  y′
       z  z′
       f x y z  f x′ y′ z′
cong₃ f x y z = cong₂  f x  f x) (cong₂ f x y) z