Fix choice formulation

rahulc29 · Dec 5, 2023 · 4b08132 · 4b08132
1 parent 2edec16
commit 4b08132
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/Realizability/Assembly.agda b/src/Realizability/Assembly.agda
@@ -707,11 +707,11 @@ module Realizability.Assembly {ℓ} {A : Type ℓ} (ca : CombinatoryAlgebra A) w
         eIsCoequalizer : IsCoequalizer {C = ASM} k₁ k₂ e
         eIsCoequalizer .glues = AssemblyMorphism≡ _ _ (funExt λ (x , x' , ex≡ex') → ex≡ex')
         eIsCoequalizer .univProp {W , ws} q k₁q≡k₂q =
-          uniqueExists {!!} {!!} {!!} {!!} where
+          uniqueExists (∃t→Σt q k₁q≡k₂q ∃t .fst) (∃t→Σt q k₁q≡k₂q ∃t .snd) (λ t → isSetAssemblyMorphism _ _ _ _) λ t e⊚t≡q → λ i → e⊚t≡qIsProp q k₁q≡k₂q (∃t→Σt q k₁q≡k₂q ∃t) (t , e⊚t≡q) i .fst where
             _⊩W_ = ws ._⊩_
             ∃t : ∃[ t ∈ AssemblyMorphism ys ws ] (e ⊚ t ≡ q)
             ∃t = (do
-                 (e⁻¹ , e⁻¹IsSection) ← choice X Y (e .map) surjection
+                 (e⁻¹ , e⁻¹IsSection) ← choice X Y (xs .isSetX) (ys .isSetX) (e .map) surjection
                  return (h e⁻¹ e⁻¹IsSection , {!!})) where
                                  module _
                                   (e⁻¹ : Y → X)

diff --git a/src/Realizability/Choice.agda b/src/Realizability/Choice.agda
@@ -9,4 +9,4 @@ open import Cubical.Data.Sigma
 module Realizability.Choice where
 
 Choice : ∀ ℓ ℓ' → Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ'))
-Choice ℓ ℓ' = (A : Type ℓ) (B : Type ℓ') (f : A → B) → isSurjection f → ∃[ f' ∈ (B → A) ] section f f'
+Choice ℓ ℓ' = (A : Type ℓ) (B : Type ℓ') → isSet A → isSet B → (f : A → B) → isSurjection f → ∃[ f' ∈ (B → A) ] section f f'