We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 667ec3b commit e967e02Copy full SHA for e967e02
1 file changed
src/plfa/part1/Connectives.lagda.md
@@ -90,7 +90,7 @@ constructor is the identity over products:
90
```
91
For record types, η-equality holds *by definition*.
92
While proving `η-×`, we do not have to
93
-pattern match on `w` to know that η-equality holds
+pattern match on `w` to know that η-equality holds.
94
95
We set the precedence of conjunction so that it binds less
96
tightly than anything save disjunction:
0 commit comments