Library UniMath.Foundations.PartA
Univalent Foundations, Part A
Contents
- Preamble
- Settings
- Imports
- Some standard constructions not using identity types (paths)
- 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
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 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 iteration {T : UU} (f : T → T) (n : nat) : T → T.
Proof.
induction n as [ | n IHn ].
+ exact (idfun T).
+ exact (f ∘ IHn).
Defined.
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).
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.
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.
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
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.
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.
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
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.
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).
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
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
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.
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
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.
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.
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.
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'.
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.
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
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.
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.
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)
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.
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.
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.
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
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.
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.
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.
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.
(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.
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
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.
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).
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.
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.
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').
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).
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
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).
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)) =