Skip to content

Instantly share code, notes, and snippets.

View cppio's full-sized avatar

Parth Shastri cppio

View GitHub Profile
-- https://arxiv.org/abs/1911.08174
def T : Prop := ∀ p, (p → p) → p → p
def δ (z : T) : T := fun p η h => η (z (T → T) id id z p η h)
def ω : T := fun _ _ h => propext ⟨fun _ => h, fun _ => id⟩ ▸ δ
def Ω : T := δ ω
noncomputable def WellFounded.fix' {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Sort v} (F : ∀ x, (∀ y, r y x → C y) → C x) x : C x :=
@Acc.rec α r (fun x _ => C x) (fun x _ => F x) x (Ω (∀ x, Acc r x) (fun wf x => ⟨x, fun y _ => wf y⟩) hwf.apply x)
theorem WellFounded.fix'_eq : @WellFounded.fix' α r hwf C F x = F x fun y _ => hwf.fix' F y := rfl
@cppio
cppio / Inf.lean
Last active August 9, 2025 22:46
noncomputable def inf : Acc (fun _ _ => True) () → Nat := Acc.rec fun _ _ ih => ih () ⟨⟩ + 1
example : inf h = inf h + 1 := @id (inf h = inf ⟨_, fun _ _ => h⟩) rfl
-- example : inf h = inf h + 1 := rfl -- fails
-- https://arxiv.org/abs/1911.08174
def T : Prop := ∀ p, (p → p) → p → p
def δ (z : T) : T := fun p η h => η (z (T → T) id id z p η h)
def ω : T := fun _ _ h => propext ⟨fun _ => h, fun _ => id⟩ ▸ δ
def Ω : T := δ ω
@cppio
cppio / Hurkens.agda
Created May 30, 2025 17:09
Girard-Hurkens paradox in Agda
{-# OPTIONS --rewriting --confluence-check #-}
module Hurkens where
open import Agda.Builtin.Equality
import Agda.Builtin.Equality.Rewrite
postulate
Π₁ : (Set₁ → Set₁) → Set₁
λ₁ : ∀ {F} → (∀ A → F A) → Π₁ F
@cppio
cppio / NoEmbedding.lean
Created May 27, 2025 12:03
Lean proof that higher universes don't embed into lower ones.
inductive Tree : Sort (max (u + 1) v)
| node {A : Sort u} (c : A → Tree)
theorem no_embedding
(Lower : Sort (max (u + 1) v) → Sort u)
(down : ∀ {α}, α → Lower α)
(up : ∀ {α}, Lower α → α)
(up_down : ∀ {α} (x : α), x = up (down x))
: False := by
induction h : Tree.node up
opaque f : Nat → Nat
opaque g : Nat → Nat → Nat
inductive T : Nat → Type
| mk₁ x : T (f x)
| mk₂ x y : T (g x y)
theorem hcongrArg₂ {α : Sort u} {β : α → Sort v} {γ : ∀ a, β a → Sort w} (f : ∀ a b, γ a b) {a₁ a₂ : α} (ha : a₁ = a₂) {b₁ : β a₁} {b₂ : β a₂} (hb : HEq b₁ b₂) : HEq (f a₁ b₁) (f a₂ b₂) :=
by cases ha; cases hb; rfl
inductive Le (x : Nat) : (y : Nat) → Prop
| refl : Le x x
| step : Le x y → Le x y.succ
inductive Ge (x : Nat) : (y : Nat) → Prop
| refl : Ge x x
| step : Ge x y.succ → Ge x y
inductive Le' : (x y : Nat) → Prop
| zero : Le' .zero y
import Lean.Elab.Command
elab tk:"#show " "macro " i:ident : command => do
let key ← Lean.Elab.Command.liftCoreM do Lean.Elab.realizeGlobalConstNoOverloadWithInfo i
let env ← Lean.getEnv
let names := Lean.Elab.macroAttribute.getEntries env key |>.map (·.declName)
Lean.logInfoAt tk (.joinSep names Lean.Format.line)
elab tk:"#show " "term_elab " i:ident : command => do
let key ← Lean.Elab.Command.liftCoreM do Lean.Elab.realizeGlobalConstNoOverloadWithInfo i
@cppio
cppio / ansi.py
Created January 5, 2025 22:34
ANSI escape codes in Python
from collections import namedtuple
colors = namedtuple("colors", "black red green yellow blue magenta cyan white default")(0, 1, 2, 3, 4, 5, 6, 7, 9)
brightcolors = namedtuple("brightcolors", "black red green yellow blue magenta cyan white")(60, 61, 62, 63, 64, 65, 66, 67)
color = namedtuple("color", "r g b")
del namedtuple
def ansi(*, bold=None, underlined=None, inverse=None, foreground=None, background=None):
params = []
if bold is not None:
␀␁␂␃␄␅␆␇␈␉␊␋␌␍␎␏␐␑␒␓␔␕␖␗␘␙␚␛␜␝␞␟
␠!"#$%&'()*+,-./0123456789:;<=>?
@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_
`abcdefghijklmnopqrstuvwxyz{|}~␡
def foo : x = y → Bool := Eq.rec true
theorem bar : False = PEmpty := propext ⟨False.elim, PEmpty.elim⟩
theorem baz : Quot.mk (fun _ _ => True) false = Quot.mk _ true := Quot.sound trivial
theorem qux : foo h = true := h.rec (motive := fun _ h => h.rec true = true) rfl
example : foo bar = true := rfl
example : foo baz = true := rfl
example : foo bar = true := qux
example : foo baz = true := qux