Fresh PR: Integers as Higher Inductive Type implementation in Coq by maxipetro · Pull Request #41 · jdchristensen/HoTT

maxipetro · 2026-04-29T13:22:38Z

This is a fresh PR for the implementation of Integers as Higher Inductive Type implementation in Coq following [Altenkirch and Scoccola 2020].

jdchristensen · 2026-04-29T14:13:25Z

Now that we've merged the BiInv.v part, can you rebase on master and force push, so there is just one commit without that material?

jdchristensen · 2026-04-29T16:55:32Z

You rebased on the previous version of master, I think. You probably need to pull in the latest master.

maxipetro · 2026-04-29T19:35:58Z

You rebased on the previous version of master, I think. You probably need to pull in the latest master.

I rebased on the updated master, the problem was the commit that I made in the other PR before it got merged. The changes of that commit were not made in this branch and so the rebasing caused a conflict. My merge editor then messed things up when I had to manually resolve the conflict. It should be fine now

jdchristensen · 2026-04-30T15:20:42Z

For the record, the previous PR is #32 .

jdchristensen · 2026-04-30T15:24:48Z

I've copied over the tasks list and updated it:

Decide on directions of pf, pf1, pf2.
There are still many style issues to be fixed, e.g. indentation, spacing, line breaks, etc.
Proof read all comments in the code and think about naming conventions for definitions/theorems. When it makes sense to do so, results should be named like those in Int.v, so this material can replace Int.v with users not needing to change much. Note that we usually use only lower case in identifiers.
Can any of the proofs be simplified, e.g. by using the uniqueness principle more? Or the new IntHIT_ind_equiv?
What is missing from Int.v that we still need to add to HITInt.v? E.g. a coercion from nat is one thing, but I suspect there is more.
Can SInt.v (formerly IntShort.v) be simplified further? If it becomes simple enough, we could inline it into HITInt.v.
Remove Int.v and rename HITInt.v to Int.v. Rename everything inside HITInt.v to the old names, so that the rest of the library can use the new approach with minimal changes. Even better, maybe some other parts of the library will simplify slightly.

Edit: minor updates 2026/6/17.

… BiInv.v, needs still clean-up

jdchristensen · 2026-05-13T18:40:01Z

I made a few cleanups. I think similar proof simplifications could be made in other places, so look around for similar things.

Co-authored-by: Dan Christensen <jdc@uwo.ca>

Add semi-additive categories infrastructure

jdchristensen · 2026-06-15T14:22:22Z

@maxipetro Just checking on the status of this.

- Remove the unused imports Categories.Additive.Biproducts and Classes.theory.groups. Nothing in the file refers to either: the monoid-morphism helpers (IsMonoidPreserving, id_monoid_morphism, compose_monoid_morphism, preserves_sg_op, ...) all come from abstract_algebra, which is already imported, and biproducts are reached transitively through SemiAdditive. - Rename inverse_morphism_unique to hom_moveL_1V, paralleling the group movement lemma grp_moveL_1V, and update its two uses. - Name the AdditiveFunctor fields consistently: the coercion is addfunctor and the monoid-preservation instance is ismonoidpreserving_addfunctor. - Remove the AdditiveFunctorLaws section; its three lemmas were direct applications of preserves_sg_op, preserves_mon_unit and preserves_inverse, which apply to an additive functor's action without a wrapper.

Add additive categories infrastructure

maxipetro · 2026-06-16T08:57:24Z

@jdchristensen I think now all the open issues are resolved. Regarding the bullet points in your list:

The directions of pf, pf1 and pf2 are changed so I think we can tick this off.

Some comments exceed the 80 character limit per line. Should I break them into two lines?

I think we should rename uniquenessZ* to something that fits the naming conventions of the library, maybe "IntHIT_uniqueness" which will be then renamed later to "Int_uniqueness"? The same for IntITtoIntHIT and similar lemmas.

I can start replacing the old Int with the new HITInt and rename the latter. If further simplifications or style fixes are found in the future they should not affect this.

…ples

jdchristensen · 2026-06-17T18:26:40Z

The directions of pf, pf1 and pf2 are changed so I think we can tick this off.

Sounds good.

Some comments exceed the 80 character limit per line. Should I break them into two lines?

No, the style for comments is to have no line breaks at all.

I think we should rename uniquenessZ* to something that fits the naming conventions of the library, maybe "IntHIT_uniqueness" which will be then renamed later to "Int_uniqueness"? The same for IntITtoIntHIT and similar lemmas.

I reworked this material (I'll push in a minute) but didn't adjust naming. I'm not exactly sure what is best. Maybe IntHIT_homotopic for now? Later, int_homotopic. (We don't capitalize the names of types in most identifiers, except for the type name itself.)

I can start replacing the old Int with the new HITInt and rename the latter. If further simplifications or style fixes are found in the future they should not affect this.

Let's wait on this, as there are too many issues right now. I'll provide feedback in a minute.

jdchristensen · 2026-06-17T18:41:07Z

I just pushed eight commits. Please read them separately, as I was careful to only put related changes together, and some of the changes overlap so won't be understandable if you just look at the overall diff. Here's a summary from oldest to newest:

BiInv, HITInt: fix spacing, indentation; remove unneeded parentheses

I only looked at a small portion of the file, but found tons of style errors. Please go through the file carefully checking the spacing, indentation, parenthesization, etc.

HITInt: use == notation, slightly simplify proof, fix comments

The == notation is good to use when it makes sense. The simplifications to the proof are also worth noting, although this proof disappears in a later commit.

BiInv: clean-ups to EquivalenceCompatibility

Various style things. In particular, notice that every definition in this section had a common argument pe, so it's natural to make this a Section variable.

HITInt: clarify/correct comments

I removed an incorrect comment that said: "Since it is an Instance that biinvertible maps are equivalent to half-adjoint equivalences using type class search one could also use IntHIT_rec_biinv instead." Only one direction is an instance, and it's not the one that would allow us to use IntHIT_rec_biinv instead. But this raises the question of why we need the other one. I'll make a comment in the appropriate spot.

HITInt: clarify two proofs

Minor.

BiInv: move prod_isbiinv and issig_biinv earlier in file

They were separating related functions, so I moved them out of the way.

BiInv: adjust retr_is_sect_isbiinv so that adjoint law holds, and dually

This is an important change. As originally defined, retr_is_sect_isbiinv and sect_is_retr_isbiinv probably don't satisfy the adjoint laws. So I inlined their proofs into the proofs of isequiv_isbiinv and isequiv_isbiinv'. Since those use adjointification, the resulting proofs that these composites are the identities will then satisfy the adjoint law.

HITInv: prove IntHIT_ind_equiv, greatly simplifying uniqueness principles

Using the adjoint law, I was able to prove a simple induction principle IntHIT_ind_equiv. This makes the proofs of the uniqueness principles very short. I suspect it can also be used in other places, but I didn't look around. Can you see if there is anywhere else that can benefit?

jdchristensen · 2026-06-17T18:45:47Z

  Let es' := eisretr_biinv e' : e' o s' == idmap.

-  Definition helper_r (pe : e' o f == g o e) : r' o g o e == f o r o e.
+  Definition helper_r : r' o g o e == f o r o e.


Are these helpers needed? Since they are one-liners and are used just once, couldn't they be inlined to where they are needed? If they are kept, they should be renamed to something less generic, or made Local.

jdchristensen · 2026-06-17T18:46:23Z

-  Definition helper_r (pe : e' o f == g o e) : r' o g o e == f o r o e.
+  Definition helper_r : r' o g o e == f o r o e.
  Proof.
    intro x.


Please use a or b, to help the reader know the type of this variable. (Not just here, everywhere that you use intro.)

jdchristensen · 2026-06-17T18:48:43Z

+Definition IntHIT_ind_hprop {P : IntHIT -> Type} `{forall x, IsHProp (P x)}
+  (t0 : P zero_i)
+  (f : forall z : IntHIT, P z -> P (succ z))
+  (g : forall z : IntHIT, P z -> P (pred z))
+  : forall x, P x.


Inconsistent variable names: x in two places and z in two places. I think using z as a variable of type IntHIT is good. Again, not just here, but everywhere.

jdchristensen · 2026-06-17T18:50:10Z

+Definition IntHIT_rec {P : Type} (t0 : P)
+  (f : P -> P) (g1 : P -> P) (g2 : P -> P)
+  (s : forall (t : P), g1 (f t) = t)
+  (r : forall (t : P), f (g2 t) = t)
+  : IntHIT -> P.


This and the corresponding beta laws should go in a Section, since they use the same variables.

jdchristensen · 2026-06-17T18:51:46Z

+Definition uniquenessZ_two_fun_equiv
+  {P : Type}
+  (f : P -> P)
+  {e' : IsEquiv f}
+  (k1 : IntHIT -> P)
+  (k2 : IntHIT -> P)
+  (p0 : k1 zero_i = k2 zero_i)
+  (pf1 : forall (z : IntHIT), (k1 o succ) z = (f o k1) z)
+  (pf2 : forall (z : IntHIT), (k2 o succ) z = (f o k2) z)


Let's make argument lists more compact, like I did for the two results before this one. (Again, not just here, but in general.)

maxipetro force-pushed the integers_hit_fresh branch from 06cf313 to f7607e4 Compare April 29, 2026 14:40

Added HITInt.v SInt.v, updated BiInv.v and related files, fresh start

5f0e4e3

maxipetro force-pushed the integers_hit_fresh branch from f7607e4 to 5f0e4e3 Compare April 29, 2026 19:33

Fixed typos and style issues

e2e3d55

maxipetro commented Apr 30, 2026

View reviewed changes

Comment thread theories/Spaces/HITInt.v Outdated

Tested change of direction of [pf] in uniquenessZ

c60ce19

jdchristensen reviewed Apr 30, 2026

View reviewed changes

Comment thread theories/Spaces/HITInt.v

maxipetro added 2 commits May 4, 2026 16:00

Changed order of [pf] in HITInt.v and statements of related lemmas in…

536c90d

… BiInv.v, needs still clean-up

reversed order in [IntITtoIntHIT_comp_*]

05c3521

jdchristensen reviewed May 13, 2026

View reviewed changes

Comment thread theories/Equiv/BiInv.v Outdated

jdchristensen added 2 commits May 13, 2026 14:37

BiInv, HITInv: fix whitespace, etc.

74177e9

BiInv, HITInt: simplify some proofs

9cf9b1a

maxipetro added 2 commits May 15, 2026 17:05

Fixed some style issues

fa6dc73

Simplified some proofs

70ddc67

maxipetro commented May 15, 2026

View reviewed changes

Comment thread theories/Spaces/HITInt.v Outdated

jdchristensen reviewed May 15, 2026

View reviewed changes

Comment thread theories/Spaces/HITInt.v Outdated

CharlesCNorton and others added 3 commits June 10, 2026 17:19

Add semi-additive categories infrastructure

c88dfc2

Co-authored-by: Dan Christensen <jdc@uwo.ca>

Merge pull request HoTT#2305 from CharlesCNorton/patch-8

c0ba3f5

Add semi-additive categories infrastructure

Rework additive categories as semi-additive plus inverses

0d6edfa

jdchristensen and others added 4 commits June 15, 2026 11:19

Additive: simplify several proofs

9ee5547

Merge pull request HoTT#2304 from CharlesCNorton/patch-7

40659d8

Add additive categories infrastructure

Merge branch 'HoTT:master' into integers_hit_fresh

ab65d13

removed [IntHIT_rec_qinv]

9007754

jdchristensen added 8 commits June 17, 2026 13:31

BiInv, HITInt: fix spacing, indentation; remove unneeded parentheses

ca075c9

HITInt: use == notation, slightly simplify proof, fix comments

76e8357

BiInv: clean-ups to EquivalenceCompatibility

411458e

HITInt: clarify/correct comments

2e9701e

HITInt: clarify two proofs

bd05ea9

BiInv: move prod_isbiinv and issig_biinv earlier in file

6ab4cc7

BiInv: adjust retr_is_sect_isbiinv so that adjoint law holds, and dually

83ca51b

HITInv: prove IntHIT_ind_equiv, greatly simplifying uniqueness princi…

aac05c5

…ples

jdchristensen reviewed Jun 17, 2026

View reviewed changes

Conversation

maxipetro commented Apr 29, 2026

Uh oh!

jdchristensen commented Apr 29, 2026

Uh oh!

jdchristensen commented Apr 29, 2026

Uh oh!

maxipetro commented Apr 29, 2026

Uh oh!

Uh oh!

jdchristensen commented Apr 30, 2026

Uh oh!

jdchristensen commented Apr 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jdchristensen commented May 13, 2026

Uh oh!

Uh oh!

Uh oh!

jdchristensen commented Jun 15, 2026

Uh oh!

maxipetro commented Jun 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jdchristensen commented Jun 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jdchristensen commented Jun 17, 2026

Uh oh!

jdchristensen Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

jdchristensen Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

jdchristensen Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

jdchristensen Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

jdchristensen Jun 17, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

jdchristensen commented Apr 30, 2026 •

edited

Loading

maxipetro commented Jun 16, 2026 •

edited

Loading

jdchristensen commented Jun 17, 2026 •

edited

Loading