search

FormationAI / dhall-bhat

Tasty meal of Dhall
66 stars 11 forks source link

Add Contravariance #29

Open FintanH opened 6 years ago

FintanH commented 6 years ago

Add contravariant functor i.e.:

λ(f : Type → Type)
→ { contra = ∀(a : Type) → ∀(b : Type) → (b → a) → f a → f b }

Should probably go under Contravariant/Functor/Type

Along with this we could add Coyoneda and other functionality.

sellout commented 6 years ago

Should probably go under Contravariant/Functor/Type

What if we put this in Functor/Contravariant/type and moved Functor to Functor/Covariant/type Then we could also add bifunctor as Functor/Product/type and profunctor as Functor/Profunctor/type.

sellout commented 6 years ago

And yeah, for Yoneda/Coyoneda maybe want the same structure – e.g., Yoneda/{Contra|Co|Prod}/type

FintanH commented 6 years ago

Another addition is mentioned in the comment here https://github.com/FormationAI/dhall-bhat/pull/31#issuecomment-410534119