{-# OPTIONS --without-K #-}
module mctt where
data Cxt : Set
data Kind : Cxt → Set
data Ty : Cxt → Set
data Sub : Cxt → Cxt → Set
data Tm : (cxt : Cxt) → Kind cxt → Set
data _≣_ : {cxt : Cxt} → Kind cxt → Kind cxt → Set
data _≡_ : {cxt : Cxt} → Ty cxt → Ty cxt → Set
data _≗_ : {cxt : Cxt} → {k : Kind cxt} → Tm cxt k → Tm cxt k → Set
data Cxt where
ε : Cxt
_,_ : (cxt : Cxt) → (t : Ty cxt) → Cxt
_,,_ : (cxt : Cxt) → (k : Kind cxt) → Cxt
infixl 8 _,_ _,,_
data Kind where
U : {cxt : Cxt} → Kind cxt
Π : {cxt : Cxt} → (t : Ty cxt) → (k : Kind (cxt , t)) → Kind cxt
_[_] : {cxt1 cxt2 : Cxt} → (k : Kind cxt2) → (f : Sub cxt1 cxt2) → Kind cxt1
data Ty where
el : {cxt : Cxt} → (x : Tm cxt U) → Ty cxt
_[_] : {cxt1 cxt2 : Cxt} → (t : Ty cxt2) → (f : Sub cxt1 cxt2) → Ty cxt1
data Sub where
id : {cxt : Cxt} → Sub cxt cxt
_∘_ : {cxt1 cxt2 cxt3 : Cxt} → (g : Sub cxt2 cxt3) → (f : Sub cxt1 cxt2) → Sub cxt1 cxt3
kpop : {cxt : Cxt} → (k : Kind cxt) → Sub (cxt ,, k) cxt
tpop : {cxt : Cxt} → (t : Ty cxt) → Sub (cxt , t) cxt
_≪_ : {cxt1 cxt2 : Cxt} → {k : Kind cxt2} → (f : Sub cxt1 cxt2) → Tm cxt1 (k [ f ]) → Sub cxt1 (cxt2 ,, k)
_id≪≣_ : (cxt : Cxt) → {k1 : Kind cxt} → {k2 : Kind cxt} → (k1 ≣ k2) → Sub (cxt ,, k1) (cxt ,, k2)
_id<≡_ : (cxt : Cxt) → {t1 : Ty cxt} → {t2 : Ty cxt} → (t1 ≡ t2) → Sub (cxt , t1) (cxt , t2)
_<id_ : {cxt1 cxt2 : Cxt} → (f : Sub cxt1 cxt2) → (t : Ty cxt2) → Sub (cxt1 , t [ f ]) (cxt2 , t)
data Tm where
ktop : {cxt : Cxt} → {k : Kind cxt} → Tm (cxt ,, k) (k [ kpop k ])
_[_] : {cxt1 cxt2 : Cxt} → {k : Kind cxt2} → Tm cxt2 k → (f : Sub cxt1 cxt2) → Tm cxt1 (k [ f ])
ap : {cxt : Cxt} → {t : Ty cxt} → {k : Kind (cxt , t)} → Tm cxt (Π t k) → Tm (cxt , t) k
coe : {cxt : Cxt} → {k1 k2 : Kind cxt} → (k1 ≣ k2) → Tm cxt k1 → Tm cxt k2
data _≣_ where
refl≣ : {cxt : Cxt} → (k : Kind cxt) → (k ≣ k)
_•_ : {cxt : Cxt} → {k1 k2 k3 : Kind cxt} → (k2 ≣ k3) → (k1 ≣ k2) → (k1 ≣ k3)
_⁻¹ : {cxt : Cxt} → {k1 k2 : Kind cxt} → (k1 ≣ k2) → (k2 ≣ k1)
k[id] : {cxt : Cxt} → (k : Kind cxt) → (k ≣ k [ id ])
k[∘] : {cxt1 cxt2 cxt3 : Cxt} → (k : Kind cxt3) → (f2 : Sub cxt2 cxt3) → (f1 : Sub cxt1 cxt2) →
k [ f2 ] [ f1 ] ≣ k [ f2 ∘ f1 ]
U[] : {cxt1 cxt2 : Cxt} → (f : Sub cxt1 cxt2) → U [ f ] ≣ U
Π[] : {cxt1 cxt2 : Cxt} → (t : Ty cxt2) → (k : Kind (cxt2 , t)) → (f : Sub cxt1 cxt2) →
(Π t k) [ f ] ≣ (Π (t [ f ]) (k [ f <id t ]))
Π≣ : {cxt : Cxt} → (t : Ty cxt) → {k k' : Kind (cxt , t)} → (k ≣ k') → (Π t k ≣ Π t k')
_[_] : {cxt1 cxt2 : Cxt} → {k1 k2 : Kind cxt2} → (k1 ≣ k2) → (f : Sub cxt1 cxt2) → (k1 [ f ] ≣ k2 [ f ])
ktpop≣ : {cxt : Cxt} → (h k : Kind cxt) → (t : Ty cxt) →
h [ kpop k ] [ tpop (t [ kpop k ]) ] ≣ h [ tpop t ] [ kpop k <id t ]
kpop∘≪ : {cxt1 cxt2 : Cxt} {k : Kind cxt2} (f : Sub cxt1 cxt2) (x : Tm cxt1 (k [ f ])) →
k [ f ] ≣ (k [ kpop k ]) [ f ≪ x ]
data _≡_ where
refl≡ : {cxt : Cxt} → (t : Ty cxt) → (t ≡ t)
_•_ : {cxt : Cxt} → {t1 t2 t3 : Ty cxt} → (t2 ≡ t3) → (t1 ≡ t2) → (t1 ≡ t3)
_⁻¹ : {cxt : Cxt} → {t1 t2 : Ty cxt} → (t1 ≡ t2) → (t2 ≡ t1)
t[id] : {cxt : Cxt} → (t : Ty cxt) → (t ≡ t [ id ])
t[∘] : {cxt1 cxt2 cxt3 : Cxt} → (t : Ty cxt3) → (f2 : Sub cxt2 cxt3) → (f1 : Sub cxt1 cxt2) →
t [ f2 ] [ f1 ] ≡ t [ f2 ∘ f1 ]
el[] : {cxt1 cxt2 : Cxt} → (x : Tm cxt2 U) → (f : Sub cxt1 cxt2) → (el x [ f ] ≡ el (coe (U[] f) (x [ f ])))
_[_] : {cxt1 cxt2 : Cxt} → {t1 t2 : Ty cxt2} → (t1 ≡ t2) → (f : Sub cxt1 cxt2) → (t1 [ f ] ≡ t2 [ f ])
ktpop≡ : {cxt : Cxt} → (s : Ty cxt) → (k : Kind cxt) → (t : Ty cxt) →
s [ kpop k ] [ tpop (t [ kpop k ]) ] ≡ s [ tpop t ] [ kpop k <id t ]
data _≗_ where
refl≗ : {cxt : Cxt} → {k : Kind cxt} → (x : Tm cxt k) → (x ≗ x)
_•_ : {cxt : Cxt} → {k : Kind cxt} → {x1 x2 x3 : Tm cxt k} → (x2 ≗ x3) → (x1 ≗ x2) → (x1 ≗ x3)
_⁻¹ : {cxt : Cxt} → {k : Kind cxt} → {x1 x2 : Tm cxt k} → (x1 ≗ x2) → (x2 ≗ x1)
coe-id : {cxt : Cxt} → {k : Kind cxt} → (x : Tm cxt k) → coe (refl≣ k) x ≗ x
coe• : {cxt : Cxt} → {k1 k2 k3 : Kind cxt} → (x : Tm cxt k1) → (e2 : k2 ≣ k3) → (e1 : k1 ≣ k2) →
coe e2 (coe e1 x) ≗ coe (e2 • e1) x
coe[] : {cxt1 cxt2 : Cxt} → {k1 k2 : Kind cxt2} → (eq : k1 ≣ k2) → (x : Tm cxt2 k1) → (f : Sub cxt1 cxt2) →
coe eq x [ f ] ≗ coe (eq [ f ]) (x [ f ])
ktop≪ : {cxt1 cxt2 : Cxt} → {k : Kind cxt2} → (f : Sub cxt1 cxt2) → (x : Tm cxt1 (k [ f ])) →
ktop [ f ≪ x ] ≗ coe (kpop∘≪ f x) x
_<≡_ : {cxt1 cxt2 : Cxt} → (f : Sub cxt1 cxt2) → {t1 : Ty cxt1} → {t2 : Ty cxt2} → (t1 ≡ t2 [ f ]) → Sub (cxt1 , t1) (cxt2 , t2)
_<≡_ {cxt1} {cxt2} f {t1} {t2} eq = (f <id t2) ∘ (cxt1 id<≡ eq)
_≪id_ : {cxt1 cxt2 : Cxt} → (f : Sub cxt1 cxt2) → (k : Kind cxt2) → Sub (cxt1 ,, k [ f ]) (cxt2 ,, k)
f ≪id k = (f ∘ kpop (k [ f ])) ≪ coe (k[∘] _ _ _) (ktop {_} {k [ f ]})
_≪≣_ : {cxt1 cxt2 : Cxt} → (f : Sub cxt1 cxt2) → {k1 : Kind cxt1} → {k2 : Kind cxt2} → (k1 ≣ k2 [ f ]) → Sub (cxt1 ,, k1) (cxt2 ,, k2)
_≪≣_ f {k1} {k2} eq = (f ≪id k2) ∘ (_ id≪≣ eq)
tpop-kpop : {cxt : Cxt} → (t : Ty cxt) → (k : Kind cxt) → Sub ((cxt ,, k) , t [ kpop k ]) ((cxt , t) ,, k [ tpop t ])
tpop-kpop {cxt} t k = (kpop k <id t) ≪ coe (ktpop≣ k k t) (ktop [ tpop (t [ kpop k ]) ])
Πap-sub : {cxt : Cxt} → (t : Ty cxt) → (k : Kind (cxt , t)) → Sub ((cxt ,, Π t k) , t [ kpop (Π t k) ]) ((cxt , t) ,, k)
Πap-sub {cxt} t k = (kpop (Π t k) <id t) ≪ ap (coe (Π[] t k (kpop (Π t k))) ktop)
infixl 8 _<id_ _id<≡_ _<≡_
infixl 8 _≪id_ _id≪≣_ _≪≣_
infixl 8 _≪_
infixl 8 _∘_ _•_