proposition: Lemma transport_relation_exchange (A : Type) (R : crelation A) : forall (a a' b b': A) (p : a = b) (q : a' = b') (t : R a a'), transport (fun z => R b z) q (transport (fun k => R k a') p t) = transport (fun k => R k b') p (transport (fun z => R a z) q t).
proof: Proof. intros a a' b b' p q t; destruct p, q; reflexivity. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Equations.Prop.Logic