Style tweaks

Changes

1 changed files (+6/-7)

• Category.lean
  • @@ -162,9 +162,8 @@ instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where
    /-- Profunctors are useful for lenses -/ class Profunctor (p : Type u → Type v → Type*) where dimap : (s → a) → (b → t) → (p a b → p s t) - id_dimap : ∀ {α β} (x : p α β), dimap id id x = x - dimap_dimap : - ∀ {α₀ α₁ α₂ β₀ β₁ β₂} (f : α₁ → α₀) (f' : α₂ → α₁) (g : β₀ → β₁) (g' : β₁ → β₂) (x : p α₀ β₀), + id_dimap (x : p α β) : dimap id id x = x + dimap_dimap (f : α₁ → α₀) (f' : α₂ → α₁) (g : β₀ → β₁) (g' : β₁ → β₂) (x : p α₀ β₀) : dimap f' g' (dimap f g x) = dimap (f ∘ f') (g' ∘ g) x -- Exponentials are profunctors
  • @@ -182,7 +181,7 @@ def mapOut [Profunctor p] [Profunctor q] (pc : Procompose p q a b) (f : {x : Typ
    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⟩ + | ⟨qax, pxb⟩ => ⟨Profunctor.dimap l id qax, Profunctor.dimap id r pxb⟩ id_dimap := by simp [Profunctor.id_dimap] dimap_dimap := by simp [Profunctor.dimap_dimap]
  • @@ -195,7 +194,7 @@ abbrev ProPair q p [Profunctor p] [Profunctor q] 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⟩ + | ⟨qax, pxb⟩ => ⟨Profunctor.dimap id r qax, Profunctor.dimap l id pxb⟩ id_dimap := by simp [Profunctor.id_dimap] dimap_dimap := by simp [Profunctor.dimap_dimap]
  • @@ -204,9 +203,9 @@ abbrev CoendCompose p q [Profunctor p] [Profunctor 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)⟩ + | ⟨x, (qay, pxb)⟩ => ⟨x, (Profunctor.dimap l id qay, Profunctor.dimap id r pxb)⟩ id_dimap := by simp [Profunctor.id_dimap] - dimap_dimap f f' g g' x := by simp [Profunctor.dimap_dimap] + dimap_dimap := by simp [Profunctor.dimap_dimap] /-- Type of a natural transformation (without the naturality condition) -/