Skip to content

Commit 0b7a4e3

Browse files
plt-amyplt-amy
committed
defn: category of assemblies
1 parent 0110b4e commit 0b7a4e3

File tree

3 files changed

+207
-1
lines changed

3 files changed

+207
-1
lines changed

‎src/Cat/Instances/Assemblies.lagda.md

Lines changed: 204 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,204 @@
1+
<!--
2+
```agda
3+
open import 1Lab.Reflection.HLevel
4+
open import 1Lab.Reflection hiding (def ; absurd)
5+
6+
open import Cat.Functor.Adjoint
7+
open import Cat.Prelude
8+
9+
open import Data.Partial.Total
10+
open import Data.Partial.Base
11+
12+
open import Realisability.PCA
13+
14+
import Realisability.Data.Pair
15+
import Realisability.PCA.Sugar
16+
import Realisability.Base
17+
18+
open Functor
19+
open _=>_
20+
open _⊣_
21+
```
22+
-->
23+
24+
```agda
25+
module Cat.Instances.Assemblies
26+
{ℓA} {A : Type ℓA} ⦃ _ : H-Level A 2 ⦄ {_%_ : ↯ A → ↯ A → ↯ A} (p : is-pca _%_)
27+
where
28+
```
29+
30+
<!--
31+
```agda
32+
open Realisability.Data.Pair p
33+
open Realisability.PCA.Sugar p
34+
open Realisability.Base p
35+
36+
private variable
37+
ℓ ℓ' : Level
38+
```
39+
-->
40+
41+
# Assemblies over a PCA
42+
43+
```agda
44+
record Assembly ℓ : Type (lsuc ℓ ⊔ ℓA) where
45+
field
46+
Ob : Type ℓ
47+
has-is-set : is-set Ob
48+
realisers : Ob → ℙ⁺ A
49+
realised : ∀ x → ∃[ a ∈ ↯ A ] (a ∈ realisers x)
50+
```
51+
52+
<!--
53+
```agda
54+
open Assembly
55+
56+
private variable
57+
X Y Z : Assembly ℓ
58+
59+
instance
60+
Underlying-Assembly : Underlying (Assembly ℓ)
61+
Underlying-Assembly = record { ⌞_⌟ = Assembly.Ob }
62+
63+
hlevel-proj-asm : hlevel-projection (quote Assembly.Ob)
64+
hlevel-proj-asm .hlevel-projection.has-level = quote Assembly.has-is-set
65+
hlevel-proj-asm .hlevel-projection.get-level _ = pure (quoteTerm (suc (suc zero)))
66+
hlevel-proj-asm .hlevel-projection.get-argument (_ ∷ c v∷ _) = pure c
67+
{-# CATCHALL #-}
68+
hlevel-proj-asm .hlevel-projection.get-argument _ = typeError []
69+
70+
module _ (X : Assembly ℓ) (a : ↯ A) (x : ⌞ X ⌟) where open Ω (X .realisers x .mem a) renaming (∣_∣ to [_]_⊩_) public
71+
```
72+
-->
73+
74+
```agda
75+
record Assembly-hom (X : Assembly ℓ) (Y : Assembly ℓ') : Type (ℓA ⊔ ℓ ⊔ ℓ') where
76+
field
77+
map : ⌞ X ⌟ → ⌞ Y ⌟
78+
tracked : ∥ [ map ] X .realisers ⊢ Y .realisers ∥
79+
```
80+
81+
<!--
82+
```agda
83+
open Assembly-hom public
84+
85+
private unquoteDecl eqv = declare-record-iso eqv (quote Assembly-hom)
86+
87+
instance
88+
H-Level-Assembly-hom : ∀ {n} → H-Level (Assembly-hom X Y) (2 + n)
89+
H-Level-Assembly-hom = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2)
90+
91+
Extensional-Assembly-hom : ∀ {ℓr} ⦃ _ : Extensional (⌞ X ⌟ → ⌞ Y ⌟) ℓr ⦄ → Extensional (Assembly-hom X Y) ℓr
92+
Extensional-Assembly-hom ⦃ e ⦄ = injection→extensional! (λ p → Iso.injective eqv (Σ-prop-path! p)) e
93+
94+
Funlike-Assembly-hom : Funlike (Assembly-hom X Y) ⌞ X ⌟ λ _ → ⌞ Y ⌟
95+
Funlike-Assembly-hom = record { _·_ = λ f x → f .map x }
96+
97+
module _ where
98+
open Precategory
99+
```
100+
-->
101+
102+
```agda
103+
Assemblies : ∀ ℓ → Precategory (lsuc ℓ ⊔ ℓA) (ℓA ⊔ ℓ)
104+
Assemblies ℓ .Ob = Assembly ℓ
105+
Assemblies ℓ .Hom = Assembly-hom
106+
Assemblies ℓ .Hom-set x y = hlevel 2
107+
Assemblies ℓ .id = record
108+
{ map = λ x → x
109+
; tracked = inc id⊢
110+
}
111+
Assemblies ℓ ._∘_ f g = record
112+
{ map = λ x → f · (g · x)
113+
; tracked = ⦇ f .tracked ∘⊢ g .tracked ⦈
114+
}
115+
Assemblies ℓ .idr f = ext λ _ → refl
116+
Assemblies ℓ .idl f = ext λ _ → refl
117+
Assemblies ℓ .assoc f g h = ext λ _ → refl
118+
```
119+
120+
## Classical assemblies
121+
122+
```agda
123+
∇ : ∀ {ℓ} (X : Type ℓ) ⦃ _ : H-Level X 2 ⦄ → Assembly ℓ
124+
∇ X .Ob = X
125+
∇ X .has-is-set = hlevel 2
126+
∇ X .realisers x = record
127+
{ mem = def
128+
; defined = λ x → x
129+
}
130+
∇ X .realised x = inc (expr ⟨ x ⟩ x , abs↓ _ _)
131+
132+
Cofree : Functor (Sets ℓ) (Assemblies ℓ)
133+
Cofree .F₀ X = ∇ ⌞ X ⌟
134+
Cofree .F₁ f = record
135+
{ map = f
136+
; tracked = inc record
137+
{ realiser = val ⟨ x ⟩ x
138+
; tracks = λ a ha → subst ⌞_⌟ (sym (abs-β _ [] (a , ha))) ha
139+
}
140+
}
141+
Cofree .F-id = ext λ _ → refl
142+
Cofree .F-∘ f g = ext λ _ → refl
143+
144+
Forget : Functor (Assemblies ℓ) (Sets ℓ)
145+
Forget .F₀ X = el! ⌞ X ⌟
146+
Forget .F₁ f = f ·_
147+
Forget .F-id = refl
148+
Forget .F-∘ f g = refl
149+
150+
Forget⊣∇ : Forget {ℓ} ⊣ Cofree
151+
Forget⊣∇ .unit .η X = record
152+
{ map = λ x → x
153+
; tracked = inc record
154+
{ realiser = val ⟨ x ⟩ x
155+
; tracks = λ a ha → subst ⌞_⌟ (sym (abs-β _ [] (a , X .realisers _ .defined ha))) (X .realisers _ .defined ha)
156+
}
157+
}
158+
Forget⊣∇ .unit .is-natural x y f = ext λ _ → refl
159+
Forget⊣∇ .counit .η X a = a
160+
Forget⊣∇ .counit .is-natural x y f = refl
161+
Forget⊣∇ .zig = refl
162+
Forget⊣∇ .zag = ext λ _ → refl
163+
```
164+
165+
## The assembly of booleans
166+
167+
```agda
168+
𝟚 : Assembly lzero
169+
𝟚 .Ob = Bool
170+
𝟚 .has-is-set = hlevel 2
171+
𝟚 .realisers true = record
172+
{ mem = λ x → elΩ (`true .fst ≡ x)
173+
; defined = rec! λ p → subst ⌞_⌟ p (`true .snd)
174+
}
175+
𝟚 .realisers false = record
176+
{ mem = λ x → elΩ (`false .fst ≡ x)
177+
; defined = rec! λ p → subst ⌞_⌟ p (`false .snd)
178+
}
179+
𝟚 .realised true = inc (`true .fst , inc refl)
180+
𝟚 .realised false = inc (`false .fst , inc refl)
181+
```
182+
183+
```agda
184+
non-constant-nabla-map
185+
: (f : Assembly-hom (∇ Bool) 𝟚)
186+
→ f · true ≠ f · false
187+
→ `true .fst ≡ `false .fst
188+
non-constant-nabla-map f x = case f .tracked of λ where
189+
record { realiser = (fp , f↓) ; tracks = t } →
190+
let
191+
a = t {true} (`true .fst) (`true .snd)
192+
b = t {false} (`true .fst) (`true .snd)
193+
194+
cases
195+
: ∀ b b' (x : ↯ A)
196+
→ [ 𝟚 ] x ⊩ b → [ 𝟚 ] x ⊩ b'
197+
→ b ≠ b' → `true .fst ≡ `false .fst
198+
cases = λ where
199+
true true p → rec! λ rb rb' t≠t → absurd (t≠t refl)
200+
true false p → rec! λ rb rb' _ → rb ∙ sym rb'
201+
false true p → rec! λ rb rb' _ → rb' ∙ sym rb
202+
false false p → rec! λ rb rb' f≠f → absurd (f≠f refl)
203+
in cases (f · true) (f · false) _ a b x
204+
```

‎src/Data/Partial/Total.lagda.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,8 @@ instance
4646
H-Level-↯⁺ : ∀ {A : Type ℓ} {n} ⦃ _ : 2 ≤ n ⦄ ⦃ _ : H-Level A n ⦄ → H-Level (↯⁺ A) n
4747
H-Level-↯⁺ {n = suc (suc n)} ⦃ s≤s (s≤s p) ⦄ = hlevel-instance $
4848
embedding→is-hlevel (1 + n) (Subset-proj-embedding λ _ → hlevel 1) (hlevel (2 + n))
49+
50+
{-# OVERLAPPING H-Level-↯⁺ #-}
4951
```
5052
-->
5153

‎src/Realisability/Base.lagda.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ import Realisability.Data.Sum as sums
1616

1717
```agda
1818
module Realisability.Base
19-
{ℓ} {𝔸 : Type ℓ} (_%_ : ↯ 𝔸 → ↯ 𝔸 → ↯ 𝔸) (p : is-pca _%_)
19+
{ℓ} {𝔸 : Type ℓ} {_%_ : ↯ 𝔸 → ↯ 𝔸 → ↯ 𝔸} (p : is-pca _%_)
2020
where
2121
```
2222

0 commit comments

Comments
 (0)