# HG changeset patch # User Shinji KONO # Date 1491794161 -32400 # Node ID 14483d9d604c747f1447616e9f52d73513dad71d # Parent 2c0e168c832e1e78a6fc5056326d3ee1f0cb3598 dead end again ... diff -r 2c0e168c832e -r 14483d9d604c SetsCompleteness.agda --- a/SetsCompleteness.agda Mon Apr 10 10:48:50 2017 +0900 +++ b/SetsCompleteness.agda Mon Apr 10 12:16:01 2017 +0900 @@ -187,7 +187,8 @@ record snequ { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I )→ sobj i → sobj j ) : Set c₂ where field - snequ1 : { i j : OC } → ( f : I → I ) → sequ ( snproj sobj smap ) (sobj j) ( λ x → smap f ( snmap x i ) ) ( λ x → snmap x j ) + sn : snproj sobj smap + snequ1 : { i j : OC } → ( f : I → I ) → sequ (sobj i) (sobj j) ( λ x → smap f ( snmap sn i ) ) ( λ x → snmap sn j ) open snequ @@ -197,24 +198,21 @@ Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) → NTrans C Sets (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ) )) Γ Cone C I s Γ = record { - TMap = λ i → λ se → snmap ( equ ( snequ1 se {i} {i} (λ x → x )) ) i + TMap = λ i → λ se → snmap ( sn se ) i ; isNTrans = record { commute = comm1 } } where comm1 : {a b : Obj C} {f : Hom C a b} → - Sets [ Sets [ FMap Γ f o (λ se → snmap (equ (snequ1 se (λ x → x))) a) ] ≈ - Sets [ (λ se → snmap (equ (snequ1 se (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ] ] - comm1 {a} {b} {f} = begin - FMap Γ f o (λ se → snmap (equ (snequ1 se (λ x → x))) a) - ≈⟨⟩ - ( λ se → FMap Γ f (snmap se a )) o (λ se → equ (snequ1 se (λ x → x)) ) - ≈⟨ {!!} ⟩ - ( λ se → snmap se b ) o (λ se → equ (snequ1 se (λ x → x)) ) - ≈⟨⟩ - (( λ se → snmap se b ) o (λ se → equ (snequ1 se (λ x → x)) ) ) o id1 Sets ( snequ (ΓObj s Γ) (ΓMap s Γ) ) - ≈⟨⟩ - (λ se → snmap (equ (snequ1 se (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f - ∎ where - open ≈-Reasoning Sets + Sets [ Sets [ FMap Γ f o (λ se → snmap (sn se) a) ] ≈ + Sets [ (λ se → snmap (sn se) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ] ] + comm1 {a} {b} {f} = extensionality Sets ( λ se → begin + FMap Γ f (snmap (sn se) a) + ≡⟨ ≡cong ( λ f → FMap Γ f ( snmap (sn se) a )) (sym ( hom-iso s )) ⟩ + FMap Γ (hom← s ( hom→ s f)) (snmap (sn se) a) + ≡⟨ fe=ge0 ( snequ1 se (hom→ s f ) ) ⟩ + snmap (sn se) b + ∎ ) where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) → Limit Sets C Γ @@ -227,19 +225,15 @@ ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} } } where - a0 : Obj Sets - a0 = snequ (ΓObj s Γ) (ΓMap s Γ) setprod : {a : Obj Sets} → NTrans C Sets (K Sets C a) Γ → (x : a ) → snproj (ΓObj s Γ) (ΓMap s Γ) setprod t x = record { snmap = λ i → TMap t i x } - comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) - → ΓMap s Γ f (TMap t i x) ≡ TMap t j x - comm2 {a} {x} t f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) comm3 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) - → Sets [ Sets [ (λ x₁ → ΓMap s Γ f (snmap x₁ i)) o setprod t ] ≈ Sets [ (λ x₁ → snmap x₁ j) o setprod t ] ] - comm3 {a} {x} t f = IsNTrans.commute (isNTrans t ) + → Sets [ Sets [ (λ x₁ → ΓMap s Γ f (snmap (setprod t x) i)) o TMap t i ] ≈ Sets [ (λ x₁ → snmap (setprod t x) j) o TMap t i ] ] + comm3 {a} {x} t f = {!!} limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ)) limit1 a t = λ ( x : a ) → record { - snequ1 = λ {i} {j} f → k ( setprod t ) (comm3 {a} {x} t f ) x + sn = setprod t x + ; snequ1 = λ {i} {j} f → k (TMap t i ) (comm3 t f ) x } t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o limit1 a t ] ≈ TMap t i ] t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin @@ -254,40 +248,16 @@ limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin limit1 a t x ≡⟨⟩ - record { snequ1 = λ {i} {j} f' → k ( setprod t ) (comm3 {a} {x} t f' ) x } - ≡⟨ ≡cong ( λ ff → record { snequ1 = λ {i} {j} f' → ff i j f' }) ( - extensionality Sets ( λ i → extensionality Sets ( λ j → extensionality Sets ( λ f' - → k-cong {i} {j} f' x - ))) - ) ⟩ - record { snequ1 = λ {i} {j} f' → snequ1 (f x) f' } + record { sn = setprod t x ; snequ1 = λ {i} f' → k ( TMap t i ) (comm3 {a} {x} t f' ) x } + ≡⟨ ≡cong2 {!!} {!!} {!!} ⟩ + record { sn = sn ( f x ) ; snequ1 = λ {i} {j} f' → ( snequ1 (f x ) f' ) } ≡⟨⟩ f x ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning snmap-cong : ( e : snequ (ΓObj s Γ) (ΓMap s Γ) ) {i : Obj C } { f g : I → I } - → snmap ( equ ( snequ1 e f)) i ≡ snmap ( equ ( snequ1 e g)) i + → {!!} -- snmap ( equ ( snequ1 e f)) i ≡ snmap ( equ ( snequ1 e g)) i snmap-cong e {i} = ≡cong ( λ s → snmap s i ) refl - k-cong : { i j : Obj C } ( f' : I → I ) ( x : a ) → k ( setprod t ) (comm3 {a} {x} t f' ) x ≡ snequ1 (f x) f' - k-cong {i} {j} f' x = begin - k ( setprod t ) (comm3 {a} {x} t f' ) x - ≡⟨ elm-cong (k ( setprod t ) (comm3 {a} {x} t f' ) x ) ( snequ1 (f x) f' ) ( begin - equ (k (setprod t) (comm3 {a} {x} t f') x) - ≡⟨⟩ - record { snmap = λ i' → TMap t i' x } - ≡⟨ ≡cong ( λ s → record { snmap = λ i' → s i' } ) ( extensionality Sets ( λ i' → ( sym ( begin - snmap ( equ ( snequ1 (f x) f')) i' - ≡⟨ snmap-cong (f x) ⟩ - snmap ( equ ( snequ1 (f x) (λ x → x ))) i' - ≡⟨ ≡cong ( λ f → f x ) cif=t ⟩ - TMap t i' x - ∎ )))) ⟩ - record { snmap = λ i' → snmap (equ (snequ1 (f x) f')) i' } - ≡⟨⟩ - equ (snequ1 (f x) f') - ∎ - ) ⟩ - snequ1 (f x) f' - ∎ - + k-cong : { i j : Obj C } ( f' : I → I ) ( x : a ) → k ( TMap t i ) {!!} x ≡ snequ1 (f x) f' + k-cong {i} {j} f' x = {!!}