// 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
);
Created
December 14, 2022 17:38
-
-
Save EduardoRFS/72abb3e89454a7e3a4acd54b59d08713 to your computer and use it in GitHub Desktop.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment