More Yoneda stuff I guess

Changes

1 changed files (+70/-13)

• Dao.lean
  • @@ -1,6 +1,6 @@
    -- https://github.com/BartoszMilewski/DaoFP - -- import Mathlib + import Mathlib -- universe u def absurd' {C : Sort u} : Empty → C := Empty.rec
  • @@ -44,7 +44,7 @@ def id' {α} (x : α) := x
    def yoneda {α} (m : Type u → Type v) [Functor m] (g : {β : Type u} → (α → β) → m β) : m α := g id - def yoneda' {α} (m : Type u → Type v) [Functor m] (y : m α) : {β : Type u} → (α → β) → m β := λ h ↦ h <$> y + def yoneda' {α} (m : Type u → Type v) [Functor m] (y : m α) : {β : Type u} → (α → β) → m β := (· <$> y) -- def map_to_T (x : String) : Type :=
  • @@ -152,17 +152,6 @@ namespace Yoneda
    -- 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 - - class ContraFunctor (f : Type → Type) where contramap : (β → α) → f α → f β id_contramap (x : f α) : contramap id x = x
  • @@ -172,3 +161,71 @@ instance (α : Type) : ContraFunctor (· → α) where
    contramap f g := fun x ↦ g (f x) id_contramap := by simp comp_contramap := by simp + + #synth Functor List + + #synth Functor Option + + instance : LawfulFunctor List where + map_const := by solve_by_elim + id_map xs := by simp + comp_map := by simp + + class Natural f [Functor f] [LawfulFunctor f] g [Functor g] [LawfulFunctor g] (η : {α : Type u} → f α → g α) where + naturality (x : f α) (h : α → β) : Functor.map h (η x) = η (Functor.map h x) + + instance : Natural List Option List.head? where + naturality x h := by simp + + def OptionToList : Option α → List α + | some a => [a] + | none => [] + + instance : Natural Option List OptionToList where + naturality x h := by + simp [OptionToList] + grind + + -- abbrev Natural (f : Type → Type) [Functor f] [LawfulFunctor f] (g : Type → Type) [Functor g] [LawfulFunctor g] := + -- ∀ α, f α → g α + + -- example (f : Type → Type) [Functor f] [LawfulFunctor f] (g : Type → Type) [Functor g] [LawfulFunctor g] (η : Natural f g) (x : f α) (h : α → β) + -- : Functor.map (f := g) h (η α x) = η β (Functor.map (f := f) h x) := by + -- simp + + -- OK time to do Yoneda part 2 + + /-- Hom-functor in enriched category -/ + @[simp] + instance (α : Type u) : Functor (α → ·) where + map f g := f ∘ g + + instance (α : Type u) : LawfulFunctor (α → ·) where + map_const := by solve_by_elim + id_map := by simp + comp_map := by simp [Function.comp_assoc] + + /-- Yoneda forward map -/ + def yoneda (g : {β : Type u} → (α → β) → m β) [Functor m] [LawfulFunctor m] : m α := g id + + /-- Yoneda reverse map -/ + def yoneda' [Functor m] [LawfulFunctor m] (y : m α) : {β : Type u} → (α → β) → m β := (· <$> y) + + /-- Reverse map always produces a natural transformation -/ + instance [Functor m] [LawfulFunctor m] : Natural (α → ·) m (yoneda' y) where + naturality x h := by simp [yoneda']; rfl + + /-- Mapping and unmapping a natural transformation returns the itself + + Note that this does work for an arbitrary function between the hom-functor and `m` because we use the naturality condition. -/ + theorem yoneda_lemma (g : {β : Type u} → (α → β) → m β) [Functor m] [LawfulFunctor m] [N : Natural (α → ·) m g] + : (yoneda' (β := ·) (yoneda (m := m) g)) = (g (β := ·)) := by + unfold yoneda yoneda' + simp [N.naturality] + + /-- Mapping and unmapping an element `m α` returns itself -/ + theorem yoneda_lemma' (y : m α) [Functor m] [LawfulFunctor m] + : yoneda (yoneda' (m := m) (α := α) y) = y := by + simp [yoneda, yoneda'] + + end Yoneda