re: latex, xtt 

still i gotta add The Cubes

Show thread

re: latex, xtt 

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

Show thread

latex, xtt 

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}$ :ms_nissthink:

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

unfortunately i totally forgot wtf cubical composition is again

Show thread

re: latex 

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

Show thread


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

more like wtf types!!! haha gottem

{-# OPTIONS --two-level #-}

agda please

haskell facts:
- To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
- Valid hole fits include: undefined :: forall a. a
- panic: the impossible happened

⊢ Γ :agda_trans: :twelf: boosted
⊢ Γ :agda_trans: :twelf: boosted

latex from another instance test (hello 


Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.