Displayed categories

src/Categories/Category/Construction/Kleisli.agda

@@ -41,7 +41,7 @@ Kleisli {𝒞 = 𝒞} M = record
   assoc′ {A} {B} {C} {D} {f} {g} {h} = begin
     (μ.η D ∘ F₁ ((μ.η D ∘ F₁ h) ∘ g)) ∘ f           ≈⟨ pushʳ homomorphism ⟩∘⟨refl ⟩
     ((μ.η D ∘ F₁ (μ.η D ∘ F₁ h)) ∘ F₁ g) ∘ f        ≈⟨ pushˡ (∘-resp-≈ˡ (∘-resp-≈ʳ homomorphism)) ⟩
-    (μ.η D ∘ (F₁ (μ.η D) ∘ F₁ (F₁ h))) ∘ (F₁ g ∘ f) ≈⟨ pushˡ (glue′ M.assoc (μ.commute h)) ⟩
+    (μ.η D ∘ (F₁ (μ.η D) ∘ F₁ (F₁ h))) ∘ (F₁ g ∘ f) ≈⟨ pushˡ (sym-glue M.assoc (μ.commute h)) ⟩
     (μ.η D ∘ F₁ h) ∘ (μ.η C ∘ (F₁ g ∘ f))           ≈⟨ refl⟩∘⟨ sym-assoc ⟩
     (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)           ∎
 

src/Categories/Category/Construction/Total.agda

@@ -0,0 +1,55 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Displayed using (Displayed)
+
+module Categories.Category.Construction.Total {o ℓ e o′ ℓ′ e′} {B : Category o ℓ e} (C : Displayed B o′ ℓ′ e′) where
+
+open import Data.Product using (proj₁; proj₂; Σ-syntax; ∃-syntax; -,_)
+open import Level using (_⊔_)
+
+open import Categories.Functor.Core using (Functor)
+
+open Category B
+open Displayed C
+open Equiv′
+
+Total : Set (o ⊔ o′)
+Total = Σ[ Carrier ∈ Obj ] Obj[ Carrier ]
+
+record Total⇒ (X Y : Total) : Set (ℓ ⊔ ℓ′) where
+  constructor total⇒
+  field
+    {arr} : proj₁ X ⇒ proj₁ Y
+    preserves : proj₂ X ⇒[ arr ] proj₂ Y
+
+open Total⇒ public using (preserves)
+
+∫ : Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
+∫ = record
+  { Obj = Total
+  ; _⇒_ = Total⇒
+  ; _≈_ = λ f g → ∃[ p ] preserves f ≈[ p ] preserves g
+  ; id = total⇒ id′
+  ; _∘_ = λ f g → total⇒ (preserves f ∘′ preserves g)
+  ; assoc = -, assoc′
+  ; sym-assoc = -, sym-assoc′
+  ; identityˡ = -, identityˡ′
+  ; identityʳ = -, identityʳ′
+  ; identity² = -, identity²′
+  ; equiv = record
+    { refl = -, refl′
+    ; sym = λ p → -, sym′ (proj₂ p)
+    ; trans = λ p q → -, trans′ (proj₂ p) (proj₂ q)
+    }
+  ; ∘-resp-≈ = λ p q → -, ∘′-resp-[]≈ (proj₂ p) (proj₂ q)
+  }
+
+display : Functor ∫ B
+display = record
+  { F₀ = proj₁
+  ; F₁ = Total⇒.arr
+  ; identity = Equiv.refl
+  ; homomorphism = Equiv.refl
+  ; F-resp-≈ = proj₁
+  }

src/Categories/Category/Displayed.agda

@@ -0,0 +1,118 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+
+module Categories.Category.Displayed where
+
+open import Data.Product
+open import Level
+
+open import Categories.Functor.Core
+open import Relation.Binary.Displayed
+import Relation.Binary.Displayed.Reasoning.Setoid as DisplayedSetoidR
+
+-- A displayed category captures the idea of placing extra structure
+-- over a base category. For example, the category of monoids can be
+-- considered as the category of setoids with extra structure on the
+-- objects and extra conditions on the morphisms.
+record Displayed {o ℓ e} (B : Category o ℓ e) o′ ℓ′ e′ : Set (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′ ⊔ e′)) where
+  open Category B
+  open Equiv
+
+  infix 4 _⇒[_]_ _≈[_]_
+  infixr 9 _∘′_
+
+  field
+    Obj[_] : Obj → Set o′
+    _⇒[_]_ : ∀ {X Y} → Obj[ X ] → X ⇒ Y → Obj[ Y ] → Set ℓ′
+    _≈[_]_ : ∀ {A B X Y} {f g : A ⇒ B} → X ⇒[ f ] Y → f ≈ g → X ⇒[ g ] Y → Set e′
+
+    id′ : ∀ {A} {X : Obj[ A ]} → X ⇒[ id ] X
+    _∘′_ : ∀ {A B C X Y Z} {f : B ⇒ C} {g : A ⇒ B}
+         → Y ⇒[ f ] Z → X ⇒[ g ] Y → X ⇒[ f ∘ g ] Z
+
+    identityʳ′ : ∀ {A B X Y} {f : A ⇒ B} → {f′ : X ⇒[ f ] Y} → f′ ∘′ id′ ≈[ identityʳ ] f′
+    identityˡ′ : ∀ {A B X Y} {f : A ⇒ B} → {f′ : X ⇒[ f ] Y} → id′ ∘′ f′ ≈[ identityˡ ] f′
+    identity²′ : ∀ {A} {X : Obj[ A ]} → id′ {X = X} ∘′ id′ ≈[ identity² ] id′
+    assoc′ : ∀ {A B C D W X Y Z} {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
+           → {f′ : Y ⇒[ f ] Z} → {g′ : X ⇒[ g ] Y} → {h′ : W ⇒[ h ] X}
+           → (f′ ∘′ g′) ∘′ h′ ≈[ assoc ] f′ ∘′ (g′ ∘′ h′)
+    sym-assoc′ : ∀ {A B C D W X Y Z} {f : C ⇒ D} {g : B ⇒ C} {h : A ⇒ B}
+           → {f′ : Y ⇒[ f ] Z} → {g′ : X ⇒[ g ] Y} → {h′ : W ⇒[ h ] X}
+           → f′ ∘′ (g′ ∘′ h′) ≈[ sym-assoc ] (f′ ∘′ g′) ∘′ h′
+
+
+    equiv′ : ∀ {A B X Y} → IsDisplayedEquivalence equiv (_≈[_]_ {A} {B} {X} {Y})
+
+    ∘′-resp-≈[] : ∀ {A B C X Y Z} {f h : B ⇒ C} {g i : A ⇒ B}
+                    {f′ : Y ⇒[ f ] Z} {h′ : Y ⇒[ h ] Z} {g′ : X ⇒[ g ] Y} {i′ : X ⇒[ i ] Y}
+                    {p : f ≈ h} {q : g ≈ i}
+                → f′ ≈[ p ] h′ → g′ ≈[ q ] i′ → f′ ∘′ g′ ≈[ ∘-resp-≈ p q ] h′ ∘′ i′
+
+  module Equiv′ {A B X Y} = IsDisplayedEquivalence (equiv′ {A} {B} {X} {Y})
+
+  open Equiv′
+
+  ∘′-resp-≈[]ˡ : ∀ {A B C X Y Z} {f h : B ⇒ C} {g : A ⇒ B} {f′ : Y ⇒[ f ] Z} {h′ : Y ⇒[ h ] Z} {g′ : X ⇒[ g ] Y}
+                 → {p : f ≈ h} → f′ ≈[ p ] h′ → f′ ∘′ g′ ≈[ ∘-resp-≈ˡ p ] h′ ∘′ g′
+  ∘′-resp-≈[]ˡ pf = ∘′-resp-≈[] pf refl′
+
+  ∘′-resp-≈[]ʳ : ∀ {A B C X Y Z} {f : B ⇒ C} {g i : A ⇒ B} {f′ : Y ⇒[ f ] Z} {g′ : X ⇒[ g ] Y} {i′ : X ⇒[ i ] Y}
+                 → {p : g ≈ i} → g′ ≈[ p ] i′ → f′ ∘′ g′ ≈[ ∘-resp-≈ʳ p ] f′ ∘′ i′
+  ∘′-resp-≈[]ʳ pf = ∘′-resp-≈[] refl′ pf
+
+  hom-setoid′ : ∀ {A B} {X : Obj[ A ]} {Y : Obj[ B ]} → DisplayedSetoid hom-setoid _ _
+  hom-setoid′ {X = X} {Y = Y} = record
+    { Carrier′ = X ⇒[_] Y
+    ; _≈[_]_ = _≈[_]_
+    ; isDisplayedEquivalence = equiv′
+    }
+
+  module HomReasoning′ {A B : Obj} {X : Obj[ A ]} {Y : Obj[ B ]} where
+    open DisplayedSetoidR (hom-setoid′ {X = X} {Y = Y}) public
+    open HomReasoning
+
+    infixr 4 _⟩∘′⟨_ refl′⟩∘′⟨_
+    infixl 5 _⟩∘′⟨refl′
+    _⟩∘′⟨_ : ∀ {M} {f h : M ⇒ B} {g i : A ⇒ M} {f≈h : f ≈ h} {g≈i : g ≈ i}
+               {M′ : Obj[ M ]} {f′ : M′ ⇒[ f ] Y} {h′ : M′ ⇒[ h ] Y} {g′ : X ⇒[ g ] M′} {i′ : X ⇒[ i ] M′}
+             → f′ ≈[ f≈h ] h′ → g′ ≈[ g≈i ] i′ → f′ ∘′ g′ ≈[ f≈h ⟩∘⟨ g≈i ] h′ ∘′ i′
+    _⟩∘′⟨_ = ∘′-resp-≈[]
+
+    refl′⟩∘′⟨_ : ∀ {M} {f : M ⇒ B} {g i : A ⇒ M} {g≈i : g ≈ i}
+                  {M′ : Obj[ M ]} {f′ : M′ ⇒[ f ] Y} {g′ : X ⇒[ g ] M′} {i′ : X ⇒[ i ] M′}
+                → g′ ≈[ g≈i ] i′ → f′ ∘′ g′ ≈[ refl⟩∘⟨ g≈i ] f′ ∘′ i′
+    refl′⟩∘′⟨_ = ∘′-resp-≈[]ʳ
+
+    _⟩∘′⟨refl′ : ∀ {M} {f h : M ⇒ B} {g : A ⇒ M} {f≈h : f ≈ h}
+                   {M′ : Obj[ M ]} {f′ : M′ ⇒[ f ] Y} {h′ : M′ ⇒[ h ] Y} {g′ : X ⇒[ g ] M′}
+                 → f′ ≈[ f≈h ] h′ → f′ ∘′ g′ ≈[ f≈h ⟩∘⟨refl ] h′ ∘′ g′
+    _⟩∘′⟨refl′ = ∘′-resp-≈[]ˡ
+
+  op′ : Displayed op o′ ℓ′ e′
+  op′ = record
+    { Obj[_] = Obj[_]
+    ; _⇒[_]_ = λ X f Y → Y ⇒[ f ] X
+    ; _≈[_]_ = _≈[_]_
+    ; id′ = id′
+    ; _∘′_ = λ f′ g′ → g′ ∘′ f′
+    ; identityʳ′ = identityˡ′
+    ; identityˡ′ = identityʳ′
+    ; identity²′ = identity²′
+    ; assoc′ = sym-assoc′
+    ; sym-assoc′ = assoc′
+    ; equiv′ = equiv′
+    ; ∘′-resp-≈[] = λ p q → ∘′-resp-≈[] q p
+    }
+
+module Definitions′ {o ℓ e} {B : Category o ℓ e} {o′ ℓ′ e′} (C : Displayed B o′ ℓ′ e′) where
+  open Category B
+  open Displayed C
+  open Definitions B
+
+  CommutativeSquare′ : ∀ {A B C D : Obj} {A′ : Obj[ A ]} {B′ : Obj[ B ]} {C′ : Obj[ C ]} {D′ : Obj[ D ]}
+                         {f : A ⇒ B} {g : A ⇒ C} {h : B ⇒ D} {i : C ⇒ D}
+                         (f′ : A′ ⇒[ f ] B′) (g′ : A′ ⇒[ g ] C′) (h′ : B′ ⇒[ h ] D′) (i′ : C′ ⇒[ i ] D′)
+                         (sq : CommutativeSquare f g h i)
+                       → Set _
+  CommutativeSquare′ f′ g′ h′ i′ sq = h′ ∘′ f′ ≈[ sq ] i′ ∘′ g′

src/Categories/Category/Displayed/Instance/DisplayedCats.agda

@@ -0,0 +1,27 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Category.Displayed.Instance.DisplayedCats where
+
+open import Level
+
+open import Categories.Category
+open import Categories.Category.Displayed
+open import Categories.Category.Instance.Cats
+open import Categories.Functor.Displayed
+open import Categories.NaturalTransformation.NaturalIsomorphism.Displayed
+
+DisplayedCats : ∀ o ℓ e o′ ℓ′ e′ → Displayed (Cats o ℓ e) (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′ ⊔ e′)) (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′)
+DisplayedCats o ℓ e o′ ℓ′ e′ = record
+  { Obj[_] = λ B → Displayed B o′ ℓ′ e′
+  ; _⇒[_]_ = λ C F D → DisplayedFunctor C D F
+  ; _≈[_]_ = λ F′ F≃G G′ → DisplayedNaturalIsomorphism F′ G′ F≃G
+  ; id′ = id′
+  ; _∘′_ = _∘F′_
+  ; identityˡ′ = unitorˡ′
+  ; identityʳ′ = unitorʳ′
+  ; identity²′ = unitor²′
+  ; assoc′ = λ {_ _ _ _ _ _ _ _ _ _ _ F′ G′ H′} → associator′ H′ G′ F′
+  ; sym-assoc′ = λ {_ _ _ _ _ _ _ _ _ _ _ F′ G′ H′} → sym-associator′ H′ G′ F′
+  ; equiv′ = isDisplayedEquivalence
+  ; ∘′-resp-≈[] = _ⓘₕ′_
+  }

src/Categories/Category/Instance/Cats.agda

@@ -9,7 +9,7 @@ open import Level
 open import Categories.Category using (Category)
 open import Categories.Functor using (Functor; id; _∘F_)
 open import Categories.NaturalTransformation.NaturalIsomorphism
-  using (NaturalIsomorphism; associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
+  using (NaturalIsomorphism; associator; sym-associator; unitorˡ; unitorʳ; unitor²; isEquivalence; _ⓘₕ_; sym)
 private
   variable
     o ℓ e : Level
@@ -24,7 +24,7 @@ Cats o ℓ e = record
   ; id        = id
   ; _∘_       = _∘F_
   ; assoc     = λ {_ _ _ _ F G H} → associator F G H
-  ; sym-assoc = λ {_ _ _ _ F G H} → sym (associator F G H)
+  ; sym-assoc = λ {_ _ _ _ F G H} → sym-associator F G H
   ; identityˡ = unitorˡ
   ; identityʳ = unitorʳ
   ; identity² = unitor²

src/Categories/Functor/Displayed.agda

@@ -0,0 +1,77 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Functor.Displayed where
+
+open import Function.Base using () renaming (id to id→; _∘_ to _∙_)
+open import Level
+
+open import Categories.Category
+open import Categories.Category.Displayed
+open import Categories.Functor
+
+private
+  variable
+    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴  : Level
+    B₁ B₂ B₃ : Category o ℓ e
+
+record DisplayedFunctor {B₁ : Category o ℓ e} {B₂ : Category o′ ℓ′ e′} (C : Displayed B₁ o″ ℓ″ e″) (D : Displayed B₂ o‴ ℓ‴ e‴) (F : Functor B₁ B₂) : Set (o ⊔ ℓ ⊔ e ⊔ o″ ⊔ ℓ″ ⊔ e″ ⊔ o‴ ⊔ ℓ‴ ⊔ e‴) where
+  private
+    module C = Displayed C
+    module D = Displayed D
+    module F = Functor F
+  field
+    F₀′ : ∀ {X} → C.Obj[ X ] → D.Obj[ F.₀ X ]
+    F₁′ : ∀ {X Y} {f : B₁ [ X , Y ]} {X′ Y′} → X′ C.⇒[ f ] Y′ → F₀′ X′ D.⇒[ F.₁ f ] F₀′ Y′
+    identity′ : ∀ {X} {X′ : C.Obj[ X ]} → F₁′ (C.id′ {X = X′}) D.≈[ F.identity ] D.id′
+    homomorphism′ : ∀ {X Y Z} {X′ : C.Obj[ X ]} {Y′ : C.Obj[ Y ]} {Z′ : C.Obj[ Z ]}
+                      {f : B₁ [ X , Y ]} {g : B₁ [ Y , Z ]} {f′ : X′ C.⇒[ f ] Y′} {g′ : Y′ C.⇒[ g ] Z′}
+                    → F₁′ (g′ C.∘′ f′) D.≈[ F.homomorphism ] F₁′ g′ D.∘′ F₁′ f′
+    F′-resp-≈[] : ∀ {X Y} {X′ : C.Obj[ X ]} {Y′ : C.Obj[ Y ]}
+                    {f g : B₁ [ X , Y ]} {f′ : X′ C.⇒[ f ] Y′} {g′ : X′ C.⇒[ g ] Y′}
+                  → {p : B₁ [ f ≈ g ]} → f′ C.≈[ p ] g′
+                  → F₁′ f′ D.≈[ F.F-resp-≈ p ] F₁′ g′
+
+  ₀′ = F₀′
+  ₁′ = F₁′
+
+  op′ : DisplayedFunctor C.op′ D.op′ F.op
+  op′ = record
+    { F₀′ = F₀′
+    ; F₁′ = F₁′
+    ; identity′ = identity′
+    ; homomorphism′ = homomorphism′
+    ; F′-resp-≈[] = F′-resp-≈[]
+    }
+
+id′ : ∀ {B : Category o ℓ e} {C : Displayed B o′ ℓ′ e′} → DisplayedFunctor C C id
+id′ {C = C} = record
+  { F₀′ = id→
+  ; F₁′ = id→
+  ; identity′ = Displayed.Equiv′.refl′ C
+  ; homomorphism′ = Displayed.Equiv′.refl′ C
+  ; F′-resp-≈[] = id→
+  }
+
+_∘F′_ : ∀ {C : Displayed B₁ o ℓ e} {D : Displayed B₂ o′ ℓ′ e′} {E : Displayed B₃ o″ ℓ″ e″}
+          {F : Functor B₂ B₃} {G : Functor B₁ B₂}
+        → DisplayedFunctor D E F → DisplayedFunctor C D G → DisplayedFunctor C E (F ∘F G)
+_∘F′_  {C = C} {D = D} {E = E} F′ G′ = record
+   { F₀′ = F′.₀′ ∙ G′.₀′
+   ; F₁′ = F′.₁′ ∙ G′.₁′
+   ; identity′ = begin′
+     F′.₁′ (G′.₁′ C.id′) ≈[]⟨ F′.F′-resp-≈[] G′.identity′ ⟩
+     F′.₁′ D.id′         ≈[]⟨ F′.identity′ ⟩
+     E.id′               ∎′
+   ; homomorphism′ = λ {_} {_} {_} {_} {_} {_} {_} {_} {f′} {g′} → begin′
+     F′.₁′ (G′.₁′ (g′ C.∘′ f′))               ≈[]⟨ F′.F′-resp-≈[] G′.homomorphism′ ⟩
+     F′.₁′ (G′.₁′ g′ D.∘′ G′.₁′ f′)           ≈[]⟨ F′.homomorphism′ ⟩
+     (F′.₁′ (G′.₁′ g′) E.∘′ F′.₁′ (G′.₁′ f′)) ∎′
+   ; F′-resp-≈[] = F′.F′-resp-≈[] ∙ G′.F′-resp-≈[]
+   }
+   where
+     module C = Displayed C
+     module D = Displayed D
+     module E = Displayed E
+     open E.HomReasoning′
+     module F′ = DisplayedFunctor F′
+     module G′ = DisplayedFunctor G′

src/Categories/Functor/Displayed/Properties.agda

@@ -0,0 +1,67 @@
+{-# OPTIONS --safe --without-K #-}
+
+module Categories.Functor.Displayed.Properties where
+
+open import Categories.Category
+open import Categories.Category.Displayed
+open import Categories.Functor
+open import Categories.Functor.Displayed
+open import Categories.Functor.Properties
+open import Categories.Morphism
+open import Categories.Morphism.Displayed
+
+module _
+  {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴}
+  {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F : Functor C D}
+  {C′ : Displayed C o″ ℓ″ e″} {D′ : Displayed D o‴ ℓ‴ e‴} (F′ : DisplayedFunctor C′ D′ F)
+  where
+
+  private
+    module C = Category C
+--    module F = Functor F
+    module C′ = Displayed C′
+    module D′ = Displayed D′
+    module F′ = DisplayedFunctor F′
+
+  open Definitions
+  open Definitions′
+
+  [_]-resp-∘′ : ∀ {X Y Z} {f : Y C.⇒ Z} {g : X C.⇒ Y} {h : X C.⇒ Z} {f∘g≈h : f C.∘ g C.≈ h}
+                  {X′  : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {Z′ : C′.Obj[ Z ]}
+                  {f′ : Y′ C′.⇒[ f ] Z′} {g′ : X′ C′.⇒[ g ] Y′} {h′ : X′ C′.⇒[ h ] Z′}
+                → f′ C′.∘′ g′ C′.≈[ f∘g≈h ] h′
+                → F′.₁′ f′ D′.∘′ F′.₁′ g′ D′.≈[ [ F ]-resp-∘ f∘g≈h ] F′.₁′ h′
+  [_]-resp-∘′ {f′ = f′} {g′ = g′} {h′ = h′} eq = begin′
+    F′.₁′ f′ D′.∘′ F′.₁′ g′ ≈˘[]⟨ F′.homomorphism′ ⟩
+    F′.₁′ (f′ C′.∘′ g′)     ≈[]⟨ F′.F′-resp-≈[] eq ⟩
+    F′.₁′ h′                ∎′
+    where open D′.HomReasoning′
+
+  [_]-resp-square′ : ∀ {W X Y Z} {f : W C.⇒ X} {g : W C.⇒ Y} {h : X C.⇒ Z} {i : Y C.⇒ Z} {sq : CommutativeSquare C f g h i}
+                       {W′ : C′.Obj[ W ]} {X′ : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {Z′ : C′.Obj[ Z ]}
+                       {f′ : W′ C′.⇒[ f ] X′} {g′ : W′ C′.⇒[ g ] Y′} {h′ : X′ C′.⇒[ h ] Z′} {i′ : Y′ C′.⇒[ i ] Z′}
+                    → CommutativeSquare′ C′ f′ g′ h′ i′ sq
+                    → CommutativeSquare′ D′ (F′.₁′ f′) (F′.₁′ g′) (F′.₁′ h′) (F′.₁′ i′) ([ F ]-resp-square sq)
+  [_]-resp-square′ {f′ = f′} {g′ = g′} {h′ = h′} {i′ = i′} sq′ = begin′
+    F′.₁′ h′ D′.∘′ F′.₁′ f′ ≈˘[]⟨ F′.homomorphism′ ⟩
+    F′.₁′ (h′ C′.∘′ f′)     ≈[]⟨ F′.F′-resp-≈[] sq′ ⟩
+    F′.₁′ (i′ C′.∘′ g′)     ≈[]⟨ F′.homomorphism′ ⟩
+    F′.₁′ i′ D′.∘′ F′.₁′ g′ ∎′
+    where open D′.HomReasoning′
+
+  [_]-resp-DisplayedIso : ∀ {X Y} {f : X C.⇒ Y} {g : Y C.⇒ X} {iso : Iso C f g}
+                            {X′ : C′.Obj[ X ]} {Y′ : C′.Obj[ Y ]} {f′ : X′ C′.⇒[ f ] Y′} {g′ : Y′ C′.⇒[ g ] X′}
+                          → DisplayedIso C′ f′ g′ iso → DisplayedIso D′ (F′.₁′ f′) (F′.₁′ g′) ([ F ]-resp-Iso iso)
+  [_]-resp-DisplayedIso {f′ = f′} {g′ = g′} diso = record
+    { isoˡ′ = begin′
+      F′.₁′ g′ D′.∘′ F′.₁′ f′ ≈[]⟨ [ isoˡ′ ]-resp-∘′ ⟩
+      F′.₁′ C′.id′            ≈[]⟨ F′.identity′ ⟩
+      D′.id′                  ∎′
+    ; isoʳ′ = begin′
+      F′.₁′ f′ D′.∘′ F′.₁′ g′ ≈[]⟨ [ isoʳ′ ]-resp-∘′ ⟩
+      F′.₁′ C′.id′            ≈[]⟨ F′.identity′ ⟩
+      D′.id′                  ∎′
+    }
+    where
+      open DisplayedIso diso
+      open D′.HomReasoning′

src/Categories/Morphism/Displayed.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Categories.Category
+open import Categories.Category.Displayed
+
+module Categories.Morphism.Displayed {o ℓ e o′ ℓ′ e′} {B : Category o ℓ e} (C : Displayed B o′ ℓ′ e′) where
+
+open import Categories.Morphism B
+
+open Category B
+open Displayed C
+
+private
+  variable
+    X Y : Obj
+    X′ : Obj[ X ]
+    Y′ : Obj[ Y ]
+
+record DisplayedIso {from : X ⇒ Y} {to : Y ⇒ X} (from′ : X′ ⇒[ from ] Y′) (to′ : Y′ ⇒[ to ] X′) (iso : Iso from to) : Set e′ where
+  open Iso iso
+  field
+    isoˡ′ : to′ ∘′ from′ ≈[ isoˡ ] id′
+    isoʳ′ : from′ ∘′ to′ ≈[ isoʳ ] id′