{-# OPTIONS --without-K #-}
open import lib.Basics
open import lib.NType2
open import lib.PathGroupoid
open import lib.types.Bool
open import lib.types.IteratedSuspension
open import lib.types.Lift
open import lib.types.LoopSpace
open import lib.types.Nat
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.Suspension
open import lib.types.TLevel
open import lib.types.Unit
open SuspensionRec public using () renaming (f to Susp-rec)
open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas
module nicolai.pseudotruncations.pointed-O-Sphere where
module _ {i} where
bool = fst (⊙Sphere {i} O)
tt₀ : bool
tt₀ = snd (⊙Sphere {i} O)
ff₀ : bool
ff₀ = lift false
module bool-neutral
{i j}
(P : bool {i} → Type j)
(p₀ : P tt₀) where
bool-pair : (P tt₀ × P ff₀) ≃ ((b : bool) → P b)
bool-pair = equiv (λ tf → (λ { (lift true) → fst tf ; (lift false) → snd tf }))
(λ f → (f tt₀ , f ff₀))
(λ f → λ= (λ { (lift true) → idp ; (lift false) → idp }))
(λ tf → idp)
pair-red : Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀) → P ff₀
pair-red ((pt , pf) , q) = pf
sing-exp : P ff₀ → Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀)
sing-exp pf = ((p₀ , pf) , idp)
red-exp : (pf : P ff₀) → pair-red (sing-exp pf) == pf
red-exp _ = idp
exp-red : (x : Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀)) → sing-exp (pair-red x) == x
exp-red ((.p₀ , pf) , idp) = idp
pair-one-determined : Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀) ≃ P ff₀
pair-one-determined = equiv pair-red sing-exp red-exp exp-red
reduction : (Σ ((b : bool) → P b) λ g → g tt₀ == p₀) ≃ P ff₀
reduction = (Σ ((b : bool) → P b) λ g → g tt₀ == p₀)
≃⟨ equiv-Σ-fst {A = P tt₀ × P ff₀}
{B = (b : bool) → P b}
(λ g → g tt₀ == p₀)
{h = fst bool-pair}
(snd bool-pair) ⁻¹ ⟩
Σ (P tt₀ × P ff₀) ((λ g → g tt₀ == p₀) ∘ fst bool-pair)
≃⟨ ide _ ⟩
Σ (P tt₀ × P ff₀) (λ tf → fst tf == p₀)
≃⟨ pair-one-determined ⟩
P ff₀
≃∎