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 ( C is image of F )

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 ]

-- pre-initial

record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (F : Functor A A )  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
   field
      preinitial : ∀{  a : Obj A } → { b : Obj A } →  Hom A ( FObj F b ) a 
      uniqueness  : ∀{  a : Obj A } → { b : Obj A } →  ( f : Hom A ( FObj F b ) a ) →
          A [ f  ≈  preinitial {a} {b} ]

-- initial object

record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
   field
      initial :  ( a : Obj A ) →  Hom A i a
      uniqueness  : ( a : Obj A ) →  ( f : Hom A i a ) → A [ f ≈  initial a ]


-- A has initial object if it has PreInitial-SmallFullSubcategory

initialFromPreInitialFullSubcategory : {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 )
      -- ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 ) -- completeness
      (SFS : SmallFullSubcategory A F FMap← ) → 
      (PreInitial A F ) → { i : Obj A } → HasInitialObject A i
initialFromPreInitialFullSubcategory A F  FMap← SFS PI {i} = record {
      initial = {!!} ; 
      uniqueness  = {!!}
    }