Skip to content

wip: Define Disc using inductive identity #623

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
aathn wants to merge 1 commit into from
Closed

wip: Define Disc using inductive identity #623

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
162 changes: 58 additions & 104 deletions src/Cat/Instances/Discrete.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
```
Expand All @@ -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)
```

<!--
Expand All @@ -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₂
Expand All @@ -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 _≅_
Expand All @@ -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)
```
-->
Loading