\import Function \import HLevel \func tupleMap {A B C D : \Type} (f : A -> B) (g : C -> D) (p : \Sigma A C) : \Sigma B D \elim p | (a, c) => (f a, g c) \func tupleMapProj1 {A B C D : \Type} (f : A -> B) (g : C -> D) (p : \Sigma A C) : (tupleMap f g p).1 = f p.1 \elim p | (_,_) => idp \func tupleMapProj2 {A B C D : \Type} (f : A -> B) (g : C -> D) (p : \Sigma A C) : (tupleMap f g p).2 = g p.2 \elim p | (_,_) => idp \func tupleMapLeft {A B C : \Type} (f : A -> B) (p : \Sigma A C) => tupleMap f id p \func tupleMapRight {A B C : \Type} (f : B -> C) (p : \Sigma A B) => tupleMap id f p \func tupleMapLeftProj1 {A B C : \Type} (f : A -> B) (p : \Sigma A C) => tupleMapProj1 f id p \func tupleMapLeftProj2 {A B C : \Type} (f : A -> B) (p : \Sigma A C) => tupleMapProj2 f id p \func tupleMapRightProj1 {A B C : \Type} (f : B -> C) (p : \Sigma A B) => tupleMapProj1 id f p \func tupleMapRightProj2 {A B C : \Type} (f : B -> C) (p : \Sigma A B) => tupleMapProj2 id f p \func unit-isContr : Contr (\Sigma) \cowith | center => () | contraction _ => idp