Show newer

Most of what I know about LaTeX is just from having used other people's snippets and random stack overflow answers and I feel like I should probably one day read, like, whatever the official reference guide for LaTeX

I'm tired of this it's so tedious
I'm sure the subsizing judgement translates to a proof of ≤
But I gotta have all my pieces ready eventually, and if I don't do it now I still have to do it later...

Show thread

If Agda people can manage suc/lsuc then people reading this can manage suc/succ

Show thread

Would it be confusing to have both suc and succ, and then both lim and limit

Show thread

I would call it "limit" but the other constructor that states that the upper bound is the least upper bound is named "limiting" so idek anymore

Show thread

I need to name the constructors of my order but the paper I'm following calls it "cocone" and I don't know what that means

Take an undecidable proof search
Sometimes you can't find the proof because its negation holds so you're spending all your time looking for something that isn't there
Sometimes you can't find the proof because there just isn't any term that proves it, or refutes it, or even irrefutes it

Show thread

You ever think about how undecidability sometimes means independence

Sometimes... It's clearer to describe syntactic sugar using words than using symbols in a pseudometafunction...

Society has moved beyond the need for fully-sized inductives

Oh I see. The paper restrict what may be declared as a Prop but the implementation allows anything in Prop and then disallows pattern matching

Show thread

Alright I'm very suspicious of whether Agda checks Prop by default because I can put naturals in Prop and that's very disallowed by the definitional proof irrelevance paper

Show thread

I can do this too:

data Pair (A : Set ℓ) (B : A → Set ℓ) : Prop ℓ where
pair : (a : A) → B a → Pair A B

Wasn't there something not good with strong pairs in Prop? Maybe that was only for impredicative Prop? Odd that definitionally strict Prop is fine

Show thread

Agda lets me put W types in Prop as long as its level is the same as the parameter universe levels, even if the parameters are in Set
Weird

bundle exec rails assets:clobber
bundle exec rails assets:precompile
Show thread
Show older
types.pl

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.