Skip to content
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.

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

Sites, sheaves and sheafification as a QIT #1031

Merged
merged 59 commits into from
Nov 21, 2023
Merged
Changes from 1 commit
Commits
Show all changes
59 commits
Select commit Hold shift + click to select a range
aa333d9
stubs for Coverage, Cover, Sieve
MatthiasHu Apr 19, 2023
14c9cb3
covers as families, sieves
MatthiasHu Apr 19, 2023
c37ac8a
pulledBackSieve
MatthiasHu Apr 20, 2023
ba9f430
finish Coverage
MatthiasHu Apr 20, 2023
44dad75
slightly simplify generatedSieve
MatthiasHu May 19, 2023
32c144a
universal property of generatedSieve
MatthiasHu May 19, 2023
960feee
make C implicit in sieve operations
MatthiasHu May 20, 2023
0c2770f
make C implicit in patchArr and patchObj
MatthiasHu May 20, 2023
fe4438e
definition of sheaves on a site
MatthiasHu May 20, 2023
e0f1ad8
tiny improvement (qualified import)
MatthiasHu May 28, 2023
9b86341
Merge branch 'master' into attempt-at-sheafification
MatthiasHu Jul 27, 2023
76dfda4
remove unnecessary parenthesis
MatthiasHu Jul 28, 2023
bdff467
indentation in equational reasoning
MatthiasHu Jul 28, 2023
49d1d06
sheafification QIT
MatthiasHu Jul 31, 2023
d31a55f
correct silly mistake
MatthiasHu Aug 1, 2023
e9008c3
rename CompatibleFamilies -> CompatibleFamily
MatthiasHu Aug 1, 2023
343170f
sheafification is a sheaf
MatthiasHu Aug 1, 2023
2d7666f
rename
MatthiasHu Aug 1, 2023
1811b11
stub of the universal property
MatthiasHu Aug 2, 2023
fbd1c26
small renaming
MatthiasHu Aug 2, 2023
363f17a
(wip)
MatthiasHu Aug 2, 2023
2b84caa
(wip) (termination checker problems)
MatthiasHu Aug 3, 2023
eb4937f
(wip) solved termination issue
MatthiasHu Aug 3, 2023
dc55c39
finish inducedMap of sheafification
MatthiasHu Aug 8, 2023
9e0e274
comment with reference
MatthiasHu Aug 8, 2023
12017ec
rename i -> patch
MatthiasHu Aug 9, 2023
4ab79ee
diagram comment and a bit of preparation
MatthiasHu Aug 9, 2023
9f5bbbc
elimProp with restrictPreservesB
MatthiasHu Aug 9, 2023
1bb1887
introduce isSeparated
MatthiasHu Aug 10, 2023
cd7469d
uniqueness part of universal property
MatthiasHu Aug 11, 2023
4ab1418
package up as universal element
MatthiasHu Aug 11, 2023
1694fdb
name constructor arguments
MatthiasHu Aug 15, 2023
fa75467
elimProp without restrictPreservesB assumption
MatthiasHu Aug 16, 2023
0cbcbda
prepare for merging module
MatthiasHu Aug 16, 2023
d55d39a
merge module
MatthiasHu Aug 16, 2023
70a8dc8
properly name elimProp assumptions
MatthiasHu Aug 16, 2023
1be4618
fix misnomer (now we have (η ⟦ _ ⟧) x = η⟦⟧ x)
MatthiasHu Aug 16, 2023
87bf43a
structure elimPropInduction more nicely
MatthiasHu Aug 16, 2023
26a8551
fix indentation
MatthiasHu Aug 16, 2023
48cb7a1
use improved elimProp in uniqueness
MatthiasHu Aug 21, 2023
7ece10f
split sheafification in several files
MatthiasHu Aug 21, 2023
833859b
clean up imports
MatthiasHu Aug 21, 2023
3e76720
eliminate Families by inlining
MatthiasHu Aug 21, 2023
e74cede
comments in ElimProp
MatthiasHu Aug 22, 2023
9e6634a
references for coverage
MatthiasHu Aug 22, 2023
b8d2c8d
make two arguments implicit
MatthiasHu Aug 22, 2023
af0e3d7
a few more comments
MatthiasHu Aug 22, 2023
d53c9fb
Merge branch 'master' into sheafification-QIT
MatthiasHu Aug 22, 2023
258e8b1
fix unresolved meta (with Agda 2.6.3)
MatthiasHu Aug 22, 2023
8f0c3e1
Merge branch 'master' into sheafification-QIT
MatthiasHu Aug 28, 2023
06a6fb9
make helpers private
MatthiasHu Aug 28, 2023
551387c
let isSheaf be an hProp
MatthiasHu Aug 31, 2023
b41e529
fix naming typo
MatthiasHu Aug 31, 2023
2eef94d
un-bundle `hProp`s in `Sheaf.agda`
MatthiasHu Nov 16, 2023
fa6a3a3
un-bundle `hProp`s in `Sieve.agda`
MatthiasHu Nov 17, 2023
24a7c5c
rename `F` -> `sheafification`
MatthiasHu Nov 18, 2023
74b0ae6
also rename the HIT `⟨F⟅_⟆⟩` and the local `F`
MatthiasHu Nov 18, 2023
6a8f149
elaborate universe level comment
MatthiasHu Nov 18, 2023
0f521b3
Merge branch 'master' into sheafification-QIT
MatthiasHu Nov 20, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Merge branch 'master' into attempt-at-sheafification
MatthiasHu committed Jul 27, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 9b863414f84421ff0a1a6450e37e54face97b71e

This merge commit was added into this branch cleanly.

There are no new changes to show, but you can still view the diff.