Mercurial > hg > Members > kono > Proof > category
changeset 581:41ef69cd5871
another approach
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 02 May 2017 00:31:00 +0900 |
| parents | c9361d23aa3a |
| children | 676f1fd4a46b |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 9 insertions(+), 112 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Sat Apr 29 22:22:20 2017 +0900 +++ b/SetsCompleteness.agda Tue May 02 00:31:00 2017 +0900 @@ -176,123 +176,20 @@ 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 ) + ( sprod : Set c₂ ) + ( sproj : sprod → (i : OC ) → sobj i ) + ( sprod1 : { q : Set c₂ } → ( qi : (i : OC ) → q → sobj i ) → q → sprod ) : 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 sprod (sobj j) ( λ x → smap f ( sproj x i ) ) ( λ x → sproj x j ) + ipp : {i j : OC } → (f : I → I ) → sproduct OC sobj + ipp {i} {j} f = record { proj = λ i → sproj (equ (slequ {i} {j} f)) i } 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 Γ) ) + → (se : slim (ΓObj s Γ) (ΓMap s Γ) (sproduct (Obj C) (ΓObj s Γ)) (λ p i → proj p i ) ( λ qi x → record { proj = λ i → (qi i) x } ) ) → 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 - ; 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 ] ] - commute1 {a} {b} {f} = extensionality Sets ( λ se → begin - (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se slid ) 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 - ≡⟨⟩ - (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) 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 - +lemma-equ C I s Γ {x} {i} {j} {i'} {j'} {f} {f'} se = ?