issues
search
pufferffish
/
agda-symmetries
MIT License
5
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Lists: Free Monoidal Groupoid
#95
dignissimus
opened
4 months ago
0
Prove pentagon coherence for lists
#94
dignissimus
opened
4 months ago
1
Prove freeness for SLists
#93
vikraman
opened
4 months ago
1
Prove freeness of Lists
#92
vikraman
opened
4 months ago
0
Define the statements of the universal property for the specific groupoid structures
#91
vikraman
opened
4 months ago
1
HoTT/UF presentation
#90
pufferffish
opened
4 months ago
0
write the eliminators for FreeSMon and prove them by pattern matching
#89
github-actions[bot]
opened
4 months ago
0
pentagon coherence for lists
#88
github-actions[bot]
opened
4 months ago
1
write the eliminators for FreeMon and prove them by pattern matching
#87
github-actions[bot]
opened
4 months ago
0
coherences on top of signatures and equations
#86
github-actions[bot]
opened
4 months ago
0
Migrate from netlify
#85
pufferffish
closed
5 months ago
0
Checkpoint upto 5.2.1
#84
pufferffish
closed
5 months ago
0
Free commutative monoid section
#83
vikraman
closed
4 months ago
0
Free monoid section
#82
vikraman
closed
4 months ago
0
Universal algebra section
#81
vikraman
closed
4 months ago
0
intrinsic verification vs extrinsic (in Coq/VFA)
#80
vikraman
closed
4 months ago
0
Move html render to netlify
#79
pufferffish
closed
6 months ago
0
Plug
#78
pufferffish
closed
6 months ago
0
Clean up sorting proof
#77
pufferffish
closed
6 months ago
0
HoTT/UF 2024 abstract
#76
pufferffish
closed
7 months ago
0
Some work on groupoids
#75
vikraman
closed
4 months ago
0
Prove section to homomorphism to SList implies linear order
#74
pufferffish
closed
6 months ago
1
Fix levels in Free so this isn't necessary
#72
github-actions[bot]
opened
9 months ago
0
Useful lemmas
#71
pufferffish
closed
9 months ago
0
Add normalization experiment
#70
vikraman
closed
9 months ago
0
Unused lemma
#69
github-actions[bot]
closed
8 months ago
1
Define isomorphism from Bag to CList
#68
pufferffish
closed
8 months ago
0
Use --exact-split and --safe
#67
vikraman
closed
8 months ago
0
Prove Bag is CMon
#66
pufferffish
closed
9 months ago
1
Add ⊕ as a helper in Mon.Desc
#65
github-actions[bot]
opened
9 months ago
0
Fix Bags
#64
vikraman
closed
9 months ago
0
Refactor permutation relation
#63
vikraman
closed
9 months ago
0
Rewrite PermRelation with Relation.Binary
#62
pufferffish
closed
9 months ago
1
Prove tptLemma using transp, not J
#61
github-actions[bot]
closed
9 months ago
1
Try to prove this to generalize all the proofs under
#60
github-actions[bot]
closed
9 months ago
1
Cleanup this mess
#59
github-actions[bot]
opened
9 months ago
0
Prove natural numbers are free X-structures on Y
#58
vikraman
opened
10 months ago
0
Define free commutative rig (or semiring)
#57
vikraman
opened
10 months ago
0
More constructions of free commutative monoids
#56
pufferffish
closed
9 months ago
3
Develop some applications
#55
vikraman
opened
10 months ago
0
More constructions of free commutative monoids
#54
vikraman
closed
9 months ago
2
: Rename the fields to shorter names
#53
github-actions[bot]
closed
10 months ago
1
Write generic lemma about compatibility between lookup and sharp
#52
github-actions[bot]
opened
10 months ago
0
Prove SList is free symmetric monoidal on groupoids
#51
github-actions[bot]
closed
4 months ago
1
Define free symmetric monoidal groupoids as a HIT
#50
github-actions[bot]
closed
4 months ago
1
Show that List A has all the monoidal coherences
#49
github-actions[bot]
closed
4 months ago
1
Define free monoidal groupoids as a HIT
#48
github-actions[bot]
closed
4 months ago
1
refactor as a coequaliser
#47
github-actions[bot]
opened
10 months ago
0
refactor as (Tree σ Unit -> Tree σ X) × (Tree σ Unit -> Tree σ X) ?
#46
github-actions[bot]
opened
10 months ago
0
Refactor Free structure lemmas
#45
vikraman
closed
10 months ago
0
Next