open import Cat.Functor.WideSubcategory
open import Cat.Instances.Functor
open import Cat.Groupoid
open import Cat.Prelude

import Cat.Reasoning

module Cat.Instances.Core where

open Functor


# The core of a category🔗

The core of a category $\mathcal{C}$ is the maximal sub-groupoid of $\mathcal{C}$: the category $\mathrm{Core}(\mathcal{C})$ constructed by keeping only the invertible morphisms. Since the identity is invertible, and invertibility is closed under composition, we can construct this as a wide subcategory of $\mathcal{C}$.

Core : ∀ {o ℓ} → Precategory o ℓ → Precategory o ℓ
Core C = Wide sub where
open Cat.Reasoning C

sub : Wide-subcat {C = C} _
sub .Wide-subcat.P = is-invertible
sub .Wide-subcat.P-prop _ = is-invertible-is-prop
sub .Wide-subcat.P-id = id-invertible
sub .Wide-subcat.P-∘ = invertible-∘

private module Core {o ℓ} (C : Precategory o ℓ) = Cat.Reasoning (Core C)

Core-is-groupoid : ∀ {o ℓ} {C : Precategory o ℓ} → is-pregroupoid (Core C)
Core-is-groupoid {C = C} f =
Core.make-invertible _ (wide f-inv.inv ((f .witness) C.invertible⁻¹))
(Wide-hom-path f-inv.invl)
(Wide-hom-path f-inv.invr)
where
module C = Cat.Reasoning C
module f-inv = C.is-invertible (f .witness)


We have mentioned that the core is the maximal sub-groupoid of $\mathcal{C}$: we can regard it as the cofree groupoid on a category, summarised by the following universal property. Suppose $\mathcal{C}$ is a groupoid and $\mathcal{D}$ is some category. Any functor $F : \mathcal{C} \to \mathcal{D}$ must factor through the core of $\mathcal{D}$.

module _
{oc ℓc od ℓd} {C : Precategory oc ℓc} {D : Precategory od ℓd}
(grpd : is-pregroupoid C)
where

Core-universal : (F : Functor C D) → Functor C (Core D)
Core-universal F .F₀ x = F .F₀ x
Core-universal F .F₁ f .hom = F .F₁ f
Core-universal F .F₁ f .witness = F-map-invertible F (grpd f)
Core-universal F .F-id = Wide-hom-path (F .F-id)
Core-universal F .F-∘ f g = Wide-hom-path (F .F-∘ f g)

Core-factor : (F : Functor C D) → F ≡ Forget-wide-subcat F∘ Core-universal F
Core-factor F = Functor-path (λ _ → refl) λ _ → refl