weak_self_types.md

// computing
C_bool = (A : Type) -> A -> A -> A;
(c_true : C_bool) = A => t => f => t;
(c_false : C_bool) = A => t => f => f;

// induction
I_bool b = (P : C_bool -> Type) -> P c_true -> P c_false -> P b;
i_true : I_bool c_true = P => p_t => p_f => p_t;
i_false : I_bool c_false = P => p_t => p_f => p_f;

// template
T_bool Rel = {
  comp : C_bool;
  ind : Ind_bool b;
  rel : Rel;
};

Bool = @Self((A : Type) => (self : T_bool A) => (x : T_bool A) -> self.comp == x.comp -> self == x);
true = %Self((self : Bool) => {
  comp = c_true;
  ind = i_true;
  rel = x => self_comp_eq_x_comp => (
    x_comp_eq_self_comp = symm self_comp_eq_x_comp;
    x_eq_self = x.rel self x_comp_eq_self_comp;
    symm x_eq_self
  );
});
false = %Self((self : Bool) => {
  comp = c_false;
  ind = i_false;
  rel = x => self_comp_eq_x_comp => (
    x_comp_eq_self_comp = symm self_comp_eq_x_comp;
    x_eq_self = x.rel self x_comp_eq_self_comp;
    symm x_eq_self
  );
});
ind_bool = b => (P : Bool -> Type) => (p_t : P true) => (p_f : P false) : P b => (
  (m, b_comp_eq_m_comp, p_m) =
    b.ind
      (x => {m : Bool; x_eq_m_comp : x == m.comp; p_m : P m})
      (true, refl, p_t)
      (false, refl, p_f);
  b_eq_m = b.rel b_comp_eq_m_comp;
  m_eq_b = symm b_eq_m;
  subst m_eq_b (x => P x) p_m
);