Mercurial > hg > Members > kono > Proof > category

changeset 479:a5034bdf6f38

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Comma Category with A B C
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 09 Mar 2017 14:16:03 +0900
parents dc24ac6ebdb3
children 08f9c8a59ff4
files Comma.agda HomReasoning.agda
diffstat 2 files changed, 45 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/Comma.agda	Thu Mar 09 09:03:07 2017 +0900
+++ b/Comma.agda	Thu Mar 09 14:16:03 2017 +0900
@@ -1,6 +1,7 @@
 open import Level
 open import Category 
-module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} ( F G : Functor A C ) where
+module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} 
+    ( F : Functor A C ) ( G : Functor B C ) where
 
 open import HomReasoning
 open import cat-utility
@@ -9,43 +10,48 @@
 --      F     G
 --    A -> C <- B
 --
--- this a special case A = B
 
 open Functor
 
 record CommaObj :  Set ( c₁  ⊔  c₂' ) where
      field
         obj : Obj A
-        hom : Hom C ( FObj F obj ) ( FObj G obj ) 
+        objb : Obj B
+        hom : Hom C ( FObj F obj ) ( FObj G objb ) 
 
 open CommaObj
 
 record CommaHom ( a b :  CommaObj ) :  Set ( c₂ ⊔   ℓ' ) where
      field
         arrow  : Hom A ( obj a ) ( obj b )
-        comm   :  C [ C [ FMap G arrow  o hom a ]  ≈ C [ hom b  o  FMap F arrow ]  ]
+        arrowg : Hom B ( objb a ) ( objb b )
+        comm   :  C [ C [ FMap G arrowg  o hom a ]  ≈ C [ hom b  o  FMap F arrow ]  ]
 
 open CommaHom
 
-_⋍_ : { a b :  CommaObj } ( f g : CommaHom a b ) →  Set ℓ
-_⋍_ f g = A [ arrow f ≈ arrow g ]
+record _⋍_ { a b :  CommaObj } ( f g : CommaHom a b ) :  Set ℓ where
+     field 
+        eqa : A [ arrow f ≈ arrow g ] 
+        eqb : B [ arrowg f ≈ arrowg g ]
+
+open _⋍_
 
 _∙_ :  {a b c : CommaObj } → CommaHom b c → CommaHom a b → CommaHom a c
 _∙_ {a} {b} {c} f g = record { 
          arrow = A [ arrow f o arrow g ] ;
          comm  = comm1
      } where
-        comm1 :  C [ C [ FMap G (A [ arrow f o arrow g ] ) o hom a ]  ≈ C [ hom c  o  FMap F (A [ arrow f o arrow g ]) ]  ]
+        comm1 :  C [ C [ FMap G (B [ arrowg f o arrowg g ] ) o hom a ]  ≈ C [ hom c  o  FMap F (A [ arrow f o arrow g ]) ]  ]
         comm1 =  let open ≈-Reasoning C in begin
-               FMap G (A [ arrow f o arrow g ] ) o hom a    
+               FMap G (B [ arrowg f o arrowg g ] ) o hom a    
            ≈⟨ car ( distr G ) ⟩
-               ( FMap G (arrow f)  o   FMap G (arrow g )) o hom a    
+               ( FMap G (arrowg f)  o   FMap G (arrowg g )) o hom a    
            ≈↑⟨ assoc ⟩
-               FMap G (arrow f)  o ( FMap G (arrow g )  o hom a )
+               FMap G (arrowg f)  o ( FMap G (arrowg g )  o hom a )
            ≈⟨ cdr ( comm g ) ⟩
-               FMap G (arrow f)  o  ( hom b  o  FMap F (arrow g ) )
+               FMap G (arrowg f)  o  ( hom b  o  FMap F (arrow g ) )
            ≈⟨ assoc  ⟩
-               ( FMap G (arrow f)  o  hom b) o  FMap F (arrow g ) 
+               ( FMap G (arrowg f)  o  hom b) o  FMap F (arrow g ) 
            ≈⟨ car ( comm f ) ⟩
                ( hom c o FMap F (arrow f)  ) o  FMap F (arrow g ) 
            ≈↑⟨ assoc  ⟩
@@ -57,11 +63,11 @@
 CommaId : { a : CommaObj } → CommaHom a a
 CommaId {a} = record {  arrow = id1 A ( obj a ) ;  
       comm = comm2 } where
-        comm2 :  C [ C [ FMap G (id1 A (obj a)) o hom a ]  ≈ C [ hom a  o  FMap F (id1 A (obj a)) ]  ]
+        comm2 :  C [ C [ FMap G (id1 B (objb a)) o hom a ]  ≈ C [ hom a  o  FMap F (id1 A (obj a)) ]  ]
         comm2 =  let open ≈-Reasoning C in begin
-                 FMap G (id1 A (obj a)) o hom a
+                 FMap G (id1 B (objb a)) o hom a
            ≈⟨ car ( IsFunctor.identity ( isFunctor G ) )  ⟩
-                 id1 C (FObj G (obj a))  o  hom a
+                 id1 C (FObj G (objb a))  o  hom a
            ≈⟨ idL  ⟩
                  hom a
            ≈↑⟨ idR  ⟩
@@ -72,24 +78,29 @@
   
 isCommaCategory : IsCategory CommaObj CommaHom _⋍_  _∙_  CommaId
 isCommaCategory = record  { 
-          isEquivalence =  let open ≈-Reasoning (A) in record {refl = refl-hom ; 
-                  sym = sym ;
-                  trans = trans-hom } 
-        ; identityL = λ{a b f} →  identityL {a} {b} {f}
-        ; identityR = λ{a b f} →   let open ≈-Reasoning A in idR
-        ; o-resp-≈ =   IsCategory.o-resp-≈ ( Category.isCategory A )
-        ; associative = IsCategory.associative (Category.isCategory A)
-        }  where 
-             identityL :  {a : CommaObj} {b : CommaObj} {f : CommaHom a b} → (CommaId ∙ f) ⋍ f
-             identityL {a} {b} {f} =  let open ≈-Reasoning A in begin
-                  arrow (CommaId ∙ f)
-                ≈⟨⟩
-                  arrow (CommaId {b} )  o arrow f
-                ≈⟨⟩
-                  id1 A (obj b)  o arrow f
-                ≈⟨ idL ⟩
-                  arrow f
-                ∎
+          isEquivalence = record { refl =  record { eqa = let open ≈-Reasoning (A) in refl-hom ; eqb =  let open ≈-Reasoning (B) in refl-hom } ;
+                  sym = λ {f} {g} f=g → record { eqa =  let open ≈-Reasoning (A) in sym ( eqa f=g) ; eqb =  let open ≈-Reasoning (B) in sym ( eqb f=g ) }   ;
+                  trans = λ {f} {g} {h}  f=g g=h → record {
+                     eqa =  let open ≈-Reasoning (A) in trans-hom (eqa f=g) (eqa g=h) 
+                     ; eqb = let open ≈-Reasoning (B) in trans-hom (eqb f=g) (eqb g=h)  
+              } }
+        ; identityL = λ{a b f} →   record { 
+                eqa = let open ≈-Reasoning (A) in idL {obj a} {obj b} {arrow f}
+              ; eqb = let open ≈-Reasoning (B) in idL {objb a} {objb b} {arrowg f}
+           }
+        ; identityR = λ{a b f} →   record { 
+                eqa = let open ≈-Reasoning (A) in idR {obj a} {obj b} {arrow f}
+              ; eqb = let open ≈-Reasoning (B) in idR {objb a} {objb b} {arrowg f}
+           }
+        ; o-resp-≈ =    λ  {a b c  } {f g } {h i } f=g h=i → record {
+                eqa = IsCategory.o-resp-≈ (Category.isCategory A)  (eqa f=g) (eqa h=i )
+              ; eqb = IsCategory.o-resp-≈ (Category.isCategory B)  (eqb f=g) (eqb h=i )
+           }
+        ; associative = λ {a b c d} {f}  {g} {h} → record {
+                eqa = IsCategory.associative (Category.isCategory A) 
+              ; eqb = IsCategory.associative (Category.isCategory B) 
+              }
+        }  
 
 _↓_   : Category  (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
 _↓_  = record { Obj = CommaObj 
--- a/HomReasoning.agda	Thu Mar 09 09:03:07 2017 +0900
+++ b/HomReasoning.agda	Thu Mar 09 14:16:03 2017 +0900
@@ -64,7 +64,7 @@
   id :  (a  : Obj A ) →  Hom A a a
   id a =  (Id {_} {_} {_} {A} a) 
 
-  idL :  {a b : Obj A } { f : Hom A b a } →  id a o f  ≈ f 
+  idL :  {a b : Obj A } { f : Hom A a b } →  id b o f  ≈ f 
   idL =  IsCategory.identityL (Category.isCategory A)
 
   idR :  {a b : Obj A } { f : Hom A a b } →  f o id a  ≈ f