next up previous contents
Next: Relations Up: The LEGO library - Previous: Vector Basics

Quotient Types

The directory lib_quotient contains one file which defines a notion of quotient types. The file defines a new type operator QU which takes a type and a relation and produces a new type representing the quotient of the old type by the relation. Elements of the quotient type are given by the operator QU_class which takes an element in the underlying type to one in the quotient, i.e. the equivalence class of the element. The assumption QU_cor then states that the equivalence classes of related elements are equal. The assumption QU_it restricts the function space on quotient types to only those functions which respect the relation used to form the quotient. Then QU_ind says that all elements of the quotient are the equivalence class of some element of the original type. The reduction rule allows function application to normalise as expected. These definitions allow one to reason with a non-substitutive equality as if it were substitutive.

Only for the final theorem do we actually need to assume that the relation quotiented by is a equivalence. This theorem also requires the assumption of extensionality of propositions.

 ** Module lib_quotient Imports lib_eq_basics
 $ext_prop : {X,Y:Prop}(X->Y)->(Y->X)->Eq X Y
 $QU : {A|Type(0)}(A->A->Prop)->Type(0)
 $QU_class : {A|Type(0)}{R:A->A->Prop}A->QU R
 $QU_cor :
    {A|Type(0)}{R:A->A->Prop}{a1,a2:A}(R a1 a2)->
    Eq (QU_class R a1) (QU_class R a2)
 $QU_it :
    ({a1,a2:A}(R a1 a2)->Eq (f a1) (f a2))->(QU R)->C
 $QU_ind :
    {A|Type(0)}{R:A->A->Prop}{P:(QU R)->Prop}({a:A}P (QU_class R a))->
    {q:QU R}P q
 [H:{a1,a2:A}(R a1 a2)->Eq (f a1) (f a2)][a:A]
    QU_it R f H (QU_class R a)  ==>  f a]

  QU_xi = ... :
    {p:{a1,a2:A}(R a1 a2)->Eq (f a1) (f a2)}
    {q:{a1,a2:A}(R a1 a2)->Eq (g a1) (g a2)}({a:A}Eq (f a) (g a))->
    {x:QU R}Eq (QU_it R f p x) (QU_it R g q x)
  QU_it_ind = ... :
    {p:{a1,a2:A}(R a1 a2)->Eq (f a1) (f a2)}({a:A}P (f a))->{x:QU R}
    P (QU_it R f p x)
  QU_in_class = ... :
    {A|Type(0)}{R:A->A->Prop}(sym R)->(trans R)->A->(QU R)->Prop
  QU_cor_inv = ... :
    {A|Type(0)}{R:A->A->Prop}(refl R)->(sym R)->(trans R)->{a,b:A}
    (Eq (QU_class R a) (QU_class R b))->R a b

Conor McBride