BeTTI.Quotient

Definitions

0 (//) : (type : Type) -> (type -> type -> Type) -> Type

  Quotient type
  type   : type to quotient
  rel : proof-relevant relation to quotient by

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 6

class : type -> type // rel

  Equivalence class of input element

Totality: total
Visibility: export

.because : (f : (type -> motive)) -> (0 _ : ((x : type) -> (y : type) -> rel x y -> f x = f y)) -> type // rel -> motive

  Eliminator for quotients
  f : eliminator for quotiented type
  motive: the reason for the elimination (to inhabit motive)

Totality: total
Visibility: export

0 quotient : rel x y -> class x = class y

  Related elements are equal in the quotient

Totality: total
Visibility: export

.Because : {0 b : a // rel -> Type} -> (f : ((x : a) -> b (class x))) -> (0 _ : ((x : a) -> (y : a) -> r x y -> f (class x) = f (class y))) -> (x : a // r) -> b x

  Dependent eliminator for quotients. Untested

Totality: total
Visibility: export