text:
------------------------------------------------------------------------
-- Types with decidable equality have unique identity proofs, and
-- related results
------------------------------------------------------------------------

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

-- The part up to "decidable⇒set" follows a proof by Michael Hedberg
-- ("A coherence theorem for Martin-Löf's type theory", JFP 1998).

open import Equality

module Equality.Decidable-UIP
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Logical-equivalence using (module _⇔_)
open import H-level eq
open import Prelude

-- Weakly constant functions.

Constant : ∀ {a b} {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Constant f = ∀ x y → f x ≡ f y

-- Left inverses.

_Left-inverse-of_ : ∀ {a b} {A : Type a} {B : Type b} →
                    (B → A) → (A → B) → Type a
g Left-inverse-of f = ∀ x → g (f x) ≡ x

abstract

  -- A set with a constant endofunction with a left inverse is a
  -- proposition.

  proposition : ∀ {a} {A : Type a} →
                (f : ∃ λ (f : A → A) → Constant f) →
                (∃ λ g → g Left-inverse-of (proj₁ f)) →
                Is-proposition A
  proposition (f , constant) (g , left-inverse) x y =
    x        ≡⟨ sym (left-inverse x) ⟩
    g (f x)  ≡⟨ cong g (constant x y) ⟩
    g (f y)  ≡⟨ left-inverse y ⟩∎
    y        ∎

  -- Endofunction families on _≡_ always have left inverses.

  left-inverse :
    ∀ {a} {A : Type a} (f : (x y : A) → x ≡ y → x ≡ y) →
    ∀ {x y} → ∃ λ g → g Left-inverse-of f x y
  left-inverse {A = A} f {x} {y} =
    (λ x≡y →
       x  ≡⟨ x≡y ⟩
       y  ≡⟨ sym (f y y (refl y)) ⟩∎
       y  ∎) ,
    elim (λ {x y} x≡y → trans (f x y x≡y) (sym (f y y (refl y))) ≡ x≡y)
         (λ _ → trans-symʳ _)

  -- A type A is a set if there is a family of constant endofunctions
  -- on _≡_ {A = A}.

  constant⇒set :
    ∀ {a} {A : Type a} →
    ((x y : A) → ∃ λ (f : x ≡ y → x ≡ y) → Constant f) →
    Is-set A
  constant⇒set constant {x} {y} =
    proposition (constant x y)
                (left-inverse (λ x y → proj₁ $ constant x y))

  -- If it is known whether or not a type is inhabited, then one can
  -- define a constant endofunction for that type.

  decidable⇒constant : ∀ {a} {A : Type a} → Dec A →
                       ∃ λ (f : A → A) → Constant f
  decidable⇒constant (yes x) = (const x , λ _ _ → refl x)
  decidable⇒constant (no ¬x) = (id      , λ _ → ⊥-elim ∘ ¬x)

  -- Types with decidable equality are sets.

  decidable⇒set : ∀ {a} {A : Type a} → Decidable-equality A → Is-set A
  decidable⇒set dec =
    constant⇒set (λ x y → decidable⇒constant (dec x y))

  -- Non-dependent functions with propositional domains are constant.

  propositional-domain⇒constant :
    ∀ {a b} {A : Type a} {B : Type b} →
    Is-proposition A → (f : A → B) → Constant f
  propositional-domain⇒constant A-prop f = λ x y →
    cong f (A-prop x y)

  -- If there is a propositional, reflexive relation on A, and related
  -- elements are equal, then A is a set.
  --
  -- (The statement of this lemma is one part of the statement of
  -- Theorem 7.2.2 in "Homotopy Type Theory: Univalent Foundations of
  -- Mathematics" (first edition).)

  propositional-identity⇒set :
    ∀ {a b} {A : Type a}
    (B : A → A → Type b) →
    (∀ x y → Is-proposition (B x y)) →
    (∀ x → B x x) →
    (∀ x y → B x y → x ≡ y) →
    Is-set A
  propositional-identity⇒set B B-prop B-refl f =
    constant⇒set λ x y →
      (λ eq → f x y (subst (B x) eq (B-refl x))) ,
      (λ _ _ → propositional-domain⇒constant (B-prop x y) (f x y) _ _)

  -- The function cong {x = x} {y = y} takes (weakly) constant
  -- functions to constant functions.
  --
  -- This is Lemma 3.1 from van Doorn's "Constructing the
  -- Propositional Truncation using Non-recursive HITs".

  cong-preserves-Constant :
    ∀ {a b} {A : Type a} {B : Type b} {f : A → B} {x y : A} →
    Constant f → Constant (cong {x = x} {y = y} f)
  cong-preserves-Constant {f = f} {x = x} {y = y} c p q =
    cong f p                     ≡⟨ lemma p ⟩
    trans (sym (c x x)) (c x y)  ≡⟨ sym (lemma q) ⟩∎
    cong f q                     ∎
    where
    lemma : ∀ p → cong {x = x} {y = y} f p ≡ trans (sym (c x x)) (c x y)
    lemma = elim
      (λ {x y} p → cong {x = x} {y = y} f p ≡ trans (sym (c x x)) (c x y))
      (λ x →
         cong f (refl x)              ≡⟨ cong-refl _ ⟩
         refl (f x)                   ≡⟨ sym $ trans-symˡ _ ⟩∎
         trans (sym (c x x)) (c x x)  ∎)

  -- The following two results come from "Generalizations of Hedberg's
  -- Theorem" by Kraus, Escardó, Coquand and Altenkirch.

  -- Proposition 3.
  --
  -- (I proved this result using cong-preserves-Constant.)

  cong-constant :
    ∀ {a b} {A : Type a} {B : Type b} {f : A → B} {x} {x≡x : x ≡ x} →
    Constant f →
    cong f x≡x ≡ refl (f x)
  cong-constant {f = f} {x} {x≡x} c =
    cong f x≡x       ≡⟨ cong-preserves-Constant c _ _ ⟩
    cong f (refl x)  ≡⟨ cong-refl _ ⟩∎
    refl (f x)       ∎

  -- The "Fixed Point Lemma".

  fixpoint-lemma :
    ∀ {a} {A : Type a} →
    (f : A → A) →
    Constant f →
    Is-proposition (∃ λ x → f x ≡ x)
  fixpoint-lemma f constant (x , fx≡x) (y , fy≡y) =
      let x≡y = x    ≡⟨ sym fx≡x ⟩
                f x  ≡⟨ constant x y ⟩
                f y  ≡⟨ fy≡y ⟩∎
                y    ∎

          x≡x = x    ≡⟨ sym fx≡x ⟩
                f x  ≡⟨ subst (λ z → f z ≡ z) (sym x≡y) fy≡y ⟩∎
                x    ∎

          lemma =
            subst (λ z → f z ≡ z) x≡x fx≡x                       ≡⟨ subst-in-terms-of-trans-and-cong ⟩

            trans (sym (cong f x≡x)) (trans fx≡x (cong id x≡x))  ≡⟨ cong₂ (λ p q → trans (sym p) (trans _ q))
                                                                          (cong-constant constant) (sym $ cong-id _) ⟩
            trans (sym (refl (f x))) (trans fx≡x x≡x)            ≡⟨ cong (λ p → trans p (trans fx≡x x≡x)) sym-refl ⟩

            trans (refl (f x)) (trans fx≡x x≡x)                  ≡⟨ trans-reflˡ _ ⟩

            trans fx≡x x≡x                                       ≡⟨ sym $ trans-assoc _ _ _ ⟩

            trans (trans fx≡x (sym fx≡x))
                  (subst (λ z → f z ≡ z) (sym x≡y) fy≡y)         ≡⟨ cong (λ p → trans p (subst (λ z → f z ≡ z) (sym x≡y) fy≡y)) $
                                                                      trans-symʳ _ ⟩
            trans (refl (f x))
                  (subst (λ z → f z ≡ z) (sym x≡y) fy≡y)         ≡⟨ trans-reflˡ _ ⟩∎

            subst (λ z → f z ≡ z) (sym x≡y) fy≡y                 ∎
      in
      x , fx≡x                                  ≡⟨ Σ-≡,≡→≡ x≡x lemma ⟩
      x , subst (λ z → f z ≡ z) (sym x≡y) fy≡y  ≡⟨ sym $ Σ-≡,≡→≡ (sym x≡y) (refl _) ⟩∎
      y , fy≡y                                  ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Binary Trees
------------------------------------------------------------------------

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

module Data.Tree.Binary where

open import Level using (Level; _⊔_)
open import Data.List.Base using (List)
open import Data.DifferenceList as DiffList using (DiffList; []; _∷_; _∷ʳ_; _++_)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Function.Base
open import Relation.Binary.PropositionalEquality

private
  variable
    a b : Level
    A : Set a
    B : Set b

data Tree (A : Set a) : Set a where
  leaf : Tree A
  node : Tree A → A → Tree A → Tree A

map : (A → B) → Tree A → Tree B
map f leaf         = leaf
map f (node l m r) = node (map f l) (f m) (map f r)

size : Tree A → ℕ
size leaf         = 0
size (node l m r) = size l + suc (size r)

foldr : (B → A → B → B) → B → Tree A → B
foldr nd lf leaf         = lf
foldr nd lf (node l m r) = nd (foldr nd lf l) m (foldr nd lf r)

------------------------------------------------------------------------
-- Extraction to lists, depth first and left to right.

module Prefix where

  toDiffList : Tree A → DiffList A
  toDiffList = foldr (λ l m r → m ∷ l ++ r) []

  toList : Tree A → List A
  toList = DiffList.toList ∘′ toDiffList

module Infix where

  toDiffList : Tree A → DiffList A
  toDiffList = foldr (λ l m r → l ++ m ∷ r) []

  toList : Tree A → List A
  toList = DiffList.toList ∘′ toDiffList

module Suffix where

  toDiffList : Tree A → DiffList A
  toDiffList = foldr (λ l m r → l ++ r ∷ʳ m) []

  toList : Tree A → List A
  toList = DiffList.toList ∘′ toDiffList

ext: agda


text:
module Formalization.ClassicalPropositionalLogic.NaturalDeduction.Proofs where

open import Data.Boolean
open import Data.Either
open import Functional
open import Formalization.ClassicalPropositionalLogic.NaturalDeduction
open import Formalization.ClassicalPropositionalLogic.Place
open import Formalization.ClassicalPropositionalLogic.Syntax
import      Lvl
open import Logic
import      Logic.Propositional as Meta
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Sets.PredicateSet using (PredSet ; _∈_ ; _∉_ ; _∪_ ; _∪•_ ; _∖_ ; _⊆_ ; _⊇_ ; ∅ ; [≡]-to-[⊆] ; [≡]-to-[⊇]) renaming (•_ to singleton ; _≡_ to _≡ₛ_)
open import Type

private variable ℓₚ ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T A B : Type{ℓ}
private variable P : Type{ℓₚ}
private variable φ ψ γ : Formula(P)
private variable Γ : Formulas(P){ℓ}
private variable f : A → B
private variable s e : Bool
private variable p : P

module _ where
  [¬]-intro-converse : ((Γ ∪ singleton(φ)) ⊢ ⊥) ← (Γ ⊢ (¬ φ))
  [¬]-intro-converse {Γ = Γ}{φ = φ} Γ¬φ = [⊥]-intro (direct (Right [≡]-intro)) (weaken-union Γ¬φ)

  excluded-middle : Γ ⊢ (φ ∨ (¬ φ))
  excluded-middle =
    ([¬¬]-elim
      ([¬]-intro
        ([⊥]-intro
          ([∨]-introᵣ
            ([¬]-intro
              ([⊥]-intro
                ([∨]-introₗ (direct (Right [≡]-intro)))
                (direct (Left (Right [≡]-intro)))
              )
            )
          )
          (direct (Right [≡]-intro))
        )
      )
    )

  [→]-disjunctive-form : (Γ ⊢ (φ ⟶ ψ)) Meta.↔ (Γ ⊢ ((¬ φ) ∨ ψ))
  [→]-disjunctive-form = Meta.[↔]-intro l r where
    l = [∨]-elim
      ([⟶]-intro ([⊥]-elim ([⊥]-intro
        (direct (Right [≡]-intro))
        (direct (Left (Right [≡]-intro)))
      )))
      ([⟶]-intro (direct (Left (Right [≡]-intro))))
    r = pq ↦
      ([∨]-elim
        ([∨]-introᵣ ([⟶]-elim (direct (Right [≡]-intro)) (weaken Left pq)))
        ([∨]-introₗ (direct (Right [≡]-intro)))
        excluded-middle
      )

  [⟷]-negated : (Γ ⊢ (φ ⟷ ψ)) → (Γ ⊢ ((¬ φ) ⟷ (¬ ψ)))
  [⟷]-negated p = [⟷]-intro
    ([¬]-intro ([⊥]-intro ([⟷]-elimᵣ (direct (Right [≡]-intro)) (weaken (Left ∘ Left) p)) (direct (Left (Right [≡]-intro)))))
    (([¬]-intro ([⊥]-intro ([⟷]-elimₗ (direct (Right [≡]-intro)) (weaken (Left ∘ Left) p)) (direct (Left (Right [≡]-intro))))))

  [⟷]-conjunction-disjunction-negation : (Γ ⊢ (φ ⟷ ψ)) Meta.↔ (Γ ⊢ ((φ ∧ ψ) ∨ ((¬ φ) ∧ (¬ ψ))))
  [⟷]-conjunction-disjunction-negation = Meta.[↔]-intro l r where
    l = [∨]-elim
      ([⟷]-intro
        ([∧]-elimₗ (direct (Left (Right [≡]-intro))))
        ([∧]-elimᵣ (direct (Left (Right [≡]-intro))))
      )
      ([⟷]-intro
        ([⊥]-elim ([⊥]-intro (direct (Right [≡]-intro)) ([∧]-elimᵣ (direct (Left (Right [≡]-intro))))))
        ([⊥]-elim ([⊥]-intro (direct (Right [≡]-intro)) ([∧]-elimₗ (direct (Left (Right [≡]-intro))))))
      )
    r = p ↦ [∨]-elim
      ([∨]-introₗ ([∧]-intro
        (direct (Right [≡]-intro))
        ([⟷]-elimᵣ (direct (Right [≡]-intro)) (weaken Left p))
      ))
      ([∨]-introᵣ ([∧]-intro
        (direct (Right [≡]-intro))
        ([⟷]-elimᵣ (direct (Right [≡]-intro)) (weaken Left ([⟷]-negated p)))
      ))
      excluded-middle

-- TODO: The two proofs contain very similar cases (the structure is identical in all cases). Are there any good ways to generalize? Maybe by using the strict variants?
positive-congruence : Positive(P) f → (Γ ⊢ (φ ⟶ ψ) ⟶ (f(φ) ⟶ f(ψ)))
negative-congruence : Negative(P) f → (Γ ⊢ (φ ⟶ ψ) ⟶ (f(φ) ⟵ f(ψ)))

positive-congruence identity           = [⟶]-intro ([⟶]-intro ([⟶]-elim (direct (Right [≡]-intro)) (direct (Left (Right [≡]-intro)))))
positive-congruence (conjunctionₗ ctx) =
  [⟶]-intro ([⟶]-intro ([∧]-intro
    ([∧]-elimₗ (direct (Right [≡]-intro)))
    ([⟶]-elim ([∧]-elimᵣ (direct (Right [≡]-intro))) ([⟶]-elim (direct (Left (Right [≡]-intro))) (positive-congruence ctx)))
  ))
positive-congruence (conjunctionᵣ ctx) =
  [⟶]-intro ([⟶]-intro ([∧]-intro
    ([⟶]-elim ([∧]-elimₗ (direct (Right [≡]-intro))) ([⟶]-elim (direct (Left (Right [≡]-intro))) (positive-congruence ctx)))
    ([∧]-elimᵣ (direct (Right [≡]-intro)))
  ))
positive-congruence (disjunctionₗ ctx) =
  [⟶]-intro ([⟶]-intro ([∨]-elim
    ([∨]-introₗ (direct (Right [≡]-intro)))
    ([∨]-introᵣ ([⟶]-elim (direct (Right [≡]-intro)) ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) (positive-congruence ctx))))
    (direct (Right [≡]-intro))
  ))
positive-congruence (disjunctionᵣ ctx) =
  [⟶]-intro ([⟶]-intro ([∨]-elim
    ([∨]-introₗ ([⟶]-elim (direct (Right [≡]-intro)) ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) (positive-congruence ctx))))
    ([∨]-introᵣ (direct (Right [≡]-intro)))
    (direct (Right [≡]-intro))
  ))
positive-congruence (implicationₗ ctx) =
  [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim
    ([⟶]-elim (direct(Right [≡]-intro)) (direct (Left (Right [≡]-intro))))
    ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) (positive-congruence ctx))
  )))
positive-congruence (implicationᵣ ctx) =
  [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim
    ([⟶]-elim (direct (Right [≡]-intro)) ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) (negative-congruence ctx)))
    (direct (Left (Right [≡]-intro)))
  )))

negative-congruence (conjunctionₗ ctx) =
  [⟶]-intro ([⟶]-intro ([∧]-intro
    ([∧]-elimₗ (direct (Right [≡]-intro)))
    ([⟶]-elim ([∧]-elimᵣ (direct (Right [≡]-intro))) ([⟶]-elim (direct (Left (Right [≡]-intro))) (negative-congruence ctx)))
  ))
negative-congruence (conjunctionᵣ ctx) =
  [⟶]-intro ([⟶]-intro ([∧]-intro
    ([⟶]-elim ([∧]-elimₗ (direct (Right [≡]-intro))) ([⟶]-elim (direct (Left (Right [≡]-intro))) (negative-congruence ctx)))
    ([∧]-elimᵣ (direct (Right [≡]-intro)))
  ))
negative-congruence (disjunctionₗ ctx) =
  [⟶]-intro ([⟶]-intro ([∨]-elim
    ([∨]-introₗ (direct (Right [≡]-intro)))
    ([∨]-introᵣ ([⟶]-elim (direct (Right [≡]-intro)) ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) (negative-congruence ctx))))
    (direct (Right [≡]-intro))
  ))
negative-congruence (disjunctionᵣ ctx) =
  [⟶]-intro ([⟶]-intro ([∨]-elim
    ([∨]-introₗ ([⟶]-elim (direct (Right [≡]-intro)) ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) (negative-congruence ctx))))
    ([∨]-introᵣ (direct (Right [≡]-intro)))
    (direct (Right [≡]-intro))
  ))
negative-congruence (implicationₗ ctx) =
  [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim
    ([⟶]-elim (direct(Right [≡]-intro)) (direct (Left (Right [≡]-intro))))
    ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) (negative-congruence ctx))
  )))
negative-congruence (implicationᵣ ctx) =
  [⟶]-intro ([⟶]-intro ([⟶]-intro ([⟶]-elim
    ([⟶]-elim (direct (Right [≡]-intro)) ([⟶]-elim (direct (Left (Left (Right [≡]-intro)))) (positive-congruence ctx)))
    (direct (Left (Right [≡]-intro)))
  )))

-- TODO: Mainly for results in minimal logic
data NegativeFragment {P : Type{ℓₚ}} : Formula(P) → Type{Lvl.of(P)} where
  atom   : NegativeFragment(¬(• p))
  bottom : NegativeFragment(⊥)
  top    : NegativeFragment(⊤)
  neg    : NegativeFragment(φ) → NegativeFragment(¬ φ)
  and    : NegativeFragment(φ) → NegativeFragment(ψ) → NegativeFragment(φ ∧ ψ)
  impl   : NegativeFragment(φ) → NegativeFragment(ψ) → NegativeFragment(φ ⟶ ψ)
  eq     : NegativeFragment(φ) → NegativeFragment(ψ) → NegativeFragment(φ ⟷ ψ)

open import Functional
open import Type.Dependent
open import Type.Dependent.Functions

module GGNegativeTranslation where
  trans : Formula(P) → Formula(P)
  trans (• p)   = ¬(¬(• p))
  trans ⊤       = ⊤
  trans ⊥       = ⊥
  trans (¬ φ)   = ¬(trans φ)
  trans (φ ∧ ψ) = (trans φ) ∧ (trans ψ)
  trans (φ ∨ ψ) = ¬((¬(trans φ)) ∧ (¬(trans ψ)))
  trans (φ ⟶ ψ) = (trans φ) ⟶ (trans ψ)
  trans (φ ⟷ ψ) = (trans φ) ⟷ (trans ψ)

  trans-negativeFragment : NegativeFragment(trans(φ))
  trans-negativeFragment {φ = • p}   = neg atom
  trans-negativeFragment {φ = ⊤}     = top
  trans-negativeFragment {φ = ⊥}     = bottom
  trans-negativeFragment {φ = ¬ φ}   = neg trans-negativeFragment
  trans-negativeFragment {φ = φ ∧ ψ} = and trans-negativeFragment trans-negativeFragment
  trans-negativeFragment {φ = φ ∨ ψ} = neg(and(neg trans-negativeFragment) (neg trans-negativeFragment))
  trans-negativeFragment {φ = φ ⟶ ψ} = impl trans-negativeFragment trans-negativeFragment
  trans-negativeFragment {φ = φ ⟷ ψ} = eq trans-negativeFragment trans-negativeFragment

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:
------------------------------------------------------------------------
-- Finite sets (currently only some type signatures)
------------------------------------------------------------------------

module Data.Sets where

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.OrderMorphism
open import Data.Function
open import Data.List as L using (List)
open import Data.Product using (∃; _×_)

module Sets₁ (dto : DecTotalOrder) where

  open DecTotalOrder dto public using (_≈_)
  open DecTotalOrder dto hiding (_≈_)

  infixr 6 _∪_
  infix  5 _∈?_
  infix  4 _∈_ _|≈|_

  abstract postulate decSetoid : DecSetoid

  <Set> : Set
  <Set> = DecSetoid.carrier decSetoid

  _|≈|_ : Rel <Set>
  _|≈|_ = DecSetoid._≈_ decSetoid

  abstract
   postulate
    empty  : <Set>
    insert : carrier → <Set> → <Set>
    _∪_    : <Set> → <Set> → <Set>
    _∈_    : carrier → <Set> → Set
    _∈?_   : (x : carrier) → (s : <Set>) → Dec (x ∈ s)
    toList : <Set> → List carrier

   postulate
    prop-∈-insert₁ : ∀ {x y s} → x ≈ y → x ∈ insert y s
    prop-∈-insert₂ : ∀ {x y s} → x ∈ s → x ∈ insert y s
    prop-∈-insert₃ : ∀ {x y s} → ¬ x ≈ y → x ∈ insert y s → x ∈ s

    prop-∈-empty : ∀ {x} → ¬ x ∈ empty

    prop-∈-∪ : ∀ {x s₁ s₂} → x ∈ s₁ → x ∈ s₁ ∪ s₂

    prop-∪₁ : ∀ {s₁ s₂}    → s₁ ∪ s₂        |≈| s₂ ∪ s₁
    prop-∪₂ : ∀ {s₁ s₂ s₃} → s₁ ∪ (s₂ ∪ s₃) |≈| (s₁ ∪ s₂) ∪ s₃

    prop-∈-|≈| : ∀ {x} → (λ s → x ∈ s) Respects _|≈|_
    prop-∈-≈   : ∀ {s} → (λ x → x ∈ s) Respects  _≈_

    -- TODO: Postulates for toList.

  singleton : carrier → <Set>
  singleton x = insert x empty

  ⋃_ : List <Set> → <Set>
  ⋃_ = L.foldr _∪_ empty

  fromList : List carrier → <Set>
  fromList = L.foldr insert empty

  _⊆_ : <Set> → <Set> → Set
  s₁ ⊆ s₂ = ∀ x → x ∈ s₁ → x ∈ s₂

open Sets₁ public
open DecTotalOrder hiding (_≈_)
open _⇒-Poset_

abstract
 postulate
  map : ∀ {do₁ do₂} → do₁ ⇒-DTO do₂ → <Set> do₁ → <Set> do₂
  mapToSet : ∀ {do₁ do₂} →
             (carrier do₁ → <Set> do₂) →
             <Set> do₁ → <Set> do₂

  prop-map-∈₁ : ∀ {do₁ do₂ f x s} →
                      x ⟨ _∈_ do₁ ⟩₁       s →
                fun f x ⟨ _∈_ do₂ ⟩₁ map f s
  prop-map-∈₂ : ∀ {do₁ do₂ f y s} →
                y ⟨ _∈_ do₂ ⟩₁ map f s →
                ∃ λ x → (fun f x ⟨ _≈_ do₂ ⟩₁ y) ×
                        (      x ⟨ _∈_ do₁ ⟩₁ s)

  prop-mapToSet₁ : ∀ {do₁ do₂ f x s} →
                     x ⟨ _∈_ do₁ ⟩₁            s →
                   f x ⟨ _⊆_ do₂ ⟩₁ mapToSet f s
  prop-mapToSet₂ : ∀ {do₁ do₂ f y s} →
                   y ⟨ _∈_ do₂ ⟩₁ mapToSet f s →
                   ∃ λ x → (y ⟨ _∈_ do₂ ⟩₁ f x) ×
                           (x ⟨ _∈_ do₁ ⟩₁ s)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Proof where

open import Basics hiding (_==_)
open import Proc
open import Path
import Graph

private
  open module G = Graph Nat
  open module P = Process param hiding (U; T; _!_)

{-

Soundness:

  if we get an answer there is a path

Completeness:

  if there is a path we get an answer

-}

infix 18 _encodes_

data _encodes_ {G : Graph} :
      {x y : Nat} -> List Node -> Path G x y -> Set where
  nul-path  : {x : Nat} -> stop :: [] encodes nul {x = x}
  step-path : {x y z : Nat}{xs : List Node}
              {step : Step G x y}{path : Path G y z} ->
              xs encodes path ->
              node y :: xs encodes step <> path

test : {G : Graph}{a b c : Nat}
       {ab : Step G a b}{bc : Step G b c} ->
       node b :: node c :: stop :: [] encodes
       ab <> bc <> nul
test = step-path (step-path nul-path)

target : {G : Graph}{x y : Nat} -> Step G x y -> Nat
target {y = y} _ = y

encoding : {G : Graph}{x y : Nat} -> Path G x y -> List Node
encoding nul            = stop :: []
encoding (step <> path) = node (target step) :: encoding path

lem-encode : {G : Graph}{x y : Nat}(path : Path G x y) ->
             encoding path encodes path
lem-encode nul            = nul-path
lem-encode (step <> path) = step-path (lem-encode path)

data WellFormed : List Node -> Set where
  good-stop : WellFormed (stop :: [])
  good-::   : forall {x xs} -> WellFormed xs -> WellFormed (node x :: xs)

data MalFormed : List Node -> Set where
  bad-[]   : MalFormed []
  bad-::   : forall {x xs} -> MalFormed xs -> MalFormed (node x :: xs)
  bad-stop : forall {x xs} -> MalFormed (stop :: x :: xs)

module Theorems (G : Graph)(start end : Nat) where

  mainp = main G start end

  Complete : Set
  Complete = (path : Path G start end) ->
             ∃ \q -> Silent q /\
                     mainp -! encoding path !->* q

  Sound : Set
  Sound = forall q xs -> Silent q -> WellFormed xs ->
          mainp -! xs !->* q ->
          ∃ \(path : Path G start end) -> xs encodes path

  Sound-Fail : Set
  Sound-Fail = forall q xs -> Silent q -> MalFormed xs ->
               mainp -! xs !->* q -> Path G start end -> False

silent-edges : {a : U} -> Graph -> Proc a
silent-edges []       = o
silent-edges (_ :: G) = o || silent-edges G

silent-silent-edges : {a : U}(G : Graph) -> Silent (silent-edges {a} G)
silent-silent-edges []       = silent-o
silent-silent-edges (_ :: G) = silent-|| silent-o (silent-silent-edges G)

module Proofs (G : Graph) where

  private open module T = Theorems G

  complete : (start end : Nat) -> Complete start end
  complete x .x nul =
    ∃-intro q (silent-q , run)
    where
      edg₁ = {! !}
      edg₂ = {! !}
      edg₃ = silent-edges G

      silent-edg₃ : Silent edg₃
      silent-edg₃ = silent-silent-edges G

      q = φ /| o || o || edg₃

      silent-q : Silent q
      silent-q = silent-/| (silent-|| silent-o (silent-|| silent-o silent-edg₃))

      rx-edg₁ : edges G -[ lift (forward stop (node x)) ]-> edg₁
      rx-edg₁ = {! !}

      rx-edg₂ : edg₁ -[ {! !} ]-> edg₂
      rx-edg₂ = {! !}

      run-edg₃ : φ /| o || o || edg₂ -! [] !->* φ /| o || o || edg₃
      run-edg₃ = {! !}

      tx-batter : (n : Nat) ->
                  if node n == node n
                  then backward stop ! o
                  else def (start x)
                  -! lift (backward stop) !-> o
      tx-batter zero    = tx-!
      tx-batter (suc n) = tx-batter n

      run : mainp x x -! stop :: [] !->* q
      run = (tx-/| (tx-!|
              (tx-def tx-!)
              (rx-|| (rx-def rx->) rx-edg₁)))
            >*>
            (tx-/| (tx-|! rx-o (tx-!| (tx-batter x) rx-edg₂)))
            >!>
            run-edg₃

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module DifferentArities where

open import Common.Equality
open import Common.Prelude

f : Nat → Nat → Nat
f zero      = λ x → x
f (suc n) m = f n (suc m)

testf1 : f zero ≡ λ x → x
testf1 = refl

testf2 : ∀ {n m} → f (suc n) m ≡ f n (suc m)
testf2 = refl

testf3 : f 4 5 ≡ 9
testf3 = refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Binary relations lifted to substitutions
------------------------------------------------------------------------

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

module Data.Fin.Substitution.Relation where

open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (ℕ; zero; suc)
open import Data.Vec.Relation.Binary.Pointwise.Inductive hiding (refl)
import Function as Fun
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

-- Term relations.
--
-- A term relation R : TermRel T₁ T₂ is a ℕ-indexed family of binary
-- relations relating T₁-terms to T₂-terms.
TermRel : (ℕ → Set) → (ℕ → Set) → Set₁
TermRel T₁ T₂ = ∀ {n} → T₁ n → T₂ n → Set

-- Substitution relations.
--
-- A substitution relation R : SubRel T₁ T₂ is a ℕ²-indexed family
-- of binary relations relating T₁-substitutions to T₂-substitutions.
SubRel : (ℕ → Set) → (ℕ → Set) → Set₁
SubRel T₁ T₂ = ∀ {m n} → Sub T₁ m n → Sub T₂ m n → Set

module LiftTermRel (T₁ T₂ : ℕ → Set) where

  -- Term relations lifted point-wise to corresponding substitutions.
  --
  -- Given a relation R on T₁ and T₂ terms, the family of relations
  -- (lift R) relates T₁ and T₂ substitutions point-wise.
  lift : TermRel T₁ T₂ → SubRel T₁ T₂
  lift P σ₁ σ₂ = Pointwise P σ₁ σ₂

  infix 4 _⟨_⟩_

  -- Syntactic sugar: and infix version of lifting.
  _⟨_⟩_ : ∀ {m n} → Sub T₁ m n → TermRel T₁ T₂ → Sub T₂ m n → Set
  σ₁ ⟨ R ⟩ σ₂ = lift R σ₁ σ₂

------------------------------------------------------------------------
-- Generic substitutions lifted to relations

module _ {T₁ T₂} (_∼_ : TermRel T₁ T₂) where
  open LiftTermRel T₁ T₂ using (_⟨_⟩_)

  -- Extensions of substitutions lifted to relations.
  record RelExtension (ext₁ : Extension T₁) (ext₂ : Extension T₂) : Set where
    private
      module E₁  = Extension ext₁
      module E₂  = Extension ext₂

    -- Weakening lifted to _∼_.
    field weaken : ∀ {n} {t₁ : T₁ n} {t₂ : T₂ n} →
                   t₁ ∼ t₂ → E₁.weaken t₁ ∼ E₂.weaken t₂

    infixr 5 _/∷_

    -- Extension.
    _/∷_ : ∀ {m n t₁ t₂} {σ₁ : Sub T₁ m n} {σ₂ : Sub T₂ m n} →
           t₁ ∼ t₂ → σ₁ ⟨ _∼_ ⟩ σ₂ → t₁ E₁./∷ σ₁ ⟨ _∼_ ⟩ t₂ E₂./∷ σ₂
    t₁∼t₂ /∷ σ₁∼σ₂ = t₁∼t₂ ∷ map⁺ weaken σ₁∼σ₂

  -- Simple substitutions lifted to relations.
  record RelSimple (simple₁ : Simple T₁) (simple₂ : Simple T₂) : Set where
    private
      module S₁ = SimpleExt simple₁
      module S₂ = SimpleExt simple₂

    field
      extension : RelExtension S₁.extension S₂.extension

      -- Relates variables.
      var : ∀ {n} (x : Fin n) → S₁.var x ∼ S₂.var x

    open RelExtension extension public

    infix  10 _↑
    infixl 10 _↑⋆_

    -- Lifting.

    _↑ : ∀ {m n} {σ₁ : Sub T₁ m n} {σ₂ : Sub T₂ m n} →
         σ₁ ⟨ _∼_ ⟩ σ₂ → σ₁ S₁.↑ ⟨ _∼_ ⟩ σ₂ S₂.↑
    σ₁∼σ₂ ↑ = var zero /∷ σ₁∼σ₂

    _↑⋆_ : ∀ {m n} {σ₁ : Sub T₁ m n} {σ₂ : Sub T₂ m n} →
           σ₁ ⟨ _∼_ ⟩ σ₂ → ∀ k → σ₁ S₁.↑⋆ k ⟨ _∼_ ⟩ σ₂ S₂.↑⋆ k
    σ₁∼σ₂ ↑⋆ zero  = σ₁∼σ₂
    σ₁∼σ₂ ↑⋆ suc k = (σ₁∼σ₂ ↑⋆ k) ↑

    -- The identity substitution.
    id : ∀ {n} → S₁.id {n} ⟨ _∼_ ⟩ S₂.id {n}
    id {zero}  = []
    id {suc n} = id ↑

    -- Weakening.

    wk⋆ : ∀ k {n} → S₁.wk⋆ k {n} ⟨ _∼_ ⟩ S₂.wk⋆ k {n}
    wk⋆ zero    = id
    wk⋆ (suc k) = map⁺ weaken (wk⋆ k)

    wk : ∀ {n} → S₁.wk {n} ⟨ _∼_ ⟩ S₂.wk {n}
    wk = wk⋆ 1

    -- A substitution which only replaces the first variable.
    sub : ∀ {n} {t₁ : T₁ n} {t₂} → t₁ ∼ t₂ → S₁.sub t₁ ⟨ _∼_ ⟩ S₂.sub t₂
    sub t₁~t₂ = t₁~t₂ ∷ id

  -- Application of substitutions lifted to relations.
  record RelApplication {T₁′ T₂′} (R : TermRel T₁′ T₂′)
                        (app₁ : Application T₁ T₁′)
                        (app₂ : Application T₂ T₂′) : Set where
    private
      module A₁ = Application app₁
      module A₂ = Application app₂
    open LiftTermRel T₁′ T₂′ using () renaming (_⟨_⟩_ to _⟨_⟩′_)

    infixl 8 _/_
    infixl 9 _⊙_

    -- Post-application of substitutions to things.
    field _/_ : ∀ {m n t₁ t₂} {σ₁ : Sub T₁′ m n} {σ₂ : Sub T₂′ m n} →
                t₁ ∼ t₂ → σ₁ ⟨ R ⟩′ σ₂ → (t₁ A₁./ σ₁) ∼ (t₂ A₂./ σ₂)

    -- Reverse composition. (Fits well with post-application.)
    _⊙_ : ∀ {m n k} {σ₁ : Sub T₁ m n} {σ₂} {σ₁′ : Sub T₁′ n k} {σ₂′} →
          σ₁ ⟨ _∼_ ⟩ σ₂ → σ₁′ ⟨ R ⟩′ σ₂′ → σ₁ A₁.⊙ σ₁′ ⟨ _∼_ ⟩ σ₂ A₂.⊙ σ₂′
    σ₁∼σ₂ ⊙ σ₁∼σ₂′ = map⁺ (λ t₁∼t₂ → t₁∼t₂ / σ₁∼σ₂′) σ₁∼σ₂

  -- A combination of the two records above.
  record RelSubst (subst₁ : Subst T₁) (subst₂ : Subst T₂) : Set where
    private
      module S₁ = Subst subst₁
      module S₂ = Subst subst₂

    field
      simple      : RelSimple          S₁.simple      S₂.simple
      application : RelApplication _∼_ S₁.application S₂.application

    open RelSimple      simple      public
    open RelApplication application public

------------------------------------------------------------------------
-- Instantiations and code for facilitating instantiations

-- Liftings from TermRel T₁ T₂ to TermRel T₁′ T₂′.
record RelLift {T₁ T₂ T₁′ T₂′} (_∼_ : TermRel T₁ T₂) (_∼′_ : TermRel T₁′ T₂′)
               (l₁ : Lift T₁ T₁′) (l₂ : Lift T₂ T₂′) : Set where
  private
    module L₁ = Lift l₁
    module L₂ = Lift l₂

  field
    simple : RelSimple _∼_ L₁.simple L₂.simple
    lift   : ∀ {n} {t₁ : T₁ n} {t₂} → t₁ ∼ t₂ → L₁.lift t₁ ∼′ L₂.lift t₂

  open RelSimple simple public

-- Variable substitutions (renamings) lifted to equality.
module VarEqSubst where
  private module V = VarSubst

  infix 4 _⟨≡⟩_

  _⟨≡⟩_ : SubRel Fin Fin
  _⟨≡⟩_ = LiftTermRel.lift Fin Fin _≡_

  subst : RelSubst _≡_ V.subst V.subst
  subst = record
    { simple      = record { extension = extension; var = λ _ → refl }
    ; application = record { _/_ = _/_ }
    }
    where
      extension = record { weaken = cong suc }

      _/_ : ∀ {m n x₁ x₂} {σ₁ σ₂ : Sub Fin n m} →
            x₁ ≡ x₂ → σ₁ ⟨≡⟩ σ₂ → x₁ V./ σ₁ ≡ x₂ V./ σ₂
      _/_ {x₁ = x} refl σ₁≡σ₂ = lookup σ₁≡σ₂ x

  open RelSubst subst public

-- "Term" substitutions lifted to relations.
record TermRelSubst {T₁ T₂ : ℕ → Set} (_∼_ : TermRel T₁ T₂)
                    (ts₁ : TermSubst T₁) (ts₂ : TermSubst T₂) : Set₁ where
  private
    module S₁ = TermSubst ts₁
    module S₂ = TermSubst ts₂
    module V  = VarEqSubst

  field
    var : ∀ {n} (x : Fin n) → S₁.var x ∼ S₂.var x
    app : ∀ {T₁′ T₂′} (R : TermRel T₁′ T₂′)
          (l₁ : Lift T₁′ T₁) (l₂ : Lift T₂′ T₂) → RelLift R _∼_ l₁ l₂ →
          let open LiftTermRel T₁′ T₂′ using (_⟨_⟩_) in
          ∀ {m n t₁ t₂} {σ₁ : Sub T₁′ m n} {σ₂ : Sub T₂′ m n} →
          t₁ ∼ t₂ → σ₁ ⟨ R ⟩ σ₂ → S₁.app l₁ t₁ σ₁ ∼ S₂.app l₂ t₂ σ₂

  module RelLifted {T₁′ T₂′} (R : TermRel T₁′ T₂′)
                   (l₁ : Lift T₁′ T₁) (l₂ : Lift T₂′ T₂)
                   (lift : RelLift R _∼_ l₁ l₂) where
    private
      module L₁ = S₁.Lifted l₁
      module L₂ = S₂.Lifted l₂

    application : RelApplication _∼_ R L₁.application L₂.application
    application = record { _/_ = app R l₁ l₂ lift }

  varLift : RelLift _≡_ _∼_ S₁.varLift S₂.varLift
  varLift = record { simple = V.simple; lift = lift }
    where
      lift : ∀ {n} {x₁ x₂ : Fin n} → x₁ ≡ x₂ → S₁.var x₁ ∼ S₂.var x₂
      lift {x₁ = x} refl = var x

  infix 8 _/Var_

  _/Var_ : ∀ {m n t₁ t₂} {σ₁ σ₂ : Sub Fin m n} →
           t₁ ∼ t₂ → σ₁ V.⟨≡⟩ σ₂ → (t₁ S₁./Var σ₁) ∼ (t₂ S₂./Var σ₂)
  _/Var_ = app _≡_ S₁.varLift S₂.varLift varLift

  simple : RelSimple _∼_ S₁.simple S₂.simple
  simple = record
    { extension = record { weaken = λ t₁∼t₂ → t₁∼t₂ /Var V.wk }
    ; var       = var
    }

  termLift : RelLift _∼_ _∼_ S₁.termLift S₂.termLift
  termLift = record { simple = simple; lift = Fun.id }

  subst : RelSubst _∼_ S₁.subst S₂.subst
  subst = record
    { simple      = simple
    ; application = RelLifted.application _∼_ S₁.termLift S₂.termLift termLift
    }

  open LiftTermRel T₁ T₂  public using (_⟨_⟩_)
  open RelSubst subst public hiding (var; simple)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


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

open import HoTT
open import cw.CW
open import cw.FinCW
open import cw.FinBoundary
open import cohomology.Theory

module cw.cohomology.cochainequiv.FirstCoboundaryCommSquare (OT : OrdinaryTheory lzero)
  (⊙fin-skel : ⊙FinSkeleton 1) where

open OrdinaryTheory OT
open import cw.cohomology.WedgeOfCells OT ⊙⦉ ⊙fin-skel ⦊
open import cw.cohomology.reconstructed.TipAndAugment OT ⊙⦉ ⊙fcw-init ⊙fin-skel ⦊
open import cw.cohomology.reconstructed.TipCoboundary OT ⊙⦉ ⊙fin-skel ⦊
open import cw.cohomology.cochainequiv.DualizedFirstBoundary OT ⊙fin-skel
open import cw.cohomology.cochainequiv.FirstCoboundary OT ⊙fin-skel

private
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel
  ac = ⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero

  ⊙fin-skel₋₁ = ⊙fcw-init ⊙fin-skel
  fin-skel₋₁ = ⊙FinSkeleton.skel ⊙fin-skel₋₁
  ac₋₁ = ⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel₋₁ lzero

abstract
  rephrase-dualized-first-boundary-comm-sqr :
    CommSquareEquiv
      (λ g <I → Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁)))
      (_∘ᴳ fboundary-last fin-skel)
      (FreeAbGroup-extend (C2-abgroup 0))
      (FreeAbGroup-extend (C2-abgroup 0))
  rephrase-dualized-first-boundary-comm-sqr =
    comm-sqr (λ g →
      equiv-adj'
        (GroupIso.f-equiv (FreeAbGroup-extend-iso (C2-abgroup 0)))
        (λ= λ <I → ! (rephrase-dualized-first-boundary-in-degree g <I))) ,
    FreeAbGroup-extend-is-equiv (C2-abgroup 0) ,
    FreeAbGroup-extend-is-equiv (C2-abgroup 0)

  rephrase-cw-co∂-head-comm-sqr :
    CommSquareEquiv
      (λ g <I → Group.sum (C2 0) (λ <I' → Group.exp (C2 0) (g <I') (fdegree-last fin-skel <I <I')))
      (GroupHom.f cw-co∂-head)
      (GroupIso.g (C2×CX₀-diag-β ac₋₁))
      (GroupIso.g (CXₙ/Xₙ₋₁-diag-β ac))
  rephrase-cw-co∂-head-comm-sqr =
    comm-sqr (λ g →
      equiv-adj'
        (GroupIso.g-equiv (CXₙ/Xₙ₋₁-diag-β ac))
        (λ= λ <I → ! (rephrase-cw-co∂-head-in-degree g <I))) ,
    (GroupIso.g-is-equiv (C2×CX₀-diag-β ac₋₁)) ,
    (GroupIso.g-is-equiv (CXₙ/Xₙ₋₁-diag-β ac))

  first-coboundary-comm-sqr :
    CommSquareEquiv
      (GroupHom.f cw-co∂-head)
      (_∘ᴳ fboundary-last fin-skel)
      (FreeAbGroup-extend (C2-abgroup 0) ∘ GroupIso.f (C2×CX₀-diag-β ac₋₁))
      (FreeAbGroup-extend (C2-abgroup 0) ∘ GroupIso.f (CXₙ/Xₙ₋₁-diag-β ac))
  first-coboundary-comm-sqr =
    CommSquareEquiv-∘v
      rephrase-dualized-first-boundary-comm-sqr
      (CommSquareEquiv-inverse-v rephrase-cw-co∂-head-comm-sqr)

  first-coboundary-comm-sqrᴳ :
    CommSquareEquivᴳ
      cw-co∂-head
      (pre∘ᴳ-hom (C2-abgroup 0) (fboundary-last fin-skel))
      (FreeAbGroup-extend-hom (C2-abgroup 0) ∘ᴳ GroupIso.f-hom (C2×CX₀-diag-β ac₋₁))
      (FreeAbGroup-extend-hom (C2-abgroup 0) ∘ᴳ GroupIso.f-hom (CXₙ/Xₙ₋₁-diag-β ac))
  first-coboundary-comm-sqrᴳ =
    comm-sqrᴳ (fst first-coboundary-comm-sqr □$_) , snd first-coboundary-comm-sqr

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.TwoSemiCategory
open import lib.two-semi-categories.Functor

module lib.two-semi-categories.FunctorInverse where

module _ {k l} {B : Type k} {C : B → B → Type l}
  (comp : {b b' b'' : B} → C b b' → C b' b'' → C b b'') where

  coe-C : {b₁ b₁' b₂ b₂' : B}
    → b₁ == b₂
    → b₁' == b₂'
    → C b₁ b₁'
    → C b₂ b₂'
  coe-C p p' = coe (ap2 C p p')

  coe-comp : {b₁ b₁' b₁'' b₂ b₂' b₂'' : B}
    → (p : b₁ == b₂) (p' : b₁' == b₂') (p'' : b₁'' == b₂'')
    → (r : C b₁ b₁') (s : C b₁' b₁'')
    → coe-C p p'' (comp r s) == comp (coe-C p p' r) (coe-C p' p'' s)
  coe-comp idp idp idp r s = idp

  coe-comp-coh : {b₁ b₁' b₁'' b₁''' b₂ b₂' b₂'' b₂''' : B}
    → (assoc : {b b' b'' b''' : B}
             → (f : C b b') (g : C b' b'') (h : C b'' b''')
             → comp (comp f g) h == comp f (comp g h))
    → (p : b₁ == b₂) (p' : b₁' == b₂') (p'' : b₁'' == b₂'') (p''' : b₁''' == b₂''')
    → (f : C b₁ b₁') (g : C b₁' b₁'') (h : C b₁'' b₁''')
    → coe-comp p p'' p''' (comp f g) h ◃∙
      ap (λ s → comp s (coe-C p'' p''' h)) (coe-comp p p' p'' f g) ◃∙
      assoc (coe-C p p' f) (coe-C p' p'' g) (coe-C p'' p''' h) ◃∎
      =ₛ
      ap (coe-C p p''') (assoc f g h) ◃∙
      coe-comp p p' p''' f (comp g h) ◃∙
      ap (comp (coe-C p p' f)) (coe-comp p' p'' p''' g h) ◃∎
  coe-comp-coh assoc idp idp idp idp f g h = =ₛ-in $
    ! (ap-idf (assoc f g h)) ∙ ! (∙-unit-r (ap (coe-C idp idp) (assoc f g h)))

module FunctorInverse
  {i₁ j₁ i₂ j₂}
  {C : TwoSemiCategory i₁ j₁} {D : TwoSemiCategory i₂ j₂}
  (F : TwoSemiFunctor C D)
  (F₀-is-equiv : is-equiv (TwoSemiFunctor.F₀ F))
  (F₁-is-equiv : ∀ x y → is-equiv (TwoSemiFunctor.F₁ F {x} {y})) where

  private

    module C = TwoSemiCategory C
    module D = TwoSemiCategory D
    module F = TwoSemiFunctor F

    module F₀-is-equiv = is-equiv F₀-is-equiv
    module F₁-is-equiv (x y : C.El) = is-equiv (F₁-is-equiv x y)

    F₀ = F.F₀
    F₁ = F.F₁

  G₀ : D.El → C.El
  G₀ = F₀-is-equiv.g

  D' : TwoSemiCategory i₂ j₂
  D' =
    record
    { El = D.El
    ; Arr = λ x y → D.Arr (F₀ (G₀ x)) (F₀ (G₀ y))
    ; Arr-level = λ x y → D.Arr-level (F₀ (G₀ x)) (F₀ (G₀ y))
    ; two-semi-cat-struct =
      record
      { comp = λ f g → D.comp f g
      ; assoc = λ f g h → D.assoc f g h
      ; pentagon-identity = λ f g h i → D.pentagon-identity f g h i
      }
    }

  N : TwoSemiFunctor D D'
  N =
    record
    { F₀ = idf D.El
    ; F₁ = λ {x} {y} f → coe (Arr-path x y) f
    ; pres-comp = λ {x} {y} {z} f g →
        coe-comp D.comp (F₀-η x) (F₀-η y) (F₀-η z) f g
    ; pres-comp-coh = λ {w} {x} {y} {z} f g h →
        coe-comp-coh D.comp D.assoc (F₀-η w) (F₀-η x) (F₀-η y) (F₀-η z) f g h
    }
    where
    F₀-η : (x : D.El) → x == F₀ (G₀ x)
    F₀-η x = ! (F₀-is-equiv.f-g x)
    Arr-path : (x y : D.El) → D.Arr x y == D.Arr (F₀ (G₀ x)) (F₀ (G₀ y))
    Arr-path x y = ap2 D.Arr (F₀-η x) (F₀-η y)

  module N = TwoSemiFunctor N

  G₁ : {x y : D.El} → D.Arr (F₀ (G₀ x)) (F₀ (G₀ y)) → C.Arr (G₀ x) (G₀ y)
  G₁ {x} {y} f = F₁-is-equiv.g (G₀ x) (G₀ y) f

  F₁-β : {x y : D.El} (f : D.Arr (F₀ (G₀ x)) (F₀ (G₀ y)))
    → F₁ (G₁ f) == f
  F₁-β {x} {y} f = F₁-is-equiv.f-g (G₀ x) (G₀ y) f

  F₁-η : {x y : D.El} (f : D.Arr (F₀ (G₀ x)) (F₀ (G₀ y)))
    → f == F₁ (G₁ f)
  F₁-η f = ! (F₁-β f)

  G₁-β : {x y : D.El} → (f : C.Arr (G₀ x) (G₀ y))
    → G₁ (F₁ f) == f
  G₁-β {x} {y} f = F₁-is-equiv.g-f (G₀ x) (G₀ y) f

  G₁-pres-comp-seq : {x y z : D.El}
    (f : D.Arr (F₀ (G₀ x)) (F₀ (G₀ y)))
    (g : D.Arr (F₀ (G₀ y)) (F₀ (G₀ z)))
    → G₁ (D.comp f g) =-= C.comp (G₁ f) (G₁ g)
  G₁-pres-comp-seq {x} {y} {z} f g =
    G₁ (D.comp f g)
      =⟪ ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η g) ⟫
    G₁ (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))
      =⟪ ap G₁ (! (F.pres-comp (G₁ f) (G₁ g))) ⟫
    G₁ (F₁ (C.comp (G₁ f) (G₁ g)))
      =⟪ G₁-β (C.comp (G₁ f) (G₁ g)) ⟫
    C.comp (G₁ f) (G₁ g) ∎∎

  abstract
    G₁-pres-comp : {x y z : D.El}
      (f : D.Arr (F₀ (G₀ x)) (F₀ (G₀ y)))
      (g : D.Arr (F₀ (G₀ y)) (F₀ (G₀ z)))
      → G₁ (D.comp f g) == C.comp (G₁ f) (G₁ g)
    G₁-pres-comp f g = ↯ (G₁-pres-comp-seq f g)

    G₁-pres-comp-β : {x y z : D.El}
      (f : D.Arr (F₀ (G₀ x)) (F₀ (G₀ y)))
      (g : D.Arr (F₀ (G₀ y)) (F₀ (G₀ z)))
      → G₁-pres-comp f g ◃∎ =ₛ G₁-pres-comp-seq f g
    G₁-pres-comp-β f g = =ₛ-in idp

  private
    G₁-pres-comp-coh : {w x y z : D.El}
      (f : D.Arr (F₀ (G₀ w)) (F₀ (G₀ x)))
      (g : D.Arr (F₀ (G₀ x)) (F₀ (G₀ y)))
      (h : D.Arr (F₀ (G₀ y)) (F₀ (G₀ z)))
      → G₁-pres-comp (D.comp f g) h ◃∙
        ap (λ s → C.comp s (G₁ h)) (G₁-pres-comp f g) ◃∙
        C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ
        ap G₁ (D.assoc f g h) ◃∙
        G₁-pres-comp f (D.comp g h) ◃∙
        ap (C.comp (G₁ f)) (G₁-pres-comp g h) ◃∎
    G₁-pres-comp-coh {w} {x} {y} {z} f g h =
      G₁-pres-comp (D.comp f g) h ◃∙
      ap (λ s → C.comp s (G₁ h)) (G₁-pres-comp f g) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ⟨ 0 & 1 & G₁-pres-comp-β (D.comp f g) h ⟩
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
      ap G₁ (! (F.pres-comp (G₁ (D.comp f g)) (G₁ h))) ◃∙
      G₁-β (C.comp (G₁ (D.comp f g)) (G₁ h)) ◃∙
      ap (λ s → C.comp s (G₁ h)) (G₁-pres-comp f g) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ⟨ 2 & 2 & !ₛ $
            homotopy-naturality
              (λ s → G₁ (F₁ (C.comp s (G₁ h))))
              (λ s → C.comp s (G₁ h))
              (λ s → G₁-β (C.comp s (G₁ h)))
              (G₁-pres-comp f g) ⟩
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
      ap G₁ (! (F.pres-comp (G₁ (D.comp f g)) (G₁ h))) ◃∙
      ap (λ s → G₁ (F₁ (C.comp s (G₁ h)))) (G₁-pres-comp f g) ◃∙
      G₁-β (C.comp (C.comp (G₁ f) (G₁ g)) (G₁ h)) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ⟨ 1 & 2 & !ₛ $
            homotopy-naturality
              (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h))))
              (λ s → G₁ (F₁ (C.comp s (G₁ h))))
              (λ s → ap G₁ (! (F.pres-comp s (G₁ h))))
              (G₁-pres-comp f g) ⟩
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
      ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (G₁-pres-comp f g) ◃∙
      ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
      G₁-β (C.comp (C.comp (G₁ f) (G₁ g)) (G₁ h)) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ⟨ 1 & 1 & ap-seq-=ₛ (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (G₁-pres-comp-β f g) ⟩
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
      ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η g)) ◃∙
      ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap G₁ (! (F.pres-comp (G₁ f) (G₁ g)))) ◃∙
      ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (G₁-β (C.comp (G₁ f) (G₁ g))) ◃∙
      ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
      G₁-β (C.comp (C.comp (G₁ f) (G₁ g)) (G₁ h)) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ₁⟨ 3 & 1 & step₅ ⟩
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
      ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η g)) ◃∙
      ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap G₁ (! (F.pres-comp (G₁ f) (G₁ g)))) ◃∙
      ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (F₁ (C.comp (G₁ f) (G₁ g)))) ◃∙
      ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
      G₁-β (C.comp (C.comp (G₁ f) (G₁ g)) (G₁ h)) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ₁⟨ 2 & 1 & ∘-ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) G₁ (! (F.pres-comp (G₁ f) (G₁ g))) ⟩
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
      ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η g)) ◃∙
      ap (λ s → G₁ (D.comp (F₁ (G₁ s)) (F₁ (G₁ h)))) (! (F.pres-comp (G₁ f) (G₁ g))) ◃∙
      ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (F₁ (C.comp (G₁ f) (G₁ g)))) ◃∙
      ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
      G₁-β (C.comp (C.comp (G₁ f) (G₁ g)) (G₁ h)) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ⟨ 2 & 2 & homotopy-naturality
                      (λ s → G₁ (D.comp (F₁ (G₁ s)) (F₁ (G₁ h))))
                      (λ s → G₁ (D.comp s (F₁ (G₁ h))))
                      (λ t → ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β t))
                      (! (F.pres-comp (G₁ f) (G₁ g))) ⟩
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
      ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η g)) ◃∙
      ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) ◃∙
      ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (! (F.pres-comp (G₁ f) (G₁ g))) ◃∙
      ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
      G₁-β (C.comp (C.comp (G₁ f) (G₁ g)) (G₁ h)) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ⟨ 0 & 3 & step₈ ⟩
      ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
      ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h)) (F₁-η g) ◃∙
      ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) s)) (F₁-η h) ◃∙
      ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (! (F.pres-comp (G₁ f) (G₁ g))) ◃∙
      ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
      G₁-β (C.comp (C.comp (G₁ f) (G₁ g)) (G₁ h)) ◃∙
      C.assoc (G₁ f) (G₁ g) (G₁ h) ◃∎
        =ₛ⟨ 5 & 2 & !ₛ $
            homotopy-naturality-to-idf (G₁ ∘ F₁) G₁-β (C.assoc (G₁ f) (G₁ g) (G₁ h)) ⟩
      ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
      ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h)) (F₁-η g) ◃∙
      ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) s)) (F₁-η h) ◃∙
      ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (! (F.pres-comp (G₁ f) (G₁ g))) ◃∙
      ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
      ap (G₁ ∘ F₁) (C.assoc (G₁ f) (G₁ g) (G₁ h)) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ⟨ 3 & 3 & step₁₀ ⟩
      ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
      ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h)) (F₁-η g) ◃∙
      ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) s)) (F₁-η h) ◃∙
      ap G₁ (D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) (F₁ (G₁ h))) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h))) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ⟨ 0 & 4 & step₁₁ ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
      ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp s h))) (F₁-η g) ◃∙
      ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) s))) (F₁-η h) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h))) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ⟨ 1 & 3 & step₁₂ ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η g) (F₁-η h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h))) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ⟨ 3 & 2 & !ₛ $
            homotopy-naturality
              (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁ ∘ G₁)
              (G₁ ∘ D.comp (F₁ (G₁ f)))
              (ap (G₁ ∘ D.comp (F₁ (G₁ f))) ∘ F₁-β)
              (! (F.pres-comp (G₁ g) (G₁ h))) ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η g) (F₁-η h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁ ∘ G₁) (! (F.pres-comp (G₁ g) (G₁ h))) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (F₁ (C.comp (G₁ g) (G₁ h)))) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ₁⟨ 3 & 1 & ap-∘ (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) G₁ (! (F.pres-comp (G₁ g) (G₁ h))) ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η g) (F₁-η h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap G₁ (! (F.pres-comp (G₁ g) (G₁ h)))) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (F₁ (C.comp (G₁ g) (G₁ h)))) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ₁⟨ 4 & 1 &
             ! $ ap (ap (G₁ ∘ D.comp (F₁ (G₁ f)))) $
             F₁-is-equiv.adj (G₀ x) (G₀ z) (C.comp (G₁ g) (G₁ h)) ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η g) (F₁-η h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap G₁ (! (F.pres-comp (G₁ g) (G₁ h)))) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f))) (ap F₁ (G₁-β (C.comp (G₁ g) (G₁ h)))) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ₁⟨ 4 & 1 & ∘-ap (G₁ ∘ D.comp (F₁ (G₁ f))) F₁ (G₁-β (C.comp (G₁ g) (G₁ h))) ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η g) (F₁-η h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap G₁ (! (F.pres-comp (G₁ g) (G₁ h)))) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (G₁-β (C.comp (G₁ g) (G₁ h))) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ⟨ 2 & 3 & ap-seq-=ₛ (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (!ₛ (G₁-pres-comp-β g h)) ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
      ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (G₁-pres-comp g h) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ⟨ 2 & 2 &
            homotopy-naturality
              (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁)
              (G₁ ∘ F₁ ∘ C.comp (G₁ f))
              (λ s → ap G₁ (! (F.pres-comp (G₁ f) s)))
              (G₁-pres-comp g h) ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (G₁ (D.comp g h)))) ◃∙
      ap (G₁ ∘ F₁ ∘ C.comp (G₁ f)) (G₁-pres-comp g h) ◃∙
      G₁-β (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        =ₛ⟨ 3 & 2 &
            homotopy-naturality
              (G₁ ∘ F₁ ∘ C.comp (G₁ f))
              (C.comp (G₁ f))
              (G₁-β ∘ C.comp (G₁ f))
              (G₁-pres-comp g h) ⟩
      ap G₁ (D.assoc f g h) ◃∙
      ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
      ap G₁ (! (F.pres-comp (G₁ f) (G₁ (D.comp g h)))) ◃∙
      G₁-β (C.comp (G₁ f) (G₁ (D.comp g h))) ◃∙
      ap (C.comp (G₁ f)) (G₁-pres-comp g h) ◃∎
        =ₛ⟨ 1 & 3 & !ₛ (G₁-pres-comp-β f (D.comp g h)) ⟩
      ap G₁ (D.assoc f g h) ◃∙
      G₁-pres-comp f (D.comp g h) ◃∙
      ap (C.comp (G₁ f)) (G₁-pres-comp g h) ◃∎ ∎ₛ
      where
        step₅ : ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (G₁-β (C.comp (G₁ f) (G₁ g)))
                ==
                ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (F₁ (C.comp (G₁ f) (G₁ g))))
        step₅ =
          ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (G₁-β (C.comp (G₁ f) (G₁ g)))
            =⟨ ap-∘ (λ s → G₁ (D.comp s (F₁ (G₁ h)))) F₁ (G₁-β (C.comp (G₁ f) (G₁ g))) ⟩
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (ap F₁ (G₁-β (C.comp (G₁ f) (G₁ g))))
            =⟨ ap (ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))))
                  (F₁-is-equiv.adj (G₀ w) (G₀ y) (C.comp (G₁ f) (G₁ g))) ⟩
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (F₁ (C.comp (G₁ f) (G₁ g)))) =∎
        step₈ : ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
                ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η g)) ◃∙
                ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) ◃∎
                =ₛ
                ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
                ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h)) (F₁-η g) ◃∙
                ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) s)) (F₁-η h) ◃∎
        step₈ =
          ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
          ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η g)) ◃∙
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) ◃∎
            =ₛ₁⟨ 1 & 1 & ap (ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))))
                            (! (ap-ap2 G₁ D.comp (F₁-η f) (F₁-η g))) ⟩
          ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
          ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) (ap G₁ (ap2 D.comp (F₁-η f) (F₁-η g))) ◃∙
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) ◃∎
            =ₛ₁⟨ 1 & 1 & ∘-ap (λ s → G₁ (D.comp (F₁ s) (F₁ (G₁ h)))) G₁ (ap2 D.comp (F₁-η f) (F₁-η g)) ⟩
          ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp f g)) (F₁-η h) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ s)) (F₁ (G₁ h)))) (ap2 D.comp (F₁-η f) (F₁-η g)) ◃∙
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) ◃∎
            =ₛ⟨ 0 & 2 & !ₛ $
                homotopy-naturality (λ s → G₁ (D.comp s h))
                                    (λ s → G₁ (D.comp (F₁ (G₁ s)) (F₁ (G₁ h))))
                                    (λ s → ap2 (λ s t → G₁ (D.comp s t)) (F₁-η s) (F₁-η h))
                                    (ap2 D.comp (F₁-η f) (F₁-η g)) ⟩
          ap (λ s → G₁ (D.comp s h)) (ap2 D.comp (F₁-η f) (F₁-η g)) ◃∙
          ap2 (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) (F₁-η h) ◃∙
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) ◃∎
            =ₛ⟨ 1 & 1 & ap2-out' (λ s t → G₁ (D.comp s t)) (F₁-η (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) (F₁-η h) ⟩
          ap (λ s → G₁ (D.comp s h)) (ap2 D.comp (F₁-η f) (F₁-η g)) ◃∙
          ap (λ t → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) t)) (F₁-η h) ◃∙
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-η (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) ◃∙
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g)))) ◃∎
            =ₛ⟨ 2 & 2 &
                ap-seq-=ₛ (λ s → G₁ (D.comp s (F₁ (G₁ h)))) $
                =ₛ-in {s = F₁-η (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) ◃∙
                           F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) ◃∎}
                      {t = D.comp (F₁ (G₁ f)) (F₁ (G₁ g)) ∎∎}
                      (!-inv-l (F₁-β (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))))) ⟩
          ap (λ s → G₁ (D.comp s h)) (ap2 D.comp (F₁-η f) (F₁-η g)) ◃∙
          ap (λ t → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) t)) (F₁-η h) ◃∎
            =ₛ₁⟨ 0 & 1 & ap-ap2 (λ s → G₁ (D.comp s h)) D.comp (F₁-η f) (F₁-η g) ⟩
          ap2 (λ s t → G₁ (D.comp (D.comp s t) h)) (F₁-η f) (F₁-η g) ◃∙
          ap (λ t → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) t)) (F₁-η h) ◃∎
            =ₛ⟨ 0 & 1 & ap2-out (λ s t → G₁ (D.comp (D.comp s t) h)) (F₁-η f) (F₁-η g) ⟩
          ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
          ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h)) (F₁-η g) ◃∙
          ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) s)) (F₁-η h) ◃∎ ∎ₛ
        step₁₀' : ap (λ s → D.comp s (F₁ (G₁ h))) (! (F.pres-comp (G₁ f) (G₁ g))) ◃∙
                  ! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h)) ◃∙
                  ap F₁ (C.assoc (G₁ f) (G₁ g) (G₁ h)) ◃∎
                  =ₛ
                  D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) (F₁ (G₁ h)) ◃∙
                  ap (D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h))) ◃∙
                  ! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h))) ◃∎
        step₁₀' =
          ap (λ s → D.comp s (F₁ (G₁ h))) (! (F.pres-comp (G₁ f) (G₁ g))) ◃∙
          ! e₀₋₁ ◃∙
          e₀₋₄ ◃∎
            =ₛ₁⟨ 0 & 1 & ap-! (λ s → D.comp s (F₁ (G₁ h))) (F.pres-comp (G₁ f) (G₁ g)) ⟩
          ! e₁₋₂ ◃∙ ! e₀₋₁ ◃∙ e₀₋₄ ◃∎
            =ₛ⟨ post-rotate-seq-in {p = ! e₁₋₂ ◃∙ ! e₀₋₁ ◃∙ e₀₋₄ ◃∎} $
                pre-rotate'-seq-in {p = e₀₋₁ ◃∙ e₁₋₂ ◃∎} $
                !ₛ $ F.pres-comp-coh (G₁ f) (G₁ g) (G₁ h) ⟩
          e₂₋₃ ◃∙ ! e₅₋₃ ◃∙ ! e₄₋₅ ◃∎
            =ₛ₁⟨ 1 & 1 & !-ap (D.comp (F₁ (G₁ f))) (F.pres-comp (G₁ g) (G₁ h)) ⟩
          e₂₋₃ ◃∙
          ap (D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h))) ◃∙
          ! e₄₋₅ ◃∎ ∎ₛ
          where
            t₀ : D.Arr (F₀ (G₀ w)) (F₀ (G₀ z))
            t₀ = F₁ (C.comp (C.comp (G₁ f) (G₁ g)) (G₁ h))
            t₁ : D.Arr (F₀ (G₀ w)) (F₀ (G₀ z))
            t₁ = D.comp (F₁ (C.comp (G₁ f) (G₁ g))) (F₁ (G₁ h))
            t₂ : D.Arr (F₀ (G₀ w)) (F₀ (G₀ z))
            t₂ = D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) (F₁ (G₁ h))
            t₃ : D.Arr (F₀ (G₀ w)) (F₀ (G₀ z))
            t₃ = D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))
            t₄ : D.Arr (F₀ (G₀ w)) (F₀ (G₀ z))
            t₄ = F₁ (C.comp (G₁ f) (C.comp (G₁ g) (G₁ h)))
            t₅ = D.comp (F₁ (G₁ f)) (F₁ (C.comp (G₁ g) (G₁ h)))
            e₀₋₁ : t₀ == t₁
            e₀₋₁ = F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h)
            e₁₋₂ : t₁ == t₂
            e₁₋₂ = ap (λ s → D.comp s (F₁ (G₁ h))) (F.pres-comp (G₁ f) (G₁ g))
            e₂₋₃ : t₂ == t₃
            e₂₋₃ = D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) (F₁ (G₁ h))
            e₀₋₄ : t₀ == t₄
            e₀₋₄ = ap F₁ (C.assoc (G₁ f) (G₁ g) (G₁ h))
            e₄₋₅ : t₄ == t₅
            e₄₋₅ = F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h))
            e₅₋₃ : t₅ == t₃
            e₅₋₃ = ap (D.comp (F₁ (G₁ f))) (F.pres-comp (G₁ g) (G₁ h))
        step₁₀ : ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (! (F.pres-comp (G₁ f) (G₁ g))) ◃∙
                 ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
                 ap (G₁ ∘ F₁) (C.assoc (G₁ f) (G₁ g) (G₁ h)) ◃∎
                 =ₛ
                 ap G₁ (D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) (F₁ (G₁ h))) ◃∙
                 ap (G₁ ∘ D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h))) ◃∙
                 ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∎
        step₁₀ =
          ap (λ s → G₁ (D.comp s (F₁ (G₁ h)))) (! (F.pres-comp (G₁ f) (G₁ g))) ◃∙
          ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
          ap (G₁ ∘ F₁) (C.assoc (G₁ f) (G₁ g) (G₁ h)) ◃∎
            =ₛ₁⟨ 0 & 1 & ap-∘ G₁ (λ s → D.comp s (F₁ (G₁ h))) (! (F.pres-comp (G₁ f) (G₁ g))) ⟩
          ap G₁ (ap (λ s → D.comp s (F₁ (G₁ h))) (! (F.pres-comp (G₁ f) (G₁ g)))) ◃∙
          ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
          ap (G₁ ∘ F₁) (C.assoc (G₁ f) (G₁ g) (G₁ h)) ◃∎
            =ₛ₁⟨ 2 & 1 & ap-∘ G₁ F₁ (C.assoc (G₁ f) (G₁ g) (G₁ h)) ⟩
          ap G₁ (ap (λ s → D.comp s (F₁ (G₁ h))) (! (F.pres-comp (G₁ f) (G₁ g)))) ◃∙
          ap G₁ (! (F.pres-comp (C.comp (G₁ f) (G₁ g)) (G₁ h))) ◃∙
          ap G₁ (ap F₁ (C.assoc (G₁ f) (G₁ g) (G₁ h))) ◃∎
            =ₛ⟨ ap-seq-=ₛ G₁ step₁₀' ⟩
          ap G₁ (D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) (F₁ (G₁ h))) ◃∙
          ap G₁ (ap (D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h)))) ◃∙
          ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∎
            =ₛ₁⟨ 1 & 1 & ∘-ap G₁ (D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h))) ⟩
          ap G₁ (D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) (F₁ (G₁ h))) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (! (F.pres-comp (G₁ g) (G₁ h))) ◃∙
          ap G₁ (! (F.pres-comp (G₁ f) (C.comp (G₁ g) (G₁ h)))) ◃∎ ∎ₛ
        step₁₁ :
          ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
          ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h)) (F₁-η g) ◃∙
          ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) s)) (F₁-η h) ◃∙
          ap G₁ (D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) (F₁ (G₁ h))) ◃∎
          =ₛ
          ap G₁ (D.assoc f g h) ◃∙
          ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp s h))) (F₁-η g) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) s))) (F₁-η h) ◃∎
        step₁₁ =
          ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
          ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h)) (F₁-η g) ◃∙
          ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) s)) (F₁-η h) ◃∙
          ap G₁ (D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) (F₁ (G₁ h))) ◃∎
            =ₛ⟨ 2 & 2 &
                homotopy-naturality (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) (F₁ (G₁ g))) s))
                                    (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) s)))
                                    (λ s → ap G₁ (D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) s))
                                    (F₁-η h) ⟩
          ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
          ap (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h)) (F₁-η g) ◃∙
          ap G₁ (D.assoc (F₁ (G₁ f)) (F₁ (G₁ g)) h) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) s))) (F₁-η h) ◃∎
            =ₛ⟨ 1 & 2 &
                homotopy-naturality (λ s → G₁ (D.comp (D.comp (F₁ (G₁ f)) s) h))
                                    (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp s h)))
                                    (λ s → ap G₁ (D.assoc (F₁ (G₁ f)) s h))
                                    (F₁-η g) ⟩
          ap (λ s → G₁ (D.comp (D.comp s g) h)) (F₁-η f) ◃∙
          ap G₁ (D.assoc (F₁ (G₁ f)) g h) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp s h))) (F₁-η g) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) s))) (F₁-η h) ◃∎
            =ₛ⟨ 0 & 2 &
                homotopy-naturality (λ s → G₁ (D.comp (D.comp s g) h))
                                    (λ s → G₁ (D.comp s (D.comp g h)))
                                    (λ s → ap G₁ (D.assoc s g h))
                                    (F₁-η f) ⟩
          ap G₁ (D.assoc f g h) ◃∙
          ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp s h))) (F₁-η g) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) s))) (F₁-η h) ◃∎ ∎ₛ
        step₁₂ : ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
                 ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp s h))) (F₁-η g) ◃∙
                 ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) s))) (F₁-η h) ◃∎
                 =ₛ
                 ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
                 ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η g) (F₁-η h)) ◃∙
                 ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))) ◃∎
        step₁₂ =
          ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp s h))) (F₁-η g) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (D.comp (F₁ (G₁ g)) s))) (F₁-η h) ◃∎
            =ₛ⟨ 1 & 2 & !ₛ (ap2-out (λ s t → G₁ (D.comp (F₁ (G₁ f)) (D.comp s t))) (F₁-η g) (F₁-η h)) ⟩
          ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
          ap2 (λ s t → G₁ (D.comp (F₁ (G₁ f)) (D.comp s t))) (F₁-η g) (F₁-η h) ◃∎
            =ₛ₁⟨ 1 & 1 & ! (ap-ap2 (G₁ ∘ D.comp (F₁ (G₁ f))) D.comp (F₁-η g) (F₁-η h)) ⟩
          ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (ap2 D.comp (F₁-η g) (F₁-η h)) ◃∎
            =ₛ⟨ 2 & 0 &
                 ap-seq-=ₛ (G₁ ∘ D.comp (F₁ (G₁ f))) $
                 =ₛ-in {s = D.comp (F₁ (G₁ g)) (F₁ (G₁ h)) ∎∎}
                       {t = F₁-η (D.comp (F₁ (G₁ g)) (F₁ (G₁ h))) ◃∙
                            F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h))) ◃∎}
                       (! (!-inv-l (F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))))) ⟩
          ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (ap2 D.comp (F₁-η g) (F₁-η h)) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-η (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))) ◃∎
            =ₛ⟨ 1 & 2 &
                homotopy-naturality (G₁ ∘ D.comp (F₁ (G₁ f)))
                                    (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁ ∘ G₁)
                                    (ap (G₁ ∘ D.comp (F₁ (G₁ f))) ∘ F₁-η)
                                    (ap2 D.comp (F₁-η g) (F₁-η h)) ⟩
          ap (λ s → G₁ (D.comp s (D.comp g h))) (F₁-η f) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-η (D.comp g h)) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁ ∘ G₁) (ap2 D.comp (F₁-η g) (F₁-η h)) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))) ◃∎
            =ₛ⟨ 0 & 2 & !ₛ (ap2-out (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h))) ⟩
          ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
          ap (λ s → G₁ (D.comp (F₁ (G₁ f)) (F₁ (G₁ s)))) (ap2 D.comp (F₁-η g) (F₁-η h)) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))) ◃∎
            =ₛ₁⟨ 1 & 1 & ap-ap2 (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁ ∘ G₁) D.comp (F₁-η g) (F₁-η h) ⟩
          ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
          ap2 (λ s t → G₁ (D.comp (F₁ (G₁ f)) (F₁ (G₁ (D.comp s t))))) (F₁-η g) (F₁-η h) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))) ◃∎
            =ₛ₁⟨ 1 & 1 &
                 ! (ap-ap2 (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁)
                           (λ s t → G₁ (D.comp s t))
                           (F₁-η g)
                           (F₁-η h)) ⟩
          ap2 (λ s t → G₁ (D.comp s t)) (F₁-η f) (F₁-η (D.comp g h)) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f)) ∘ F₁) (ap2 (λ s t → G₁ (D.comp s t)) (F₁-η g) (F₁-η h)) ◃∙
          ap (G₁ ∘ D.comp (F₁ (G₁ f))) (F₁-β (D.comp (F₁ (G₁ g)) (F₁ (G₁ h)))) ◃∎ ∎ₛ

    G : TwoSemiFunctor D' C
    G =
      record
      { F₀ = G₀
      ; F₁ = G₁
      ; pres-comp = G₁-pres-comp
      ; pres-comp-coh = G₁-pres-comp-coh
      }

    module G = TwoSemiFunctor G

  module Comp = FunctorComposition N G
  open Comp using () renaming (composition to functor) public
  open TwoSemiFunctor functor public

  abstract
    pres-comp-β : {x y z : D.El} (f : D.Arr x y) (g : D.Arr y z)
      → pres-comp f g ◃∎
        =ₛ
        ap G.F₁ (N.pres-comp f g) ◃∙
        G₁-pres-comp-seq (N.F₁ f) (N.F₁ g)
    pres-comp-β f g =
      pres-comp f g ◃∎
        =ₛ⟨ Comp.pres-comp-β f g ⟩
      ap G.F₁ (N.pres-comp f g) ◃∙
      G₁-pres-comp (N.F₁ f) (N.F₁ g) ◃∎
        =ₛ⟨ 1 & 1 & G₁-pres-comp-β (N.F₁ f) (N.F₁ g) ⟩
      ap G.F₁ (N.pres-comp f g) ◃∙
      G₁-pres-comp-seq (N.F₁ f) (N.F₁ g) ∎ₛ

open FunctorInverse
  using ()
  renaming (functor to functor-inverse) public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

module Dodo.Nullary where

open import Dodo.Nullary.Disjoint public
open import Dodo.Nullary.Unique public
open import Dodo.Nullary.XOpt public

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

open import Data.Unit

module MyTestModule where

e1 : let x = ⊤ in x
e1 = checkProperty record
  { databasePath = DATABASE_PATH
  ; propertyUUID = ????
  }

max_stars_repo_name: Yiergot/vehicle

max_issues_repo_name: Yiergot/vehicle

max_forks_repo_name: Yiergot/vehicle


text:
-- 2010-10-14

{-# OPTIONS --universe-polymorphism #-}

module ProjectionsPreserveGuardednessTrivialExample where

-- Coinduction is only available with universe polymorphism

postulate
  Level : Set
  zero : Level
  suc  : (i : Level) → Level
  _⊔_ : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX _⊔_ #-}

infixl 6 _⊔_

-- Coinduction

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

-- Products

infixr 4 _,_
infixr 2 _×_

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

open Σ public

syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ[ x ∶ A ] B

-- Streams

infixr 5 _∷_

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

mutual

  repeat : {A : Set}(a : A) → Stream A
  repeat a = a ∷ proj₂ (repeat' a)

  repeat' : {A : Set}(a : A) → A × ∞ (Stream A)
  repeat' a = a , ♯ repeat a

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Left-biased universe-sensitive functor and monad instances for These.
--
-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b).
-- See the Data.Product.Categorical.Examples for how this is done in a
-- Product-based similar setting.
------------------------------------------------------------------------

-- This functor can be understood as a notion of computation which can
-- either fail (this), succeed (that) or accumulate warnings whilst
-- delivering a successful computation (these).

-- It is a good alternative to Data.Product.Categorical when the notion
-- of warnings does not have a neutral element (e.g. List⁺).

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

open import Level
open import Algebra

module Data.These.Categorical.Left {c ℓ} (W : Semigroup c ℓ) (b : Level) where

open Semigroup W
open import Data.These.Categorical.Left.Base Carrier b public

open import Data.These
open import Category.Applicative
open import Category.Monad

module _ {a b} {A : Set a} {B : Set b} where

applicative : RawApplicative Theseₗ
applicative = record
  { pure = that
  ; _⊛_  = ap
  } where

  ap : ∀ {A B}→ Theseₗ (A → B) → Theseₗ A → Theseₗ B
  ap (this w)    t = this w
  ap (that f)    t = map₂ f t
  ap (these w f) t = map (w ∙_) f t

monad : RawMonad Theseₗ
monad = record
  { return = that
  ; _>>=_  = bind
  } where

  bind : ∀ {A B} → Theseₗ A → (A → Theseₗ B) → Theseₗ B
  bind (this w)    f = this w
  bind (that t)    f = f t
  bind (these w t) f = map₁ (w ∙_) (f t)


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

module Dodo.Binary.Flip where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Function.Base using (flip)
open import Relation.Binary using (Rel; REL)
open import Relation.Binary using (Symmetric)
-- Local imports
open import Dodo.Binary.Equality

-- # Operations

-- ## Operations: ⊆₂

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} where

  flip-⊆₂ : P ⊆₂ Q → flip P ⊆₂ flip Q
  flip-⊆₂ (⊆: P⊆Q) = ⊆: (flip P⊆Q)

module _ {a ℓ₁ : Level} {A : Set a} {P : Rel A ℓ₁} where

  flip-sym-⊆₂ : Symmetric P → P ⊆₂ flip P
  flip-sym-⊆₂ symP = ⊆: (λ _ _ → symP)

-- ## Operations: ⇔₂

module _ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
    {P : REL A B ℓ₁} {Q : REL A B ℓ₂} where

  flip-⇔₂ : P ⇔₂ Q → flip P ⇔₂ flip Q
  flip-⇔₂ = ⇔₂-compose flip-⊆₂ flip-⊆₂

module _ {a ℓ₁ : Level} {A : Set a} {P : Rel A ℓ₁} where

  flip-sym-⇔₂ : Symmetric P → P ⇔₂ flip P
  flip-sym-⇔₂ symP = ⇔₂-intro (flip-sym-⊆₂ symP) (flip-sym-⊆₂ symP)


text:
module MatchUpNames where
open import ParseTree
open import ScopeState
open import Data.Sum

open import Data.List hiding (lookup)
open import AgdaHelperFunctions

matchUpSignature : TypeSignature -> ScopeState TypeSignature

matchUpExpr : Expr -> ScopeState Expr
matchUpExpr (ident identifier₁) = do
  x <- access identifier₁
  return $ ident x
matchUpExpr (functionApp x x₁ {b} ) = do
  r1 <- matchUpExpr x
  r2 <- matchUpExpr x₁
  return $ functionApp r1 r2 {b}
matchUpExpr (namedArgument arg {b} {bef} {aft}) = do
  x <- matchUpSignature arg
  return $ namedArgument x {b} {bef} {aft}
matchUpExpr x =  return x

matchUpSignature (typeSignature funcName funcType) = do
  newName <- access funcName
  newType <- matchUpExpr funcType
  return $ typeSignature newName newType

matchUpPragma : Pragma -> ScopeState Pragma
matchUpPragma (builtin concept definition) = do
  x <- access definition
  return $ builtin concept x
matchUpPragma x = return x

matchUpTree : ParseTree -> ScopeState ParseTree
matchUpTree (signature signature₁ range₁) = do
  x <- matchUpSignature signature₁
  return $ signature x range₁
matchUpTree (functionDefinition definitionOf params body range₁) = do
  newDef <- access definitionOf
  newParams <- mapState matchUpExpr params
  newBody <- matchUpExpr body
  return $ functionDefinition newDef newParams newBody range₁
matchUpTree (dataStructure dataName parameters indexInfo constructors range₁ {comments}) = do
  newName <- access dataName
  newParams <- mapState matchUpSignature parameters
  newIndex <- matchUpExpr indexInfo
  newCons <- mapState matchUpSignature constructors
  return $ dataStructure newName newParams newIndex newCons range₁ {comments}
matchUpTree (pragma pragma₁ range₁) = do
  x <- matchUpPragma pragma₁
  return $ pragma x range₁
matchUpTree (moduleName id r) = do
  x <- access id
  return $ moduleName x r
matchUpTree x = return x

matchUpNames : List ParseTree -> ScopeState (List ParseTree)
matchUpNames list = mapState matchUpTree list


text:
------------------------------------------------------------------------
-- Cyclic groups
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

import Equality.Path as P

module Group.Cyclic
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude as P
  hiding (id; _^_) renaming (_∘_ to _⊚_; _+_ to _⊕_)

open import Equality.Path.Isomorphisms eq
open import Equality.Path.Isomorphisms.Univalence eq
open import Equivalence-relation equality-with-J
  using (Is-equivalence-relation)
open import Equivalence equality-with-J using (_≃_)
open import Erased.Cubical eq
open import Function-universe equality-with-J hiding (_∘_)
open import Group equality-with-J as G
  using (Group; Abelian; _≃ᴳ_; Homomorphic)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as T using (∥_∥; ∣_∣)
open import Integer equality-with-J hiding (suc) renaming (_*_ to _⊛_)
import Nat equality-with-J as Nat
open import Quotient eq as Q using (_/_)

open Homomorphic

private
  module ℤG = Group ℤ-group

private
  variable
    a     : Level
    A     : Type a
    g     : A
    G₁ G₂ : Group g
    n     : ℕ
    i j k : ℤ

------------------------------------------------------------------------
-- Cyclic groups

-- The property of being generated by an element.

Generated-by : (G : Group g) → Group.Carrier G → Type g
Generated-by G g =
  (x : Carrier) → ∥ (∃ λ (i : ℤ) → x ≡ g ^ i) ∥
  where
  open Group G

-- The property of being cyclic.

Cyclic : Group g → Type g
Cyclic G = ∥ ∃ (Generated-by G) ∥

-- Cyclic groups are abelian.

Cyclic→Abelian : (G : Group g) → Cyclic G → Abelian G
Cyclic→Abelian G c x y =
  flip (T.rec Carrier-is-set) c          λ (g , gen-by) →
  flip (T.rec Carrier-is-set) (gen-by x) λ (i , x≡) →
  flip (T.rec Carrier-is-set) (gen-by y) λ (j , y≡) →
    x ∘ y          ≡⟨ cong₂ _∘_ x≡ y≡ ⟩
    g ^ i ∘ g ^ j  ≡⟨ ^∘^ i ⟩
    g ^ (i + j)    ≡⟨ cong (g ^_) $ +-comm i ⟩
    g ^ (j + i)    ≡⟨ sym $ ^∘^ j ⟩
    g ^ j ∘ g ^ i  ≡⟨ sym $ cong₂ _∘_ y≡ x≡ ⟩∎
    y ∘ x          ∎
  where
  open Group G

-- If two groups are isomorphic, and one is generated by g, then the
-- other is generated by the image of g under the isomorphism.

≃ᴳ→Generated-by→Generated-by :
  (G₁≃G₂ : G₁ ≃ᴳ G₂) →
  Generated-by G₁ g →
  Generated-by G₂ (to G₁≃G₂ g)
≃ᴳ→Generated-by→Generated-by
  {G₁ = G₁} {G₂ = G₂} {g = g} G₁≃G₂ gen-by x =
  flip T.∥∥-map (gen-by (_≃_.from (G₁≃G₂ .related) x)) λ (i , x≡) →
    i
  , (x                    ≡⟨ sym $ _≃_.from-to (G₁≃G₂ .related) x≡ ⟩
     to G₁≃G₂ (g G₁.^ i)  ≡⟨ G.→ᴳ-^ G₁≃G₂ g i ⟩∎
     to G₁≃G₂ g G₂.^ i    ∎)
  where
  module G₁ = Group G₁
  module G₂ = Group G₂

-- If two groups are isomorphic, and one is cyclic, then the other one
-- is cyclic.

≃ᴳ→Cyclic→Cyclic : G₁ ≃ᴳ G₂ → Cyclic G₁ → Cyclic G₂
≃ᴳ→Cyclic→Cyclic G₁≃G₂ =
  T.∥∥-map λ (_ , gen-by) →
    _ , ≃ᴳ→Generated-by→Generated-by G₁≃G₂ gen-by

------------------------------------------------------------------------
-- The group of integers is cyclic

-- The group of integers is generated by + 1.

ℤ-generated-by-1 : Generated-by ℤ-group (+ 1)
ℤ-generated-by-1 i = ∣ i , sym (*-left-identity i) ∣

-- The group of integers is cyclic.

ℤ-cyclic : Cyclic ℤ-group
ℤ-cyclic = ∣ _ , ℤ-generated-by-1 ∣

------------------------------------------------------------------------
-- The group ℤ × ℤ is not cyclic

-- The direct product of the group of integers and the group of
-- integers is not cyclic.

ℤ×ℤ-not-cyclic : ¬ Cyclic (ℤ-group G.× ℤ-group)
ℤ×ℤ-not-cyclic =
  T.rec ⊥-propositional λ (g , gen-by) →
  flip (T.rec ⊥-propositional) (gen-by (+ 0 , + 1)) λ (i , 0,1≡) →
  flip (T.rec ⊥-propositional) (gen-by (+ 1 , + 0)) λ (j , 1,0≡) →
  lemma₂ g i j (0,1≡ , 1,0≡)
  where
  module G² = Group (ℤ-group G.× ℤ-group)

  0≡*+→≡0 : ∀ n i → + 0 ≡ i *+ P.suc n → i ≡ + 0
  0≡*+→≡0 n i 0≡ = case -⊎0⊎+ i of λ where
    (inj₁ neg)        → ⊥-elim $ ¬-0 (<0→*+suc<0 i n neg) (sym 0≡)
    (inj₂ (inj₁ ≡0))  → ≡0
    (inj₂ (inj₂ pos)) → ⊥-elim $ ¬+0 (>0→*+suc> i n pos) (sym 0≡)

  1≢0* : ∀ i → + 1 ≢ + 0 ⊛ i
  1≢0* i =
    + 1 ≡ + 0 ⊛ i  ↝⟨ flip trans (ℤG.id^ i) ⟩
    + 1 ≡ + 0      ↝⟨ +[1+]≢- ⟩□
    ⊥              □

  -≡0→≡0 : - i ≡ + 0 → i ≡ + 0
  -≡0→≡0 {i = i} hyp =
    i      ≡⟨ sym $ ℤG.involutive _ ⟩
    - - i  ≡⟨ cong -_ hyp ⟩
    - + 0  ≡⟨ ℤG.identity ⟩∎
    + 0    ∎

  lemma₁ :
    ∀ g₁ g₂ i j →
    ¬ ((+ 0 ≡ g₁ ⊛ i × + 1 ≡ g₂ ⊛ i) ×
       (+ 1 ≡ g₁ ⊛ j × + 0 ≡ g₂ ⊛ j))
  lemma₁ _ _ (+ zero) _ =
    (_ × + 1 ≡ + 0) × _  ↝⟨ proj₂ ⊚ proj₁ ⟩
    + 1 ≡ + 0            ↝⟨ +[1+]≢- ⟩□
    ⊥                    □

  lemma₁ g₁ g₂ (+ P.suc m) j =
    (+ 0 ≡ g₁ *+ P.suc m × _) × (+ 1 ≡ g₁ ⊛ j × _)  ↝⟨ Σ-map (0≡*+→≡0 m _ ⊚ proj₁) proj₁ ⟩
    g₁ ≡ + 0 × + 1 ≡ g₁ ⊛ j                         ↝⟨ (λ (p , q) → trans q (cong (_⊛ j) p)) ⟩
    + 1 ≡ (+ 0) ⊛ j                                 ↝⟨ 1≢0* j ⟩□
    ⊥                                               □

  lemma₁ g₁ g₂ -[1+ m ] j =
    (+ 0 ≡ (- g₁) *+ P.suc m × _) × (+ 1 ≡ g₁ ⊛ j × _)  ↝⟨ Σ-map (0≡*+→≡0 m _ ⊚ proj₁) proj₁ ⟩
    - g₁ ≡ + 0 × + 1 ≡ g₁ ⊛ j                           ↝⟨ Σ-map -≡0→≡0 P.id ⟩
    g₁ ≡ + 0 × + 1 ≡ g₁ ⊛ j                             ↝⟨ (λ (p , q) → trans q (cong (_⊛ j) p)) ⟩
    + 1 ≡ (+ 0) ⊛ j                                     ↝⟨ 1≢0* j ⟩□
    ⊥                                                   □

  lemma₂ : ∀ g i j → ¬ ((+ 0 , + 1) ≡ g G².^ i × (+ 1 , + 0) ≡ g G².^ j)
  lemma₂ g@(g₁ , g₂) i j =
    (+ 0 , + 1) ≡ g G².^ i × (+ 1 , + 0) ≡ g G².^ j  ↝⟨ Σ-map (flip trans (G.^-× ℤ-group ℤ-group i))
                                                              (flip trans (G.^-× ℤ-group ℤ-group j)) ⟩
    (+ 0 , + 1) ≡ (g₁ ⊛ i , g₂ ⊛ i) ×
    (+ 1 , + 0) ≡ (g₁ ⊛ j , g₂ ⊛ j)                  ↔⟨ inverse $ ≡×≡↔≡ ×-cong ≡×≡↔≡ ⟩

    (+ 0 ≡ g₁ ⊛ i × + 1 ≡ g₂ ⊛ i) ×
    (+ 1 ≡ g₁ ⊛ j × + 0 ≡ g₂ ⊛ j)                    ↝⟨ lemma₁ g₁ g₂ i j ⟩□

    ⊥                                                □

-- The group of integers is not isomorphic to the direct product of
-- the group of integers and the group of integers.

ℤ≄ᴳℤ×ℤ : ¬ ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)
ℤ≄ᴳℤ×ℤ =
  ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)  ↝⟨ flip ≃ᴳ→Cyclic→Cyclic ℤ-cyclic ⟩
  Cyclic (ℤ-group G.× ℤ-group)      ↝⟨ ℤ×ℤ-not-cyclic ⟩□
  ⊥                                 □

-- The group of integers is not equal to the direct product of the
-- group of integers and the group of integers.

ℤ≢ℤ×ℤ : ℤ-group ≢ (ℤ-group G.× ℤ-group)
ℤ≢ℤ×ℤ =
  ℤ-group ≡ (ℤ-group G.× ℤ-group)   ↝⟨ flip (subst (ℤ-group ≃ᴳ_)) G.↝ᴳ-refl ⟩
  ℤ-group ≃ᴳ (ℤ-group G.× ℤ-group)  ↝⟨ ℤ≄ᴳℤ×ℤ ⟩□
  ⊥                                 □

------------------------------------------------------------------------
-- The "equality modulo n" relation

-- Equality modulo n.

infix 4 _≡_mod_

_≡_mod_ : ℤ → ℤ → ℕ → Type
i ≡ j mod n = ∥ (∃ λ k → i ≡ j + k *+ n) ∥

-- The relation _≡_mod n is an equivalence relation.

≡-mod-is-equivalence-relation :
  ∀ n → Is-equivalence-relation (_≡_mod n)
≡-mod-is-equivalence-relation n = λ where
  .Is-equivalence-relation.reflexive {x = i} →
    ∣ + 0
    , (i             ≡⟨ sym +-right-identity ⟩
       i + + 0       ≡⟨ cong (_+_ i) $ sym $ ℤG.id^+ n ⟩∎
       i + + 0 *+ n  ∎)
    ∣
  .Is-equivalence-relation.symmetric {x = i} {y = j} →
    T.∥∥-map λ (k , i≡j+kn) →
        - k
      , (j                        ≡⟨ sym +-right-identity ⟩
         j + + 0                  ≡⟨ cong (_+_ j) $ sym $ +-right-inverse (k *+ n) ⟩
         j + (k *+ n - k *+ n)    ≡⟨ cong (_+_ j) $ cong (_+_ (k *+ n)) $ ℤG.^+⁻¹ n ⟩
         j + (k *+ n + - k *+ n)  ≡⟨ +-assoc j ⟩
         j + k *+ n + - k *+ n    ≡⟨ cong (_+ - k *+ n) $ sym i≡j+kn ⟩∎
         i + - k *+ n             ∎)

  .Is-equivalence-relation.transitive {x = i} {y = j} {z = k} →
    T.rec (Π-closure ext 1 λ _ →
           T.truncation-is-proposition) λ (l₁ , i≡j+l₁n) →
    T.∥∥-map λ (l₂ , j≡k+l₂n) →
        l₂ + l₁
      , (i                        ≡⟨ i≡j+l₁n ⟩
         j + l₁ *+ n              ≡⟨ cong (_+ l₁ *+ n) j≡k+l₂n ⟩
         k + l₂ *+ n + l₁ *+ n    ≡⟨ sym $ +-assoc k ⟩
         k + (l₂ *+ n + l₁ *+ n)  ≡⟨ cong (_+_ k) $ sym $ *+-distrib-+ n ⟩∎
         k + (l₂ + l₁) *+ n       ∎)

-- If i and j are equal modulo n, then i + k and j + k are also equal
-- modulo n.

+-cong : ∀ n j → i ≡ j mod n → i + k ≡ j + k mod n
+-cong {i = i} {k = k} n j = T.∥∥-map λ (l , i≡j+ln) →
    l
  , (i + k             ≡⟨ cong (_+ k) i≡j+ln ⟩
     j + l *+ n + k    ≡⟨ sym $ +-assoc j ⟩
     j + (l *+ n + k)  ≡⟨ cong (_+_ j) $ +-comm (l *+ n) ⟩
     j + (k + l *+ n)  ≡⟨ +-assoc j ⟩∎
     j + k + l *+ n    ∎)

-- If i and j are equal modulo n, then - i and - j are also equal
-- modulo n.

negate-cong : ∀ n j → i ≡ j mod n → - i ≡ - j mod n
negate-cong {i = i} n j = T.∥∥-map λ (k , i≡j+kn) →
    - k
  , (- i               ≡⟨ cong -_ i≡j+kn ⟩
     - (j + k *+ n)    ≡⟨ ℤG.∘⁻¹ {p = j} ⟩
     - (k *+ n) + - j  ≡⟨ +-comm (- (k *+ n)) ⟩
     - j + - (k *+ n)  ≡⟨ cong (_+_ (- j)) $ ℤG.^+⁻¹ n ⟩∎
     - j + - k *+ n    ∎)

-- If i and j are equal modulo n, then i *+ m and j *+ m are equal
-- modulo m * n.

*+-cong : ∀ m → i ≡ j mod n → i *+ m ≡ j *+ m mod m * n
*+-cong {i = i} {j = j} {n = n} m = T.∥∥-map λ (k , i≡j+kn) →
    k
  , (i *+ m                 ≡⟨ cong (_*+ m) i≡j+kn ⟩
     (j + k *+ n) *+ m      ≡⟨ ℤG.∘^+≡^+∘^+ (+-comm j) m ⟩
     j *+ m + k *+ n *+ m   ≡⟨ cong (_+_ (j *+ m)) $ ℤG.^+^+≡^+* n ⟩
     j *+ m + k *+ (n * m)  ≡⟨ cong (_+_ (j *+ m)) $ cong (k *+_) $ Nat.*-comm n ⟩∎
     j *+ m + k *+ (m * n)  ∎)

-- If i and j are equal modulo 2 * n, then ⌊ i /2⌋ and ⌊ j /2⌋ are
-- equal modulo n.

⌊/2⌋-cong : ∀ j n → i ≡ j mod 2 * n → ⌊ i /2⌋ ≡ ⌊ j /2⌋ mod n
⌊/2⌋-cong {i = i} j n = T.∥∥-map λ (k , i≡j+k2n) →
    k
  , (⌊ i /2⌋                  ≡⟨ cong ⌊_/2⌋ i≡j+k2n ⟩
     ⌊ j + k *+ (2 * n) /2⌋   ≡⟨ cong (⌊_/2⌋ ⊚ (_+_ j) ⊚ (k *+_)) $ sym $ Nat.*-comm n ⟩
     ⌊ j + k *+ (n * 2) /2⌋   ≡⟨ cong (⌊_/2⌋ ⊚ (_+_ j)) $ sym $ ℤG.^+^+≡^+* n ⟩
     ⌊ j + (k *+ n) *+ 2 /2⌋  ≡⟨ ⌊+*+2/2⌋≡ j ⟩∎
     ⌊ j /2⌋ + k *+ n         ∎)

-- It is not the case that 0 is equal to 1 modulo n, if n is at least
-- 2.

0≢1mod2+ : ∀ n → ¬ + 0 ≡ + 1 mod 2 ⊕ n
0≢1mod2+ n = T.rec ⊥-propositional $ uncurry lemma
  where
  lemma : ∀ k → + 0 ≢ + 1 + k *+ (2 ⊕ n)
  lemma (+ 0) =
    + 0 ≡ + 1 + + 0 *+ (2 ⊕ n)  ↝⟨ flip trans (cong (_+_ (+ 1)) $ ℤG.id^+ (2 ⊕ n)) ⟩
    + 0 ≡ + 1 + + 0             ↔⟨⟩
    + 0 ≡ + 1                   ↝⟨ +[1+]≢- ⊚ sym ⟩□
    ⊥                           □
  lemma (+ suc k) =
    + 0 ≡ + 1 + + suc k *+ (2 ⊕ n)         ↝⟨ flip ¬+0 ⊚ sym ⟩
    ¬ Positive (+ 1 + + suc k *+ (2 ⊕ n))  ↝⟨ _⊚ >0→>0→+>0 (+ 1) (+ suc k *+ (2 ⊕ n)) _ ⟩
    ¬ Positive (+ suc k *+ (2 ⊕ n))        ↝⟨ _$ >0→*+suc> (+ suc k) (suc n) _ ⟩□
    ⊥                                      □
  lemma -[1+ zero ] =
    + 0 ≡ + 1 + -[1+ 0 ] *+ (2 ⊕ n)             ↝⟨ flip trans (+-assoc (+ 1) {j = -[1+ 0 ]} {k = -[1+ 0 ] *+ (1 ⊕ n)}) ⟩
    + 0 ≡ + 1 + -[1+ 0 ] + -[1+ 0 ] *+ (1 ⊕ n)  ↝⟨ flip trans +-left-identity ⟩
    + 0 ≡ -[1+ 0 ] *+ (1 ⊕ n)                   ↝⟨ flip ¬-0 ⊚ sym ⟩
    ¬ Negative (-[1+ 0 ] *+ (1 ⊕ n))            ↝⟨ _$ <0→*+suc<0 -[1+ 0 ] n _ ⟩□
    ⊥                                           □
  lemma -[1+ suc k ] =
    + 0 ≡ + 1 + -[1+ suc k ] *+ (2 ⊕ n)                 ↝⟨ flip trans (+-assoc (+ 1) {j = -[1+ suc k ]} {k = -[1+ suc k ] *+ (1 ⊕ n)}) ⟩
    + 0 ≡ + 1 + -[1+ suc k ] + -[1+ suc k ] *+ (1 ⊕ n)  ↔⟨⟩
    + 0 ≡ -[1+ k ] + -[1+ suc k ] *+ (1 ⊕ n)            ↝⟨ flip ¬-0 ⊚ sym ⟩
    ¬ Negative (-[1+ k ] + -[1+ suc k ] *+ (1 ⊕ n))     ↝⟨ _⊚ <0→<0→+<0 -[1+ k ] (-[1+ suc k ] *+ (1 ⊕ n)) _ ⟩
    ¬ Negative (-[1+ suc k ] *+ (1 ⊕ n))                ↝⟨ _$ <0→*+suc<0 -[1+ suc k ] n _ ⟩□
    ⊥                                                   □

-- It is not the case that ⌊_/2⌋ distributes over _+_ modulo 2 ⊕ n
-- (for any n).

¬⌊+/2⌋≡⌊/2⌋+⌊/2⌋mod2+ :
  ¬ (∀ i j → ⌊ i + j /2⌋ ≡ ⌊ i /2⌋ + ⌊ j /2⌋ mod 2 ⊕ n)
¬⌊+/2⌋≡⌊/2⌋+⌊/2⌋mod2+ {n = n} =
  (∀ i j → ⌊ i + j /2⌋ ≡ ⌊ i /2⌋ + ⌊ j /2⌋ mod 2 ⊕ n)  ↝⟨ (_$ (+ 1)) ⊚ (_$ (+ 1)) ⟩
  + 1 ≡ + 0 mod 2 ⊕ n                                  ↝⟨ ≡-mod-is-equivalence-relation (2 ⊕ n)
                                                            .Is-equivalence-relation.symmetric ⟩
  + 0 ≡ + 1 mod 2 ⊕ n                                  ↝⟨ 0≢1mod2+ n ⟩□
  ⊥                                                    □

------------------------------------------------------------------------
-- Finite cyclic groups

-- ℤ/[1+ n ]ℤ is the group of integers with addition modulo 1 + n (the
-- finite cyclic group of order 1 + n).

ℤ/[1+_]ℤ : ℕ → Group lzero
ℤ/[1+ n ]ℤ = λ where
    .Group.Carrier        → ℤ / (_≡_mod suc n)
    .Group.Carrier-is-set → Q./-is-set
    .Group._∘_            → _+′_
    .Group.id             → Q.[ + 0 ]
    .Group._⁻¹            → -′_
    .Group.left-identity  → left-identity
    .Group.right-identity → right-identity
    .Group.assoc          → assoc
    .Group.left-inverse   → left-inverse
    .Group.right-inverse  → right-inverse
  where
  _+′_ : ℤ / (_≡_mod suc n) → ℤ / (_≡_mod suc n) → ℤ / (_≡_mod suc n)
  _+′_ = Q.rec λ where
    .Q.[]ʳ i → _+_ i Q./-map λ j₁ j₂ →
      j₁ ≡ j₂ mod suc n            ↝⟨ +-cong (suc n) j₂ ⟩
      j₁ + i ≡ j₂ + i mod suc n    ↝⟨ ≡⇒↝ _ $ cong₂ (_≡_mod suc n) (+-comm j₁) (+-comm j₂) ⟩□
      i + j₁ ≡ i + j₂ mod suc n    □
    .Q.is-setʳ →
      Π-closure ext 2 λ _ →
      Q./-is-set
    .Q.[]-respects-relationʳ {x = i₁} {y = i₂} i₁≡i₂ →
      ⟨ext⟩ $ Q.elim-prop λ where
        .Q.is-propositionʳ _ → Q./-is-set
        .Q.[]ʳ j             →         $⟨ i₁≡i₂ ⟩
          i₁ ≡ i₂ mod suc n            ↝⟨ +-cong (suc n) i₂ ⟩
          i₁ + j ≡ i₂ + j mod suc n    ↝⟨ Q.[]-respects-relation ⟩□
          Q.[ i₁ + j ] ≡ Q.[ i₂ + j ]  □

  -′_ : ℤ / (_≡_mod suc n) → ℤ / (_≡_mod suc n)
  -′_ = -_ Q./-map λ i₁ i₂ →
    i₁ ≡ i₂ mod suc n      ↝⟨ negate-cong (suc n) i₂ ⟩□
    - i₁ ≡ - i₂ mod suc n  □

  left-identity : ∀ i → Q.[ + 0 ] +′ i ≡ i
  left-identity = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Q./-is-set
    .Q.[]ʳ _             → cong Q.[_] +-left-identity

  right-identity : ∀ i → i +′ Q.[ + 0 ] ≡ i
  right-identity = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Q./-is-set
    .Q.[]ʳ _             → cong Q.[_] +-right-identity

  assoc : ∀ i j k → (i +′ (j +′ k)) ≡ ((i +′ j) +′ k)
  assoc = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Π-closure ext 1 λ _ →
                           Π-closure ext 1 λ _ →
                           Q./-is-set
    .Q.[]ʳ i             → Q.elim-prop λ where
      .Q.is-propositionʳ _ → Π-closure ext 1 λ _ →
                             Q./-is-set
      .Q.[]ʳ _             → Q.elim-prop λ where
        .Q.is-propositionʳ _ → Q./-is-set
        .Q.[]ʳ _             → cong Q.[_] $ +-assoc i

  left-inverse : ∀ i → ((-′ i) +′ i) ≡ Q.[ + 0 ]
  left-inverse = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Q./-is-set
    .Q.[]ʳ i             → cong Q.[_] $ +-left-inverse i

  right-inverse : ∀ i → (i +′ (-′ i)) ≡ Q.[ + 0 ]
  right-inverse = Q.elim-prop λ where
    .Q.is-propositionʳ _ → Q./-is-set
    .Q.[]ʳ i             → cong Q.[_] $ +-right-inverse i

-- ℤ/[1+ n ]ℤ is cyclic.

ℤ/ℤ-cyclic : Cyclic ℤ/[1+ n ]ℤ
ℤ/ℤ-cyclic {n = n} =
  ∣ Q.[ + 1 ]
  , (Q.elim-prop λ where
       .Q.is-propositionʳ _ → T.truncation-is-proposition
       .Q.[]ʳ i             →
         ∣ i
         , (Q.[ i ]           ≡⟨ cong Q.[_] $ sym $ *-left-identity i ⟩
            Q.[ + 1 ⊛ i ]     ≡⟨ lemma i ⟩∎
            Q.[ + 1 ] ℤ/.^ i  ∎)
         ∣)
  ∣
  where
  module ℤ/ = Group ℤ/[1+ n ]ℤ

  *+-lemma : ∀ n → Q.[ + 1 *+ n ] ≡ Q.[ + 1 ] ℤ/.^+ n
  *+-lemma zero    = refl _
  *+-lemma (suc n) =
    Q.[ + 1 *+ suc n ]                ≡⟨⟩
    Q.[ + 1 ] ℤ/.∘ Q.[ + 1 *+ n ]     ≡⟨ cong (Q.[ + 1 ] ℤ/.∘_) $ *+-lemma n ⟩∎
    Q.[ + 1 ] ℤ/.∘ Q.[ + 1 ] ℤ/.^+ n  ∎

  lemma : ∀ i → Q.[ + 1 ⊛ i ] ≡ Q.[ + 1 ] ℤ/.^ i
  lemma (+ n)    = *+-lemma n
  lemma -[1+ n ] =
    Q.[ + 1 ⊛ -[1+ n ] ]           ≡⟨⟩
    Q.[ -[ 1 ] *+ suc n ]          ≡⟨ cong Q.[_] $ sym $ ℤG.^+⁻¹ {p = + 1} (suc n) ⟩
    Q.[ - (+ 1 *+ suc n) ]         ≡⟨⟩
    Q.[ + 1 *+ suc n ] ℤ/.⁻¹       ≡⟨ cong ℤ/._⁻¹ $ *+-lemma (suc n) ⟩
    (Q.[ + 1 ] ℤ/.^+ suc n) ℤ/.⁻¹  ≡⟨ ℤ/.^+⁻¹ {p = Q.[ + 1 ]} (suc n) ⟩
    (Q.[ + 1 ] ℤ/.⁻¹) ℤ/.^+ suc n  ≡⟨⟩
    Q.[ + 1 ] ℤ/.^ -[1+ n ]        ∎

-- ℤ/[1+ n ]ℤ is abelian.

ℤ/ℤ-abelian : Abelian ℤ/[1+ n ]ℤ
ℤ/ℤ-abelian = Cyclic→Abelian ℤ/[1+ _ ]ℤ ℤ/ℤ-cyclic

-- For finite cyclic groups of order at least 2 the number 0 is not
-- equal to 1.
--
-- The proof uses propositional extensionality.

ℤ/ℤ-0≢1 :
  ∀ n →
  _≢_ {A = Group.Carrier ℤ/[1+ suc n ]ℤ}
    Q.[ + 0 ] Q.[ + 1 ]
ℤ/ℤ-0≢1 n =
  Stable-¬
    [ Q.[ + 0 ] ≡ Q.[ + 1 ]  ↔⟨ inverse $
                                Q.related≃[equal]
                                  prop-ext
                                  (≡-mod-is-equivalence-relation (2 P.+ n))
                                  T.truncation-is-proposition ⟩
      (+ 0 ≡ + 1 mod 2 ⊕ n)  ↝⟨ 0≢1mod2+ n ⟩□
      ⊥                      □
    ]

-- If any element in ℤ/2ℤ is added to itself we get 0.

private
  module ℤ/2ℤ = Group ℤ/[1+ 1 ]ℤ

ℤ/2ℤ-+≡0 : ∀ i → i ℤ/2ℤ.∘ i ≡ ℤ/2ℤ.id
ℤ/2ℤ-+≡0 = Q.elim-prop λ where
  .Q.is-propositionʳ _ → Q./-is-set
  .Q.[]ʳ i → Q.[]-respects-relation
    ∣ i
    , (i + i          ≡⟨ cong (_+_ i) $ sym +-right-identity ⟩
       i + (i + + 0)  ≡⟨⟩
       i *+ 2         ≡⟨ sym +-left-identity ⟩∎
       + 0 + i *+ 2   ∎)
    ∣


text:
import Structure.Logic.Classical.NaturalDeduction

module Structure.Logic.Classical.PredicateBoundedQuantification {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)

open import Functional hiding (Domain)
open import Lang.Instance
import      Lvl
open import Type.Dependent

-- Bounded universal quantifier
∀ₚ : (Domain → Formula) → (Domain → Formula) → Formula
∀ₚ(B)(P) = ∀ₗ(x ↦ B(x) ⟶ P(x))

[∀ₚ]-intro : ∀{B}{P} → (∀{x} → Proof(B(x)) → Proof(P(x))) → Proof(∀ₚ(B)(P))
[∀ₚ]-intro {B}{P} proof =
  ([∀].intro(\{x} →
    ([→].intro(bx ↦
      proof{x}(bx)
    ))
  ))

[∀ₚ]-elim : ∀{B}{P} → Proof(∀ₚ(B)(P)) → ∀{x} → Proof(B(x)) → Proof(P(x))
[∀ₚ]-elim {B}{P} allSφ {x} bx =
  ([→].elim
    ([∀].elim allSφ{x})
    (bx)
  )

-- Bounded existential quantifier
∃ₚ : (Domain → Formula) → (Domain → Formula) → Formula
∃ₚ(B)(P) = ∃ₗ(x ↦ B(x) ∧ P(x))

[∃ₚ]-intro : ∀{B}{P}{x} → Proof(B(x)) → Proof(P(x)) → Proof(∃ₚ(B)(P))
[∃ₚ]-intro {B}{P}{x} bx φx =
  ([∃].intro{_}
    {x}
    ([∧].intro
      (bx)
      (φx)
    )
  )

[∃ₚ]-elim : ∀{B}{P₁}{P₂} → (∀{x} → Proof(B(x)) → Proof(P₁(x)) → Proof(P₂)) → Proof(∃ₚ(B)(P₁)) → Proof(P₂)
[∃ₚ]-elim {B}{P₁}{P₂} proof existence =
  ([∃].elim{_}{P₂}
    (\{x} → conj ↦ (
      (proof
        {x}
        ([∧].elimₗ(conj))
        ([∧].elimᵣ(conj))
      )
    ))
    (existence)
  )

[∃ₚ]-to-[∃ₗ] : ∀{B P} → Proof(∃ₚ(B)(P)) → Proof(∃ₗ(P))
[∃ₚ]-to-[∃ₗ] ebp = [∃ₚ]-elim (\{x} → bx ↦ px ↦ [∃].intro px) (ebp)

[∃ₚ]-witness : ∀{B P} → ⦃ _ : Proof(∃ₚ B P) ⦄ → Domain
[∃ₚ]-witness ⦃ proof ⦄ = [∃]-witness ⦃ proof ⦄

[∃ₚ]-bound : ∀{B P} → ⦃ p : Proof(∃ₚ B P) ⦄ → Proof(B([∃ₚ]-witness{B}{P} ⦃ p ⦄))
[∃ₚ]-bound ⦃ proof ⦄ = [∧].elimₗ([∃]-proof ⦃ proof ⦄)

[∃ₚ]-proof : ∀{B P} → ⦃ p : Proof(∃ₚ B P) ⦄ → Proof(P([∃ₚ]-witness{B}{P} ⦃ p ⦄))
[∃ₚ]-proof ⦃ proof ⦄ = [∧].elimᵣ([∃]-proof ⦃ proof ⦄)

Uniqueₚ : (Domain → Formula) → (Domain → Formula) → Formula
Uniqueₚ(B)(P) = ∀ₚ(B)(x ↦ ∀ₚ(B)(y ↦ (P(x) ∧ P(y)) ⟶ (x ≡ y)))

-- Bounded unique existential quantifier
∃ₚ! : (Domain → Formula) → (Domain → Formula) → Formula
∃ₚ!(B)(P) = ((∃ₚ(B) P) ∧ Uniqueₚ(B)(P))

[∃ₚ!]-witness : ∀{B P} → ⦃ _ : Proof(∃ₚ! B P) ⦄ → Domain
[∃ₚ!]-witness ⦃ proof ⦄ = [∃ₚ]-witness ⦃ [∧].elimₗ proof ⦄

[∃ₚ!]-bound : ∀{B P} → ⦃ p : Proof(∃ₚ! B P) ⦄ → Proof(B([∃ₚ!]-witness{B}{P} ⦃ p ⦄))
[∃ₚ!]-bound ⦃ proof ⦄ = [∃ₚ]-bound ⦃ [∧].elimₗ proof ⦄

[∃ₚ!]-proof : ∀{B P} → ⦃ p : Proof(∃ₚ! B P) ⦄ → Proof(P([∃ₚ!]-witness{B}{P} ⦃ p ⦄))
[∃ₚ!]-proof ⦃ proof ⦄ = [∃ₚ]-proof ⦃ [∧].elimₗ proof ⦄

postulate [∃ₚ!]-unique : ∀{B P} → ⦃ p : Proof(∃ₚ! B P) ⦄ → Proof(∀ₗ(x ↦ P(x) ⟶ (x ≡ [∃ₚ!]-witness{B}{P} ⦃ p ⦄)))

boundedClassicalLogicSignature : (Domain → Formula) → Structure.Logic.Classical.NaturalDeduction.Domained.Predicate.Signature {ℓₗ} {Formula} {ℓₘₗ} (Proof) {ℓₒ} (Domain)
boundedClassicalLogicSignature(B) =
  record{
    ∀ₗ = ∀ₚ(B) ;
    ∃ₗ = ∃ₚ(B)
  }

-- TODO: This should make it possible to embed a theory inside of another theory (e.g. group theory in set theory), but does not work. How should I formulate something like this for it to work?
{-
module _ (B : Domain → Formula) {ℓₒ₂} {Domain₂} (dom : Domain₂ → Domain) (dom-proof : ∀{x} → Proof(B(dom(x)))) (dom⁻¹ : Domain → Domain₂) where
  instance
    boundedPredEqSignature : Structure.Logic.Classical.NaturalDeduction.Domained.Predicate.Signature {ℓₗ} {Formula} {ℓₘₗ} (Proof) {ℓₒ₂} (Domain₂)
    boundedPredEqSignature =
      record{
        ∀ₗ = P ↦ ∀ₗ(x ↦ B(x) ⟶ P(x)) ;
        ∃ₗ = P ↦ ∃ₚ(B) (x ↦ P(dom⁻¹ x))
      }

  instance
    boundedPredEqTheory : Structure.Logic.Classical.NaturalDeduction.Domained.Predicate.Theory {ℓₗ} {Formula} {ℓₘₗ} (Proof) {ℓₒ₂} (Domain₂) ⦃ boundedPredEqSignature ⦄
    boundedPredEqTheory =
      record{
        universalQuantification =
          record{
            intro = \{P} → proof ↦ [∀ₚ]-intro{B}{P ∘ dom⁻¹} (\{x} → bx ↦ proof{dom⁻¹ x}) ;
            elim  = \{P} → ap ↦ \{x} → [∀ₚ]-elim ap{dom x} (dom-proof{x})
          } ;
        existentialQuantification =
          record{
            intro = \{P}{a} → pa ↦ [∃ₚ]-intro{B}{P}{dom a} (dom-proof{a}) pa;
            elim  = \{P}{Z} → axpxz ↦ ep ↦ [∃ₚ]-elim{B}{P} (\{x} → bx ↦ px ↦ axpxz{dom⁻¹ x}(px)) ep
          }
      }
-}

{-
module _ (B : Domain → Formula) {ℓₒ₂} {Domain₂} (morph : (x : Domain) → Proof(B(x)) → Domain₂) (morph₂ : Domain₂ → Domain) (ident : ∀{x} → Proof(B(x)) → morph(morph₂(x))(proof) ≡ x) (proof : ∀{x} → Proof(B(morph₂(x)))) where
  instance
    boundedPredEqSignature : Structure.Logic.Classical.NaturalDeduction.Domained.Predicate.Signature {ℓₗ} {Formula} {ℓₘₗ} (Proof) {ℓₒ₂} (Domain₂)
    boundedPredEqSignature =
      record{
        ∀ₗ = ∀ₚ(B) ;
        ∃ₗ = ∃ₚ(B)
      }

  instance
    boundedPredEqTheory : Structure.Logic.Classical.NaturalDeduction.Domained.Predicate.Theory {ℓₗ} {Formula} {ℓₘₗ} (Proof) {ℓₒ₂} (Domain₂) ⦃ boundedPredEqSignature ⦄
    boundedPredEqTheory =
      record{
        universalQuantification =
          record{
            intro = \{P} → proof ↦ [∀ₚ]-intro{B}{P ∘ dom⁻¹} (\{x} → bx ↦ proof{dom⁻¹ x}) ;
            elim  = \{P} → ap ↦ \{x} → [∀ₚ]-elim ap{dom x} (dom-proof{x})
          } ;
        existentialQuantification =
          record{
            intro = \{P}{a} → pa ↦ [∃ₚ]-intro{B}{P}{dom a} (dom-proof{a}) pa;
            elim  = \{P}{Z} → axpxz ↦ ep ↦ [∃ₚ]-elim{B}{P} (\{x} → bx ↦ px ↦ axpxz{dom⁻¹ x}(px)) ep
          }
      }
-}

{-
module _ (B : Domain → Formula) where
  instance
    boundedPredEqSignature2 : Structure.Logic.Classical.NaturalDeduction.Domained.Predicate.Signature {ℓₗ} {Formula} {ℓₘₗ} (Proof) {ℓₒ} (Σ B Domain)
    boundedPredEqSignature2 =
      record{
        ∀ₗ = P ↦ ∀ₚ(B)(P) ;
        ∃ₗ = P ↦ ∃ₚ(B)(P)
      }

  instance
    boundedPredEqTheory2 : Structure.Logic.Classical.NaturalDeduction.Domained.Predicate.Theory {ℓₗ} {Formula} {ℓₘₗ} (Proof) {ℓₒ} (Σ B Domain) ⦃ boundedPredEqSignature2 ⦄
    boundedPredEqTheory2 =
      record{
        universalQuantification =
          record{
            intro = \{P} → proof ↦ [∀ₚ]-intro{B}{P} (\{x} → bx ↦ proof{dom⁻¹ x}) ;
            elim  = \{P} → ap ↦ \{x} → [∀ₚ]-elim ap{x} (dom-proof{x})
          } ;
        existentialQuantification =
          record{
            intro = \{P}{a} → pa ↦ [∃ₚ]-intro{B}{P}{dom a} (dom-proof{a}) pa;
            elim  = \{P}{Z} → axpxz ↦ ep ↦ [∃ₚ]-elim{B}{P} (\{x} → bx ↦ px ↦ axpxz{dom⁻¹ x}(px)) ep
          }
      }
-}


text:
-- Andreas, 2013-10-21
-- Test case for CheckInternal extracted from The Agda standard library
-- Propositional (intensional) equality

module FunExt where

open import Common.Level
open import Common.Equality

Extensionality : (a b : Level) → Set _
Extensionality a b =
  {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
  (∀ x → f x ≡ g x) → f ≡ g

-- Functional extensionality implies a form of extensionality for
-- Π-types.

∀-extensionality :
  ∀ {a b} →
  Extensionality a (lsuc b) →
  {A : Set a} (B₁ B₂ : A → Set b) →
  (∀ x → B₁ x ≡ B₂ x) → (∀ x → B₁ x) ≡ (∀ x → B₂ x)
∀-extensionality ext B₁ B₂ B₁≡B₂ with ext B₁≡B₂
∀-extensionality ext B .B  B₁≡B₂ | refl = refl