Definition of bicategory and oplax functor in terms of composition functor

bicategory_functor.lean

import category_theory.products.associator
import category_theory.currying
namespace category_theory
universes w w₁ w₂ v v₁ v₂ u u₁ u₂
class bicategory (B : Type u) extends quiver.{v+1} B :=
(hom_category (a b : B) : category.{w} (a ⟶ b) . tactic.apply_instance)
(comp (a b c : B) : (a ⟶ b) × (b ⟶ c) ⥤ (a ⟶ c))
-- encompass `whisker_left_(id,comp), whisker_right_(id,comp), whisker_exchange (category.theory.bifunctor.diagonal)`
(associator (a b c d : B) : (comp a b c).prod (𝟭 _) ⋙ comp a c d ⟶
   prod.associator _ _ _ ⋙ (𝟭 _).prod (comp b c d) ⋙ comp a b d)
(notation `α_` := associator)
-- encompass naturality
(id (a : B) : a ⟶ a)
(left_unitor (a b : B) : prod.sectr (id a) _ ⋙ comp a a b ⟶ 𝟭 _)
(right_unitor (a b : B) : prod.sectl _ (id b) ⋙ comp a b b ⟶ 𝟭 _)
-- encompass naturality
(pentagon (a b c d e : B) : let pa := λ {A A' B B' C C'}, @prod.associator A A' B B' C C',
  l1 := whisker_right (nat_trans.prod (α_ a b c d) (𝟙 (𝟭 _))) (comp a d e),
  l2 := whisker_left ((pa ⋙ (𝟭 _).prod (comp b c d)).prod (𝟭 _)) (α_ a b d e),
  l3 := whisker_left (pa.prod (𝟭 _) ⋙ pa) (whisker_right (nat_trans.prod (𝟙 (𝟭 _)) (α_ b c d e)) (comp a b e)),
  r1 := whisker_left (((comp a b c).prod (𝟭 _)).prod (𝟭 _)) (α_ a c d e),
  r2 := whisker_left (pa ⋙ (𝟭 _).prod (comp c d e)) (α_ a b c e)
  in l1 ≫ l2 ≫ l3 = r1 ≫ r2)
(triangle (a b c : B) : let
  l1 := whisker_left ((prod.sectl _ (id b)).prod (𝟭 _)) (α_ a b b c),
  l2 := whisker_right (nat_trans.prod (𝟙 (𝟭 _)) (left_unitor b c)) (comp a b c)
  in l1 ≫ l2 = whisker_right (nat_trans.prod (right_unitor a b) (𝟙 (𝟭 _))) (comp a b c))

attribute [instance] bicategory.hom_category

instance category_struct_of_bicategory (B : Type u) [bicategory.{w v} B] :
  category_struct.{v} B :=
{ id := bicategory.id, comp := λ a b c f g, (bicategory.comp a b c).obj (f,g) }

variables (B : Type u₁) [bicategory.{w₁ v₁} B] (C : Type u₂) [bicategory.{w₂ v₂} C]
variables (obj : B → C) {B C}

abbreviation map_aux := ∀ (a b : B), (a ⟶ b) ⥤ (obj a ⟶ obj b)
-- encompass `map, map₂, map₂_id, map₂_comp`
variables (map : map_aux obj) {obj}
abbreviation map_id_aux := ∀ (a : B), (map a a).obj (𝟙 a) ⟶ 𝟙 (obj a)
variable (map_id : map_id_aux map)
abbreviation map_comp_aux := ∀ (a b c : B), bicategory.comp a b c ⋙ map a c ⟶
  (map a b).prod (map b c) ⋙ bicategory.comp (obj a) (obj b) (obj c)
-- encompass naturality
variables (map_comp : map_comp_aux map) {map} (a b c d : B)

abbreviation map_associator_aux : Prop := let
  l1 := whisker_right (bicategory.associator a b c d) (map a d),
  k := (𝟭 (a ⟶ b)).prod (bicategory.comp b c d),
  l2 := whisker_left (prod.associator _ _ _ ⋙ k) (map_comp a b d),
  l3 := whisker_left (prod.associator _ _ _) (whisker_right
    (nat_trans.prod (𝟙 (map a b)) (map_comp b c d)) (bicategory.comp (obj a) (obj b) (obj d))),
  r1 := whisker_left ((bicategory.comp a b c).prod (𝟭 _)) (map_comp a c d),
  r2 := whisker_right (nat_trans.prod (map_comp a b c) (𝟙 (map c d))) (bicategory.comp _ _ _),
  r3 := whisker_left (((map a b).prod (map b c)).prod (map c d)) (bicategory.associator _ _ _ _)
  in l1 ≫ l2 ≫ l3 = r1 ≫ r2 ≫ r3

abbreviation map_left_unitor_aux : Prop := let
  r1 := whisker_left (prod.sectr (𝟙 a) _) (map_comp a a b),
  k := bicategory.comp (obj a) (obj a) (obj b),
  r1' : _ ⟶ map a b ⋙ (curry_obj k).obj ((map a a).obj (𝟙 a)) := r1 ≫ { app := λ _, 𝟙 _ },
  r23 := whisker_left (map a b) ((curry_obj k).map (map_id a) ≫ bicategory.left_unitor (obj a) (obj b))
  in whisker_right (bicategory.left_unitor a b) (map a b) = r1' ≫ r23

abbreviation map_right_unitor_aux : Prop := let
  r1 := whisker_left (prod.sectl _ (𝟙 b)) (map_comp a b b),
  k := prod.swap (obj b ⟶ obj b) (obj a ⟶ obj b) ⋙ bicategory.comp _ _ _,
  r1' : _ ⟶ map a b ⋙ (curry_obj k).obj ((map b b).obj (𝟙 b)) := r1 ≫ { app := λ _, 𝟙 _ },
  r23 := whisker_left (map a b) ((curry_obj k).map (map_id b) ≫ bicategory.right_unitor (obj a) (obj b))
  in whisker_right (bicategory.right_unitor a b) (map a b) = r1' ≫ r23

structure oplax_functor :=
(obj : B → C) (map : map_aux obj) (map_id : map_id_aux map) (map_comp : map_comp_aux map)
(map_associator (a b c d : B) : map_associator_aux map_comp a b c d)
(map_left_unitor (a b : B) : map_left_unitor_aux map_id map_comp a b)
(map_right_unitor (a b : B) : map_right_unitor_aux map_id map_comp a b)

end category_theory