# Questions tagged [quotient]

In type theory a quotient type is an algebraic data type that represents a type whose equality relation has been redefined by a given equivalence relation such that the elements of the type are partitioned into a set of equivalence classes whose cardinality is less than or equal to that of the base type. (from Wikipedia)

7 questions
Filter by
Sorted by
Tagged with
106 views

### How to lift a binary function to a quotient?

Kia ora :) I am trying to use Quot. in Lean4 to define the integers as the quotient of the Cartesian product of two copies of the natural numbers (type Peano) under the relation: ...
187 views

### State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

I don't think a particular choice of such type theory matters much. Extensional MLTT, SetoidTT, OTT, HoTT, HOTT, CuTT -- they all support quotient types. Reals is supposed to be a Set (in HoTT ...
• 345
494 views

### Paths Between Quotient Types in Cubical Agda

I'm new to Cubical Agda and I am trying to define the dependent set eliminator for certain quotient types. In particular, my quotient type is the integers, quotiented by the absolute value function (<...
• 61
291 views

### Seven Trees in One, or How to formalize the Semiring of Types?

This is somewhat conceptual beginner's question about proof assistants. I've been re-reading the famous Seven Trees in One / Objects of categories as complex numbers. The gist: The type $T$ of binary ...
• 213
349 views

### Case splitting with quotient types in Cubical Agda

I'm getting started with Cubcal Agda and I'm quite confused. I've got a HIT A defined, with a path constructor eq returning <...
3k views

### What exactly is setoid hell?

One of the only arguments I've heard about why Lean is better than Coq is that you can construct quotients of built-in structures by default. (In Coq, you apparently have to use Setoids instead of ...
• 511
359 views

### What are the possible kinds of type theories or logics with quotients?

As described in this answer, one of the differences between Coq and Lean is the presence of definitional quotients in the latter. By contrast, the absence of definitional quotients in Coq forces one ...
• 3,095