Comments (11)
FTR I asked about semantics of strict path computation rules on Zulip and it doesn't look good. It doesn't seem to be known to be possible to have strict path computation rules. So there is that to keep in mind.
On the other hand, cubical agda has them, but the semantics of cubical type theory deal with HITs in a way that allows for them. They don't run into the issue of trying to relate Id's J and HIT eliminators. Then again, I have no idea what a model of cubical sets is supposed to correspond to in homotopy theory.
from coq-hott.
It would be nice to resolve the semantic issue, but until then, I guess we should avoid this.
Symbol Circle_rec : forall (P : Type), P -> (paths base base) -> Circle -> P.
Just a minor point that this doesn't have the right type. paths base base
should instead be a loop in P
at the chosen point.
from coq-hott.
I didn't notice it the first time, but since Circle_rec ?B ?b ?loop base
can reduce, your second rewrite rule would in practice never be triggered and you would be stuck with a term match loop return paths ?b ?b with idpath => idpath end
which would not reduce.
I guess the better solution using rewrite rules would be to do what ThΓ©o Winterhalter suggested, a symbol for ap
and a reduction for ap ?f idpath
.
from coq-hott.
That also appears to be the suggestion semantically, but this is not a desirable thing to have. ap
appears naturally unrelated to the HIT in question, so I think it would be quite awkward to have to translate back and forth, defeating the purpose of the rewrite rule for the path eliminator in the first place.
from coq-hott.
Is it not possible to have a single symbol ap
satisfying rewrite rules for all HITs? Do the rewrite rules for a given symbol have to all be declared at the same time?
from coq-hott.
The rewrite rules don't have to be declared at the same time. Since they are added to the environment as a block, this is necessary to have rewrite rules which have a correct type thanks to previous rewrite rules (and it's also just convenient).
from coq-hott.
Ok, then we could just declare the symbol ap
along with its rewrite rule for refl
in Overture
, and then whenever we introduce a new HIT we give ap
a rewrite rule for the eliminator of that HIT. I very much doubt we ever use the fact that ap
is defined by path induction rather than just its rewrite rule for refl
.
from coq-hott.
That also appears to be the suggestion semantically, but this is not a desirable thing to have.
ap
appears naturally unrelated to the HIT in question, so I think it would be quite awkward to have to translate back and forth, defeating the purpose of the rewrite rule for the path eliminator in the first place.
But it might work if we used the new ap
symbol everywhere that we currently use the ap
defined by path induction. I think I know one or two places where we use that some other path induction specializes to our current ap
definitionally, so a lemma would be needed there, but I think it's fairly rare. (This comment overlapped with Mike's, but I'm still adding it because I do know one or two places where I currently rely on the definition of ap
.)
from coq-hott.
Oh, okay, I'm surprised. But it should be rare and easy to work around, as you say.
from coq-hott.
I wonder whether one could prove a conservativity result for a type theory with a primitive ap
and apd
and definitional path-constructor computation over ordinary Book HoTT. It feels kind of like saying we introduce a new thing ap
/apd
, and then we say how that new thing computes, and so it's almost like a "definitional extension".
from coq-hott.
With my logician hat on, I like to think of strict path computation rules as something akin to cut elimination. I would expect that if the two versions of HoTT really do have the same models, then there ought to be some syntactic procedure allowing you to transform proofs in the slightly stricter HoTT to book HoTT. Comparing the size of say the 3x3 lemma for pushouts' proof in cubical type theory vs Brunerie's proof, its easy to see there is quite a large blowup in various metrics for proof size. This is something that reminds me of the size of proofs with cut eliminated in classical logic.
As you put it @mikeshulman (faster than I could write), this would essentially be equivalent to a conservativity result about these two type theories.
The lack of such a result is still something that makes me uncomfortable however. Even if both HoTTs had the same models, the fact that we don't have anything like completeness for HoTT, means that there is still the question of "is this provable in the weaker theory?".
Practically this would mean we would second-guess every result we prove here with respect to book HoTT.
from coq-hott.
Related Issues (20)
- Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 HOT 11
- Generate coqdoc using Dune
- Library description for a handbook chapter HOT 5
- HITs in Spaces/No/Core.v might be inconsistent HOT 1
- Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 HOT 1
- coqdoc section links don't work for alectryon and timing toc pages HOT 1
- experiment with Hint Constants Opaque in typeclass search HOT 3
- Generalise ExactSequence.v to a pointed wildcat with kernels HOT 1
- Flattening lemma for GraphQuotient HOT 6
- Add transport lemmas for families of equivalences
- Split HIT files into Core and lemmas HOT 2
- slow builds with Coq 8.19 and/or dune 3.14.0 HOT 19
- Dependences of Nat/Core.v and DProp.v HOT 4
- Bifunctors HOT 12
- Generalise results about wedge for pointed categories
- Preservation of products
- Show that pType has all coproducts
- Change definition of smash HOT 2
- Project: coherence for monoidal categories HOT 4
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
π Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. πππ
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google β€οΈ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq-hott.