Mercurial > hg > Members > kono > Proof > category
changeset 597:b281e8352158
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 May 2017 08:27:03 +0900 |
| parents | 9367813d3f61 |
| children | 2e3459a9a69f |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 11 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Tue May 23 10:39:18 2017 +0900 +++ b/SetsCompleteness.agda Thu May 25 08:27:03 2017 +0900 @@ -213,7 +213,7 @@ → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) → proj (ipp se {i} {j} f) i ≡ proj (ipp se {i} {i} (slid C I s i) ) i lemma-equ' C I s Γ {i} {j} {f} se = - fe=ge0 ? + fe=ge0 {!!} 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 } @@ -241,25 +241,25 @@ 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} (λ x → x) ) i + TMap = λ i → λ se → proj ( ipp se {i} {i} (slid C I s i) ) 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 (λ x → x) ) a) ] ≈ - Sets [ (λ se → proj ( ipp se (λ x → x) ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ] + commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se (slid C I s a) ) a) ] ≈ + Sets [ (λ se → proj ( ipp se (slid C I s b) ) 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 (λ x → x) ) a) ]) se + (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se (slid C I s a) ) a) ]) se ≡⟨⟩ - FMap Γ f (proj ( ipp se {a} {a} (λ x → x) ) a) - ≡⟨ ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (λ x → x) ) a)) (sym ( hom-iso s ) ) ⟩ - FMap Γ (hom← s ( hom→ s f)) (proj ( ipp se {a} {a} (λ x → x) ) a) + FMap Γ f (proj ( ipp se {a} {a} (slid C I s a) ) a) + ≡⟨ ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (slid C I s a) ) a)) (sym ( hom-iso s ) ) ⟩ + FMap Γ (hom← s ( hom→ s f)) (proj ( ipp se {a} {a} (slid C I s a) ) a) ≡⟨ ≡cong ( λ g → FMap Γ (hom← s ( hom→ s f)) g ) ( lemma-equ C I s Γ 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 Γ se ) ⟩ - proj (ipp se {b} {b} (λ x → x)) b + proj (ipp se {b} {b} (slid C I s b)) b ≡⟨⟩ - (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se + (Sets [ (λ se₁ → proj (ipp se₁ (slid C I s b)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se ∎ ) where open import Relation.Binary.PropositionalEquality open ≡-Reasoning @@ -294,7 +294,7 @@ ≡⟨ ≡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} (λ x → x) ) i } + record { proj = λ i → proj (ipp (f x) {i} {i} (slid C I s i) ) i } ≡⟨ ≡cong ( λ g → record { proj = λ i' → g i' } ) ( extensionality Sets ( λ i'' → lemma-equ C I s Γ (f x))) ⟩ record { proj = λ i → proj (ipp (f x) f') i } ∎ where