Here is the type of our main thm for elementary equations (Cf Summary.v):
`
Check (@elementary_equations_preserve_initiality :
∏
(Sig : SIGNATURE)
(** The 1-signature must be an epi-signature )
(epiSig : sig_preservesNatEpiMonad Sig)
(* this is implied by the axiom of choice )
(SR_epi : ∏ R : Monad SET, preserves_Epi (Sig R))
(* A family of equations )
(O : UU) (eq : O → elementary_equation (Sig := Sig))
(eq' := fun o => soft_equation_from_elementary_equation epiSig SR_epi (eq o)),
(* If the category of 1-models has an initial object, .. )
∏ (R : Initial (rep_fiber_category Sig)) ,
(* preserving epis (implied by the axiom of choice )
preserves_Epi (InitialObject R : model Sig)
(* .. then the category of 2-models has an initial object *)
→ Initial (precategory_model_equations eq')).
`
Can we show that some of the hypotheses which requires the axiom of choice are true for some cases?
For example, maybe SR_epi cannot be shown, but SR_epi' supposing that R preserves epis can be shown is Sig is algebraic, which may be enough for the theorem.
The initial model of an algebraic signature should also preserves epis I think.
Here is the type of our main thm for elementary equations (Cf Summary.v):
`
Check (@elementary_equations_preserve_initiality :
∏
(Sig : SIGNATURE)
(** The 1-signature must be an epi-signature )
(epiSig : sig_preservesNatEpiMonad Sig)
(* this is implied by the axiom of choice )
(SR_epi : ∏ R : Monad SET, preserves_Epi (Sig R))
(* A family of equations )
(O : UU) (eq : O → elementary_equation (Sig := Sig))
(eq' := fun o => soft_equation_from_elementary_equation epiSig SR_epi (eq o)),
(* If the category of 1-models has an initial object, .. )
∏ (R : Initial (rep_fiber_category Sig)) ,
(* preserving epis (implied by the axiom of choice )
preserves_Epi (InitialObject R : model Sig)
(* .. then the category of 2-models has an initial object *)
→ Initial (precategory_model_equations eq')).
`
Can we show that some of the hypotheses which requires the axiom of choice are true for some cases?
For example, maybe SR_epi cannot be shown, but SR_epi' supposing that R preserves epis can be shown is Sig is algebraic, which may be enough for the theorem.
The initial model of an algebraic signature should also preserves epis I think.