{-# OPTIONS --postfix-projections --rewriting --prop #-}

module Cat where
open import Lib

{-
 - We postulate an internal category.
 -}

postulate
  Ob : Set
  Hom : Ob → Ob → Set
  EqHom : ∀ {x y} → Hom x y → Hom x y → Prop

  id : ∀ {x} → Hom x x
  _∘_ : ∀ {x y z} → Hom y z → Hom x y → Hom x z

postulate
  idl : ∀ {x y} {f : Hom x y} → (id ∘ f) ≡ f
  idr : ∀ {x y} {f : Hom x y} → (f ∘ id) ≡ f
  assoc : ∀ {x y z w} {f : Hom z w} {g : Hom y z} {h : Hom x y} → ((f ∘ g) ∘ h) ≡ (f ∘ (g ∘ h))
{-# REWRITE idl idr assoc #-}

postulate
  irefl : ∀ {x y} {f : Hom x y} → EqHom f f
  reflect : ∀ {x y} {f g : Hom x y} → EqHom f g → f ≡ g

{-
 - Helper functions and definitions for a category.
 -}

unreflect : ∀ {x y} {f g : Hom x y} → f ≡ g → EqHom f g
unreflect refl = irefl

whisker : ∀ {x y z w} (l : Hom z w) {f g : Hom y z} (p : f ≡ g) (r : Hom x y) → (l ∘ (f ∘ r)) ≡ (l ∘ (g ∘ r))
whisker l refl r = refl

record Iso x y : Set where
  field iso-f  : Hom x y
        iso-g  : Hom y x
        iso-fg : EqHom (iso-f ∘ iso-g) id
        iso-gf : EqHom (iso-g ∘ iso-f) id
open Iso public

inv : ∀ {x y} → Iso x y → Iso y x
inv f .iso-f  = f .iso-g
inv f .iso-g  = f .iso-f
inv f .iso-fg = f .iso-gf
inv f .iso-gf = f .iso-fg

id-iso : ∀ {x} → Iso x x
id-iso .iso-f = id
id-iso .iso-g = id
id-iso .iso-fg = irefl
id-iso .iso-gf = irefl

_∘i_ : ∀ {x y z} → Iso y z → Iso x y → Iso x z
(f ∘i g) .iso-f = f .iso-f ∘ g .iso-f
(f ∘i g) .iso-g = inv g .iso-f ∘ inv f .iso-f
(f ∘i g) .iso-fg = unreflect ( whisker (f .iso-f) (reflect (g .iso-fg)) (f .iso-g)
                             ∙ reflect (f .iso-fg))
(f ∘i g) .iso-gf = unreflect ( whisker (g .iso-g) (reflect (f .iso-gf)) (g .iso-f)
                             ∙ reflect (g .iso-gf))

{-
 - The components of the pre-reflexive graphs model PreReflGraph(T_Cat)
 -}

Obᴱ : Ob → Ob → Set
Obᴱ xₗ xᵣ = Iso xₗ xᵣ

Homᴱ : ∀ {xₗ} {xᵣ} (xₑ : Obᴱ xₗ xᵣ)
         {yₗ} {yᵣ} (yₑ : Obᴱ yₗ yᵣ)
       → Hom xₗ yₗ → Hom xᵣ yᵣ → Set
Homᴱ xₑ yₑ fₗ fᵣ
  = LiftP (EqHom (yₑ .iso-f ∘ fₗ) (fᵣ ∘ xₑ .iso-f))

EqHomᴱ : ∀ {xₗ} {xᵣ} (xₑ : Obᴱ xₗ xᵣ)
           {yₗ} {yᵣ} (yₑ : Obᴱ yₗ yᵣ)
           {fₗ} {fᵣ} (fₑ : Homᴱ xₑ yₑ fₗ fᵣ)
           {gₗ} {gᵣ} (gₑ : Homᴱ xₑ yₑ gₗ gᵣ)
         → EqHom fₗ gₗ → EqHom fᵣ gᵣ → Set
EqHomᴱ xₑ yₑ fₑ gₑ _ _ = ⊤

Obᴿ : (x : Ob) → Obᴱ x x → Set
Obᴿ x xₑ = LiftP (EqHom (xₑ .iso-f) id)

Homᴿ : ∀ {x} {xₑ} (xᵣ : Obᴿ x xₑ)
         {y} {yₑ} (yᵣ : Obᴿ y yₑ)
       → (f : Hom x y) → Homᴱ xₑ yₑ f f → Set
Homᴿ xᵣ yᵣ f fᵣ = ⊤

EqHomᴿ : ∀ {x} {xₑ} (xᵣ : Obᴿ x xₑ)
           {y} {yₑ} (yᵣ : Obᴿ y yₑ)
           {f} {fₑ : Homᴱ xₑ yₑ f f} (fᵣ : Homᴿ {x} {xₑ} xᵣ {y} {yₑ} yᵣ f fₑ)
           {g} {gₑ : Homᴱ xₑ yₑ g g} (gᵣ : Homᴿ {x} {xₑ} xᵣ {y} {yₑ} yᵣ g gₑ)
         → (p : EqHom f g) → EqHomᴱ xₑ yₑ fₑ gₑ p p → Set
EqHomᴿ xᵣ yᵣ fᵣ gᵣ _ _ = ⊤

idᴱ : ∀ {xₗ} {xᵣ} (xₑ : Obᴱ xₗ xᵣ)
    → Homᴱ xₑ xₑ id id
idᴱ xₑ = lift irefl

idᴿ : ∀ {x} {xₑ} (xᵣ : Obᴿ x xₑ)
    → Homᴿ {xₑ = xₑ} xᵣ {yₑ = xₑ} xᵣ id (idᴱ xₑ)
idᴿ xᵣ = tt

∘ᴱ : ∀ {xₗ} {xᵣ} (xₑ : Obᴱ xₗ xᵣ)
       {yₗ} {yᵣ} (yₑ : Obᴱ yₗ yᵣ)
       {zₗ} {zᵣ} (zₑ : Obᴱ zₗ zᵣ)
       {fₗ} {fᵣ} (fₑ : Homᴱ yₑ zₑ fₗ fᵣ)
       {gₗ} {gᵣ} (gₑ : Homᴱ xₑ yₑ gₗ gᵣ)
     → Homᴱ xₑ zₑ (fₗ ∘ gₗ) (fᵣ ∘ gᵣ)
∘ᴱ xₑ yₑ zₑ {fₗ} {fᵣ} (lift fₑ) {gₗ} {gᵣ} (lift gₑ)
  = lift (unreflect (whisker id (reflect fₑ) gₗ
                   ∙ whisker fᵣ (reflect gₑ) id))

∘ᴿ : ∀ {x} {xₑ} (xᵣ : Obᴿ x xₑ)
       {y} {yₑ} (yᵣ : Obᴿ y yₑ)
       {z} {zₑ} (zᵣ : Obᴿ z zₑ)
       {f} {fₑ} (fᵣ : Homᴿ {xₑ = yₑ} yᵣ {yₑ = zₑ} zᵣ f fₑ)
       {g} {gₑ} (gᵣ : Homᴿ {xₑ = xₑ} xᵣ {yₑ = yₑ} yᵣ g gₑ)
     → Homᴿ {xₑ = xₑ} xᵣ {yₑ = zₑ} zᵣ (f ∘ g) (∘ᴱ xₑ yₑ zₑ {fᵣ = f} fₑ {gᵣ = g} gₑ)
∘ᴿ xᵣ yᵣ zᵣ fᵣ gᵣ = tt

{-
 - Reflexivity operations for every generating sort.
 -}

reflᴱ-Ob : (x : Ob) → Obᴱ x x
reflᴱ-Ob x = id-iso

reflᴿ-Ob : (x : Ob) → Obᴿ x (reflᴱ-Ob x)
reflᴿ-Ob x = lift irefl

reflᴱ-Hom : {x : Ob} {xₑ : Obᴱ x x} (xᵣ : Obᴿ x xₑ)
            {y : Ob} {yₑ : Obᴱ y y} (yᵣ : Obᴿ y yₑ)
            (f : Hom x y)
          → Homᴱ xₑ yₑ f f
reflᴱ-Hom xᵣ yᵣ f with reflect (xᵣ .lower) | reflect (yᵣ .lower)
... | refl | refl = lift irefl

reflᴿ-Hom : {x : Ob} {xₑ : Obᴱ x x} (xᵣ : Obᴿ x xₑ)
            {y : Ob} {yₑ : Obᴱ y y} (yᵣ : Obᴿ y yₑ)
            (f : Hom x y)
          → Homᴿ {xₑ = xₑ} xᵣ {yₑ = yₑ} yᵣ f (reflᴱ-Hom {xₑ = xₑ} xᵣ {yₑ = yₑ} yᵣ f)
reflᴿ-Hom xᵣ yᵣ f = tt


reflᴱ-EqHom : {x : Ob} (xₑ : Obᴱ x x) (xᵣ : Obᴿ x xₑ)
              {y : Ob} (yₑ : Obᴱ y y) (yᵣ : Obᴿ y yₑ)
              {f : Hom x y} (fₑ : Homᴱ xₑ yₑ f f) (fᵣ : Homᴿ {xₑ = xₑ} xᵣ {yₑ = yₑ} yᵣ f fₑ)
              {g : Hom x y} (gₑ : Homᴱ xₑ yₑ g g) (gᵣ : Homᴿ {xₑ = xₑ} xᵣ {yₑ = yₑ} yᵣ g gₑ)
              (p : EqHom f g)
            → EqHomᴱ xₑ yₑ fₑ gₑ p p
reflᴱ-EqHom xₑ xᵣ yₑ yᵣ fₑ fᵣ gₑ gᵣ p = tt

reflᴿ-EqHom : {x : Ob} (xₑ : Obᴱ x x) (xᵣ : Obᴿ x xₑ)
              {y : Ob} (yₑ : Obᴱ y y) (yᵣ : Obᴿ y yₑ)
              {f : Hom x y} (fₑ : Homᴱ xₑ yₑ f f) (fᵣ : Homᴿ {xₑ = xₑ} xᵣ {yₑ = yₑ} yᵣ f fₑ)
              {g : Hom x y} (gₑ : Homᴱ xₑ yₑ g g) (gᵣ : Homᴿ {xₑ = xₑ} xᵣ {yₑ = yₑ} yᵣ g gₑ)
              (p : EqHom f g)
            → EqHomᴿ {xₑ = xₑ} xᵣ {yₑ = yₑ} yᵣ {fₑ = fₑ} fᵣ {gₑ = gₑ} gᵣ p (reflᴱ-EqHom xₑ xᵣ yₑ yᵣ fₑ fᵣ gₑ gᵣ p)
reflᴿ-EqHom xₑ xᵣ yₑ yᵣ fₑ fᵣ gₑ gᵣ p = tt

{-
 - The basic contractible types.
 -}

data isContrᵇ : Set → Set where
  isContr-Obₗ
    : (xₗ : Ob)
    → isContrᵇ (Σ Ob λ xᵣ → Obᴱ xₗ xᵣ)

  isContr-Obᵣ
    : (xᵣ : Ob)
    → isContrᵇ (Σ Ob λ xₗ → Obᴱ xₗ xᵣ)

  isContr-Ob~
    : (x : Ob)
    → isContrᵇ (Σ Ob λ y → Iso x y)

  isContr-Homₗ
    : ∀ (xₗ xᵣ : Ob) (xₑ : Obᴱ xₗ xᵣ)
        (yₗ yᵣ : Ob) (yₑ : Obᴱ yₗ yᵣ)
        (fₗ : Hom xₗ yₗ)
      → isContrᵇ (Σ (Hom xᵣ yᵣ) λ fᵣ → Homᴱ xₑ yₑ fₗ fᵣ)

  isContr-Homᵣ
    : ∀ (xₗ xᵣ : Ob) (xₑ : Obᴱ xₗ xᵣ)
        (yₗ yᵣ : Ob) (yₑ : Obᴱ yₗ yᵣ)
        (fᵣ : Hom xᵣ yᵣ)
      → isContrᵇ (Σ (Hom xₗ yₗ) λ fₗ → Homᴱ xₑ yₑ fₗ fᵣ)

  isContr-Hom~
    : ∀ (x y : Ob) (f : Hom x y)
      → isContrᵇ (Σ (Hom x y) λ g → LiftP (EqHom f g))

  isContr-EqHomₗ
    : ∀ (xₗ xᵣ : Ob) (xₑ : Obᴱ xₗ xᵣ)
        (yₗ yᵣ : Ob) (yₑ : Obᴱ yₗ yᵣ)
        (fₗ : Hom xₗ yₗ) (fᵣ : Hom xᵣ yᵣ) (fₑ : Homᴱ xₑ yₑ fₗ fᵣ)
        (gₗ : Hom xₗ yₗ) (gᵣ : Hom xᵣ yᵣ) (gₑ : Homᴱ xₑ yₑ gₗ gᵣ)
        (pₗ : EqHom fₗ gₗ)
      → isContrᵇ (Σ (LiftP (EqHom fᵣ gᵣ)) λ pᵣ → EqHomᴱ xₑ yₑ fₑ gₑ pₗ (pᵣ .lower))

  isContr-EqHomᵣ
    : ∀ (xₗ xᵣ : Ob) (xₑ : Obᴱ xₗ xᵣ)
        (yₗ yᵣ : Ob) (yₑ : Obᴱ yₗ yᵣ)
        (fₗ : Hom xₗ yₗ) (fᵣ : Hom xᵣ yᵣ) (fₑ : Homᴱ xₑ yₑ fₗ fᵣ)
        (gₗ : Hom xₗ yₗ) (gᵣ : Hom xᵣ yᵣ) (gₑ : Homᴱ xₑ yₑ gₗ gᵣ)
        (pᵣ : EqHom fᵣ gᵣ)
      → isContrᵇ (Σ (LiftP (EqHom fₗ gₗ)) λ pₗ → EqHomᴱ xₑ yₑ fₑ gₑ (pₗ .lower) pᵣ)

  isContr-EqHom~
    : ∀ (x y : Ob) (f g : Hom x y) (p : EqHom f g)
      → isContrᵇ (Σ (LiftP (EqHom f g)) λ q → ⊤)

{-
 - The center of contraction of isContr-Obₗ
 -}
module _ (x : Ob) where
  center-Obₗ : Σ Ob λ y → Obᴱ x y
  center-Obₗ .fst = x
  center-Obₗ .snd .iso-f = id
  center-Obₗ .snd .iso-g = id
  center-Obₗ .snd .iso-fg = irefl
  center-Obₗ .snd .iso-gf = irefl

{-
 - The homogeneous "all-paths" operation of isContr-Obₗ
 -}
module _ (x : Ob) (xₑ : Obᴱ x x) (xᵣ : Obᴿ x xₑ)
         (yₗ : Ob) (fₗ : Obᴱ x yₗ)
         (yᵣ : Ob) (fᵣ : Obᴱ x yᵣ) where
  path-Obₗ : Σ (Obᴱ yₗ yᵣ) λ yₑ →
               Homᴱ xₑ yₑ (fₗ .iso-f) (fᵣ .iso-f)
             × Homᴱ yₑ xₑ (fₗ .iso-g) (fᵣ .iso-g)
  path-Obₗ .fst = fᵣ ∘i (xₑ ∘i inv fₗ)
  path-Obₗ .snd .fst = lift (unreflect (whisker (fᵣ .iso-f ∘ xₑ .iso-f) (reflect (fₗ .iso-gf)) id))
  path-Obₗ .snd .snd = lift (unreflect (whisker id (reflect (fᵣ .iso-gf) ⁻¹) (xₑ .iso-f ∘ fₗ .iso-g)))