It's just a theorem prover. Like every theorem prover it has a logic that you use for stating propositions, and proving theorem. The logic is a specific logic

It's just a theorem prover. Like every theorem prover it has a logic that you use for stating propositions, and proving theorem. The logic is a specific logic that is closely related to HoTT.