Elims.agda

{-# OPTIONS --cubical #-}
module _ where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.SetTruncation

elimSetTrunc : ∀ {ℓ} (A : Type ℓ) (B : ∥ A ∥₀ → Type ℓ) →
  (f : (a : A) → B (∣ a ∣₀)) →
  (g : (x y : ∥ A ∥₀) → (p q : x ≡ y) →
        (bx : B x) (by : B y) ->
        (bp : PathP (\ i -> B (p i)) bx by)
        (bq : PathP (\ i -> B (q i)) bx by) ->
        SquareP (\ i j → B (squash₀ x y p q i j))
                bp bq (\ _ → bx) (\ _ → by)) →
  ((a : ∥ A ∥₀) → B a)
elimSetTrunc A B f g ∣ a ∣₀ = f a
elimSetTrunc A B f g (squash₀ x y p q i j) =
  g x y p q (elimSetTrunc A B f g x) (elimSetTrunc A B f g y)
    (cong (elimSetTrunc A B f g) p) (cong (elimSetTrunc A B f g) q) i j



module M {ℓ : _} (G-type : Type ℓ) (G-id : G-type) (G-comp : G-type → G-type → G-type) where

 data B : Type ℓ where
    base : B
    path : G-type → base ≡ base
    id : path G-id ≡ refl
    conc : (g h : G-type) → path g ∙ path h ≡ path (G-comp g h)
    groupoid : (p q : base ≡ base) (r s : p ≡ q) → r ≡ s

 elimProp : {ℓ' : Level} (P : B → Type ℓ') → (∀ b → isProp (P b)) →
            (b : P base) → ∀ x → P x
 elimProp P Pprop b base = b
 elimProp P Pprop b (path x i) = isOfHLevel→isOfHLevelDep 1 Pprop b b (path x) i
 elimProp P Pprop b (id i i₁) = isOfHLevel→isOfHLevelDep 2 (\ x → isProp→isSet (Pprop x))
            b b (isOfHLevel→isOfHLevelDep 1 Pprop b b (path G-id)) (\ _ → b) id i i₁
 elimProp P Pprop b (conc g h i j) = { }0
  -- This is complicated by the _∙_ in the path constructor.
  -- The recursive calls in the boundaries actually reduce away under
  -- the various faces, but it's still a complicated composition to
  -- deal with.
 elimProp P Pprop b (groupoid p q r s i j k) =
          isOfHLevel→isOfHLevelDep 3 (\ x → isSet→isGroupoid (isProp→isSet (Pprop x)))
             b b (cong (elimProp P Pprop b) p) (cong (elimProp P Pprop b) q)
                 (cong (cong (elimProp P Pprop b)) r) (cong (cong (elimProp P Pprop b)) s)
                 (groupoid p q r s)
                 i j k

 -- If I were to continue with this version of "B" I would instead define the general eliminator first.
 -- The type of the type of the method for the "conc" constructor
 -- would involve a "SquareP" and transitivity for "PathP" though.


-- Following Thierry suggestion, things are a bit smoother.
module M2 {ℓ : _} (G-type : Type ℓ) (G-id : G-type) (G-comp : G-type → G-type → G-type) where

 data B : Type ℓ where
    base : B
    path : G-type → base ≡ base
    id : path G-id ≡ refl
    conc : {g h g1 h1 : G-type} → G-comp g h ≡ G-comp g1 h1 → Square (path g) (path h) (path g1) (path h1)
    groupoid : (p q : base ≡ base) (r s : p ≡ q) → r ≡ s

 postulate
   isSet'→isSet'Dep : {ℓ ℓ' : Level}{A : Type ℓ} (P : A → Type ℓ') (Pset : ∀ b → isSet' (P b))
                    → ∀ (a : I → I → A) → ∀ {w x y z} p q r s →
                      SquareP (\ i j → P (a i j)) {w} {x} p {y} {z} q r s                                                                                                                                                                                                                                            

 elimProp : {ℓ' : Level} (P : B → Type ℓ') → (∀ b → isProp (P b)) →
            (b : P base) → ∀ x → P x
 elimProp P Pprop b base = b
 elimProp P Pprop b (path x i) = isOfHLevel→isOfHLevelDep 1 Pprop b b (path x) i
 elimProp P Pprop b (id i j) = isOfHLevel→isOfHLevelDep 2 (\ x → isProp→isSet (Pprop x))
            b b (isOfHLevel→isOfHLevelDep 1 Pprop b b (path G-id)) (\ _ → b) id i j
 elimProp P Pprop b (conc eq i j) = isSet'→isSet'Dep P (λ x → isSet→isSet' (isProp→isSet (Pprop x)))
                                      (λ i j → conc eq i j)
                                        (isOfHLevel→isOfHLevelDep 1 Pprop b b (path _))
                                        (isOfHLevel→isOfHLevelDep 1 Pprop b b (path _))
                                        (isOfHLevel→isOfHLevelDep 1 Pprop b b (path _))
                                        (isOfHLevel→isOfHLevelDep 1 Pprop b b (path _)) i j
 elimProp P Pprop b (groupoid p q r s i j k) =
          isOfHLevel→isOfHLevelDep 3 (\ x → isSet→isGroupoid (isProp→isSet (Pprop x)))
             b b (cong (elimProp P Pprop b) p) (cong (elimProp P Pprop b) q)
                 (cong (cong (elimProp P Pprop b)) r) (cong (cong (elimProp P Pprop b)) s)
                 (groupoid p q r s)
                 i j k