Commit 2017-11-24 05:18 bade51a0

View on Github →

feat(data/quot): add trunc type (like nonempty in Type) It is named after the propositional truncation operator in HoTT, although of course the behavior is a bit different in a proof irrelevant setting.

Estimated changes

Modified data/quot.lean

modified theorem forall_quotient_iff

added theorem quot.out_eq

added theorem quotient.mk_out

added theorem quotient.out_eq

added theorem trunc.exists_rep

added theorem trunc.ind

added def trunc.lift

added def trunc.mk

added theorem trunc.out_eq

added def {u}