Define PERs and refactor assembly modules

src/Realizability/Assembly/Base.agda

@@ -2,6 +2,10 @@
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Functions.FunExtEquiv
 open import Cubical.Data.Sigma
 open import Cubical.HITs.PropositionalTruncation
 open import Cubical.Reflection.RecordEquiv
@@ -11,32 +15,55 @@ module Realizability.Assembly.Base {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra
   record Assembly (X : Type ℓ) : Type (ℓ-suc ℓ) where
     infix 25 _⊩_
     field
-      isSetX : isSet X
       _⊩_ : A → X → Type ℓ
+      isSetX : isSet X
       ⊩isPropValued : ∀ a x → isProp (a ⊩ x)
       ⊩surjective : ∀ x → ∃[ a ∈ A ] a ⊩ x
 
+  open Assembly public
+  _⊩[_]_ : ∀ {X : Type ℓ} → A → Assembly X → X → Type ℓ
+  a ⊩[ A ] x = A ._⊩_ a x
 
   AssemblyΣ : Type ℓ → Type _
   AssemblyΣ X =
-    Σ[ isSetX ∈ isSet X ]
     Σ[ _⊩_ ∈ (A → X → hProp ℓ) ]
-    (∀ x → ∃[ a ∈ A ] ⟨ a ⊩ x ⟩)
-
-  AssemblyΣX→isSetX : ∀ X → AssemblyΣ X → isSet X
-  AssemblyΣX→isSetX X (isSetX , _ , _) = isSetX
-
-  AssemblyΣX→⊩ : ∀ X → AssemblyΣ X → (A → X → hProp ℓ)
-  AssemblyΣX→⊩ X (_ , ⊩ , _) = ⊩
-
-  AssemblyΣX→⊩surjective : ∀ X → (asm : AssemblyΣ X) → (∀ x → ∃[ a ∈ A ] ⟨ AssemblyΣX→⊩ X asm a x ⟩)
-  AssemblyΣX→⊩surjective X (_ , _ , ⊩surjective) = ⊩surjective
+    (∀ x → ∃[ a ∈ A ] ⟨ a ⊩ x ⟩) ×
+    (isSet X)
 
   isSetAssemblyΣ : ∀ X → isSet (AssemblyΣ X)
-  isSetAssemblyΣ X = isSetΣ (isProp→isSet isPropIsSet) λ isSetX → isSetΣ (isSetΠ (λ a → isSetΠ λ x → isSetHProp)) λ _⊩_ → isSetΠ λ x → isProp→isSet isPropPropTrunc
+  isSetAssemblyΣ X = isSetΣ (isSetΠ2 λ _ _ → isSetHProp) (λ rel → isSet× (isSetΠ λ x → isProp→isSet isPropPropTrunc) (isProp→isSet isPropIsSet))
 
-  unquoteDecl AssemblyIsoΣ = declareRecordIsoΣ AssemblyIsoΣ (quote Assembly)
+  AssemblyΣ≡Equiv : ∀ X → (a b : AssemblyΣ X) → (a ≡ b) ≃ (∀ r x → ⟨ a .fst r x ⟩ ≃ ⟨ b .fst r x ⟩)
+  AssemblyΣ≡Equiv X a b =
+    a ≡ b
+      ≃⟨ invEquiv (Σ≡PropEquiv (λ rel → isProp× (isPropΠ λ x → isPropPropTrunc) isPropIsSet) {u = a} {v = b}) ⟩
+    a .fst ≡ b .fst
+      ≃⟨ invEquiv (funExt₂Equiv {f = a .fst} {g = b .fst}) ⟩
+    (∀ (r : A) (x : X) → a .fst r x ≡ b .fst r x)
+      ≃⟨
+        equivΠCod
+          (λ r →
+            equivΠCod
+              λ x →
+                compEquiv
+                  (invEquiv (Σ≡PropEquiv (λ _ → isPropIsProp) {u = a .fst r x} {v = b .fst r x}))
+                  (univalence {A = a .fst r x .fst} {B = b .fst r x .fst}))
+       ⟩
+    (∀ (r : A) (x : X) → ⟨ a .fst r x ⟩ ≃ ⟨ b .fst r x ⟩)
+      ■
 
-  open Assembly public
+  -- definitional isomorphism
+  AssemblyΣIsoAssembly : ∀ X → Iso (AssemblyΣ X) (Assembly X)
+  _⊩_ (Iso.fun (AssemblyΣIsoAssembly X) (rel , surj , isSetX)) a x = ⟨ rel a x ⟩
+  Assembly.isSetX (Iso.fun (AssemblyΣIsoAssembly X) (rel , surj , isSetX)) = isSetX
+  ⊩isPropValued (Iso.fun (AssemblyΣIsoAssembly X) (rel , surj , isSetX)) a x = str (rel a x)
+  ⊩surjective (Iso.fun (AssemblyΣIsoAssembly X) (rel , surj , isSetX)) x = surj x
+  Iso.inv (AssemblyΣIsoAssembly X) asm = (λ a x → (a ⊩[ asm ] x) , (asm .⊩isPropValued a x)) , (λ x → asm .⊩surjective x) , asm .isSetX
+  Iso.rightInv (AssemblyΣIsoAssembly X) asm = refl
+  Iso.leftInv (AssemblyΣIsoAssembly X) (rel , surj , isSetX) = refl
 
-
+  AssemblyΣ≃Assembly : ∀ X → AssemblyΣ X ≃ Assembly X
+  AssemblyΣ≃Assembly X = isoToEquiv (AssemblyΣIsoAssembly X)
+
+  isSetAssembly : ∀ X → isSet (Assembly X)
+  isSetAssembly X = isOfHLevelRespectEquiv 2 (AssemblyΣ≃Assembly X) (isSetAssemblyΣ X)

src/Realizability/Assembly/BinCoproducts.agda

@@ -3,15 +3,15 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sum hiding (map)
 open import Cubical.Data.Sigma
-open import Cubical.Data.Fin
+open import Cubical.Data.FinData
 open import Cubical.Data.Nat
 open import Cubical.Data.Vec hiding (map)
 open import Cubical.HITs.PropositionalTruncation hiding (map)
 open import Cubical.HITs.PropositionalTruncation.Monad
 open import Cubical.Categories.Category
 open import Cubical.Categories.Limits.BinCoproduct
 open import Realizability.CombinatoryAlgebra
-open import Realizability.ApplicativeStructure renaming (λ*-chain to `λ*; λ*-naturality to `λ*ComputationRule) hiding (λ*)
+open import Realizability.ApplicativeStructure
 
 module Realizability.Assembly.BinCoproducts {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) where
 
@@ -20,9 +20,6 @@ open import Realizability.Assembly.Base ca
 open Realizability.CombinatoryAlgebra.Combinators ca renaming (i to Id; ia≡a to Ida≡a)
 open import Realizability.Assembly.Morphism ca
 
-λ* = `λ* as fefermanStructure
-λ*ComputationRule = `λ*ComputationRule as fefermanStructure
-
 infixl 23 _⊕_
 _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B)
 (as ⊕ bs) .isSetX = isSet⊎ (as .isSetX) (bs .isSetX)
@@ -61,12 +58,13 @@ _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B)
 [ f , g ] .map (inr y) = g .map y
 [_,_] {asmZ = asmZ} f g .tracker =
   do
+    -- these are not considered structurally smaller since these are in the propositional truncation
     (f~ , f~tracks) ← f .tracker
     (g~ , g~tracks) ← g .tracker
     -- if (pr₁ r) then f (pr₂ r) else g (pr₂ r)
     let
       tracker : Term as (suc zero)
-      tracker = ` Id ̇ (` pr₁ ̇ (# fzero)) ̇ (` f~ ̇ (` pr₂ ̇ (# fzero))) ̇ (` g~ ̇ (` pr₂ ̇ (# fzero)))
+      tracker = ` Id ̇ (` pr₁ ̇ (# zero)) ̇ (` f~ ̇ (` pr₂ ̇ (# zero))) ̇ (` g~ ̇ (` pr₂ ̇ (# zero)))
     return
       (λ* tracker ,
         λ { (inl x) r r⊩inl →
@@ -79,7 +77,7 @@ _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B)
                          (λ r → asmZ ._⊩_ r ([ f , g ] .map (inl x)))
                          (sym
                            (λ* tracker ⨾ r
-                             ≡⟨ λ*ComputationRule tracker (r ∷ []) ⟩
+                             ≡⟨ λ*ComputationRule tracker r ⟩
                             Id ⨾ (pr₁ ⨾ r) ⨾ (f~ ⨾ (pr₂ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))
                              ≡⟨ cong (λ r → Id ⨾ (pr₁ ⨾ r) ⨾ (f~ ⨾ (pr₂ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))) r≡pair⨾true⨾rₓ ⟩
                             Id ⨾ (pr₁ ⨾ (pair ⨾ true ⨾ rₓ)) ⨾ (f~ ⨾ (pr₂ ⨾ (pair ⨾ true ⨾ rₓ))) ⨾ (g~ ⨾ (pr₂ ⨾ (pair ⨾ true ⨾ rₓ)))
@@ -101,7 +99,7 @@ _⊕_ : {A B : Type ℓ} → Assembly A → Assembly B → Assembly (A ⊎ B)
                          (λ r → asmZ ._⊩_ r ([ f , g ] .map (inr y)))
                          (sym
                            ((λ* tracker ⨾ r
-                             ≡⟨ λ*ComputationRule tracker (r ∷ []) ⟩
+                             ≡⟨ λ*ComputationRule tracker r ⟩
                             Id ⨾ (pr₁ ⨾ r) ⨾ (f~ ⨾ (pr₂ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))
                              ≡⟨ cong (λ r → Id ⨾ (pr₁ ⨾ r) ⨾ (f~ ⨾ (pr₂ ⨾ r)) ⨾ (g~ ⨾ (pr₂ ⨾ r))) r≡pair⨾false⨾yᵣ ⟩
                             Id ⨾ (pr₁ ⨾ (pair ⨾ false ⨾ yᵣ)) ⨾ (f~ ⨾ (pr₂ ⨾ (pair ⨾ false ⨾ yᵣ))) ⨾ (g~ ⨾ (pr₂ ⨾ (pair ⨾ false ⨾ yᵣ)))
@@ -126,6 +124,7 @@ BinCoproductsASM (X , asmX) (Y , asmY) .univProp {Z , asmZ} f g =
     (λ ! → isProp× (isSetAssemblyMorphism _ _ _ _) (isSetAssemblyMorphism _ _ _ _))
     λ ! (κ₁⊚!≡f , κ₂⊚!≡g) → AssemblyMorphism≡ _ _ (funExt λ { (inl x) i → κ₁⊚!≡f (~ i) .map x ; (inr y) i → κ₂⊚!≡g (~ i) .map y })
 
+-- I have no idea why I did these since this can be derived from the universal property of the coproduct anyway?
 module _
   {X Y : Type ℓ}
   (asmX : Assembly X)
@@ -142,7 +141,7 @@ module _
     do
       let
         tracker : Term as 1
-        tracker = ` Id ̇ (` pr₁ ̇ # fzero) ̇ (` pair ̇ ` false ̇ (` pr₂ ̇ # fzero)) ̇ (` pair ̇ ` true ̇ (` pr₂ ̇ # fzero))
+        tracker = ` Id ̇ (` pr₁ ̇ # zero) ̇ (` pair ̇ ` false ̇ (` pr₂ ̇ # zero)) ̇ (` pair ̇ ` true ̇ (` pr₂ ̇ # zero))
       return
         ((λ* tracker) ,
          (λ { (inl x) r r⊩inl →
@@ -154,7 +153,7 @@ module _
                          λ*trackerEq : λ* tracker ⨾ r ≡ pair ⨾ false ⨾ rₓ
                          λ*trackerEq =
                            λ* tracker ⨾ r
-                             ≡⟨ λ*ComputationRule tracker (r ∷ []) ⟩
+                             ≡⟨ λ*ComputationRule tracker r ⟩
                            Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ r))
                              ≡⟨ cong (λ r → Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ r))) r≡pair⨾true⨾rₓ ⟩
                            Id ⨾ (pr₁ ⨾ (pair ⨾ true ⨾ rₓ)) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ (pair ⨾ true ⨾ rₓ))) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ (pair ⨾ true ⨾ rₓ)))
@@ -175,7 +174,7 @@ module _
                          λ*trackerEq : λ* tracker ⨾ r ≡ pair ⨾ true ⨾ yᵣ
                          λ*trackerEq =
                            λ* tracker ⨾ r
-                             ≡⟨ λ*ComputationRule tracker (r ∷ []) ⟩
+                             ≡⟨ λ*ComputationRule tracker r ⟩
                            Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ r))
                              ≡⟨ cong (λ r → Id ⨾ (pr₁ ⨾ r) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ r)) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ r))) r≡pair⨾false⨾yᵣ ⟩
                            Id ⨾ (pr₁ ⨾ (pair ⨾ false ⨾ yᵣ)) ⨾ (pair ⨾ false ⨾ (pr₂ ⨾ (pair ⨾ false ⨾ yᵣ))) ⨾ (pair ⨾ true ⨾ (pr₂ ⨾ (pair ⨾ false ⨾ yᵣ)))