open import Cat.Functor.Equivalence.Path
open import Cat.Functor.Equivalence
open import Cat.Displayed.Functor
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Prelude

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.

private
  module
    _ {o β„“ oβ€² β„“β€²} {B : I β†’ Precategory o β„“}
      {E : Displayed (B i0) oβ€² β„“β€²}
      {F : Displayed (B i1) oβ€² β„“β€²}
    where
    private
      module E = Displayed E
      module F = Displayed F

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.

      homp-set :
        PathP
          (Ξ» i β†’ (a b : B i .Ob) (f : B i .Hom a b) (x : obp i a) (y : obp i b) β†’ is-set (homp i f x y))
          (Ξ» a b β†’ E .Hom[_]-set) Ξ» a b β†’ F .Hom[_]-set
      homp-set i a b f x y = is-prop→pathp
        (Ξ» i    β†’ Ξ -is-hlevelΒ³ {A = B i .Ob} {B = Ξ» _ β†’ B i .Ob} {C = Ξ» a b β†’ B i .Hom a b} 1
          Ξ» a b f β†’ Ξ -is-hlevelΒ² {A = obp i a} {B = Ξ» _ β†’ obp i b} 1
          Ξ» x y   β†’ is-hlevel-is-prop {A = homp i f x y} 2)
        (Ξ» _ _ β†’ E .Hom[_]-set) (Ξ» _ _ β†’ F .Hom[_]-set) i a b f x y

      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.

module
  _ {o β„“ oβ€² β„“β€²} {B C : Precategory o β„“} (F : Functor B C)
    {β„° : Displayed B oβ€² β„“β€²} {β„± : Displayed C oβ€² β„“β€²}
    (G : Displayed-functor β„° β„± F)
  where
  private
    module β„° = Displayed β„°
    module β„± = Displayed β„±
    module G = Displayed-functor G
    module C = Precategory C
    module F = Functor F

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

module
  _ {o β„“ oβ€² β„“β€²} {B : Precategory o β„“} {β„° β„± : Displayed B oβ€² β„“β€²}
    (F : Displayed-functor β„° β„± Id)
  where
  private
    module F = Displayed-functor F
    module β„° = Displayed β„°

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)