Don't need to manually specify type class instance in a lot of places

Changes

1 changed files (+21/-13)

• Category.lean
  • @@ -82,10 +82,10 @@ infixr:100 " <¥> " => Cofunctor.comap
    theorem Cofunctor.id_comap' [Cofunctor f] : Cofunctor.comap (f := f) (@id α) = id := by ext x - exact Cofunctor.id_comap (f := f) x + exact Cofunctor.id_comap x theorem Cofunctor.comap_comp_comap [Cofunctor f] (g : α → β) (h : β → γ) : - ((g <¥> ·) ∘ (h <¥> ·) : f γ → f α) = Cofunctor.comap (f := f) (h ∘ g) := + ((g <¥> ·) ∘ (h <¥> ·) : f γ → f α) = Cofunctor.comap (h ∘ g) := funext fun _ ↦ (comp_comap _ _ _).symm
  • @@ -145,7 +145,7 @@ instance [Cofunctor f] [Cofunctor g] : LawfulFunctor (f ∘ g) where
    @[simp] instance [Functor f] [LawfulFunctor f] [Cofunctor g] : Cofunctor (f ∘ g) where comap h x := Functor.map (f := f) (h <¥> ·) x - id_comap := by simp [Cofunctor.id_comap (f := g)] + id_comap := by simp [Cofunctor.id_comap] comp_comap := by simp [Cofunctor.comp_comap] @[simp]
  • @@ -153,9 +153,9 @@ instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where
    comap h x := Cofunctor.comap (f := f) (h <$> ·) x id_comap := by simp only [Function.comp_apply, id_map] - exact Cofunctor.id_comap (f := f) + exact Cofunctor.id_comap comp_comap h h' x := by - simp only [← Functor.map_comp_map h' h, Cofunctor.comp_comap (f := f)] + simp only [← Functor.map_comp_map h' h, Cofunctor.comp_comap] -- Bifunctors map Lean × Lean to Lean
  • @@ -265,7 +265,7 @@ Horizontal composition of natural transformations
    Intuitively this is like repackaging data in nested "containers" -/ instance (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [M : Natural f f' η] [N : Natural g g' μ] : - Natural (g ∘ f) (g' ∘ f') (μ ∘ (Functor.map (f := g) η ·)) := + Natural (g ∘ f) (g' ∘ f') (μ ∘ (η <$> ·)) := ⟨by simp [N.naturality, M.naturality]⟩ /-- Alternatively we do `μ` first and then the map second -/
  • @@ -275,15 +275,17 @@ instance (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunc
    /-- The two orderings are equivalent, which only requires the outer transformation to be natural -/ lemma horizontal_comp_equiv (η : NaturalType f f') (μ : NaturalType g g') [Functor f] [LawfulFunctor f] [Functor f'] [LawfulFunctor f'] [Functor g] [LawfulFunctor g] [Functor g'] [LawfulFunctor g'] [N : Natural g g' μ] : - (μ ∘ (Functor.map (f := g) η ·)) x = ((Functor.map (f := g') η ·) ∘ μ) x := by + (μ ∘ (η <$> ·)) x = ((Functor.map (f := g') η ·) ∘ μ) x := by simp [N.naturality] /-- Yoneda forward map (g is not necessarily natural) -/ - def yoneda (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] : f α := g id + def yoneda (g : NaturalType (α → ·) f) [Functor f] [LawfulFunctor f] : f α := + g id /-- Yoneda reverse map -/ - def yoneda' [Functor f] [LawfulFunctor f] (y : f α) : NaturalType (α → ·) f := (· <$> y) + def yoneda' [Functor f] [LawfulFunctor f] (y : f α) : NaturalType (α → ·) f := + (· <$> y) /-- Reverse map always produces a natural transformation -/ instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) :=
  • @@ -302,10 +304,12 @@ theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : yoneda (yoneda'
    simp [yoneda, yoneda'] /-- Coyoneda forward map -/ - def coyoneda (g : NaturalType (· → α) f) [Cofunctor f] : f α := g id + def coyoneda (g : NaturalType (· → α) f) [Cofunctor f] : f α := + g id /-- Coyoneda reverse map -/ - def coyoneda' [Cofunctor f] (y : f α) : NaturalType (· → α) f := (· <¥> y) + def coyoneda' [Cofunctor f] (y : f α) : NaturalType (· → α) f := + (· <¥> y) /-- Reverse map always produces a natural transformation -/ instance [Cofunctor f] : Conatural (· → α) f (coyoneda' y) :=
  • @@ -502,8 +506,9 @@ class EndofunctorMonoid m extends Functor m, LawfulFunctor m where
    join : NaturalType (m ∘ m) m pure : NaturalType Id m join_pure : (join ∘ pure) x = x - join_map_pure : (join ∘ (Functor.map (f := m) pure ·)) x = x - join_join : (join ∘ (Functor.map (f := m) join ·)) x = (join ∘ join) x + -- When using <$>, Lean synthesizes the wrong type class instance for some weird reason + join_map_pure : (join ∘ (map pure ·)) x = x + join_join : (join ∘ (map join ·)) x = (join ∘ join) x @[simp] def bindFromJoin [EndofunctorMonoid m] (join : NaturalType (m ∘ m) m) (x : m α) (f : α → m β) :=
  • @@ -554,10 +559,13 @@ 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 + -- Unlike Haskell, Lean is powerful enough that we can also use it for doing category theory in any category, not just the category Lean #check CategoryTheory.Category