Skip to main content

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)

Filter by
Sorted by
Tagged with
3 votes
1 answer

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: ...
user avatar
3 votes
2 answers

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 ...
Russoul's user avatar
  • 345
6 votes
1 answer

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 (<...
Max Fan's user avatar
  • 61
11 votes
1 answer

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 ...
Dario's user avatar
  • 213
9 votes
1 answer

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 <...
Joey Eremondi's user avatar
41 votes
3 answers

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 ...
setholopolus's user avatar
13 votes
3 answers

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 ...
Greg Nisbet's user avatar
  • 3,095