Lemma transportOverSet {X:UU} {Y:X->UU} (i:isaset X) {x:X} (e:x=x) {y y':Y x} : transportf Y e y = y. Proof. exact ((transportf (λ k, transportf Y k y = y) (pr1 (i x x (idpath x) e))) (idpath y)). Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.RepresentableFunctors.Precategories. Require Import UniMath.MoreFoundations.Tactics.