{-# OPTIONS --without-K #-}

module lib where

open import Agda.Primitive

idfun : ∀{ℓ}{A : Set ℓ} → A → A
idfun x = x

------------------------------------------------------------------------------
-- equality
------------------------------------------------------------------------------

data _≡_ {ℓ}{A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x

infix 4 _≡_

_◾_ : ∀{ℓ}{A : Set ℓ}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ◾ e = e

infixl 4 _◾_

_⁻¹ : ∀{ℓ}{A : Set ℓ}{x y : A} → x ≡ y → y ≡ x
refl ⁻¹ = refl

infix 5 _⁻¹

_≡⟨_⟩_ : ∀{ℓ}{A : Set ℓ}(x : A){y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ x≡y ⟩ y≡z = x≡y ◾ y≡z

infixr 2 _≡⟨_⟩_

_∎ : ∀{ℓ}{A : Set ℓ}(x : A) → x ≡ x
x ∎ = refl

infix  3 _∎

coe : ∀{ℓ}{A B : Set ℓ} → A ≡ B → A → B
coe refl a = a

_≡[_]≡_ : ∀{ℓ}{A B : Set ℓ} → A → A ≡ B → B → Set ℓ
x ≡[ α ]≡ y = ((coe α x) ≡ y)

infix 4 _≡[_]≡_

ap : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(f : A → B){a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
    → f a₀ ≡ f a₁
ap f refl = refl

transport : ∀{ℓ ℓ'}{A : Set ℓ}(P : A → Set ℓ'){x y : A}(p : x ≡ y) → P x → P y
transport P p a = coe (ap P p) a

trap : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{P : A → Set ℓ'}{B : Set ℓ''}{x y : B}{f : B → A}(e : x ≡ y){u : P (f x)} →
  transport P (ap f e) u ≡ transport (λ z → P (f z)) e u
trap refl = refl

trconst : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{x y : A}(e : x ≡ y){u : B} → transport (λ _ → B) e u ≡ u
trconst refl = refl

apd : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}(f : (x : A) → B x){a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
    → f a₀ ≡[ ap B a₂ ]≡ f a₁
apd f refl = refl

apd' : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}(f : (x : A) → B x){a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
    → f a₀ ≡ transport B (a₂ ⁻¹) (f a₁)
apd' f refl = refl

apd'' : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}(f : (x : A) → B x){a₀ a₁ : A}(a₂ : a₁ ≡ a₀)
    → f a₀ ≡ transport B a₂ (f a₁)
apd'' f refl = refl

apid : ∀{ℓ}{A : Set ℓ}{x y : A}(p : x ≡ y) → ap (λ x → x) p ≡ p
apid refl = refl

apap : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}{f : A → B}{g : B → C}
       {a₀ a₁ : A}(a₂ : a₀ ≡ a₁) → ap (λ x → g (f x)) a₂ ≡ ap g (ap f a₂)
apap refl = refl

trtr : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : Set ℓ'}(P : B → Set ℓ'')(f : A → B)
       {a a' : A}(p : a ≡ a'){b : B}(q : b ≡ f a){u : P b}
     → transport (λ z → P (f z)) p (transport P q u)
     ≡ transport P (q ◾ ap f p) u
trtr P f refl refl = refl

trtr' : ∀{ℓ ℓ'}{A : Set ℓ}(P : A → Set ℓ'){x y : A}(p : y ≡ x){u : P x} →
  transport P p (transport P (p ⁻¹) u) ≡ u
trtr' P refl = refl

trself :
  ∀{ℓ ℓ'}{A : Set ℓ}(P : A → Set ℓ')(f : (x : A) → P x){a a' : A}(p : a ≡ a') →
  transport P (p ⁻¹) (f a') ≡ f a
trself P f refl = refl

tr$ : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}(P : A → Set ℓ'){C : Set ℓ''}{a a' : A}(f : P a → C)(e : a ≡ a'){u : P a'} →
  f (transport P (e ⁻¹) u) ≡ transport (λ z → P z → C) e f u
tr$ P f refl = refl

J : ∀{ℓ ℓ'}{A : Set ℓ} {x : A} (P : {y : A} → x ≡ y → Set ℓ') → P refl → {y : A} → (w : x ≡ y) → P w
J P pr refl = pr

trrefl : ∀{ℓ ℓ'}{A : Set ℓ}(P : A → Set ℓ'){x : A}(w : P x) → transport P refl w ≡ w
trrefl P w = refl

tr2 : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : A → Set ℓ'}(P : (a : A) → B a → Set ℓ'')
  {a₀ a₁ : A}(a₀₁ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}(b₀₁ : transport B a₀₁ b₀ ≡ b₁) →
  P a₀ b₀ → P a₁ b₁
tr2 {A = A}{B} P {a₀}{a₁} a₀₁ {b₀} b₀₁ w = transport (P a₁) b₀₁ (J (λ {a₁} a₀₁ → P a₁ (transport B a₀₁ b₀)) (transport (P a₀) (trrefl B b₀ ⁻¹) w) a₀₁)

tr2' : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : Set ℓ'}(P : A → B → Set ℓ'')
  {a₀ a₁ : A}(a₀₁ : a₀ ≡ a₁){b₀ b₁ : B}(b₀₁ : b₀ ≡ b₁) → P a₀ b₀ → P a₁ b₁
tr2' {A = A}{B} P {a₀}{a₁} a₀₁ {b₀} b₀₁ w = transport (P a₁) b₀₁ (J (λ {a₁} a₀₁ → P a₁ b₀) w a₀₁)

≡inv : ∀{ℓ}{A : Set ℓ} {x y : A} (p : x ≡ y) → (p ◾ p ⁻¹) ≡ refl
≡inv refl = refl

≡inv' : ∀{ℓ}{A : Set ℓ} {x y : A} (p : x ≡ y) → (p ⁻¹ ◾ p) ≡ refl
≡inv' refl = refl

coeap2 : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a₀ a₁ : A}(a₂ : a₀ ≡ a₁){t : B a₁}
       → coe (ap B a₂) (coe (ap B (a₂ ⁻¹)) t) ≡ t
coeap2 refl = refl

coeap2' : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a₀ a₁ : A}(a₂ : a₀ ≡ a₁){t : B a₀}
       → coe (ap B (a₂ ⁻¹)) (coe (ap B a₂) t) ≡ t
coeap2' refl = refl

ap2 : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}(f : A → B → C)
    → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁){b₀ b₁ : B}(b₂ : b₀ ≡ b₁)
    → f a₀ b₀ ≡ f a₁ b₁
ap2 f refl refl = refl

ap2d : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : A → Set ℓ'}{C : Set ℓ''}(f : (x : A) → B x → C)
    → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}(b₂ : b₀ ≡[ ap B a₂ ]≡ b₁)
    → f a₀ b₀ ≡ f a₁ b₁
ap2d f refl refl = refl

[_]_◾_ : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a a' : A}{b : B a}
         (f : (x : A) → B x)(p : b ≡ f a)(q : a ≡ a')
       → b ≡[ ap B q ]≡ f a'
[ f ] refl ◾ refl = refl

$$Set=
  : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : A → Set ℓ'}(C : (x : A) → B x → Set ℓ'')
  → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}(b₂ : b₀ ≡[ ap B a₂ ]≡ b₁)
  → C a₀ b₀ ≡ C a₁ b₁
$$Set= C refl refl = refl

$$= : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : A → Set ℓ'}{C : (x : A) → B x → Set ℓ''}
      (f : (a : A)(b : B a) → C a b)
    → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}(b₂ : b₀ ≡[ ap B a₂ ]≡ b₁)
    → f a₀ b₀ ≡[ $$Set= C a₂ b₂ ]≡ f a₁ b₁
$$= f refl refl = refl

$$Set=i
  : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : A → Set ℓ'}(C : {x : A} → B x → Set ℓ'')
  → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}(b₂ : b₀ ≡[ ap B a₂ ]≡ b₁)
  → C b₀ ≡ C b₁
$$Set=i C refl refl = refl

$$=i : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : A → Set ℓ'}{C : {x : A} → B x → Set ℓ''}
       (f : {a : A}(b : B a) → C b)
     → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}(b₂ : b₀ ≡[ ap B a₂ ]≡ b₁)
     → f b₀ ≡[ $$Set=i C a₂ b₂ ]≡ f b₁
$$=i f refl refl = refl

ap3 : ∀{ℓ ℓ' ℓ'' ℓ'''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}{D : Set ℓ'''}
      (f : A → B → C → D)
    → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
      {b₀ b₁ : B}(b₂ : b₀ ≡ b₁)
      {c₀ c₁ : C}(c₂ : c₀ ≡ c₁)
    → f a₀ b₀ c₀ ≡ f a₁ b₁ c₁
ap3 f refl refl refl = refl

ap3d : ∀{ℓ ℓ' ℓ'' ℓ'''}{A : Set ℓ}{B : A → Set ℓ'}{C : (a : A) → B a → Set ℓ''}{D : Set ℓ'''}
       (f : (x : A)(y : B x) → C x y → D)
     → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}(b₂ : b₀ ≡[ ap B a₂ ]≡ b₁)
       {c₀ : C a₀ b₀}{c₁ : C a₁ b₁}(c₂ : c₀ ≡[ ap2d C a₂ b₂ ]≡ c₁)
     → f a₀ b₀ c₀ ≡ f a₁ b₁ c₁
ap3d f refl refl refl = refl

ap4 : ∀{ℓ ℓ' ℓ'' ℓ''' ℓ''''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}{D : Set ℓ'''}{E : Set ℓ''''}
      (f : A → B → C → D → E)
    → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
      {b₀ b₁ : B}(b₂ : b₀ ≡ b₁)
      {c₀ c₁ : C}(c₂ : c₀ ≡ c₁)
      {d₀ d₁ : D}(d₂ : d₀ ≡ d₁)
    → f a₀ b₀ c₀ d₀ ≡ f a₁ b₁ c₁ d₁
ap4 f refl refl refl refl = refl

ap4' : ∀{ℓ ℓ' ℓ'' ℓ''' ℓ''''}
       {A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}{D : B → Set ℓ'''}{E : Set ℓ''''}
      (f : A → (b : B) → C → D b → E)
    → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
      {b₀ b₁ : B}(b₂ : b₀ ≡ b₁)
      {c₀ c₁ : C}(c₂ : c₀ ≡ c₁)
      {d₀ : D b₀}{d₁ : D b₁}(d₂ : d₀ ≡[ ap D b₂ ]≡ d₁)
    → f a₀ b₀ c₀ d₀ ≡ f a₁ b₁ c₁ d₁
ap4' f refl refl refl refl = refl

coe2r : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a₀ a₁ : A}
        (a₂ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}
      → b₀ ≡[ ap B a₂ ]≡ b₁ → b₀ ≡ coe (ap B (a₂ ⁻¹)) b₁
coe2r refl p = p

coe2l : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a₀ a₁ : A}
        (a₂ : a₀ ≡ a₁){b₀ : B a₀}{b₁ : B a₁}
      → b₀ ≡ coe (ap B (a₂ ⁻¹)) b₁ → b₀ ≡[ ap B a₂ ]≡ b₁
coe2l refl p = p

coecoeap
  : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a b c : A}(p : a ≡ b)(q : b ≡ c)
    {t : B a}
  → coe (ap B q) (coe (ap B p) t) ≡ coe (ap B (p ◾ q)) t
coecoeap refl refl = refl

coecoe : ∀{ℓ}{A B C : Set ℓ}(P : A ≡ B)(Q : B ≡ C){a : A}
       → coe Q (coe P a) ≡ coe (P ◾ Q) a
coecoe refl refl = refl

≡= : ∀{ℓ}{A₀ A₁ : Set ℓ}(A₂ : A₀ ≡ A₁)
     {a₀ : A₀}{a₁ : A₁}(a₂ : a₀ ≡[ A₂ ]≡ a₁)
     {b₀ : A₀}{b₁ : A₁}(b₂ : b₀ ≡[ A₂ ]≡ b₁)
   → (a₀ ≡ b₀) ≡ (a₁ ≡ b₁)
≡= refl refl refl = refl

◾lid : ∀{ℓ}{A : Set ℓ}{x y : A}(p : x ≡ y) → (refl ◾ p) ≡ p
◾lid refl = refl

◾rid : ∀{ℓ}{A : Set ℓ}{x y : A}(p : x ≡ y) → (p ◾ refl) ≡ p
◾rid refl = refl

◾ass : ∀{ℓ}{A : Set ℓ}{a b c d : A}(p : a ≡ b)(q : b ≡ c)(r : c ≡ d)
     → (p ◾ (q ◾ r)) ≡ ((p ◾ q) ◾ r)
◾ass refl refl refl = refl

ap◾ : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(f : A → B){a b c : A}(p : a ≡ b)(q : b ≡ c)
    → ap f (p ◾ q) ≡ (ap f p ◾ ap f q)
ap◾ f refl refl = refl

◾ap◾ap
  : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}
    (f : A → B)(g : B → C){a a' : A}(r : a ≡ a'){b : B}(q : b ≡ f a){c : C}(p : c ≡ g b)
  → (p ◾ ap g q ◾ ap (λ z → g (f z)) r)
  ≡ (p ◾ ap g (q ◾ ap f r))
◾ap◾ap f g refl refl refl = refl

coe-apply :
 ∀ {α β γ}{A : Set α}{B : Set β}(C : A → B → Set γ)
   {b b' : B}(p : b ≡ b')(f : ∀ a → C a b)(a : A)
 → coe (ap (λ x → ∀ a → C a x) p) f a ≡ coe (ap (C a) p) (f a)
coe-apply C refl f a = refl

coe=
  : ∀{ℓ}{A B : Set ℓ}
    {p₀ p₁ : A ≡ B}(p₂ : p₀ ≡ p₁)
    {t : A}
  → coe p₀ t ≡ coe p₁ t
coe= refl = refl

apconst : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{a b : A}(p : a ≡ b){t : B} → ap (λ _ → t) p ≡ refl
apconst refl = refl

ap3const
  : ∀{ℓ ℓ' ℓ'' ℓ'''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}{D : Set ℓ'''}
    → {a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
      {b₀ b₁ : B}(b₂ : b₀ ≡ b₁)
      {c₀ c₁ : C}(c₂ : c₀ ≡ c₁)
      {d : D}
    → ap3 (λ _ _ _ → d) a₂ b₂ c₂ ≡ refl
ap3const refl refl refl = refl

coeap : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : A → Set ℓ'}{C : A → Set ℓ''}{a a' : A}(p : a ≡ a')
        (f : {a : A} → B a → C a){b : B a}
      → coe (ap C p) (f b) ≡ f (coe (ap B p) b)
coeap refl _ = refl

coeap2d : ∀{ℓ ℓ' ℓ''}{A : Set ℓ}{B : A → Set ℓ'}{C : {a : A} → B a → Set ℓ''}
        {a a' : A}(p : a ≡ a')
        (f : {a : A}(b : B a) → C b){b : B a}
      → coe ($$Set=i C p refl) (f b) ≡ f (coe (ap B p) b)
coeap2d refl _ = refl

apap3 : ∀{ℓ ℓ' ℓ'' ℓ'''}{A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''}{D : Set ℓ'''}
        (f : A → B → C → D)
        {a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
        {b₀ b₁ : B}(b₂ : b₀ ≡ b₁)
        {c₀ c₁ : C}(c₂ : c₀ ≡ c₁)
        {ℓ''''}{E : Set ℓ''''}
        (g : D → E)
      → ap g (ap3 f a₂ b₂ c₂) ≡ ap3 (λ x y z → g (f x y z)) a₂ b₂ c₂
apap3 f refl refl refl g = refl

------------------------------------------------------------------------------
-- sigma
------------------------------------------------------------------------------

record Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  constructor _,Σ_
  field
    proj₁ : A
    proj₂ : B proj₁

infixl 5 _,Σ_

open Σ public

aptot : ∀{ℓ}{A : Set ℓ}{B : A → Set}(f : (x : A) → B x){a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
    → _≡_ {A = Σ Set λ X → X} (B a₀ ,Σ f a₀) (B a₁ ,Σ f a₁)
aptot f refl = refl

,Σ= : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a a' : A}{b : B a}{b' : B a'}
     (p : a ≡ a') → b ≡[ ap B p ]≡ b' → _≡_ {A = Σ A B} (a ,Σ b) (a' ,Σ b')
,Σ= refl refl = refl

,Σ=0 : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a a' : A}{b : B a}{b' : B a'}
    → _≡_ {A = Σ A B} (a ,Σ b) (a' ,Σ b') → a ≡ a'
,Σ=0 = ap proj₁

,Σ=1 : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a a' : A}{b : B a}{b' : B a'}
      (p : (a ,Σ b) ≡ (a' ,Σ b')) → b ≡[ ap B (,Σ=0 p) ]≡ b'
,Σ=1 {B = B}{b = b}{b'} p = coe (ap (λ z → coe z b ≡ b') (apap {f = proj₁}{B} p)) (apd proj₂ p)

,Σ=η : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{w w' : Σ A B}
      (p : w ≡ w') → ,Σ= (,Σ=0 p) (,Σ=1 p) ≡ p
,Σ=η refl = refl

,Σ=β0 : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a a' : A}{b : B a}{b' : B a'}
       (p : a ≡ a')(q : b ≡[ ap B p ]≡ b') → ,Σ=0 (,Σ= p q) ≡ p
,Σ=β0 refl refl = refl

,Σ=β1 : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}{a a' : A}{b : B a}{b' : B a'}
       (p : a ≡ a')(q : b ≡[ ap B p ]≡ b')
     → ,Σ=1 (,Σ= p q) ≡[ ap (λ r → b ≡[ ap B r ]≡ b') (,Σ=β0 p q) ]≡ q
,Σ=β1 refl refl = refl

Σ= : ∀{ℓ ℓ'}
     {A₀ A₁ : Set ℓ}(A₂ : A₀ ≡ A₁)
     {B₀ : A₀ → Set ℓ'}{B₁ : A₁ → Set ℓ'}(B₂ : B₀ ≡[ ap (λ z → z → Set ℓ') A₂ ]≡ B₁)
   → Σ A₀ B₀ ≡ Σ A₁ B₁
Σ= refl refl = refl

,Σ=2 : {A : Set}{B : A → Set}{a : A}{b : B a}
       {α : a ≡ a}{β : b ≡[ ap B α ]≡ b}
     → (w : α ≡ refl) → β ≡[ ap (λ γ → b ≡[ ap B γ ]≡ b) w ]≡ refl
     → ,Σ= α β ≡ refl
,Σ=2 refl refl = refl

,Σ==
  : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}
    {a₀ a₁ : A}{b₀ : B a₀}{b₁ : B a₁}
    {p₀ p₁ : a₀ ≡ a₁}(p₂ : p₀ ≡ p₁)
    {q₀ : b₀ ≡[ ap B p₀ ]≡ b₁}{q₁ : b₀ ≡[ ap B p₁ ]≡ b₁}(q₂ : q₀ ≡[ ≡= refl {a₀ = coe (ap B p₀) b₀}{coe (ap B p₁) b₀} (ap (λ z → coe (ap B z) b₀) p₂) refl ]≡ q₁)
  → _≡_ (,Σ= p₀ q₀) (,Σ= p₁ q₁)
,Σ== refl refl = refl

ΣisSet
  : ∀{ℓ ℓ'}{A : Set ℓ}{B : A → Set ℓ'}
    (isSetA : {a a' : A}(p q : a ≡ a') → p ≡ q)
    (isSetB : {a : A}{b b' : B a}(p q : b ≡ b') → p ≡ q)
  → {w w' : Σ A B}(p q : w ≡ w') → p ≡ q
ΣisSet {A = A}{B} isSetA isSetB {a ,Σ b}{a' ,Σ b'} p q = ,Σ=η p ⁻¹ ◾ ,Σ== {p₀ = ,Σ=0 p}{,Σ=0 q} (isSetA _ _) {,Σ=1 p}{,Σ=1 q} (isSetB _ _) ◾ ,Σ=η q

-- pointed types

,Σp= : {A₀ A₁ : Set}(A₂ : A₀ ≡ A₁){a₀ : A₀}{a₁ : A₁}(a₂ : a₀ ≡[ A₂ ]≡ a₁)
    → _≡_ {A = Σ Set λ X → X} (A₀ ,Σ a₀) (A₁ ,Σ a₁)
,Σp= A₂ {b₀}{b₁} b₂ = ,Σ= A₂ (coe (ap (λ z → b₀ ≡[ z ]≡ b₁) (apid A₂ ⁻¹)) b₂)

,Σp=1 : {A₀ A₁ : Set}{a₀ : A₀}{a₁ : A₁}
     → (p : (A₀ ,Σ a₀) ≡ (A₁ ,Σ a₁)) → a₀ ≡[ ,Σ=0 p ]≡ a₁
,Σp=1 refl = refl

-- nondependent

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

infixl 4 _×_

,×= : ∀{ℓ}{A B : Set ℓ}{a a' : A}{b b' : B}
    → a ≡ a' → b ≡ b' → _≡_ {A = A × B} (a ,Σ b) (a' ,Σ b')
,×= refl refl = refl

------------------------------------------------------------------------------
-- top
------------------------------------------------------------------------------

record ⊤ : Set where
  constructor tt

set⊤ : {x y : ⊤}(p q : x ≡ y) → p ≡ q
set⊤ refl refl = refl

------------------------------------------------------------------------------
-- bottom
------------------------------------------------------------------------------

data ⊥ : Set where

⊥-elim : ∀{ℓ}{A : Set ℓ} → ⊥ → A
⊥-elim ()

¬ : Set → Set
¬ A = A → ⊥

------------------------------------------------------------------------------
-- disjoint union
------------------------------------------------------------------------------

data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B
infixr 1 _⊎_

ind⊎ : {A B : Set}(P : A ⊎ B → Set) → ((a : A) → P (inl a)) → ((b : B) → P (inr b))
     → (w : A ⊎ B) → P w
ind⊎ P ca cb (inl a) = ca a
ind⊎ P ca cb (inr b) = cb b

------------------------------------------------------------------------------
-- function space
------------------------------------------------------------------------------

infixr -1 _$_

_$_ : ∀{i}{A : Set i}{j}{B : A → Set j} →
  ((x : A) → B x) → ((x : A) → B x)
f $ x = f x

→=''
  : ∀{ℓ ℓ'}
    {A₀ A₁ : Set ℓ}(A₂ : A₀ ≡ A₁)
    {B₀ B₁ : Set ℓ'}(B₂ : B₀ ≡ B₁)
  → (A₀ → B₀) ≡ (A₁ → B₁)
→='' refl refl = refl

→='
  : ∀{ℓ ℓ'}
    {A₀ A₁ : Set ℓ}(A₂ : A₀ ≡ A₁)
    {B₀ : A₀ → Set ℓ'}{B₁ : A₁ → Set ℓ'}(B₂ : B₀ ≡[ →='' A₂ refl ]≡ B₁)
  → ((x₀ : A₀) → B₀ x₀) ≡ ((x₁ : A₁) → B₁ x₁)
→=' refl refl = refl

→i='
  : ∀{ℓ ℓ'}
    {A₀ A₁ : Set ℓ}(A₂ : A₀ ≡ A₁)
    {B₀ : A₀ → Set ℓ'}{B₁ : A₁ → Set ℓ'}(B₂ : B₀ ≡[ →='' A₂ refl ]≡ B₁)
  → ({x₀ : A₀} → B₀ x₀) ≡ ({x₁ : A₁} → B₁ x₁)
→i=' refl refl = refl

→='''
  : ∀{ℓ ℓ'}
    {A₀ A₁ : Set ℓ}(A₂ : A₀ ≡ A₁)
    {B₀ : A₀ → A₀ → Set ℓ'}{B₁ : A₁ → A₁ → Set ℓ'}(B₂ : B₀ ≡[ →='' A₂ (→='' A₂ refl) ]≡ B₁)
  → ((x₀ : A₀) → B₀ x₀ x₀) ≡ ((x₁ : A₁) → B₁ x₁ x₁)
→=''' refl refl = refl

$T=
  : ∀{ℓ ℓ'}
    {A₀ A₁ : Set ℓ}(A₂ : A₀ ≡ A₁)
    {B₀ : A₀ → Set ℓ'}{B₁ : A₁ → Set ℓ'}(B₂ : {x₀ : A₀}{x₁ : A₁}(x₂ : x₀ ≡[ A₂ ]≡ x₁) → B₀ x₀ ≡ B₁ x₁)
    {a₀ : A₀}{a₁ : A₁}(a₂ : a₀ ≡[ A₂ ]≡ a₁)
  → B₀ a₀ ≡ B₁ a₁
$T= refl B₂ refl = B₂ refl

------------------------------------------------------------------------------
-- lifting a type
------------------------------------------------------------------------------

record Lift {ℓ ℓ'}(A : Set ℓ) : Set (ℓ ⊔ ℓ') where
  constructor lift
  field
    unlift : A

open Lift public

------------------------------------------------------------------------------
-- natural numbers
------------------------------------------------------------------------------

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

ind : (P : ℕ → Set)(z : P zero)(s : {n : ℕ} → P n → P (suc n))(n : ℕ) → P n
ind P z s zero = z
ind P z s (suc n) = s (ind P z s n)

toLevel : ℕ → Level
toLevel zero = lzero
toLevel (suc n) = lsuc (toLevel n)

------------------------------------------------------------------------------
-- finite sets
------------------------------------------------------------------------------

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} → Fin n → Fin (suc n)

toLevelF : {n : ℕ} → Fin n → Level
toLevelF zero = lzero
toLevelF (suc n) = lsuc (toLevelF n)

------------------------------------------------------------------------------
-- booleans
------------------------------------------------------------------------------

data 𝟚 : Set where
  tt ff : 𝟚

if_then_else_ : ∀{ℓ}{C : 𝟚 → Set ℓ}(b : 𝟚)(c : C tt)(d : C ff) → C b
if tt then c else d = c
if ff then c else d = d

------------------------------------------------------------------------------
-- propositions
------------------------------------------------------------------------------

F : ∀{i} → Set i → Set i
F A = A → A → A

fst : ∀{i}{A : Set i} → F A
fst = λ x x' → x

snd : ∀{i}{A : Set i} → F A
snd = λ x x' → x'

-- TODO: rename to isPfProp
isprop : ∀{i} → Set i → Set i
isprop A = _≡_ {A = F A} fst snd

fst1 : ∀{i}{A : Set i}{j}{B : A → Set j} → (x : A) → F (B x)
fst1 x y y' = y

snd1 : ∀{i}{A : Set i}{j}{B : A → Set j} → (x : A) → F (B x)
snd1 x y y' = y'

-- TODO: rename to isPfPropd
isprop1 : ∀{i}{A : Set i}{j}(B : A → Set j) → Set (i ⊔ j)
isprop1 {_}{A} B = _≡_ {A = (x : A) → F (B x)} fst1 snd1

isprop1→isprop : ∀{i}{A : Set i}{j}{B : Set j}(a : A) → isprop1 (λ (a : A) → B) → isprop B
isprop1→isprop a₀ pB = ap (λ z → z a₀) pB

isprop× : ∀{i}{A : Set i}{j}{B : Set j} → isprop A → isprop B → isprop (A × B)
isprop× {A = A}{B = B} pA pB =
  ap (λ z → λ (w w' : A × B) → (z (proj₁ w) (proj₁ w') ,Σ proj₂ w))  pA ◾
  ap (λ z → λ (w w' : A × B) → (proj₁ w' ,Σ z (proj₂ w) (proj₂ w'))) pB

ispropΣ : ∀{i}{A : Set i}{j}{B : A → Set j} → isprop A → isprop1 B → isprop (Σ A B)
ispropΣ {_}{A}{_}{B} pA pB =
  J {A = F A} {fst} (λ {h} e → _≡_ {A = F (Σ A B)} fst (λ w w' → h (proj₁ w) (proj₁ w') ,Σ transport B (ap (λ z → z (proj₁ w) (proj₁ w')) e) (proj₂ w))) refl pA ◾
  ap (λ z → λ w w' → proj₁ w' ,Σ z (proj₁ w') (transport B (ap (λ z → z (proj₁ w) (proj₁ w')) pA) (proj₂ w)) (proj₂ w')) pB

f : ∀{i}{D : Set i}{j}{A : D → Set j}{k}(B : Σ D A → Set k)
  (d : D)(ab ab' : Σ (A d) λ a → B (d ,Σ a))(h : (d : D) → F (A d))(e : _≡_ {A = (d : D) → F (A d)} (λ d a a' → a) h) → B (d ,Σ h d (proj₁ ab) (proj₁ ab'))
f B d ab ab' h e = transport (λ a → B (d ,Σ a)) (ap (λ z → z d (proj₁ ab) (proj₁ ab')) e) (proj₂ ab)

ispropΣ1 : ∀{i}{D : Set i}{j}{A : D → Set j}{k}{B : Σ D A → Set k} →
  isprop1 A →
  isprop1 B →
  isprop1 (λ d → Σ (A d) λ a → B (d ,Σ a))
ispropΣ1 {B = B} pA pB =
  J (λ {h} e → fst1 ≡ (λ d ab ab' → h d (proj₁ ab) (proj₁ ab') ,Σ f B d ab ab' h e)) refl pA ◾
  ap (λ z → λ d ab ab' → proj₁ ab' ,Σ z (d ,Σ proj₁ ab') (f B d ab ab' _ pA) (proj₂ ab')) pB

ispropΣ' : ∀{i}{A : Set i}{j}{B : A → Set j} → isprop A → isprop1 B → isprop (Σ A B)
ispropΣ' {_}{A}{_}{B} pA pB = ap (λ z → z tt) (ispropΣ1 {_}{⊤}{_}{λ _ → A}{_}{λ ta → B (proj₂ ta)} (ap (λ z _ → z) pA) (ap (λ z ta → z (proj₂ ta)) pB))

isprop→ : ∀{i}{A : Set i}{j}{B : Set j} → isprop B → isprop (A → B)
isprop→ pB = ap (λ z → λ f f' → λ x → z (f x) (f' x)) pB

ispropΠ : ∀{i}{A : Set i}{j}{B : A → Set j} → isprop1 B → isprop ((x : A) → B x)
ispropΠ pB = ap (λ z → λ f f' x → z x (f x) (f' x)) pB

ispropΠi : ∀{i}{A : Set i}{j}{B : A → Set j} → isprop1 B → isprop ({x : A} → B x)
ispropΠi pB = ap (λ z → λ f f' {x} → z x (f {x}) (f' {x})) pB

ispropΠ1' : ∀{i}{A : Set i}{j}{B : A → Set j}{k}{C : (x : A) → B x → Set k} →
  isprop1 (λ w → C (proj₁ w) (proj₂ w)) → isprop1 (λ x → (y : B x) → C x y)
ispropΠ1' {_}{A}{_}{B}{_}{C} pC = ap (λ z x f f' y → z (x ,Σ y) (f y) (f' y)) pC

ispropΠ1 : ∀{i}{D : Set i}{j}{A : D → Set j}{k}{B : Σ D A → Set k} →
  isprop1 B → isprop1 (λ d → (a : A d) → B (d ,Σ a))
ispropΠ1 {_}{D}{_}{A}{_}{B} pB = ap (λ z d f f' a → z (d ,Σ a) (f a) (f' a)) pB

ispropΠ' : ∀{i}{A : Set i}{j}{B : A → Set j} → isprop1 B → isprop ((x : A) → B x)
ispropΠ' {_}{A}{_}{B} pB = ap (λ z → z tt) (ispropΠ1 {_}{⊤}{_}{λ _ → A}{_}{λ ta → B (proj₂ ta)} (ap (λ z ta → z (proj₂ ta)) pB))

ispropΠi1 : ∀{i}{A : Set i}{j}{B : A → Set j}{k}{C : (x : A) → B x → Set k} →
  isprop1 (λ w → C (proj₁ w) (proj₂ w)) → isprop1 (λ x → {y : B x} → C x y)
ispropΠi1 {_}{A}{_}{B}{_}{C} pC = ap (λ z x f f' {y} → z (x ,Σ y) (f {y}) (f' {y})) pC

ispropLift1 : ∀{i}{A : Set i}{j}{B : A → Set j} → isprop1 B →
  ∀{k} → isprop1 (λ a → Lift {_}{k} (B a))
ispropLift1 pB = ap (λ z x y y' → lift (z x (unlift y) (unlift y'))) pB

isProp : ∀{i} → Set i → Set i
isProp A = (x y : A) → x ≡ y

toProp : ∀{i}{A : Set i} → isprop A → isProp A
toProp pA x y = ap (λ z → z x y) pA

toProp1 : ∀{i}{A : Set i}{j}{B : A → Set j} → isprop1 B → {x : A} → isProp (B x)
toProp1 pB {x} y y' = ap (λ z → z x y y') pB

isset : ∀{i}(A : Set i) → Set i
isset A = _≡_ {A = {x x' : A} → F (x ≡ x')} fst snd

isSet : ∀{i}(A : Set i) → Set i
isSet A = {x x' : A}(e e' : x ≡ x') → e ≡ e'

toSet : ∀{i}{A : Set i} → isprop A → isSet A
toSet {i}{A} pA {x}{x'} e e' = k e ◾ k e' ⁻¹
  where
    k : {y : A}(p : x ≡ y) → p ≡ (toProp pA x' x ⁻¹ ◾ toProp pA x' y)
    k refl = ≡inv' (toProp pA x' x) ⁻¹

p⊤ : isprop ⊤
p⊤ = refl

isPropΣ : ∀{A : Set}{B : A → Set} → isProp A → ((x : A) → isProp (B x)) → isProp (Σ A B)
isPropΣ f g (a ,Σ b) (a' ,Σ b') with f a a'
... | refl with g a b b'
... | refl = refl

{-
-- TODO: 

hh : ∀{i}{A : Set i} → isprop A → (f : A → A → A) → (λ x x' → x) ≡ f
hh {i}{A} pA f = {!!} -- I don't think we can prove this (e.g. ×Bool countermodel)

s→Pp : ∀{i}{A : Set i} → isset A → isProp (isprop A)
s→Pp {_}{A} s p p' = J (λ {f} p' → transport ((λ x x' → x) ≡_) {!!} p ≡ p') {!!} p'

isPropisprop : ∀{i}(A : Set i) → isProp (isprop A)
isPropisprop A p p' = {!toSet p!}

ispropisprop : ∀{i}{A : Set i} → isprop (isprop A)
ispropisprop {i}{A} = {!!}

f : _≡_ {A = (A : Set) → (_≡_ {A = A → A → A}(λ y y' → y)(λ y y' → y')) → A → A → A}
        (λ A pA y y' → y)
        (λ A pA y y' → y')
f = {!ap
  (λ (z : (A : Set) → isprop A → A → A → A)(A : Set)(pA : isprop A)(y : A)(y' : A) → y)
  (refl {A = (A : Set) → isprop A → A → A → A}{λ A pA y y' → y})!}
-}