Augment assumptions for Thm 5.4.4, 5.4.5, and 5.4.7

[HyunggyuJang]

https://github.com/HoTT/book/blob/16a4bfa34919b94b8a56a75bc77b40278a0857dd/induction.tex#L459

From Coq-HoTT, it is generalized as a (universal) Algebra type, where additional assumptions has been made.

I think those assumptions should be added to the text explicitly unless cannot prove the theorems.

[mikeshulman]

What assumptions are you referring to?

[HyunggyuJang]

Mainly the HSet assumptions, https://github.com/HoTT/Coq-HoTT/blob/7c6a120f1dd1ecd53266a52c2566aa0b24be2abc/theories/Algebra/Universal/Algebra.v#L44-L45

[mikeshulman]

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).

[HyunggyuJang]

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?

[mikeshulman]

It should be possible. Where are you stuck?

[HyunggyuJang]

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.

[mikeshulman]

Can you explain in words what goes wrong?

[HyunggyuJang]

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.

[mikeshulman]

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.

[HyunggyuJang]

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.

[awodey]

The details can be found in: Inductive types in homotopy type theory, Awodey, Gambino, Sojakova, arXiv:1201.3898, and the Coq formalization cited there.

[HyunggyuJang]

@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!

[HyunggyuJang]

@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.

[awodey]

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

[mikeshulman]

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.

[awodey]

@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!

[HyunggyuJang]

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.

[HyunggyuJang]

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

[HyunggyuJang]

@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.