This is a repo of my master's thesis written as part of my studies at the University of Wrocław.
Despite many applications for quotient types, Coq does not have built-in support for them. This thesis will discuss how to mitigate this problem by defining quotient-like types in which precisely one element exists for each abstraction class. We will focus on two approaches: the first relies on subtyping, while the second involves defining inductive types based on normalization traces. Additionally, we will mention other methods of defining quotient types, such as using setoids, additional axioms, or higher inductive types.