Intro to HoTT No. 2, Part 2
An essential piece of HoTT is judgmental equality, which is how we state that two things are "equal by definition". In this video, I explain (what I consider to be) the most helpful intuition for judgmental equality: computational confluence. Two terms (or types) in HoTT are judgmentally equal if they can be computed to the same thing. This turns out to be a fruitful way to think of judgmental equality, particularly because computer formalization is important to us. Later on, we'll improve upon judgmental equality to get another notion of equality, propositional equality, which is the central object of study in homotopy type theory.
