Groupoid Model of HoTT in Lean 4
Authors