# HG changeset patch # User Shinji KONO # Date 1495364038 -32400 # Node ID a158ebb391f2eed5202f0b446aa89339d17a0638 # Parent 0448a74c0a0389cd3eafa03bed0312632b496906 fix diff -r 0448a74c0a03 -r a158ebb391f2 SetsCompleteness.agda --- a/SetsCompleteness.agda Mon May 15 18:09:33 2017 +0900 +++ b/SetsCompleteness.agda Sun May 21 19:53:58 2017 +0900 @@ -180,134 +180,36 @@ ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j ) : 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 ) + slproj : ( i : OC ) → sobj i + slequ : (i j : OC) (f : I → I ) → sequ OC (sobj j) (λ x → smap f (slproj i) ) (λ x → slproj j ) + slprod : sproduct OC sobj + slprod = record { proj = slproj } slmap : { i j : OC } → (f : I → I ) → sobj i → sobj j slmap f x = smap f x open slim -slprod : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) - {i : Obj C } → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) → sproduct (Obj C) (ΓObj s Γ) -slprod C I s Γ {i} se = equ ( slequ se i i (slid C I s i ) ) - open import HomReasoning open NTrans -llid : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) - → ( x : FObj Γ a ) - → slmap se (slid C I s a ) x ≡ x -llid C I s Γ a b f se x = begin - slmap se (slid C I s a) x - ≡⟨⟩ - FMap Γ (hom← s (slid C I s a)) x - ≡⟨ ≡cong ( λ g → FMap Γ g x ) (hom-iso s ) ⟩ - FMap Γ (id1 C a) x - ≡⟨ ≡cong ( λ g → g x ) ( IsFunctor.identity (isFunctor Γ ) ) ⟩ - x - ∎ where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - -lldistr : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → (a b c : Obj C) (f g : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) - → ( x : FObj Γ a ) - → slmap se {a} {c} ( λ y → f ( g y )) x ≡ slmap se {b} {c} f ( ( slmap se {a} {b} g ) x ) -lldistr C I s Γ a b c f g se x = begin - slmap se {a} {c} ( λ y → f ( g y )) x - ≡⟨⟩ - FMap Γ (hom← s (λ y → f (g y))) x - ≡⟨ ? ⟩ - FMap Γ (hom← s (λ y → f ( hom→ s ( hom← s g) y ))) x - ≡⟨ {!!} ⟩ - FMap Γ (C [ hom← s f o hom← s g ]) x - ≡⟨ ≡cong ( λ g → g x ) ( IsFunctor.distr (isFunctor Γ ) ) ⟩ - (Sets [ FMap Γ (hom← s f) o FMap Γ (hom← s g ) ]) x - ≡⟨⟩ - slmap se {b} {c} f ( ( slmap se {a} {b} g ) x ) - ∎ where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - - -lemma-equ : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) - {i j i' j' : Obj C } →　 { f f' : I → I } - → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) - → proj (equ (slequ se i j f)) i ≡ proj (equ (slequ se i' j' f' )) i -lemma-equ C I s Γ {i} {j} {i'} {j'} {f} {f'} se = ≡cong ( λ p -> proj p i ) ( begin - equ (slequ se i j f ) - ≡⟨⟩ - record { proj = λ x → proj (equ (slequ se i j f)) x } - ≡⟨ ≡cong ( λ p → record { proj = proj p i }) ( ≡cong ( λ QIX → record { proj = QIX } ) ( - extensionality Sets ( λ x → ≡cong ( λ qi →　qi x ) refl - ) )) ⟩ - record { proj = λ x → proj (equ (slequ se i' j' f')) x } - ≡⟨⟩ - equ (slequ se i' j' f' ) +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₁} C I s Γ = record { + TMap = λ i → λ se → proj ( slprod se ) i + ; isNTrans = record { commute = commute1 } + } where + commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (slprod se) a) ] ≈ + Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ] + commute1 {a} {b} {f} = extensionality Sets ( λ se → begin + FMap Γ f (proj (slprod se ) a ) + ≡⟨ ≡cong ( λ g → FMap Γ g (proj (slprod se) a)) (sym ( hom-iso s ) ) ⟩ + FMap Γ (hom← s ( hom→ s f)) (proj (slprod se) a) + ≡⟨ fe=ge0 (slequ se a b ( hom→ s f) ) ⟩ + proj (slprod se) b ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning -llcomm : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) - → proj ( equ ( slequ se a b f)) a ≡ slmap se f (proj (slprod C I s Γ {a} se ) a ) -llcomm C I s Γ a b f se = begin - proj ( equ ( slequ se a b f)) a - ≡⟨ {!!} ⟩ - slmap se f (proj (equ ( slequ se a a (slid C I s a))) a ) - ≡⟨⟩ - slmap se f (proj (slprod C I s Γ {a} se ) a ) - ∎ where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - - -lla : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) - → proj ( equ ( slequ se a b f)) a ≡ proj (slprod C I s Γ {a} se ) a -lla C I s Γ a b f se = begin - proj ( equ ( slequ se a b f)) a - ≡⟨ {!!} ⟩ - proj ( equ ( slequ se a a (slid C I s a))) a - ∎ where - open import Relation.Binary.PropositionalEquality - open ≡-Reasoning - - -llb : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) - → (a b : Obj C) (f : I → I ) → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) - → proj ( equ ( slequ se a b f)) b ≡ proj (slprod C I s Γ {b} se ) b -llb C I s Γ a b f se = {!!} - - -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₁} C I s Γ = record { - TMap = λ i → λ se → proj (slprod C I s Γ {i} se ) i - ; isNTrans = record { commute = commute1 } - } where - commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (slprod C I s Γ {a} se ) a) ] - ≈ Sets [ (λ se → proj (slprod C I s Γ {b} se ) 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 (slprod C I s Γ {a} se ) a) ]) se - ≡⟨⟩ - FMap Γ f (proj (slprod C I s Γ {a} se ) a ) - ≡⟨ ≡cong ( λ g → FMap Γ g (proj (slprod C I s Γ {a} se ) a)) (sym ( hom-iso s ) ) ⟩ - FMap Γ (hom← s ( hom→ s f)) (proj (slprod C I s Γ {a} se ) a) - ≡⟨ ≡cong ( λ g → FMap Γ (hom← s ( hom→ s f)) g ) (sym (lla C I s Γ a b ( hom→ s f) se ) ) ⟩ - FMap Γ (hom← s ( hom→ s f)) (proj (equ ( slequ se a b ( hom→ s f))) a) - ≡⟨ fe=ge0 (slequ se a b ( hom→ s f) ) ⟩ - proj (equ (slequ se a b ( hom→ s f))) b - ≡⟨ llb C I s Γ a b ( hom→ s f) se ⟩ - proj (slprod C I s Γ {b} se ) b - ≡⟨⟩ - (Sets [ (λ se → proj (slprod C I s Γ {b} se ) 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 { @@ -315,11 +217,28 @@ ; t0 = Cone C I s Γ ; isLimit = record { limit = limit1 - ; t0f=t = λ {a t i } → {!!} - ; limit-uniqueness = λ {a t i } → {!!} + ; t0f=t = λ {a t i } → refl + ; limit-uniqueness = λ {a t f } → limit-uniqueness {a} {t} {f} } } where - -- ( e : Obj C → sproduct (Obj C) sobj ) - -- sequ (Obj C) (ΓObj s Γ j) (λ x₁ → ΓMap s Γ f (proj (e x₁) i)) (λ x₁ → proj (e x₁) j) limit1 : (a : Obj Sets) → 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 }) ( ≡cong ( λ g → g x) (IsNTrans.commute (isNTrans t ))) } + limit1 a t = λ x → record { + slequ = λ i j f → elem {!!} ( ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )) + ; slproj = λ i → ( TMap t i ) x + } + limit-uniqueness : {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 ] + limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin + limit1 a t x + ≡⟨ {!!} ⟩ + f x + ∎ ) where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning + + + + + + + +