{-# OPTIONS --postfix-projections --prop #-}
module Id-Acyclic where

open import Agda.Primitive
open import Lib
open import Fam as _
open import Id as _
open import Id-Tele as _
open import Id-Misc as _
open import Pi as _

-----------------------------
--- "John Major" equality ---
-----------------------------
--  If A is a hSet and B a type family over A, we can compare (b₁ : B a₁) and (b₂ : B a₂)
--   by comparing (a₁, b₁) and (a₂, b₂) in Σ A B.

module JM where
  module _ {ic jc} {C : Fam {ic} {jc}} ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄ where
    private
      open Id-Tele-r C
      module C   = Fam C
      module CId = IdM C _

    module _ {id jd} {D : Fam {id} {jd}} ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ ⦃ DId-Elim-C : Id-Elim D C ⦄ where
      private
        open Id-Tele-r D
        module D          = Fam D
        module DId        = IdM D _
        module DC         = Fam (D ∗ C)
        module DId-Elim-C = Id-ElimM D C _
        module DCId       = Id-Intro (Id-Intro-∗ {C = D} {D = C})

      module _ {A : D.Ty} ⦃ IsSet-A : DId.IsSet A ⦄ (B : D.Tm A → C.Ty) where
        module IsSet-A = DId.IsSet IsSet-A

        Id : ∀ {a₁ a₂ : D.Tm A} (b₁ : C.Tm (B a₁)) (b₂ : C.Tm (B a₂)) → DC.Ty
        Id {a₁} {a₂} b₁ b₂ = DCId.Id (a₁ , b₁) (a₂ , b₂)

        Id-in : ∀ {a : D.Tm A} {b₁ : C.Tm (B a)} {b₂ : C.Tm (B a)}
               → C.Tm (CId.Id b₁ b₂) → DC.Tm (Id b₁ b₂)
        Id-in p = DId.idp , CId.trans DId-Elim-C.transp-β p

        Id-out : ∀ {a : D.Tm A} {b₁ : C.Tm (B a)} {b₂ : C.Tm (B a)}
               → DC.Tm (Id b₁ b₂) → C.Tm (CId.Id b₁ b₂)
        Id-out (p , q) = CId.trans (CId.sym (CId.trans (DId-Elim-C.ap (DId-Elim-C.transp B _) (IsSet-A.K _)) DId-Elim-C.transp-β)) q

    module _ {id jd ie je} {D : Fam {id} {jd}} ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ ⦃ DId-Elim-C : Id-Elim D C ⦄ ⦃ CId-Elim-D : Id-Elim C D ⦄
             {E : Fam {ie} {je}} ⦃ EId : Id-Intro E ⦄ ⦃ EId-Elim-E : Id-Elim E E ⦄ ⦃ EId-Elim-C : Id-Elim E C ⦄
             ⦃ CId-Elim-E : Id-Elim C E ⦄ ⦃ DId-Elim-E : Id-Elim D E ⦄ where
      private
        open Id-Tele-r D
        open Id-Tele-r E
        module D    = Fam D
        module DId  = IdM D _
        module DC   = Fam (D ∗ C)
        module DCId = IdM (D ∗ C) _
        module E    = Fam E
        module EId  = IdM E _
        module EC   = Fam (E ∗ C)
        module ECId = IdM (E ∗ C) _
        module EId-Elim-C = Id-ElimM E C _
        module DId-Elim-C = Id-ElimM D C _
        module DId-Elim-E = Id-ElimM D E _

      module _ {A : D.Ty} ⦃ IsSet-A : DId.IsSet A ⦄ {B : E.Ty} ⦃ IsSet-B : EId.IsSet B ⦄ (F : D.Tm A → E.Tm B) (P : E.Tm B → C.Ty) where
        abstract
          baseChange↑ : ∀ {a₁ a₂ : D.Tm A} {c₁ : C.Tm (P (F a₁))} {c₂ : C.Tm (P (F a₂))}
                     → D.Tm (DId.Id a₁ a₂) → EC.Tm (Id P c₁ c₂) → DC.Tm (Id (P ∘ F) c₁ c₂)
          baseChange↑ {a₁} {a₂} {c₁} {c₂} p q = DCId.trans e₀ e₃ where
            e₀ : DC.Tm (Id (P ∘ F) c₁ (DId-Elim-C.transp (P ∘ F) c₁ p))
            e₀ = p , CId.idp

            e₁ : EC.Tm (Id P c₁ (DId-Elim-C.transp (P ∘ F) c₁ p))
            e₁ = DId-Elim-E.ap F p , DId-Elim-C.J (λ (y , p) → CId.Id (EId-Elim-C.transp P c₁ (DId-Elim-E.ap F p)) (DId-Elim-C.transp (P ∘ F) c₁ p))
                                                  (CId.trans (CId.trans (EId-Elim-C.ap (EId-Elim-C.transp P c₁) DId-Elim-E.J-β) EId-Elim-C.transp-β) (CId.sym DId-Elim-C.transp-β)) _

            e₂ : EC.Tm (Id P (DId-Elim-C.transp (P ∘ F) c₁ p) c₂)
            e₂ = ECId.trans (ECId.sym e₁) q

            e₃ : DC.Tm (Id (P ∘ F) (DId-Elim-C.transp (P ∘ F) c₁ p) c₂)
            e₃ = Id-in (P ∘ F) (Id-out P e₂)

        abstract
          baseChange↓ : ∀ {a₁ a₂ : D.Tm A} {c₁ : C.Tm (P (F a₁))} {c₂ : C.Tm (P (F a₂))}
                     → D.Tm (DId.Id a₁ a₂) → DC.Tm (Id (P ∘ F) c₁ c₂) → EC.Tm (Id P c₁ c₂)
          baseChange↓ {a₁} {a₂} {c₁} {c₂} p q = ECId.trans e₁ e₃ where
            e₀ : DC.Tm (Id (P ∘ F) c₁ (DId-Elim-C.transp (P ∘ F) c₁ p))
            e₀ = p , CId.idp

            e₁ : EC.Tm (Id P c₁ (DId-Elim-C.transp (P ∘ F) c₁ p))
            e₁ = DId-Elim-E.ap F p , DId-Elim-C.J (λ (y , p) → CId.Id (EId-Elim-C.transp P c₁ (DId-Elim-E.ap F p)) (DId-Elim-C.transp (P ∘ F) c₁ p))
                                                  (CId.trans (CId.trans (EId-Elim-C.ap (EId-Elim-C.transp P c₁) DId-Elim-E.J-β) EId-Elim-C.transp-β) (CId.sym DId-Elim-C.transp-β)) _

            e₂ : DC.Tm (Id (P ∘ F) (DId-Elim-C.transp (P ∘ F) c₁ p) c₂)
            e₂ = DCId.trans (DCId.sym e₀) q

            e₃ : EC.Tm (Id P (DId-Elim-C.transp (P ∘ F) c₁ p) c₂)
            e₃ = Id-in P (Id-out (P ∘ F) e₂)

  module _ {ic jc} {C : Fam {ic} {jc}} ⦃ CId : Id-Intro C ⦄ ⦃ CId-Elim-C : Id-Elim C C ⦄
           {id jd} {D : Fam {id} {jd}} ⦃ DId : Id-Intro D ⦄ ⦃ DId-Elim-D : Id-Elim D D ⦄ ⦃ DId-Elim-C : Id-Elim D C ⦄ ⦃ CId-Elim-D : Id-Elim C D ⦄
           {ie je} {E : Fam {ie} {je}} ⦃ EId : Id-Intro E ⦄ ⦃ EId-Elim-E : Id-Elim E E ⦄ ⦃ EId-Elim-C : Id-Elim E C ⦄ ⦃ CId-Elim-E : Id-Elim C E ⦄
           ⦃ DId-Elim-E : Id-Elim D E ⦄ ⦃ EId-Elim-D : Id-Elim E D ⦄
           (U : E .Fam.Ty) (El : E .Fam.Tm U → E .Fam.Ty) where
    private
      open Id-Tele-r C
      open Id-Tele-r D
      open Id-Tele-r E
      module C                    = Fam C
      module CId                  = IdM C _
      module D                    = Fam D
      module DId                  = IdM D _
      module DC                   = Fam (D ∗ C)
      module E                    = Fam E
      module EId                  = IdM E _
      module DEC                  = Fam ((D ∗ E) ∗ C)
      module DE                   = Fam (D ∗ E)
      module DEId                 = IdM (D ∗ E) _
      module DECId                = IdM ((D ∗ E) ∗ C) _
      module DId-Elim-C           = Id-ElimM D C _
      module EId-Elim-C           = Id-ElimM E C _
      module DId-Elim-E           = Id-ElimM D E _
      module DId-Elim↕-E          = Id-Elim↕ D E _
      module DId-Elim-DEC-Param-E = Id-Elim-ParamM D E ((D ∗ E) ∗ C) ⦃ CId-Elim-E-Param-D = cheat ⦄ _
      module EId-Elim-DEC         = Id-ElimM E ((D ∗ E) ∗ C) _

    IE : Fam
    IE = record { Ty = E.Tm U ; Tm = λ A → E.Tm (El A) }
    module _ ⦃ ECPi : Pi IE C ⦄ where
      module ECPi = Pi ECPi

      abstract
        transp-Π : ∀ {A : D.Ty} {P : D.Tm A → E.Tm U} {Q : ∀ a → E.Tm (El (P a)) → C.Ty} {x y} {p : D.Tm (DId.Id x y)} {f : ∀ p → C.Tm (Q x p)}
                   → C.Tm (CId.Id (DId-Elim-C.transp (λ a → ECPi.Π (P a) (Q a)) (ECPi.lam f) p)
                                  (ECPi.lam (λ b → let e₀ = f (DId-Elim↕-E.J↕ (λ (z , _) → El (P z)) (_ , p) b (_ , DId.idp))
                                                       e₁ = DId-Elim-C.J (λ (z , q) → Q z (DId-Elim↕-E.J↕ (λ (z , _) → El (P z)) (_ , p) b (_ , q))) e₀ (_ , p)
                                                       e₂ = EId-Elim-C.transp (Q _) e₁ (DId-Elim↕-E.J↕-β _ _ _)
                                                   in e₂)))
        transp-Π {A} {P} {Q} {x} {y} {p} {f}
          = DId-Elim-C.J (λ (y , p) → CId.Id (DId-Elim-C.transp (λ a → ECPi.Π (P a) (Q a)) (ECPi.lam f) p)
                                             (ECPi.lam (λ b → let e₀ = f (DId-Elim↕-E.J↕ (λ (z , _) → El (P z)) (_ , p) b (_ , DId.idp))
                                                                  e₁ = DId-Elim-C.J (λ (z , q) → Q z (DId-Elim↕-E.J↕ (λ (z , _) → El (P z)) (_ , p) b (_ , q))) e₀ (_ , p)
                                                                  e₂ = EId-Elim-C.transp (Q _) e₁ (DId-Elim↕-E.J↕-β _ _ _)
                                                              in e₂)))
                         (CId.trans DId-Elim-C.transp-β (ECPi.xi (λ b →
                            EId-Elim-C.J (λ (z , q) → CId.Id (f z) (EId-Elim-C.transp (Q _)
                                                                    (DId-Elim-C.J (λ (z , q) → Q z (DId-Elim↕-E.J↕ (λ (z , _) → El (P z)) (_ , DId.idp) b (_ , q)))
                                                                    (f (DId-Elim↕-E.J↕ (λ (z , _) → El (P z)) (_ , DId.idp) b (_ , DId.idp))) (_ , DId.idp)) q))
                                         (CId.sym (CId.trans EId-Elim-C.transp-β DId-Elim-C.J-β)) _)))
                         _

      module _ {A : D.Ty} ⦃ IsSet-A : DId.IsSet A ⦄ {P : D.Tm A → E.Tm U} ⦃ IsSet-P : ∀ {a} → EId.IsSet (El (P a)) ⦄ {Q : ∀ a → E.Tm (El (P a)) → C.Ty}
               {a₁ a₂ : D.Tm A} {b₁ : ∀ p → C.Tm (Q a₁ p)} {b₂ : ∀ p → C.Tm (Q a₂ p)} where

        abstract
          funext : D.Tm (DId.Id a₁ a₂)
                 → (∀ p₁ p₂ → DE.Tm (Id (El ∘ P) p₁ p₂) → DEC.Tm (Id {A = A , El ∘ P} (λ (a , p) → Q a p) (b₁ p₁) (b₂ p₂)))
                 → DC.Tm (Id (λ a → ECPi.Π (P a) (Q a)) (ECPi.lam b₁) (ECPi.lam b₂))
          funext q h = q , CId.trans transp-Π (ECPi.xi (λ a →
            let a'  = DId-Elim-E.transp (El ∘ P) a (DId.sym q)
                r   = q , EId.trans DId-Elim-E.transp-trans (EId.trans (DId-Elim-E.ap (DId-Elim-E.transp (El ∘ P) _) (DId.trans-sym-l _)) DId-Elim-E.transp-β)
                h'  = h a' a r
                l₁ : ∀ a → DEC.Tm (Id {A = A , El ∘ P} (λ (a , p) → Q a p)
                                      (b₁ (DId-Elim-E.transp (El ∘ P) a (DId.sym DId.idp)))
                                      (b₁ a))
                l₁ a = EId-Elim-DEC.J
                         (λ (b , _) → Id {A = A , (El ∘ P)} (λ (a , p) → Q a p) (b₁ b) (b₁ a))
                         DECId.idp (_ , EId.sym (EId.trans (DId-Elim-E.ap (DId-Elim-E.transp (El ∘ P) a) DId.sym-β) DId-Elim-E.transp-β))
                l₂ : ∀ a → DEC.Tm (Id {A = A , El ∘ P} (λ (a , p) → Q a p)
                                      (EId-Elim-C.transp (Q a₁)
                                        (DId-Elim-C.J (λ (y , p) → Q y (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) (a₁ , DId.idp) a (y , p)))
                                          (b₁ (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) _ a _)) (_ , DId.idp))
                                        (DId-Elim↕-E.J↕-β (λ (y , _) → El (P y)) (a₁ , DId.idp) a))
                                      (EId-Elim-C.transp (Q a₁)
                                        (b₁ (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) _ a _))
                                        (DId-Elim↕-E.J↕-β (λ (y , _) → El (P y)) (a₁ , DId.idp) a)))
                l₂ a = Id-in (λ (a , p) → Q a p)
                       (CId.ap (λ k → EId-Elim-C.transp (Q a₁) k (DId-Elim↕-E.J↕-β (λ (y , _) → El (P y)) (a₁ , DId.idp) a)) DId-Elim-C.J-β)
                l₃ : ∀ a → DEC.Tm (Id {A = A , El ∘ P} (λ (a , p) → Q a p)
                                      (EId-Elim-C.transp (Q a₁)
                                        (b₁ (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) _ a _))
                                        (DId-Elim↕-E.J↕-β (λ (y , _) → El (P y)) (a₁ , DId.idp) a))
                                      (b₁ a))
                l₃ a = EId-Elim-DEC.J (λ (b , q) → Id {A = A , El ∘ P} (λ (a , p) → Q a p)
                                                      (EId-Elim-C.transp (Q a₁) (b₁ _) q)
                                                      (b₁ b))
                                      (Id-in (λ (a , p) → Q a p) EId-Elim-C.transp-β)
                                      (_ , DId-Elim↕-E.J↕-β (λ (y , _) → El (P y)) (a₁ , DId.idp) a)
                l₀ : ∀ a → DEC.Tm (Id {A = A , El ∘ P} (λ (a , p) → Q a p)
                                      (EId-Elim-C.transp (Q a₁)
                                        (DId-Elim-C.J (λ (y , p) → Q y (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) (a₁ , DId.idp) a (y , p)))
                                          (b₁ (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) _ a _)) (_ , DId.idp))
                                        (DId-Elim↕-E.J↕-β (λ (y , _) → El (P y)) (a₁ , DId.idp) a))
                                      (b₁ (DId-Elim-E.transp (El ∘ P) a (DId.sym DId.idp))))
                l₀ a = DECId.trans (DECId.trans (l₂ a) (l₃ a)) (DECId.sym (l₁ a))
                l : DEC.Tm (Id {A = A , El ∘ P} (λ (a , p) → Q a p)
                               (EId-Elim-C.transp (Q a₂)
                                 (DId-Elim-C.J (λ (y , p) → Q y (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) (a₂ , q) a (y , p)))
                                   (b₁ (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) _ a _)) (_ , q))
                                 (DId-Elim↕-E.J↕-β (λ (y , _) → El (P y)) (a₂ , q) a))
                               (b₁ a'))
                l = DId-Elim-DEC-Param-E.J _
                    (λ (a₂ , q) a → Id {A = A , El ∘ P} (λ (a , p) → Q a p)
                                       (EId-Elim-C.transp (Q a₂)
                                         (DId-Elim-C.J (λ (y , p) → Q y (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) (a₂ , q) a (y , p)))
                                           (b₁ (DId-Elim↕-E.J↕ (λ (y , _) → El (P y)) _ a _)) (_ , q))
                                         (DId-Elim↕-E.J↕-β (λ (y , _) → El (P y)) (a₂ , q) a))
                                       (b₁ (DId-Elim-E.transp (El ∘ P) a (DId.sym q))))
                    l₀ _ a
                h'' = Id-out {D = D ∗ E} (λ (a , p) → Q a p) (DECId.trans l h')
            in h''))

        -- JM.funext' is a variant of JM.funext with some propositional truncations added.
        -- JM.funext' actually cannot be proven in general: it would require the
        --  axiom of choice (note that even if we assume the axiom of choice
        --  externally, it does not neccessarily hold in our presheaf model).
        -- However, it only needs instances of the axiom of choice that do hold in
        --  our applications, when the families involved are representable.
        postulate
          choice-U : ∀ {A} {i} {X : E.Tm (El A) → Set i} → (∀ a → ∥ X a ∥) → ∥ (∀ a → X a) ∥
          choice-E : ∀ {A x} {i} {X : EId.Singl {A} x → Set i} → (∀ a → ∥ X a ∥) → ∥ (∀ a → X a) ∥
        --   ∥ (a : Tm A) → X a ∥ ≃ (a : Tm A) → ∥ X a ∥ holds: when evaluating
        --   these presheaves at some context Γ, both sides are the propositional
        --   truncation of the evaluation of X at the extended context (Γ ▷ A).

        abstract
          funext' : ∥ D.Tm (DId.Id a₁ a₂) ∥
                  → (∀ p₁ p₂ → DE.Tm (Id (El ∘ P) p₁ p₂) → ∥ DEC.Tm (Id {A = A , El ∘ P} (λ (a , p) → Q a p) (b₁ p₁) (b₂ p₂)) ∥)
                  → ∥ DC.Tm (Id (λ a → ECPi.Π (P a) (Q a)) (ECPi.lam b₁) (ECPi.lam b₂)) ∥
          funext' p h = ∥-∥-bind p λ p →
                        ∥-∥-bind (choice-U λ p₁ → choice-E λ (p₂ , q) → h p₁ p₂ (p , q)) λ h →
                        ∣ funext p (λ p₁ p₂ q → h p₁ (p₂ , Id-out (El ∘ P) (DEId.trans (DEId.sym (p , EId.idp)) q))) ∣