Library UniMath.Foundations.PartA

Univalent Foundations, Part A

Vladimir Voevodsky. Feb. 2010 - Sep. 2011.

This file is based on the first part of the original uu0 file.

The uu0 file contained the basic results of the univalent foundations that required the use of only one universe.

Eventually the requirement concerning one universe was removed because of the general uncertainty in what does it mean for a construction to require only one universe. For example, boolsumfun , when written in terms of the eliminatior bool_rect instead of the match , requires application of bool_rect to an argument that is not a member of the base universe UU . This would be different if the universe management in Coq was constructed differently. Due to this uncertainty we do not consider any more the single universe requirement as a defining one when selecting results for the inclusion in Foundations.

Part A was created as a separate file on Dec. 3, 2014.

Together with Part B it contains those results that do not require any axioms.

This file was edited and expanded by Benedikt Ahrens 2014-2016, Dan Grayson 2014-2016, Vladimir Voevodsky 2014-2016, Alex Kavvos 2014, Peter LeFanu Lumsdaine 2016 and Tomi Pannila 2016.

Preamble
- Settings
- Imports
Some standard constructions not using identity types (paths)
- Canonical functions from empty and to unit
- Identity functions and function composition, curry and uncurry
- Iteration of an endomorphism
- Basic constructions related to the adjoint evaluation function X → ((X → Y) → Y)
- Pairwise direct products
- Negation and double negation
- Logical equivalence
Paths and operations on paths
- Associativity of function composition and mutual invertibility of curry/uncurry
- Composition of paths and inverse paths
- Direct product of paths
- The function maponpaths between paths types defined by a function between ambient types
- maponpaths for the identity functions and compositions of functions
- Homotopy between functions
- Equality between functions defines a homotopy
- maponpaths for a function homotopic to the identity
- maponpaths in the case of a projection p with a section s
- Fibrations and paths - the transport functions
- A series of lemmas about paths and total2
- Lemmas about transport adapted from the HoTT library and the HoTT book
- Homotopies between families and the total spaces
First fundamental notions
- Contractibility iscontr
- Homotopy fibers hfiber
- The functions between the hfibers of homotopic functions over the same point
- Paths in homotopy fibers
- Coconuses: spaces of paths that begin (coconusfromt) or end (coconustot) at a given point
- The total paths space of a type - two definitions
- Coconus of a function: the total space of the family of h-fibers
Weak equivalences
- Basics - isweq and weq
- Weak equivalences and paths spaces (more results in further sections)
- Adjointness property of a weak equivalence and its inverse
- Transport functions are weak equivalences
- Weak equivalences between contractible types (one implication)
- Unit and contractibility
- Homotopy equivalence is a weak equivalence
- Some weak equivalences
- 2-out-of-3 property of weak equivalences
- Any function between contractible types is a weak equivalence
- Composition of weak equivalences
- 2-out-of-6 property of weak equivalences
- Pairwise direct products of weak equivalences
- Weak equivalence of a type and its direct product with the unit
- Associativity of total2 as a weak equivalence
- Associativity and commutativity of direct products as weak equivalences
Binary coproducts and their basic properties
- Distributivity of coproducts and direct products as a weak equivalence
- Total space of a family over a coproduct
- Pairwise sum of functions, coproduct associativity and commutativity
- Coproduct with a "negative" type
- Coproduct of two functions
- The equality_cases construction and four applications to ii1 and ii2
- Bool as coproduct
- Pairwise coproducts as dependent sums of families over bool
- Splitting of X into a coproduct defined by a function X → Y ⨿ Z
- Some properties of bool
- Fibrations with only one non-empty fiber
Basics about fibration sequences
- The structures of a complex and of a fibration sequence on a composable pair of functions
- Construction of the derived fibration sequence
- Explicit description of the first map in the second derived sequence
- Fibration sequences based on tpair P z and pr1 : total2 P → Z ( the "pr1-case" )
- Fibration sequences based on hfiberpr1 : hfiber g z → Y and g : Y → Z (the "g-case")
- Fibration sequence of h-fibers defined by a composable pair of functions (the "hf-case")
Functions between total spaces of families
- Function totalfun between total spaces from a family of functions between the fibers
- Function fpmap between the total spaces from a function between the bases
- Homotopy fibers of fpmap
- The fpmap from a weak equivalence is a weak equivalence
- Total spaces of families over a contractible base
- Function on the total spaces from functions between the bases and between the fibers
Homotopy fiber squares
- Homotopy commutative squares
- Short complexes and homotopy commutative squares
- Homotopy fiber products
- Homotopy fiber products and homotopy fibers
- Homotopy fiber squares
- Fiber sequences and homotopy fiber squares

Preamble

Imports

Require Export UniMath.Foundations.Preamble.

Some standard constructions not using identity types (paths)

Canonical functions from empty and to unit

Definition fromempty : ∏ X : UU , empty → X. Proof.
  intro X.
  intro H.
  induction H.
Defined.

Arguments fromempty { X } _.

Definition tounit {X : UU} : X → unit := λ _, tt.

Functions from unit corresponding to terms

Definition termfun {X : UU} (x : X) : unit → X := λ _, x.

Identity functions and function composition, curry and uncurry

Definition idfun (T : UU) := λ t:T , t.

makes simpl, cbn, etc. unfold idfun X x but not idfun X :

Arguments idfun _ _ /.

Definition funcomp {X Y : UU} {Z:Y →UU} (f : X → Y) (g : ∏ y:Y , Z y) := λ x , g (f x).

make simpl, cbn, etc. unfold (f ∘ g) x but not f ∘ g :

Arguments funcomp {_ _ _} _ _ _/.

Declare Scope functions.
Delimit Scope functions with functions.

Open Scope functions.

Notation "g ∘ f" := (funcomp f g) : functions.

back and forth between functions of pairs and functions returning functions

Definition curry {X : UU} {Y : X → UU} {Z : (∑ x , Y x ) → UU}
           (f : ∏ p , Z p) : (∏ x : X , ∏ y : Y x , Z (x ,, y)) :=
  λ x y , f (x ,, y).

Definition uncurry {X : UU} {Y : X → UU} {Z : (∑ x , Y x ) → UU}
           (g : ∏ x : X , ∏ y : Y x , Z (x ,, y)) : (∏ p , Z p) :=
  λ x , g (pr1 x) (pr2 x).

Definition of binary operation

Definition binop (X : UU) : UU := X → X → X.

Iteration of an endomorphism

Definition iteration {T : UU} (f : T → T) (n : nat) : T → T.
Proof.
  induction n as [ | n IHn ].
  + exact (idfun T).
  + exact (f ∘ IHn).
Defined.

Basic constructions related to the adjoint evaluation function X → ((X → Y) → Y)

Definition adjev {X Y : UU} (x : X) (f : X → Y) : Y := f x.

Definition adjev2 {X Y : UU} (phi : ((X → Y ) → Y ) → Y) : X → Y :=
λ x , phi (λ f , f x).

Pairwise direct products

Definition dirprod (X Y : UU) := ∑ x:X , Y.

Notation "A × B" := (dirprod A B) : type_scope.

Definition dirprod_pr1 {X Y : UU} := pr1 : X × Y → X.
Definition dirprod_pr2 {X Y : UU} := pr2 : X × Y → Y.

Definition make_dirprod {X Y : UU} (x:X) (y:Y) : X × Y := x ,,y.

Definition dirprodadj {X Y Z : UU} (f : X × Y → Z) : X → Y → Z :=
  λ x y , f (x ,,y).

Definition dirprodf {X Y X' Y' : UU}
           (f : X → Y) (f' : X' → Y') (xx' : X × X') : Y × Y' :=
  make_dirprod (f (pr1 xx')) (f' (pr2 xx')).

Definition ddualand {X Y P : UU}
           (xp : (X → P ) → P) (yp : (Y → P ) → P) : (X × Y → P ) → P.
Proof.
  intros X0.
  apply xp. intro x.
  apply yp. intro y.
  apply (X0 (make_dirprod x y)).
Defined.

Negation and double negation

Definition neg (X : UU) : UU := X → empty.

Notation "'¬' X" := (neg X).

Notation "x != y" := (neg (x = y)) : type_scope.

Definition negf {X Y : UU} (f : X → Y) : ¬ Y → ¬ X := λ phi x , phi (f x).

Definition dneg (X : UU) : UU := ¬ ¬ X.

Notation "'¬¬' X" := (dneg X).

Definition dnegf {X Y : UU} (f : X → Y) : dneg X → dneg Y :=
  negf (negf f).

Definition todneg (X : UU) : X → dneg X := adjev.

Definition dnegnegtoneg {X : UU} : ¬¬ ¬ X → ¬ X := adjev2.

Lemma dneganddnegl1 {X Y : UU} (dnx : ¬¬ X) (dny : ¬¬ Y) : ¬ (X → ¬ Y ).
Proof.
  intros.
  intros X2.
  apply (dnegf X2).
  + apply dnx.
  + apply dny.
Defined.

Definition dneganddnegimpldneg {X Y : UU}
           (dnx : ¬¬ X) (dny : ¬¬ Y) : ¬¬ (X × Y ) := ddualand dnx dny.

Logical equivalence

Definition logeq (X Y : UU) := (X → Y ) × (Y → X ).
Notation " X <-> Y " := (logeq X Y) : type_scope.

Lemma isrefl_logeq (X : UU) : X ↔ X.
Proof.
  intros. split; apply idfun.
Defined.

Lemma issymm_logeq (X Y : UU) : (X ↔ Y ) → (Y ↔ X ).
Proof.
  intros e.
  exact (pr2 e,,pr1 e).
Defined.

Definition logeqnegs {X Y : UU} (l : X ↔ Y) : (¬ X ) ↔ (¬ Y ) :=
  make_dirprod (negf (pr2 l)) (negf (pr1 l)).

Definition logeq_both_true {X Y : UU} : X → Y → (X ↔ Y ).
Proof.
  intros x y.
  split.
  - intros x'. exact y.
  - intros y'. exact x.
Defined.

Definition logeq_both_false {X Y : UU} : ¬X → ¬Y → (X ↔ Y ).
Proof.
  intros nx ny.
  split.
  - intros x. induction (nx x).
  - intros y. induction (ny y).
Defined.

Definition logeq_trans {X Y Z : UU} : (X ↔ Y ) → (Y ↔ Z ) → (X ↔ Z ).
Proof.
  intros i j. exact (pr1 j ∘ pr1 i,, pr2 i ∘ pr2 j).
Defined.

Paths and operations on paths

Associativity of function composition and mutual invertibility of curry/uncurry

While the paths in two of the three following lemmas are trivial, having them as lemmas turns out to be convenient in some future proofs. They are used to apply a particular definitional equality to modify the syntactic form of the goal in order to make the next tactic, which uses the syntactic form of the goal to guess how to proceed, to work.

The same applies to other lemmas below whose proof is by immediate "reflexivity" or "idpath".

Lemma funcomp_assoc {X Y Z W : UU} (f : X → Y) (g : Y → Z) (h : Z → W)
: h ∘ (g ∘ f ) = (h ∘ g ) ∘ f.
Proof.
  intros .
  apply idpath.
Defined.

Lemma uncurry_curry {X Z : UU} {Y : X → UU} (f : (∑ x : X , Y x ) → Z) :
  ∏ p , uncurry (curry f) p = f p.
Proof.
  intros. induction p as [x y]. apply idpath.
Defined.

Lemma curry_uncurry {X Z : UU} {Y : X → UU} (g : ∏ x : X , Y x → Z) :
  ∏ x y , curry (uncurry g) x y = g x y.
Proof.
  intros. apply idpath.
Defined.

Composition of paths and inverse paths

Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c.
Proof.
intros. induction e1. apply e2.
Defined.

Hint Resolve @pathscomp0 : pathshints.

Ltac intermediate_path x := apply (pathscomp0 (b := x)).
Ltac etrans := eapply pathscomp0.

Notation "p @ q" := (pathscomp0 p q).

Definition pathscomp0rid {X : UU} {a b : X} (e1 : a = b) : e1 @ idpath b = e1.
Proof.
intros. induction e1. simpl. apply idpath.
Defined.

Note that we do not introduce pathscomp0lid since the corresponding two terms are convertible to each other due to our definition of pathscomp0 . If we defined it by inductioning e2 and applying e1 then pathscomp0rid would be trivial but pathscomp0lid would require a proof. Similarly we do not introduce a lemma to connect pathsinv0 (idpath _) to idpath .

Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a.
Proof.
  intros. induction e. apply idpath.
Defined.

Hint Resolve @pathsinv0 : pathshints.

Definition path_assoc {X} {a b c d:X}
           (f : a = b) (g : b = c) (h : c = d)
  : f @ (g @ h ) = (f @ g ) @ h.
Proof.
  intros. induction f. apply idpath.
Defined.

Notation "! p " := (pathsinv0 p).

Definition pathsinv0l {X : UU} {a b : X} (e : a = b) : !e @ e = idpath _.
Proof.
  intros. induction e. apply idpath.
Defined.

Definition pathsinv0r {X : UU} {a b : X} (e : a = b) : e @ !e = idpath _.
Proof.
  intros. induction e. apply idpath.
Defined.

Definition pathsinv0inv0 {X : UU} {x x' : X} (e : x = x') : !(!e ) = e.
Proof.
  intros. induction e. apply idpath.
Defined.

Lemma pathscomp_cancel_left {X : UU} {x y z : X} (p : x = y) (r s : y = z) :
  p @ r = p @ s → r = s.
Proof.
  intros e. induction p. exact e.
Defined.

Lemma pathscomp_cancel_right {X : UU} {x y z : X} (p q : x = y) (s : y = z) :
  p @ s = q @ s → p = q.
Proof.
  intros e. induction s. refine (_ @ e @ _).
  - apply pathsinv0, pathscomp0rid.
  - apply pathscomp0rid.
Defined.

Lemma pathscomp_inv {X : UU} {x y z : X} (p : x = y) (q : y = z)
  : !(p @ q ) = !q @ !p.
Proof.
  induction p. induction q.
  apply idpath.
Defined.

Direct product of paths

Definition pathsdirprod {X Y : UU} {x1 x2 : X} {y1 y2 : Y}
           (ex : x1 = x2) (ey : y1 = y2) :
  make_dirprod x1 y1 = make_dirprod x2 y2.
Proof.
  intros. induction ex. induction ey. apply idpath.
Defined.

Lemma dirprodeq (A B : UU) (ab ab' : A × B) :
  pr1 ab = pr1 ab' → pr2 ab = pr2 ab' → ab = ab'.
Proof.
  intros H H'.
  induction ab as [a b].
  induction ab' as [a' b']; simpl in ×.
  induction H.
  induction H'.
  apply idpath.
Defined.

The function maponpaths between paths types defined by a function between ambient types

and its behavior relative to @ and !

Definition maponpaths {T1 T2 : UU} (f : T1 → T2) {t1 t2 : T1}
           (e: t1 = t2) : f t1 = f t2.
Proof.
  intros. induction e. apply idpath.
Defined.

Definition map_on_two_paths {X Y Z : UU} (f : X → Y → Z) {x x' y y'} (ex : x = x') (ey: y = y') :
  f x y = f x' y'.
Proof.
  intros. induction ex. induction ey. apply idpath.
Defined.

Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X}
           (f : X → Y) (e1 : x1 = x2) (e2 : x2 = x3) :
  maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2.
Proof.
  intros. induction e1. induction e2. apply idpath.
Defined.

Definition maponpathsinv0 {X Y : UU} (f : X → Y)
           {x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e ).
Proof.
  intros. induction e. apply idpath.
Defined.

maponpaths for the identity functions and compositions of functions

Lemma maponpathsidfun {X : UU} {x x' : X}
      (e : x = x') : maponpaths (idfun _) e = e.
Proof.
  intros. induction e. apply idpath.
Defined.

Lemma maponpathscomp {X Y Z : UU} {x x' : X} (f : X → Y) (g : Y → Z)
      (e : x = x') : maponpaths g (maponpaths f e) = maponpaths (g ∘ f) e.
Proof.
  intros. induction e. apply idpath.
Defined.

Homotopy between sections

Definition homot {X : UU} {P : X → UU} (f g : ∏ x : X , P x) := ∏ x : X , f x = g x.

Notation "f ~ g" := (homot f g).

Definition homotrefl {X : UU} {P : X → UU} (f: ∏ x : X , P x) : f ¬ f.
Proof.
  intros x. apply idpath.
Defined.

Definition homotcomp {X:UU} {Y:X →UU} {f f' f'' : ∏ x : X , Y x}
           (h : f ¬ f') (h' : f' ¬ f'') : f ¬ f'' := λ x , h x @ h' x.

Definition invhomot {X:UU} {Y:X →UU} {f f' : ∏ x : X , Y x}
           (h : f ¬ f') : f' ¬ f := λ x , !(h x ).

Definition funhomot {X Y Z:UU} (f : X → Y) {g g' : Y → Z}
           (h : g ¬ g') : g ∘ f ¬ g' ∘ f := λ x , h (f x).

Definition funhomotsec {X Y:UU} {Z:Y →UU} (f : X → Y) {g g' : ∏ y:Y , Z y}
           (h : g ¬ g') : g ∘ f ¬ g' ∘ f := λ x , h (f x).

Definition homotfun {X Y Z : UU} {f f' : X → Y} (h : f ¬ f')
           (g : Y → Z) : g ∘ f ¬ g ∘ f' := λ x , maponpaths g (h x).

Equality between functions defines a homotopy

Definition toforallpaths {T:UU} (P:T →UU) (f g:∏ t:T , P t) : f = g → f ¬ g.
Proof.
intros h t. induction h. apply (idpath _).
Defined.

Definition eqtohomot {T:UU} {P:T →UU} {f g:∏ t:T , P t} : f = g → f ¬ g.
Proof.
intros e t. induction e. apply idpath.
Defined.

maponpaths for a function homotopic to the identity

The following three statements show that maponpaths defined by a function f which is homotopic to the identity is "surjective". It is later used to show that the maponpaths defined by a function which is a weak equivalence is itself a weak equivalence.

Note that the type of the assumption h below can equivalently be written as homot f ( idfun X )

Definition maponpathshomidinv {X : UU} (f : X → X)
           (h : ∏ x : X , f x = x) (x x' : X) (e : f x = f x') :
  x = x' := ! (h x ) @ e @ (h x').

Lemma maponpathshomid1 {X : UU} (f : X → X) (h: ∏ x : X , f x = x)
      {x x' : X} (e : x = x') : maponpaths f e = (h x ) @ e @ (! h x').
Proof.
  intros. induction e. simpl.
  apply pathsinv0.
  apply pathsinv0r.
Defined.

Lemma maponpathshomid2 {X : UU} (f : X → X) (h : ∏ x : X , f x = x)
      (x x' : X) (e: f x = f x') :
  maponpaths f (maponpathshomidinv f h _ _ e) = e.
Proof.
  intros.
  unfold maponpathshomidinv.
  apply (pathscomp0 (maponpathshomid1 f h (! h x @ e @ h x'))).

  assert (l : ∏ (X : UU) (a b c d : X) (p : a = b) (q : a = c) (r : c = d ),
              p @ (!p @ q @ r ) @ !r = q).
  { intros. induction p. induction q. induction r. apply idpath. }

  apply (l _ _ _ _ _ (h x) e (h x')).
Defined.

maponpaths in the case of a projection p with a section s

Note that the type of the assumption eps below can equivalently be written as homot ( funcomp s p ) ( idfun X )

Definition pathssec1 {X Y : UU} (s : X → Y) (p : Y → X)
           (eps : ∏ (x : X ) , p (s x) = x)
           (x : X) (y : Y) (e : s x = y) : x = p y.
Proof.
  intros.
  apply (pathscomp0 (! eps x)).
  apply (maponpaths p e).
Defined.

Definition pathssec2 {X Y : UU} (s : X → Y) (p : Y → X)
           (eps : ∏ (x : X ), p (s x) = x)
           (x x' : X) (e : s x = s x') : x = x'.
Proof.
  intros.
  set (e' := pathssec1 s p eps _ _ e).
  apply (e' @ (eps x')).
Defined.

Definition pathssec2id {X Y : UU} (s : X → Y) (p : Y → X)
           (eps : ∏ x : X , p (s x) = x)
           (x : X) : pathssec2 s p eps _ _ (idpath (s x)) = idpath x.
Proof.
  intros.
  unfold pathssec2. unfold pathssec1. simpl.
  assert (e : ∏ X : UU , ∏ a b : X ,
                                ∏ p : a = b , (! p @ idpath _) @ p = idpath _).
  { intros. induction p0. simpl. apply idpath. }
  apply e.
Defined.

Definition pathssec3 {X Y : UU} (s : X → Y) (p : Y → X)
           (eps : ∏ x : X , p (s x) = x) {x x' : X} (e : x = x') :
  pathssec2 s p eps _ _ (maponpaths s e) = e.
Proof.
  intros. induction e. simpl.
  apply pathssec2id.
Defined.

Fibrations and paths - the transport functions

Definition constr1 {X : UU} (P : X → UU) {x x' : X} (e : x = x') :
  ∑ (f : P x → P x'),
  ∑ (ee : ∏ p : P x , tpair _ x p = tpair _ x' (f p)),
  ∏ (pp : P x ), maponpaths pr1 (ee pp) = e.
Proof.
  intros. induction e.
  split with (idfun (P x)).
  split with (λ p , idpath _).
  unfold maponpaths. simpl.
  intro. apply idpath.
Defined.

Definition transportf {X : UU} (P : X → UU) {x x' : X}
           (e : x = x') : P x → P x' := pr1 (constr1 P e).

Definition transportf_eq {X : UU} (P : X → UU) {x x' : X} (e : x = x') ( p : P x ) :
  tpair _ x p = tpair _ x' ( transportf P e p ) := ( pr1 ( pr2 ( constr1 P e ))) p .

Definition transportb {X : UU} (P : X → UU) {x x' : X}
           (e : x = x') : P x' → P x := transportf P (!e).

Declare Scope transport.
Notation "p # x" := (transportf _ p x) (only parsing) : transport.
Notation "p #' x" := (transportb _ p x) (only parsing) : transport.
Delimit Scope transport with transport.

Definition idpath_transportf {X : UU} (P : X → UU) {x : X} (p : P x) :
  transportf P (idpath x) p = p.
Proof.
  intros. apply idpath.
Defined.

Lemma functtransportf {X Y : UU} (f : X → Y) (P : Y → UU) {x x' : X}
      (e : x = x') (p : P (f x)) :
  transportf (λ x , P (f x)) e p = transportf P (maponpaths f e) p.
Proof.
  intros. induction e. apply idpath.
Defined.

Lemma functtransportb {X Y : UU} (f : X → Y) (P : Y → UU) {x x' : X}
      (e : x' = x) (p : P (f x)) :
  transportb (λ x , P (f x)) e p = transportb P (maponpaths f e) p.
Proof.
  intros. induction e. apply idpath.
Defined.

Definition transport_f_b {X : UU} (P : X →UU) {x y z : X} (e : y = x)
           (e' : y = z) (p : P x) :
  transportf P e' (transportb P e p) = transportf P (!e @ e') p.
Proof.
  intros. induction e'. induction e. apply idpath.
Defined.

Definition transport_b_f {X : UU} (P : X →UU) {x y z : X} (e : x = y)
           (e' : z = y) (p : P x) :
  transportb P e' (transportf P e p) = transportf P (e @ !e') p.
Proof.
  intros. induction e'. induction e. apply idpath.
Defined.

Definition transport_f_f {X : UU} (P : X →UU) {x y z : X} (e : x = y)
           (e' : y = z) (p : P x) :
  transportf P e' (transportf P e p) = transportf P (e @ e') p.
Proof.
  intros. induction e'. induction e. apply idpath.
Defined.

Definition transport_b_b {X : UU} (P : X →UU) {x y z : X} (e : x = y)
           (e' : y = z) (p : P z) :
  transportb P e (transportb P e' p) = transportb P (e @ e') p.
Proof.
  intros. induction e'. induction e. apply idpath.
Defined.

Definition transport_map {X : UU} {P Q : X → UU} (f : ∏ x , P x → Q x)
           {x : X} {y : X} (e : x = y) (p : P x) :
  transportf Q e (f x p) = f y (transportf P e p).
Proof.
  intros. induction e. apply idpath.
Defined.

Definition transport_section {X : UU} {P:X → UU} (f : ∏ x , P x)
           {x : X} {y : X} (e : x = y) :
  transportf P e (f x) = f y.
Proof.
  intros. exact (transport_map (P:= λ _,unit) (λ x _,f x) e tt).
Defined.

Definition transportf_fun {X Y : UU}(P : X → UU)
           {x1 x2 : X}(e : x1 = x2)(f : P x1 → Y) :
  transportf (λ x , (P x → Y )) e f = f ∘ transportb P e .
Proof.
  intros. induction e. apply idpath .
Defined.

Lemma transportb_fun' {X:UU} {P:X →UU} {Z:UU}
      {x x':X} (f:P x'→Z) (p:x =x') (y:P x) :
  f (transportf P p y) = transportb (λ x , P x →Z) p f y.
Proof.
  intros. induction p. apply idpath.
Defined.

Definition transportf_const {X : UU}{x1 x2 : X}(e : x1 = x2)(Y : UU) :
  transportf (λ x , Y) e = idfun Y.
Proof.
  intros. induction e. apply idpath.
Defined.

Definition transportb_const {X : UU}{x1 x2 : X}(e : x1 = x2)(Y : UU) :
  transportb (λ x , Y) e = idfun Y.
Proof.
  intros. induction e. apply idpath.
Defined.

Lemma transportf_paths {X : UU} (P : X → UU) {x1 x2 : X} {e1 e2 : x1 = x2} (e : e1 = e2)
      (p : P x1) : transportf P e1 p = transportf P e2 p.
Proof.
  induction e. apply idpath.
Defined.
Opaque transportf_paths.

Local Open Scope transport.

Definition transportbfinv {T} (P:T →Type) {t u:T} (e:t = u) (p:P t) : e #'e #p = p.
Proof.
  intros. induction e. apply idpath.
Defined.

Definition transportfbinv {T} (P:T →Type) {t u:T} (e:t = u) (p:P u) : e #e #'p = p.
Proof.
  intros. induction e. apply idpath.
Defined.

Close Scope transport.

A series of lemmas about paths and total2

Some lemmas are adapted from the HoTT library http://github.com/HoTT/HoTT

Lemma base_paths {A : UU} {B : A → UU}
      (a b : total2 B) : a = b → pr1 a = pr1 b.
Proof.
  intros.
  apply maponpaths; assumption.
Defined.

Lemma two_arg_paths {A B C:UU} {f : A → B → C} {a1 b1 a2 b2} (p : a1 = a2)
      (q : b1 = b2) : f a1 b1 = f a2 b2.
Proof.
  intros. induction p. induction q. apply idpath.
Defined.

Lemma two_arg_paths_f {A : UU} {B : A → UU} {C:UU} {f : ∏ a , B a → C} {a1 b1 a2 b2}
      (p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2.
Proof.
  intros. induction p. induction q. apply idpath.
Defined.

Lemma two_arg_paths_b {A : UU} {B : A → UU} {C:UU} {f : ∏ a , B a → C} {a1 b1 a2 b2}
      (p : a1 = a2) (q : b1 = transportb B p b2) : f a1 b1 = f a2 b2.
Proof.
  intros. induction p. change _ with (b1 = b2) in q. induction q. apply idpath.
Defined.

Lemma dirprod_paths {A : UU} {B : UU} {s s' : A × B}
      (p : pr1 s = pr1 s') (q : pr2 s = pr2 s') : s = s'.
Proof.
  intros.
  induction s as [a b]; induction s' as [a' b']; simpl in ×.
  exact (two_arg_paths p q).
Defined.

Lemma total2_paths_f {A : UU} {B : A → UU} {s s' : ∑ x , B x}
      (p : pr1 s = pr1 s')
      (q : transportf B p (pr2 s) = pr2 s') : s = s'.
Proof.
  intros.
  induction s as [a b]; induction s' as [a' b']; simpl in ×.
  exact (two_arg_paths_f p q).
Defined.

Lemma total2_paths_b {A : UU} {B : A → UU} {s s' : ∑ x , B x}
      (p : pr1 s = pr1 s')
      (q : pr2 s = transportb B p (pr2 s')) : s = s'.
Proof.
  intros.
  induction s as [a b]; induction s' as [a' b']; simpl in ×.
  exact (two_arg_paths_b p q).
Defined.

Lemma total2_paths2 {A : UU} {B : UU} {a1 a2:A} {b1 b2:B}
      (p : a1 = a2) (q : b1 = b2) : a1 ,,b1 = a2 ,,b2.
Proof.
  intros. exact (two_arg_paths p q).
Defined.

Lemma total2_paths2_f {A : UU} {B : A → UU} {a1 : A} {b1 : B a1}
      {a2 : A} {b2 : B a2} (p : a1 = a2)
      (q : transportf B p b1 = b2) : a1 ,,b1 = a2 ,,b2.
Proof.
  intros. exact (two_arg_paths_f p q).
Defined.

Lemma total2_paths2_b {A : UU} {B : A → UU} {a1 : A} {b1 : B a1}
  {a2 : A} {b2 : B a2} (p : a1 = a2)
  (q : b1 = transportb B p b2) : a1 ,,b1 = a2 ,,b2.
Proof.
  intros. exact (two_arg_paths_b p q).
Defined.

Definition pair_path_in2 {X : UU} (P : X → UU) {x : X} {p q : P x} (e : p = q) :
  x ,,p = x ,,q.
Proof.
  intros. apply maponpaths. exact e.
Defined.

Definition fiber_paths {A : UU} {B : A → UU} {u v : ∑ x , B x} (p : u = v) :
  transportf (λ x , B x) (base_paths _ _ p) (pr2 u) = pr2 v.
Proof.
  induction p.
  apply idpath.
Defined.

Lemma total2_fiber_paths {A : UU} {B : A → UU} {x y : ∑ x , B x} (p : x = y) :
  total2_paths_f _ (fiber_paths p) = p.
Proof.
  induction p.
  induction x.
  apply idpath.
Defined.

Lemma base_total2_paths {A : UU} {B : A → UU} {x y : ∑ x , B x}
      {p : pr1 x = pr1 y} (q : transportf _ p (pr2 x) = pr2 y) :
  (base_paths _ _ (total2_paths_f _ q)) = p.
Proof.
  induction x as [x H].
  induction y as [y K].
  simpl in ×.
  induction p.
  induction q.
  apply idpath.
Defined.

Lemma transportf_fiber_total2_paths {A : UU} (B : A → UU)
      (x y : ∑ x , B x)
      (p : pr1 x = pr1 y) (q : transportf _ p (pr2 x) = pr2 y) :
  transportf (λ p' : pr1 x = pr1 y , transportf _ p' (pr2 x) = pr2 y)
             (base_total2_paths q) (fiber_paths (total2_paths_f _ q)) = q.
Proof.
  induction x as [x H].
  induction y as [y K].
  simpl in ×.
  induction p.
  induction q.
  apply idpath.
Defined.

Definition total2_base_map {S T:UU} {P: T → UU} (f : S →T) : (∑ i , P(f i)) → (∑ j , P j ).
Proof.
  intros x.
  exact (f(pr1 x),,pr2 x).
Defined.

Lemma total2_section_path {X:UU} {Y:X →UU} (a:X) (b:Y a) (e:∏ x , Y x) : (a ,,e a ) = (a ,,b ) → e a = b.
Proof.
  intros p. simple refine (_ @ fiber_paths p). unfold base_paths. simpl.
  apply pathsinv0, transport_section.
Defined.

Lemmas about transport adapted from the HoTT library and the HoTT book

Definition transportD {A : UU} (B : A → UU) (C : ∏ a : A , B a → UU)
           {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1 y) :
  C x2 (transportf _ p y).
Proof.
  intros.
  induction p.
  exact z.
Defined.

Definition transportf_total2 {A : UU} {B : A → UU} {C : ∏ a:A , B a → UU}
           {x1 x2 : A} (p : x1 = x2) (yz : ∑ y : B x1 , C x1 y) :
  transportf (λ x , ∑ y : B x , C x y) p yz =
  tpair (λ y , C x2 y) (transportf _ p (pr1 yz))
        (transportD _ _ p (pr1 yz) (pr2 yz)).
Proof.
  intros.
  induction p.
  induction yz.
  apply idpath.
Defined.

Definition transportf_dirprod (A : UU) (B B' : A → UU)
           (x x' : ∑ a , B a × B' a) (p : pr1 x = pr1 x') :
  transportf (λ a , B a × B' a) p (pr2 x) =
  make_dirprod (transportf (λ a , B a) p (pr1 (pr2 x)))
              (transportf (λ a , B' a) p (pr2 (pr2 x))).
Proof.
  induction p.
  apply idpath.
Defined.

Definition transportb_dirprod (A : UU) (B B' : A → UU)
  (x x' : ∑ a , B a × B' a) (p : pr1 x = pr1 x') :
  transportb (λ a , B a × B' a) p (pr2 x') =
    make_dirprod (transportb (λ a , B a) p (pr1 (pr2 x')))
                (transportb (λ a , B' a) p (pr2 (pr2 x'))).
Proof.
  intros.
  apply transportf_dirprod.
Defined.

Definition transportf_id1 {A : UU} {a x1 x2 : A}
           (p : x1 = x2) (q : a = x1) :
  transportf (λ (x : A ), a = x) p q = q @ p.
Proof.
  intros. induction p. induction q. apply idpath.
Defined.

Definition transportf_id2 {A : UU} {a x1 x2 : A}
           (p : x1 = x2) (q : x1 = a) :
  transportf (λ (x : A ), x = a) p q = !p @ q.
Proof.
  intros. induction p. induction q. apply idpath.
Defined.

Definition transportf_id3 {A : UU} {x1 x2 : A}
           (p : x1 = x2) (q : x1 = x1) :
  transportf (λ (x : A ), x = x) p q = !p @ q @ p.
Proof.
  intros. induction p. simpl. apply pathsinv0. apply pathscomp0rid.
Defined.

Homotopies between families and the total spaces

Definition famhomotfun {X : UU} {P Q : X → UU}
           (h : P ¬ Q) (xp : total2 P) : total2 Q.
Proof.
  intros.
  ∃ (pr1 xp).
  induction (h (pr1 xp)).
  apply (pr2 xp).
Defined.

Definition famhomothomothomot {X : UU} {P Q : X → UU} (h1 h2 : P ¬ Q)
           (H : h1 ¬ h2) : famhomotfun h1 ¬ famhomotfun h2.
Proof.
  intros.
  intro xp.
  apply (maponpaths (λ q , tpair Q (pr1 xp) q)).
  induction (H (pr1 xp)).
  apply idpath.
Defined.

First fundamental notions

Contractibility iscontr

Definition iscontr (T:UU) : UU := ∑ cntr:T , ∏ t:T , t =cntr.

Notation "'∃!' x .. y , P"
  := (iscontr (∑ x , .. (∑ y , P) ..))
       (at level 200, x binder, y binder, right associativity) : type_scope.

Definition make_iscontr {T : UU} : ∏ x : T , (∏ t : T , t = x ) → iscontr T
  := tpair _.

Definition iscontrpr1 {T : UU} : iscontr T → T := pr1.

Definition iscontr_uniqueness {T} (i:iscontr T) (t:T) : t = iscontrpr1 i
  := pr2 i t.

Lemma iscontrretract {X Y : UU} (p : X → Y) (s : Y → X)
      (eps : ∏ y : Y , p (s y) = y) (is : iscontr X) : iscontr Y.
Proof.
  intros. set (x := iscontrpr1 is). set (fe := pr2 is). split with (p x).
  intro t. apply (! (eps t) @ maponpaths p (fe (s t))).
Defined.

Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'.
Proof.
  intros.
  apply ((pr2 is) x @ !(pr2 is x')).
Defined.

Lemma path_to_ctr (A : UU) (B : A → UU) (isc : ∃! a , B a)
      (a : A) (p : B a) : a = pr1 (pr1 isc).
Proof.
  set (Hi := tpair _ a p).
  apply (maponpaths pr1 (pr2 isc Hi)).
Defined.

Homotopy fibers hfiber

Definition hfiber {X Y : UU} (f : X → Y) (y : Y) : UU := ∑ x : X , f x = y.

Definition make_hfiber {X Y : UU} (f : X → Y) {y : Y}
           (x : X) (e : f x = y) : hfiber f y :=
  tpair _ x e.

Definition hfiberpr1 {X Y : UU} (f : X → Y) (y : Y) : hfiber f y → X := pr1.

Definition hfiberpr2 {X Y : UU} (f : X → Y) (y : Y) (y' : hfiber f y) : f (hfiberpr1 f y y') = y :=
  pr2 y'.

The functions between the hfibers of homotopic functions over the same point

Lemma hfibershomotftog {X Y : UU} (f g : X → Y)
      (h : f ¬ g) (y : Y) : hfiber f y → hfiber g y.
Proof.
  intros xe.
  induction xe as [x e].
  split with x.
  apply (!(h x) @ e).
Defined.

Lemma hfibershomotgtof {X Y : UU} (f g : X → Y)
      (h : f ¬ g) (y : Y) : hfiber g y → hfiber f y.
Proof.
  intros xe.
  induction xe as [x e].
  split with x.
  apply (h x @ e).
Defined.

Paths in homotopy fibers

Lemma hfibertriangle1 {X Y : UU} (f : X → Y) {y : Y} {xe1 xe2 : hfiber f y}
      (e : xe1 = xe2) :
  pr2 xe1 = maponpaths f (maponpaths pr1 e) @ pr2 xe2.
Proof.
  intros. induction e. simpl. apply idpath.
Defined.

Corollary hfibertriangle1' {X Y : UU} (f : X → Y) {x : X} {xe1: hfiber f (f x)}
          (e : xe1 = (x ,,idpath (f x))) :
  pr2 xe1 = maponpaths f (maponpaths pr1 e).
Proof.
  intros.
  intermediate_path (maponpaths f (maponpaths pr1 e) @ idpath (f x)).
  - apply hfibertriangle1.
  - apply pathscomp0rid.
Defined.

Lemma hfibertriangle1inv0 {X Y : UU} (f : X → Y) {y : Y} {xe1 xe2: hfiber f y}
      (e : xe1 = xe2) :
  maponpaths f (! (maponpaths pr1 e )) @ (pr2 xe1 ) = pr2 xe2.
Proof.
  intros. induction e. apply idpath.
Defined.

Corollary hfibertriangle1inv0' {X Y : UU} (f : X → Y) {x : X}
          {xe2: hfiber f (f x)} (e : (x ,,idpath (f x)) = xe2) :
  maponpaths f (! (maponpaths pr1 e )) = pr2 xe2.
Proof.
  intros.
  intermediate_path (maponpaths f (! (maponpaths pr1 e)) @ idpath (f x)).
  - apply pathsinv0, pathscomp0rid.
  - apply hfibertriangle1inv0.
Defined.

Lemma hfibertriangle2 {X Y : UU} (f : X → Y) {y : Y} (xe1 xe2: hfiber f y)
      (ee: pr1 xe1 = pr1 xe2) (eee: pr2 xe1 = maponpaths f ee @ (pr2 xe2 )) :
  xe1 = xe2.
Proof.
  intros.
  induction xe1 as [t e1].
  induction xe2 as [t' e2].
  simpl in ×.
  fold (make_hfiber f t e1).
  fold (make_hfiber f t' e2).
  induction ee.
  simpl in eee.
  apply (maponpaths (λ e , make_hfiber f t e) eee).
Defined.

Coconuses: spaces of paths that begin coconusfromt or end coconustot at a given point

Definition coconusfromt (T : UU) (t : T) := ∑ t' : T , t = t'.

Definition coconusfromtpair (T : UU) {t t' : T} (e: t = t') : coconusfromt T t
  := tpair _ t' e.

Definition coconusfromtpr1 (T : UU) (t : T) : coconusfromt T t → T := pr1.

Definition coconustot (T : UU) (t : T) := ∑ t' : T , t' = t.

Definition coconustotpair (T : UU) {t t' : T} (e: t' = t) : coconustot T t
  := tpair _ t' e.

Definition coconustotpr1 (T : UU) (t : T) : coconustot T t → T := pr1.

Lemma coconustot_isProofIrrelevant {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2.
Proof.
  intros.
  induction c1 as [x0 x].
  induction x.
  induction c2 as [x1 y].
  induction y.
  apply idpath.
Defined.

Lemma iscontrcoconustot (T : UU) (t : T) : iscontr (coconustot T t).
Proof.
  use (tpair _ (t,, idpath t)).
  intros [u []].
  reflexivity.
Defined.

Lemma coconusfromt_isProofIrrelevant {T : UU} {t : T} (c1 c2 : coconusfromt T t) : c1 = c2.
Proof.
  intros.
  induction c1 as [x0 x].
  induction x.
  induction c2 as [x1 y].
  induction y.
  apply idpath.
Defined.

Lemma iscontrcoconusfromt (T : UU) (t : T) : iscontr (coconusfromt T t).
Proof.
  use (tpair _ (t,, idpath t)).
  intros [u []].
  reflexivity.
Defined.

The total paths space of a type - two definitions

The definitions differ by the (non) associativity of the total2 .

Definition pathsspace (T : UU) := ∑ t:T , coconusfromt T t.

Definition pathsspacetriple (T : UU) {t1 t2 : T}
(e : t1 = t2) : pathsspace T := tpair _ t1 (coconusfromtpair T e).

Definition deltap (T : UU) : T → pathsspace T :=
λ (t : T ), pathsspacetriple T (idpath t).

Definition pathsspace' (T : UU) := ∑ xy : T × T , pr1 xy = pr2 xy.

Coconus of a function: the total space of the family of h-fibers

Definition coconusf {X Y : UU} (f : X → Y) := ∑ y:Y , hfiber f y.

Definition fromcoconusf {X Y : UU} (f : X → Y) : coconusf f → X :=
  λ yxe , pr1 (pr2 yxe).

Definition tococonusf {X Y : UU} (f : X → Y) : X → coconusf f :=
  λ x , tpair _ (f x) (make_hfiber f x (idpath _)).

Lemma homottofromcoconusf {X Y : UU} (f : X → Y) :
  ∏ yxe : coconusf f , tococonusf f (fromcoconusf f yxe) = yxe.
Proof.
  intros.
  induction yxe as [y xe].
  induction xe as [x e].
  unfold fromcoconusf.
  unfold tococonusf.
  simpl.
  induction e.
  apply idpath.
Defined.

Lemma homotfromtococonusf {X Y : UU} (f : X → Y) :
  ∏ x : X , fromcoconusf f (tococonusf f x) = x.
Proof.
  intros.
  unfold fromcoconusf.
  unfold tococonusf.
  simpl.
  apply idpath.
Defined.

Weak equivalences

Basics - isweq and weq

Definition isweq {X Y : UU} (f : X → Y) : UU :=
  ∏ y : Y , iscontr (hfiber f y).

Lemma idisweq (T : UU) : isweq (idfun T).
Proof.
  intros. unfold isweq. intro y.
  unfold iscontr.
  split with (make_hfiber (idfun T) y (idpath y)).
  intro t.
  induction t as [x e].
  induction e.
  apply idpath.
Defined.

Definition weq (X Y : UU) : UU := ∑ f:X →Y , isweq f.

Notation "X ≃ Y" := (weq X%type Y%type) : type_scope.

Definition pr1weq {X Y : UU} := pr1 : X ≃ Y → (X → Y ).
Coercion pr1weq : weq >-> Funclass.

Definition weqproperty {X Y} (f:X ≃Y) : isweq f := pr2 f.

Definition weqccontrhfiber {X Y : UU} (w : X ≃ Y) (y : Y) : hfiber w y.
Proof.
  intros. apply (iscontrpr1 (weqproperty w y)).
Defined.

Definition weqccontrhfiber2 {X Y : UU} (w : X ≃ Y) (y : Y) :
  ∏ x : hfiber w y , x = weqccontrhfiber w y.
Proof.
  intros. unfold weqccontrhfiber. apply (pr2 (pr2 w y)).
Defined.

Definition make_weq {X Y : UU} (f : X → Y) (is: isweq f) : X ≃ Y :=
  tpair (λ f : X → Y , isweq f) f is.

Definition idweq (X : UU) : X ≃ X :=
  tpair (λ f : X → X , isweq f) (λ (x : X ), x) (idisweq X).

Definition isweqtoempty {X : UU} (f : X → ∅) : isweq f.
Proof.
  intros. intro y. apply (fromempty y).
Defined.

Definition weqtoempty {X : UU} (f : X → ∅) : X ≃ ∅ :=
  make_weq _ (isweqtoempty f).

Lemma isweqtoempty2 {X Y : UU} (f : X → Y) (is : ¬ Y) : isweq f.
Proof.
  intros. intro y. induction (is y).
Defined.

Definition weqtoempty2 {X Y : UU} (f : X → Y) (is : ¬ Y) : X ≃ Y
  := make_weq _ (isweqtoempty2 f is).

Definition weqempty {X Y : UU} : ¬X → ¬Y → X ≃Y.
Proof.
  intros nx ny.
  use make_weq.
  - intro x. apply fromempty, nx. exact x.
  - intro y. apply fromempty, ny. exact y.
Defined.

Definition invmap {X Y : UU} (w : X ≃ Y) : Y → X :=
  λ (y : Y ), hfiberpr1 _ _ (weqccontrhfiber w y).

Weak equivalences and paths spaces (more results in further sections)

We now define different homotopies and maps between the paths spaces corresponding to a weak equivalence. What may look like unnecessary complexity in the definition of homotinvweqweq is due to the fact that the "naive" definition needs to be corrected in order for lemma homotweqinvweqweq to hold.

Definition homotweqinvweq {X Y : UU} (w : X ≃ Y) :
  ∏ y : Y , w (invmap w y) = y.
Proof.
  intros.
  unfold invmap.
  apply (pr2 (weqccontrhfiber w y)).
Defined.

Definition homotinvweqweq0 {X Y : UU} (w : X ≃ Y) :
  ∏ x : X , x = invmap w (w x).
Proof.
  intros.
  unfold invmap.
  set (xe1 := weqccontrhfiber w (w x)).
  set (xe2 := make_hfiber w x (idpath (w x))).
  set (p := weqccontrhfiber2 w (w x) xe2).
  apply (maponpaths pr1 p).
Defined.

Definition homotinvweqweq {X Y : UU} (w : X ≃ Y) :
  ∏ x : X , invmap w (w x) = x
  := λ (x : X ), ! (homotinvweqweq0 w x ).

Definition invmaponpathsweq {X Y : UU} (w : X ≃ Y) (x x' : X) :
  w x = w x' → x = x'
  := pathssec2 w (invmap w) (homotinvweqweq w) x x'.

Definition invmaponpathsweqid {X Y : UU} (w : X ≃ Y) (x : X) :
  invmaponpathsweq w _ _ (idpath (w x)) = idpath x
  := pathssec2id w (invmap w) (homotinvweqweq w) x.

Definition pathsweq1 {X Y : UU} (w : X ≃ Y) (x : X) (y : Y) :
  w x = y → x = invmap w y
  := λ e , maponpaths pr1 (pr2 (weqproperty w y) (x ,,e)).

Definition pathsweq1' {X Y : UU} (w : X ≃ Y) (x : X) (y : Y) :
  x = invmap w y → w x = y
  := λ e , maponpaths w e @ homotweqinvweq w y.

Definition pathsweq3 {X Y : UU} (w : X ≃ Y) {x x' : X}
           (e : x = x') : invmaponpathsweq w x x' (maponpaths w e) = e
  := pathssec3 w (invmap w) (homotinvweqweq w) _.

Definition pathsweq4 {X Y : UU} (w : X ≃ Y) (x x' : X)
           (e : w x = w x') : maponpaths w (invmaponpathsweq w x x' e) = e.
Proof.
  intros.
  induction w as [f is1].
  set (w := make_weq f is1).
  set (g := invmap w).
  set (ee := maponpaths g e).
  simpl in ×.
  set (eee := maponpathshomidinv (g ∘ f) (homotinvweqweq w) x x' ee).

  assert (e1 : maponpaths f eee = e).
  {
    assert (e2 : maponpaths (g ∘ f) eee = ee).
    { apply maponpathshomid2. }
    assert (e3 : maponpaths g (maponpaths f eee) = maponpaths g e).
    { apply (maponpathscomp f g eee @ e2). }
    set (s := @maponpaths _ _ g (f x) (f x')).
    set (p := @pathssec2 _ _ g f (homotweqinvweq w) (f x) (f x')).
    set (eps := @pathssec3 _ _ g f (homotweqinvweq w) (f x) (f x')).
    apply (pathssec2 s p eps _ _ e3).
  }

  assert (e4:
            maponpaths f (invmaponpathsweq w x x' (maponpaths f eee)) =
            maponpaths f (invmaponpathsweq w x x' e)).
  {
    apply (maponpaths (λ e0: f x = f x',
                         maponpaths f (invmaponpathsweq w x x' e0))
                      e1).
  }

  assert (X0 : invmaponpathsweq w x x' (maponpaths f eee) = eee).
  { apply (pathsweq3 w). }

  assert (e5: maponpaths f (invmaponpathsweq w x x' (maponpaths f eee))
              = maponpaths f eee).
  { apply (maponpaths (λ eee0: x = x', maponpaths f eee0) X0). }

  apply (! e4 @ e5 @ e1).
Defined.

Lemma homotweqinv {X Y Z} (f:X →Z) (w:X ≃Y) (g:Y →Z) : f ¬ g ∘ w → f ∘ invmap w ¬ g.
Proof.
  intros p y.
  simple refine (p (invmap w y) @ _); clear p.
  simpl. apply maponpaths. apply homotweqinvweq.
Defined.

Lemma homotweqinv' {X Y Z} (f:X →Z) (w:X ≃Y) (g:Y →Z) : f ¬ g ∘ w <- f ∘ invmap w ¬ g.
Proof.
  intros q x.
  simple refine (_ @ q (w x)).
  simpl. apply maponpaths, pathsinv0. apply homotinvweqweq.
Defined.

Definition isinjinvmap {X Y} (v w:X ≃Y) : invmap v ¬ invmap w → v ¬ w.
Proof.
  intros h x.
  intermediate_path (w ((invmap w) (v x))).
  { apply pathsinv0. apply homotweqinvweq. }
  rewrite <- h. rewrite homotinvweqweq. apply idpath.
Defined.

Definition isinjinvmap' {X Y} (v w:X →Y) (v' w':Y →X) : w ∘ w' ¬ idfun Y → v' ∘ v ¬ idfun X → v' ¬ w' → v ¬ w.
Proof.
  intros p q h x .
  intermediate_path (w (w' (v x))).
  { apply pathsinv0. apply p. }
  apply maponpaths. rewrite <- h. apply q.
Defined.

Adjointness property of a weak equivalence and its inverse

Lemma diaglemma2 {X Y : UU} (f : X → Y) {x x' : X}
      (e1 : x = x') (e2 : f x' = f x)
      (ee : idpath (f x) = maponpaths f e1 @ e2) : maponpaths f (! e1) = e2.
Proof.
  intros. induction e1. simpl in ×. exact ee.
Defined.

Definition homotweqinvweqweq {X Y : UU} (w : X ≃ Y) (x : X) :
  maponpaths w (homotinvweqweq w x) = homotweqinvweq w (w x).
Proof.
  intros.
  unfold homotinvweqweq.
  unfold homotinvweqweq0.
  set (hfid := make_hfiber w x (idpath (w x))).
  set (hfcc := weqccontrhfiber w (w x)).
  unfold homotweqinvweq.
  apply diaglemma2.
  apply (@hfibertriangle1 _ _ w _ hfid hfcc (weqccontrhfiber2 w (w x) hfid)).
Defined.

Definition weq_transportf_adjointness {X Y : UU} (w : X ≃ Y) (P : Y → UU)
           (x : X) (p : P (w x)) :
  transportf (P ∘ w) (! homotinvweqweq w x) p
  = transportf P (! homotweqinvweq w (w x)) p.
Proof.
  intros. refine (functtransportf w P (!homotinvweqweq w x) p @ _).
  apply (maponpaths (λ e , transportf P e p)).
  rewrite maponpathsinv0. apply maponpaths. apply homotweqinvweqweq.
Defined.

Definition weq_transportb_adjointness {X Y : UU} (w : X ≃ Y) (P : Y → UU)
           (x : X) (p : P (w x)) :
  transportb (P ∘ w) (homotinvweqweq w x) p
  = transportb P (homotweqinvweq w (w x)) p.
Proof.
  intros.
  refine (functtransportb w P (homotinvweqweq w x) p @ _).
  apply (maponpaths (λ e , transportb P e p)).
  apply homotweqinvweqweq.
Defined.

Transport functions are weak equivalences

Lemma isweqtransportf {X : UU} (P : X → UU) {x x' : X}
      (e : x = x') : isweq (transportf P e).
Proof.
  intros. induction e. unfold transportf. simpl. apply idisweq.
Defined.

Lemma isweqtransportb {X : UU} (P : X → UU) {x x' : X}
      (e : x = x') : isweq (transportb P e).
Proof.
  intros. apply (isweqtransportf _ (pathsinv0 e)).
Defined.

Weak equivalences between contractible types (one implication)

Lemma iscontrweqb {X Y : UU} (w : X ≃ Y) (is : iscontr Y) : iscontr X.
Proof.
intros. apply (iscontrretract (invmap w) w (homotinvweqweq w) is).
Defined.

unit and contractibility

unit is contractible (recall that tt is the name of the canonical term of the type unit ).

Lemma isProofIrrelevantUnit : ∏ x x' : unit , x = x'.
Proof.
  intros. induction x. induction x'. apply idpath.
Defined.

Lemma unitl0 : tt = tt → coconustot _ tt.
Proof.
  intros e. apply (coconustotpair unit e).
Defined.

Lemma unitl1: coconustot _ tt → tt = tt.
Proof.
  intro cp. induction cp as [x t]. induction x. exact t.
Defined.

Lemma unitl2: ∏ e : tt = tt , unitl1 (unitl0 e) = e.
Proof.
  intros. unfold unitl0. simpl. apply idpath.
Defined.

Lemma unitl3: ∏ e : tt = tt , e = idpath tt.
Proof.
  intros.

  assert (e0 : unitl0 (idpath tt) = unitl0 e).
  { apply coconustot_isProofIrrelevant. }

  set (e1 := maponpaths unitl1 e0).

  apply (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))).
Defined.

Theorem iscontrunit: iscontr (unit).
Proof.
  split with tt. intros t. apply (isProofIrrelevantUnit t tt).
Defined.

paths in unit are contractible.

Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x').
Proof.
  intros.
  split with (isProofIrrelevantUnit x x').
  intros e'.
  induction x.
  induction x'.
  simpl.
  apply unitl3.
Defined.

A type T : UU is contractible if and only if T → unit is a weak equivalence.

Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2.
Proof.
  intros.
  apply proofirrelevancecontr.
  apply (iscontrpathsinunit tt tt).
Defined.

Lemma isweqcontrtounit {T : UU} (is : iscontr T) : isweq (λ (_ : T ), tt).
Proof.
  intros. unfold isweq. intro y. induction y.
  induction is as [c h].
  set (hc := make_hfiber _ c (idpath tt)).
  split with hc.
  intros ha.
  induction ha as [x e].
  unfold hc. unfold make_hfiber. unfold isProofIrrelevantUnit.
  simpl.
  apply (λ q , two_arg_paths_f (h x) q).
  apply ifcontrthenunitl0.
Defined.

Definition weqcontrtounit {T : UU} (is : iscontr T) : T ≃ unit :=
  make_weq _ (isweqcontrtounit is).

Theorem iscontrifweqtounit {X : UU} (w : X ≃ unit) : iscontr X.
Proof.
  intros.
  apply (iscontrweqb w).
  apply iscontrunit.
Defined.

Homotopy equivalence is a weak equivalence

Definition hfibersgftog {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (xe : hfiber (g ∘ f) z) : hfiber g z :=
  make_hfiber g (f (pr1 xe)) (pr2 xe).

Lemma constr2 {X Y : UU} (f : X → Y) (g : Y → X)
      (efg: ∏ y : Y , f (g y) = y) (x0 : X) (xe : hfiber g x0) :
  ∑ xe' : hfiber (g ∘ f) x0 , xe = hfibersgftog f g x0 xe'.
Proof.
  intros.
  induction xe as [y0 e].
  set (eint := pathssec1 _ _ efg _ _ e).
  set (ee := ! (maponpaths g eint) @ e).
  split with (make_hfiber (g ∘ f) x0 ee).
  unfold hfibersgftog.
  unfold make_hfiber.
  simpl.
  apply (two_arg_paths_f eint).
  induction eint.
  apply idpath.
Defined.

Lemma iscontrhfiberl1 {X Y : UU} (f : X → Y) (g : Y → X)
      (efg: ∏ y : Y , f (g y) = y) (x0 : X)
      (is : iscontr (hfiber (g ∘ f) x0)) : iscontr (hfiber g x0).
Proof.
  intros.
  set (f1 := hfibersgftog f g x0).
  set (g1 := λ (xe : hfiber g x0), pr1 (constr2 f g efg x0 xe)).
  set (efg1 := λ (xe : hfiber g x0), ! (pr2 (constr2 f g efg x0 xe))).
  apply (iscontrretract f1 g1 efg1).
  apply is.
Defined.

Definition homothfiber1 {X Y : UU} (f g : X → Y)
           (h : f ¬ g) (y : Y) (xe : hfiber f y) : hfiber g y.
Proof.
  intros.
  set (x := pr1 xe).
  set (e := pr2 xe).
  apply (make_hfiber g x (!(h x) @ e)).
Defined.

Definition homothfiber2 {X Y : UU} (f g : X → Y)
           (h : f ¬ g) (y : Y) (xe : hfiber g y) : hfiber f y.
Proof.
  intros.
  set (x := pr1 xe).
  set (e := pr2 xe).
  apply (make_hfiber f x (h x @ e)).
Defined.

Definition homothfiberretr {X Y : UU} (f g : X → Y)
           (h : f ¬ g) (y : Y) (xe : hfiber g y) :
  homothfiber1 f g h y (homothfiber2 f g h y xe) = xe.
Proof.
  intros.
  induction xe as [x e].
  simpl.
  fold (make_hfiber g x e).
  set (xe1 := make_hfiber g x (! h x @ h x @ e)).
  set (xe2 := make_hfiber g x e).
  apply (hfibertriangle2 g xe1 xe2 (idpath _)).
  simpl.

  assert (ee : ∏ a b c : Y, ∏ p : a = b , ∏ q : b = c ,
                                               !p @ (p @ q ) = q).
  { intros. induction p. induction q. apply idpath. }

  apply ee.
Defined.

Lemma iscontrhfiberl2 {X Y : UU} (f g : X → Y)
      (h : f ¬ g) (y : Y) (is : iscontr (hfiber f y)) : iscontr (hfiber g y).
Proof.
  intros.
  set (a := homothfiber1 f g h y).
  set (b := homothfiber2 f g h y).
  set (eab := homothfiberretr f g h y).
  apply (iscontrretract a b eab is).
Defined.

Corollary isweqhomot {X Y : UU} (f1 f2 : X → Y)
          (h : f1 ¬ f2) : isweq f1 → isweq f2.
Proof.
  intros x0.
  unfold isweq.
  intro y.
  apply (iscontrhfiberl2 f1 f2 h).
  apply x0.
Defined.

Corollary remakeweq {X Y : UU} {f:X ≃Y} {g:X →Y} : f ¬ g → X ≃Y.
Proof.
  intros e.
  exact (g ,, isweqhomot f g e (weqproperty f)).
Defined.

Lemma remakeweq_eq {X Y : UU} (f1:X ≃Y) (f2:X →Y) (e:f1 ¬f2) : pr1weq (remakeweq e) = f2.
Proof.
  intros. apply idpath.
Defined.

Lemma remakeweq_eq' {X Y : UU} (f1:X ≃Y) (f2:X →Y) (e:f1 ¬f2) : invmap (remakeweq e) = invmap f1.
Proof.
  intros. apply idpath.
Defined.

Lemma iscontr_move_point {X} : X → iscontr X → iscontr X.
Proof.
  intros x i.
  ∃ x.
  intro y.
  apply proofirrelevancecontr.
  exact i.
Defined.

Lemma iscontr_move_point_eq {X} (x:X) (i:iscontr X) : iscontrpr1 (iscontr_move_point x i) = x.
Proof.
  intros. apply idpath.
Defined.

Corollary remakeweqinv {X Y : UU} {f:X ≃Y} {h:Y →X} : invmap f ¬ h → X ≃Y.
Proof.
  intros e. ∃ f. intro y.
  assert (p : hfiber f y).
  { ∃ (h y). apply pathsweq1', pathsinv0. apply e. }
  exact (iscontr_move_point p (weqproperty f y)).
Defined.

Lemma remakeweqinv_eq {X Y : UU} (f:X ≃Y) (h:Y →X) (e:invmap f ¬ h) : pr1weq (remakeweqinv e) = pr1weq f.
Proof.
  intros. apply idpath.
Defined.

Lemma remakeweqinv_eq' {X Y : UU} (f:X ≃Y) (h:Y →X) (e:invmap f ¬ h) : invmap (remakeweqinv e) = h.
Proof.
  intros. apply idpath.
Defined.

Corollary remakeweqboth {X Y : UU} {f:X ≃Y} {g:X →Y} {h:Y →X} : f ¬ g → invmap f ¬ h → X ≃Y.
Proof.
  intros r s.
  use (remakeweqinv (f := remakeweq r) s).
Defined.

Lemma remakeweqboth_eq {X Y : UU} (f:X ≃Y) (g:X →Y) (h:Y →X) (r:f ¬g) (s:invmap f ¬ h) :
  pr1weq (remakeweqboth r s) = g.
Proof.
  intros. apply idpath.
Defined.

Lemma remakeweqboth_eq' {X Y : UU} (f:X ≃Y) (g:X →Y) (h:Y →X) (r:f ¬g) (s:invmap f ¬ h) :
  invmap (remakeweqboth r s) = h.
Proof.
  intros. apply idpath.
Defined.

Corollary isweqhomot_iff {X Y : UU} (f1 f2 : X → Y)
          (h : f1 ¬ f2) : isweq f1 ↔ isweq f2.
Proof.
  intros. split.
  - apply isweqhomot; assumption.
  - apply isweqhomot, invhomot; assumption.
Defined.

Lemma isweq_to_isweq_unit {X:UU} (f g:X →unit) : isweq f → isweq g.
Proof.
  intros i.
  assert (h : f ¬ g).
  { intros t. apply isProofIrrelevantUnit. }
  exact (isweqhomot f g h i).
Defined.

Theorem isweq_iso {X Y : UU} (f : X → Y) (g : Y → X)
        (egf: ∏ x : X , g (f x) = x)
        (efg: ∏ y : Y , f (g y) = y) : isweq f.
Proof.
  intros.
  unfold isweq.
  intro y.
  assert (X0 : iscontr (hfiber (f ∘ g) y)).
  assert (efg' : ∏ y : Y, y = f (g y)).
  { intro y0.
    apply pathsinv0.
    apply (efg y0). }
  apply (iscontrhfiberl2 (idfun _) (f ∘ g) efg' y (idisweq Y y)).
  apply (iscontrhfiberl1 g f egf y).
  apply X0.
Defined.

This is kept to preserve compatibility with publications that use the name "gradth" for the "grad theorem".

Definition gradth {X Y : UU} (f : X → Y) (g : Y → X)
        (egf: ∏ x : X , g (f x) = x)
        (efg: ∏ y : Y , f (g y) = y) : isweq f := isweq_iso f g egf efg.

Definition weq_iso {X Y : UU} (f : X → Y) (g : Y → X)
           (egf: ∏ x : X , g (f x) = x)
           (efg: ∏ y : Y , f (g y) = y) : X ≃ Y :=
  make_weq _ (isweq_iso _ _ egf efg).

Definition UniqueConstruction {X Y:UU} (f:X →Y) :=
  (∏ y , ∑ x , f x = y ) × (∏ x x', f x = f x' → x = x').

Corollary UniqueConstruction_to_weq {X Y:UU} (f:X →Y) : UniqueConstruction f → isweq f.

Proof.
  intros bij. assert (sur := pr1 bij). assert (inj := pr2 bij).
  use (isweq_iso f).
  - intros y. exact (pr1 (sur y)).
  - intros. simpl. simpl in inj. apply inj. exact (pr2 (sur (f x))).
  - intros. simpl. exact (pr2 (sur y)).
Defined.

Some weak equivalences

Corollary isweqinvmap {X Y : UU} (w : X ≃ Y) : isweq (invmap w).
Proof.
  intros.
  assert (efg : ∏ (y : Y), w (invmap w y) = y).
  apply homotweqinvweq.
  assert (egf : ∏ (x : X), invmap w (w x) = x).
  apply homotinvweqweq.
  apply (isweq_iso _ _ efg egf).
Defined.

Definition invweq {X Y : UU} (w : X ≃ Y) : Y ≃ X :=
  make_weq (invmap w) (isweqinvmap w).

Lemma invinv {X Y : UU} (w : X ≃ Y) (x : X) :
  invmap (invweq w) x = w x.
Proof.
  intros. apply idpath.
Defined.

Lemma pr1_invweq {X Y : UU} (w : X ≃ Y) : pr1weq (invweq w) = invmap w.
Proof.
  intros. apply idpath.
Defined.

Corollary iscontrweqf {X Y : UU} (w : X ≃ Y) (is : iscontr X) : iscontr Y.
Proof.
  intros. apply (iscontrweqb (invweq w) is).
Defined.

Equality between pairs is equivalent to pairs of equalities between components. Theorem adapted from HoTT library http://github.com/HoTT/HoTT.

Definition PathPair {A : UU} {B : A → UU} (x y : ∑ x , B x) :=
  ∑ p : pr1 x = pr1 y , transportf _ p (pr2 x) = pr2 y.

Notation "a ╝ b" := (PathPair a b) : type_scope.

Theorem total2_paths_equiv {A : UU} (B : A → UU) (x y : ∑ x , B x) :
  x = y ≃ x ╝ y.
Proof.
  intros.
  ∃ (λ r : x = y,
            tpair (λ p : pr1 x = pr1 y, transportf _ p (pr2 x) = pr2 y)
                  (base_paths _ _ r) (fiber_paths r)).
  apply (isweq_iso _ (λ pq , total2_paths_f (pr1 pq) (pr2 pq))).
  - intro p.
    apply total2_fiber_paths.
  - intros [p q]. simpl.
    apply (two_arg_paths_f (base_total2_paths q)).
    apply transportf_fiber_total2_paths.
Defined.

The standard weak equivalence from unit to a contractible type

Definition wequnittocontr {X : UU} (is : iscontr X) : unit ≃ X.
Proof.
  intros.
  set (f := λ (_ : unit ), pr1 is).
  set (g := λ (_ : X), tt).
  split with f.
  assert (egf : ∏ t : unit , g (f t) = t).
  { intro. induction t. apply idpath. }
  assert (efg : ∏ x : X, f (g x) = x).
  { intro. apply (! (pr2 is x)). }
  apply (isweq_iso _ _ egf efg).
Defined.

A weak equivalence between types defines weak equivalences on the corresponding paths types.

Corollary isweqmaponpaths {X Y : UU} (w : X ≃ Y) (x x' : X) :
  isweq (@maponpaths _ _ w x x').
Proof.
  intros.
  apply (isweq_iso (@maponpaths _ _ w x x')
                (@invmaponpathsweq _ _ w x x')
                (@pathsweq3 _ _ w x x')
                (@pathsweq4 _ _ w x x')).
Defined.

Definition weqonpaths {X Y : UU} (w : X ≃ Y) (x x' : X) : x = x' ≃ w x = w x'
  := make_weq _ (isweqmaponpaths w x x').

The inverse path and the composition with a path functions are weak equivalences

Lemma isweqpathsinv0 {X : Type} (x y : X) : isweq (@pathsinv0 X x y).
Proof.
  intros. intros p. use tpair.
  - ∃ (!p). apply pathsinv0inv0.
  - cbn. intros [q k]. induction q,k. reflexivity.
Defined.

Definition weqpathsinv0 {X : UU} (x x' : X) : x = x' ≃ x' = x
  := make_weq _ (isweqpathsinv0 x x').

Corollary isweqpathscomp0r {X : UU} (x : X) {x' x'' : X} (e' : x' = x'') :
  isweq (λ e : x = x', e @ e').
Proof.
  intros.
  set (f := λ e : x = x', e @ e').
  set (g := λ e'' : x = x'', e'' @ (! e')).
  assert (egf : ∏ e : _, g (f e) = e).
  { intro e. induction e. induction e'. apply idpath. }
  assert (efg : ∏ e : _, f (g e) = e).
  { intro e. induction e. induction e'. apply idpath. }
  apply (isweq_iso f g egf efg).
Defined.

Weak equivalences to and from coconuses and total path spaces

Corollary isweqtococonusf {X Y : UU} (f : X → Y) : isweq (tococonusf f).
Proof.
  intros.
  apply (isweq_iso _ _ (homotfromtococonusf f) (homottofromcoconusf f)).
Defined.

Definition weqtococonusf {X Y : UU} (f : X → Y) : X ≃ coconusf f :=
  make_weq _ (isweqtococonusf f).

Corollary isweqfromcoconusf {X Y : UU} (f : X → Y) : isweq (fromcoconusf f).
Proof.
  intros.
  apply (isweq_iso _ _ (homottofromcoconusf f) (homotfromtococonusf f)).
Defined.

Definition weqfromcoconusf {X Y : UU} (f : X → Y) : coconusf f ≃ X :=
  make_weq _ (isweqfromcoconusf f).

Corollary isweqdeltap (T : UU) : isweq (deltap T).
Proof.
  intros.
  set (ff := deltap T). set (gg := λ (z : pathsspace T), pr1 z).
  assert (egf : ∏ t : T, gg (ff t) = t).
  { intro. apply idpath. }
  assert (efg : ∏ (tte : _), ff (gg tte) = tte).
  { intro tte. induction tte as [t c].
    induction c as [x e]. induction e.
    apply idpath.
  }
  apply (isweq_iso _ _ egf efg).
Defined.

Corollary isweqpr1pr1 (T : UU) :
  isweq (λ (a : pathsspace' T ), pr1 (pr1 a)).
Proof.
  intros.
  set (f := λ (a : pathsspace' T), pr1 (pr1 a)).
  set (g := λ (t : T),
              tpair _ (make_dirprod t t) (idpath t) : pathsspace' T).
  assert (efg : ∏ t : T, f (g t) = t).
  { intros t. unfold f. unfold g. simpl. apply idpath. }
  assert (egf : ∏ a : _, g (f a) = a).
  { intros a. induction a as [xy e].
    induction xy as [x y]. simpl in e.
    induction e. unfold f. unfold g.
    apply idpath.
  }
  apply (isweq_iso _ _ egf efg).
Defined.

The weak equivalence between hfibers of homotopic functions

Theorem weqhfibershomot {X Y : UU} (f g : X → Y)
        (h : f ¬ g) (y : Y) : hfiber f y ≃ hfiber g y.
Proof.
  intros.
  set (ff := hfibershomotftog f g h y).
  set (gg := hfibershomotgtof f g h y).

  split with ff.

  assert (effgg : ∏ xe : _, ff (gg xe) = xe).
  {
    intro xe.
    induction xe as [x e].
    simpl.
    assert (eee : ! h x @ h x @ e = maponpaths g (idpath x) @ e).
    { simpl. induction e. induction (h x). apply idpath. }
    set (xe1 := make_hfiber g x (! h x @ h x @ e)).
    set (xe2 := make_hfiber g x e).
    apply (hfibertriangle2 g xe1 xe2 (idpath x) eee).
  }

  assert (eggff : ∏ xe : _, gg (ff xe) = xe).
  {
    intro xe.
    induction xe as [x e].
    simpl.
    assert (eee : h x @ !h x @ e = maponpaths f (idpath x) @ e).
    { simpl. induction e. induction (h x). apply idpath. }
    set (xe1 := make_hfiber f x (h x @ ! h x @ e)).
    set (xe2 := make_hfiber f x e).
    apply (hfibertriangle2 f xe1 xe2 (idpath x) eee).
  }

  apply (isweq_iso _ _ eggff effgg).
Defined.

The 2-out-of-3 property of weak equivalences

Theorems showing that if any two of three functions f, g, gf are weak equivalences then so is the third - the 2-out-of-3 property.

Theorem twooutof3a {X Y Z : UU} (f : X → Y) (g : Y → Z)
        (isgf: isweq (g ∘ f)) (isg: isweq g) : isweq f.
Proof.
  intros.
  set (gw := make_weq g isg).
  set (gfw := make_weq (g ∘ f) isgf).
  set (invg := invmap gw).
  set (invgf := invmap gfw).

  set (invf := invgf ∘ g).

  assert (efinvf : ∏ y : Y, f (invf y) = y).
  {
    intro y.
    assert (int1 : g (f (invf y)) = g y).
    { unfold invf. apply (homotweqinvweq gfw (g y)). }
    apply (invmaponpathsweq gw _ _ int1).
  }

  assert (einvff: ∏ x : X, invf (f x) = x).
  { intro. unfold invf. apply (homotinvweqweq gfw x). }

  apply (isweq_iso f invf einvff efinvf).
Defined.

Theorem twooutof3b {X Y Z : UU} (f : X → Y) (g : Y → Z)
        (isf : isweq f) (isgf : isweq (g ∘ f)) : isweq g.
Proof.
  intros.
  set (wf := make_weq f isf).
  set (wgf := make_weq (g ∘ f) isgf).
  set (invf := invmap wf).
  set (invgf := invmap wgf).

  set (invg := f ∘ invgf).

  assert (eginvg : ∏ z : Z, g (invg z) = z).
  { intro. unfold invg. apply (homotweqinvweq wgf z). }

  assert (einvgg : ∏ y : Y, invg (g y) = y).
  { intro. unfold invg.

    assert (isinvf: isweq invf).
    { apply isweqinvmap. }
    assert (isinvgf: isweq invgf).
    { apply isweqinvmap. }

    assert (int1 : g y = (g ∘ f) (invf y )).
    apply (maponpaths g (! homotweqinvweq wf y)).

    assert (int2 : (g ∘ f) (invgf (g y )) = (g ∘ f) (invf y )).
    {
      assert (int3: (g ∘ f) (invgf (g y )) = g y).
      { apply (homotweqinvweq wgf). }
      induction int1.
      apply int3.
    }

    assert (int4: (invgf (g y)) = (invf y)).
    { apply (invmaponpathsweq wgf). apply int2. }

    assert (int5: (invf (f (invgf (g y)))) = (invgf (g y))).
    { apply (homotinvweqweq wf). }

    assert (int6: (invf (f (invgf (g (y))))) = (invf y)).
    { induction int4. apply int5. }

    apply (invmaponpathsweq (make_weq invf isinvf)).
    simpl.
    apply int6.
  }

  apply (isweq_iso g invg einvgg eginvg).
Defined.

Lemma isweql3 {X Y : UU} (f : X → Y) (g : Y → X)
      (egf : ∏ x : X , g (f x) = x) : isweq f → isweq g.
Proof.
  intros w.
  assert (int1 : isweq (g ∘ f)).
  {
    apply (isweqhomot (idfun X) (g ∘ f) (λ (x : X), ! (egf x ))).
    apply idisweq.
  }
  apply (twooutof3b f g w int1).
Defined.

Theorem twooutof3c {X Y Z : UU} (f : X → Y) (g : Y → Z)
        (isf : isweq f) (isg : isweq g) : isweq (g ∘ f).
Proof.
  intros.
  set (wf := make_weq f isf).
  set (wg := make_weq g isg).
  set (invf := invmap wf).
  set (invg := invmap wg).

  set (gf := g ∘ f).
  set (invgf := invf ∘ invg).

  assert (egfinvgf : ∏ x : X, invgf (gf x) = x).
  {
    intros x.
    assert (int1 : invf (invg (g (f x))) = invf (f x)).
    { apply (maponpaths invf (homotinvweqweq wg (f x))). }
    assert (int2 : invf (f x) = x).
    { apply (homotinvweqweq wf x). }
    induction int1.
    apply int2.
  }

  assert (einvgfgf : ∏ z : Z, gf (invgf z) = z).
  {
    intros z.
    assert (int1 : g (f (invgf z)) = g (invg z)).
    {
      unfold invgf.
      apply (maponpaths g (homotweqinvweq wf (invg z))).
    }
    assert (int2 : g (invg z) = z).
    { apply (homotweqinvweq wg z). }
    induction int1.
    apply int2.
  }

  apply (isweq_iso gf invgf egfinvgf einvgfgf).
Defined.

Corollary twooutof3c_iff_2 {X Y Z : UU} (f : X → Y) (g : Y → Z) :
  isweq f → (isweq g ↔ isweq (g ∘ f)).
Proof.
  intros i. split.
  - intro j. exact (twooutof3c f g i j).
  - intro j. exact (twooutof3b f g i j).
Defined.

Corollary twooutof3c_iff_1 {X Y Z : UU} (f : X → Y) (g : Y → Z) :
  isweq g → (isweq f ↔ isweq (g ∘ f)).
Proof.
  intros i. split.
  - intro j. exact (twooutof3c f g j i).
  - intro j. exact (twooutof3a f g j i).
Defined.

Corollary twooutof3c_iff_1_homot {X Y Z : UU}
          (f : X → Y) (g : Y → Z) (h : X → Z) :
  g ∘ f ¬ h → isweq g → (isweq f ↔ isweq h ).
Proof.
  intros r i.
  apply (logeq_trans (Y := isweq (g ∘ f))).
  - apply twooutof3c_iff_1; assumption.
  - apply isweqhomot_iff; assumption.
Defined.

Corollary twooutof3c_iff_2_homot {X Y Z : UU}
          (f : X → Y) (g : Y → Z) (h : X → Z) :
  g ∘ f ¬ h → isweq f → (isweq g ↔ isweq h ).
Proof.
  intros r i.
  apply (logeq_trans (Y := isweq (g ∘ f))).
  - apply twooutof3c_iff_2; assumption.
  - apply isweqhomot_iff; assumption.
Defined.

Any function between contractible types is a weak equivalence

Corollary isweqcontrcontr {X Y : UU} (f : X → Y)
          (isx : iscontr X) (isy: iscontr Y): isweq f.
Proof.
  intros.
  set (py := λ (y : Y), tt).
  apply (twooutof3a f py (isweqcontrtounit isx) (isweqcontrtounit isy)).
Defined.

Definition weqcontrcontr {X Y : UU} (isx : iscontr X) (isy : iscontr Y) : X ≃ Y
  := make_weq (λ _, pr1 isy) (isweqcontrcontr _ isx isy).

Composition of weak equivalences

Definition weqcomp {X Y Z : UU} (w1 : X ≃ Y) (w2 : Y ≃ Z) : X ≃ Z :=
  make_weq (λ (x : X ), w2 (w1 x)) (twooutof3c w1 w2 (pr2 w1) (pr2 w2)).

Declare Scope weq_scope.
Notation "g ∘ f" := (weqcomp f g) : weq_scope.

Delimit Scope weq_scope with weq.

Ltac intermediate_weq Y' := apply (weqcomp (Y := Y')).

Definition weqcomp_to_funcomp_app {X Y Z : UU} {x : X} {f : X ≃ Y} {g : Y ≃ Z} :
  (weqcomp f g) x = pr1weq g (pr1weq f x).
Proof.
  intros. apply idpath.
Defined.

Definition weqcomp_to_funcomp {X Y Z : UU} {f : X ≃ Y} {g : Y ≃ Z} :
  pr1weq (weqcomp f g) = pr1weq g ∘ pr1weq f.
Proof.
  intros. apply idpath.
Defined.

Definition invmap_weqcomp_expand {X Y Z : UU} {f : X ≃ Y} {g : Y ≃ Z} :
  invmap (weqcomp f g) = invmap f ∘ invmap g.
Proof.
  intros. apply idpath.
Defined.

The 2-out-of-6 (two-out-of-six) property of weak equivalences

Theorem twooutofsixu {X Y Z K : UU} {u : X → Y} {v : Y → Z} {w : Z → K}
        (isuv : isweq (funcomp u v)) (isvw : isweq (funcomp v w)) : isweq u.
Proof.
  intros.

  set (invuv := invmap (make_weq _ isuv)).
  set (pu := funcomp v invuv).
  set (hupu := homotinvweqweq (make_weq _ isuv)
               : homot (funcomp u pu) (idfun X)).

  set (invvw := invmap (make_weq _ isvw)).
  set (pv := funcomp w invvw).
  set (hvpv := homotinvweqweq (make_weq _ isvw)
               : homot (funcomp v pv) (idfun Y)).

  set (h0 := funhomot v (homotweqinvweq (make_weq _ isuv))).
  set (h1 := funhomot (funcomp pu u) (invhomot hvpv)).
  set (h2 := homotfun h0 pv).

  set (hpuu := homotcomp (homotcomp h1 h2) hvpv).

  exact (isweq_iso u pu hupu hpuu).
Defined.

Theorem twooutofsixv {X Y Z K : UU} {u : X → Y} {v : Y → Z} {w : Z → K}
        (isuv : isweq (funcomp u v))(isvw : isweq (funcomp v w)) : isweq v.
Proof.
  intros. exact (twooutof3b _ _ (twooutofsixu isuv isvw) isuv).
Defined.

Theorem twooutofsixw {X Y Z K : UU} {u : X → Y} {v : Y → Z} {w : Z → K}
        (isuv : isweq (funcomp u v))(isvw : isweq (funcomp v w)) : isweq w.
Proof.
  intros. exact (twooutof3b _ _ (twooutofsixv isuv isvw) isvw).
Defined.

Pairwise direct products of weak equivalences

Theorem isweqdirprodf {X Y X' Y' : UU} (w : X ≃ Y) (w' : X' ≃ Y') :
  isweq (dirprodf w w').
Proof.
  intros.
  set (f := dirprodf w w'). set (g := dirprodf (invweq w) (invweq w')).
  assert (egf : ∏ a : _, (g (f a)) = a).
  intro a. induction a as [ x x' ]. simpl. apply pathsdirprod.
  apply (homotinvweqweq w x). apply (homotinvweqweq w' x').
  assert (efg : ∏ a : _, (f (g a)) = a).
  intro a. induction a as [ x x' ]. simpl. apply pathsdirprod.
  apply (homotweqinvweq w x). apply (homotweqinvweq w' x').
  apply (isweq_iso _ _ egf efg).
Defined.

Definition weqdirprodf {X Y X' Y' : UU} (w : X ≃ Y) (w' : X' ≃ Y') : X × X' ≃ Y × Y'
  := make_weq _ (isweqdirprodf w w').

Weak equivalence of a type and its direct product with the unit

Definition weqtodirprodwithunit (X : UU): X ≃ X × unit.
Proof.
  intros.
  set (f := λ x : X, make_dirprod x tt).
  split with f.
  set (g := λ xu : X × unit , pr1 xu).
  assert (egf : ∏ x : X, (g (f x)) = x). intro. apply idpath.
  assert (efg : ∏ xu : _, (f (g xu)) = xu). intro. induction xu as [ t x ].
  induction x. apply idpath.
  apply (isweq_iso f g egf efg).
Defined.

Associativity of total2 as a weak equivalence

Lemma total2asstor {X : UU} (P : X → UU) (Q : total2 P → UU) :
  total2 Q → ∑ x:X , ∑ p : P x , Q (tpair P x p).
Proof.
  intros xpq.
  ∃ (pr1 (pr1 xpq)).
  ∃ (pr2 (pr1 xpq)).
  exact (pr2 xpq).
Defined.

Lemma total2asstol {X : UU} (P : X → UU) (Q : total2 P → UU) :
  (∑ x : X , ∑ p : P x , Q (tpair P x p)) → total2 Q.
Proof.
  intros xpq.
  use tpair.
  - use tpair.
    + apply (pr1 xpq).
    + apply (pr1 (pr2 xpq)).
  - exact (pr2 (pr2 xpq)).
Defined.

Theorem weqtotal2asstor {X : UU} (P : X → UU) (Q : total2 P → UU) :
  total2 Q ≃ ∑ x : X , ∑ p : P x , Q (tpair P x p).
Proof.
  intros.
  set (f := total2asstor P Q). set (g:= total2asstol P Q).
  split with f.
  assert (egf : ∏ xpq : _ , (g (f xpq)) = xpq).
  intro. apply idpath.
  assert (efg : ∏ xpq : _ , (f (g xpq)) = xpq).
  intro. apply idpath.
  apply (isweq_iso _ _ egf efg).
Defined.

Definition weqtotal2asstol {X : UU} (P : X → UU) (Q : total2 P → UU) :
  (∑ x : X , ∑ p : P x , Q (tpair P x p)) ≃ total2 Q
  := invweq (weqtotal2asstor P Q).

Associativity and commutativity of direct products as weak equivalences

Definition weqdirprodasstor (X Y Z : UU) : (X × Y ) × Z ≃ X × (Y × Z ).
Proof.
  intros. apply weqtotal2asstor.
Defined.

Definition weqdirprodasstol (X Y Z : UU) : X × (Y × Z ) ≃ (X × Y ) × Z
  := invweq (weqdirprodasstor X Y Z).

Definition weqdirprodcomm (X Y : UU) : X × Y ≃ Y × X.
Proof.
  intros.
  set (f := λ xy : X × Y, make_dirprod (pr2 xy) (pr1 xy)).
  set (g := λ yx : Y × X, make_dirprod (pr2 yx) (pr1 yx)).
  assert (egf : ∏ xy : _, (g (f xy)) = xy).
  intro. induction xy. apply idpath.
  assert (efg : ∏ yx : _, (f (g yx)) = yx).
  intro. induction yx. apply idpath.
  split with f. apply (isweq_iso _ _ egf efg).
Defined.

Definition weqtotal2dirprodcomm {X Y : UU} (P : X × Y → UU) :
  (∑ xy : X × Y , P xy ) ≃ (∑ xy : Y × X , P (weqdirprodcomm _ _ xy)).
Proof.
  intros.
  use weq_iso.
  - intros xyp.
    exact ((pr2 (pr1 xyp),, pr1 (pr1 xyp)),,pr2 xyp).
  - intros yxp.
    exact (((pr2 (pr1 yxp)),, (pr1 (pr1 yxp))),, pr2 yxp).
  - intros xyp.
    apply idpath.
  - intros yxp.
    apply idpath.
Defined.

Definition weqtotal2dirprodassoc {X Y : UU} (P : X × Y → UU) :
  (∑ xy : X × Y , P xy ) ≃ (∑ (x : X) (y : Y ), P (x ,,y)).
  intros.
  use weq_iso.
  - intros xyp.
    exact (pr1 (pr1 xyp),,pr2 (pr1 xyp),, pr2 xyp).
  - intros xyp.
    exact (((pr1 xyp),, pr1 (pr2 xyp)),, pr2 (pr2 xyp)).
  - intros xyp.
    apply idpath.
  - intros xyp.
    apply idpath.
Defined.

Definition weqtotal2dirprodassoc' {X Y : UU} (P : X × Y → UU) :
  (∑ xy : X × Y , P xy ) ≃ (∑ (y : Y) (x : X ), P (x ,,y)).
Proof.
  intros.
  use weq_iso.
  - intros xyp.
    exact (pr2 (pr1 xyp),,pr1 (pr1 xyp),,pr2 xyp).
  - intros yxp.
    exact ((pr1 (pr2 yxp),,pr1 yxp),,pr2 (pr2 yxp)).
  - intros xyp.
    apply idpath.
  - intros yxp.
    apply idpath.
Defined.

Definition weqtotal2comm12 {X} (P Q : X → UU) :
  (∑ (w : ∑ x , P x ), Q (pr1 w)) ≃ (∑ (w : ∑ x , Q x ), P (pr1 w)).
Proof.
  intros.
  use weq_iso.
  - intro xpq. exact ((pr1 (pr1 xpq),,pr2 xpq),, pr2 (pr1 xpq)).
  - intro xqp. exact ((pr1 (pr1 xqp),, pr2 xqp),, pr2 (pr1 xqp)).
  - intro. apply idpath.
  - intro. apply idpath.
Defined.

Binary coproducts and their basic properties

Binary coproducts have not been introduced or used earlier except for the lines in the Preamble.v that define coprod and ⨿ as a notation for the inductive type family sum that is defined in Coq.Init.

Distributivity of coproducts and direct products as a weak equivalence

Definition rdistrtocoprod (X Y Z : UU) :
  X × (Y ⨿ Z ) → (X × Y ) ⨿ (X × Z ).
Proof.
  intros X0.
  induction X0 as [ t x ]. induction x as [ y | z ].
  apply (ii1 (make_dirprod t y)).
  apply (ii2 (make_dirprod t z)).
Defined.

Definition rdistrtoprod (X Y Z : UU) : (X × Y ) ⨿ (X × Z ) → X × (Y ⨿ Z ).
Proof.
  intros X0.
  induction X0 as [ d | d ]. induction d as [ t x ].
  apply (make_dirprod t (ii1 x)).
  induction d as [ t x ]. apply (make_dirprod t (ii2 x)).
Defined.

Theorem isweqrdistrtoprod (X Y Z : UU) : isweq (rdistrtoprod X Y Z).
Proof.
  intros.
  set (f := rdistrtoprod X Y Z). set (g := rdistrtocoprod X Y Z).

  assert (egf: ∏ a , (g (f a)) = a).
  intro. induction a as [ d | d ]. induction d. apply idpath. induction d.
  apply idpath.

  assert (efg: ∏ a , (f (g a)) = a). intro. induction a as [ t x ].
  induction x. apply idpath. apply idpath.

  apply (isweq_iso f g egf efg).
Defined.

Definition weqrdistrtoprod (X Y Z : UU) := make_weq _ (isweqrdistrtoprod X Y Z).

Corollary isweqrdistrtocoprod (X Y Z : UU) : isweq (rdistrtocoprod X Y Z).
Proof.
  intros. apply (isweqinvmap (weqrdistrtoprod X Y Z)).
Defined.

Definition weqrdistrtocoprod (X Y Z : UU)
  := make_weq _ (isweqrdistrtocoprod X Y Z).

Total space of a family over a coproduct

Definition fromtotal2overcoprod {X Y : UU} (P : X ⨿ Y → UU) (xyp : total2 P) :
  coprod (∑ x : X , P (ii1 x)) (∑ y : Y , P (ii2 y)).
Proof.
  intros.
  set (PX := λ x : X, P (ii1 x)). set (PY := λ y : Y, P (ii2 y)).
  induction xyp as [ xy p ]. induction xy as [ x | y ].
  apply (ii1 (tpair PX x p)). apply (ii2 (tpair PY y p)).
Defined.

Definition tototal2overcoprod {X Y : UU} (P : X ⨿ Y → UU)
           (xpyp : coprod (∑ x : X , P (ii1 x)) (∑ y : Y , P (ii2 y))) : total2 P.
Proof.
  intros.
  induction xpyp as [ xp | yp ]. induction xp as [ x p ].
  apply (tpair P (ii1 x) p).
  induction yp as [ y p ]. apply (tpair P (ii2 y) p).
Defined.

Theorem weqtotal2overcoprod {X Y : UU} (P : X ⨿ Y → UU) :
  (∑ xy , P xy ) ≃ (∑ x : X , P (ii1 x)) ⨿ (∑ y : Y , P (ii2 y)).
Proof.
  intros.
  set (f := fromtotal2overcoprod P). set (g := tototal2overcoprod P).
  split with f.
  assert (egf : ∏ a : _ , (g (f a)) = a).
  { intro a.
    induction a as [ xy p ].
    induction xy as [ x | y ].
    simpl.
    apply idpath.
    simpl.
    apply idpath. }
  assert (efg : ∏ a : _ , (f (g a)) = a).
  { intro a.
    induction a as [ xp | yp ].
    induction xp as [ x p ].
    simpl.
    apply idpath.
    induction yp as [ y p ].
    apply idpath. }
  apply (isweq_iso _ _ egf efg).
Defined.

Pairwise sum of functions, coproduct associativity and commutativity

Definition sumofmaps {X Y Z : UU} (fx : X → Z)(fy : Y → Z) :
  (X ⨿ Y ) → Z := λ xy : _, match xy with ii1 x ⇒ fx x | ii2 y ⇒ fy y end.

Definition coprodasstor (X Y Z : UU) : (X ⨿ Y ) ⨿ Z → X ⨿ (Y ⨿ Z ).
Proof.
  intros X0.
  induction X0 as [ c | z ]. induction c as [ x | y ].
  apply (ii1 x). apply (ii2 (ii1 y)). apply (ii2 (ii2 z)).
Defined.

Definition coprodasstol (X Y Z : UU): X ⨿ (Y ⨿ Z ) → (X ⨿ Y ) ⨿ Z.
Proof.
  intros X0.
  induction X0 as [ x | c ]. apply (ii1 (ii1 x)). induction c as [ y | z ].
  apply (ii1 (ii2 y)). apply (ii2 z).
Defined.

Definition sumofmaps_assoc_left {X Y Z T : UU} (f : X → T) (g : Y → T)
           (h : Z → T) :
  sumofmaps (sumofmaps f g) h ∘ coprodasstol _ _ _ ¬ sumofmaps f (sumofmaps g h).
Proof.
  intros. intros [x|[y|z]]; apply idpath.
Defined.

Definition sumofmaps_assoc_right {X Y Z T : UU} (f : X → T) (g : Y → T)
           (h : Z → T) :
  sumofmaps f (sumofmaps g h) ∘ coprodasstor _ _ _ ¬ sumofmaps (sumofmaps f g) h.
Proof.
  intros. intros [[x|y]|z]; apply idpath.
Defined.

Theorem isweqcoprodasstor (X Y Z : UU): isweq (coprodasstor X Y Z).
Proof.
  intros. set (f := coprodasstor X Y Z). set (g := coprodasstol X Y Z).
  assert (egf : ∏ xyz , (g (f xyz)) = xyz).
  intro xyz. induction xyz as [ c | z ]. induction c.
  apply idpath. apply idpath. apply idpath.
  assert (efg : ∏ xyz , (f (g xyz)) = xyz). intro xyz.
  induction xyz as [ x | c ]. apply idpath. induction c.
  apply idpath. apply idpath.
  apply (isweq_iso f g egf efg).
Defined.

Definition weqcoprodasstor (X Y Z : UU) := make_weq _ (isweqcoprodasstor X Y Z).

Corollary isweqcoprodasstol (X Y Z : UU) : isweq (coprodasstol X Y Z).
Proof.
  intros. apply (isweqinvmap (weqcoprodasstor X Y Z)).
Defined.

Definition weqcoprodasstol (X Y Z : UU) := make_weq _ (isweqcoprodasstol X Y Z).

Definition coprodcomm (X Y : UU) : X ⨿ Y → Y ⨿ X
  := λ xy : _, match xy with ii1 x ⇒ ii2 x | ii2 y ⇒ ii1 y end.

Theorem isweqcoprodcomm (X Y : UU) : isweq (coprodcomm X Y).
Proof.
  intros.
  set (f := coprodcomm X Y). set (g := coprodcomm Y X).
  assert (egf : ∏ xy : _, (g (f xy)) = xy). intro.
  induction xy. apply idpath. apply idpath.
  assert (efg : ∏ yx : _, (f (g yx)) = yx). intro.
  induction yx. apply idpath. apply idpath.
  apply (isweq_iso f g egf efg).
Defined.

Definition weqcoprodcomm (X Y : UU) := make_weq _ (isweqcoprodcomm X Y).

Coproduct with a "negative" type

Theorem isweqii1withneg (X : UU) {Y : UU} (nf : Y → empty) : isweq (@ii1 X Y).
Proof.
  intros.
  set (f := @ii1 X Y).
  set (g := λ xy : X ⨿ Y, match xy with
                          | ii1 x ⇒ x
                          | ii2 y ⇒ fromempty (nf y)
                          end).
  assert (egf : ∏ x : X, (g (f x)) = x). intro. apply idpath.
  assert (efg : ∏ xy : X ⨿ Y, (f (g xy)) = xy). intro.
  induction xy as [ x | y ]. apply idpath. apply (fromempty (nf y)).
  apply (isweq_iso f g egf efg).
Defined.

Definition weqii1withneg (X : UU) {Y : UU} (nf : ¬ Y)
  := make_weq _ (isweqii1withneg X nf).

Theorem isweqii2withneg {X : UU} (Y : UU) (nf : X → empty) : isweq (@ii2 X Y).
Proof.
  intros.
  set (f:= @ii2 X Y).
  set (g:= λ xy : X ⨿ Y, match xy with
                         | ii1 x ⇒ fromempty (nf x)
                         | ii2 y ⇒ y
                         end).
  assert (egf : ∏ y : Y, (g (f y)) = y). intro. apply idpath.
  assert (efg : ∏ xy : X ⨿ Y, (f (g xy)) = xy). intro.
  induction xy as [ x | y ]. apply (fromempty (nf x)). apply idpath.
  apply (isweq_iso f g egf efg).
Defined.

Definition weqii2withneg {X : UU} (Y : UU) (nf : ¬ X)
  := make_weq _ (isweqii2withneg Y nf).

Coproduct of two functions

Definition coprodf {X Y X' Y' : UU} (f : X → X') (g : Y → Y') : X ⨿ Y → X' ⨿ Y'
  := λ xy: X ⨿ Y ,
           match xy with
           | ii1 x ⇒ ii1 (f x)
           | ii2 y ⇒ ii2 (g y)
           end.

Definition coprodf1 {X Y X' : UU} : (X → X') → X ⨿ Y → X' ⨿ Y.
Proof.
  intros f. exact (coprodf f (idfun Y)).
Defined.

Definition coprodf2 {X Y Y' : UU} : (Y → Y') → X ⨿ Y → X ⨿ Y'.
Proof.
  intros g. exact (coprodf (idfun X) g).
Defined.

Definition homotcoprodfcomp {X X' Y Y' Z Z' : UU} (f : X → Y)
           (f' : X' → Y') (g : Y → Z) (g' : Y' → Z') :
  homot (funcomp (coprodf f f') (coprodf g g'))
        (coprodf (funcomp f g) (funcomp f' g')).
Proof.
  intros. intro xx'. induction xx' as [ x | x' ].
  apply idpath. apply idpath.
Defined.

Definition homotcoprodfhomot {X X' Y Y' : UU} (f g : X → Y)
           (f' g' : X' → Y') (h : homot f g) (h' : homot f' g') :
  homot (coprodf f f') (coprodf g g')
  := λ xx' : _, match xx' with
                    | ii1 x ⇒ maponpaths (@ii1 _ _) (h x)
                    | ii2 x' ⇒ maponpaths (@ii2 _ _) (h' x')
                    end.

Theorem isweqcoprodf {X Y X' Y' : UU} (w : X ≃ X') (w' : Y ≃ Y') :
  isweq (coprodf w w').
Proof.
  intros.
  set (finv := invmap w). set (ginv := invmap w').
  set (ff := coprodf w w'). set (gg := coprodf finv ginv).
  assert (egf : ∏ xy : X ⨿ Y, (gg (ff xy)) = xy).
  intro. induction xy as [ x | y ]. simpl.
  apply (maponpaths (@ii1 X Y) (homotinvweqweq w x)).
  apply (maponpaths (@ii2 X Y) (homotinvweqweq w' y)).
  assert (efg : ∏ xy' : coprod X' Y', (ff (gg xy')) = xy').
  intro. induction xy' as [ x | y ]. simpl.
  apply (maponpaths (@ii1 X' Y') (homotweqinvweq w x)).
  apply (maponpaths (@ii2 X' Y') (homotweqinvweq w' y)).
  apply (isweq_iso ff gg egf efg).
Defined.

Definition weqcoprodf {X Y X' Y' : UU} : X ≃ X' → Y ≃ Y' → X ⨿ Y ≃ X' ⨿ Y'.
Proof.
  intros w1 w2. exact (make_weq _ (isweqcoprodf w1 w2)).
Defined.

Definition weqcoprodf1 {X Y X' : UU} : X ≃ X' → X ⨿ Y ≃ X' ⨿ Y.
Proof.
  intros w. exact (weqcoprodf w (idweq Y)).
Defined.

Definition weqcoprodf2 {X Y Y' : UU} : Y ≃ Y' → X ⨿ Y ≃ X ⨿ Y'.
Proof.
  intros w. exact (weqcoprodf (idweq X) w).
Defined.

The equality_cases construction and four applications to ii1 and ii2

Definition equality_cases {P Q : UU} (x x' : P ⨿ Q) : UU.
Proof.
  intros. induction x as [p|q].
  - induction x' as [p'|q'].
    + exact (p = p').
    + exact empty.
  - induction x' as [p'|q'].
    + exact empty.
    + exact (q = q').
Defined.

Definition equality_by_case {P Q : UU} {x x' : P ⨿ Q} :
  x = x'→ equality_cases x x'.
Proof.
  intros e. induction x as [p|q].
  - induction x' as [p'|q'].
    + simpl.
      exact (maponpaths (@coprod_rect P Q (λ _, P) (λ p , p) (λ _, p)) e).
    + simpl.
      exact (transportf (@coprod_rect P Q (λ _, UU) (λ _, unit) (λ _, empty))
                        e tt).
  - induction x' as [p'|q'].
    + simpl.
      exact (transportb (@coprod_rect P Q (λ _, UU) (λ _, unit) (λ _, empty))
                        e tt).
    + simpl.
      exact (maponpaths (@coprod_rect P Q (λ _,Q) (λ _, q) (λ q , q)) e).
Defined.

Definition inv_equality_by_case {P Q : UU} {x x' : P ⨿ Q} :
  equality_cases x x' → x = x'.
Proof.
  intros e.
  induction x as [p|q].
  - induction x' as [p'|q'].
    + exact (maponpaths (@ii1 P Q) e).
    + induction e.
  - induction x' as [p'|q'].
    + induction e.
    + exact (maponpaths (@ii2 P Q) e).
Defined.

Lemma ii1_injectivity {P Q : UU} (p p' : P) :
  ii1 (B := Q) p = ii1 (B := Q) p' → p = p'.
Proof.
  exact equality_by_case.
Defined.

Lemma ii2_injectivity {P Q : UU} (q q' : Q) :
  ii2 (A := P) q = ii2 (A := P) q' → q = q'.
Proof.
  exact equality_by_case.
Defined.

Lemma negpathsii1ii2 {X Y : UU} (x : X) (y : Y) : ii1 x != ii2 y.
Proof.
  exact equality_by_case.
Defined.

Lemma negpathsii2ii1 {X Y : UU} (x : X) (y : Y) : ii2 y != ii1 x.
Proof.
  exact equality_by_case.
Defined.

Bool as coproduct

Definition boolascoprod: unit ⨿ unit ≃ bool.
Proof.
  set (f := λ xx : coprod unit unit ,
                   match xx with ii1 t ⇒ true | ii2 t ⇒ false end).
  split with f.
  set (g := λ t:bool , match t with true ⇒ ii1 tt | false ⇒ ii2 tt end).

  assert (egf : ∏ xx : _, g (f xx) = xx).
  intro xx. induction xx as [ u | u ]. induction u. apply idpath.
  induction u. apply idpath.

  assert (efg : ∏ t : _, f (g t) = t). induction t. apply idpath.
  apply idpath.

  apply (isweq_iso f g egf efg).
Defined.

Pairwise coproducts as dependent sums of families over bool

Definition coprodtobool {X Y : UU} (xy : X ⨿ Y) : bool
  := match xy with
     | ii1 x ⇒ true
     | ii2 y ⇒ false
     end.

Definition boolsumfun (X Y : UU) : bool → UU
  := λ t : _, match t with
                  | true ⇒ X
                  | false ⇒ Y
                  end.

Definition coprodtoboolsum (X Y : UU) : X ⨿ Y → total2 (boolsumfun X Y)
  := λ xy : _, match xy with
                   | ii1 x ⇒ tpair (boolsumfun X Y) true x
                   | ii2 y ⇒ tpair (boolsumfun X Y) false y
                   end.

Definition boolsumtocoprod (X Y : UU): (total2 (boolsumfun X Y)) → X ⨿ Y
  := λ xy , match xy with
           | tpair _ true x ⇒ ii1 x
           | tpair _ false y ⇒ ii2 y
           end.

Theorem isweqcoprodtoboolsum (X Y : UU) : isweq (coprodtoboolsum X Y).
Proof.
  intros.
  set (f := coprodtoboolsum X Y). set (g := boolsumtocoprod X Y).
  assert (egf : ∏ xy : X ⨿ Y , (g (f xy)) = xy).
  induction xy. apply idpath. apply idpath.
  assert (efg : ∏ xy : total2 (boolsumfun X Y), (f (g xy)) = xy).
  intro. induction xy as [ t x ]. induction t. apply idpath. apply idpath.
  apply (isweq_iso f g egf efg).
Defined.

Definition weqcoprodtoboolsum (X Y : UU) := make_weq _ (isweqcoprodtoboolsum X Y).

Corollary isweqboolsumtocoprod (X Y : UU): isweq (boolsumtocoprod X Y).
Proof.
  intros. apply (isweqinvmap (weqcoprodtoboolsum X Y)).
Defined.

Definition weqboolsumtocoprod (X Y : UU) := make_weq _ (isweqboolsumtocoprod X Y).

Splitting of X into a coproduct defined by a function X → Y ⨿ Z

Definition weqcoprodsplit {X Y Z : UU} (f : X → coprod Y Z) :
  X ≃ (∑ y : Y , hfiber f (ii1 y)) ⨿ (∑ z : Z , hfiber f (ii2 z)).
Proof.
  intros.
  set (w1 := weqtococonusf f).
  set (w2 := weqtotal2overcoprod (λ yz : coprod Y Z, hfiber f yz)).
  apply (weqcomp w1 w2).
Defined.

Some properties of bool

Definition boolchoice (x : bool) : (x = true ) ⨿ (x = false ).
Proof.
  induction x. apply (ii1 (idpath _)). apply (ii2 (idpath _)).
Defined.

Definition bool_to_type : bool → UU.
Proof.
  intros b. induction b as [|]. { exact unit. } { exact empty. }
Defined.

Theorem nopathstruetofalse : true = false → empty.
Proof.
  intro X. apply (transportf bool_to_type X tt).
Defined.

Corollary nopathsfalsetotrue : false = true → empty.
Proof.
  intro X. apply (transportb bool_to_type X tt).
Defined.

Definition truetonegfalse (x : bool) : x = true → x != false.
Proof.
  intros e. rewrite e. unfold neg. apply nopathstruetofalse.
Defined.

Definition falsetonegtrue (x : bool) : x = false → x != true.
Proof.
  intros e. rewrite e. unfold neg. apply nopathsfalsetotrue.
Defined.

Definition negtruetofalse (x : bool) : x != true → x = false.
Proof.
  intros ne. induction (boolchoice x) as [t | f]. induction (ne t). apply f.
Defined.

Definition negfalsetotrue (x : bool) : x != false → x = true.
Proof.
  intros ne. induction (boolchoice x) as [t | f]. apply t. induction (ne f).
Defined.

Fibrations with only one non-empty fiber

Theorem saying that if a fibration has only one non-empty fiber then the total space is weakly equivalent to this fiber.

Theorem onefiber {X : UU} (P : X → UU) (x : X)
        (c : ∏ x' : X , (x = x') ⨿ ¬ P x') : isweq (λ p , tpair P x p).
Proof.
  intros.
  set (f := λ p : P x, tpair _ x p).
  set (cx := c x).
  transparent assert (cnew : (∏ x' : X, (x = x') ⨿ ¬ P x')).
  { intro x'. refine (coprod_rect (λ _, _) _ _ (cx)).
    - intro x0. refine (coprod_rect (λ _, _) _ _ (c x')).
      + intro ee. apply ii1; exact (pathscomp0 (pathsinv0 x0) ee).
      + intro phi. apply ii2, phi.
    - intro phi. exact (c x'). }

  set (g := λ pp : total2 P,
              match (cnew (pr1 pp)) with
              | ii1 e ⇒ transportb P e (pr2 pp)
              | ii2 phi ⇒ fromempty (phi (pr2 pp))
              end).

  assert (efg : ∏ pp : total2 P, (f (g pp)) = pp).
  intro. induction pp as [ t x0 ]. set (cnewt := cnew t).
  unfold g. unfold f. simpl. change (cnew t) with cnewt.
  induction cnewt as [ x1 | y ].
  apply (pathsinv0 (pr1 (pr2 (constr1 P (pathsinv0 x1))) x0)).
  induction (y x0).

  set (cnewx := cnew x).
  assert (e1 : (cnew x) = cnewx). apply idpath.
  unfold cnew in cnewx. change (c x) with cx in cnewx.
  induction cx as [ x0 | e0 ].
  assert (e : (cnewx) = (ii1 (idpath x))).
  apply (maponpaths (@ii1 (x = x) (P x → empty)) (pathsinv0l x0)).

  assert (egf : ∏ p: P x, (g (f p)) = p). intro. simpl in g.
  unfold g. unfold f. simpl.

  set (ff := λ cc:(x = x) ⨿ (P x → empty ),
               match cc with
               | ii1 e0 ⇒ transportb P e0 p
               | ii2 phi ⇒ fromempty (phi p)
               end).
  assert (ee : (ff (cnewx)) = (ff (@ii1 (x = x) (P x → empty) (idpath x)))).
  apply (maponpaths ff e).
  assert (eee : (ff (@ii1 (x = x) (P x → empty) (idpath x))) = p). apply idpath.
  fold (ff (cnew x)).
  assert (e2 : (ff (cnew x)) = (ff cnewx)). apply (maponpaths ff e1).
  apply (pathscomp0 (pathscomp0 e2 ee) eee).
  apply (isweq_iso f g egf efg).

  unfold isweq. intro y0. induction (e0 (g y0)).
Defined.

Basics about fibration sequences.

Fibrations sequences and their first "left shifts"

The group of constructions related to fibration sequences forms one of the most important computational toolboxes of homotopy theory.

Given a pair of functions (f : X → Y) (g : Y → Z) and a point z : Z , a structure of the complex on such a triple is a homotopy from the composition funcomp f g to the constant function X → Z corresponding to z i.e. a term ez : ∏ x : X, (g (f x)) = z . Specifing such a structure is essentially equivalent to specifing a structure of the form ezmap : X → hfiber g z . The mapping in one direction is given in the definition of ezmap below. The mapping in another is given by f := λ x : X, pr1 (ezmap x) and ez := λ x : X, pr2 (ezmap x) .

A complex is called a fibration sequence if ezmap is a weak equivalence. Correspondingly, the structure of a fibration sequence on f g z is a pair (ez , is) where is : isweq (ezmap f g z ez) . For a fibration sequence f g z fs where fs : fibseqstr f g z and any y : Y there is defined a function diff1 : (g y) = z → X and a structure of the fibration sequence fibseqdiff1 on the triple diff1 g y . This new fibration sequence is called the derived fibration sequence of the original one.

The first function of the second derived of f g z fs corresponding to (y : Y) (x : X) is of the form (f x) = y → (g y) = z and it is homotopic to the function defined by e ⇒ pathscomp0 (maponpaths g (pathsinv0 e)) (ez x) . The first function of the third derived of f g z fs corresponding to (y : Y) (x : X) (e : (g y) = z) is of the form (diff1 e) = x → (f x) = y . Therefore, the third derived of a sequence based on X Y Z is based entirely on types = of X , Y and Z . When this construction is applied to types of finite h-level (see below) and combined with the fact that the h-level of a path type is strictly lower than the h-level of the ambient type it leads to the possibility of building proofs about types by induction on h-level.

There are three important special cases in which fibration sequences arise:

( pr1 - case ) The fibration sequence fibseqpr1 P z defined by family P : Z → UU and a term z : Z . It is based on the sequence of functions (tpair P z : P z → total2 P) (pr1 : total2 P → Z) . The corresponding ezmap is defined by an obvious rule and the fact that it is a weak equivalence is proved in isweqfibertohfiber .

( g - case ) The fibration sequence fibseqg g z defined by a function g : Y → Z and a term z : Z . It is based on the sequence of functions (hfiberpr1 : hfiber g z → Y) (g : Y → Z) and the corresponding ezmap is the function which takes a term ye : hfiber to make_hfiber g (pr1 ye) (pr2 ye) . We now have eta-coercion for dependent sums, so it is the identity function, which is sufficient to ensure that it is a weak equivalence. The first derived of fibseqg g z corresponding to y : Y coincides with fibseqpr1 (λ y' : Y , (g y') = z) y .

( hf -case ) The fibration sequence of homotopy fibers defined for any pair of functions (f : X → Y) (g : Y → Z) and any terms (z : Z) (ye : hfiber g z) . It is based on functions hfiberftogf : hfiber f (pr1 ye) → hfiber (funcomp f g) z and hfibergftog : hfiber (funcomp f g) z → hfiber g z which are defined below.

The structures of a complex and of a fibration sequence on a composable pair of functions

The structure of a complex on a composable pair of functions (f : X → Y) (g : Y → Z) relative to a term z : Z .

Definition complxstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
:= ∏ x : X , (g (f x)) = z.

The structure of a fibration sequence on a complex.

Definition ezmap {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ez : complxstr f g z) :
  X → hfiber g z := λ x : X , make_hfiber g (f x) (ez x).

Definition isfibseq {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ez : complxstr f g z) := isweq (ezmap f g z ez).

Definition fibseqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
  := ∑ ez : complxstr f g z , isfibseq f g z ez.
Definition make_fibseqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
  := tpair (λ ez : complxstr f g z , isfibseq f g z ez).
Definition fibseqstrtocomplxstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z) :
  fibseqstr f g z → complxstr f g z
  := @pr1 _ (λ ez : complxstr f g z , isfibseq f g z ez).
Coercion fibseqstrtocomplxstr : fibseqstr >-> complxstr.

Definition ezweq {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (fs : fibseqstr f g z) : X ≃ hfiber g z
  := make_weq _ (pr2 fs).

Construction of the derived fibration sequence

Definition d1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (fs : fibseqstr f g z) (y : Y) : (g y ) = z → X
  := λ e : _, invmap (ezweq f g z fs) (make_hfiber g y e).

Definition ezmap1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (fs : fibseqstr f g z) (y : Y) (e : (g y ) = z) : hfiber f y.
Proof.
  intros.
  split with (d1 f g z fs y e).
  unfold d1.
  change (f (invmap (ezweq f g z fs) (make_hfiber g y e)))
  with (hfiberpr1 _ _ (ezweq f g z fs (invmap (ezweq f g z fs)
                                              (make_hfiber g y e)))).
  apply (maponpaths (hfiberpr1 g z)
                    (homotweqinvweq (ezweq f g z fs) (make_hfiber g y e))).
Defined.

Definition invezmap1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ez : complxstr f g z) (y : Y) : hfiber f y → (g y ) = z
  := λ xe: hfiber f y ,
           match xe with
             tpair _ x e ⇒ pathscomp0 (maponpaths g (pathsinv0 e)) (ez x)
           end.

Theorem isweqezmap1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
        (fs : fibseqstr f g z) (y : Y) : isweq (ezmap1 f g z fs y).
Proof.
  intros.
  set (ff := ezmap1 f g z fs y). set (gg := invezmap1 f g z (pr1 fs) y).
  assert (egf : ∏ e : _, (gg (ff e)) = e).
  intro. simpl.
  apply (hfibertriangle1inv0 g (homotweqinvweq (ezweq f g z fs)
                                               (make_hfiber g y e))).
  assert (efg : ∏ xe : _, (ff (gg xe)) = xe).
  intro. induction xe as [ x e ]. induction e. simpl.
  unfold ff. unfold ezmap1. unfold d1.
  change (make_hfiber g (f x) (pr1 fs x)) with (ezmap f g z fs x).
  apply (hfibertriangle2
           f (make_hfiber f (invmap (ezweq f g z fs) (ezmap f g z fs x)) _)
           (make_hfiber f x (idpath _))
           (homotinvweqweq (ezweq f g z fs) x)).
  simpl.
  set (e1 := pathsinv0 (pathscomp0rid (maponpaths f (homotinvweqweq
                                                       (ezweq f g z fs) x)))).
  assert (e2 : (maponpaths (hfiberpr1 g z)
                           (homotweqinvweq (ezweq f g z fs)
                                           ((ezmap f g z fs) x)))
               = (maponpaths f (homotinvweqweq (ezweq f g z fs) x))).
  set (e3 := maponpaths (λ e : _, maponpaths (hfiberpr1 g z) e)
                        (pathsinv0 (homotweqinvweqweq (ezweq f g z fs) x))).
  simpl in e3.
  set (e4 := maponpathscomp (ezmap f g z (pr1 fs)) (hfiberpr1 g z)
                            (homotinvweqweq (ezweq f g z fs) x)).
  simpl in e4. apply (pathscomp0 e3 e4). apply (pathscomp0 e2 e1).
  apply (isweq_iso _ _ egf efg).
Defined.

Definition ezweq1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (fs : fibseqstr f g z) (y : Y) := make_weq _ (isweqezmap1 f g z fs y).

Definition fibseq1 {X Y Z : UU} (f :X → Y) (g : Y → Z) (z : Z)
           (fs : fibseqstr f g z) (y : Y) : fibseqstr (d1 f g z fs y) f y
  := make_fibseqstr _ _ _ _ (isweqezmap1 f g z fs y).

Explicit description of the first map in the second derived sequence

Definition d2 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (fs : fibseqstr f g z) (y : Y) (x : X) (e : (f x ) = y) :
  (g y ) = z := pathscomp0 (maponpaths g (pathsinv0 e)) ((pr1 fs) x).
Definition ezweq2 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (fs : fibseqstr f g z) (y : Y) (x : X) :
  f x = y ≃ hfiber (d1 f g z fs y) x
  := ezweq1 (d1 f g z fs y) f y (fibseq1 f g z fs y) x.
Definition fibseq2 {X Y Z : UU} (f : X → Y) (g : Y →Z) (z : Z)
           (fs : fibseqstr f g z) (y : Y) (x : X) :
  fibseqstr (d2 f g z fs y x) (d1 f g z fs y) x
  := make_fibseqstr _ _ _ _
                   (isweqezmap1 (d1 f g z fs y) f y (fibseq1 f g z fs y) x).

Fibration sequences based on tpair P z and pr1 : total2 P → Z ( the "pr1-case" )

Construction of the fibration sequence.

Definition ezmappr1 {Z : UU} (P : Z → UU) (z : Z) :
  P z → hfiber (@pr1 Z P) z
  := λ p : P z , tpair _ (tpair _ z p) (idpath z).

Definition invezmappr1 {Z : UU} (P : Z → UU) (z : Z) :
  hfiber (@pr1 Z P) z → P z
  := λ te , transportf P (pr2 te) (pr2 (pr1 te)).

Definition isweqezmappr1 {Z : UU} (P : Z → UU) (z : Z) :
  isweq (ezmappr1 P z).
Proof.
  intros.
  assert (egf : ∏ x: P z , (invezmappr1 _ z ((ezmappr1 P z) x)) = x).
  intro. unfold ezmappr1. unfold invezmappr1. simpl. apply idpath.
  assert (efg : ∏ x: hfiber (@pr1 Z P) z ,
                     (ezmappr1 _ z (invezmappr1 P z x)) = x).
  intros. induction x as [ x t0 ]. induction t0. simpl in x. simpl.
  induction x. simpl. unfold transportf. unfold ezmappr1. apply idpath.
  apply (isweq_iso _ _ egf efg).
Defined.

Definition ezweqpr1 {Z : UU} (P : Z → UU) (z : Z)
  := make_weq _ (isweqezmappr1 P z).

Lemma isfibseqpr1 {Z : UU} (P : Z → UU) (z : Z) :
  isfibseq (λ p : P z , tpair _ z p) (@pr1 Z P) z (λ p : P z , idpath z).
Proof.
  intros. unfold isfibseq. unfold ezmap. apply isweqezmappr1.
Defined.

Definition fibseqpr1 {Z : UU} (P : Z → UU) (z : Z) :
  fibseqstr (λ p : P z , tpair _ z p) (@pr1 Z P) z
  := make_fibseqstr _ _ _ _ (isfibseqpr1 P z).

The main weak equivalence defined by the first derived of fibseqpr1 .

Definition ezweq1pr1 {Z : UU} (P : Z → UU) (z : Z) (zp : total2 P) :
pr1 zp = z ≃ hfiber (tpair P z) zp
:= ezweq1 _ _ z (fibseqpr1 P z) zp.

Fibration sequences based on hfiberpr1 : hfiber g z → Y and g : Y → Z (the "g-case")

Theorem isfibseqg {Y Z : UU} (g : Y → Z) (z : Z) :
  isfibseq (hfiberpr1 g z) g z (λ ye: _, pr2 ye).
Proof.
  intros.
  simple refine (isweqhomot _ _ _ (idisweq _)).
  - intro. apply idpath.
Defined.

Definition ezweqg {Y Z : UU} (g : Y → Z) (z : Z) := make_weq _ (isfibseqg g z).
Definition fibseqg {Y Z : UU} (g : Y → Z) (z : Z)
  : fibseqstr (hfiberpr1 g z) g z := make_fibseqstr _ _ _ _ (isfibseqg g z).

The first derived of fibseqg .

Definition d1g {Y Z : UU} (g : Y → Z) (z : Z) (y : Y) :
(g y ) = z → hfiber g z := make_hfiber g y.

note that d1g coincides with d1 _ _ _ (fibseqg g z) which makes the following two definitions possible.

Definition ezweq1g {Y Z : UU} (g : Y → Z) (z : Z) (y : Y) :
  g y = z ≃ hfiber (hfiberpr1 g z) y
  := make_weq _ (isweqezmap1 (hfiberpr1 g z) g z (fibseqg g z) y).
Definition fibseq1g {Y Z : UU} (g : Y → Z) (z : Z) (y : Y) :
  fibseqstr (d1g g z y) (hfiberpr1 g z) y
  := make_fibseqstr _ _ _ _ (isweqezmap1 (hfiberpr1 g z) g z (fibseqg g z) y).

The second derived of fibseqg .

Definition d2g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
(e: (pr1 ye') = y) : (g y ) = z
:= pathscomp0 (maponpaths g (pathsinv0 e)) (pr2 ye').

note that d2g coincides with d2 _ _ _ (fibseqg g z) which makes the following two definitions possible.

Definition ezweq2g
           {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z) :
  (pr1 ye') = y ≃ hfiber (make_hfiber g y) ye'
  := ezweq2 _ _ _ (fibseqg g z) _ _.
Definition fibseq2g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z) :
  fibseqstr (d2g g y ye') (make_hfiber g y) ye'
  := fibseq2 _ _ _ (fibseqg g z) _ _.

The third derived of fibseqg and an explicit description of the corresponding first map.

Definition d3g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
           (e : (g y ) = z) : (make_hfiber g y e ) = ye' → (pr1 ye') = y
  := d2 (d1g g z y) (hfiberpr1 g z) y (fibseq1g g z y) ye' e.

Lemma homotd3g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
      (e : (g y ) = z) (ee : (make_hfiber g y e ) = ye') :
  (d3g g y ye' e ee ) = (maponpaths (@pr1 _ _) (pathsinv0 ee)).
Proof.
  intros. unfold d3g. unfold d2. simpl. apply pathscomp0rid.
Defined.

Definition ezweq3g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
           (e : (g y ) = z)
  := ezweq2 (d1g g z y) (hfiberpr1 g z) y (fibseq1g g z y) ye' e.
Definition fibseq3g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
           (e : (g y ) = z)
  := fibseq2 (d1g g z y) (hfiberpr1 g z) y (fibseq1g g z y) ye' e.

Fibration sequence of h-fibers defined by a composable pair of functions (the "hf-case")

We construct a fibration sequence based on hfibersftogf f g z ye : hfiber f (pr1 ye) → hfiber gf z) and hfibersgftog f g z : hfiber gf z → hfiber g z) .

Definition hfibersftogf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ye : hfiber g z) (xe : hfiber f (pr1 ye)) : hfiber (funcomp f g) z.
Proof.
  intros.
  split with (pr1 xe).
  apply (pathscomp0 (maponpaths g (pr2 xe)) (pr2 ye)).
Defined.

Definition ezmaphf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ye : hfiber g z) (xe : hfiber f (pr1 ye)) :
  hfiber (hfibersgftog f g z) ye.
Proof.
  intros.
  split with (hfibersftogf f g z ye xe). simpl.
  apply (hfibertriangle2
           g (make_hfiber g (f (pr1 xe)) (pathscomp0 (maponpaths g (pr2 xe))
                                                    (pr2 ye))) ye (pr2 xe)).
  simpl. apply idpath.
Defined.

Definition invezmaphf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) :
  hfiber f (pr1 ye).
Proof.
  intros.
  split with (pr1 (pr1 xee')).
  apply (maponpaths (hfiberpr1 _ _) (pr2 xee')).
Defined.

Definition ffgg {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) :
  hfiber (hfibersgftog f g z) ye.
Proof.
  intros.
  induction ye as [ y e ]. induction e. unfold hfibersgftog.
  unfold hfibersgftog in xee'.
  induction xee' as [ xe e' ]. induction xe as [ x e ].
  set (e'' := (maponpaths g (maponpaths (hfiberpr1 g (g y)) e'))).
  simpl in e'.
  split with (make_hfiber (funcomp f g) x (pathscomp0 e'' (idpath (g y)))).
  simpl.
  apply (hfibertriangle2 _ (make_hfiber g (f x) (pathscomp0 e'' (idpath (g y))))
                         (make_hfiber g y (idpath _))
                         (maponpaths (hfiberpr1 _ _) e') (idpath _)).
Defined.

Definition homotffggid {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) :
  (ffgg f g z ye xee') = xee'.
Proof.
  intros.
  induction ye as [ y e ]. induction e.
  induction xee' as [ xe e' ]. induction e'.
  induction xe as [ x e ]. induction e.
  simpl. apply idpath.
Defined.

Theorem isweqezmaphf {X Y Z : UU} (f : X → Y) (g : Y → Z)
        (z : Z) (ye : hfiber g z) : isweq (ezmaphf f g z ye).
Proof.
  intros.
  set (ff := ezmaphf f g z ye). set (gg := invezmaphf f g z ye).
  assert (egf : ∏ xe : _ , (gg (ff xe)) = xe).
  induction ye as [ y e ]. induction e. intro xe.
  apply (hfibertriangle2 f (gg (ff xe)) xe (idpath (pr1 xe))).
  induction xe as [ x ex ]. simpl in ex. induction ex. simpl. apply idpath.
  assert (efg : ∏ xee' : _ , (ff (gg xee')) = xee').
  induction ye as [ y e ]. induction e. intro xee'.
  assert (hint : (ff (gg xee'))
                 = (ffgg f g (g y) (make_hfiber g y (idpath _)) xee')).
  induction xee' as [ xe e' ]. induction xe as [ x e ]. apply idpath.
  apply (pathscomp0 hint (homotffggid _ _ _ _ xee')).
  apply (isweq_iso _ _ egf efg).
Defined.

Definition ezweqhf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ye : hfiber g z) :
  hfiber f (pr1 ye) ≃ hfiber (hfibersgftog f g z) ye
  := make_weq _ (isweqezmaphf f g z ye).

Definition fibseqhf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ye : hfiber g z) :
  fibseqstr (hfibersftogf f g z ye) (hfibersgftog f g z) ye
  := make_fibseqstr _ _ _ _ (isweqezmaphf f g z ye).

Definition isweqinvezmaphf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
           (ye : hfiber g z) :
  isweq (invezmaphf f g z ye) := pr2 (invweq (ezweqhf f g z ye)).

Corollary weqhfibersgwtog {X Y Z : UU} (w : X ≃ Y) (g : Y → Z) (z : Z) :
  hfiber (funcomp w g) z ≃ hfiber g z.
Proof.
  intros.
  split with (hfibersgftog w g z).
  intro ye.
  apply (iscontrweqf (ezweqhf w g z ye) ((pr2 w) (pr1 ye))).
Defined.

Functions between total spaces of families

Definition totalfun {X : UU} (P Q : X → UU) (f : ∏ x : X , P x → Q x)
  : (∑ y , P y ) → (∑ y , Q y )
  := (λ z: total2 P , tpair Q (pr1 z) (f (pr1 z) (pr2 z))).

Theorem isweqtotaltofib {X : UU} (P Q : X → UU) (f : ∏ x : X , P x → Q x):
  isweq (totalfun _ _ f) → ∏ x : X , isweq (f x).
Proof.
  intros X0 x.
  set (totp := total2 P). set (totq := total2 Q).
  set (totf := (totalfun _ _ f)).
  set (pip := λ z: totp, pr1 z). set (piq:= λ z: totq, pr1 z).
  set (hfx := hfibersgftog totf piq x). simpl in hfx.
  assert (H : isweq hfx). unfold isweq. intro y.
  set (int := invezmaphf totf piq x y).
  assert (X1 : isweq int). apply (isweqinvezmaphf totf piq x y).
  induction y as [ t e ].
  assert (is1 : iscontr (hfiber totf t)).
  apply (X0 t). apply (iscontrweqb (make_weq int X1) is1).
  set (ip := ezmappr1 P x). set (iq := ezmappr1 Q x).
  set (h := λ p: P x, hfx (ip p)).
  assert (is2 : isweq h).
  apply (twooutof3c ip hfx (isweqezmappr1 P x) H).
  set (h':= λ p: P x, iq ((f x) p)).
  assert (ee : ∏ p:P x, (h p ) = (h' p )). intro. apply idpath.
  assert (X2 : isweq h'). apply (isweqhomot h h' ee is2).
  apply (twooutof3a (f x) iq X2).
  apply (isweqezmappr1 Q x).
Defined.

Definition weqtotaltofib {X : UU} (P Q : X → UU) (f : ∏ x : X , P x → Q x)
           (is : isweq (totalfun _ _ f)) (x : X) : P x ≃ Q x
  := make_weq _ (isweqtotaltofib P Q f is x).

Theorem isweqfibtototal {X : UU} (P Q : X → UU) (f : ∏ x : X , P x ≃ Q x) :
  isweq (totalfun _ _ f).
Proof.
  set (fpq := totalfun P Q f). set (pr1p := λ z : total2 P, pr1 z).
  set (pr1q := λ z : total2 Q, pr1 z).
  unfold isweq. intro xq.
  set (x:= pr1q xq).
  set (xqe:= make_hfiber pr1q xq (idpath _)).
  set (hfpqx:= hfibersgftog fpq pr1q x).

  assert (isint : iscontr (hfiber hfpqx xqe)).
  assert (isint1 : isweq hfpqx).
  set (ipx := ezmappr1 P x). set (iqx := ezmappr1 Q x).
  set (diag := λ p : P x, (iqx ((f x) p))).
  assert (is2: isweq diag).
  apply (twooutof3c (f x) iqx (pr2 (f x)) (isweqezmappr1 Q x)).
  apply (twooutof3b ipx hfpqx (isweqezmappr1 P x) is2).
  unfold isweq in isint1. apply (isint1 xqe).
  set (intmap := invezmaphf fpq pr1q x xqe).
  apply (iscontrweqf (make_weq intmap (isweqinvezmaphf fpq pr1q x xqe)) isint).
Defined.

Theorem isweqfibtototal' {X : UU} (P Q : X → UU) (f : ∏ x : X , P x ≃ Q x) :
  isweq (totalfun _ _ f).
Proof.
  use isweq_iso.
  - use totalfun.
    intro x. apply (invmap (f x)).
  - intro xp.
    use total2_paths_f.
    + apply idpath.
    + apply homotinvweqweq.
  - intro xp.
    use total2_paths_f.
    + apply idpath.
    + apply homotweqinvweq.
Defined.

Definition weqfibtototal {X : UU} (P Q : X → UU) (f : ∏ x , P x ≃ Q x) :
  (∑ x , P x ) ≃ (∑ x , Q x ) := make_weq _ (isweqfibtototal' P Q f).

Function fpmap between the total spaces from a function between the bases

Given X Y in UU , P:Y → UU and f: X → Y we get a function fpmap: total2 X (P f) → total2 Y P . The main theorem of this section asserts that the homotopy fiber of fpmap over yp:total Y P is naturally weakly equivalent to the homotopy fiber of f over pr1 yp . In particular, if f is a weak equivalence then so is fpmap .

Definition fpmap {X Y : UU} (f : X → Y) (P : Y → UU) :
  (∑ x , P (f x)) → (∑ y , P y ) := λ z , tpair P (f (pr1 z)) (pr2 z).

Definition hffpmap2 {X Y : UU} (f : X → Y) (P : Y → UU) :
  (∑ x , P (f x)) → ∑ u : total2 P , hfiber f (pr1 u).
Proof.
  intros X0.
  set (u:= fpmap f P X0).
  split with u.
  set (x:= pr1 X0).
  split with x.
  simpl. apply idpath.
Defined.

Lemma centralfiber {X : UU} (P : X → UU) (x : X) :
  isweq (λ p : P x , tpair (λ u : coconusfromt X x , P (pr1 u))
                              (coconusfromtpair X (idpath x)) p).
Proof.
  intros.
  set (f := λ p: P x, tpair (λ u: coconusfromt X x, P(pr1 u))
                                (coconusfromtpair X (idpath x)) p).
  set (g := λ z: total2 (λ u: coconusfromt X x, P (pr1 u)),
            transportf P (pathsinv0 (pr2 (pr1 z))) (pr2 z)).

  assert (efg : ∏ z : total2 (λ u : coconusfromt X x, P (pr1 u)),
                      (f (g z)) = z).
  intro.
  induction z as [ t x0 ]. induction t as [ t x1 ].
  simpl. induction x1. simpl. apply idpath.

  assert (egf : ∏ p : P x , (g (f p)) = p). intro. apply idpath.

  apply (isweq_iso f g egf efg).
Defined.

Lemma isweqhff {X Y : UU} (f : X → Y) (P : Y → UU) : isweq (hffpmap2 f P).
Proof.
  intros.
  set (int := total2 (λ x : X, total2 (λ u : coconusfromt Y (f x),
                                             P (pr1 u)))).
  set (intpair := tpair (λ x:X, total2 (λ u : coconusfromt Y (f x),
                                              P (pr1 u)))).
  set (toint :=
         λ z : (total2 (λ u : total2 P, hfiber f (pr1 u))),
               intpair (pr1 (pr2 z))
                       (tpair (fun u: coconusfromt Y (f (pr1 (pr2 z))) ⇒ P (pr1 u))
                              (coconusfromtpair _ (pr2 (pr2 z))) (pr2 (pr1 z)))).
  set (fromint := λ z : int,
                        tpair (λ u : total2 P, hfiber f (pr1 u))
                              (tpair P (pr1 (pr1 (pr2 z))) (pr2 (pr2 z)))
                              (make_hfiber f (pr1 z) (pr2 (pr1 (pr2 z))))).

  assert (fromto : ∏ u : (total2 (λ u : total2 P, hfiber f (pr1 u))),
                         (fromint (toint u)) = u).
  simpl in toint. simpl in fromint. simpl.
  intro u. induction u as [ t x ]. induction x. induction t as [ p0 p1 ].
  simpl. unfold toint. unfold fromint. simpl. apply idpath.

  assert (tofrom : ∏ u : int, (toint (fromint u)) = u).
  intro. induction u as [ t x ]. induction x as [ t0 x ]. induction t0.
  simpl in x. simpl. unfold fromint. unfold toint. simpl. apply idpath.

  assert (is : isweq toint). apply (isweq_iso toint fromint fromto tofrom).

  clear tofrom. clear fromto. clear fromint.
  set (h := λ u : total2 (λ x : X, P (f x)), toint ((hffpmap2 f P) u)).
  simpl in h.

  assert (l1 : ∏ x : X, isweq (λ p: P (f x),
                                 tpair (λ u : coconusfromt _ (f x), P (pr1 u))
                                       (coconusfromtpair _ (idpath (f x))) p)).
  intro. apply (centralfiber P (f x)).

  assert (X0 : isweq h).
  apply (isweqfibtototal
           (λ x : X, P (f x))
           (λ x : X, total2 (λ u : coconusfromt _ (f x), P (pr1 u)))
           (λ x : X, make_weq _ (l1 x))).

  apply (twooutof3a (hffpmap2 f P) toint X0 is).
Defined.

Homotopy fibers of fpmap

Definition hfiberfpmap {X Y : UU} (f : X → Y) (P : Y → UU) (yp : total2 P) :
  hfiber (fpmap f P) yp → hfiber f (pr1 yp).
Proof.
  intros X0.
  set (int1:= hfibersgftog (hffpmap2 f P)
                           (λ u : (∑ u : total2 P, hfiber f (pr1 u)),
                                  (pr1 u )) yp).
  set (phi := invezmappr1 (λ u:total2 P, hfiber f (pr1 u)) yp).
  apply (phi (int1 X0)).
Defined.

Theorem isweqhfiberfp {X Y : UU} (f : X → Y) (P : Y → UU) (yp : total2 P) :
  isweq (hfiberfpmap f P yp).
Proof.
  intros.

  set (int1 := hfibersgftog
                 (hffpmap2 f P)
                 (λ u : (total2 (λ u : total2 P, hfiber f (pr1 u))), (pr1 u ))
                 yp).
  assert (is1 : isweq int1). simpl in int1.
  apply (pr2 (weqhfibersgwtog
                (make_weq _ (isweqhff f P))
                (λ u : total2 (λ u : total2 P, hfiber f (pr1 u)), pr1 u) yp)).

  set (phi := invezmappr1 (λ u : total2 P, hfiber f (pr1 u)) yp).
  assert (is2 : isweq phi).
  apply (pr2 (invweq (ezweqpr1 (λ u : total2 P, hfiber f (pr1 u)) yp))).

  apply (twooutof3c int1 phi is1 is2).
Defined.

The fpmap from a weak equivalence is a weak equivalence

Corollary isweqfpmap {X Y : UU} (w : X ≃ Y)(P : Y → UU) : isweq (fpmap w P).
Proof.
  intros.
  unfold isweq. intro y. set (h := hfiberfpmap w P y).
  assert (X1 : isweq h). apply isweqhfiberfp.
  assert (is : iscontr (hfiber w (pr1 y))). apply (pr2 w).
  apply (iscontrweqb (make_weq h X1) is).
Defined.

Definition weqfp_map {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
  (∑ x , P(w x)) → (∑ y , P y ).
Proof.
  intros xp. exact (w (pr1 xp),,pr2 xp).
Defined.

Definition weqfp_invmap {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
  (∑ y , P y ) → (∑ x , P(w x)).
Proof.
  intros yp.
  exact (invmap w (pr1 yp),,
                transportf P (! homotweqinvweq w (pr1 yp)) (pr2 yp)).
Defined.

Definition weqfp {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
  (∑ x : X , P (w x)) ≃ (∑ y , P y ).
Proof.
  intros.
  ∃ (weqfp_map w P).
  refine (isweq_iso _ (weqfp_invmap w P) _ _).
  { intros xp. use total2_paths_f.
    { simpl. apply homotinvweqweq. }
    simpl. rewrite <- weq_transportf_adjointness.
    rewrite transport_f_f. rewrite pathsinv0l.
    apply idpath. }
  { intros yp. simple refine (total2_paths_f _ _).
    { simpl. apply homotweqinvweq. }
    simpl. rewrite transport_f_f. rewrite pathsinv0l. apply idpath. }
Defined.

Definition weqfp_compute_1 {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
  weqfp w P ¬ weqfp_map w P.
Proof.
  intros. intros xp. apply idpath.
Defined.

Definition weqfp_compute_2 {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
  invmap (weqfp w P) ¬ weqfp_invmap w P.
Proof.
  intros. intros yp. apply idpath.
Defined.

Definition weqtotal2overcoprod' {W X Y : UU} (P : W → UU) (f : X ⨿ Y ≃ W) :
  (∑ w , P w ) ≃ (∑ x : X , P (f (ii1 x))) ⨿ (∑ y : Y , P (f (ii2 y))).
Proof.
  intros.
  exact (weqcomp (invweq (weqfp f _)) (weqtotal2overcoprod (P ∘ f))).
Defined.

Total spaces of families over a contractible base

Definition fromtotal2overunit (P : unit → UU) (tp : total2 P) : P tt.
Proof.
  intros. induction tp as [ t p ]. induction t. apply p.
Defined.

Definition tototal2overunit (P : unit → UU) (p : P tt) : total2 P
  := tpair P tt p.

Theorem weqtotal2overunit (P : unit → UU) : (∑ u , P u ) ≃ P tt.
Proof.
  set (f := fromtotal2overunit P). set (g := tototal2overunit P).
  split with f.
  assert (egf : ∏ a : _ , (g (f a)) = a).
  intro a. induction a as [ t p ]. induction t. apply idpath.
  assert (efg : ∏ a : _ , (f (g a)) = a).
  intro a. apply idpath. apply (isweq_iso _ _ egf efg).
Defined.

The function on the total spaces from functions on the bases and on the fibers

Definition bandfmap {X Y : UU} (f : X → Y) (P : X → UU) (Q : Y → UU)
           (fm : ∏ x : X , P x → (Q (f x))) :
  (∑ x , P x ) → (∑ x , Q x ) := λ xp , f (pr1 xp) ,, fm (pr1 xp) (pr2 xp).

Theorem isweqbandfmap {X Y : UU} (w : X ≃ Y) (P : X → UU) (Q : Y → UU)
        (fw : ∏ x : X , P x ≃ Q (w x)) : isweq (bandfmap _ P Q fw).
Proof.
  intros.
  set (f1 := totalfun P _ fw).
  set (is1 := isweqfibtototal P (λ x:X, Q (w x)) fw).
  set (f2:= fpmap w Q).
  set (is2:= isweqfpmap w Q).
  assert (h: ∏ xp: total2 P, (f2 (f1 xp)) = (bandfmap w P Q fw xp )).
  { intro. apply idpath. }
  apply (isweqhomot _ _ h (twooutof3c f1 f2 is1 is2)).
Defined.

Definition weqbandf {X Y : UU} (w : X ≃ Y) (P : X → UU) (Q : Y → UU)
           (fw : ∏ x : X , P x ≃ Q (w x))
  := make_weq _ (isweqbandfmap w P Q fw).

Homotopy fiber squares

Homotopy commutative squares

Definition commsqstr {X X' Y Z : UU} (g' : Z → X') (f' : X' → Y) (g : Z → X)
           (f : X → Y) := ∏ (z : Z ), (f' (g' z)) = (f (g z)).

Definition hfibersgtof' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
           (g' : Z → X') (h : commsqstr g' f' g f) (x : X) (ze : hfiber g x) :
  hfiber f' (f x).
Proof.
  intros.
  induction ze as [ z e ].
  split with (g' z).
  apply (pathscomp0 (h z) (maponpaths f e)).
Defined.

Definition hfibersg'tof {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f) (x' : X')
           (ze : hfiber g' x') : hfiber f (f' x').
Proof.
  intros.
  induction ze as [ z e ].
  split with (g z).
  apply (pathscomp0 (pathsinv0 (h z)) (maponpaths f' e)).
Defined.

Definition transposcommsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') :
  commsqstr g' f' g f → commsqstr g f g' f'
  := λ h : _, λ z : Z , (pathsinv0 (h z)).

Short complexes and homotopy commutative squares

Lemma complxstrtocommsqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
      (h : complxstr f g z) :
  commsqstr f g (λ x : X , tt) (λ t : unit , z).
Proof.
  intros. assumption.
Defined.

Lemma commsqstrtocomplxstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
      (h : commsqstr f g (λ x : X , tt) (λ t : unit , z)) :
  complxstr f g z.
Proof.
  intros. assumption.
Defined.

Homotopy fiber products

Definition hfp {X X' Y : UU} (f : X → Y) (f' : X' → Y)
  := total2 (λ xx' : X × X', (f' (pr2 xx')) = (f (pr1 xx'))).
Definition hfpg {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
  hfp f f' → X := λ xx'e , (pr1 (pr1 xx'e)).
Definition hfpg' {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
  hfp f f' → X' := λ xx'e , (pr2 (pr1 xx'e)).

Definition commsqZtohfp {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f) :
  Z → hfp f f' := λ z : _, tpair _ (make_dirprod (g z) (g' z)) (h z).

Definition commsqZtohfphomot {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f) :
  ∏ z : Z , (hfpg _ _ (commsqZtohfp _ _ _ _ h z)) = (g z )
  := λ z : _, idpath _.

Definition commsqZtohfphomot' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f) :
  ∏ z : Z , (hfpg' _ _ (commsqZtohfp _ _ _ _ h z)) = (g' z )
  := λ z : _, idpath _.

Definition hfpoverX {X X' Y : UU} (f : X → Y) (f' : X' → Y)
  := total2 (λ x : X , hfiber f' (f x)).
Definition hfpoverX' {X X' Y : UU} (f : X → Y) (f' : X' → Y)
  := total2 (λ x' : X', hfiber f (f' x')).

Definition weqhfptohfpoverX {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
  hfp f f' ≃ hfpoverX f f'.
Proof.
  intros.
  exact (weqtotal2asstor _ (λ xx', f' (pr2 xx') = f (pr1 xx'))).
Defined.

Definition weqhfptohfpoverX' {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
  hfp f f' ≃ hfpoverX' f f'.
Proof.
  intros.
  set (w1 := weqfp (weqdirprodcomm X X')
                   (λ xx' : X' × X , (f' (pr1 xx')) = (f (pr2 xx')))).
  simpl in w1.
  set (w2 := weqfibtototal
               (λ x'x : X' × X, (f' (pr1 x'x)) = (f (pr2 x'x)))
               (λ x'x : X' × X, (f (pr2 x'x)) = (f' (pr1 x'x)))
               (λ x'x : _, weqpathsinv0 (f' (pr1 x'x)) (f (pr2 x'x)))).
  set (w3 := weqtotal2asstor
               (λ x' : X', X)
               (λ x'x : X' × X, (f (pr2 x'x)) = (f' (pr1 x'x)))).
  simpl in w3.
  apply (weqcomp (weqcomp w1 w2) w3).
Defined.

Lemma weqhfpcomm {X X' Y : UU} (f : X → Y) (f' : X' → Y):
  hfp f f' ≃ hfp f' f.
Proof.
  intros.
  set (w1 := weqfp (weqdirprodcomm X X')
                   (λ xx' : X' × X, (f' (pr1 xx')) = (f (pr2 xx')))).
  simpl in w1.
  set (w2 := weqfibtototal
               (λ x'x : X' × X, (f' (pr1 x'x)) = (f (pr2 x'x)))
               (λ x'x : X' × X, (f (pr2 x'x)) = (f' (pr1 x'x)))
               (λ x'x : _, weqpathsinv0 (f' (pr1 x'x)) (f (pr2 x'x)))).
  apply (weqcomp w1 w2).
Defined.

Definition commhfp {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
  commsqstr (hfpg' f f') f' (hfpg f f') f
  := λ xx'e : hfp f f', pr2 xx'e.

Homotopy fiber products and homotopy fibers

Definition hfibertohfp {X Y : UU} (f : X → Y) (y : Y) (xe : hfiber f y) :
  hfp (λ t : unit , y) f := tpair (λ tx : unit × X , (f (pr2 tx)) = y)
                                     (make_dirprod tt (pr1 xe)) (pr2 xe).

Definition hfptohfiber {X Y : UU} (f : X → Y) (y : Y)
           (hf : hfp (λ t : unit , y) f) : hfiber f y
  := make_hfiber f (pr2 (pr1 hf)) (pr2 hf).

Lemma weqhfibertohfp {X Y : UU} (f : X → Y) (y : Y) :
  hfiber f y ≃ hfp (λ _:unit , y) f.
Proof.
  intros.
  set (ff := hfibertohfp f y).
  set (gg := hfptohfiber f y).
  split with ff.
  assert (egf : ∏ xe : _, (gg (ff xe)) = xe).
  intro. induction xe. apply idpath.
  assert (efg : ∏ hf : _, (ff (gg hf)) = hf).
  intro.
  induction hf as [ tx e ]. induction tx as [ t x ].
  induction t. apply idpath. apply (isweq_iso _ _ egf efg).
Defined.

Lemma hfp_left {X Y Z : UU} (f : X → Z) (g : Y → Z) :
  hfp f g ≃ ∑ x , hfiber g (f x).
Proof.
  intros. apply weqtotal2dirprodassoc.
Defined.

Definition hfp_right {X Y Z : UU} (f : X → Z) (g : Y → Z) :
  hfp f g ≃ ∑ y , hfiber f (g y).
Proof.
  intros. use weq_iso.
  - intros [[x y] e]. exact (y,,x,,!e).
  - intros [x [y e]]. exact ((y,,x),,!e).
  - intros [[x y] e]. apply maponpaths, pathsinv0inv0.
  - intros [x [y e]]. apply maponpaths, maponpaths, pathsinv0inv0.
Defined.

Definition hfiber_comm {X Y Z : UU} (f : X → Z) (g : Y → Z) :
  (∑ x , hfiber g (f x)) ≃ (∑ y , hfiber f (g y)).
Proof.
  intros. use weq_iso.
  - intros [x [y e]]. exact (y,,x,,!e).
  - intros [y [x e]]. exact (x,,y,,!e).
  - intros [x [y e]]. apply maponpaths, maponpaths, pathsinv0inv0.
  - intros [y [x e]]. apply maponpaths, maponpaths, pathsinv0inv0.
Defined.

Homotopy fiber squares

Definition ishfsq {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f)
  := isweq (commsqZtohfp f f' g g' h).

Definition hfsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X')
  := total2 (λ h : commsqstr g' f' g f , isweq (commsqZtohfp f f' g g' h)).

Definition make_hfsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X')
  := tpair (λ h : commsqstr g' f' g f , isweq (commsqZtohfp f f' g g' h)).

Definition hfsqstrtocommsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') :
  hfsqstr f f' g g' → commsqstr g' f' g f
  := @pr1 _ (λ h : commsqstr g' f' g f , isweq (commsqZtohfp f f' g g' h)).
Coercion hfsqstrtocommsqstr : hfsqstr >-> commsqstr.

Definition weqZtohfp {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
           (g' : Z → X') (hf : hfsqstr f f' g g') : Z ≃ hfp f f'
  := make_weq _ (pr2 hf).

Lemma isweqhfibersgtof' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
      (g' : Z → X') (hf : hfsqstr f f' g g') (x : X) :
  isweq (hfibersgtof' f f' g g' hf x).
Proof.
  intros.
  set (is := pr2 hf).
  set (h := pr1 hf).
  set (a := weqtococonusf g).
  set (c := make_weq _ is).
  set (d := weqhfptohfpoverX f f').
  set (b0 := totalfun _ _ (hfibersgtof' f f' g g' h)).

  assert (h1 : ∏ z : Z, (d (c z)) = (b0 (a z))).
  intro. simpl. unfold b0. unfold a. unfold weqtococonusf. unfold tococonusf.
  simpl. unfold totalfun, total2asstor, hfibersgtof'; simpl.
  assert (e : (h z) = (pathscomp0 (h z) (idpath (f (g z))))).
  apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath.

  assert (is1 : isweq (λ z : _, b0 (a z))).
  apply (isweqhomot _ _ h1). apply (twooutof3c _ _ (pr2 c) (pr2 d)).

  assert (is2 : isweq b0).
  apply (twooutof3b _ _ (pr2 a) is1).

  apply (isweqtotaltofib _ _ _ is2 x).
Defined.

Definition weqhfibersgtof' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') (hf : hfsqstr f f' g g') (x : X)
  := make_weq _ (isweqhfibersgtof' _ _ _ _ hf x).

Lemma ishfsqweqhfibersgtof' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
      (g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f)
      (is : ∏ x : X , isweq (hfibersgtof' f f' g g' h x)) : hfsqstr f f' g g'.
Proof.
  intros. split with h.
  set (a := weqtococonusf g).
  set (c0 := commsqZtohfp f f' g g' h).
  set (d := weqhfptohfpoverX f f').
  set (b := weqfibtototal _ _ (λ x : X, make_weq _ (is x))).

  assert (h1 : ∏ z : Z, (d (c0 z)) = (b (a z))).
  intro. simpl. unfold b. unfold a. unfold weqtococonusf. unfold tococonusf.
  simpl. unfold totalfun, total2asstor, hfibersgtof'; simpl.
  assert (e : (h z) = (pathscomp0 (h z) (idpath (f (g z))))).
  apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath.

  assert (is1 : isweq (λ z : _, d (c0 z))).
  apply (isweqhomot _ _ (λ z : Z, (pathsinv0 (h1 z)))).
  apply (twooutof3c _ _ (pr2 a) (pr2 b)).

  apply (twooutof3a _ _ is1 (pr2 d)).
Defined.

Lemma isweqhfibersg'tof {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
      (g' : Z → X') (hf : hfsqstr f f' g g') (x' : X') :
  isweq (hfibersg'tof f f' g g' hf x').
Proof.
  intros.
  set (is := pr2 hf).
  set (h := pr1 hf).
  set (a' := weqtococonusf g').
  set (c' := make_weq _ is).
  set (d' := weqhfptohfpoverX' f f').
  set (b0' := totalfun _ _ (hfibersg'tof f f' g g' h)).

  assert (h1 : ∏ z : Z, (d' (c' z)) = (b0' (a' z))).
  intro. unfold b0'. unfold a'. unfold weqtococonusf. unfold tococonusf.
  unfold totalfun, hfibersg'tof; simpl.
  assert (e : (pathsinv0 (h z))
              = (pathscomp0 (pathsinv0 (h z)) (idpath (f' (g' z))))).
  apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath.

  assert (is1 : isweq (λ z : _, b0'(a' z))).
  apply (isweqhomot _ _ h1). apply (twooutof3c _ _ (pr2 c') (pr2 d')).

  assert (is2 : isweq b0'). apply (twooutof3b _ _ (pr2 a') is1).

  apply (isweqtotaltofib _ _ _ is2 x').
Defined.

Definition weqhfibersg'tof {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
           (g : Z → X) (g' : Z → X') (hf : hfsqstr f f' g g') (x' : X')
  := make_weq _ (isweqhfibersg'tof _ _ _ _ hf x').

Lemma ishfsqweqhfibersg'tof {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
      (g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f)
      (is : ∏ x' : X', isweq (hfibersg'tof f f' g g' h x')) : hfsqstr f f' g g'.
Proof.
  intros.
  split with h.
  set (a' := weqtococonusf g').
  set (c0' := commsqZtohfp f f' g g' h).
  set (d' := weqhfptohfpoverX' f f').
  set (b' := weqfibtototal _ _ (λ x' : X', make_weq _ (is x'))).

  assert (h1 : ∏ z : Z, (d' (c0' z)) = (b' (a' z))).
  intro. simpl. unfold b'. unfold a'. unfold weqtococonusf. unfold tococonusf.
  unfold totalfun, total2asstor, hfibersg'tof; simpl.
  assert (e : (pathsinv0 (h z)) =
              (pathscomp0 (pathsinv0 (h z)) (idpath (f' (g' z))))).
  apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath.

  assert (is1 : isweq (λ z : _, d' (c0' z))).
  apply (isweqhomot _ _ (λ z : Z, (pathsinv0 (h1 z)))).
  apply (twooutof3c _ _ (pr2 a') (pr2 b')).

  apply (twooutof3a _ _ is1 (pr2 d')).
Defined.

Theorem transposhfpsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
        (g' : Z → X') (hf : hfsqstr f f' g g') : hfsqstr f' f g' g.
Proof.
  intros.
  set (is := pr2 hf). set (h := pr1 hf).
  set (th := transposcommsqstr f f' g g' h).
  split with th.
  set (w1 := weqhfpcomm f f').
  assert (h1 : ∏ z : Z, (w1 (commsqZtohfp f f' g g' h z))
                        = (commsqZtohfp f' f g' g th z )).
  intro. unfold commsqZtohfp. simpl. unfold fpmap. unfold totalfun.
  simpl. apply idpath.
  apply (isweqhomot _ _ h1). apply (twooutof3c _ _ is (pr2 w1)).
Defined.

Fiber sequences and homotopy fiber squares

Theorem fibseqstrtohfsqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
        (hf : fibseqstr f g z) : hfsqstr (λ t : unit , z) g (λ x : X , tt) f.
Proof.
  intros.
  split with (pr1 hf).
  set (ff := ezweq f g z hf).
  set (ggff := commsqZtohfp (λ t : unit , z) g (λ x : X, tt) f (pr1 hf)).
  set (gg := weqhfibertohfp g z).
  apply (pr2 (weqcomp ff gg)).
Defined.

Theorem hfsqstrtofibseqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
        (hf : hfsqstr (λ t : unit , z) g (λ x : X , tt) f) : fibseqstr f g z.
Proof.
  intros. split with (pr1 hf). set (ff := ezmap f g z (pr1 hf)).
  set (ggff := weqZtohfp (λ t : unit , z) g (λ x : X, tt) f hf).
  set (gg := weqhfibertohfp g z).
  apply (twooutof3a ff gg (pr2 ggff) (pr2 gg)).
Defined.

Library UniMath.Foundations.PartA

Univalent Foundations, Part A

Contents

Preamble

Imports

Some standard constructions not using identity types (paths)

Canonical functions from empty and to unit

Functions from unit corresponding to terms

Identity functions and function composition, curry and uncurry

Definition of binary operation

Iteration of an endomorphism

Basic constructions related to the adjoint evaluation function X → ((X → Y) → Y)

Pairwise direct products

Negation and double negation

Logical equivalence

Paths and operations on paths

Associativity of function composition and mutual invertibility of curry/uncurry

Composition of paths and inverse paths

Direct product of paths

The function maponpaths between paths types defined by a function between ambient types

maponpaths for the identity functions and compositions of functions

Homotopy between sections

Equality between functions defines a homotopy

maponpaths for a function homotopic to the identity

maponpaths in the case of a projection p with a section s

Fibrations and paths - the transport functions

A series of lemmas about paths and total2

Lemmas about transport adapted from the HoTT library and the HoTT book

Homotopies between families and the total spaces

First fundamental notions

Contractibility iscontr

Homotopy fibers hfiber

The functions between the hfibers of homotopic functions over the same point

Paths in homotopy fibers

Coconuses: spaces of paths that begin coconusfromt or end coconustot at a given point

The total paths space of a type - two definitions

Coconus of a function: the total space of the family of h-fibers

Weak equivalences

Basics - isweq and weq

Weak equivalences and paths spaces (more results in further sections)

Adjointness property of a weak equivalence and its inverse

Transport functions are weak equivalences

Weak equivalences between contractible types (one implication)

unit and contractibility

Homotopy equivalence is a weak equivalence

Some weak equivalences

The 2-out-of-3 property of weak equivalences

Any function between contractible types is a weak equivalence

Composition of weak equivalences

The 2-out-of-6 (two-out-of-six) property of weak equivalences

Pairwise direct products of weak equivalences

Weak equivalence of a type and its direct product with the unit

Associativity of total2 as a weak equivalence

Associativity and commutativity of direct products as weak equivalences

Binary coproducts and their basic properties

Distributivity of coproducts and direct products as a weak equivalence

Total space of a family over a coproduct

Pairwise sum of functions, coproduct associativity and commutativity

Coproduct with a "negative" type

Coproduct of two functions

The equality_cases construction and four applications to ii1 and ii2

Bool as coproduct

Pairwise coproducts as dependent sums of families over bool

Splitting of X into a coproduct defined by a function X → Y ⨿ Z

Some properties of bool

Fibrations with only one non-empty fiber

Basics about fibration sequences.

Fibrations sequences and their first "left shifts"

The structures of a complex and of a fibration sequence on a composable pair of functions

Construction of the derived fibration sequence

Explicit description of the first map in the second derived sequence

Fibration sequences based on tpair P z and pr1 : total2 P → Z ( the "pr1-case" )

Fibration sequences based on hfiberpr1 : hfiber g z → Y and g : Y → Z (the "g-case")

Fibration sequence of h-fibers defined by a composable pair of functions (the "hf-case")

Functions between total spaces of families

Function fpmap between the total spaces from a function between the bases

Homotopy fibers of fpmap

The fpmap from a weak equivalence is a weak equivalence

Total spaces of families over a contractible base

The function on the total spaces from functions on the bases and on the fibers