-definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
-≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6x:A.z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
+\ 5img class="anchor" src="icons/tick.png" id="surjective"\ 6definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
+≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6x:A\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.