text:
module Functional where

import      Lvl
open import Type

infixl 10000 _∘_
infixl 10000 _⩺_
infixl 10000 _⩹_
infixl 30 _→ᶠ_ _←_ _←ᶠ_
infixr 0 _$_

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T X X₁ X₂ X₃ X₄ Y Y₁ Y₂ Y₃ Y₄ Z : Type{ℓ}

-- Converse of a function type
_←_ : Type{ℓ₁} → Type{ℓ₂} → Type{ℓ₁ Lvl.⊔ ℓ₂}
Y ← X = X → Y

-- Function type as a function
_→ᶠ_ : Type{ℓ₁} → Type{ℓ₂} → Type{ℓ₁ Lvl.⊔ ℓ₂}
X →ᶠ Y = X → Y

-- Converse function type as a function
_←ᶠ_ : Type{ℓ₁} → Type{ℓ₂} → Type{ℓ₁ Lvl.⊔ ℓ₂}
Y ←ᶠ X = Y ← X

-- The identity function.
-- Returns the applied argument.
id : T → T
id(x) = x
{-# INLINE id #-}

-- The constant function.
-- Returns the first argument independent of the second.
const : let _ = X in Y → (X → Y)
const(x)(_) = x

-- Function application as a function.
-- Applies the first argument on the function on the second argument.
apply : X → (X → Y) → Y
apply(x)(f) = f(x)
{-# INLINE apply #-}

-- Function application as an operator
_$_ : (X → Y) → X → Y
_$_ = id
{-# INLINE _$_ #-}

_$ᵢₘₚₗ_ : ({ _ : X } → Y) → (X → Y)
f $ᵢₘₚₗ x = f{x}
{-# INLINE _$ᵢₘₚₗ_ #-}

_$ᵢₙₛₜ_ : (⦃ _ : X ⦄ → Y) → (X → Y)
f $ᵢₙₛₜ x = f ⦃ x ⦄
{-# INLINE _$ᵢₙₛₜ_ #-}

-- Function application as an operator. Function to the left, value to the right.
_⩹_ : (X → Y) → X → Y
f ⩹ x = f(x)
{-# INLINE _⩹_ #-}

-- Function application as an operator. Value to the left, function to the right.
_⩺_ : X → (X → Y) → Y
x ⩺ f = f(x)
{-# INLINE _⩺_ #-}

-- Swapping the arguments of a binary operation
swap : (X → Y → Z) → (Y → X → Z)
swap f(y)(x) = f(x)(y)
{-# INLINE swap  #-}

-- Function composition
_∘_ : let _ = X in (Y → Z) → (X → Y) → (X → Z)
(f ∘ g)(x) = f(g(x))

-- Function composition on implicit argument
_∘ᵢₘₚₗ_ : let _ = X in ({Y} → Z) → ({X} → Y) → ({X} → Z)
(f ∘ᵢₘₚₗ g){x} = f{g{x}}

-- Function composition on instance argument
_∘ᵢₙₛₜ_ : let _ = X in (⦃ Y ⦄ → Z) → (⦃ X ⦄ → Y) → (⦃ X ⦄ → Z)
(f ∘ᵢₙₛₜ g) ⦃ x ⦄ = f ⦃ g ⦃ x ⦄ ⦄

-- The S-combinator from combinatory logic.
-- It is sometimes described as a generalized version of the application operator or the composition operator.
-- Note: TODO: Applicative instance
_∘ₛ_ : (X → Y → Z) → (X → Y) → (X → Z)
(f ∘ₛ g)(x) = (f x) (g x)

_on₀_ : let _ = X in Z → (X → Y) → Z
((▫) on₀ f) = ▫ -- const

_on₁_ : let _ = X in (Y → Z) → (X → Y) → (X → Z)
((_▫) on₁ f)(y₁) = (f(y₁) ▫) on₀ f -- f(y₁) ▫

-- Function composition on a binary operator
-- A function is composed on every argument of the binary operator.
_on₂_ : let _ = X in (Y → Y → Z) → (X → Y) → (X → X → Z)
((_▫_) on₂ f)(y₁) = (f(y₁) ▫_) on₁ f -- f(y₁) ▫ f(y₂)

_on₃_ : let _ = X in (Y → Y → Y → Z) → (X → Y) → (X → X → X → Z)
((_▫_▫_) on₃ f)(y₁) = (f(y₁) ▫_▫_) on₂ f -- f(y₁) ▫ f(y₂) ▫ f(y₃)

-- TODO: Move these to Function.Multi
_∘₀_ : (Y → Z) → Y → Z
_∘₀_ = id

_∘₁_ : let _ = X₁ in (Y → Z) → (X₁ → Y) → (X₁ → Z)
_∘₁_ f = (f ∘₀_) ∘_

-- (f ∘₂ g)(x)(y) = f(g(x)(y))
_∘₂_ : let _ = X₁ ; _ = X₂ in (Y → Z) → (X₁ → X₂ → Y) → (X₁ → X₂ → Z)
_∘₂_ f = (f ∘₁_) ∘_

-- (f ∘₃ g)(x)(y)(z) = f(g(x)(y)(z))
_∘₃_ : let _ = X₁ ; _ = X₂ ; _ = X₃ in (Y → Z) → (X₁ → X₂ → X₃ → Y) → (X₁ → X₂ → X₃ → Z)
_∘₃_ f = (f ∘₂_) ∘_

-- (f ∘₄ g)(x)(y)(z)(w) = f(g(x)(y)(z)(w))
_∘₄_ : let _ = X₁ ; _ = X₂ ; _ = X₃ ; _ = X₄ in (Y → Z) → (X₁ → X₂ → X₃ → X₄ → Y) → (X₁ → X₂ → X₃ → X₄ → Z)
_∘₄_ f = (f ∘₃_) ∘_

-- map₂Arg₁ : let _ = X in (Y₁ → Y₂ → Z) → (X → Y₁) → (X → Y₂) → (X → Z)
-- map₂Arg₁ f g₁ g₂ x = f(g₁ x)(g₂ x)

-- map₂Arg₂ : let _ = X₁ ; _ = X₂ in (Y₁ → Y₂ → Z) → (X₁ → Y₁) → (X₂ → Y₂) → (X₁ → X₂ → Z)
-- map₂Arg₂ f g₁ g₂ x₁ x₂ = f(g₁ x₁)(g₂ x₂)

-- Function lifting //TODO: Consider removing because it is the same as _∘_
liftₗ : (X → Y) → ((Z → X) → (Z → Y))
liftₗ = _∘_ -- liftₗ(f) = f ∘_

liftᵣ : (X → Y) → ((Y → Z) → (X → Z))
liftᵣ = swap(_∘_) -- liftᵣ(f) = _∘ f

-- Applies an argument to two arguments of a binary function.
_$₂_ : (X → X → Y) → (X → Y)
f $₂ x = f x x

apply₂ : X → (X → X → Y) → Y
apply₂ x f = f x x

proj₂ₗ : X → Y → X
proj₂ₗ = const

proj₂ᵣ : X → Y → Y
proj₂ᵣ = const id

open import Syntax.Function public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- Properties related to negation
------------------------------------------------------------------------

module Relation.Nullary.Negation where

open import Relation.Nullary
open import Relation.Unary
open import Data.Empty
open import Data.Function
open import Data.Product as Prod
open import Data.Fin
open import Data.Fin.Dec
open import Category.Monad

contradiction : ∀ {P whatever} → P → ¬ P → whatever
contradiction p ¬p = ⊥-elim (¬p p)

contraposition : ∀ {P Q} → (P → Q) → ¬ Q → ¬ P
contraposition f ¬q p = contradiction (f p) ¬q

-- Note also the following use of flip:

private
  note : ∀ {P Q} → (P → ¬ Q) → Q → ¬ P
  note = flip

------------------------------------------------------------------------
-- Quantifier juggling

∃⟶¬∀¬ : ∀ {A} {P : Pred A} → ∃ P → ¬ (∀ x → ¬ P x)
∃⟶¬∀¬ = flip uncurry

∀⟶¬∃¬ : ∀ {A} {P : Pred A} → (∀ x → P x) → ¬ ∃ λ x → ¬ P x
∀⟶¬∃¬ ∀xPx (x , ¬Px) = ¬Px (∀xPx x)

¬∃⟶∀¬ : ∀ {A} {P : Pred A} → ¬ ∃ (λ x → P x) → ∀ x → ¬ P x
¬∃⟶∀¬ = curry

∀¬⟶¬∃ : ∀ {A} {P : Pred A} → (∀ x → ¬ P x) → ¬ ∃ (λ x → P x)
∀¬⟶¬∃ = uncurry

∃¬⟶¬∀ : ∀ {A} {P : Pred A} → ∃ (λ x → ¬ P x) → ¬ (∀ x → P x)
∃¬⟶¬∀ = flip ∀⟶¬∃¬

-- When P is a decidable predicate over a finite set the following
-- lemma can be proved.

¬∀⟶∃¬ : ∀ n (P : Pred (Fin n)) → (∀ i → Dec (P i)) →
        ¬ (∀ i → P i) → ∃ λ i → ¬ P i
¬∀⟶∃¬ n P dec ¬P = Prod.map id proj₁ $ ¬∀⟶∃¬-smallest n P dec ¬P

------------------------------------------------------------------------
-- Double-negation

¬¬-map : ∀ {P Q} → (P → Q) → ¬ ¬ P → ¬ ¬ Q
¬¬-map f = contraposition (contraposition f)

¬¬-drop : {P : Set} → ¬ ¬ ¬ P → ¬ P
¬¬-drop ¬¬¬P P = ¬¬¬P (λ ¬P → ¬P P)

¬¬-drop-Dec : {P : Set} → Dec P → ¬ ¬ P → P
¬¬-drop-Dec (yes p) ¬¬p = p
¬¬-drop-Dec (no ¬p) ¬¬p = ⊥-elim (¬¬p ¬p)

¬-drop-Dec : {P : Set} → Dec (¬ ¬ P) → Dec (¬ P)
¬-drop-Dec (yes ¬¬p) = no ¬¬p
¬-drop-Dec (no ¬¬¬p) = yes (¬¬-drop ¬¬¬p)

-- Double-negation is a monad (if we assume that all elements of ¬ ¬ P
-- are equal).

¬¬-Monad : RawMonad (λ P → ¬ ¬ P)
¬¬-Monad = record
  { return = contradiction
  ; _>>=_  = λ x f → ¬¬-drop (¬¬-map f x)
  }

¬¬-push : {P : Set} {Q : P → Set} →
          ¬ ¬ ((x : P) → Q x) → (x : P) → ¬ ¬ Q x
¬¬-push ¬¬P⟶Q P ¬Q = ¬¬P⟶Q (λ P⟶Q → ¬Q (P⟶Q P))

-- A double-negation-translated variant of excluded middle (or: every
-- nullary relation is decidable in the double-negation monad).

excluded-middle : {P : Set} → ¬ ¬ Dec P
excluded-middle ¬h = ¬h (no (λ p → ¬h (yes p)))

-- If whatever is instantiated with ¬ ¬ something, then this function
-- is call with current continuation in the double-negation monad, or,
-- if you will, a double-negation translation of Peirce's law.
--
-- In order to prove ¬ ¬ P one can assume ¬ P and prove ⊥. However, it
-- is sometimes nice to avoid leaving the double-negation monad; in
-- that case this function can be used (with whatever instantiated to
-- ⊥).

call/cc : ∀ {whatever P : Set} → ((P → whatever) → ¬ ¬ P) → ¬ ¬ P
call/cc hyp ¬p = hyp (λ p → ⊥-elim (¬p p)) ¬p

ext: agda

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Common.Prelude
open import Common.Reflection
open import Common.Equality

` : Term → Term
` (def f []) = con (quote def) (vArg (lit (qname f)) ∷ vArg (con (quote []) []) ∷ [])
` _ = lit (string "other")

macro
  primQNameType : QName → Tactic
  primQNameType f hole =
    bindTC (getType f) λ a →
    bindTC (normalise a) λ a →
    give (` a) hole

A : Set
a : A
A = _

B : Set
b : B
B = _

aName=bName : primQNameType a ≡ primQNameType b
aName=bName = refl

a = 0
b = 1.0

empty : ⊥
empty with aName=bName
... | ()

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-11-01, issue #2824
-- allow built-in pragmas in parametrized modules

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Equality

module _ (A : Set) where  -- This is the top-level module header.

{-# BUILTIN REWRITE _≡_ #-}

postulate
  P : A → Set
  a b : A
  a→b : a ≡ b

{-# REWRITE a→b #-}

test : P a → P b
test x = x

-- Should succeed.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2019-11-06 issue #4168, version with shape-irrelevance.

-- Eta-contraction of records with all-irrelevant fields is unsound.
-- In this case, it lead to a compilation error.

{-# OPTIONS --irrelevant-projections #-}

-- {-# OPTIONS -v tc.cc:20 #-}

open import Agda.Builtin.Unit
open import Common.IO using (IO; return)

main : IO ⊤
main = return _

record Box (A : Set) : Set where
  constructor box
  field
    ..unbox : A

open Box

record R (M : Set → Set) : Set₁ where
  field
    bind : (A B : Set) → M A → (A → M B) → M B
open R

works : R Box
works .bind A B x g .unbox = unbox (g (unbox x))

test : R Box
test .bind A B x g = box (unbox (g (unbox x)))
-- WAS eta-contracted to: test .bind A B x g = g (unbox x)
-- crashing compilation.

-- Compilation should succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Unit

postulate
  @0 A : Set

@0 _ : @0 Set → (Set → Set) → Set
_ = λ @0 where
  A G → G A

@0 _ : @0 Set → (Set → Set) → Set
_ = λ @0 { A G → G A }

data ⊥ : Set where

@0 _ : @0 ⊥ → Set
_ = λ @0 { () }

@0 _ : @0 ⊥ → Set
_ = λ @0 where
  ()

@0 _ : @0 ⊥ → Set
_ =
  λ @0
    @ω
    @erased
    @plenty
    @(tactic (λ _ → Set))
    @irr
    @irrelevant
    @shirr
    @shape-irrelevant
    @relevant
    @♭
    @flat
    @notlock
    @lock
    @tick where
    ()

F : ⊤ → ⊤
F = λ { tt → tt }

macro

  `F : Term → TC ⊤
  `F goal = do
    F ← withNormalisation true (quoteTC F)
    F ← quoteTC F
    unify goal F

_ :
  `F ≡
  pat-lam
    (clause []
      (arg (arg-info visible relevant) (con (quote tt) []) ∷ [])
      (con (quote tt) []) ∷
     [])
    []
_ = refl


text:
-- Category of □-coalgebras
module SOAS.Abstract.Coalgebra {T : Set} where

open import SOAS.Common
open import SOAS.Construction.Structure as Structure
open import SOAS.Context
open import SOAS.ContextMaps.Combinators
open import SOAS.ContextMaps.CategoryOfRenamings {T}
open import SOAS.Sorting
open import SOAS.Families.Core {T}
open import SOAS.Variable
open import SOAS.Families.BCCC
open import Data.Unit using (tt)

open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Box {T} as □

private
  variable
    α : T
    Γ Δ Θ : Ctx

-- Unsorted □-coalgebras
module Unsorted where
  open □.Unsorted
  record Coalg (X : Family) : Set where
    field
      r      : X ⇾ □ X
      counit : {t : X Γ} → r t id ≡ t
      comult : {ρ : Γ ↝ Δ}{ϱ : Δ ↝ Θ}{t : X Γ}
             → r t (ϱ ∘ ρ) ≡ r (r t ρ) ϱ

    -- Weakening of terms
    wkr : (Θ : Ctx) → X Γ → X (Θ ∔ Γ)
    wkr Θ t = r t (inr Θ)

    wkl : (Γ : Ctx) → X Γ → X (Γ ∔ Θ)
    wkl Γ t = r t (inl Γ)

    wk : X Γ → X (α ∙ Γ)
    wk t = r t old

  -- Unsorted coalgebra homomorphism
  record Coalg⇒ {X Y}(Xᵇ : Coalg X)(Yᵇ : Coalg Y) (f : X ⇾ Y) : Set where
    private module X = Coalg Xᵇ
    private module Y = Coalg Yᵇ
    field
      ⟨r⟩ : {ρ : Γ ↝ Δ}{t : X Γ} → f (X.r t ρ) ≡ Y.r (f t) (ρ)

  private module CoalgebraStructure = Structure 𝔽amilies Coalg

  -- Eilenberg-Moore category of a comonad
  ℂoalgebras : Category 1ℓ 0ℓ 0ℓ
  ℂoalgebras = CoalgebraStructure.StructCat (record
    { IsHomomorphism = Coalg⇒
    ; id-hom = record { ⟨r⟩ = refl }
    ; comp-hom = λ{ g f record { ⟨r⟩ = g⟨r⟩ } record { ⟨r⟩ = f⟨r⟩ } → record
      { ⟨r⟩ = trans (cong g f⟨r⟩) g⟨r⟩ } }
    })

  module ℂoalg = Category ℂoalgebras

  Coalgebra : Set₁
  Coalgebra = ℂoalg.Obj

  Coalgebra⇒ : Coalgebra → Coalgebra → Set
  Coalgebra⇒ = ℂoalg._⇒_

  module AsCoalgebra (Xᵇ : Coalgebra) where
    open Object Xᵇ public renaming (𝐶 to X ; ˢ to ᵇ)
    open Coalg ᵇ public

  -- Terminal object is a coalgebra
  ⊤ᵇ : Coalg ⊤ₘ
  ⊤ᵇ = record { r = λ _ _ → tt ; counit = refl ; comult = refl }

  -- □ X is the free coalgebra on X
  □ᵇ : (X : Family) → Coalg (□ X)
  □ᵇ X = record { r = λ b ρ ϱ → b (ϱ ∘ ρ) ; counit = refl ; comult = refl }

-- | Sorted □-coalgebras
module Sorted where
  open □.Sorted
  record Coalg (𝒳 : Familyₛ) : Set where
    field
      r      : 𝒳 ⇾̣ □ 𝒳
      counit : {t : 𝒳 α Γ} → r t id ≡ t
      comult : {ρ : Γ ↝ Δ}{ϱ : Δ ↝ Θ}{t : 𝒳 α Γ}
             → r t (ϱ ∘ ρ) ≡ r (r t ρ) ϱ

    -- Congruence in both arguments
    r≈₁ : {ρ : Γ ↝ Δ}{t₁ t₂ : 𝒳 α Γ} → t₁ ≡ t₂ → r t₁ ρ ≡ r t₂ ρ
    r≈₁ {ρ = ρ} p = cong (λ - → r - ρ) p

    r≈₂ : {ρ₁ ρ₂ : Γ ↝ Δ}{t : 𝒳 α Γ}
        → ({τ : T}{x : ℐ τ Γ} → ρ₁ x ≡ ρ₂ x)
        → r t ρ₁ ≡ r t ρ₂
    r≈₂ {t = t} p = cong (r t) (dext′ p)

    wkr : (Θ : Ctx) → 𝒳 α Γ → 𝒳 α (Θ ∔ Γ)
    wkr Θ t = r t (inr Θ)

    wkl : (Γ : Ctx) → 𝒳 α Γ → 𝒳 α (Γ ∔ Θ)
    wkl Γ t = r t (inl Γ)

    wk : {τ : T} → 𝒳 α Γ → 𝒳 α (τ ∙ Γ)
    wk t = r t old

  -- Coalgebra homomorphism
  record Coalg⇒ {𝒳 𝒴}(Xᵇ : Coalg 𝒳)(𝒴ᵇ : Coalg 𝒴) (f : 𝒳 ⇾̣ 𝒴) : Set where
    private module 𝒳 = Coalg Xᵇ
    private module 𝒴 = Coalg 𝒴ᵇ
    field
      ⟨r⟩ : {ρ : Γ ↝ Δ}{t : 𝒳 α Γ} → f (𝒳.r t ρ) ≡ 𝒴.r (f t) (ρ)

  private module CoalgebraStructure = Structure 𝔽amiliesₛ Coalg

  -- Eilenberg-Moore category of a comonad
  ℂoalgebras : Category 1ℓ 0ℓ 0ℓ
  ℂoalgebras = CoalgebraStructure.StructCat (record
    { IsHomomorphism = Coalg⇒
    ; id-hom = record { ⟨r⟩ = refl }
    ; comp-hom = λ{ g f record { ⟨r⟩ = g⟨r⟩ } record { ⟨r⟩ = f⟨r⟩ } → record
      { ⟨r⟩ = trans (cong g f⟨r⟩) g⟨r⟩ } }
    })

  module ℂoalg = Category ℂoalgebras

  Coalgebra : Set₁
  Coalgebra = ℂoalg.Obj

  Coalgebra⇒ : Coalgebra → Coalgebra → Set
  Coalgebra⇒ = ℂoalg._⇒_

  module AsCoalgebra (𝒳ᵇ : Coalgebra) where
    open Object 𝒳ᵇ public renaming (𝐶 to 𝒳 ; ˢ to ᵈ)

  -- 〖 𝒳 , 𝒴 〗 is a coalgebra for any 𝒳 and 𝒴
  〖_,_〗ᵇ : (𝒳 𝒴 : Familyₛ) → Coalg (〖 𝒳 , 𝒴 〗)
  〖 𝒳 , 𝒴 〗ᵇ = record { r = λ h ρ ϱ → h (ϱ ∘ ρ) ; counit = refl ; comult = refl }

  -- □ 𝒳 is the free coalgebra on 𝒳
  □ᵇ : (𝒳 : Familyₛ) → Coalg (□ 𝒳)
  □ᵇ 𝒳 = 〖 ℐ , 𝒳 〗ᵇ

  -- Pointed coalgebra
  record Coalgₚ (𝒳 : Familyₛ) : Set where

    field
      ᵇ : Coalg 𝒳
      η : ℐ ⇾̣ 𝒳

    open Coalg ᵇ public

    field
      r∘η : {α : T}{Γ Δ : Ctx}{v : ℐ α Γ}{ρ : Γ ↝ Δ}
          → r (η v) ρ ≡ η (ρ v)

  -- Pointed coalgebra homomorphism
  record Coalgₚ⇒  {𝒳 𝒴 : Familyₛ}(𝒳ᴮ : Coalgₚ 𝒳)(𝒴ᴮ : Coalgₚ 𝒴)
                  (f : 𝒳 ⇾̣ 𝒴) : Set where
    private module 𝒳 = Coalgₚ 𝒳ᴮ
    private module 𝒴 = Coalgₚ 𝒴ᴮ
    field
      ᵇ⇒ : Coalg⇒ 𝒳.ᵇ 𝒴.ᵇ f
      ⟨η⟩ : {α : T}{Γ : Ctx}{v : ℐ α Γ}
          → f (𝒳.η v) ≡ 𝒴.η v

    open Coalg⇒ ᵇ⇒ public

  -- Pointed coalgebra of variables
  ℐᵇ : Coalg ℐ
  ℐᵇ = record { r = λ v ρ → ρ v ; counit = refl ; comult = refl }

  ℐᴮ : Coalgₚ ℐ
  ℐᴮ = record { ᵇ = ℐᵇ ; η = id ; r∘η = refl }

  -- □ 𝒳 is free pointed coalgebra on pointed families
  □ᴮ : (𝒳 : Familyₛ) → ℐ ⇾̣ 𝒳 → Coalgₚ (□ 𝒳)
  □ᴮ 𝒳 η = record { ᵇ = □ᵇ 𝒳 ; η = λ v ρ → η (ρ v) ; r∘η = refl }

  -- Identity and point are homomorphisms
  idᴮ⇒ : {𝒳 : Familyₛ}{𝒳ᴮ : Coalgₚ 𝒳} → Coalgₚ⇒ 𝒳ᴮ 𝒳ᴮ id
  idᴮ⇒ = record { ᵇ⇒ = record { ⟨r⟩ = refl } ; ⟨η⟩ = refl }

  ηᴮ⇒ : {𝒳 : Familyₛ}(𝒳ᴮ : Coalgₚ 𝒳) → Coalgₚ⇒ ℐᴮ 𝒳ᴮ (Coalgₚ.η 𝒳ᴮ)
  ηᴮ⇒ 𝒳ᴮ = record { ᵇ⇒ = record { ⟨r⟩ = sym (Coalgₚ.r∘η 𝒳ᴮ) } ; ⟨η⟩ = refl }


text:
{-# OPTIONS --without-K --safe #-}

-- The identity pseudofunctor

module Categories.Pseudofunctor.Identity where

open import Data.Product using (_,_)

open import Categories.Bicategory using (Bicategory)
import Categories.Bicategory.Extras as BicategoryExt
open import Categories.Category using (Category)
open import Categories.Category.Instance.One using (shift)
open import Categories.Category.Product using (_⁂_)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
import Categories.Morphism.Reasoning as MorphismReasoning
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; _≃_; niHelper)
open import Categories.Pseudofunctor using (Pseudofunctor)

open Category using (module HomReasoning)
open NaturalIsomorphism using (F⇒G; F⇐G)

-- The identity pseudofunctor

idP : ∀ {o ℓ e t} {C : Bicategory o ℓ e t} → Pseudofunctor C C
idP {o} {ℓ} {e} {t} {C = C} = record
  { P₀             = λ x → x
  ; P₁             = idF
  ; P-identity     = P-identity
  ; P-homomorphism = P-homomorphism
  ; unitaryˡ       = unitaryˡ
  ; unitaryʳ       = unitaryʳ
  ; assoc          = assoc
  }
  where
    open BicategoryExt C

    P-identity : ∀ {x} → id {x} ∘F shift o ℓ e ≃ idF ∘F id
    P-identity {x} = niHelper (record
      { η       = λ _ → id₂
      ; η⁻¹     = λ _ → id₂
      ; commute = λ _ → MorphismReasoning.id-comm-sym (hom x x)
      ; iso     = λ _ → record { isoˡ = hom.identity² ; isoʳ = hom.identity² }
      })

    P-homomorphism : ∀ {x y z} → ⊚ ∘F (idF ⁂ idF) ≃ idF ∘F ⊚ {x} {y} {z}
    P-homomorphism {x} {_} {z} = niHelper (record
      { η       = λ _ → id₂
      ; η⁻¹     = λ _ → id₂
      ; commute = λ _ → MorphismReasoning.id-comm-sym (hom x z)
      ; iso     = λ _ → record { isoˡ = hom.identity² ; isoʳ = hom.identity² }
      })

    Pid  = λ {A} → NaturalTransformation.η (F⇒G (P-identity {A})) _
    Phom = λ {x} {y} {z} f,g →
           NaturalTransformation.η (F⇒G (P-homomorphism {x} {y} {z})) f,g
    λ⇒   = unitorˡ.from
    ρ⇒   = unitorʳ.from
    α⇒   = associator.from

    unitaryˡ : ∀ {x y} {f : x ⇒₁ y} →
               let open ComHom in
               [ id₁ ⊚₀ f ⇒ f ]⟨
                 Pid ⊚₁ id₂      ⇒⟨ id₁ ⊚₀ f ⟩
                 Phom (id₁ , f)  ⇒⟨ id₁ ⊚₀ f ⟩
                 λ⇒
               ≈ λ⇒
               ⟩
    unitaryˡ {x} {y} {f} = begin
      λ⇒ ∘ᵥ Phom (id₁ , f) ∘ᵥ (Pid ⊚₁ id₂)  ≈⟨ refl⟩∘⟨ elimʳ ⊚.identity ⟩
      λ⇒ ∘ᵥ Phom (id₁ , f)                  ≈⟨ hom.identityʳ ⟩
      λ⇒                                    ∎
      where
        open HomReasoning (hom x y)
        open MorphismReasoning (hom x y)

    unitaryʳ : ∀ {x y} {f : x ⇒₁ y} →
               let open ComHom in
               [ f ⊚₀ id₁ ⇒ f ]⟨
                 id₂ ⊚₁ Pid      ⇒⟨ f ⊚₀ id₁ ⟩
                 Phom (f , id₁)  ⇒⟨ f ⊚₀ id₁ ⟩
                 ρ⇒
               ≈ ρ⇒
               ⟩
    unitaryʳ {x} {y} {f} = begin
      ρ⇒ ∘ᵥ Phom (f , id₁) ∘ᵥ (id₂ ⊚₁ Pid)  ≈⟨ refl⟩∘⟨ elimʳ ⊚.identity ⟩
      ρ⇒ ∘ᵥ Phom (f , id₁)                  ≈⟨ hom.identityʳ ⟩
      ρ⇒                                    ∎
      where
        open HomReasoning (hom x y)
        open MorphismReasoning (hom x y)

    assoc : ∀ {x y z w} {f : x ⇒₁ y} {g : y ⇒₁ z} {h : z ⇒₁ w} →
            let open ComHom in
            [ (h ⊚₀ g) ⊚₀ f ⇒ h ⊚₀ (g ⊚₀ f) ]⟨
              Phom (h , g) ⊚₁ id₂  ⇒⟨ (h ⊚₀ g) ⊚₀ f ⟩
              Phom (_ , f)         ⇒⟨ (h ⊚₀ g) ⊚₀ f ⟩
              α⇒
            ≈ α⇒                   ⇒⟨ h ⊚₀ (g ⊚₀ f) ⟩
              id₂ ⊚₁ Phom (g , f)  ⇒⟨ h ⊚₀ (g ⊚₀ f) ⟩
              Phom (h , _)
            ⟩
    assoc {x} {_} {_} {w} {f} {g} {h} = begin
      α⇒ ∘ᵥ Phom (_ , f) ∘ᵥ Phom (h , g) ⊚₁ id₂  ≈⟨ refl⟩∘⟨ elimʳ ⊚.identity ⟩
      α⇒ ∘ᵥ Phom (_ , f)                         ≈⟨ hom.identityʳ ⟩
      α⇒                                         ≈˘⟨ elimˡ ⊚.identity ⟩
      id₂ ⊚₁ Phom (g , f) ∘ᵥ α⇒                  ≈˘⟨ hom.identityˡ ⟩
      Phom (h , _) ∘ᵥ id₂ ⊚₁ Phom (g , f) ∘ᵥ α⇒  ∎
      where
        open HomReasoning (hom x w)
        open MorphismReasoning (hom x w)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --cubical --safe #-}

module Data.Binary.Equatable where

open import Prelude
open import Data.Binary.Definition
open import Data.Bits.Equatable public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Andreas, 2012-02-14, issue reported by Wolfram Kahl
-- {-# OPTIONS -v scope.top:10 #-}
module Issue562 where

data Bool : Set where true false : Bool

f : Bool → Bool
f b with b
f true | _ = b
-- WAS: panic unbound variable b
-- should be:  Not in scope: b

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- 2010-11-21
-- testing correct implementation of eta for records with higher-order fields

module Issue366 where

data Bool : Set where
  true false : Bool

record R (A : Set) : Set where
  constructor r
  field
    unR : A

open R

foo : Bool
foo = unR (r (unR (r (λ (_ : Bool) → false))
              true))
-- before 2010-11-21, an incorrect implementation of eta-contraction
-- reduced foo to (unR true)
-- Error message was (due to clause compilation):
-- Incomplete pattern matching

data _==_ {A : Set}(a : A) : A -> Set where
  refl : a == a

test : foo == false
test = refl


text:
module TerminationMixingTupledCurried where

data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

data _×_ (A B : Set) : Set where
    _,_ : A -> B -> A × B

good : Nat × Nat -> Nat -> Nat
good (succ x , y) z = good (x , succ y) (succ z)
good (x , succ y) z = good (x , y) x
good xy (succ z) = good xy z
good _ _ = zero


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group where

open import Cubical.Algebra.Group.Base public
open import Cubical.Algebra.Group.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
data Nat : Set where
  zero : Nat
  suc : Nat → Nat

test : ∀{N M : Nat} → Nat → Nat → Nat
test N M = {!.N N .M!}
-- Andreas, 2016-07-10, issue 2088
-- Changed behavior:
-- The hidden variables .N and .M are made visible
-- only the visible N is split.


text:
postulate
  A : Set
  f : A → A

mutual

  F : A → Set
  F x = D (f x)

  data D : A → Set where
    c : (x : A) → F x

G : (x : A) → D x → Set₁
G _ (c _) = Set


text:
{-# OPTIONS --copatterns #-}

module Issue950b where

postulate
  A : Set

record R : Set where
  field
    x : A

record S : Set where
  field
    y : A

open R

f : ?
x f = ?

-- Good error:

-- Cannot eliminate type ?0 with projection pattern x
-- when checking that the clause x f = ? has type ?0


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT

module groups.KernelSndImageInl {i j k}
  (G : Group i) {H : Group j} {K : Group k}
  -- the argument [φ-snd], which is intended to be [φ ∘ᴳ ×-snd],
  -- gives the possibility of making the second part
  -- (the proof of being a group homomorphism) abstract.
  (φ : H →ᴳ K) (φ-snd : G ×ᴳ H →ᴳ K)
  (φ-snd-β : ∀ x → GroupHom.f φ-snd x == GroupHom.f φ (snd x))
  (G×H-is-abelian : is-abelian (G ×ᴳ H))
  where

  open import groups.KernelImage
    φ-snd (×ᴳ-inl {G = G} {H = H}) G×H-is-abelian

  private
    module G = Group G
    module H = Group H

  Ker-φ-snd-quot-Im-inl : Ker φ ≃ᴳ Ker/Im
  Ker-φ-snd-quot-Im-inl = to-hom , is-eq to from to-from from-to where
    to : Ker.El φ → Ker/Im.El
    to (h , h-in-ker) = q[ (G.ident , h) , lemma ]
      where abstract lemma = φ-snd-β (G.ident , h) ∙ h-in-ker

    abstract
      to-pres-comp : ∀ k₁ k₂ → to (Ker.comp φ k₁ k₂) == Ker/Im.comp (to k₁) (to k₂)
      to-pres-comp _ _ = ap q[_] $ Ker.El=-out φ-snd $
        pair×= (! (G.unit-l G.ident)) idp

    to-hom : Ker φ →ᴳ Ker/Im
    to-hom = group-hom to to-pres-comp

    abstract
      from' : Ker.El φ-snd → Ker.El φ
      from' ((g , h) , h-in-ker) = h , ! (φ-snd-β (g , h)) ∙ h-in-ker

      from-rel : ∀ {gh₁ gh₂} → ker/im-rel gh₁ gh₂ → from' gh₁ == from' gh₂
      from-rel {gh₁} {gh₂} = Trunc-rec (Ker.El-is-set φ _ _)
        (λ{(g , inl-g=h₁h₂⁻¹) → Ker.El=-out φ
          (H.zero-diff-same (snd (fst gh₁)) (snd (fst gh₂)) (! (snd×= inl-g=h₁h₂⁻¹)))})

    from : Ker/Im.El → Ker.El φ
    from = SetQuot-rec (Ker.El-is-set φ) from' from-rel

    abstract
      to-from : ∀ g → to (from g) == g
      to-from = SetQuot-elim
        {P = λ g → to (from g) == g}
        (λ _ → =-preserves-set Ker/Im.El-is-set)
        (λ{((g , h) , h-in-ker) → quot-rel
          [ G.inv g , ap2 _,_ (! (G.unit-l (G.inv g))) (! (H.inv-r h)) ]})
        (λ _ → prop-has-all-paths-↓ (Ker/Im.El-is-set _ _))

      from-to : ∀ g → from (to g) == g
      from-to _ = Ker.El=-out φ idp

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Unit.Base where

-- Obtain Unit
open import Agda.Builtin.Unit public
  renaming ( ⊤ to Unit )

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for Cowriter
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

module Codata.Cowriter.Bisimilarity where

open import Level using (Level; _⊔_)
open import Size
open import Codata.Thunk
open import Codata.Cowriter
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)

private
  variable
    a b c p q pq r s rs v w x : Level
    A : Set a
    B : Set b
    C : Set c
    V : Set v
    W : Set w
    X : Set x
    i : Size

data Bisim {V : Set v} {W : Set w} {A : Set a} {B : Set b}
           (R : REL V W r) (S : REL A B s) (i : Size) :
           REL (Cowriter V A ∞) (Cowriter W B ∞) (r ⊔ s ⊔ v ⊔ w ⊔ a ⊔ b) where
  [_] : ∀ {a b} → S a b → Bisim R S i [ a ] [ b ]
  _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R S) i xs ys →
        Bisim R S i (x ∷ xs) (y ∷ ys)

module _ {R : Rel W r} {S : Rel A s}
         (refl^R : Reflexive R) (refl^S : Reflexive S) where

 reflexive : Reflexive (Bisim R S i)
 reflexive {x = [ a ]}  = [ refl^S ]
 reflexive {x = w ∷ ws} = refl^R ∷ λ where .force → reflexive

module _ {R : REL V W r} {S : REL W V s} {P : REL A B p} {Q : REL B A q}
         (sym^RS : Sym R S) (sym^PQ : Sym P Q) where

 symmetric : Sym (Bisim R P i) (Bisim S Q i)
 symmetric [ a ]    = [ sym^PQ a ]
 symmetric (p ∷ ps) = sym^RS p ∷ λ where .force → symmetric (ps .force)

module _ {R : REL V W r} {S : REL W X s} {RS : REL V X rs}
         {P : REL A B p} {Q : REL B C q} {PQ : REL A C pq}
         (trans^RS : Trans R S RS) (trans^PQ : Trans P Q PQ) where

 transitive : Trans (Bisim R P i) (Bisim S Q i) (Bisim RS PQ i)
 transitive [ p ]    [ q ]    = [ trans^PQ p q ]
 transitive (p ∷ ps) (q ∷ qs) =
   trans^RS p q ∷ λ where .force → transitive (ps .force) (qs .force)

-- Pointwise Equality as a Bisimilarity
------------------------------------------------------------------------

module _ {W : Set w} {A : Set a} where

  infix 1 _⊢_≈_
  _⊢_≈_ : ∀ i → Cowriter W A ∞ → Cowriter W A ∞ → Set (a ⊔ w)
  _⊢_≈_ = Bisim _≡_ _≡_

  refl : Reflexive (i ⊢_≈_)
  refl = reflexive Eq.refl Eq.refl

  fromEq : ∀ {as bs} → as ≡ bs → i ⊢ as ≈ bs
  fromEq Eq.refl = refl

  sym : Symmetric (i ⊢_≈_)
  sym = symmetric Eq.sym Eq.sym

  trans : Transitive (i ⊢_≈_)
  trans = transitive Eq.trans Eq.trans

module _ {R : Rel W r} {S : Rel A s}
         (equiv^R : IsEquivalence R) (equiv^S : IsEquivalence S) where

  private
    module equiv^R = IsEquivalence equiv^R
    module equiv^S = IsEquivalence equiv^S

  isEquivalence : IsEquivalence (Bisim R S i)
  isEquivalence = record
    { refl  = reflexive equiv^R.refl equiv^S.refl
    ; sym   = symmetric equiv^R.sym equiv^S.sym
    ; trans = transitive equiv^R.trans equiv^S.trans
    }

setoid : Setoid w r → Setoid a s → Size → Setoid (w ⊔ a) (w ⊔ a ⊔ r ⊔ s)
setoid R S i = record
  { isEquivalence = isEquivalence (Setoid.isEquivalence R)
                                  (Setoid.isEquivalence S) {i = i}
  }

module ≈-Reasoning {W : Set w} {A : Set a} {i} where

  open import Relation.Binary.Reasoning.Setoid
              (setoid (Eq.setoid W) (Eq.setoid A) i) public


text:
{-# OPTIONS --without-K #-}

module Ch2-3 where

open import Level hiding (lift)

open import Ch2-1
open import Ch2-2

--           p
--    x ~~~~~~~~~ y
--
--
--  P x --------> P y
--
-- Lemma 2.3.1 (transport)
transport : ∀ {a b} {A : Set a} {x y : A}
  → (P : A → Set b)
  → (p : x ≡ y)
  → P x → P y
transport {a} {b} {A} {x} {y} P p = J A D d x y p P
  -- J A D d x y p P
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set (a ⊔ suc b)
    D x y p = (P : A → Set b) → P x → P y

    -- base case
    d : (x : A) → D x x refl
    d x P y = y

open import Data.Product

--   proof
--  +-----+     p      +-----+
--  |  x ~~~~~~~~~~~~~~~~ y  |
--  |     |            |     |
--  | P x |~~~~~~~~~~~~| P y |
--  +-----+     *      +-----+
--
-- Lemma 2.3.2 (path lifting property)
lift : ∀ {a b} {A : Set a}
  → (P : A → Set b)
  → (proof : Σ[ x ∈ A ] P x)
  → (y : A)
  → (p : proj₁ proof ≡ y)
  → proof ≡ (y , transport P p (proj₂ proof))
lift {a} {b} {A} P proof y p = J A D d (proj₁ proof) y p (proj₂ proof)
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set (a ⊔ b)
    D x y p = (u : P x) → (x , u) ≡ (y , transport P p u)

    -- base case
    d : (x : A) → D x x refl
    d x u = refl

--    A
--    +----------------------------------------------+
--    |                      p                       |
--    |   x ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ y  |
--    |   +                                       +  |
--    +----------------------------------------------+
--        |                                       |
--    P x |       P y                             |
--    +-------+   +----------------------------------+
--    |   v   |   |                          *    v  |
--    |  f x +-------> transport P p (f x) ~~~~~ f y |
--    |       |   |                                  |
--    +-------+   +----------------------------------+
--
-- Lemma 2.3.4 (dependent map)
apd : ∀ {a b} {A : Set a} {x y : A}
  → {P : A → Set b}
  → (f : (z : A) → P z)
  → (p : x ≡ y)
  → transport P p (f x) ≡ f y
apd {a} {b} {A} {x} {y} {P} f p = J A D d x y p P f
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → _
    D x y p = (P : A → Set b) (f : (z : A) → P z) → transport P p (f x) ≡ f y

    -- base case
    d : (x : A) → D x x refl
    d x P f = refl

open import Function using (const; _∘_)

-- Lemma 2.3.5
transportconst : ∀ {a ℓ} {A : Set a} {x y : A}
  → {B : Set ℓ}
  → (p : x ≡ y)
  → (b : B)
  → transport (const B) p b ≡ b
transportconst {a} {ℓ} {A} {x} {y} {B} p b = J A D d x y p B b
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → _
    D x y p = (B : Set ℓ) (b : B) → transport (const B) p b ≡ b

    -- base case
    d : (x : A) → D x x refl
    d x B b = refl

open import Ch2-2

-- Lemma 2.3.8
lemma-2-3-8 : ∀ {a ℓ} {A : Set a} {B : Set ℓ} {x y : A}
  → (f : A → B)
  → (p : x ≡ y)
  → apd f p ≡ transportconst p (f x) ∙ ap f p
lemma-2-3-8 {a} {ℓ} {A} {B} {x} {y} f p = J {a} {a ⊔ ℓ} A D d x y p f
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → _
    D x y p = (f : A → B) → apd f p ≡ transportconst p (f x) ∙ ap f p

    -- base case
    d : (x : A) → D x x refl
    d x f = refl

-- Lemma 2.3.9
lemma-2-3-9 : ∀ {a b} {A : Set a} {x y z : A}
  → (P : A → Set b)
  → (p : x ≡ y)
  → (q : y ≡ z)
  → (u : P x)
  → transport P q (transport P p u) ≡ transport P (p ∙ q) u
lemma-2-3-9 {a} {b} {A} {x} {y} {z} P p q u = J A D d x y p P z q u
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set _
    D x y p = (P : A → Set b) (z : A) (q : y ≡ z) (u : P x)
      → transport P q (transport P p u) ≡ transport P (p ∙ q) u

    -- base case
    d : (x : A) → D x x refl
    d x P z q u = J A E e x z q P u
      where
        -- the predicate
        E : (x z : A) (q : x ≡ z) → Set _
        E x z q = (P : A → Set b) (u : P x)
          → transport P q (transport P refl u) ≡ transport P (refl ∙ q) u

        -- base case
        e : (x : A) → E x x refl
        e x P u = refl

-- Lemma 2.3.10
lemma-2-3-10 : ∀ {a b c} {A : Set a} {B : Set b} {x y : A}
  → (P : B → Set c)
  → (f : A → B)
  → (p : x ≡ y)
  → (u : P (f x))
  → transport (P ∘ f) p u ≡ transport P (ap f p) u
lemma-2-3-10 {a} {b} {c} {A} {B} {x} {y} P f p u = J A D d x y p P f u
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set _
    D x y p = (P : B → Set c) (f : A → B) (u : P (f x))
      → transport (P ∘ f) p u ≡ transport P (ap f p) u

    -- base case
    d : (x : A) → D x x refl
    d x P f u = refl

-- Lemma 2.3.11
lemma-2-3-11 : {a b c : Level} {A : Set a} {x y : A}
  → (P : A → Set b) (Q : A → Set c)
  → (f : (z : A) → P z → Q z)
  → (p : x ≡ y)
  → (u : P x)
  → transport Q p (f x u) ≡ f y (transport P p u)
lemma-2-3-11 {a} {b} {c} {A} {x} {y} P Q f p u = J A D d x y p P Q f u
  -- J A D d x y p {!   !} {!   !} {!   !} {!   !}
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set _
    D x y p = (P : A → Set b) (Q : A → Set c) (f : (z : A) → P z → Q z) (u : P x)
      → transport Q p (f x u) ≡ f y (transport P p u)

    -- base case
    d : (x : A) → D x x refl
    d x P Q f u = refl

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


text:
module Rationals.Multiply.Comm where

open import Equality
open import Rationals
open import Nats.Multiply.Comm

------------------------------------------------------------------------
-- internal stuffs

private

  a*b=b*a : ∀ x y → x * y ≡ y * x
  a*b=b*a (a ÷ c) (b ÷ d)
    rewrite nat-multiply-comm a b
          | nat-multiply-comm c d
            = refl

------------------------------------------------------------------------
-- public aliases

rational-multiply-comm : ∀ x y → x * y ≡ y * x
rational-multiply-comm = a*b=b*a


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open Struct struct
open import MLib.Algebra.Operations struct

open Table using (head; tail; rearrange; fromList; toList; _≗_)

open import MLib.Matrix.Core public
open import MLib.Matrix.Equality struct public
open import MLib.Matrix.Plus struct public
open import MLib.Matrix.Mul struct public
open import MLib.Matrix.Tensor struct public
open import MLib.Matrix.SemiTensor struct public
open FunctionProperties


text:
-- This file serves to aggregate all the top-level dependencies in the Silica project.

open import preservation
open import progress

max_stars_repo_name: ivoysey/Obsidian

max_issues_repo_name: ivoysey/Obsidian

max_forks_repo_name: ivoysey/Obsidian


text:
{-# OPTIONS --without-K --exact-split #-}

module 07-equivalences where

import 06-universes
open 06-universes public

-- Section 7.1 Homotopies

-- Definition 7.1.1

_~_ :
  {i j : Level} {A : UU i} {B : A → UU j} (f g : (x : A) → B x) → UU (i ⊔ j)
f ~ g = (x : _) → Id (f x) (g x)

-- Definition 7.1.2

refl-htpy :
  {i j : Level} {A : UU i} {B : A → UU j} {f : (x : A) → B x} → f ~ f
refl-htpy x = refl

{- Most of the time we get by with refl-htpy. However, sometimes Agda wants us
   to specify the implicit argument. The it is easier to call refl-htpy' than
   to use Agda's {f = ?} notation. -}

refl-htpy' :
  {i j : Level} {A : UU i} {B : A → UU j} (f : (x : A) → B x) → f ~ f
refl-htpy' f = refl-htpy

htpy-inv :
  {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x} →
  (f ~ g) → (g ~ f)
htpy-inv H x = inv (H x)

_∙h_ :
  {i j : Level} {A : UU i} {B : A → UU j} {f g h : (x : A) → B x} →
  (f ~ g) → (g ~ h) → (f ~ h)
_∙h_ H K x = (H x) ∙ (K x)

htpy-concat :
  {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x} →
  (f ~ g) → (h : (x : A) → B x) → (g ~ h) → (f ~ h)
htpy-concat H h K x = concat (H x) (h x) (K x)

htpy-concat' :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  (f : (x : A) → B x) {g h : (x : A) → B x} →
  (g ~ h) → (f ~ g) → (f ~ h)
htpy-concat' f K H = H ∙h K

htpy-assoc :
  {i j : Level} {A : UU i} {B : A → UU j} {f g h k : (x : A) → B x} →
  (H : f ~ g) → (K : g ~ h) → (L : h ~ k) →
  ((H ∙h K) ∙h L) ~ (H ∙h (K ∙h L))
htpy-assoc H K L x = assoc (H x) (K x) (L x)

htpy-left-unit :
  {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x}
  {H : f ~ g} → (refl-htpy ∙h H) ~ H
htpy-left-unit x = left-unit

htpy-right-unit :
  {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x}
  {H : f ~ g} → (H ∙h refl-htpy) ~ H
htpy-right-unit x = right-unit

htpy-left-inv :
  {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x}
  (H : f ~ g) → ((htpy-inv H) ∙h H) ~ refl-htpy
htpy-left-inv H x = left-inv (H x)

htpy-right-inv :
  {i j : Level} {A : UU i} {B : A → UU j} {f g : (x : A) → B x}
  (H : f ~ g) → (H ∙h (htpy-inv H)) ~ refl-htpy
htpy-right-inv H x = right-inv (H x)

-- Definition 7.1.3

htpy-left-whisk :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k}
  (h : B → C) {f g : A → B} → (f ~ g) → ((h ∘ f) ~ (h ∘ g))
htpy-left-whisk h H x = ap h (H x)

_·l_ = htpy-left-whisk

htpy-right-whisk :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k}
  {g h : B → C} (H : g ~ h) (f : A → B) → ((g ∘ f) ~ (h ∘ f))
htpy-right-whisk H f x = H (f x)

_·r_ = htpy-right-whisk

-- Section 7.2 Bi-invertible maps

-- Definition 7.2.1

sec :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
sec {i} {j} {A} {B} f = Σ (B → A) (λ g → (f ∘ g) ~ id)

retr :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
retr {i} {j} {A} {B} f = Σ (B → A) (λ g → (g ∘ f) ~ id)

_retract-of_ :
  {i j : Level} → UU i → UU j → UU (i ⊔ j)
A retract-of B = Σ (A → B) retr

section-retract-of :
  {i j : Level} {A : UU i} {B : UU j} → A retract-of B → A → B
section-retract-of = pr1

retr-section-retract-of :
  {i j : Level} {A : UU i} {B : UU j} (R : A retract-of B) →
  retr (section-retract-of R)
retr-section-retract-of = pr2

retraction-retract-of :
  {i j : Level} {A : UU i} {B : UU j} → (A retract-of B) → B → A
retraction-retract-of R = pr1 (retr-section-retract-of R)

is-retr-retraction-retract-of :
  {i j : Level} {A : UU i} {B : UU j} (R : A retract-of B) →
  ((retraction-retract-of R) ∘ (section-retract-of R)) ~ id
is-retr-retraction-retract-of R = pr2 (retr-section-retract-of R)

is-equiv :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
is-equiv f = sec f × retr f

_≃_ :
  {i j : Level} (A : UU i) (B : UU j) → UU (i ⊔ j)
A ≃ B = Σ (A → B) (λ f → is-equiv f)

map-equiv :
  {i j : Level} {A : UU i} {B : UU j} → (A ≃ B) → (A → B)
map-equiv e = pr1 e

is-equiv-map-equiv :
  {i j : Level} {A : UU i} {B : UU j} (e : A ≃ B) → is-equiv (map-equiv e)
is-equiv-map-equiv e = pr2 e

-- Remark 7.2.2

has-inverse :
  {i j : Level} {A : UU i} {B : UU j} (f : A → B) → UU (i ⊔ j)
has-inverse {i} {j} {A} {B} f =
  Σ (B → A) (λ g → ((f ∘ g) ~ id) × ((g ∘ f) ~ id))

is-equiv-has-inverse' :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  has-inverse f → is-equiv f
is-equiv-has-inverse' (pair g (pair H K)) = pair (pair g H) (pair g K)

is-equiv-has-inverse :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  (g : B → A) (H : (f ∘ g) ~ id) (K : (g ∘ f) ~ id) → is-equiv f
is-equiv-has-inverse g H K =
  is-equiv-has-inverse' (pair g (pair H K))

-- Lemma 7.2.3

{- We now show that if f is an equivalence, then it has an inverse. -}

htpy-section-retraction :
  { i j : Level} {A : UU i} {B : UU j} {f : A → B}
  ( is-equiv-f : is-equiv f) →
  ( (pr1 (pr1 is-equiv-f))) ~ (pr1 (pr2 is-equiv-f))
htpy-section-retraction {i} {j} {A} {B} {f} (pair (pair g G) (pair h H)) =
    (htpy-inv (H ·r g)) ∙h (h ·l G)

has-inverse-is-equiv :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  is-equiv f → has-inverse f
has-inverse-is-equiv {i} {j} {A} {B} {f} (pair (pair g G) (pair h H)) =
  let is-equiv-f = pair (pair g G) (pair h H) in
  pair g (pair G (((htpy-section-retraction is-equiv-f) ·r f) ∙h H))

-- Corollary 7.2.4

inv-is-equiv :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} → is-equiv f → B → A
inv-is-equiv is-equiv-f = pr1 (has-inverse-is-equiv is-equiv-f)

issec-inv-is-equiv :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  (is-equiv-f : is-equiv f) → (f ∘ (inv-is-equiv is-equiv-f)) ~ id
issec-inv-is-equiv is-equiv-f = pr1 (pr2 (has-inverse-is-equiv is-equiv-f))

isretr-inv-is-equiv :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  (is-equiv-f : is-equiv f) → ((inv-is-equiv is-equiv-f) ∘ f) ~ id
isretr-inv-is-equiv is-equiv-f = pr2 (pr2 (has-inverse-is-equiv is-equiv-f))

is-equiv-inv-is-equiv :
  {i j : Level} {A : UU i} {B : UU j} {f : A → B} →
  (is-equiv-f : is-equiv f) → is-equiv (inv-is-equiv is-equiv-f)
is-equiv-inv-is-equiv {i} {j} {A} {B} {f} is-equiv-f =
  is-equiv-has-inverse f
    ( isretr-inv-is-equiv is-equiv-f)
    ( issec-inv-is-equiv is-equiv-f)

inv-map-equiv :
  {i j : Level} {A : UU i} {B : UU j} → (A ≃ B) → (B → A)
inv-map-equiv e = inv-is-equiv (is-equiv-map-equiv e)

is-equiv-inv-map-equiv :
  {i j : Level} {A : UU i} {B : UU j} (e : A ≃ B) → is-equiv (inv-map-equiv e)
is-equiv-inv-map-equiv e =
  is-equiv-inv-is-equiv (is-equiv-map-equiv e)

inv-equiv :
  {i j : Level} {A : UU i} {B : UU j} → (A ≃ B) → (B ≃ A)
inv-equiv e = pair (inv-map-equiv e) (is-equiv-inv-map-equiv e)

-- Remark 7.2.5

is-equiv-id :
  {i : Level} (A : UU i) → is-equiv (id {i} {A})
is-equiv-id A = pair (pair id refl-htpy) (pair id refl-htpy)

equiv-id :
  {i : Level} (A : UU i) → A ≃ A
equiv-id A = pair id (is-equiv-id A)

-- Example 7.2.6

inv-Π-swap :
  {i j k : Level} {A : UU i} {B : UU j} (C : A → B → UU k) →
  ((y : B) (x : A) → C x y) → ((x : A) (y : B) → C x y)
inv-Π-swap C g x y = g y x

abstract
  is-equiv-Π-swap :
    {i j k : Level} {A : UU i} {B : UU j} (C : A → B → UU k) →
    is-equiv (Π-swap {i} {j} {k} {A} {B} {C})
  is-equiv-Π-swap C =
    is-equiv-has-inverse
      ( inv-Π-swap C)
      ( refl-htpy)
      ( refl-htpy)

-- Section 7.3 The identity type of a Σ-type

-- Definition 7.3.1

Eq-Σ :
  {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) → UU (i ⊔ j)
Eq-Σ {B = B} s t = Σ (Id (pr1 s) (pr1 t)) (λ α → Id (tr B α (pr2 s)) (pr2 t))

-- Lemma 7.3.2

reflexive-Eq-Σ :
  {i j : Level} {A : UU i} {B : A → UU j} (s : Σ A B) → Eq-Σ s s
reflexive-Eq-Σ (pair a b) = pair refl refl

-- Definition 7.3.3

pair-eq :
  {i j : Level} {A : UU i} {B : A → UU j} {s t : Σ A B} →
  (Id s t) → Eq-Σ s t
pair-eq {s = s} refl = reflexive-Eq-Σ s

-- Theorem 7.3.4

eq-pair :
  {i j : Level} {A : UU i} {B : A → UU j} {s t : Σ A B} →
  (α : Id (pr1 s) (pr1 t)) → Id (tr B α (pr2 s)) (pr2 t) → Id s t
eq-pair {B = B} {pair x y} {pair .x .y} refl refl = refl

eq-pair' :
  {i j : Level} {A : UU i} {B : A → UU j} {s t : Σ A B} →
  Eq-Σ s t → Id s t
eq-pair' (pair α β) = eq-pair α β

isretr-pair-eq :
  {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) →
  ((pair-eq {s = s} {t}) ∘ (eq-pair' {s = s} {t})) ~ id {A = Eq-Σ s t}
isretr-pair-eq (pair x y) (pair .x .y) (pair refl refl) = refl

issec-pair-eq :
  {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) →
  ((eq-pair' {s = s} {t}) ∘ (pair-eq {s = s} {t})) ~ id
issec-pair-eq (pair x y) .(pair x y) refl = refl

abstract
  is-equiv-eq-pair :
    {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) →
    is-equiv (eq-pair' {s = s} {t})
  is-equiv-eq-pair s t =
    is-equiv-has-inverse
      ( pair-eq)
      ( issec-pair-eq s t)
      ( isretr-pair-eq s t)

abstract
  is-equiv-pair-eq :
    {i j : Level} {A : UU i} {B : A → UU j} (s t : Σ A B) →
    is-equiv (pair-eq {s = s} {t})
  is-equiv-pair-eq s t =
    is-equiv-has-inverse
      ( eq-pair')
      ( isretr-pair-eq s t)
      ( issec-pair-eq s t)

η-pair :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (t : Σ A B) →
  Id (pair (pr1 t) (pr2 t)) t
η-pair t = eq-pair refl refl

{- For our convenience, we repeat the above argument for cartesian products. -}

Eq-prod :
  {i j : Level} {A : UU i} {B : UU j} (s t : A × B) → UU (i ⊔ j)
Eq-prod s t = (Id (pr1 s) (pr1 t)) × (Id (pr2 s) (pr2 t))

{- We also define a function eq-pair-triv, which is like eq-pair but simplified
   for the case where B is just a type. -}

eq-pair-triv' :
  {i j : Level} {A : UU i} {B : UU j} (s t : prod A B) →
  Eq-prod s t → Id s t
eq-pair-triv' (pair x y) (pair .x .y) (pair refl refl) = refl

eq-pair-triv :
  {i j : Level} {A : UU i} {B : UU j} {s t : prod A B} →
  Eq-prod s t → Id s t
eq-pair-triv {s = s} {t} = eq-pair-triv' s t

{- Ideally, we would use the 3-for-2 property of equivalences to show that
   eq-pair-triv is an equivalence, using that eq-pair is an equivalence.
   Indeed, there is an equivalence

     (Id x x') × (Id y y') → Σ (Id x x') (λ p → Id (tr (λ x → B) p y) y').

   However, to show that this map is an equivalence we either give a direct
   proof (in which case we might as well have given a direct proof that
   eq-pair-triv is an equivalence), or we use the fact that it is the induced
   map on total spaces of a fiberwise equivalence (the topic of Lecture 8).
   Thus it seems that a direct proof showing that eq-pair-triv is an
   equivalence is quickest for now. -}

pair-eq-triv' :
  {i j : Level} {A : UU i} {B : UU j} (s t : prod A B) →
  Id s t → Eq-prod s t
pair-eq-triv' s t α = pair (ap pr1 α) (ap pr2 α)

isretr-pair-eq-triv' :
  {i j : Level} {A : UU i} {B : UU j} (s t : prod A B) →
  ((pair-eq-triv' s t) ∘ (eq-pair-triv' s t)) ~ id
isretr-pair-eq-triv' (pair x y) (pair .x .y) (pair refl refl) = refl

issec-pair-eq-triv' :
  {i j : Level} {A : UU i} {B : UU j} (s t : prod A B) →
  ((eq-pair-triv' s t) ∘ (pair-eq-triv' s t)) ~ id
issec-pair-eq-triv' (pair x y) (pair .x .y) refl = refl

abstract
  is-equiv-eq-pair-triv' :
    {i j : Level} {A : UU i} {B : UU j} (s t : prod A B) →
    is-equiv (eq-pair-triv' s t)
  is-equiv-eq-pair-triv' s t =
    is-equiv-has-inverse
      ( pair-eq-triv' s t)
      ( issec-pair-eq-triv' s t)
      ( isretr-pair-eq-triv' s t)

-- Exercises

-- Exercise 7.1

{- We show that inv is an equivalence. -}

inv-inv :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) → Id (inv (inv p)) p
inv-inv refl = refl

abstract
  is-equiv-inv :
    {i : Level} {A : UU i} (x y : A) →
    is-equiv (λ (p : Id x y) → inv p)
  is-equiv-inv x y =
    is-equiv-has-inverse inv inv-inv inv-inv

equiv-inv :
  {i : Level} {A : UU i} (x y : A) → (Id x y) ≃ (Id y x)
equiv-inv x y = pair inv (is-equiv-inv x y)

{- We show that concat p is an equivalence, for any path p. -}

inv-concat :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) (z : A) →
  (Id x z) → (Id y z)
inv-concat p = concat (inv p)

isretr-inv-concat :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) (z : A) →
  ((inv-concat p z) ∘ (concat p z)) ~ id
isretr-inv-concat refl z q = refl

issec-inv-concat :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) (z : A) →
  ((concat p z) ∘ (inv-concat p z)) ~ id
issec-inv-concat refl z refl = refl

abstract
  is-equiv-concat :
    {i : Level} {A : UU i} {x y : A} (p : Id x y) (z : A) →
    is-equiv (concat p z)
  is-equiv-concat p z =
    is-equiv-has-inverse
      ( inv-concat p z)
      ( issec-inv-concat p z)
      ( isretr-inv-concat p z)

equiv-concat :
  {i : Level} {A : UU i} {x y : A} (p : Id x y) (z : A) →
  Id y z ≃ Id x z
equiv-concat p z = pair (concat p z) (is-equiv-concat p z)

{- We show that concat' q is an equivalence, for any path q. -}

concat' :
  {i : Level} {A : UU i} (x : A) {y z : A} → Id y z → Id x y → Id x z
concat' x q p = p ∙ q

inv-concat' :
  {i : Level} {A : UU i} (x : A) {y z : A} → Id y z →
  Id x z → Id x y
inv-concat' x q = concat' x (inv q)

isretr-inv-concat' :
  {i : Level} {A : UU i} (x : A) {y z : A} (q : Id y z) →
  ((inv-concat' x q) ∘ (concat' x q)) ~ id
isretr-inv-concat' x refl refl = refl

issec-inv-concat' :
  {i : Level} {A : UU i} (x : A) {y z : A} (q : Id y z) →
  ((concat' x q) ∘ (inv-concat' x q)) ~ id
issec-inv-concat' x refl refl = refl

abstract
  is-equiv-concat' :
    {i : Level} {A : UU i} (x : A) {y z : A} (q : Id y z) →
    is-equiv (concat' x q)
  is-equiv-concat' x q =
    is-equiv-has-inverse
      ( inv-concat' x q)
      ( issec-inv-concat' x q)
      ( isretr-inv-concat' x q)

equiv-concat' :
  {i : Level} {A : UU i} (x : A) {y z : A} (q : Id y z) →
  Id x y ≃ Id x z
equiv-concat' x q = pair (concat' x q) (is-equiv-concat' x q)

{- We show that tr B p is an equivalence, for an path p and any type family B.
   -}

inv-tr :
  {i j : Level} {A : UU i} (B : A → UU j) {x y : A} →
  Id x y → B y → B x
inv-tr B p = tr B (inv p)

isretr-inv-tr :
  {i j : Level} {A : UU i} (B : A → UU j) {x y : A}
  (p : Id x y) → ((inv-tr B p ) ∘ (tr B p)) ~ id
isretr-inv-tr B refl b = refl

issec-inv-tr :
  {i j : Level} {A : UU i} (B : A → UU j) {x y : A}
  (p : Id x y) → ((tr B p) ∘ (inv-tr B p)) ~ id
issec-inv-tr B refl b = refl

abstract
  is-equiv-tr :
    {i j : Level} {A : UU i} (B : A → UU j) {x y : A}
    (p : Id x y) → is-equiv (tr B p)
  is-equiv-tr B p =
    is-equiv-has-inverse
      ( inv-tr B p)
      ( issec-inv-tr B p)
      ( isretr-inv-tr B p)

equiv-tr :
  {i j : Level} {A : UU i} (B : A → UU j) {x y : A}
  (p : Id x y) → (B x) ≃ (B y)
equiv-tr B p = pair (tr B p) (is-equiv-tr B p)

-- Exercise 7.2

{- We prove the left unit law for coproducts. -}

inv-inr-coprod-empty :
  {l : Level} (X : UU l) → coprod empty X → X
inv-inr-coprod-empty X (inr x) = x

issec-inv-inr-coprod-empty :
  {l : Level} (X : UU l) → (inr ∘ (inv-inr-coprod-empty X)) ~ id
issec-inv-inr-coprod-empty X (inr x) = refl

isretr-inv-inr-coprod-empty :
  {l : Level} (X : UU l) → ((inv-inr-coprod-empty X) ∘ inr) ~ id
isretr-inv-inr-coprod-empty X x = refl

is-equiv-inr-coprod-empty :
  {l : Level} (X : UU l) → is-equiv (inr {A = empty} {B = X})
is-equiv-inr-coprod-empty X =
  is-equiv-has-inverse
    ( inv-inr-coprod-empty X)
    ( issec-inv-inr-coprod-empty X)
    ( isretr-inv-inr-coprod-empty X)

left-unit-law-coprod :
  {l : Level} (X : UU l) → X ≃ (coprod empty X)
left-unit-law-coprod X = pair inr (is-equiv-inr-coprod-empty X)

{- We prove the right unit law for coproducts. -}

inv-inl-coprod-empty :
  {l : Level} (X : UU l) → (coprod X empty) → X
inv-inl-coprod-empty X (inl x) = x

issec-inv-inl-coprod-empty :
  {l : Level} (X : UU l) → (inl ∘ (inv-inl-coprod-empty X)) ~ id
issec-inv-inl-coprod-empty X (inl x) = refl

isretr-inv-inl-coprod-empty :
  {l : Level} (X : UU l) → ((inv-inl-coprod-empty X) ∘ inl) ~ id
isretr-inv-inl-coprod-empty X x = refl

is-equiv-inl-coprod-empty :
  {l : Level} (X : UU l) → is-equiv (inl {A = X} {B = empty})
is-equiv-inl-coprod-empty X =
  is-equiv-has-inverse
    ( inv-inl-coprod-empty X)
    ( issec-inv-inl-coprod-empty X)
    ( isretr-inv-inl-coprod-empty X)

right-unit-law-coprod :
  {l : Level} (X : UU l) → X ≃ (coprod X empty)
right-unit-law-coprod X =
  pair inl (is-equiv-inl-coprod-empty X)

{- We prove a left zero law for cartesian products. -}

inv-pr1-prod-empty :
  {l : Level} (X : UU l) → empty → empty × X
inv-pr1-prod-empty X ()

issec-inv-pr1-prod-empty :
  {l : Level} (X : UU l) → (pr1 ∘ (inv-pr1-prod-empty X)) ~ id
issec-inv-pr1-prod-empty X ()

isretr-inv-pr1-prod-empty :
  {l : Level} (X : UU l) → ((inv-pr1-prod-empty X) ∘ pr1) ~ id
isretr-inv-pr1-prod-empty X (pair () x)

is-equiv-pr1-prod-empty :
  {l : Level} (X : UU l) → is-equiv (pr1 {A = empty} {B = λ t → X})
is-equiv-pr1-prod-empty X =
  is-equiv-has-inverse
    ( inv-pr1-prod-empty X)
    ( issec-inv-pr1-prod-empty X)
    ( isretr-inv-pr1-prod-empty X)

left-zero-law-prod :
  {l : Level} (X : UU l) → (empty × X) ≃ empty
left-zero-law-prod X =
  pair pr1 (is-equiv-pr1-prod-empty X)

{- We prove the right zero law for cartesian products. -}

inv-pr2-prod-empty :
  {l : Level} (X : UU l) → empty → (X × empty)
inv-pr2-prod-empty X ()

issec-inv-pr2-prod-empty :
  {l : Level} (X : UU l) → (pr2 ∘ (inv-pr2-prod-empty X)) ~ id
issec-inv-pr2-prod-empty X ()

isretr-inv-pr2-prod-empty :
  {l : Level} (X : UU l) → ((inv-pr2-prod-empty X) ∘ pr2) ~ id
isretr-inv-pr2-prod-empty X (pair x ())

is-equiv-pr2-prod-empty :
  {l : Level} (X : UU l) → is-equiv (pr2 {A = X} {B = λ x → empty})
is-equiv-pr2-prod-empty X =
  is-equiv-has-inverse
    ( inv-pr2-prod-empty X)
    ( issec-inv-pr2-prod-empty X)
    ( isretr-inv-pr2-prod-empty X)

right-zero-law-prod :
  {l : Level} (X : UU l) → (X × empty) ≃ empty
right-zero-law-prod X =
  pair pr2 (is-equiv-pr2-prod-empty X)

-- Exercise 7.3

-- Exercise 7.3(a)

abstract
  is-equiv-htpy :
    {i j : Level} {A : UU i} {B : UU j} {f : A → B} (g : A → B) →
    f ~ g → is-equiv g → is-equiv f
  is-equiv-htpy g H (pair (pair gs issec) (pair gr isretr)) =
    pair
      ( pair gs ((H ·r gs) ∙h issec))
      ( pair gr ((gr ·l H) ∙h isretr))

abstract
  is-equiv-htpy' :
    {i j : Level} {A : UU i} {B : UU j} (f : A → B) {g : A → B} →
    f ~ g → is-equiv f → is-equiv g
  is-equiv-htpy' f H = is-equiv-htpy f (htpy-inv H)

-- Exercise 7.3(b)

htpy-inv-is-equiv :
  {i j : Level} {A : UU i} {B : UU j} {f f' : A → B} (H : f ~ f') →
  (is-equiv-f : is-equiv f) (is-equiv-f' : is-equiv f') →
  (inv-is-equiv is-equiv-f) ~ (inv-is-equiv is-equiv-f')
htpy-inv-is-equiv H is-equiv-f is-equiv-f' b =
  ( inv (isretr-inv-is-equiv is-equiv-f' (inv-is-equiv is-equiv-f b))) ∙
  ( ap (inv-is-equiv is-equiv-f')
    ( ( inv (H (inv-is-equiv is-equiv-f b))) ∙
      ( issec-inv-is-equiv is-equiv-f b)))

-- Exercise 7.4

-- Exercise 7.4(a)

{- Exercise 7.4 (a) asks to show that, given a commuting triangle f ~ g ∘ h and
   a section s of h, we get a new commuting triangle g ~ f ∘ s. Moreover, under
   the same assumptions it follows that f has a section if and only if g has a
   section. -}

triangle-section :
  {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) (S : sec h) →
  g ~ (f ∘ (pr1 S))
triangle-section f g h H (pair s issec) =
  htpy-inv (( H ·r s) ∙h (g ·l issec))

section-comp :
  {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
  sec h → sec f → sec g
section-comp f g h H sec-h sec-f =
  pair (h ∘ (pr1 sec-f)) ((htpy-inv (H ·r (pr1 sec-f))) ∙h (pr2 sec-f))

section-comp' :
  {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
  sec h → sec g → sec f
section-comp' f g h H sec-h sec-g =
  pair
    ( (pr1 sec-h) ∘ (pr1 sec-g))
    ( ( H ·r ((pr1 sec-h) ∘ (pr1 sec-g))) ∙h
      ( ( g ·l ((pr2 sec-h) ·r (pr1 sec-g))) ∙h ((pr2 sec-g))))

-- Exercise 7.4(b)

{- Exercise 7.4 (b) is dual to exercise 5.5 (a). It asks to show that, given a
   commuting triangle f ~ g ∘ h and a retraction r of g, we get a new commuting
   triangle h ~ r ∘ f. Moreover, under these assumptions it also follows that f
   has a retraction if and only if h has a retraction. -}

triangle-retraction :
  {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) (R : retr g) →
  h ~ ((pr1 R) ∘ f)
triangle-retraction f g h H (pair r isretr) =
  htpy-inv (( r ·l H) ∙h (isretr ·r h))

retraction-comp :
  {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
  retr g → retr f → retr h
retraction-comp f g h H retr-g retr-f =
  pair
    ( (pr1 retr-f) ∘ g)
    ( (htpy-inv ((pr1 retr-f) ·l H)) ∙h (pr2 retr-f))

retraction-comp' :
  {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
  (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
  retr g → retr h → retr f
retraction-comp' f g h H retr-g retr-h =
  pair
    ( (pr1 retr-h) ∘ (pr1 retr-g))
    ( ( ((pr1 retr-h) ∘ (pr1 retr-g)) ·l H) ∙h
      ( ((pr1 retr-h) ·l ((pr2 retr-g) ·r h)) ∙h (pr2 retr-h)))

-- Exercise 7.4(c)

{- In Exercise 7.4 (c) we use the constructions of parts (a) and (b) to derive
   the 3-for-2 property of equivalences. -}

abstract
  is-equiv-comp :
    {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
    (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
    is-equiv h → is-equiv g → is-equiv f
  is-equiv-comp f g h H (pair sec-h retr-h) (pair sec-g retr-g) =
    pair
      ( section-comp' f g h H sec-h sec-g)
      ( retraction-comp' f g h H retr-g retr-h)

abstract
  is-equiv-comp' :
    {i j k : Level} {A : UU i} {B : UU j} {X : UU k} (g : B → X) (h : A → B) →
    is-equiv h → is-equiv g → is-equiv (g ∘ h)
  is-equiv-comp' g h = is-equiv-comp (g ∘ h) g h refl-htpy

equiv-comp :
  {i j k : Level} {A : UU i} {B : UU j} {X : UU k} →
  (B ≃ X) → (A ≃ B) → (A ≃ X)
equiv-comp g h =
  pair ((pr1 g) ∘ (pr1 h)) (is-equiv-comp' (pr1 g) (pr1 h) (pr2 h) (pr2 g))

_∘e_ :
  {i j k : Level} {A : UU i} {B : UU j} {X : UU k} →
  (B ≃ X) → (A ≃ B) → (A ≃ X)
_∘e_ = equiv-comp

abstract
  is-equiv-left-factor :
    {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
    (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
    is-equiv f → is-equiv h → is-equiv g
  is-equiv-left-factor f g h H
    ( pair sec-f retr-f)
    ( pair (pair sh sh-issec) retr-h) =
    pair
      ( section-comp f g h H (pair sh sh-issec) sec-f)
      ( retraction-comp' g f sh
        ( triangle-section f g h H (pair sh sh-issec))
        ( retr-f)
        ( pair h sh-issec))

abstract
  is-equiv-left-factor' :
    {i j k : Level} {A : UU i} {B : UU j} {X : UU k} (g : B → X) (h : A → B) →
    is-equiv (g ∘ h) → is-equiv h → is-equiv g
  is-equiv-left-factor' g h =
    is-equiv-left-factor (g ∘ h) g h refl-htpy

abstract
  is-equiv-right-factor :
    {i j k : Level} {A : UU i} {B : UU j} {X : UU k}
    (f : A → X) (g : B → X) (h : A → B) (H : f ~ (g ∘ h)) →
    is-equiv g → is-equiv f → is-equiv h
  is-equiv-right-factor f g h H
    ( pair sec-g (pair rg rg-isretr))
    ( pair sec-f retr-f) =
    pair
      ( section-comp' h rg f
        ( triangle-retraction f g h H (pair rg rg-isretr))
        ( sec-f)
        ( pair g rg-isretr))
      ( retraction-comp f g h H (pair rg rg-isretr) retr-f)

abstract
  is-equiv-right-factor' :
    {i j k : Level} {A : UU i} {B : UU j} {X : UU k} (g : B → X) (h : A → B) →
    is-equiv g → is-equiv (g ∘ h) → is-equiv h
  is-equiv-right-factor' g h =
    is-equiv-right-factor (g ∘ h) g h refl-htpy

-- Exercise 7.5

-- Exercise 7.5(a)

{- In this exercise we show that the negation function on the booleans is an
   equivalence. Moreover, we show that any constant function on the booleans is
   not an equivalence. -}

neg-neg-𝟚 : (neg-𝟚 ∘ neg-𝟚) ~ id
neg-neg-𝟚 true = refl
neg-neg-𝟚 false = refl

abstract
  is-equiv-neg-𝟚 : is-equiv neg-𝟚
  is-equiv-neg-𝟚 = is-equiv-has-inverse neg-𝟚 neg-neg-𝟚 neg-neg-𝟚

equiv-neg-𝟚 : bool ≃ bool
equiv-neg-𝟚 = pair neg-𝟚 is-equiv-neg-𝟚

-- Exercise 7.5(b)

abstract
  not-true-is-false : ¬ (Id true false)
  not-true-is-false p =
    tr (Eq-𝟚 true) p (reflexive-Eq-𝟚 true)

-- Exercise 7.5(c)

abstract
  not-equiv-const :
    (b : bool) → ¬ (is-equiv (const bool bool b))
  not-equiv-const true (pair (pair s issec) (pair r isretr)) =
    not-true-is-false (issec false)
  not-equiv-const false (pair (pair s issec) (pair r isretr)) =
    not-true-is-false (inv (issec true))

-- Exercise 7.6

  is-equiv-succ-ℤ : is-equiv succ-ℤ
  is-equiv-succ-ℤ =
    is-equiv-has-inverse pred-ℤ right-inverse-pred-ℤ left-inverse-pred-ℤ

equiv-succ-ℤ : ℤ ≃ ℤ
equiv-succ-ℤ = pair succ-ℤ is-equiv-succ-ℤ

-- Exercise 7.7

{- In this exercise we construct an equivalence from A + B to B + A, showing
   that the coproduct is commutative. -}

swap-coprod :
  {i j : Level} (A : UU i) (B : UU j) → coprod A B → coprod B A
swap-coprod A B (inl x) = inr x
swap-coprod A B (inr x) = inl x

swap-swap-coprod :
  {i j : Level} (A : UU i) (B : UU j) →
  ((swap-coprod B A) ∘ (swap-coprod A B)) ~ id
swap-swap-coprod A B (inl x) = refl
swap-swap-coprod A B (inr x) = refl

abstract
  is-equiv-swap-coprod :
    {i j : Level} (A : UU i) (B : UU j) → is-equiv (swap-coprod A B)
  is-equiv-swap-coprod A B =
    is-equiv-has-inverse
      ( swap-coprod B A)
      ( swap-swap-coprod B A)
      ( swap-swap-coprod A B)

equiv-swap-coprod :
  {i j : Level} (A : UU i) (B : UU j) → coprod A B ≃ coprod B A
equiv-swap-coprod A B = pair (swap-coprod A B) (is-equiv-swap-coprod A B)

swap-prod :
  {i j : Level} (A : UU i) (B : UU j) → prod A B → prod B A
swap-prod A B t = pair (pr2 t) (pr1 t)

swap-swap-prod :
  {i j : Level} (A : UU i) (B : UU j) →
  ((swap-prod B A) ∘ (swap-prod A B)) ~ id
swap-swap-prod A B (pair x y) = refl

abstract
  is-equiv-swap-prod :
    {i j : Level} (A : UU i) (B : UU j) →
    is-equiv (swap-prod A B)
  is-equiv-swap-prod A B =
    is-equiv-has-inverse
      ( swap-prod B A)
      ( swap-swap-prod B A)
      ( swap-swap-prod A B)

equiv-swap-prod :
  {i j : Level} (A : UU i) (B : UU j) → (A × B) ≃ (B × A)
equiv-swap-prod A B = pair (swap-prod A B) (is-equiv-swap-prod A B)

-- Exercise 7.8

{- In this exercise we show that if A is a retract of B, then so are its
   identity types. -}

ap-retraction :
  {i j : Level} {A : UU i} {B : UU j}
  (i : A → B) (r : B → A) (H : (r ∘ i) ~ id)
  (x y : A) → Id (i x) (i y) → Id x y
ap-retraction i r H x y p =
    ( inv (H x)) ∙ ((ap r p) ∙ (H y))

isretr-ap-retraction :
  {i j : Level} {A : UU i} {B : UU j}
  (i : A → B) (r : B → A) (H : (r ∘ i) ~ id)
  (x y : A) → ((ap-retraction i r H x y) ∘ (ap i {x} {y})) ~ id
isretr-ap-retraction i r H x .x refl = left-inv (H x)

retr-ap :
  {i j : Level} {A : UU i} {B : UU j} (i : A → B) →
  retr i → (x y : A) → retr (ap i {x} {y})
retr-ap i (pair r H) x y =
  pair (ap-retraction i r H x y) (isretr-ap-retraction i r H x y)

Id-retract-of-Id :
  {i j : Level} {A : UU i} {B : UU j} (R : A retract-of B) →
  (x y : A) → (Id x y) retract-of (Id (pr1 R x) (pr1 R y))
Id-retract-of-Id (pair i (pair r H)) x y =
  pair
    ( ap i {x} {y})
    ( retr-ap i (pair r H) x y)

-- Exercise 7.9

Σ-assoc :
  {i j k : Level} (A : UU i) (B : A → UU j) (C : (Σ A B) → UU k) →
  Σ (Σ A B) C → Σ A (λ x → Σ (B x) (λ y → C (pair x y)))
Σ-assoc A B C (pair (pair x y) z) = pair x (pair y z)

Σ-assoc' :
  {i j k : Level} (A : UU i) (B : A → UU j) (C : (Σ A B) → UU k) →
  Σ A (λ x → Σ (B x) (λ y → C (pair x y))) → Σ (Σ A B) C
Σ-assoc' A B C t = pair (pair (pr1 t) (pr1 (pr2 t))) (pr2 (pr2 t))

Σ-assoc-assoc :
  {i j k : Level} (A : UU i) (B : A → UU j)
  (C : (Σ A B) → UU k) → ((Σ-assoc' A B C) ∘ (Σ-assoc A B C)) ~ id
Σ-assoc-assoc A B C (pair (pair x y) z) = refl

Σ-assoc-assoc' :
  {i j k : Level} (A : UU i) (B : A → UU j)
  (C : (Σ A B) → UU k) → ((Σ-assoc A B C) ∘ (Σ-assoc' A B C)) ~ id
Σ-assoc-assoc' A B C (pair x (pair y z)) = refl

abstract
  is-equiv-Σ-assoc :
    {i j k : Level} (A : UU i) (B : A → UU j)
    (C : (Σ A B) → UU k) → is-equiv (Σ-assoc A B C)
  is-equiv-Σ-assoc A B C =
    is-equiv-has-inverse
      ( Σ-assoc' A B C)
      ( Σ-assoc-assoc' A B C)
      ( Σ-assoc-assoc A B C)

equiv-Σ-assoc :
  {i j k : Level} (A : UU i) (B : A → UU j) (C : (Σ A B) → UU k) →
  Σ (Σ A B) C ≃ Σ A (λ x → Σ (B x) (λ y → C (pair x y)))
equiv-Σ-assoc A B C =
  pair (Σ-assoc A B C) (is-equiv-Σ-assoc A B C)

-- Exercise 7.10

Σ-swap :
  {i j k : Level} (A : UU i) (B : UU j) (C : A → B → UU k) →
  Σ A (λ x → Σ B (C x)) → Σ B (λ y → Σ A (λ x → C x y))
Σ-swap A B C t = pair (pr1 (pr2 t)) (pair (pr1 t) (pr2 (pr2 t)))

Σ-swap' :
  {i j k : Level} (A : UU i) (B : UU j) (C : A → B → UU k) →
  Σ B (λ y → Σ A (λ x → C x y)) → Σ A (λ x → Σ B (C x))
Σ-swap' A B C = Σ-swap B A (λ y x → C x y)

Σ-swap-swap :
  {i j k : Level} (A : UU i) (B : UU j) (C : A → B → UU k) →
  ((Σ-swap' A B C) ∘ (Σ-swap A B C)) ~ id
Σ-swap-swap A B C (pair x (pair y z)) = refl

abstract
  is-equiv-Σ-swap :
    {i j k : Level} (A : UU i) (B : UU j) (C : A → B → UU k) →
    is-equiv (Σ-swap A B C)
  is-equiv-Σ-swap A B C =
    is-equiv-has-inverse
      ( Σ-swap' A B C)
      ( Σ-swap-swap B A (λ y x → C x y))
      ( Σ-swap-swap A B C)

-- Exercise 7.11

abstract
  is-equiv-add-ℤ-right :
    (x : ℤ) → is-equiv (add-ℤ x)
  is-equiv-add-ℤ-right x =
    is-equiv-has-inverse
      ( add-ℤ (neg-ℤ x))
      ( λ y →
        ( inv (associative-add-ℤ x (neg-ℤ x) y)) ∙
        ( ap (λ t → add-ℤ t y) (right-inverse-law-add-ℤ x)))
      ( λ y →
        ( inv (associative-add-ℤ (neg-ℤ x) x y)) ∙
        ( ap (λ t → add-ℤ t y) (left-inverse-law-add-ℤ x)))

abstract
  is-equiv-add-ℤ-left :
    (y : ℤ) → is-equiv (λ x → add-ℤ x y)
  is-equiv-add-ℤ-left y =
    is-equiv-htpy (add-ℤ y)
      ( λ x → commutative-add-ℤ x y)
      ( is-equiv-add-ℤ-right y)

-- Exercise 7.12

-- Exercise 7.13

{- We construct the functoriality of coproducts. -}

functor-coprod :
  {l1 l2 l1' l2' : Level} {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'} →
  (A → A') → (B → B') → coprod A B → coprod A' B'
functor-coprod f g (inl x) = inl (f x)
functor-coprod f g (inr y) = inr (g y)

htpy-functor-coprod :
  {l1 l2 l1' l2' : Level} {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'}
  {f f' : A → A'} (H : f ~ f') {g g' : B → B'} (K : g ~ g') →
  (functor-coprod f g) ~ (functor-coprod f' g')
htpy-functor-coprod H K (inl x) = ap inl (H x)
htpy-functor-coprod H K (inr y) = ap inr (K y)

id-functor-coprod :
  {l1 l2 : Level} (A : UU l1) (B : UU l2) →
  (functor-coprod (id {A = A}) (id {A = B})) ~ id
id-functor-coprod A B (inl x) = refl
id-functor-coprod A B (inr x) = refl

compose-functor-coprod :
  {l1 l2 l1' l2' l1'' l2'' : Level}
  {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'}
  {A'' : UU l1''} {B'' : UU l2''}
  (f : A → A') (f' : A' → A'') (g : B → B') (g' : B' → B'') →
  (functor-coprod (f' ∘ f) (g' ∘ g)) ~
  ((functor-coprod f' g') ∘ (functor-coprod f g))
compose-functor-coprod f f' g g' (inl x) = refl
compose-functor-coprod f f' g g' (inr y) = refl

abstract
  is-equiv-functor-coprod :
    {l1 l2 l1' l2' : Level} {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'}
    {f : A → A'} {g : B → B'} →
    is-equiv f → is-equiv g → is-equiv (functor-coprod f g)
  is-equiv-functor-coprod {A = A} {B = B} {A' = A'} {B' = B'} {f = f} {g = g}
    (pair (pair sf issec-sf) (pair rf isretr-rf))
    (pair (pair sg issec-sg) (pair rg isretr-rg)) =
    pair
      ( pair
        ( functor-coprod sf sg)
        ( ( ( htpy-inv (compose-functor-coprod sf f sg g)) ∙h
            ( htpy-functor-coprod issec-sf issec-sg)) ∙h
          ( id-functor-coprod A' B')))
      ( pair
        ( functor-coprod rf rg)
        ( ( ( htpy-inv (compose-functor-coprod f rf g rg)) ∙h
            ( htpy-functor-coprod isretr-rf isretr-rg)) ∙h
          ( id-functor-coprod A B)))

equiv-functor-coprod :
  {l1 l2 l1' l2' : Level} {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'} →
  (A ≃ A') → (B ≃ B') → ((coprod A B) ≃ (coprod A' B'))
equiv-functor-coprod (pair e is-equiv-e) (pair f is-equiv-f) =
  pair
    ( functor-coprod e f)
    ( is-equiv-functor-coprod is-equiv-e is-equiv-f)

-- Extra material

abstract
  is-equiv-inv-con :
    {i : Level} {A : UU i} {x y z : A} (p : Id x y)
    (q : Id y z) (r : Id x z) → is-equiv (inv-con p q r)
  is-equiv-inv-con refl q r = is-equiv-id (Id q r)

equiv-inv-con :
  {i : Level} {A : UU i} {x y z : A} (p : Id x y) (q : Id y z) (r : Id x z) →
  Id (p ∙ q) r ≃ Id q ((inv p) ∙ r)
equiv-inv-con p q r = pair (inv-con p q r) (is-equiv-inv-con p q r)

abstract
  is-equiv-con-inv :
    {i : Level} {A : UU i} {x y z : A} (p : Id x y)
    (q : Id y z) (r : Id x z) → is-equiv (con-inv p q r)
  is-equiv-con-inv p refl r =
    is-equiv-comp'
      ( concat' p (inv right-unit))
      ( concat (inv right-unit) r)
      ( is-equiv-concat (inv right-unit) r)
      ( is-equiv-concat' p (inv right-unit))

equiv-con-inv :
  {i : Level} {A : UU i} {x y z : A} (p : Id x y) (q : Id y z) (r : Id x z) →
  Id (p ∙ q) r ≃ Id p (r ∙ (inv q))
equiv-con-inv p q r = pair (con-inv p q r) (is-equiv-con-inv p q r)

-- Extra constructions with homotopies

htpy-inv-con :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} →
  (H : f ~ g) (K : g ~ h) (L : f ~ h) →
  (H ∙h K) ~ L → K ~ ((htpy-inv H) ∙h L)
htpy-inv-con H K L M x = inv-con (H x) (K x) (L x) (M x)

htpy-con-inv :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} →
  (H : f ~ g) (K : g ~ h) (L : f ~ h) →
  (H ∙h K) ~ L → H ~ (L ∙h (htpy-inv K))
htpy-con-inv H K L M x = con-inv (H x) (K x) (L x) (M x)

htpy-ap-concat :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} →
  (H : f ~ g) (K K' : g ~ h) →
  K ~ K' → (H ∙h K) ~ (H ∙h K')
htpy-ap-concat {g = g} {h} H K K' L x =
  ap (concat (H x) (h x)) (L x)

htpy-ap-concat' :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} →
  (H H' : f ~ g) (K : g ~ h) →
  H ~ H' → (H ∙h K) ~ (H' ∙h K)
htpy-ap-concat' H H' K L x =
  ap (concat' _ (K x)) (L x)

htpy-distributive-inv-concat :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} →
  (H : f ~ g) (K : g ~ h) →
  (htpy-inv (H ∙h K)) ~ ((htpy-inv K) ∙h (htpy-inv H))
htpy-distributive-inv-concat H K x = distributive-inv-concat (H x) (K x)

htpy-ap-inv :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} →
  {H H' : f ~ g} →
  H ~ H' → (htpy-inv H) ~ (htpy-inv H')
htpy-ap-inv K x = ap inv (K x)

htpy-left-whisk-htpy-inv :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  {f f' : A → B} (g : B → C) (H : f ~ f') →
  (g ·l (htpy-inv H)) ~ htpy-inv (g ·l H)
htpy-left-whisk-htpy-inv g H x = ap-inv g (H x)

htpy-right-whisk-htpy-inv :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  {g g' : B → C} (H : g ~ g') (f : A → B) →
  ((htpy-inv H) ·r f) ~ (htpy-inv (H ·r f))
htpy-right-whisk-htpy-inv H f = refl-htpy

-- Old stuff

element :
  {i : Level} {A : UU i} → A → unit → A
element a star = a

htpy-element-constant :
  {i : Level} {A : UU i} (a : A) →
  (element a) ~ (const unit A a)
htpy-element-constant a star = refl

ap-const :
  {i j : Level} {A : UU i} {B : UU j} (b : B) (x y : A) →
  (ap (const A B b) {x} {y}) ~ const (Id x y) (Id b b) refl
ap-const b x .x refl = refl

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
module Tactic.Nat.Coprime.Reflect where

import Agda.Builtin.Nat as Builtin

open import Prelude
open import Control.Monad.State
open import Control.Monad.Zero
open import Control.Monad.Transformer
open import Container.Traversable
open import Numeric.Nat.GCD

open import Tactic.Reflection
open import Tactic.Reflection.Parse
open import Tactic.Reflection.Quote
open import Tactic.Deriving.Quotable
open import Tactic.Nat.Coprime.Problem

-- Reflection --

instance
  unquoteDecl QuoteExp     = deriveQuotable QuoteExp (quote Exp)
  unquoteDecl QuoteFormula = deriveQuotable QuoteFormula (quote Formula)
  unquoteDecl QuoteProblem = deriveQuotable QuoteProblem (quote Problem)

data ExpF (A : Set) : Set where
  atom : (x : Atom) → ExpF A
  _⊗_ : (a b : A) → ExpF A

instance
  FunExpF : Functor ExpF
  fmap ⦃ FunExpF ⦄ f (atom x) = atom x
  fmap ⦃ FunExpF ⦄ f (a ⊗ b) = f a ⊗ f b

  TravExpF : Traversable ExpF
  traverse ⦃ TravExpF ⦄ f (atom x) = pure (atom x)
  traverse ⦃ TravExpF ⦄ f (a ⊗ b) = ⦇ f a ⊗ f b ⦈

foldExp : ExpF Exp → Exp
foldExp (atom x) = atom x
foldExp (a ⊗ b) = a ⊗ b

-- Requires normalisation!
matchExp : Term → Maybe (ExpF Term)
matchExp (def₂ (quote Builtin._*_) a b) = just (a ⊗ b)
matchExp _ = nothing

parseExp : Term → ParseTerm TC Exp
parseExp = parseTerm atom matchExp foldExp

parseEq : Term → ParseTerm TC (Term × Term)
parseEq (def (quote _≡_) (_ ∷ _ ∷ vArg x ∷ vArg y ∷ [])) = pure (x , y)
parseEq (meta x _) = lift (blockOnMeta! x)
parseEq _ = empty

parseGCD : Term → ParseTerm TC (Term × Term)
parseGCD (def (quote get-gcd) (_ ∷ _ ∷ vArg (def₂ (quote gcd) a b) ∷ [])) = pure (a , b)
parseGCD (meta x _) = lift (blockOnMeta x)
parseGCD t = empty

parseFormula : Term → ParseTerm TC Formula
parseFormula t = do
  lhs , lit (nat 1) ← parseEq t where _ → empty
  a , b ← parseGCD lhs
  ⦇ parseExp a ⋈ parseExp b ⦈

underBinder : ParseTerm TC ⊤
underBinder = _ <$ modify (second $ map $ first $ weaken 1)

-- Parse a Problem from the context and goal type.
parseProblem : List Term → Term → ParseTerm TC (Nat × List Term × Problem)
parseProblem [] t = do
  φ ← parseFormula t
  pure (0 , [] , ([] ⊨ φ))
parseProblem (h ∷ Δ) t =
  caseM just <$> parseFormula h <|> pure nothing of λ where
    (just ψ) → do
      underBinder
      fv , Hs , (Γ ⊨ φ) ← parseProblem Δ t
      pure (suc fv , var fv [] ∷ Hs , (ψ ∷ Γ ⊨ φ))
    nothing  → do
      underBinder
      fv , Hs , Q ← parseProblem Δ t
      pure (suc fv , Hs , Q)

buildEnv : List Nat → Env
buildEnv []        i      = 0
buildEnv (x ∷ xs)  zero   = x
buildEnv (x ∷ xs) (suc i) = buildEnv xs i

quotedEnv : List Term → Term
quotedEnv ts = def₁ (quote buildEnv) (quoteList ts)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
-- Andreas, 2012-06-05 let for record patterns

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.term.let.pattern:100 #-}
-- {-# OPTIONS -v tc.lhs.top:100 #-}

module LetPair where

import Common.Level
open import Common.Equality

infixl 6 _×_
infixl 0 _,_

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

swap : {A B : Set} → A × B → B × A
swap p =
  let (a , b) = p
  in  (b , a)

prop_swap : {A B : Set}{p : A × B} →
  (fst (swap p) ≡ snd p) ×
  (snd (swap p) ≡ fst p)
prop_swap = refl , refl

rot3 : {A B C : Set} → A × B × C → B × C × A
rot3 = λ t → let
      a , b , c = t
  in  b , c , a

postulate
  A B C : Set

rot3' = λ t → let
      x : A × B × C
      x = t
      a , b , c = x
  in  b , c , a

record ⊤ : Set where
  constructor tt

test = let tt , _ = tt , tt in A


text:
{-# OPTIONS --cubical #-}
module ExerciseSession1 where

open import Part1 hiding (B)

-- We redefine B to be a family of types in this file
variable
  B : A → Type ℓ

-- Exercise 1: state and prove funExt for dependent functions f g : (x : A) → B x

-- Exercise 2: generalize the type of cong to dependent function f : (x : A) → B x
-- (hint: the result should be a PathP)

-- Exercise 3 (easy) state and prove that inhabited propositions are contractible

-- We could have stated isProp as follows:
isProp' : Type ℓ → Type ℓ
isProp' A = (x y : A) → isContr (x ≡ y)

-- Exercise 4 (easy): prove that isProp' A implies isProp A

-- For the converse we need path composition, see ExerciseSession2

-- Exercise 5: prove isPropΠ
isPropΠ : (h : (x : A) → isProp (B x)) → isProp ((x : A) → B x)
isPropΠ h = {!!}

-- Exercise 6: prove the inverse of funExt (sometimes called happly)
funExt⁻ : {f g : (x : A) → B x} → f ≡ g → ((x : A) → f x ≡ g x)
funExt⁻ p = {!!}

-- Exercise 7: use funExt⁻ to prove isSetΠ
isSetΠ : (h : (x : A) → isSet (B x)) → isSet ((x : A) → B x)
isSetΠ h = {!!}

-- We could have defined the type of singletons as follows
singl' : {A : Type ℓ} (a : A) → Type ℓ
singl' {A = A} a = Σ[ x ∈ A ] x ≡ a

-- Exercise 8 (harder): prove the corresponding version of contractibility of singetons for singl'
-- (hint: use a suitable combinations of connections and _~)
isContrSingl' : (x : A) → isContr (singl' x)
isContrSingl' x = {!!}


text:
module Tabs where

-- Tabs are not treated as white space.

tab:	 : Set₁
tab:	 = Set


text:
module Logic.Propositional.Theorems where

open import Data
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic
open import Logic.Propositional
import      Lvl
open import Syntax.Type
open import Type

------------------------------------------
-- Reflexivity

module _ {ℓ} {P : Stmt{ℓ}} where
  [↔]-reflexivity : (P ↔ P)
  [↔]-reflexivity = [↔]-intro id id

  [→]-reflexivity : (P → P)
  [→]-reflexivity = id

------------------------------------------
-- Transitivity

module _ {ℓ₁}{ℓ₂}{ℓ₃} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}}{R : Stmt{ℓ₃}} where
  [→]-transitivity : (P → Q) → (Q → R) → (P → R)
  [→]-transitivity = liftᵣ

  [↔]-transitivity : (P ↔ Q) → (Q ↔ R) → (P ↔ R)
  [↔]-transitivity ([↔]-intro qp pq) ([↔]-intro rq qr) = [↔]-intro (qp ∘ rq) (qr ∘ pq)

  [∧]-transitivity : (P ∧ Q) → (Q ∧ R) → (P ∧ R)
  [∧]-transitivity ([∧]-intro p _) ([∧]-intro _ r) = [∧]-intro p r

------------------------------------------
-- Symmetry

module _ {ℓ₁}{ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [∧]-symmetry : (P ∧ Q) → (Q ∧ P)
  [∧]-symmetry = Tuple.swap

  [∨]-symmetry : (P ∨ Q) → (Q ∨ P)
  [∨]-symmetry = Either.swap

module _ {ℓ₁}{ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [↔]-symmetry : (P ↔ Q) → (Q ↔ P)
  [↔]-symmetry = [∧]-symmetry

------------------------------------------
-- Operators that implies other ones

module _ {ℓ₁}{ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [∧]-to-[↔] : (P ∧ Q) → (P ↔ Q)
  [∧]-to-[↔] ([∧]-intro p q) = [↔]-intro (const p) (const q)

  [∧]-to-[→] : (P ∧ Q) → (P → Q)
  [∧]-to-[→] ([∧]-intro p q) = const q

  [∧]-to-[←] : (P ∧ Q) → (P ← Q)
  [∧]-to-[←] ([∧]-intro p q) = const p

  [∧]-to-[∨] : (P ∧ Q) → (P ∨ Q)
  [∧]-to-[∨] ([∧]-intro p q) = [∨]-introₗ p

  [∨]-to-[←][→] : (P ∨ Q) → (P ← Q)∨(P → Q)
  [∨]-to-[←][→] ([∨]-introₗ p) = [∨]-introₗ (const p)
  [∨]-to-[←][→] ([∨]-introᵣ q) = [∨]-introᵣ (const q)

------------------------------------------
-- Associativity (with respect to ↔)

module _ {ℓ₁}{ℓ₂}{ℓ₃} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}}{R : Stmt{ℓ₃}} where
  [∧]-associativity : ((P ∧ Q) ∧ R) ↔ (P ∧ (Q ∧ R))
  [∧]-associativity = [↔]-intro l r
    where l : ((P ∧ Q) ∧ R) ← (P ∧ (Q ∧ R))
          l ([∧]-intro p ([∧]-intro q r)) = [∧]-intro ([∧]-intro p q) r

          r : ((P ∧ Q) ∧ R) → (P ∧ (Q ∧ R))
          r ([∧]-intro ([∧]-intro p q) r) = [∧]-intro p ([∧]-intro q r)

  [∨]-associativity : ((P ∨ Q) ∨ R) ↔ (P ∨ (Q ∨ R))
  [∨]-associativity = [↔]-intro l r
    where l : ((P ∨ Q) ∨ R) ← (P ∨ (Q ∨ R))
          l ([∨]-introₗ p) = [∨]-introₗ([∨]-introₗ p)
          l ([∨]-introᵣ([∨]-introₗ q)) = [∨]-introₗ([∨]-introᵣ q)
          l ([∨]-introᵣ([∨]-introᵣ r)) = [∨]-introᵣ r

          r : ((P ∨ Q) ∨ R) → (P ∨ (Q ∨ R))
          r ([∨]-introₗ([∨]-introₗ p)) = [∨]-introₗ p
          r ([∨]-introₗ([∨]-introᵣ q)) = [∨]-introᵣ([∨]-introₗ q)
          r ([∨]-introᵣ r) = [∨]-introᵣ([∨]-introᵣ r)

-- TODO: According to https://math.stackexchange.com/questions/440261/associativity-of-iff , this is unprovable
{-[↔]-associativity : ∀{P Q R : Stmt} → ((P ↔ Q) ↔ R) ↔ (P ↔ (Q ↔ R))
[↔]-associativity {P}{Q}{R} = [↔]-intro [↔]-associativityₗ [↔]-associativityᵣ where
  [↔]-associativityₗ : ((P ↔ Q) ↔ R) ← (P ↔ (Q ↔ R))
  [↔]-associativityₗ ([↔]-intro yz2x x2yz) = [↔]-intro z2xy xy2z where
    z2xy : (P ↔ Q) ← R
    z2xy r = [↔]-intro y2x x2y where
      y2x : Q → P
      y2x q = yz2x([∧]-to-[↔]([∧]-intro q r))

      x2y : P → Q
      x2y p = [↔]-elimₗ (x2yz(p)) (r)

    xy2z : (P ↔ Q) → R -- TODO: How?
    xy2z ([↔]-intro y2x x2y) = ?

  [↔]-associativityᵣ : ((P ↔ Q) ↔ R) → (P ↔ (Q ↔ R))
  [↔]-associativityᵣ ([↔]-intro z2xy xy2z) = [↔]-intro yz2x x2yz where
    yz2x : P ← (Q ↔ R)
    yz2x ([↔]-intro z2y y2z) = ?

    x2yz : P → (Q ↔ R)
    x2yz p = [↔]-intro z2y y2z where
      z2y : R → Q
      z2y r = [↔]-elimᵣ (z2xy(r)) (p)

      y2z : Q → R
      y2z q = xy2z([∧]-to-[↔]([∧]-intro p q))
-}

------------------------------------------
-- Distributivity

module _ {ℓ₁}{ℓ₂}{ℓ₃} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}}{R : Stmt{ℓ₃}} where
  [∧][∨]-distributivityₗ : (P ∧ (Q ∨ R)) ↔ (P ∧ Q)∨(P ∧ R)
  [∧][∨]-distributivityₗ = [↔]-intro l r where
    l : (P ∧ (Q ∨ R)) ← (P ∧ Q)∨(P ∧ R)
    l([∨]-introₗ ([∧]-intro p q)) = [∧]-intro p ([∨]-introₗ q)
    l([∨]-introᵣ ([∧]-intro p r)) = [∧]-intro p ([∨]-introᵣ r)

    r : (P ∧ (Q ∨ R)) → (P ∧ Q)∨(P ∧ R)
    r([∧]-intro p ([∨]-introₗ q)) = [∨]-introₗ([∧]-intro p q)
    r([∧]-intro p ([∨]-introᵣ r)) = [∨]-introᵣ([∧]-intro p r)

  [∧][∨]-distributivityᵣ : ((P ∨ Q) ∧ R) ↔ (P ∧ R)∨(Q ∧ R)
  [∧][∨]-distributivityᵣ = [↔]-intro l r where
    l : ((P ∨ Q) ∧ R) ← (P ∧ R)∨(Q ∧ R)
    l([∨]-introₗ ([∧]-intro p r)) = [∧]-intro ([∨]-introₗ p) r
    l([∨]-introᵣ ([∧]-intro q r)) = [∧]-intro ([∨]-introᵣ q) r

    r : ((P ∨ Q) ∧ R) → (P ∧ R)∨(Q ∧ R)
    r([∧]-intro ([∨]-introₗ p) r) = [∨]-introₗ([∧]-intro p r)
    r([∧]-intro ([∨]-introᵣ q) r) = [∨]-introᵣ([∧]-intro q r)

  [∨][∧]-distributivityₗ : (P ∨ (Q ∧ R)) ↔ (P ∨ Q)∧(P ∨ R)
  [∨][∧]-distributivityₗ = [↔]-intro l r where
    l : (P ∨ (Q ∧ R)) ← (P ∨ Q)∧(P ∨ R)
    l([∧]-intro ([∨]-introₗ p) ([∨]-introₗ _)) = [∨]-introₗ(p)
    l([∧]-intro ([∨]-introₗ p) ([∨]-introᵣ r)) = [∨]-introₗ(p)
    l([∧]-intro ([∨]-introᵣ q) ([∨]-introₗ p)) = [∨]-introₗ(p)
    l([∧]-intro ([∨]-introᵣ q) ([∨]-introᵣ r)) = [∨]-introᵣ([∧]-intro q r)

    r : (P ∨ (Q ∧ R)) → (P ∨ Q)∧(P ∨ R)
    r([∨]-introₗ p)               = [∧]-intro ([∨]-introₗ p) ([∨]-introₗ p)
    r([∨]-introᵣ ([∧]-intro q r)) = [∧]-intro ([∨]-introᵣ q) ([∨]-introᵣ r)

  [∨][∧]-distributivityᵣ : ((P ∧ Q) ∨ R) ↔ (P ∨ R)∧(Q ∨ R)
  [∨][∧]-distributivityᵣ = [↔]-intro l r where
    l : ((P ∧ Q) ∨ R) ← (P ∨ R)∧(Q ∨ R)
    l([∧]-intro ([∨]-introₗ p) ([∨]-introₗ q)) = [∨]-introₗ([∧]-intro p q)
    l([∧]-intro ([∨]-introₗ p) ([∨]-introᵣ r)) = [∨]-introᵣ(r)
    l([∧]-intro ([∨]-introᵣ r) ([∨]-introₗ q)) = [∨]-introᵣ(r)
    l([∧]-intro ([∨]-introᵣ r) ([∨]-introᵣ _)) = [∨]-introᵣ(r)

    r : ((P ∧ Q) ∨ R) → (P ∨ R)∧(Q ∨ R)
    r([∨]-introₗ ([∧]-intro p q)) = [∧]-intro ([∨]-introₗ p) ([∨]-introₗ q)
    r([∨]-introᵣ r)               = [∧]-intro ([∨]-introᵣ r) ([∨]-introᵣ r)

------------------------------------------
-- Identity (with respect to →)

module _ {ℓ} {P : Stmt{ℓ}} where
  [∧]-identityₗ : (⊤ ∧ P) → P
  [∧]-identityₗ ([∧]-intro _ p) = p

  [∧]-identityᵣ : (P ∧ ⊤) → P
  [∧]-identityᵣ ([∧]-intro p _) = p

  [∨]-identityₗ : (⊥ ∨ P) → P
  [∨]-identityₗ ([∨]-introₗ ())
  [∨]-identityₗ ([∨]-introᵣ p) = p

  [∨]-identityᵣ : (P ∨ ⊥) → P
  [∨]-identityᵣ ([∨]-introₗ p) = p
  [∨]-identityᵣ ([∨]-introᵣ ())

  [→]-identityₗ : (⊤ → P) → P
  [→]-identityₗ f = f([⊤]-intro)

  [∧]-nullifierₗ : (⊥ ∧ P) → ⊥
  [∧]-nullifierₗ ([∧]-intro () _)

  [∧]-nullifierᵣ : (P ∧ ⊥) → ⊥
  [∧]-nullifierᵣ ([∧]-intro _ ())

module _ {ℓ₂}{ℓ₃} {_▫_ : Stmt{Lvl.𝟎} → Stmt{ℓ₂} → Stmt{ℓ₃}} where
  [⊤]-as-nullifierₗ : ∀{P : Stmt} → (⊤ ▫ P) → ⊤
  [⊤]-as-nullifierₗ _ = [⊤]-intro

module _ {ℓ₁}{ℓ₃} {_▫_ : Stmt{ℓ₁} → Stmt{Lvl.𝟎} → Stmt{ℓ₃}} where
  [⊤]-as-nullifierᵣ : ∀{P : Stmt} → (P ▫ ⊤) → ⊤
  [⊤]-as-nullifierᵣ _ = [⊤]-intro

------------------------------------------
-- Other

module _ {ℓ₁}{ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [∨]-not-left : (P ∨ Q) → (¬ P) → Q
  [∨]-not-left ([∨]-introₗ p) np = [⊥]-elim(np p)
  [∨]-not-left ([∨]-introᵣ q) = const q

  [∨]-not-right : (P ∨ Q) → (¬ Q) → P
  [∨]-not-right ([∨]-introₗ p) = const p
  [∨]-not-right ([∨]-introᵣ q) nq = [⊥]-elim(nq q)

module _ {ℓ₁}{ℓ₂}{ℓ₃} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}}{T : Stmt{ℓ₃}} where
  [→]-lift : (P → Q) → ((T → P) → (T → Q))
  [→]-lift = liftₗ

module _ {ℓ₁ ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  contrapositiveᵣ : (P → Q) → ((¬ P) ← (¬ Q))
  contrapositiveᵣ = [→]-transitivity

  contrapositive-variant : (P → (¬ Q)) ↔ ((¬ P) ← Q)
  contrapositive-variant = [↔]-intro swap swap

  modus-tollens : (P → Q) → (¬ Q) → (¬ P)
  modus-tollens = contrapositiveᵣ

module _ {ℓ₁}{ℓ₂}{ℓ₃}{ℓ₄} {A : Stmt{ℓ₁}}{B : Stmt{ℓ₂}}{C : Stmt{ℓ₃}}{D : Stmt{ℓ₄}} where
  constructive-dilemma : (A → B) → (C → D) → (A ∨ C) → (B ∨ D)
  constructive-dilemma = [∨]-elim2

  destructive-dilemma : (A → B) → (C → D) → ((¬ B) ∨ (¬ D)) → ((¬ A) ∨ (¬ C))
  destructive-dilemma l r = [∨]-elim2 (contrapositiveᵣ l) (contrapositiveᵣ r)

module _ {ℓ} {P : Stmt{ℓ}} where
  [¬¬]-intro : P → (¬¬ P)
  [¬¬]-intro = apply
    -- P → (P → ⊥) → ⊥

  [¬¬¬]-elim : (¬ (¬ (¬ P))) → (¬ P)
  [¬¬¬]-elim = contrapositiveᵣ [¬¬]-intro

module _ {ℓ₁}{ℓ₂}{ℓ₃} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}}{R : Stmt{ℓ₃}} where
  [↔]-move-out-[∧]ᵣ : ((P ∧ R) ↔ (Q ∧ R)) → (R → (P ↔ Q))
  [↔]-move-out-[∧]ᵣ ([↔]-intro qrpr prqr) r =
    ([↔]-intro
      (q ↦ [∧]-elimₗ(qrpr([∧]-intro q r)))
      (p ↦ [∧]-elimₗ(prqr([∧]-intro p r)))
    )

  [∧]-unaryOperatorₗ : (P ↔ Q) → ((P ∧ R) ↔ (Q ∧ R))
  [∧]-unaryOperatorₗ ([↔]-intro qp pq) =
    ([↔]-intro
      (qr ↦ [∧]-intro (qp([∧]-elimₗ qr)) ([∧]-elimᵣ qr))
      (pr ↦ [∧]-intro (pq([∧]-elimₗ pr)) ([∧]-elimᵣ pr))
    )

  currying : (P → (Q → R)) ↔ ((P ∧ Q) → R)
  currying = [↔]-intro Tuple.curry Tuple.uncurry

module _ {ℓ₁}{ℓ₂}{ℓ₃}{ℓ₄} {A : Stmt{ℓ₁}}{B : Stmt{ℓ₂}}{C : Stmt{ℓ₃}}{D : Stmt{ℓ₄}} where
  [∧]-binaryOperator : (A ↔ C) → (B ↔ D) → ((A ∧ B) ↔ (C ∧ D))
  [∧]-binaryOperator ([↔]-intro ca ac) ([↔]-intro db bd) = [↔]-intro (Tuple.map ca db) (Tuple.map ac bd)

  [∨]-binaryOperator : (A ↔ C) → (B ↔ D) → ((A ∨ B) ↔ (C ∨ D))
  [∨]-binaryOperator ([↔]-intro ca ac) ([↔]-intro db bd) = [↔]-intro (Either.map ca db) (Either.map ac bd)

module _ {ℓ₁}{ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [↔]-not-left : (P ↔ Q) → (¬ P) → (¬ Q)
  [↔]-not-left pq np q = np([↔]-elimₗ(q)(pq))

  [↔]-not-right : (P ↔ Q) → (¬ Q) → (¬ P)
  [↔]-not-right pq nq p = nq([↔]-elimᵣ(p)(pq))

  [¬]-unaryOperator : (P ↔ Q) → ((¬ P) ↔ (¬ Q))
  [¬]-unaryOperator pq = [↔]-intro ([↔]-not-right (pq)) ([↔]-not-left (pq))

module _ {ℓ₁}{ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [↔]-elim-[∨] : (P ↔ Q) → (P ∨ Q) → (P ∧ Q)
  [↔]-elim-[∨] (p↔q) ([∨]-introₗ p) = [∧]-intro p ([↔]-elimᵣ(p) p↔q)
  [↔]-elim-[∨] (p↔q) ([∨]-introᵣ q) = [∧]-intro ([↔]-elimₗ(q) p↔q) q

module _ {ℓ} {P : Stmt{ℓ}} where
  provable-top-equivalence : P → (P ↔ ⊤)
  provable-top-equivalence p = [↔]-intro (const p) (const [⊤]-intro)

  unprovable-bottom-equivalence : (¬ P) → (P ↔ ⊥)
  unprovable-bottom-equivalence np = [↔]-intro [⊥]-elim np

------------------------------------------
-- Negation is almost preserved over the conjunction-dijunction dual (De-morgan's laws).

module _ {ℓ₁ ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [¬]-preserves-[∧][∨]ₗ : (¬ (P ∧ Q)) ← ((¬ P) ∨ (¬ Q))
  [¬]-preserves-[∧][∨]ₗ ([∨]-introₗ np) = np ∘ [∧]-elimₗ
  [¬]-preserves-[∧][∨]ₗ ([∨]-introᵣ nq) = nq ∘ [∧]-elimᵣ

  [¬]-preserves-[∨][∧] : (¬ (P ∨ Q)) ↔ ((¬ P) ∧ (¬ Q))
  [¬]-preserves-[∨][∧] = [↔]-intro l r where
    l : ¬(P ∨ Q) ← ((¬ P) ∧ (¬ Q))
    l ([∧]-intro np nq) = [∨]-elim np nq

    r : (¬ (P ∨ Q)) → ((¬ P) ∧ (¬ Q))
    r f = [∧]-intro (f ∘ [∨]-introₗ) (f ∘ [∨]-introᵣ)

------------------------------------------
-- Conjunction and implication (Tuples and functions)

module _ {ℓ₁}{ℓ₂}{ℓ₃} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}}{R : Stmt{ℓ₃}} where
  [→][∧]-assumption : ((P ∧ Q) → R) ↔ (P → Q → R)
  [→][∧]-assumption = [↔]-intro Tuple.uncurry Tuple.curry

  [→][∧]-distributivityₗ : (P → (Q ∧ R)) ↔ ((P → Q) ∧ (P → R))
  [→][∧]-distributivityₗ = [↔]-intro l r
    where l : ((P → Q) ∧ (P → R)) → (P → (Q ∧ R))
          l ([∧]-intro pq pr) p = [∧]-intro (pq(p)) (pr(p))

          r : ((P → Q) ∧ (P → R)) ← (P → (Q ∧ R))
          r both = [∧]-intro ([∧]-elimₗ ∘ both) ([∧]-elimᵣ ∘ both)

  [→][∨]-distributivityₗₗ : (P → (Q ∨ R)) ← ((P → Q) ∨ (P → R))
  [→][∨]-distributivityₗₗ = l
    where l : ((P → Q) ∨ (P → R)) → (P → (Q ∨ R))
          l ([∨]-introₗ pq) p = [∨]-introₗ (pq(p))
          l ([∨]-introᵣ pr) p = [∨]-introᵣ (pr(p))

  [→ₗ][∨][∧]-preserving : ((P ∨ Q) → R) ↔ ((P → R) ∧ (Q → R))
  [→ₗ][∨][∧]-preserving = [↔]-intro l r where
    l : ((P ∨ Q) → R) ← ((P → R) ∧ (Q → R))
    l ([∧]-intro pr qr) ([∨]-introₗ p) = pr p
    l ([∧]-intro pr qr) ([∨]-introᵣ q) = qr q

    r : ((P ∨ Q) → R) → ((P → R) ∧ (Q → R))
    r pqr = [∧]-intro (pqr ∘ [∨]-introₗ) (pqr ∘ [∨]-introᵣ)

module _ {ℓ} {P : Stmt{ℓ}} where
  non-contradiction : ¬(P ∧ (¬ P))
  non-contradiction(p , np) = np p

------------------------------------------
-- Redundant formulas in operations

module _ {ℓ₁}{ℓ₂} {A : Stmt{ℓ₁}}{B : Stmt{ℓ₂}} where
  [→]-redundancy : (A → A → B) → (A → B)
  [→]-redundancy = _$₂_

module _ {ℓ} {A : Stmt{ℓ}} where
  [∧]-redundancy : (A ∧ A) ↔ A
  [∧]-redundancy = [↔]-intro ([∧]-intro $₂_) [∧]-elimₗ

  [∨]-redundancy : (A ∨ A) ↔ A
  [∨]-redundancy = [↔]-intro [∨]-introₗ ([∨]-elim id id)

------------------------------------------
-- Disjunctive forms

module _ {ℓ₁}{ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  -- Also called: Material implication
  [→]-disjunctive-formₗ : (P → Q) ← ((¬ P) ∨ Q)
  [→]-disjunctive-formₗ = [∨]-elim ([→]-lift [⊥]-elim) const

  [↔]-disjunctive-formₗ : (P ↔ Q) ← ((P ∧ Q) ∨ ((¬ P) ∧ (¬ Q)))
  [↔]-disjunctive-formₗ ([∨]-introₗ pq)   = [∧]-to-[↔] pq
  [↔]-disjunctive-formₗ ([∨]-introᵣ npnq) = Tuple.map ([⊥]-elim ∘_) ([⊥]-elim ∘_) (Tuple.swap npnq)

  -- TODO: Probably unprovable
  -- [↔]-disjunctive-formᵣ : ∀{P Q : Stmt} → (P ↔ Q) → ((P ∧ Q) ∨ ((¬ P) ∧ (¬ Q)))
  -- [↔]-disjunctive-formᵣ ([↔]-intro qp pq) =

  [¬→]-disjunctive-formₗ : ((¬ P) → Q) ← (P ∨ Q)
  [¬→]-disjunctive-formₗ = [∨]-not-left

------------------------------------------
-- Conjuctive forms

-- TODO: None of them are provable?
-- [↔]-conjunctive-form : ∀{P Q : Stmt} → (P ↔ Q) ↔ ((P ∨ Q) ∧ ((¬ P) ∨ (¬ Q)))
-- [↔]-conjunctive-form ([↔]-intro qp pq) = [∨]-elim ([→]-lift [⊥]-elim) (const)

module _ {ℓ₁ ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [→][∧]ᵣ : (P → Q) → ¬(P ∧ (¬ Q))
  [→][∧]ᵣ f = Tuple.uncurry([¬¬]-intro ∘ f)

  [¬→][∧]ₗ : ¬(P → Q) ← (P ∧ (¬ Q))
  [¬→][∧]ₗ = swap [→][∧]ᵣ

  [→¬]-¬[∧] : (P → (¬ Q)) ↔ ¬(P ∧ Q)
  [→¬]-¬[∧] = currying

------------------------------------------
-- Equivalences (TODO: I remember these being defined somewhere else, but I am not sure. At least some special cases have been used somewhere else)

module _ where
  private variable ℓ : Lvl.Level
  private variable A A₁ A₂ B B₁ B₂ : Type{ℓ}

  [∧]-map-[↔] : (A₁ ↔ A₂) → (B₁ ↔ B₂) → ((A₁ ∧ B₁) ↔ (A₂ ∧ B₂))
  [∧]-map-[↔] a b = [↔]-intro (Tuple.map ([↔]-to-[←] a) ([↔]-to-[←] b)) (Tuple.map ([↔]-to-[→] a) ([↔]-to-[→] b))

  [∧]-mapₗ-[↔] : (A₁ ↔ A₂) → ((A₁ ∧ B) ↔ (A₂ ∧ B))
  [∧]-mapₗ-[↔] a = [∧]-map-[↔] a [↔]-reflexivity

  [∧]-mapᵣ-[↔] : (B₁ ↔ B₂) → ((A ∧ B₁) ↔ (A ∧ B₂))
  [∧]-mapᵣ-[↔] b = [∧]-map-[↔] [↔]-reflexivity b

  [∨]-map-[↔] : (A₁ ↔ A₂) → (B₁ ↔ B₂) → ((A₁ ∨ B₁) ↔ (A₂ ∨ B₂))
  [∨]-map-[↔] a b = [↔]-intro (Either.map ([↔]-to-[←] a) ([↔]-to-[←] b)) (Either.map ([↔]-to-[→] a) ([↔]-to-[→] b))

  [∨]-mapₗ-[↔] : (A₁ ↔ A₂) → ((A₁ ∨ B) ↔ (A₂ ∨ B))
  [∨]-mapₗ-[↔] a = [∨]-map-[↔] a [↔]-reflexivity

  [∨]-mapᵣ-[↔] : (B₁ ↔ B₂) → ((A ∨ B₁) ↔ (A ∨ B₂))
  [∨]-mapᵣ-[↔] b = [∨]-map-[↔] [↔]-reflexivity b

  [↔]-map-[↔] : (A₁ ↔ A₂) → (B₁ ↔ B₂) → ((A₁ ↔ B₁) ↔ (A₂ ↔ B₂))
  [↔]-map-[↔] a b =
    [↔]-intro
      (Tuple.map
        (b₂a₂ ↦ [↔]-to-[←] a ∘ b₂a₂ ∘ [↔]-to-[→] b)
        (a₂b₂ ↦ [↔]-to-[←] b ∘ a₂b₂ ∘ [↔]-to-[→] a)
      )
      (Tuple.map
        (b₁a₁ ↦ [↔]-to-[→] a ∘ b₁a₁ ∘ [↔]-to-[←] b)
        (a₁b₁ ↦ [↔]-to-[→] b ∘ a₁b₁ ∘ [↔]-to-[←] a)
      )

  [↔]-mapₗ-[↔] : (A₁ ↔ A₂) → ((A₁ ↔ B) ↔ (A₂ ↔ B))
  [↔]-mapₗ-[↔] a = [↔]-map-[↔] a [↔]-reflexivity

  [↔]-mapᵣ-[↔] : (B₁ ↔ B₂) → ((A ↔ B₁) ↔ (A ↔ B₂))
  [↔]-mapᵣ-[↔] b = [↔]-map-[↔] [↔]-reflexivity b

  [→]-map-[↔] : (A₁ ↔ A₂) → (B₁ ↔ B₂) → ((A₁ → B₁) ↔ (A₂ → B₂))
  [→]-map-[↔] a b = [↔]-intro (ab ↦ [↔]-to-[←] b ∘ ab ∘ [↔]-to-[→] a) (ab ↦ [↔]-to-[→] b ∘ ab ∘ [↔]-to-[←] a)

------------------------------------------
-- Stuff related to classical logic

module _ {ℓ} {P : Stmt{ℓ}} where
  [¬¬]-excluded-middle : ¬¬(P ∨ (¬ P))
  [¬¬]-excluded-middle =
    ([¬]-intro(naorna ↦
      ((non-contradiction([∧]-intro
        (([∨]-introᵣ
          (([¬]-intro(a ↦
            ((non-contradiction([∧]-intro
              (([∨]-introₗ a) :of:  (P ∨ (¬ P)))
              (naorna         :of: ¬(P ∨ (¬ P)))
            )) :of: ⊥)
          )) :of: (¬ P))
        ) :of: (P ∨ (¬ P)))
        (naorna :of: ¬(P ∨ (¬ P)))
      )) :of: ⊥)
    )) :of: ¬¬(P ∨ (¬ P))

  -- Note:
  --   ∀{P} → (P ∨ (¬ P)) ← ((¬¬ P) → P)
  --   is not provable because the statement (P ∨ (¬ P)) requires a [¬¬]-elim.
  --   TODO: ...I think? I do not think (∀{P} → ¬¬(P ∨ (¬ P)) → ((¬¬ P) ∨ (¬ P))) is provable.
  [¬¬]-elim-from-excluded-middle : (P ∨ (¬ P)) → ((¬¬ P) → P)
  [¬¬]-elim-from-excluded-middle ([∨]-introₗ p)  (nnp) = p
  [¬¬]-elim-from-excluded-middle ([∨]-introᵣ np) (nnp) = [⊥]-elim(nnp(np))

  [¬¬]-elim-from-callcc : (∀{Q : Stmt{Lvl.𝟎}} → (((P → Q) → P) → P)) → ((¬¬ P) → P)
  [¬¬]-elim-from-callcc (callcc) (nnp) = callcc{⊥} ([⊥]-elim ∘ nnp)

module _ {ℓ} where
  [[¬¬]-elim]-[excluded-middle]-eqₗ : (∀{P : Stmt{ℓ}} → (¬¬ P) → P) ←ᶠ (∀{P : Stmt{ℓ}} → (P ∨ (¬ P)))
  [[¬¬]-elim]-[excluded-middle]-eqₗ or {P} (nnp) with or
  ... | ([∨]-introₗ p ) = p
  ... | ([∨]-introᵣ np) = [⊥]-elim(nnp(np))

  [[¬¬]-elim]-[excluded-middle]-eqᵣ : (∀{P : Stmt{ℓ}} → (¬¬ P) → P) → (∀{P : Stmt{ℓ}} → (P ∨ (¬ P)))
  [[¬¬]-elim]-[excluded-middle]-eqᵣ (nnpp) = nnpp([¬¬]-excluded-middle)

  -- TODO: https://math.stackexchange.com/questions/910240/equivalence-between-middle-excluded-law-and-double-negation-elimination-in-heyti

  [callcc]-[[¬¬]-elim]-eqₗ : (∀{P : Stmt{ℓ}}{Q : Stmt{Lvl.𝟎}} → (((P → Q) → P) → P)) → (∀{P} → (¬¬ P) → P)
  [callcc]-[[¬¬]-elim]-eqₗ (callcc) {P} (nnp) = callcc{P}{⊥} (np ↦ [⊥]-elim(nnp(np)))

  [callcc]-[[¬¬]-elim]-eqᵣ : (∀{P : Stmt{ℓ}} → (¬¬ P) → P) → (∀{P Q : Stmt{ℓ}} → (((P → Q) → P) → P))
  [callcc]-[[¬¬]-elim]-eqᵣ (nnpp) {P}{Q} (pqp) = nnpp([¬]-intro(np ↦ np(pqp(p ↦ [⊥]-elim(np p)))))

  [callcc]-[excluded-middle]-eqₗ : (∀{P : Stmt{ℓ}} → (P ∨ (¬ P))) → (∀{P Q : Stmt{ℓ}} → (((P → Q) → P) → P))
  [callcc]-[excluded-middle]-eqₗ or {P}{Q} (pqp) with or
  ... | ([∨]-introₗ p ) = p
  ... | ([∨]-introᵣ np) = pqp([⊥]-elim ∘ np)

  [callcc]-[excluded-middle]-eqᵣ : (∀{P : Stmt{ℓ}}{Q : Stmt{Lvl.𝟎}} → (((P → Q) → P) → P)) → (∀{P : Stmt{ℓ}} → (P ∨ (¬ P)))
  [callcc]-[excluded-middle]-eqᵣ (callcc) {P} = callcc{P ∨ (¬ P)}{⊥} (nor ↦ [⊥]-elim ([¬¬]-excluded-middle (nor)))

  -- TODO: Does not have to be over all propositions P in assumption. Only wem P and wem Q are used.
  weak-excluded-middle-[¬][∧]ₗ : (∀{P : Stmt{ℓ}} → (¬ P) ∨ (¬¬ P)) ↔ (∀{P : Stmt{ℓ}}{Q : Stmt{ℓ}} → ((¬ P) ∨ (¬ Q)) ← (¬ (P ∧ Q)))
  weak-excluded-middle-[¬][∧]ₗ = [↔]-intro l r where
    l : (∀{P : Stmt{ℓ}} → (¬ P) ∨ (¬¬ P)) ← (∀{P : Stmt{ℓ}}{Q : Stmt{ℓ}} → ((¬ P) ∨ (¬ Q)) ← (¬ (P ∧ Q)))
    l [¬][∧]ₗ = [¬][∧]ₗ non-contradiction

    r : (∀{P : Stmt{ℓ}} → (¬ P) ∨ (¬¬ P)) → (∀{P : Stmt{ℓ}}{Q : Stmt{ℓ}} → ((¬ P) ∨ (¬ Q)) ← (¬ (P ∧ Q)))
    r wem {P = P} {Q = Q} npq with wem {P = P} | wem {P = Q}
    r wem {P = P} {Q = Q} npq | [∨]-introₗ np  | [∨]-introₗ nq  = [∨]-introₗ np
    r wem {P = P} {Q = Q} npq | [∨]-introₗ np  | [∨]-introᵣ nnq = [∨]-introₗ np
    r wem {P = P} {Q = Q} npq | [∨]-introᵣ nnp | [∨]-introₗ nq  = [∨]-introᵣ nq
    r wem {P = P} {Q = Q} npq | [∨]-introᵣ nnp | [∨]-introᵣ nnq = [∨]-introᵣ (q ↦ nnp (p ↦ npq ([∧]-intro p q)))

------------------------------------------
-- XOR

module _ {ℓ₁}{ℓ₂} {P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} where
  [⊕][↔]-contradiction : (P ⊕ Q) → (P ↔ Q) → ⊥
  [⊕][↔]-contradiction ([⊕]-introₗ p nq) pq = nq([↔]-elimᵣ p pq)
  [⊕][↔]-contradiction ([⊕]-introᵣ q np) pq = np([↔]-elimₗ q pq)

  [⊕][∧]-contradiction : (P ⊕ Q) → (P ∧ Q) → ⊥
  [⊕][∧]-contradiction xor = [⊕][↔]-contradiction xor ∘ [∧]-to-[↔]

  [⊕]-not-both : (P ⊕ Q) → P → Q → ⊥
  [⊕]-not-both = Tuple.curry ∘ [⊕][∧]-contradiction

  [⊕]-not-left : (P ⊕ Q) → P → (¬ Q)
  [⊕]-not-left = [⊕]-not-both

  [⊕]-not-right : (P ⊕ Q) → Q → (¬ P)
  [⊕]-not-right = swap ∘ [⊕]-not-both

  [⊕]-to-[∨] : (P ⊕ Q) → (P ∨ Q)
  [⊕]-to-[∨] ([⊕]-introₗ p _) = [∨]-introₗ p
  [⊕]-to-[∨] ([⊕]-introᵣ q _) = [∨]-introᵣ q

  [⊕]-to-[¬∨] : (P ⊕ Q) → ((¬ P) ∨ (¬ Q))
  [⊕]-to-[¬∨] ([⊕]-introₗ _ nq) = [∨]-introᵣ nq
  [⊕]-to-[¬∨] ([⊕]-introᵣ _ np) = [∨]-introₗ np

  [⊕]-excluded-middleₗ : (P ⊕ Q) → (P ∨ (¬ P))
  [⊕]-excluded-middleₗ ([⊕]-introₗ p nq) = [∨]-introₗ p
  [⊕]-excluded-middleₗ ([⊕]-introᵣ q np) = [∨]-introᵣ np

  [⊕]-excluded-middleᵣ : (P ⊕ Q) → (Q ∨ (¬ Q))
  [⊕]-excluded-middleᵣ ([⊕]-introₗ p nq) = [∨]-introᵣ nq
  [⊕]-excluded-middleᵣ ([⊕]-introᵣ q np) = [∨]-introₗ q

  [⊕]-or-not-both : (P ∨ Q) → ¬(P ∧ Q) → (P ⊕ Q)
  [⊕]-or-not-both or nand with or
  ... | [∨]-introₗ p = [⊕]-introₗ p (q ↦ nand([↔]-intro p q))
  ... | [∨]-introᵣ q = [⊕]-introᵣ q (p ↦ nand([↔]-intro p q))


text:
module Two where

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

import Data.Nat as ℕ
import Data.Nat.Properties as ℕₚ

open ℕ using (ℕ; zero; suc; _+_)

-- Our language consists of constants and addition
data Expr : Set where
  const : ℕ → Expr
  plus : Expr → Expr → Expr

-- Straightforward semantics
eval-expr : Expr → ℕ
eval-expr (const n) = n
eval-expr (plus e1 e2) = eval-expr e1 + eval-expr e2

-- Tail recursive semantics
eval-expr-tail' : Expr → ℕ → ℕ
eval-expr-tail' (const n) acc = n + acc
eval-expr-tail' (plus e1 e2) acc = eval-expr-tail' e2 (eval-expr-tail' e1 acc)

eval-expr-tail : Expr → ℕ
eval-expr-tail e = eval-expr-tail' e 0

--
-- Task: prove that eval-expr-tail is equivalent to eval-expr.
--

-- The tail recursive evaluation does not depend on its accumulator
eval-expr-tail-correct-lemma : ∀ e acc → eval-expr-tail' e acc ≡ eval-expr-tail' e 0 + acc
eval-expr-tail-correct-lemma e acc = ?

-- The tail recursive evaluation agrees with the straightforward evaluation
eval-expr-tail-correct : ∀ e → eval-expr-tail e ≡ eval-expr e
eval-expr-tail-correct e = ?


text:
-- Opening this module allows lists to be written using "list notation".
-- Examples:
--   []            = ∅
--   [ a ]         = a ⊰ ∅
--   [ a , b ]     = a ⊰ b ⊰ ∅
--   [ a , b , c ] = a ⊰ b ⊰ c ⊰ ∅
module Syntax.List where

open import Data.List

{-
infixl 1      [_
infixr 1000   _,_
infixl 100000 _]

pattern []      = ∅
pattern [_ l    = l
pattern _,_ x l = x ⊰ l
pattern _] x    = x ⊰ ∅
-}

pattern []                                             = ∅
pattern [_]                 x₁                         = x₁ ⊰ ∅
pattern [_,_]               x₁ x₂                      = x₁ ⊰ x₂ ⊰ ∅
pattern [_,_,_]             x₁ x₂ x₃                   = x₁ ⊰ x₂ ⊰ x₃ ⊰ ∅
pattern [_,_,_,_]           x₁ x₂ x₃ x₄                = x₁ ⊰ x₂ ⊰ x₃ ⊰ x₄ ⊰ ∅
pattern [_,_,_,_,_]         x₁ x₂ x₃ x₄ x₅             = x₁ ⊰ x₂ ⊰ x₃ ⊰ x₄ ⊰ x₅ ⊰ ∅
pattern [_,_,_,_,_,_]       x₁ x₂ x₃ x₄ x₅ x₆          = x₁ ⊰ x₂ ⊰ x₃ ⊰ x₄ ⊰ x₅ ⊰ x₆ ⊰ ∅
pattern [_,_,_,_,_,_,_]     x₁ x₂ x₃ x₄ x₅ x₆ x₇       = x₁ ⊰ x₂ ⊰ x₃ ⊰ x₄ ⊰ x₅ ⊰ x₆ ⊰ x₇ ⊰ ∅
pattern [_,_,_,_,_,_,_,_]   x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈    = x₁ ⊰ x₂ ⊰ x₃ ⊰ x₄ ⊰ x₅ ⊰ x₆ ⊰ x₇ ⊰ x₈ ⊰ ∅
pattern [_,_,_,_,_,_,_,_,_] x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ = x₁ ⊰ x₂ ⊰ x₃ ⊰ x₄ ⊰ x₅ ⊰ x₆ ⊰ x₇ ⊰ x₈ ⊰ x₉ ⊰ ∅