Notions of anonymous existence in Martin-Löf type theory
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Published: |
IfCoLog
2016
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/38092/ |