Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: type of propositions

Bottom of Page

1 to 12 of 12

  1.  
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeDec 1st 2016

    Is there any point to having both type of propositions and Prop? The analogous page-name Type is a redirect to type of types.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeDec 1st 2016

    Not sure why this happened. I have merged the two entries now.

  3. added a section on the definition of types of propositions

    Anonymous

    diff, v9, current

  4. added rules for the type of all propositions

    Anonymous

    diff, v13, current

    • CommentRowNumber5.
    • CommentAuthorGuest
    • CommentTimeOct 17th 2022

    Should be possible to define the type of propositions via the universal property of the subobject classifier, something like

    ΓctxΓ⊢Ωtype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \Omega \; \mathrm{type}} ΓctxΓ⊢true:Ω\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{true}:\Omega} Γ⊢AtypeΓ⊢BtypeΓ⊢i:A↪BΓ⊢χ B:B→Ω\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash i:A \hookrightarrow B}{\Gamma \vdash \chi_B:B \to \Omega}

    et cetera

    • CommentRowNumber6.
    • CommentAuthorChristian Sattler
    • CommentTimeOct 17th 2022
    • (edited Oct 17th 2022)

    That’s effectively being done already when you say every proposition is classified by Ω\Omega. To derive your proposed rule, consider the proposition in context Γ.(b:B)\Gamma.(b : B) of preimages of bb under ii.

    Side note: we don’t currently have models of the type of all propositions (as currently defined, with a meta-equality El(A Ω)≡A\mathsf{El}(A_\Omega) \equiv A) in HoTT.

  7. added section on the type of all decidable propositions, or the type of booleans

    Anonymous

    diff, v17, current

  8. Added rules for the type of all propositions as a Russell universe.

    Anonymouse

    diff, v21, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeAug 2nd 2023

    Incidentally, I see that this entry is lacking any reference to subtype.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeAug 2nd 2023

    added a sentence to the Idea-section which cross-links back to subtype.

    diff, v22, current

  11. Moved the sections on the “type of decidable propositions” and “type of booleans” from this article over to boolean domain, since those definitions are really talking about defining the boolean domain

    diff, v29, current

  12. More reorganizing of this page - moved subsection titled “the empty proposition and falsehood” under a new section “Properties” and showed how to directly construct the empty type from the type of propositions and dependent function types, and how to show that the empty type is a proposition.

    diff, v29, current

1 to 12 of 12

  1.