{-# OPTIONS --without-K #-}
module Lib where

open import Agda.Primitive
private
  variable
    i j k l : Level
    A B C : Set i

{- Functions -}

id : A → A
id x = x

infixr 9 _∘_
_∘_ : {A : Set i} {B : A → Set j} {C : {x : A} → B x → Set k} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) → ((x : A) → C (g x))
f ∘ g = λ x → f (g x)
{-# INLINE _∘_ #-}

infixr -1 _$_
_$_ : {A : Set i} {B : A → Set j} → ((a : A) → B a) → ((a : A) → B a)
f $ x = f x
{-# INLINE _$_ #-}

{- Equality -}

infix 4 _≡_
data _≡_ {A : Set i} (x : A) : A → Set i where
  instance refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}

J : {A : Set i}{a₀ : A} → (P : {a₁ : A} → a₀ ≡ a₁ → Set j) → P refl → {a₁ : A} → (a₍₀₁₎ : a₀ ≡ a₁) → P a₍₀₁₎
J P p refl = p

cong : {a₀ a₁ : A} → (f : A → B) → a₀ ≡ a₁ → f a₀ ≡ f a₁
cong f refl = refl

cong-id : {a₀ a₁ : A} (a₍₀₁₎ : a₀ ≡ a₁) → cong id a₍₀₁₎ ≡ a₍₀₁₎
cong-id refl = refl

cong-id' : {a₀ a₁ : A} (a₍₀₁₎ : a₀ ≡ a₁) → a₍₀₁₎ ≡ cong id a₍₀₁₎
cong-id' refl = refl

cong-∘ : {a₀ a₁ : A} {f : B → C} {g : A → B} (a₍₀₁₎ : a₀ ≡ a₁) →
         cong (f ∘ g) a₍₀₁₎ ≡ cong f (cong g a₍₀₁₎)
cong-∘ refl = refl

cong-cong : {a₀ a₁ : A} {f : B → C} {g : A → B} (a₍₀₁₎ : a₀ ≡ a₁) →
            cong f (cong g a₍₀₁₎) ≡ cong (f ∘ g) a₍₀₁₎
cong-cong refl = refl

sym : {a₀ a₁ : A} → (a₍₀₁₎ : a₀ ≡ a₁) → a₁ ≡ a₀
sym refl = refl

trans : {a₀ a₁ a₂ : A} → (a₍₀₁₎ : a₀ ≡ a₁) → (a₍₁₂₎ : a₁ ≡ a₂) → a₀ ≡ a₂
trans refl refl = refl

subst : {a₀ a₁ : A} → (P : A → Set i) → a₀ ≡ a₁ → P a₀ → P a₁
subst P refl p = p

subst2 : {A : Set i} → {B : A → Set j} →
         {a₀ a₁ : A} → {b₀ : B a₀} → {b₁ : B a₁} →
         (P : (a : A) → (b : B a) → Set k) →
         (a₍₀₁₎ : a₀ ≡ a₁) → subst B a₍₀₁₎ b₀ ≡ b₁ →
         P a₀ b₀ → P a₁ b₁
subst2 P refl refl p = p

-- TODO: Express this with `subst3`?
subst2' : {A : Set i} → {B : A → Set j} → {C : A → Set k} →
          {a₀ a₁ : A} → {b₀ : B a₀}{b₁ : B a₁} → {c₀ : C a₀}{c₁ : C a₁} →
          (P : (a : A) → (b : B a) → (c : C a) → Set l) →
          (a₍₀₁₎ : a₀ ≡ a₁) →
          (b₍₀₁₎ : subst B a₍₀₁₎ b₀ ≡ b₁) →
          (c₍₀₁₎ : subst C a₍₀₁₎ c₀ ≡ c₁) →
          P a₀ b₀ c₀ → P a₁ b₁ c₁
subst2' P refl refl refl p = p

subst3 : {A : Set i} → {B : A → Set j} → {C : (a : A) → B a → Set k} →
         {a₀ a₁ : A} → {b₀ : B a₀}{b₁ : B a₁} → {c₀ : C a₀ b₀}{c₁ : C a₁ b₁} →
         (P : (a : A) → (b : B a) → (c : C a b) → Set l) →
         (a₍₀₁₎ : a₀ ≡ a₁) →
         (b₍₀₁₎ : subst B a₍₀₁₎ b₀ ≡ b₁) →
         subst2 C a₍₀₁₎ b₍₀₁₎ c₀ ≡ c₁ →
         P a₀ b₀ c₀ → P a₁ b₁ c₁
subst3 P refl refl refl p = p

-- https://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.Core.html#2708
module ≡-Reasoning {A : Set i} where

  infix  3 _∎
  infixr 2 _≡⟨⟩_ step-≡ step-≡˘
  infix  1 begin_

  begin_ : ∀{x y : A} → x ≡ y → x ≡ y
  begin_ x≡y = x≡y

  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
  _ ≡⟨⟩ x≡y = x≡y

  step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
  step-≡ _ y≡z x≡y = trans x≡y y≡z

  step-≡˘ : ∀ (x {y z} : A) → y ≡ z → y ≡ x → x ≡ z
  step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z

  _∎ : ∀ (x : A) → x ≡ x
  _∎ _ = refl

  syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
  syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

{- Unit / Top -}

record ⊤ : Set where
  instance constructor tt
{-# BUILTIN UNIT ⊤ #-}

{- Sigma -}

infixr 4 _,_
record Σ (A : Set i) (B : A → Set j) : Set (i ⊔ j) where
  constructor _,_
  field
    π₁ : A
    π₂ : B π₁
open Σ public
{-# BUILTIN SIGMA Σ #-}

{- Product -}

infixr 4 _,′_
infixr 2 _×_

_×_ : (A : Set i) → (B : Set j) → Set (i ⊔ j)
A × B = Σ A (λ _ → B)

_,′_ : A → B → A × B
_,′_ = _,_