issues
search
vikraman
/
2DTypes
Collaborative work on reversible computing
17
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Prove the equivalence of UFin paths and Aut (Fin n)
#59
vikraman
closed
3 years ago
0
Prove postulates in Equiv1Norm.agda
#58
vikraman
closed
3 years ago
0
Sketch a first draft of the paper
#57
vikraman
closed
3 years ago
0
Prove Lehmer is a set
#56
vikraman
closed
3 years ago
0
Show the univalent sub-universe structure of UFin
#55
vikraman
closed
3 years ago
0
Prove eval₂
#54
vikraman
closed
3 years ago
3
Deal with the transports in Equiv1.agda
#53
vikraman
closed
3 years ago
1
Finish proving braid-transpos (in Level0)
#52
vikraman
closed
3 years ago
19
Some work on conjectures
#51
inexxt
closed
3 years ago
0
Some work on FSMG
#50
vikraman
closed
3 years ago
0
Use github actions for ci
#49
vikraman
closed
3 years ago
0
Extend the Coxeter relation to n=0
#48
inexxt
closed
3 years ago
0
Fill in Conjectures
#47
inexxt
closed
3 years ago
0
Fill in Conjectures
#46
inexxt
closed
3 years ago
0
Is Lemma 5.1 of "Categories of Petri Nets" somehow relevant
#45
JacquesCarette
closed
3 years ago
1
Brute-force transport Level0
#44
inexxt
closed
3 years ago
0
Prove the Coxeter HIT and set quotient versions are equivalent
#43
vikraman
opened
3 years ago
0
Prove the group structure of CList
#42
vikraman
opened
3 years ago
0
Sketch the equivalence between M 1 and UFin
#41
vikraman
opened
3 years ago
0
Prove the universal property of FSMG.M
#40
vikraman
opened
3 years ago
0
Show that FSMG.M is a symmetric monoidal groupoid
#39
vikraman
opened
3 years ago
0
Prove the universal property of FSMG
#38
vikraman
opened
3 years ago
0
Prove the symmetric monoidal laws for Fin n with coproduct
#37
vikraman
opened
3 years ago
0
Update the conjectures for equivalence between Pi and UFin
#36
vikraman
closed
3 years ago
0
[WIP] Pi+ parametrized Coxeter
#35
inexxt
closed
3 years ago
0
Some possible Coxeter (interface) definitons
#34
inexxt
closed
3 years ago
3
Pi+ finish coxter proof
#33
inexxt
closed
3 years ago
0
Define Sn as a HIT
#32
vikraman
closed
3 years ago
3
Normalized subset of Pi+
#31
inexxt
closed
3 years ago
1
Global goal and plan
#30
JacquesCarette
opened
3 years ago
6
Everything reduces to an immersion of a Lehmer code
#29
inexxt
closed
3 years ago
0
Lehmer codes - immersion is injective
#28
inexxt
closed
3 years ago
0
Write the two definitions of FSMG and assert their universal properties
#27
vikraman
closed
3 years ago
0
Fix CI
#26
inexxt
closed
3 years ago
1
Coxeter <-> MCoxeter
#25
inexxt
closed
3 years ago
1
Show that the 1-combinators in the normalized subset of Pi+ can be expressed as adjacent transpositions.
#24
vikraman
closed
3 years ago
0
Merge work on Pi+ and setup
#23
vikraman
closed
3 years ago
1
Prove eval (quote X) == X for level 0
#22
vikraman
closed
3 years ago
1
Setup a CI which typechecks the main theorems/conjectures
#21
vikraman
closed
3 years ago
0
Prove quote-eval^₁
#20
inexxt
closed
3 years ago
5
Finish writing the conjectures between Pi.U and UFin
#19
vikraman
closed
3 years ago
0
Show that UFin is a symmetric monoidal groupoid
#18
vikraman
opened
3 years ago
0
Fix the problem with termination checker in Diamond
#17
inexxt
opened
3 years ago
0
Write the equivalence between path space of `FSMG 1` and Coxeter
#16
vikraman
opened
3 years ago
1
Prove the equivalence between Coxeter and LongCoxeter
#15
vikraman
closed
3 years ago
1
Compose the equivalences: ∀ n, 1-paths in FSMG.M 1 ≃ Coxeter ≃ LongCoxeter ≃ Lehmer ≃ Aut (Fin n)
#14
vikraman
closed
3 years ago
10
Migrate the proof of equivalence between LongCoxeter and Lehmer
#13
vikraman
closed
3 years ago
0
Finish the proof of equivalence between Coxeter and Lehmer
#12
vikraman
closed
3 years ago
0
Construct the quotient of List (Fin n) by the Coxeter relation
#11
vikraman
closed
3 years ago
1
Write the two definitions of FSMG and assert their universal properties
#10
vikraman
closed
3 years ago
0
Previous
Next