Lemma E_transport_target : ∏ (C : folds_pre_2_cat) (a b b' : C) (f g : a ⇒ b) (p : b = b'), E f g → E (transportf (λ c, a ⇒ c) p f) (transportf (λ c, a ⇒ c) 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.