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)) = a).
{ intro a.
induction a as [ xp | yp ].
induction xp as [ x p ].
simpl.
apply idpath.
induction yp as [ y p ].
apply idpath. }
apply (isweq_iso _ _ egf efg).
Defined.
Definition sumofmaps {X Y Z : UU} (fx : X → Z)(fy : Y → Z) :
(X ⨿ Y) → Z := λ xy : _, match xy with ii1 x ⇒ fx x | ii2 y ⇒ fy y end.
Definition coprodasstor (X Y Z : UU) : (X ⨿ Y) ⨿ Z → X ⨿ (Y ⨿ Z).
Proof.
intros X0.
induction X0 as [ c | z ]. induction c as [ x | y ].
apply (ii1 x). apply (ii2 (ii1 y)). apply (ii2 (ii2 z)).
Defined.
Definition coprodasstol (X Y Z : UU): X ⨿ (Y ⨿ Z) → (X ⨿ Y) ⨿ Z.
Proof.
intros X0.
induction X0 as [ x | c ]. apply (ii1 (ii1 x)). induction c as [ y | z ].
apply (ii1 (ii2 y)). apply (ii2 z).
Defined.
Definition sumofmaps_assoc_left {X Y Z T : UU} (f : X → T) (g : Y → T)
(h : Z → T) :
sumofmaps (sumofmaps f g) h ∘ coprodasstol _ _ _ ¬ sumofmaps f (sumofmaps g h).
Proof.
intros. intros [x|[y|z]]; apply idpath.
Defined.
Definition sumofmaps_assoc_right {X Y Z T : UU} (f : X → T) (g : Y → T)
(h : Z → T) :
sumofmaps f (sumofmaps g h) ∘ coprodasstor _ _ _ ¬ sumofmaps (sumofmaps f g) h.
Proof.
intros. intros [[x|y]|z]; apply idpath.
Defined.
Theorem isweqcoprodasstor (X Y Z : UU): isweq (coprodasstor X Y Z).
Proof.
intros. set (f := coprodasstor X Y Z). set (g := coprodasstol X Y Z).
assert (egf : ∏ xyz, (g (f xyz)) = xyz).
intro xyz. induction xyz as [ c | z ]. induction c.
apply idpath. apply idpath. apply idpath.
assert (efg : ∏ xyz, (f (g xyz)) = xyz). intro xyz.
induction xyz as [ x | c ]. apply idpath. induction c.
apply idpath. apply idpath.
apply (isweq_iso f g egf efg).
Defined.
Definition weqcoprodasstor (X Y Z : UU) := make_weq _ (isweqcoprodasstor X Y Z).
Corollary isweqcoprodasstol (X Y Z : UU) : isweq (coprodasstol X Y Z).
Proof.
intros. apply (isweqinvmap (weqcoprodasstor X Y Z)).
Defined.
Definition weqcoprodasstol (X Y Z : UU) := make_weq _ (isweqcoprodasstol X Y Z).
Definition coprodcomm (X Y : UU) : X ⨿ Y → Y ⨿ X
:= λ xy : _, match xy with ii1 x ⇒ ii2 x | ii2 y ⇒ ii1 y end.
Theorem isweqcoprodcomm (X Y : UU) : isweq (coprodcomm X Y).
Proof.
intros.
set (f := coprodcomm X Y). set (g := coprodcomm Y X).
assert (egf : ∏ xy : _, (g (f xy)) = xy). intro.
induction xy. apply idpath. apply idpath.
assert (efg : ∏ yx : _, (f (g yx)) = yx). intro.
induction yx. apply idpath. apply idpath.
apply (isweq_iso f g egf efg).
Defined.
Definition weqcoprodcomm (X Y : UU) := make_weq _ (isweqcoprodcomm X Y).
Theorem isweqii1withneg (X : UU) {Y : UU} (nf : Y → empty) : isweq (@ii1 X Y).
Proof.
intros.
set (f := @ii1 X Y).
set (g := λ xy : X ⨿ Y, match xy with
| ii1 x ⇒ x
| ii2 y ⇒ fromempty (nf y)
end).
assert (egf : ∏ x : X, (g (f x)) = x). intro. apply idpath.
assert (efg : ∏ xy : X ⨿ Y, (f (g xy)) = xy). intro.
induction xy as [ x | y ]. apply idpath. apply (fromempty (nf y)).
apply (isweq_iso f g egf efg).
Defined.
Definition weqii1withneg (X : UU) {Y : UU} (nf : ¬ Y)
:= make_weq _ (isweqii1withneg X nf).
Theorem isweqii2withneg {X : UU} (Y : UU) (nf : X → empty) : isweq (@ii2 X Y).
Proof.
intros.
set (f:= @ii2 X Y).
set (g:= λ xy : X ⨿ Y, match xy with
| ii1 x ⇒ fromempty (nf x)
| ii2 y ⇒ y
end).
assert (egf : ∏ y : Y, (g (f y)) = y). intro. apply idpath.
assert (efg : ∏ xy : X ⨿ Y, (f (g xy)) = xy). intro.
induction xy as [ x | y ]. apply (fromempty (nf x)). apply idpath.
apply (isweq_iso f g egf efg).
Defined.
Definition weqii2withneg {X : UU} (Y : UU) (nf : ¬ X)
:= make_weq _ (isweqii2withneg Y nf).
Definition coprodf {X Y X' Y' : UU} (f : X → X') (g : Y→ Y') : X ⨿ Y → X' ⨿ Y'
:= λ xy: X ⨿ Y,
match xy with
| ii1 x ⇒ ii1 (f x)
| ii2 y ⇒ ii2 (g y)
end.
Definition coprodf1 {X Y X' : UU} : (X → X') → X ⨿ Y → X' ⨿ Y.
Proof.
intros f. exact (coprodf f (idfun Y)).
Defined.
Definition coprodf2 {X Y Y' : UU} : (Y → Y') → X ⨿ Y → X ⨿ Y'.
Proof.
intros g. exact (coprodf (idfun X) g).
Defined.
Definition homotcoprodfcomp {X X' Y Y' Z Z' : UU} (f : X → Y)
(f' : X' → Y') (g : Y → Z) (g' : Y' → Z') :
homot (funcomp (coprodf f f') (coprodf g g'))
(coprodf (funcomp f g) (funcomp f' g')).
Proof.
intros. intro xx'. induction xx' as [ x | x' ].
apply idpath. apply idpath.
Defined.
Definition homotcoprodfhomot {X X' Y Y' : UU} (f g : X → Y)
(f' g' : X' → Y') (h : homot f g) (h' : homot f' g') :
homot (coprodf f f') (coprodf g g')
:= λ xx' : _, match xx' with
| ii1 x ⇒ maponpaths (@ii1 _ _) (h x)
| ii2 x' ⇒ maponpaths (@ii2 _ _) (h' x')
end.
Theorem isweqcoprodf {X Y X' Y' : UU} (w : X ≃ X') (w' : Y ≃ Y') :
isweq (coprodf w w').
Proof.
intros.
set (finv := invmap w). set (ginv := invmap w').
set (ff := coprodf w w'). set (gg := coprodf finv ginv).
assert (egf : ∏ xy : X ⨿ Y, (gg (ff xy)) = xy).
intro. induction xy as [ x | y ]. simpl.
apply (maponpaths (@ii1 X Y) (homotinvweqweq w x)).
apply (maponpaths (@ii2 X Y) (homotinvweqweq w' y)).
assert (efg : ∏ xy' : coprod X' Y', (ff (gg xy')) = xy').
intro. induction xy' as [ x | y ]. simpl.
apply (maponpaths (@ii1 X' Y') (homotweqinvweq w x)).
apply (maponpaths (@ii2 X' Y') (homotweqinvweq w' y)).
apply (isweq_iso ff gg egf efg).
Defined.
Definition weqcoprodf {X Y X' Y' : UU} : X ≃ X' → Y ≃ Y' → X ⨿ Y ≃ X' ⨿ Y'.
Proof.
intros w1 w2. exact (make_weq _ (isweqcoprodf w1 w2)).
Defined.
Definition weqcoprodf1 {X Y X' : UU} : X ≃ X' → X ⨿ Y ≃ X' ⨿ Y.
Proof.
intros w. exact (weqcoprodf w (idweq Y)).
Defined.
Definition weqcoprodf2 {X Y Y' : UU} : Y ≃ Y' → X ⨿ Y ≃ X ⨿ Y'.
Proof.
intros w. exact (weqcoprodf (idweq X) w).
Defined.
The equality_cases construction and four applications to ii1 and ii2
Definition equality_cases {P Q : UU} (x x' : P ⨿ Q) : UU.
Proof.
intros. induction x as [p|q].
- induction x' as [p'|q'].
+ exact (p = p').
+ exact empty.
- induction x' as [p'|q'].
+ exact empty.
+ exact (q = q').
Defined.
Definition equality_by_case {P Q : UU} {x x' : P ⨿ Q} :
x = x'→ equality_cases x x'.
Proof.
intros e. induction x as [p|q].
- induction x' as [p'|q'].
+ simpl.
exact (maponpaths (@coprod_rect P Q (λ _, P) (λ p, p) (λ _, p)) e).
+ simpl.
exact (transportf (@coprod_rect P Q (λ _, UU) (λ _, unit) (λ _, empty))
e tt).
- induction x' as [p'|q'].
+ simpl.
exact (transportb (@coprod_rect P Q (λ _, UU) (λ _, unit) (λ _, empty))
e tt).
+ simpl.
exact (maponpaths (@coprod_rect P Q (λ _,Q) (λ _, q) (λ q, q)) e).
Defined.
Definition inv_equality_by_case {P Q : UU} {x x' : P ⨿ Q} :
equality_cases x x' → x = x'.
Proof.
intros e.
induction x as [p|q].
- induction x' as [p'|q'].
+ exact (maponpaths (@ii1 P Q) e).
+ induction e.
- induction x' as [p'|q'].
+ induction e.
+ exact (maponpaths (@ii2 P Q) e).
Defined.
Lemma ii1_injectivity {P Q : UU} (p p' : P) :
ii1 (B := Q) p = ii1 (B := Q) p' → p = p'.
Proof.
exact equality_by_case.
Defined.
Lemma ii2_injectivity {P Q : UU} (q q' : Q) :
ii2 (A := P) q = ii2 (A := P) q' → q = q'.
Proof.
exact equality_by_case.
Defined.
Lemma negpathsii1ii2 {X Y : UU} (x : X) (y : Y) : ii1 x != ii2 y.
Proof.
exact equality_by_case.
Defined.
Lemma negpathsii2ii1 {X Y : UU} (x : X) (y : Y) : ii2 y != ii1 x.
Proof.
exact equality_by_case.
Defined.
Definition boolascoprod: unit ⨿ unit ≃ bool.
Proof.
set (f := λ xx : coprod unit unit,
match xx with ii1 t ⇒ true | ii2 t ⇒ false end).
split with f.
set (g := λ t:bool, match t with true ⇒ ii1 tt | false ⇒ ii2 tt end).
assert (egf : ∏ xx : _, g (f xx) = xx).
intro xx. induction xx as [ u | u ]. induction u. apply idpath.
induction u. apply idpath.
assert (efg : ∏ t : _, f (g t) = t). induction t. apply idpath.
apply idpath.
apply (isweq_iso f g egf efg).
Defined.
Pairwise coproducts as dependent sums of families over bool
Definition coprodtobool {X Y : UU} (xy : X ⨿ Y) : bool
:= match xy with
| ii1 x ⇒ true
| ii2 y ⇒ false
end.
Definition boolsumfun (X Y : UU) : bool → UU
:= λ t : _, match t with
| true ⇒ X
| false ⇒ Y
end.
Definition coprodtoboolsum (X Y : UU) : X ⨿ Y → total2 (boolsumfun X Y)
:= λ xy : _, match xy with
| ii1 x ⇒ tpair (boolsumfun X Y) true x
| ii2 y ⇒ tpair (boolsumfun X Y) false y
end.
Definition boolsumtocoprod (X Y : UU): (total2 (boolsumfun X Y)) → X ⨿ Y
:= λ xy, match xy with
| tpair _ true x ⇒ ii1 x
| tpair _ false y ⇒ ii2 y
end.
Theorem isweqcoprodtoboolsum (X Y : UU) : isweq (coprodtoboolsum X Y).
Proof.
intros.
set (f := coprodtoboolsum X Y). set (g := boolsumtocoprod X Y).
assert (egf : ∏ xy : X ⨿ Y , (g (f xy)) = xy).
induction xy. apply idpath. apply idpath.
assert (efg : ∏ xy : total2 (boolsumfun X Y), (f (g xy)) = xy).
intro. induction xy as [ t x ]. induction t. apply idpath. apply idpath.
apply (isweq_iso f g egf efg).
Defined.
Definition weqcoprodtoboolsum (X Y : UU) := make_weq _ (isweqcoprodtoboolsum X Y).
Corollary isweqboolsumtocoprod (X Y : UU): isweq (boolsumtocoprod X Y).
Proof.
intros. apply (isweqinvmap (weqcoprodtoboolsum X Y)).
Defined.
Definition weqboolsumtocoprod (X Y : UU) := make_weq _ (isweqboolsumtocoprod X Y).
Definition weqcoprodsplit {X Y Z : UU} (f : X → coprod Y Z) :
X ≃ (∑ y : Y, hfiber f (ii1 y)) ⨿ (∑ z : Z, hfiber f (ii2 z)).
Proof.
intros.
set (w1 := weqtococonusf f).
set (w2 := weqtotal2overcoprod (λ yz : coprod Y Z, hfiber f yz)).
apply (weqcomp w1 w2).
Defined.
Some properties of bool
Definition boolchoice (x : bool) : (x = true) ⨿ (x = false).
Proof.
induction x. apply (ii1 (idpath _)). apply (ii2 (idpath _)).
Defined.
Definition bool_to_type : bool → UU.
Proof.
intros b. induction b as [|]. { exact unit. } { exact empty. }
Defined.
Theorem nopathstruetofalse : true = false → empty.
Proof.
intro X. apply (transportf bool_to_type X tt).
Defined.
Corollary nopathsfalsetotrue : false = true → empty.
Proof.
intro X. apply (transportb bool_to_type X tt).
Defined.
Definition truetonegfalse (x : bool) : x = true → x != false.
Proof.
intros e. rewrite e. unfold neg. apply nopathstruetofalse.
Defined.
Definition falsetonegtrue (x : bool) : x = false → x != true.
Proof.
intros e. rewrite e. unfold neg. apply nopathsfalsetotrue.
Defined.
Definition negtruetofalse (x : bool) : x != true → x = false.
Proof.
intros ne. induction (boolchoice x) as [t | f]. induction (ne t). apply f.
Defined.
Definition negfalsetotrue (x : bool) : x != false → x = true.
Proof.
intros ne. induction (boolchoice x) as [t | f]. apply t. induction (ne f).
Defined.
Fibrations with only one non-empty fiber
Theorem onefiber {X : UU} (P : X → UU) (x : X)
(c : ∏ x' : X, (x = x') ⨿ ¬ P x') : isweq (λ p, tpair P x p).
Proof.
intros.
set (f := λ p : P x, tpair _ x p).
set (cx := c x).
transparent assert (cnew : (∏ x' : X, (x = x') ⨿ ¬ P x')).
{ intro x'. refine (coprod_rect (λ _, _) _ _ (cx)).
- intro x0. refine (coprod_rect (λ _, _) _ _ (c x')).
+ intro ee. apply ii1; exact (pathscomp0 (pathsinv0 x0) ee).
+ intro phi. apply ii2, phi.
- intro phi. exact (c x'). }
set (g := λ pp : total2 P,
match (cnew (pr1 pp)) with
| ii1 e ⇒ transportb P e (pr2 pp)
| ii2 phi ⇒ fromempty (phi (pr2 pp))
end).
assert (efg : ∏ pp : total2 P, (f (g pp)) = pp).
intro. induction pp as [ t x0 ]. set (cnewt := cnew t).
unfold g. unfold f. simpl. change (cnew t) with cnewt.
induction cnewt as [ x1 | y ].
apply (pathsinv0 (pr1 (pr2 (constr1 P (pathsinv0 x1))) x0)).
induction (y x0).
set (cnewx := cnew x).
assert (e1 : (cnew x) = cnewx). apply idpath.
unfold cnew in cnewx. change (c x) with cx in cnewx.
induction cx as [ x0 | e0 ].
assert (e : (cnewx) = (ii1 (idpath x))).
apply (maponpaths (@ii1 (x = x) (P x → empty)) (pathsinv0l x0)).
assert (egf : ∏ p: P x, (g (f p)) = p). intro. simpl in g.
unfold g. unfold f. simpl.
set (ff := λ cc:(x = x) ⨿ (P x → empty),
match cc with
| ii1 e0 ⇒ transportb P e0 p
| ii2 phi ⇒ fromempty (phi p)
end).
assert (ee : (ff (cnewx)) = (ff (@ii1 (x = x) (P x → empty) (idpath x)))).
apply (maponpaths ff e).
assert (eee : (ff (@ii1 (x = x) (P x → empty) (idpath x))) = p). apply idpath.
fold (ff (cnew x)).
assert (e2 : (ff (cnew x)) = (ff cnewx)). apply (maponpaths ff e1).
apply (pathscomp0 (pathscomp0 e2 ee) eee).
apply (isweq_iso f g egf efg).
unfold isweq. intro y0. induction (e0 (g y0)).
Defined.
Basics about fibration sequences.
Fibrations sequences and their first "left shifts"
The structures of a complex and of a fibration sequence on a composable pair of functions
The structure of a fibration sequence on a complex.
Definition ezmap {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ez : complxstr f g z) :
X → hfiber g z := λ x : X, make_hfiber g (f x) (ez x).
Definition isfibseq {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ez : complxstr f g z) := isweq (ezmap f g z ez).
Definition fibseqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
:= ∑ ez : complxstr f g z, isfibseq f g z ez.
Definition make_fibseqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
:= tpair (λ ez : complxstr f g z, isfibseq f g z ez).
Definition fibseqstrtocomplxstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z) :
fibseqstr f g z → complxstr f g z
:= @pr1 _ (λ ez : complxstr f g z, isfibseq f g z ez).
Coercion fibseqstrtocomplxstr : fibseqstr >-> complxstr.
Definition ezweq {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(fs : fibseqstr f g z) : X ≃ hfiber g z
:= make_weq _ (pr2 fs).
Definition d1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(fs : fibseqstr f g z) (y : Y) : (g y) = z → X
:= λ e : _, invmap (ezweq f g z fs) (make_hfiber g y e).
Definition ezmap1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(fs : fibseqstr f g z) (y : Y) (e : (g y) = z) : hfiber f y.
Proof.
intros.
split with (d1 f g z fs y e).
unfold d1.
change (f (invmap (ezweq f g z fs) (make_hfiber g y e)))
with (hfiberpr1 _ _ (ezweq f g z fs (invmap (ezweq f g z fs)
(make_hfiber g y e)))).
apply (maponpaths (hfiberpr1 g z)
(homotweqinvweq (ezweq f g z fs) (make_hfiber g y e))).
Defined.
Definition invezmap1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ez : complxstr f g z) (y : Y) : hfiber f y → (g y) = z
:= λ xe: hfiber f y,
match xe with
tpair _ x e ⇒ pathscomp0 (maponpaths g (pathsinv0 e)) (ez x)
end.
Theorem isweqezmap1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(fs : fibseqstr f g z) (y : Y) : isweq (ezmap1 f g z fs y).
Proof.
intros.
set (ff := ezmap1 f g z fs y). set (gg := invezmap1 f g z (pr1 fs) y).
assert (egf : ∏ e : _, (gg (ff e)) = e).
intro. simpl.
apply (hfibertriangle1inv0 g (homotweqinvweq (ezweq f g z fs)
(make_hfiber g y e))).
assert (efg : ∏ xe : _, (ff (gg xe)) = xe).
intro. induction xe as [ x e ]. induction e. simpl.
unfold ff. unfold ezmap1. unfold d1.
change (make_hfiber g (f x) (pr1 fs x)) with (ezmap f g z fs x).
apply (hfibertriangle2
f (make_hfiber f (invmap (ezweq f g z fs) (ezmap f g z fs x)) _)
(make_hfiber f x (idpath _))
(homotinvweqweq (ezweq f g z fs) x)).
simpl.
set (e1 := pathsinv0 (pathscomp0rid (maponpaths f (homotinvweqweq
(ezweq f g z fs) x)))).
assert (e2 : (maponpaths (hfiberpr1 g z)
(homotweqinvweq (ezweq f g z fs)
((ezmap f g z fs) x)))
= (maponpaths f (homotinvweqweq (ezweq f g z fs) x))).
set (e3 := maponpaths (λ e : _, maponpaths (hfiberpr1 g z) e)
(pathsinv0 (homotweqinvweqweq (ezweq f g z fs) x))).
simpl in e3.
set (e4 := maponpathscomp (ezmap f g z (pr1 fs)) (hfiberpr1 g z)
(homotinvweqweq (ezweq f g z fs) x)).
simpl in e4. apply (pathscomp0 e3 e4). apply (pathscomp0 e2 e1).
apply (isweq_iso _ _ egf efg).
Defined.
Definition ezweq1 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(fs : fibseqstr f g z) (y : Y) := make_weq _ (isweqezmap1 f g z fs y).
Definition fibseq1 {X Y Z : UU} (f :X → Y) (g : Y → Z) (z : Z)
(fs : fibseqstr f g z) (y : Y) : fibseqstr (d1 f g z fs y) f y
:= make_fibseqstr _ _ _ _ (isweqezmap1 f g z fs y).
Definition d2 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(fs : fibseqstr f g z) (y : Y) (x : X) (e : (f x) = y) :
(g y) = z := pathscomp0 (maponpaths g (pathsinv0 e)) ((pr1 fs) x).
Definition ezweq2 {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(fs : fibseqstr f g z) (y : Y) (x : X) :
f x = y ≃ hfiber (d1 f g z fs y) x
:= ezweq1 (d1 f g z fs y) f y (fibseq1 f g z fs y) x.
Definition fibseq2 {X Y Z : UU} (f : X → Y) (g : Y→Z) (z : Z)
(fs : fibseqstr f g z) (y : Y) (x : X) :
fibseqstr (d2 f g z fs y x) (d1 f g z fs y) x
:= make_fibseqstr _ _ _ _
(isweqezmap1 (d1 f g z fs y) f y (fibseq1 f g z fs y) x).
Fibration sequences based on tpair P z and pr1 : total2 P → Z ( the "pr1-case" )
Definition ezmappr1 {Z : UU} (P : Z → UU) (z : Z) :
P z → hfiber (@pr1 Z P) z
:= λ p : P z, tpair _ (tpair _ z p) (idpath z).
Definition invezmappr1 {Z : UU} (P : Z → UU) (z : Z) :
hfiber (@pr1 Z P) z → P z
:= λ te, transportf P (pr2 te) (pr2 (pr1 te)).
Definition isweqezmappr1 {Z : UU} (P : Z → UU) (z : Z) :
isweq (ezmappr1 P z).
Proof.
intros.
assert (egf : ∏ x: P z , (invezmappr1 _ z ((ezmappr1 P z) x)) = x).
intro. unfold ezmappr1. unfold invezmappr1. simpl. apply idpath.
assert (efg : ∏ x: hfiber (@pr1 Z P) z ,
(ezmappr1 _ z (invezmappr1 P z x)) = x).
intros. induction x as [ x t0 ]. induction t0. simpl in x. simpl.
induction x. simpl. unfold transportf. unfold ezmappr1. apply idpath.
apply (isweq_iso _ _ egf efg).
Defined.
Definition ezweqpr1 {Z : UU} (P : Z → UU) (z : Z)
:= make_weq _ (isweqezmappr1 P z).
Lemma isfibseqpr1 {Z : UU} (P : Z → UU) (z : Z) :
isfibseq (λ p : P z, tpair _ z p) (@pr1 Z P) z (λ p : P z, idpath z).
Proof.
intros. unfold isfibseq. unfold ezmap. apply isweqezmappr1.
Defined.
Definition fibseqpr1 {Z : UU} (P : Z → UU) (z : Z) :
fibseqstr (λ p : P z, tpair _ z p) (@pr1 Z P) z
:= make_fibseqstr _ _ _ _ (isfibseqpr1 P z).
The main weak equivalence defined by the first derived of fibseqpr1 .
Definition ezweq1pr1 {Z : UU} (P : Z → UU) (z : Z) (zp : total2 P) :
pr1 zp = z ≃ hfiber (tpair P z) zp
:= ezweq1 _ _ z (fibseqpr1 P z) zp.
Theorem isfibseqg {Y Z : UU} (g : Y → Z) (z : Z) :
isfibseq (hfiberpr1 g z) g z (λ ye: _, pr2 ye).
Proof.
intros.
simple refine (isweqhomot _ _ _ (idisweq _)).
- intro. apply idpath.
Defined.
Definition ezweqg {Y Z : UU} (g : Y → Z) (z : Z) := make_weq _ (isfibseqg g z).
Definition fibseqg {Y Z : UU} (g : Y → Z) (z : Z)
: fibseqstr (hfiberpr1 g z) g z := make_fibseqstr _ _ _ _ (isfibseqg g z).
The first derived of fibseqg .
note that d1g coincides with d1 _ _ _ (fibseqg g z) which makes
the following two definitions possible.
Definition ezweq1g {Y Z : UU} (g : Y → Z) (z : Z) (y : Y) :
g y = z ≃ hfiber (hfiberpr1 g z) y
:= make_weq _ (isweqezmap1 (hfiberpr1 g z) g z (fibseqg g z) y).
Definition fibseq1g {Y Z : UU} (g : Y → Z) (z : Z) (y : Y) :
fibseqstr (d1g g z y) (hfiberpr1 g z) y
:= make_fibseqstr _ _ _ _ (isweqezmap1 (hfiberpr1 g z) g z (fibseqg g z) y).
The second derived of fibseqg .
Definition d2g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
(e: (pr1 ye') = y) : (g y) = z
:= pathscomp0 (maponpaths g (pathsinv0 e)) (pr2 ye').
note that d2g coincides with d2 _ _ _ (fibseqg g z) which makes
the following two definitions possible.
Definition ezweq2g
{Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z) :
(pr1 ye') = y ≃ hfiber (make_hfiber g y) ye'
:= ezweq2 _ _ _ (fibseqg g z) _ _.
Definition fibseq2g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z) :
fibseqstr (d2g g y ye') (make_hfiber g y) ye'
:= fibseq2 _ _ _ (fibseqg g z) _ _.
The third derived of fibseqg and an explicit description of the
corresponding first map.
Definition d3g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
(e : (g y) = z) : (make_hfiber g y e) = ye' → (pr1 ye') = y
:= d2 (d1g g z y) (hfiberpr1 g z) y (fibseq1g g z y) ye' e.
Lemma homotd3g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
(e : (g y) = z) (ee : (make_hfiber g y e) = ye') :
(d3g g y ye' e ee) = (maponpaths (@pr1 _ _) (pathsinv0 ee)).
Proof.
intros. unfold d3g. unfold d2. simpl. apply pathscomp0rid.
Defined.
Definition ezweq3g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
(e : (g y) = z)
:= ezweq2 (d1g g z y) (hfiberpr1 g z) y (fibseq1g g z y) ye' e.
Definition fibseq3g {Y Z : UU} (g : Y → Z) {z : Z} (y : Y) (ye' : hfiber g z)
(e : (g y) = z)
:= fibseq2 (d1g g z y) (hfiberpr1 g z) y (fibseq1g g z y) ye' e.
Fibration sequence of h-fibers defined by a composable pair of functions (the "hf-case")
Definition hfibersftogf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ye : hfiber g z) (xe : hfiber f (pr1 ye)) : hfiber (funcomp f g) z.
Proof.
intros.
split with (pr1 xe).
apply (pathscomp0 (maponpaths g (pr2 xe)) (pr2 ye)).
Defined.
Definition ezmaphf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ye : hfiber g z) (xe : hfiber f (pr1 ye)) :
hfiber (hfibersgftog f g z) ye.
Proof.
intros.
split with (hfibersftogf f g z ye xe). simpl.
apply (hfibertriangle2
g (make_hfiber g (f (pr1 xe)) (pathscomp0 (maponpaths g (pr2 xe))
(pr2 ye))) ye (pr2 xe)).
simpl. apply idpath.
Defined.
Definition invezmaphf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) :
hfiber f (pr1 ye).
Proof.
intros.
split with (pr1 (pr1 xee')).
apply (maponpaths (hfiberpr1 _ _) (pr2 xee')).
Defined.
Definition ffgg {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) :
hfiber (hfibersgftog f g z) ye.
Proof.
intros.
induction ye as [ y e ]. induction e. unfold hfibersgftog.
unfold hfibersgftog in xee'.
induction xee' as [ xe e' ]. induction xe as [ x e ].
set (e'' := (maponpaths g (maponpaths (hfiberpr1 g (g y)) e'))).
simpl in e'.
split with (make_hfiber (funcomp f g) x (pathscomp0 e'' (idpath (g y)))).
simpl.
apply (hfibertriangle2 _ (make_hfiber g (f x) (pathscomp0 e'' (idpath (g y))))
(make_hfiber g y (idpath _))
(maponpaths (hfiberpr1 _ _) e') (idpath _)).
Defined.
Definition homotffggid {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ye : hfiber g z) (xee' : hfiber (hfibersgftog f g z) ye) :
(ffgg f g z ye xee') = xee'.
Proof.
intros.
induction ye as [ y e ]. induction e.
induction xee' as [ xe e' ]. induction e'.
induction xe as [ x e ]. induction e.
simpl. apply idpath.
Defined.
Theorem isweqezmaphf {X Y Z : UU} (f : X → Y) (g : Y → Z)
(z : Z) (ye : hfiber g z) : isweq (ezmaphf f g z ye).
Proof.
intros.
set (ff := ezmaphf f g z ye). set (gg := invezmaphf f g z ye).
assert (egf : ∏ xe : _ , (gg (ff xe)) = xe).
induction ye as [ y e ]. induction e. intro xe.
apply (hfibertriangle2 f (gg (ff xe)) xe (idpath (pr1 xe))).
induction xe as [ x ex ]. simpl in ex. induction ex. simpl. apply idpath.
assert (efg : ∏ xee' : _ , (ff (gg xee')) = xee').
induction ye as [ y e ]. induction e. intro xee'.
assert (hint : (ff (gg xee'))
= (ffgg f g (g y) (make_hfiber g y (idpath _)) xee')).
induction xee' as [ xe e' ]. induction xe as [ x e ]. apply idpath.
apply (pathscomp0 hint (homotffggid _ _ _ _ xee')).
apply (isweq_iso _ _ egf efg).
Defined.
Definition ezweqhf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ye : hfiber g z) :
hfiber f (pr1 ye) ≃ hfiber (hfibersgftog f g z) ye
:= make_weq _ (isweqezmaphf f g z ye).
Definition fibseqhf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ye : hfiber g z) :
fibseqstr (hfibersftogf f g z ye) (hfibersgftog f g z) ye
:= make_fibseqstr _ _ _ _ (isweqezmaphf f g z ye).
Definition isweqinvezmaphf {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(ye : hfiber g z) :
isweq (invezmaphf f g z ye) := pr2 (invweq (ezweqhf f g z ye)).
Corollary weqhfibersgwtog {X Y Z : UU} (w : X ≃ Y) (g : Y → Z) (z : Z) :
hfiber (funcomp w g) z ≃ hfiber g z.
Proof.
intros.
split with (hfibersgftog w g z).
intro ye.
apply (iscontrweqf (ezweqhf w g z ye) ((pr2 w) (pr1 ye))).
Defined.
Definition totalfun {X : UU} (P Q : X → UU) (f : ∏ x : X, P x → Q x)
: (∑ y, P y) → (∑ y, Q y)
:= (λ z: total2 P, tpair Q (pr1 z) (f (pr1 z) (pr2 z))).
Theorem isweqtotaltofib {X : UU} (P Q : X → UU) (f : ∏ x : X, P x → Q x):
isweq (totalfun _ _ f) → ∏ x : X, isweq (f x).
Proof.
intros X0 x.
set (totp := total2 P). set (totq := total2 Q).
set (totf := (totalfun _ _ f)).
set (pip := λ z: totp, pr1 z). set (piq:= λ z: totq, pr1 z).
set (hfx := hfibersgftog totf piq x). simpl in hfx.
assert (H : isweq hfx). unfold isweq. intro y.
set (int := invezmaphf totf piq x y).
assert (X1 : isweq int). apply (isweqinvezmaphf totf piq x y).
induction y as [ t e ].
assert (is1 : iscontr (hfiber totf t)).
apply (X0 t). apply (iscontrweqb (make_weq int X1) is1).
set (ip := ezmappr1 P x). set (iq := ezmappr1 Q x).
set (h := λ p: P x, hfx (ip p)).
assert (is2 : isweq h).
apply (twooutof3c ip hfx (isweqezmappr1 P x) H).
set (h':= λ p: P x, iq ((f x) p)).
assert (ee : ∏ p:P x, (h p) = (h' p)). intro. apply idpath.
assert (X2 : isweq h'). apply (isweqhomot h h' ee is2).
apply (twooutof3a (f x) iq X2).
apply (isweqezmappr1 Q x).
Defined.
Definition weqtotaltofib {X : UU} (P Q : X → UU) (f : ∏ x : X , P x → Q x)
(is : isweq (totalfun _ _ f)) (x : X) : P x ≃ Q x
:= make_weq _ (isweqtotaltofib P Q f is x).
Theorem isweqfibtototal {X : UU} (P Q : X → UU) (f : ∏ x : X, P x ≃ Q x) :
isweq (totalfun _ _ f).
Proof.
set (fpq := totalfun P Q f). set (pr1p := λ z : total2 P, pr1 z).
set (pr1q := λ z : total2 Q, pr1 z).
unfold isweq. intro xq.
set (x:= pr1q xq).
set (xqe:= make_hfiber pr1q xq (idpath _)).
set (hfpqx:= hfibersgftog fpq pr1q x).
assert (isint : iscontr (hfiber hfpqx xqe)).
assert (isint1 : isweq hfpqx).
set (ipx := ezmappr1 P x). set (iqx := ezmappr1 Q x).
set (diag := λ p : P x, (iqx ((f x) p))).
assert (is2: isweq diag).
apply (twooutof3c (f x) iqx (pr2 (f x)) (isweqezmappr1 Q x)).
apply (twooutof3b ipx hfpqx (isweqezmappr1 P x) is2).
unfold isweq in isint1. apply (isint1 xqe).
set (intmap := invezmaphf fpq pr1q x xqe).
apply (iscontrweqf (make_weq intmap (isweqinvezmaphf fpq pr1q x xqe)) isint).
Defined.
Theorem isweqfibtototal' {X : UU} (P Q : X → UU) (f : ∏ x : X, P x ≃ Q x) :
isweq (totalfun _ _ f).
Proof.
use isweq_iso.
- use totalfun.
intro x. apply (invmap (f x)).
- intro xp.
use total2_paths_f.
+ apply idpath.
+ apply homotinvweqweq.
- intro xp.
use total2_paths_f.
+ apply idpath.
+ apply homotweqinvweq.
Defined.
Definition weqfibtototal {X : UU} (P Q : X → UU) (f : ∏ x, P x ≃ Q x) :
(∑ x, P x) ≃ (∑ x, Q x) := make_weq _ (isweqfibtototal' P Q f).
Function fpmap between the total spaces from a function between the bases
Definition fpmap {X Y : UU} (f : X → Y) (P : Y → UU) :
(∑ x, P (f x)) → (∑ y, P y) := λ z, tpair P (f (pr1 z)) (pr2 z).
Definition hffpmap2 {X Y : UU} (f : X → Y) (P : Y → UU) :
(∑ x, P (f x)) → ∑ u : total2 P, hfiber f (pr1 u).
Proof.
intros X0.
set (u:= fpmap f P X0).
split with u.
set (x:= pr1 X0).
split with x.
simpl. apply idpath.
Defined.
Lemma centralfiber {X : UU} (P : X → UU) (x : X) :
isweq (λ p : P x, tpair (λ u : coconusfromt X x, P (pr1 u))
(coconusfromtpair X (idpath x)) p).
Proof.
intros.
set (f := λ p: P x, tpair (λ u: coconusfromt X x, P(pr1 u))
(coconusfromtpair X (idpath x)) p).
set (g := λ z: total2 (λ u: coconusfromt X x, P (pr1 u)),
transportf P (pathsinv0 (pr2 (pr1 z))) (pr2 z)).
assert (efg : ∏ z : total2 (λ u : coconusfromt X x, P (pr1 u)),
(f (g z)) = z).
intro.
induction z as [ t x0 ]. induction t as [ t x1 ].
simpl. induction x1. simpl. apply idpath.
assert (egf : ∏ p : P x , (g (f p)) = p). intro. apply idpath.
apply (isweq_iso f g egf efg).
Defined.
Lemma isweqhff {X Y : UU} (f : X → Y) (P : Y → UU) : isweq (hffpmap2 f P).
Proof.
intros.
set (int := total2 (λ x : X, total2 (λ u : coconusfromt Y (f x),
P (pr1 u)))).
set (intpair := tpair (λ x:X, total2 (λ u : coconusfromt Y (f x),
P (pr1 u)))).
set (toint :=
λ z : (total2 (λ u : total2 P, hfiber f (pr1 u))),
intpair (pr1 (pr2 z))
(tpair (fun u: coconusfromt Y (f (pr1 (pr2 z))) ⇒ P (pr1 u))
(coconusfromtpair _ (pr2 (pr2 z))) (pr2 (pr1 z)))).
set (fromint := λ z : int,
tpair (λ u : total2 P, hfiber f (pr1 u))
(tpair P (pr1 (pr1 (pr2 z))) (pr2 (pr2 z)))
(make_hfiber f (pr1 z) (pr2 (pr1 (pr2 z))))).
assert (fromto : ∏ u : (total2 (λ u : total2 P, hfiber f (pr1 u))),
(fromint (toint u)) = u).
simpl in toint. simpl in fromint. simpl.
intro u. induction u as [ t x ]. induction x. induction t as [ p0 p1 ].
simpl. unfold toint. unfold fromint. simpl. apply idpath.
assert (tofrom : ∏ u : int, (toint (fromint u)) = u).
intro. induction u as [ t x ]. induction x as [ t0 x ]. induction t0.
simpl in x. simpl. unfold fromint. unfold toint. simpl. apply idpath.
assert (is : isweq toint). apply (isweq_iso toint fromint fromto tofrom).
clear tofrom. clear fromto. clear fromint.
set (h := λ u : total2 (λ x : X, P (f x)), toint ((hffpmap2 f P) u)).
simpl in h.
assert (l1 : ∏ x : X, isweq (λ p: P (f x),
tpair (λ u : coconusfromt _ (f x), P (pr1 u))
(coconusfromtpair _ (idpath (f x))) p)).
intro. apply (centralfiber P (f x)).
assert (X0 : isweq h).
apply (isweqfibtototal
(λ x : X, P (f x))
(λ x : X, total2 (λ u : coconusfromt _ (f x), P (pr1 u)))
(λ x : X, make_weq _ (l1 x))).
apply (twooutof3a (hffpmap2 f P) toint X0 is).
Defined.
Homotopy fibers of fpmap
Definition hfiberfpmap {X Y : UU} (f : X → Y) (P : Y → UU) (yp : total2 P) :
hfiber (fpmap f P) yp → hfiber f (pr1 yp).
Proof.
intros X0.
set (int1:= hfibersgftog (hffpmap2 f P)
(λ u : (∑ u : total2 P, hfiber f (pr1 u)),
(pr1 u)) yp).
set (phi := invezmappr1 (λ u:total2 P, hfiber f (pr1 u)) yp).
apply (phi (int1 X0)).
Defined.
Theorem isweqhfiberfp {X Y : UU} (f : X → Y) (P : Y → UU) (yp : total2 P) :
isweq (hfiberfpmap f P yp).
Proof.
intros.
set (int1 := hfibersgftog
(hffpmap2 f P)
(λ u : (total2 (λ u : total2 P, hfiber f (pr1 u))), (pr1 u))
yp).
assert (is1 : isweq int1). simpl in int1.
apply (pr2 (weqhfibersgwtog
(make_weq _ (isweqhff f P))
(λ u : total2 (λ u : total2 P, hfiber f (pr1 u)), pr1 u) yp)).
set (phi := invezmappr1 (λ u : total2 P, hfiber f (pr1 u)) yp).
assert (is2 : isweq phi).
apply (pr2 (invweq (ezweqpr1 (λ u : total2 P, hfiber f (pr1 u)) yp))).
apply (twooutof3c int1 phi is1 is2).
Defined.
The fpmap from a weak equivalence is a weak equivalence
Corollary isweqfpmap {X Y : UU} (w : X ≃ Y)(P : Y → UU) : isweq (fpmap w P).
Proof.
intros.
unfold isweq. intro y. set (h := hfiberfpmap w P y).
assert (X1 : isweq h). apply isweqhfiberfp.
assert (is : iscontr (hfiber w (pr1 y))). apply (pr2 w).
apply (iscontrweqb (make_weq h X1) is).
Defined.
Definition weqfp_map {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
(∑ x, P(w x)) → (∑ y, P y).
Proof.
intros xp. exact (w (pr1 xp),,pr2 xp).
Defined.
Definition weqfp_invmap {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
(∑ y, P y) → (∑ x, P(w x)).
Proof.
intros yp.
exact (invmap w (pr1 yp),,
transportf P (! homotweqinvweq w (pr1 yp)) (pr2 yp)).
Defined.
Definition weqfp {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
(∑ x : X, P (w x)) ≃ (∑ y, P y).
Proof.
intros.
∃ (weqfp_map w P).
refine (isweq_iso _ (weqfp_invmap w P) _ _).
{ intros xp. use total2_paths_f.
{ simpl. apply homotinvweqweq. }
simpl. rewrite <- weq_transportf_adjointness.
rewrite transport_f_f. rewrite pathsinv0l.
apply idpath. }
{ intros yp. simple refine (total2_paths_f _ _).
{ simpl. apply homotweqinvweq. }
simpl. rewrite transport_f_f. rewrite pathsinv0l. apply idpath. }
Defined.
Definition weqfp_compute_1 {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
weqfp w P ¬ weqfp_map w P.
Proof.
intros. intros xp. apply idpath.
Defined.
Definition weqfp_compute_2 {X Y : UU} (w : X ≃ Y) (P : Y → UU) :
invmap (weqfp w P) ¬ weqfp_invmap w P.
Proof.
intros. intros yp. apply idpath.
Defined.
Definition weqtotal2overcoprod' {W X Y : UU} (P : W → UU) (f : X ⨿ Y ≃ W) :
(∑ w, P w) ≃ (∑ x : X, P (f (ii1 x))) ⨿ (∑ y : Y, P (f (ii2 y))).
Proof.
intros.
exact (weqcomp (invweq (weqfp f _)) (weqtotal2overcoprod (P ∘ f))).
Defined.
Definition fromtotal2overunit (P : unit → UU) (tp : total2 P) : P tt.
Proof.
intros. induction tp as [ t p ]. induction t. apply p.
Defined.
Definition tototal2overunit (P : unit → UU) (p : P tt) : total2 P
:= tpair P tt p.
Theorem weqtotal2overunit (P : unit → UU) : (∑ u, P u) ≃ P tt.
Proof.
set (f := fromtotal2overunit P). set (g := tototal2overunit P).
split with f.
assert (egf : ∏ a : _ , (g (f a)) = a).
intro a. induction a as [ t p ]. induction t. apply idpath.
assert (efg : ∏ a : _ , (f (g a)) = a).
intro a. apply idpath. apply (isweq_iso _ _ egf efg).
Defined.
Definition bandfmap {X Y : UU} (f : X → Y) (P : X → UU) (Q : Y → UU)
(fm : ∏ x : X, P x → (Q (f x))) :
(∑ x, P x) → (∑ x, Q x) := λ xp, f (pr1 xp) ,, fm (pr1 xp) (pr2 xp).
Theorem isweqbandfmap {X Y : UU} (w : X ≃ Y) (P : X → UU) (Q : Y → UU)
(fw : ∏ x : X, P x ≃ Q (w x)) : isweq (bandfmap _ P Q fw).
Proof.
intros.
set (f1 := totalfun P _ fw).
set (is1 := isweqfibtototal P (λ x:X, Q (w x)) fw).
set (f2:= fpmap w Q).
set (is2:= isweqfpmap w Q).
assert (h: ∏ xp: total2 P, (f2 (f1 xp)) = (bandfmap w P Q fw xp)).
{ intro. apply idpath. }
apply (isweqhomot _ _ h (twooutof3c f1 f2 is1 is2)).
Defined.
Definition weqbandf {X Y : UU} (w : X ≃ Y) (P : X → UU) (Q : Y → UU)
(fw : ∏ x : X, P x ≃ Q (w x))
:= make_weq _ (isweqbandfmap w P Q fw).
Definition commsqstr {X X' Y Z : UU} (g' : Z → X') (f' : X' → Y) (g : Z → X)
(f : X → Y) := ∏ (z : Z), (f' (g' z)) = (f (g z)).
Definition hfibersgtof' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
(g' : Z → X') (h : commsqstr g' f' g f) (x : X) (ze : hfiber g x) :
hfiber f' (f x).
Proof.
intros.
induction ze as [ z e ].
split with (g' z).
apply (pathscomp0 (h z) (maponpaths f e)).
Defined.
Definition hfibersg'tof {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f) (x' : X')
(ze : hfiber g' x') : hfiber f (f' x').
Proof.
intros.
induction ze as [ z e ].
split with (g z).
apply (pathscomp0 (pathsinv0 (h z)) (maponpaths f' e)).
Defined.
Definition transposcommsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') :
commsqstr g' f' g f → commsqstr g f g' f'
:= λ h : _, λ z : Z, (pathsinv0 (h z)).
Lemma complxstrtocommsqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(h : complxstr f g z) :
commsqstr f g (λ x : X, tt) (λ t : unit, z).
Proof.
intros. assumption.
Defined.
Lemma commsqstrtocomplxstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(h : commsqstr f g (λ x : X, tt) (λ t : unit, z)) :
complxstr f g z.
Proof.
intros. assumption.
Defined.
Definition hfp {X X' Y : UU} (f : X → Y) (f' : X' → Y)
:= total2 (λ xx' : X × X', (f' (pr2 xx')) = (f (pr1 xx'))).
Definition hfpg {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
hfp f f' → X := λ xx'e, (pr1 (pr1 xx'e)).
Definition hfpg' {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
hfp f f' → X' := λ xx'e, (pr2 (pr1 xx'e)).
Definition commsqZtohfp {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f) :
Z → hfp f f' := λ z : _, tpair _ (make_dirprod (g z) (g' z)) (h z).
Definition commsqZtohfphomot {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f) :
∏ z : Z, (hfpg _ _ (commsqZtohfp _ _ _ _ h z)) = (g z)
:= λ z : _, idpath _.
Definition commsqZtohfphomot' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f) :
∏ z : Z, (hfpg' _ _ (commsqZtohfp _ _ _ _ h z)) = (g' z)
:= λ z : _, idpath _.
Definition hfpoverX {X X' Y : UU} (f : X → Y) (f' : X' → Y)
:= total2 (λ x : X, hfiber f' (f x)).
Definition hfpoverX' {X X' Y : UU} (f : X → Y) (f' : X' → Y)
:= total2 (λ x' : X', hfiber f (f' x')).
Definition weqhfptohfpoverX {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
hfp f f' ≃ hfpoverX f f'.
Proof.
intros.
exact (weqtotal2asstor _ (λ xx', f' (pr2 xx') = f (pr1 xx'))).
Defined.
Definition weqhfptohfpoverX' {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
hfp f f' ≃ hfpoverX' f f'.
Proof.
intros.
set (w1 := weqfp (weqdirprodcomm X X')
(λ xx' : X' × X , (f' (pr1 xx')) = (f (pr2 xx')))).
simpl in w1.
set (w2 := weqfibtototal
(λ x'x : X' × X, (f' (pr1 x'x)) = (f (pr2 x'x)))
(λ x'x : X' × X, (f (pr2 x'x)) = (f' (pr1 x'x)))
(λ x'x : _, weqpathsinv0 (f' (pr1 x'x)) (f (pr2 x'x)))).
set (w3 := weqtotal2asstor
(λ x' : X', X)
(λ x'x : X' × X, (f (pr2 x'x)) = (f' (pr1 x'x)))).
simpl in w3.
apply (weqcomp (weqcomp w1 w2) w3).
Defined.
Lemma weqhfpcomm {X X' Y : UU} (f : X → Y) (f' : X' → Y):
hfp f f' ≃ hfp f' f.
Proof.
intros.
set (w1 := weqfp (weqdirprodcomm X X')
(λ xx' : X' × X, (f' (pr1 xx')) = (f (pr2 xx')))).
simpl in w1.
set (w2 := weqfibtototal
(λ x'x : X' × X, (f' (pr1 x'x)) = (f (pr2 x'x)))
(λ x'x : X' × X, (f (pr2 x'x)) = (f' (pr1 x'x)))
(λ x'x : _, weqpathsinv0 (f' (pr1 x'x)) (f (pr2 x'x)))).
apply (weqcomp w1 w2).
Defined.
Definition commhfp {X X' Y : UU} (f : X → Y) (f' : X' → Y) :
commsqstr (hfpg' f f') f' (hfpg f f') f
:= λ xx'e : hfp f f', pr2 xx'e.
Definition hfibertohfp {X Y : UU} (f : X → Y) (y : Y) (xe : hfiber f y) :
hfp (λ t : unit, y) f := tpair (λ tx : unit × X, (f (pr2 tx)) = y)
(make_dirprod tt (pr1 xe)) (pr2 xe).
Definition hfptohfiber {X Y : UU} (f : X → Y) (y : Y)
(hf : hfp (λ t : unit, y) f) : hfiber f y
:= make_hfiber f (pr2 (pr1 hf)) (pr2 hf).
Lemma weqhfibertohfp {X Y : UU} (f : X → Y) (y : Y) :
hfiber f y ≃ hfp (λ _:unit, y) f.
Proof.
intros.
set (ff := hfibertohfp f y).
set (gg := hfptohfiber f y).
split with ff.
assert (egf : ∏ xe : _, (gg (ff xe)) = xe).
intro. induction xe. apply idpath.
assert (efg : ∏ hf : _, (ff (gg hf)) = hf).
intro.
induction hf as [ tx e ]. induction tx as [ t x ].
induction t. apply idpath. apply (isweq_iso _ _ egf efg).
Defined.
Lemma hfp_left {X Y Z : UU} (f : X → Z) (g : Y → Z) :
hfp f g ≃ ∑ x, hfiber g (f x).
Proof.
intros. apply weqtotal2dirprodassoc.
Defined.
Definition hfp_right {X Y Z : UU} (f : X → Z) (g : Y → Z) :
hfp f g ≃ ∑ y, hfiber f (g y).
Proof.
intros. use weq_iso.
- intros [[x y] e]. exact (y,,x,,!e).
- intros [x [y e]]. exact ((y,,x),,!e).
- intros [[x y] e]. apply maponpaths, pathsinv0inv0.
- intros [x [y e]]. apply maponpaths, maponpaths, pathsinv0inv0.
Defined.
Definition hfiber_comm {X Y Z : UU} (f : X → Z) (g : Y → Z) :
(∑ x, hfiber g (f x)) ≃ (∑ y, hfiber f (g y)).
Proof.
intros. use weq_iso.
- intros [x [y e]]. exact (y,,x,,!e).
- intros [y [x e]]. exact (x,,y,,!e).
- intros [x [y e]]. apply maponpaths, maponpaths, pathsinv0inv0.
- intros [y [x e]]. apply maponpaths, maponpaths, pathsinv0inv0.
Defined.
Definition ishfsq {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f)
:= isweq (commsqZtohfp f f' g g' h).
Definition hfsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X')
:= total2 (λ h : commsqstr g' f' g f, isweq (commsqZtohfp f f' g g' h)).
Definition make_hfsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X')
:= tpair (λ h : commsqstr g' f' g f, isweq (commsqZtohfp f f' g g' h)).
Definition hfsqstrtocommsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') :
hfsqstr f f' g g' → commsqstr g' f' g f
:= @pr1 _ (λ h : commsqstr g' f' g f, isweq (commsqZtohfp f f' g g' h)).
Coercion hfsqstrtocommsqstr : hfsqstr >-> commsqstr.
Definition weqZtohfp {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
(g' : Z → X') (hf : hfsqstr f f' g g') : Z ≃ hfp f f'
:= make_weq _ (pr2 hf).
Lemma isweqhfibersgtof' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
(g' : Z → X') (hf : hfsqstr f f' g g') (x : X) :
isweq (hfibersgtof' f f' g g' hf x).
Proof.
intros.
set (is := pr2 hf).
set (h := pr1 hf).
set (a := weqtococonusf g).
set (c := make_weq _ is).
set (d := weqhfptohfpoverX f f').
set (b0 := totalfun _ _ (hfibersgtof' f f' g g' h)).
assert (h1 : ∏ z : Z, (d (c z)) = (b0 (a z))).
intro. simpl. unfold b0. unfold a. unfold weqtococonusf. unfold tococonusf.
simpl. unfold totalfun, total2asstor, hfibersgtof'; simpl.
assert (e : (h z) = (pathscomp0 (h z) (idpath (f (g z))))).
apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath.
assert (is1 : isweq (λ z : _, b0 (a z))).
apply (isweqhomot _ _ h1). apply (twooutof3c _ _ (pr2 c) (pr2 d)).
assert (is2 : isweq b0).
apply (twooutof3b _ _ (pr2 a) is1).
apply (isweqtotaltofib _ _ _ is2 x).
Defined.
Definition weqhfibersgtof' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (hf : hfsqstr f f' g g') (x : X)
:= make_weq _ (isweqhfibersgtof' _ _ _ _ hf x).
Lemma ishfsqweqhfibersgtof' {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f)
(is : ∏ x : X, isweq (hfibersgtof' f f' g g' h x)) : hfsqstr f f' g g'.
Proof.
intros. split with h.
set (a := weqtococonusf g).
set (c0 := commsqZtohfp f f' g g' h).
set (d := weqhfptohfpoverX f f').
set (b := weqfibtototal _ _ (λ x : X, make_weq _ (is x))).
assert (h1 : ∏ z : Z, (d (c0 z)) = (b (a z))).
intro. simpl. unfold b. unfold a. unfold weqtococonusf. unfold tococonusf.
simpl. unfold totalfun, total2asstor, hfibersgtof'; simpl.
assert (e : (h z) = (pathscomp0 (h z) (idpath (f (g z))))).
apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath.
assert (is1 : isweq (λ z : _, d (c0 z))).
apply (isweqhomot _ _ (λ z : Z, (pathsinv0 (h1 z)))).
apply (twooutof3c _ _ (pr2 a) (pr2 b)).
apply (twooutof3a _ _ is1 (pr2 d)).
Defined.
Lemma isweqhfibersg'tof {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
(g' : Z → X') (hf : hfsqstr f f' g g') (x' : X') :
isweq (hfibersg'tof f f' g g' hf x').
Proof.
intros.
set (is := pr2 hf).
set (h := pr1 hf).
set (a' := weqtococonusf g').
set (c' := make_weq _ is).
set (d' := weqhfptohfpoverX' f f').
set (b0' := totalfun _ _ (hfibersg'tof f f' g g' h)).
assert (h1 : ∏ z : Z, (d' (c' z)) = (b0' (a' z))).
intro. unfold b0'. unfold a'. unfold weqtococonusf. unfold tococonusf.
unfold totalfun, hfibersg'tof; simpl.
assert (e : (pathsinv0 (h z))
= (pathscomp0 (pathsinv0 (h z)) (idpath (f' (g' z))))).
apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath.
assert (is1 : isweq (λ z : _, b0'(a' z))).
apply (isweqhomot _ _ h1). apply (twooutof3c _ _ (pr2 c') (pr2 d')).
assert (is2 : isweq b0'). apply (twooutof3b _ _ (pr2 a') is1).
apply (isweqtotaltofib _ _ _ is2 x').
Defined.
Definition weqhfibersg'tof {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (hf : hfsqstr f f' g g') (x' : X')
:= make_weq _ (isweqhfibersg'tof _ _ _ _ hf x').
Lemma ishfsqweqhfibersg'tof {X X' Y Z : UU} (f : X → Y) (f' : X' → Y)
(g : Z → X) (g' : Z → X') (h : commsqstr g' f' g f)
(is : ∏ x' : X', isweq (hfibersg'tof f f' g g' h x')) : hfsqstr f f' g g'.
Proof.
intros.
split with h.
set (a' := weqtococonusf g').
set (c0' := commsqZtohfp f f' g g' h).
set (d' := weqhfptohfpoverX' f f').
set (b' := weqfibtototal _ _ (λ x' : X', make_weq _ (is x'))).
assert (h1 : ∏ z : Z, (d' (c0' z)) = (b' (a' z))).
intro. simpl. unfold b'. unfold a'. unfold weqtococonusf. unfold tococonusf.
unfold totalfun, total2asstor, hfibersg'tof; simpl.
assert (e : (pathsinv0 (h z)) =
(pathscomp0 (pathsinv0 (h z)) (idpath (f' (g' z))))).
apply (pathsinv0 (pathscomp0rid _)). induction e. apply idpath.
assert (is1 : isweq (λ z : _, d' (c0' z))).
apply (isweqhomot _ _ (λ z : Z, (pathsinv0 (h1 z)))).
apply (twooutof3c _ _ (pr2 a') (pr2 b')).
apply (twooutof3a _ _ is1 (pr2 d')).
Defined.
Theorem transposhfpsqstr {X X' Y Z : UU} (f : X → Y) (f' : X' → Y) (g : Z → X)
(g' : Z → X') (hf : hfsqstr f f' g g') : hfsqstr f' f g' g.
Proof.
intros.
set (is := pr2 hf). set (h := pr1 hf).
set (th := transposcommsqstr f f' g g' h).
split with th.
set (w1 := weqhfpcomm f f').
assert (h1 : ∏ z : Z, (w1 (commsqZtohfp f f' g g' h z))
= (commsqZtohfp f' f g' g th z)).
intro. unfold commsqZtohfp. simpl. unfold fpmap. unfold totalfun.
simpl. apply idpath.
apply (isweqhomot _ _ h1). apply (twooutof3c _ _ is (pr2 w1)).
Defined.
Theorem fibseqstrtohfsqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(hf : fibseqstr f g z) : hfsqstr (λ t : unit, z) g (λ x : X, tt) f.
Proof.
intros.
split with (pr1 hf).
set (ff := ezweq f g z hf).
set (ggff := commsqZtohfp (λ t : unit, z) g (λ x : X, tt) f (pr1 hf)).
set (gg := weqhfibertohfp g z).
apply (pr2 (weqcomp ff gg)).
Defined.
Theorem hfsqstrtofibseqstr {X Y Z : UU} (f : X → Y) (g : Y → Z) (z : Z)
(hf : hfsqstr (λ t : unit, z) g (λ x : X, tt) f) : fibseqstr f g z.
Proof.
intros. split with (pr1 hf). set (ff := ezmap f g z (pr1 hf)).
set (ggff := weqZtohfp (λ t : unit, z) g (λ x : X, tt) f hf).
set (gg := weqhfibertohfp g z).
apply (twooutof3a ff gg (pr2 ggff) (pr2 gg)).
Defined.