iup_induction.md

// Church booleans
C_bool : Type 1 = (L : Level) -> (A : Type L) -> A -> A -> A;
c_true : Bool = L => A => t => f => t;
c_false : Bool = L => A => t => f => f;

// Induction principle
I_bool = b : Type 1 => (L : Level) -> (P : C_bool -> Type L) -> P c_true -> P c_false -> P b;
// Without IUP, Bool would be placed on Type Omega, making it useless
Bool : Type 1 = (b : Bool) & (ind : I_bool b);
true : Bool = L => X => t => f => t;
false : Bool = L => X => t => f => t;

ind_bool : (b : Bool) -> (L : Level) -> (P : Bool -> Type L) -> P true -> P false -> P b =
  b => L => P => p_t => p_f => (
    (m, b1_eq_m1, p_m) =
      b.2
        L
        (x => (m : Bool, x_eq_m1 : x == m.1, p_m : P m))
        (true, refl, p_t)
        (false, refl, p_f);
    // b.1 == m.1 implies in b == m
    b_eq_m : b == m = b1_eq_m1;
    // use b == m to change P m into P b
    (p_m : _[m := b | b_eq_m]);
);