Mercurial > hg > Members > kono > Proof > category
changeset 595:0386e82f0dd8
dead end
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 May 2017 10:37:39 +0900 |
| parents | db76b73b526c |
| children | |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 16 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon May 22 12:04:34 2017 +0900 +++ b/SetsCompleteness.agda Tue May 23 10:37:39 2017 +0900 @@ -110,8 +110,8 @@ irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' irr refl refl = refl -elm-cong : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → (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' ) +elem-cong : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y +elem-cong ( elem x eq ) (elem .x eq' ) refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' ) fe=ge : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → Sets [ Sets [ f o (λ e → equ {_} {a} {b} {f} {g} e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] @@ -143,7 +143,7 @@ Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin k h fh=gh x - ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ + ≡⟨ elem-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ k' x ∎ ) where open import Relation.Binary.PropositionalEquality @@ -226,11 +226,11 @@ record { slproj = λ i → slproj s i ; slequ = λ i j f → slequ s i j f } ≡⟨ ≡cong2 ( λ x y → - record { slproj = λ i → x i ; slequ = λ i j f → {!!} } ) ( extensionality Sets ( λ i → eq1 i ) ) + record { slproj = λ i → x i ; slequ = λ i j f → y x i j f} ) ( extensionality Sets ( λ i → eq1 i ) ) ( extensionality Sets ( λ x → ( extensionality Sets ( λ i → ( extensionality Sets ( λ j → - ( extensionality Sets ( λ f → {!!} + ( extensionality Sets ( λ f → elem-cong {!!} {!!} {!!} )))))))) ⟩ record { slproj = λ i → slproj t i ; slequ = λ i j f → slequ t i j f } @@ -260,7 +260,17 @@ limit1 a t x ≡⟨⟩ record { slproj = λ i → TMap t i x ; slequ = λ i j f → elem i ( ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )) } - ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) (eq1 x) (eq2 x ) (eq3 x ) ⟩ + ≡⟨ + ≡cong2 ( λ z y → + record { slproj = λ i → z i ; slequ = λ i j f' → elem i (y z i j f')} ) ( extensionality Sets ( λ i → eq1 x i ) ) + ( extensionality Sets ( λ z → + ( extensionality Sets ( λ i → + ( extensionality Sets ( λ j → + ( extensionality Sets ( λ f' → irr (eq2 x i j f' ){!!} + )))))))) + ⟩ + record { slproj = λ i → slproj (f x ) i ; slequ = λ i j f' → elem i (fe=ge0 (slequ (f x) i j f')) } + ≡⟨ {!!} ⟩ record { slproj = λ i → slproj (f x ) i ; slequ = slequ (f x ) } ≡⟨⟩ f x