The summary file should state the main theorems outside any section, that is, with all the hypotheses inside the statement of the theorem.

For its proof, it can apply the theorem proved in another file.

To be more precise, how do I tell the satellite repository where the UniMath build resides?
Currently, there is only an instruction for using make, based on an "installed" UniMath (and I know how to "install" UniMath from the Dune build by creating a TAR file of the .vo files and injecting it).

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.

I am seeing this:

$ make
COQC Modules/Signatures/BindingSig.v
File "./Modules/Signatures/BindingSig.v", line 205, characters 8-31:
Error:
Found no subterm matching "foldr1_map ?M43 ?M44 ?M45
                             (cons ?M46 (cons ?M47 ?M48))" in the current goal.

make[1]: *** [build/CoqMakefile.make:848: Modules/Signatures/BindingSig.vo] Error 1
make[1]: *** [Modules/Signatures/BindingSig.vo] Deleting file 'Modules/Signatures/BindingSig.glob'
make: *** [build/CoqMakefile.make:417: all] Error 2

@rmatthes : do you see the same?

Can wait until later....

Compilation error after upgrade to Coq 8.11:

File "./Modules/Signatures/ModelCat.v", line 726, characters 14-79:
Error: Cannot infer this placeholder of type "Monad C" in
environment:
C : category
bc : BinCoproducts C
Sig : signature C
R : model Sig
iR : isInitial (rep_fiber_category Sig) R
fR := iscontrpr1 (iR (mod_id_model R)) : rep_fiber_mor R (mod_id_model R)
h1 : fR · mod_id_model_mor R = identity R
c : C

@amblafont : can you fix this?

Rename old arities into half-arities
aritiesalt -> Half Arities

We should use the main result to construct some initial objects, e.g., the initial object of the signature LC+beta+eta.

This will show if our definitions are chosen well.

Many simpl. and cbn. now unfold too much, hence take ages, following a change in UniMath/UniMath where proofs of categorical axioms have been transparencified (UniMath/UniMath#1030).

Here is the bug report: UniMath/UniMath#1036

Like the definition of a quotient functor, a quotient monad (on sets) only seems to rely on two pieces of input:

• a monad
• a pointwise relation

Factor out this construction.

Error:
Ltac call to "simple refine (uconstr)" failed.
In environment
C : category
F := left_adjoint TwoSignature_To_One_right_adjoint
 : signature_category ⟶ total_precategory two_signature_disp
The term "F" has type
 "signature_category ⟶ total_precategory two_signature_disp"
while it is expected to have type "signature_category ⟶ ?D".

The problem here is that isounit_coreflection requires a functor between categories, whereas left_adjoint only gives a functor between precategories.