{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Pointed.Homogeneous where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Data.Sigma
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary
open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Pointed.Properties
open import Cubical.Structures.Pointed
isHomogeneous : ∀ {ℓ} → Pointed ℓ → Type (ℓ-suc ℓ)
isHomogeneous {ℓ} (A , x) = ∀ y → Path (Pointed ℓ) (A , x) (A , y)
isHomogeneousPi : ∀ {ℓ ℓ'} {A : Type ℓ} {B∙ : A → Pointed ℓ'}
→ (∀ a → isHomogeneous (B∙ a)) → isHomogeneous (Πᵘ∙ A B∙)
isHomogeneousPi h f i = (∀ a → typ (h a (f a) i)) , (λ a → pt (h a (f a) i))
isHomogeneousProd : ∀ {ℓ ℓ'} {A∙ : Pointed ℓ} {B∙ : Pointed ℓ'}
→ isHomogeneous A∙ → isHomogeneous B∙ → isHomogeneous (A∙ ×∙ B∙)
isHomogeneousProd hA hB (a , b) i = (typ (hA a i)) × (typ (hB b i)) , (pt (hA a i) , pt (hB b i))
isHomogeneousPath : ∀ {ℓ} (A : Type ℓ) {x y : A} (p : x ≡ y) → isHomogeneous ((x ≡ y) , p)
isHomogeneousPath A {x} {y} p q
= pointed-sip ((x ≡ y) , p) ((x ≡ y) , q) (eqv , compPathr-cancel p q)
where eqv : (x ≡ y) ≃ (x ≡ y)
eqv = compPathlEquiv (q ∙ sym p)
module HomogeneousDiscrete {ℓ} {A∙ : Pointed ℓ} (dA : Discrete (typ A∙)) (y : typ A∙) where
switch : typ A∙ → typ A∙
switch x with dA x (pt A∙)
... | yes _ = y
... | no _ with dA x y
... | yes _ = pt A∙
... | no _ = x
switch-ptA∙ : switch (pt A∙) ≡ y
switch-ptA∙ with dA (pt A∙) (pt A∙)
... | yes _ = refl
... | no ¬p = ⊥.rec (¬p refl)
switch-idp : ∀ x → switch (switch x) ≡ x
switch-idp x with dA x (pt A∙)
switch-idp x | yes p with dA y (pt A∙)
switch-idp x | yes p | yes q = q ∙ sym p
switch-idp x | yes p | no _ with dA y y
switch-idp x | yes p | no _ | yes _ = sym p
switch-idp x | yes p | no _ | no ¬p = ⊥.rec (¬p refl)
switch-idp x | no ¬p with dA x y
switch-idp x | no ¬p | yes p with dA y (pt A∙)
switch-idp x | no ¬p | yes p | yes q = ⊥.rec (¬p (p ∙ q))
switch-idp x | no ¬p | yes p | no _ with dA (pt A∙) (pt A∙)
switch-idp x | no ¬p | yes p | no _ | yes _ = sym p
switch-idp x | no ¬p | yes p | no _ | no ¬q = ⊥.rec (¬q refl)
switch-idp x | no ¬p | no ¬q with dA x (pt A∙)
switch-idp x | no ¬p | no ¬q | yes p = ⊥.rec (¬p p)
switch-idp x | no ¬p | no ¬q | no _ with dA x y
switch-idp x | no ¬p | no ¬q | no _ | yes q = ⊥.rec (¬q q)
switch-idp x | no ¬p | no ¬q | no _ | no _ = refl
switch-eqv : typ A∙ ≃ typ A∙
switch-eqv = isoToEquiv (iso switch switch switch-idp switch-idp)
isHomogeneousDiscrete : ∀ {ℓ} {A∙ : Pointed ℓ} (dA : Discrete (typ A∙)) → isHomogeneous A∙
isHomogeneousDiscrete {ℓ} {A∙} dA y
= pointed-sip (typ A∙ , pt A∙) (typ A∙ , y) (switch-eqv , switch-ptA∙)
where open HomogeneousDiscrete {ℓ} {A∙} dA y