Mercurial > hg > Members > kono > Proof > category

changeset 1011:a104c3baefe4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 20 Mar 2021 16:03:45 +0900
parents bfd9c55ac628
children 5dcbf2b9194e
files src/CCC.agda src/deductive.agda
diffstat 2 files changed, 56 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Sat Mar 20 13:01:16 2021 +0900
+++ b/src/CCC.agda	Sat Mar 20 16:03:45 2021 +0900
@@ -156,6 +156,30 @@
          ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
          isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε 
 
+open Functor
+
+record CCCFunctor {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+         (ca : CCC A) (cb : CCC B) (functor : Functor A B)
+         : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ')) where
+     field
+       f１ : FObj functor (CCC.１ ca) ≡ CCC.１ cb 
+       f○ : {a : Obj A} → B [ FMap functor (CCC.○ ca a) ≈
+           subst (λ k → Hom B (FObj functor a) k) (sym f１) (CCC.○ cb (FObj functor a)) ]
+       f∧  : {a b : Obj A}   → FObj functor ( CCC._∧_ ca a b ) ≡ CCC._∧_ cb (FObj functor a ) (FObj functor b)
+       f<= : {a b : Obj A}   → FObj functor ( CCC._<=_ ca a b ) ≡ CCC._<=_ cb (FObj functor a ) (FObj functor b)
+       f<> : {a b c : Obj A} → (f : Hom A c a ) → (g : Hom A c b )
+           → B [ FMap functor (CCC.<_,_> ca f  g )  ≈
+                   subst (λ k → Hom B (FObj functor c) k ) (sym f∧ ) ( CCC.<_,_> cb (FMap functor f ) ( FMap functor g )) ]
+       fπ  : {a b : Obj A} → B [ FMap functor (CCC.π ca {a} {b})  ≈
+                   subst (λ k → Hom B k (FObj functor a) ) (sym f∧ ) (CCC.π  cb {FObj functor a} {FObj functor b}) ]
+       fπ' : {a b : Obj A} → B [ FMap functor (CCC.π' ca {a} {b})  ≈
+                   subst (λ k → Hom B k (FObj functor b) ) (sym f∧ ) (CCC.π' cb {FObj functor a} {FObj functor b}) ]
+       f*  : {a b c : Obj A} → (f : Hom A (CCC._∧_ ca a b) c )  → B [ FMap functor (CCC._* ca f)  ≈
+                   subst (λ k → Hom B (FObj functor a) k) (sym f<=) (CCC._*  cb ((subst (λ k → Hom B k (FObj functor c) ) f∧ (FMap functor f) ))) ]
+       fε  : {a b : Obj A} → B [ FMap functor (CCC.ε ca {a} {b} )
+          ≈  subst (λ k → Hom B k (FObj functor a)) (trans (cong (λ k → CCC._∧_ cb k (FObj functor b)) (sym f<=)) (sym f∧))
+              (CCC.ε cb {FObj functor a} {FObj functor b}) ]
+
 ----
 --
 -- Sub Object Classifier as Topos
--- a/src/deductive.agda	Sat Mar 20 13:01:16 2021 +0900
+++ b/src/deductive.agda	Sat Mar 20 16:03:45 2021 +0900
@@ -26,9 +26,7 @@
   _・_ = _[_o_] A
   
   -- every proof b →  c with assumption a has following forms
-
-  ⊤ = １
-  data  φ  {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ⊔ ℓ) where
+  data  φ  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ⊔ ℓ) where
      i   : {b c : Obj A} {k : Hom A b c } → φ x k
      ii  : φ x {⊤} {a} x
      iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c'  ∧ c''} < f , g > 
@@ -41,7 +39,7 @@
   
   -- genetate (a ∧ b) → c proof from  proof b →  c with assumption a
   
-  k : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x∈a z ) → Hom A (a ∧ b) c
+  k : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x∈a z ) → Hom A (a ∧ b) c
   k x∈a {k} i = k ・ π'
   k x∈a ii = π
   k x∈a (iii ψ χ ) = < k x∈a ψ  , k x∈a χ  >
@@ -49,10 +47,10 @@
   k x∈a (v ψ ) = ( k x∈a ψ  ・ α ) *
   k x∈a (φ-cong  eq ψ) = k x∈a  ψ
 
-  toφ : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
-  toφ {a} {b} {c} x∈a z = i
+  toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
+  toφ {a} {⊤} {b} {c} x∈a z = i
 
-  record PHom {a : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+  record PHom {a ⊤ : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
     field
        hom : Hom A b c 
        phi : φ x {b} {c} hom
@@ -60,20 +58,37 @@
   open PHom
   open import HomReasoning
   open import cat-utility
-  
-  Polynominal :  {a : Obj A } ( x : Hom A ⊤ a ) → Category c₁ (c₁ ⊔ c₂ ⊔ ℓ) ℓ 
-  Polynominal {a} x =  record {
+
+  -- date _≅_ : {a b c : Hom A} → { x : Hom A ⊤ a } → (f g : PHom b c ) → Set (c₁ ⊔ c₂ ⊔ ℓ) where
+  --    pcomp : { a b c : Hom A } → A [ A [ hom g o hom f ] ≈ hom h ] → (A [ hom g o hom f ]) ≅ hom h
+
+  -- this is too easy, so what is A[x]?
+  Polynominal :  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Category c₁ (c₁ ⊔ c₂ ⊔ ℓ) ℓ 
+  Polynominal {a} {⊤} x =  record {
             Obj  = Obj A;
-            Hom = λ b c → PHom {a} {x} b c ;
+            Hom = λ b c → PHom {a} {⊤} {x} b c ;
             _o_ =  λ{a} {b} {c} x y → record { hom = A [ hom x o hom y ] ; phi = iv (phi x) (phi y) } ;
             _≈_ =  λ x y → A [ hom x ≈ hom y ] ;
             Id  =  λ{a} → record { hom = id1 A a ; phi = i } ;
             isCategory  = record {
-                    isEquivalence =  {!!} ;
-                    identityL  = λ {a b f} → {!!} ;
-                    identityR  = λ {a b f} → {!!} ;
-                    o-resp-≈  = λ {a b c f g h i} → {!!} ;
-                    associative  = λ{a b c d f g h } → {!!} 
+                    isEquivalence =  record { sym = sym-hom ; trans = trans-hom ; refl = refl-hom } ;
+                    identityL  = λ {a b f} → idL ;
+                    identityR  = λ {a b f} → idR ;
+                    o-resp-≈  = λ {a b c f g h i} → resp ;
+                    associative  = λ{a b c d f g h } → assoc 
                }
-           } 
+           }  where
+              open ≈-Reasoning A
 
+  Hx :  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Functor A (Polynominal x)
+  Hx {a} x = record {
+     FObj = λ a → a
+   ; FMap = λ f → record { hom = f ; phi = i }
+   ; isFunctor = record {
+        identity = refl-hom
+      ; distr = refl-hom
+      ; ≈-cong = λ eq → eq
+     }
+   } where
+      open ≈-Reasoning A
+