Fix the profunctor stuff using abbrevs instead of defs

Changes

1 changed files (+10/-13)

• Category.lean
  • @@ -160,7 +160,7 @@ instance [Cofunctor f] [Functor g] [LawfulFunctor g] : Cofunctor (f ∘ g) where
    /-- Profunctors are useful for lenses -/ - class Profunctor (p : Type u → Type v → Type (max u v)) where + 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 :
  • @@ -186,12 +186,12 @@ instance [Profunctor p] [Profunctor q] : Profunctor (Procompose p q) where
    id_dimap := by simp [Profunctor.id_dimap] dimap_dimap := by simp [Profunctor.dimap_dimap] - def End p [Profunctor p] := ∀ x, p x x + abbrev End p [Profunctor p] := ∀ x, p x x - def Coend p [Profunctor p] := Σ x, p x x + abbrev Coend p [Profunctor p] := Σ x, p x x - inductive ProPair q p [Profunctor p] [Profunctor q] a b x y - | mk : q a y → p x b → ProPair q p a b x y + abbrev ProPair q p [Profunctor p] [Profunctor q] a b x y := + q a y × p x b instance [Profunctor p] [Profunctor q] : Profunctor (ProPair q p a b) where dimap l r
  • @@ -199,17 +199,14 @@ instance [Profunctor p] [Profunctor q] : Profunctor (ProPair q p a b) where
    id_dimap := by simp [Profunctor.id_dimap] dimap_dimap := by simp [Profunctor.dimap_dimap] - inductive CoendCompose p q [Profunctor p] [Profunctor q] a b - | mk : Coend (ProPair q p a b) → CoendCompose p q a b + abbrev CoendCompose p q [Profunctor p] [Profunctor q] a b := + Coend (ProPair q p 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⟩⟩ - id_dimap := by - simp [Profunctor.id_dimap] - grind - dimap_dimap f f' g g' x := by - simp [Profunctor.id_dimap] + | ⟨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] /-- Type of a natural transformation (without the naturality condition) -/