> The syntax rules for modal operators ◻ {\displaystyle \Box } and
◊ {\displaystyle \Diamond } are very similar to those for universal and existential quantifiers; In fact, any formula with modal operators ◻ and ◊, and the usual logical connectives in propositional calculus (
∧
,
∨
,
¬
,
→
,
↔
can be rewritten
> box operator □ is a functor
Functor > Relation to other categorical concepts: https://en.wikipedia.org/wiki/Functor#Relation_to_other_cate...
Modal operator: https://en.wikipedia.org/wiki/Modal_operator ,:
> The syntax rules for modal operators ◻ {\displaystyle \Box } and ◊ {\displaystyle \Diamond } are very similar to those for universal and existential quantifiers; In fact, any formula with modal operators ◻ and ◊, and the usual logical connectives in propositional calculus ( ∧ , ∨ , ¬ , → , ↔ can be rewritten
□ signifies a D'Alembert operator in physics, not logic: https://en.wikipedia.org/wiki/D%27Alembert_operator
HoTT may be the ultimate extension of category theory?
"Natural Number Game: build the basic theory of the natural numbers from scratch" https://news.ycombinator.com/item?id=42440016#42444882
"Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?" https://link.springer.com/article/10.1007/s10516-023-09676-0 .. https://news.ycombinator.com/item?id=43191103 :
HoTT in Lean4: https://github.com/forked-from-1kasper/ground_zero