Lemma E_implies_folds_iso (C : folds_pre_2_cat) (a b : C) (f g : a ⇒ b) : E f g → folds_iso f g. Proof. set (H' := pr2 (pr2 (pr1 C))). simpl in H'. destruct H' as [[[Erefl Esym] Etrans] [EI ET]]. intro Efg. repeat split; intros; apply weqimplimpl; intro; folds_pre_2_cat_props C. - apply (ET _ _ _ u u f g v v); auto. - apply (ET _ _ _ u u g f v v) ; auto. - apply (ET _ _ _ u u v v f g); auto. - apply (ET _ _ _ u u v v g f); auto. - apply (ET _ _ _ f g u u v v); auto. - apply (ET _ _ _ g f u u v v); auto. - destruct p; apply (ET _ _ _ f g f g u u); auto. - destruct p; apply (ET _ _ _ g f g f u u); auto. - apply (ET _ _ _ (transportf (λ c, c ⇒ b) p f) (p ## g) u u f g); try apply E_transport_source; auto. - apply (ET _ _ _ (transportf (λ c, c ⇒ b) p g) (p ## f) u u g f); try apply E_transport_source; auto. - apply (ET _ _ _ u u (transportf (λ c, a ⇒ c) p f) (p ## g) f g); try apply E_transport_target; auto. - apply (ET _ _ _ u u (transportf (λ c, a ⇒ c) p g) (p ## f) g f); try apply E_transport_target; auto. - apply (ET _ _ _ (folds_double_transport p q f) (folds_double_transport p q g) (transportf (λ c, a ⇒ c) r f) (r ## g) f g); try apply E_transport_target; try apply E_transport_source; auto. - apply (ET _ _ _ (folds_double_transport p q g) (folds_double_transport p q f) (transportf (λ c, a ⇒ c) r g) (r ## f) g f); try apply E_transport_target; try apply E_transport_source; auto. - destruct p. apply (EI _ f); auto. - destruct p; apply (EI _ g); auto. - apply (Etrans _ _ g f u). + apply Esym; auto. + auto. - apply (Etrans _ _ f g u); auto. - apply (Etrans _ _ u f g); auto. - apply (Etrans _ _ u g f). + auto. + apply Esym; auto. - apply (Etrans _ _ (folds_double_transport p q g) (folds_double_transport p q f) g). + apply E_transport_target. apply E_transport_source. apply Esym; auto. + apply (Etrans _ _ (folds_double_transport p q f) f g); auto. - apply (Etrans _ _ (folds_double_transport p q f) (folds_double_transport p q g) f). + apply E_transport_target. apply E_transport_source. auto. + apply (Etrans _ _ (folds_double_transport p q g) g f); auto. Qed.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.