load "misc.quox";

namespace bool {

def0 Bool : ★⁰ = {true, false};

def boolω : 1.Bool → [ω.Bool] =
  λ b ⇒ case1 b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] };

def if : 0.(A : ★⁰) → 1.Bool → ω.A → ω.A → A =
  λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f };

-- [todo]: universe lifting
def0 If : 1.Bool → 0.★⁰ → 0.★⁰ → ★⁰ =
  λ b T F ⇒ case1 b return ★⁰ of { 'true ⇒ T; 'false ⇒ F };

def0 T : ω.Bool → ★⁰ = λ b ⇒ If b True False;

def true-not-false : Not ('true ≡ 'false : Bool) =
  λ eq ⇒ coe (i ⇒ T (eq @i)) 'true;


-- [todo] infix
def and : 1.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false;
def or  : 1.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b;

}

def0 Bool = bool.Bool;