Mercurial > hg > Members > kono > Proof > category

changeset 799:82a8c1ab4ef5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Apr 2019 11:30:34 +0900
parents 6e6c7ad8ea1c
children bca72fffdc1a
files CCChom.agda deductive.agda discrete.agda limit-to.agda
diffstat 4 files changed, 176 insertions(+), 103 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Tue Apr 23 06:39:24 2019 +0900
+++ b/CCChom.agda	Tue Apr 23 11:30:34 2019 +0900
@@ -586,4 +586,58 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
+module ccc-from-graph ( Atom : Set ) ( homm : Atom → Atom → Set ) where
 
+   open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
+
+   data Objs : Set where
+      ⊤ : Objs
+      atom : Atom → Objs
+      _∧_ : Objs → Objs → Objs
+      _<=_ : Objs → Objs → Objs
+
+   data arrow  : Objs → Objs → Set where
+      hom : {a b : Atom} →  homm a b → arrow (atom a) (atom b)
+      id : (a : Objs ) → arrow a a
+      _・_ : {a b c : Objs } → arrow b c → arrow a b → arrow a c
+      ○ : (a : Objs ) → arrow a ⊤
+      π : {a b : Objs } → arrow ( a ∧ b ) a
+      π' : {a b : Objs } → arrow ( a ∧ b ) b
+      <_,_> : {a b c : Objs } → arrow c a → arrow c b → arrow c (a ∧ b)
+      ε : {a b : Objs } → arrow ((a <= b) ∧ b ) a
+      _* : {a b c : Objs } → arrow (c ∧ b ) a → arrow c ( a <= b )
+
+   open import discrete
+
+   GLCat : Category Level.zero Level.zero Level.zero
+   GLCat = GraphtoCat Objs arrow
+      where open graphtocat
+
+   open graphtocat
+
+   product : {a b c : Obj GLCat} → Hom GLCat c a → Hom GLCat c b → Hom GLCat c ( a ∧ b )
+   product {a} {b} {c} y (connected {_} {_} {d} x g) =   connected (< π , x ・ π'  >) ( product y g )
+   product {a} {b} {c} (connected {_} {_} {d} x g) y =   connected (< x ・ π , π'  >) ( product g y )
+   product {a} {.a} {.a} (id a) (id .a) = mono ( < id a , id a > )
+   product {a} {b} {.a} (id a) (mono x) = mono ( < id a , x > )
+   product {a} {.a₁} {.a₁} (mono x) (id a₁) = mono ( < x , id a₁ > )
+   product {a} {b} {c} (mono x) (mono x₁) = mono ( < x , x₁ > )
+
+   star : {a b c : Obj GLCat} → Hom GLCat (a ∧ b) c → Hom GLCat a (c <= b)
+   star {a} {b} {.(a ∧ b)} (id .(a ∧ b)) = mono ( id (a ∧ b ) * )
+   star {a} {b} {c} (mono x) = mono ( x * )
+   star {a} {b} {c} (connected {_} {d} {_} x y) = connected (  ( x  ・  ε  ) * ) ( star y )
+
+--   GL :  PositiveLogic GLCat
+--   GL = record {
+--         ⊤ = ⊤
+--       ; ○ = λ f → mono (○ f)
+--       ; _∧_ =  _∧_
+--       ; <_,_> = λ f g → product f g
+--       ; π =  mono π
+--       ; π' = mono π'
+--       ; _<=_ = _<=_
+--       ; _* =  star
+--       ; ε = mono ε
+--    }
+
--- a/deductive.agda	Tue Apr 23 06:39:24 2019 +0900
+++ b/deductive.agda	Tue Apr 23 11:30:34 2019 +0900
@@ -18,63 +18,6 @@
          _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
          ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
 
-module ccc-from-graph ( Atom : Set ) ( Hom : Atom → Atom → Set ) where
-
-   open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
-
-   data Objs : Set where
-      ⊤ : Objs 
-      atom : Atom → Objs
-      _∧_ : Objs → Objs → Objs
-      _<=_ : Objs → Objs → Objs
-   
-   data Arrow  : Objs → Objs → Set where
-      hom : (a b : Atom) →  Hom a b → Arrow (atom a) (atom b)
-      id : (a : Objs ) → Arrow a a
-      _・_ : {a b c : Objs } → Arrow b c → Arrow a b → Arrow a c 
-      ○ : (a : Objs ) → Arrow a ⊤
-      π : {a b : Objs } → Arrow ( a ∧ b ) a
-      π' : {a b : Objs } → Arrow ( a ∧ b ) b
-      <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b) 
-      ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
-      _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
-
-   record GraphCat : Set where
-     field
-        identityL : {a b : Objs} {f : Arrow a b } → (id b ・ f) ≡ f
-        identityR : {a b : Objs} {f : Arrow a b } → (f ・ id a) ≡ f
-        resp : {a b c : Objs} {f g : Arrow a b } {h i : Arrow b c } → f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
-        associative : {a b c d : Objs} {f : Arrow c d }{g : Arrow b c }{h : Arrow a b } → (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
-
-
-   GLCat :  GraphCat → Category Level.zero Level.zero Level.zero 
-   GLCat gc  = record {
-    Obj  = Objs ;
-    Hom = λ a b →   Arrow a b  ;
-    _o_ =  _・_ ; -- λ{a} {b} {c} x y →    ; -- _×_ {c₁ } { c₂} {a} {b} {c} x y ;
-    _≈_ =  λ x y → x  ≡ y ;
-    Id  =  λ{a} → id a ;
-    isCategory  = record {
-            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } 
-          ; identityL  = λ{a b f} → GraphCat.identityL gc 
-          ; identityR  = λ{a b f} → GraphCat.identityR gc 
-          ; o-resp-≈  = λ {a b c f g h i} f=g h=i →  GraphCat.resp gc f=g h=i
-          ; associative  = λ{a b c d f g h } → GraphCat.associative gc
-       }
-    }  
-      
-   GL :  (gc : GraphCat ) → PositiveLogic (GLCat gc )
-   GL _ = record {
-         ⊤ = ⊤
-       ; ○ = ○
-       ; _∧_ =  _∧_
-       ; <_,_> = <_,_>
-       ; π = π
-       ; π' = π'
-       ; _<=_ = _<=_
-       ; _* = _*
-       ; ε = ε
-     }
 
 module deduction-theorem (  L :  PositiveLogic A ) where
 
--- a/discrete.agda	Tue Apr 23 06:39:24 2019 +0900
+++ b/discrete.agda	Tue Apr 23 11:30:34 2019 +0900
@@ -7,7 +7,73 @@
 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym )
 
 
-data  TwoObject {c₁ : Level}  : Set c₁ where
+
+module graphtocat where
+
+  data Arrow { obj : Set } { hom : obj → obj → Set } : ( a b : obj ) → Set where
+    id : ( a : obj ) → Arrow a a
+    mono : { a b : obj } → hom a b → Arrow a b
+    connected : {a b : obj } → {c : obj} → hom b c →  Arrow {obj} {hom} a b → Arrow a c
+
+  _+_ : { obj : Set } { hom : obj → obj → Set } {a b c : obj   } (f : (Arrow {obj} {hom} b c )) → (g : (Arrow {obj} {hom} a b )) → Arrow {obj} {hom} a c
+  id a + id .a = id a
+  id b + mono x = mono x
+  id a + connected x y = connected x y
+  mono x + id a = mono x
+  mono x + mono y = connected x (mono y)
+  mono x + connected y z = connected x ( connected y z )
+  connected x y + z = connected x ( y + z )
+
+  assoc-+ : { obj : Set } { hom : obj → obj → Set }  {a b c d : obj   }
+       (f : (Arrow  {obj} {hom} c d )) → (g : (Arrow {obj} {hom} b c )) → (h : (Arrow {obj} {hom} a b )) →
+       ( f + (g + h)) ≡  ((f + g) + h )
+  assoc-+ (id a) (id .a) (id .a) = refl
+  assoc-+ (id a) (id .a) (mono x) = refl
+  assoc-+ (id a) (id .a) (connected h h₁) = refl
+  assoc-+ (id a) (mono x) (id a₁) = refl
+  assoc-+ (id a) (mono x) (mono x₁) = refl
+  assoc-+ (id a) (mono x) (connected h h₁) = refl
+  assoc-+ (id a) (connected g h) _ = refl
+  assoc-+ (mono x) (id a) (id .a) = refl
+  assoc-+ (mono x) (id a) (mono x₁) = refl
+  assoc-+ (mono x) (id a) (connected h h₁) = refl
+  assoc-+ (mono x) (mono x₁) (id a) = refl
+  assoc-+ (mono x) (mono x₁) (mono x₂) = refl
+  assoc-+ (mono x) (mono x₁) (connected h h₁) = refl
+  assoc-+ (mono x) (connected g g₁) _ = refl
+  assoc-+ (connected f g) (x) (y) = cong (λ k → connected f k) (assoc-+ g x y )
+
+  open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
+
+  GraphtoCat : ( obj : Set ) ( hom : obj → obj → Set ) →  Category  Level.zero Level.zero Level.zero   
+  GraphtoCat  obj hom  = record {
+            Obj  = obj ;
+            Hom = λ a b →   Arrow a b  ;
+            _o_ =  λ{a} {b} {c} x y → _+_  x y ;
+            _≈_ =  λ x y → x  ≡ y ;
+            Id  =  λ{a} → id a ;
+            isCategory  = record {
+                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
+                    identityL  = λ{a b f} → identityL    {a} {b} {f} ;
+                    identityR  = λ{a b f} → identityR    {a} {b} {f} ;
+                    o-resp-≈  = λ{a b c f g h i} →  o-resp-≈     {a} {b} {c} {f} {g} {h} {i} ;
+                    associative  = λ{a b c d f g h } → assoc-+  f g h
+               }
+           }  where
+                identityL :   {A B : obj } {f : ( Arrow    A B) } →  ((id B)  + f)  ≡ f
+                identityL {_} {_} {id a} = refl
+                identityL {_} {_} {mono x} = refl
+                identityL {_} {_} {connected x f} = refl
+                identityR :   {A B : obj } {f : ( Arrow {obj} {hom}  A B) } →   ( f + id A )  ≡ f
+                identityR {_} {_} {id a} = refl
+                identityR {_} {_} {mono x} = refl
+                identityR {_} {_} {connected x f} =  cong (λ k → connected x k) ( identityR {_} {_} {f} )
+                o-resp-≈ :   {A B C : obj   } {f g :  ( Arrow    A B)} {h i : ( Arrow B C)} →
+                    f  ≡ g → h  ≡ i → ( h + f )  ≡ ( i + g )
+                o-resp-≈     {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
+
+
+data  TwoObject   : Set  where
    t0 : TwoObject
    t1 : TwoObject
 
@@ -22,20 +88,24 @@
 --
 --     missing arrows are constrainted by TwoHom data
 
-data TwoHom {c₁ c₂ : Level } : TwoObject {c₁}  → TwoObject {c₁} → Set c₂ where
+data TwoHom  : TwoObject   → TwoObject  → Set  where
    id-t0 :    TwoHom t0 t0
    id-t1 :    TwoHom t1 t1
    arrow-f :  TwoHom t0 t1
    arrow-g :  TwoHom t0 t1
 
+TwoCat' : Category  Level.zero Level.zero Level.zero
+TwoCat'  = GraphtoCat TwoObject TwoHom 
+   where open graphtocat
 
-_×_ :  ∀ {c₁  c₂}  → {a b c : TwoObject {c₁}} →  TwoHom {c₁} {c₂} b c  →  TwoHom {c₁} {c₂} a b   →  TwoHom {c₁} {c₂} a c 
-_×_ {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-f  = arrow-f 
-_×_ {_}  {_}  {t0} {t1} {t1}  id-t1   arrow-g  = arrow-g 
-_×_ {_}  {_}  {t1} {t1} {t1}  id-t1   id-t1    = id-t1 
-_×_ {_}  {_}  {t0} {t0} {t1}  arrow-f id-t0    = arrow-f 
-_×_ {_}  {_}  {t0} {t0} {t1}  arrow-g id-t0    = arrow-g 
-_×_ {_}  {_}  {t0} {t0} {t0}  id-t0   id-t0    = id-t0 
+_×_ :  {a b c : TwoObject } →  TwoHom   b c  →  TwoHom   a b   →  TwoHom   a c 
+_×_ {t0} {t1} {t1}  id-t1   arrow-f  = arrow-f 
+_×_ {t0} {t1} {t1}  id-t1   arrow-g  = arrow-g 
+_×_ {t1} {t1} {t1}  id-t1   id-t1    = id-t1 
+_×_ {t0} {t0} {t1}  arrow-f id-t0    = arrow-f 
+_×_ {t0} {t0} {t1}  arrow-g id-t0    = arrow-g 
+_×_ {t0} {t0} {t0}  id-t0   id-t0    = id-t0 
+
 
 open TwoHom
 
@@ -44,56 +114,62 @@
 --
 --   It can be proved without TwoHom constraints
 
-assoc-× :   {c₁  c₂ : Level } {a b c d : TwoObject  {c₁} }
-       {f : (TwoHom {c₁}  {c₂ } c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
+assoc-× :    {a b c d : TwoObject   }
+       {f : (TwoHom    c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} →
        ( f × (g × h)) ≡ ((f × g) × h )
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0   }{ id-t0   }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0   }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0   }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1   }{ arrow-f }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1   }{ arrow-g }{ id-t0   } = refl
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-f } = refl
-assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-g } = refl
-assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ id-t1   } = refl
+assoc-×   {t0} {t0} {t0} {t0} { id-t0   }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t0} {t1} { arrow-f }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t0} {t1} { arrow-g }{ id-t0   }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t1} {t1} { id-t1   }{ arrow-f }{ id-t0   } = refl
+assoc-×   {t0} {t0} {t1} {t1} { id-t1   }{ arrow-g }{ id-t0   } = refl
+assoc-×   {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-f } = refl
+assoc-×   {t0} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ arrow-g } = refl
+assoc-×   {t1} {t1} {t1} {t1} { id-t1   }{ id-t1   }{ id-t1   } = refl
 
-TwoId :  {c₁  c₂ : Level } (a : TwoObject  {c₁} ) →  (TwoHom {c₁}  {c₂ } a a )
-TwoId {_} {_} t0 = id-t0 
-TwoId {_} {_} t1 = id-t1 
+TwoId :   (a : TwoObject   ) →  (TwoHom    a a )
+TwoId  t0 = id-t0 
+TwoId   t1 = id-t1 
 
 open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
 
-TwoCat : {c₁ c₂ : Level  } →  Category   c₁  c₂  c₂
-TwoCat   {c₁}  {c₂} = record {
+TwoCat :  Category  Level.zero Level.zero Level.zero   
+TwoCat      = record {
     Obj  = TwoObject ;
     Hom = λ a b →   TwoHom a b  ;
-    _o_ =  λ{a} {b} {c} x y → _×_ {c₁ } { c₂} {a} {b} {c} x y ;
     _≈_ =  λ x y → x  ≡ y ;
     Id  =  λ{a} → TwoId a ;
     isCategory  = record {
             isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
-            identityL  = λ{a b f} → identityL {c₁}  {c₂ } {a} {b} {f} ;
-            identityR  = λ{a b f} → identityR {c₁}  {c₂ } {a} {b} {f} ;
-            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈  {c₁}  {c₂ } {a} {b} {c} {f} {g} {h} {i} ;
-            associative  = λ{a b c d f g h } → assoc-×   {c₁}  {c₂} {a} {b} {c} {d} {f} {g} {h}
+            identityL  = λ{a b f} → identityL    {a} {b} {f} ;
+            identityR  = λ{a b f} → identityR    {a} {b} {f} ;
+            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈     {a} {b} {c} {f} {g} {h} {i} ;
+            associative  = λ{a b c d f g h } → assoc-×      {a} {b} {c} {d} {f} {g} {h}
        }
    }  where
-        identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  ((TwoId B)  × f)  ≡ f
-        identityL  {c₁}  {c₂}  {t1} {t1} { id-t1 } = refl
-        identityL  {c₁}  {c₂}  {t0} {t0} { id-t0 } = refl
-        identityL  {c₁}  {c₂}  {t0} {t1} { arrow-f } = refl
-        identityL  {c₁}  {c₂}  {t0} {t1} { arrow-g } = refl
-        identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   ( f × TwoId A )  ≡ f
-        identityR  {c₁}  {c₂}  {t1} {t1} { id-t1  } = refl
-        identityR  {c₁}  {c₂}  {t0} {t0} { id-t0 } = refl
-        identityR  {c₁}  {c₂}  {t0} {t1} { arrow-f } = refl
-        identityR  {c₁}  {c₂}  {t0} {t1} { arrow-g } = refl
-        o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
+        identityL :   {A B : TwoObject } {f : ( TwoHom    A B) } →  ((TwoId B)  × f)  ≡ f
+        identityL      {t1} {t1} { id-t1 } = refl
+        identityL      {t0} {t0} { id-t0 } = refl
+        identityL      {t0} {t1} { arrow-f } = refl
+        identityL      {t0} {t1} { arrow-g } = refl
+        identityR :   {A B : TwoObject } {f : ( TwoHom    A B) } →   ( f × TwoId A )  ≡ f
+        identityR      {t1} {t1} { id-t1  } = refl
+        identityR      {t0} {t0} { id-t0 } = refl
+        identityR      {t0} {t1} { arrow-f } = refl
+        identityR      {t0} {t1} { arrow-g } = refl
+        o-resp-≈ :   {A B C : TwoObject   } {f g :  ( TwoHom    A B)} {h i : ( TwoHom B C)} →
             f  ≡ g → h  ≡ i → ( h × f )  ≡ ( i × g )
-        o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
+        o-resp-≈     {a} {b} {c} {f} {.f} {h} {.h}  refl refl = refl
 
 
 -- Category with no arrow but identity
 
+
+open import Data.Empty
+
+DiscreteCat' : (S : Set) → Category  Level.zero Level.zero Level.zero
+DiscreteCat'  S = GraphtoCat S ( λ _ _ →  ⊥  )
+   where open graphtocat 
+
 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S) 
       : Set c₁ where
    field
--- a/limit-to.agda	Tue Apr 23 06:39:24 2019 +0900
+++ b/limit-to.agda	Tue Apr 23 11:30:34 2019 +0900
@@ -41,7 +41,7 @@
 
 -- Functor Γ : TwoCat → A
 
-IndexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat  {c₁} {c₂}) A
+IndexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat ) A
 IndexFunctor  {c₁} {c₂} {ℓ} A a b f g = record {
          FObj = λ a → fobj a
        ; FMap = λ {a} {b} f → fmap {a} {b} f
@@ -51,7 +51,7 @@
              ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
        }
       } where
-          T = TwoCat   {c₁} {c₂}
+          T = TwoCat 
           fobj :  Obj T → Obj A
           fobj t0 = a
           fobj t1 = b
@@ -119,7 +119,7 @@
         commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh
     }
  } where
-         I = TwoCat  {c₁} {c₂}
+         I = TwoCat 
          Γ : Functor I A
          Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
          nmap :  (x : Obj I ) ( d : Obj (A)  ) (h : Hom A d a ) → Hom A (FObj (K I A d) x) (FObj Γ x)
@@ -169,7 +169,7 @@
         ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
         ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
      } where
-         I : Category  c₁ c₂ c₂
+         I : Category Level.zero Level.zero Level.zero   
          I = TwoCat
          Γ : Functor I A
          Γ = IndexFunctor A a b f g
@@ -185,7 +185,7 @@
                 ≈⟨⟩
                     FMap  Γ arrow-f o TMap (Limit.t0 lim) discrete.t0
                 ≈⟨  IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-f} ⟩ 
-                    TMap (Limit.t0 lim) discrete.t1 o FMap (K (TwoCat {c₁} {c₂} ) A (a0 lim)) id-t0
+                    TMap (Limit.t0 lim) discrete.t1 o FMap (K (TwoCat   ) A (a0 lim)) id-t0
                 ≈↑⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-g} ⟩ 
                     FMap  Γ arrow-g o TMap (Limit.t0 lim) discrete.t0
                 ≈⟨⟩