--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Comma1.agda	Fri Mar 10 18:56:21 2017 +0900
@@ -0,0 +1,171 @@
+open import Level
+open import Category 
+module Comma1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ}  {C : Category c₁' c₂' ℓ'} 
+    ( F : Functor A C ) ( G : Functor A C ) where
+
+open import HomReasoning
+open import cat-utility
+
+--
+--      F     G
+--    A -> C <- A
+--
+
+open Functor
+
+record CommaObj :  Set ( c₁  ⊔  c₂' ) where
+     field
+        obj : Obj A
+        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   :  C [ C [ FMap G arrow  o hom a ]  ≈ C [ hom b  o  FMap F arrow ]  ]
+
+open CommaHom
+
+_∙_ :  {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 =  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 :  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))
+           ∎ 
+ 
+_⋍_ : { a b :  CommaObj } ( f g : CommaHom a b ) →  Set ℓ
+f ⋍ g  = A [ arrow f ≈ arrow g ]
+
+ 
+isCommaCategory : IsCategory CommaObj CommaHom _⋍_  _∙_  CommaId
+isCommaCategory = record  { 
+          isEquivalence = record { refl =  let open ≈-Reasoning (A) in refl-hom ;
+                  sym = let open ≈-Reasoning (A) in sym ;
+                  trans = let open ≈-Reasoning (A) in trans-hom 
+              } 
+        ; identityL = let open ≈-Reasoning (A) in idL
+        ; identityR = let open ≈-Reasoning (A) in idR
+        ; o-resp-≈ =   IsCategory.o-resp-≈ ( Category.isCategory A )
+        ; associative =  IsCategory.associative ( Category.isCategory A )
+        }  
+
+CommaCategory   : Category  (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
+CommaCategory  = record { Obj = CommaObj 
+         ; Hom = CommaHom
+         ; _o_ = _∙_
+         ; _≈_ = _⋍_
+         ; Id  = CommaId
+         ; isCategory = isCommaCategory
+         }
+
+open NTrans
+
+nat-lemma : NTrans A C F G → Functor A CommaCategory
+nat-lemma n = record {
+        FObj = λ x → fobj x ;
+        FMap = λ {a} {b} f → fmap {a} {b} f ;
+        isFunctor = record {
+             identity = λ{x} → identity x
+             ; distr = λ {a} {b} {c} {f} {g}   → distr1 {a} {b} {c} {f} {g}
+             ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
+          }
+   } where
+        fobj :  Obj A → Obj CommaCategory
+        fobj x = record { obj = x ; hom = TMap n x }
+        fmap :  {a b : Obj A } → Hom A a b → Hom CommaCategory (fobj a) (fobj b )
+        fmap f = record { arrow = f ; comm = IsNTrans.commute (isNTrans n ) }
+        ≈-cong :  {a : Obj A} {b : Obj A} {f g : Hom A a b}  → A [ f ≈ g ]  → CommaCategory [ fmap f ≈ fmap g ]
+        ≈-cong  {a} {b} {f} {g} f=g = f=g
+        identity : (x : Obj A ) ->  CommaCategory [ fmap (id1 A x) ≈  id1 CommaCategory (fobj x) ]
+        identity x = let open ≈-Reasoning (A) in  begin
+                arrow (fmap (id1 A x))
+             ≈⟨⟩
+                id1 A x
+             ≈⟨⟩
+                arrow (id1 CommaCategory (fobj x))
+             ∎
+        distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} →
+               CommaCategory [ fmap (A [ g o f ])  ≈  CommaCategory [ fmap g o fmap f ] ]
+        distr1 = let open ≈-Reasoning (A) in  refl-hom
+
+nat-f : Functor A C  → Functor A CommaCategory → Functor A C
+nat-f F N = record {
+        FObj = λ x → FObj F ( obj ( FObj N x )) ;
+        FMap = λ {a} {b} f → FMap F (arrow (FMap N f))  ;
+        isFunctor = record {
+             identity = λ{x} → identity x
+             ; distr = λ {a} {b} {c} {f} {g}   → distr1 {a} {b} {c} {f} {g}
+             ; ≈-cong = λ {a} {b} {f} {g}   →  ≈-cong  {a} {b} {f} {g}
+          }
+   } where
+        identity : (x : Obj A ) ->   C [ FMap F (arrow (FMap N (id1 A x))) ≈ id1 C (FObj F (obj (FObj N x))) ]
+        identity x = let open ≈-Reasoning (C) in  begin
+                 FMap F (arrow (FMap N (id1 A x)))
+             ≈⟨ fcong F ( IsFunctor.identity ( isFunctor N)  ) ⟩
+                 FMap F (id1 A (obj (FObj N x)))
+             ≈⟨ IsFunctor.identity ( isFunctor F ) ⟩
+                id1 C (FObj F (obj (FObj N x)))
+             ∎
+        distr1 : {a : Obj A} {b : Obj A} {c : Obj A} {f : Hom A a b} {g : Hom A b c} →
+                C [ FMap F (arrow (FMap N (A [ g o f ]))) ≈
+                C [ FMap F (arrow (FMap N g)) o FMap F (arrow (FMap N f)) ] ]
+        distr1 {a} {b} {c} {f} {g} =  let open ≈-Reasoning (C) in  begin
+                 FMap F (arrow (FMap N (A [ g o f ])))
+             ≈⟨ fcong F ( IsFunctor.distr ( isFunctor N)  ) ⟩
+                 FMap F (A [ arrow (FMap N g ) o arrow (FMap N f ) ] )
+             ≈⟨ ( IsFunctor.distr ( isFunctor F )  ) ⟩
+                FMap F (arrow (FMap N g)) o FMap F (arrow (FMap N f)) 
+             ∎
+        ≈-cong :  {a : Obj A} {b : Obj A} {f g : Hom A a b}  → A [ f ≈ g ]  → C [ FMap F (arrow (FMap N f)) ≈ FMap F (arrow (FMap N g)) ]
+        ≈-cong  {a} {b} {f} {g} f=g = let open ≈-Reasoning (C) in  begin
+                 FMap F (arrow (FMap N f)) 
+             ≈⟨ fcong F (( IsFunctor.≈-cong ( isFunctor N)  ) f=g ) ⟩
+                 FMap F (arrow (FMap N g)) 
+             ∎
+
+nat-lemma← : ( N : Functor A CommaCategory ) →  NTrans A C (nat-f F N) (nat-f G N)
+nat-lemma← N = record {
+        TMap = λ (a : Obj A ) →  tmap1 a
+        ; isNTrans = record {
+             commute = λ {a} {b} {f} → commute2 {a} {b} {f}
+          }
+   } where
+       tmap1 : (a : Obj A ) →   Hom C (FObj F (obj ( FObj N a))) (FObj G (obj ( FObj N a)))
+       tmap1 a = hom (FObj N a)
+       commute2 :  {a b : Obj A } {f : Hom A a b  } →  
+           C [ C [ FMap G ( arrow ( FMap N f)) o tmap1 a  ] ≈ C [ tmap1 b  o FMap F ( arrow ( FMap N f )) ]  ]
+       commute2 {a} {b} {f} = comm ( FMap N f )