HoTT/HoTT-Agda — pull request #14 by mikeshulman (2014-06-08 23:29:33+00:00)
Title: lib.types.Nat: export injectivity of S, close #12

Again, let me know if I broke a convention. I renamed it `N-S-inj`, with a prefix to match the other exported lemmas, and shortened to match `equiv-inj`. I also replaced `N-get-S` by the standard truncated predecessor function `N-pred`.