I've set up my blog (with one post!).

You can find it here: https://no-learns.neocities.org/

Thank you so much for this. This is gonna simplify my thesis development as well!

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.

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?

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". :blobhappy:

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.

So here it just means the existence of an injective map (`inl` in this case), I guess.

lyxia@lyxia@niu.moe@abs

Awesome, thanks for writing this!