# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1488824506 -32400
# Node ID f3d6d0275a0a7e357b8a3f055066645b108d7d1d
# Parent  65ab0da524b8b13756f53430149e62146c3bf230
discrete equality as a dom equality
product from limit done

diff -r 65ab0da524b8 -r f3d6d0275a0a discrete.agda
--- a/discrete.agda	Mon Mar 06 17:16:27 2017 +0900
+++ b/discrete.agda	Tue Mar 07 03:21:46 2017 +0900
@@ -102,6 +102,8 @@
       : Set c₁ where
    field
       discrete : a ≡ b
+   dom : DiscreteObj S
+   dom = a
 
 open DiscreteHom
 
@@ -115,16 +117,15 @@
 
 assoc-* :   {c₁  : Level } { S : Set c₁} {a b c d : DiscreteObj  {c₁}  S}
        {f : (DiscreteHom  c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} →
-       ( f * (g * h)) ≡ ((f * g) * h )
-assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } with discrete f | discrete g | discrete h
-assoc-* {c₁} {S} {a} {.a} {.a} {.a} {f} {g} {h } | refl | refl | refl =  refl
+       dom ( f * (g * h)) ≡ dom ((f * g) * h )
+assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl
 
 DiscreteCat : {c₁ : Level  } →  (S : Set c₁) → Category   c₁   c₁   c₁  
 DiscreteCat   {c₁}  S = record {
     Obj  = DiscreteObj  {c₁} S ;
     Hom = λ a b →   DiscreteHom  {c₁} {S} a b  ;
     _o_ =  λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
-    _≈_ =  λ x y → x  ≡ y ;
+    _≈_ =  λ x y → dom x  ≡ dom y ;
     Id  =  λ{a} → DiscreteId a ;
     isCategory  = record {
             isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
@@ -134,24 +135,16 @@
             associative  = λ{a b c d f g h } → assoc-*  { c₁} {S}  {a} {b} {c} {d} {f} {g} {h}
        }
    }  where
-        identityL :   {a b : DiscreteObj {c₁} S} {f : ( DiscreteHom {c₁}  a b) } →  ((DiscreteId b)  * f)  ≡ f
-        identityL   {a} {b} {f} with discrete f 
-        identityL   {a} {.a} {f} | refl =  let open ≡-Reasoning in begin
-              record { discrete = trans refl refl }
-          ≡⟨⟩
-              record { discrete = refl }
-          ≡⟨ sym (   ≡-cong ( \x -> record { discrete = x } ) {!!} ) ⟩
-              record { discrete = discrete f }
-          ≡⟨⟩
-              f
-          ∎ 
-        identityR :   {A B : DiscreteObj S} {f : ( DiscreteHom {c₁}   A B) } →   ( f * DiscreteId A )  ≡ f
-        identityR   {a} {b} {f} = {!!}
+        identityL :   {a b : DiscreteObj {c₁} S} {f : ( DiscreteHom {c₁}  a b) } →  dom ((DiscreteId b)  * f)  ≡ dom f
+        identityL   {a} {b} {f} = refl
+        identityR :   {A B : DiscreteObj S} {f : ( DiscreteHom {c₁}   A B) } →  dom ( f * DiscreteId A )  ≡ dom f
+        identityR   {a} {b} {f} = refl
         o-resp-≈ :   {A B C : DiscreteObj  S } {f g :  ( DiscreteHom {c₁}   A B)} {h i : ( DiscreteHom B C)} →
-            f  ≡ g → h  ≡ i → ( h * f )  ≡ ( i * g )
-        o-resp-≈  {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
+            dom f  ≡ dom g → dom h  ≡ dom i → dom ( h * f )  ≡ dom ( i * g )
+        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  refl refl = refl
 
 
 
 
 
+
diff -r 65ab0da524b8 -r f3d6d0275a0a limit-to.agda
--- a/limit-to.agda	Mon Mar 06 17:16:27 2017 +0900
+++ b/limit-to.agda	Tue Mar 07 03:21:46 2017 +0900
@@ -238,6 +238,9 @@
       →  ( Γ : Functor (DiscreteCat  S ) A ) → Obj A
 plimit A S comp Γ = limit-c comp Γ
 
+discrete-identity : { c₁ : Level} { S : Set c₁} { a : DiscreteObj {c₁} S } → (f : DiscreteHom a a ) →  (DiscreteCat S)  [ f  ≈  id1 (DiscreteCat S) a ]
+discrete-identity  f =   refl
+
 pnat :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  (S : Set  c₁) (comp : Complete A ( DiscreteCat  S ) ) 
     → (Γ : Functor (DiscreteCat  S ) A )
     →  (q : Obj A )  ( qi : (i : Obj ( DiscreteCat  S)) → Hom A q (FObj Γ i) )
@@ -250,14 +253,18 @@
                 A [ A [ FMap Γ f o qi a ] ≈
                 A [ qi  b o FMap (K A (DiscreteCat  S )q) f ] ]
         commute {a} {b} {f} with discrete f
-        commute {a} {b} {f} | refl =  let open  ≈-Reasoning A in  begin
+        commute {a} {.a} {f} | refl =  let open  ≈-Reasoning A in  begin
                   FMap Γ f o qi a
-                ≈⟨ {!!} ⟩
-                   qi  b 
+                ≈⟨ car ( fcong Γ (discrete-identity f )) ⟩
+                  FMap Γ (id1 (DiscreteCat S) a ) o qi a
+                ≈⟨ car ( IsFunctor.identity (isFunctor Γ) ) ⟩
+                  id1 A (FObj Γ a)  o qi a
+                ≈⟨ idL ⟩
+                   qi  a 
                 ≈↑⟨ idR ⟩
-                   qi  b o id q
+                   qi  a o id q
                 ≈⟨⟩
-                   qi  b o FMap (K A (DiscreteCat S) q) f
+                   qi  a o FMap (K A (DiscreteCat S) q) f
                 ∎
 
 lim-to-product :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set  c₁ )