Mercurial > hg > Members > kono > Proof > category
changeset 521:00bf9eca0db7
only yellow remains in uniquness
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 22 Mar 2017 17:48:22 +0900 |
| parents | 5b4a794f3784 |
| children | 8fd030f9f572 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 13 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Wed Mar 22 11:27:15 2017 +0900 +++ b/SetsCompleteness.agda Wed Mar 22 17:48:22 2017 +0900 @@ -122,16 +122,14 @@ ek=h {d} {h} {eq} = refl fhy=ghy : {d : Obj Sets } { h : Hom Sets d a } {y : d } → (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]) → f (h y) ≡ g (h y) fhy=ghy {d} {h} {y} fh=gh = ≡cong ( λ f → f y ) fh=gh - xequ : (x : a ) → { fx=gx : f x ≡ g x } → sequ a b f g - xequ x { fx=gx } = elem x fx=gx 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} → {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] } → - {h' : Hom Sets d a} → Sets [ h ≈ h' ] → {fh'=gh' : Sets [ Sets [ f o h' ] ≈ Sets [ g o h' ] ] } → + 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} {fh=gh} {h'} h=h' {fh'=gh'} = extensionality Sets ( λ y → begin + 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 ) @@ -154,15 +152,21 @@ 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 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 ⟩ - k ( Sets [ (λ e → equ e) o k' ] ) {!!} - ≈⟨⟩ + ≈↑⟨ k-cong ek'=h (lemma4 {d} ) (lemma3 {d} ) ⟩ Sets [ ( λ e → elem (equ e) (fe=ge0 e )) o k' ] - ≈⟨ car lemma2 ⟩ + ≈⟨ car (lemma2 ) ⟩ Sets [ ( λ e → e ) o k' ] ≈⟨⟩ k'