Pseudofunctor.v

Require Export Category.Core Category.Morphisms Cat FunctorCategory.
Require Import Common.

Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.

Local Open Scope morphism_scope.

Section PseudoFunctor.
  Context `{Funext}.

  Variable C : PreCategory.

  (** Quoting from nCatLab (http://ncatlab.org/nlab/show/pseudofunctor):

      Given bicategories [C] and [D], a pseudofunctor (or weak 2-functor,
      or just functor) [P : C → D] consists of:

      * for each object [x] of [C], an object [P_x] of [D];

      * for each hom-category [C(x,y)] in [C], a functor [P_{x,y} :
        C(x,y) → D(P_x, P_y)];

      * for each object [x] of [C], an invertible 2-morphism (2-cell)
        [P_{id_x} : id_{P_x} ⇒ P_{x,x}(id_x);

      * for each triple [x],[y],[z] of [C]-objects, a isomorphism
        (natural in [f : x → y] and [g : y → z]) [P_{x,y,z}(f,g) :
        P_{x,y}(f);P_{y,z}(g) ⇒ P_{x,z}(f;g)];

...
*)

  Record Pseudofunctor :=
    {
      PObjectOf :> C -> PreCategory;
      PMorphismOf : forall s d, Morphism C s d -> Functor (PObjectOf s) (PObjectOf d);
      PFCompositionOf : forall s d d' (m1 : Morphism C d d') (m2 : Morphism C s d),
                          (** XXX Somehow this should be natural in [m1] and [m2].  What does that even mean? *)
                          Isomorphic (C := [PObjectOf s, PObjectOf d'])
                                     (PMorphismOf _ _ (m1 ∘ m2))
                                     (PMorphismOf _ _ m1 ∘ PMorphismOf _ _ m2)%functor;
      PFIdentityOf : forall x,
                       Isomorphic (C := [PObjectOf x, PObjectOf x])
                                  (IdentityFunctor _)
                                  (PMorphismOf x x (Identity x));
      PFCompositionOfCoherent : forall w x y z f g h α

    }.