Last active
January 14, 2020 12:24
-
-
Save pnlph/1f02c89fade7a62d40d86d554b53fa50 to your computer and use it in GitHub Desktop.
Lemma 1.17 from Jesper Cockx's thesis
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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