Mercurial > hg > Members > kono > Proof > category
changeset 577:de530823f80b
dead end
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 28 Apr 2017 17:13:29 +0900 |
| parents | 9455768b05f4 |
| children | |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 13 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Thu Apr 27 20:54:16 2017 +0900 +++ b/SetsCompleteness.agda Fri Apr 28 17:13:29 2017 +0900 @@ -199,24 +199,29 @@ 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 + TMap = λ i → λ se → proj (ipp se) 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) a) ] ≈ + commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (ipp se ) a) ] ≈ Sets [ (λ se → proj (ipp 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 (ipp se) a) ]) se ≡⟨⟩ FMap Γ f (proj (ipp se) a) - ≡⟨ ≡cong ( λ g → FMap Γ g (proj (ipp se) a)) (sym ( hom-iso s ) ) ⟩ + ≡⟨ ≡cong ( λ g → FMap Γ g (sproj se a)) (sym ( hom-iso s ) ) ⟩ FMap Γ (hom← s ( hom→ s f)) (proj (ipp se) a) ≡⟨ {!!} ⟩ - ((Sets [ (λ x → ΓMap s Γ (hom→ s f) (proj x a)) o equ ]) (slequ se (hom→ s f))) - + ((Sets [ (λ x → ΓMap s Γ (hom→ s f) (sproj x a)) o equ ]) {!!} ) ≡⟨ fe=ge0 ( slequ se (hom→ s f ) ) ⟩ - {!!} - ≡⟨ {!!} ⟩ - proj (ipp se) b + (Sets [ (λ x → proj x b) o equ ]) (slequ se (hom→ s f) ) + ≡⟨⟩ + proj ( equ (slequ se (hom→ s f) ) ) b + ≡⟨⟩ + proj ( record { proj = ? } ) b + ≡⟨ {!!} ⟩ + proj ( record { proj = sproj se } ) b + ≡⟨⟩ + proj (ipp se) b ≡⟨⟩ (Sets [ (λ se₁ → proj (ipp se) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se ∎ ) where