fact: Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sig P) (pq : {p : u.1 = v.1 & p # u.2 = v.2}) : u = v := match pq.2 in (_ = v2) return u = (v.1; v2) with | 1 => match pq.1 as p in (_ = v1) return u = (v1; p # u.2) with | 1 => 1 end end.
imports: HoTT.Basics Types.Arrow Types.Paths