Sigma

\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