namespace true {
  def0 True : ★ = {true}

  def drop : 0.(A : ★) → True → A → A =
    λ A t x ⇒ case t return A of { 'true ⇒ x }

  def0 eta : (s : True) → s ≡ 'true : True =
    λ s ⇒ case s return s' ⇒ s' ≡ 'true : True of { 'true ⇒ δ 𝑖 ⇒ 'true }

  def0 irr : (s t : True) → s ≡ t : True =
    λ s t ⇒
      coe (𝑖 ⇒ eta s @𝑖 ≡ t : True) @1 @0
        (coe (𝑖 ⇒ 'true ≡ eta t @𝑖 : True) @1 @0 (δ _ ⇒ 'true))
}
def0 True = true.True

namespace false {
  def0 False : ★ = {}

  def void : 0.(A : ★) → 0.False → A =
    λ A v ⇒ case0 v return A of { }

  def0 irr : (u v : False) → u ≡ v : False =
    λ u v ⇒ void (u ≡ v : False) u
}
def0 False = false.False
def void = false.void


def0 Not : ★ → ★ = λ A ⇒ ω.A → False

def0 Iff : ★ → ★ → ★ = λ A B ⇒ (A → B) × (B → A)

def0 All : (A : ★) → (A → ★) → ★ =
  λ A P ⇒ (x : A) → P x

def0 cong :
    (A : ★) → (P : A → ★) → (p : All A P) →
    (x y : A) → (xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) =
  λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖)

def0 cong' :
    (A B : ★) → (f : A → B) →
    (x y : A) → (xy : x ≡ y : A) → f x ≡ f y : B =
  λ A B ⇒ cong A (λ _ ⇒ B)

def0 coherence :
    (A B : ★) → (AB : A ≡ B : ★) → (x : A) →
    Eq (𝑖 ⇒ AB @𝑖) x (coe (𝑖 ⇒ AB @𝑖) x) =
  λ A B AB x ⇒
    δ 𝑗 ⇒ coe (𝑖 ⇒ AB @𝑖) @0 @𝑗 x


def0 eq-f : (A : ★) → (P : A → ★) → (p : All A P) → (q : All A P) → A → ★ =
  λ A P p q x ⇒ p x ≡ q x : P x

def funext :
    0.(A : ★) → 0.(P : A → ★) → 0.(p q : All A P) →
    (All A (eq-f A P p q)) → p ≡ q : All A P =
  λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖

def refl : 0.(A : ★) → (x : A) → x ≡ x : A = λ A x ⇒ δ _ ⇒ x

def sym : 0.(A : ★) → 0.(x y : A) → (x ≡ y : A) → y ≡ x : A =
  λ A x y eq ⇒ coe (𝑗 ⇒ eq @𝑗 ≡ x : A) (δ _ ⇒ eq @0)
    -- btw this uses eq @0 instead of just x because of the quantities

def trans10 : 0.(A : ★) → 0.(x y z : A) →
              1.(x ≡ y : A) → 0.(y ≡ z : A) → x ≡ z : A =
  λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ x ≡ eq2 @𝑗 : A) eq1

def trans01 : 0.(A : ★) → 0.(x y z : A) →
              0.(x ≡ y : A) → 1.(y ≡ z : A) → x ≡ z : A =
  λ A x y z eq1 eq2 ⇒ coe (𝑗 ⇒ eq1 @𝑗 ≡ z : A) @1 @0 eq2

def trans : 0.(A : ★) → 0.(x y z : A) →
            ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
  λ A x y z eq1 eq2 ⇒ trans01 A x y z eq1 eq2

def appω : 0.(A B : ★) → ω.(f : ω.A → B) → [ω.A] → [ω.B] =
  λ A B f x ⇒
  case x return [ω.B] of { [x'] ⇒ [f x'] }

def app2ω : 0.(A B C : ★) → ω.(f : ω.A → ω.B → C) → [ω.A] → [ω.B] → [ω.C] =
  λ A B C f x y ⇒
  case x return [ω.C] of { [x'] ⇒
    case y return [ω.C] of { [y'] ⇒ [f x' y'] }
  }

def getω : 0.(A : ★) → [ω.A] → A =
  λ A x ⇒ case x return A of { [x] ⇒ x }

def0 get0 : (A : ★) → [0.A] → A =
  λ A x ⇒ case x return A of { [x] ⇒ x }

def drop0 : 0.(A B : ★) → [0.A] → B → B =
  λ A B x y ⇒ case x return B of { [_] ⇒ y }

def0 drop0-eq : (A B : ★) → (x : [0.A]) → (y : B) → drop0 A B x y ≡ y : B =
  λ A B x y ⇒
  case x return x' ⇒ drop0 A B x' y ≡ y : B of { [_] ⇒ δ 𝑖 ⇒ y }

def0 HEq : (A B : ★) → A → B → ★¹ =
  λ A B x y ⇒ (AB : A ≡ B : ★) × Eq (𝑖 ⇒ AB @𝑖) x y

def0 boxω-inj : (A : ★) → (x y : A) → [x] ≡ [y] : [ω.A] → x ≡ y : A =
  λ A x y xy ⇒ δ 𝑖 ⇒ getω A (xy @𝑖)

def revive0 : 0.(A : ★) → 0.[0.A] → [0.A] =
  λ A s ⇒ [get0 A s]


def0 Sing : (A : ★) → A → ★ =
  λ A x ⇒ (val : A) × [0. val ≡ x : A]

def sing : 0.(A : ★) → (x : A) → Sing A x =
  λ A x ⇒ (x, [δ _ ⇒ x])

def0 Dup : (A : ★) → A → ★ =
  λ A x ⇒ (x! : [ω.A]) × [0. x! ≡ [x] : [ω.A]]

def dup-from-parts :
    0.(A : ★) →
    (dup : A → [ω.A]) →
    0.(prf : (x : A) → dup x ≡ [x] : [ω.A]) →
    (x : A) → Dup A x =
  λ A dup prf x ⇒ (dup x, [prf x])

def drop-from-dup :
    0.(A : ★) → (A → [ω.A]) → 0.(B : ★) → A → B → B =
  λ A dup B x y ⇒ case dup x return B of { [_] ⇒ y }


def dup0 : 0.(A : ★) → [0.A] → [ω.[0.A]] =
  λ A x ⇒ case x return [ω.[0.A]] of { [x] ⇒ [[x]] }

def0 dup0-ok : (A : ★) → (x : [0.A]) → dup0 A x ≡ [x] : [ω.[0.A]] =
  λ A x ⇒
  case x return x' ⇒ dup0 A x' ≡ [x'] : [ω.[0.A]] of { [x] ⇒ δ 𝑖 ⇒ [[x]] }

def dup0! : 0.(A : ★) → (x : [0.A]) → Dup [0.A] x =
  λ A ⇒ dup-from-parts [0.A] (dup0 A) (dup0-ok A)


namespace sing {

def val : 0.(A : ★) → 0.(x : A) → Sing A x → A =
  λ A x sg ⇒
  case sg return A of { (x', eq) ⇒ drop0 (x' ≡ x : A) A eq x' }

def0 val-fst : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ fst sg : A =
  λ A x sg ⇒ drop0-eq (fst sg ≡ x : A) A (snd sg) (fst sg)

def0 proof : (A : ★) → (x : A) → (sg : Sing A x) → val A x sg ≡ x : A =
  λ A x sg ⇒
  trans A (val A x sg) (fst sg) x
    (val-fst A x sg) (get0 (fst sg ≡ x : A) (snd sg))

def app : 0.(A B : ★) → 0.(x : A) →
          (f : A → B) → Sing A x → Sing B (f x) =
  λ A B x f sg ⇒
  case sg return Sing B (f x) of { (x_, eq) ⇒
    case eq return Sing B (f x) of { [eq] ⇒ (f x_, [δ 𝑖 ⇒ f (eq @𝑖)]) }
  }

}