Guess what functors are defined

guess.k

(Lam Object:**.

 Lam Hom: Object -> Object -> *.

 Lam identity: Pi A:Object. Hom A A.

 Lam compose: Pi A:Object.
              Pi B:Object.
              Pi C:Object.
              Pi AB:Hom A B.
              Pi BC:Hom B C.
              Hom A C.

 Lam Functor: Object -> Object.

 Lam pure: Pi A:Object.
           Hom A (Functor A).

 Lam map: Pi A:Object.
          Pi B:Object.
          (Hom A B) -> (Hom (Functor A) (Functor B)).

 Lam Bifunctor: Object -> Object -> Object.

 Lam bimap: Pi A:Object.
            Pi B:Object.
            Pi C:Object.
            Pi D:Object.
            (Hom A C) -> (Hom B D) -> (Hom (Bifunctor A B) (Bifunctor C D)).

 Lam Profunctor: Object -> Object -> Object.

 Lam dimap: Pi A:Object.
            Pi B:Object.
            Pi C:Object.
            Pi D:Object.
            (Hom C A) -> (Hom B D) -> (Hom (Profunctor A B) (Profunctor C D)).
            *)
 
 (*)
 (Lam A:*. Lam B:*. A -> B)
 (Lam A:*. Lam x:A. x)
 (Lam A:*. Lam B:*. Lam C:*. Lam f:A -> B. Lam g:B -> C. Lam x:A. g (f x))

 (Lam A:*. Pi R:*. (A -> R) -> R -> R)
 (Lam A:*. Lam x:A. Lam R:*. Lam k:A -> R. Lam s:R. k x)
 (Lam A:*.
  Lam B:*.
  Lam f:A -> B.
  Lam fa: Pi R:*. (A -> R) -> R -> R.
  Lam R:*.
  Lam k:B -> R.
  Lam s:R.
  fa R (Lam x:A. k (f x)) s)

 (Lam A:*. Lam B:*. Pi R:*. (A -> R) -> (B -> R) -> R)
 (Lam A:*.
  Lam B:*.
  Lam C:*.
  Lam D:*.
  Lam f:A -> C.
  Lam g:B -> D.
  Lam fab: Pi R:*. (A -> R) -> (B -> R) -> R.
  Lam R:*.
  Lam mu:C -> R.
  Lam nu:D -> R.
  fab R (Lam x:A. mu (f x)) (Lam y:B. nu (g y)))

 (Lam A:*. Lam B:*. A -> B)
 (Lam A:*.
  Lam B:*.
  Lam C:*.
  Lam D:*.
  Lam f:C -> A.
  Lam g:B -> D.
  Lam fab: A -> B.
  Lam x:C.
  g (fab (f x)))