Skip to content

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.