Abstract:

Abstract: We start by discussing pushouts and (-1)- and 0-truncations, then we use these to discuss quotients of sets by mere relations and algebraic structures on sets. We finish with a particular case of the flattening lemma, which says that if W is a particular higher inductive type, then the total space of the fibration corresponding to a presheaf on W is equivalent to an appropriate higher inductive type.