Mercurial > hg > Members > kono > Proof > category

changeset 967:472bcadfd216

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 Thu, 25 Feb 2021 13:08:17 +0900
parents cb970ab7c32b
children 3a096cb82dc4
files src/CCC.agda src/bi-ccc.agda
diffstat 2 files changed, 60 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCC.agda	Thu Feb 25 11:13:31 2021 +0900
+++ b/src/CCC.agda	Thu Feb 25 13:08:17 2021 +0900
@@ -32,29 +32,29 @@
        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 [ ○ １ ≈ id1 A １ ]
-     e'2 = let open  ≈-Reasoning A in begin
+     open  ≈-Reasoning A 
+     e'2 :  ○ １ ≈ id1 A １ 
+     e'2 = begin
             ○ １
         ≈↑⟨ e2  ⟩
            id1 A １
         ∎
-     e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [  ○ b o f ] ≈ ○ a ]
-     e''2 {a} {b} {f} = let open  ≈-Reasoning A in begin
+     e''2 : {a b : Obj A} {f : Hom A a b } →  ( ○ b o f ) ≈ ○ a 
+     e''2 {a} {b} {f} = begin
            ○ b o f
         ≈⟨ e2  ⟩
            ○ a
         ∎
-     π-id : {a b : Obj A} → A [ < π ,  π' >  ≈ id1 A (a ∧ b ) ]
-     π-id {a} {b} = let open  ≈-Reasoning A in begin
+     π-id : {a b : Obj A} →  < π ,  π' >  ≈ id1 A (a ∧ b ) 
+     π-id {a} {b} = begin
            < π ,  π' > 
         ≈↑⟨ π-cong idR idR  ⟩
           < π o id1 A (a ∧ b)  ,  π'  o id1 A (a ∧ b) >
         ≈⟨ e3c ⟩
           id1 A (a ∧ b )
         ∎
-     distr-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
-     distr-π {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
+     distr-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → ( < f , g > o h )  ≈  < ( f o h ) , ( g o h ) > 
+     distr-π {a} {b} {c} {d} {f} {g} {h} = begin
             < f , g > o h
         ≈↑⟨ e3c ⟩
             < π o  < f , g > o h  , π' o  < f , g > o h  >
@@ -64,8 +64,28 @@
             < f o h ,  g o h  >
         ∎
      _×_ :  {  a b c d  : Obj A } ( f : Hom A a c ) (g : Hom A b d )  → Hom A (a ∧ b) ( c ∧ d )
-     f × g  = < (A [ f o  π ] ) , (A [ g o π' ])  >
-     distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → A [ A [ h * o k ]  ≈ ( A [ h o < A [ k o π ] , π' > ] ) * ]
+     f × g  = < ( f o  π )  ,  (g o π' )  >
+     π-exchg : {a b c  : Obj A} {f : Hom A c a }{g : Hom A c b }  →  < π' , π > o < f , g >   ≈  < g , f > 
+     π-exchg {a} {b} {c} {f} {g} = begin
+            < π' , π > o < f , g >
+        ≈⟨ distr-π ⟩
+            < π' o < f , g > , π o < f , g > >
+        ≈⟨ π-cong e3b e3a ⟩
+           < g , f >
+        ∎ 
+     π'π : {a b : Obj A}   →  < π' , π > o < π' , π >   ≈  id1 A (a ∧ b)
+     π'π = trans-hom π-exchg π-id
+     exchg-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A d b }  →  < f o π , g o π' > o < π' , π >   ≈  < f o π' , g o π > 
+     exchg-π {a} {b} {c} {d} {f} {g} = begin
+           < f o π , g o π' > o < π' , π >
+        ≈⟨ distr-π ⟩
+           < (f o π) o < π' , π >  , (g o π' ) o < π' , π > > 
+        ≈↑⟨ π-cong assoc assoc ⟩
+           < f o (π o < π' , π > ) , g o (π' o < π' , π >)> 
+        ≈⟨ π-cong (cdr e3a)  (cdr e3b) ⟩
+           < f o π' , g o π >
+        ∎ 
+     distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → ( h * o k )  ≈ ( h o < ( k o π ) , π' > )  * 
      distr-* {a} {b} {c} {d} {h} {k} = begin
              h * o k
         ≈↑⟨ e4b  ⟩
@@ -86,12 +106,12 @@
                h o < k o π , π' > 
         ∎ ) ⟩
             ( h o  <  k o π  , π' > ) *
-        ∎ where open  ≈-Reasoning A
+        ∎ 
      α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
-     α = < A [ π  o π  ]  , < A [ π'  o π ]  , π'  > >
+     α = < ( π  o π  )  , < ( π'  o π )  , π'  > >
      α' : {a b c : Obj A } → Hom A  ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c )
-     α' = < < π , A [ π o π' ] > ,  A [ π'  o π' ]  >
-     β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → A [ A [ α o < < f , g > , h > ] ≈  < f , < g , h > > ]
+     α' = < < π , ( π o π' ) > ,  ( π'  o π' )  >
+     β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → ( α o < < f , g > , h > ) ≈  < f , < g , h > > 
      β {a} {b} {c} {d} {f} {g} {h} = begin
              α o < < f , g > , h >
         ≈⟨⟩
@@ -106,7 +126,7 @@
              < (  π o < f , g >  ) ,  < (  π' o < f , g >  ) , h >   >  
         ≈⟨ π-cong e3a ( π-cong e3b refl-hom )  ⟩
             < f , < g , h > >
-         ∎ where open  ≈-Reasoning A
+         ∎ 
 
 
 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
--- a/src/bi-ccc.agda	Thu Feb 25 11:13:31 2021 +0900
+++ b/src/bi-ccc.agda	Thu Feb 25 13:08:17 2021 +0900
@@ -45,9 +45,31 @@
        bi-hom→ : {a c : Obj A } →  Hom A ⊥ (c <= a ) → Hom A (a ∧ ⊥) c
        bi-hom→ f =  ε o ( < π' , π > o < π , f o π' > )
        bi-hom-iso : {a : Obj A } → {f : Hom A  (a ∧ ⊥) (a ∧ ⊥)}  →  A [ bi-hom→ (bi-hom← f )  ≈ f ] 
-       bi-hom-iso = {!!}
+       bi-hom-iso {a} {f} = begin
+            bi-hom→ (bi-hom← f )
+          ≈⟨⟩
+            ε o ( < π' , π > o < π , ((f o < π' , π > ) *) o π' > )
+          ≈⟨ cdr (IsCCC.π-exchg isCCC)  ⟩
+            ε o ( < ((f o < π' , π > ) *) o π' , π > )
+          ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym idL)) ⟩
+            ε o ( < ((f o < π' , π > ) *) o π' , id1 A _ o π > )
+          ≈↑⟨ cdr (IsCCC.exchg-π isCCC) ⟩
+            ε o (( < ((f o < π' , π > ) *) o π , id1 A _ o π' > ) o < π' , π > )
+          ≈⟨ cdr (car ( IsCCC.π-cong isCCC refl-hom idL)) ⟩
+            ε o (( < ((f o < π' , π > ) *) o π , π' > ) o < π' , π > )
+          ≈⟨ assoc ⟩
+            (ε o ( < ((f o < π' , π > ) *) o π , π' > )) o < π' , π > 
+          ≈⟨ car (IsCCC.e4a isCCC) ⟩
+            (f o < π' , π >) o < π' , π >
+          ≈⟨ sym assoc ⟩
+            f o (< π' , π > o < π' , π >)
+          ≈⟨ cdr (IsCCC.π'π isCCC) ⟩
+            f o id1 A _
+          ≈⟨ idR ⟩
+            f  
+          ∎ 
        bi-hom-cong : {a c : Obj A } → {f g : Hom A ⊥ (c <= a )} → A [ f ≈ g ]  →  A [ bi-hom→ f   ≈ bi-hom→ g ]
-       bi-hom-cong = {!!}
+       bi-hom-cong f=g = cdr ( cdr (IsCCC.π-cong isCCC refl-hom (car f=g) ))
        bi-ccc-0 :  A [ A [ □ ( a ∧ ⊥ ) o π' ] ≈ id1 A ( a ∧ ⊥ ) ]
        bi-ccc-0 = begin
              □ ( a ∧ ⊥ ) o π'