open import Category
open import Level
module subcat {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') (B : Category c₁ c₂ ℓ) (F : Functor A B) where

    open import cat-utility
    open import Relation.Binary.PropositionalEquality
    open Functor

    FCat : Category c₁' c₂ ℓ
    FCat = record {
          Obj = Obj A
          ; Hom = λ a b → Hom B (FObj F a) (FObj F b)
          ; _o_ = Category._o_ B
          ; _≈_ = Category._≈_ B
          ; Id  = λ {a} → id1 B (FObj F a)
          ; isCategory = record {
                    isEquivalence =  IsCategory.isEquivalence (Category.isCategory B) ;
                    identityL  = λ {a b f} → IsCategory.identityL (Category.isCategory B) ;
                    identityR  = λ {a b f} → IsCategory.identityR (Category.isCategory B) ;
                    o-resp-≈  = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B);
                    associative  = λ{a b c d f g h } → IsCategory.associative (Category.isCategory B) 
             }
      }