{A B : pType} (m : forall (a : A), (point A) = (point A) -> a = a) (q : m pt == idmap) {f g : B ->* A} (K : pointed_fun f = pointed_fun g) : f ==* g. Proof. nrapply issig_phomotopy. destruct f as [f fpt], g as [g gpt]; cbn in *. induction K. destruct A as [A a0]; cbn in *. induction fpt. exists (fun b => m (f b) (idpath @ gpt^)). apply q. Defined.
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.