desc₋₁

Core.agda

@@ -123,6 +123,9 @@ pattern type a = univ (lsuc a)
 univ# = univ  ∘ natToLevel
 type# = univ# ∘ suc
 
+desc₋₁ : ∀ {a i} {ι : Level i} -> Type ι -> (α : Level a) -> Univ _
+desc₋₁ I α = desc I (lsuc lzero ⊔ α)
+
 _&_ : ∀ {a b} {α : Level a} {β : Level b} -> Univ α -> Univ β -> Univ (α ⊔  β)
 A & B = σ A λ _ -> B
 

Data/Fin.agda

@@ -11,7 +11,7 @@ fin = icmu
 Fin : ℕ -> Set
 Fin n = ⟦ fin n ⟧
 
-pattern fzeroₑ {n} q   = #₀  (n , q)
+pattern fzeroₑ {n} q   =  #₀ (n , q)
 pattern fsucₑ  {n} q i = !#₁ (n , i , q)
 
 fzero : ∀ {n} -> Fin (suc n)

Data/List.agda

@@ -13,7 +13,7 @@ list A = mu $ π (enum 2) (fromTuple (pos , (A ⇨ pos ⊛ pos)))
 List : ∀ {a} {α : Level a} -> Univ α -> Set
 List A = ⟦ list A ⟧
 
-pattern []       = #₀ tt
+pattern []       =  #₀  tt
 pattern _∷_ x xs = !#₁ (x , xs , tt)
 
 elimList : ∀ {a π} {α : Level a} {A : Univ α}
@@ -42,9 +42,9 @@ icmu Ds = imu $ π (enum (length Ds)) (fromList Ds)
 cmu : ∀ {a} {α : Level a} -> List (desc unit (lsuc α)) -> Type α
 cmu Ds = icmu Ds triv
 
-icmu′ : ∀ {i a} {ι : Level i} {I : Type ι}
-      -> (α : Level a) -> List (desc I α) -> ⟦ I ⟧ -> Type₋₁ α
-icmu′ α Ds = imu $ π (enum (length Ds)) (liftDesc ∘ fromList Ds)
+icmu₋₁ : ∀ {i a} {ι : Level i} {I : Type ι}
+       -> (α : Level a) -> List (desc₋₁ I α) -> ⟦ I ⟧ -> Type₋₁ α
+icmu₋₁ α Ds = imu $ π (enum (length Ds)) (fromList Ds)
 
-cmu′ : ∀ {a} -> (α : Level a) -> List (desc unit α) -> Type₋₁ α
-cmu′ α Ds = icmu′ α Ds triv
+cmu₋₁ : ∀ {a} -> (α : Level a) -> List (desc₋₁ unit α) -> Type₋₁ α
+cmu₋₁ α Ds = icmu₋₁ α Ds triv

Data/Maybe.agda

@@ -3,12 +3,15 @@ module OTT.Data.Maybe where
 open import OTT.Main
 
 maybe : ∀ {a} {α : Level a} -> Univ α -> Type₋₁ α
-maybe {α = α} A = cmu′ α $ pos ∷ (A ⇨ pos) ∷ []
+maybe {α = α} A = cmu₋₁ α
+                $ pos
+                ∷ (A ⇨ pos)
+                ∷ []
 
 Maybe : ∀ {a} {α : Level a} -> Univ α -> Set
 Maybe A = ⟦ maybe A ⟧
 
-pattern nothing = #₀  tt
+pattern nothing =  #₀  tt
 pattern just x  = !#₁ (x , tt)
 
 elimMaybe : ∀ {a π} {α : Level a} {A : Univ α} {P : Maybe A -> Set π}

Data/Sum.agda

@@ -5,12 +5,15 @@ open import OTT.Main
 infixr 3 _⊕_ _⊎_
 
 _⊕_ : ∀ {a b} {α : Level a} {β : Level b} -> Univ α -> Univ β -> Type₋₁ (α ⊔ β)
-_⊕_ {α = α} {β} A B = cmu′ (α ⊔ β) $ (A ⇨ pos) ∷ (B ⇨ pos) ∷ []
+_⊕_ {α = α} {β} A B = cmu₋₁ (α ⊔ β)
+                    $ (A ⇨ pos)
+                    ∷ (B ⇨ pos)
+                    ∷ []
 
 _⊎_ : ∀ {a b} {α : Level a} {β : Level b} -> Univ α -> Univ β -> Set
 A ⊎ B = ⟦ A ⊕ B ⟧
 
-pattern inj₁ x = #₀ (x , tt)
+pattern inj₁ x =  #₀ (x , tt)
 pattern inj₂ y = !#₁ (y , tt)
 
 [_,_] : ∀ {a b π} {α : Level a} {β : Level b} {A : Univ α} {B : Univ β} {P : A ⊎ B -> Set π}

Data/Vec.agda

@@ -4,25 +4,25 @@ open import OTT.Main
 
 infixr 5 _∷ᵥ_
 
-vec : ∀ {a} {α : Level a} -> Type α -> ℕ -> Type α
-vec {α = α} A = icmu
-      $ var 0
-      ∷ (π nat λ n -> A ⇨ var n ⊛ var (suc n))
-      ∷ []
+vec : ∀ {a} {α : Level a} -> Univ α -> ℕ -> Type₋₁ α
+vec {α = α} A = icmu₋₁ α
+              $ var 0
+              ∷ (π nat λ n -> A ⇨ var n ⊛ var (suc n))
+              ∷ []
 
-Vec : ∀ {a} {α : Level a} -> Type α -> ℕ -> Set
+Vec : ∀ {a} {α : Level a} -> Univ α -> ℕ -> Set
 Vec A n = ⟦ vec A n ⟧
 
-pattern vnilₑ      q      = #₀ q
+pattern vnilₑ      q      =  #₀  q
 pattern vconsₑ {n} q x xs = !#₁ (n , x , xs , q)
 
-[]ᵥ : ∀ {a} {α : Level a} {A : Type α} -> Vec A 0
+[]ᵥ : ∀ {a} {α : Level a} {A : Univ α} -> Vec A 0
 []ᵥ = vnilₑ (refl 0)
 
-_∷ᵥ_ : ∀ {n a} {α : Level a} {A : Type α} -> ⟦ A ⇒ vec A n ⇒ vec A (suc n) ⟧
+_∷ᵥ_ : ∀ {n a} {α : Level a} {A : Univ α} -> ⟦ A ⇒ vec A n ⇒ vec A (suc n) ⟧
 _∷ᵥ_ {n} = vconsₑ (refl (suc n))
 
-gelimVec : ∀ {n a π} {α : Level a} {A : Type α}
+gelimVec : ∀ {n a π} {α : Level a} {A : Univ α}
          -> (P : ∀ {n} -> Vec A n -> Set π)
          -> (∀ {n m} {xs : Vec A n}
                -> (q : ⟦ suc n ≅ m ⟧) -> (x : ⟦ A ⟧) -> P xs -> P {m} (vconsₑ q x xs))
@@ -31,22 +31,22 @@ gelimVec : ∀ {n a π} {α : Level a} {A : Type α}
          -> P xs
 gelimVec P f z = gelim P (fromTuple ((λ _ -> z) , (λ n x xs r _ q -> f q x r)))
 
-foldVec : ∀ {n a π} {α : Level a} {A : Type α} {P : Set π}
+foldVec : ∀ {n a π} {α : Level a} {A : Univ α} {P : Set π}
         -> (⟦ A ⟧ -> P -> P) -> P -> Vec A n -> P
 foldVec f z = gelimVec _ (const f) (const z)
 
-fromVec : ∀ {n a} {α : Level a} {A : Type α} -> Vec A n -> List A
+fromVec : ∀ {n a} {α : Level a} {A : Univ α} -> Vec A n -> List A
 fromVec = foldVec _∷_ []
 
-elimVec′ : ∀ {n a π} {α : Level a} {A : Type α}
+elimVec′ : ∀ {n a π} {α : Level a} {A : Univ α}
          -> (P : List A -> Set π)
          -> (∀ {n} {xs : Vec A n} -> (x : ⟦ A ⟧) -> P (fromVec xs) -> P (x ∷ fromVec xs))
          -> P []
          -> (xs : Vec A n)
          -> P (fromVec xs)
 elimVec′ P f z = gelimVec (P ∘ fromVec) (λ {n m xs} _ -> f {xs = xs}) (const z)
 
-elimVec : ∀ {n a p} {α : Level a} {π : Level p} {A : Type α}
+elimVec : ∀ {n a p} {α : Level a} {π : Level p} {A : Univ α}
         -> (P : ∀ {n} -> Vec A n -> Univ π)
         -> (∀ {n} {xs : Vec A n} -> (x : ⟦ A ⟧) -> ⟦ P xs ⇒ P (x ∷ᵥ xs) ⟧)
         -> ⟦ P []ᵥ ⟧

Function/Erase.agda

@@ -10,12 +10,12 @@ unitView : ∀ {a} {α : Level a} -> (A : Univ α) -> UnitView A
 unitView unit = yes-unit
 unitView A    = no-unit
 
-Erase : ∀ {i b} {I : Type i} {β : Level b} -> Desc I β -> Desc unit β
+Erase : ∀ {i b} {ι : Level i} {I : Type ι} {β : Level b} -> Desc I β -> Desc unit β
 Erase (var i) = pos
 Erase (π A D) = π A (λ x -> Erase (D x))
 Erase (D ⊛ E) = Erase D ⊛ Erase E
 
-module _ {i b} {I : Type i} {β : Level b} {D : Desc I β} where
+module _ {i b} {ι : Level i} {I : Type ι} {β : Level b} {D : Desc I β} where
   mutual
     eraseSem : (E : Desc I β) -> ⟦ E ⟧ᵈ (μ D) -> ⟦ Erase E ⟧ᵈ (μ (Erase D))
     eraseSem (var i)  d      = erase d
@@ -31,7 +31,7 @@ module _ {i b} {I : Type i} {β : Level b} {D : Desc I β} where
     erase : ∀ {j} -> μ D j -> μ (Erase D) triv
     erase (node e) = node (eraseExtend D e)
 
-module _ {i b} {I : Type i} {β : Level b} {B} where
+module _ {i b} {ι : Level i} {I : Type ι} {β : Level b} {B} where
   mutual
     eraseConstSem : (D : Desc I β) -> ⟦ D ⟧ᵈ (const B) -> ⟦ Erase D ⟧ᵈ (const B)
     eraseConstSem (var i)  y      = y
@@ -57,12 +57,12 @@ module _ {b} {β : Level b} {B : Unit -> Set} where
     uneraseExtend (π A D) (x , e) = x , uneraseExtend (D x) e
     uneraseExtend (D ⊛ E) (x , e) = uneraseSem D x , uneraseExtend E e
 
-CheckErase : ∀ {i b} {I : Type i} {β : Level b} -> Desc I β -> Desc unit β
+CheckErase : ∀ {i b} {ι : Level i} {I : Type ι} {β : Level b} -> Desc I β -> Desc unit β
 CheckErase {I = I} D with unitView I
 ... | yes-unit = D
 ... | no-unit  = Erase D
 
-checkErase : ∀ {i b} {I : Type i} {β : Level b} {D : Desc I β} {j}
+checkErase : ∀ {i b} {ι : Level i} {I : Type ι} {β : Level b} {D : Desc I β} {j}
            -> μ D j -> μ (CheckErase D) triv
 checkErase {I = I} d with unitView I
 ... | yes-unit = d

readme.md

@@ -4,7 +4,7 @@ It's an implementation of Observational Type Theory as an Agda library. The univ
 
 ## Details
 
-(The readme is a bit old, a `Level` now fully reifies the corresponding `MetaLevel`)
+(The readme is a bit old: a `Level` now fully reifies the corresponding `MetaLevel` and there is also a [generic machinery](https://github.com/effectfully/OTT/blob/master/Function/Elim.agda) which allows to derive intensional-type-theory-like eliminators which is annoying to do by hand when a data type is indexed and you need to explicitly use `J`)
 
 There are two main kinds of universe levels (there is also yet another one, but it's not important): metatheory levels (the usual `Level` type renamed to `MetaLevel`) and target theory levels, indexed by metalevels: