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. Show proof.
  intro X.
  intro H.
  induction H.

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.
Show proof.
  induction n as [ | n IHn ].
  + exact (idfun T).
  + exact (f ∘ IHn).

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.
Show proof.
  intros X0.
  apply xp. intro x.
  apply yp. intro y.
  apply (X0 (make_dirprod x y)).

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).
Show proof.
  intros.
  intros X2.
  apply (dnegf X2).
  + apply dnx.
  + apply dny.

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.
Show proof.
  intros. split; apply idfun.

Lemma issymm_logeq (X Y : UU) : (X <-> Y) -> (Y <-> X).
Show proof.
  intros e.
  exact (pr2 e,,pr1 e).

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).
Show proof.
  intros x y.
  split.
  - intros x'. exact y.
  - intros y'. exact x.

Definition logeq_both_false {X Y : UU} : ¬X -> ¬Y -> (X <-> Y).
Show proof.
  intros nx ny.
  split.
  - intros x. induction (nx x).
  - intros y. induction (ny y).

Definition logeq_trans {X Y Z : UU} : (X <-> Y) -> (Y <-> Z) -> (X <-> Z).
Show proof.
  intros i j. exact (pr1 j ∘ pr1 i,, pr2 i ∘ pr2 j).


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.
Show proof.
  intros .
  apply idpath.

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

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.
Show proof.
  intros. apply idpath.

Composition of paths and inverse paths


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

#[global]
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.
Show proof.
  intros. induction e1. simpl. apply idpath.

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.
Show proof.
  intros. induction e. apply idpath.

#[global]
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.
Show proof.
  intros. induction f. apply idpath.

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

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

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

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

Lemma pathscomp_cancel_left {X : UU} {x y z : X} (p : x = y) (r s : y = z) :
  p @ r= p @ s -> r = s.
Show proof.
  intros e. induction p. exact e.

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

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

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.
Show proof.
  intros. induction ex. induction ey. apply idpath.

Lemma dirprodeq (A B : UU) (ab ab' : A × B) :
  pr1 ab = pr1 ab' -> pr2 ab = pr2 ab' -> ab = ab'.
Show proof.
  intros H H'.
  induction ab as [a b].
  induction ab' as [a' b']; simpl in *.
  induction H.
  induction H'.
  apply idpath.

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.
Show proof.
  intros. induction e. apply idpath.

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'.
Show proof.
  intros. induction ex. induction ey. apply idpath.

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.
Show proof.
  intros. induction e1. induction e2. apply idpath.

Definition maponpathsinv0 {X Y : UU} (f : X -> Y)
           {x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e).
Show proof.
  intros. induction e. apply idpath.

maponpaths for the identity functions and compositions of functions


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

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.
Show proof.
  intros. induction e. apply idpath.

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.
Show proof.
  intros x. apply idpath.

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.
Show proof.
  intros h t. induction h. apply (idpath _).

Definition eqtohomot {T:UU} {P:T->UU} {f g:∏ t:T, P t} : f = g -> f ~ g.
Show proof.
  intros e t. induction e. apply idpath.

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').
Show proof.
  intros. induction e. simpl.
  apply pathsinv0.
  apply pathsinv0r.

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

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.
Show proof.
  intros.
  apply (pathscomp0 (! eps x)).
  apply (maponpaths p e).

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'.
Show proof.
  intros.
  set (e' := pathssec1 s p eps _ _ e).
  apply (e' @ (eps x')).

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

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.
Show proof.
  intros. induction e. simpl.
  apply pathssec2id.

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.
Show proof.
  intros. induction e.
  split with (idfun (P x)).
  split with (λ p, idpath _).
  unfold maponpaths. simpl.
  intro. apply idpath.

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.
Show proof.
  intros. apply idpath.

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.
Show proof.
  intros. induction e. apply idpath.

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.
Show proof.
  intros. induction e. apply idpath.

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.
Show proof.
  intros. induction e'. induction e. apply idpath.

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.
Show proof.
  intros. induction e'. induction e. apply idpath.

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.
Show proof.
  intros. induction e'. induction e. apply idpath.

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.
Show proof.
  intros. induction e'. induction e. apply idpath.

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).
Show proof.
  intros. induction e. apply idpath.

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.
Show proof.
  intros. exact (transport_map (P:= λ _,unit) (λ x _,f x) e tt).

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 .
Show proof.
  intros. induction e. apply idpath .

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.
Show proof.
  intros. induction p. apply idpath.

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

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

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.
Show proof.
  induction e. apply idpath.
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.
Show proof.
  intros. induction e. apply idpath.

Definition transportfbinv {T} (P:T->Type) {t u:T} (e:t = u) (p:P u) : e#e#'p = p.
Show proof.
  intros. induction e. apply idpath.

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.
Show proof.
  intros.
  apply maponpaths; assumption.

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.
Show proof.
  intros. induction p. induction q. apply idpath.

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.
Show proof.
  intros. induction p. induction q. apply idpath.

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.
Show proof.
  intros. induction p. change _ with (b1 = b2) in q. induction q. apply idpath.

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

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'.
Show proof.
  intros.
  induction s as [a b]; induction s' as [a' b']; simpl in *.
  exact (two_arg_paths_f p q).

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'.
Show proof.
  intros.
  induction s as [a b]; induction s' as [a' b']; simpl in *.
  exact (two_arg_paths_b p q).

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

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.
Show proof.
  intros. exact (two_arg_paths_f p q).

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.
Show proof.
  intros. exact (two_arg_paths_b p q).

Definition pair_path_in2 {X : UU} (P : X -> UU) {x : X} {p q : P x} (e : p = q) :
  x,,p = x,,q.
Show proof.
  intros. apply maponpaths. exact e.

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.
Show proof.
  induction p.
  apply idpath.

Lemma total2_fiber_paths {A : UU} {B : A -> UU} {x y : ∑ x, B x} (p : x = y) :
  total2_paths_f _ (fiber_paths p) = p.
Show proof.
  induction p.
  induction x.
  apply idpath.

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.
Show proof.
  induction x as [x H].
  induction y as [y K].
  simpl in *.
  induction p.
  induction q.
  apply idpath.

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.
Show proof.
  induction x as [x H].
  induction y as [y K].
  simpl in *.
  induction p.
  induction q.
  apply idpath.

Definition total2_base_map {S T:UU} {P: T -> UU} (f : S->T) : (∑ i, P(f i)) -> (∑ j, P j).
Show proof.
  intros x.
  exact (f(pr1 x),,pr2 x).

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.
Show proof.
  intros p. simple refine (_ @ fiber_paths p). unfold base_paths. simpl.
  apply pathsinv0, transport_section.

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).
Show proof.
  intros.
  induction p.
  exact z.

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)).
Show proof.
  intros.
  induction p.
  induction yz.
  apply idpath.

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))).
Show proof.
  induction p.
  apply idpath.

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'))).
Show proof.
  intros.
  apply transportf_dirprod.

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

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

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

Homotopies between families and the total spaces


Definition famhomotfun {X : UU} {P Q : X -> UU}
           (h : P ~ Q) (xp : total2 P) : total2 Q.
Show proof.
  intros.
  exists (pr1 xp).
  induction (h (pr1 xp)).
  apply (pr2 xp).

Definition famhomothomothomot {X : UU} {P Q : X -> UU} (h1 h2 : P ~ Q)
           (H : h1 ~ h2) : famhomotfun h1 ~ famhomotfun h2.
Show proof.
  intros.
  intro xp.
  apply (maponpaths (λ q, tpair Q (pr1 xp) q)).
  induction (H (pr1 xp)).
  apply idpath.

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.
Show proof.
  intros. set (x := iscontrpr1 is). set (fe := pr2 is). split with (p x).
  intro t. apply (! (eps t) @ maponpaths p (fe (s t))).

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

Lemma path_to_ctr (A : UU) (B : A -> UU) (isc : ∃! a, B a)
      (a : A) (p : B a) : a = pr1 (pr1 isc).
Show proof.
  set (Hi := tpair _ a p).
  apply (maponpaths pr1 (pr2 isc Hi)).

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.
Show proof.
  intros xe.
  induction xe as [x e].
  split with x.
  apply (!(h x) @ e).

Lemma hfibershomotgtof {X Y : UU} (f g : X -> Y)
      (h : f ~ g) (y : Y) : hfiber g y -> hfiber f y.
Show proof.
  intros xe.
  induction xe as [x e].
  split with x.
  apply (h x @ e).

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.
Show proof.
  intros. induction e. simpl. apply idpath.

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).
Show proof.
  intros.
  intermediate_path (maponpaths f (maponpaths pr1 e) @ idpath (f x)).
  - apply hfibertriangle1.
  - apply pathscomp0rid.

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.
Show proof.
  intros. induction e. apply idpath.

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.
Show proof.
  intros.
  intermediate_path (maponpaths f (! (maponpaths pr1 e)) @ idpath (f x)).
  - apply pathsinv0, pathscomp0rid.
  - apply hfibertriangle1inv0.

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

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.
Show proof.
  intros.
  induction c1 as [x0 x].
  induction x.
  induction c2 as [x1 y].
  induction y.
  apply idpath.

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

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

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

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.
Show proof.
  intros.
  induction yxe as [y xe].
  induction xe as [x e].
  unfold fromcoconusf.
  unfold tococonusf.
  simpl.
  induction e.
  apply idpath.

Lemma homotfromtococonusf {X Y : UU} (f : X -> Y) :
  ∏ x : X, fromcoconusf f (tococonusf f x) = x.
Show proof.
  intros.
  unfold fromcoconusf.
  unfold tococonusf.
  simpl.
  apply idpath.

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

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.
Show proof.
  intros. apply (iscontrpr1 (weqproperty w y)).

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

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.
Show proof.
  intros. intro y. apply (fromempty y).

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

Lemma isweqtoempty2 {X Y : UU} (f : X -> Y) (is : ¬ Y) : isweq f.
Show proof.
  intros. intro y. induction (is y).

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.
Show proof.
  intros nx ny.
  use make_weq.
  - intro x. apply fromempty, nx. exact x.
  - intro y. apply fromempty, ny. exact y.

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.
Show proof.
  intros.
  unfold invmap.
  apply (pr2 (weqccontrhfiber w y)).

Definition homotinvweqweq0 {X Y : UU} (w : X ≃ Y) :
  ∏ x : X, x = invmap w (w x).
Show 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).

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

Lemma homotweqinv {X Y Z} (f:X->Z) (w:X≃Y) (g:Y->Z) : f ~ g ∘ w -> f ∘ invmap w ~ g.
Show proof.
  intros p y.
  simple refine (p (invmap w y) @ _); clear p.
  simpl. apply maponpaths. apply homotweqinvweq.

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

Definition isinjinvmap {X Y} (v w:X≃Y) : invmap v ~ invmap w -> v ~ w.
Show proof.
  intros h x.
  intermediate_path (w ((invmap w) (v x))).
  { apply pathsinv0. apply homotweqinvweq. }
  rewrite <- h. rewrite homotinvweqweq. apply idpath.

Definition isinjinvmap' {X Y} (v w:X->Y) (v' w':Y->X) : w ∘ w' ~ idfun Y -> v' ∘ v ~ idfun X -> v' ~ w' -> v ~ w.
Show proof.
  intros p q h x .
  intermediate_path (w (w' (v x))).
  { apply pathsinv0. apply p. }
  apply maponpaths. rewrite <- h. apply q.

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.
Show proof.
  intros. induction e1. simpl in *. exact ee.

Definition homotweqinvweqweq {X Y : UU} (w : X ≃ Y) (x : X) :
  maponpaths w (homotinvweqweq w x) = homotweqinvweq w (w x).
Show 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)).

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.
Show proof.
  intros. refine (functtransportf w P (!homotinvweqweq w x) p @ _).
  apply (maponpaths (λ e, transportf P e p)).
  rewrite maponpathsinv0. apply maponpaths. apply homotweqinvweqweq.

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.
Show proof.
  intros.
  refine (functtransportb w P (homotinvweqweq w x) p @ _).
  apply (maponpaths (λ e, transportb P e p)).
  apply homotweqinvweqweq.

Transport functions are weak equivalences


Lemma isweqtransportf {X : UU} (P : X -> UU) {x x' : X}
      (e : x = x') : isweq (transportf P e).
Show proof.
  intros. induction e. unfold transportf. simpl. apply idisweq.

Lemma isweqtransportb {X : UU} (P : X -> UU) {x x' : X}
      (e : x = x') : isweq (transportb P e).
Show proof.
  intros. apply (isweqtransportf _ (pathsinv0 e)).

Weak equivalences between contractible types (one implication)


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

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'.
Show proof.
  intros. induction x. induction x'. apply idpath.

Lemma unitl0 : tt = tt -> coconustot _ tt.
Show proof.
  intros e. apply (coconustotpair unit e).

Lemma unitl1: coconustot _ tt -> tt = tt.
Show proof.
  intro cp. induction cp as [x t]. induction x. exact t.

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

Lemma unitl3: ∏ e : tt = tt, e = idpath tt.
Show proof.
  intros.

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

  set (e1 := maponpaths unitl1 e0).

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

Theorem iscontrunit: iscontr (unit).
Show proof.
  split with tt. intros t. apply (isProofIrrelevantUnit t tt).

paths in unit are contractible.

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

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

Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2.
Show proof.
  intros.
  apply proofirrelevancecontr.
  apply (iscontrpathsinunit tt tt).

Lemma isweqcontrtounit {T : UU} (is : iscontr T) : isweq (λ (_ : T), tt).
Show 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.

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

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

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'.
Show 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.

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

Definition homothfiber1 {X Y : UU} (f g : X -> Y)
           (h : f ~ g) (y : Y) (xe : hfiber f y) : hfiber g y.
Show proof.
  intros.
  set (x := pr1 xe).
  set (e := pr2 xe).
  apply (make_hfiber g x (!(h x) @ e)).

Definition homothfiber2 {X Y : UU} (f g : X -> Y)
           (h : f ~ g) (y : Y) (xe : hfiber g y) : hfiber f y.
Show proof.
  intros.
  set (x := pr1 xe).
  set (e := pr2 xe).
  apply (make_hfiber f x (h x @ e)).

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

Lemma iscontrhfiberl2 {X Y : UU} (f g : X -> Y)
      (h : f ~ g) (y : Y) (is : iscontr (hfiber f y)) : iscontr (hfiber g y).
Show 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).

Corollary isweqhomot {X Y : UU} (f1 f2 : X -> Y)
          (h : f1 ~ f2) : isweq f1 -> isweq f2.
Show proof.
  intros x0.
  unfold isweq.
  intro y.
  apply (iscontrhfiberl2 f1 f2 h).
  apply x0.

Corollary remakeweq {X Y : UU} {f:X≃Y} {g:X->Y} : f ~ g -> X≃Y.
Show proof.
  intros e.
  exact (g ,, isweqhomot f g e (weqproperty f)).

Lemma remakeweq_eq {X Y : UU} (f1:X≃Y) (f2:X->Y) (e:f1~f2) : pr1weq (remakeweq e) = f2.
Show proof.
  intros. apply idpath.

Lemma remakeweq_eq' {X Y : UU} (f1:X≃Y) (f2:X->Y) (e:f1~f2) : invmap (remakeweq e) = invmap f1.
Show proof.
  intros. apply idpath.

Lemma iscontr_move_point {X} : X -> iscontr X -> iscontr X.
Show proof.
  intros x i.
  exists x.
  intro y.
  apply proofirrelevancecontr.
  exact i.

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

Corollary remakeweqinv {X Y : UU} {f:X≃Y} {h:Y->X} : invmap f ~ h -> X≃Y.
Show proof.
  intros e. exists f. intro y.
  assert (p : hfiber f y).
  { exists (h y). apply pathsweq1', pathsinv0. apply e. }
  exact (iscontr_move_point p (weqproperty f y)).

Lemma remakeweqinv_eq {X Y : UU} (f:X≃Y) (h:Y->X) (e:invmap f ~ h) : pr1weq (remakeweqinv e) = pr1weq f.
Show proof.
  intros. apply idpath.

Lemma remakeweqinv_eq' {X Y : UU} (f:X≃Y) (h:Y->X) (e:invmap f ~ h) : invmap (remakeweqinv e) = h.
Show proof.
  intros. apply idpath.

Corollary remakeweqboth {X Y : UU} {f:X≃Y} {g:X->Y} {h:Y->X} : f ~ g -> invmap f ~ h -> X≃Y.
Show proof.
  intros r s.
  use (remakeweqinv (f := remakeweq r) s).

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.
Show proof.
  intros. apply idpath.

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.
Show proof.
  intros. apply idpath.

Corollary isweqhomot_iff {X Y : UU} (f1 f2 : X -> Y)
          (h : f1 ~ f2) : isweq f1 <-> isweq f2.
Show proof.
  intros. split.
  - apply isweqhomot; assumption.
  - apply isweqhomot, invhomot; assumption.

Lemma isweq_to_isweq_unit {X:UU} (f g:X->unit) : isweq f -> isweq g.
Show proof.
  intros i.
  assert (h : f ~ g).
  { intros t. apply isProofIrrelevantUnit. }
  exact (isweqhomot f g h i).

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

This is kept to preserve compatibility with publications that use the name "gradth" for the "grad theorem".
#[deprecated(note="Use isweq_iso instead.")]
Notation gradth := isweq_iso (only parsing).

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.

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

Some weak equivalences



Corollary isweqinvmap {X Y : UU} (w : X ≃ Y) : isweq (invmap w).
Show 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).

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.
Show proof.
  intros. apply idpath.

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

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

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.
Show proof.
  intros.
  exists (λ 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.

The standard weak equivalence from unit to a contractible type

Definition wequnittocontr {X : UU} (is : iscontr X) : unit ≃ X.
Show 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).

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').
Show proof.
  intros.
  apply (isweq_iso (@maponpaths _ _ w x x')
                (@invmaponpathsweq _ _ w x x')
                (@pathsweq3 _ _ w x x')
                (@pathsweq4 _ _ w x x')).

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).
Show proof.
  intros. intros p. use tpair.
  - exists (!p). apply pathsinv0inv0.
  - cbn. intros [q k]. induction q,k. reflexivity.

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

Weak equivalences to and from coconuses and total path spaces

Corollary isweqtococonusf {X Y : UU} (f : X -> Y) : isweq (tococonusf f).
Show proof.
  intros.
  apply (isweq_iso _ _ (homotfromtococonusf f) (homottofromcoconusf f)).

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).
Show proof.
  intros.
  apply (isweq_iso _ _ (homottofromcoconusf f) (homotfromtococonusf f)).

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

Corollary isweqdeltap (T : UU) : isweq (deltap T).
Show 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).

Corollary isweqpr1pr1 (T : UU) :
  isweq (λ (a : pathsspace' T), pr1 (pr1 a)).
Show 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).

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

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

Theorem twooutof3b {X Y Z : UU} (f : X -> Y) (g : Y -> Z)
        (isf : isweq f) (isgf : isweq (g ∘ f)) : isweq g.
Show 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).

Lemma isweql3 {X Y : UU} (f : X -> Y) (g : Y -> X)
      (egf : ∏ x : X, g (f x) = x) : isweq f -> isweq g.
Show 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).

Theorem twooutof3c {X Y Z : UU} (f : X -> Y) (g : Y -> Z)
        (isf : isweq f) (isg : isweq g) : isweq (g ∘ f).
Show 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).

Corollary twooutof3c_iff_2 {X Y Z : UU} (f : X -> Y) (g : Y -> Z) :
  isweq f -> (isweq g <-> isweq (g ∘ f)).
Show proof.
  intros i. split.
  - intro j. exact (twooutof3c f g i j).
  - intro j. exact (twooutof3b f g i j).

Corollary twooutof3c_iff_1 {X Y Z : UU} (f : X -> Y) (g : Y -> Z) :
  isweq g -> (isweq f <-> isweq (g ∘ f)).
Show proof.
  intros i. split.
  - intro j. exact (twooutof3c f g j i).
  - intro j. exact (twooutof3a f g j i).

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).
Show proof.
  intros r i.
  apply (logeq_trans (Y := isweq (g ∘ f))).
  - apply twooutof3c_iff_1; assumption.
  - apply isweqhomot_iff; assumption.

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).
Show proof.
  intros r i.
  apply (logeq_trans (Y := isweq (g ∘ f))).
  - apply twooutof3c_iff_2; assumption.
  - apply isweqhomot_iff; assumption.

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.
Show proof.
  intros.
  set (py := λ (y : Y), tt).
  apply (twooutof3a f py (isweqcontrtounit isx) (isweqcontrtounit isy)).

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).
Show proof.
  intros. apply idpath.

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

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

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

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.
Show proof.
  intros. exact (twooutof3b _ _ (twooutofsixu isuv isvw) isuv).

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.
Show proof.
  intros. exact (twooutof3b _ _ (twooutofsixv isuv isvw) isvw).

Pairwise direct products of weak equivalences


Theorem isweqdirprodf {X Y X' Y' : UU} (w : X ≃ Y) (w' : X' ≃ Y') :
  isweq (dirprodf w w').
Show 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).

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

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).
Show proof.
  intros xpq.
  exists (pr1 (pr1 xpq)).
  exists (pr2 (pr1 xpq)).
  exact (pr2 xpq).

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

Theorem weqtotal2asstor {X : UU} (P : X -> UU) (Q : total2 P -> UU) :
  total2 Q ≃ ∑ x : X, ∑ p : P x, Q (tpair P x p).
Show 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).

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).
Show proof.
  intros. apply weqtotal2asstor.

Definition weqdirprodasstol (X Y Z : UU) :