Skip to main content
MathOverflow

Return to Answer

added 14 characters in body
Source Link
Madeleine Birchfield
Madeleine Birchfield
  • 2.6k
  • 1
  • 7
  • 23

Given a typeuniverse $A:U$$U$, the type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$ ForGiven a type $A:U$, for $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The set-truncation of $A$ is the quotient set $$[A]_0 \equiv \sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$

In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.

Given a type $A:U$, the type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$ For $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The set-truncation of $A$ is the quotient set $$[A]_0 \equiv \sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$

In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.

Given a universe $U$, the type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$ Given a type $A:U$, for $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The set-truncation of $A$ is the quotient set $$[A]_0 \equiv \sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$

In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.

added 14 characters in body
Source Link
Madeleine Birchfield
Madeleine Birchfield
  • 2.6k
  • 1
  • 7
  • 23

Given a type $A:U$, forthe type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$ For $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The quotient set $$\sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$ is the set-truncation of $A$. is the quotient set $$[A]_0 \equiv \sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$

In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.

Given a type $A:U$, for $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The quotient set $$\sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$ is the set-truncation of $A$. In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.

Given a type $A:U$, the type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$ For $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The set-truncation of $A$ is the quotient set $$[A]_0 \equiv \sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$

In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.

Source Link
Madeleine Birchfield
Madeleine Birchfield
  • 2.6k
  • 1
  • 7
  • 23

Given a type $A:U$, for $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The quotient set $$\sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$ is the set-truncation of $A$. In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.