Mercurial > hg > Members > kono > Proof > category

changeset 528:531547cf3b92

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Mar 2017 18:18:38 +0900
parents beac7b0786cb
children 18aea9cb0fdb
files SetsCompleteness.agda
diffstat 1 files changed, 13 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Mar 28 18:10:15 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 28 18:18:38 2017 +0900
@@ -6,7 +6,6 @@
 module SetsCompleteness where
 
 
-open import HomReasoning
 open import cat-utility
 open import Relation.Binary.Core
 open import Function
@@ -144,7 +143,6 @@
 
 
 open Functor
-open NTrans
 
 record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
@@ -198,12 +196,18 @@
           proj i prod = iid (  pi1 prod ( small→ s i )  )
           comm1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o Sets [ proj a o e ] ] ≈
                 Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ]
-          comm1 {a} {b} {f} = extensionality Sets  ( λ  x → begin
-                 ? 
-             ≡⟨ {!!}  ⟩
-                {!!}
-             ∎ )  where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+          comm1 {a} {b} {f} = begin
+                  Sets [ FMap Γ f o Sets [ proj a o e ]  ]
+              ≈⟨ assoc ⟩
+                  Sets [ Sets [ FMap Γ f o  proj a ] o e   ]
+              ≈⟨ {!!}  ⟩
+                  Sets [ proj b o e ] 
+              ≈↑⟨ idR  ⟩
+                  Sets [ Sets [ proj b o e ] o id1 Sets a0 ]
+              ≈⟨⟩
+                  Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] 
+             ∎   where
+                  open import HomReasoning
+                  open  ≈-Reasoning Sets