Functor_Fmap
 (F:* -> *) (X:*) (Y:*)
 = (X -> Y) -> F X -> F Y

Functor_Class
 (F:* -> *) (Data:*)
 =  (fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y)
 -> Data
Functor_Polytype
 (F:* -> *) : *p
 = (Data:*) -> Functor_Class F Data -> Data
Functor
 (F:* -> *) : *m
 = Monotype (Functor_Polytype F)

functor
 (F:* -> *)
 (fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y)
 : Functor F
 = monotype (Functor_Polytype F)
     (λ(Data:*) (functor_class:Functor_Class F Data) -> functor_class fmap)
unFunctor
 (F:* -> *) (Data:*)
 (functor_class:Functor_Class F Data)
 (functor:Functor F)
 : Data
 = polytype (Functor_Polytype F) functor Data functor_class

Functor_fmap
 (F:* -> *) (functor:Functor F) (X:*) (Y:*)
 : Functor_Fmap F X Y
 = unFunctor F (Functor_Fmap F X Y)
    (λ(fmap:∀(X:*) -> ∀(Y:*) -> Functor_Fmap F X Y) -> fmap X Y)
    functor