Directed polynomial as strict categories https://danel.ahman.ee/papers/msfp16.pdf

DPoly.agda

{-# OPTIONS --cubical #-}

module DPoly where

open import Cubical.Core.Everything
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels
open import Cubical.Categories.Category
open import Cubical.Data.Sigma

record DPoly (ℓ ℓ₁ : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ₁)) where
  infixr 8 _⨟_
  field
    ObSet : hSet ℓ
    HomSet : ⟨ ObSet ⟩ → hSet ℓ₁

  Ob : Type ℓ
  Ob = ⟨ ObSet ⟩

  Hom : Ob → Type ℓ₁
  Hom a = ⟨ HomSet a ⟩

  field
    tgt : {a : Ob} → Hom a → Ob
    id : {a : Ob} → Hom a
    _⨟_ : {a : Ob} → (f : Hom a) → (g : Hom (tgt f)) → Hom a
    tgt-id : {a : Ob} → tgt (id {a = a}) ≡ a
    tgt-⨟ : {a : Ob} → (f : Hom a) → (g : Hom (tgt f)) →
      tgt (f ⨟ g) ≡ tgt g
    id-⨟ˡ : {a : Ob} → (f : Hom a) → id ⨟ subst⁻ Hom tgt-id f ≡ f
    -- id-⨟ˡ : {a : Ob} → (λ (i : I) → Hom (tgt-id {a = a} i) → Hom a) [ (λ (f : Hom _) → id ⨟ f) ≡ (λ (f : Hom _) → f) ]
    id-⨟ʳ : {a : Ob} → (f : Hom a) → f ⨟ id ≡ f
    assoc-⨟ : {a : Ob} → (f : Hom a) → (g : Hom (tgt f)) → (h : Hom (tgt g)) →
      (f ⨟ g) ⨟ subst⁻ Hom (tgt-⨟ f g) h ≡ f ⨟ g ⨟ h

private variable
  ℓ : Level
  A : Type ℓ

module _ {ℓ ℓ₁} (D : DPoly ℓ ℓ₁) where
  open DPoly D

  assoc-⨟′ : {a : Ob} → (f : Hom a) → (g : Hom (tgt f)) → (h : Hom (tgt (f ⨟ g))) →
    (f ⨟ g) ⨟ h ≡ f ⨟ g ⨟ subst Hom (tgt-⨟ f g) h
  assoc-⨟′ f g h = cong ((f ⨟ g) ⨟_) (sym (subst⁻Subst Hom (tgt-⨟ f g) h)) ∙ assoc-⨟ f g (subst Hom (tgt-⨟ f g) h)

  refl-∙ʳ : ∀ {ℓ} {A : Type ℓ} {a b : A} (p : a ≡ b) → p ∙ refl ≡ p
  refl-∙ʳ p = sym (compPath-filler p refl)

  flip-J : ∀ {ℓ₁} {A : Type ℓ} {x : A} (P : ∀ y → x ≡ y → Type ℓ₁) {y} → (p : x ≡ y) → (d : P x refl) → P y p
  flip-J P p d = J P d p

  private
    Hom[_,_] : Ob → Ob → Type (ℓ-max ℓ ℓ₁)
    Hom[ a , b ] = Σ[ f ∈ Hom a ] tgt f ≡ b

    Id : {a : Ob} → Hom[ a , a ]
    Id = id , tgt-id

    _⋆_ : {a b c : Ob} → Hom[ a , b ] → Hom[ b , c ] → Hom[ a , c ]
    _⋆_ {x} {y} {z} (f , tgt-f≡y) (g , tgt-g≡z) = (f ⨟ subst⁻ Hom tgt-f≡y g) ,
      ( tgt (f ⨟ subst⁻ Hom tgt-f≡y g)
        ≡⟨ tgt-⨟ f _ ⟩
        tgt (subst⁻ Hom tgt-f≡y g)
        ≡⟨ congP₂ (λ i a → tgt {a = a}) tgt-f≡y (symP (subst⁻-filler Hom tgt-f≡y g)) ⟩
        tgt-g≡z
      )

  aux : {a : Ob} → (f : I -> Hom a) → (g : ∀ i → Hom (tgt (f i))) → (h : ∀ i → Hom (tgt (f i ⨟ g i))) → (f i0 ⨟ g i0) ⨟ h i0 ≡ (f i1 ⨟ g i1) ⨟ h i1
  aux f g h = λ i → (f i ⨟ g i) ⨟ h i

  private module _ {a : Ob} (f : Hom a) (g : Hom (tgt f)) (h : Hom (tgt g)) where
    private
      f′ : f ≡ f
      f′ = refl

      g′ : subst⁻ Hom refl g ≡ g
      g′ i = subst⁻-filler Hom refl g (~ i)

      subst⁻Composite : {A : Type ℓ} (B : A → Type ℓ₁) {x y z : A} (p : x ≡ y) (q : y ≡ z) (u : B z)
        → subst⁻ B (p ∙ q) u ≡ subst⁻ B p (subst⁻ B q u)
      subst⁻Composite B p q u i = transport⁻-fillerExt (cong B p) i (transport⁻ (cong B (compPath-filler' p q (~ i))) u)

      h2 : subst⁻ Hom (snd ((f , refl) ⋆ (g , refl))) h
          ≡ subst⁻ Hom (tgt-⨟ f _) (subst⁻ Hom (cong tgt g′) h)
      h2 = x {p₁ = tgt-⨟ f _} where
        x : ∀ {a b c : Ob} {p₁ : a ≡ b} {p₂ : b ≡ c} {h : Hom c} →
          subst⁻ Hom (p₁ ∙ p₂ ∙ refl) h ≡ subst⁻ Hom p₁ (subst⁻ Hom p₂ h)
        x {p₁ = p₁} {p₂ = p₂} {h = h} =
          cong (λ p → subst⁻ Hom (p₁ ∙ p) h) (refl-∙ʳ p₂) ∙
          subst⁻Composite Hom p₁ p₂ _

      h1′ : PathP (λ i → Hom (tgt (g′ i))) (subst⁻ Hom (cong tgt g′) h) h 
      h1′ = symP (subst⁻-filler (Hom ∘ tgt) g′ h)

      h1 : PathP (λ i → Hom (tgt (f ⨟ g′ i)))
             (subst⁻ Hom (tgt-⨟ f _) (subst⁻ Hom (cong tgt g′) h))
             (subst⁻ Hom (tgt-⨟ f _) h)
      h1 = congP (λ i → subst⁻ Hom (tgt-⨟ f (g′ i))) h1′

      h′ : PathP (λ i → Hom (tgt (f ⨟ g′ i)))
             (subst⁻ Hom (snd ((f , refl) ⋆ (g , refl))) h)
             (subst⁻ Hom (tgt-⨟ f g) h)
      h′ = h2 ◁ h1

    fgh : (f ⨟ subst⁻ Hom refl g) ⨟ subst⁻ Hom (snd ((f , refl) ⋆ (g , refl))) h
        ≡ (f ⨟ g) ⨟ subst⁻ Hom (tgt-⨟ f g) h
    fgh = aux (λ i → f) (λ i → g′ i) (λ i → h′ i)

  ⋆-refl-assoc : {a : Ob} → (f : Hom a) → (g : Hom (tgt f)) → (h : Hom (tgt g)) →
    ((f , refl) ⋆ (g , refl)) ⋆ (h , refl) ≡ (f , refl) ⋆ ((g , refl) ⋆ (h , refl))
  ⋆-refl-assoc f g h =
    Σ≡Prop (λ _ → str ObSet _ _)
      ( ((f ⨟ subst⁻ Hom refl g) ⨟ subst⁻ Hom (snd ((f , refl) ⋆ (g , refl))) h)
      ≡⟨ fgh f g h ⟩
        (f ⨟ g) ⨟ subst⁻ Hom (tgt-⨟ f g) h
      ≡⟨ assoc-⨟ f g h ⟩
        f ⨟ (g ⨟ h)
      ≡⟨ cong (λ h′ → f ⨟ (g ⨟ h′)) (subst⁻-filler Hom refl _) ⟩
        f ⨟ (g ⨟ subst⁻ Hom refl h)
      ≡⟨ cong (f ⨟_) (subst⁻-filler Hom refl _) ⟩
        f ⨟ subst⁻ Hom refl (g ⨟ subst⁻ Hom refl h)
      ∎)

  private
    IdR : {a b : Ob} → (f : Hom[ a , b ]) → f ⋆ Id ≡ f
    IdR (f , tgt-f≡) =
      let p₁ = f ⨟ subst⁻ Hom refl id
           ≡⟨ cong (f ⨟_) (sym (subst⁻-filler Hom refl id)) ⟩
           f ⨟ id
           ≡⟨ id-⨟ʳ f ⟩
           f
           ∎
      in
      J (λ b r → (f , r) ⋆ Id ≡ (f , r)) (Σ≡Prop (λ _ → str ObSet _ _) p₁) tgt-f≡

    IdL : {a b : Ob} → (f : Hom[ a , b ]) → Id ⋆ f ≡ f
    IdL (f , tgt-f≡) = Σ≡Prop (λ _ → str ObSet _ _) (id-⨟ˡ f)

    Assoc : ∀ {a b c d : Ob} (f : Hom[ a , b ]) (g : Hom[ b , c ]) (h : Hom[ c , d ]) →
      (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)
    Assoc =
      λ{ (f , tgt-f≡) → flip-J (λ b r → ∀ g h → ((f , r) ⋆ g) ⋆ h ≡ (f , r) ⋆ (g ⋆ h)) tgt-f≡
      λ{ (g , tgt-g≡) → flip-J (λ b r → ∀ h → ((_ ⋆ (g , r)) ⋆ h ≡ _ ⋆ ((g , r) ⋆ h))) tgt-g≡
      λ{ (h , tgt-h≡) → flip-J (λ b r → (((f , refl) ⋆ _) ⋆ (h , r) ≡ _ ⋆ (_ ⋆ (h , r)))) tgt-h≡
       (⋆-refl-assoc f g h)
       }}}

    isSetHom : ∀ {x y} → isSet Hom[ x , y ]
    isSetHom = isSetΣSndProp (str (HomSet _)) (λ _ → str ObSet _ _)

  DPoly-to-Cat : Category ℓ (ℓ-max ℓ ℓ₁)
  DPoly-to-Cat = λ where
    .Category.ob → Ob
    .Category.Hom[_,_] → Hom[_,_]
    .Category.id → Id
    .Category._⋆_ → _⋆_
    .Category.⋆IdR → IdR
    .Category.⋆IdL → IdL
    .Category.⋆Assoc → Assoc
    .Category.isSetHom → isSetHom

module _ {ℓ ℓ₁} (C : Category ℓ ℓ₁) (open Category C) (isSetOb : isSet ob) where

  private
    Hom : ob → Type (ℓ-max ℓ ℓ₁)
    Hom a = Σ[ b ∈ ob ] Hom[ a , b ]

    id-⨟ˡ : ∀ {a b : ob} (f : Hom[ a , b ]) →
      let (b′ , f′) = subst⁻ Hom refl (b , f) in
      Path (Hom a) (b′ , id ⋆ f′) (b , f)
    id-⨟ˡ f = congS (λ{ (b′ , f′) → (b′ , id ⋆ f′) }) (sym (subst⁻-filler Hom refl (_ , f)))
            ∙ congS (_ ,_) (⋆IdL f)

    assoc-⨟ : ∀ {a b c d : ob} (f : Hom[ a , b ]) (g : Hom[ b , c ]) (h : Hom[ c , d ]) →
      let (d′ , h′) = subst⁻ Hom refl (d , h) in
      Path (Hom a) (d′ , (f ⋆ g) ⋆ h′) (d , f ⋆ (g ⋆ h))
    assoc-⨟ f g h
      = congS (λ{ (d′ , h′) → (d′ , (f ⋆ g) ⋆ h′) }) (sym (subst⁻-filler Hom refl (_ , h)))
      ∙ congS (_ ,_) (⋆Assoc f g h)

  Cat-to-DPoly : DPoly ℓ (ℓ-max ℓ ℓ₁)
  Cat-to-DPoly = λ where
    .DPoly.ObSet → ob , isSetOb
    .DPoly.HomSet a → Hom a , isSetΣ isSetOb (λ _ → isSetHom)
    .DPoly.id → _ , id
    .DPoly.tgt → fst
    .DPoly.tgt-id → refl
    .DPoly._⨟_ (_ , f) (_ , g) → _ , f ⋆ g
    .DPoly.tgt-⨟ f g → refl
    .DPoly.id-⨟ˡ (_ , f) → id-⨟ˡ f
    .DPoly.id-⨟ʳ (_ , f) → cong (_ ,_) (⋆IdR f)
    .DPoly.assoc-⨟ (_ , f) (_ , g) (_ , h) → (assoc-⨟ f g h)