← Feed

Posts

• Post #2728851

  Does anybody know of a good introductory reference or lecture notes for the use of categorical gluing in proofs of normalization and other metatheoretic properties of type theory? It's topic I'm finding more and more interesting, but I'm also finding it very hard to get into. I've tried going back to the source, the Altenkirch, Hofmann, Streicher articles from the 90s, and although I feel like I have the necessary categorical background, I'm finding them p...

• Post #2728850

  I'm not sure if this is too specific a question for anyone to answer, but here goes. I've recently been looking into Krivine's proof of a variant of the completeness theorem for classical first order logic. In the paper "Krivine’s intuitionistic proof of classical completeness (for countable languages)", Berardo and Valentini say: > It is a bit puzzling that, even if Krivine’s algorithm was recently implemented by Raffalli, no explicit description...

• Post #2728849

  I have a question about models of second order theories. Suppose we have a theory with a single sort Tm and two operations, app : Tm -> Tm -> Tm and lam : (Tm -> Tm) -> Tm possibly also satisfying the equation app (lam u) v = u v. We would like to say that a model of this theory is a type 𝑀, equipped with functions app_M and lam_M of the appropriate type. With this setup, is it the case that we don't necessarily have an interpretation function [| _ |] : Tm...

• Post #2728848

  There more I think about it, the more excited I become about @jonmsterling 's idea of implementing custom eliminators in Pterodactyl. I was recently working with a binary representation of natural numbers in agda. You can prove these are equivalent to the usual natural numbers and this gives a very useful alternative induction principle that comes from the binary structure. It would be so nice to have a native syntax for this! Currently you have to just apply the function and supply the...