# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1490862877 -32400
# Node ID 09beac05a0fbd83add28a35e41046b519fd5d68c
# Parent  5d7f8921bac057b50c6f932be9902bd3b45e912a
add iso1

diff -r 5d7f8921bac0 -r 09beac05a0fb SetsCompleteness.agda
--- a/SetsCompleteness.agda	Thu Mar 30 17:08:16 2017 +0900
+++ b/SetsCompleteness.agda	Thu Mar 30 17:34:37 2017 +0900
@@ -152,24 +152,20 @@
      small→ : Obj C → I
      small← : I → Obj C
      small-iso : { x : Obj C  } → Hom C (small← ( small→ x ))  x
-     small-≡   : { x : Obj C  } →  (small← ( small→ x )) ≡ x
      shom→ : {i j : Obj C  } →    Hom C i j →  I → I 
      shom← : {i j : I } →  ( f : I → I ) →  Hom C ( small←  i  ) (  small←  j )
-     shom-iso : {i j : I } →  ( f : Hom C ( small←  i  ) (  small←  j ) ) →  C [ shom← ( shom→ f )  ≈ f ]
+     iso1 :   {a b : Obj C} {f : Hom C a b} →  C [ f o small-iso  ] ≡ C [ small-iso  o shom←  (shom→  f) ]
+
+     -- iso1 should be proved by these ...
+     -- small-≡   : { x : Obj C  } →  (small← ( small→ x )) ≡ x
+     -- shom-iso : {i j : I } →  ( f : Hom C ( small←  i  ) (  small←  j ) ) →  C [ shom← ( shom→ f )  ≈ f ]
+     -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y
 
 open Small 
 
 ≡subst : {c : Level } { x y : Set c } { f :  Set c → Set c } → ( x ≡ y ) → f x ≡ f y 
 ≡subst {c} {x} {.x} {f} refl =  ≡cong ( λ x → f x ) refl
 
-small-hom-iso : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )  { x y : Obj C  }  → 
-    (s : Small C I ) → Hom C (small← s ( small→ s x )) y  ≡ Hom C x y
-small-hom-iso C I {x} {y} s = ≡cong ( λ x → Hom C x y ) ( small-≡ s )
-
-small-hom-iso' : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )  { x y : Obj C  }  → 
-    (s : Small C I ) → Hom C (small← s ( small→ s x )) y  →  Hom C x y
-small-hom-iso' C I {x} {y} s f = {!!}
-
 iid :   {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ }  {I :  Set  c₁} ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) ){i : Obj C } → 
      Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i)
 iid  s Γ = FMap Γ ( small-iso s ) 
@@ -201,8 +197,6 @@
                TMap = λ i →  λ sn →  iid s Γ ( snmap sn (small→ s i )  )
              ; isNTrans = record { commute = comm1 }
       } where
-    iso1 :   {a b : Obj C} {f : Hom C a b} →  C [ f o small-iso s ] ≡ C [ small-iso s o shom← s (shom→ s f) ]
-    iso1 = {!!}
     comm1 :  {a b : Obj C} {f : Hom C a b} →
         Sets [ Sets [ FMap Γ f o (λ sn → iid s Γ (snmap sn (small→ s a))) ] ≈
         Sets [ (λ sn → iid s Γ (snmap sn (small→ s b))) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
@@ -212,7 +206,7 @@
                  ( Sets [ FMap Γ f o  FMap Γ ( small-iso s ) ] ) (snmap sn (small→ s a)) 
              ≡⟨ ≡cong (λ z → z (snmap sn (small→ s a))  ) (sym ( IsFunctor.distr (isFunctor Γ ) ))  ⟩
                  FMap Γ ( C [ f o  (small-iso s) ] ) (snmap sn (small→ s a) )
-             ≡⟨  ≡cong (λ z → ( FMap Γ z ) (snmap sn (small→ s a))) iso1 ⟩
+             ≡⟨  ≡cong (λ z → ( FMap Γ z ) (snmap sn (small→ s a))) (iso1 s) ⟩
                  FMap  Γ ( C [ (small-iso s) o   shom← s (shom→ s f)  ]  )  ( snmap sn ( small→ s a )) 
              ≡⟨  ≡cong (λ z → z (snmap sn (small→ s a))  ) ( IsFunctor.distr (isFunctor Γ ) )  ⟩
                  ( Sets [  FMap  Γ (small-iso s) o  FMap Γ  (shom← s (shom→ s f)) ]  )  ( snmap sn ( small→ s a ))