open import Cat.Displayed.Instances.DisplayedFunctor hiding (_β—†'_)
open import Cat.Displayed.Instances.TotalProduct
open import Cat.Displayed.Functor.Naturality
open import Cat.Displayed.Morphism
open import Cat.Displayed.Functor
open import Cat.Instances.Product
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Bi.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning as DR
module Cat.Bi.Displayed.Base where

Displayed bicategoriesπŸ”—

Source

The definition here was adapted from the one given by Ahrens et al. (2022)

Just as a displayed category allows us to describe categorical structure over the category a displayed bicategory allows us to describe bicategorical structure over the bicategory 

open Functor
open Displayed-functor
open _=[_]=>_
open make-natural-iso[_]

module _ where
 
  compose-assocΛ‘' : βˆ€ {o o' d d' β„“ β„“'} {O : Type o} {H : O β†’ O β†’ Precategory β„“ β„“'}
                  β†’ {O' : O β†’ Type o'} {H' : βˆ€ {a b} β†’ O' a β†’ O' b β†’ Displayed (H a b) d d'}
                  β†’ {F : βˆ€ {A B C} β†’ Functor (H B C Γ—αΆœ H A B) (H A C)}
                  β†’ (F' : βˆ€ {A B C} {A' : O' A} {B' : O' B} {C' : O' C} β†’ Displayed-functor F (H' B' C' Γ—α΅€α΄° H' A' B') (H' A' C'))
                  β†’ βˆ€ {A B C D} {A' : O' A} {B' : O' B} {C' : O' C} {D' : O' D} 
                  β†’ Displayed-functor (compose-assocΛ‘ {O = O} {H = H} F) (H' C' D' Γ—α΅€α΄° H' B' C' Γ—α΅€α΄° H' A' B') (H' A' D')
  compose-assocΛ‘' F' .Fβ‚€' (F , G , H) = F' .Fβ‚€' (F' .Fβ‚€' (F , G) , H)
  compose-assocΛ‘' F' .F₁' (f , g , h) = F' .F₁' (F' .F₁' (f , g) , h)
  compose-assocΛ‘' {H' = H'} F' {A' = A'} {D' = D'} .F-id' = 
    cast[] (apd (Ξ» _ β†’ F' .F₁') (F' .F-id' ,β‚š refl) βˆ™[] (F' .F-id')) 
    where 
      open DR (H' A' D')
  compose-assocˑ' {H' = H'} F' {A' = A'} {D' = D'} .F-∘' = 
    cast[] (apd (Ξ» _ β†’ F' .F₁') (F' .F-∘' ,β‚š refl) βˆ™[] F' .F-∘')
    where 
      open DR (H' A' D')

  compose-assocΚ³' : βˆ€ {o o' d d' β„“ β„“'} {O : Type o} {H : O β†’ O β†’ Precategory β„“ β„“'}
                   β†’ {O' : O β†’ Type o'} {H' : βˆ€ {a b} β†’ O' a β†’ O' b β†’ Displayed (H a b) d d'}
                   β†’ {F : βˆ€ {A B C} β†’ Functor (H B C Γ—αΆœ H A B) (H A C)}
                   β†’ (F' : βˆ€ {A B C} {A' : O' A} {B' : O' B} {C' : O' C}
                         β†’ Displayed-functor F (H' B' C' Γ—α΅€α΄° H' A' B') (H' A' C'))
                   β†’ βˆ€ {A B C D} {A' : O' A} {B' : O' B} {C' : O' C} {D' : O' D}
                   β†’ Displayed-functor (compose-assocΚ³ {O = O} {H = H} F)
                                       (H' C' D' Γ—α΅€α΄° H' B' C' Γ—α΅€α΄° H' A' B') (H' A' D')
  compose-assocΚ³' F' .Fβ‚€' (F , G , H) = F' .Fβ‚€' (F , F' .Fβ‚€' (G , H))
  compose-assocΚ³' F' .F₁' (f , g , h) = F' .F₁' (f , F' .F₁' (g , h))
  compose-assocΚ³' {H' = H'} F' {A' = A'} {D' = D'} .F-id' =
    cast[] (apd (Ξ» _ β†’ F' .F₁') (refl ,β‚š F' .F-id') βˆ™[] F' .F-id')
    where
      open DR (H' A' D')
  compose-assocʳ' {H' = H'} F' {A' = A'} {D' = D'} .F-∘' =
    cast[] (apd (Ξ» _ β†’ F' .F₁') (refl ,β‚š F' .F-∘') βˆ™[] F' .F-∘')
    where
      open DR (H' A' D')
record Bidisplayed {o oh β„“h} (B : Prebicategory o oh β„“h) o' oh' β„“h' : Type (lsuc (o' βŠ” oh' βŠ” β„“h') βŠ” o βŠ” oh βŠ” β„“h) where
  no-eta-equality
  open Prebicategory B

For each object of the base bicateogry, we have a type of displayed objects indexed over it.

  field
    Ob[_] : Ob β†’ Type o'

For any two displayed objects, we have a category displayed over the category of their bases.

    Hom[_,_] : βˆ€ {A B} β†’ Ob[ A ] β†’ Ob[ B ] β†’ Displayed (Hom A B) oh' β„“h'

  module Hom[] {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} = Displayed (Hom[ A' , B' ])

The displayed objects of these displayed categories are the displayed 1-cells. The displayed morphims are the displayed 2-cells.

  _[_]↦_ : βˆ€ {A B} β†’ Ob[ A ] β†’ (A ↦ B) β†’ Ob[ B ] β†’ Type _
  A' [ f ]↦ B' = Hom[ A' , B' ] .Displayed.Ob[_] f


  _[_]β‡’_ : βˆ€ {A B} {f g : A ↦ B} 
         β†’ {A' : Ob[ A ]} {B' : Ob[ B ]} 
         β†’ A' [ f ]↦ B' β†’ (f β‡’ g) β†’ A' [ g ]↦ B'
         β†’ Type _
  _[_]β‡’_ {A' = A'} {B' = B'} f' Ξ± g' = Hom[ A' , B' ] .Displayed.Hom[_] Ξ± f' g'

We require an identity 1-cell displayed over the identity 1-cell of the base bicategory.

  field
    ↦id' : βˆ€ {x} {x' : Ob[ x ]} β†’ x' [ id ]↦ x'

We get displayed identity 2-cells automatically from the displayed structure.

  β‡’id' : βˆ€ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]}
      β†’ {f : A ↦ B} {f' : A' [ f ]↦ B'}
      β†’ f' [ Hom.id ]β‡’ f'
  β‡’id' = Hom[].id'

The displayed composition functor is between total products of displayed categories, and lies over the composition functor of the base bicategory.

  field
    compose' : βˆ€ {A B C} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} 
             β†’ Displayed-functor compose (Hom[ B' , C' ] Γ—α΅€α΄° Hom[ A' , B' ]) Hom[ A' , C' ]
    
  module compose' {A} {B} {C} {A'} {B'} {C'} = Displayed-functor (compose' {A} {B} {C} {A'} {B'} {C'})

Displayed 1-cell and 2-cell composition proceeds in the same way.

  _βŠ—'_ : βˆ€ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B} β†’ (B' [ f ]↦ C') β†’ (A' [ g ]↦ B') β†’ A' [ f βŠ— g ]↦ C'
  _βŠ—'_ f' g' = compose'.β‚€' (f' , g') 

  _∘'_ : βˆ€ {A B A' B'} {f g h : A ↦ B} 
      β†’ {f' : A' [ f ]↦ B'} {g' : A' [ g ]↦ B'} {h' : A' [ h ]↦ B'}
      β†’ {Ξ² : g β‡’ h} {Ξ± : f β‡’ g} 
      β†’ g' [ Ξ² ]β‡’ h' β†’ f' [ Ξ± ]β‡’ g'
      β†’ f' [ Ξ² ∘ Ξ± ]β‡’ h'
  _∘'_ = Hom[]._∘'_

  _β—†'_ : βˆ€ {A B C A' B' C'} 
       β†’ {f₁ fβ‚‚ : B ↦ C} {Ξ² : f₁ β‡’ fβ‚‚} 
       β†’ {g₁ gβ‚‚ : A ↦ B} {Ξ± : g₁ β‡’ gβ‚‚}
       β†’ {f₁' : B' [ f₁ ]↦ C'} {fβ‚‚' : B' [ fβ‚‚ ]↦ C'}
       β†’ {g₁' : A' [ g₁ ]↦ B'} {gβ‚‚' : A' [ gβ‚‚ ]↦ B'}
       β†’ (Ξ²' : f₁' [ Ξ² ]β‡’ fβ‚‚') (Ξ±' : g₁' [ Ξ± ]β‡’ gβ‚‚')
       β†’ (f₁' βŠ—' g₁') [ Ξ² β—† Ξ± ]β‡’ (fβ‚‚' βŠ—' gβ‚‚') 
  _β—†'_ Ξ±' Ξ²' = compose'.₁' (Ξ±' , Ξ²')

  infixr 30 _∘'_
  infixr 25 _βŠ—'_
  infix 35 _β—€'_ _β–Ά'_

  _β–Ά'_ : βˆ€ {A B C A' B' C'} {f : B ↦ C} {g₁ gβ‚‚ : A ↦ B} {Ξ± : g₁ β‡’ gβ‚‚}
        β†’ {g₁' : A' [ g₁ ]↦ B'} {gβ‚‚' : A' [ gβ‚‚ ]↦ B'} 
        β†’ (f' : B' [ f ]↦ C')
        β†’ (Ξ±' : g₁' [ Ξ± ]β‡’ gβ‚‚')
        β†’ f' βŠ—' g₁' [ f β–Ά Ξ± ]β‡’ f' βŠ—' gβ‚‚'
  _β–Ά'_ f' Ξ±' = compose'.₁' (β‡’id' , Ξ±')


  _β—€'_ : βˆ€ {A B C A' B' C'} {g : A ↦ B} {f₁ fβ‚‚ : B ↦ C} {Ξ² : f₁ β‡’ fβ‚‚}
        β†’ {f₁' : B' [ f₁ ]↦ C'} {fβ‚‚' : B' [ fβ‚‚ ]↦ C'} 
        β†’ (Ξ²' : f₁' [ Ξ² ]β‡’ fβ‚‚')
        β†’ (g' : A' [ g ]↦ B')
        β†’ f₁' βŠ—' g' [ Ξ² β—€ g ]β‡’ fβ‚‚' βŠ—' g'
  _β—€'_ Ξ²' g' = compose'.₁' (Ξ²' , β‡’id')

The unitors and associator are displayed isomorphims over the unitors and associator the base bicategory.

  field
    unitor-l' : βˆ€ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} β†’ Id' {β„° = Hom[ A' , B' ]} β‰…[ unitor-l ]ⁿ (Right' compose' ↦id')
    unitor-r' : βˆ€ {A B} {A' : Ob[ A ]} {B' : Ob[ B ]} β†’ Id' {β„° = Hom[ A' , B' ]} β‰…[ unitor-r ]ⁿ (Left'  compose' ↦id')

    associator' : βˆ€ {A B C D} {A' : Ob[ A ]} {B' : Ob[ B ]} {C' : Ob[ C ]} {D' : Ob[ D ]}
                β†’ _β‰…[_]_ Disp[ Hom[ C' , D' ] Γ—α΅€α΄° (Hom[ B' , C' ] Γ—α΅€α΄° Hom[ A' , B' ]) , Hom[ A' , D' ] ] 
                  (compose-assocΛ‘' {H' = Hom[_,_]}  compose') associator (compose-assocΚ³' {H' = Hom[_,_]}  compose')
    
  module unitor-l' {A} {B} {A'} {B'} = _β‰…[_]_ (unitor-l' {A} {B} {A'} {B'})
  module unitor-r' {A} {B} {A'} {B'} = _β‰…[_]_ (unitor-r' {A} {B} {A'} {B'})
  module associator' {A} {B} {C} {D} {A'} {B'} {C'} {D'} = _β‰…[_]_ (associator' {A} {B} {C} {D} {A'} {B'} {C'} {D'})

The associated displayed cell combinators proceed in the same way.

  λ←' : βˆ€ {A B A' B'} {f : A ↦ B} (f' : A' [ f ]↦ B') β†’ (↦id' βŠ—' f') [ λ← f ]β‡’ f'
  λ←' = unitor-l'.from' .Ξ·' 

  Ξ»β†’' : βˆ€ {A B A' B'} {f : A ↦ B}
       β†’ (f' : A' [ f ]↦ B')
       β†’ f' [ Ξ»β†’ f ]β‡’ (↦id' βŠ—' f')
  Ξ»β†’' = unitor-l'.to' .Ξ·'

  ρ←' : βˆ€ {A B A' B'} {f : A ↦ B}
       β†’ (f' : A' [ f ]↦ B')
       β†’ (f' βŠ—' ↦id') [ ρ← f ]β‡’ f'
  ρ←' = unitor-r'.from' .Ξ·'

  ρ→' : βˆ€ {A B A' B'} {f : A ↦ B}
       β†’ (f' : A' [ f ]↦ B')
       β†’ f' [ ρ→ f ]β‡’ (f' βŠ—' ↦id')
  ρ→' = unitor-r'.to' .Ξ·'

  ρ←nat' : βˆ€ {A B A' B'} {f₁ fβ‚‚ : A ↦ B} {Ξ² : f₁ β‡’ fβ‚‚}
         β†’ {f₁' : A' [ f₁ ]↦ B'} {fβ‚‚' : A' [ fβ‚‚ ]↦ B'}
         β†’ (Ξ²' : f₁' [ Ξ² ]β‡’ fβ‚‚')
         β†’ (ρ←' _ ∘' (Ξ²' β—€' ↦id')) Hom[].≑[ ρ←nat Ξ² ] (Ξ²' ∘' ρ←' _)
  ρ←nat' Ξ²' = unitor-r'.from' .is-natural' _ _ Ξ²'

  λ←nat' : βˆ€ {A B A' B'} {f₁ fβ‚‚ : A ↦ B} {Ξ² : f₁ β‡’ fβ‚‚}
         β†’ {f₁' : A' [ f₁ ]↦ B'} {fβ‚‚' : A' [ fβ‚‚ ]↦ B'}
         β†’ (Ξ²' : f₁' [ Ξ² ]β‡’ fβ‚‚')
         β†’ (λ←' _ ∘' (↦id' β–Ά' Ξ²')) Hom[].≑[ λ←nat Ξ² ] (Ξ²' ∘' λ←' _)
  λ←nat' Ξ²' = unitor-l'.from' .is-natural' _ _ Ξ²'

  ρ→nat' : βˆ€ {A B A' B'} {f₁ fβ‚‚ : A ↦ B} {Ξ² : f₁ β‡’ fβ‚‚}
         β†’ {f₁' : A' [ f₁ ]↦ B'} {fβ‚‚' : A' [ fβ‚‚ ]↦ B'}
         β†’ (Ξ²' : f₁' [ Ξ² ]β‡’ fβ‚‚')
         β†’ (ρ→' _ ∘' Ξ²') Hom[].≑[ ρ→nat Ξ² ] ((Ξ²' β—€' ↦id') ∘' ρ→' _)
  ρ→nat' Ξ²' = unitor-r'.to' .is-natural' _ _ Ξ²'

  Ξ»β†’nat' : βˆ€ {A B A' B'} {f₁ fβ‚‚ : A ↦ B} {Ξ² : f₁ β‡’ fβ‚‚}
         β†’ {f₁' : A' [ f₁ ]↦ B'} {fβ‚‚' : A' [ fβ‚‚ ]↦ B'}
         β†’ (Ξ²' : f₁' [ Ξ² ]β‡’ fβ‚‚')
         β†’ (Ξ»β†’' _ ∘' Ξ²') Hom[].≑[ Ξ»β†’nat Ξ² ] ((↦id' β–Ά' Ξ²') ∘' Ξ»β†’' _)
  Ξ»β†’nat' Ξ²' = unitor-l'.to' .is-natural' _ _ Ξ²'

  Ξ±β†’' : βˆ€ {A B C D A' B' C' D'}
       {f : C ↦ D} {g : B ↦ C} {h : A ↦ B}
       β†’ (f' : C' [ f ]↦ D') (g' : B' [ g ]↦ C') (h' : A' [ h ]↦ B')
       β†’ ((f' βŠ—' g') βŠ—' h') [ Ξ±β†’ f g h ]β‡’ (f' βŠ—' (g' βŠ—' h'))
  Ξ±β†’' f' g' h' = associator'.to' .Ξ·' (f' , g' , h')

  α←' : βˆ€ {A B C D A' B' C' D'}
       {f : C ↦ D} {g : B ↦ C} {h : A ↦ B}
       β†’ (f' : C' [ f ]↦ D') (g' : B' [ g ]↦ C') (h' : A' [ h ]↦ B')
       β†’ (f' βŠ—' (g' βŠ—' h')) [ α← f g h ]β‡’ ((f' βŠ—' g') βŠ—' h')
  α←' f' g' h' = associator'.from' .Ξ·' (f' , g' , h')

  α←nat' : βˆ€ {A B C D A' B' C' D'}
         {f₁ fβ‚‚ : C ↦ D} {g₁ gβ‚‚ : B ↦ C} {h₁ hβ‚‚ : A ↦ B}
         {Ξ² : f₁ β‡’ fβ‚‚} {Ξ³ : g₁ β‡’ gβ‚‚} {Ξ΄ : h₁ β‡’ hβ‚‚}
         {f₁' : C' [ f₁ ]↦ D'} {fβ‚‚' : C' [ fβ‚‚ ]↦ D'}
         {g₁' : B' [ g₁ ]↦ C'} {gβ‚‚' : B' [ gβ‚‚ ]↦ C'}
         {h₁' : A' [ h₁ ]↦ B'} {hβ‚‚' : A' [ hβ‚‚ ]↦ B'}
         β†’ (Ξ²' : f₁' [ Ξ² ]β‡’ fβ‚‚') (Ξ³' : g₁' [ Ξ³ ]β‡’ gβ‚‚') (Ξ΄' : h₁' [ Ξ΄ ]β‡’ hβ‚‚')
         β†’ (α←' _ _ _ ∘' (Ξ²' β—†' (Ξ³' β—†' Ξ΄'))) Hom[].≑[ α←nat Ξ² Ξ³ Ξ΄ ]
              (((Ξ²' β—†' Ξ³') β—†' Ξ΄') ∘' α←' _ _ _)
  α←nat' Ξ²' Ξ³' Ξ΄' =
    associator'.from' .is-natural' (_ , _ , _) (_ , _ , _) (Ξ²' , Ξ³' , Ξ΄')

  Ξ±β†’nat' : βˆ€ {A B C D A' B' C' D'}
         {f₁ fβ‚‚ : C ↦ D} {g₁ gβ‚‚ : B ↦ C} {h₁ hβ‚‚ : A ↦ B}
         {Ξ² : f₁ β‡’ fβ‚‚} {Ξ³ : g₁ β‡’ gβ‚‚} {Ξ΄ : h₁ β‡’ hβ‚‚}
         {f₁' : C' [ f₁ ]↦ D'} {fβ‚‚' : C' [ fβ‚‚ ]↦ D'}
         {g₁' : B' [ g₁ ]↦ C'} {gβ‚‚' : B' [ gβ‚‚ ]↦ C'}
         {h₁' : A' [ h₁ ]↦ B'} {hβ‚‚' : A' [ hβ‚‚ ]↦ B'}
         β†’ (Ξ²' : f₁' [ Ξ² ]β‡’ fβ‚‚') (Ξ³' : g₁' [ Ξ³ ]β‡’ gβ‚‚') (Ξ΄' : h₁' [ Ξ΄ ]β‡’ hβ‚‚')
         β†’ (Ξ±β†’' _ _ _ ∘' ((Ξ²' β—†' Ξ³') β—†' Ξ΄')) Hom[].≑[ Ξ±β†’nat Ξ² Ξ³ Ξ΄ ]
              ((Ξ²' β—†' (Ξ³' β—†' Ξ΄')) ∘' Ξ±β†’' _ _ _)
  Ξ±β†’nat' Ξ²' Ξ³' Ξ΄' =
    associator'.to' .is-natural' (_ , _ , _) (_ , _ , _) (Ξ²' , Ξ³' , Ξ΄')

As do the triangle and pentagon identities.

  field
    triangle' 
      : βˆ€ {A B C A' B' C'} {f : B ↦ C} {g : A ↦ B}
      β†’ (f' : B' [ f ]↦ C') (g' : A' [ g ]↦ B')
      β†’ ((ρ←' f' β—€' g') ∘' α←' f' ↦id' g') Hom[].≑[ triangle f g ] (f' β–Ά' λ←' g')

    pentagon'
      : βˆ€ {A B C D E A' B' C' D' E'}
      β†’ {f : D ↦ E} {g : C ↦ D} {h : B ↦ C} {i : A ↦ B}
      β†’ (f' : D' [ f ]↦ E')
      β†’ (g' : C' [ g ]↦ D')
      β†’ (h' : B' [ h ]↦ C')
      β†’ (i' : A' [ i ]↦ B')
      β†’ ((α←' f' g' h' β—€' i') ∘' α←' f' (g' βŠ—' h') i' ∘' (f' β–Ά' α←' g' h' i'))
          Hom[].≑[ pentagon f g h i ]
          (α←' (f' βŠ—' g') h' i' ∘' α←' f' g' (h' βŠ—' i'))

The displayed bicategory of displayed categoriesπŸ”—

Displayed categories naturally assemble into a displayed biacategory over with displayed functor categories as 

open Bidisplayed hiding (_∘'_)
Displayed-cat : βˆ€ o β„“ o' β„“' β†’ Bidisplayed (Cat o β„“) _ _ _
Displayed-cat o β„“ o' β„“' .Ob[_] C = Displayed C o' β„“'
Displayed-cat o β„“ o' β„“' .Hom[_,_] D E = Disp[ D , E ]
Displayed-cat o β„“ o' β„“' .↦id' = Id'
Displayed-cat o β„“ o' β„“' .compose' = F∘'-functor
Displayed-cat o β„“ o' β„“' .unitor-l' {B' = B'} = to-natural-iso' ni where
  open DR B'
  ni : make-natural-iso[ _ ] _ _
  ni .eta' x' = NT' (Ξ» _ β†’ id') Ξ» _ _ _ β†’ id-comm-sym[]
  ni .inv' x' = NT' (Ξ» _ β†’ id') Ξ» _ _ _ β†’ id-comm-sym[]
  ni .eta∘inv' x' = Nat'-path Ξ» x'' β†’ idl' _
  ni .inv∘eta' x' = Nat'-path Ξ» x'' β†’ idl' _
  ni .natural' x' y' f' = Nat'-path Ξ» x'' β†’ cast[] $ symP $ (idr' _ βˆ™[] id-comm[])

Displayed-cat o β„“ o' β„“' .unitor-r' {B' = B'} = to-natural-iso' ni where
  open DR B'
  ni : make-natural-iso[ _ ] _ _
  ni .eta' x' = NT' (Ξ» _ β†’ id') Ξ» _ _ _ β†’ id-comm-sym[]
  ni .inv' x' = NT' (Ξ» _ β†’ id') Ξ» _ _ _ β†’ id-comm-sym[]
  ni .eta∘inv' x' = Nat'-path Ξ» x'' β†’ idl' _
  ni .inv∘eta' x' = Nat'-path Ξ» x'' β†’ idl' _
  ni .natural' x' y' f' = Nat'-path Ξ» x'' β†’ cast[] $ (idl' _ βˆ™[] symP (idr' _ βˆ™[] ((y' .F-id' ⟩∘'⟨refl) βˆ™[] idl' _)))
  
Displayed-cat o β„“ o' β„“' .associator' {C' = C'} {D' = D'} = to-natural-iso' ni where
  open DR D'
  module C' = Displayed C'
  ni : make-natural-iso[ _ ] _ _ 
  ni .eta' x' = NT' (Ξ» _ β†’ id') Ξ» _ _ _ β†’ id-comm-sym[]
  ni .inv' x' = NT' (Ξ» _ β†’ id') Ξ» _ _ _ β†’ id-comm-sym[]
  ni .eta∘inv' x' = Nat'-path (Ξ» _ β†’ idl' _)
  ni .inv∘eta' x' = Nat'-path (Ξ» _ β†’ idl' _)
  ni .natural' (x₁ , xβ‚‚ , x₃) (y₁ , yβ‚‚ , y₃) (α₁ , Ξ±β‚‚ , α₃) = Nat'-path Ξ» z β†’ cast[] $
    (idl' _ βˆ™[] symP (pushl[] _ (y₁ .F-∘')) βˆ™[] symP (idr' _))

Displayed-cat o β„“ o' β„“' .triangle' {B' = B'} {C' = C'} f' g' = Nat'-path Ξ» x' β†’ C'.idr' _ where
  module C' = Displayed C'
Displayed-cat o β„“ o' β„“' .pentagon' {B' = B'} {C' = C'} {D' = D'} {E' = E'} f' g' h' i' = Nat'-path Ξ» x' β†’ cast[] $
  (f' .F₁' (g' .F₁' (h' .F₁' B'.id')) ∘' id') ∘' (id' ∘' f' .F₁' D'.id' ∘' id') ≑[]⟨ idr' _ ⟩∘'⟨ idl' _ ⟩
  (f' .F₁' (g' .F₁' (h' .F₁' B'.id'))) ∘' (f' .F₁' D'.id' ∘' id')               ≑[]⟨ ((apd (Ξ» _ z β†’ f' .F₁' (g' .F₁' z)) (h' .F-id')) ⟩∘'⟨ (idr' _)) ⟩ 
  (f' .F₁' (g' .F₁' C'.id')) ∘' (f' .F₁' D'.id')                                ≑[]⟨ ((apd (Ξ» _ β†’ f' .F₁') (g' .F-id') βˆ™[] f' .F-id') ⟩∘'⟨ f' .F-id') ⟩
  id' ∘' id'                                                                    ∎
  where
    open DR E'
    module B' = Displayed B'
    module C' = Displayed C'
    module D' = Displayed D'

References