# HG changeset patch # User Shinji KONO # Date 1493802889 -32400 # Node ID cd65d5c9a54d5eeef69d5468bade2fb64ee1d8da # Parent c9361d23aa3a988eb22747c479728eeea13a0c09 anothter approach diff -r c9361d23aa3a -r cd65d5c9a54d SetsCompleteness.agda --- a/SetsCompleteness.agda Sat Apr 29 22:22:20 2017 +0900 +++ b/SetsCompleteness.agda Wed May 03 18:14:49 2017 +0900 @@ -176,123 +176,41 @@ slid : { c₁ : Level} { I : Set c₁ } → I → I slid x = x -record slim { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j ) +record slim { c₂ } { I OC : Set c₂ } + ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j ) + (lim : Set c₂ ) ( e : lim → sproduct OC sobj ) : Set c₂ where field - slequ : { i j : OC } → ( f : I → I ) → sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) ( λ x → proj x j ) - ipp : {i j : OC } → (f : I → I ) → sproduct OC sobj - ipp {i} {j} f = equ ( slequ {i} {j} f ) - slobj : OC → Set c₂ - slobj i = sobj i - llr : {i j : OC } → ( f : I → I ) → proj ( equ ( slequ {i} {i} slid )) i ≡ proj ( equ ( slequ {i} {j} f )) i - llr {i} {j} f = ? - lll : {i j : OC } → ( f : I → I ) → proj ( equ ( slequ {i} {j} f )) j ≡ proj ( equ ( slequ {j} {j} slid )) j - lll {i} {j} f = {!!} - ll : {x i j i' j' : OC } → ( f f' : I → I ) → proj ( equ ( slequ {i} {j} f )) x ≡ proj ( equ ( slequ {i'} {j'} f' )) x - ll {x} {i} {j} {i'} {j'} f f' = begin - proj ( equ {_} {sproduct OC sobj } {sobj j} ( slequ {i} {j} f )) x - ≡⟨ {!!} ⟩ - proj ( equ {_} {sproduct OC sobj } {sobj j'} ( slequ {i'} {j'} f' )) x - ∎ where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - - -- slmap : {i j : OC } → (f : I → I ) → sobj i → sobj j - -- slmap f = smap f + slequ : (i j : OC) (f : I → I ) → sequ lim (sobj j) (λ x → smap f (proj (e x) i) ) (λ x → proj (e x) j ) open slim -lemma-equ : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) - {x i j i' j' : Obj C } →　 { f f' : I → I } - → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) - → proj (ipp se {i} {j} f) x ≡ proj (ipp se {i'} {j'} f' ) x -lemma-equ C I s Γ {x} {i} {j} {i'} {j'} {f} {f'} se = ll se f f' - - 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 (slim (ΓObj s Γ) (ΓMap s Γ) )) Γ -Cone C I s Γ = record { - TMap = λ i → λ se → proj ( ipp se {i} {i} slid ) i + → ( lim : Set c₁ ) + → ( e : Hom Sets lim (sproduct (Obj C) (ΓObj s Γ)) ) + → NTrans C Sets (K Sets C lim) Γ +Cone C I s Γ lim e = record { + TMap = λ i → λ se → proj ( equ {_} { sproduct (Obj C) (ΓObj s Γ)} {FObj Γ i} + {λ x → proj x i} {λ x → proj x i} (elem (e se ) refl )) i ; isNTrans = record { commute = commute1 } } where - commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se slid ) a) ] ≈ - Sets [ (λ se → proj ( ipp se slid ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ] + cone-equ : (a b : Obj C) (f : Hom C a b) → (se : lim ) → sequ lim (FObj Γ b) (λ x → FMap Γ f (proj (e x) a) ) (λ x → proj (e x) b ) + cone-equ a b f se = slequ ? ? ? ? + commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (equ (elem (e se) refl)) a) ] + ≈ Sets [ (λ se → proj (equ (elem (e se) refl)) b) o FMap (K Sets C lim) f ] ] commute1 {a} {b} {f} = extensionality Sets ( λ se → begin - (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se slid ) a) ]) se + (Sets [ FMap Γ f o (λ se → proj (equ (elem (e se) refl)) a) ]) se ≡⟨⟩ - FMap Γ f (proj ( ipp se {a} {a} slid ) a) - ≡⟨ ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} slid ) a)) (sym ( hom-iso s ) ) ⟩ - FMap Γ (hom← s ( hom→ s f)) (proj ( ipp se {a} {a} slid ) a) - ≡⟨ ≡cong ( λ g → FMap Γ (hom← s ( hom→ s f)) g ) ( lemma-equ C I s Γ {a} se ) ⟩ - FMap Γ (hom← s ( hom→ s f)) (proj ( ipp se {a} {b} (hom→ s f) ) a) - ≡⟨ fe=ge0 ( slequ se (hom→ s f ) ) ⟩ - proj (ipp se {a} {b} ( hom→ s f )) b - ≡⟨ sym ( lemma-equ C I s Γ {b} se ) ⟩ - proj (ipp se {b} {b} (λ x → x)) b + FMap Γ f (proj (e se) a ) + ≡⟨ fe=ge0 (cone-equ a b f se ) ⟩ + proj (e se) b ≡⟨⟩ - (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se + (Sets [ (λ se → proj (equ (elem (e se) refl)) b) o FMap (K Sets C lim) f ]) se ∎ ) 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 Γ -SetsLimit { c₂} C I s Γ = record { - a0 = slim (ΓObj s Γ) (ΓMap s Γ) - ; t0 = Cone C I s Γ - ; isLimit = record { - limit = limit1 - ; t0f=t = λ {a t i } → refl - ; limit-uniqueness = λ {a} {t} {f} → uniquness1 {a} {t} {f} - } - } where - limit2 : (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → {i j : Obj C } →　 ( f : I → I ) - → ( x : a ) → ΓMap s Γ f (TMap t i x) ≡ TMap t j x - limit2 a t f x = ≡cong ( λ g → g x ) ( IsNTrans.commute ( isNTrans t ) ) - limit1 : (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) ) - limit1 a t x = record { - slequ = λ {i} {j} f → elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f x ) - } - uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) )} - → ( i j : Obj C ) → - ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → (f' : I → I ) → (x : a ) - → record { proj = λ i₁ → TMap t i₁ x } ≡ equ (slequ (f x) f') - uniquness2 {a} {t} {f} i j cif=t f' x = begin - record { proj = λ i → TMap t i x } - ≡⟨ ≡cong ( λ g → record { proj = λ i → g i } ) ( extensionality Sets ( λ i → sym ( ≡cong ( λ e → e x ) cif=t ) ) ) ⟩ - record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x } - ≡⟨⟩ - record { proj = λ i → proj (ipp (f x) {i} {i} slid ) i } - ≡⟨ ≡cong ( λ g → record { proj = λ i' → g i' } ) ( extensionality Sets ( λ i'' → lemma-equ C I s Γ {i''} (f x))) ⟩ - record { proj = λ i → proj (ipp (f x) f') i } - ∎ where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - uniquness1 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (Γ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 ] - uniquness1 {a} {t} {f} cif=t = extensionality Sets ( λ x → begin - limit1 a t x - ≡⟨⟩ - record { slequ = λ {i} {j} f' → elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f' x ) } - ≡⟨ ≡cong ( λ e → record { slequ = λ {i} {j} f' → e i j f' x } ) ( - extensionality Sets ( λ i → - extensionality Sets ( λ j → - extensionality Sets ( λ f' → - extensionality Sets ( λ x → - elm-cong ( elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 {a} {t} {f} i j cif=t f' x ) ) - ))) - ) ⟩ - record { slequ = λ {i} {j} f' → slequ (f x ) f' } - ≡⟨⟩ - f x - ∎ ) where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning -