More random cat theory experiments

Changes

1 changed files (+21/-0)

• Dao.lean
  • @@ -140,3 +140,24 @@ def getResidue : LensE s a → c
    | ⟨l, _⟩ => (l _).1 end Ch18 + + + namespace Yoneda + + -- inductive Natural f g [Functor f] [Functor g] + -- | mk : (f a → g a) → Natural f g + + -- def Hom (a : Type u) := fun (x : Type u) ↦ x → a + + -- instance : Functor (Hom a) where + -- map f a := + + def Natural f g [Functor f] [Functor g] {a} := f a → g a + + + + def yoneda {α} f [Functor f] (g : {β : Type u} → (α → β) → f β) : f α := g id + + def yoneda' {α} f [Functor f] (y : f α) : {β : Type u} → (α → β) → f β := (· <$> y) + + end Yoneda