fact: Definition IsTrunc_unfolded (n : trunc_index) (A : Type) := match n with | minus_two => { center : A & forall y, center = y } | n.+1 => forall x y : A, IsTrunc n (x = y) end.
imports: Basics.Notations Basics.Datatypes Basics.Logic