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.

Contents

  • 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.

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

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)).

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 Y) : 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.
  unfold funcomp. 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)).
  unfold funcomp. 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)) =