proposition: Lemma map_graph_equiv_isfun `{Funext} {A B : Type@{i}} (R : A -> B -> Type@{i}) : map_graph R <~> IsFun R.
proof: Proof. apply (equiv_composeR' (map_graph_equiv_sigma _ _ R)). transitivity (forall x : A, {y : B & {r : R x y & forall yr', (y; r) = yr'}}); last first. { apply equiv_functor_forall_id => a. apply (equiv_compose' (issig_contr _)). apply equiv_sigma_assoc'. } apply (equiv_compose' (equiv_sig_coind _ _)). apply equiv_functor_sigma_id => map. apply (equiv_compose' (equiv_sig_coind _ _)). apply (equiv_composeR' (equiv_sigma_symm _)). transitivity {f : forall x, R x (map x) & forall (x : A) (y : B) (r : R x y), (map x; f x) = (y; r)}; last first. { apply equiv_functor_sigma_id => comap. apply equiv_functor_forall_id => a. exact: (equiv_composeR' equiv_forall_sigma). } transitivity {f : forall x, R x (map x) & forall (x : A) (y : B) (r : R x y), {e : map x = y & e # f x = r}}; last first. { apply equiv_functor_sigma_id => comap. apply equiv_functor_forall_id => a. apply equiv_functor_forall_id => b. apply equiv_functor_forall_id => r. apply (equiv_compose' equiv_path_sigma_dp). apply equiv_functor_sigma_id => e. exact: equiv_dp_path_transport. } transitivity {f : forall x, R x (map x) & forall x y, {g : forall (r : R x y), map x = y & forall (r : R x y), g r # f x = r }}; last first. { apply equiv_functor_sigma_id => comap. apply equiv_functor_forall_id => a. apply equiv_functor_forall_id => b. exact: equiv_sig_coind. } transitivity{f : forall x, R x (map x) & forall x, {g : forall (y : B) (r : R x y), map x = y & forall (y : B) (r : R x y), g y r # f x = r }}; last first. { apply equiv_functor_sigma_id => comap. apply equiv_functor_forall_id => a. exact: equiv_sig_coind. } transitivity {f : forall x, R x (map x) & {g : forall (x : A) (y : B) (r : R x y), map x = y & forall x y r, g x y r # f x = r }}; last first. { apply equiv_functor_sigma_id => comap; exact: equiv_sig_coind. } apply (equiv_compose' (equiv_sigma_symm _)). apply equiv_functor_sigma_id => Rm. transitivity {g : forall (x : A) (y : B) (e : map x = y), R x y & forall (x : A) (y : B) (r : R x y), Rm x y r # g x (map x) idpath = r }. { apply equiv_functor_sigma_id => mR. apply equiv_functor_forall_id => a. apply equiv_functor_forall_id => b. apply equiv_functor_forall_id => r. unshelve econstructor. { apply: concat. elim (Rm a b r). reflexivity. } unshelve econstructor. { apply: concat. elim (Rm a b r). reflexivity. } all: move=> r'; elim r'; elim (Rm a b r); reflexivity. } symmetry. unshelve eapply equiv_functor_sigma. - move=> mR a b e; exact (e # mR a). - move=> mR mRK x y r; apply: mRK. - apply: isequiv_biinv. split; (unshelve eexists; first by move=> + a; apply) => //. move=> r; apply path_forall => a; apply path_forall => b. by apply path_arrow; elim. - by move=> mR; unshelve econstructor. Defined.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions