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

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

open import cat-utility
open import HomReasoning
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   -- codomain 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 ]

-- pre-initial

record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (F : Functor A A )  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
   field
      preinitialObj : ∀{  a : Obj A } →  Obj A 
      preinitialArrow : ∀{  a : Obj A } →  Hom A ( FObj F (preinitialObj {a} )) a 

-- 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 complete catagory has initial object if it has PreInitial-SmallFullSubcategory

open NTrans
open Limit
open SmallFullSubcategory
open PreInitial

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 A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
      ( equ : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g )
      (SFS : SmallFullSubcategory A F FMap← ) → 
      (PI : PreInitial A F ) → { a0 : Obj A } → 
      { ee : {a b : Obj A} → {f g : Hom A a b}  → Obj A }
      { ep :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ee {a} {b} {f} {g} ) a }
      { u : (a : Obj A) → NTrans A A (K A A a) F }  
          → HasInitialObject A a0
initialFromPreInitialFullSubcategory A F  FMap← lim equ SFS PI {a0} {ee} {ep} {u} = record {
      initial = initialArrow ; 
      uniqueness  = λ a f → lemma1 a f
    } where
      f : {a : Obj A} -> Hom A  a0 (FObj F  (preinitialObj PI {a} ) ) 
      f {a} = limit (lim F {FObj F (preinitialObj PI {a} )} {u (FObj F (preinitialObj PI))} ) a0 (u a0 )  
      initialArrow :  ∀( a : Obj A )  →  Hom A a0 a
      initialArrow a  = A [ preinitialArrow PI {a}  o f ]
      limit-u : Limit A A F a0 (u a0)
      limit-u = lim F {a0} {u a0}
      equ-fi : { a c : Obj A} -> { p : Hom A c a0 } -> {f' : Hom A a0 a} -> 
          Equalizer A p ( A [ preinitialArrow PI {a} o  f ] ) f'
      equ-fi  {a} {c} {p} {f'} = equ ( A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ] ) f'
      e=id : {e : Hom A a0 a0} -> ( {c : Obj A} -> A [ A [ TMap (u a0)  c o  e ]  ≈  TMap (u a0) c ] ) -> A [ e  ≈ id1 A a0 ]
      e=id  {e} uce=uc =  let open ≈-Reasoning (A) in
            begin
              e
            ≈↑⟨ limit-uniqueness limit-u {a0} {u a0} {e} ( \{i} -> uce=uc ) ⟩
              limit limit-u a0 (u a0)
            ≈⟨ limit-uniqueness limit-u {a0} {u a0} {id1 A a0} ( \{i} -> idR ) ⟩
              id1 A a0
            ∎
      open Equalizer
      kfuc=uc : {c k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ TMap (u a0)  c  o  
              A [ p o A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ]  
                      ≈ TMap (u a0) c ]
      kfuc=uc {k1} {c} = {!!}
      kfuc=1 : {k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ p o A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ≈ id1 A a0 ]
      kfuc=1 {k1} {p} = e=id ( kfuc=uc )
      -- if equalizer has right inverse, f = g
      lemma2 :  (a b : Obj A) {c : Obj A} ( f g : Hom A a b ) 
            {e : Hom A c a } {e' : Hom A a c } ( equ : Equalizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] )
           -> A [ f ≈ g ]
      lemma2 a b {c} f g {e} {e'} equ inv-e = let open ≈-Reasoning (A) in
            let open Equalizer in
            begin
                f
               ≈↑⟨ idR ⟩
                 f o  id1 A a 
               ≈↑⟨ cdr inv-e ⟩
                 f o  (  e o e'  ) 
               ≈⟨ assoc  ⟩
                 ( f o  e ) o e'  
               ≈⟨ car ( fe=ge equ ) ⟩
                 ( g o  e ) o e'  
               ≈↑⟨ assoc  ⟩
                 g o  (  e o e'  ) 
               ≈⟨ cdr inv-e   ⟩
                 g o  id1 A a
               ≈⟨ idR ⟩
                g
            ∎
      lemma1 : (a : Obj A) (f' : Hom A a0 a) → A [ f' ≈ initialArrow a ]
      lemma1 a f' = let open ≈-Reasoning (A) in 
             sym (
             begin
                 initialArrow a
             ≈⟨⟩
                 preinitialArrow PI {a} o  limit (lim F) a0 (u a0) 
             ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ]) f' {ep {a0} {a} {f'} {f'} } equ-fi 
                      (kfuc=1 {ee} {ep} ) ⟩
                 f'
             ∎  )