Mercurial > hg > Members > kono > Proof > category
changeset 520:5b4a794f3784
k-cong done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 22 Mar 2017 11:27:15 +0900 |
| parents | 844328b49d5d |
| children | 00bf9eca0db7 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 15 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Tue Mar 21 16:28:34 2017 +0900 +++ b/SetsCompleteness.agda Wed Mar 22 11:27:15 2017 +0900 @@ -14,7 +14,7 @@ -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ -≡-cong = Relation.Binary.PropositionalEquality.cong +≡cong = Relation.Binary.PropositionalEquality.cong @@ -75,7 +75,7 @@ ipcx {q} {qi} {qi'} qi=qi x = begin record { pi1 = λ i → (qi i) x } - ≡⟨ ≡-cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡-cong ( λ f → f x ) (qi=qi i) )) ⟩ + ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩ record { pi1 = λ i → (qi' i) x } ∎ where open import Relation.Binary.PropositionalEquality @@ -117,24 +117,26 @@ fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] fe=ge = extensionality Sets (fe=ge0 ) k : {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g) - k {d} h eq = λ x → elem (h x) ( cong ( λ y → y x ) eq ) + k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) eq ) ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e ) o k h eq ] ≈ h ] 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 + 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 - elem-cong : {x x' : a } → ( x ≡ x' ) → ( eq eq' : f x ≡ g x ) → ( elem x eq ) ≡ ( elem x' eq' ) - elem-cong refl eq eq' = {!!} + 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' ] ] } → 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 h fh=gh y ≡⟨⟩ - elem (h y) ( fhy=ghy d h y fh=gh ) - ≡⟨ {!!} ⟩ - elem (h' y) ( fhy=ghy d h' y fh'=gh' ) + 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 @@ -144,11 +146,7 @@ Sets [ g o Sets [ (λ e → equ e) o k' ] ] ] lemma3 {d} {k'} = begin Sets [ f o Sets [ (λ e → equ e) o k' ] ] - ≈⟨ assoc ⟩ - Sets [ Sets [ f o (λ e → equ e) ] o k' ] - ≈⟨ car {!!} ⟩ - Sets [ Sets [ g o (λ e → equ e) ] o k' ] - ≈↑⟨ assoc ⟩ + ≈⟨ extensionality Sets ( λ y → fe=ge0 (k' y ) ) ⟩ Sets [ g o Sets [ (λ e → equ e) o k' ] ] ∎ where open ≈-Reasoning Sets @@ -161,10 +159,10 @@ uniqueness {d} {h} {fh=gh} {k'} ek'=h = begin k h fh=gh ≈↑⟨ k-cong ek'=h ⟩ - k ( Sets [ (λ e → equ e) o k' ] ) ( lemma3 {d} {k'} ) + k ( Sets [ (λ e → equ e) o k' ] ) {!!} ≈⟨⟩ Sets [ ( λ e → elem (equ e) (fe=ge0 e )) o k' ] - ≈⟨ car ( lemma2 {{!!}} ) ⟩ + ≈⟨ car lemma2 ⟩ Sets [ ( λ e → e ) o k' ] ≈⟨⟩ k'