text: {-
  
  Definition of a homogeneous pointed type, and proofs that pi, product, path, and discrete types are homogeneous
  
  Portions of this file adapted from Nicolai Kraus' code here:
    https://bitbucket.org/nicolaikraus/agda/src/e30d70c72c6af8e62b72eefabcc57623dd921f04/trunc-inverse.lagda
  
  -}
  {-# 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
  
    -- switches pt A∙ with y
    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
  