Skip to content

Instantly share code, notes, and snippets.

@pnlph
Last active January 14, 2020 12:24
Show Gist options
  • Save pnlph/1f02c89fade7a62d40d86d554b53fa50 to your computer and use it in GitHub Desktop.
Save pnlph/1f02c89fade7a62d40d86d554b53fa50 to your computer and use it in GitHub Desktop.
Lemma 1.17 from Jesper Cockx's thesis
{-# OPTIONS --without-K #-}
-- Lemma 1.17 from Jesper Cockx's PhD thesis
-- Dependent Pattern Matching and Proof-Relevant Unification.
-- KU Leuven 2017
module Lemma1-17-h where
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
cong : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl
record _≃_ (A B : Set) : Set where
field
apply : A → B
linv : B → A
rinv : B → A
isLinv : (x : A) → linv (apply x) ≡ x
isRinv : (y : B) → apply (rinv y) ≡ y
open _≃_
-- Enunciation of lemma 1.17
lemma1-17 : Set₁
lemma1-17 = {A B : Set} (f : A ≃ B) (y : B) → linv f y ≡ rinv f y
-- One-click proof of lemma 1.17
.linv-is-rinv : {A B : Set} (f : A ≃ B) (y : B) → linv f y ≡ rinv f y
linv-is-rinv f y = sym (trans (sym (isLinv f (rinv f y))) (cong (linv f) (isRinv f y)))
------------------------------------------------------------------------
-- Step-by-step proof of lemma 1.17
------------------------------------------------------------------------
-- Step -2 Branch A
-- f rinv f y = y
-- follows from the definition of isRinv
f-rinvf-y-is-y : {A B : Set} (f : A ≃ B) (y : B) → apply f (rinv f y) ≡ y
f-rinvf-y-is-y f y = isRinv f y
-- Step -1 Branch A
-- linv f f rinv f y = linv f y
-- follows by applying cong linv f to the proof of -2A
linvf-f-rinvf-y-is-linvf-y : {A B : Set} (f : A ≃ B) (y : B) → linv f (apply f (rinv f y)) ≡ linv f y
linvf-f-rinvf-y-is-linvf-y f y = cong (linv f) (f-rinvf-y-is-y f y)
-- Step -3 Branch B
-- linv f f x = x
-- follows from the definition of isLinv
linvf-f-x-is-x : {A B : Set} (f : A ≃ B) (x : A) → linv f (apply f x) ≡ x
linvf-f-x-is-x f x = isLinv f x
-- Step -2 Branch B
-- x = linv f f x
-- follows by applying sym to the proof of -3B
x-is-linvf-f-x : {A B : Set} (f : A ≃ B) (x : A) → x ≡ linv f (apply f x)
x-is-linvf-f-x f x = sym (linvf-f-x-is-x f x)
-- Step -1 Branch B
-- rinv f y = linv f f rinv f y
-- follows by applying the proof of -2B to the value rinv f y
rinvf-y-is-linvf-f-rinvf-y : {A B : Set} (f : A ≃ B) (y : B) → rinv f y ≡ linv f (apply f (rinv f y))
rinvf-y-is-linvf-f-rinvf-y f y = x-is-linvf-f-x f (rinv f y)
-- Step 1
-- rinv f y = linv f y
-- follows by applying trans to the proofs of -1B and -1A
rinvf-y-is-linvf-y : {A B : Set} (f : A ≃ B) (y : B) → rinv f y ≡ linv f y
rinvf-y-is-linvf-y f y = trans (rinvf-y-is-linvf-f-rinvf-y f y) (linvf-f-rinvf-y-is-linvf-y f y)
-- Step 2
-- linv f y = rinv f y
-- follows by applying sym to the proof of 1
linvf-y-is-rinvf-y : {A B : Set} (f : A ≃ B) (y : B) → linv f y ≡ rinv f y
linvf-y-is-rinvf-y f y = sym (rinvf-y-is-linvf-y f y)
-- ∎
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment