proposition: Lemma functor_ext (F G : functor) : forall (H : Functor.sort F = Functor.sort G), @actm G = eq_rect _ (fun m : UU0 -> UU0 => forall A B : UU0, (A -> B) -> m A -> m B) (@actm F) _ H -> G = F.
proof: Proof. move: F G => [F [[HF1 HF2 HF3]]] [G [[HG1 HG2 HG3]]] /= H. subst F => /= H. congr (Functor.Pack (Functor.Class _)). have ? : HG1 = HF1. rewrite /actm /= in H. apply funext_dep => x. apply funext_dep => y. apply funext_dep => z. by move/(congr1 (fun i => i x y z)) : H. subst HG1. congr (isFunctor.Axioms_ _); exact/proof_irr. Defined.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)