What is the state of the art on adding quotients types to simple type theory? Bart Jacobs has written a lot about it in a categorical setting that suits me very well. But I wonder how other proof theorists have handled it. best, Colin