QuotientOver

structure QuotientOver[T] {
    qrel: QuotientRelation[T]
    carrier: Set[T]
} constraint {
    is_equivalence_class(qrel.rel, carrier)
}

A quotient element whose relation is carried as part of the element.

GitHub

---

carrier

QuotientOver.carrier: QuotientOver[T] -> Set[T]

The equivalence class represented by this quotient element.

qrel

QuotientOver.qrel: QuotientOver[T] -> QuotientRelation[T]

The equivalence relation whose classes form this quotient element.