Library UniMath.CategoryTheory.catiso

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.whiskering.

Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.

Isomorphism of (pre)categories


Definition is_catiso {A B : precategory_data}
  (F : functor A B)
  := (fully_faithful F) × (isweq (functor_on_objects F)).

Definition catiso (A B : precategory_data)
  := total2 (λ F : functor A B, is_catiso F).

Lemma isaprop_is_catiso
  {A B : precategory_data}
  {F : functor A B}
  : isaprop (is_catiso F).
Show proof.
  apply isapropdirprod.
  - apply isaprop_fully_faithful.
  - apply isapropisweq.

Definition functor_from_catiso (A B : precategory_data)
  (F : catiso A B)
  : functor A B := pr1 F.
Coercion functor_from_catiso :
  catiso >-> functor.

Definition identity_catiso (A : precategory_data)
  : catiso A A.
Show proof.
  use tpair.
  - exact (functor_identity A).
  - use tpair.
    + apply identity_functor_is_fully_faithful.
    + apply idisweq.

Definition catiso_ob_weq {A B : precategory_data}
  (F : catiso A B)
  : (ob A) ≃ (ob B)
  := make_weq (functor_on_objects F) (pr2 (pr2 F)).

Definition catiso_to_precategory_ob_path {A B : precategory_data}
  (F : catiso A B)
  : ob A = ob B
  := (invmap (univalence _ _) (catiso_ob_weq F)).

Definition catiso_fully_faithful_weq {A B : precategory_data}
  (F : catiso A B)
  : forall a a' : A, (a --> a') ≃ (F a --> F a')
  := λ a a', (make_weq (functor_on_morphisms F) (pr1 (pr2 F) a a')).

Lemma catiso_fully_faithful_path {A B : precategory_data}
  (F : catiso A B)
  : forall a a' : A, (a --> a') = (F a --> F a').
Show proof.
  intros a a'.
  apply (invmap (univalence _ _)).
  apply (catiso_fully_faithful_weq F).

Construction of a map (catiso A B) -> (A = B)




Lemma correct_hom {A B : precategory_data}
  (F : catiso A B)
  : forall a a' : A,
      F a --> F a'
      = (eqweqmap (catiso_to_precategory_ob_path F) a) -->
        (eqweqmap (catiso_to_precategory_ob_path F) a').
Show proof.
  intros a a'.
  assert (W := (!(homotweqinvweq (univalence _ _)) (catiso_ob_weq F))).
  exact (maponpaths (λ T, (pr1weq T) a --> (pr1weq T) a') W ).

Lemma eqweq_ob_path_is_functor_app {A B : precategory_data}
  (F : catiso A B)
  : forall a : A, eqweqmap (catiso_to_precategory_ob_path F) a = F a.
Show proof.
  intros a.
  exact (! toforallpaths (λ _ : A, B) F
    (pr1 (eqweqmap (invmap (univalence A B) (catiso_ob_weq F))))
    (maponpaths pr1 (! homotweqinvweq (univalence A B) (catiso_ob_weq F))) a).

Lemma eqweq_ob_path_is_functor_app_compute
  (A B : precategory)
  (F : catiso A B)
  (a a' : A)
  (f : B ⟦ F a, F a' ⟧):
  eqweq_ob_path_is_functor_app F a =
  ! toforallpaths (λ _ : A, B) F
      (pr1weq (eqweqmap (invmap (univalence A B) (catiso_ob_weq F))))
      (maponpaths pr1weq (! homotweqinvweq (univalence A B) (catiso_ob_weq F))) a.
Show proof.
  unfold eqweq_ob_path_is_functor_app.
Abort.

Lemma eqweq_maponpaths_mor {A B : precategory}
  (F G : A ≃ B) (p : F = G) (a a' : A) (f : F a --> F a')
  : eqweqmap (maponpaths (λ T : A ≃ B, (pr1 T) a --> (pr1 T) a') p) f
    = (idtomor _ _ (!toforallpaths _ _ _ (maponpaths pr1 p) a))
      · f
      · (idtomor _ _ (toforallpaths _ _ _ (maponpaths pr1 p) a')).
Proof.
  induction p.
  rewrite id_left.
  rewrite id_right.
  reflexivity.

Lemma eqweq_correct_hom_is_comp {A B : precategory}
  (F : catiso A B)
  : forall a a' : A, forall f : F a --> F a',
      eqweqmap (correct_hom F _ _) f
    = (idtomor _ _ (eqweq_ob_path_is_functor_app F a))
      · f
      · (idtomor _ _ (!eqweq_ob_path_is_functor_app F a')).
Show proof.
  intros a a' f.
  rewrite (eqweq_maponpaths_mor _ _
             (! homotweqinvweq (univalence A B) (catiso_ob_weq F))
             a a').
  apply maponpaths. apply maponpaths.
  unfold eqweq_ob_path_is_functor_app.
  rewrite pathsinv0inv0.
  reflexivity.

Lemma eqweq_fully_faithful_is_functor_app {A B : precategory_data}
  (F : catiso A B)
  : forall a a' : A,
    eqweqmap (catiso_fully_faithful_path F a a')
    = catiso_fully_faithful_weq F _ _.
Show proof.
  intros a a'.
  unfold catiso_fully_faithful_path.

  assert (W := (@homotweqinvweq _ _ (univalence (a --> a') (F a --> F a')))).
  simpl in W.
  rewrite W.

  reflexivity.

Lemma transport_mor {A B : UU} (B1 : B -> B -> UU) (p : A = B) :
  forall a a' : A,
    B1 (eqweqmap p a) (eqweqmap p a')
  = (transportb (λ T, T -> T -> UU) p B1) a a'.
Show proof.
  induction p.
  reflexivity.

Lemma catiso_to_precategory_mor_path {A B : precategory_data}
  (F : catiso A B)
  : forall a a', (precategory_morphisms (C:=A)) a a'
  = transportb (λ T, T -> T -> UU) (catiso_to_precategory_ob_path F)
    (precategory_morphisms (C:=B)) a a'.
Show proof.
  intros a.
  intros a'.

  eapply pathscomp0. apply (catiso_fully_faithful_path F).
  eapply pathscomp0. apply correct_hom.
  eapply pathscomp0. apply transport_mor.

  reflexivity.

Lemma catiso_to_precategory_mor_path_funext {A B : precategory_data}
  (F : catiso A B)
  : (precategory_morphisms (C:=A))
  = transportb (λ T, T -> T -> UU) (catiso_to_precategory_ob_path F)
    (precategory_morphisms (C:=B)).
Show proof.
  apply (pr1 (weqfunextsec _ _ _)).
  intros a.
  apply (pr1 (weqfunextsec _ _ _)).
  intros a'.
  apply (catiso_to_precategory_mor_path F).

Definition catiso_to_precategory_ob_mor_path {A B : precategory_data}
  (F : catiso A B)
  : precategory_ob_mor_from_precategory_data A = precategory_ob_mor_from_precategory_data B
  := total2_paths_b (catiso_to_precategory_ob_path F) (catiso_to_precategory_mor_path_funext F).


Lemma transport_id {A0 B0 : UU} (p0 : A0 = B0)
  (A1 : A0 -> A0 -> UU) (B1 : B0 -> B0 -> UU) (p1 : A1 = transportb _ p0 B1)
  (idB : forall b : B0, B1 b b)
  : forall a : A0,
    (transportb (X := total2 (λ T, T -> T -> UU))
                (λ T, forall a, (pr2 T) a a)
                (total2_paths2_b p0 p1) idB) a
  = (eqweqmap ( (transport_mor B1 p0 _ _)
               @ !weqtoforallpaths _ _ _ (weqtoforallpaths _ _ _ p1 a) a))
    (idB (eqweqmap p0 a)).
Show proof.
  intro.
  induction p0.
  change (transportb _ _ _) with B1 in p1.
  induction p1.
  simpl.
  reflexivity.

Lemma correct_hom_on_id {A B : precategory}
  (F : catiso A B)
  : forall a,
    identity ((eqweqmap (catiso_to_precategory_ob_path F)) a) =
    (eqweqmap (correct_hom F a a)) (identity (F a)).
Show proof.
  intros a.

  apply pathsinv0.
  eapply pathscomp0. apply eqweq_correct_hom_is_comp.

  induction (eqweq_ob_path_is_functor_app F a).
  simpl.
  rewrite 2 id_right.
  reflexivity.

Lemma catiso_to_precategory_id_path {A B : precategory}
  (F : catiso A B)
  : forall a : A,
    (transportb (X := total2 (λ T, T -> T -> UU))
                (λ T, forall a, (pr2 T) a a)
                (total2_paths2_b (catiso_to_precategory_ob_path F)
                                 (catiso_to_precategory_mor_path_funext F))
     identity) a
   = identity a.
Show proof.
  intros a.

  eapply pathscomp0. apply transport_id.

  unfold catiso_to_precategory_mor_path_funext.
  unfold catiso_to_precategory_mor_path.
  unfold weqfunextsec.
  simpl (pr1 _).
  rewrite !(homotweqinvweq (weqtoforallpaths _ _ _)).

  rewrite pathscomp_inv.
  rewrite pathscomp_inv.
  rewrite path_assoc.
  rewrite path_assoc.
  rewrite pathscomp0rid.
  rewrite pathsinv0r.
  simpl.

  apply pathsweq1'.
  rewrite <- pathscomp_inv.
  rewrite eqweqmap_pathsinv0.
  rewrite invinv.

  rewrite <- eqweqmap_pathscomp0.

  rewrite (eqweq_fully_faithful_is_functor_app F a a).
  simpl.

  rewrite functor_id.
  apply correct_hom_on_id.

Lemma transport_comp_target {A0 B0 : UU} (p0 : A0 = B0)
  (A1 : A0 -> A0 -> UU) (B1 : B0 -> B0 -> UU) (p1 : A1 = transportb (λ T, T -> T -> UU) p0 B1)
  : forall a a' a'' : A0,
    ( B1 (eqweqmap p0 a) (eqweqmap p0 a')
      -> B1 (eqweqmap p0 a') (eqweqmap p0 a'')
      -> B1 (eqweqmap p0 a) (eqweqmap p0 a''))
  -> ( A1 a a' -> A1 a' a'' -> A1 a a'').
Show proof.
  intros a a' a''.
  intros Bhom.
  intros f g.

  set (X := λ a a', (transport_mor B1 p0 a a')
                    @ (! weqtoforallpaths _ _ _ (weqtoforallpaths _ _ _ p1 a) a') ).

  apply (eqweqmap (X a a'')).
  apply Bhom.

  apply (eqweqmap (! X a a')).
  exact f.

  apply (eqweqmap (! X a' a'')).
  exact g.

Lemma transport_comp {A0 B0 : UU} (p0 : A0 = B0)
  (A1 : A0 -> A0 -> UU) (B1 : B0 -> B0 -> UU) (p1 : A1 = transportb _ p0 B1)
  (compB : forall b b' b'' : B0, B1 b b' -> B1 b' b'' -> B1 b b'')
  : forall a a' a'' : A0,
      (transportb (X := total2 (λ T, T -> T -> UU))
                  (λ T, forall a b c, (pr2 T) a b -> (pr2 T) b c -> (pr2 T) a c)
                  (total2_paths2_b p0 p1) compB)
        a a' a''
    = transport_comp_target p0 A1 B1 p1 a a' a''
        (compB (eqweqmap p0 a) (eqweqmap p0 a') (eqweqmap p0 a'')).
Show proof.
  intros.
  induction p0.
  change (A1 = B1) in p1.
  induction p1.
  reflexivity.

Lemma correct_hom_on_comp {A B : precategory}
  (F : catiso A B)
  : forall a a' a'', forall f : F a --> F a', forall g : F a' --> F a'',
       (eqweqmap (correct_hom F _ _)) f
    · (eqweqmap (correct_hom F _ _)) g
    = (eqweqmap (correct_hom F _ _)) (f · g).
Show proof.
  intros a a' a'' f g.
  rewrite !eqweq_correct_hom_is_comp.
  induction (eqweq_ob_path_is_functor_app F a).
  induction (eqweq_ob_path_is_functor_app F a').
  induction (eqweq_ob_path_is_functor_app F a'').
  rewrite 3 id_left.
  simpl.
  rewrite 3 id_right.
  reflexivity.

Lemma catiso_to_precategory_comp_path {A B : precategory}
  (F : catiso A B)
  : forall a a' a'' : A,
    (transportb (X := total2 (λ T, T -> T -> UU))
                (λ T, forall a b c : (pr1 T), (pr2 T) a b -> (pr2 T) b c -> (pr2 T) a c)
                (total2_paths2_b (catiso_to_precategory_ob_path F)
                                 (catiso_to_precategory_mor_path_funext F))
     (@compose B)) a a' a''
   = (@compose A a a' a'').
Show proof.
  intros a a' a''.

  eapply pathscomp0. apply transport_comp.
  apply funextsec. intros f.
  apply funextsec. intros g.

  unfold transport_comp_target.

  unfold catiso_to_precategory_mor_path_funext.
  simpl.

  set (W := homotweqinvweq
              (weqtoforallpaths (λ _ : A, A -> UU)
                                precategory_morphisms
                                (transportb (λ T, T -> T -> UU)
                                            (catiso_to_precategory_ob_path F)
                                            precategory_morphisms))).
  simpl in W. rewrite !W. clear W.

  set (W := homotweqinvweq
              (weqtoforallpaths (λ _ : A, UU)
                                (precategory_morphisms a)
                                (transportb (λ T, T -> T -> UU)
                                            (catiso_to_precategory_ob_path F)
                                            precategory_morphisms a))).
  simpl in W. rewrite !W. clear W.

  set (W := homotweqinvweq
              (weqtoforallpaths (λ _ : A, UU)
                                (precategory_morphisms a')
                                (transportb (λ T, T -> T -> UU)
                                            (catiso_to_precategory_ob_path F)
                                            precategory_morphisms a'))).
  simpl in W. rewrite !W. clear W.

  unfold catiso_to_precategory_mor_path.
  rewrite !pathscomp0rid.
  rewrite !pathscomp_inv.
  rewrite !pathsinv0inv0.
  rewrite path_assoc.
  rewrite path_assoc.
  rewrite pathsinv0r.
  simpl.
  rewrite <- path_assoc.
  rewrite <- path_assoc.
  rewrite pathsinv0r.
  rewrite pathscomp0rid.
  rewrite <- path_assoc.
  rewrite <- path_assoc.
  rewrite pathsinv0r.
  rewrite pathscomp0rid.
  rewrite <- pathscomp_inv.

  apply pathsweq1'.
  rewrite eqweqmap_pathsinv0.
  rewrite invinv.

  rewrite <- !eqweqmap_pathscomp0.
  rewrite !eqweq_fully_faithful_is_functor_app.
  simpl.
  rewrite functor_comp.

  apply (correct_hom_on_comp F).

Lemma catiso_to_precategory_data_path {A B : precategory}
  (F : catiso A B)
  : precategory_data_from_precategory A
    = precategory_data_from_precategory B.
Show proof.
  destruct A as [[[Ao Am] [Ai Ac]] Aax].
  destruct B as [[[Bo Bm] [Bi Bc]] Bax].

  eapply total2_paths_b. Unshelve.
  2: { simpl. exact (catiso_to_precategory_ob_mor_path F). }
  apply pathsinv0.
  eapply pathscomp0.
  apply (transportb_dirprod _ _ _ _ _ (catiso_to_precategory_ob_mor_path F)).
  apply dirprodeq.
  - apply funextsec.
    intros a.
    apply (catiso_to_precategory_id_path F).
  - apply funextsec.
    intro.
    apply funextsec.
    intro.
    apply funextsec.
    intro.
    apply (catiso_to_precategory_comp_path F).

If either precategory has homsets, then an isomorphism between them becomes a path. This is essentially one half of univalence for categories.
Lemma catiso_to_precategory_path_f {A B : precategory}
  (hs : has_homsets A)
  (F : catiso A B)
  : A = B.
Show proof.
  use total2_paths_b.
  - exact (catiso_to_precategory_data_path F).
  - apply proofirrelevance, isaprop_is_precategory.
    apply hs.

Lemma catiso_to_precategory_path_b {A B : precategory}
  (hs : has_homsets B)
  (F : catiso A B)
  : A = B.
Show proof.
  use total2_paths_f.
  - exact (catiso_to_precategory_data_path F).
  - apply proofirrelevance, isaprop_is_precategory.
    apply hs.

A special case is that they both have homsets
Corollary catiso_to_category_path {A B : category}
  (F : catiso A B) : A = B.
Show proof.
  apply category_eq.
  apply catiso_to_precategory_data_path.
  assumption.

Definition inv_catiso
           {C D : category}
           (F : catiso C D)
  : D ⟶ C.
Show proof.
  use make_functor.
  - use tpair.
    + exact (invweq (catiso_ob_weq F)).
    + intros X Y f ; cbn.
      refine (invmap
                (catiso_fully_faithful_weq F
                                           (invmap (catiso_ob_weq F) X)
                                           (invmap (catiso_ob_weq F) Y))
                _).
      exact ((idtoiso (homotweqinvweq (catiso_ob_weq F) X))
               · f
               · idtoiso (!(homotweqinvweq (catiso_ob_weq F) Y))).
  - split.
    + intro X ; cbn.
      rewrite id_right.
      etrans.
      {
        apply maponpaths.
        exact (!(maponpaths pr1
                            (idtoiso_concat D _ _ _
                                            (homotweqinvweq (catiso_ob_weq F) X)
                                            (! homotweqinvweq (catiso_ob_weq F) X)))).
      }
      rewrite pathsinv0r ; cbn.
      apply invmap_eq ; cbn.
      rewrite functor_id.
      reflexivity.
    + intros X Y Z f g ; cbn.
      apply invmap_eq ; cbn.
      rewrite functor_comp.
      pose (homotweqinvweq
              (catiso_fully_faithful_weq F
                                         (invmap (catiso_ob_weq F) X)
                                         (invmap (catiso_ob_weq F) Y))) as p.
      cbn in p.
      rewrite p ; clear p.
      pose (homotweqinvweq
              (catiso_fully_faithful_weq F
                                         (invmap (catiso_ob_weq F) Y)
                                         (invmap (catiso_ob_weq F) Z))) as p.
      cbn in p.
      rewrite p ; clear p.
      rewrite <- !assoc.
      repeat (apply (maponpaths (λ z, _ · (f · z)))).
      refine (!(id_left _) @ _).
      rewrite !assoc.
      repeat (apply (maponpaths (λ z, z · _))).
      rewrite idtoiso_inv.
      cbn.
      rewrite z_iso_after_z_iso_inv.
      reflexivity.

Definition adj_equivalence_of_cats_to_cat_iso
      {C D : category}
      {F : functor C D}
      (Fa : adj_equivalence_of_cats F)
      (Cuniv : is_univalent C) (Duniv : is_univalent D)
  : catiso C D.
Show proof.
  exists F.
  split.
  - apply fully_faithful_from_equivalence, Fa.
  - apply(weq_on_objects_from_adj_equiv_of_cats C D Cuniv Duniv F Fa).

More operations on isomorphisms of categories
Section CatIso.
  Context {C D : setcategory}
          (F : catiso C D).

  Definition catiso_to_fully_faithful
    : fully_faithful F.
  Show proof.
    intros x y.
    apply F.

  Definition catiso_inv_ob
             (y : D)
    : C
    := invmap (catiso_ob_weq F) y.

  Proposition catiso_catiso_inv_ob
              (y : D)
    : F (catiso_inv_ob y) = y.
  Show proof.
    apply (homotweqinvweq (catiso_ob_weq F) y).

  Proposition catiso_inv_ob_catiso
              (x : C)
    : catiso_inv_ob (F x) = x.
  Show proof.
    apply (homotinvweqweq (catiso_ob_weq F) x).

  Proposition catiso_reflect_ob_eq
              {x y : C}
              (p : F x = F y)
    : x = y.
  Show proof.
    refine (!(catiso_inv_ob_catiso x) @ _ @ catiso_inv_ob_catiso y).
    apply maponpaths.
    exact p.

  Proposition catiso_inv_hom_idtoiso
              {x y : C}
              (p : F x = F y)
    : fully_faithful_inv_hom catiso_to_fully_faithful x y (idtoiso p)
      =
      idtoiso (catiso_reflect_ob_eq p).
  Show proof.
    refine (!_ @ fully_faithful_inv_hom_is_inv catiso_to_fully_faithful _).
    apply maponpaths.
    refine (!(pr1_maponpaths_idtoiso F (catiso_reflect_ob_eq p)) @ _).
    apply setcategory_eq_idtoiso.

  Definition catiso_inv_mor
             {y₁ y₂ : D}
             (f : y₁ --> y₂)
    : catiso_inv_ob y₁ --> catiso_inv_ob y₂
    := fully_faithful_inv_hom
         catiso_to_fully_faithful
         _ _
         (idtoiso (catiso_catiso_inv_ob y₁)
          · f
          · idtoiso (!(catiso_catiso_inv_ob y₂))).

  Proposition catiso_inv_mor_cat_iso
              {x₁ x₂ : C}
              (f : x₁ --> x₂)
    : catiso_inv_mor (#F f)
      =
      idtoiso (catiso_inv_ob_catiso x₁)
      · f
      · idtoiso (!(catiso_inv_ob_catiso x₂)).
  Show proof.
    unfold catiso_inv_mor.
    rewrite !fully_faithful_inv_comp.
    rewrite fully_faithful_inv_hom_is_inv.
    rewrite !catiso_inv_hom_idtoiso.
    apply setcategory_eq_idtoiso_comp.

  Proposition catiso_catiso_inv_mor
              {y₁ y₂ : D}
              (f : y₁ --> y₂)
    : #F (catiso_inv_mor f)
      =
      idtoiso (catiso_catiso_inv_ob y₁)
      · f
      · idtoiso (!(catiso_catiso_inv_ob y₂)).
  Show proof.
    apply functor_on_fully_faithful_inv_hom.

  Proposition catiso_inv_mor_eq
              {y₁ y₂ : D}
              (f : y₁ --> y₂)
              (g : catiso_inv_ob y₁ --> catiso_inv_ob y₂)
              (p : f
                   =
                   idtoiso (!(catiso_catiso_inv_ob y₁))
                   · #F g
                   · idtoiso (catiso_catiso_inv_ob y₂))
    : catiso_inv_mor f = g.
  Show proof.
    use (invmaponpathsweq
           (weq_from_fully_faithful catiso_to_fully_faithful _ _)).
    cbn -[catiso_inv_mor].
    rewrite catiso_catiso_inv_mor.
    rewrite p.
    rewrite !assoc.
    etrans.
    {
      etrans.
      {
        do 3 apply maponpaths_2.
        refine (!_).
        apply pr1_idtoiso_concat.
      }
      rewrite pathsinv0r ; cbn.
      rewrite id_left.
      rewrite !assoc'.
      etrans.
      {
        apply maponpaths.
        refine (!_).
        apply (pr1_idtoiso_concat (catiso_catiso_inv_ob y₂)).
      }
      rewrite pathsinv0r ; cbn.
      apply id_right.
    }
    apply idpath.
End CatIso.