Mercurial > hg > Members > kono > Proof > category
changeset 522:8fd030f9f572
Equalizer in Sets done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 26 Mar 2017 19:41:44 +0900 |
| parents | 00bf9eca0db7 |
| children | 4b097a010fd9 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 11 insertions(+), 50 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Wed Mar 22 17:48:22 2017 +0900 +++ b/SetsCompleteness.agda Sun Mar 26 19:41:44 2017 +0900 @@ -93,6 +93,7 @@ -- | . h --y : d + -- cf. https://github.com/danr/Agda-projects/blob/master/Category-Theory/Equalizer.agda data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g @@ -124,62 +125,22 @@ fhy=ghy {d} {h} {y} fh=gh = ≡cong ( λ f → f y ) fh=gh irr : {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' irr refl refl = refl - elm-cong : {x y : sequ a b f g} → equ x ≡ equ y → x ≡ y - elm-cong { elem x eq } {elem .x eq' } refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' ) - k-cong : {d : Obj Sets} {h : Hom Sets d a} → {h' : Hom Sets d a} → Sets [ h ≈ h' ] - → (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] ) → (fh'=gh' : Sets [ Sets [ f o h' ] ≈ Sets [ g o h' ] ] ) → - Sets [ k h fh=gh ≈ k h' fh'=gh' ] - k-cong {d} {h} {h'} h=h' fh=gh fh'=gh' = extensionality Sets ( λ y → begin - k h fh=gh y - ≡⟨⟩ - elem (h y) ( fhy=ghy fh=gh ) - ≡⟨ elm-cong ( ≡cong ( λ h → h y ) h=h') ⟩ - elem (h' y) ( fhy=ghy fh'=gh' ) - ≡⟨⟩ - k h' fh'=gh' y - ∎ ) where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - lemma3 : {d : Obj Sets} {k' : Hom Sets d (sequ a b f g)} → Sets [ Sets [ f o Sets [ (λ e → equ e) o k' ] ] ≈ - Sets [ g o Sets [ (λ e → equ e) o k' ] ] ] - lemma3 {d} {k'} = begin - Sets [ f o Sets [ (λ e → equ e) o k' ] ] - ≈⟨ extensionality Sets ( λ y → fe=ge0 (k' y ) ) ⟩ - Sets [ g o Sets [ (λ e → equ e) o k' ] ] - ∎ where - open ≈-Reasoning Sets - lemma1 : ( e : sequ a b f g ) → ( z : sequ a b f g ) → elem (equ z) (fe=ge0 z) ≡ z - lemma1 ( elem x eq ) (elem x' eq' ) = refl - lemma2 : { e : sequ a b f g } → ( λ e → elem (equ e) (fe=ge0 e ) ) ≡ ( λ e → e ) - lemma2 {e} = extensionality Sets ( λ z → lemma1 e z ) - lemma4 : {d : Obj Sets } {k' : Hom Sets d (sequ a b f g)} → Sets [ Sets [ f o Sets [ equ o k' ] ] ≈ Sets [ g o Sets [ equ o k' ] ] ] - lemma4 {d} {k'} = extensionality Sets ( λ y → begin - f ( equ ( k' y ) ) - ≡⟨ ≡cong ( λ e → e ( k' y) ) fe=ge ⟩ - g ( equ ( k' y ) ) - ∎ ) where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning + elm-cong : (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y + elm-cong ( elem x eq ) (elem .x eq' ) refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' ) + lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → + Sets [ f ≈ g ] → (x : a ) → f x ≡ g x + lemma1 refl x = refl + lemma5 : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → + Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x) + lemma5 refl x = refl -- somehow this is not equal to lemma1 uniqueness : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] - uniqueness {d} {h} {fh=gh} {k'} ek'=h = begin - k h fh=gh - ≈↑⟨ k-cong ek'=h (lemma4 {d} ) (lemma3 {d} ) ⟩ - Sets [ ( λ e → elem (equ e) (fe=ge0 e )) o k' ] - ≈⟨ car (lemma2 ) ⟩ - Sets [ ( λ e → e ) o k' ] - ≈⟨⟩ - k' - ∎ where - open ≈-Reasoning Sets - - + uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → + elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ) open Functor open NTrans - - record ΓObj { c₂ } ( I : Set c₂ ) : Set c₂ where field obj : I