Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
chore(category_theory/closed/cartesian): make exp right-associative (#…
Browse files Browse the repository at this point in the history
…11172)

This makes `X ⟹ Y ⟹ Z` parse as `X ⟹ (Y ⟹ Z)`, like ordinary function types.
  • Loading branch information
dwarn committed Dec 31, 2021
1 parent 559951c commit 8db2fa0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/category_theory/closed/cartesian.lean
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ lemma coev_naturality {X Y : C} (f : X ⟶ Y) :
f ≫ (coev A).app Y = (coev A).app X ≫ (exp A).map (limits.prod.map (𝟙 A) f) :=
(coev A).naturality f

notation A ` ⟹ `:20 B:20 := (exp A).obj B
notation A ` ⟹ `:20 B:19 := (exp A).obj B
notation B ` ^^ `:30 A:30 := (exp A).obj B

@[simp, reassoc] lemma ev_coev :
Expand Down

0 comments on commit 8db2fa0

Please sign in to comment.