Library Univalence.components
Require Import HoTT.
Embeddings
The HoTT library uses IsEmbedding f to mean that a map f is
(-1)-truncated, i.e., its fibers are HProps. lemma 7.6.2 in the
book says that they are equivalent, but I couldn't find this in
the HoTT library, so the next two results show this.
Theorem isembedding_isembed {X Y : Type} (f : X → Y) (H1 : IsEmbed f): IsEmbedding f.
Proof.
unfold IsEmbedding.
(* Goal: ∀ y : Y, IsHProp (hfiber f y) *)
intro y.
apply hprop_inhabited_contr.
(* Goal: hfiber f y → Contr (hfiber f y) *)
intros [x0 p].
unfold hfiber.
(* Goal: Contr {x : X & f x = y} *)
(* We'll show that f x = y is equivalent to x = x0, and then Coq knows that the
resulting sigma type is contractible. *)
assert (S : ∀ (x : X), (x = x0) <~> (f x = y)).
{
intro x.
(* We'll show they are equivalent via this intermediate type: *)
equiv_via ((f x) = (f x0)).
- (* Goal: x = x0 <~> f x = f x0 *)
(* This is just the IsEmbedding assumption on the given map f: *)
exact (BuildEquiv _ _ (ap f) (H1 x x0)).
- (* Goal: f x = f x0 <~> f x = y *)
(* For this we just use the path p. *)
exact (equiv_concat_r p _).
}
(* Back to the earlier goal: Contr {x : X & f x = y} *)
(* We use S to substitute inside this: *)
pose (SigS := equiv_functor_sigma_id S).
(* SigS has type { x : X & x = x0 } <~> { x : X & f x = y} *)
(* We use SigS to replace the goal Contr {x : X & f x = y} with
Contr {x : X & x = x0}, which Coq knows is contractible. *)
apply (contr_equiv _ SigS).
Qed.
(* It's also possible to prove the above result using equiv_path_hfiber,
but because of the way that is phrased, it still takes a few steps. *)
Proof.
unfold IsEmbedding.
(* Goal: ∀ y : Y, IsHProp (hfiber f y) *)
intro y.
apply hprop_inhabited_contr.
(* Goal: hfiber f y → Contr (hfiber f y) *)
intros [x0 p].
unfold hfiber.
(* Goal: Contr {x : X & f x = y} *)
(* We'll show that f x = y is equivalent to x = x0, and then Coq knows that the
resulting sigma type is contractible. *)
assert (S : ∀ (x : X), (x = x0) <~> (f x = y)).
{
intro x.
(* We'll show they are equivalent via this intermediate type: *)
equiv_via ((f x) = (f x0)).
- (* Goal: x = x0 <~> f x = f x0 *)
(* This is just the IsEmbedding assumption on the given map f: *)
exact (BuildEquiv _ _ (ap f) (H1 x x0)).
- (* Goal: f x = f x0 <~> f x = y *)
(* For this we just use the path p. *)
exact (equiv_concat_r p _).
}
(* Back to the earlier goal: Contr {x : X & f x = y} *)
(* We use S to substitute inside this: *)
pose (SigS := equiv_functor_sigma_id S).
(* SigS has type { x : X & x = x0 } <~> { x : X & f x = y} *)
(* We use SigS to replace the goal Contr {x : X & f x = y} with
Contr {x : X & x = x0}, which Coq knows is contractible. *)
apply (contr_equiv _ SigS).
Qed.
(* It's also possible to prove the above result using equiv_path_hfiber,
but because of the way that is phrased, it still takes a few steps. *)
This follows the proof from the book, lemma 7.6.2.
Theorem isembed_isembedding {X Y : Type} (f : X → Y) (H1 : IsEmbedding f): IsEmbed f.
Proof.
unfold IsEmbed.
intros x1 x2.
(* Goal: IsEquiv (ap f) *)
apply isequiv_fcontr.
intro p.
(* Goal: Contr {a : x1 = x2 & ap f a = p} *)
apply (contr_equiv ((x1 ; p) = (x2 ; idpath) :> hfiber f (f x2))
(hfiber_ap p)^-1).
(* This should have produced the goal that the path space (x1; p) = (x2; idpath)
is contractible, but apparently Coq was able to use H1 to figure that out. *)
Qed.
Definition IsSurj {X Y : Type} (f : X → Y) := ∀ y : Y, merely (∃ x : X, f x = y).
Theorem isequiv_isembed_issurj {X Y : Type} (f : X → Y) (E : IsEmbed f) (S : IsSurj f)
: IsEquiv f.
Proof.
(* Goal: IsEquiv f *)
apply isequiv_fcontr.
(* Goal: ∀ b : Y, Contr {a : X & f a = b} *)
intro y.
eapply contr_inhab_prop. (* {A} `{IsHProp A} (ma : merely A) : Contr A *)
(* Goal: merely {a : X & f a = y} *)
exact (S y).
Unshelve.
(* Goal: IsHProp {a : X & f a = y} *)
exact (isembedding_isembed f E y).
Qed.
(* This also follows from isequiv_surj_emb in Truncations.v, but that uses
different definitions of embedding and surjection, so isn't as convenient. *)
Proof.
unfold IsEmbed.
intros x1 x2.
(* Goal: IsEquiv (ap f) *)
apply isequiv_fcontr.
intro p.
(* Goal: Contr {a : x1 = x2 & ap f a = p} *)
apply (contr_equiv ((x1 ; p) = (x2 ; idpath) :> hfiber f (f x2))
(hfiber_ap p)^-1).
(* This should have produced the goal that the path space (x1; p) = (x2; idpath)
is contractible, but apparently Coq was able to use H1 to figure that out. *)
Qed.
Definition IsSurj {X Y : Type} (f : X → Y) := ∀ y : Y, merely (∃ x : X, f x = y).
Theorem isequiv_isembed_issurj {X Y : Type} (f : X → Y) (E : IsEmbed f) (S : IsSurj f)
: IsEquiv f.
Proof.
(* Goal: IsEquiv f *)
apply isequiv_fcontr.
(* Goal: ∀ b : Y, Contr {a : X & f a = b} *)
intro y.
eapply contr_inhab_prop. (* {A} `{IsHProp A} (ma : merely A) : Contr A *)
(* Goal: merely {a : X & f a = y} *)
exact (S y).
Unshelve.
(* Goal: IsHProp {a : X & f a = y} *)
exact (isembedding_isembed f E y).
Qed.
(* This also follows from isequiv_surj_emb in Truncations.v, but that uses
different definitions of embedding and surjection, so isn't as convenient. *)
We just need this partial converse.
Lemma isembed_equiv {X Y : Type} (f : X → Y) `{H : IsEquiv X Y f} : IsEmbed f.
Proof.
apply isembed_isembedding.
unfold IsEmbedding.
(* Goal: ∀ y : Y, IsHProp (hfiber f y) *)
intro y.
apply (@trunc_leq -2 -1).
(* Goal: (-2 ≤ -1)%trunc *)
simpl; exact tt.
(* Goal: Contr (hfiber f y) *)
apply fcontr_isequiv.
(* Goal: IsEquiv f *)
assumption.
Qed.
Theorem isembed_compose {X Y Z : Type} (f : X → Y) (g : Y → Z) (Ef : IsEmbed f) (Eg : IsEmbed g)
: IsEmbed (g o f).
Proof.
intros x1 x2.
eapply (isequiv_homotopic ((ap g) o (@ap _ _ f x1 x2))).
- (* Goal: (fun p ⇒ ap g (ap f p)) == ap (fun x ⇒ g (f x)) *)
intro p.
symmetry.
apply ap_compose´.
Unshelve.
(* Goal: IsEquiv (ap g o ap f) *)
apply (isequiv_compose´ (ap f)).
+ apply Ef.
+ apply Eg.
Qed.
Theorem cancelL_isembed {X Y Z : Type} (f : X → Y) (g : Y → Z) (Eg : IsEmbed g) (Egf : IsEmbed (g o f))
: IsEmbed f.
Proof.
intros x1 x2.
(* Goal: IsEquiv (ap f) *)
(* To show r is an equivalence, it suffices to show s o r and s are for some s: *)
apply (@cancelL_isequiv _ _ _ (@ap _ _ g (f x1) (f x2)) (* s *)
(@ap _ _ f x1 x2)). (* r *)
- (* Goal: IsEquiv (ap g) s *)
apply Eg.
- (* Goal: IsEquiv (fun x : x1 = x2 ⇒ ap g (ap f x)) s o r *)
eapply (isequiv_homotopic (ap (g o f))).
+ unfold "==".
apply ap_compose´.
Unshelve.
apply Egf.
Qed.
Definition sigma_inclusion {S1 S2 : Type} (T : S1 → S2) (C : S2 → Type) (u : ∃ s1 : S1, C(T(s1)))
: (∃ s2 : S2, C(s2))
:= (T u.1 ; u.2).
(* sigma_inclusion T C turns out to be the same as @functor_sigma S1 _ S2 C T (fun s1 ⇒ idmap). *)
Theorem isembed_sigma_inclusion {S1 S2 : Type} (T : S1 → S2)
(ET : IsEmbed T) (C : S2 → Type)
: IsEmbed (sigma_inclusion T C).
Proof.
apply isembed_isembedding.
unfold IsEmbedding.
intros [s2 c].
(* Goal: IsHProp (hfiber (sigma_inclusion T C) y) *)
eapply (trunc_equiv _ (hfiber_functor_sigma (fun s1 ⇒ C (T s1))
C T
(fun s1 ⇒ idmap)
s2 c)^-1).
(* hfiber_functor_sigma shows that the thing inside the IsHProp
above is equivalent to what is inside the IsHProp below: *)
Unshelve.
simpl.
(* Goal: IsHProp {w : hfiber T s2 & hfiber idmap (transport C (w.2)^ c)} *)
(* Since the fibers of idmap are contractible, pr1 is an equivalence. *)
eapply (trunc_equiv _ (equiv_sigma_contr _)^-1).
Unshelve.
(* Goal: IsHProp (hfiber T s2) *)
apply isembedding_isembed.
apply ET.
Qed.
Proof.
apply isembed_isembedding.
unfold IsEmbedding.
(* Goal: ∀ y : Y, IsHProp (hfiber f y) *)
intro y.
apply (@trunc_leq -2 -1).
(* Goal: (-2 ≤ -1)%trunc *)
simpl; exact tt.
(* Goal: Contr (hfiber f y) *)
apply fcontr_isequiv.
(* Goal: IsEquiv f *)
assumption.
Qed.
Theorem isembed_compose {X Y Z : Type} (f : X → Y) (g : Y → Z) (Ef : IsEmbed f) (Eg : IsEmbed g)
: IsEmbed (g o f).
Proof.
intros x1 x2.
eapply (isequiv_homotopic ((ap g) o (@ap _ _ f x1 x2))).
- (* Goal: (fun p ⇒ ap g (ap f p)) == ap (fun x ⇒ g (f x)) *)
intro p.
symmetry.
apply ap_compose´.
Unshelve.
(* Goal: IsEquiv (ap g o ap f) *)
apply (isequiv_compose´ (ap f)).
+ apply Ef.
+ apply Eg.
Qed.
Theorem cancelL_isembed {X Y Z : Type} (f : X → Y) (g : Y → Z) (Eg : IsEmbed g) (Egf : IsEmbed (g o f))
: IsEmbed f.
Proof.
intros x1 x2.
(* Goal: IsEquiv (ap f) *)
(* To show r is an equivalence, it suffices to show s o r and s are for some s: *)
apply (@cancelL_isequiv _ _ _ (@ap _ _ g (f x1) (f x2)) (* s *)
(@ap _ _ f x1 x2)). (* r *)
- (* Goal: IsEquiv (ap g) s *)
apply Eg.
- (* Goal: IsEquiv (fun x : x1 = x2 ⇒ ap g (ap f x)) s o r *)
eapply (isequiv_homotopic (ap (g o f))).
+ unfold "==".
apply ap_compose´.
Unshelve.
apply Egf.
Qed.
Definition sigma_inclusion {S1 S2 : Type} (T : S1 → S2) (C : S2 → Type) (u : ∃ s1 : S1, C(T(s1)))
: (∃ s2 : S2, C(s2))
:= (T u.1 ; u.2).
(* sigma_inclusion T C turns out to be the same as @functor_sigma S1 _ S2 C T (fun s1 ⇒ idmap). *)
Theorem isembed_sigma_inclusion {S1 S2 : Type} (T : S1 → S2)
(ET : IsEmbed T) (C : S2 → Type)
: IsEmbed (sigma_inclusion T C).
Proof.
apply isembed_isembedding.
unfold IsEmbedding.
intros [s2 c].
(* Goal: IsHProp (hfiber (sigma_inclusion T C) y) *)
eapply (trunc_equiv _ (hfiber_functor_sigma (fun s1 ⇒ C (T s1))
C T
(fun s1 ⇒ idmap)
s2 c)^-1).
(* hfiber_functor_sigma shows that the thing inside the IsHProp
above is equivalent to what is inside the IsHProp below: *)
Unshelve.
simpl.
(* Goal: IsHProp {w : hfiber T s2 & hfiber idmap (transport C (w.2)^ c)} *)
(* Since the fibers of idmap are contractible, pr1 is an equivalence. *)
eapply (trunc_equiv _ (equiv_sigma_contr _)^-1).
Unshelve.
(* Goal: IsHProp (hfiber T s2) *)
apply isembedding_isembed.
apply ET.
Qed.
Pi0 is a functor.
The map sending a point to its component.
Theorem issurj_tr (X : Type): IsSurj (tr : X → Pi0 X).
Proof.
unfold IsSurj.
intro c.
(* Goal: merely {x : X & tr x = c} *)
(* Since merely ... is an hProp, we can assume c is tr x0 for some x0 : X. *)
strip_truncations. rename c into x0.
(* Remove the outer merely from the conclusion. *)
apply tr.
(* Goal: {x : X & tr x = tr x0} *)
exact (x0; idpath (tr x0)).
Qed.
Proof.
unfold IsSurj.
intro c.
(* Goal: merely {x : X & tr x = c} *)
(* Since merely ... is an hProp, we can assume c is tr x0 for some x0 : X. *)
strip_truncations. rename c into x0.
(* Remove the outer merely from the conclusion. *)
apply tr.
(* Goal: {x : X & tr x = tr x0} *)
exact (x0; idpath (tr x0)).
Qed.
Theorem comp_equiv_comp_tr {X : Type} (c : Pi0 X) : merely (∃ x0 : X, (comp c) <~> (comp_tr x0)).
Proof.
strip_truncations.
apply tr.
exact (c; equiv_idmap).
Qed.
Proof.
strip_truncations.
apply tr.
exact (c; equiv_idmap).
Qed.
The inclusion of a component into the original type.
These inclusions are embeddings.
Theorem isembed_comp_incl {X : Type} (c : Pi0 X) : IsEmbed (comp_incl c).
Proof.
intros x y.
unfold comp_incl.
apply isequiv_ap_pr1_hprop.
(* isequiv_ap_pr1_hprop is in Types/Sigma.v; can also use isequiv_pr1_path_hprop.
Not sure why Coq doesn't find it automatically here. *)
Qed.
Proof.
intros x y.
unfold comp_incl.
apply isequiv_ap_pr1_hprop.
(* isequiv_ap_pr1_hprop is in Types/Sigma.v; can also use isequiv_pr1_path_hprop.
Not sure why Coq doesn't find it automatically here. *)
Qed.
We now study the coproduct of the components of a type.
Each X is equivalent to the set-indexed coproduct of its components.
Theorem isequiv_natmap (X : Type) : IsEquiv (natmap X).
Proof.
(* We'll express natmap X as a composite of the map
{c : Pi0 X & {x : X & tr x = c}} → {x : X & {c : Pi0 X & tr x = c}}
which swaps the sigmas, with the map pr1 from the latter to X. *)
apply (isequiv_compose´ (equiv_sigma_symm (fun (c : Pi0 X) ⇒ fun (x : X) ⇒ tr x = c)) _ pr1).
(* Goal: IsEquiv pr1 *)
apply isequiv_pr1_contr.
Qed.
Definition coproduct_of_components (X : Type) : (∃ c : Pi0 X, comp c) <~> X
:= BuildEquiv _ _ (natmap X) (isequiv_natmap X).
Proof.
(* We'll express natmap X as a composite of the map
{c : Pi0 X & {x : X & tr x = c}} → {x : X & {c : Pi0 X & tr x = c}}
which swaps the sigmas, with the map pr1 from the latter to X. *)
apply (isequiv_compose´ (equiv_sigma_symm (fun (c : Pi0 X) ⇒ fun (x : X) ⇒ tr x = c)) _ pr1).
(* Goal: IsEquiv pr1 *)
apply isequiv_pr1_contr.
Qed.
Definition coproduct_of_components (X : Type) : (∃ c : Pi0 X, comp c) <~> X
:= BuildEquiv _ _ (natmap X) (isequiv_natmap X).
This lemma is used in the proof of the main result.
Lemma isembed_pi0_isembed `{Univalence} {X Y : Type} (f : X → Y) (E : IsEmbed f)
: IsEmbed (pi0_functor f).
Proof.
unfold IsEmbed.
intros x0 x1.
strip_truncations.
(* Goal: IsEquiv (ap (pi0_functor f)) *)
apply isequiv_fcontr.
intro q.
compute in q. (* q : tr (f x0) = tr (f x1) *)
(* Goal: Contr {a : tr x0 = tr x1 & ap (pi0_functor f) a = q} *)
apply contr_inhab_prop.
(* Coq knows it's an HProp, so we just need to show it is merely inhabited. *)
(* Goal: merely {a : tr x0 = tr x1 & ap (pi0_functor f) a = q} *)
cut (Trunc (-1) ((f x0) = (f x1))).
- (* Goal: Trunc (-1) (f x0 = f x1) → merely {a : tr x0 = tr x1 & ap (pi0_functor f) a = q} *)
intro p.
strip_truncations.
apply tr.
(* Goal: {a : tr x0 = tr x1 & ap (pi0_functor f) a = q} *)
(* I need to convince Coq that ap f is an equivalence. *)
pose (apf := BuildEquiv (x0 = x1) _ (ap f) (E x0 x1)).
∃ ((ap tr) ((apf)^-1 p)).
(* Goal: ap (pi0_functor f) (ap tr (apf^-1 p)) = q *)
apply set_path2.
- (* Goal: Trunc (-1) (f x0 = f x1) *)
exact ((equiv_path_Tr (f x0) (f x1))^-1 q). (* Uses Univalence. *)
Qed.
: IsEmbed (pi0_functor f).
Proof.
unfold IsEmbed.
intros x0 x1.
strip_truncations.
(* Goal: IsEquiv (ap (pi0_functor f)) *)
apply isequiv_fcontr.
intro q.
compute in q. (* q : tr (f x0) = tr (f x1) *)
(* Goal: Contr {a : tr x0 = tr x1 & ap (pi0_functor f) a = q} *)
apply contr_inhab_prop.
(* Coq knows it's an HProp, so we just need to show it is merely inhabited. *)
(* Goal: merely {a : tr x0 = tr x1 & ap (pi0_functor f) a = q} *)
cut (Trunc (-1) ((f x0) = (f x1))).
- (* Goal: Trunc (-1) (f x0 = f x1) → merely {a : tr x0 = tr x1 & ap (pi0_functor f) a = q} *)
intro p.
strip_truncations.
apply tr.
(* Goal: {a : tr x0 = tr x1 & ap (pi0_functor f) a = q} *)
(* I need to convince Coq that ap f is an equivalence. *)
pose (apf := BuildEquiv (x0 = x1) _ (ap f) (E x0 x1)).
∃ ((ap tr) ((apf)^-1 p)).
(* Goal: ap (pi0_functor f) (ap tr (apf^-1 p)) = q *)
apply set_path2.
- (* Goal: Trunc (-1) (f x0 = f x1) *)
exact ((equiv_path_Tr (f x0) (f x1))^-1 q). (* Uses Univalence. *)
Qed.
An equivalent description of components, in the presence of Univalence.
The two definitions of components agree.
Definition comp_eq_equiv_comp_tr `{Univalence} {X : Type} (x0 : X) : (comp_eq x0) <~> (comp_tr x0).
Proof.
unfold comp_eq, comp_tr, comp.
(* Goal: {x : X & merely (x = x0)} <~> {x : X & tr x = tr x0} *)
(* Both sides are sigma types over X, so suffices to show that
the families are equivalent pointwise: *)
apply equiv_functor_sigma_id; intro x.
(* Goal: merely (x = x0) <~> tr x = tr x0 *)
(* Here, tr is really @tr 0 and merely is Tr -1. *)
(* Next line needs Univalence: *)
apply equiv_path_Tr.
Defined.
Definition comp_tr_equiv_comp_eq `{Univalence} {X : Type} (x0 : X) : (comp_tr x0) <~> (comp_eq x0)
:= (comp_eq_equiv_comp_tr x0)^-1.
Proof.
unfold comp_eq, comp_tr, comp.
(* Goal: {x : X & merely (x = x0)} <~> {x : X & tr x = tr x0} *)
(* Both sides are sigma types over X, so suffices to show that
the families are equivalent pointwise: *)
apply equiv_functor_sigma_id; intro x.
(* Goal: merely (x = x0) <~> tr x = tr x0 *)
(* Here, tr is really @tr 0 and merely is Tr -1. *)
(* Next line needs Univalence: *)
apply equiv_path_Tr.
Defined.
Definition comp_tr_equiv_comp_eq `{Univalence} {X : Type} (x0 : X) : (comp_tr x0) <~> (comp_eq x0)
:= (comp_eq_equiv_comp_tr x0)^-1.
We can show without Univalence that the comp_eq components are connected.
Definition MyIsConn (A : Type) := ∀ (a b : A), merely (a = b).
Theorem myisconn_comp_eq {X : Type} (x0 : X) : MyIsConn (comp_eq x0).
Proof.
unfold MyIsConn.
(* Goal: ∀ a b : comp_eq x0, merely (a = b) *)
intros [x1 p1] [x2 p2].
(* Goal: merely ((x1; p1) = (x2; p2)) with p_i : merely (x_i = x_0). *)
(* Remove the merely's from hypotheses; changes p_i to tr p_i in conclusion: *)
strip_truncations.
(* Remove the outer merely from the conclusion: *)
apply tr.
(* Goal: (x1; tr p1) = (x2; tr p2) *)
apply path_sigma_hprop; simpl.
(* Goal: x1 = x2 *)
exact (p1 @ p2^).
Qed.
Theorem myisconn_comp_eq {X : Type} (x0 : X) : MyIsConn (comp_eq x0).
Proof.
unfold MyIsConn.
(* Goal: ∀ a b : comp_eq x0, merely (a = b) *)
intros [x1 p1] [x2 p2].
(* Goal: merely ((x1; p1) = (x2; p2)) with p_i : merely (x_i = x_0). *)
(* Remove the merely's from hypotheses; changes p_i to tr p_i in conclusion: *)
strip_truncations.
(* Remove the outer merely from the conclusion: *)
apply tr.
(* Goal: (x1; tr p1) = (x2; tr p2) *)
apply path_sigma_hprop; simpl.
(* Goal: x1 = x2 *)
exact (p1 @ p2^).
Qed.
The image of a map.
Definition im {X Y : Type} (f : X → Y) := { y : Y & merely (∃ x : X, f x = y) }.
Definition to_im {X Y : Type} (f : X → Y) : X → im f :=
fun x ⇒ ( f x; tr ( x; idpath ) ).
Definition incl_im {X Y : Type} (f : X → Y) : im f → Y := pr1.
Theorem factors {X Y : Type} (f : X → Y) : f == (incl_im f) o (to_im f).
Proof.
intro x.
reflexivity.
Qed.
Theorem isembed_incl_im {X Y : Type} (f : X → Y) : IsEmbed (incl_im f).
Proof.
intros x y.
unfold incl_im.
apply isequiv_ap_pr1_hprop.
(* isequiv_ap_pr1_hprop is in Types/Sigma.v; can also use isequiv_pr1_path_hprop.
Not sure why Coq doesn't find it automatically here. *)
Qed.
Theorem issurj_to_im {X Y : Type} (f : X → Y) : IsSurj (to_im f).
Proof.
(* Goal: IsSurj (to_im f) *)
intros [y q].
(* Goal: merely {x : X & to_im f x = (y; tr q)} *)
strip_truncations.
apply tr.
(* Goal: {x : X & to_im f x = (y; tr q)} *)
destruct q as [x p].
∃ x.
(* Goal: to_im f x = (y; tr (x; p)) *)
unfold to_im.
(* Goal: (f x; tr (x; 1)) = (y; tr (x; p)) *)
apply path_sigma_hprop.
simpl.
(* Goal: f x = y *)
exact p.
Qed.
Theorem isembed_to_im {X Y : Type} (f : X → Y) (E : IsEmbed f): IsEmbed (to_im f).
Proof.
apply (cancelL_isembed (to_im f) (incl_im f) (isembed_incl_im f)).
(* Goal: IsEmbed (fun x : X ⇒ incl_im f (to_im f x)) *)
unfold IsEmbed.
intros x0 x1.
(* Goal: IsEquiv (ap (fun x : X ⇒ incl_im f (to_im f x))) *)
eapply (isequiv_homotopic (ap f)).
- (* Goal: ap f == ap (fun x : X ⇒ incl_im f (to_im f x)) *)
intro x.
reflexivity.
Unshelve.
(* Goal: IsEquiv (ap f) *)
apply E.
Qed.
Theorem isequiv_to_im {X Y : Type} (f : X → Y) (E : IsEmbed f): IsEquiv (to_im f).
Proof.
apply isequiv_isembed_issurj.
exact (isembed_to_im f E).
exact (issurj_to_im f).
Qed.
Definition equiv_to_im {X Y : Type} (f : X → Y) (E : IsEmbed f): X <~> im f
:= BuildEquiv _ _ (to_im f) (isequiv_to_im f E).
Definition pointed_connected (X : Type) (x0 : X) := ∀ (x : X), merely (x = x0).
Definition equiv_im_f_comp_eq {X Y : Type} (x0 : X) (pc : pointed_connected X x0) (f : X → Y)
: im f <~> comp_eq (f x0).
Proof.
apply equiv_functor_sigma_id; intro y.
(* Goal: merely {x : X & f x = y} <~> merely (y = f x0) *)
apply equiv_iff_hprop.
- (* Goal: merely {x : X & f x = y} → merely (y = f x0) *)
intro xp.
strip_truncations.
destruct xp as [x p].
(* Goal: merely (y = f x0) *)
(* Have pc x : merely (x = x0) and p : f x = y. *)
(* fun q : x = x0 ⇒ p^ @ ap f q has type x = x0 → y = f x0. *)
exact (Trunc_functor -1 (fun q : x = x0 ⇒ p^ @ ap f q) (pc x)).
- (* Goal: merely (y = f x0) → merely {x : X & f x = y} *)
apply Trunc_functor.
(* Goal: y = f x0 → {x : X & f x = y} *)
intro p.
exact (x0; p^).
Defined.
Definition im´ {X Y : Type} (f : X → Y) := { y : Y & merely (∃ s : Pi0 X, (pi0_functor f) s = tr y) }.
Definition equiv_im_im´ `{Univalence} {X Y : Type} (f : X → Y) : im f <~> im´ f.
Proof.
unfold im, im´.
apply equiv_functor_sigma_id. intro y.
(* Goal: merely {x : X & f x = y} <~> merely {s : Pi0 X & pi0_functor f s = tr y} *)
apply equiv_iff_hprop. (* From Trunc.v. *)
- (* Goal: merely {x : X & f x = y} → merely {s : Pi0 X & pi0_functor f s = tr y} *)
apply Trunc_functor.
intros [x p].
(* Goal: {s : Pi0 X & pi0_functor f s = tr y} *)
∃ (tr x).
compute. (* Just for the reader's sake. *)
(* Goal: tr (f x) = tr y *)
exact (ap tr p).
- (* Goal: merely {s : Pi0 X & pi0_functor f s = tr y} → merely {x : X & f x = y} *)
apply Trunc_rec.
(* Goal: {s : Pi0 X & pi0_functor f s = tr y} → merely {x : X & f x = y} *)
intros [s p].
revert p. (* In order to strip_truncations, need to revert p first. *)
strip_truncations; rename s into x.
compute.
(* Goal: tr (f x) = tr y → Trunc (-1) {x0 : X & f x0 = y} *)
(* We'll produce this function as the composite of the equivalence from
tr (f x) = tr y to Trunc (-1) ((f x) = y) followed by Trunc_functor
applied to the obvious map from (f x) = y to {x0 : X & f x0 = y}. *)
intro p.
apply (Trunc_functor -1 (fun q ⇒ (x ; q))).
apply equiv_path_Tr. (* Uses Univalence. *)
exact p.
Defined.
Definition equiv_im_im´ `{Univalence} {X Y : Type} (f : X → Y) : im f <~> im´ f.
Proof.
unfold im, im´.
apply equiv_functor_sigma_id. intro y.
(* Goal: merely {x : X & f x = y} <~> merely {s : Pi0 X & pi0_functor f s = tr y} *)
apply equiv_iff_hprop. (* From Trunc.v. *)
- (* Goal: merely {x : X & f x = y} → merely {s : Pi0 X & pi0_functor f s = tr y} *)
apply Trunc_functor.
intros [x p].
(* Goal: {s : Pi0 X & pi0_functor f s = tr y} *)
∃ (tr x).
compute. (* Just for the reader's sake. *)
(* Goal: tr (f x) = tr y *)
exact (ap tr p).
- (* Goal: merely {s : Pi0 X & pi0_functor f s = tr y} → merely {x : X & f x = y} *)
apply Trunc_rec.
(* Goal: {s : Pi0 X & pi0_functor f s = tr y} → merely {x : X & f x = y} *)
intros [s p].
revert p. (* In order to strip_truncations, need to revert p first. *)
strip_truncations; rename s into x.
compute.
(* Goal: tr (f x) = tr y → Trunc (-1) {x0 : X & f x0 = y} *)
(* We'll produce this function as the composite of the equivalence from
tr (f x) = tr y to Trunc (-1) ((f x) = y) followed by Trunc_functor
applied to the obvious map from (f x) = y to {x0 : X & f x0 = y}. *)
intro p.
apply (Trunc_functor -1 (fun q ⇒ (x ; q))).
apply equiv_path_Tr. (* Uses Univalence. *)
exact p.
Defined.
This is a technical helper lemma that is used in the next result.
Definition equiv_im´_components {X Y : Type} (f : X → Y) (E : IsEmbed (pi0_functor f))
: im´ f <~> { s : Pi0 X & (∃ y : Y, tr y = (pi0_functor f) s ) }.
Proof.
unfold im´.
set (f´ := pi0_functor f).
equiv_via {y : Y & {s : Pi0 X & f´ s = tr y}}.
- (* Goal: {y : Y & merely {s : Pi0 X & f´ s = tr y}} <~> {y : Y & {s : Pi0 X & tr y = f´ s}} *)
apply equiv_functor_sigma_id. intro y.
apply symmetry.
refine (equiv_tr -1 _). (* A → merely A is an equivalence when IsHProp A. *)
(* Goal: IsHProp {s : Pi0 X & f´ s = tr y} *)
apply (isembedding_isembed _ E).
- (* Goal: {y : Y & {s : Pi0 X & f´ s = tr y}} <~> {s : Pi0 X & {y : Y & tr y = f´ s}} *)
apply (equiv_composeR´ (equiv_sigma_symm _)).
(* Goal: {b : Pi0 X & {a : Y & f´ b = tr a}} <~> {s : Pi0 X & {y : Y & tr y = f´ s}} *)
apply equiv_functor_sigma_id. intro s.
apply equiv_functor_sigma_id. intro y.
apply equiv_path_inverse.
Defined.
: im´ f <~> { s : Pi0 X & (∃ y : Y, tr y = (pi0_functor f) s ) }.
Proof.
unfold im´.
set (f´ := pi0_functor f).
equiv_via {y : Y & {s : Pi0 X & f´ s = tr y}}.
- (* Goal: {y : Y & merely {s : Pi0 X & f´ s = tr y}} <~> {y : Y & {s : Pi0 X & tr y = f´ s}} *)
apply equiv_functor_sigma_id. intro y.
apply symmetry.
refine (equiv_tr -1 _). (* A → merely A is an equivalence when IsHProp A. *)
(* Goal: IsHProp {s : Pi0 X & f´ s = tr y} *)
apply (isembedding_isembed _ E).
- (* Goal: {y : Y & {s : Pi0 X & f´ s = tr y}} <~> {s : Pi0 X & {y : Y & tr y = f´ s}} *)
apply (equiv_composeR´ (equiv_sigma_symm _)).
(* Goal: {b : Pi0 X & {a : Y & f´ b = tr a}} <~> {s : Pi0 X & {y : Y & tr y = f´ s}} *)
apply equiv_functor_sigma_id. intro s.
apply equiv_functor_sigma_id. intro y.
apply equiv_path_inverse.
Defined.
Definition IsCanon {X Y : Type} (f : X → Y) := ∃ S : Type, ∃ HS : IsHSet S,
∃ T : S → Pi0 Y, ∃ ET : IsEmbed T, ∃ e : X → { s : S | comp (T s) },
∃ Ee : IsEquiv e, f = (fun x ⇒ (e x).2.1).
(* The last lambda expression is pr1 o pr2 o e, or (comp_incl _) o pr2 o e, but Coq
won't accept those for some reason. *)
One direction of the main result.
Theorem iscanon_embed `{Univalence} {X Y : Type} (f : X → Y) (E : IsEmbed f) : IsCanon f.
Proof.
unfold IsCanon.
∃ (Pi0 X). (* S *)
∃ (isset_pi0 _). (* HS *)
∃ (pi0_functor f). (* T *)
pose (ET := isembed_pi0_isembed f E).
∃ ET. (* ET *)
∃ ((equiv_im´_components f ET) oE (equiv_im_im´ f) oE (equiv_to_im f E)). (* e *)
∃ _. (* Ee *)
(* Goal: f = (fun x : X ⇒ (((equiv_im´_components f ET oE equiv_im_im´ f oE equiv_to_im f E) x).2).1) *)
reflexivity.
(* Coq is able to unroll those complicated definitions! *)
Qed.
Proof.
unfold IsCanon.
∃ (Pi0 X). (* S *)
∃ (isset_pi0 _). (* HS *)
∃ (pi0_functor f). (* T *)
pose (ET := isembed_pi0_isembed f E).
∃ ET. (* ET *)
∃ ((equiv_im´_components f ET) oE (equiv_im_im´ f) oE (equiv_to_im f E)). (* e *)
∃ _. (* Ee *)
(* Goal: f = (fun x : X ⇒ (((equiv_im´_components f ET oE equiv_im_im´ f oE equiv_to_im f E) x).2).1) *)
reflexivity.
(* Coq is able to unroll those complicated definitions! *)
Qed.
And the converse.
Theorem isembed_canon {X Y : Type} (f : X → Y) (E : IsCanon f) : IsEmbed f.
Proof.
(* Extract the components of E. Do in reverse order, so that a name like S
gets used in the display of a term like e. *)
(* Why is this proof so slow to process? *)
set (p := E.2.2.2.2.2.2) in ×.
set (Ee := E.2.2.2.2.2.1) in ×.
set (e := E.2.2.2.2.1) in ×.
set (ET := E.2.2.2.1) in ×.
set (T := E.2.2.1) in ×.
set (HS := E.2.1) in ×.
set (S := E.1) in ×.
simpl in p.
rewrite p.
(* Goal: IsEmbed (fun x : X ⇒ ((e x).2).1) *)
apply (isembed_compose e (fun (sy : {s : S & comp (T s)}) ⇒ sy.2.1)).
- (* Goal: IsEmbed e *)
apply isembed_equiv.
exact Ee.
- (* Goal: IsEmbed (fun sy : {s : S & comp (T s)} ⇒ (sy.2).1) *)
(* Now the plan is to factor this into a composite g2 o g1, with g2 an equivalence. *)
set (g1 := sigma_inclusion T comp).
set (g2 := natmap Y).
(* Since the factorization works definitionally, we can substitute: *)
change (fun sy : {s´ : S & comp (T s´)} ⇒ (sy.2).1) with (g2 o g1).
(* The previous line gives:
Warning: Collision between bound variables of name s'
(twice). Not sure why. *)
(* Goal: IsEmbed (g2 o g1) *)
apply (isembed_compose g1 g2).
+ (* Goal: IsEmbed g1 *)
apply isembed_sigma_inclusion.
(* Goal: IsEmbed T *)
exact ET.
+ (* Goal: IsEmbed g2 *)
apply isembed_equiv.
(* Goal: IsEquiv g2 *)
apply isequiv_natmap.
Qed.
Proof.
(* Extract the components of E. Do in reverse order, so that a name like S
gets used in the display of a term like e. *)
(* Why is this proof so slow to process? *)
set (p := E.2.2.2.2.2.2) in ×.
set (Ee := E.2.2.2.2.2.1) in ×.
set (e := E.2.2.2.2.1) in ×.
set (ET := E.2.2.2.1) in ×.
set (T := E.2.2.1) in ×.
set (HS := E.2.1) in ×.
set (S := E.1) in ×.
simpl in p.
rewrite p.
(* Goal: IsEmbed (fun x : X ⇒ ((e x).2).1) *)
apply (isembed_compose e (fun (sy : {s : S & comp (T s)}) ⇒ sy.2.1)).
- (* Goal: IsEmbed e *)
apply isembed_equiv.
exact Ee.
- (* Goal: IsEmbed (fun sy : {s : S & comp (T s)} ⇒ (sy.2).1) *)
(* Now the plan is to factor this into a composite g2 o g1, with g2 an equivalence. *)
set (g1 := sigma_inclusion T comp).
set (g2 := natmap Y).
(* Since the factorization works definitionally, we can substitute: *)
change (fun sy : {s´ : S & comp (T s´)} ⇒ (sy.2).1) with (g2 o g1).
(* The previous line gives:
Warning: Collision between bound variables of name s'
(twice). Not sure why. *)
(* Goal: IsEmbed (g2 o g1) *)
apply (isembed_compose g1 g2).
+ (* Goal: IsEmbed g1 *)
apply isembed_sigma_inclusion.
(* Goal: IsEmbed T *)
exact ET.
+ (* Goal: IsEmbed g2 *)
apply isembed_equiv.
(* Goal: IsEquiv g2 *)
apply isequiv_natmap.
Qed.
Definition omega {B : Type} (E : B → Type) (x y : B) := ap E: (x = y) → ((E x) = (E y)).
Definition IsUnivalent {B : Type} (E : B → Type) := ∀ (x y : B), IsEquiv (omega E x y).
IsUnivalent is definitionally equal to IsEmbed.
Definition check_isunivalent {B : Type} (E : B → Type) : IsEmbed E = IsUnivalent E := idpath.
Theorem univalent_iff_canon `{Univalence} {B : Type} (E : B → Type) : IsUnivalent E ↔ IsCanon E.
Proof.
split.
(* Goal: IsUnivalent E → IsCanon E *)
apply iscanon_embed.
(* Goal: IsCanon E → IsUnivalent E *)
apply isembed_canon.
Qed.
Definition omegaEq {B : Type} (E : B → Type) (x y : B)
:= (equiv_path _ _) o (omega E x y) : (x = y) → ((E x) <~> (E y)).
(* Here, equiv_path : (E x) = (E y) → (E x) <~> (E y) is the natural map. *)
Definition IsUnivalentEq {B : Type} (E : B → Type) := ∀ (x y : B), IsEquiv (omegaEq E x y).
Lemma isequiv_compose_with_equiv `{Funext} {A B C : Type} (f : A → B) (g : B → C) {Eg : IsEquiv g}
: IsEquiv f <~> IsEquiv (g o f).
Proof.
(* Under Funext, IsEquiv is an hprop, so the goal reduces to showing that each implies the other. *)
apply equiv_iff_hprop.
(* → *)
- intro isequiv_omega.
exact isequiv_compose.
(* <- *)
- intro isequiv_omegaEq.
exact (cancelL_isequiv g).
Qed.
Theorem univalent_iff_canon `{Univalence} {B : Type} (E : B → Type) : IsUnivalent E ↔ IsCanon E.
Proof.
split.
(* Goal: IsUnivalent E → IsCanon E *)
apply iscanon_embed.
(* Goal: IsCanon E → IsUnivalent E *)
apply isembed_canon.
Qed.
Definition omegaEq {B : Type} (E : B → Type) (x y : B)
:= (equiv_path _ _) o (omega E x y) : (x = y) → ((E x) <~> (E y)).
(* Here, equiv_path : (E x) = (E y) → (E x) <~> (E y) is the natural map. *)
Definition IsUnivalentEq {B : Type} (E : B → Type) := ∀ (x y : B), IsEquiv (omegaEq E x y).
Lemma isequiv_compose_with_equiv `{Funext} {A B C : Type} (f : A → B) (g : B → C) {Eg : IsEquiv g}
: IsEquiv f <~> IsEquiv (g o f).
Proof.
(* Under Funext, IsEquiv is an hprop, so the goal reduces to showing that each implies the other. *)
apply equiv_iff_hprop.
(* → *)
- intro isequiv_omega.
exact isequiv_compose.
(* <- *)
- intro isequiv_omegaEq.
exact (cancelL_isequiv g).
Qed.
In the presence of Univalence of the universe, the two definitions of
univalent family agree, since equiv_path is an equivalence.
Lemma equiv_univalent_univalenteq `{Univalence} {B : Type} (E : B → Type) :
IsUnivalent E <~> IsUnivalentEq E.
Proof.
unfold IsUnivalent, IsEmbed, IsUnivalentEq.
apply equiv_functor_forall_id; intro x. (* From Types.Forall *)
apply equiv_functor_forall_id; intro y.
apply (isequiv_compose_with_equiv _ (equiv_path _ _)).
Qed.
Lemma iff_equiv {P Q : Type} (E : P <~> Q) : P ↔ Q.
Proof.
split.
exact E.
exact (E^-1).
Qed.
IsUnivalent E <~> IsUnivalentEq E.
Proof.
unfold IsUnivalent, IsEmbed, IsUnivalentEq.
apply equiv_functor_forall_id; intro x. (* From Types.Forall *)
apply equiv_functor_forall_id; intro y.
apply (isequiv_compose_with_equiv _ (equiv_path _ _)).
Qed.
Lemma iff_equiv {P Q : Type} (E : P <~> Q) : P ↔ Q.
Proof.
split.
exact E.
exact (E^-1).
Qed.
This is the main theorem, in full generality.
Theorem univalenteq_iff_canon `{Univalence} {B : Type} (E : B → Type) : IsUnivalentEq E ↔ IsCanon E.
Proof.
apply (iff_compose (B := IsUnivalent E)).
- (* Goal: IsUnivalent E ↔ IsCanon E *)
apply univalent_iff_canon.
- (* Goal: IsUnivalentEq E ↔ IsUnivalent E *)
apply iff_equiv.
symmetry.
apply equiv_univalent_univalenteq.
Qed.
Proof.
apply (iff_compose (B := IsUnivalent E)).
- (* Goal: IsUnivalent E ↔ IsCanon E *)
apply univalent_iff_canon.
- (* Goal: IsUnivalentEq E ↔ IsUnivalent E *)
apply iff_equiv.
symmetry.
apply equiv_univalent_univalenteq.
Qed.
Expressing the result using BAut.
A variation, closer to the homotopy theoretic notion.
With this notation, univalent_iff_canon says that a univalent
type family is equivalent to a coproduct of BAut´ F´'s, with
their natural maps to Type.
All three are equivalent under Univalence.
Theorem equiv_bauteq_baut `{Univalence} (F : Type) : (BAutEq F) <~> (BAut F).
Proof.
apply equiv_functor_sigma_id; intro X.
∃ (Trunc_functor -1 (equiv_path_universe X F)).
(* equiv_path_universe is from Types.Universe *)
apply isequiv_Trunc_functor.
exact _.
Qed.
Definition equiv_baut_baut´ `{Univalence} (F : Type) : BAut F <~> BAut´ (tr F)
:= comp_eq_equiv_comp_tr F.
Proof.
apply equiv_functor_sigma_id; intro X.
∃ (Trunc_functor -1 (equiv_path_universe X F)).
(* equiv_path_universe is from Types.Universe *)
apply isequiv_Trunc_functor.
exact _.
Qed.
Definition equiv_baut_baut´ `{Univalence} (F : Type) : BAut F <~> BAut´ (tr F)
:= comp_eq_equiv_comp_tr F.
They have the expected loop spaces.
Definition Aut (F : Type) := F = F.
Definition pt F := (F; tr idpath) : BAut F.
Theorem deloop_baut (F : Type) : Aut F <~> (pt F = pt F).
Proof.
exact (equiv_path_sigma_hprop (pt F) (pt F)).
Qed.
Definition pt F := (F; tr idpath) : BAut F.
Theorem deloop_baut (F : Type) : Aut F <~> (pt F = pt F).
Proof.
exact (equiv_path_sigma_hprop (pt F) (pt F)).
Qed.
The analogous result holds for BAutEq, using:
Definition AutEq (F : Type) := F <~> F.
Theorem auteq_equiv_aut `{Univalence} (F : Type) : (AutEq F) <~> (Aut F).
Proof.
exact (equiv_path_universe F F).
Qed.
Theorem auteq_equiv_aut `{Univalence} (F : Type) : (AutEq F) <~> (Aut F).
Proof.
exact (equiv_path_universe F F).
Qed.
The natural type families over BAut´ F´ and BAut F are univalent.
BAut´ F´ is a sigma type coming from the type family Type → Type
sending Z to tr Z = F´, and pr1 is the natural map to Type.
This is what we called comp_incl earlier.
Theorem isunivalent_baut´_pr1 (F´ : Pi0 Type) : IsUnivalent (BAut´_pr1 F´).
Proof.
apply isembed_comp_incl.
Qed.
Proof.
apply isembed_comp_incl.
Qed.
BAut F is a sigma type coming from the type family Type → Type
sending Z to merely (Z = F), and pr1 is the natural map to Type.
This is defined in BAut.v:
Definition BAut_pr1 F : BAut F → Type := pr1.
The natural type family over BAut´ F´ is univalent, since
the fibres are hProps.
Theorem isunivalent_baut_pr1 (F : Type) : IsUnivalent (BAut_pr1 F).
Proof.
intros Ze Ze´.
unfold BAut_pr1. (* For Coq. *)
unfold omega. (* For the user. *)
(* Goal: IsEquiv (ap pr1) *)
apply isequiv_ap_pr1_hprop.
(* isequiv_ap_pr1_hprop is in Types/Sigma.v; can also use isequiv_pr1_path_hprop.
Not sure why Coq doesn't find it automatically here. *)
Qed.
Proof.
intros Ze Ze´.
unfold BAut_pr1. (* For Coq. *)
unfold omega. (* For the user. *)
(* Goal: IsEquiv (ap pr1) *)
apply isequiv_ap_pr1_hprop.
(* isequiv_ap_pr1_hprop is in Types/Sigma.v; can also use isequiv_pr1_path_hprop.
Not sure why Coq doesn't find it automatically here. *)
Qed.
Alternate proof, that needs Univalence.
Theorem isunivalent_baut_pr1´ `{Univalence} (F : Type) : IsUnivalent (BAut_pr1 F).
Proof.
(* BAut_pr1 is the composite of equiv_baut_baut´ with BAut´_pr1. *)
change (BAut_pr1 F) with ((BAut´_pr1 (tr F)) o (equiv_baut_baut´ F)).
apply (isembed_compose (equiv_baut_baut´ F)).
apply isembed_equiv. exact _.
apply isunivalent_baut´_pr1.
Qed.
(* Of course, IsUnivalentEq holds for the above as well, under Univalence. *)
Proof.
(* BAut_pr1 is the composite of equiv_baut_baut´ with BAut´_pr1. *)
change (BAut_pr1 F) with ((BAut´_pr1 (tr F)) o (equiv_baut_baut´ F)).
apply (isembed_compose (equiv_baut_baut´ F)).
apply isembed_equiv. exact _.
apply isunivalent_baut´_pr1.
Qed.
(* Of course, IsUnivalentEq holds for the above as well, under Univalence. *)
A univalent type family over a pointed connected space is equivalent to the
natural family over some BAut. The underlying map is the classifying map
of the type family.
Definition equiv_conn_BAut {B : Type} (x0 : B) (pc : pointed_connected B x0) (E : B → Type) (un : IsUnivalent E)
: B <~> BAut (E x0).
Proof.
equiv_via (im E).
- (* Goal: B <~> im E *)
apply (equiv_to_im _ un).
- (* Goal: im E <~> BAut (E x0) *)
apply equiv_im_f_comp_eq.
exact pc.
Defined.
: B <~> BAut (E x0).
Proof.
equiv_via (im E).
- (* Goal: B <~> im E *)
apply (equiv_to_im _ un).
- (* Goal: im E <~> BAut (E x0) *)
apply equiv_im_f_comp_eq.
exact pc.
Defined.
And the type families agree across this equivalence.
Theorem families_agree {B : Type} (x0 : B) (pc : pointed_connected B x0) (E : B → Type) (un : IsUnivalent E)
: E == BAut_pr1 (E x0) o (equiv_conn_BAut x0 pc E un).
Proof.
intro x.
reflexivity.
Qed.
: E == BAut_pr1 (E x0) o (equiv_conn_BAut x0 pc E un).
Proof.
intro x.
reflexivity.
Qed.