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

module Path where

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

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

infixr  _⨾_
_⨾_ : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_⨾_ = Cubical.Foundations.Prelude._∙_

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

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

syntax PathP-syntax (λ i → Ty) lhs rhs = lhs ≡[ i ≔ Ty ]≡ rhs

cong₂ : (f : A → B → C)
      → {x x′ : A}
      → {y y′ : B}
      → x ≡ x′
      → y ≡ y′
      → f x y ≡ f x′ y′
cong₂ f x y i = f (x i) (y i)

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 i = f (x i) (y i) (z i)