⊢ Γ  @g@types.pl

still i gotta add The Cubes

um yes thats literally how its defined. nm no scary new judgment today

wait isnt
$\Psi \mathrel| \Gamma \vdash M : A [\overline{\xi_i \mapsto N_i}]$
just the same as
$\overline{\Psi, \xi_i \mathrel| \Gamma \vdash M = N_i: A}$ ​

cubes,,,,,,,,,

huohughuhg "s has type A and also is equal to these terms under these constraints"

put cube on top of other cube

unfortunately i totally forgot wtf cubical composition is again

😏

😏 cube time

​

[in case people on other instances missed it: u can open ​ posts with latex in them in a new tab & have it nice and rendered]

ok i am gonna post about quox on here instead now so i can actually write like $(x :_\pi A) \times B$

also cos this is literally the place for that stuff