removed instance mess

Author: effectfully

Coerce.agda

@@ -160,14 +160,14 @@ mutual
     π[ ptrans (pright (pcong (a ⊔ₘ_) qo) q) qa ] A (coerceUDesc qI qo qa ∘ D)
   coerceUDesc qI qo qa (D ⊛ E)          = coerceUDesc qI qo qa D ⊛ coerceUDesc qI qo qa E
 
-  coerceSem : ∀ {i₁ i₂ o₁ o₂ a₁ a₂ b₁ b₂} {ω₁ : Level o₁} {ω₂ : Level o₂}
-                {{β₁ : Level b₁}} {{β₂ : Level b₂}}
+  coerceSem : ∀ {i₁ i₂ o₁ o₂ a₁ a₂ b₁ b₂}
+                {ω₁ : Level o₁} {ω₂ : Level o₂} {β₁ : Level b₁} {β₂ : Level b₂}
                 {I₁ : Type i₁} {I₂ : Type i₂}
                 {F₁ : ⟦ I₁ ⟧ -> Univ β₁} {F₂ : ⟦ I₂ ⟧ -> Univ β₂}
             -> (D₁ : UDesc I₁ ω₁ a₁)
             -> (D₂ : UDesc I₂ ω₂ a₂)
             -> ⟦ D₁ ≅ᵈ D₂ ⟧
-            -> ⟦ F₁ ≅  F₂ ⟧
+            -> ⟦ F₁ ≅ F₂ ⟧
             -> (⟦ D₁ ⟧ᵈ λ x₁ -> ⟦ F₁ x₁ ⟧)
             -> (⟦ D₂ ⟧ᵈ λ x₂ -> ⟦ F₂ x₂ ⟧)
   coerceSem (var′ j₁)  (var′ j₂)   qj       qF  x      = coerce (qF j₁ j₂ qj) x
@@ -184,8 +184,8 @@ mutual
   coerceSem (_ ⊛ _ ) (var′ _) ()
   coerceSem (_ ⊛ _ ) (π′ _ _) ()
 
-  coerceExtend : ∀ {i₁ i₂ o₁ o₂ a₁ a₂ b₁ b₂} {ω₁ : Level o₁} {ω₂ : Level o₂}
-                   {{β₁ : Level b₁}} {{β₂ : Level b₂}}
+  coerceExtend : ∀ {i₁ i₂ o₁ o₂ a₁ a₂ b₁ b₂}
+                   {ω₁ : Level o₁} {ω₂ : Level o₂} {β₁ : Level b₁} {β₂ : Level b₂}
                    {I₁ : Type i₁} {I₂ : Type i₂}
                    {F₁ : ⟦ I₁ ⟧ -> Univ β₁} {F₂ : ⟦ I₂ ⟧ -> Univ β₂} {j₁ j₂}
                -> (D₁ : UDesc I₁ ω₁ a₁)
@@ -209,11 +209,11 @@ mutual
 
   coerceMu : ∀ {i₁ i₂ a₁ a₂} {α₁ : Level a₁} {α₂ : Level a₂}
                {I₁ : Type i₁} {I₂ : Type i₂} {D₁ : Desc I₁ α₁} {D₂ : Desc I₂ α₂} {j₁ j₂}
-           -> ⟦ D₁ ≊ᵈ D₂ ⟧ -> ⟦ j₁ ≅ j₂ ⟧ -> μ D₁ j₁ -> μ D₂ j₂
+           -> ⟦ D₁ ≊ᵈ D₂ ⟧ -> ⟦ j₁ ≅ j₂ ⟧ -> μ D₁ j₁ -> μ D₂ j₂     
   coerceMu {α₁ = lzero } {lzero }                qD qj (node e) =
     node (unwrap (proj₁ (qD _ _ qj) (wrap e)))
   coerceMu {α₁ = lsuc _} {lsuc _} {D₁ = D₁} {D₂} qD qj (node e) =
-    node (coerceExtend {{lsuc _}} {{lsuc _}} D₁ D₂ qD (λ _ _ -> _,_ qD) qj e)
+    node (coerceExtend D₁ D₂ qD (λ _ _ -> _,_ qD) qj e)
   coerceMu {α₁ = lzero } {lsuc _} ()
   coerceMu {α₁ = lsuc _} {lzero } ()
 

Core.agda

@@ -9,9 +9,12 @@ infixr 2 _⇒_ _⊛_
 infix  3 _≈_ _≃_ _≅_ _≅ᵉ_ _≅ᵈ_ _≊ᵈ_ _≅s_ _≅e_
 
 data Level : MetaLevel -> Set where
-  instance
-    lzero : Level lzeroₘ
-    lsuc  : ∀ a -> Level (lsucₘ a)
+  lzero : Level lzeroₘ
+  lsuc  : ∀ a -> Level (lsucₘ a)
+
+data SomeLevel : Set where
+  meta  : MetaLevel -> SomeLevel
+  level : ∀ {a} -> Level a -> SomeLevel
 
 natToMetaLevel : ℕ -> MetaLevel
 natToMetaLevel  0      = lzeroₘ
@@ -35,15 +38,14 @@ _⊔₀_ : ∀ {a b} -> Level a -> (β : Level b) -> Level (a ⊔ₘ₀ β)
 α ⊔₀ lzero  = lzero
 α ⊔₀ lsuc b = α ⊔ lsuc b
 
+meta-inj : ∀ {a b} -> meta a ≡ meta b -> a ≡ b
+meta-inj prefl = prefl
+
 Enum : ℕ -> Set
 Enum  0            = ⊥
 Enum  1            = ⊤
 Enum (suc (suc n)) = Maybe (Enum (suc n))
 
-data SomeLevel : Set where
-  meta  : MetaLevel -> SomeLevel
-  level : ∀ {a} -> Level a -> SomeLevel
-
 data Univ : ∀ {a} -> Level a -> Set
 
 Prop = Univ lzero
@@ -87,10 +89,10 @@ data Univ where
          -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔  β)
   π      : ∀ {a b} {α : Level a} {β : Level b}
          -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔₀ β)
-  udesc  : ∀ {o i} -> Type i -> Level o -> ∀ a -> {{α : Level a}} -> Type a
-  extend : ∀ {i o a b} {ω : Level o} {{β : Level b}} {I : Type i}
+  udesc  : ∀ {o i} -> Type i -> Level o -> ∀ a -> Type a
+  extend : ∀ {i o a b} {ω : Level o} {β : Level b} {I : Type i}
          -> UDesc I ω a -> (⟦ I ⟧ -> Univ β) -> ⟦ I ⟧ -> Univ β
-  imu    : ∀ {i a} {{α : Level a}} {I : Type i} -> Desc I α -> ⟦ I ⟧ -> Univ α
+  imu    : ∀ {i a} {α : Level a} {I : Type i} -> Desc I α -> ⟦ I ⟧ -> Univ α
 
 record μ {i a} {α : Level a} {I : Type i} (D : Desc I α) i : Set where
   inductive
@@ -121,7 +123,7 @@ _⇒_ : ∀ {a b} {α : Level a} {β : Level b} -> Univ α -> Univ β -> Univ (
 A ⇒ B = π A λ _ -> B
 
 desc : ∀ {a i} -> Type i -> Level a -> Type a
-desc I α = udesc I α _ {{α}}
+desc {a} I α = udesc I α a
 
 _≟ⁿ_ : ℕ -> ℕ -> Prop
 0     ≟ⁿ 0     = top
@@ -168,7 +170,7 @@ imu D₁ i₁          ≃ imu D₂ i₂          = D₁ ≊ᵈ D₂ & i₁ ≅
 _                  ≃ _                  = bot
 
 _≅e_ : ∀ {i₁ i₂ o₁ o₂ a₁ a₂ b₁ b₂}
-         {ω₁ : Level o₁} {ω₂ : Level o₂} {{β₁ : Level b₁}} {{β₂ : Level b₂}}
+         {ω₁ : Level o₁} {ω₂ : Level o₂} {β₁ : Level b₁} {β₂ : Level b₂}
          {I₁ : Type i₁} {I₂ : Type i₂} {F₁ : ⟦ I₁ ⟧ -> Univ β₁} {F₂ : ⟦ I₂ ⟧ -> Univ β₂} {j₁ j₂}
      -> (∃ λ (D₁ : UDesc I₁ ω₁ a₁) -> Extend D₁ (λ x₁ -> ⟦ F₁ x₁ ⟧) j₁)
      -> (∃ λ (D₂ : UDesc I₂ ω₂ a₂) -> Extend D₂ (λ x₂ -> ⟦ F₂ x₂ ⟧) j₂)
@@ -188,7 +190,7 @@ _≅_ {A = imu D₁ _     } {imu D₂ _     } a₁ a₂ = let node e₁ = a₁;
 _≅_                                     _  _  = bot
 
 _≅s_ : ∀ {i₁ i₂ o₁ o₂ a₁ a₂ b₁ b₂}
-         {ω₁ : Level o₁} {ω₂ : Level o₂} {{β₁ : Level b₁}} {{β₂ : Level b₂}}
+         {ω₁ : Level o₁} {ω₂ : Level o₂} {β₁ : Level b₁} {β₂ : Level b₂}
          {I₁ : Type i₁} {I₂ : Type i₂} {F₁ : ⟦ I₁ ⟧ -> Univ β₁} {F₂ : ⟦ I₂ ⟧ -> Univ β₂}
      -> (∃ λ (D₁ : UDesc I₁ ω₁ a₁) -> ⟦ D₁ ⟧ᵈ λ x₁ -> ⟦ F₁ x₁ ⟧)
      -> (∃ λ (D₂ : UDesc I₂ ω₂ a₂) -> ⟦ D₂ ⟧ᵈ λ x₂ -> ⟦ F₂ x₂ ⟧)
@@ -218,9 +220,6 @@ module _ {i o} {ω : Level o} {I : Type i} where
        -> (A : Univ α) -> UDesc I ω (a ⊔ₘ o) -> UDesc I ω (a ⊔ₘ o)
   A ⇒ᵈ D = πᵈ A λ _ -> D
 
-meta-inj : ∀ {a b} -> meta a ≡ meta b -> a ≡ b
-meta-inj prefl = prefl
-
 pattern #₀ p = node (tag  nothing                                   , p)
 pattern #₁ p = node (tag (just nothing)                             , p)
 pattern #₂ p = node (tag (just (just nothing))                      , p)

Data/List.agda

@@ -30,13 +30,13 @@ foldList f = elimList _ f
 length : ∀ {a} {A : Type a} -> List A -> ℕ
 length = foldList (const suc) 0
 
-icmu : ∀ {i} {{a}} {I : Type i} -> List (desc I (lsuc a)) -> ⟦ I ⟧ -> Type a
+icmu : ∀ {i a} {I : Type i} -> List (desc I (lsuc a)) -> ⟦ I ⟧ -> Type a
 icmu {I = I} Ds = imu $ πᵈ (enum (length Ds)) (go Ds ∘ detag) where
-  go : ∀ {a} -> (Ds : List (desc I (lsuc a))) -> Enum (length Ds) -> Desc I (lsuc a)
+  go : ∀ {a} {A : Type a} -> (xs : List A) -> Enum (length xs) -> ⟦ A ⟧
   go  []           ()
-  go (D ∷ [])      tt      = D
-  go (D ∷ E ∷ Ds)  nothing = D
-  go (D ∷ E ∷ Ds) (just e) = go (E ∷ Ds) e
+  go (x ∷ [])      tt      = x
+  go (x ∷ y ∷ xs)  nothing = x
+  go (x ∷ y ∷ xs) (just e) = go (y ∷ xs) e
 
 cmu : ∀ {a} -> List (desc unit (lsuc a)) -> Type a
 cmu Ds = icmu Ds triv

Data/Vec.agda

@@ -4,7 +4,7 @@ open import OTT.Main
 
 infixr 5 _∷ᵥ_
 
-vec : ∀ {{a}} -> Type a -> ℕ -> Type a
+vec : ∀ {a} -> Type a -> ℕ -> Type a
 vec A = icmu
       $ var 0
       ∷ (πᵈ nat λ n -> A ⇒ᵈ var n ⊛ var (suc n))

Data/W.agda

@@ -2,13 +2,6 @@ module OTT.Data.W where
 
 open import OTT.Main
 
--- instance
---   level-⊔ : ∀ {a b} {{α : Level a}} {{β : Level b}} -> Level (a ⊔ₘ b)
---   level-⊔ {{α}} {{β}} = α ⊔ β
-
--- w : ∀ {a b} {α : Level a} {β : Level b} -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔ β)
--- w {α = α} {β} A B = mu {{_}} (πᵈ {{α ⊔ β}} A λ x -> (_⇒ᵈ_ {{α ⊔ β}} (B x) pos) ⊛ pos)
-
 w : ∀ {a b} {α : Level a} {β : Level b} -> (A : Univ α) -> (⟦ A ⟧ -> Univ β) -> Univ (α ⊔ β)
 w A B = mu (πᵈ A λ x -> (B x ⇒ᵈ pos) ⊛ pos)