In type theory and categorical logic, a **quotient type** is a way to construct a new type from an existing type by identifying certain elements of that type as equivalent. It can be thought of as a generalization of the concept from set theory where you can form a quotient set by considering an equivalence relation on a set. ### Structure of a Quotient Type 1. **Base Type**: Start with a set or type \( A \).
New to topics? Read the docs here!