Injective type families imply nominal injectivity, but NOT rep inj

Authored by ezyang on Feb 26 2017, 11:10 PM.