\begin{code}
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Categories where

open import Prelude
open import Cubical.Foundations.HLevels

\end{code}
%<*precategory>
\begin{code}
record PreCategory ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    Ob    : Type ℓ₁
    Hom   : Ob → Ob → Type ℓ₂
    Id    : ∀ {X} → Hom X X
    Comp  : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z
    assoc-Comp : ∀  {W X Y Z}
                    (f : Hom Y Z)
                    (g : Hom X Y)
                    (h : Hom W X) →
                    Comp f (Comp g h) ≡ Comp (Comp f g) h
    Comp-Id  : ∀ {X Y} (f : Hom X Y) → Comp f Id ≡ f
    Id-Comp  : ∀ {X Y} (f : Hom X Y) → Comp Id f ≡ f
    Hom-Set  : ∀ {X Y} → isSet (Hom X Y)
\end{code}
%</precategory>
\begin{code}
  infixr  _⟶_
\end{code}
%<*morph-arrow>
\begin{code}
  _⟶_ = Hom
\end{code}
%</morph-arrow>
\begin{code}

  infixl  _⟵_
  _⟵_ = flip Hom

  infixr  _·_
  _·_ = Comp

  variable
    X Y Z : Ob

  infix  _≅_
  _≅_ : Ob → Ob → Type _
\end{code}
%<*isomorphism>
\begin{code}
  Isomorphism : (X ⟶ Y) → Type ℓ₂
  Isomorphism {X} {Y} f = Σ[ g ⦂ Y ⟶ X ] ((g · f ≡ Id) × (f · g ≡ Id))

  X ≅ Y = Σ (X ⟶ Y) Isomorphism
\end{code}
%</isomorphism>
\begin{code}

  Domain : (X ⟶ Y) → Ob
  Domain {X} {Y} _ = X

  Codomain : (X ⟶ Y) → Ob
  Codomain {X} {Y} _ = Y

  module _ {X Y : Ob} where
    Monic : (X ⟶ Y) → Type _
    Monic f = ∀ {Z} → (g₁ g₂ : Z ⟶ X) → f · g₁ ≡ f · g₂ → g₁ ≡ g₂

    Epic : (X ⟶ Y) → Type _
    Epic f = ∀ {Z} → (g₁ g₂ : Y ⟶ Z) → g₁ · f ≡ g₂ · f → g₁ ≡ g₂

  IsInitial : Ob → Type _
  IsInitial I = ∀ {X} → isContr (I ⟶ X)

  IsTerminal : Ob → Type _
  IsTerminal T = ∀ {X} → isContr (X ⟶ T)

  Initial = ∃ IsInitial
  Terminal = ∃ IsTerminal

  refl-≅ : X ≅ X
  refl-≅ .fst = Id
  refl-≅ .snd .fst = Id
  refl-≅ .snd .snd .fst = Comp-Id Id
  refl-≅ .snd .snd .snd = Comp-Id Id

  sym-≅ : X ≅ Y → Y ≅ X
  sym-≅ X≅Y .fst = X≅Y .snd .fst
  sym-≅ X≅Y .snd .fst = X≅Y .fst
  sym-≅ X≅Y .snd .snd .fst = X≅Y .snd .snd .snd
  sym-≅ X≅Y .snd .snd .snd = X≅Y .snd .snd .fst

  open import Path.Reasoning

  trans-≅ : X ≅ Y → Y ≅ Z → X ≅ Z
  trans-≅ X≅Y Y≅Z .fst = Y≅Z .fst · X≅Y .fst
  trans-≅ X≅Y Y≅Z .snd .fst = X≅Y .snd .fst · Y≅Z .snd .fst
  trans-≅ X≅Y Y≅Z .snd .snd .fst =
    (X≅Y .snd .fst · Y≅Z .snd .fst) · (Y≅Z .fst · X≅Y .fst) ≡⟨ assoc-Comp _ _ _ ⟩
    ((X≅Y .snd .fst · Y≅Z .snd .fst) · Y≅Z .fst) · X≅Y .fst ≡˘⟨ cong (_· X≅Y .fst) (assoc-Comp _ _ _) ⟩
    (X≅Y .snd .fst · (Y≅Z .snd .fst · Y≅Z .fst)) · X≅Y .fst ≡⟨ cong (λ yz → (X≅Y .snd .fst · yz) · X≅Y .fst) (Y≅Z .snd .snd .fst) ⟩
    (X≅Y .snd .fst · Id) · X≅Y .fst ≡⟨ cong (_· X≅Y .fst) (Comp-Id (X≅Y .snd .fst)) ⟩
    X≅Y .snd .fst · X≅Y .fst ≡⟨ X≅Y .snd .snd .fst ⟩
    Id ∎
  trans-≅ X≅Y Y≅Z .snd .snd .snd =
    (Y≅Z .fst · X≅Y .fst) · (X≅Y .snd .fst · Y≅Z .snd .fst) ≡⟨ assoc-Comp _ _ _ ⟩
    ((Y≅Z .fst · X≅Y .fst) · X≅Y .snd .fst) · Y≅Z .snd .fst ≡˘⟨ cong (_· Y≅Z .snd .fst) (assoc-Comp _ _ _) ⟩
    (Y≅Z .fst · (X≅Y .fst · X≅Y .snd .fst)) · Y≅Z .snd .fst ≡⟨ cong (λ xy → (Y≅Z .fst · xy) · Y≅Z .snd .fst) (X≅Y .snd .snd .snd) ⟩
    (Y≅Z .fst · Id) · Y≅Z .snd .fst ≡⟨ cong (_· Y≅Z .snd .fst) (Comp-Id _) ⟩
    Y≅Z .fst · Y≅Z .snd .fst ≡⟨ Y≅Z .snd .snd .snd ⟩
    Id ∎

  idToIso : X ≡ Y → X ≅ Y
  idToIso {X} {Y} X≡Y = subst (X ≅_) X≡Y refl-≅

  ≅-set : isSet (X ≅ Y)
  ≅-set = isOfHLevelΣ  Hom-Set
    λ _ → isOfHLevelΣ  Hom-Set
    λ _ → isOfHLevelΣ  (hLevelSuc  (Hom _ _) Hom-Set _ _)
    λ _ → hLevelSuc  (Hom _ _) Hom-Set _ _

open import Cubical.Foundations.Transport

record Category ℓ₁ ℓ₂ : Type (ℓsuc (ℓ₁ ℓ⊔ ℓ₂)) where
  field
    preCategory : PreCategory ℓ₁ ℓ₂
  open PreCategory preCategory public
  field
\end{code}
%<*cat-univalence>
\begin{code}
    univalent : {X Y : Ob} → (X ≡ Y) ≃ (X ≅ Y)
\end{code}
%</cat-univalence>
\begin{code}

module _ {ℓ₁ ℓ₂} (C : Category ℓ₁ ℓ₂) where
  open Category C

  _[_,_] : Ob → Ob → Type ℓ₂
  _[_,_] = Hom
  {-# INLINE _[_,_] #-}

  _[_∘_] : (Y ⟶ Z) → (X ⟶ Y) → (X ⟶ Z)
  _[_∘_] = Comp
  {-# INLINE _[_∘_] #-}
\end{code}