search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

Non-trivial argument types in CITs #202

Open jonsterling opened 6 years ago

jonsterling commented 6 years ago

Right now, the only kind of "argument type" allowed is just Self; this should be generalized to A -> Self, where A is a type. Combining this with #200, the W-type connective would be definable.

favonia commented 6 years ago

And maybe path types too.

jonsterling commented 6 years ago

@favonia Yes, a formal extension type would be very cool!

jonsterling commented 6 years ago

@ecavallo @favonia IMO now that we are finishing #347, this ticket should be the next priority for the CIT project. I'd like us to add the "family recursive argument spec" (i.e. A -> R, where R is a recursive argument spec) first, because this lets us generalize W-types. It will also let me define cool examples like some kinds of interaction trees...

jonsterling commented 6 years ago

@ecavallo I guess a first step would be to define an operator in the semantic domain that does the thing that act in Part IV does, or what is called func in the short paper version. In order to implement this for the formal function spec, we may need to add a new form of closure. Any Thoughts, @favonia?

favonia commented 6 years ago

@jonsterling IMO the essence is the "obvious" non-dependent interpretation (in the data type) and the dependent type interpretation (in the codomain of the eliminator of the data type). You can add whatever you like as long as it makes sense both non-dependently and dependently. Once these two interpretations are settled, I believe what act should do will be obvious.

PS: The act was called func, so we understand both. :smile: @ecavallo

favonia commented 6 years ago

My hypothesis is that the dependent interpretation of a recursor is a recursor with dependent interpretations of the motive and methods. Have not checked anything carefully yet. Peter Lumsdaine and @ecavallo have thought about this much more than I do. (I wanted to tag Peter but was afraid that we are using a cryptic language to discuss higher inductive types.)