Began implementing intrinsically typed regions #476
Conversation
There was a problem hiding this comment.
LGTM after changes I've made, but also ping @tobiasgrosser. @alexkeizer on Zulip.
|
Alive Statistics: 59 / 93 (34 failed) |
SSA/Core/ErasedContext.lean
Outdated
| /-- | ||
| Typeclass for a `baseType` which supports Gödel codes for coproducts | ||
| -/ | ||
| class TyHasCoprodDenote (β : Type) [TyDenote β] [C : TyHasCoprod β] where | ||
| inl : toType a → toType (C.coprod a b) | ||
| inr : toType a → toType (C.coprod a b) | ||
| elim : (toType a → γ) → (toType b → γ) → toType (C.coprod a b) → γ | ||
|
|
||
| /- | ||
| TODO: implement a thing `left? : toType (C.coprod α β) → Option (toType α)` using `elim`. This will | ||
| allow us to cleanup case_inl by writing `(ha : (l : toType α) ∈ a.evaluate VΓ |>.left?)` | ||
| -/ | ||
|
|
||
| /- | ||
| TODO: add lawful instance of TyHasCoprodDenote for proving properties about the universal property. | ||
| -/ |
There was a problem hiding this comment.
Would it be easier to have LawfulTyHasCoprod simply state that for all a, b : Ty, it is the case that toType (C.coprod a b) is equivalent to Sum (toType a) (toType b), then you would not need TyHasCoprodDenote at all anymore
There was a problem hiding this comment.
I don't think that suffices, because my iso can be non-natural. I can do the terrible trick I showed you last time, where I match on a : Ty and build something super non-canonical.
There was a problem hiding this comment.
my iso can be non-natural
I'm not sure what natural means in this context?
You're right that this equivalence is stronger than TyHasCoprodDenote as currently stated, but surely a Lawful version would impy the equivalence?
Normally, you'd separate out the laws into a separate typeclass to facilitate programming where you might not necessarily care about things being 100% lawful, but that hardly seems applicable in our setting; if you're just programming you'd probably use untyped datastructures, rather than our highly dependent ones.
Co-authored-by: Siddharth <[email protected]>
|
Alive Statistics: 59 / 93 (34 failed) |
|
Alive Statistics: 59 / 93 (34 failed) |
No description provided.