proposition: Lemma functor_ext (G : {functor C -> D}) (pm : F =1 G) : (forall (A B : C) (f : {hom A, B}), transport_hom (pm A) (pm B) (F # f) = G # f) -> F = G.
proof: Proof. move: pm. case: F => mf cf; case: G => mg cg /= pm. move: cf cg. rewrite /transport_hom. move: (funext pm) => ppm. subst mg => -[[ff idf cf]] -[[fg idg cg]] p. have pp : ff = fg. apply functional_extensionality_dep=> A. apply functional_extensionality_dep=> B. apply functional_extensionality_dep=> f. move: (p A B f). have -> // : pm = (fun _ => erefl). exact: proof_irr. rewrite {p}. move: idf cf idg cg; rewrite pp => idf cf idg cg. have -> : idf = idg by exact: proof_irr. have -> : cf = cg by exact: proof_irr. exact: erefl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)