Make unit level polymorphic

pcapriotti · Jun 4, 2015 · 9cf9e3f · 9cf9e3f
1 parent d18f57d
commit 9cf9e3f
Show file tree

Hide file tree

Showing 10 changed files with 125 additions and 114 deletions.
diff --git a/container/m/from-nat/coalgebra.agda b/container/m/from-nat/coalgebra.agda
@@ -18,11 +18,11 @@ module _ {li la lb} (c : Container li la lb) where
   open import container.m.coalgebra c hiding (_≅_; module _≅_)
 
   Xⁱ : ℕ → I → Set (la ⊔ lb)
-  Xⁱ zero = λ _ → ↑ _ ⊤
+  Xⁱ zero = λ _ → ⊤
   Xⁱ (suc n) = F (Xⁱ n)
 
   πⁱ : ∀ n → Xⁱ (suc n) →ⁱ Xⁱ n
-  πⁱ zero = λ _ _ → lift tt
+  πⁱ zero = λ _ _ → tt
   πⁱ (suc n) = imap (πⁱ n)
 
   module _ (i : I) where
@@ -129,7 +129,7 @@ module _ {li la lb} (c : Container li la lb) where
         open cones c Xⁱ πⁱ 𝓩
 
         X₀-contr : ∀ i → contr (X i 0)
-        X₀-contr i = ↑-level _ ⊤-contr
+        X₀-contr i = ⊤-contr
 
         Z→X₀-contr : contr (Z →ⁱ Xⁱ 0)
         Z→X₀-contr = Π-level λ i → Π-level λ _ → X₀-contr i
@@ -138,7 +138,7 @@ module _ {li la lb} (c : Container li la lb) where
         step v = imap v ∘ⁱ θ
 
         Φ₀ : Cone₀ → Cone₀
-        Φ₀ u 0 = λ _ _ → lift tt
+        Φ₀ u 0 = λ _ _ → tt
         Φ₀ u (suc n) = step (u n)
 
         Φ₀' : Cone → Cone₀
@@ -155,7 +155,7 @@ module _ {li la lb} (c : Container li la lb) where
         Φ (u , q) = (Φ₀ u , Φ₁ u q)
 
         u₀ : Cone₀
-        u₀ zero = λ _ _ → lift tt
+        u₀ zero = λ _ _ → tt
         u₀ (suc n) = step (u₀ n)
 
         p₀ : ∀ n → u₀ n ≡ Φ₀ u₀ n
@@ -175,7 +175,7 @@ module _ {li la lb} (c : Container li la lb) where
         Fix₀-iso = begin
             ( Σ Cone₀ λ u → u ≡ Φ₀ u )
           ≅⟨ ( Σ-ap-iso refl≅ λ u → sym≅ strong-funext-iso ·≅ ℕ-elim-shift ) ⟩
-            ( Σ Cone₀ λ u → (u 0 ≡ λ _ _ → lift tt)
+            ( Σ Cone₀ λ u → (u 0 ≡ λ _ _ → tt)
                           × (∀ n → u (suc n) ≡ step (u n)) )
           ≅⟨ ( Σ-ap-iso refl≅ λ u → (×-ap-iso (contr-⊤-iso (h↑ Z→X₀-contr _ _)) refl≅)
                                   ·≅ ×-left-unit ) ⟩

diff --git a/decidable.agda b/decidable.agda
@@ -2,7 +2,7 @@
 
 module decidable where
 
-open import level using (Level)
+open import level
 open import sets.empty using (⊥; ¬_)
 open import sets.unit using (⊤; tt)
 
@@ -12,7 +12,7 @@ data Dec {i} (P : Set i) : Set i where
   yes : ( p :   P) → Dec P
   no  : (¬p : ¬ P) → Dec P
 
-True : ∀ {i}{P : Set i} → Dec P → Set
+True : ∀ {i}{P : Set i} → Dec P → Set lzero
 True (yes _) = ⊤
 True (no _) = ⊥
 

diff --git a/function/extensionality/proof.agda b/function/extensionality/proof.agda
@@ -8,27 +8,22 @@ open import function.extensionality.core
 open import hott.univalence
 open import hott.level.core
 open import hott.level.closure.core
+open import hott.level.sets.core
 open import hott.equivalence.core
 open import sets.unit
 
-top : ∀ {i} → Set i
-top = ↑ _ ⊤
-
-⊤-contr' : ∀ {i} → contr (↑ i ⊤)
-⊤-contr' {i} = lift tt , λ { (lift tt) → refl }
-
 -- this uses definitional η for ⊤
-contr-exp-⊤ : ∀ {i j}{A : Set i} → contr (A → top {j})
-contr-exp-⊤ = (λ _ → lift tt) , (λ f → refl)
+contr-exp-⊤ : ∀ {i j}{A : Set i} → contr (A → ⊤ {j})
+contr-exp-⊤ = (λ _ → tt) , (λ f → refl)
 
 module Weak where
   →-contr : ∀ {i j}{A : Set i}{B : Set j}
           → contr B
           → contr (A → B)
   →-contr {A = A}{B = B} hB = subst contr p contr-exp-⊤
     where
-      p : (A → top) ≡ (A → B)
-      p = ap (λ X → A → X) (unique-contr ⊤-contr' hB)
+      p : (A → ⊤) ≡ (A → B)
+      p = ap (λ X → A → X) (unique-contr ⊤-contr hB)
 
   funext : ∀ {i j}{A : Set i}{B : Set j}
       → (f : A → B)(b : B)(h : (x : A) → b ≡ f x)
@@ -45,10 +40,10 @@ abstract
           → contr ((x : A) → B x)
   Π-contr {i}{j}{A}{B} hB = subst contr p contr-exp-⊤
     where
-      p₀ : (λ _ → top) ≡ B
-      p₀ = Weak.funext B top (λ x → unique-contr ⊤-contr' (hB x))
+      p₀ : (λ _ → ⊤) ≡ B
+      p₀ = Weak.funext B ⊤ (λ x → unique-contr ⊤-contr (hB x))
 
-      p : (A → top {j}) ≡ ((x : A) → B x)
+      p : (A → ⊤ {j}) ≡ ((x : A) → B x)
       p = ap (λ Z → (x : A) → Z x) p₀
 
   private

diff --git a/function/isomorphism/utils.agda b/function/isomorphism/utils.agda
@@ -2,6 +2,7 @@
 
 module function.isomorphism.utils where
 
+open import level
 open import sum
 open import equality.core
 open import equality.calculus
@@ -285,22 +286,22 @@ impl-iso = record
       ; (inj₂ x) → refl }
   ; iso₂ = λ { (g₁ , g₂) → refl } }
 
-×-left-unit : ∀ {i}{X : Set i} → (⊤ × X) ≅ X
+×-left-unit : ∀ {i j}{X : Set i} → (⊤ {j} × X) ≅ X
 ×-left-unit = record
   { to = λ {(tt , x) → x }
   ; from = λ x → tt , x
   ; iso₁ = λ _ → refl
   ; iso₂ = λ _ → refl }
 
-×-right-unit : ∀ {i}{X : Set i} → (X × ⊤) ≅ X
+×-right-unit : ∀ {i j}{X : Set i} → (X × ⊤ {j}) ≅ X
 ×-right-unit = record
   { to = λ {(x , tt) → x }
   ; from = λ x → x , tt
   ; iso₁ = λ _ → refl
   ; iso₂ = λ _ → refl }
 
 contr-⊤-iso : ∀ {i}{X : Set i}
-            → contr X → X ≅ ⊤
+            → contr X → X ≅ ⊤ {lzero}
 contr-⊤-iso hX = record
   { to = λ x → tt
   ; from = λ { tt → proj₁ hX }
@@ -323,8 +324,8 @@ empty-⊥-iso u = record
   ; iso₁ = λ _ → refl
   ; iso₂ = λ _ → refl }
 
-Π-left-unit : ∀ {i}{X : Set i}
-            → (⊤ → X) ≅ X
+Π-left-unit : ∀ {i j}{X : Set i}
+            → (⊤ {j} → X) ≅ X
 Π-left-unit = record
   { to = λ f → f tt
   ; from = λ x _ → x

diff --git a/hott/level/sets.agda b/hott/level/sets.agda
@@ -1,85 +1,5 @@
 {-# OPTIONS --without-K #-}
 module hott.level.sets where
 
-open import level
-open import decidable
-open import sum
-open import equality.core
-open import equality.calculus
-open import equality.reasoning
-open import function.core
-open import function.extensionality.proof
-open import sets.empty
-open import sets.unit
-open import hott.level.core
-
--- ⊤ is contractible
-⊤-contr : contr ⊤
-⊤-contr = tt , λ { tt → refl }
-
--- ⊥ is propositional
-⊥-prop : h 1 ⊥
-⊥-prop x _ = ⊥-elim x
-
-⊥-initial : ∀ {i} {A : Set i} → contr (⊥ → A)
-⊥-initial = (λ ()) , (λ f → funext λ ())
-
--- Hedberg's theorem
-hedberg : ∀ {i} {A : Set i}
-        → ((x y : A) → Dec (x ≡ y))
-        → h 2 A
-hedberg {A = A} dec x y = prop⇒h1 ≡-prop
-  where
-    open ≡-Reasoning
-
-    canonical : {x y : A} → x ≡ y → x ≡ y
-    canonical {x} {y} p with dec x y
-    ... | yes q = q
-    ... | no _ = p
-
-    canonical-const : {x y : A}
-                    → (p q : x ≡ y)
-                    → canonical p ≡ canonical q
-    canonical-const {x} {y} p q with dec x y
-    ... | yes _ = refl
-    ... | no f = ⊥-elim (f p)
-
-    canonical-inv : {x y : A}(p : x ≡ y)
-                  → canonical p · sym (canonical refl) ≡ p
-    canonical-inv refl = left-inverse (canonical refl)
-
-    ≡-prop : {x y : A}(p q : x ≡ y) → p ≡ q
-    ≡-prop p q = begin
-        p
-      ≡⟨ sym (canonical-inv p) ⟩
-        canonical p · sym (canonical refl)
-      ≡⟨ ap (λ z → z · sym (canonical refl))
-              (canonical-const p q) ⟩
-        canonical q · sym (canonical refl)
-      ≡⟨ canonical-inv q ⟩
-        q
-      ∎
-
--- Bool is a set
-private
-  module BoolSet where
-    open import sets.bool
-    bool-set : h 2 Bool
-    bool-set = hedberg _≟_
-open BoolSet public
-
--- Nat is a set
-private
-  module NatSet where
-    open import sets.nat.core
-    nat-set : h 2 ℕ
-    nat-set = hedberg _≟_
-open NatSet public
-
--- Fin is a set
-private
-  module FinSet where
-    open import sets.fin.core
-    fin-set : ∀ n → h 2 (Fin n)
-    fin-set n = hedberg _≟_
-open FinSet public
+open import hott.level.sets.core public
+open import hott.level.sets.extra public
diff --git a/hott/level/sets/core.agda b/hott/level/sets/core.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --without-K #-}
+module hott.level.sets.core where
+
+open import sum
+open import equality.core
+open import sets.unit
+open import sets.empty
+open import hott.level.core
+
+⊤-contr : ∀ {i} → contr (⊤ {i})
+⊤-contr = tt , λ { tt → refl }
+
+⊥-prop : h 1 ⊥
+⊥-prop x _ = ⊥-elim x
diff --git a/hott/level/sets/extra.agda b/hott/level/sets/extra.agda
@@ -0,0 +1,77 @@
+{-# OPTIONS --without-K #-}
+module hott.level.sets.extra where
+
+open import level
+open import decidable
+open import sum
+open import equality.core
+open import equality.calculus
+open import equality.reasoning
+open import function.core
+open import function.extensionality.proof
+open import sets.empty
+open import sets.unit
+open import hott.level.core
+
+⊥-initial : ∀ {i} {A : Set i} → contr (⊥ → A)
+⊥-initial = (λ ()) , (λ f → funext λ ())
+
+-- Hedberg's theorem
+hedberg : ∀ {i} {A : Set i}
+        → ((x y : A) → Dec (x ≡ y))
+        → h 2 A
+hedberg {A = A} dec x y = prop⇒h1 ≡-prop
+  where
+    open ≡-Reasoning
+
+    canonical : {x y : A} → x ≡ y → x ≡ y
+    canonical {x} {y} p with dec x y
+    ... | yes q = q
+    ... | no _ = p
+
+    canonical-const : {x y : A}
+                    → (p q : x ≡ y)
+                    → canonical p ≡ canonical q
+    canonical-const {x} {y} p q with dec x y
+    ... | yes _ = refl
+    ... | no f = ⊥-elim (f p)
+
+    canonical-inv : {x y : A}(p : x ≡ y)
+                  → canonical p · sym (canonical refl) ≡ p
+    canonical-inv refl = left-inverse (canonical refl)
+
+    ≡-prop : {x y : A}(p q : x ≡ y) → p ≡ q
+    ≡-prop p q = begin
+        p
+      ≡⟨ sym (canonical-inv p) ⟩
+        canonical p · sym (canonical refl)
+      ≡⟨ ap (λ z → z · sym (canonical refl))
+              (canonical-const p q) ⟩
+        canonical q · sym (canonical refl)
+      ≡⟨ canonical-inv q ⟩
+        q
+      ∎
+
+-- Bool is a set
+private
+  module BoolSet where
+    open import sets.bool
+    bool-set : h 2 Bool
+    bool-set = hedberg _≟_
+open BoolSet public
+
+-- Nat is a set
+private
+  module NatSet where
+    open import sets.nat.core
+    nat-set : h 2 ℕ
+    nat-set = hedberg _≟_
+open NatSet public
+
+-- Fin is a set
+private
+  module FinSet where
+    open import sets.fin.core
+    fin-set : ∀ n → h 2 (Fin n)
+    fin-set n = hedberg _≟_
+open FinSet public
diff --git a/sets/fin/universe.agda b/sets/fin/universe.agda
@@ -1,6 +1,7 @@
 {-# OPTIONS --without-K  #-}
 module sets.fin.universe where
 
+open import level
 open import sum
 open import decidable
 open import equality.core
@@ -28,7 +29,7 @@ open import hott.level.core
 open import hott.level.closure
 open import hott.level.sets
 
-fin-struct-iso : ∀ {n} → Fin (suc n) ≅ (⊤ ⊎ Fin n)
+fin-struct-iso : ∀ {n} → Fin (suc n) ≅ (⊤ {lzero} ⊎ Fin n)
 fin-struct-iso = record
   { to = λ { zero → inj₁ tt; (suc i) → inj₂ i }
   ; from = [ (λ _ → zero) ,⊎ (suc) ]
@@ -38,7 +39,7 @@ fin-struct-iso = record
 fin0-empty : ⊥ ≅ Fin 0
 fin0-empty = sym≅ (empty-⊥-iso (λ ()))
 
-fin1-unit : ⊤ ≅ Fin 1
+fin1-unit : ∀ {i} → ⊤ {i} ≅ Fin 1
 fin1-unit = record
   { to = λ _ → zero
   ; from = λ { zero → tt ; (suc ()) }

diff --git a/sets/nat/struct.agda b/sets/nat/struct.agda
@@ -1,6 +1,7 @@
 {-# OPTIONS --without-K #-}
 module sets.nat.struct where
 
+open import level
 open import sum
 open import equality
 open import function
@@ -15,14 +16,14 @@ open import hott.level
 
 ℕ-c : Container _ _ _
 ℕ-c = record
-  { I = ⊤
+  { I = ⊤ {lzero}
   ; A = λ _ → Fin 2
   ; B = ⊥ ∷∷ ⊤ ∷∷ ⟦⟧
   ; r = λ _ → tt }
 
 open Container ℕ-c
 
-ℕ-algebra-iso : (⊤ ⊎ ℕ) ≅ ℕ
+ℕ-algebra-iso : (⊤ {lzero} ⊎ ℕ) ≅ ℕ
 ℕ-algebra-iso = record
   { to = λ { (inj₁ _) → zero ; (inj₂ n) → suc n }
   ; from = λ { zero → inj₁ tt ; (suc n) → inj₂ n }