Library UniMath.CategoryTheory.Core.Univalence

Univalent categories (AKA saturated categories)

Contents


Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.

Local Open Scope cat.

Univalent categories: idtoiso is an equivalence


Definition idtoiso {C : precategory} {a b : ob C}:
      a = b -> z_iso a b.
Show proof.
  intro H.
  induction H.
  exact (identity_z_iso a).

Proposition idtoiso_idpath
            {C : category}
            (x : C)
  : pr1 (idtoiso (idpath x)) = identity x.
Show proof.
  apply idpath.

Definition is_univalent (C : category) :=
   (a b : ob C), isweq (fun p : a = b => idtoiso p).


Lemma eq_idtoiso_idtomor {C:precategory} (a b:ob C) (e:a = b) :
    pr1 (idtoiso e) = idtomor _ _ e.
Show proof.
  destruct e; reflexivity.

Lemma isaprop_is_univalent (C : category) : isaprop (is_univalent C).
Show proof.
  apply impred.
  intro a.
  apply impred.
  intro b.
  apply isapropisweq.

Definition univalent_category : UU := C : category, is_univalent C.

Definition make_univalent_category (C : category) (H : is_univalent C) : univalent_category
  := tpair _ C H.

#[reversible] Coercion univalent_category_to_category (C : univalent_category) : category := pr1 C.

#[reversible] Coercion univalent_category_has_homsets (C : univalent_category)
  : has_homsets C
  := pr2 (pr1 C).

Definition univalent_category_is_univalent (C : univalent_category) : is_univalent C := pr2 C.

Lemma univalent_category_has_groupoid_ob (C : univalent_category): isofhlevel 3 (ob C).
Show proof.
  change (isofhlevel 3 C) with
        ( a b : C, isofhlevel 2 (a = b)).
  intros a b.
  apply (isofhlevelweqb _ (tpair _ _ (pr2 C a b))).
  apply isaset_z_iso.

Definition of isotoid


Definition isotoid (C : category) (H : is_univalent C) {a b : ob C}:
      z_iso a b -> a = b := invmap (make_weq _ (H a b)).

Lemma idtoiso_isotoid (C : category) (H : is_univalent C) (a b : ob C)
    (f : z_iso a b) : idtoiso (isotoid _ H f) = f.
Show proof.
  unfold isotoid.
  set (Hw := homotweqinvweq (make_weq idtoiso (H a b))).
  simpl in Hw.
  apply Hw.

Lemma isotoid_idtoiso (C : category) (H : is_univalent C) (a b : ob C)
    (p : a = b) : isotoid _ H (idtoiso p) = p.
Show proof.
  unfold isotoid.
  set (Hw := homotinvweqweq (make_weq idtoiso (H a b))).
  simpl in Hw.
  apply Hw.

Properties of idtoiso and isotoid


Definition double_transport {C : precategory_ob_mor} {a a' b b' : ob C}
   (p : a = a') (q : b = b') (f : a --> b) : a' --> b' :=
  transportf (λ c, a' --> c) q (transportf (λ c, c --> b) p f).

Lemma double_transport_transpose
  {C : precategory_ob_mor}
  {a a' b b' : C} {f : a --> b} {g : a' --> b'}
  {px : a' = a} {py : b' = b}
  : double_transport px py g = f -> g = double_transport (!px) (!py) f.
Show proof.
  intro H.
  destruct H.
  destruct px, py.
  reflexivity.

Lemma double_transport_transpose'
  {C : precategory_ob_mor}
  {a a' b b' : C} {f : a' --> b'} {g : a --> b}
  {px : a' = a} {py : b' = b}
  : f = double_transport (!px) (!py) g -> double_transport px py f = g.
Show proof.
  intro H.
  destruct (!H).
  destruct px, py.
  reflexivity.

Lemma double_transport_compose
  {C : precategory}
  {a a' b b' c c' : C} {f : a --> b} {g : b --> c}
  {px : a = a'} {py : b = b'} {pz : c = c'}
  : double_transport px py f
  · double_transport py pz g =
  double_transport px pz (f · g).
Show proof.
  unfold double_transport.
  destruct px, py, pz.
  reflexivity.

Lemma idtoiso_postcompose (C : precategory) (a b b' : ob C)
  (p : b = b') (f : a --> b) :
      f · idtoiso p = transportf (λ b, a --> b) p f.
Show proof.
  destruct p.
  apply id_right.

Lemma idtoiso_postcompose_iso (C : category) (a b b' : ob C)
  (p : b = b') (f : z_iso a b) :
    z_iso_comp f (idtoiso p) = transportf (λ b, z_iso a b) p f.
Show proof.
  destruct p.
  apply z_iso_eq.
  apply id_right.

Lemma idtoiso_precompose (C : precategory) (a a' b : ob C)
  (p : a = a') (f : a --> b) :
      (idtoiso (!p)) · f = transportf (λ a, a --> b) p f.
Show proof.
  destruct p.
  apply id_left.

Lemma idtoiso_precompose_iso (C : category) (a a' b : ob C)
  (p : a = a') (f : z_iso a b) :
      z_iso_comp (idtoiso (!p)) f = transportf (λ a, z_iso a b) p f.
Show proof.
  destruct p.
  apply z_iso_eq.
  apply id_left.

Lemma double_transport_idtoiso (C : precategory) (a a' b b' : ob C)
  (p : a = a') (q : b = b') (f : a --> b) :
  double_transport p q f = inv_from_z_iso (idtoiso p) · f · idtoiso q.
Show proof.
  destruct p.
  destruct q.
  intermediate_path (identity _ · f).
  - apply pathsinv0; apply id_left.
  - apply pathsinv0; apply id_right.

Lemma idtoiso_inv (C : category) (a a' : ob C)
  (p : a = a') : idtoiso (!p) = z_iso_inv_from_z_iso (idtoiso p).
Show proof.
  destruct p.
  simpl. apply z_iso_eq.
  apply idpath.

Lemma idtoiso_concat (C : category) (a a' a'' : ob C)
  (p : a = a') (q : a' = a'') :
  idtoiso (p @ q) = z_iso_comp (idtoiso p) (idtoiso q).
Show proof.
  destruct p.
  destruct q.
  apply z_iso_eq.
  simpl; apply pathsinv0, id_left.

Definition pr1_idtoiso_concat
           {C : category}
           {x y z : C}
           (f : x = y) (g : y = z)
  : pr1 (idtoiso (f @ g)) = pr1 (idtoiso f) · pr1 (idtoiso g).
Show proof.
  exact (maponpaths pr1 (idtoiso_concat _ _ _ _ f g)).

Lemma idtoiso_inj (C : category) (H : is_univalent C) (a a' : ob C)
   (p p' : a = a') : idtoiso p = idtoiso p' -> p = p'.
Show proof.
  apply invmaponpathsincl.
  apply isinclweq.
  apply H.

Lemma isotoid_inj (C : category) (H : is_univalent C) (a a' : ob C)
   (f f' : z_iso a a') : isotoid _ H f = isotoid _ H f' -> f = f'.
Show proof.
  apply invmaponpathsincl.
  apply isinclweq.
  apply isweqinvmap.

Lemma isotoid_comp (C : category) (H : is_univalent C) (a b c : ob C)
  (e : z_iso a b) (f : z_iso b c) :
  isotoid _ H (z_iso_comp e f) = isotoid _ H e @ isotoid _ H f.
Show proof.
  apply idtoiso_inj.
    assumption.
  rewrite idtoiso_concat.
  repeat rewrite idtoiso_isotoid.
  apply idpath.

Lemma isotoid_identity_iso (C : category) (H : is_univalent C) (a : C) :
  isotoid _ H (identity_z_iso a) = idpath _ .
Show proof.
  apply idtoiso_inj; try assumption.
  rewrite idtoiso_isotoid;
  apply idpath.

Lemma inv_isotoid (C : category) (H : is_univalent C) (a b : C)
    (f : z_iso a b) : ! isotoid _ H f = isotoid _ H (z_iso_inv_from_z_iso f).
Show proof.
  apply idtoiso_inj; try assumption.
  rewrite idtoiso_isotoid.
  rewrite idtoiso_inv.
  rewrite idtoiso_isotoid.
  apply idpath.

Lemma transportf_isotoid (C : category) (H : is_univalent C)
   (a a' b : ob C) (p : z_iso a a') (f : a --> b) :
 transportf (λ a0 : C, a0 --> b) (isotoid C H p) f = inv_from_z_iso p · f.
Show proof.
  rewrite <- idtoiso_precompose.
  rewrite idtoiso_inv.
  rewrite idtoiso_isotoid.
  apply idpath.

Lemma transportf_isotoid' (C : category) (H : is_univalent C)
   (a b b' : ob C) (p : z_iso b b') (f : a --> b) :
 transportf (λ a0 : C, a --> a0) (isotoid C H p) f = f · p.
Show proof.
  rewrite <- idtoiso_postcompose.
  apply maponpaths.
  rewrite idtoiso_isotoid.
  apply idpath.

Lemma transportb_isotoid (C : category) (H : is_univalent C)
  (a b b' : ob C) (p : z_iso b b') (f : a --> b') :
  transportb (λ b0 : C, a --> b0) (isotoid C H p) f = f · inv_from_z_iso p.
Show proof.
  apply pathsinv0.
  apply transportb_transpose_right.
  change (precategory_morphisms a) with (λ b0 : C, a --> b0).
  rewrite transportf_isotoid'.
  rewrite <- assoc.
  rewrite z_iso_after_z_iso_inv.
  apply id_right.

Lemma transportf_isotoid_dep (C : precategory)
   (a a' : C) (p : a = a') (f : c, a --> c) :
 transportf (λ x : C, c, x --> c) p f = λ c, idtoiso (!p) · f c.
Show proof.
  destruct p.
  simpl.
  apply funextsec.
  intro.
  rewrite id_left.
  apply idpath.

Lemma forall_isotoid (A : category) (a_is : is_univalent A)
      (a a' : A) (P : z_iso a a' -> UU) :
  ( e, P (idtoiso e)) i, P i.
Show proof.
  intros H i.
  rewrite <- (idtoiso_isotoid _ a_is).
  apply H.

Lemma transportf_isotoid_dep' (J : UU) (C : precategory) (F : J -> C)
  (a a' : C) (p : a = a') (f : c, a --> F c) :
  transportf (λ x : C, c, x --> F c) p f = λ c, idtoiso (!p) · f c.
Show proof.
  now destruct p; apply funextsec; intro x; rewrite id_left.

 Lemma transportf_isotoid_dep'' (J : UU) (C : precategory) (F : J -> C)
   (a a' : C) (p : a = a') (f : c, F c --> a) :
   transportf (λ x : C, c, F c --> x) p f = λ c, f c · idtoiso p.
Show proof.
  now destruct p; apply funextsec; intro x; rewrite id_right.