Add Binary Sum Types and Truncations #12
Conversation
still working on cases
There was a problem hiding this comment.
Hello Bruno, thanks for the contribution!
Would you be willing to share the motivation for these additions?
Looking at the typing rules, what is called truncation here seems to be a generic monad (with just the left identity law).
Since the formalisation already has Sigma types, an alternative to the sum type would have been booleans or more generally, finite (enum) types. Then disjoint sum types would be encodable with Sigma. Or maybe they already are as Sigma Nat T where T zero = A and T (suc n) = B.
| → Γ ⊢ u ∷ A ▹▹ C | ||
| → Γ ⊢ v ∷ B ▹▹ C | ||
| → Γ ⊢ C -- necessary? | ||
| → Γ ⊢ cases C t u v ∷ C |
There was a problem hiding this comment.
So case distinction on the binary sum is non-dependent, it seems.
| → Γ ⊢ B | ||
| → Γ ⊢ a ∷ A | ||
| → Γ ⊢ f ∷ A ▹▹ ∥ B ∥ | ||
| → Γ ⊢ ∥ₑ B (∥ᵢ a) f ≡ f ∘ a ∷ ∥ B ∥ |
There was a problem hiding this comment.
What is called "truncation" here looks like a generic monad with just the left identity law.
Are there any special equalities for truncation (like extensionality laws)?
|
(Notes to myself from looking at the CI results:)
|
We have extended the type theory with binary sum types denoted
A ∪ Band truncations denoted∥ A ∥and proved decidability of conversion for this extended theory.