Skip to content

Commit 8d072d6

Browse files
committed
fix: add missing entries!
1 parent 3c577cf commit 8d072d6

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

CHANGELOG.md

+6
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,12 @@ Additions to existing modules
152152
module Section (surj : Surjective ≈₁ ≈₂ f)
153153
```
154154

155+
* In `Function.Construct.Symmetry`:
156+
```agda
157+
isBijectionWithoutCongruence : (IsBijection ≈₁ ≈₂ f) → IsBijection ≈₂ ≈₁ section
158+
bijectionWithoutCongruence : (Bijection R S) → IsBijection S R
159+
```
160+
155161
* In `Function.Properties.Bijection`:
156162
```agda
157163
sym : Bijection S T → Bijection T S

0 commit comments

Comments
 (0)