Oh cool contravariant functor stuff

Changes

1 changed files (+7/-0)

• Dao.lean
  • @@ -161,3 +161,10 @@ def yoneda {α} f [Functor f] (g : {β : Type u} → (α → β) → f β) : f
    def yoneda' {α} f [Functor f] (y : f α) : {β : Type u} → (α → β) → f β := (· <$> y) end Yoneda + + + class ContraFunctor (f : Type → Type) where + contramap : (β → α) → f α → f β + + instance (α : Type) : ContraFunctor (· → α) where + contramap f g := fun x ↦ g (f x)