This plugin is very useful to play with models or with forcing in direct style. Do you have further plans with it? E.g. cubical presheaves?
I have a couple of questions:
It does not support (co)fixpoints: were there particular difficulties to support them? The guard condition?
It seems that more possible interpretations of the universes have been investigated nowadays (I'm thinking e.g. to Sattler's construction of universes in presheaves, or also the "optimization" interpreting Prop by Prop and Type(i) by Type(i) in case the Hom are proof-irrelevant). There is also the combination with realisability (e.g. @ppedrot's "pre-prefascist" variant with parametricity). Do you have plans in this direction?
Also, I wonder whether you'd be interested in moving the plugin to coq-community. Other limitations I collected include the support for polymorphism (which naively would require mapping universes of the source to universes of the target?) and the support for the new term constructors Int, Float, Array, but that's maybe not a limitation enough to make it more visible.
Hi coq-forcing developers,
This plugin is very useful to play with models or with forcing in direct style. Do you have further plans with it? E.g. cubical presheaves?
I have a couple of questions:
PropbyPropandType(i)byType(i)in case theHomare proof-irrelevant). There is also the combination with realisability (e.g. @ppedrot's "pre-prefascist" variant with parametricity). Do you have plans in this direction?Also, I wonder whether you'd be interested in moving the plugin to coq-community. Other limitations I collected include the support for polymorphism (which naively would require mapping universes of the source to universes of the target?) and the support for the new term constructors
Int,Float,Array, but that's maybe not a limitation enough to make it more visible.