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)
3
questions
8
votes
1
answer
165
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 <...
- 475
28
votes
2
answers
561
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 ...
- 381
12
votes
3
answers
227
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 ...
- 2,477