Library Univalence.components

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) := (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:  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. *)

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 s1C (T s1))
C T
(fun s1idmap)
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 ( 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 : 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) : ( 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.

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) := (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.

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 ( 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 = x0p^ @ 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 ( 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.

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 ( := pi0_functor f).
equiv_via {y : Y & {s : Pi0 X & s = tr y}}.
- (* Goal: {y : Y & merely {s : Pi0 X & s = tr y}} <~> {y : Y & {s : Pi0 X & tr y = 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 & s = tr y} *)
apply (isembedding_isembed _ E).
- (* Goal: {y : Y & {s : Pi0 X & s = tr y}} <~> {s : Pi0 X & {y : Y & tr y = s}} *)
apply (equiv_composeR´ (equiv_sigma_symm _)).
(* Goal: {b : Pi0 X & {a : Y & b = tr a}} <~> {s : Pi0 X & {y : Y & tr y = 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) := 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.

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 & comp (T )}(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) := (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 FunextIsEquiv 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: 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.

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 = .
Definition BAut´ ( : Pi0 Type) := comp .

A variation, closer to the homotopy theoretic notion.
Definition BAutEq (F : Type) := (X : Type), merely (X <~> F).

With this notation, univalent_iff_canon says that a univalent type family is equivalent to a coproduct of BAut´ '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.

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´ and BAut F are univalent.
BAut´ is a sigma type coming from the type family Type Type sending Z to tr Z = , and pr1 is the natural map to Type. This is what we called comp_incl earlier.
Definition BAut´_pr1 ( : Pi0 Type) : BAut´ Type := comp_incl .

The natural type family over BAut´ is univalent, since the fibres are hProps.
Theorem isunivalent_baut´_pr1 ( : Pi0 Type) : IsUnivalent (BAut´_pr1 ).
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´ 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.