Augment assumptions for Thm 5.4.4, 5.4.5, and 5.4.7 about book HOT 19 CLOSED

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.