Library UniMath.Bicategories.WkCatEnrichment.Cat

Require Import UniMath.Foundations.PartD.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.categories.StandardCategories. Require Import UniMath.CategoryTheory.HorizontalComposition.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.
Local Open Scope cat.
Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory.


Definition Catlike_associator ( a b c d : precategory )
   (hsB : has_homsets b) (hsC : has_homsets c) (hsD : has_homsets d) :
   nat_trans
     (functor_composite
        (pair_functor
           (functor_identity (functor_precategory a b hsB))
           (functorial_composition b c d hsC hsD))
        (functorial_composition a b d hsB hsD))
     (functor_composite
        (precategory_binproduct_assoc (functor_precategory a b hsB)
           (functor_precategory b c hsC)
           (functor_precategory c d hsD))
        (functor_composite
           (pair_functor
              (functorial_composition a b c hsB hsC)
              (functor_identity (functor_precategory c d hsD)))
           (functorial_composition a c d hsC hsD))).
Proof.
  use tpair.
  -
    

    intros x.
    simpl.

    ∃ (λ x, identity _).

    intros oba oba' f.
    use (id_right _ @ !(id_left _)).

  -
    intros [F [G H]].
    intros [F' [G' H']].
    intros [f [g h]].

    apply nat_trans_eq. exact hsD.
    intros oba.

    simpl.

    rewrite id_right.
    rewrite id_left.

    rewrite functor_comp.
    rewrite assoc.
    reflexivity.
Defined.

Definition Catlike_associator_is_iso ( a b c d : precategory )
  (hsB : has_homsets b) (hsC : has_homsets c) (hsD : has_homsets d) :
  ∏ f g h, is_iso (Catlike_associator a b c d hsB hsC hsD
                    (make_precatbinprod f (make_precatbinprod g h))).
Proof.
  intros f g h.
  apply functor_iso_if_pointwise_iso.
  intros oba.
  apply (identity_is_iso d).
Defined.

Definition Catlike_left_unitor (a b : precategory) (hsA : has_homsets a) (hsB : has_homsets b) :
  nat_trans
     (functor_composite
        (bindelta_pair_functor
           (functor_composite (functor_to_unit (functor_precategory a b hsB))
              (constant_functor unit_category (functor_precategory a a hsA) (functor_identity a)))
           (functor_identity (functor_precategory a b hsB)))
        (functorial_composition a a b hsA hsB))
     (functor_identity (functor_precategory a b hsB)).
Proof.
  use tpair.
  -
    intros x.
    ∃ (λ x, identity _).
    intros oba oba' f.
    exact (id_right _ @ !(id_left _)).

  -
    intros F F' f.

    apply nat_trans_eq. exact hsB.
    intros oba.

    simpl.
    rewrite id_right.
    rewrite id_left.
    rewrite functor_id.
    rewrite id_right.
    reflexivity.
Defined.

Definition Catlike_left_unitor_is_iso (a b : precategory)
  (hsA : has_homsets a) (hsB : has_homsets b) :
  ∏ f, is_iso (Catlike_left_unitor a b hsA hsB f).
Proof.
  intros f.
  apply functor_iso_if_pointwise_iso.
  intros oba.
  apply (identity_is_iso b).
Defined.

Definition Catlike_right_unitor (a b : precategory) (hsB : has_homsets b) :
  nat_trans
     (functor_composite
        (bindelta_pair_functor (functor_identity (functor_precategory a b hsB))
           (functor_composite (functor_to_unit (functor_precategory a b hsB))
              (constant_functor unit_category (functor_precategory b b hsB) (functor_identity b))))
        (functorial_composition a b b hsB hsB))
     (functor_identity (functor_precategory a b hsB)).
Proof.
  use tpair.   - intros x.
    ∃ (λ x, identity _).
    intros oba oba' f.
    exact (id_right _ @ !(id_left _)).

  - intros F F' f.
    apply nat_trans_eq. exact hsB.
    intros oba.

    simpl.
    rewrite (id_right _).
    rewrite (id_left _).
    reflexivity.
Defined.

Definition Catlike_right_unitor_is_iso (a b : precategory) (hsB : has_homsets b) :
  ∏ f, is_iso (Catlike_right_unitor a b hsB f).
Proof.
  intros f.
  apply functor_iso_if_pointwise_iso.
  intros oba.
  apply (identity_is_iso b).
Defined.

Definition Catlike_pentagon ( a b c d e : precategory )
  (hsB : has_homsets b) (hsC : has_homsets c) (hsD : has_homsets d)
  (hsE : has_homsets e) :
  ∏ k h g f,
  (Catlike_associator a b c e _ _ _)
     (make_precatbinprod k
        (make_precatbinprod h ((functorial_composition c d e hsD _) (make_dirprod g f)))) ·
   (Catlike_associator a c d e _ _ _)
     (make_precatbinprod ((functorial_composition a b c hsB hsC) (make_dirprod k h))
        (make_precatbinprod g f))
  = (functor_on_morphisms (functorial_composition a b e hsB hsE)
      (precatbinprodmor (identity k)
         ((Catlike_associator b c d e _ _ _) (make_precatbinprod h (make_precatbinprod g f)))) ·
    (Catlike_associator a b d e _ _ _)
      (make_precatbinprod k
         (make_precatbinprod ((functorial_composition b c d _ _) (make_dirprod h g)) f))) ·
   functor_on_morphisms (functorial_composition a d e _ _)
     (precatbinprodmor
        ((Catlike_associator a b c d _ _ _) (make_precatbinprod k (make_precatbinprod h g)))
        (identity f)).
Proof.
  intros k h g f.
  apply nat_trans_eq. exact hsE.

  intros oba.
  simpl.

  repeat rewrite functor_id.
  repeat rewrite (id_left _).
  reflexivity.
Defined.

Definition Catlike_triangle ( a b c : precategory )
  (hsB : has_homsets b) (hsC : has_homsets c) :
   ∏ f g, functor_on_morphisms (functorial_composition a b c _ _)
                               (precatbinprodmor (identity f) (Catlike_left_unitor b c _ hsC g))
   =
      (Catlike_associator a b b c hsB _ _
        (make_precatbinprod f (make_precatbinprod (functor_identity_as_ob b hsB) g)))
   · functor_on_morphisms (functorial_composition a b c _ _)
                           (precatbinprodmor (Catlike_right_unitor a b _ f) (identity g)).
Proof.
  intros f g.
  apply nat_trans_eq. exact hsC.
  intros oba.
  simpl.
  repeat rewrite functor_id.
  repeat rewrite (id_left _).
  reflexivity.
Defined.


Definition PreCat_1mor_2mor : prebicategory_ob_hom.
Proof.
  ∃ category.
  intros a b.
  exact (functor_precategory a b (homset_property b)).
Defined.

Definition PreCat_id_comp : prebicategory_id_comp.
Proof.
  ∃ PreCat_1mor_2mor.
  split.
  - simpl.
    exact functor_identity.
  - simpl.
    intros a b c.
    exact (functorial_composition a b c (homset_property b)
                                        (homset_property c)).
Defined.

Definition PreCat_data : prebicategory_data.
Proof.
  unfold prebicategory_data.
  ∃ PreCat_id_comp.
  repeat split.
  - intros.
    simpl in a,b,c,d.
    exact (Catlike_associator a b c d (homset_property b)
                                      (homset_property c)
                                      (homset_property d)).
  - intros.
    simpl in a, b.
    exact (Catlike_left_unitor a b (homset_property a)
                                   (homset_property b)).
  - intros.
    simpl in a, b.
    exact (Catlike_right_unitor a b (homset_property b)).
Defined.

Definition PreCat_has_2mor_set : has_2mor_sets PreCat_data.
Proof.
  unfold has_2mor_sets.
  intros a b f g.
  apply isaset_nat_trans.
  exact (homset_property b).
Defined.

Definition PreCat_associator_and_unitors_are_iso : associator_and_unitors_are_iso PreCat_data.
Proof.
  repeat split.
  - intros a b c d.
    apply Catlike_associator_is_iso.
  - intros a b.
    apply Catlike_left_unitor_is_iso.
  - intros a b.
    apply Catlike_right_unitor_is_iso.
Defined.

Definition PreCat_coherence : prebicategory_coherence PreCat_data.
Proof.
  unfold prebicategory_coherence.
  split.
  - intros a b c d e.
    apply Catlike_pentagon.
  - intros a b c.
    apply Catlike_triangle.
Defined.

Definition PreCat : prebicategory.
Proof.
  use tpair.
  exact PreCat_data.
  split.
  exact PreCat_has_2mor_set.
  split.
  exact PreCat_associator_and_unitors_are_iso.
  exact PreCat_coherence.
Defined.


Definition Cat_1mor_2mor : prebicategory_ob_hom.
Proof.
  ∃ univalent_category.
  intros a b.
  exact (functor_precategory a b (univalent_category_has_homsets b)).
Defined.

Definition Cat_id_comp : prebicategory_id_comp.
Proof.
  ∃ Cat_1mor_2mor.
  split.
  - simpl.
    exact functor_identity.
  - simpl.
    intros a b c.
    exact (functorial_composition a b c (univalent_category_has_homsets b)
                                        (univalent_category_has_homsets c)).
Defined.

Definition Cat_data : prebicategory_data.
Proof.
  unfold prebicategory_data.
  ∃ Cat_id_comp.
  repeat split.
  - intros.
    simpl in a,b,c,d.
    exact (Catlike_associator a b c d (univalent_category_has_homsets b)
                                      (univalent_category_has_homsets c)
                                      (univalent_category_has_homsets d)).
  - intros.
    simpl in a, b.
    exact (Catlike_left_unitor a b (univalent_category_has_homsets a)
                                   (univalent_category_has_homsets b)).
  - intros.
    simpl in a, b.
    exact (Catlike_right_unitor a b (univalent_category_has_homsets b)).
Defined.

Definition Cat_has_2mor_set : has_2mor_sets Cat_data.
Proof.
  unfold has_2mor_sets.
  intros a b f g.
  apply isaset_nat_trans.
  exact (univalent_category_has_homsets b).
Defined.

Definition Cat_associator_and_unitors_are_iso : associator_and_unitors_are_iso Cat_data.
Proof.
  repeat split.
  - intros a b c d.
    apply Catlike_associator_is_iso.
  - intros a b.
    apply Catlike_left_unitor_is_iso.
  - intros a b.
    apply Catlike_right_unitor_is_iso.
Defined.

Definition Cat_coherence : prebicategory_coherence Cat_data.
Proof.
  split.
  - intros a b c d e.
    apply Catlike_pentagon.
  - intros a b c.
    apply Catlike_triangle.
Defined.

Definition Cat_prebicategory : prebicategory.
Proof.
  use tpair.
  exact Cat_data.
  unfold is_prebicategory.
  split.
  exact Cat_has_2mor_set.
  split.
  exact Cat_associator_and_unitors_are_iso.
  exact Cat_coherence.
Defined.

Definition Cat_has_homcats : has_homcats Cat_prebicategory.
Proof.
  unfold has_homcats.
  intros a b.
  apply is_univalent_functor_category.
Defined.