next

previous

contents

index

Next: SET Up: The Rules Previous: PRODUCT

QUOTIENT

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* formation universe_intro_quotient(A E x y z): term

term

tok

tok

tok

rule.

quotient_formation(x y z): tok tok tok rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* canonical quotient_intro(level): int

rule.

quotient_equality_element(level): int rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* noncanonical quotient_elim (hyp level v w): int

int

tok

tok

rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* equality quotient_equality(r s): tok

tok

rule.

quotient_equality_element(level): int rule.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995