Lemma E_transport_source : ∏ (C : folds_pre_2_cat) (a a' b : C) (f g : a ⇒ b) (p : a = a'), E f g → E (transportf (λ c, c ⇒ b) p f) (transportf (λ c, c ⇒ b) p g). Proof. intros. destruct p. assumption. Defined.
Require Import UniMath.Folds.UnicodeNotations. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets.