Skip to content

Commit 31ff70d

Browse files
pcapriottipcapriotti
committed
Prove homotopy-initiality of W types
1 parent e9a3bf9 commit 31ff70d

File tree

7 files changed

+313
-141
lines changed

7 files changed

+313
-141
lines changed

‎container/core.agda‎

Lines changed: 38 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,8 @@ module container.core where
44

55
open import level
66
open import sum
7-
open import function.core
7+
open import equality
8+
open import function
89

910
record Container (li la lb : Level) : Set (lsuc (li ⊔ la ⊔ lb)) where
1011
constructor container
@@ -31,10 +32,46 @@ record Container (li la lb : Level) : Set (lsuc (li ⊔ la ⊔ lb)) where
3132
→ (Y →ⁱ Z) → (X →ⁱ Y) → (X →ⁱ Z)
3233
(f ∘ⁱ g) i = f i ∘ g i
3334

35+
-- extensionality
36+
funext-isoⁱ : ∀ {lx ly} {X : I → Set lx}{Y : I → Set ly}
37+
→ {f g : X →ⁱ Y}
38+
→ (∀ i x → f i x ≡ g i x)
39+
≅ (f ≡ g)
40+
funext-isoⁱ {f = f}{g = g}
41+
= (Π-ap-iso refl≅ λ i → strong-funext-iso)
42+
·≅ strong-funext-iso
43+
44+
funext-invⁱ : ∀ {lx ly} {X : I → Set lx}{Y : I → Set ly}
45+
→ {f g : X →ⁱ Y}
46+
→ f ≡ g → ∀ i x → f i x ≡ g i x
47+
funext-invⁱ = invert funext-isoⁱ
48+
49+
funextⁱ : ∀ {lx ly} {X : I → Set lx}{Y : I → Set ly}
50+
→ {f g : X →ⁱ Y}
51+
→ (∀ i x → f i x ≡ g i x) → f ≡ g
52+
funextⁱ = apply funext-isoⁱ
53+
3454
-- morphism map for the functor F
3555
imap : ∀ {lx ly}
3656
→ {X : I → Set lx}
3757
→ {Y : I → Set ly}
3858
→ (X →ⁱ Y)
3959
→ (F X →ⁱ F Y)
4060
imap g i (a , f) = a , λ b → g (r b) (f b)
61+
62+
-- action of a functor on homotopies
63+
hmap : ∀ {lx ly}
64+
→ {X : I → Set lx}
65+
→ {Y : I → Set ly}
66+
→ {f g : X →ⁱ Y}
67+
→ (∀ i x → f i x ≡ g i x)
68+
→ (∀ i x → imap f i x ≡ imap g i x)
69+
hmap p i (a , u) = ap (_,_ a) (funext (λ b → p (r b) (u b)))
70+
71+
hmap-id : ∀ {lx ly}
72+
→ {X : I → Set lx}
73+
→ {Y : I → Set ly}
74+
→ (f : X →ⁱ Y)
75+
→ ∀ i x
76+
→ hmap (λ i x → refl {x = f i x}) i x ≡ refl
77+
hmap-id f i (a , u) = ap (ap (_,_ a)) (funext-id _)

‎container/w.agda‎

Lines changed: 2 additions & 130 deletions
Original file line numberDiff line numberDiff line change
@@ -1,132 +1,4 @@
11
module container.w where
22

3-
open import level
4-
open import sum
5-
open import equality
6-
open import function.extensionality
7-
open import function.isomorphism
8-
open import function.isomorphism.properties
9-
open import function.overloading
10-
open import sets.empty
11-
open import sets.nat.core using (suc)
12-
open import sets.unit
13-
open import hott.level
14-
open import container.core
15-
open import container.fixpoint
16-
open import container.equality
17-
18-
private
19-
module Definition {li la lb} (c : Container li la lb) where
20-
open Container c
21-
22-
-- definition of indexed W-types using a type family
23-
data W (i : I) : Set (la ⊔ lb) where
24-
sup : (a : A i) → ((b : B a) → W (r b)) → W i
25-
26-
-- initial F-algebra
27-
inW : F W →ⁱ W
28-
inW i (a , f) = sup a f
29-
30-
module Elim {lx} {X : I → Set lx}
31-
(α : F X →ⁱ X) where
32-
-- catamorphisms
33-
fold : W →ⁱ X
34-
fold i (sup a f) = α i (a , λ b → fold _ (f b))
35-
36-
-- computational rule for catamorphisms
37-
-- this holds definitionally
38-
fold-β : ∀ {i} (x : F W i) → fold i (inW i x) ≡ α i (imap fold i x)
39-
fold-β x = refl
40-
41-
-- η-rule, this is only propositional
42-
fold-η : (h : W →ⁱ X)
43-
→ (∀ {i} (x : F W i) → h i (inW i x) ≡ α i (imap h i x))
44-
→ ∀ {i} (x : W i) → h i x ≡ fold i x
45-
fold-η h p {i} (sup a f) = p (a , λ b → f b) · lem
46-
where
47-
lem : α i (a , (λ b → h _ (f b)))
48-
≡ α i (a , (λ b → fold _ (f b)))
49-
lem = ap (λ z → α i (a , z))
50-
(funext λ b → fold-η h p (f b))
51-
open Elim public
52-
53-
head : ∀ {i} → W i → A i
54-
head (sup a f) = a
55-
56-
tail : ∀ {i} (x : W i)(b : B (head x)) → W (r b)
57-
tail (sup a f) = f
58-
59-
fixpoint : (i : I) → W i ≅ F W i
60-
fixpoint _ = iso f g H K
61-
where
62-
f : {i : I} → W i → F W i
63-
f (sup a f) = a , f
64-
65-
g : {i : I} → F W i → W i
66-
g (a , f) = sup a f
67-
68-
H : {i : I}(w : W i) → g (f w) ≡ w
69-
H (sup a f) = refl
70-
71-
K : {i : I}(w : F W i) → f (g w) ≡ w
72-
K (a , f) = refl
73-
74-
private
75-
module Properties {li la lb}{c : Container li la lb} where
76-
open Container c
77-
open Definition c
78-
79-
open Equality c (fix W fixpoint)
80-
open Container equality
81-
using ()
82-
renaming (F to F-≡')
83-
open Definition equality
84-
using ()
85-
renaming ( W to W-≡
86-
; fixpoint to fixpoint-≡ )
87-
88-
F-≡ : ∀ {lx}
89-
→ (∀ {i} → W i → W i → Set lx)
90-
→ (∀ {i} → W i → W i → Set _)
91-
F-≡ X u v = F-≡' (λ {(i , u , v) → X {i} u v}) (_ , u , v)
92-
93-
_≡W_ : ∀ {i} → W i → W i → Set _
94-
_≡W_ {i} u v = W-≡ (i , u , v)
95-
96-
fixpoint-W : ∀ {i}{u v : W i} → (u ≡ v) ≅ F-≡ _≡_ u v
97-
fixpoint-W {i}{sup a f}{sup a' f'} = begin
98-
(sup a f ≡ sup a' f')
99-
≅⟨ iso≡ (fixpoint i) ⟩
100-
(apply (fixpoint i) (sup a f) ≡ apply (fixpoint i) (sup a' f'))
101-
≅⟨ sym≅ Σ-split-iso ⟩
102-
(Σ (a ≡ a') λ p → subst (λ a → (b : B a) → W (r b)) p f ≡ f')
103-
≅⟨ Σ-ap-iso refl≅ (substX-β f f') ⟩
104-
(Σ (a ≡ a') λ p → ∀ b → f b ≡ substX p b (f' (subst B p b)))
105-
∎
106-
where open ≅-Reasoning
107-
108-
str-iso : ∀ {i}{u v : W i} → (u ≡ v) ≅ (u ≡W v)
109-
str-iso {i}{sup a f}{sup a' f'} = begin
110-
(sup a f ≡ sup a' f')
111-
≅⟨ fixpoint-W ⟩
112-
(Σ (a ≡ a') λ p → ∀ b → f b ≡ substX p b (f' (subst B p b)))
113-
≅⟨ Σ-ap-iso refl≅ (λ a → Π-ap-iso refl≅ λ b → str-iso) ⟩
114-
(Σ (a ≡ a') λ p → ∀ b → f b ≡W substX p b (f' (subst B p b)))
115-
≅⟨ sym≅ (fixpoint-≡ _) ⟩
116-
(sup a f ≡W sup a' f')
117-
∎
118-
where open ≅-Reasoning
119-
120-
w-level : ∀ {n} → ((i : I) → h (suc n) (A i)) → (i : I) → h (suc n) (W i)
121-
w-level hA i (sup a f) (sup a' f') = iso-level (sym≅ lem)
122-
(Σ-level (hA i a a') (λ p → Π-level λ b → w-level hA _ _ _))
123-
where
124-
lem : ∀ {i}{a a' : A i}
125-
{f : (b : B a) → W (r b)}
126-
{f' : (b : B a') → W (r b)}
127-
→ (sup a f ≡ sup a' f')
128-
≅ Σ (a ≡ a') λ p → ∀ b → f b ≡ substX p b (f' (subst B p b))
129-
lem = fixpoint-W
130-
131-
open Definition public
132-
open Properties public using (w-level)
3+
open import container.w.core public
4+
open import container.w.algebra public

‎container/w/algebra.agda‎

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
{-# OPTIONS --without-K #-}
2+
module container.w.algebra where
3+
4+
open import sum
5+
open import equality
6+
open import container.core
7+
open import container.w.core
8+
open import function.extensionality
9+
open import function.isomorphism
10+
open import hott.level.core
11+
12+
module _ {li la lb}(c : Container li la lb) where
13+
open Container c
14+
15+
Alg : ∀ ℓ → Set _
16+
Alg ℓ = Σ (I → Set ℓ) λ X → F X →ⁱ X
17+
18+
carrier : ∀ {ℓ} → Alg ℓ → I → Set ℓ
19+
carrier (X , _) = X
20+
21+
IsMor : ∀ {ℓ₁ ℓ₂}(𝓧 : Alg ℓ₁)(𝓨 : Alg ℓ₂)
22+
→ (carrier 𝓧 →ⁱ carrier 𝓨) → Set _
23+
IsMor (X , θ) (Y , ψ) f = ψ ∘ⁱ imap f ≡ f ∘ⁱ θ
24+
25+
Mor : ∀ {ℓ₁ ℓ₂} → Alg ℓ₁ → Alg ℓ₂ → Set _
26+
Mor 𝓧 𝓨 = Σ (carrier 𝓧 →ⁱ carrier 𝓨) (IsMor 𝓧 𝓨)
27+
28+
𝓦 : Alg _
29+
𝓦 = W c , inW c
30+
31+
module _ {ℓ₁ ℓ₂}(𝓧 : Alg ℓ₁)(𝓨 : Alg ℓ₂) where
32+
private
33+
X = proj₁ 𝓧; θ = proj₂ 𝓧
34+
Y = proj₁ 𝓨; ψ = proj₂ 𝓨
35+
36+
is-mor-transp : {f g : X →ⁱ Y}(p : f ≡ g)
37+
→ (α : IsMor 𝓧 𝓨 f)
38+
→ sym (ap (λ h → ψ ∘ⁱ imap h) p) · α · ap (λ h → h ∘ⁱ θ) p
39+
≡ subst (IsMor 𝓧 𝓨) p α
40+
is-mor-transp {f} {.f} refl α = left-unit α
41+
42+
MorEq : Mor 𝓧 𝓨 → Mor 𝓧 𝓨 → Set _
43+
MorEq (f , α) (g , β) = Σ (f ≡ g) λ p
44+
→ sym (ap (λ h → ψ ∘ⁱ imap h) p) · α · ap (λ h → h ∘ⁱ θ) p ≡ β
45+
46+
MorH : Mor 𝓧 𝓨 → Mor 𝓧 𝓨 → Set _
47+
MorH (f , α) (g , β) = Σ (∀ i x → f i x ≡ g i x) λ p
48+
→ ∀ i x → sym (ap (ψ i) (hmap p i x)) · funext-invⁱ α i x · p i (θ i x)
49+
≡ funext-invⁱ β i x
50+
51+
mor-eq-h-iso : (f g : Mor 𝓧 𝓨) → MorEq f g ≅ MorH f g
52+
mor-eq-h-iso (f , α) (g , β) = Σ-ap-iso (sym≅ funext-isoⁱ) λ p → lem f g α β p
53+
where
54+
lem : (f g : X →ⁱ Y)(α : IsMor 𝓧 𝓨 f)(β : IsMor 𝓧 𝓨 g)(p : f ≡ g)
55+
→ (sym (ap (λ h → ψ ∘ⁱ imap h) p) · α · ap (λ h → h ∘ⁱ θ) p ≡ β)
56+
≅ (∀ i x → sym (ap (ψ i) (hmap (funext-invⁱ p) i x))
57+
· funext-invⁱ α i x
58+
· funext-invⁱ p i (θ i x)
59+
≡ funext-invⁱ β i x)
60+
lem f .f α β refl = begin
61+
(α · refl ≡ β)
62+
≅⟨ sym≅ (trans≡-iso (left-unit α)) ⟩
63+
(α ≡ β)
64+
≅⟨ iso≡ (sym≅ funext-isoⁱ) ⟩
65+
(funext-invⁱ α ≡ funext-invⁱ β)
66+
≅⟨ sym≅ ((Π-ap-iso refl≅ λ _ → strong-funext-iso) ·≅ strong-funext-iso) ⟩
67+
(∀ i x → funext-invⁱ α i x ≡ funext-invⁱ β i x)
68+
≅⟨ ( Π-ap-iso refl≅ λ i
69+
→ Π-ap-iso refl≅ λ x
70+
→ trans≡-iso (comp i x) ) ⟩
71+
(∀ i x → sym (ap (ψ i) (hmap (funext-invⁱ p₀) i x))
72+
· funext-invⁱ α i x
73+
· refl
74+
≡ funext-invⁱ β i x)
75+
∎
76+
where
77+
open ≅-Reasoning
78+
79+
p₀ : f ≡ f
80+
p₀ = refl
81+
82+
comp : ∀ i x → sym (ap (ψ i) (hmap (funext-invⁱ (refl {x = f})) i x))
83+
· funext-invⁱ α i x
84+
· refl
85+
≡ funext-invⁱ α i x
86+
comp i x = ap (λ q → sym (ap (ψ i) q) · funext-invⁱ α i x · refl)
87+
(hmap-id f i x)
88+
· left-unit (funext-invⁱ α i x)
89+
90+
eq-mor-iso : {f g : Mor 𝓧 𝓨} → (f ≡ g) ≅ MorH f g
91+
eq-mor-iso {f , α} {g , β} = begin
92+
((f , α) ≡ (g , β))
93+
≅⟨ sym≅ Σ-split-iso ⟩
94+
(Σ (f ≡ g) λ p → subst (IsMor 𝓧 𝓨) p α ≡ β)
95+
≅⟨ (Σ-ap-iso refl≅ λ p → trans≡-iso (is-mor-transp p α)) ⟩
96+
MorEq (f , α) (g , β)
97+
≅⟨ mor-eq-h-iso _ _ ⟩
98+
MorH (f , α) (g , β)
99+
∎
100+
where
101+
open ≅-Reasoning
102+
103+
module _ {ℓ} (𝓧 : Alg ℓ) where
104+
private
105+
X = proj₁ 𝓧; θ = proj₂ 𝓧
106+
107+
lem : ∀ {ℓ}{A : Set ℓ}{x y z w : A}
108+
→ (p : x ≡ w) (q : y ≡ x) (r : y ≡ z) (s : z ≡ w)
109+
→ p ≡ sym q · r · s → sym r · q · p ≡ s
110+
lem p refl refl refl α = α
111+
112+
W-mor-prop : (f g : Mor 𝓦 𝓧) → f ≡ g
113+
W-mor-prop (f , α) (g , β) = invert (eq-mor-iso 𝓦 𝓧) (p , p-h)
114+
where
115+
p : ∀ i x → f i x ≡ g i x
116+
p i (sup a u)
117+
= sym (funext-invⁱ α i (a , u))
118+
· ap (θ i) (ap (_,_ a) (funext (λ b → p (r b) (u b))))
119+
· funext-invⁱ β i (a , u)
120+
121+
p-h : ∀ i x
122+
→ sym (ap (θ i) (hmap p i x))
123+
· funext-invⁱ α i x
124+
· p i (inW c i x)
125+
≡ funext-invⁱ β i x
126+
p-h i (a , u) = lem (p i (sup a u))
127+
(funext-invⁱ α i (a , u)) _
128+
(funext-invⁱ β i (a , u))
129+
refl
130+
131+
W-mor : Mor 𝓦 𝓧
132+
W-mor = fold c θ , funextⁱ (λ i x → fold-β c θ x)
133+
134+
W-initial : contr (Mor 𝓦 𝓧)
135+
W-initial = W-mor , W-mor-prop W-mor

0 commit comments

Comments
 (0)