Skip to content

Add Rezk Completion by HIT #1188

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 9 commits into from
Jun 25, 2025
Merged

Add Rezk Completion by HIT #1188

merged 9 commits into from
Jun 25, 2025

Conversation

anshwad10
Copy link
Contributor

No description provided.

@anshwad10
Copy link
Contributor Author

Just noticed that the HIT can be replaced with a GroupoidQuotient. This would have saved me from writing so many elimination principles if I had found it earlier

@felixwellen
Copy link
Collaborator

Nice!

@felixwellen felixwellen merged commit ac62dd4 into agda:master Jun 25, 2025
1 check passed
@anshwad10 anshwad10 deleted the patch-3 branch June 25, 2025 11:50
marcinjangrzybowski added a commit to marcinjangrzybowski/cubical that referenced this pull request Jun 26, 2025
@marcinjangrzybowski
Squashed commit of the following:
18f8334 
commit d08dabfacb486fb77a2ded077a3f0593968412e8
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Thu Jun 26 22:32:26 2025 +0200

    works

commit 74b6ee0df2aaba26be3f09f81b2020470b27cc44
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Thu Jun 26 22:29:59 2025 +0200

    gi

commit f89d4d7f172ae7da24a385efdd783209a5b2bdea
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Thu Jun 26 22:29:15 2025 +0200

    gi

commit 3528c1128f48573748c240b3b5d3ea27fee5e0e5
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Thu Jun 26 20:04:00 2025 +0200

    cleanup

commit 4028c0010c1f0f48f54577ce418185648b2b9902
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Thu Jun 26 20:02:46 2025 +0200

    cleanup

commit 02f1aa892a739e61be52f2a609d0bd5891133639
Merge: 07914eea ac62dd4
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Thu Jun 26 19:09:38 2025 +0200

    pre-merge

commit 07914eeae43b77109983039e6d2e6c67fbae3f2f
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Thu Jun 26 18:59:53 2025 +0200

    integration done

commit ac62dd4
Author: anshwad10 <[email protected]>
Date:   Wed Jun 25 17:16:13 2025 +0530

    Add Rezk Completion by HIT (agda#1188)

    * Add Rezk Completion by HIT

    * Update Construction.agda

    * Removed trailing whitespaces

    * Remove trailing whitespace

    * Replace HIT with GroupoidQuotient

    * shorter proof of `inc-surj`

    * fix whitespace

    * Forgot to import GroupoidQuotients

    * add implicit argument

commit b15ec4e
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Tue Jun 24 06:45:56 2025 +0200

    wip

commit 55479ef
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Wed May 28 16:00:42 2025 +0200

    wip - dirty

commit ecf1bbb
Author: Laine Taffin Altman <[email protected]>
Date:   Fri May 23 03:17:16 2025 -0700

    Fix makefile race condition (agda#1210)

    If you use `make -j gen-everythings listings`, currently there is a near-certainty that the `listings` task will fail because the Everythings modules haven't been generated yet.  This PR enforces the dependency.

commit 43183c8
Author: michael <[email protected]>
Date:   Thu May 22 17:01:37 2025 -0500

    Five lemma (agda#1166)

    * exact sequences

    * complete five proof

    * make five safe

    * fix newline

    * exactness over a successor structure

    * working again

    * fix whitespace...

    * clean up, just five

    * clean up

    * make implicit + rename isExact so the names are more descriptive

    * fix whitespace

commit 63d187d
Author: anshwad10 <[email protected]>
Date:   Tue May 20 22:52:24 2025 +0530

    Formalize Theorem 7.2.2 in the HoTT Book (agda#1180)

    * Formalize Theorem 7.2.2 in the HoTT Book

    * move Theorem 7.2.2 to Cubical.Relation.Binary.Properties

    * Remove a few extra spaces

    This is not really necessary but it looks better

commit 06e62f4
Author: michael <[email protected]>
Date:   Tue May 20 07:24:54 2025 -0500

    Composition of left module homomorphisms (agda#1176)

    * implement composition of left module homomorphisms

    * pull out to top level

    * fix whitespace

commit 78203ee
Author: anshwad10 <[email protected]>
Date:   Mon May 19 21:41:29 2025 +0530

    Remove duplicated lemma (agda#1189)

    * Remove duplicated lemma

    agda#1017

    * Insert brackets

commit 2738401
Author: LorenzoMolena <[email protected]>
Date:   Mon May 19 17:52:30 2025 +0200

    Strict order equational reasoning (agda#1203)

    * Add QuosetReasoning.agda

    Co-authored-by: Ettore Forigo <[email protected]>

    * add missing `no-eta-equality` in SubRelation, make SubRelation instance private

    ---------

    Co-authored-by: Ettore Forigo <[email protected]>

commit 69b70a2
Author: anshwad10 <[email protected]>
Date:   Mon May 19 21:19:57 2025 +0530

    Add inducedFun for EM1 (agda#1208)

    * Add files via upload

    * Delete Base.agda

    No idea what this file is doing here

    * Delete Properties.agda

    Must have accidentally put this here when I was editing dagger-cat

    * Add inducedFun for EM1

commit 22458b7
Author: LeeeeT <[email protected]>
Date:   Mon May 19 18:46:33 2025 +0300

    Add missing minus symbol (agda#1207)

commit 3291fc1
Author: Felix Cherubini <[email protected]>
Date:   Mon May 19 17:24:35 2025 +0200

    Release for agda 2.7 (agda#1206)

    * test new ci script

    * fix

    * use fix-whitespace action

    * blindly try stuff

    * blindly try stuff

    * blindly try stuff

    * untabify...

    * Revert "blindly try stuff"

    This reverts commit 6fe71f3.

    # Conflicts:
    #	.github/workflows/ci-ubuntu.yml

    * use fix-whitespace action

    * whitespace

    * whitespace

    * fix

    * fix

    * fix

    * fix

    * Fix path of fix-whitespace

    * Remove unnecessary step to generate user-manual.pdf

    * Bump base in cubical-utils.cabal

    * bump version number everywhere, update README and RELEASE

    * trailing newline needed?

    * update flake

    ---------

    Co-authored-by: Andreas Abel <[email protected]>
    Co-authored-by: Naïm Favier <[email protected]>

commit eef2ed6
Author: Marcin Jan Turek-Grzybowski <[email protected]>
Date:   Thu May 15 07:17:58 2025 +0200

    wip

commit 71f32f0
Author: Andreas Abel <[email protected]>
Date:   Fri May 9 21:51:25 2025 +0200

    Prep for Agda 2.8.0: remove some spurious `private`

commit d5b7bce
Author: Marcin Grzybowski <[email protected]>
Date:   Mon Apr 21 20:46:48 2025 +0200

    sync

commit 35d2919
Merge: 385066b cb0510c
Author: Evan Cavallo <[email protected]>
Date:   Fri Mar 21 06:08:36 2025 +0100

    Merge pull request agda#1157 from Trebor-Huang/devalapurkar-haine

    Devalapurkar & Haine

commit cb0510c
Author: ecavallo <[email protected]>
Date:   Thu Mar 20 18:40:56 2025 +0100

    cosmetic changes

commit 52cf2a1
Author: ecavallo <[email protected]>
Date:   Thu Mar 20 18:40:42 2025 +0100

    more informative type signatures

commit 01c36f4
Author: ecavallo <[email protected]>
Date:   Thu Mar 20 18:40:23 2025 +0100

    prefer copattern matching to record syntax

commit fa0eba6
Author: ecavallo <[email protected]>
Date:   Thu Mar 20 13:59:26 2025 +0100

    make pushout to wedge equivalence opaque

commit 4155afd
Merge: 01fa420 385066b
Author: ecavallo <[email protected]>
Date:   Tue Mar 18 14:01:34 2025 +0100

    Merge branch 'master' into devalapurkar-haine

commit 385066b
Author: Loïc Pujet <[email protected]>
Date:   Tue Mar 4 16:53:03 2025 +0100

    Reduced homology of CW complexes (agda#1175)

    * Reduced homology of CW complexes

    * explicit description of the augmentation map

commit 90c3244
Author: Marcin Grzybowski <[email protected]>
Date:   Fri Feb 14 16:53:06 2025 +0100

    wip

commit e8ff0c1
Author: anshwad10 <[email protected]>
Date:   Fri Feb 14 21:06:39 2025 +0530

    Move `factorial` from `Cubical.Data.Fin.LehmerCode` to `Cubical.Data.Nat.Properties` (agda#1184)

    * Update LehmerCode.agda

    * Update Properties.agda

    add `factorial` here

    * Update LehmerCode.agda

    made it export `factorial` so nothing else in the library that depends on `factorial` being exported breaks

    * Removed dependency on LehmerCode exporting `factorial`

    * Removed dependency on LehmerCode exporting `factorial`

    * Removed dependency on LehmerCode exporting `factorial`

    * Remove the public export of `factorial` from LehmerCode.agda

commit 3d5bb7d
Author: Brad Dragun <[email protected]>
Date:   Tue Feb 11 23:02:11 2025 -0700

    Fix missed rename of StrictPoset to Quoset (agda#1185)

commit c16edad
Author: anshwad10 <[email protected]>
Date:   Sat Feb 8 21:32:52 2025 +0530

    Remove duplicated factorial function (agda#1183)

    `_!` is defined in `Cubical.Data.Nat.Properties`, `factorial` is defined in `Cubical.Data.Fin.LehmerCode`, and they both have identical definitions.

commit f717d46
Author: Brad Dragun <[email protected]>
Date:   Fri Feb 7 09:27:29 2025 -0700

    Basic Order Theory (agda#1154)

    * Add inverses to monoids/comm monoids

    * Add meets and joins to order properties

    * Rewrite isConnected and rename isStronglyConnected

    * Decidable total and linear orders imply discrete

    * Remove discrete requirement

    * Move decidable->discrete from toset to poset

    * Define binary meets/joins and prove properties

    * The negation of a linear order is a poset

    * Define bounds on a poset

    * Mild refactoring

    Rename preorder to proset; rename strict poset
    to quoset (quasiorder) and add strict orders
    as quasiorders with weak linearity

    * Remove unnecessary constructors

    * Define tight relations

    * Reintroduce constructors

    * Lattice basics

    * Distributive lattices

    * Replace compEquiv usages

    * Total orders are distributive pseudolattices

    * Add pseudolattice assumption to make more useful

    * Mappings on posets

    * Downsets and upsets are preserved

    * Defined complete lattices

    * Duals and closures

    * Embeddings form a complete lattice

    * Dual closures

    * Bicomplete subsets

    * Poset equivalences

    * Galois connections

    * Fix typo

    * Fix whitespace

    * Fix build failures

    * Move PosetDownset to where principalDownsets are

    * Fix build failures

    * Split mappings and subsets

    * Fix whitespace

    * Proofs regarding residuals and involutions

    * Cleaner proof

commit f344485
Author: Marcin Grzybowski <[email protected]>
Date:   Thu Jan 30 15:55:08 2025 +0100

    wip

commit 01fa420
Author: Trebor-Huang <[email protected]>
Date:   Thu Sep 19 22:16:54 2024 +0800

    safe flags

commit 54a2b1f
Author: Trebor-Huang <[email protected]>
Date:   Thu Sep 19 21:42:05 2024 +0800

    Fix whitespace

commit a181af8
Merge: f0d49bc 53e400e
Author: Trebor-Huang <[email protected]>
Date:   Thu Sep 19 21:36:50 2024 +0800

    Merge remote-tracking branch 'origin/master' into devalapurkar-haine

commit f0d49bc
Author: Trebor-Huang <[email protected]>
Date:   Thu Sep 19 21:27:40 2024 +0800

    James

commit d99570a
Author: Trebor-Huang <[email protected]>
Date:   Thu Sep 19 21:10:57 2024 +0800

    Hilton–Milnor

commit c983de7
Author: Trebor-Huang <[email protected]>
Date:   Thu Sep 19 20:36:36 2024 +0800

    Splitting of loopspace

commit 08a56c4
Author: Trebor-Huang <[email protected]>
Date:   Thu Sep 19 20:21:45 2024 +0800

    Oddly specific sigma lemma

commit 51fa7d0
Author: Trebor-Huang <[email protected]>
Date:   Thu Sep 19 20:12:35 2024 +0800

    Remove my version in favor of the other

commit dee0c56
Author: Trebor-Huang <[email protected]>
Date:   Sun Aug 18 00:08:50 2024 +0800

    extend commutative squares

commit 98bbb7a
Author: Trebor-Huang <[email protected]>
Date:   Sun Aug 18 00:08:43 2024 +0800

    tweak

commit a4b23dd
Author: Trebor-Huang <[email protected]>
Date:   Thu Aug 15 17:45:42 2024 +0800

    Rename

commit dac0c0e
Author: Trebor-Huang <[email protected]>
Date:   Tue Aug 13 02:07:32 2024 +0800

    Pushout using Unit*

commit f9fc7e3
Author: Trebor-Huang <[email protected]>
Date:   Mon Aug 12 13:50:15 2024 +0800

    Use PushoutSquare instead

commit 72a7557
Author: Trebor-Huang <[email protected]>
Date:   Mon Aug 12 03:58:36 2024 +0800

    Universes

commit 9d50340
Author: Trebor-Huang <[email protected]>
Date:   Mon Aug 12 03:18:06 2024 +0800

    Susp (X∙ ⋀ Y∙) ≡ join X Y

commit 4bc6517
Author: Trebor-Huang <[email protected]>
Date:   Mon Aug 12 02:51:38 2024 +0800

    Pushout⋁≃Unit

commit 90f1ca9
Author: Trebor-Huang <[email protected]>
Date:   Mon Aug 12 02:50:52 2024 +0800

    Remove redundant definition

commit fa2da1a
Author: Trebor-Huang <[email protected]>
Date:   Mon Aug 12 02:50:36 2024 +0800

    projection functions

commit 54038ae
Author: Trebor-Huang <[email protected]>
Date:   Mon Aug 12 02:31:37 2024 +0800

    join inclusions are null

commit 313b74e
Author: Trebor-Huang <[email protected]>
Date:   Mon Aug 12 00:22:40 2024 +0800

    Use pushout squares for cofibInl-⋁

commit d0a06cd
Author: Trebor-Huang <[email protected]>
Date:   Sun Aug 11 21:40:16 2024 +0800

    pushout along identity

commit b4e74c1
Author: Trebor-Huang <[email protected]>
Date:   Sun Aug 11 21:08:23 2024 +0800

    Susp is Pushout 1 <- X -> 1

commit 5dae632
Author: aljungstrom <[email protected]>
Date:   Tue Sep 17 01:01:18 2024 +0200

    fixes

commit e13f9ab
Merge: 10aea90 e2370fb
Author: aljungstrom <[email protected]>
Date:   Mon Sep 16 22:22:28 2024 +0200

    Merge remote-tracking branch 'master/master' into cellular_pointed

commit 10aea90
Author: aljungstrom <[email protected]>
Date:   Tue Jun 4 14:42:34 2024 +0200

    minor

commit 1dff2d5
Merge: 46482af a0b4ba3
Author: aljungstrom <[email protected]>
Date:   Tue Jun 4 14:39:52 2024 +0200

    merge

commit 46482af
Author: aljungstrom <[email protected]>
Date:   Tue Jun 4 14:22:49 2024 +0200

    connected clean

commit 787f34f
Author: aljungstrom <[email protected]>
Date:   Tue Jun 4 14:12:57 2024 +0200

    connected done?

commit 73afa8e
Author: aljungstrom <[email protected]>
Date:   Tue Jun 4 02:59:48 2024 +0200

    cleaning

commit 0cb5678
Author: aljungstrom <[email protected]>
Date:   Tue Jun 4 02:59:42 2024 +0200

    cleaning

commit 6bc3664
Author: aljungstrom <[email protected]>
Date:   Fri May 31 18:51:51 2024 +0200

    pretty much done

commit e4f4003
Author: aljungstrom <[email protected]>
Date:   Fri May 31 04:09:48 2024 +0200

    almost

commit c7acbee
Author: aljungstrom <[email protected]>
Date:   Wed May 29 18:11:46 2024 +0200

    stuff

commit 77623bb
Author: aljungstrom <[email protected]>
Date:   Mon May 27 03:16:45 2024 +0200

    wip...

commit dac2fd3
Author: aljungstrom <[email protected]>
Date:   Thu May 23 18:08:06 2024 +0200

    stuff

commit afe51a4
Author: aljungstrom <[email protected]>
Date:   Wed May 8 18:20:52 2024 +0200

    p2

commit 87fa4c0
Author: aljungstrom <[email protected]>
Date:   Tue May 7 18:15:55 2024 +0200

    done?

commit eb6b12e
Author: aljungstrom <[email protected]>
Date:   Tue May 7 10:12:34 2024 +0200

    Pointed

commit 3784dcd
Author: aljungstrom <[email protected]>
Date:   Thu May 2 11:34:11 2024 +0200

    comments

commit beccacd
Author: aljungstrom <[email protected]>
Date:   Mon Mar 4 12:03:53 2024 +0100

    ojdå

commit 3e53282
Author: aljungstrom <[email protected]>
Date:   Mon Mar 4 11:31:38 2024 +0100

    broken code

commit ac5249e
Author: aljungstrom <[email protected]>
Date:   Mon Mar 4 09:39:57 2024 +0100

    wups

commit 1b005a6
Author: aljungstrom <[email protected]>
Date:   Mon Mar 4 02:22:00 2024 +0100

    ugh

commit 2d3fe1c
Author: aljungstrom <[email protected]>
Date:   Mon Mar 4 01:48:45 2024 +0100

    wups

commit b1f9e1d
Author: aljungstrom <[email protected]>
Date:   Mon Mar 4 01:30:09 2024 +0100

    readme

commit 6e259af
Author: aljungstrom <[email protected]>
Date:   Mon Mar 4 00:38:02 2024 +0100

    cleanup

commit a3f6a9e
Merge: 6ce70a4 f4745a2 4ba3c8e
Author: aljungstrom <[email protected]>
Date:   Sun Mar 3 21:13:21 2024 +0100

    merge

commit 4ba3c8e
Author: aljungstrom <[email protected]>
Date:   Sun Mar 3 20:55:52 2024 +0100

    stuff

commit a3bb47e
Author: aljungstrom <[email protected]>
Date:   Sun Mar 3 20:48:17 2024 +0100

    done?

commit 53bb0f2
Author: aljungstrom <[email protected]>
Date:   Sun Mar 3 03:52:29 2024 +0100

    stuff

commit 54c7919
Author: aljungstrom <[email protected]>
Date:   Fri Mar 1 19:08:20 2024 +0100

    stuff

commit 42d6b77
Author: aljungstrom <[email protected]>
Date:   Thu Feb 29 15:34:05 2024 +0100

    stuff

commit df55d55
Author: aljungstrom <[email protected]>
Date:   Thu Feb 29 02:49:34 2024 +0100

    More

commit ae6e813
Author: aljungstrom <[email protected]>
Date:   Tue Feb 27 00:10:56 2024 +0100

    stuf

commit b694120
Author: aljungstrom <[email protected]>
Date:   Mon Feb 26 16:42:26 2024 +0100

    stuff

commit ea5fefd
Author: aljungstrom <[email protected]>
Date:   Sun Feb 25 23:02:26 2024 +0100

    stuff

commit f4745a2
Merge: 1c0396c 227b10b
Author: aljungstrom <[email protected]>
Date:   Wed Jan 31 10:49:17 2024 +0100

    Merge remote-tracking branch 'origin/master'

commit 9071481
Author: aljungstrom <[email protected]>
Date:   Wed Jan 31 10:46:56 2024 +0100

    stuff

commit e47bad5
Author: aljungstrom <[email protected]>
Date:   Wed Jan 24 19:53:25 2024 +0100

    wups

commit f7524eb
Author: aljungstrom <[email protected]>
Date:   Tue Jan 23 19:44:57 2024 +0100

    ugh...

commit b7716a4
Author: aljungstrom <[email protected]>
Date:   Tue Jan 23 19:19:56 2024 +0100

    fixes

commit 7313a31
Author: aljungstrom <[email protected]>
Date:   Tue Jan 23 15:04:18 2024 +0100

    wups

commit 7875e3e
Author: aljungstrom <[email protected]>
Date:   Tue Jan 23 14:51:05 2024 +0100

    wups

commit 74a8521
Author: aljungstrom <[email protected]>
Date:   Tue Jan 23 14:47:14 2024 +0100

    wups

commit 5e8b305
Author: aljungstrom <[email protected]>
Date:   Tue Jan 23 14:17:35 2024 +0100

    done?

commit 74596b5
Author: aljungstrom <[email protected]>
Date:   Tue Jan 23 03:52:06 2024 +0100

    ..

commit 2b8b5fd
Author: aljungstrom <[email protected]>
Date:   Mon Jan 22 18:50:46 2024 +0100

    more

commit 2fef4ef
Author: aljungstrom <[email protected]>
Date:   Mon Jan 22 18:36:10 2024 +0100

    stuff

commit c034578
Author: aljungstrom <[email protected]>
Date:   Thu Jan 18 17:17:24 2024 +0100

    stuff

commit 9d1915d
Author: aljungstrom <[email protected]>
Date:   Wed Jan 17 02:53:26 2024 +0100

    fix

commit 227b10b
Author: aljungstrom <[email protected]>
Date:   Thu Jun 8 09:45:56 2023 +0200

    w

commit 3acc6b8
Author: aljungstrom <[email protected]>
Date:   Thu Jun 8 09:45:28 2023 +0200

    w

commit ea75092
Author: aljungstrom <[email protected]>
Date:   Thu Jun 8 09:44:37 2023 +0200

    w

commit 52429ff
Merge: 9341710 814d54b
Author: aljungstrom <[email protected]>
Date:   Thu Jun 8 09:38:02 2023 +0200

    Merge branch 'newM'

commit 9341710
Author: aljungstrom <[email protected]>
Date:   Fri Jun 2 15:04:54 2023 +0200

    ganea stuff

commit 17f3fc1
Author: aljungstrom <[email protected]>
Date:   Mon Apr 24 17:13:52 2023 +0200

    rme

commit aadde33
Author: aljungstrom <[email protected]>
Date:   Mon Apr 24 17:12:41 2023 +0200

    wups

commit e8244ac
Author: aljungstrom <[email protected]>
Date:   Mon Apr 24 17:10:45 2023 +0200

    duplicate

commit cc6ced2
Merge: b4b6efb f0ad815
Author: aljungstrom <[email protected]>
Date:   Mon Apr 24 17:10:10 2023 +0200

    done

commit b4b6efb
Merge: 93d7248 9acdecf
Author: aljungstrom <[email protected]>
Date:   Tue Feb 1 04:02:50 2022 +0100

    m

commit 93d7248
Author: aljungstrom <[email protected]>
Date:   Tue Feb 1 04:00:15 2022 +0100

    t
@maxsnew maxsnew mentioned this pull request Jul 29, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@anshwad10 @felixwellen