Skip to content

Instantly share code, notes, and snippets.

@rzrn
Created May 2, 2024 06:28
Show Gist options
  • Save rzrn/4b0440f84a836fcb2633ee952861cf33 to your computer and use it in GitHub Desktop.
Save rzrn/4b0440f84a836fcb2633ee952861cf33 to your computer and use it in GitHub Desktop.
universe u
inductive Eq' {A : Type u} : A → A → Type u
| idp (a : A) : Eq' a a
def f {A : Type u} {a b : A} : Eq' a b → Eq a b :=
λ q => @Eq'.casesOn A a (λ b q' => Eq a b) b q (Eq.refl a)
def g {A : Type u} {a b : A} : Eq a b → Eq' a b :=
λ p => @Eq.casesOn A a (λ b p' => Eq' a b) b p (Eq'.idp a)
def fg {A : Type u} {a b : A} (p : Eq a b) : f (g p) = p :=
rfl
def gf {A : Type u} {a b : A} (q : Eq' a b) : g (f q) = q :=
@Eq'.casesOn A a (λ b q' => g (f q') = q') b q rfl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment