Prove the univalent subuniverse structure of UFin

Fixes #55
vikraman · Jan 26, 2021 · 911baa7 · 911baa7
1 parent a507db2
commit 911baa7
Show file tree

Hide file tree

Showing 7 changed files with 163 additions and 96 deletions.
diff --git a/Pi+/Equiv2.agda b/Pi+/Equiv2.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --without-K --exact-split --allow-unsolved-metas --rewriting #-}
+{-# OPTIONS --without-K --exact-split --allow-unsolved-metas --rewriting --overlapping-instances #-}
 
 module Pi+.Equiv2 where
 
@@ -29,4 +29,4 @@ quote-eval₂ : {X Y : U} {p q : X ⟷₁ Y } (α : p ⟷₂ q) → quote₂ (ev
 quote-eval₂ {p = p} {q = q} α = trunc (quote₂ (eval₂ α)) (trans⟷₂ (quote-eval₁ p) (trans⟷₂ (id⟷₂ ⊡ (α ⊡ id⟷₂)) (!⟷₂ (quote-eval₁ q))))
 
 eval-quote₂ : {X Y : UFin} {p q : X == Y} (α : p == q) → eval₂ (quote₂ α) == ap (λ e → eval₁ (quote₁ e)) α
-eval-quote₂ α = prop-has-all-paths {{has-level-apply (has-level-apply UFin-is-gpd _ _) _ _}} _ _
+eval-quote₂ α = prop-has-all-paths _ _
diff --git a/Pi+/FSMG/UFin.agda b/Pi+/FSMG/UFin.agda
@@ -20,7 +20,7 @@ UFin : ∀ {i} → Type i → Type (lmax (lsucc lzero) i)
 UFin A = Σ FinSet λ X → X .fst → A
 
 open import Pi+.FSMG.SMG
-open import Pi+.FSMG.BAut
+open import Pi+.UFin.BAut
 
 open import Pi+.Extra
 

diff --git a/Pi+/UFin.agda b/Pi+/UFin.agda
@@ -2,95 +2,5 @@
 
 module Pi+.UFin where
 
-open import lib.Base
-open import lib.PathGroupoid
-open import lib.Equivalence
-open import lib.NType
-open import lib.Univalence
-open import lib.types.Nat
-open import lib.types.Fin
-open import lib.types.Coproduct
-open import lib.types.Truncation
-open import homotopy.FinSet public
-
-open import Pi+.Misc
-open import Pi+.Extra
-
-UFin = FinSet
-
-instance
-    UFin-is-gpd : has-level (S (S (S ⟨-2⟩))) UFin
-    UFin-is-gpd = TODO
-
-⊔-comm : (A B : Type₀) -> (A ⊔ B) ≃ (B ⊔ A)
-⊔-comm A B = equiv f g f-g g-f
-  where f : (A ⊔ B) -> (B ⊔ A)
-        f (inl x) = inr x
-        f (inr x) = inl x
-        g : (B ⊔ A) -> (A ⊔ B)
-        g (inl x) = inr x
-        g (inr x) = inl x
-        f-g : ∀ x -> f (g x) == x
-        f-g (inl x) = idp
-        f-g (inr x) = idp
-        g-f : ∀ x -> g (f x) == x
-        g-f (inl x) = idp
-        g-f (inr x) = idp
-
-⊔-assoc : (A B C : Type₀) -> (A ⊔ B) ⊔ C ≃ A ⊔ (B ⊔ C)
-⊔-assoc A B C = equiv f g f-g g-f
-  where f : (A ⊔ B) ⊔ C -> A ⊔ (B ⊔ C)
-        f (inl (inl x)) = inl x
-        f (inl (inr x)) = inr (inl x)
-        f (inr x) = inr (inr x)
-        g : A ⊔ (B ⊔ C) -> (A ⊔ B) ⊔ C
-        g (inl x) = inl (inl x)
-        g (inr (inl x)) = inl (inr x)
-        g (inr (inr x)) = inr x
-        f-g : ∀ x -> f (g x) == x
-        f-g (inl x) = idp
-        f-g (inr (inl x)) = idp
-        f-g (inr (inr x)) = idp
-        g-f : ∀ x -> g (f x) == x
-        g-f (inl (inl x)) = idp
-        g-f (inl (inr x)) = idp
-        g-f (inr x) = idp
-
-Fin-⊔ : {n m : ℕ} → (Fin n ⊔ Fin m) ≃ Fin (n + m)
-Fin-⊔ {O} {m} = pp
-  where
-  lemma : Fin 0 ⊔ Fin m == Empty ⊔ Fin m
-  lemma = ap (λ x -> x ⊔ Fin m) (ua Fin-equiv-Empty)
-
-  pp =
-      Fin 0 ⊔ Fin m
-        ≃⟨ coe-equiv lemma ⟩
-      Empty ⊔ Fin m
-        ≃⟨ ⊔₁-Empty (Fin m) ⟩
-      Fin m
-        ≃∎
-Fin-⊔ {S n} {m} = pp
-  where
-    lemma : Fin (S n) ⊔ Fin m == (Fin n ⊔ Unit) ⊔ Fin m
-    lemma = ap (λ x -> x ⊔ Fin m) (ua Fin-equiv-Coprod)
-
-    pp =  Fin (S n) ⊔ Fin m
-        ≃⟨ coe-equiv lemma ⟩
-          (Fin n ⊔ Unit) ⊔ Fin m
-        ≃⟨ ⊔-assoc (Fin n) Unit (Fin m) ⟩
-          Fin n ⊔ (Unit ⊔ Fin m)
-        ≃⟨ coe-equiv ((ap (λ x -> Fin n ⊔ x) (ua (⊔-comm Unit (Fin m) ))))⟩
-          Fin n ⊔ (Fin m ⊔ Unit)
-        ≃⟨ coe-equiv (ap (λ x -> Fin n ⊔ x) (ua Fin-equiv-Coprod)) ⁻¹ ⟩
-          Fin n ⊔ Fin (S m)
-        ≃⟨ Fin-⊔ {n} {(S m)} ⟩
-          Fin (n + (S m))
-        ≃⟨ coe-equiv (ap Fin (+-βr n m)) ⟩
-          Fin (S (n + m))
-        ≃∎
-
-_∪_ : FinSet -> FinSet → FinSet
-(X , ϕ) ∪ (Y , ψ) = X ⊔ Y , Trunc-fmap2 tx ϕ ψ
-  where
-    tx : Σ ℕ (λ n → Fin n == X) → Σ ℕ (λ n → Fin n == Y) → Σ ℕ (λ n → Fin n == X ⊔ Y)
-    tx (n , α) (m , β)= (n + m) , ua ((Fin-⊔ ∘e transport2-equiv (λ x y ->  x ⊔ y) (! α) (! β)) ⁻¹)
+open import Pi+.UFin.Base public
+open import Pi+.UFin.Univ public
diff --git a/Pi+/FSMG/BAut.agda → Pi+/UFin/BAut.agda b/Pi+/FSMG/BAut.agda → Pi+/UFin/BAut.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --exact-split --rewriting #-}
 
-module Pi+.FSMG.BAut where
+module Pi+.UFin.BAut where
 
 open import lib.Base
 open import lib.NType

diff --git a/Pi+/UFin/Base.agda b/Pi+/UFin/Base.agda
@@ -0,0 +1,17 @@
+{-# OPTIONS --without-K --exact-split --rewriting #-}
+
+module Pi+.UFin.Base where
+
+open import HoTT
+open import homotopy.FinSet public
+
+open import Pi+.UFin.BAut
+
+UFin = FinSet
+
+instance
+  FinSet-exp-level : is-gpd FinSet-exp
+  FinSet-exp-level = Σ-level (raise-level 0 ℕ-level) λ n → BAut-level {{Fin-is-set}}
+
+  FinSet-level : is-gpd FinSet
+  FinSet-level = equiv-preserves-level FinSet-econv {{FinSet-exp-level}}
diff --git a/Pi+/UFin/Monoidal.agda b/Pi+/UFin/Monoidal.agda
@@ -0,0 +1,83 @@
+{-# OPTIONS --without-K --exact-split --rewriting #-}
+
+module Pi+.UFin.Monoidal where
+
+open import HoTT
+open import homotopy.FinSet public
+
+open import Pi+.UFin.Base
+open import Pi+.Misc
+open import Pi+.Extra
+
+⊔-comm : (A B : Type₀) -> (A ⊔ B) ≃ (B ⊔ A)
+⊔-comm A B = equiv f g f-g g-f
+  where f : (A ⊔ B) -> (B ⊔ A)
+        f (inl x) = inr x
+        f (inr x) = inl x
+        g : (B ⊔ A) -> (A ⊔ B)
+        g (inl x) = inr x
+        g (inr x) = inl x
+        f-g : ∀ x -> f (g x) == x
+        f-g (inl x) = idp
+        f-g (inr x) = idp
+        g-f : ∀ x -> g (f x) == x
+        g-f (inl x) = idp
+        g-f (inr x) = idp
+
+⊔-assoc : (A B C : Type₀) -> (A ⊔ B) ⊔ C ≃ A ⊔ (B ⊔ C)
+⊔-assoc A B C = equiv f g f-g g-f
+  where f : (A ⊔ B) ⊔ C -> A ⊔ (B ⊔ C)
+        f (inl (inl x)) = inl x
+        f (inl (inr x)) = inr (inl x)
+        f (inr x) = inr (inr x)
+        g : A ⊔ (B ⊔ C) -> (A ⊔ B) ⊔ C
+        g (inl x) = inl (inl x)
+        g (inr (inl x)) = inl (inr x)
+        g (inr (inr x)) = inr x
+        f-g : ∀ x -> f (g x) == x
+        f-g (inl x) = idp
+        f-g (inr (inl x)) = idp
+        f-g (inr (inr x)) = idp
+        g-f : ∀ x -> g (f x) == x
+        g-f (inl (inl x)) = idp
+        g-f (inl (inr x)) = idp
+        g-f (inr x) = idp
+
+Fin-⊔ : {n m : ℕ} → (Fin n ⊔ Fin m) ≃ Fin (n + m)
+Fin-⊔ {O} {m} = pp
+  where
+  lemma : Fin 0 ⊔ Fin m == Empty ⊔ Fin m
+  lemma = ap (λ x -> x ⊔ Fin m) (ua Fin-equiv-Empty)
+
+  pp =
+      Fin 0 ⊔ Fin m
+        ≃⟨ coe-equiv lemma ⟩
+      Empty ⊔ Fin m
+        ≃⟨ ⊔₁-Empty (Fin m) ⟩
+      Fin m
+        ≃∎
+Fin-⊔ {S n} {m} = pp
+  where
+    lemma : Fin (S n) ⊔ Fin m == (Fin n ⊔ Unit) ⊔ Fin m
+    lemma = ap (λ x -> x ⊔ Fin m) (ua Fin-equiv-Coprod)
+
+    pp =  Fin (S n) ⊔ Fin m
+        ≃⟨ coe-equiv lemma ⟩
+          (Fin n ⊔ Unit) ⊔ Fin m
+        ≃⟨ ⊔-assoc (Fin n) Unit (Fin m) ⟩
+          Fin n ⊔ (Unit ⊔ Fin m)
+        ≃⟨ coe-equiv ((ap (λ x -> Fin n ⊔ x) (ua (⊔-comm Unit (Fin m) ))))⟩
+          Fin n ⊔ (Fin m ⊔ Unit)
+        ≃⟨ coe-equiv (ap (λ x -> Fin n ⊔ x) (ua Fin-equiv-Coprod)) ⁻¹ ⟩
+          Fin n ⊔ Fin (S m)
+        ≃⟨ Fin-⊔ {n} {(S m)} ⟩
+          Fin (n + (S m))
+        ≃⟨ coe-equiv (ap Fin (+-βr n m)) ⟩
+          Fin (S (n + m))
+        ≃∎
+
+_∪_ : FinSet -> FinSet → FinSet
+(X , ϕ) ∪ (Y , ψ) = X ⊔ Y , Trunc-fmap2 tx ϕ ψ
+  where
+    tx : Σ ℕ (λ n → Fin n == X) → Σ ℕ (λ n → Fin n == Y) → Σ ℕ (λ n → Fin n == X ⊔ Y)
+    tx (n , α) (m , β)= (n + m) , ua ((Fin-⊔ ∘e transport2-equiv (λ x y ->  x ⊔ y) (! α) (! β)) ⁻¹)
diff --git a/Pi+/UFin/Univ.agda b/Pi+/UFin/Univ.agda
@@ -0,0 +1,57 @@
+{-# OPTIONS --without-K --exact-split --rewriting --overlapping-instances #-}
+
+module Pi+.UFin.Univ where
+
+open import HoTT
+
+private
+  variable
+    i j : ULevel
+
+-- TODO: we need a better definition of transport-equiv to compute it on fst
+transport-equiv-fst :
+  {P : Type i → Type j} {X Y : Type i} → (p : X == Y) →
+  {ux : P X} {uy : P Y} → (up : ux == uy [ P ↓ p ]) →
+  transport-equiv fst (pair= p up) == coe-equiv p
+transport-equiv-fst idp idp = idp
+
+is-univ-fib : {A : Type i} (B : A → Type j) → Type (lmax i j)
+is-univ-fib B = ∀ {x y} → is-equiv (transport-equiv B {x} {y})
+
+module _ (P : SubtypeProp (Type i) j) where
+
+  open SubtypeProp P
+
+  fib : Subtype P → Type i
+  fib = fst
+
+  fib-lift : (X Y : Subtype P) → (fib X == fib Y) → (X == Y)
+  fib-lift X Y p = Subtype=-out P p
+
+  fib-lift-equiv : (X Y : Subtype P) → (fib X == fib Y) ≃ (X == Y)
+  fib-lift-equiv X Y = Subtype=-econv P X Y
+
+  Subtype-is-univ : is-univ-fib fib
+  Subtype-is-univ {X , ϕ} {Y , ψ} = is-eq f g f-g g-f
+    where f : X , ϕ == Y , ψ → X ≃ Y
+          f = transport-equiv fst
+          g : X ≃ Y → X , ϕ == Y , ψ
+          g e = –> (fib-lift-equiv (X , ϕ) (Y , ψ)) (ua e)
+          f-g : (e : X ≃ Y) → f (g e) == e
+          f-g e = transport-equiv-fst (ua e) (prop-has-all-paths-↓ {{level Y}}) ∙ coe-equiv-β e
+          g-f : (p : X , ϕ == Y , ψ) → g (f p) == p
+          g-f idp = pair== (ua-η idp) prop-has-all-paths-↓
+            where instance _ = level X
+
+open import homotopy.FinSet
+
+FinSet-is-univ : is-univ-fib (fib FinSet-prop)
+FinSet-is-univ = Subtype-is-univ FinSet-prop
+
+BAut-is-univ : (A : Type i) → is-univ-fib (fib (BAut-prop A))
+BAut-is-univ A = Subtype-is-univ (BAut-prop A)
+
+FinSet-exp-is-univ : {n : ℕ} → is-univ-fib (fib (BAut-prop (Fin n)))
+FinSet-exp-is-univ {n} = Subtype-is-univ (BAut-prop (Fin n))
+
+UFin-is-univ = FinSet-is-univ