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,73 @@
+{-# 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
+import Relation.Binary.Displayed.Reasoning.Setoid as DisplayedSetoidR
+
+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′
+    }
+
+  module HomReasoning′ {A B : Obj} {X : Obj[ A ]} {Y : Obj[ B ]} where
+    open DisplayedSetoidR (hom-setoid′ {X = X} {Y = Y}) public
+
+    -- more stuff

src/Categories/Functor/Displayed.agda

@@ -0,0 +1,68 @@
+{-# 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₁′
+
+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/Morphism/Reasoning/Core.agda

@@ -171,11 +171,11 @@ glue {c′ = c′} {a′ = a′} {a = a} {c″ = c″} {c = c} {b′ = b′} {b
   a ∘ (c′ ∘ b′)  ≈⟨ extendʳ sq-a ⟩
   c″ ∘ (a′ ∘ b′) ∎
 
--- A "rotated" version of glue′. Equivalent to 'Equiv.sym (glue (Equiv.sym sq-a) (Equiv.sym sq-b))'
-glue′ : CommutativeSquare a′ c′ c″ a →
-        CommutativeSquare b′ c c′ b →
-        CommutativeSquare (a′ ∘ b′) c c″ (a ∘ b)
-glue′ {a′ = a′} {c′ = c′} {c″ = c″} {a = a} {b′ = b′} {c = c} {b = b} sq-a sq-b = begin
+-- A "rotated" version of glue. Equivalent to 'Equiv.sym (glue (Equiv.sym sq-a) (Equiv.sym sq-b))'
+sym-glue : CommutativeSquare a′ c′ c″ a →
+           CommutativeSquare b′ c c′ b →
+           CommutativeSquare (a′ ∘ b′) c c″ (a ∘ b)
+sym-glue {a′ = a′} {c′ = c′} {c″ = c″} {a = a} {b′ = b′} {c = c} {b = b} sq-a sq-b = begin
   c″ ∘ (a′ ∘ b′) ≈⟨ pullˡ sq-a ⟩
   (a ∘ c′) ∘ b′  ≈⟨ extendˡ sq-b ⟩
   (a ∘ b) ∘ c    ∎

src/Categories/NaturalTransformation/Core.agda

@@ -83,7 +83,7 @@ _∘ᵥ_ : ∀ {F G H : Functor C D} →
 _∘ᵥ_ {C = C} {D = D} {F} {G} {H} X Y = record
   { η       = λ q → D [ X.η q ∘ Y.η q ]
   ; commute = λ f → glue (X.commute f) (Y.commute f)
-  ; sym-commute = λ f → Category.Equiv.sym D (glue (X.commute f) (Y.commute f))
+  ; sym-commute = λ f → sym-glue (X.sym-commute f) (Y.sym-commute f)
   }
   where module X = NaturalTransformation X
         module Y = NaturalTransformation Y
@@ -92,9 +92,10 @@ _∘ᵥ_ {C = C} {D = D} {F} {G} {H} X Y = record
 -- "Horizontal composition"
 _∘ₕ_ : ∀ {F G : Functor C D} {H I : Functor D E} →
          NaturalTransformation H I → NaturalTransformation F G → NaturalTransformation (H ∘F F) (I ∘F G)
-_∘ₕ_ {E = E} {F} {I = I} Y X = ntHelper record
+_∘ₕ_ {E = E} {F} {I = I} Y X = record
   { η = λ q → E [ I₁ (X.η q) ∘ Y.η (F.F₀ q) ]
   ; commute = λ f → glue ([ I ]-resp-square (X.commute f)) (Y.commute (F.F₁ f))
+  ; sym-commute = λ f → sym-glue ([ I ]-resp-square (X.sym-commute f)) (Y.sym-commute (F.₁ f))
   }
   where module F = Functor F
         module X = NaturalTransformation X

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

src/Relation/Binary/Displayed/Reasoning/Setoid.agda

@@ -0,0 +1,41 @@
+{-# OPTIONS --safe --without-K #-}
+
+open import Relation.Binary
+open import Relation.Binary.Displayed
+
+module Relation.Binary.Displayed.Reasoning.Setoid {a ℓ a′ ℓ′} {S : Setoid a ℓ} (S′ : DisplayedSetoid S a′ ℓ′) where
+
+open import Level
+open import Relation.Binary.Reasoning.Setoid S
+
+open Setoid S
+open DisplayedSetoid S′
+
+infix 4 _IsRelatedTo[_]_
+
+data _IsRelatedTo[_]_ {x y : Carrier} (x′ : Carrier′ x) (p : x IsRelatedTo y) (y′ : Carrier′ y) : Set (ℓ ⊔ ℓ′) where
+  relTo[] : (x′≈[x≈y]y′ : x′ ≈[ begin p ] y′) → x′ IsRelatedTo[ p ] y′
+
+infix  1 begin′_
+infixr 2 step-≈[] step-≈˘[]
+infix  4 _∎′
+
+begin′_ : ∀ {x y} {x′ : Carrier′ x} {y′ : Carrier′ y} {x∼y : x IsRelatedTo y}
+          → x′ IsRelatedTo[ x∼y ] y′ → x′ ≈[ begin x∼y ] y′
+begin′ relTo[] x′≈[x≈y]y′ = x′≈[x≈y]y′
+
+step-≈[] : ∀ {x y z} (x′ : Carrier′ x) {y′ : Carrier′ y} {z′ : Carrier′ z} {y∼z : y IsRelatedTo z} {x≈y : x ≈ y}
+         → y′ IsRelatedTo[ y∼z ] z′ → x′ ≈[ x≈y ] y′ → x′ IsRelatedTo[ step-≈ x y∼z x≈y ] z′
+step-≈[] x′ {y∼z = relTo _} (relTo[] y≈[]z) x≈[]y = relTo[] (trans′ x≈[]y y≈[]z)
+syntax step-≈[] x′ y′∼z′ x′≈[]y′ = x′ ≈[]⟨ x′≈[]y′ ⟩ y′∼z′
+
+step-≈˘[] : ∀ {x y z} (x′ : Carrier′ x) {y′ : Carrier′ y} {z′ : Carrier′ z} {y∼z : y IsRelatedTo z} {y≈x : y ≈ x}
+          → y′ IsRelatedTo[ y∼z ] z′ → y′ ≈[ y≈x ] x′ → x′ IsRelatedTo[ step-≈˘ x y∼z y≈x ] z′
+step-≈˘[] x′ y′∼z′ y′≈x′ = x′ ≈[]⟨ sym′ y′≈x′ ⟩ y′∼z′ 
+syntax step-≈˘[] x′ y′∼z′ y′≈[]x′ = x′ ≈˘[]⟨ y′≈[]x′ ⟩ y′∼z′
+
+_∎′ : ∀ {x} (x′ : Carrier′ x) → x′ IsRelatedTo[ x ∎ ] x′
+_∎′ x′ = relTo[] refl′
+
+-- TODO: propositional equality
+-- Maybe TODO: have a convenient way to specify the base equality, e.g. _≈[_]⟨_⟩_