module HeterogenousCongruence where

open import Level using ()

data _≃_ {l} {A : Set l} (a : A) : {A' : Set l} → A' → Set l where
  refl : a ≃ a

cong : ∀ {a b} {A₁ A₂ : Set a} {t₁ : A₁} {t₂ : A₂} →
            {B₁ : A₁ → Set b} → {B₂ : A₂ → Set b} →
            {f₁ : (x : A₁) → B₁ x} → {f₂ : (x : A₂) → B₂ x} →
            t₁ ≃ t₂ → f₁ ≃ f₂ → f₁ t₁ ≃ f₂ t₂
cong {a} {b} {A₁} {.A₁} {t₁} refl eqf = {!!}

cong₂ : ∀ {a b} {A₁ A₂ : Set a} {t₁ : A₁} {t₂ : A₂} →
             {B₁ : A₁ → Set b} → {B₂ : A₂ → Set b} →
             {f₁ : (x : A₁) → B₁ x} → {f₂ : (x : A₂) → B₂ x} →
             t₁ ≃ t₂ → B₁ ≃ B₂ → f₁ ≃ f₂ → f₁ t₁ ≃ f₂ t₂
cong₂ {a} {b} {A₁} {.A₁} {t₁} refl refl refl = refl