open import Level
open import Categories.Category
open import Categories.Functor.Core
open import Categories.FreeObjects.Free

module Object.FreeObject where
  private
    variable
      o ℓ e o' ℓ' e' : Level

  record IsFreeObject {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) (η : C [ X , Functor.₀ U FX ]) : Set (suc (e ⊔ e' ⊔ o ⊔ ℓ ⊔ o' ⊔ ℓ')) where
    private
      module C = Category C using (Obj; id; identityʳ; identityˡ; _⇒_; _∘_; equiv; module Equiv)
      module D = Category D using (Obj; _⇒_; _∘_; equiv)
      module U = Functor U using (₀; ₁)

    field
      _* : ∀ {A : D.Obj} → C [ X , U.₀ A ] → D [ FX , A ]
      *-lift : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) → C [ (U.₁ (f *) C.∘ η) ≈ f ]
      *-uniq : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ FX , A ]) → C [ (U.₁ g) C.∘ η ≈ f ] → D [ g ≈ f * ]


  IsFreeObject⇒FreeObject : ∀ {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) (η : C [ X , Functor.₀ U FX ]) → IsFreeObject U X FX η → FreeObject U X
  IsFreeObject⇒FreeObject U X FX η isFO = record 
    { FX = FX 
    ; η = η 
    ; _* = _* 
    ; *-lift = *-lift 
    ; *-uniq = *-uniq 
    }
    where open IsFreeObject isFO