 |
Post Ay6SYOwJreRo7uN6fI by [email protected] |
 |
More posts by [email protected] |
|
Post #Ay0FJXnMC2aOtY0O9o by [email protected] |
|
0 likes, 0 repeats |
|
|
|
i dont really understand why substitutions are contravariant. why do you say &q… |
|
|
|
Post #Ay0FJXu5mzyRER9lei by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh If I have a substution γ : Δ → Γ and a term Γ ⊢ M : A and I … |
|
|
|
Post #Ay0FJY07QanJX7ya36 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@maxsnew Δ |- M : A[γ] ? |
|
|
|
Post #Ay0FJY5n5VKboid6tE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh Right, so that's why it makes sense to orient it as γ : Δ → … |
|
|
|
Post #Ay0FJYCAhmR48VcCps by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@maxsnew i dont quite follow. why are we composing Δ → Γ and Δ → A lol |
|
|
|
Post #Ay0FJYHqMgyMQ6Gjg0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh sorry typos |
|
|
|
Post #Ay0FJYnkS4Ue13CDPE by [email protected] |
|
0 likes, 0 repeats |
|
|
|
i am simply going to think of everything as going backwards until we actually h… |
|
|
|
Post #Ay0FJlubhshig5VNOy by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@maxsnew ah i see. so "applying" a substitution is semantically a com… |
|
|
|
Post #Ay6SXCBdnH8iHhxmdM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh Repeating a bit from other answers but what started to make this cli… |
|
|
|
Post #Ay6SXCI1PYFAbUwsa0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@mevenlennonbertrand this is really really nice actually, thank you for this :) |
|
|
|
Post #Ay6SYGYd1qkA87E4cy by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh I like to think of a substitution as Δ ⊢ γ : Γ, where it acts o… |
|
|
|
Post #Ay6SYGeefRZ2Qo2t1M by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ionchy this is a cool way to think of it, the judgement form really helps - i … |
|
|
|
Post #Ay6SYOosJKUbkotA3s by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh Hm, well, of course, nothing stops us from defining Sb' D G = Sb… |
|
|
|
Post #Ay6SYOwJreRo7uN6fI by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh I think it helps a bit to think of contexts not as big bags of varia… |
|
|
|
Post #Ay6SYP1dXshWOOrLxA by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@danielgratzer sorry, I don't quite follow. when you say "substitution… |
|
|
|
Post #Ay6SYP8N8q5YjI0jS4 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh Uh, sorry, I just needed some notation for the empty context that I … |
|
|
|
Post #Ay6SYPDgp4LGzmUyjw by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@danielgratzer i see, this makes a bit of sense (not entirely, because the noti… |
|
|
|
Post #Ay6SYVeUuJLowf5TMG by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@bhaktishh Of course! (For whatever it's worth, I believe I also found this… |
