Univalent higher categories via complete semi-segal types
Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.)solves this by considering only truncated types, roughly corresponding to an ordin...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Published: |
Association for Computing Machinery
2018
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/49374/ |