W-ind.agda

{-# OPTIONS --without-K --postfix-projections #-}

open import Agda.Primitive public

infixr 50 _,_
infixr 30 _×_

-- Unit type
record ⊤ {j} : Set j where
  constructor tt
open ⊤ public

-- Σ-types
record Σ {i j} (A : Set i) (B : A → Set j) : Set (i ⊔ j) where
  constructor _,_
  field fst : A
        snd : B fst
open Σ public

_×_ : ∀ {i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
A × B = Σ A λ _ → B

record Lift {i} j (A : Set i) : Set (i ⊔ j) where
  constructor lift
  field
    lower : A
open Lift public

-- _＝_ types
data _＝_ {i} {A : Set i} (x : A) : A → Set i where refl : _＝_ x x

--------------------------------------------------------------------------------

ap : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) {x y : A} (p : _＝_ x y) → _＝_ (f x) (f y)
ap f refl = refl

ap-id : ∀ {i} {A : Set i} {x y : A} {p : _＝_ x y} → _＝_ (ap (λ x → x) p) p
ap-id {p = refl} = refl

ap-∘ : ∀ {i j k} {A : Set i} {B : Set j} {C : Set k} {x y : A} {p : _＝_ x y} {f : B → C} {g : A → B}
     → _＝_ (ap f (ap g p)) (ap (λ x → f (g x)) p)
ap-∘ {p = refl} = refl

ap₂ : ∀ {i j k} {A : Set i} {B : Set j} {C : Set k} (f : A → B → C) {x y : A} {z w : B} (p : _＝_ x y) (q : _＝_ z w) → _＝_ (f x z) (f y w)
ap₂ f refl refl = refl

J : ∀ {i j} {A : Set i} {x : A} (B : ∀ y → _＝_ x y → Set j) {y} (p : _＝_ x y) → B x refl → B y p
J B refl bx = bx

J' : ∀ {i j} {A : Set i} {x : A} (B : ∀ y → _＝_ y x → Set j) {y} (p : _＝_ y x) → B x refl → B y p
J' B refl bx = bx

transp : ∀ {i j} {A : Set i} (B : A → Set j) {x y : A} (p : _＝_ x y) → B x → B y
transp B refl bx = bx

_∙_ : ∀ {i} {A : Set i} {x y z : A} → _＝_ x y → _＝_ y z → _＝_ x z
refl ∙ refl = refl

∙-idl : ∀ {i} {A : Set i} {x y : A} {p : _＝_ x y} → _＝_ (refl ∙ p) p
∙-idl {p = refl} = refl

∙-idr : ∀ {i} {A : Set i} {x y : A} {p : _＝_ x y} → _＝_ (p ∙ refl) p
∙-idr {p = refl} = refl

sym : ∀ {i} {A : Set i} {x y : A} → _＝_ x y → _＝_ y x
sym refl = refl

cancelr : ∀ {i} {A : Set i} {x y z : A} {p q : _＝_ x y} {r : _＝_ y z} → _＝_ (p ∙ r) (q ∙ r) → _＝_ p q
cancelr {r = refl} h = sym ∙-idr ∙ (h ∙ ∙-idr)

∙-transpose-left : ∀ {i} {A : Set i} {x y z : A} {q : _＝_ x z} {p : _＝_ x y} {r : _＝_ y z} → _＝_ q (p ∙ r) → _＝_ (sym p ∙ q) r
∙-transpose-left {p = refl} {r = refl} refl = refl

trans-sym-l : ∀ {i} {A : Set i} {x y : A} {p : _＝_ x y} → _＝_ (sym p ∙ p) refl
trans-sym-l {p = refl} = refl

transp-const : ∀ {i j} {A : Set i} {B : Set j} {x y} {p : _＝_ {A = A} x y} {d} → _＝_ (transp (λ _ → B) p d) d
transp-const {p = refl} = refl

--------------------------------------------------------------------------------

record is-contr {i} (A : Set i) : Set i where
  field
    is-contr-center : A
    is-contr-path   : ∀ y → _＝_ is-contr-center y

  abstract
    is-contr-all-paths : ∀ x y → _＝_ {A = A} x y
    is-contr-all-paths x y = sym (is-contr-path x) ∙ is-contr-path y
    
    is-contr-all-paths-β : ∀ {x} → _＝_ (is-contr-all-paths x x) refl
    is-contr-all-paths-β = trans-sym-l
open is-contr public

is-contr-⊤ : ∀ {i} → is-contr (⊤ {i})
is-contr-⊤ .is-contr-center = tt
is-contr-⊤ .is-contr-path = λ y → refl

is-contr-path-to : ∀ {i} {A : Set i} {x : A} → is-contr (Σ A λ y → _＝_ y x)
is-contr-path-to .is-contr-center = _ , refl
is-contr-path-to .is-contr-path (_ , refl) = refl

is-contr-path-from : ∀ {i} {A : Set i} {x : A} → is-contr (Σ A λ y → _＝_ x y)
is-contr-path-from .is-contr-center = _ , refl
is-contr-path-from .is-contr-path (_ , refl) = refl

is-equiv : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) → Set (i ⊔ j)
is-equiv f = ∀ b → is-contr (Σ _ λ a → _＝_ (f a) b)

equiv : ∀ {i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
equiv A B = Σ (A → B) is-equiv

abstract
  transp-contr : ∀ {i j} {A : Set i} → is-contr A → (B : A → Set j) → ∀ x y → B x → B y
  transp-contr cA B x y bx = transp B (is-contr-all-paths cA x y) bx
  
  transp-contr-β : ∀ {i j} {A : Set i} {cA : is-contr A} {B : A → Set j} {x : A} {bx} → _＝_ (transp-contr cA B x x bx) bx
  transp-contr-β {i} {j} {A} {cA} {B} {x} {bx} = ap (λ p → transp B p bx) (is-contr-all-paths-β cA)

pair-＝ : ∀ {i j} {A : Set i} {B : A → Set j} {a₁ a₂} (p : _＝_ {A = A} a₁ a₂)
            {b₁ : B a₁} {b₂ : B a₂} (q : _＝_ (transp B p b₁) b₂)
          → _＝_ {A = Σ A B} (a₁ , b₁) (a₂ , b₂)
pair-＝ refl refl = refl

pair×-＝ : ∀ {i j} {A : Set i} {B : Set j} {a₁ a₂} (p : _＝_ {A = A} a₁ a₂)
               {b₁ : B} {b₂ : B} (q : _＝_ b₁ b₂)
          → _＝_ {A = A × B} (a₁ , b₁) (a₂ , b₂)
pair×-＝ refl refl = refl

--------------------------------------------------------------------------------

happly : ∀ {i j} {A : Set i} {B : A → Set j} {f g : (a : A) → B a}
       → _＝_ f g → (a : A) → _＝_ (f a) (g a)
happly refl a = refl

postulate
  funext : ∀ {i j} {A : Set i} {B : A → Set j} {f : (a : A) → B a}
         → is-contr (Σ ((a : A) → B a) λ g → (∀ a → _＝_ (f a) (g a)))

--------------------------------------------------------------------------------

abstract
  lam-＝ : ∀ {i j} {A : Set i} {B : A → Set j} {f g : (a : A) → B a}
             (h : (a : A) → _＝_ (f a) (g a)) → _＝_ f g
  lam-＝ {f = f} h = transp-contr funext (λ { (g , _) → _＝_ f g }) (_ , λ _ → refl) (_ , h) refl

  lam-＝-β : ∀ {i j} {A : Set i} {B : A → Set j} {f : (a : A) → B a}
           → _＝_ (lam-＝ {g = f} (λ x → refl)) refl
  lam-＝-β = transp-contr-β

module _ {i j k l} {A : Set i} {B : A → Set j} {C : Set k} {r : C → A} {D : ∀ c → B (r c) → Set l}
         {f g : (a : A) → B a} {h : (a : A) → _＝_ (f a) (g a)}
         {d : ∀ c → D c (f (r c))}
  where
  abstract
    transp-funext : _＝_ (transp {A = ∀ a → B a} (λ f → (c : C) → D c (f (r c))) (lam-＝ h) d)
                       (λ c → transp (D c) (h (r c)) (d c))
    transp-funext
      = transp-contr (funext {f = f}) (λ { (g , h) → ∀ d 
                                                   → _＝_ (transp {A = ∀ a → B a} (λ f → (c : C) → D c (f (r c))) (lam-＝ h) d)
                                                        (λ c → transp (D c) (h (r c)) (d c)) })
        (f , λ _ → refl)
        (g , h)
        (λ d → ap (λ p → transp {A = ∀ a → B a} (λ f → (c : C) → D c (f (r c))) p d) lam-＝-β ∙ refl)
        d
--------------------------------------------------------------------------------

module _ {i} {j} {A : Set i} {B : Set j} (r : A → B) (s : B → A) (p : ∀ a → _＝_ (r (s a)) a) where
  abstract
    is-contr-retract : is-contr A → is-contr B
    is-contr-retract cA .is-contr-center = r (cA .is-contr-center)
    is-contr-retract cA .is-contr-path b = ap r (cA .is-contr-path _) ∙ p _

module _ {i} {j} {A : Set i} {B : Set j} (r : A → B) (r-equiv : is-equiv r) where
  abstract
    is-contr-equiv : is-contr A → is-contr B
    is-contr-equiv = is-contr-retract r (λ b → r-equiv b .is-contr-center .fst) (λ b → r-equiv b .is-contr-center .snd)

module _ {i j} {A : Set i} {B : Set j}
  (g : B → A) (f : A → B)
  (gf : ∀ a → _＝_ (g (f a)) a)
  (fg : ∀ b → _＝_ (f (g b)) b)
  where

  private
    nat : ∀ {i j} {A : Set i} {B : Set j} {f g : A → B} (h : ∀ a → _＝_ (f a) (g a)) {x y} (p : _＝_ x y)
        → _＝_ (ap f p ∙ h y) (h x ∙ ap g p)
    nat h refl = ∙-idl ∙ sym ∙-idr

    lemma : ∀ {i} {A : Set i} (f : A → A) (h : ∀ a → _＝_ (f a) a) a
          → _＝_ (h (f a)) (ap f (h a))
    lemma f h a = sym (cancelr (nat h (h a) ∙ ap₂ _∙_ refl ap-id))

    gf' : ∀ a → _＝_ (g (f a)) a
    gf' a = sym (gf (g (f a))) ∙ (ap g (fg (f a)) ∙ gf a)

    coherence : ∀ b → _＝_ (gf' (g b)) (ap g (fg b))
    coherence b
        = ∙-transpose-left
          ( ap₂ _∙_ (ap (ap g) (lemma _ fg _) ∙ ap-∘) refl ∙
            nat (λ b → gf (g b)) (fg _))

    compute-transp : ∀ {b} {x y} (p : _＝_ x y) q → _＝_ (transp (λ a → _＝_ (g a) b) p q) (sym (ap g p) ∙ q)
    compute-transp refl refl = refl

  abstract
    iso→equiv : is-equiv g
    iso→equiv a .is-contr-center
        = f a , gf' a
    iso→equiv _ .is-contr-path (y , refl)
        = pair-＝
          (fg y)
          ( compute-transp (fg y) (gf' (g y)) ∙
            (ap₂ _∙_ refl (coherence _) ∙ ∙-transpose-left (sym ∙-idr)))

--------------------------------------------------------------------------------

abstract
  is-contr-＝ : ∀ {i} {A : Set i} → is-contr A → ∀ x y → is-contr (_＝_ {A = A} x y)
  is-contr-＝ cA x y .is-contr-center
    = sym (is-contr-all-paths cA x x) ∙ is-contr-all-paths cA x y
  is-contr-＝ cA x .x .is-contr-path refl
    = ∙-transpose-left (sym ∙-idr)

module _ {i j} {A : Set i} {B : A → Set j} (cA : is-contr A) (cB : ∀ a → is-contr (B a)) where
  abstract
    is-contr-Σ : is-contr (Σ A B)
    is-contr-Σ .is-contr-center = cA .is-contr-center , cB _ .is-contr-center
    is-contr-Σ .is-contr-path (a , b) = pair-＝ (cA .is-contr-path _) (is-contr-all-paths (cB _) _ _)

module _ {i j} {A : Set i} {B : A → Set j} (cA : is-contr A) (cAB : is-contr (Σ A B)) where
  abstract
    is-contr-π₂ : ∀ a → is-contr (B a)
    is-contr-π₂ a
      = is-contr-retract {A = Σ A B}
        (λ { (a' , b) → transp-contr cA B a' a b })
        (λ b → (a , b))
        (λ b → transp-contr-β)
        cAB

module _ {ia ib ic id} {A : Set ia} {B : A → Set ib} {C : A → Set ic} {D : ∀ a → B a → C a → Set id} where
  abstract
    is-contr-ΣΣ : is-contr (Σ A B) → (∀ a b → is-contr (Σ (C a) (D a b))) → is-contr (Σ (Σ A C) λ { (a , c) → Σ (B a) λ b → D a b c })
    is-contr-ΣΣ cAB cCD = is-contr-retract {A = Σ (Σ A B) λ { (a , b) → Σ (C a) (D a b) }}
                            (λ { ((a , b) , (c , d)) → ((a , c) , (b , d)) })
                            (λ { ((a , c) , (b , d)) → ((a , b) , (c , d)) })
                            (λ _ → refl)
                            (is-contr-Σ cAB λ { (a , b) → cCD a b })

module _ {i j} {A : Set i} {B : A → Set j} (cB : ∀ a → is-contr (B a)) where
  abstract
    is-contr-Π : is-contr (∀ a → B a)
    is-contr-Π .is-contr-center a = cB a .is-contr-center
    is-contr-Π .is-contr-path f = lam-＝ λ a → cB a .is-contr-path (f a)

module _ {i j k l} {A : Set i} {B : A → Set j} {C : Set k} (r : C → A) (p : is-equiv r) {D : ∀ c → B (r c) → Set l}
         (cBD : ∀ c → is-contr (Σ (B (r c)) (D c)))
  where
  abstract
    private
      helper : is-contr (Σ (∀ c → B (r c)) λ b → (∀ c → D c (b _)))
      helper
        = is-contr-retract
          (λ f → (λ c → f c .fst) , (λ c → f c .snd))
          (λ { (g , h) c → g c , h c })
          (λ a → refl)
          (is-contr-Π cBD)

      inv : A → C
      inv a = p a .is-contr-center .fst

      β : ∀ a → _＝_ (r (inv a)) a
      β a = p a .is-contr-center .snd

    is-contr-ΣΠ : is-contr (Σ (∀ a → B a) λ b → (∀ c → D c (b _)))
    is-contr-ΣΠ
      = is-contr-retract
        (λ { (f , g) → (λ a → transp B (β a) (f (inv a)))
                     , (λ c → transp-contr
                                {A = Σ C λ c' → _＝_ (r c') (r c)} (p (r c))
                                (λ { (p , e) → D c (transp B e (f p)) })
                                (_ , refl) _
                                (g c)) })
        (λ { (f , g) → (λ c → f (r c)) , (λ c → g c) })
        (λ { (f , g) → pair-＝
                       (lam-＝ (λ a → J' (λ a' q → _＝_ (transp B q (f a')) (f a)) (β a) refl))
                       ( transp-funext {B = B} {D = D}
                       ∙ lam-＝ λ c →
                         transp-contr (p (r c))
                         (λ { (xx , yy) → _＝_ (transp (D c) (J' (λ a' q → _＝_ (transp B q (f a')) (f (r c))) yy refl)
                                              (transp (λ { (p , e) → D c (transp B e (f (r p))) })
                                               (is-contr-all-paths (p (r c)) (c , refl) (xx , yy)) (g c)))
                                             (g c) })
                         (c , refl) (inv (r c) , β (r c))
                         (ap {A = _＝_ {A = Σ C λ c' → _＝_ (r c') (r c)} (c , refl) (c , refl)} (λ q → transp (λ { (p , e) → D c (transp B e (f (r p))) }) q _)
                             {x = is-contr-all-paths (p (r c)) (c , refl) (c , refl)} (is-contr-all-paths-β _))
                       )})
        helper

abstract
  fst-equiv : ∀ {i j} {A : Set i} {B : A → Set j} → (∀ a → is-contr (B a)) → is-equiv (fst {B = B})
  fst-equiv {i} {j} {A} {B} cB a
    = is-contr-retract {A = B a}
      (λ b → (a , b) , refl)
      (λ { ((_ , b) , refl) → b })
      (λ { ((_ , b) , refl) → refl })
      (cB a)

abstract
  id-equiv : ∀ {i} {A : Set i} → equiv A A
  id-equiv = (λ x → x) , iso→equiv _ _ (λ _ → refl) (λ _ → refl)

module _ {i j k} {A : Set i} {B : Set j} {C : Set k} where
  abstract
    comp-equiv : equiv A B → equiv B C → equiv A C
    comp-equiv (f , f-equiv) (g , g-equiv)
      = (λ a → g (f a))
      , (λ c → is-contr-retract 
               (λ { ((b , refl) , (a , refl)) → _ , refl })
               (λ { (a , refl) → (_ , refl) , (_ , refl) })
               (λ { (a , refl) → refl })
               (is-contr-Σ (g-equiv c) (λ { (b , _) → f-equiv b })))

abstract
  is-equiv-lift : ∀ {i j} {A : Set i} → is-equiv (lift {i} {j} {A})
  is-equiv-lift = iso→equiv _ lower (λ _ → refl) (λ _ → refl)

  is-equiv-lower : ∀ {i j} {A : Set i} → is-equiv (lower {i} {j} {A})
  is-equiv-lower = iso→equiv _ lift (λ _ → refl) (λ _ → refl)

--------------------------------------------------------------------------------

is-prop : ∀ {i} → Set i → Set i
is-prop A = A → is-contr A

all-paths→is-prop : ∀ {i} {A : Set i} → ((x y : A) → _＝_ x y) → is-prop A
all-paths→is-prop p a .is-contr-center = a
all-paths→is-prop p a .is-contr-path y = p _ _

abstract
  is-prop-all-paths : ∀ {i} {A : Set i} → is-prop A → (x y : A) → _＝_ x y
  is-prop-all-paths pA x y = is-contr-all-paths (pA x) x y

abstract
  is-prop-is-contr : ∀ {i} {A : Set i} → is-prop (is-contr A)
  is-prop-is-contr {i} {A} cA .is-contr-center = cA
  is-prop-is-contr {i} {A} cA .is-contr-path cA'
    = ap (λ { (x , y) → record { is-contr-center = x ; is-contr-path = y } }) inner
    where
      inner : _＝_ {A = Σ A λ a → ∀ b → _＝_ a b} (cA .is-contr-center , cA .is-contr-path) (cA' .is-contr-center , cA' .is-contr-path)
      inner = pair-＝
              (is-contr-all-paths cA _ _)
              (lam-＝ λ a → is-contr-all-paths (is-contr-＝ cA _ _) _ _)

abstract
  is-prop-⊤ : ∀ {i} → is-prop (⊤ {i})
  is-prop-⊤ = λ _ → is-contr-⊤

abstract
  is-prop-Σ : ∀ {i j} {A : Set i} {B : A → Set j} → is-prop A → (∀ a → is-prop (B a)) → is-prop (Σ A B)
  is-prop-Σ {A = A} {B = B} pA pB (a , b) = is-contr-Σ (pA a) (λ a → pB a (transp B (is-prop-all-paths pA _ _) b))

abstract
  is-prop-Π : ∀ {i j} {A : Set i} {B : A → Set j} → (∀ a → is-prop (B a)) → is-prop (∀ a → B a)
  is-prop-Π {A = A} {B = B} pB f = is-contr-Π (λ a → pB a (f a))

--------------------------------------------------------------------------------

postulate
  uip : ∀ {ℓ} {A : Set ℓ} {x y : A} → is-prop (x ＝ y)

module _ (A : Set) (B : A → Set) where
  data W : Set where
    sup : (a : A) (f : B a → W) → W

  module _ (P : W → Set)
           (ps : ∀ {a} {f}
                   (IH : ∀ ba → P (f ba))
                   (ext : ∀ b1 b2 (p : f b1 ＝ f b2) → transp P p (IH b1) ＝ IH b2)
                 → P (sup a f))
           where

    record ↯ {i} (A : Set i) ℓ : Set (lsuc ℓ ⊔ i) where
      field
        def : Set ℓ
        def-is-prop : is-prop def
        elt : def → A

    e : ∀ w → ↯ (P w) lzero
    e (sup a f) .↯.def
      = Σ (∀ x → e (f x) .↯.def) λ d → ∀ x y (p : f x ＝ f y) → transp P p (e (f x) .↯.elt (d x)) ＝ e (f y) .↯.elt (d y)
    e (sup a f) .↯.def-is-prop
      = is-prop-Σ (is-prop-Π (λ x → e (f x) .↯.def-is-prop))
        λ _ → is-prop-Π λ _ → is-prop-Π λ _ → is-prop-Π λ _ → uip
    e (sup a f) .↯.elt (d , r)
      = ps (λ x → e (f x) .↯.elt (d x)) (λ b1 b2 p → r _ _ p)

    ap-e : ∀ (x y : W) (p : x ＝ y) dx dy → transp P p (e x .↯.elt dx) ＝ e y .↯.elt dy
    ap-e x _ refl _ _ = ap (e x .↯.elt) (is-prop-all-paths (e x .↯.def-is-prop) _ _)

    e-is-def : ∀ w → (e w) .↯.def
    e-is-def (sup a f) .fst = λ x → e-is-def (f x)
    e-is-def (sup a f) .snd = λ x y p → ap-e (f x) (f y) p _ _

    W-ind : ∀ w → P w
    W-ind w = e w .↯.elt (e-is-def w)