Library UniMath.Bicategories.WkCatEnrichment.Cat

**********************************************************
Mitchell Riley
June 2016
I am very grateful to Peter LeFanu Lumsdaine, whose unreleased bicategories code strongly influenced the proofs in this file.

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 : category )
  :
   nat_trans
     (functor_composite
        (pair_functor
           (functor_identity (functor_category a b))
           (functorial_composition b c d ))
        (functorial_composition a b d ))
     (functor_composite
        (precategory_binproduct_assoc (functor_category a b )
           (functor_category b c)
           (functor_category c d ))
        (functor_composite
           (pair_functor
              (functorial_composition a b c )
              (functor_identity (functor_category c d)))
           (functorial_composition a c d ))).
Show proof.
  use tpair.
  -
    

    intros x.
    simpl.

    exists (λ 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_alt).
    intros oba.

    simpl. do 2 (unfold horcomp_data; simpl).

    rewrite id_right.
    rewrite id_left.

    rewrite (functor_comp H).
    rewrite assoc.
    apply idpath.

Definition Catlike_associator_is_iso ( a b c d : category )
  : ∏ f g h, is_iso (Catlike_associator a b c d
                    (make_catbinprod f (make_catbinprod g h))).
Show proof.
  intros f g h.
  apply functor_iso_if_pointwise_iso.
  intros oba.
  apply (identity_is_iso d).

Definition Catlike_left_unitor (a b : category)
  :
  nat_trans
     (functor_composite
        (bindelta_pair_functor
           (functor_composite (functor_to_unit (functor_category a b))
              (constant_functor unit_category (functor_category a a) (functor_identity a)))
           (functor_identity (functor_category a b)))
        (functorial_composition a a b))
     (functor_identity (functor_category a b)).
Show proof.
  use tpair.
  -
    intros x.
    exists (λ x, identity _).
    intros oba oba' f.
    exact (id_right _ @ !(id_left _)).

  -
    intros F F' f.

    apply (nat_trans_eq_alt).
    intros oba.

    simpl. unfold horcomp_data; simpl.
    rewrite id_right.
    rewrite id_left.
    rewrite (functor_id F).
    apply id_left.

Definition Catlike_left_unitor_is_iso (a b : category)
  : ∏ f, is_iso (Catlike_left_unitor a b f).
Show proof.
  intros f.
  apply functor_iso_if_pointwise_iso.
  intros oba.
  apply (identity_is_iso b).

Definition Catlike_right_unitor (a b : category)
  :
  nat_trans
     (functor_composite
        (bindelta_pair_functor (functor_identity (functor_category a b))
           (functor_composite (functor_to_unit (functor_category a b))
              (constant_functor unit_category (functor_category b b) (functor_identity b))))
        (functorial_composition a b b))
     (functor_identity (functor_category a b)).
Show proof.
  use tpair.   - intros x.
    exists (λ x, identity _).
    intros oba oba' f.
    exact (id_right _ @ !(id_left _)).

  - intros F F' f.
    apply (nat_trans_eq_alt).
    intros oba.

    simpl. unfold horcomp_data; simpl.
    rewrite (id_right _).
    rewrite (id_left _).
    apply id_right.

Definition Catlike_right_unitor_is_iso (a b : category) :
  ∏ f, is_iso (Catlike_right_unitor a b f).
Show proof.
  intros f.
  apply functor_iso_if_pointwise_iso.
  intros oba.
  apply (identity_is_iso b).

Definition Catlike_pentagon ( a b c d e : category )
  (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_catbinprod k
        (make_catbinprod h ((functorial_composition c d e ) (make_dirprod g f)))) ·
   (Catlike_associator a c d e )
     (make_catbinprod ((functorial_composition_legacy a b c) (make_dirprod k h))
        (make_catbinprod g f))
  = (functor_on_morphisms (functorial_composition_legacy a b e)
      (catbinprodmor (identity k)
         ((Catlike_associator b c d e) (make_catbinprod h (make_catbinprod g f)))) ·
    (Catlike_associator a b d e )
      (make_catbinprod k
         (make_catbinprod ((functorial_composition_legacy b c d ) (make_dirprod h g)) f))) ·
   functor_on_morphisms (functorial_composition_legacy a d e )
     (catbinprodmor
        ((Catlike_associator a b c d ) (make_catbinprod k (make_catbinprod h g)))
        (identity f)).
Show proof.
  intros k h g f.
  apply (nat_trans_eq hsE).

  intros oba.
  simpl. unfold horcomp_data; simpl.

  repeat rewrite functor_id.
  repeat rewrite (id_left _).
  apply idpath.

Definition Catlike_triangle ( a b c : category )
  :
   ∏ f g, functor_on_morphisms (functorial_composition_legacy a b c)
                               (catbinprodmor (identity f) (Catlike_left_unitor b c g))
   =
      (Catlike_associator a b b c
        (make_catbinprod f (make_catbinprod (functor_identity b : [ _, _] ) g)))
   · functor_on_morphisms (functorial_composition_legacy a b c)
                           (catbinprodmor (Catlike_right_unitor a b f) (identity g)).
Show proof.
  intros f g.
  apply (nat_trans_eq c).
  intros oba.
  simpl. unfold horcomp_data; simpl.
  repeat rewrite functor_id.
  repeat rewrite (id_left _).
  apply idpath.


Definition PreCat_1mor_2mor : prebicategory_ob_hom.
Show proof.
  exists category.
  intros a b.
  exact (functor_category a b).

Definition PreCat_id_comp : prebicategory_id_comp.
Show proof.
  exists PreCat_1mor_2mor.
  split.
  - simpl.
    exact functor_identity.
  - simpl.
    intros a b c.
    exact (functorial_composition_legacy a b c).