[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Type theory (dependent function types, dependent sum types, identity types, function extensionality) -> Predicate logic -> Set theory -> Number theory For $Q:(S \to \mathrm{Bool}) \to \mathrm{Prop}$ we have $$\mathrm{hasAllFiniteSubtypes}(Q) \coloneqq ((\lambda x:S.\mathrm{false}) \in Q) \times \prod_{A:S \to \mathrm{Bool}} \prod_{B:S \to \mathrm{Bool}} (A \in Q) \to (\exists!x:S.B(x) =_\mathrm{Bool} \mathrm{true}) \to \left(\prod_{x:S} A(x) \wedge B(x) =_\mathrm{Bool} \mathrm{false}\right) \to ((\lambda x:S.A(x) \vee B(x)) \in Q)$$ Then we have that $$B(S) \coloneqq \sum_{Q:(S \to \mathrm{Bool}) \to \mathrm{Prop}} \mathrm{hasAllFiniteSubtypes}(Q) \times \prod_{R:(S \to \mathrm{Bool}) \to \mathrm{Prop}} \mathrm{hasAllFiniteSubtypes}(R) \to \prod_{C:S \to \mathrm{Bool}} (C \in Q) \to (C \in R)$$ category: redirected to nlab