From 5efde68f7cfcc93e279232a60aa8783686680524 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20=C3=85gren=20Thun=C3=A9?= <anders@aathn.org>
Date: Mon, 20 Apr 2026 23:03:38 +0200
Subject: [PATCH] Define Disc using inductive identity

---
 src/Cat/Instances/Discrete.lagda.md | 162 ++++++++++------------------
 1 file changed, 58 insertions(+), 104 deletions(-)

diff --git a/src/Cat/Instances/Discrete.lagda.md b/src/Cat/Instances/Discrete.lagda.md
index 7b730ca5c..bb22a507c 100644
--- a/src/Cat/Instances/Discrete.lagda.md
+++ b/src/Cat/Instances/Discrete.lagda.md
@@ -8,6 +8,7 @@ open import Cat.Groupoid
 open import Cat.Morphism
 open import Cat.Prelude
 
+open import Data.Id.Properties
 open import Data.Id.Base
 open import Data.Dec
 
@@ -37,20 +38,22 @@ open _=>_
 Given a [[groupoid]] $A$, we can see $A$ as a [[category]] with
 space of objects $A$ and path types $x \equiv y$ as $\hom$-sets $x \to
 y$. When $A$ is a [[set]], we call this the **discrete category** on $A$.
+For technical reasons, we prefer to define this category using the
+[[inductive identity]] type instead of the path type.
 
 ```agda
 Disc : (A : Type ℓ) → is-groupoid A → Precategory ℓ ℓ
-Disc A A-grpd .Ob = A
-Disc A A-grpd .Hom = _≡_
-Disc A A-grpd .Hom-set = A-grpd
-Disc A A-grpd .id = refl
-Disc A A-grpd ._∘_ p q = q ∙ p
-Disc A A-grpd .idr _ = ∙-idl _
-Disc A A-grpd .idl _ = ∙-idr _
-Disc A A-grpd .assoc _ _ _ = sym (∙-assoc _ _ _)
+Disc A A-grpd .Ob          = A
+Disc A A-grpd .Hom         = _≡ᵢ_
+Disc A A-grpd .Hom-set     = ≡ᵢ-is-hlevel' {n = 2} A-grpd
+Disc A A-grpd .id          = reflᵢ
+Disc A A-grpd ._∘_ p q     = q ∙ᵢ p
+Disc A A-grpd .idr _       = refl
+Disc A A-grpd .idl _       = ∙ᵢ-idr _
+Disc A A-grpd .assoc p q r = sym (∙ᵢ-assoc r q p)
 
 Disc' : Set ℓ → Precategory ℓ ℓ
-Disc' A = Disc ∣ A ∣ h where abstract
+Disc' A = Disc ∣ A ∣ h module Disc' where abstract
   h : is-groupoid ∣ A ∣
   h = is-hlevel-suc 2 (A .is-tr)
 ```
@@ -60,26 +63,12 @@ By construction, this is a [[univalent|univalent category]]
 
 ```agda
 Disc-is-category : ∀ {A : Type ℓ} {A-grpd} → is-category (Disc A A-grpd)
-Disc-is-category .to-path is = is .to
-Disc-is-category .to-path-over is = ≅-pathp _ _ _ λ i j → is .to (i ∧ j)
+Disc-is-category .to-path is              = Id≃path.to (is .to)
+Disc-is-category .to-path-over {a = a} is = ≅-pathp _ _ _ $
+  Jᵢ (λ _ p → PathP (λ i → a ≡ᵢ Id≃path.to p i) reflᵢ p) refl (is .to)
 
 Disc-is-groupoid : ∀ {A : Type ℓ} {A-grpd} → is-pregroupoid (Disc A A-grpd)
-Disc-is-groupoid p = make-invertible _ (sym p) (∙-invl p) (∙-invr p)
-```
-
-We can lift any function between the underlying types to a functor
-between discrete categories. This is because every function
-automatically respects equality in a functorial way.
-
-```agda
-lift-disc
-  : ∀ {A : Set ℓ} {B : Set ℓ'}
-  → (∣ A ∣ → ∣ B ∣)
-  → Functor (Disc' A) (Disc' B)
-lift-disc f .F₀ = f
-lift-disc f .F₁ = ap f
-lift-disc f .F-id = refl
-lift-disc f .F-∘ p q = ap-∙ f q p
+Disc-is-groupoid p = make-invertible _ (symᵢ p) (∙ᵢ-invl p) (∙ᵢ-invr p)
 ```
 
 <!--
@@ -98,105 +87,68 @@ Codisc' x .assoc _ _ _ = refl
 
 ## Diagrams in Disc(X)
 
-If $X$ is a [[discrete]] type, then it is in
-particular a [[set]], and we can make diagrams of shape
-$\rm{Disc}(X)$ in some category $\cC$, using the decidable
-equality on $X$ to improve computation. We note that the decidable
-equality is _superfluous_ information: the construction `Disc'`{.Agda}
-above extends into a [[left adjoint]] to the `Ob`{.Agda} functor.
+Because the morphisms in a discrete category are identifications, and
+functions respect equality, any function on objects out of a discrete
+category induces a functor.
 
 ```agda
 Disc-diagram
-  : ∀ {X : Set ℓ} ⦃ _ : Discrete ∣ X ∣ ⦄
-  → (∣ X ∣ → Ob C)
-  → Functor (Disc' X) C
-Disc-diagram {C = C} {X = X} ⦃ d ⦄ f = F where
+  : {X : Type ℓ} (iss : is-groupoid X)
+  → (X → Ob C)
+  → Functor (Disc X iss) C
+Disc-diagram {C = C} {X = X} _ f = F where
   module C = Precategory C
 
-  P : ∣ X ∣ → ∣ X ∣ → Type _
-  P x y = C.Hom (f x) (f y)
+  go : ∀ {x y : X} → x ≡ᵢ y → C.Hom (f x) (f y)
+  go = Jᵢ (λ y _ → C.Hom (f _) (f y)) C.id
 
-  go : ∀ {x y : ∣ X ∣} → x ≡ y → Dec (x ≡ᵢ y) → P x y
-  go {x} {.x} p (yes reflᵢ) = C.id
-  go {x} {y}  p (no ¬p)     = absurd (¬p (Id≃path.from p))
+  F : Functor _ _
+  F .F₀      = f
+  F .F₁      = go
+  F .F-id    = refl
+  F .F-∘ f g =
+    Jᵢ (λ y g → ∀ f → go (g ∙ᵢ f) ≡ go f C.∘ go g) (λ _ → sym (C.idr _)) g f
 ```
 
-The object part of the functor is the provided $f : X \to
-\rm{Ob}(\cC)$, and the decidable equality is used to prove that
-$f$ respects equality. This is why it's redundant: $f$ automatically
-respects equality, because it's a function! However, by using the
-decision procedure, we get better computational behaviour: Very often,
-$\rm{disc}(x,x)$ will be $\rm{yes}(\refl)$, and
-substitution along $\refl$ is easy to deal with.
-
+<!--
 ```agda
-  F : Functor _ _
-  F .F₀ = f
-  F .F₁ {x} {y} p = go p (x ≡ᵢ? y)
+Disc-diagram!
+  : ∀ ⦃ iss : H-Level {ℓ} X 3 ⦄
+  → (X → Ob C)
+  → Functor (Disc X (hlevel 3)) C
+Disc-diagram! = Disc-diagram (hlevel 3)
 ```
+-->
 
-Proving that our our $F_1$ is functorial involves a bunch of tedious
-computations with equalities and a whole waterfall of absurd cases:
+As a corollary, we can lift any function between underlying types to a
+functor between discrete categories.
 
 ```agda
-  F .F-id {x} = refl
-  F .F-∘  {x} {y} {z} f g =
-    J (λ y g → ∀ {z} (f : y ≡ z) → go (g ∙ f) (x ≡ᵢ? z) ≡ go f (y ≡ᵢ? z) C.∘ go g (x ≡ᵢ? y))
-      (λ f → J (λ z f → go (refl ∙ f) (x ≡ᵢ? z) ≡ go f (x ≡ᵢ? z) C.∘ C.id) (sym (C.idr _)) f)
-      g f
+lift-disc : {A : Set ℓ} {B : Set ℓ'} → (∣ A ∣ → ∣ B ∣) → Functor (Disc' A) (Disc' B)
+lift-disc {A = A} f = Disc-diagram (Disc'.h A) f
 ```
 
 <!--
 ```agda
-Disc'-adjunct
-  : ∀ { iss : is-groupoid X}
-  → (X → Ob C)
-  → Functor (Disc X iss) C
-Disc'-adjunct {C = C} F .F₀ = F
-Disc'-adjunct {C = C} F .F₁ p = subst (C .Hom (F _) ⊙ F) p (C .id)
-Disc'-adjunct {C = C} F .F-id = transport-refl _
-Disc'-adjunct {C = C} {iss} F .F-∘ {x} {y} {z} f g = path where
-  import Cat.Reasoning C as C
-  go = Disc'-adjunct {C = C} {iss} F .F₁
-  abstract
-    path : go (g ∙ f) ≡ C ._∘_ (go f) (go g)
-    path =
-      J' (λ y z f → ∀ {x} (g : x ≡ y) → go (g ∙ f) ≡ go f C.∘ go g)
-        (λ x g → subst-∙ (C .Hom (F _) ⊙ F) _ _ _
-              ∙∙ transport-refl _
-              ∙∙ C.introl (transport-refl _))
-        f {x} g
-
-Disc-adjunct
-  : ∀ ⦃ iss : H-Level {ℓ} X 3 ⦄
-  → (X → Ob C)
-  → Functor (Disc X (hlevel 3)) C
-Disc-adjunct = Disc'-adjunct {iss = hlevel 3}
-
 Disc-into
   : ∀ {ℓ} (X : Set ℓ)
   → (F : C .Ob → ∣ X ∣)
-  → (F₁ : ∀ {x y} → C .Hom x y → F x ≡ F y)
+  → (F₁ : ∀ {x y} → C .Hom x y → F x ≡ᵢ F y)
   → Functor C (Disc' X)
-Disc-into X F F₁ .F₀ = F
-Disc-into X F F₁ .F₁ = F₁
-Disc-into X F F₁ .F-id = X .is-tr _ _ _ _
-Disc-into X F F₁ .F-∘ _ _ = X .is-tr _ _ _ _
-```
--->
+Disc-into X F F₁ .F₀      = F
+Disc-into X F F₁ .F₁      = F₁
+Disc-into X F F₁ .F-id    = ≡ᵢ-is-hlevel' {n = 1} (X .is-tr) _ _ _ _
+Disc-into X F F₁ .F-∘ _ _ = ≡ᵢ-is-hlevel' {n = 1} (X .is-tr) _ _ _ _
 
-<!--
-```agda
 Disc-natural
   : ∀ {X : Set ℓ}
   → {F G : Functor (Disc' X) C}
   → (∀ x → C .Hom (F .F₀ x) (G .F₀ x))
   → F => G
 Disc-natural fam .η = fam
-Disc-natural {C = C} {F = F} {G = G} fam .is-natural x y f =
-  J (λ y p → fam y C.∘ F .F₁ p ≡ G .F₁ p C.∘ fam x)
+Disc-natural {C = C} {F = F} {G = G} fam .is-natural x y =
+  Jᵢ (λ y p → fam y C.∘ F .F₁ p ≡ G .F₁ p C.∘ fam x)
     (C.elimr (F .F-id) ∙ C.introl (G .F-id))
-    f
   where module C = Cat.Reasoning C
 
 Disc-natural₂
@@ -207,10 +159,11 @@ Disc-natural₂
   → F => G
 Disc-natural₂ fam .η = fam
 Disc-natural₂ {C = C} {F = F} {G = G} fam .is-natural x y (p , q) =
-  J (λ y' p' → fam y' C.∘ F .F₁ (ap fst p' , ap snd p')
-             ≡ G .F₁ (ap fst p' , ap snd p') C.∘ fam x)
-    (C.elimr (F .F-id) ∙ C.introl (G .F-id))
-    (Σ-pathp p q)
+  Jᵢ (λ y₁ p → ∀ y₂ q → fam (y₁ , y₂) C.∘ F .F₁ (p , q) ≡ G .F₁ (p , q) C.∘ fam x)
+    (λ y₂ → Jᵢ
+      (λ y₂ q → fam (x .fst , y₂) C.∘ F .F₁ (reflᵢ , q) ≡ G .F₁ (reflᵢ , q) C.∘ fam x)
+      (C.elimr (F .F-id) ∙ C.introl (G .F-id)))
+    p (y .snd) q
   where module C = Cat.Reasoning C
 
 open _≅_
@@ -219,8 +172,9 @@ Disc-natural-iso : ∀ {X : Set ℓ}
   → {F G : Functor (Disc' X) C}
   → (∀ x → Isomorphism C (F .F₀ x) (G .F₀ x))
   → F ≅ⁿ G
-Disc-natural-iso isos .to = Disc-natural λ x → isos x .to
-Disc-natural-iso isos .from = Disc-natural λ x → isos x .from
-Disc-natural-iso isos .inverses = to-inversesⁿ (λ x → isos x .inverses .invl) (λ x → isos x .inverses .invr)
+Disc-natural-iso isos .to       = Disc-natural λ x → isos x .to
+Disc-natural-iso isos .from     = Disc-natural λ x → isos x .from
+Disc-natural-iso isos .inverses =
+  to-inversesⁿ (λ x → isos x .inverses .invl) (λ x → isos x .inverses .invr)
 ```
 -->