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 {!!} {!!} ℓ
_↑_  = {!!}