Track HLevels of Sets and Theories#40
Conversation
olynch
left a comment
olynch
left a comment
There was a problem hiding this comment.
Overall looks quite good.
What is the rational behind having a distinction between SetTheory and SetPropTheory? Maybe FunctionVariant should be a record of two things: SetTheory | TheoryTop and then the h-Level of the codomain.
This will also need to be rebased against ts-ffi-trunk, because that may have some changes to the Haskell. I will merge this in after ts-ffi-trunk is merged in.
olynch
left a comment
olynch
left a comment
There was a problem hiding this comment.
Looks good, I'll rebase and merge.
olynch
force-pushed
the
coln-compiler/hlevels
branch
from
a17ec09 to
28e6913
Compare
olynch
left a comment
olynch
left a comment
There was a problem hiding this comment.
There's a mysterious failing test now
|
Web demo preview: https://pr-40--coln-web-demo.netlify.app |
mvr
force-pushed
the
coln-compiler/hlevels
branch
from
26b4702 to
09fef4a
Compare
olynch
left a comment
olynch
left a comment
There was a problem hiding this comment.
Just one minor change; I think we can drop PropTheoryU.
| = PropU | ||
| | SetU | ||
| | TheoryU | ||
| | PropTheoryU -- TODO: better name? |
There was a problem hiding this comment.
We could call this LawU, but also I can't think of a case where we would ever use this universe, so we don't need to put it in for now. A propositional theory can be encoded into TheoryU, and when it is decoded we still can know that it is propositional, because decode . code is the identity.
2 participants
Split Level into Sort (Set/Theory) and HLevel (HProp/HSet).
I haven't looked into realms yet, so I don't know how this is supposed to interact with "EltOf" etc.