# Start a new discussion

## Not signed in

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

## Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeJan 2nd 2023

added the following redirects (which used to point to truth value):

  [[!redirects boolean]]
[[!redirects booleans]]

[[!redirects Boolean]]
[[!redirects Booleans]]


and to

  [[!redirects Bit]]


and cross-linked with bit and more terms (such as top and bottom)

added reference to the Wikipedia entry

will next add inference rules for Bool as an inductive type…

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeJan 2nd 2023

spelled out (here) the type inference rules.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJan 3rd 2023

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJan 5th 2023

added a paragraph (here) making explicit that $Bit \;\simeq\; S^0$, and used the occasion for the fun remark that in this sense the $S^n$ are types of “higher homotopy bits”

am making a corresponding edit also at 0-sphere

1. added section about the boolean domain’s rules with typal computation and uniqueness rules, and the corresponding dependent universal property of the boolean domain

Anonymous

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJan 24th 2023

Not sure if it makes sense to duplicate the rules in this way, it seems confusing without comment. Maybe better to merge the two rule sets and add a comment below on the different posdibilities of equality in the computation rule.

• CommentRowNumber7.
• CommentAuthorGuest
• CommentTime4 days ago