Mercurial > hg > Members > kono > Proof > category
diff SetsCompleteness.agda @ 589:6584db867bd0
dead end
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 14 May 2017 09:55:10 +0900 |
| parents | 11b5eeb4a9e7 |
| children | 2c5d8c3c9086 |
line wrap: on
line diff
--- a/SetsCompleteness.agda Fri May 12 13:45:31 2017 +0900 +++ b/SetsCompleteness.agda Sun May 14 09:55:10 2017 +0900 @@ -181,7 +181,8 @@ : 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 ) - slprod : sproduct OC sobj + slprod : {i : OC } → sproduct OC sobj + slprod {i} = equ ( slequ i i slid ) open slim @@ -190,9 +191,14 @@ cone-equ : { 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 Γ) ) - → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x → FMap Γ (hom← s f) (proj (slprod x) a) ) (λ x → proj (slprod x) b ) + → sequ (slim (ΓObj s Γ) (ΓMap s Γ)) (FObj Γ b) (λ x → FMap Γ (hom← s f) (proj (slprod x {a}) a) ) (λ x → proj (slprod x {b}) b ) cone-equ C I s Γ a b f se = elem se {!!} -- (( fe=ge0 (slequ se a b f )) ) +cone-equ' : { 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 Γ) ) + → FMap Γ (hom← s f) (proj (equ (slequ se a b f )) a) ≡ proj (equ (slequ se a b f)) b +cone-equ' C I s Γ a b f se = fe=ge0 (slequ se a b 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 I s Γ = record { @@ -203,15 +209,15 @@ 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 - (Sets [ FMap Γ f o (λ se → proj (slprod se) a) ]) se + (Sets [ FMap Γ f o (λ se → proj (slprod se {a}) a) ]) se ≡⟨⟩ 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) + FMap Γ (hom← s ( hom→ s f)) (proj (slprod se {a}) a) ≡⟨ fe=ge0 (cone-equ C I s Γ a b ( hom→ s f) se ) ⟩ - proj (slprod se) b + proj (slprod se {b}) b ≡⟨⟩ - (Sets [ (λ se → proj (slprod se) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se + (Sets [ (λ se → proj (slprod se {b}) b) o FMap (K Sets C ( slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning @@ -237,6 +243,5 @@ ≈⟨ car (nat t) ⟩ (λ x₁ → proj x₁ j) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) ∎ - ) x - ; slprod = record { proj = λ i → TMap t i x } } + ) x } where open ≈-Reasoning (Sets { c₂})