Categories with families and first-order logic with dependent sorts

Erik Palmgren

First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic…