# HG changeset patch # User Shinji KONO # Date 1491618951 -32400 # Node ID 09b1f66f7d7cc00d1358b94408063548a0e8e1a9 # Parent 97b98b81e99075ee91e329f2138055eafa490513 equalizer approach diff -r 97b98b81e990 -r 09b1f66f7d7c SetsCompleteness.agda --- a/SetsCompleteness.agda Thu Apr 06 04:15:57 2017 +0900 +++ b/SetsCompleteness.agda Sat Apr 08 11:35:51 2017 +0900 @@ -153,8 +153,8 @@ record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where field - hom→ : {i j : Obj C } → Hom C i j → I - hom← : {i j : Obj C } → ( f : I ) → Hom C i j + hom→ : {i j : Obj C } → Hom C i j → I → I + hom← : {i j : Obj C } → ( f : I → I ) → Hom C i j hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } → (x≈y : C [ x ≈ y ] ) → x ≡ y @@ -165,83 +165,29 @@ ΓObj s Γ i = FObj Γ i ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) - {i j : Obj C } →　 ( f : I ) → ΓObj s Γ i → ΓObj s Γ j + {i j : Obj C } →　 ( f : I → I ) → ΓObj s Γ i → ΓObj s Γ j ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) -record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) - ( smap : { i j : OC } → (f : I )→ sobj i → sobj j ) : Set c₂ where +record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I )→ sobj i → sobj j ) + ( Equ : { i j : OC } → { f : I → I } → sequ (sobj i) (sobj j) ( smap f ) ( smap (λ x → x ) )) : Set c₂ where field snmap : ( i : OC ) → sobj i - sncommute : { i j : OC } → ( f : I ) → smap f ( snmap i ) ≡ snmap j + sncommute : { i j : OC } → ( f : I → I ) → smap f ( snmap i ) ≡ snmap j open snat -snmeq : { c₂ : Level } { I OC : Set c₂ } { SO : OC → Set c₂ } { SM : { i j : OC } → (f : I )→ SO i → SO j } - ( s t : snat SO SM ) → ( i : OC ) → - { snmapsi snmapti : SO i } → snmapsi ≡ snmapti → SO i -snmeq s t i {pi} {.pi} refl = pi - -snat1 : { c₂ : Level } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I )→ sobj i → sobj j ) - ( s t : snat sobj smap ) - ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) → - (( i j : OC ) → (f : I ) → smap f (snmeq s t i (eq1 i) ) ≡ (snmeq s t j (eq1 j) )) → snat sobj smap -snat1 SO SM s t eq1 eqcomm = record { snmap = λ i → snmeq s t i (eq1 i); sncommute = λ {i} {j} f → eqcomm i j f } - -≡cong2 : { c : Level } { A B C : Set c } { a a' : A } { b b' : B } ( f : A → B → C ) - → a ≡ a' - → b ≡ b' - → f a b ≡ f a' b' -≡cong2 _ refl refl = refl - -snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j) - { s t : snat SObj SMap } - → (( i : OC ) → snmap s i ≡ snmap t i ) - → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j ) - → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j ) - → s ≡ t -snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = ≡cong ( λ x → snat1 SO SM s t eq1 x ) - ( extensionality Sets ( λ i → - ( extensionality Sets ( λ j → - ( extensionality Sets ( λ f → irr2 (λ i → snmeq s t i (eq1 i) )i j f ( eq2s i j f (eq1 i) (λ i → snmeq s t i (eq1 i) ){!!} {!!} (eq2 i j f ) ) {!!} )))))) - where - eq2s1 : { i j : OC } { f : I } → {si : SO i} { sj : SO j } - ( snm : ( i : OC ) → SO i ) → ( si ≡ snm i ) → ( sj ≡ snm j ) → SM {i} {j} f si ≡ sj → SM f ( snm i) ≡ snm j - eq2s1 {i} {j} {f} {si} {sj} snm eq1 eq2 eq3 = begin - SM f ( snm i) - ≡⟨ ≡cong (λ x → SM f x ) (sym eq1) ⟩ - SM f si - ≡⟨ eq3 ⟩ - sj - ≡⟨ eq2 ⟩ - snm j - ∎ where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - eq2s : ( i j : OC ) ( f : I ) → ( snmap s i ≡ snmap t i ) → - ( snm : ( i : OC ) → SO i ) - → snmap s i ≡ snm i → snmap s j ≡ snm j - → SM {i} {j} f ( snmap s i ) ≡ snmap s j → SM f ( snm i) ≡ snm j - eq2s i j f eq1 snm eq2 eq3 eq4 = eq2s1 snm eq2 eq3 eq4 - irr3 : { i j : OC } { f : I } → {snmapsi : SO i } → {snmapsj : SO j } → - ( es et : SM f ( snmapsi ) ≡ snmapsj ) → es ≡ et - irr3 refl refl = refl - irr2 : ( snm : ( i : OC ) → SO i ) ( i j : OC ) (f : I ) → - ( es et : SM f (snm i ) ≡ snm j ) → es ≡ et - irr2 snm i j f es et = irr3 es et - - open import HomReasoning open NTrans 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 (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ + → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) {!!} ) ) Γ Cone C I s Γ = record { TMap = λ i → λ sn → snmap sn i ; isNTrans = record { commute = comm1 } } where comm1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ - Sets [ (λ sn → (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] + Sets [ (λ sn → (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) {!!} )) f ] ] comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin FMap Γ f (snmap sn a ) ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( hom-iso s )) ⟩ @@ -258,7 +204,7 @@ SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) → Limit Sets C Γ SetsLimit { c₂} C I s Γ = record { - a0 = snat (ΓObj s Γ) (ΓMap s Γ) + a0 = snat (ΓObj s Γ) (ΓMap s Γ) {!!} ; t0 = Cone C I s Γ ; isLimit = record { limit = limit1 @@ -267,11 +213,11 @@ } } where a0 : Obj Sets - a0 = snat (ΓObj s Γ) (ΓMap s Γ) - comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) + a0 = snat (ΓObj s Γ) (ΓMap s Γ) {!!} + 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 ) ) - limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) + limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ) {!!} ) limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; sncommute = λ f → comm2 t f } 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 ] @@ -284,13 +230,13 @@ ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning - limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → + limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ) {!!} )} → ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin limit1 a t x ≡⟨⟩ record { snmap = λ i → ( TMap t i ) x ; sncommute = λ f → comm2 t f } - ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) {!!} {!!} {!!} ⟩ + ≡⟨ {!!} (ΓObj s Γ) (ΓMap s Γ) {!!} {!!} {!!} ⟩ record { snmap = λ i → snmap (f x ) i ; sncommute = sncommute (f x ) } ≡⟨⟩ f x @@ -299,10 +245,3 @@ open ≡-Reasoning - - - - - - -