Library UniMath.MoreFoundations.PartA

This file contain various results that could be upstreamed to Foundations/PartA.v

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.Tactics.

Generalisations of maponpaths

The following are a uniformly-named set of lemmas giving how multi-argument (non-dependent) functions act on paths, generalising maponpaths.

The naming convention is that e.g. maponpaths_135 takes paths in the 1st, 3rd, and 5th arguments, counting backwards from the end. (The “counting backwards” is so that it doesn’t depend on the total number of arguments the function takes.)

All are defined in terms of maponpaths, to allow use of lemmas about it for reasoning about these.

See below for a note about defining duplicates/special cases of these lemmas downstream.

Definition maponpaths_1 {X A : UU} (f : X -> A) {x x'} (e : x = x')
  : f x = f x'
:= maponpaths f e.

Definition maponpaths_2 {Y X A : UU} (f : Y -> X -> A)
    {y y'} (e_y : y = y') x
  : f y x = f y' x
:= maponpaths (fun y => f y x) e_y.

Definition maponpaths_12 {Y X A : UU} (f : Y -> X -> A)
    {y y'} (e_y : y = y') {x x'} (e_x : x = x')
  : f y x = f y' x'
:= maponpaths_1 _ e_x @ maponpaths_2 f e_y _.

Definition maponpaths_3 {Z Y X A : UU} (f : Z -> Y -> X -> A)
    {z z'} (e_z : z = z') y x
  : f z y x = f z' y x
:= maponpaths (fun z => f z y x) e_z.

Definition maponpaths_123 {Z Y X A : UU} (f : Z -> Y -> X -> A)
    {z z'} (e_z : z = z') {y y'} (e_y : y = y') {x x'} (e_x : x = x')
  : f z y x = f z' y' x'
:= maponpaths_12 _ e_y e_x @ maponpaths_3 f e_z _ _.

Definition maponpaths_13 {Z Y X A : UU} (f : Z -> Y -> X -> A)
    {z z'} (e_z : z = z') (y:Y) {x x'} (e_x : x = x')
  : f z y x = f z' y x'
:= maponpaths_123 _ e_z (idpath y) e_x.

Definition maponpaths_4 {W Z Y X A : UU} (f : W -> Z -> Y -> X -> A)
    {w w'} (e_w : w = w') z y x
  : f w z y x = f w' z y x
:= maponpaths (fun w => f w z y x) e_w.

Definition maponpaths_1234 {W Z Y X A : UU} (f : W -> Z -> Y -> X -> A)
    {w w'} (e_w : w = w') {z z'} (e_z : z = z')
    {y y'} (e_y : y = y') {x x'} (e_x : x = x')
  : f w z y x = f w' z' y' x'
:= maponpaths_123 _ e_z e_y e_x @ maponpaths_4 _ e_w _ _ _.

Notes on duplication issues:

Duplicates and special cases of these lemmas have been re-written multiple times, in multiple packages, by multiple contributors.

Sometimes this is intended and useful — e.g. for frequently-used specialisations such as base_paths, especially when subsequent definitions mention them, like fiber_paths.

Other times, it just happens because the contributor hasn’t been aware of the applicable general versions (or they weren’t available at the time of writing). These cases are code duplication, causing redundancy and inconsistent coding style, and should be avoided/refactored.

To keep these clearly distinguished: if you are defining duplicates or special cases of these lemmas, please (a) define them in terms of the general ones, so that lemmas about these are applicable, and (b) add a comment noting why your definitions are desirable.

A few direct duplicates remain:

Foundations.PartA.two_arg_paths and Foundations.PartA.map_on_two_paths are complete duplicates of maponpaths_12, and of each other (modulo reordering of arguments).
Foundations.PartA.pathsdirprod and Foundations.PartA.total2_paths2 are complete duplicates of each other.

Lemma maponpaths_for_constant_function {T1 T2 : UU} (x : T2) {t1 t2 : T1}
(e: t1 = t2): maponpaths (fun _: T1 => x) e = idpath x.
Show proof.

induction e.
apply idpath.

Lemma base_paths_pair_path_in2 {X : UU} (P : X → UU) {x : X} {p q : P x} (e : p = q) :
base_paths _ _ (pair_path_in2 P e) = idpath x.
Show proof.

now induction e.

Lemma transportf_transpose_right
      {X : UU}
      {P : X → UU}
      {x x' : X}
      {e : x = x'}
      {y : P x}
      {y' : P x'} :
      transportb P e y' = y -> y' = transportf P e y.
Show proof.

induction e; apply idfun.

Definition transportb_transpose_right
           {A : UU}
           {P : A → UU}
           {x x' : A}
           {e : x = x'}
           {y : P x} {y' : P x'}
  : transportf P e y = y' → y = transportb P e y'.
Show proof.

induction e; apply idfun.

Definition transportf_transpose_left
           {X : UU}
           {P : X → UU}
           {x x' : X}
           {e : x = x'}
           {y : P x}
           {y' : P x'}
  : y = transportb P e y' → transportf P e y = y'.
Show proof.

induction e; apply idfun.

Definition transportb_transpose_left
           {X : UU}
           {P : X → UU}
           {x x' : X}
           {e : x = x'}
           {y : P x}
           {y' : P x'}
  : y' = transportf P e y → transportb P e y' = y.
Show proof.

induction e; apply idfun.

Very handy for reasoning with “dependent paths” —

Note: similar to transportf_pathsinv0_var, transportf_pathsinv0', but not quite a special case of them, or (as far as I can find) any other library lemma.

Definition transportf_pathsinv0 {X} (P:X ->UU) {x y:X} (p:x = y) (u:P x) (v:P y) :
transportf _ (!p) v = u -> transportf _ p u = v.
Show proof.

intro e. induction p, e. reflexivity.

Lemma transportf_comp_lemma (X : UU) (B : X -> UU) {A A' A'': X} (e : A = A'') (e' : A' = A'')
  (x : B A) (x' : B A')
  : transportf _ (e @ !e') x = x'
  -> transportf _ e x = transportf _ e' x'.
Show proof.

  intro H.
  eapply pathscomp0.
  2: { apply maponpaths. exact H. }
  eapply pathscomp0.
  2: { symmetry. apply transport_f_f. }
  apply (maponpaths (λ p , transportf _ p x)).
  apply pathsinv0.
  eapply pathscomp0.
  - apply @pathsinv0, path_assoc.
  - eapply pathscomp0.
    apply maponpaths.
    apply pathsinv0l.
    apply pathscomp0rid.

Lemma transportf_comp_lemma_hset (X : UU) (B : X -> UU) (A : X) (e : A = A)
  {x x' : B A} (hs : isaset X)
  : x = x'
  -> transportf _ e x = x'.
Show proof.

  intros ex.
  apply @pathscomp0 with (transportf _ (idpath _) x).
  - apply (maponpaths (λ p , transportf _ p x)).
    apply hs.
  - exact ex.

Lemma transportf_bind {X : UU} {P : X → UU}
{x x' x'' : X} (e : x' = x) (e' : x = x'')
y y'
: y = transportf P e y' -> transportf _ e' y = transportf _ (e @ e') y'.
Show proof.

intro H; destruct e, e'; exact H.

Lemma pathscomp0_dep {X : UU} {P : X → UU}
  {x x' x'' : X} {e : x' = x} {e' : x'' = x'}
  {y} {y'} {y''}
: (y = transportf P e y') -> (y' = transportf _ e' y'')
  -> y = transportf _ (e' @ e) y''.
Show proof.

  intros ee ee'.
  etrans. apply ee.
  apply transportf_bind, ee'.

Tactic Notation "etrans_dep" := eapply @pathscomp0_dep.

Lemma transportf_set {A : UU} (B : A → UU)
      {a : A} (e : a = a) (b : B a)
      (X : isaset A)
  : transportf B e b = b.
Show proof.

  apply transportf_comp_lemma_hset.
  - apply X.
  - apply idpath.

Lemma transportf_pair {A B} (P : A × B -> UU) {a a' : A} {b b' : B}
      (eA : a = a') (eB : b = b') (p : P (a ,,b))
      : transportf P (pathsdirprod eA eB) p =
        transportf (λ bb , P(a',,bb) ) eB (transportf (λ aa , P(aa ,,b)) eA p).
Show proof.

induction eA. induction eB. apply idpath.

Lemma weqhomot {A B : UU} (f : A -> B) (w : A ≃ B) (H : w ~ f) : isweq f.
Show proof.

apply isweqhomot with w. apply H. apply weqproperty.

Lemma invmap_eq {A B : UU} (f : A ≃ B) (b : B) (a : A)
: b = f a → invmap f b = a.
Show proof.

  intro H.
  apply (invmaponpathsweq f).
  etrans. apply homotweqinvweq. apply H.

Lemma pr1_transportf {A : UU} {B : A -> UU} {P : ∏ a , B a -> UU}
   {a a' : A} (e : a = a') (xs : ∑ b : B a , P _ b):
   pr1 (transportf (λ x , ∑ b : B x , P _ b) e xs) =
     transportf (λ x , B x) e (pr1 xs).
Show proof.

apply pathsinv0.
apply (transport_map (λ a , pr1 (P := P a))).

Lemma pr2_transportf {A} {B1 B2 : A → UU}
{a a' : A} (e : a = a') (xs : B1 a × B2 a)
: pr2 (transportf (λ a , B1 a × B2 a) e xs) = transportf _ e (pr2 xs).
Show proof.

apply pathsinv0.
apply (transport_map (λ a , pr2 (P := λ _, B2 a))).

Lemma coprodcomm_coprodcomm {X Y : UU} (v : X ⨿ Y) : coprodcomm Y X (coprodcomm X Y v) = v.
Show proof.

induction v as [x|y]; reflexivity.

Definition sumofmaps_funcomp {X1 X2 Y1 Y2 Z : UU} (f1 : X1 → X2) (f2 : X2 → Z) (g1 : Y1 → Y2)
(g2 : Y2 → Z) : sumofmaps (f2 ∘ f1) (g2 ∘ g1) ~ sumofmaps f2 g2 ∘ coprodf f1 g1.
Show proof.

intro x. induction x as [x|y]; reflexivity.

Definition sumofmaps_homot {X Y Z : UU} {f f' : X → Z} {g g' : Y → Z} (h : f ~ f') (h2 : g ~ g')
: sumofmaps f g ~ sumofmaps f' g'.
Show proof.

  intro x. induction x as [x|y].
  - exact (h x).
  - exact (h2 y).

coprod computation helper lemmas

Definition coprod_rect_compute_1
           (A B : UU) (P : A ⨿ B -> UU)
           (f : ∏ (a : A ), P (ii1 a))
           (g : ∏ (b : B ), P (ii2 b)) (a:A) :
  coprod_rect P f g (ii1 a) = f a.
Show proof.

intros.
apply idpath.

Definition coprod_rect_compute_2
           (A B : UU) (P : A ⨿ B -> UU)
           (f : ∏ a : A , P (ii1 a))
           (g : ∏ b : B , P (ii2 b)) (b:B) :
  coprod_rect P f g (ii2 b) = g b.
Show proof.

intros.
apply idpath.

Flip the arguments of a function

Definition flipsec {A B : UU} {C : A -> B -> UU} (f : ∏ a b , C a b) : ∏ b a , C a b :=
λ x y , f y x.
Notation flip := flipsec.

Flip is a weak equivalence (in fact, it is an involution)

Lemma isweq_flipsec {A B : UU} {C : A -> B -> UU} : isweq (@flipsec A B C).
Show proof.

apply (isweq_iso _ flipsec); reflexivity.

Definition flipsec_weq {A B : UU} {C : A -> B -> UU} :
(∏ a b , C a b ) ≃ (∏ b a , C a b ) := make_weq flipsec isweq_flipsec.

hlevel of empty type

Definition empty_hlevel
(n : nat)
: isofhlevel (n + 1) ∅.
Show proof.

  induction n.
  - exact isapropempty.
  - exact (λ x , fromempty x).

Definition empty_HLevel
           (n : nat)
  : HLevel (n + 1)
  := empty ,, empty_hlevel n.

Definition HLevel_fun
           {n : nat}
           (X Y : HLevel n)
  : HLevel n.
Show proof.

  simple refine (_ ,, _).
  - exact (pr1 X → pr1 Y).
  - apply impredfun.
    exact (pr2 Y).

The subtypes of a type of hlevel S n are also of hlevel S n. This doesn't work for types of hlevel 0: a subtype of a contractible type might be empty, not contractible!

Lemma isofhlevel_hsubtype {X : UU} {n : nat} (isof : isofhlevel (S n) X) :
∏ subt : hsubtype X , isofhlevel (S n) subt.
Show proof.

  intros subt.
  apply isofhleveltotal2.
  - assumption.
  - intro.
    apply isofhlevelsnprop.
    apply propproperty.

Homotopy equivalence on total spaces.

This result combines weqfp and weqfibtototal conveniently.

Lemma weqtotal2 {X Y:Type} {P:X ->Type} {Q:Y ->Type} (f : X ≃ Y) :
(∏ x , P x ≃ Q (f x)) -> (∑ x:X , P x ) ≃ (∑ y:Y , Q y ).
Show proof.

intros e. exists (λ xp , (f(pr1 xp),,e (pr1 xp) (pr2 xp))).
exact (twooutof3c _ _ (isweqfibtototal P (Q ∘ f) e) (pr2 (weqfp f Q))).

Lemma weq_subtypes'
    {X Y : UU} (w : X ≃ Y)
    {S : X -> UU} {T : Y -> UU}
    (HS : isPredicate S)
    (HT : isPredicate T)
    (HST : ∏ x : X , S x <-> T (w x))
  : (∑ x , S x ) ≃ (∑ y , T y ).
Show proof.

  apply (weqbandf w).
  intros. apply weqiff.
  - apply HST.
  - apply HS.
  - apply HT.

Lemma weq_subtypes_iff
    {X : UU} {S T : X -> UU}
    (HS : isPredicate S)
    (HT : isPredicate T)
    (HST : ∏ x , S x <-> T x)
  : (∑ x , S x ) ≃ (∑ x , T x ).
Show proof.

apply (weq_subtypes' (idweq X)); assumption.

Lemma hlevel_total2 n {A : UU} {B : A → UU} :
isofhlevel n (∑ (x :A ), B x) → isofhlevel (S n) A → ∏ (x : A ), isofhlevel n (B x).
Show proof.

intros ic ia x.
exact (isofhlevelweqf _ (invweq (ezweqpr1 _ _)) (isofhlevelffromXY _ _ ic ia _)).

Definition path_sigma_hprop
           {A : UU}
           (B : A → UU)
           (x y : ∑ (z : A ), B z)
           (HB : isaprop (B (pr1 y)))
  : x = y ≃ pr1 x = pr1 y.
Show proof.

  refine (weqpr1 _ _ ∘ total2_paths_equiv _ _ _)%weq.
  intros.
  apply HB.

Pointed types

Section PointedTypes.
  Definition PointedType := ∑ X , X.
  Definition pointedType X x := X ,,x : PointedType.
  Definition underlyingType (X:PointedType) := pr1 X.
  Coercion underlyingType : PointedType >-> UU.
  Definition basepoint (X:PointedType) := pr2 X.
  Definition loopSpace (X:PointedType) :=
    pointedType (basepoint X = basepoint X) (idpath _).
  Definition underlyingLoop {X:PointedType} (l:loopSpace X) : basepoint X = basepoint X.
  Show proof.

intros. exact l.

Definition Ω := loopSpace.
End PointedTypes.

associativity of ∑

Definition weq_total2_prod {X Y} (Z:Y ->Type) : (∑ y , X × Z y ) ≃ (X × ∑ y , Z y ).
Show proof.

  intros. simple refine (make_weq _ (isweq_iso _ _ _ _)).
  { intros [y [x z]]. exact (x,,y,,z). }
  { intros [x [y z]]. exact (y,,x,,z). }
  { intros [y [x z]]. reflexivity. }
  { intros [x [y z]]. reflexivity. }

Definition totalAssociativity {X:UU} {Y: ∏ (x:X ), UU} (Z: ∏ (x:X) (y:Y x ), UU) : (∑ (x:X) (y:Y x ), Z x y ) ≃ (∑ (p:∑ (x:X ), Y x ), Z (pr1 p) (pr2 p)).
Show proof.

  intros. simple refine (_,,isweq_iso _ _ _ _).
  { intros [x [y z]]. exact ((x,,y),,z). }
  { intros [[x y] z]. exact (x,,(y,,z)). }
  { intros [x [y z]]. reflexivity. }
  { intros [[x y] z]. reflexivity. }

Definition paths3 {X Y Z} {x x':X} {y y':Y} {z z':Z} :
x = x' -> y = y' -> z = z' -> @paths (_×_×_) (x ,,y ,,z) (x',,y',,z').
Show proof.

intros p q r. induction p, q, r. reflexivity.

Definition confun T {Y} (y:Y) := λ _:T , y.
Definition path_type {X} {x x':X} (p:x = x') := X.
Definition path_start {X} {x x':X} (p:x = x') := x.
Definition path_end {X} {x x':X} (p:x = x') := x'.

Definition uniqueness {T} (i:iscontr T) (t:T) : t = iscontrpr1 i.
Show proof.

intros. exact (pr2 i t).

Definition uniqueness' {T} (i:iscontr T) (t:T) : iscontrpr1 i = t.
Show proof.

intros. exact (! (pr2 i t)).

Definition path_inverse_to_right {X} {x y:X} (p q:x = y) : p = q -> !q@p = idpath _.
Show proof.

intros e. induction e. induction p. reflexivity.

Definition path_inverse_to_right' {X} {x y:X} (p q:x = y) : p = q -> p@!q = idpath _.
Show proof.

intros e. induction e. induction p. reflexivity.

Paths

Definition pathsinv0_to_right {X} {x y z:X} (p:y = x) (q:y = z) (r:x = z) :
q = p @ r -> !p @ q = r.
Show proof.

intros e. induction p, q. exact e.

Definition pathsinv0_to_right' {X} {x y:X} (p:y = x) (r:x = y) :
idpath _ = p @ r -> !p = r.
Show proof.

intros e. induction p. exact e.

Definition pathsinv0_to_right'' {X} {x:X} (p:x = x) :
idpath _ = p -> !p = idpath _.
Show proof.

intros e. apply pathsinv0_to_right'. rewrite pathscomp0rid. exact e.

Definition loop_power_nat {Y} {y:Y} (l:y = y) (n:nat) : y = y.
Show proof.

  intros. induction n as [|n p].
  { exact (idpath _). }
  { exact (p@l). }

Lemma irrel_paths {X} (irr:∏ x y:X , x = y) {x y:X} (p q:x = y) : p = q.
Show proof.

  intros.
  assert (k : ∏ z:X, ∏ r:x = z , r @ irr z z = irr x z).
  { intros. induction r. reflexivity. }
  assert (l := k y p @ !k y q).
  apply (pathscomp_cancel_right _ _ _ l).

Definition path_inv_rotate_2 {X} {a b c d:X} (p:a = b) (p':c = d) (q:a = c) (q':b = d) :
q @ p' = p @ q' -> p' @ ! q' = !q @ p.
Show proof.

induction q,q'. simpl. repeat rewrite pathscomp0rid. apply idfun.

Definition maponpaths_naturality {X Y : UU} {f : X -> Y}
           {x x' x'' : X} {p : x = x'} {q : x' = x''}
           {p': f x = f x'} {q': f x' = f x''}
           (r : maponpaths f p = p') (s : maponpaths f q = q') :
  maponpaths f (p @ q) = p' @ q'.
Show proof.

intros. induction r, s. apply maponpathscomp0.

Definition maponpaths_naturality' {X Y : UU} {f : X -> Y}
           {x x' x'' : X} {p : x' = x} {q : x' = x''}
           {p' : f x' = f x} {q' : f x' = f x''}
           (r : maponpaths f p = p') (s : maponpaths f q = q') :
  maponpaths f (!p @ q) = (!p') @ q'.
Show proof.

intros. induction r, s, p, q. reflexivity.

Pairs

Definition pr2_of_make_hfiber {X Y} {f:X ->Y} {x:X} {y:Y} {e:f x = y} :
pr2 (make_hfiber f x e) = e.
Show proof.

reflexivity.

Definition pr2_of_pair {X} {P:X ->Type} (x:X) (p:P x) : pr2 (tpair P x p) = p.
Show proof.

reflexivity.

Definition pr2_of_make_weq {X Y} (f:X ->Y) (i:isweq f) : pr2 (make_weq f i) = i.
Show proof.

reflexivity.

Paths between pairs

Definition pair_path_props {X} {P:X ->Type} {x y:X} {p:P x} {q:P y} :
x = y -> (∏ z , isaprop (P z)) -> x ,,p = y ,,q.
Show proof.

  intros e is. now apply subtypePairEquality.
Abort.

Local Open Scope transport.

Definition pair_path2 {A} {B:A ->UU} {a a1 a2} {b1:B a1} {b2:B a2}
           (p:a1 = a) (q:a2 = a) (e:p #b1 = q #b2) : a1 ,,b1 = a2 ,,b2.
Proof.
  intros. induction p,q; compute in e. induction e. reflexivity.

Projections from pair types

Definition pair_path_in2_comp1 {X} (P:X ->Type) {x:X} {p q:P x} (e:p = q) :
maponpaths pr1 (maponpaths (tpair P _) e) = idpath x.
Show proof.

intros. induction e. reflexivity.

Definition total2_paths2_comp1 {X} {Y:X ->Type} {x} {y:Y x} {x'} {y':Y x'}
(p:x = x') (q:p #y = y') : maponpaths pr1 (two_arg_paths_f (f := tpair Y) p q) = p.
Show proof.

intros. induction p. induction q. reflexivity.

Definition total2_paths2_comp2 {X} {Y:X ->Type} {x} {y:Y x} {x'} {y':Y x'}
(p:x = x') (q:p #y = y') :
! maponpaths_2 _ (total2_paths2_comp1 p q) y @ fiber_paths (two_arg_paths_f p q) = q.
Show proof.

intros. induction p, q. reflexivity.

Maps from pair types

Definition from_total2 {X} {P:X ->Type} {Y} : (∏ x , P x ->Y ) -> total2 P -> Y.
Show proof.

intros f [x p]. exact (f x p).

Paths in coproducts

Definition inv_equality_by_case_equality_by_case
           {A B : UU}
           {x y : A ⨿ B}
           (p : x = y)
  : @inv_equality_by_case A B x y (equality_by_case p) = p.
Show proof.

induction x, y, p ; apply idpath.

Definition equality_by_case_inv_equality_by_case
           {A B : UU}
           {x y : A ⨿ B}
           (p : equality_cases x y)
  : equality_by_case (inv_equality_by_case p) = p.
Show proof.

induction x, y, p; apply idpath.

Lemma equality_by_case_equiv {A B} (t u : A ⨿ B) : (t = u ) ≃ equality_cases t u.
Show proof.

  use weq_iso.
  - apply equality_by_case.
  - apply inv_equality_by_case.
  - apply inv_equality_by_case_equality_by_case.
  - apply equality_by_case_inv_equality_by_case.

Definition paths_inl_inl_equiv {A B : UU} (a a' : A)
: @inl A B a = inl a' ≃ a = a'.
Show proof.

apply @equality_by_case_equiv.

Definition paths_inl_inr_equiv {A B : UU} (a : A) (b : B)
: inl a = inr b ≃ empty.
Show proof.

apply @equality_by_case_equiv.

Definition paths_inr_inr_equiv {A B : UU} (b b' : B)
: @inr A B b = inr b' ≃ b = b'.
Show proof.

apply @equality_by_case_equiv.

Definition paths_inr_inl_equiv {A B : UU} (a : A) (b : B)
: inr b = inl a ≃ empty.
Show proof.

apply @equality_by_case_equiv.

Lemma isInjective_inl {A B : UU} : isInjective (@inl A B).
Show proof.

intros ? ?.
refine (isweqinvmap (@paths_inl_inl_equiv _ _ _ _)).

Lemma isInjective_inr {A B : UU} : isInjective (@inr A B).
Show proof.

intros ? ?.
refine (isweqinvmap (@paths_inr_inr_equiv _ _ _ _)).

Sections and functions

Notation homotsec := homot.

Naturality of homotopies

Definition homotsec_natural
           {X Y : UU}
           {f g : X → Y}
           (e : f ~ g)
           {x y : X}
           (p : x = y)
  : maponpaths f p @ e y = e x @ maponpaths g p.
Show proof.

induction p.
exact (!(pathscomp0rid _)).

Definition evalat {T} {P:T ->UU} (t:T) (f:∏ t:T , P t) := f t.

Definition apfun {X Y} {f f':X ->Y} (p:f = f') {x x'} (q:x = x') : f x = f' x'.
intros. induction q. exact (eqtohomot p x).
Defined.

Definition fromemptysec { X : empty -> UU } (nothing:empty) : X nothing.
Show proof.

induction nothing.

Definition maponpaths_idpath {X Y} {f:X ->Y} {x:X} : maponpaths f (idpath x) = idpath (f x).
Show proof.

intros. reflexivity.

Transport

Definition cast {T U:Type} : T = U -> T -> U
:= transportf (λ T:Type, T).

Definition transport_type_path {X Y:Type} (p:X = Y) (x:X) :
transportf (λ T:Type, T) p x = cast p x.
Show proof.

reflexivity.

Definition transport_fun_path {X Y} {f g:X ->Y} {x x':X} {p:x = x'} {e:f x = g x} {e':f x' = g x'} :
e @ maponpaths g p = maponpaths f p @ e' ->
transportf (λ x , f x = g x) p e = e'.
Show proof.

intros k. induction p. rewrite maponpaths_idpath in k. rewrite maponpaths_idpath in k.
rewrite pathscomp0rid in k. exact k.

Definition transportf_pathsinv0' {X} (P:X ->UU) {x y:X} (p:x = y) (u:P x) (v:P y) :
p # u = v -> !p # v = u.
Show proof.

intros e. induction p, e. reflexivity.

Lemma transport_idfun {X} (P:X ->UU) {x y:X} (p:x = y) (u:P x) :
transportf P p u = transportf (idfun UU) (maponpaths P p) u.
Show proof.

intros. induction p. reflexivity.

Lemma transport_functions {X} {Y:X ->Type} {Z:∏ x (y:Y x ), Type}
      {f f':∏ x : X , Y x} (p:f = f') (z:∏ x , Z x (f x)) x :
    transportf (λ f , ∏ x , Z x (f x)) p z x =
    transportf (Z x) (toforallpaths _ _ _ p x) (z x).
Show proof.

intros. induction p. reflexivity.

Definition transport_funapp {T} {X Y:T ->Type}
           (f:∏ t , X t -> Y t) (x:∏ t , X t)
           {t t':T} (p:t = t') :
  transportf _ p ((f t)(x t))
  = (transportf (λ t , X t -> Y t) p (f t)) (transportf _ p (x t)).
Show proof.

intros. induction p. reflexivity.

Definition helper_A {T} {Y} (P:T ->Y ->Type) {y y':Y} (k:∏ t , P t y) (e:y = y') t :
  transportf (λ y , P t y) e (k t)
  =
  (transportf (λ y , ∏ t , P t y) e k) t.
Show proof.

intros. induction e. reflexivity.

Definition helper_B {T} {Y} (f:T ->Y) {y y':Y} (k:∏ t , y = f t) (e:y = y') t :
  transportf (λ y , y = f t) e (k t)
  =
  (transportf (λ y , ∏ t , y = f t) e k) t.
Show proof.

intros. exact (helper_A _ k e t).

Definition transport_invweq {T} {X Y:T ->Type} (f:∏ t , (X t ) ≃ (Y t ))
           {t t':T} (p:t = t') :
  transportf (λ t , (Y t ) ≃ (X t )) p (invweq (f t))
  =
  invweq (transportf (λ t , (X t ) ≃ (Y t )) p (f t)).
Show proof.

intros. induction p. reflexivity.

Definition transport_invmap {T} {X Y:T ->Type} (f:∏ t , (X t ) ≃ (Y t ))
           {t t':T} (p:t =t') :
  transportf (λ t , Y t -> X t) p (invmap (f t))
  =
  invmap (transportf (λ t , (X t ) ≃ (Y t )) p (f t)).
Show proof.

intros. induction p. reflexivity.

Double transport

Definition transportf2 {X} {Y:X ->Type} (Z:∏ x , Y x ->Type)
{x x'} (p:x = x')
(y:Y x) (z:Z x y) : Z x' (p #y).
Show proof.

intros. induction p. exact z.

Definition transportb2 {X} {Y:X ->Type} (Z:∏ x , Y x ->Type)
{x x'} (p:x =x')
(y':Y x') (z':Z x' y') : Z x (p #'y').
Show proof.

intros. induction p. exact z'.

Definition maponpaths_pr1_pr2 {X} {P:X ->UU} {Q:∏ x , P x ->Type}
           {w w': ∑ x p , Q x p}
           (p : w = w') :
  transportf P (maponpaths pr1 p) (pr1 (pr2 w)) = pr1 (pr2 w').
Show proof.

intros. induction p. reflexivity.

Transport a pair

Definition transportb_pair X (Y:X ->Type) (Z:∏ x , Y x ->Type)
           x x' (p:x = x')
           (y':Y x') (z':Z x' y')
           (z'' : (Z x' y')) :
  transportb (λ x , total2 (Z x)) p (tpair (Z x') y' z')
  =
  tpair (Z x) (transportb Y p y') (transportb2 _ p y' z').
Show proof.

intros. induction p. reflexivity.

Lemma transportf_total2_const (A B : UU) (P : B -> A -> UU) (b : B) (a1 a2 : A) (e : a1 = a2) (p : P b a1) :
transportf (λ x , ∑ y , P y x) e (b ,, p) = b ,, transportf (P b) e p.
Show proof.

induction e.
apply idpath.

h-levels and paths

Lemma isaprop_wma_inhab X : (X -> isaprop X ) -> isaprop X.
Show proof.

intros f. apply invproofirrelevance. intros x y. apply (f x).

Lemma isaprop_wma_inhab' X : (X -> iscontr X ) -> isaprop X.
Show proof.

intros f. apply isaprop_wma_inhab. intro x. apply isapropifcontr.
apply (f x).

Goal ∏ (X :hSet ) (x y :X ) (p q :x = y ), p = q.
Show proof.

intros. apply setproperty.

Goal ∏ (X :Type ) (x y :X ) (p q :x = y ), isaset X -> p = q.
Show proof.

intros * is. apply is.

Definition funset X (Y:hSet) : hSet
  := make_hSet (X ->Y) (impredfun 2 _ _ (setproperty Y)).

Lemma eq_equalities_between_pairs (A : UU) (B : A -> UU)(x y : total2 (λ x , B x))
    (p q : x = y) (H : base_paths _ _ p = base_paths _ _ q)
    (H2 : transportf (fun p : pr1 x = pr1 y => transportf _ p (pr2 x) = pr2 y )
         H (fiber_paths p) = fiber_paths q) : p = q.
Show proof.

  apply (invmaponpathsweq (total2_paths_equiv _ _ _ )).
  apply (total2_paths_f (B:=(fun p : pr1 x = pr1 y =>
          transportf (λ x : A, B x) p (pr2 x) = pr2 y))
          (s := (total2_paths_equiv B x y) p)
          (s' := (total2_paths_equiv B x y) q) H).
  assumption.

Lemma total2_reassoc_paths {A} {B : A → UU} {C : (∑ a , B a ) -> UU}
    (BC : A -> UU := λ a , ∑ b , C (a ,,b))
    {a1 a2 : A} (bc1 : BC a1) (bc2 : BC a2)
    (ea : a1 = a2)
    (eb : transportf _ ea (pr1 bc1) = pr1 bc2)
    (ec : transportf C (two_arg_paths_f ea eb) (pr2 bc1) = pr2 bc2)
  : transportf _ ea bc1 = bc2.
Show proof.

  destruct bc1 as [b1 c1], bc2 as [b2 c2]; simpl in *.
  destruct ea. destruct eb. simpl in *. destruct ec.
  apply idpath.

Lemma total2_reassoc_paths' {A} {B : A → UU} {C : (∑ a , B a ) -> UU}
    (BC : A -> UU := λ a , ∑ b , C (a ,,b))
    {a1 a2 : A} (bc1 : BC a1) (bc2 : BC a2)
    (ea : a1 = a2)
    (eb : pr1 bc1 = transportb _ ea (pr1 bc2))
    (ec : pr2 bc1 = transportb C (total2_paths2_b ea eb) (pr2 bc2))
  : bc1 = transportb BC ea bc2.
Show proof.

  destruct ea, bc1 as [b1 c1], bc2 as [b2 c2].
  cbn in eb; destruct eb; cbn in ec; destruct ec.
  apply idpath.

Section InvRot.

moving pathsinv0 to the other side in equations

  Local Set Implicit Arguments.
  Local Unset Strict Implicit.

  Definition invrot (X:Type) (x y:X) (p:x =y) (p':y =x) : !p = p' -> p = !p'.
  Show proof.

intros e. induction e. apply pathsinv0. apply pathsinv0inv0.

Definition invrot' (X:Type) (x y:X) (p:x =y) (p':y =x) : p = !p' -> !p = p'.
Show proof.

intros e. induction (!e); clear e. apply pathsinv0inv0.

  Definition invrot'rot (X:Type) (x y:X) (p:x =y) (p':y =x) (e : !p = p') :
    invrot' (invrot e) = e.
  Show proof.

now induction e,p.

  Definition invrotrot' (X:Type) (x y:X) (p:x =y) (p':y =x) (e : p = !p') :
    invrot (invrot' e) = e.
  Show proof.

    rewrite <- (pathsinv0inv0 e).
    generalize (!e); clear e.
    intros e.
    now induction e, p'.

End InvRot.

Section Weqpaths.

a more basic approach to proving isweqpathscomp0r

  Local Set Implicit Arguments.
  Local Unset Strict Implicit.

  Definition hornRotation_rr {X:Type} {x y z : X} {p : x = z} {q : y = z} {r : x = y} :
    r = p @ !q ≃ r @ q = p.
  Show proof.

induction q, r; cbn. apply eqweqmap.
apply (maponpaths (λ k , idpath x = k)). apply pathscomp0rid.

  Definition hornRotation_lr {X:Type} {x y z : X} {p : x = z} {q : y = z} {r : x = y} :
    q = (!r ) @ p ≃ r @ q = p.
  Show proof.

induction p, r; cbn. apply idweq.

  Definition hornRotation_rl {X:Type} {x y z : X} {p : x = z} {q : y = z} {r : x = y} :
    p @ !q = r ≃ p = r @ q.
  Show proof.

induction q, r; cbn. apply eqweqmap.
apply (maponpaths (λ k , k = idpath x)). apply pathscomp0rid.

  Definition hornRotation_ll {X:Type} {x y z : X} {p : x = z} {q : y = z} {r : x = y} :
    (!r ) @ p = q ≃ p = r @ q.
  Show proof.

induction p, r; cbn. apply idweq.

  Corollary uniqueFiller (X:Type) (x y z : X) (p : x = z) (q : y = z) :
    ∃! r , r @ q = p.
  Show proof.

    refine (@iscontrweqf (∑ r , r = p @ !q) _ _ _).
    { apply weqfibtototal; intro r. exact hornRotation_rr. }
    { apply iscontrcoconustot. }

  Lemma fillerEquation {X:Type} {x y z : X} {p : x = z} {q : y = z}
        (r : x = y) (k : r @ q = p) :
    @paths (∑ r , r@q =p)
           (r ,, k)
           ((p @ !q ) ,, hornRotation_rr (idpath _)).
  Show proof.

apply proofirrelevancecontr. apply uniqueFiller.

  Corollary isweqpathscomp0r' {X : UU} (x : X) {x' x'' : X} (e' : x' = x'') :
    isweq (λ e : x = x', e @ e').
  Show proof.

intros p. use tpair. exists (p @ !e'). now apply hornRotation_rr.
cbn. intros [q l]. apply fillerEquation.

  Definition transportPathTotal {X:Type} {x x':X} {Y : X -> Type} (y : Y x) (y' : Y x')
             (r : (x ,,y ) = (x',,y'))
             (T : ∏ (a:X) (b:Y a ), Type) : T x y → T x' y'.
  Show proof.

    induction (total2_paths_equiv _ _ _ r) as [p q].
    change (x=x') in p. change (transportf _ p y = y') in q.
    induction p.
    change (y=y') in q.
    induction q.
    trivial.

  Definition inductionOnFiller {X:Type} {x y z:X} (p:x =z) (q:y =z)
             (S := λ r:x =y , r @ q = p)
             (T : ∏ r (e : S r ), Type)
             (t : T (p @ !q) (hornRotation_rr (idpath _))) :
    ∏ (r:x =y) (e : r @ q = p ), T r e.
  Show proof.

    intros.
    use (transportPathTotal _ t).
    apply pathsinv0.
    apply fillerEquation.

End Weqpaths.

Lemma transportf_paths_FlFr {A B : UU} {f g : A -> B} {x1 x2 : A}
(p : x1 = x2) (q : f x1 = g x1)
: transportf (λ x , f x = g x) p q = !maponpaths f p @ q @ maponpaths g p.
Show proof.

induction p. cbn.
apply pathsinv0.
apply pathscomp0rid.

Lemma transportf_sec_constant
{A B : UU} {C : A -> B -> UU}
{x1 x2 : A} (p : x1 = x2) (f : ∏ y : B , C x1 y)
: (transportf (λ x , ∏ y : B , C x y) p f )
= (λ y , transportf (λ x , C x y) p (f y)).
Show proof.

induction p; reflexivity.

More facts on fiber products

Definition path_hfp
           {X Y Z : UU}
           {f : X → Z}
           {g : Y → Z}
           {x y : hfp f g}
           (p₁ : hfpg f g x = hfpg f g y)
           (p₂ : hfpg' f g x = hfpg' f g y)
           (p₃ : commhfp f g x @ maponpaths f p₁
                 =
                 maponpaths g p₂ @ commhfp f g y)
  : x = y.
Show proof.

  induction x as [ [ x₁ x₂ ] px ].
  induction y as [ [ y₁ y₂ ] py ].
  cbn in p₁, p₂.
  induction p₁, p₂.
  cbn in p₃.
  apply maponpaths.
  exact (!(pathscomp0rid _) @ p₃).

Definition maponpaths_hfpg_path_hfp
           {X Y Z : UU}
           {f : X → Z}
           {g : Y → Z}
           {x y : hfp f g}
           (p₁ : hfpg f g x = hfpg f g y)
           (p₂ : hfpg' f g x = hfpg' f g y)
           (p₃ : commhfp f g x @ maponpaths f p₁
                 =
                 maponpaths g p₂ @ commhfp f g y)
  : maponpaths
      (hfpg f g)
      (path_hfp p₁ p₂ p₃)
    =
    p₁.
Show proof.

  induction x as [ [ x₁ x₂ ] px ].
  induction y as [ [ y₁ y₂ ] py ].
  cbn in p₁, p₂.
  induction p₁, p₂.
  cbn in p₃.
  induction p₃ ; cbn.
  etrans.
  {
    apply (maponpathscomp
             (tpair (λ xx', g (pr2 xx') = f (pr1 xx')) (x₁,, x₂))
             (hfpg f g)).
  }
  apply maponpaths_for_constant_function.

Definition maponpaths_hfpg'_path_hfp
           {X Y Z : UU}
           {f : X → Z}
           {g : Y → Z}
           {x y : hfp f g}
           (p₁ : hfpg f g x = hfpg f g y)
           (p₂ : hfpg' f g x = hfpg' f g y)
           (p₃ : commhfp f g x @ maponpaths f p₁
                 =
                 maponpaths g p₂ @ commhfp f g y)
  : maponpaths
      (hfpg' f g)
      (path_hfp p₁ p₂ p₃)
    =
    p₂.
Show proof.

  induction x as [ [ x₁ x₂ ] px ].
  induction y as [ [ y₁ y₂ ] py ].
  cbn in p₁, p₂.
  induction p₁, p₂.
  cbn in p₃.
  induction p₃ ; cbn.
  etrans.
  {
    apply (maponpathscomp
             (tpair (λ xx', g (pr2 xx') = f (pr1 xx')) (x₁,, x₂))
             (hfpg' f g)).
  }
  apply maponpaths_for_constant_function.

Definition path_hfp_eta
           {X Y Z : UU}
           {f : X → Z}
           {g : Y → Z}
           {x y : hfp f g}
           (p : x = y)
  : p
    =
    path_hfp
      (maponpaths (hfpg f g) p)
      (maponpaths (hfpg' f g) p)
      (maponpaths (λ z , _ @ z) (maponpathscomp (hfpg f g) f p)
       @ !(homotsec_natural (commhfp f g) p )
       @ maponpaths (λ z , z @ _) (!(maponpathscomp (hfpg' f g) g p ))).
Show proof.

  induction p.
  cbn.
  refine (!_).
  etrans.
  {
    apply maponpaths.
    etrans.
    {
      apply maponpaths.
      etrans.
      {
        apply pathscomp0rid.
      }
      apply pathsinv0inv0.
    }
    apply pathsinv0l.
  }
  apply idpath.

Definition homot_hfp
           {X Y Z : UU}
           {f : X → Z} {g : Y → Z}
           {x y : hfp f g}
           {h₁ h₁' : hfpg f g x = hfpg f g y}
           (e₁ : h₁ = h₁')
           {h₂ h₂' : hfpg' f g x = hfpg' f g y}
           (e₂ : h₂ = h₂')
           (h₃ : commhfp f g x @ maponpaths f h₁ = maponpaths g h₂ @ commhfp f g y)
  : path_hfp h₁ h₂ h₃
    =
    path_hfp
      h₁' h₂'
      (maponpaths
         (λ z , _ @ maponpaths f z)
         (!e₁)
       @ h₃
       @ maponpaths
           (λ z , maponpaths g z @ _)
           e₂).
Show proof.

  induction e₁ ; induction e₂.
  simpl.
  apply maponpaths.
  exact (!(pathscomp0rid _)).

Definition homot_hfp_one_type
           {X Y Z : UU}
           (HZ : isofhlevel 3 Z)
           {f : X → Z}
           {g : Y → Z}
           {x y : hfp f g}
           (p q : x = y)
           (r₁ : maponpaths (hfpg f g) p
                 =
                 maponpaths (hfpg f g) q)
           (r₂ : maponpaths (hfpg' f g) p
                 =
                 maponpaths (hfpg' f g) q)
  : p = q.
Show proof.

  refine (path_hfp_eta p @ _ @ !(path_hfp_eta q)).
  etrans.
  {
    exact (homot_hfp r₁ r₂ _).
  }
  apply maponpaths.
  apply HZ.

Definition hfp_is_of_hlevel
           (n : nat)
           {X Y Z : UU}
           (HX : isofhlevel n X)
           (HY : isofhlevel n Y)
           (HZ : isofhlevel n Z)
           (f : X → Z)
           (g : Y → Z)
  : isofhlevel n (hfp f g).
Show proof.

  use isofhleveltotal2.
  - use isofhleveldirprod.
    + exact HX.
    + exact HY.
  - simpl.
    intro x.
    apply (hlevelntosn n _ HZ).

Definition hfp_HLevel
           (n : nat)
           {X Y Z : HLevel n}
           (f : pr1 X → pr1 Z)
           (g : pr1 Y → pr1 Z)
  : HLevel n.
Show proof.

  simple refine (hfp f g ,, _).
  apply hfp_is_of_hlevel.
  - exact (pr2 X).
  - exact (pr2 Y).
  - exact (pr2 Z).

Transport along a path of total2

Definition transportf_total2_paths_f
           {A : UU}
           {B : A → UU}
           (C : A → UU)
           {a₁ a₂ : A}
           {b₁ : B a₁}
           {b₂ : B a₂}
           (p : a₁ = a₂)
           (q : transportf B p b₁ = b₂)
           (c₁ : C a₁)
  : transportf
      (λ z , C (pr1 z))
      (@total2_paths_f
         A B
         (a₁ ,, b₁) (a₂ ,, b₂)
         p
         q)
      c₁
    =
    transportf
      C
      p
      c₁.
Show proof.

  induction p.
  induction q.
  apply idpath.

Paths of products

Definition maponpaths_pr1_pathsdirprod
           {X Y : UU}
           {x₁ x₂ : X}
           {y₁ y₂ : Y}
           (p : x₁ = x₂)
           (q : y₁ = y₂)
  : maponpaths dirprod_pr1 (pathsdirprod p q) = p.
Show proof.

induction p, q.
apply idpath.

Definition maponpaths_pr2_pathsdirprod
           {X Y : UU}
           {x₁ x₂ : X}
           {y₁ y₂ : Y}
           (p : x₁ = x₂)
           (q : y₁ = y₂)
  : maponpaths dirprod_pr2 (pathsdirprod p q) = q.
Show proof.

induction p, q.
apply idpath.

Definition pathsdirprod_eta
           {X Y : UU}
           {x y : X × Y}
           (p : x = y)
  : p
    =
    pathsdirprod (maponpaths dirprod_pr1 p) (maponpaths dirprod_pr2 p).
Show proof.

induction p.
apply idpath.

Definition paths_pathsdirprod
           {X Y : UU}
           {x₁ x₂ : X}
           {y₁ y₂ : Y}
           {p₁ p₂ : x₁ = x₂}
           {q₁ q₂ : y₁ = y₂}
           (r₁ : p₁ = p₂)
           (r₂ : q₁ = q₂)
  : pathsdirprod p₁ q₁
    =
    pathsdirprod p₂ q₂.
Show proof.

induction r₁, r₂.
apply idpath.

Paths on functions

Definition app_fun
           {X Y : UU}
  : (X → Y ) × X → Y
  := λ fx , pr1 fx (pr2 fx).

Definition app_homot
           {X Y₁ Y₂ : UU}
           {f g : Y₁ → X → Y₂}
           (p : ∏ (z : Y₁ × X ), f (pr1 z) (pr2 z) = g (pr1 z) (pr2 z))
           (y : Y₁)
  : f y = g y
  := funextsec _ _ _ (λ x , p (y ,, x)).

Definition maponpaths_app_fun
           {X Y : UU}
           {fx gx : (X → Y ) × X}
           (p : fx = gx)
  : maponpaths (λ (fx : (X → Y ) × X ), app_fun fx) p
    =
    maponpaths (λ z , z (pr2 fx)) (maponpaths dirprod_pr1 p)
    @
    maponpaths (pr1 gx) (maponpaths dirprod_pr2 p).
Show proof.

induction p.
apply idpath.

Product of a propositions with itself

Definition dirprod_with_prop (A : UU) (isa : isaprop A) : A × A ≃ A.
Show proof.

apply weqpr1, iscontraprop1; assumption.

A variation on the above theme

Definition dirprod_with_prop' (A B : UU) (isa : isaprop A) : A × B × A ≃ B × A.
Show proof.

  intermediate_weq ((A × B) × A).
  apply invweq, weqtotal2asstor.
  intermediate_weq (A × (A × B)).
  apply weqdirprodcomm.
  intermediate_weq ((A × A) × B).
  apply invweq, weqtotal2asstor.
  intermediate_weq (A × B).
  apply weqdirprodf.
  - apply dirprod_with_prop; assumption.
  - apply idweq.
  - apply weqdirprodcomm.

Surjectivity

Section surjectivity.
Lemma issurjective_idfun (X : UU) : issurjective (idfun X).
Show proof.

exact(λ (x : X), hinhpr (x ,, idpath x)).

  Lemma issurjective_to_contr {X Y : UU}
    (x : X)
    (f : X → Y)
    (contr : iscontr Y) : issurjective f.
  Show proof.

    intro; apply hinhpr.
    apply(make_hfiber f x).
    apply proofirrelevancecontr, contr.

Lemma issurjective_tounit {X : UU} : X -> issurjective (@tounit X).
Show proof.

    intro x.
    apply(issurjective_to_contr x).
    apply iscontrunit.

  Lemma issurjective_coprodf {X Y W Z : UU}
    {f : X → W}
    {g : Y → Z}
    (fsurjective : issurjective f)
    (gsurjective : issurjective g)
    : issurjective (coprodf f g).
  Show proof.

    red; apply coprod_rect.
    - intro w.
      apply(hinhfun (weqhfibercoprodf1 f g w)).
      exact(fsurjective w).
    - intro z.
      apply(hinhfun (weqhfibercoprodf2 f g z)).
      exact(gsurjective z).

  Lemma issurjective_dirprodf {X Y U W}
    {f : X → U}
    {g : Y → W}
    (fsurjective : issurjective f)
    (gsurjective : issurjective g)
    : issurjective (dirprodf f g).
  Show proof.

    intros [u w].
    use(hinhfun2 _ (fsurjective u) (gsurjective w)).
    intros ffiber gfiber.
    use make_hfiber.
    - exact(hfiberpr1 f u ffiber
              ,, hfiberpr1 g w gfiber).
    - apply dirprodeq
      ; apply hfiberpr2.

  Lemma issurjective_totalfun
    {X : UU}
    (P Q : X → UU)
    (f : ∏ (x : X ), P x → Q x)
    (fsurjective : ∏ (x : X ), issurjective (f x))
    : issurjective (totalfun P Q f).
  Show proof.

    intros [x qx].
    use(hinhfun _ (fsurjective x qx)).

    intros [px pathpx].     use make_hfiber.
    - exact(x ,, px).
    - exact(pair_path_in2 Q pathpx).

  Lemma issurjective_sumofmaps_1 {X A B : UU}
    (f : A -> X)
    (g : B -> X)
    (fsurjective : issurjective f)
    : issurjective (sumofmaps f g).
  Show proof.

    intro x.
    use(hinhfun _ (fsurjective x)).
    intro ffiber; apply coprodofhfiberstohfiber.
    exact(inl ffiber).

  Lemma issurjective_sumofmaps_2 {X A B : UU}
    (f : A -> X)
    (g : B -> X)
    (gsurjective : issurjective g)
    : issurjective (sumofmaps f g).
  Show proof.

    intro x.
    use(hinhfun _ (gsurjective x)).
    intro gfiber; apply coprodofhfiberstohfiber.
    exact(inr gfiber).

End surjectivity.