Roman Avermann

@mattecapu this is gold

Good Will Hunting Bar scene but it's about fibrations in category theory 🧵👇

@evie_fp @tangled_zans "Some animals are humans" corresponds with the type Σ(x: Animal) Σ(y: Human) x = y a function of type "Animal -> Bool" corresponds to an implication that if Animal is inhabited, then Bool is inhabited I don't know if I'm being dense or something but I don't see your point

@parabeans @tangled_zans Here's an example of what I mean: consider something like "Some animals are humans". In logic, you can plug in "blue" to see whether it's a human and just get ⊥. Same goes for "Spike". OTOH, with `isHuman : Animal → Bool`, you get a type error for "blue, and ⊥ for "Spike".

@tangled_zans You can write any garbled collection of words as a (false) logical proposition, but technically you shouldn't be able to do the same in a type theory because it'd need to typecheck?

BASED path induction?????? 😳😳

@davidtolnay yesss! but I wonder why this wasn't implemented in the first place?

This is the impact of Cargo sparse registry protocol (Rust 1.68+) on my CI jobs.

no, I don't use haskell. now give me the damn pizza