Questions about certain HoTT rules...