open import Category -- https://github.com/konn/category-agda                                                                                     
open import Level
open import Category.Sets

module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
  where

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

-- C is small full subcategory of A

record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
           : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
   field
      ≈→≡ : {a b : Obj A } →  { x y : Hom A (FObj F a) (FObj F b) } → 
                (x≈y : A [ FMap F x ≈ FMap F y  ]) → FMap F x ≡ FMap F y   -- co-comain of FMap is local small
      full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ]
      full← : { a b : Obj A } { x : Hom A a b } → A [ FMap← ( FMap F x ) ≈ x ]

record PreInitial-SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
      (SFS : SmallFullSubcategory A F FMap← ) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
   field
      pre-initial : ∀{  a : Obj A } → { a' : Obj A } →  Hom A ( FObj F a' ) a 
      uniqueness  : ∀{  a : Obj A } → { a' : Obj A } →  ( f' : Hom A ( FObj F a' ) a ) →
          A [ f'  ≈  pre-initial {a} {a'} ]