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.