Comments (19)
What assumptions are you referring to?
from book.
Mainly the HSet assumptions, https://github.com/HoTT/Coq-HoTT/blob/7c6a120f1dd1ecd53266a52c2566aa0b24be2abc/theories/Algebra/Universal/Algebra.v#L44-L45
from book.
These theorems do not require hset assumptions. The file you refer to is part of a library for set-level universal algebra, but these theorems are more general than that in that they refer to arbitrary types (though more specific in that they refer only to the natural numbers rather than arbitrary initial algebras).
from book.
I tried to formalize 5.4.4 and 5.4.5 (Theorem 5.4.7 also), but couldn't without HSet assumptions; one last question, can we formalize these theorems in Coq without further assumptions?
from book.
It should be possible. Where are you stuck?
from book.
For 5.4.5, https://github.com/HyunggyuJang/HoTT/blob/655af1a877eefa0f1d99db926141053bfc44ff09/contrib/HoTTBook.v#L868-L894 is the attempt. For 5.4.4, https://github.com/HyunggyuJang/HoTT/blob/655af1a877eefa0f1d99db926141053bfc44ff09/contrib/HoTTBook.v#L850-L863.
Basically, without HSet assumption, I couldn't make it further, except the type equality (e.g. C = D between NAlgs of (C; (c0, c_s)) and (D; (d0, d_s)))
I'm aware that I can resolve equivalence problem aroused at https://github.com/HyunggyuJang/HoTT/blob/655af1a877eefa0f1d99db926141053bfc44ff09/contrib/HoTTBook.v#L848 like https://github.com/HoTT/Coq-HoTT/blob/master/theories/Algebra/Universal/Algebra.v#L103; nonetheless, it doesn't solve above problems.
from book.
Can you explain in words what goes wrong?
from book.
Yes, for 5.4.4, what I wanted to show is (C; (c0, c_s)) = (D; (d0, d_s))) given that both are N-initial algebras where C is the underlying type, c0 is the 0 element of C, and c_s is the successor, same for D. I was able to prove C = D; the rest is to prove (c0, c_s) = (d0, d_s) by transporting over p: C = D. But couldn’t prove it currently.
Note that, in the book, just noted “it is possible” but never worked further. If it possible to prove the theorems without HSet assumptions, I still think we need to augment the proof with more details, at least.
This phenomenon also occurs for 5.4.5 and 5.4.7.
from book.
What did you try? I think it should be a fairly straightforward unwinding of the fact that p
comes from an equivalence of N-algebras.
from book.
Let me get back after I fully tried with the issig approach (defining NAlg with Record, then change to sigma type to exploit properties for sigma type). I cannot answer how it goes wrong with the suggested approach for now.
from book.
The details can be found in:
Inductive types in homotopy type theory, Awodey, Gambino, Sojakova, arXiv:1201.3898,
and the Coq formalization cited there.
from book.
@awodey
Thanks for directing me to a valuable source! I’ll look into your paper with supporting formalization, https://github.com/HoTT/Archive/tree/master/LICS2012, and hopefully formalize 5.4.4 - 5.4.7 based on that!
from book.
@awodey Seems like Proposition 5 in your paper
couldn't formalize as it is; you added eta rules as axioms in https://github.com/HoTT/Archive/blob/master/LICS2012/two_is_hinitial/two_simp.v. Especially, eta rules cannot be derived from the elimination rule and beta rules, contrary to what asserted in the paper.
@mikeshulman Such eta rules are the culprits I met during the formalization of Thm. 5.4.4 ~ 5.4.7, which cannot be derived, as far as I know.
from book.
one of the the main results of the paper is:
dependent elimination ("induction") = simple elimination ("recursion") + eta
you are looking at a corollary of that, which says:
simple elimination + eta = h-initial
from book.
In particular, the eta-rule follows from dependent elimination, which you have in 5.4.5 and 5.4.7, and from h-initiality, which you have in 5.4.4.
from book.
@HyunggyuJang:
"Especially, eta rules cannot be derived from the elimination rule and beta rules, contrary to what asserted in the paper."
Everything in the formalization is just as it is asserted in the paper, which you should perhaps read more closely before making such an accusation!
from book.
Thanks for your detailed instruction, @awodey, I thought
This term follows from a propositional eta-rule, which is derivable by 2-elimination over a suitable identity type.
is an assertion that propositional eta-rules can be proved from the elimination rule and beta rules. I'll look through the paper more closely, to digest this sentence.
So, from the dependent elimination rule, we can derive simple elimination + eta rules; the part of Coq source code I linked is just stating
- simple elimination + eta = h-initial
I couldn't see this flow before. Now I can see the big picture of the paper. I'll go through it again based on your instruction. Sorry for the interruption, and again thanks for guiding me.
from book.
In particular, the eta-rule follows from dependent elimination, which you have in 5.4.5 and 5.4.7, and from h-initiality, which you have in 5.4.4.
Make sense once the eta-rule can be derived from dependent elimination; think if I can understand that piece, all the problems (I've believed to be) will be resolved. Much appreciated, @mikeshulman
from book.
@awodey Totally right. I overlooked the dependent elimination part. I should have fully understood before making any statement. I'm really sorry that I offended you; solely comes from my logical incapability. I learned a lot today, both in logical part and etiquette; will not make the same mistake from now on.
from book.
Related Issues (20)
- 自动驾驶更新笔记 Autopilot Updating Notes HOT 1
- Typos in proof of Lemma 10.3.12 HOT 5
- Use parentheses in the proof of Lemma 2.1.4(iii) HOT 3
- Cumulativity of the universe hierarchy HOT 4
- CI problem: "dubious ownership" HOT 1
- Provided Hashes in errata.pdf Not Found HOT 2
- Errata PDF unreadable
- Corollary 8.8.5 HOT 4
- Lemma 8.5.9 is missing a label
- Nightly builds pdfs are dead links HOT 8
- Exercise 7.3 could be made stronger
- Indexing of maps in fiber and exact sequences HOT 3
- proof-theoretic consistency in the introduction HOT 6
- cardinal numbers in the introduction HOT 5
- real numbers in the introduction HOT 7
- Switch to using truncated logic as default in the book HOT 2
- max and sup HOT 9
- Exercise 11.6 seems to need WLPO not LPO HOT 3
- Incorrect diagram for Example 8.7.16 HOT 1
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 book.