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 : {A|Type(0)}{R:A->A->Prop}{C|Type}{f:A->C} ({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 [[A|Type(0)][R:A->A->Prop][C|Type][f:A->C] [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 = ... : {A|Type(0)}{R:A->A->Prop}{C|Type}{f,g:A->C} {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 = ... : {A|Type(0)}{R:A->A->Prop}{C|Type}{P:C->Prop}{f:A->C} {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