Introduce the right Kan extension

[joneshf]

Re: #30

First go an implementing Ran f g a. There's more that could be moved from Codensity/Yoneda, but requires some additional concepts. E.g.

• We could define Applicative (Ran f g) if we have a an isomorphism between f and g (or at least forall (a : Type) -> f a -> g a and forall (a : Type) -> g a -> f a).
• We could define Ran/lower if we have forall (a : Type) -> f a -> a (I think).

I didn't want to add these just things for the sake of redefining everything in terms of Ran, but can if they're wanted.

In any case, let me know if this is what we're thinking and if anything needs to change!

[FintanH]

This LGTM

[joneshf]

Given this comment, maybe it should be Ran/Covariant/Type? And also add Ran/Contravariant/Type as:

(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(b : Type) → (f b → a) → g b

[FintanH]

I think since it's a standalone concept and would just cause code duplication I'll merge as is. I believe Contravariant and Covariant idea just applies to things that have those distinguishable characteristics.

[joneshf]

Oh, sorry for being unclear. The two are different.

Ran/Covariant/Type

∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type

λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(b : Type)
→ (a → f b)
→ g b

Ran/Contravariant/Type

∀(f : Type → Type) → ∀(g : Type → Type) → ∀(a : Type) → Type

λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ ∀(b : Type)
→ (f b → a)
→ g b

N.B. (a → f b) vs. (f b → a).

The derived types end up being similarly defined, but over their variance:

Yoneda/Covariant/Type

∀(f : Type → Type) → ∀(a : Type) → Type

./../../Ran/Covariant/Type ./../../Id/Type

Yoneda/Contravariant/Type

∀(f : Type → Type) → ∀(a : Type) → Type

./../../Ran/Contravariant/Type ./../../Id/Type

It makes an impact in expressions like lift and lower

Ran/Covariant/lift

∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ./../../Comonad/Type f
→ ./../../Functor/Type g
→ g a
→ ./Type f g a

λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ λ(comonad : ./../../Comonad/Type f)
→ λ(functor : ./../../Functor/Type g)
→ λ(x : g a)
→ λ(b : Type)
→ λ(k : a → f b)
→ functor.map a b (λ(y : a) → comonad.extract b (k y)) x

Ran/Contravariant/lift

∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ./../../Applicative/Type f
→ ./../../Contravariant/Type g
→ g a
→ ./Type f g a

λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ λ(applicative : ./../../Applicative/Type f)
→ λ(contravariant : ./../../Contravariant/Type g)
→ λ(x : g a)
→ λ(b : Type)
→ λ(k : f b → a)
→ contravariant.map a b (λ(y : b) → k (applicative.pure b y)) x

Ran/Covariant/lower

∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ./../../Applicative/Type f
→ ./Type f g a
→ g a

λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ λ(applicative : ./../../Applicative/Type f)
→ λ(ran : ./Type f g a)
→ ran a (applicative.pure a)

Ran/Contravariant/lower

∀(f : Type → Type)
→ ∀(g : Type → Type)
→ ∀(a : Type)
→ ./../../Comonad/Type f
→ ./Type f g a
→ g a

λ(f : Type → Type)
→ λ(g : Type → Type)
→ λ(a : Type)
→ λ(comonad : ./../../Comonad/Type f)
→ λ(ran : ./Type f g a)
→ ran a (comonad.extract a)

I.e. Where one version requires Applicative f, the other version requires Comonad f. Similarly for Functor f and Contravariant f.

Ends up with a version of Codensity, Yoneda, etc for both covariant and contravariant types.

I'm down to submit a PR, if that seems useful.