We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent f56cd9e commit b855ebcCopy full SHA for b855ebc
src/Function/Properties/Surjection.agda
@@ -67,9 +67,9 @@ trans = Compose.surjection
67
-- Other
68
69
injective⇒section-cong : (surj : Surjection S T) →
70
- (open Surjection surj) →
71
- Injective Eq₁._≈_ Eq₂._≈_ to →
72
- Congruent Eq₂._≈_ Eq₁._≈_ section
+ (open Surjection surj) →
+ Injective Eq₁._≈_ Eq₂._≈_ to →
+ Congruent Eq₂._≈_ Eq₁._≈_ section
73
injective⇒section-cong {T = T} surj injective {x} {y} x≈y = injective $ begin
74
to (section x) ≈⟨ section-strictInverseˡ x ⟩
75
x ≈⟨ x≈y ⟩
0 commit comments