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

open import Agda.Primitive

infixr  _,_
infixr  _×_

-- 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

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

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

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

ap-id : ∀ {i} {A : Set i} {x y : A} {p : Id x y} → Id (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 : Id x y} {f : B → C} {g : A → B}
     → Id (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 : Id x y) (q : Id z w) → Id (f x z) (f y w)
ap₂ f refl refl = refl

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

J' : ∀ {i j} {A : Set i} {x : A} (B : ∀ y → Id y x → Set j) {y} (p : Id 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 : Id x y) → B x → B y
transp B refl bx = bx

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

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

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

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

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

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

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

transp-const : ∀ {i j} {A : Set i} {B : Set j} {x y} {p : Id {A = A} x y} {d} → Id (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 → Id is-contr-center y

  abstract
    is-contr-all-paths : ∀ x y → Id {A = A} x y
    is-contr-all-paths x y = sym (is-contr-path x) ∙ is-contr-path y
    
    is-contr-all-paths-β : ∀ {x} → Id (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 → Id 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 → Id 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 → Id (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} → Id (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-Id : ∀ {i j} {A : Set i} {B : A → Set j} {a₁ a₂} (p : Id {A = A} a₁ a₂)
            {b₁ : B a₁} {b₂ : B a₂} (q : Id (transp B p b₁) b₂)
          → Id {A = Σ A B} (a₁ , b₁) (a₂ , b₂)
pair-Id refl refl = refl

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

happly : ∀ {i j} {A : Set i} {B : A → Set j} {f g : (a : A) → B a}
       → Id f g → (a : A) → Id (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 → Id (f a) (g a)))
  ua : ∀ {i} (A : Set i) → is-contr (Σ (Set i) λ B → Σ (A → B) is-equiv)

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

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

  lam-Id-β : ∀ {i j} {A : Set i} {B : A → Set j} {f : (a : A) → B a}
           → Id (lam-Id {g = f} (λ x → refl)) refl
  lam-Id-β = 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) → Id (f a) (g a)}
         {d : ∀ c → D c (f (r c))}
  where
  abstract
    transp-funext : Id (transp {A = ∀ a → B a} (λ f → (c : C) → D c (f (r c))) (lam-Id h) d)
                       (λ c → transp (D c) (h (r c)) (d c))
    transp-funext
      = transp-contr (funext {f = f}) (λ { (g , h) → ∀ d 
                                                   → Id (transp {A = ∀ a → B a} (λ f → (c : C) → D c (f (r c))) (lam-Id 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-Id-β ∙ refl)
        d
--------------------------------------------------------------------------------

module _ {i} {j} {A : Set i} {B : Set j} (r : A → B) (s : B → A) (p : ∀ a → Id (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 → Id (g (f a)) a)
  (fg : ∀ b → Id (f (g b)) b)
  where

  private
    nat : ∀ {i j} {A : Set i} {B : Set j} {f g : A → B} (h : ∀ a → Id (f a) (g a)) {x y} (p : Id x y)
        → Id (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 → Id (f a) a) a
          → Id (h (f a)) (ap f (h a))
    lemma f h a = sym (cancelr (nat h (h a) ∙ ap₂ _∙_ refl ap-id))

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

    coherence : ∀ b → Id (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 : Id x y) q → Id (transp (λ a → Id (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-Id
          (fg y)
          ( compute-transp (fg y) (gf' (g y)) ∙
            (ap₂ _∙_ refl (coherence _) ∙ ∙-transpose-left (sym ∙-idr)))

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

abstract
  is-contr-Id : ∀ {i} {A : Set i} → is-contr A → ∀ x y → is-contr (Id {A = A} x y)
  is-contr-Id cA x y .is-contr-center
    = sym (is-contr-all-paths cA x x) ∙ is-contr-all-paths cA x y
  is-contr-Id 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-Id (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-Id λ 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 → Id (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' → Id (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-Id
                       (lam-Id (λ a → J' (λ a' q → Id (transp B q (f a')) (f a)) (β a) refl))
                       ( transp-funext {B = B} {D = D}
                       ∙ lam-Id λ c →
                         transp-contr (p (r c))
                         (λ { (xx , yy) → Id (transp (D c) (J' (λ a' q → Id (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 = Id {A = Σ C λ c' → Id (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)

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

data W {i j} (A : Set i) (B : A → Set j) : Set (i ⊔ j) where
  sup : (a : A) (f : B a → W A B) → W A B

module _ {i j k} {A : Set i} {B : A → Set j}
  (P : W A B → Set k) (sup' : ∀ a f → (∀ b → P (f b)) → P (sup a f))
  where

  W-elim : ∀ x → P x
  W-elim (sup a f) = sup' a f (λ b → W-elim (f b))

module _ {i j k} (I : Set i) (A : I → Set j) (B : ∀ {i} → A i → Set k) (child : ∀ {i} {a} → B {i} a → I) where
  
  -- data IW₁ : I → Set where
  --   sup : ∀ i (a : A i) (f : (b : B a) → IW₁ (child b)) → IW₁ i

  IW₀ : Set (i ⊔ j ⊔ k)
  IW₀ = W (Σ I A) λ p → B (snd p)

  wf : IW₀ → I → Set (i ⊔ k)
  wf (sup (i , a) f) j = Id i j × (∀ b → wf (f b) (child b))

  IW : I → Set (i ⊔ j ⊔ k)
  IW i = Σ IW₀ λ x → wf x i

  IW-sup : ∀ i (a : A i) (f : (b : B a) → IW (child b)) → IW i
  IW-sup i a f = (sup (i , a) (λ b → fst (f b)))
               , refl
               , λ b → snd (f b)

  IW-elim
    : (P : ∀ i → IW i → Set)
    → (∀ i a f → (∀ b → P _ (f b)) → P i (IW-sup i a f))
    → ∀ i x → P i x
  IW-elim P d i (sup a f , refl , g) = d i (a .snd) (λ b → f b , g b) λ b → IW-elim P d _ (f b , g b)

  IW-elim-β
    : (P : ∀ i → IW i → Set)
    → (d : ∀ i a f → (∀ b → P _ (f b)) → P i (IW-sup i a f))
    → ∀ i a f → Id (IW-elim P d i (IW-sup i a f)) (d i a f λ b → IW-elim P d _ (f b))
  IW-elim-β P d i a f = refl

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

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

abstract
  is-prop-all-paths : ∀ {i} {A : Set i} → is-prop A → (x y : A) → Id 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 : Id {A = Σ A λ a → ∀ b → Id a b} (cA .is-contr-center , cA .is-contr-path) (cA' .is-contr-center , cA' .is-contr-path)
      inner = pair-Id
              (is-contr-all-paths cA _ _)
              (lam-Id λ a → is-contr-all-paths (is-contr-Id 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))