Questions tagged [homotopy-type-theory]

For questions about the field of study known as homotopy type theory.

Filter by
Sorted by
Tagged with
0
votes
2answers
220 views

Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?

I've been curious about the 'geometric situation' that one has when considering the type $\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$. Here, addition is defined in the ...