{-# OPTIONS --without-K --safe #-}
 
open import Categories.Category
 
module Categories.Functor.Construction.SubCategory {o ℓ e} (C : Category o ℓ e) where
 
open import Categories.Category.SubCategory C
 
open Category C
open Equiv
 
open import Level
open import Function.Base using () renaming (id to id→)
open import Data.Product
 
open import Categories.Functor using (Functor)
 
private
  variable
    ℓ′ i : Level
    I : Set i
    U : I → Obj
 
Sub : ∀ (sub : SubCat {i} {ℓ′} I) → Functor (SubCategory sub) C
Sub (record {U = U}) = record
  { F₀ = U
  ; F₁ = proj₁
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = id→
  }
 
FullSub : Functor (FullSubCategory U) C
FullSub {U = U} = record
  { F₀ = U
  ; F₁ = id→
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = id→
  }