bsc-leon-vatthauer/agda/src/FreeObject.lagda.md

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

Free objects

The notion of free object has been formalized in agda-categories:

open import Categories.FreeObjects.Free

but we need a predicate expressing that an object 'is free':

record IsFreeObject {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) : 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
     η : C [ X , U.₀ FX ]
     _* : ∀ {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 * ]

and some way to convert between these notions:

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

  -- TODO FreeObject⇒IsFreeObject