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

open import HomReasoning
open import cat-utility

--
--      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 ) 

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 :  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 :  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))
           ∎ 
  
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
                ∎

_↓_   : Category  (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ
_↓_  = record { Obj = CommaObj 
         ; Hom = CommaHom
         ; _o_ = _∙_
         ; _≈_ = _⋍_
         ; Id  = CommaId
         ; isCategory = isCommaCategory
         }