Post #2121596

@ltchen @MartinEscardo @typeintype Peter Lumsdaine also gave a nice talk about setoids and univalent categories at the Palmgren memorial conference in 2020: https://logic.math.su.se/palmgren-memorial/slides/Lumsdaine-slides-Palmgren-memorial-conference.pdf