Awesome, thanks for writing this!
@abs Here's what I alluded to earlier about record projections (which makes the first naive attempt in your post typecheck) https://gist.github.com/Lysxia/1ee6f3371536e1a00a9c3788faa7e6f1
@lyxia Oooh, these are both excellent!
Thank you so much for this. This is gonna simplify my thesis development as well!
@abs So, AFAIU, the β-expansion made the type-checker happy because the λ-abstraction properly "guided" the type-inference, keeping the type more general?
@amiloradovsky No, the problem is that matches only have effect on the return type of the match.
In the example without the lambda, the return type of the match is `@arith (sig_ext Sigma)` which is turned into `@arith (sig_ext Sig)` below the match. However, the type of e stays `@arith Sigma`.
By adding the lambda, the return type of the match now is `@arith Sigma -> @arith (sig_ext Sigma)` which is then turned into `@arith Sig -> @arith (sig_ext Sig)` below the match.
@amiloradovsky We're essentially doing the same thing by hand that the `revert` tactic does in Coq.
@abs Also, a tangent, but still: Why do people call these maps "lifts", shouldn't they be called "exten(d|sion)s" instead?
AFAIU, lifting is when we have two maps
f: X→Y and g: Z→Y (cospan), then build a map h: X→Z (e.g. lifting of continuous path from the base to the total space).
While extension is when we have maps f: X→Y and g: X→Z (span), then build a map h: Y→Z.
Here we have a span, of the enrichment map between the signatures (g) and interpretation (f). It's even a retraction, no?
@amiloradovsky I don't know anything about topology (which I think you're talking about?) so I can't justify the terminology with regards to that.
I took the terminology from my PF intuition, where lifting is used for operations that lift values of a type X into a subsuming type Y. For example, here `@arith Sigma` is clearly subsumed by `@arith (sig_ext Sigma)`. I don't know where this originated from, though.
@amiloradovsky Whoops, that should of course be my "FP" as in "functional programming".
@abs Yes, the terminology most likely originated from general topology, but nowadays it's used throughout category theory, AFAIK, because the formulation doesn't require anything topology-specific.
BTW, what "subsuming" means?
Here `arith` seems to be the interpretation, a map from a signature to a structure, and that better fits into the extension construction, rather than lifting.
Anyway, CS terminology isn't always consistent with purely mathematical.
@amiloradovsky Subsumes here is just the informal notion that values of type X intuitively are values of type Y as well (were it not for those pesky syntactic details). For example, X is subsumed by X + Y.
@abs OK, but IMO it's a deceiving notion: types aren't sets, and terms of one type can't/shouldn't be considered the terms of another type (unless one of the types is a universe containing the other, of course).
So here it just means the existence of an injective map (`inl` in this case), I guess.
@amiloradovsky It also, very crucially, carries with it the "triviality" of that injective map. For example, I wouldn't say that `nat * nat` is subsumed by `nat`, even though there does exist a fitting injective mapping.
Welcome to your niu world ! We are a cute and loving international community Ｏ(≧▽≦)Ｏ !