# HG changeset patch # User Shinji KONO # Date 1589289969 -32400 # Node ID f19425b54abaac3d07e24202002c4721036220a6 # Parent 98b5fafb1efba105a601ad7314f8a319fe542bb2 introduce detailed level on CCCGraph diff -r 98b5fafb1efb -r f19425b54aba CCCGraph.agda --- a/CCCGraph.agda Tue May 12 15:56:48 2020 +0900 +++ b/CCCGraph.agda Tue May 12 22:26:09 2020 +0900 @@ -1,6 +1,6 @@ open import Level open import Category -module CCCgraph (c₁ : Level ) where +module CCCgraph where open import HomReasoning open import cat-utility @@ -21,13 +21,10 @@ postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ -c₂ = suc c₁ -c₃ = suc c₂ - data One {c : Level } : Set c where OneObj : One -- () in Haskell ( or any one object set ) -sets : CCC (Sets {c₁}) +sets : {c : Level } → CCC (Sets {c}) sets = record { １ = One ; ○ = λ _ → λ _ → OneObj @@ -97,20 +94,21 @@ Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ] *-cong refl = refl + open import graph -module ccc-from-graph (G : Graph {c₂} {c₁} ) where +module ccc-from-graph {c₁ c₂ : Level } (G : Graph {c₁} {c₂}) where open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] ) open Graph - data Objs : Set c₂ where + data Objs : Set (suc c₁) where atom : (vertex G) → Objs ⊤ : Objs _∧_ : Objs → Objs → Objs _<=_ : Objs → Objs → Objs - data Arrows : (b c : Objs ) → Set c₂ - data Arrow : Objs → Objs → Set c₂ where --- case i + data Arrows : (b c : Objs ) → Set (suc c₁ ⊔ c₂) + data Arrow : Objs → Objs → Set (suc c₁ ⊔ c₂) where --- case i arrow : {a b : vertex G} → (edge G) a b → Arrow (atom a) (atom b) π : {a b : Objs } → Arrow ( a ∧ b ) a π' : {a b : Objs } → Arrow ( a ∧ b ) b @@ -146,7 +144,7 @@ assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h ) -- positive intutionistic calculus - PL : Category c₂ c₂ c₂ + PL : Category (suc c₁) (suc c₁ ⊔ c₂) (suc c₁ ⊔ c₂) PL = record { Obj = Objs; Hom = λ a b → Arrows a b ; @@ -173,12 +171,14 @@ -- open import Category.Sets -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionalit y c₂ c₂ + open import Data.List + C = graphtocat.Chain G tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b - tr f x y = graphtocat.next f (x y) + tr f x y = graphtocat.next f (x y) - fobj : ( a : Objs ) → Set c₂ + fobj : ( a : Objs ) → Set (c₁ ⊔ c₂) fobj (atom x) = ( y : vertex G ) → C y x fobj ⊤ = One fobj (a ∧ b) = ( fobj a /\ fobj b) @@ -186,7 +186,7 @@ fmap : { a b : Objs } → Hom PL a b → fobj a → fobj b amap : { a b : Objs } → Arrow a b → fobj a → fobj b - amap (arrow x) = tr x + amap (arrow x) y = tr x y -- tr x amap π ( x , y ) = x amap π' ( x , y ) = y amap ε (f , x ) = f x @@ -200,10 +200,10 @@ -- Sets is CCC, so we have a cartesian closed category generated by a graph -- as a sub category of Sets - CS : Functor PL (Sets {c₁}) - FObj CS a = {!!} -- fobj a - FMap CS {a} {b} f = {!!} -- fmap {a} {b} f - isFunctor CS = {!!} where -- isf where + CS : Functor PL (Sets {c₁ ⊔ c₂}) + FObj CS a = fobj a + FMap CS {a} {b} f = fmap {a} {b} f + isFunctor CS = isf where _+_ = Category._o_ PL ++idR = IsCategory.identityR ( Category.isCategory PL ) distr : {a b c : Obj PL} { f : Hom PL a b } { g : Hom PL b c } → (z : fobj a ) → fmap (g + f) z ≡ fmap g (fmap f z) @@ -229,15 +229,15 @@ --- smap (a b : vertex g ) → {a} → {b} -record CCCObj : Set c₃ where +record CCCObj {c₁ c₂ ℓ : Level} : Set (suc (ℓ ⊔ (c₂ ⊔ c₁))) where field - cat : Category c₂ c₁ c₁ + cat : Category c₁ c₂ ℓ ≡←≈ : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g ccc : CCC cat open CCCObj -record CCCMap (A B : CCCObj ) : Set c₃ where +record CCCMap {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (A : CCCObj {c₁} {c₂} {ℓ} ) (B : CCCObj {c₁′} {c₂′}{ℓ′} ) : Set (suc (ℓ′ ⊔ (c₂′ ⊔ c₁′) ⊔ ℓ ⊔ (c₂ ⊔ c₁))) where field cmap : Functor (cat A ) (cat B ) ccf : CCC (cat A) → CCC (cat B) @@ -247,9 +247,9 @@ open CCCMap open import Relation.Binary.Core -Cart : Category c₃ c₃ c₃ -Cart = record { - Obj = CCCObj +Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (ℓ ⊔ (c₂ ⊔ c₁))) (suc (ℓ ⊔ c₁ ⊔ c₂)) +Cart {c₁} {c₂} {ℓ} = record { + Obj = CCCObj {c₁} {c₂} {ℓ} ; Hom = CCCMap ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) } ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g @@ -268,7 +268,7 @@ open import graph open Graph -record GMap (x y : Graph {c₂} {c₁} ) : Set c₂ where +record GMap {c₁ c₂ c₁' c₂' : Level} (x : Graph {c₁} {c₂} ) (y : Graph {c₁'} {c₂'} ) : Set (c₁ ⊔ c₂ ⊔ c₁' ⊔ c₂') where field vmap : vertex x → vertex y emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b) @@ -277,20 +277,20 @@ open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) -data [_]_==_ (C : Graph {c₂} {c₁} ) {A B : vertex C} (f : edge C A B) - : ∀{X Y : vertex C} → edge C X Y → Set c₂ where +data [_]_==_ {c₁ c₂ : Level} (C : Graph {c₁} {c₂}) {A B : vertex C} (f : edge C A B) + : ∀{X Y : vertex C} → edge C X Y → Set (c₁ ⊔ c₂ ) where mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g -_=m=_ : {C D : Graph {c₂} {c₁} } - → (F G : GMap C D) → Set c₂ +_=m=_ : {c₁ c₂ c₁' c₂' : Level} {C : Graph {c₁} {c₂} } {D : Graph {c₁'} {c₂'} } + → (F G : GMap C D) → Set (c₁ ⊔ c₂ ⊔ c₁' ⊔ c₂') _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f -_&_ : {x y z : Graph {c₂} {c₁}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z +_&_ : {c₁ c₂ : Level} {x y z : Graph {c₁} {c₂} } ( f : GMap y z ) ( g : GMap x y ) → GMap x z f & g = record { vmap = λ x → vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) } -Grph : Category c₃ c₂ c₂ -Grph = record { - Obj = Graph {c₂} {c₁} +Grph : {c₁ c₂ : Level} → Category (suc (c₁ ⊔ c₂)) (c₁ ⊔ c₂) (c₁ ⊔ c₂) +Grph {c₁} {c₂} = record { + Obj = Graph {c₁} {c₂} ; Hom = GMap ; _o_ = _&_ ; _≈_ = _=m=_ @@ -302,21 +302,21 @@ ; o-resp-≈ = m--resp-≈ ; associative = λ e → mrefl refl }} where - msym : {x y : Graph {c₂} {c₁} } { f g : GMap x y } → f =m= g → g =m= f + msym : {x y : Graph {c₁} {c₂} } { f g : GMap x y } → f =m= g → g =m= f msym {x} {y} f=g f = lemma ( f=g f ) where lemma : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f lemma (mrefl Ff≈Gf) = mrefl (sym Ff≈Gf) - mtrans : {x y : Graph {c₂} {c₁} } { f g h : GMap x y } → f =m= g → g =m= h → f =m= h + mtrans : {x y : Graph {c₁} {c₂} } { f g h : GMap x y } → f =m= g → g =m= h → f =m= h mtrans {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f} → [ y ] p == q → [ y ] q == r → [ y ] p == r lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( trans eqv eqv₁ ) - ise : {x y : Graph {c₂} {c₁}} → IsEquivalence {_} {suc c₁ } {_} ( _=m=_ {x} {y}) + ise : {x y : Graph {c₁} {c₂} } → IsEquivalence {_} {c₁ ⊔ c₂} {_} ( _=m=_ {_} {_} {_} {_} {x} {y}) ise = record { refl = λ f → mrefl refl ; sym = msym ; trans = mtrans } - m--resp-≈ : {A B C : Graph {c₂} {c₁} } + m--resp-≈ : {A B C : Graph {c₁} {c₂} } {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g ) m--resp-≈ {A} {B} {C} {f} {g} {h} {i} f=g h=i e = lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where @@ -368,13 +368,13 @@ open ccc-from-graph.Arrows open graphtocat.Chain -Sets0 : Category c₂ c₁ c₁ -Sets0 = Sets {c₁} +Sets0 : {c₂ : Level } → Category (suc c₂) c₂ c₂ +Sets0 {c₂} = Sets {c₂} ccc-graph-univ : UniversalMapping Grph Cart forgetful.UX ccc-graph-univ = record { - F = λ g → csc g ; - η = λ a → record { vmap = λ y → {!!} ; emap = λ f x → {!!} } ; -- graphtocat.Chain a ? ? + F = λ g → csc {!!} ; + η = λ a → record { vmap = λ y → graphtocat.Chain {!!} {!!} {!!} ; emap = λ f x → {!!} } ; -- _* = solution ; isUniversalMapping = record { universalMapping = {!!} ; @@ -383,19 +383,19 @@ } where open forgetful open ccc-from-graph - csc : Graph {c₂} {c₁} → Obj Cart - csc g = record { cat = Sets ; ccc = sets ; ≡←≈ = λ eq → eq } - cs : (g : Graph {c₂}{c₁} ) → Functor (ccc-from-graph.PL g) (Sets {c₁}) + csc : {c₁ c₂ : Level} → Graph {c₂} {c₁} → Obj Cart + csc {c₁} {c₂} g = record { cat = Sets {c₂} ; ccc = sets ; ≡←≈ = λ eq → eq } + cs : {c₁ c₂ : Level} → (g : Graph {c₁} {c₂} ) → Functor (ccc-from-graph.PL g) (Sets {_}) cs g = CS g - pl : (g : Graph {c₂} {c₁ } ) → Category _ _ _ + pl : {c₁ c₂ : Level} → (g : Graph {c₁} {c₂} ) → Category _ _ _ pl g = PL g - cobj : {g : Obj Grph } {c : Obj Cart} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c) + cobj : {g : Obj Grph } {c : Obj Cart} → Hom Grph g (FObj UX c) → Objs g → Obj (cat c) cobj {g} {c} f (atom x) = vmap f x cobj {g} {c} f ⊤ = CCC.１ (ccc c) cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) (cobj {g} {c} f x) (cobj {g} {c} f y) cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) - c-map : {g : Obj (Grph )} {c : Obj Cart} {A B : Objs {!!}} - → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl {!!}) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B) + c-map : {g : Obj (Grph )} {c : Obj Cart} {A B : Objs g} + → (f : Hom Grph g (FObj UX c) ) → (p : Hom (pl g) A B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B) c-map {g} {c} {atom a} {atom x} f y = {!!} c-map {g} {c} {⊤} {atom x} f (iv f1 y) = {!!} c-map {g} {c} {a ∧ b} {atom x} f (iv f1 y) = {!!}