{A B C D} (h : A <~> C) (k : B <~> D) : (A <~> B) -> (C <~> D) := fun f => ((k oE f) oE h^-1). Global Instance isequiv_functor_equiv {A B C D} (h : A <~> C) (k : B <~> D) : IsEquiv ( h k). Proof. refine (isequiv_adjointify _ ( (equiv_inverse h) (equiv_inverse k)) _ _). - intros f; apply path_equiv, path_arrow; intros x; simpl. exact (eisretr k _ @ ap f (eisretr h x)). - intros g; apply path_equiv, path_arrow; intros x; simpl. exact (eissect k _ @ ap g (eissect h x)). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.