public open import Primitives using
  ( Partial
  , coe
  , Sub
  , inS
  , outS
  )
public open import Intervals

variable A B C D : Type
def Path (A : I → Type) (a : A 0) (b : A 1) : Type ⇒ ⟦ i ⟧ A i { ~ i := a | i := b }
def Eq (A : Type) (a b : A) : Type ⇒ Path (\ i ⇒ A) a b
def infix = {A : Type} ⇒ Eq A looser ~
def idp {a : A} : a = a ⇒ \i ⇒ a
def funExt (f g : A → B) (p : ∀ a → f a = g a) : f = g ⇒ \i a ⇒ p a i
def pmap (f : A → B) {a b : A} (p : a = b) : f a = f b ⇒ \i ⇒ f (p i)
def sym (p : ⟦ i ⟧ A) : p 1 = p 0 ⇒ \i ⇒ p (~ i)

def isContr (A : Type) ⇒ Σ (a : A) ** (∀ b → a = b)

/// Carlo Angiuli's PhD thesis, Section 3.2
module Angiuli {
  def transport {a b : A} (B : A → Type) (p : a = b) (x : B a) : B b
    ⇒ coe 0 1 (\y ⇒ B (p y)) x

  def IdSys (a : A) ⇒ ⟦ i ⟧ A { ~ i := a }

  def uniqueness (a : A) : isContr (IdSys a)
    ⇒ (idp,  \ b i j ⇒ coe 0 j (\k ⇒ a = b k) idp i)

  def J {a : A} (B : IdSys a → Type)
      (r : B idp) (b : IdSys a) : B b ⇒
      transport B ((uniqueness a).2 b) r
}

public open Angiuli using (transport, J)

// Bye, regularity!
// def Jβ {a : A} (B : ∀ b -> a = b -> Type)
//         (r : B a idp) : J B r idp = r => idp

def funExt2 (f g : A → B → C) (p : ∀ a b → f a b = g a b) : f = g
  ⇒ \ i a b ⇒ p a b i

def funExt3 (f g : A → B → C → D) (p : ∀ a b c → f a b c = g a b c) : f = g
  ⇒ \ i a b c ⇒ p a b c i

// The most general path mapping
def pmapd {A : I → Type} (B : ∀ i → A i → Type)
    (f : ∀ i → ∀ (a : A i) → B i a)
    (p : ⟦ i ⟧ A i)
  : ⟦ i ⟧ B i (p i) { ~ i := f 0 (p 0) | i := f 1 (p 1) } ⇒ \ i ⇒ f i (p i)

def hcomp2d
  {c d : A}
  (p : ⟦ i ⟧ A)
  (q : p 1 = d)
  (r : p 0 = c) : c = d
  ⇒ coe 0 1 (\ k ⇒ r k = q k) p

def <=3=> {c d : A} (p : ⟦ i ⟧ A) (q : p 1 = c) (r : c = d) : p 0 = d ⇒
  hcomp2d q r (sym p)

def infixr <==>
  (p : ⟦ i ⟧ A)
  (q : ⟦ i ⟧ A { ~ i := p 1 })
  : p 0 = q 1 ⇒ <=3=> idp p q
  tighter =