changeset 787:ca5eba647990

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Apr 2019 20:07:22 +0900
parents 287d25c87b60
children a3e124e36acf
files CCC.agda CCChom.agda HomReasoning.agda
diffstat 3 files changed, 97 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/CCC.agda	Thu Apr 18 10:00:20 2019 +0900
+++ b/CCC.agda	Thu Apr 18 20:07:22 2019 +0900
@@ -30,6 +30,7 @@
        -- closed
        e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } →  A [ A [ ε o < A [ (h *) o π ]  ,  π' > ] ≈ h ]
        e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o < A [ k o  π ]  ,  π' > ] ) * ≈ k ]
+       *-cong :  {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ]  → A [  f *  ≈  f' * ] 
 
      e'2 : A [ ○ 1 ≈ id1 A 1 ]
      e'2 = let open  ≈-Reasoning A in begin
--- a/CCChom.agda	Thu Apr 18 10:00:20 2019 +0900
+++ b/CCChom.agda	Thu Apr 18 20:07:22 2019 +0900
@@ -43,6 +43,8 @@
            ≅← :  Hom B a' b' → Hom A a b
            iso→  : {f : Hom B a' b' }  → B [ ≅→ ( ≅← f) ≈ f ]
            iso←  : {f : Hom A a b }    → A [ ≅← ( ≅→ f) ≈ f ]
+           cong→ : {f g : Hom A a b }  → A [ f ≈ g ] →  B [ ≅→ f ≈ ≅→ g ]
+           cong← : {f g : Hom B a' b'} → B [ f ≈ g ] →  A [ ≅← f ≈ ≅← g ]
 
 
 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (1 : Obj A) 
@@ -73,9 +75,9 @@
      ; _*_ = CCC._∧_ c 
      ; _^_ = CCC._<=_ c
      ; isCCChom = record {
-            ccc-1 =  λ {a} {b} {c'} → record {   ≅→ =  c101  ; ≅← = c102  ; iso→  = c103 {a} {b} {c'} ; iso←  = c104 }
-          ; ccc-2 =  record {   ≅→ =  c201 ; ≅← = c202 ; iso→  = c203 ; iso←  = c204  }
-          ; ccc-3 =   record {   ≅→ =  c301 ; ≅← = c302 ; iso→  = c303 ; iso←  = c304  }
+            ccc-1 =  λ {a} {b} {c'} → record {   ≅→ =  c101  ; ≅← = c102  ; iso→  = c103 {a} {b} {c'} ; iso←  = c104 ; cong← = c105 ; cong→ = c106 }
+          ; ccc-2 =  record {   ≅→ =  c201 ; ≅← = c202 ; iso→  = c203 ; iso←  = c204  ; cong← = c205; cong→ = c206 }
+          ; ccc-3 =   record {   ≅→ =  c301 ; ≅← = c302 ; iso→  = c303 ; iso←  = c304 ; cong← = c305 ; cong→ = c306 }
         }
    } where
       c101 : {a : Obj A} → Hom A a (CCC.1 c) → Hom OneCat OneObj OneObj
@@ -102,6 +104,31 @@
       c303 = IsCCC.e4a (CCC.isCCC c)
       c304 : { c₁ a b  : Obj A} →  {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f ))  ≈ f ]
       c304 = IsCCC.e4b (CCC.isCCC c)
+      c105 :  {a : Obj A } {f g : Hom OneCat OneObj OneObj} → _[_≈_] OneCat {OneObj} {OneObj} f g → A [ c102 {a} f ≈ c102 {a} g ]
+      c105 refl = let  open  ≈-Reasoning A in refl-hom
+      c106 : { a  : Obj A }  {f g : Hom A a (CCC.1 c)} → A [ f ≈ g ] → _[_≈_] OneCat {OneObj} {OneObj}  OneObj  OneObj 
+      c106 _ = refl
+      c205  : { a b c₁ : Obj A } {f g : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ f ≈ g ] → A [ c202 f ≈ c202 g ]
+      c205  f=g = IsCCC.π-cong (CCC.isCCC c ) (proj₁ f=g ) (proj₂ f=g )
+      c206  : { a b c₁ : Obj A } {f g : Hom A c₁ ((c CCC.∧ a) b)} → A [ f ≈ g ] → (A × A) [ c201 f ≈ c201 g ]
+      c206 {a} {b} {c₁} {f} {g}  f=g = ( begin
+                      CCC.π c o f 
+                  ≈⟨ cdr f=g   ⟩
+                      CCC.π c o g
+                  ∎ ) , ( begin
+                      CCC.π' c o f 
+                  ≈⟨ cdr  f=g   ⟩
+                      CCC.π' c o g 
+                  ∎ ) where open ≈-Reasoning A
+      c305  : { a b  c₁ : Obj A } {f g : Hom A ((c CCC.∧ a) b) c₁} → A [ f ≈ g ] → A [ (c CCC.*) f ≈ (c CCC.*) g ]
+      c305  f=g = IsCCC.*-cong (CCC.isCCC c ) f=g
+      c306  : { a b  c₁ : Obj A } {f g : Hom A a ((c CCC.<= c₁) b)} → A [ f ≈ g ] → A [ c301 f ≈ c301 g ]
+      c306  {a} {b} {c₁} {f} {g} f=g =  begin
+                       CCC.ε c o  CCC.<_,_> c (  f o CCC.π c ) ( CCC.π' c ) 
+                  ≈⟨ cdr ( IsCCC.π-cong (CCC.isCCC c ) (car f=g )  refl-hom)  ⟩
+                       CCC.ε c o  CCC.<_,_> c (  g o CCC.π c ) ( CCC.π' c ) 
+                  ∎  where open ≈-Reasoning A
+
 
 open CCChom
 open IsCCChom
@@ -147,6 +174,7 @@
              ; π-cong = π-cong
              ; e4a = e4a
              ; e4b = e4b
+             ; *-cong = *-cong
            } where
                e20 : ∀ ( f : Hom OneCat OneObj OneObj ) →  _[_≈_] OneCat {OneObj} {OneObj} f OneObj 
                e20 OneObj = refl
@@ -161,22 +189,46 @@
                   ≈⟨⟩
                      ○ a
                   ∎ where open ≈-Reasoning A
-               e30 : {a b c d e : Obj A} → { f : Hom A ((_*_ h b) c) ((_*_ h d) e)  } → {g : Hom A a ((_*_ h b) c) }
-                   → A [ A [ proj₁ (≅→ (ccc-2 (isCCChom h)) f ) o g ] ≈  proj₁ (≅→ (ccc-2 (isCCChom h)) (A [ f o g ] ) ) ]
-               e30 = {!!}
-               e31 : {a b c d e : Obj A} → {i : Hom (A × A) (b , c) (d , e )}   → { f : Hom A a b  } → {g : Hom A a c }
-                   → A [ A [ {!!} o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ] ≈  ( ≅← (ccc-2 (isCCChom h)) ( _[_o_] (A × A) i (f , g ) )) ]
+               --
+               --             g                 id
+               --     a -------------> b * c ------>  b * c
+               --
+               --     a -------------> b * c ------>  b
+               --     a -------------> b * c ------>  c
+               --
+               e31 : {a b c  : Obj A} → {f : Hom A ((_*_ h b) c) ((_*_ h b) c) } → {g : Hom A a ((_*_ h b) c) }
+                 → (A × A) [ (A × A) [ ≅→ (ccc-2 (isCCChom h)) f o (g , g ) ] ≈  ≅→ (ccc-2 (isCCChom h)) ( A [ f o g ] ) ]
                e31 = {!!}
+               e30 : {a b c  : Obj A} → {g : Hom A a ((_*_ h b) c) }
+                   → (A × A) [ (A × A) [ (≅→ (ccc-2 (isCCChom h)) (id1 A ((_*_ h b) c))) o (g , g) ] ≈ (≅→ (ccc-2 (isCCChom h)) (A [ id1 A ((_*_ h b) c)  o g ] ) ) ]
+               e30 {a} {b} {c} {g} =   begin
+                    (≅→ (ccc-2 (isCCChom h)) (id1 A ((_*_ h b) c))) o (g , g)
+                  ≈⟨⟩
+                    ( π , π' ) o ( g , g )
+                  ≈⟨⟩
+                    ( _[_o_] A π  g , _[_o_] A π'  g ) 
+                  ≈↑⟨ cdr1 A (iso← (ccc-2 (isCCChom h)))  , cdr1 A (iso← (ccc-2 (isCCChom h)))  ⟩
+                    ( _[_o_] A (proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h b c) )))  (≅← (ccc-2 (isCCChom h))((≅→ (ccc-2 (isCCChom h)))  g)) , 
+                      _[_o_] A π' (≅← (ccc-2 (isCCChom h))((≅→ (ccc-2 (isCCChom h)))  g)) )
+                  ≈⟨ {!!} ⟩
+                    ( proj₁ ((≅→ (ccc-2 (isCCChom h)))  g) ,  proj₂ ((≅→ (ccc-2 (isCCChom h)))  g) ) 
+                  ≈⟨⟩
+                     ≅→ (ccc-2 (isCCChom h)) g
+                  ≈↑⟨ cong→ (ccc-2 (isCCChom h)) ( idL1 A )  ⟩
+                     ≅→ (ccc-2 (isCCChom h)) (_[_o_] A ( id1 A ((_*_ h b) c))   g  )
+                  ∎ where open ≈-Reasoning (A × A)
+               cong-proj₁ : {a b c d  : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₁ f  ≈ proj₁ g ]
+               cong-proj₁ eq =  proj₁ eq
                e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o <,> f g  ] ≈ f ]
                e3a {a} {b} {c} {f} {g} =  begin
                     π o <,> f g
                   ≈⟨⟩
                      proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o  (≅← (ccc-2 (isCCChom h)) (f , g))
-                  ≈⟨ e30 ⟩
-                     proj₁ (≅→ (ccc-2 (isCCChom h)) (_[_o_] A ( id1 A ( _*_ h a  b )) ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
-                  ≈⟨ {!!} ⟩
-                     proj₁ (≅→ (ccc-2 (isCCChom h)) (≅← (ccc-2 (isCCChom h)) ( _[_o_] (A × A )  ( id1 A a , id1 A b )  (f , g)  )))
-                  ≈⟨ {!!} ⟩
+                  ≈⟨ cong-proj₁ e30 ⟩
+                     proj₁ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a  b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
+                  ≈⟨ cong-proj₁  ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
+                     proj₁ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
+                  ≈⟨ cong-proj₁ ( iso→ (ccc-2 (isCCChom h))) ⟩
                      proj₁ ( f , g )
                   ≈⟨⟩
                     f 
@@ -190,20 +242,37 @@
                       <,> f  g 
                   ≈⟨⟩
                        ≅← (ccc-2 (isCCChom h)) (f , g)
-                  ≈⟨ ≡-cong {!!} {!!} ⟩
+                  ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 )  ⟩
                        ≅← (ccc-2 (isCCChom h)) (f' , g')
                   ≈⟨⟩
                       <,> f'  g' 
                   ∎ where open ≈-Reasoning A
+               e40 : {a c : Obj A} → { f : Hom A (_*_ h a c ) a } → A [ ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) f) ≈ f ]
+               e40 = iso→  (ccc-3 (isCCChom h))
+               e41 : {a c : Obj A} → { f : Hom A a (_^_ h c a )} → A [ ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h))  f) ≈ f ]
+               e41 = iso←  (ccc-3 (isCCChom h))
                e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } →  A [ A [ ε o ( <,> ( A [ (k *) o π ] )   π')  ] ≈ k ]
                e4a {a} {b} {c} {k} =  begin
                       ε o ( <,> ((k *)  o π  ) π' )
                   ≈⟨⟩
-                      ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o 
-                          (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π'))
+                      ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π'))
                   ≈⟨ {!!} ⟩
+                      ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k) 
+                  ≈⟨ iso→  (ccc-3 (isCCChom h))  ⟩
                       k
                   ∎ where open ≈-Reasoning A
                e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o ( <,> ( A [ k o  π ]  )  π' ) ] ) * ≈ k ]
-               e4b = {!!}
+               e4b {a} {b} {c} {k} =  begin
+                      ( ε o ( <,> (  k o  π  )  π' ) ) *
+                  ≈⟨⟩
+                     ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o  π , π'))) 
+                  ≈⟨ {!!} ⟩
+                     ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k)
+                  ≈⟨ iso←  (ccc-3 (isCCChom h))  ⟩
+                      k
+                  ∎ where open ≈-Reasoning A
+               *-cong  : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
+               *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
 
+
+
--- a/HomReasoning.agda	Thu Apr 18 10:00:20 2019 +0900
+++ b/HomReasoning.agda	Thu Apr 18 20:07:22 2019 +0900
@@ -54,11 +54,19 @@
 
   car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
           x ≈ y  → ( x o f ) ≈ ( y  o f )
-  car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq
+  car  eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq
+
+  car1 : { c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
+          A [ x ≈ y ] → A [ A [  x o f ] ≈ A [  y  o f  ] ]
+  car1 A  eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))  ) eq
 
   cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
           x ≈ y  →  f o x  ≈  f  o y 
-  cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom  ) 
+  cdr eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom  ) 
+
+  cdr1 : { c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
+          A [ x ≈ y ] →  A [ A [ f o x ]  ≈  A [ f  o y  ] ]
+  cdr1 A eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))  ) 
 
   id :  (a  : Obj A ) →  Hom A a a
   id a =  (Id {_} {_} {_} {A} a)