Ends and coends stuff

Changes

2 changed files (+64/-3)

• BadSort.lean
  • @@ -10,4 +10,8 @@ def WorstSort [LinearOrder α] (A : List α) (f : ℕ → ℕ) := BadSort A <| f
    def DiabolicalSort [LinearOrder α] (A : List α) := WorstSort A fun n ↦ ack n n + theorem BadSortCorrect [LinearOrder α] (A : List α) n : (BadSort A n).Perm A ∧ (BadSort A n).SortedLE := by + sorry + + -- Probably not to hard to prove that this is correct but left as an exercise to the reader
• Dao.lean
  • @@ -21,9 +21,9 @@ inductive Bool'
    #check Bool'.true' = Bool'.false' - def f - | 0 => 1 - | x + 1 => (x + 1) * f x + -- def f + -- | 0 => 1 + -- | x + 1 => (x + 1) * f x #eval f 69
  • @@ -83,3 +83,60 @@ def ap [Monad m] (fs : m (α → β)) (as : m α) : m β := do
    class Monad' (m : Type → Type) where fish : (β → m γ) → (α → m β) → (α → m γ) join : (a : m (m α)) → m α := fish id id + + namespace Ch18 + + class Profunctor (p : Type u → Type u → Type (u + 1)) where + dimap : (s → a) → (b → t) → (p a b → p s t) + + inductive Procompose p q [Profunctor p] [Profunctor q] a b + | mk : q a x → p x b → Procompose p q a b + + def mapOut [Profunctor p] [Profunctor q] (pc : Procompose p q a b) (f : {x : Type} → q a x → p x b → c) := + match pc with + | ⟨qax, pxb⟩ => f qax pxb + + instance [Profunctor p] [Profunctor q] : Profunctor (Procompose p q) where + dimap l r + | ⟨qax, pxb⟩ => ⟨Profunctor.dimap l id qax, Profunctor.dimap id r pxb⟩ + + def End p [Profunctor p] := ∀ x, p x x + + def Coend p [Profunctor p] := Σ x, p x x + + inductive ProPair q p [Profunctor p] [Profunctor q] a b x y + | mk : q a y → p x b → ProPair q p a b x y + + instance [Profunctor p] [Profunctor q] : Profunctor (ProPair q p a b) where + dimap l r + | ⟨qax, pxb⟩ => ⟨Profunctor.dimap id r qax, Profunctor.dimap l id pxb⟩ + + inductive CoEndCompose p q [Profunctor p] [Profunctor q] a b + | mk : Coend (ProPair q p a b) → CoEndCompose p q a b + + instance [Profunctor p] [Profunctor q] : Profunctor (CoEndCompose p q) where + dimap l r + | ⟨x, ⟨qay, pxb⟩⟩ => ⟨x, ⟨Profunctor.dimap l id qay,Profunctor.dimap id r pxb⟩⟩ + + inductive Yo f [Functor f] a x y + | mk : ((a → x) → f y) → Yo f a x y + + instance [Functor f] : Profunctor (Yo f a) + + + def yoneda f [Functor f] : (End (Yo f a)) → f a + | ⟨x, g⟩ => g id + + inductive LensE s a + | mk : (s → (c × a)) → (c × a → s) → LensE s a + + def toGet : LensE s a → (s → a) + | ⟨l, _⟩ => (l · |>.2) + + def toSet : LensE s a → (s → a → s) + | ⟨l, r⟩ => fun s a ↦ r ((l s).1, a) + + def getResidue : LensE s a → c + | ⟨l, _⟩ => (l _).1 + + end Ch18