# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556435022 -32400
# Node ID b27b231c2d5465cb3aa46e268d68f18100110c56
# Parent  bc244fc604c8a1791167dc5294cb7eb3fdb3a23b
one

diff -r bc244fc604c8 -r b27b231c2d54 CCCGraph.agda
--- a/CCCGraph.agda	Sun Apr 28 13:02:36 2019 +0900
+++ b/CCCGraph.agda	Sun Apr 28 16:03:42 2019 +0900
@@ -117,6 +117,55 @@
       <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b)
       _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )
 
+   data one {v : Level} {S : Set v} : Set v where
+             elm : (x : S ) → one 
+
+   iso→ : {v : Level} {S : Set v} → one → S
+   iso→ (elm x) = x
+
+   data iso← {v : Level} {S : Set v} : (one {v} {S} ) → S → Set v where
+       elmeq : {x : S} →  iso←  ( elm x ) x
+
+   iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso← x a → iso→ x ≡ a
+   iso-left (elm x) .x elmeq = refl
+
+   iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x ) 
+   iso-right (elm x) = elmeq
+
+--   record one {v : Level} {S : Set v} : Set (suc v) where
+--      field
+--         elm : S
+--
+--   iso→ : {v : Level} {S : Set v} → one {v} {S} → One {Level.zero} → S
+--   iso→ x OneObj = one.elm x
+--   iso← : {v : Level} {S : Set v} → one {v} {S} → S → One {Level.zero}
+--   iso← x y = OneObj
+--
+--   iso-left : {v : Level} {S : Set v} → (x : one {v} {S} ) → (a : S ) → iso→ x ( iso← x a ) ≡ a
+--   iso-left x a =  {!!}
+--
+--   iso-right : {v : Level} {S : Set v} → (x : one {v} {S} ) → iso← x ( iso→ x OneObj ) ≡ OneObj
+--   iso-right x =  refl
+
+   record one' {v : Level} {S : Set v} : Set (suc v) where
+     field
+        elm' : S
+        iso→' : One {Level.zero} → S
+        iso←' : S → One {Level.zero}
+        iso-left' : iso→' ( iso←' elm' ) ≡ elm'
+        iso-right' : iso←' ( iso→' OneObj ) ≡ OneObj
+
+   tmp : {v : Level} {S : Set v} → one {v} {S}  → one' {v} {S}
+   tmp x = record {
+         elm' = iso→ x
+       ; iso→' = λ _ → iso→ x
+       ; iso←' = λ _ → OneObj
+       ; iso-left' = refl
+       ; iso-right' = refl
+     }
+     
+
+
    record SM {v : Level} : Set (suc v)  where
       field
         graph : Graph  {v}