public
Last active

  • Download Gist
gistfile1.txt
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
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.

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.