More doc comments

Changes

1 changed files (+3/-2)

• Category.lean
  • @@ -39,7 +39,8 @@ https://math.andrej.com/2016/08/06/hask-is-not-a-category/
    /- - Endofunctors + Endofunctors in Lean! + f maps objects f.map maps morphisms `(α → β) → f α → f β` is the same thing as `(α → β) → (f α → f β)`
  • @@ -166,7 +167,7 @@ class Profunctor (p : Type u → Type v → Type*) where
    dimap_dimap (f : α₁ → α₀) (f' : α₂ → α₁) (g : β₀ → β₁) (g' : β₁ → β₂) (x : p α₀ β₀) : dimap f' g' (dimap f g x) = dimap (f ∘ f') (g' ∘ g) x - -- Exponentials are profunctors + /-- Exponentials are profunctors -/ instance : Profunctor (· → ·) where dimap f g h := g ∘ h ∘ f id_dimap := by simp