Epilogue

I’ve had an enquiry for more details on quotients in the new Epigram setup, so I’ll take that as a cue to blog a bit.

First, I’d better sketch some basics about propositions and equality. It’s the novel treatment of these things which lets us handle quotients in (hopefully) a neater way than has been possible thus far in a decidable type theory. The headlines:

• quotients given by a ‘carrier’ set, equivalence relation
• definitional equality on equivalence classes inherited from carrier on representatives
• propositional equality on equivalence classes is equivalence of representatives
• propositional equality is substitutive

The tabloid headline is STUFF YOUR SETOIDS.

I’d better fill in a bit of the necessary background information.

Each Set universe (and so far there is one, inconsistently containing itself, but later we shall have some sort of hierarchy) has a propositional subuniverse Prop, with an explicit embedding. If P : Prop, :- P is the set of its proofs. We abbreviate p : (:- P) by p :- P when we talk about proof objects at all.

We have heterogeneous propositional equality in a kind of worker-wrapper style: if S, T : Set, s : S, t : T, then (s:S)==(t:T), (s:S)<->(t:T) : Prop. We use == in public: it wraps a constructor around the corresponding <-> equation to stop it computing, so that we know an equation when we see one. We use <-> internally: it computes by recursion on the structure of sets to whatever is appropriate. We get to design <-> according to the observations we permit, where the traditional intensional equality enforces equality-by-construction, whether or not that’s how we think. For example, equality on functions computes like this:

  (f:(x:S)->T) <-> (f’:(x’:S’)->T’) =
    (x:S)(x’:S’)=>((x:S)==(x’:S’))=> (f x:T)<->(f’ x’:T’)

indicating that equal functions take equal inputs to equal outputs. (We write (x:S)=>P for universally quantified propositions to distinguish them from sets of dependent functions.) Note that heterogeneous equality has a conditional rather than a conjunctive meaning (unlike in Agda): ‘if the sets are equal, then the values are equal’ rather than ‘the sets are equal and the values are equal’. We have

  (P:Prop) <-> (Q:Prop) = (P => Q) /\ (Q => P)
  (p:-P) <-> (q:-Q) = TT

So what of quotients? Quotient X R rst : Set if X : Set, R : X -> X -> Prop, and rst :- Equivalence X R, where the latter expresses reflexivity, symmetry, and transitivity. Moreover, [x] : Quotient X R rst if x : X, so that each element of the carrier has an equivalence class. [x] and [x'] are definitionally equal in the quotient just when x and x’ are definitionally equal in X, so that’s finer than we want, but it’s what we can afford, operationally.

How do we observe quotients? We supply an elimination rule with a side condition.

qelim(X, R, rst, z : Quotient X R rst, P : Quotient X R rst -> Set,
    m : (x : X) -> P [x],
    ssh :- (x : X)(x’ : X) => R x x’ => (m x : P [x])==(m x’ : P [x']))
    : P z

That’s to say that the method m may access the underlying carrier elements provided you can prove it respects the equivalence, effectively keeping the choice of representative secret. Note the essential use of heterogeneous equality in stating this condition. As you might hope, this operator computes

  qelim(X, R, rst, [x], P, m, ssh) = m x

We’re nearly done. I should explain what happens for propositional equality, given that it’s type-specific. Equality on the sets is exactly structural

  (Quotient X R rst : Set) <-> (Quotient X’ R’ rst’) =
    (X : Set) <-> (X’ : Set) /\
    (R : X -> X -> Prop) <-> (R’ : X’ -> X’ -> Prop) /\
    TT

Equality on values is a wee bit sneaky. We are obliged to explain not when classes of a quotient are equal, but when classes of quotients plural are equal. This is tricky, as we cannot invoke the equivalence directly. However, the problem—heterogeneity—is also the solution.

  ([x]:Quotient X R rst) <-> ([x']:Quotient X’ R’ rst’) =
    (y:X’) => (x:X)==(y:X’) => R’ y x’

The above is logically equivalent to R’ x x’ whenever X and X’ coincide, which is also equivalent to R x x’ whenever the quotients are equal, which in turn is when we care about the meaning of equality for classes.

So that’s it. A quotient is a setoid stuffed into a set, an abstract datatype whose interface ensures representation-hiding. Correspondingly it’s reasonable to take the given equivalence as the ad hoc propositional equality, and to allow that equality to act substitutively.

What might we do with this? Fun combinatorial data structures (unordered pairs, bags, cycles, Joyal’s species of structures) should fit this picture. Quotients of free monads by equational theories are also a distinct possibility. Finger trees, anyone?

This entry was posted on Monday, February 8th, 2010 at 3:02 pm and is filed under General, Observational Type Theory. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.