Re: Equality constraints (~): type-theory behind them