Style tweaks

Changes

1 changed files (+11/-11)

• Category.lean
  • @@ -166,10 +166,10 @@ 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 + 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 + 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⟩⟩
  • @@ -209,14 +209,14 @@ instance [Functor f] [LawfulFunctor f] : Natural (α → ·) f (yoneda' y) where
    /-- 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} → (α → β) → f β) [Functor f] [LawfulFunctor f] [N : Natural (α → ·) f g] - : (yoneda' (β := ·) (yoneda (f := f) g)) = (g (β := ·)) := by + theorem yoneda_lemma (g : {β : Type u} → (α → β) → f β) [Functor f] [LawfulFunctor f] [N : Natural (α → ·) f g] : + (yoneda' (β := ·) (yoneda (f := f) g)) = (g (β := ·)) := by unfold yoneda yoneda' simp [N.naturality] /-- Mapping and unmapping an element `m α` returns itself -/ - theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] - : yoneda (yoneda' (f := f) (α := α) y) = y := by + theorem yoneda_lemma' (y : f α) [Functor f] [LawfulFunctor f] : + yoneda (yoneda' (f := f) (α := α) y) = y := by simp [yoneda, yoneda']
  • @@ -227,13 +227,13 @@ def coyoneda (g : {β : Type u} → (β → α) → f β) [Cofunctor f] : f α :
    def coyoneda' [Cofunctor f] (y : f α) : {β : Type u} → (β → α) → f β := (Cofunctor.comap · y) /-- Same but for Coyoneda -/ - theorem coyoneda_lemma (g : {β : Type u} → (β → α) → f β) [Cofunctor f] [N : Conatural (· → α) f g] - : (coyoneda' (β := ·) (coyoneda (f := f) g)) = (g (β := ·)) := by + theorem coyoneda_lemma (g : {β : Type u} → (β → α) → f β) [Cofunctor f] [N : Conatural (· → α) f g] : + (coyoneda' (β := ·) (coyoneda (f := f) g)) = (g (β := ·)) := by unfold coyoneda coyoneda' simp [N.naturality] - theorem coyoneda_lemma' (y : f α) [Cofunctor f] - : coyoneda (coyoneda' (f := f) (α := α) y) = y := by + theorem coyoneda_lemma' (y : f α) [Cofunctor f] : + coyoneda (coyoneda' (f := f) (α := α) y) = y := by simp [coyoneda, coyoneda', Cofunctor.id_comap]