Closed jonsterling closed 6 years ago
(P.S. This would need to be a "cubical logical framework", in the sense of being indexed in cubes. I do not think it is necessary to have any Kan structure at the LF-level, however, so the semantics of the logical framework could just be the obvious CWF in the category of cubical sets. /cc @freebroccolo)
We would probably need to have some kind of an adjunction between a cubical logical framework and a "nominal" logical framework, and could work with the latter via the monad of the adjunction or something. This is necessary for formulating the operational semantics of CTT.
Sounds interesting. It's been awhile since I've worked on the LF thing we were talking about earlier. I suppose the more recent cubical setoids stuff was supposed to be a part of that story though. Anyway, I'd be interested to hear more about what you have in mind if you want to chat about it sometime.
Bob and I (and separately Danny and I) have been talking about the ultimate necessity of developing a higher order logical framework to replace second-order syntax. This is a huge undertaking, so it should not be taken lightly—we would need to think carefully about the design, and ensure that we can use it to achieve our aims.
Bob suggests something along the lines of Martin-Löf's "semantic" logical framework might be called for, because each type comes with its equations. Ours would have more of a "refinement" flavor in the sense that types could share elements. The way that it might play out is the following:
Each categorical judgment would be defined as a LF type—namely, the type of its synthesis/evidence. Because of the way that MLLF works, this entails also defining an equivalence relation on this evidence. As an example, the
A true
judgment would be a family of (LF) typesTrue(A) : type
, and eachTrue(A)
would have an equivalence relation, which would be the CTT equality for the members ofA
. A more mysterious example could be the family of (LF) typesSynth(R)
whose elements would be the possible CTT types of the termR
identified up to CTT type equality.The functional sequent judgment simply be defined as the LF
Pi
type. This means that the appropriate functionality conditions that are needed for CTT/Nuprl sequents would be induced automatically.Higher-order generic judgments would be immediately possible using the LF
Pi
type. "Derived rules" would just be a mode of use of this.To make this practical for use in a proof assistant, we would need to use a variadic version of the
Pi
type, where you quantify overn
variables.This is all probably also related to what @freebroccolo and I have been discussing in the past several months.
/cc @cangiuli @jozefg