Link to my Lean class

Changes

1 changed files (+8/-1)

• Category.lean
  • @@ -6,6 +6,7 @@ Objects: Types
    Morphisms: (Total) Functions Resources: + https://www.mit.edu/~xy/lean/ https://raw.githubusercontent.com/BartoszMilewski/DaoFP/refs/heads/master/DaoFP.pdf https://math.andrej.com/2016/08/06/hask-is-not-a-category/ -/
  • @@ -226,7 +227,11 @@ Intuitively, it represents moving data from one "container" to another
    abbrev NaturalType.{u} (f : Type u → Type v) (g : Type u → Type v) := {α : Type u} → f α → g α - /-- Naturality is automatically guarenteed for parametrically polymorphic functions (where the implementation is the same for each type), AKA "theorems for free". This is not guarenteed in general though since we could have a function which inspects the input type and does something crazy. -/ + /-- + Naturality is automatically guarenteed for parametrically polymorphic functions (where the implementation is the same for each type), AKA "theorems for free". This is not guarenteed in general though since we could have a function which inspects the input type and does something crazy. + + TODO: Would it be more convenient to make this a subtype? + -/ class Natural f [Functor f] [LawfulFunctor f] g [Functor g] [LawfulFunctor g] (η : NaturalType f g) where naturality (h : α → β) (x : f α) : h <$> (η x) = η (h <$> x)
  • @@ -540,4 +545,6 @@ theorem bind_join_equiv [Monad m] [LawfulMonad m] : (bindFromJoin (m := m) (join
    theorem bind_join_equiv' [E : EndofunctorMonoid m] : joinFromBind (bindFromJoin E.join) x = E.join x := by simp + -- TODO: Monad transformers + -- TODO: Enrichment