Require Import HoTT.
(** * Embeddings *)
(** [IsEmbed] is what is called an Embedding in the HoTT book, and
[IsUnivalent] is the special case where [Y = Type]. *)
Definition IsEmbed {X Y : Type} (f : X -> Y) := forall (x0 x1 : X), IsEquiv (@ap X Y f x0 x1).
(** 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: [forall 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 : forall (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) := forall y : Y, merely (exists 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: [forall 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: [forall 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 : exists s1 : S1, C(T(s1)))
: (exists 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.
(** * Every type is a "coproduct" of its components. *)
(** The type of components of [X]. *)
Definition Pi0 (X : Type) : Type := Tr 0 X.
(** [Pi0 X] is a set. *)
Theorem isset_pi0 (X : Type) : IsHSet (Pi0 X).
Proof.
exact (istrunc_truncation 0 X).
Qed.
(** [Pi0] is a functor. *)
Definition pi0_functor {X Y : Type} (f : X -> Y) : Pi0 X -> Pi0 Y := Trunc_functor 0 f.
(** Each term of [Pi0 X] determines a component of [X]. This is just the
homotopy fibre of tr. *)
Definition comp {X : Type} (c : Pi0 X) : Type := { x : X & tr x = c }.
(** The map sending a point to its component. *)
Definition comp_tr {X : Type} (x0 : X) : Type := comp (tr x0).
(** Every term of [Pi0 X] is of the form [tr x0]. Not used elsewhere. *)
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.
(** Similarly, every [comp c] is equivalent to a [comp_tr x0]. *)
Theorem comp_equiv_comp_tr {X : Type} (c : Pi0 X) : merely (exists x0 : X, (comp c) <~> (comp_tr x0)).
Proof.
strip_truncations.
apply tr.
exact (c; equiv_idmap).
Qed.
(** The inclusion of a component into the original type. *)
Definition comp_incl {X : Type} (c : Pi0 X) : comp c -> X := pr1.
(** 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.
(** We now study the coproduct of the components of a type. *)
Definition natmap (X : Type) (u : exists c : Pi0 X, comp c) : X := u.2.1.
(** 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) : (exists c : Pi0 X, comp c) <~> X
:= BuildEquiv _ _ (natmap X) (isequiv_natmap X).
(* This is really just [equiv_fibration_replacement (@tr 0 X)], but the above
proof is easier to understand. *)
(** 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)).
exists ((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. *)
Definition comp_eq {X : Type} (x0 : X) : Type := { x : X & merely (x = x0) }.
(** 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.
(** We can show without Univalence that the [comp_eq] components are connected. *)
Definition MyIsConn (A : Type) := forall (a b : A), merely (a = b).
Theorem myisconn_comp_eq {X : Type} (x0 : X) : MyIsConn (comp_eq x0).
Proof.
unfold MyIsConn.
(* Goal: [forall 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. *)
(** Some of the following is in Modality.v, but is hard to understand,
so I'll spell out our special case. *)
Definition im {X Y : Type} (f : X -> Y) := { y : Y & merely (exists 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].
exists 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) := forall (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.
(** For our main result, we need to show that the following is equivalent to [im f]. *)
Definition im' {X Y : Type} (f : X -> Y) := { y : Y & merely (exists 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}] *)
exists (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 & (exists 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.
(** * The characterization of embeddings as inclusions of a subset of the components. *)
Definition IsCanon {X Y : Type} (f : X -> Y) := exists S : Type, exists HS : IsHSet S,
exists T : S -> Pi0 Y, exists ET : IsEmbed T, exists e : X -> { s : S | comp (T s) },
exists 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.
exists (Pi0 X). (* S *)
exists (isset_pi0 _). (* HS *)
exists (pi0_functor f). (* T *)
pose (ET := isembed_pi0_isembed f E).
exists ET. (* ET *)
exists ((equiv_im'_components f ET) oE (equiv_im_im' f) oE (equiv_to_im f E)). (* e *)
exists _. (* 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.
(** * The characterization of univalent type families. *)
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) := forall (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) := forall (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.
(** 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: [IsUnivalentEq E <-> IsUnivalent E] *)
apply iff_equiv.
symmetry.
apply equiv_univalent_univalenteq.
- (* Goal: [IsUnivalent E <-> IsCanon E] *)
apply univalent_iff_canon.
Qed.
(** * Expressing the result using [BAut]. *)
(** There are three ways one might define [BAut]: *)
(** [BAut] is defined in Spaces.BAut as those [X] merely equal to [F]. *)
Definition check_BAut (F : Type) : BAut F = comp_eq F := idpath.
(** Or we can take those [X] such that [tr X = F']. *)
Definition BAut' (F' : Pi0 Type) := comp F'.
(** A variation, closer to the homotopy theoretic notion. *)
Definition BAutEq (F : Type) := exists (X : Type), merely (X <~> F).
(** 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.
exists (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.
(** 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.
(** 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. *)
Definition BAut'_pr1 (F' : Pi0 Type) : BAut' F' -> Type := comp_incl F'.
(** The natural type family over [BAut' F'] is univalent, since
the fibres are hProps. *)
Theorem isunivalent_baut'_pr1 (F' : Pi0 Type) : IsUnivalent (BAut'_pr1 F').
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.
(** 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]. *)
(** 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.
(** 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.