Changes
1 changed files (+1/-1)
-
-
@@ -164,7 +164,7 @@ class Profunctor (p : Type u → Type v → Type*) wheredimap : (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 α₀ β₀) : dimap f' g' (dimap f g x) = dimap (f ∘ f') (g' ∘ g) x dimap f' g' (dimap f g x) = dimap (f ∘ f') (g' ∘ g) x -- Exponentials are profunctors instance : Profunctor (· → ·) where
-