Displayed categories

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,67 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+
+module Categories.Category.Displayed {o ℓ e} (B : Category o ℓ e) where
+
+open import Data.Product
+open import Level
+
+open import Categories.Functor.Core
+open import Relation.Binary.Displayed
+
+open Category B
+open Equiv
+
+-- 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′ : Set (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′ ⊔ e′)) where
+  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′
+    }

src/Relation/Binary/Displayed.agda

@@ -0,0 +1,30 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Displayed where
+
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+private
+  variable
+    a ℓ a′ ℓ′ : Level
+
+record IsDisplayedEquivalence
+  {A : Set a} {_≈_ : Rel A ℓ} (isEquivalence : IsEquivalence _≈_)
+  {A′ : A → Set a′} (_≈[_]_ : ∀ {x y} → A′ x → x ≈ y → A′ y → Set ℓ′) : Set (a ⊔ ℓ ⊔ a′ ⊔ ℓ′)
+  where
+  open IsEquivalence isEquivalence
+  field
+    refl′ : ∀ {x} {x′ : A′ x} → x′ ≈[ refl ] x′
+    sym′ : ∀ {x y} {x′ : A′ x} {y′ : A′ y} {p : x ≈ y} → x′ ≈[ p ] y′ → y′ ≈[ sym p ] x′
+    trans′ : ∀ {x y z} {x′ : A′ x} {y′ : A′ y} {z′ : A′ z} {p : x ≈ y} {q : y ≈ z} → x′ ≈[ p ] y′ → y′ ≈[ q ] z′ → x′ ≈[ trans p q ] z′
+
+record DisplayedSetoid (B : Setoid a ℓ) a′ ℓ′ : Set (a ⊔ ℓ ⊔ suc (a′ ⊔ ℓ′)) where
+  open Setoid B
+  field
+    Carrier′ : Carrier → Set a′
+    _≈[_]_ : ∀ {x y} → Carrier′ x → x ≈ y → Carrier′ y → Set ℓ′
+    isDisplayedEquivalence : IsDisplayedEquivalence isEquivalence _≈[_]_
+  open IsDisplayedEquivalence isDisplayedEquivalence public