module Cat.Displayed.Path where

open Precategory
open Displayed

Paths of displayed categories🔗

If you have a pair of displayed categories EB0\mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B}_0 and FB1\mathcal{F} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B}_1 over a line of precategories Bi,i:I\mathcal{B}_i, i : \mathbb{I}, it might be interesting — if you, like me, are a lunatic — to know when they can be connected by a PathP over B\mathcal{B}. This module answers that! A path between displayed categories, over a path of their corresponding bases, is a displayed functor

which is componentwise an equivalence.

The first step🔗

We write this proof in two steps: First, we write a helper function which abstracts over the contentful part of the path (the displayed object spaces, displayed Hom spaces, etc) and automatically fills in the proofs that the laws are preserved. We have a record displayed-pathp-data which contains paths for all the interesting components:

    record displayed-pathp-data : Type (lsuc (o ⊔ ℓ ⊔ o′ ⊔ ℓ′)) where
      no-eta-equality
      field
        obp  : PathP (λ i → B i .Ob → Type o′) E.Ob[_] F.Ob[_]
        homp : PathP
          (λ i → {x y : B i .Ob} (f : B i .Hom x y) → obp i x → obp i y → Type ℓ′)
          E.Hom[_] F.Hom[_]

The types get increasingly unhinged as we go: The identification between displayed object spaces lies over the identification of objects of the underlying category; The identification between displayed Hom spaces lies over a path in the base category and the path of displayed object spaces we just defined.

The paths between the identity morphisms and composite morphisms lie over both of those, and they have to quantify over every implicit argument inside the path! That’s why this record is in a private helper module, you see.

        idp : PathP (λ i → ∀ {x} {x′ : obp i x} → homp i (B i .id) x′ x′) E.id′ F.id′
        compp : PathP
          (λ i → ∀ {x y z}    {f : B i .Hom y z}    {g : B i .Hom x y}
               → ∀ {x′ y′ z′} (f′ : homp i f y′ z′) (g′ : homp i g x′ y′)
               → homp i (B i ._∘_ f g) x′ z′)
          E._∘′_ F._∘′_

An instance of this record determines a path of displayed categories,

    displayed-pathp-worker
      : displayed-pathp-data → PathP (λ i → Displayed (B i) o′ ℓ′) E F
    displayed-pathp-worker input = go where
      open displayed-pathp-data input

such that all the interesting components are literal, and the coherence components are, by definition, unimportant.

      go : PathP (λ i → Displayed (B i) o′ ℓ′) E F
      Ob[ go i ] x = obp i x
      Hom[ go i ] = homp i
      Hom[ go i ]-set {a} {b} f x y = homp-set i a b f x y
      go i .id′ = idp i
      go i ._∘′_ = compp i
      go i .idr′ {a} {b} {x} {y} {f} f′ j = is-set→squarep
        (λ i j     → Π-is-hlevel³ {A = B i .Ob} {B = λ _ → B i .Ob}      {C = λ a _ → obp i a}      2
          λ a b x  → Π-is-hlevel³ {A = obp i b} {B = λ _ → B i .Hom a b} {C = λ y f → homp i f x y} 2
          λ y f f′ → homp-set i a b (B i .idr f j) x y)
        (λ i a b x y f f′ → compp i f′ (idp i))
        (λ i a b x y f f′ → E .idr′ f′ i)
        (λ i a b x y f f′ → F .idr′ f′ i)
        (λ i a b x y f f′ → f′)
        i j a b x y f f′
      go i .idl′ {a} {b} {x} {y} {f} f′ j = is-set→squarep
        (λ i j    → Π-is-hlevel³ {A = B i .Ob} {B = λ _ → B i .Ob}      {C = λ a _ → obp i a}      2
          λ a b x  → Π-is-hlevel³ {A = obp i b} {B = λ _ → B i .Hom a b} {C = λ y f → homp i f x y} 2
          λ y f f′ → homp-set i a b (B i .idl f j) x y)
        (λ i a b x y f f′ → compp i (idp i) f′)
        (λ i a b x y f f′ → E .idl′ f′ i)
        (λ i a b x y f f′ → F .idl′ f′ i)
        (λ i a b x y f f′ → f′)
        i j a b x y f f′
      go i .assoc′ {a} {b} {c} {d} {w} {x} {y} {z} {f} {g} {h} f′ g′ h′ j = is-set→squarep
        (λ i j    → Π-is-hlevel³ {A = B i .Ob}      {B = λ _ → B i .Ob}      {C = λ _ _ → B i .Ob}      2
          λ a b c  → Π-is-hlevel³ {A = B i .Ob}      {B = λ _ → obp i a}      {C = λ _ _ → obp i b}      2
          λ d w x  → Π-is-hlevel³ {A = obp i c}      {B = λ _ → obp i d}      {C = λ _ - → B i .Hom c d} 2
          λ y z f  → Π-is-hlevel³ {A = B i .Hom b c} {B = λ _ → B i .Hom a b} {C = λ _ _ → homp i f y z} 2
          λ g h f′ → Π-is-hlevel² {A = homp i g x y} {B = λ _ → homp i h w x}                            2
          λ g′ h′  → homp-set i a d (B i .assoc f g h j) w z)
        (λ i a b c d w x y z f g h f′ g′ h′ → compp i f′ (compp i g′ h′))
        (λ i a b c d w x y z f g h f′ g′ h′ → E .assoc′ f′ g′ h′ i)
        (λ i a b c d w x y z f g h f′ g′ h′ → F .assoc′ f′ g′ h′ i)
        (λ i a b c d w x y z f g h f′ g′ h′ → compp i (compp i f′ g′) h′)
        i j a b c d w x y z f g h f′ g′ h′

Complicating it🔗

Suppose that we have EB\mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B} and FC\mathcal{F} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{C}, together with a functor F:B→CF : \mathcal{B} \to \mathcal{C} which is an isomorphism of precategories, and a functor G:E→FG : \mathcal{E} \to \mathcal{F} over FF. This is the situation in the introduction, but where the line Bi\mathcal{B}_i comes from the identity system on precategories given by isomorphisms of precategories.

The functor GG must be componentwise an isomorphism of types: This is the displayed equivalent of an isomorphism of precategories.

  Displayed-pathp
    : (eqv : is-precat-iso F)
    → (∀ a → is-equiv {A = ℰ.Ob[ a ]} G.F₀′)
    → ( ∀ {a b} {f} {a′ : ℰ.Ob[ a ]} {b′ : ℰ.Ob[ b ]}
      → is-equiv {A = ℰ.Hom[ f ] a′ b′} G.F₁′)
    → PathP (λ i → Displayed (Precategory-path F eqv i) o′ ℓ′) ℰ ℱ
  Displayed-pathp eqv obeqv homeqv = displayed-pathp-worker input where
    ps = Precategory-path F eqv

We’ll define a displayed-pathp-data. We define the paths between displayed object spaces and displayed path spaces by gluing against the ungluing of the paths in the underlying category, in the right endpoint category F\mathcal{F}. Diagramatically, this looks something like

    p1 : PathP (λ i → ps i .Ob → Type o′) ℰ.Ob[_] ℱ.Ob[_]
    p1 i x = Glue ℱ.Ob[ unglue (∂ i) x ] λ where
      (i = i0) → ℰ.Ob[ x ] , G.F₀′ , obeqv x
      (i = i1) → ℱ.Ob[ x ] , _ , id-equiv

We glue the type E[x]\mathcal{E}[x] along F0′F_0' — the action of the displayed functor on objects — against the line of types given by applying the space of displayed objects of F\mathcal{F} to the ungluing of xx, giving a line of type families p1 ranging from E[−]→F[−]\mathcal{E}[-] \to \mathcal{F}[-]. The situation for Hom spaces is analogous.

    sys : ∀ i (x y : ps i .Ob) (f : ps i .Hom x y) (x′ : p1 i x) (y′ : p1 i y)
        → Partial (i ∨ ~ i) _
    sys i x y f x′ y′ (i = i0) = ℰ.Hom[ f ] x′ y′ , G.F₁′ , homeqv
    sys i x y f x′ y′ (i = i1) = ℱ.Hom[ f ] x′ y′ , _ , id-equiv

    p2 : PathP
      (λ i → {x y : ps i .Ob} (f : ps i .Hom x y) → p1 i x → p1 i y → Type ℓ′)
      ℰ.Hom[_] ℱ.Hom[_]
    p2 i {x} {y} f x′ y′ = Glue
      (ℱ.Hom[ unglue (∂ i) f ] (unglue (∂ i) x′) (unglue (∂ i) y′))
      (sys i x y f x′ y′)

    open displayed-pathp-data
    input : displayed-pathp-data
    input .obp  = p1
    input .homp = p2

We now “just” have to produce inhabitants of p2 along i:Ii : \mathbb{I} which restrict to E\mathcal{E} and F\mathcal{F}’s identity morphisms (and composition morphisms) at the endoints of ii. We can do so by gluing, now at the level of terms, against a heterogeneous composition. The details are quite nasty, but the core of it is extending the witness that GG respects identity to a path, over line given by gluing F1′F_1' and ungluing the domain/codomain, between the identity maps in E\mathcal{E} and F\mathcal{F}.

    input .idp i {x} {x′} = glue-inc (∂ i)
      {Tf = sys i x x (ps i .id {x}) x′ x′}
      (λ { (i = i0) → ℰ.id′ ; (i = i1) → ℱ.id′ })
      (inS (comp (λ j → ℱ.Hom[ p (~ j) ] (unglue (∂ i) x′) (unglue (∂ i) x′)) (∂ i)
        λ { j (j = i0) → ℱ.id′
          ; j (i = i0) → G.F-id′ (~ j)
          ; j (i = i1) → ℱ.id′ }))
      where
        p : unglue (∂ i) (ps i .id {x}) ≡ C.id
        p j = hfill (∂ i) (~ j) λ where
          k (k = i0) → C.id
          k (i = i0) → F.F-id (~ k)
          k (i = i1) → C.id
The case for compositions is analogous and yet much nastier, so I won’t comment on it. You can’t make me.
    input .compp i {x} {y} {z} {f} {g} {x′} {y′} {z′} f′ g′ = glue-inc (∂ i)
        {Tf = sys i x z (ps i ._∘_ {x} {y} {z} f g) x′ z′}
        (λ { (i = i0) → f′ ℰ.∘′ g′ ; (i = i1) → f′ ℱ.∘′ g′ })
        (inS (comp (λ j → ℱ.Hom[ p j ] (unglue (∂ i) x′) (unglue (∂ i) z′)) (∂ i)
          λ { k (k = i0) →
                   unglue (∂ i) {T = λ .∂i=i1 → sys i y z f y′ z′ ∂i=i1 .fst} f′
              ℱ.∘′ unglue (∂ i) g′
            ; k (i = i0) → G.F-∘′ {f′ = f′} {g′ = g′} (~ k)
            ; k (i = i1) → f′ ℱ.∘′ g′ }))
      where
        p : I → C .Hom (unglue (i ∨ ~ i) x) (unglue (i ∨ ~ i) z)
        p j = hfill (∂ i) j λ where
          k (i = i0) → F.F-∘ f g (~ k)
          k (i = i1) → f C.∘ g
          k (k = i0) → unglue (∂ i) f C.∘ unglue (∂ i) g

As one last step, we show that if the functor GG is displayed over the identity, the path E→F\mathcal{E} \to \mathcal{F} is an actual identity, rather than a PathP.

  Displayed-path
    : (F₀-eqv : ∀ a → is-equiv F.₀′)
    → (F₁-eqv : ∀ {a b} {f : B .Hom a b} {a′ : ℰ.Ob[ a ]} {b′ : ℰ.Ob[ b ]}
              → is-equiv (F.₁′ {f = f} {a′ = a′} {b′ = b′}))
    → ℰ ≡ ℱ
  Displayed-path F₀-eqv F₁-eqv =
    transport
      (λ i → PathP
        (λ j → Displayed
          (to-path-refl {a = B} Precategory-identity-system i j) o′ ℓ′) ℰ ℱ)
      (Displayed-pathp Id F (iso id-equiv id-equiv) F₀-eqv F₁-eqv)