/Dao.lean at 0788e09e757c811218932ea378e8c7c10535401b

-- https://github.com/BartoszMilewski/DaoFP

import Mathlib

-- universe u
def absurd' {C : Sort u} : Empty → C := Empty.rec

#check absurd'

#check id

-- Universes sad
-- #eval id id

-- Naturality condition

inductive Bool'
  | true' (a : Unit) : Bool'
  | false' (a : Unit) : Bool'

#check Bool'.true' = Bool'.false'


-- def f
--   | 0 => 1
--   | x + 1 => (x + 1) * f x

#eval f 69

def third {α β γ} (x : α × β × γ) :=
  let (_, _, c) := x
  c


universe v

-- class Natural (f : (Type u → Type v) → Type u → Type v) : Type (max (u + 1) v) where
-- Oops it's not a typeclass


def id' {α} (x : α) := x

#check id'

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 β := (· <$> y)


-- def map_to_T (x : String) : Type :=
-- if x = "0" then
--   Nat
-- else
--   String

-- def natOrStringThree (b : Bool) : if b then Nat else String :=
--   match b with
--   | true => (3 : Nat)
--   | false => "three"

-- abbrev map_to_T (x : String) : Type :=
--   if x = "0" then Nat else String

-- def map_to (x : String) : map_to_T x :=
--   match decide (x = "0") with
--   | true => (42 : Nat)
--   | false => x

-- def map_to (x : String) : map_to_T x :=
--   if h : x = "0" then by
--     simp [map_to_T, h]
--     exact 42
--   else by
--     simp [map_to_T, h]
--     exact x


def ap [Monad m] (fs : m (α → β)) (as : m α) : m β := do
  -- fs >>= λ f ↦ as >>= λ a ↦ pure (f a)
  -- fs >>= (· <$> as)
  return (← fs) (← as)

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


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 :=

class ContraFunctor (f : Type → Type) where
  contramap : (β → α) → f α → f β
  id_contramap (x : f α) : contramap id x = x
  comp_contramap (g : β → α) (h : γ → β) (x : f α) : contramap (g ∘ h) x = contramap h (contramap g x)

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