--- a/Comma.agda	Wed Mar 08 22:33:31 2017 +0900
+++ b/Comma.agda	Thu Mar 09 09:03:07 2017 +0900
@@ -1,26 +1,29 @@
 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
+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
 
 open import HomReasoning
 open import cat-utility
 
-
--- this a special case A = A, B = A, C = B
+--
+--      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 B ( FObj F obj ) ( FObj G obj ) 
+        hom : Hom C ( 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 ]  ]
+        comm   :  C [ C [ FMap G arrow  o hom a ]  ≈ C [ hom b  o  FMap F arrow ]  ]
 
 open CommaHom
 
@@ -32,31 +35,69 @@
          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 = {!!}
+        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 =  let open ≈-Reasoning C in begin
+               FMap G (A [ arrow f o arrow g ] ) o hom a    
+           ≈⟨ car ( distr G ) ⟩
+               ( FMap G (arrow f)  o   FMap G (arrow g )) o hom a    
+           ≈↑⟨ assoc ⟩
+               FMap G (arrow f)  o ( FMap G (arrow g )  o hom a )
+           ≈⟨ cdr ( comm g ) ⟩
+               FMap G (arrow f)  o  ( hom b  o  FMap F (arrow g ) )
+           ≈⟨ assoc  ⟩
+               ( FMap G (arrow 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  ⟩
+                hom c o ( FMap F (arrow f)   o  FMap F (arrow g ) )
+           ≈↑⟨ cdr ( distr F) ⟩
+                hom c o  FMap F (A [ arrow f o arrow g ])
+           ∎ 
 
 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 = {!!}
+        comm2 :  C [ C [ FMap G (id1 A (obj 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
+           ≈⟨ car ( IsFunctor.identity ( isFunctor G ) )  ⟩
+                 id1 C (FObj G (obj a))  o  hom a
+           ≈⟨ idL  ⟩
+                 hom a
+           ≈↑⟨ idR  ⟩
+                 hom a  o  id1 C (FObj F (obj a))
+           ≈↑⟨ cdr ( IsFunctor.identity ( isFunctor F ) )⟩
+                 hom a  o  FMap F (id1 A (obj a))
+           ∎ 
   
-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 = {!!} 
+        ; 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 
-             o-resp-≈1 : {!!}
-             o-resp-≈1  = {!!}
+             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
+                ∎
+
+_↓_   : Category  (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
+_↓_  = record { Obj = CommaObj 
+         ; Hom = CommaHom
+         ; _o_ = _∙_
+         ; _≈_ = _⋍_
+         ; Id  = CommaId
+         ; isCategory = isCommaCategory
+         }
 
 
-_↑_   : Category {!!} {!!} ℓ
-_↑_  = {!!}
-