Homotopy Type Theory predicate > history (changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

~~Definition~~

~~predicate~~ ~~over a type~~ ~~$A$~~ ~~is a~~ ~~type family~~ ~~$P$~~ ~~such that for every~~ ~~$a:A$~~ , ~~$P(a)$~~ ~~is a proposition:~~

~~$a:A \vdash \pi(a):isProp(P(a))$~~
~~See also~~

relation

proposition

type family

~~category: not redirected to nlab yet~~

Last revised on June 16, 2022 at 02:31:57. See the history of this page for a list of all contributions to it.