### changeset 819:b27b231c2d54

one
author Shinji KONO Sun, 28 Apr 2019 16:03:42 +0900 bc244fc604c8 658daaa74df3 CCCGraph.agda 1 files changed, 49 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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}