From 75542d1be240cf2d88906ecb209e73b8ff2fabab Mon Sep 17 00:00:00 2001
From: effectfully <effectfully@gmail.com>
Date: Tue, 12 Jul 2016 12:21:23 +0300
Subject: [PATCH] =?UTF-8?q?desc=E2=82=8B=E2=82=81?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Core.agda           |  3 +++
 Data/Fin.agda       |  2 +-
 Data/List.agda      | 12 ++++++------
 Data/Maybe.agda     |  7 +++++--
 Data/Sum.agda       |  7 +++++--
 Data/Vec.agda       | 28 ++++++++++++++--------------
 Function/Erase.agda | 10 +++++-----
 readme.md           |  2 +-
 8 files changed, 40 insertions(+), 31 deletions(-)

diff --git a/Core.agda b/Core.agda
index f81e7e2..bbeee85 100644
--- a/Core.agda
+++ b/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
 
diff --git a/Data/Fin.agda b/Data/Fin.agda
index c7f5e1e..ff41e4e 100644
--- a/Data/Fin.agda
+++ 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)
diff --git a/Data/List.agda b/Data/List.agda
index 967e943..4e53e46 100644
--- a/Data/List.agda
+++ b/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
diff --git a/Data/Maybe.agda b/Data/Maybe.agda
index 34c41b7..ba67012 100644
--- a/Data/Maybe.agda
+++ b/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 π}
diff --git a/Data/Sum.agda b/Data/Sum.agda
index 8d949c1..f093812 100644
--- a/Data/Sum.agda
+++ b/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 π}
diff --git a/Data/Vec.agda b/Data/Vec.agda
index 5c857fc..2f4d3da 100644
--- a/Data/Vec.agda
+++ b/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,14 +31,14 @@ 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 []
@@ -46,7 +46,7 @@ elimVec′ : ∀ {n a π} {α : Level a} {A : Type α}
          -> 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 []ᵥ ⟧
diff --git a/Function/Erase.agda b/Function/Erase.agda
index 160350c..0ff5c0a 100644
--- a/Function/Erase.agda
+++ b/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
diff --git a/readme.md b/readme.md
index 6a5f2f7..29f4f61 100644
--- a/readme.md
+++ b/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: