Newer
Older
{-# OPTIONS --cubical --rewriting --guarded #-}
{-# OPTIONS --guardedness #-}
{-# OPTIONS -W noUnsupportedIndexedMatch #-}
-- to allow opening this module in other files while there are still holes
{-# OPTIONS --allow-unsolved-metas #-}
module Semantics.Adequacy.Coinductive.DelayCoalgebra where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sum
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Functions.Embedding
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit renaming (Unit to ⊤)
open import Cubical.Foundations.Isomorphism
import Cubical.Data.Equality as Eq
open import Common.Common
open import Semantics.Adequacy.Coinductive.Delay
private
variable
ℓ : Level
module _ (X : Type ℓ) (isSetX : isSet X) where
record Coalg (ℓc : Level) : Type (ℓ-suc (ℓ-max ℓ ℓc)) where
field
V : Type ℓc
un : V -> (X ⊎ V)
liftSum : {ℓA ℓB : Level} -> {A : Type ℓA} -> {B : Type ℓB} ->
(A -> B) -> (X ⊎ A) -> (X ⊎ B)
liftSum f (inl x) = inl x
liftSum f (inr a) = inr (f a)
open Coalg
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
CoalgMorphism : {ℓ1 ℓ2 : Level} (c : Coalg ℓ1) (d : Coalg ℓ2) ->
Type (ℓ-max (ℓ-max ℓ ℓ1) ℓ2)
CoalgMorphism c d = Σ[ h ∈ (c .V -> d .V) ]
d .un ∘ h ≡ liftSum h ∘ c .un
final-coalgebra : ∀ {ℓd : Level} -> Coalg ℓd ->
Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓd))
final-coalgebra {ℓd} d = ∀ (c : Coalg ℓd) -> isContr (CoalgMorphism c d)
unfold-delay : Delay X -> X ⊎ Delay X
unfold-delay d with (view d)
... | done x = inl x
... | running d' = inr d'
unfold-delay-inv : X ⊎ Delay X -> Delay X
unfold-delay-inv (inl x) .view = done x
unfold-delay-inv (inr d) .view = running d
-- Might be able to simplify this because d .view is isomorphic to X + Delay X
delay-iso-sum : Iso (Delay X) (X ⊎ Delay X)
delay-iso-sum = iso unfold-delay unfold-delay-inv sec retr
where
sec : section unfold-delay unfold-delay-inv
sec (inl x) = refl
sec (inr d) = refl
retr : retract unfold-delay unfold-delay-inv
retr d i .view with d .view
... | done x = done x
... | running d' = running d'
unfold-delay-inj : (d1 d2 : Delay X) ->
unfold-delay d1 ≡ unfold-delay d2 -> d1 ≡ d2
unfold-delay-inj d1 d2 eq = isoFunInjective delay-iso-sum d1 d2 eq
unfold-inv1 : (d : Delay X) -> (x : X) ->
unfold-delay d ≡ inl x -> d .view ≡ done x
unfold-inv1 d x H =
cong view (isoFunInjective delay-iso-sum d (doneD x) H)
unfold-inv2 : (d : Delay X) -> (d' : Delay X) ->
unfold-delay d ≡ inr d' -> d .view ≡ running d'
unfold-inv2 d d' H =
cong view (isoFunInjective delay-iso-sum d (stepD d') H)
DelayCoalg : Coalg ℓ
DelayCoalg = record {
V = Delay X ;
un = unfold-delay }
DelayCoalgFinal : {ℓc : Level} ->
(c : Coalg ℓ) ->
isContr (CoalgMorphism c DelayCoalg) -- i.e. isContr (Σ[ h ∈ (c .V -> Delay X) ] unfold-delay ∘ h ≡ liftSum h ∘ c. un)
(fun , (funExt commute)) , unique' (fun , funExt commute)
where
fun : c .V -> Delay X
view (fun v) with c .un v
... | inl x = done x
... | inr v' = running (fun v')
commute : (v : c. V) -> (DelayCoalg .un ∘ fun) v ≡ (liftSum fun ∘ c .un) v
commute v with c. un v
... | inl x = refl
... | inr v' = refl
unique' : (s s' : Σ[ h ∈ (c .V → Delay X) ]
(unfold-delay ∘ (h) ≡ liftSum h ∘ (c .un))) ->
s ≡ s'
unique' (h , com) (h' , com') =
Σ≡Prop (λ g -> isSetΠ (λ v -> isSet⊎ isSetX (isSetDelay isSetX)) _ _) (funExt eq-fun)
where
eq-fun : (v : c .V) -> h v ≡ h' v
view (eq-fun v i) with c .un v in eq
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
... | inl x = view (unfold-delay-inj (h v) (h' v) (com-v ∙ sym com'-v) i)
where
com-v : (unfold-delay (h v)) ≡ inl x
com-v = funExtS⁻ com v ∙ (λ j -> liftSum h (Eq.eqToPath eq j))
com'-v : (unfold-delay (h' v)) ≡ inl x
com'-v = funExtS⁻ com' v ∙ (λ j -> liftSum h' (Eq.eqToPath eq j))
... | inr v' = (goal (h v .view) (h' v .view)
(Eq.pathToEq eq-hv) (Eq.pathToEq eq-h'v) i)
-- We state an auxiliary goal to which we pass the equalities eq-hv and eq-h'v
-- as the built-in equality type so we can pattern match.
-- If we tried to use transport instead, the termination checker would complain.
where
com-v : unfold-delay (h v) ≡ inr (h v')
com-v = funExtS⁻ com v ∙ λ j -> liftSum h (Eq.eqToPath eq j)
com'-v : unfold-delay (h' v) ≡ inr (h' v')
com'-v = funExtS⁻ com' v ∙ λ j -> liftSum h' (Eq.eqToPath eq j)
eq-hv : h v .view ≡ running (h v')
eq-hv = unfold-inv2 (h v) (h v') com-v
eq-h'v : h' v .view ≡ running (h' v')
eq-h'v = unfold-inv2 (h' v) (h' v') com'-v
goal : ∀ s1 s2 ->
s1 Eq.≡ running (h v') ->
s2 Eq.≡ running (h' v') ->
s1 ≡ s2
goal .(running (h v')) .(running (h' v')) Eq.refl Eq.refl =
cong running (eq-fun v')