# Contents

## Idea

In type theory the kind of type corresponding in categorical semantics to a quotient object / coequalizer.

## Properties

Quotient type may be constructed as higher inductive types. See here

Revised on January 10, 2013 19:14:37 by Urs Schreiber (89.204.153.52)