gistfile1.txt

we introduce type variables and require the satisfaction of type substitution as usual.

new judgments:

  A functor a   - type A is functorial in variable a

using type contexts D, we introduce some new basic inference rules for functoriality:

     D, a type !- tyctx
  ------------------------ (type variables are functorial in themselves: identity functor)
  D, a type !- a functor a
  
  D !- X type     D, a type !- tyctx
  ---------------------------------- (types without a in them are functorial in a: constant functor)
       D, a type !- X functor a

using type contexts D with variable contexts G, like D | G, we also introduce a new
principle for fmap: 

               ~D                 ~E                  ~F
  D | G, x : X !- M : Y     D | G !- N : F[X/a]     D !- F functor a
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
                D | G !- fmap(a.F, x.M, N) : F[Y/a]

thus if F(a) = ... is our functor (Represented here by syntax a.F) and f is our morphism,
represented here by x.M, then Ff is the functorial arrow Ff : FX -> FY and FfN : FY. we
would expect this principle to satisfy the functor laws, and we expect it to hold whenever
F functor a is provable. that is to say, it's supposed to be a _principle_ not an inference
rule (like substitution), and is conditioned on the presence of functoriality. proving
functoriality will typically involve induction on the proof ~E and ~F.

for the ID functor case we define:

                                                                            ~F1
                                                                  D, a type !- tyctx
                       ~D                         ~E           ------------------------
  D, a type | G, x : X !- M : Y     D, a type | G !- N : X     D, a type !- a functor a
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
                        D, a type | G !- fmap(a.a, x.M, N) : Y

which reduces immediately to
  
        ~E                        ~D
  D, a type | G !- N : X     D, a type | G, x : X !- M : Y
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
               D, a type | G !- M[N/x] : Y

and for the constant functor case we define:

                                                                 ~F1                     ~F2
                                                               D !- C type     D, a type !- tyctx
                       ~D                         ~E           ----------------------------------
  D, a type | G, x : X !- M : Y     D, a type | G !- N : C          D, a type !- C functor a
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
                          D, a type | G !- fmap(a.C, x.M, N) : C

which reduces immediately to

                ~E
  D, a type | G !- N : C

we can provide functoriality modularly:

for * we define:

  D !- X functor a   D !- Y functor a
  ----------------------------------- *Functor
         D !- X*Y functor a

to prove admissibility, we match on ~E. either it's *I or *E. lets consider *I:

                                  ~E1                       ~E2                      ~F1                   ~F2
                            D | G !- N1 : F1[X/a]     D | G !- N2 : F2[X/a]        D !- F1 functor a     D !- F2 functor a
               ~D           ----------------------------------------------- *I     --------------------------------------- *Functor
  D | G, x : X !- M : Y          D | G !- <N1,N2> : F1[X/a] * F2[X/a]                      D !- F1 * F2 functor a
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
                                D | G !- fmap(a.(F1 * F2), x.M, <N1,N2>) : F1[Y/a] * F2[Y/a]
  
by induction, we know that

               ~D                 ~E1                   ~F1
  D | G, x : X !- M : Y     D | G !- N1 : F1[Y/a]     D !- F1 functor a
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -     =     IH(~D,~E1,~F1)
               D | G !- fmap(a.F1, x.M, N1) : F1[Y/a]

and similarly for IH(~D,~E2,~F2)

so this reduces to

            IH(~D,~E1,~F1)                             IH(~D,~E2,~F2)
  D | G !- fmap(a.F1, x.M, N1) : F1[Y/a]     D | G !- fmap(a.F2, x.M, N2) : F2[Y/a]
  --------------------------------------------------------------------------------- *I
     D | G !- < fmap(a.F1, x.M, N1) , fmap(a.F2, x.M, N2) > : F1[Y/a] * F2[Y/a]

for *E we define:

                                  ~E1                                     ~E2
                            D | G !- N1 : A * B     D | G, n1 : A, n2 : B !- N2 : C[X/a]
               ~D           ------------------------------------------------------------ *E       ~F
  D | G, x : X !- M : Y             D | G !- case N1 of <n1,n2> -> N2 : C[X/a]                  D !- C functor a
  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
                          D | G !- fmap(a.C, x.M, case N1 of <n1,n2> -> N2) : C[Y/a]

reduces to

                                     weakening on ~D                                       ~E2                  ~F
                          D | G, n1 : A, n2 : B, x : X !- M : Y     D | G, n1 : A, n2 : B !- N2 : C[X/a]     D !- C functor a
        ~E1               - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  D | G !- N1 : A * B                           D | G, n1 : A, n2 : B !- fmap(a.C, x.M, N2) : C[Y/a]
  -------------------------------------------------------------------------------------------------- *E
                    D | G !- case N1 of <n1,n2> -> fmap(a.C, x.M, N2) : C[Y/a]

since this might (will?) get stuck when the functor isn't ID and the term is a variable,
it might not be sufficient to describe fmap as a principle, and it might need to be
introduced as a term.