dependent_elimination.md

refl : {A} -> A == A = _;
C_bool = {A} -> A -> A -> A;
c_true : C_bool = {A} => t => f => t;
c_false : C_bool = {A} => t => f => f;

Ind_bool : C_bool -> Type =
  b => {P} -> P c_true -> P c_false -> P b;
ind_true : Ind_bool c_true = {P} => t => f => t;
ind_false : Ind_bool c_false = {P} => t => f => f;

Bool : Type = (b : C_bool) & Ind_bool b;
true : Bool = (b = c_true & ind_true);
false : Bool = (b = c_false & ind_false);

ind_bool : (b : Bool) -> {P} -> P true -> P false -> P b =
  b => {P} => t => f => (
    f : {X} -> ((m : Bool) -> b.1 == m.1 -> P m -> X) -> X =
      @b.2
        (x => {X} -> ((m : Bool) -> x == m.1 -> P m -> X) -> X)
        ({X} => c => c true refl t)
        ({X} => c => c false refl f);
    f (m => (e : b.1 == m.1) => (u : P m) =>
      e : b == m = e; // injective
      u[m := b | e]
    )
);

match_bool_with_eq :
  {A} -> (b : Bool) ->
  (t : (b == true) -> A) ->
  (f : (b == false) -> A) -> A =
  {A} => b =>
    @ind_bool b
      (m =>
        (t : (m == true) -> A) ->
        (f : (m == false) -> A) -> A)
      (t => f => t refl)
      (t => f => f refl);
simple_dependent_elimination = (tag : Bool) => (payload : tag Type Int String) => (
  @ind_bool tag
    (tag => (payload : tag Type Int String) -> String)
    (payload => Int.to_string payload)
    (payload => payload);
    payload
);