Eckmann Hilton #90
Eckmann Hilton #90
Conversation
thibautbenjamin
force-pushed
the
eckmann-hilton
branch
2 times, most recently
from
016b66b to
87d5206
Compare
thibautbenjamin
force-pushed
the
eckmann-hilton
branch
12 times, most recently
from
1547e06 to
72d53e6
Compare
thibautbenjamin
force-pushed
the
eckmann-hilton
branch
from
2f38d5c to
d1cadbf
Compare
thibautbenjamin
force-pushed
the
eckmann-hilton
branch
6 times, most recently
from
1a32b70 to
dad68e0
Compare
thibautbenjamin
force-pushed
the
eckmann-hilton
branch
from
dad68e0 to
54f8d94
Compare
thibautbenjamin
force-pushed
the
eckmann-hilton
branch
from
54f8d94 to
b4f8546
Compare
lib/eh.ml
Outdated
| val n : int | ||
| end | ||
|
|
||
| let memo_args = Hashtbl.create 97 |
There was a problem hiding this comment.
Why is this memoized? Very confused - it should basically just be a tuple or even a single integer!
Is it to support pointer equality on what would be objects? Seems a bit bizarre
There was a problem hiding this comment.
FTR, the aim is exactly to have pointer equality, as those are passed as arguments to modules which memoize stuff, and so we want the pointers to be the same, so that the modules are the same and the memoization is effective. It's a bit ugly, but I don't know of a good workaround
| Construct.wcomp_n (n - 1) | ||
| [ p; Tm.constr (psfpad_aux (n - 1)); q ]; | ||
| ] | ||
| | _ -> |
There was a problem hiding this comment.
There was a problem hiding this comment.
I don't know how to do this without duplicating all the declarations just above the match to compare with n
There was a problem hiding this comment.
You don't have to duplicate them. Leave the nested match. Change line 284 to be '''_ when (m < i) && (i <= n)'''
Change the inner match to be i < n or any other case. You can even match on '''i < n'''
wilfofford
left a comment
wilfofford
left a comment
There was a problem hiding this comment.
reviewed up to eh.mli
| let x = Var.Db 0 | ||
| let x_constr = (Var x, Obj) | ||
|
|
||
| let id2 i j = |
There was a problem hiding this comment.
id2 makes me think id^2(x). Perhaps id_i_j_id_i although this is longer?
There was a problem hiding this comment.
Agreed, took me a while to figure out
lib/eh.ml
Outdated
| module D = struct | ||
| let ps _ = Unchecked.disc 0 | ||
| let p_src i = id2 i Args.k | ||
| let q_tgt i = id2 i Args.k |
There was a problem hiding this comment.
or
let q_tgt i = p_src i
| module D = struct | ||
| let ps i = Unchecked.disc i | ||
| let p_src i = d_src i | ||
| let q_tgt i = d_src i |
There was a problem hiding this comment.
or let q_tgt i = p_src i
| module Prev = Padding.Suspend (UnbiasedPadding (PrevArgs)) | ||
|
|
||
| module M : Padding.FiltrationMorphismS = struct | ||
| let name = "Susp" |
There was a problem hiding this comment.
If I have understood correctly, this is the name of a substitution. In which case, I think it is confusing to call it "Susp", as suspension is a meta-operation, not a substitution. A suggestion for another name would be "Reduce" as it is a substitution from the suspension to the reduced suspension. However, this is perhaps also not optimal since we have the concept of reduced pasting contexts. If anyone has a better idea let me know - the only other one I can think of is "MergeBasePoints".
| let w_sub = [ w_constr; x_constr ] in | ||
| let witness_constr = | ||
| match i with | ||
| | i when i = m -> Construct.id_n 1 (Construct.wcomp v_c (n - 1) w_c) |
There was a problem hiding this comment.
I think you could use Construct.id instead of Construct.id_n 1. The same thing occurs in the "witness" implementation in construct.ml
| module type S = sig | ||
| include MakerS | ||
|
|
||
| val repadded : Tm.t |
There was a problem hiding this comment.
I don't love "repadded" as a name. If I have understood correctly, S.repadded is the name of the repadding term phi : Padded1(v) -> Padded2(v) . But to me "repadded" means Padded2(v) itself, i.e. the target of repadding. What would be wrong with calling this repadding?
| let f_constr = (Var (Var.Db 2), Construct.arr x_constr y_constr) in | ||
| let cohty = | ||
| Construct.arr f_constr | ||
| (Construct.comp_n [ f_constr; Construct.id_n 1 y_constr ]) |
There was a problem hiding this comment.
Can probably use Construct.id instead of Construct.id_n 1
| in | ||
| aux (F.ctx i) | ||
|
|
||
| let sub i = |
There was a problem hiding this comment.
I'm not super happy with this as it only accounts for filtration substitutions that leave everything except the marked variable constant. But since this covers all the examples we consider we can leave this here, as long as we are happy that this does not match the formalism in the paper.
Implementation of higher-dimensional EH cells.