Skip to main content
MathOverflow

Return to Question

Clarify the meaning of "non-truncated quotients".
Source Link
Hexirp
Hexirp
  • 325
  • 2
  • 10

Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just generalized algebraic data types and non-truncated quotientsnon-truncated quotients?

Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just generalized algebraic data types and non-truncated quotients?

Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just generalized algebraic data types and non-truncated quotients?

Source Link
Hexirp
Hexirp
  • 325
  • 2
  • 10

Construct higher inductive types with only generalized algebraic data types and non-truncated quotients?

Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just generalized algebraic data types and non-truncated quotients?