Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
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
{-# OPTIONS --cubical --rewriting --guarded #-}
module Later where
-- | This file is from the supplementary material for the paper
-- | https://doi.org/10.1145/3372885.3373814
-- | and is originally written by Niccolò Veltri and Andrea Vezzosi
-- | see the LICENSE.txt for their license.
open import Agda.Builtin.Equality renaming (_≡_ to _≣_)
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Sigma
open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
module Prims where
primitive
primLockUniv : Set₁
open Prims renaming (primLockUniv to LockU) public
private
variable
l : Level
A B : Set l
-- We postulate Tick as it is supposed to be an abstract sort.
postulate
Tick : LockU
▹_ : ∀ {l} → Set l → Set l
▹_ A = (@tick x : Tick) -> A
▸_ : ∀ {l} → ▹ Set l → Set l
▸ A = (@tick x : Tick) → A x
next : A → ▹ A
next x _ = x
_⊛_ : ▹ (A → B) → ▹ A → ▹ B
_⊛_ f x a = f a (x a)
map▹ : (f : A → B) → ▹ A → ▹ B
map▹ f x α = f (x α)
-- The behaviour of fix is encoded with rewrite rules, following the
-- definitional equalities of TCTT.
postulate
dfix : ∀ {l} {A : Set l} → (f : ▹ A → A) → I → ▹ A
dfix-beta : ∀ {l} {A : Set l} → (f : ▹ A → A) → dfix f i1 ≣ next (f (dfix f i0))
{-# REWRITE dfix-beta #-}
pfix : ∀ {l} {A : Set l} → (f : ▹ A → A) → dfix f i0 ≡ next (f (dfix f i0))
pfix f i = dfix f i
abstract
fix : ∀ {l} {A : Set l} → (f : ▹ A → A) → A
fix f = f (pfix f i0)
fix-eq : ∀ {l} {A : Set l} → (f : ▹ A → A) → fix f ≡ f (next (fix f))
fix-eq f = cong f (pfix f)
later-ext : ∀ {A : ▹ Set} → {f g : ▸ A} → (▸ \ a → f a ≡ g a) → f ≡ g
later-ext eq i a = eq a i
transpLater : ∀ (A : I → ▹ Set) → ▸ (A i0) → ▸ (A i1)
transpLater A u0 a = transp (\ i → A i a) i0 (u0 a)
hcompLater : ∀ (A : ▹ Set) φ (u : I → Partial φ (▸ A)) → (u0 : ▸ A [ φ ↦ u i0 ]) → ▸ A
hcompLater A φ u u0 a = hcomp (\ { i (φ = i1) → u i 1=1 a }) (outS u0 a)