{-# OPTIONS --type-in-type --rewriting #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

infixl 30 _∙_
infixr 30 _,_

postulate
  _＝_ : {A : Set} → A → A → Set
  refl' : {A : Set} (a : A) → (a ＝ a)
  Σ : (A : Set) (B : A → Set) → Set
  _,_ : {A : Set} {B : A → Set} (a : A) → B a → Σ A B
  fst : {A : Set} {B : A → Set} → Σ A B → A
  snd : {A : Set} {B : A → Set} (u : Σ A B) → B (fst u)
  fstβ : {A : Set} {B : A → Set} (a : A) (b : B a) → fst {A} {B} (a , b) ≡ a
{-# REWRITE fstβ #-}
postulate
  sndβ : {A : Set} {B : A → Set} (a : A) (b : B a) → snd {A} {B} (a , b) ≡ b
{-# REWRITE sndβ #-}
postulate
  Π : (A : Set) (B : A → Set) → Set
  𝛌 : {A : Set} {B : A → Set} (f : (x : A) → B x) → Π A B
  _∙_ : {A : Set} {B : A → Set} (f : Π A B) (a : A) → B a
  Πβ : {A : Set} {B : A → Set} (f : (x : A) → B x) (a : A) → (𝛌 f ∙ a) ≡ f a
{-# REWRITE Πβ #-}
postulate
  Id : {A : Set} (B : A → Set) {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) (b₀ : B a₀) (b₁ : B a₁) → Set
  Id-const : (A B : Set) {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) →
    Id {A} (λ _ → B) a₂ ≡ _＝_ {B}
{-# REWRITE Id-const #-}
postulate
  ap : {A : Set} {B : A → Set} (f : (x : A) → B x)
    {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) → Id B a₂ (f a₀) (f a₁)
  ＝-Σ : {A : Set} {B : A → Set} (u v : Σ A B) →
    (u ＝ v) ≡ Σ (fst u ＝ fst v) (λ p → Id B p (snd u) (snd v))
{-# REWRITE ＝-Σ #-}
postulate
  Id-Π : {Δ : Set} {A : Δ → Set} {B : (x : Δ) → A x → Set}
    {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁)
    (f₀ : Π (A δ₀) (B δ₀)) (f₁ : Π (A δ₁) (B δ₁)) →
    Id (λ x → Π (A x) (B x)) δ₂ f₀ f₁ ≡
    Π (Σ (A δ₀) (λ a₀ → Σ (A δ₁) (λ a₁ → Id A δ₂ a₀ a₁))) (λ aₓ →
    Id {Σ Δ A} (λ x → B (fst x) (snd x)) {δ₀ , fst aₓ} {δ₁ , fst (snd aₓ)} (δ₂ , snd (snd aₓ))
      (f₀ ∙ fst aₓ) (f₁ ∙ fst (snd aₓ)))
{-# REWRITE Id-Π #-}
postulate
  _↓ : {X₀ X₁ : Set} (X₂ : X₀ ＝ X₁) → (X₀ → X₁ → Set)
  refl'↓ : (A : Set) → (refl' A ↓) ≡ (_＝_ {A})
{-# REWRITE refl'↓ #-}
postulate
  Id-∙ : {Δ : Set} {A : Δ → Set} (f : (δ : Δ) → Π (A δ) (λ _ → Set))
    (a : (δ : Δ) → A δ) {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁)
    (x₀ : f δ₀ ∙ a δ₀) (x₁ : f δ₁ ∙ a δ₁) →
    Id (λ δ → f δ ∙ a δ) δ₂ x₀ x₁ ≡ ((ap f δ₂ ∙ (a δ₀ , a δ₁ , ap a δ₂) ↓) x₀ x₁)
{-# REWRITE Id-∙ #-}

frob-ap-∙² : {Δ : Set} (A B : Π Δ (λ _ → Set))
  {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁) (x₀ : A ∙ δ₀) (x₁ : A ∙ δ₁) (x₂ : Id (A ∙_) δ₂ x₀ x₁) (y₀ : B ∙ δ₀) (y₁ : B ∙ δ₁) →
  Id (λ u → B ∙ (fst u)) {δ₀ , x₀} {δ₁ , x₁} (δ₂ , x₂) y₀ y₁ →
  Id (B ∙_) δ₂ y₀ y₁
frob-ap-∙² {Δ} A B f a {δ₀} {δ₁} δ₂ x₀ x₁ x₂ = ?