-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathZOL2.lagda
130 lines (107 loc) · 6.27 KB
/
ZOL2.lagda
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
\begin{code}
{-# OPTIONS --prop --rewriting #-}
open import PropUtil
module ZOL2 where
open import Agda.Primitive
open import ListUtil
variable
ℓ¹ ℓ² ℓ³ ℓ⁴ : Level
ℓ¹' ℓ²' ℓ³' ℓ⁴' : Level
record ZOL : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴)) where
infixr 10 _∘_
field
--# We first make the base category with its terminal object
Con : Set ℓ¹
Sub : Con → Con → Prop ℓ² -- It makes a posetal category
_∘_ : {Γ Δ Ξ : Con} → Sub Δ Ξ → Sub Γ Δ → Sub Γ Ξ
id : {Γ : Con} → Sub Γ Γ
◇ : Con -- The terminal object of the category
ε : {Γ : Con} → Sub Γ ◇ -- The morphism from any object to the terminal
--# Categorical equations don't need to be stated as the category is *posetal*
--∘-ass : {Γ Δ Ξ Ψ : Con}{α : Sub Γ Δ}{β : Sub Δ Ξ}{γ : Sub Ξ Ψ}
--idl : {Γ Δ : Con} {σ : Sub Γ Δ} → (id {Δ}) ∘ σ ≡ σ
--idr : {Γ Δ : Con} {σ : Sub Γ Δ} → σ ∘ (id {Γ}) ≡ σ
-- → (γ ∘ β) ∘ α ≡ γ ∘ (β ∘ α)
--ε-u : {Γ : Con} → {σ : Sub Γ ◇} → σ ≡ ε {Γ}
--# Functor Con → Set called For
For : Con → Set ℓ³
_[_]f : {Γ Δ : Con} → For Γ → Sub Δ Γ → For Δ -- Action on morphisms
[]f-id : {Γ : Con} → {F : For Γ} → F [ id {Γ} ]f ≡ F
[]f-∘ : {Γ Δ Ξ : Con} → {α : Sub Ξ Δ} → {β : Sub Δ Γ} → {F : For Γ}
→ F [ β ∘ α ]f ≡ (F [ β ]f) [ α ]f
--# Functor Con × For → Prop called Pf or ⊢
Pf : (Γ : Con) → For Γ → Prop ℓ⁴
-- Action on morphisms
_[_]p : {Γ Δ : Con} → {F : For Γ} → Pf Γ F → (σ : Sub Δ Γ) → Pf Δ (F [ σ ]f)
--# Equalities below are useless because Pf Γ F is in prop
-- []p-id : {Γ : Con} → {F : For Γ} → {prf : Pf Γ F}
-- → prf [ id {Γ} ]p ≡ prf
-- []p-∘ : {Γ Δ Ξ : Con}{α : Sub Ξ Δ}{β : Sub Δ Γ}{F : For Γ}{prf : Pf Γ F}
-- → prf [ α ∘ β ]p ≡ (prf [ β ]p) [ α ]p
--# → Prop⁺
_▹ₚ_ : (Γ : Con) → For Γ → Con
πₚ¹ : {Γ Δ : Con}{F : For Γ} → Sub Δ (Γ ▹ₚ F) → Sub Δ Γ
πₚ² : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ (Γ ▹ₚ F)) → Pf Δ (F [ πₚ¹ σ ]f)
_,ₚ_ : {Γ Δ : Con}{F : For Γ} → (σ : Sub Δ Γ) → Pf Δ (F [ σ ]f) → Sub Δ (Γ ▹ₚ F)
--# Equality below are useless because Pf and Sub are in Prop
--,ₚ∘πₚ : {Γ Δ : Con}{F : For Γ}{σ : Sub Δ (Γ ▹ₚ F)} → (πₚ¹ σ) ,ₚ (πₚ² σ) ≡ σ
--πₚ¹∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Pf Δ (F [ σ ]f)}
-- → πₚ¹ (σ ,ₚ prf) ≡ σ
-- πₚ²∘,ₚ : {Γ Δ : Con}{σ : Sub Δ Γ}{F : For Γ}{prf : Pf Δ (F [ σ ]f)}
-- → πₚ² (σ ,ₚ prf) ≡ prf
--,ₚ∘ : {Γ Δ Ξ : Con}{σ : Sub Γ Ξ}{δ : Sub Δ Γ}{F : For Ξ}{prf : Pf Γ (F [ σ ]f)}
-- → (σ ,ₚ prf) ∘ δ ≡ (σ ∘ δ) ,ₚ (substP (Pf Δ) (≡sym []f-∘) (prf [ δ ]p))
--#
{-- FORMULAE CONSTRUCTORS --}
--# i formula
ι : {Γ : Con} → For Γ
[]f-ι : {Γ Δ : Con} {σ : Sub Δ Γ}→ ι [ σ ]f ≡ ι
--# Implication
_⇒_ : {Γ : Con} → For Γ → For Γ → For Γ
[]f-⇒ : {Γ Δ : Con} → {F G : For Γ} → {σ : Sub Δ Γ}
→ (F ⇒ G) [ σ ]f ≡ (F [ σ ]f) ⇒ (G [ σ ]f)
--#
{-- PROOFS CONSTRUCTORS --}
-- Again, we don't have to write the _[_]p equalities as Proofs are in Prop
--# Lam & App
lam : {Γ : Con}{F G : For Γ} → Pf (Γ ▹ₚ F) (G [ πₚ¹ id ]f) → Pf Γ (F ⇒ G)
app : {Γ : Con}{F G : For Γ} → Pf Γ (F ⇒ G) → Pf Γ F → Pf Γ G
--#
record Mapping (S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) (D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ¹' ⊔ ℓ²' ⊔ ℓ³' ⊔ ℓ⁴')) where
field
--#
mCon : (ZOL.Con S) → (ZOL.Con D)
mSub : {Δ : (ZOL.Con S)}{Γ : (ZOL.Con S)} →
(ZOL.Sub S Δ Γ) → (ZOL.Sub D (mCon Δ) (mCon Γ))
mFor : {Γ : (ZOL.Con S)} → (ZOL.For S Γ) → (ZOL.For D (mCon Γ))
mPf : {Γ : (ZOL.Con S)} {A : ZOL.For S Γ}
→ ZOL.Pf S Γ A → ZOL.Pf D (mCon Γ) (mFor A)
--#
record Morphism (S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}) (D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ¹' ⊔ ℓ²' ⊔ ℓ³' ⊔ ℓ⁴')) where
field m : Mapping S D
mCon = Mapping.mCon m
mSub = Mapping.mSub m
mFor = Mapping.mFor m
mPf = Mapping.mPf m
field
--#
e◇ : mCon (ZOL.◇ S) ≡ ZOL.◇ D
e[]f : {Γ Δ : ZOL.Con S}{A : ZOL.For S Γ}{σ : ZOL.Sub S Δ Γ} →
mFor (ZOL._[_]f S A σ) ≡ ZOL._[_]f D (mFor A) (mSub σ)
e▹ₚ : {Γ : ZOL.Con S}{A : ZOL.For S Γ} →
mCon (ZOL._▹ₚ_ S Γ A) ≡ ZOL._▹ₚ_ D (mCon Γ) (mFor A)
eι : {Γ : ZOL.Con S} → mFor (ZOL.ι S {Γ}) ≡ ZOL.ι D {mCon Γ}
e⇒ : {Γ : ZOL.Con S}{A B : ZOL.For S Γ} →
mFor (ZOL._⇒_ S A B) ≡ ZOL._⇒_ D (mFor A) (mFor B)
-- No equation needed for lam, app, ∀i, ∀e as their output are in prop
--#
record TrNat {S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}} {D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}} (a : Mapping S D) (b : Mapping S D) : Set (lsuc (ℓ¹ ⊔ ℓ² ⊔ ℓ³ ⊔ ℓ⁴ ⊔ ℓ¹' ⊔ ℓ²' ⊔ ℓ³' ⊔ ℓ⁴')) where
field
f : (Γ : ZOL.Con S) → ZOL.Sub D (Mapping.mCon a Γ) (Mapping.mCon b Γ)
-- Unneeded because Sub are in prop
--eq : (Γ Δ : ZOL.Con S)(σ : ZOL.Sub S Γ Δ) → (ZOL._∘_ D (f Δ) (Mapping.mSub a σ)) ≡ (ZOL._∘_ D (Mapping.mSub b σ) (f Γ))
_∘TrNat_ : {S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}}{D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}}{a b c : Mapping S D} → TrNat a b → TrNat b c → TrNat a c
_∘TrNat_ {D = D} α β = record { f = λ Γ → ZOL._∘_ D (TrNat.f β Γ) (TrNat.f α Γ) }
idTrNat : {S : ZOL {ℓ¹} {ℓ²} {ℓ³} {ℓ⁴}}{D : ZOL {ℓ¹'} {ℓ²'} {ℓ³'} {ℓ⁴'}}{a : Mapping S D} → TrNat a a
idTrNat {D = D} = record { f = λ Γ → ZOL.id D }
\end{code}