The results of my internship

[AextraT]

M Types in the case of Sets

[rmatthes]

only on omega-continuity

[rmatthes]

I would add "set-based" somewhere.

[rmatthes]

This would be better a local definition - the name is just too short for the global name space.

This for all names that are not telling at all out of context.

[rmatthes]

This should now have a name for the outside world.

[rmatthes]

this is in the library as pathsinv0, please use that one

[rmatthes]

various comments on different files

[rmatthes]

I now this should be ended by Defined.

[rmatthes]

Why F' in the name?

[rmatthes]

This already exists as TerminalHSET in UniMath.CategoryTheory.Categories.HSET.Limits. Please replace.

[rmatthes]

It should say more what is done in this file. It starts set-based just assuming a final coalgebra there and still uses ComputationalM to get the computation rule.

[rmatthes]

In this part, I think there should be much more type info - so that one can relate all these items and see where the good rule is obtained.

[rmatthes]

Suggested change

	(** ** Exemple of construction of M Types using ComputationalMWithSets
	(** ** Example of construction of M Types using ComputationalMWithSets

[rmatthes]

Suggested change

	(* The final coalgebra obtained corresponds to the type of possibly infinite binary trees labeled with booleands. *)
	(* The final coalgebra obtained corresponds to the type of possibly infinite binary trees labeled with booleans. *)

[rmatthes]

Also in this part, I would hope for some more types.

[rmatthes]

In the time of the UniMath schools, this assert would not have worked because that list would not have been available in the sequel. The way out was transparent assert. Rocq has moved on...

[rmatthes]

I comment on the adjunction part: what is the advantage of having the dedicated file FunctorCoalgebras_legacy_alt_HSET.v ? Of course, this is then in parallel with the UU version. But the notion of morphism is not essentially changed w.r.t. FunctorCoalgebras.CoAlg_category F'. And being so inessential can be expressed by having weakly equivalent hom types, as follows:

Definition cat2_not_really_a_variant_of_coalgHSET (C1 C2 : cat2): cat2⟦C1, C2⟧ ≃ FunctorCoalgebras.CoAlg_category F' ⟦C1, C2⟧.
    Proof.
      use weq_iso.
      - intros [f Hyp].
        exists f.
        apply funextfun.
        intro x.
        simple refine (factor_through_squash _  _ (Hyp x)).
        + apply setproperty.
        + trivial.
      - intros [f Hyp].
        exists f.
        intro x.
        apply hinhpr.
        apply (toforallpaths _ _ _ Hyp).
      - intros [f Hyp].
        use total2_paths_f.
        + apply idpath.
        + show_id_type.
          assert (aux : isaprop TYPE).
          { apply impred.
            intro x.
            apply isapropishinh.
          }
          apply aux.
      - intros [f Hyp].
        use total2_paths_f.
        + apply idpath.
        + show_id_type.
          set (is_set := isaset_forall_hSet (pr11 C1) (λ _, F' (pr1 C2))).
          apply is_set.
    Defined.

I do not claim that this proof is exemplary. I think, minimally you should say that this definition was there only for convenience in something that is anyway more of an illustration. You could say that this produces a weakly equivalent notion of morphisms of coalgebras. But I suspect it would be easy enough to replace cat2 by just the ordinary one and adapt the reasoning.