{-# OPTIONS --without-K --safe #-}

open import Categories.Category

-- The core of a category.
-- See https://ncatlab.org/nlab/show/core

module Categories.Category.Construction.Core {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level using (_⊔_)
open import Function using (flip)

open import Categories.Category.Groupoid using (Groupoid; IsGroupoid)
open import Categories.Morphism 𝒞 as Morphism
open import Categories.Morphism.IsoEquiv 𝒞 as IsoEquiv

open Category 𝒞
open _≃_

Core : Category o (ℓ ⊔ e) e
Core = record
  { Obj       = Obj
  ; _⇒_       = _≅_
  ; _≈_       = _≃_
  ; id        = ≅.refl
  ; _∘_       = flip ≅.trans
  ; assoc     = ⌞ assoc     ⌟
  ; sym-assoc = ⌞ sym-assoc ⌟
  ; identityˡ = ⌞ identityˡ ⌟
  ; identityʳ = ⌞ identityʳ ⌟
  ; identity² = ⌞ identity² ⌟
  ; equiv     = ≃-isEquivalence
  ; ∘-resp-≈  = λ where ⌞ eq₁ ⌟ ⌞ eq₂ ⌟ → ⌞ ∘-resp-≈ eq₁ eq₂ ⌟
  }

Core-isGroupoid : IsGroupoid Core
Core-isGroupoid = record
  { _⁻¹ = ≅.sym
  ; iso = λ {_ _ f} → record { isoˡ = ⌞ isoˡ f ⌟ ; isoʳ = ⌞ isoʳ f ⌟ }
  }
  where open _≅_

CoreGroupoid : Groupoid o (ℓ ⊔ e) e
CoreGroupoid = record { category = Core; isGroupoid = Core-isGroupoid }

module CoreGroupoid = Groupoid CoreGroupoid

-- Useful shorthands for reasoning about isomorphisms and morphisms of
-- 𝒞 in the same module.

module Shorthands where
  module Commutationᵢ where
    open Commutation Core public using () renaming ([_⇒_]⟨_≈_⟩ to [_≅_]⟨_≈_⟩)

    infixl  connectᵢ
    connectᵢ : ∀ {A C : Obj} (B : Obj) → A ≅ B → B ≅ C → A ≅ C
    connectᵢ B f g = ≅.trans f g

    syntax connectᵢ B f g = f ≅⟨ B ⟩ g

  open _≅_ public
  open _≃_ public
  open Morphism public using (module _≅_)
  open IsoEquiv public using (⌞_⌟) renaming (module _≃_ to _≈ᵢ_)
  open CoreGroupoid public using (_⁻¹) renaming
    ( _⇒_                 to _≅_
    ; _≈_                 to _≈ᵢ_
    ; id                  to idᵢ
    ; _∘_                 to _∘ᵢ_
    ; iso                 to ⁻¹-iso
    ; module Equiv        to Equivᵢ
    ; module HomReasoning to HomReasoningᵢ
    ; module iso          to ⁻¹-iso
    )