--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Comma.agda	Wed Mar 08 22:33:31 2017 +0900
@@ -0,0 +1,62 @@
+open import Level
+open import Category 
+module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( F G : Functor A B ) where
+
+open import HomReasoning
+open import cat-utility
+
+
+-- this a special case A = A, B = A, C = B
+
+open Functor
+
+record CommaObj :  Set ( c₁  ⊔  c₂' ) where
+     field
+        obj : Obj A
+        hom : Hom B ( FObj F obj ) ( FObj G obj ) 
+
+open CommaObj
+
+record CommaHom ( a b :  CommaObj ) :  Set ( c₂ ⊔   ℓ' ) where
+     field
+        arrow  : Hom A ( obj a ) ( obj b )
+        comm   :  B [ B [ FMap G arrow  o hom a ]  ≈ B [ hom b  o  FMap F arrow ]  ]
+
+open CommaHom
+
+_⋍_ : { a b :  CommaObj } ( f g : CommaHom a b ) →  Set ℓ
+_⋍_ f g = A [ arrow f ≈ arrow g ]
+
+_∙_ :  {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 :  B [ B [ FMap G (A [ arrow f o arrow g ] ) o hom a ]  ≈ B [ hom c  o  FMap F (A [ arrow f o arrow g ]) ]  ]
+        comm1 = {!!}
+
+CommaId : { a : CommaObj } → CommaHom a a
+CommaId {a} = record {  arrow = id1 A ( obj a ) ;  
+      comm = comm2 } where
+        comm2 :  B [ B [ FMap G (id1 A (obj a)) o hom a ]  ≈ B [ hom a  o  FMap F (id1 A (obj a)) ]  ]
+        comm2 = {!!}
+  
+open import Relation.Binary.Core
+
+isCommaCategory : IsCategory CommaObj CommaHom _⋍_  _∙_  CommaId
+isCommaCategory = record  { 
+          isEquivalence =  let open ≈-Reasoning (A) in record {refl = refl-hom ; 
+                  sym = sym ;
+                  trans = trans-hom } 
+        ; identityL = {!!} 
+        ; identityR = {!!} 
+        ; o-resp-≈ =  λ{a b c f g h i } → o-resp-≈1      {a} {b} {c} {f} {g} {h} {i}
+        ; associative = {!!} 
+        }  where 
+             o-resp-≈1 : {!!}
+             o-resp-≈1  = {!!}
+
+
+_↑_   : Category {!!} {!!} ℓ
+_↑_  = {!!}
+