text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the case expressions can be used
------------------------------------------------------------------------

module README.Case where

open import Data.Fin   hiding (pred)
open import Data.Maybe hiding (from-just)
open import Data.Nat   hiding (pred)
open import Function

-- Some simple examples.

empty : ∀ {a} {A : Set a} → Fin 0 → A
empty i = case i of λ()

pred : ℕ → ℕ
pred n = case n of λ
  { zero    → zero
  ; (suc n) → n
  }

from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just A x
from-just x = case x return From-just _ of λ
  { (just x) → x
  ; nothing  → _
  }

-- Note that some natural uses of case are rejected by the termination
-- checker:
--
-- plus : ℕ → ℕ → ℕ
-- plus m n = case m of λ
--   { zero    → n
--   ; (suc m) → suc (plus m n)
--   }

ext: agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.FunctorCategory where

open import Data.Product

open import Categories.Category
import Categories.Functor as Cat
open import Categories.Functor hiding (equiv; id; _∘_; _≡_)
open import Categories.NaturalTransformation
open import Categories.Product
open import Categories.Square

Functors : ∀ {o ℓ e} {o′ ℓ′ e′} → Category o ℓ e → Category o′ ℓ′ e′ → Category _ _ _
Functors C D = record
  { Obj = Functor C D
  ; _⇒_ = NaturalTransformation
  ; _≡_ = _≡_
  ; _∘_ = _∘₁_
  ; id = id
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} → assoc₁ {X = f} {g} {h}
  ; identityˡ = λ {_} {_} {f} → identity₁ˡ {X = f}
  ; identityʳ = λ {_} {_} {f} → identity₁ʳ {X = f}
  ; equiv = λ {F} {G} → equiv {F = F} {G = G}
  ; ∘-resp-≡ = λ {_} {_} {_} {f} {h} {g} {i} → ∘₁-resp-≡ {f = f} {h} {g} {i}
  }

eval : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e}{D : Category o′ ℓ′ e′} → Functor (Product (Functors C D) C) D
eval {C = C} {D = D} =
    record {
      F₀ = λ x → let F , c = x in F₀ F c;
      F₁ = λ { {F , c₁} {G , c₂} (ε , f) → F₁ G f D.∘ η ε _};
      identity = λ { {F , c} → begin
                                 F₁ F C.id D.∘ D.id ↓⟨ D.identityʳ ⟩
                                 F₁ F C.id          ↓⟨ identity F ⟩
                                 D.id               ∎};
      homomorphism = λ { {F , c₁} {G , c₂} {H , c₃} {ε₁ , f₁} {ε₂ , f₂} →
         begin
           F₁ H (f₂ C.∘ f₁) D.∘ η ε₂ c₁ D.∘ η ε₁ c₁        ↑⟨ D.assoc ⟩
           (F₁ H (f₂ C.∘ f₁) D.∘ η ε₂ c₁) D.∘ η ε₁ c₁
              ↓⟨ D.∘-resp-≡ˡ (begin
                                F₁ H (C [ f₂ ∘ f₁ ]) D.∘ η ε₂ c₁  ↓⟨ D.∘-resp-≡ˡ (homomorphism H) ⟩
                                (F₁ H f₂ D.∘ F₁ H f₁) D.∘ η ε₂ c₁ ↓⟨ D.assoc ⟩
                                F₁ H f₂ D.∘ F₁ H f₁ D.∘ η ε₂ c₁   ↑⟨ D.∘-resp-≡ʳ (commute ε₂ f₁) ⟩
                                F₁ H f₂ D.∘ η ε₂ c₂ D.∘ F₁ G f₁   ↑⟨ D.assoc ⟩
                                (F₁ H f₂ D.∘ η ε₂ c₂) D.∘ F₁ G f₁ ∎)
               ⟩
           ((F₁ H f₂ D.∘ η ε₂ c₂) D.∘ F₁ G f₁) D.∘ η ε₁ c₁ ↓⟨ D.assoc ⟩
           (F₁ H f₂ D.∘ η ε₂ c₂) D.∘ F₁ G f₁ D.∘ η ε₁ c₁   ∎ };
      F-resp-≡ = λ { {F , c₁} {G , c₂} {ε₁ , f₁} {ε₂ , f₂} (ε₁≡ε₂ , f₁≡f₂)
                        → D.∘-resp-≡ (F-resp-≡ G f₁≡f₂) ε₁≡ε₂} }
  where
    module C = Category C
    module D = Category D

    open Functor
    open NaturalTransformation
    open D.HomReasoning

Cat[-∘_] : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃} {A : Category o₁ ℓ₁ e₁} {B : Category o₂ ℓ₂ e₂}
             {C : Category o₃ ℓ₃ e₃} -> Functor A B -> Functor (Functors B C) (Functors A C)
Cat[-∘_] {C = C} r = record
  { F₀ = λ X → X Cat.∘ r
  ; F₁ = λ η → η ∘ʳ r
  ; identity = C.Equiv.refl
  ; homomorphism = C.Equiv.refl
  ; F-resp-≡ = λ x → x
  }
 where
   module C = Category C

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma

open import Sec2preliminaries

module Sec3hedberg where

-- Lemma 3.2
discr→pathHasConst : {X : Type} → has-dec-eq X → pathHasConst X
discr→pathHasConst dec x₁ x₂ with (dec x₁ x₂)
discr→pathHasConst dec x₁ x₂ | inl p  = (λ _ → p) , (λ _ _ → idp)
discr→pathHasConst dec x₁ x₂ | inr np = idf _ , λ p → Empty-elim (np p)

-- Lemma 3.3
pathHasConst→isSet : {X : Type} → pathHasConst X → is-set X
pathHasConst→isSet {X} pc x₁ x₂ = all-paths-is-prop paths-equal where
  claim : (y₁ y₂ : X) → (p : y₁ == y₂) → p == ! (fst (pc _ _) idp) ∙ fst (pc _ _) p
  claim x₁ .x₁ idp = ! (!-inv-l (fst (pc x₁ x₁) idp))
  paths-equal : (p₁ p₂ : x₁ == x₂) → p₁ == p₂
  paths-equal p₁ p₂ =
    p₁                                      =⟨ claim _ _ p₁ ⟩
    ! (fst (pc _ _) idp) ∙ fst (pc _ _) p₁  =⟨ ap (λ q → (! (fst (pc x₁ x₁) idp)) ∙ q) (snd (pc _ _) p₁ p₂) ⟩ -- whiskering
    ! (fst (pc _ _) idp) ∙ fst (pc _ _) p₂  =⟨ ! (claim _ _ p₂) ⟩
    p₂                                      ∎

-- Theorem 3.1
hedberg : {X : Type} → has-dec-eq X → is-set X
hedberg = pathHasConst→isSet ∘ discr→pathHasConst

-- Definition 3.4
stable : Type → Type
stable X = ¬ (¬ X) → X

separated : Type → Type
separated X = (x₁ x₂ : X) → stable (x₁ == x₂)

-- Lemma 3.5
sep→set : {X : Type} → (separated X) → ({x₁ x₂ : X} → Funext {¬ (x₁ == x₂)} {Empty}) → is-set X
sep→set {X} sep ⊥-funext = pathHasConst→isSet isPc where
  isPc : pathHasConst X
  isPc x₁ x₂ = f , c where
    f : x₁ == x₂ → x₁ == x₂
    f = (sep x₁ x₂) ∘ (λ p np → np p)
    c : const f
    c p₁ p₂ =
      f p₁                        =⟨ idp ⟩
      (sep x₁ x₂) (λ np → np p₁)  =⟨ ap (sep x₁ x₂)
                                     (⊥-funext _ _ λ np → Empty-elim {A = λ _ → np p₁ == np p₂} (np p₁)) ⟩
      (sep x₁ x₂) (λ np → np p₂)  =⟨ idp ⟩
      f p₂                        ∎

-- Definition 3.6
postulate
  Trunc : Type → Type
  h-tr : (X : Type) → is-prop (Trunc X)
  ∣_∣ : {X : Type} → X → Trunc X
  rec : {X : Type} → {P : Type} → (is-prop P) → (X → P) → Trunc X → P

-- the propositional β rule is derivable:
trunc-β : {X : Type} → {P : Type} → (pp : is-prop P) → (f : X → P) → (x : X) → rec pp f ∣ x ∣ == f x
trunc-β pp f x = prop-has-all-paths pp _ _

-- Lemma 3.7
module _ (X : Type) (P : Trunc X → Type) (h : (z : Trunc X) → is-prop (P z)) (k : (x : X) → P(∣ x ∣)) where
  total : Type
  total = Σ (Trunc X) P

  j : X → total
  j x = ∣ x ∣ , k x

  total-prop : is-prop total
  total-prop = Σ-level (h-tr X) h

  total-map : Trunc X → total
  total-map = rec total-prop j

  induction : (z : Trunc X) → P z
  induction z = transport P (prop-has-all-paths (h-tr _) _ _) (snd (total-map z))

-- comment: Trunc is functorial
trunc-functorial : {X Y : Type} → (X → Y) → (Trunc X → Trunc Y)
trunc-functorial {X} {Y} f = rec (h-tr Y) (∣_∣ ∘ f)

-- Theorem 3.8
impred : {X : Type} → (Trunc X ↔₀₁ ((P : Type) → (is-prop P) → (X → P) → P))
impred {X} = one , two where
  one : Trunc X → (P : Type) → (is-prop P) → (X → P) → P
  one z P p-prop f = rec p-prop f z
  two : ((P : Type) → (is-prop P) → (X → P) → P) → Trunc X
  two k = k (Trunc X) (h-tr _) ∣_∣

-- Definition 3.9
splitSup : Type → Type
splitSup X = Trunc X → X

hseparated : Type → Type
hseparated X = (x₁ x₂ : X) → splitSup (x₁ == x₂)

-- Theorem 3.10
set-characterizations : {X : Type} → (pathHasConst X → is-set X)
                                   × ((is-set X → hseparated X)
                                   × (hseparated X → pathHasConst X))
set-characterizations {X} = one , two , three where
  one : pathHasConst X → is-set X
  one = pathHasConst→isSet
  two : is-set X → hseparated X
  two h = λ x₁ x₂ → rec (h x₁ x₂) (idf _)
  three : hseparated X → pathHasConst X
  three hsep x₁ x₂ = f , c where
    f = (hsep _ _) ∘ ∣_∣
    c = λ p₁ p₂ → f p₁              =⟨ idp ⟩
                  hsep _ _ (∣ p₁ ∣)  =⟨ ap (hsep _ _) (prop-has-all-paths (h-tr _) _ _) ⟩
                  hsep _ _ (∣ p₂ ∣)  =⟨ idp ⟩
                  f p₂              ∎

-- The rest of this section is only a replication of the arguments that we have given so far (for that reason, the proofs are not given in the article).
-- They do not directly follow from the statements that we have proved before, but they directly imply them.
-- Of course, replication of arguments is not a good style for a formalization -
-- we chose this "disadvantageous" order purely as we believe it led to a better presentation in the article.

-- Lemma 3.11
pathHasConst→isSet-local : {X : Type} → {x₀ : X} → ((y : X) → hasConst (x₀ == y)) → (y : X) → is-prop (x₀ == y)
pathHasConst→isSet-local {X} {x₀} pc y = all-paths-is-prop paths-equal  where
  claim : (y : X) → (p : x₀ == y) → p == ! (fst (pc _) idp) ∙ fst (pc _) p
  claim .x₀ idp = ! (!-inv-l (fst (pc _) idp))
  paths-equal : (p₁ p₂ : x₀ == y) → p₁ == p₂
  paths-equal p₁ p₂ =
    p₁                                  =⟨ claim _ p₁ ⟩
    ! (fst (pc _) idp) ∙ fst (pc _) p₁  =⟨ ap (λ q → (! (fst (pc x₀) idp)) ∙ q) (snd (pc y) p₁ p₂) ⟩ -- whiskering
    ! (fst (pc _) idp) ∙ fst (pc _) p₂  =⟨ ! (claim _ p₂) ⟩
    p₂                                  ∎

-- Theorem 3.12
hedberg-local : {X : Type} → {x₀ : X} → ((y : X) → (x₀ == y) + ¬(x₀ == y)) → (y : X) → is-prop (x₀ == y)
hedberg-local {X} {x₀} dec = pathHasConst→isSet-local local-pathHasConst where
  local-pathHasConst : (y : X) → hasConst (x₀ == y)
  local-pathHasConst y with (dec y)
  local-pathHasConst y₁ | inl p  = (λ _ → p) , (λ _ _ → idp)
  local-pathHasConst y₁ | inr np = idf _ , (λ p → Empty-elim (np p))

-- Lemma 3.13
sep→set-local : {X : Type} → {x₀ : X} → ((y : X) → stable (x₀ == y)) → ({y : X} → Funext {¬ (x₀ == y)} {Empty}) → (y : X) → is-prop (x₀ == y)
sep→set-local {X} {x₀} sep ⊥-funext = pathHasConst→isSet-local is-pathHasConst where
  is-pathHasConst : (y : X) → hasConst (x₀ == y)
  is-pathHasConst y = f , c where
    f : x₀ == y → x₀ == y
    f = (sep y) ∘ (λ p np → np p)
    c : const f
    c p₁ p₂ =
      f p₁                    =⟨ idp ⟩
      (sep _) (λ np → np p₁)  =⟨ ap (sep _)
                                     (⊥-funext _ _ λ np → Empty-elim {A = λ _ → np p₁ == np p₂} (np p₁)) ⟩
      (sep _) (λ np → np p₂)  =⟨ idp ⟩
      f p₂ ∎

-- Theorem 3.14
set-characterizations-local : {X : Type} → {x₀ : X} →
  (((y : X) → hasConst (x₀ == y)) → (y : X) → is-prop (x₀ == y))
  × ((((y : X) → is-prop (x₀ == y)) → (y : X) → splitSup (x₀ == y))
  × (((y : X) → splitSup (x₀ == y)) → (y : X) → hasConst (x₀ == y)))
set-characterizations-local {X} {x₀} = one , two , three where
  one = pathHasConst→isSet-local
  two : ((y : X) → is-prop (x₀ == y)) → (y : X) → splitSup (x₀ == y)
  two h y = rec (h y) (idf _)
  three : ((y : X) → splitSup (x₀ == y)) → (y : X) → hasConst (x₀ == y)
  three hsep y = f , c where
    f = (hsep _) ∘ ∣_∣
    c = λ p₁ p₂ →
      f p₁           =⟨ idp ⟩
      (hsep _) ∣ p₁ ∣ =⟨ ap (hsep _) (prop-has-all-paths (h-tr _) _ _) ⟩
      (hsep _) ∣ p₂ ∣ =⟨ idp ⟩
      f p₂           ∎

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Raw where

open import Cubical.Relation.Binary.Base public
open import Cubical.Relation.Binary.Raw.Definitions public
open import Cubical.Relation.Binary.Raw.Structures public
open import Cubical.Relation.Binary.Raw.Bundles public


text:
{-# OPTIONS --allow-unsolved-metas #-}
postulate
  Nat : Set

variable
  A : _
  F : _ → _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to Fin, and operations making use of these
-- properties (or other properties not available in Data.Fin)
------------------------------------------------------------------------

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

module Data.Fin.Properties where

open import Category.Applicative using (RawApplicative)
open import Category.Functor using (RawFunctor)
open import Data.Bool.Base using (Bool; true; false; not; _∧_; _∨_)
open import Data.Empty using (⊥-elim)
open import Data.Fin.Base
open import Data.Fin.Patterns
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; _∸_)
import Data.Nat.Properties as ℕₚ
open import Data.Unit using (tt)
open import Data.Product using (∃; ∃₂; ∄; _×_; _,_; map; proj₁; uncurry; <_,_>)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Sum.Properties using ([,]-map-commute; [,]-∘-distr)
open import Function.Base using (_∘_; id; _$_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Function.Injection using (_↣_)
open import Relation.Binary as B hiding (Decidable)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; sym; trans; cong; subst; module ≡-Reasoning)
open import Relation.Nullary.Decidable as Dec using (map′)
open import Relation.Nullary.Reflects
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary
  using (Reflects; ofʸ; ofⁿ; Dec; _because_; does; proof; yes; no; ¬_)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Unary as U
  using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
open import Relation.Unary.Properties using (U?)

------------------------------------------------------------------------
-- Fin
------------------------------------------------------------------------

¬Fin0 : ¬ Fin 0
¬Fin0 ()

------------------------------------------------------------------------
-- Properties of _≡_
------------------------------------------------------------------------

suc-injective : ∀ {o} {m n : Fin o} → Fin.suc m ≡ suc n → m ≡ n
suc-injective refl = refl

infix 4 _≟_

_≟_ : ∀ {n} → B.Decidable {A = Fin n} _≡_
zero  ≟ zero  = yes refl
zero  ≟ suc y = no λ()
suc x ≟ zero  = no λ()
suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y)

------------------------------------------------------------------------
-- Structures

≡-isDecEquivalence : ∀ {n} → IsDecEquivalence (_≡_ {A = Fin n})
≡-isDecEquivalence = record
  { isEquivalence = P.isEquivalence
  ; _≟_           = _≟_
  }

------------------------------------------------------------------------
-- Bundles

≡-preorder : ℕ → Preorder _ _ _
≡-preorder n = P.preorder (Fin n)

≡-setoid : ℕ → Setoid _ _
≡-setoid n = P.setoid (Fin n)

≡-decSetoid : ℕ → DecSetoid _ _
≡-decSetoid n = record
  { isDecEquivalence = ≡-isDecEquivalence {n}
  }

------------------------------------------------------------------------
-- toℕ
------------------------------------------------------------------------

toℕ-injective : ∀ {n} {i j : Fin n} → toℕ i ≡ toℕ j → i ≡ j
toℕ-injective {zero}  {}      {}      _
toℕ-injective {suc n} {zero}  {zero}  eq = refl
toℕ-injective {suc n} {suc i} {suc j} eq =
  cong suc (toℕ-injective (cong ℕ.pred eq))

toℕ-strengthen : ∀ {n} (i : Fin n) → toℕ (strengthen i) ≡ toℕ i
toℕ-strengthen zero    = refl
toℕ-strengthen (suc i) = cong suc (toℕ-strengthen i)

toℕ-raise : ∀ {m} n (i : Fin m) → toℕ (raise n i) ≡ n ℕ.+ toℕ i
toℕ-raise zero    i = refl
toℕ-raise (suc n) i = cong suc (toℕ-raise n i)

toℕ<n : ∀ {n} (i : Fin n) → toℕ i ℕ.< n
toℕ<n zero    = s≤s z≤n
toℕ<n (suc i) = s≤s (toℕ<n i)

toℕ≤pred[n] : ∀ {n} (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
toℕ≤pred[n] zero                 = z≤n
toℕ≤pred[n] (suc {n = suc n} i)  = s≤s (toℕ≤pred[n] i)

-- A simpler implementation of toℕ≤pred[n],
-- however, with a different reduction behavior.
-- If no one needs the reduction behavior of toℕ≤pred[n],
-- it can be removed in favor of toℕ≤pred[n]′.
toℕ≤pred[n]′ : ∀ {n} (i : Fin n) → toℕ i ℕ.≤ ℕ.pred n
toℕ≤pred[n]′ i = ℕₚ.<⇒≤pred (toℕ<n i)

------------------------------------------------------------------------
-- fromℕ
------------------------------------------------------------------------

toℕ-fromℕ : ∀ n → toℕ (fromℕ n) ≡ n
toℕ-fromℕ zero    = refl
toℕ-fromℕ (suc n) = cong suc (toℕ-fromℕ n)

fromℕ-toℕ : ∀ {n} (i : Fin n) → fromℕ (toℕ i) ≡ strengthen i
fromℕ-toℕ zero    = refl
fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)

------------------------------------------------------------------------
-- fromℕ<
------------------------------------------------------------------------

fromℕ<-toℕ : ∀ {m} (i : Fin m) (i<m : toℕ i ℕ.< m) → fromℕ< i<m ≡ i
fromℕ<-toℕ zero    (s≤s z≤n)       = refl
fromℕ<-toℕ (suc i) (s≤s (s≤s m≤n)) = cong suc (fromℕ<-toℕ i (s≤s m≤n))

toℕ-fromℕ< : ∀ {m n} (m<n : m ℕ.< n) → toℕ (fromℕ< m<n) ≡ m
toℕ-fromℕ< (s≤s z≤n)       = refl
toℕ-fromℕ< (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ< (s≤s m<n))

-- fromℕ is a special case of fromℕ<.
fromℕ-def : ∀ n → fromℕ n ≡ fromℕ< ℕₚ.≤-refl
fromℕ-def zero    = refl
fromℕ-def (suc n) = cong suc (fromℕ-def n)

------------------------------------------------------------------------
-- fromℕ<″
------------------------------------------------------------------------

fromℕ<≡fromℕ<″ : ∀ {m n} (m<n : m ℕ.< n) (m<″n : m ℕ.<″ n) →
                 fromℕ< m<n ≡ fromℕ<″ m m<″n
fromℕ<≡fromℕ<″ (s≤s z≤n)       (ℕ.less-than-or-equal refl) = refl
fromℕ<≡fromℕ<″ (s≤s (s≤s m<n)) (ℕ.less-than-or-equal refl) =
  cong suc (fromℕ<≡fromℕ<″ (s≤s m<n) (ℕ.less-than-or-equal refl))

toℕ-fromℕ<″ : ∀ {m n} (m<n : m ℕ.<″ n) → toℕ (fromℕ<″ m m<n) ≡ m
toℕ-fromℕ<″ {m} {n} m<n = begin
  toℕ (fromℕ<″ m m<n)  ≡⟨ cong toℕ (sym (fromℕ<≡fromℕ<″ (ℕₚ.≤″⇒≤ m<n) m<n)) ⟩
  toℕ (fromℕ< _)       ≡⟨ toℕ-fromℕ< (ℕₚ.≤″⇒≤ m<n) ⟩
  m ∎
  where open ≡-Reasoning

------------------------------------------------------------------------
-- cast
------------------------------------------------------------------------

toℕ-cast : ∀ {m n} .(eq : m ≡ n) (k : Fin m) → toℕ (cast eq k) ≡ toℕ k
toℕ-cast {n = suc n} eq zero    = refl
toℕ-cast {n = suc n} eq (suc k) = cong suc (toℕ-cast (cong ℕ.pred eq) k)

------------------------------------------------------------------------
-- Properties of _≤_
------------------------------------------------------------------------
-- Relational properties

≤-reflexive : ∀ {n} → _≡_ ⇒ (_≤_ {n})
≤-reflexive refl = ℕₚ.≤-refl

≤-refl : ∀ {n} → Reflexive (_≤_ {n})
≤-refl = ≤-reflexive refl

≤-trans : ∀ {n} → Transitive (_≤_ {n})
≤-trans = ℕₚ.≤-trans

≤-antisym : ∀ {n} → Antisymmetric _≡_ (_≤_ {n})
≤-antisym x≤y y≤x = toℕ-injective (ℕₚ.≤-antisym x≤y y≤x)

≤-total : ∀ {n} → Total (_≤_ {n})
≤-total x y = ℕₚ.≤-total (toℕ x) (toℕ y)

≤-irrelevant : ∀ {n} → Irrelevant (_≤_ {n})
≤-irrelevant = ℕₚ.≤-irrelevant

infix 4 _≤?_ _<?_

_≤?_ : ∀ {n} → B.Decidable (_≤_ {n})
a ≤? b = toℕ a ℕₚ.≤? toℕ b

_<?_ : ∀ {n} → B.Decidable (_<_ {n})
m <? n = suc (toℕ m) ℕₚ.≤? toℕ n

------------------------------------------------------------------------
-- Structures

≤-isPreorder : ∀ {n} → IsPreorder _≡_ (_≤_ {n})
≤-isPreorder = record
  { isEquivalence = P.isEquivalence
  ; reflexive     = ≤-reflexive
  ; trans         = ≤-trans
  }

≤-isPartialOrder : ∀ {n} → IsPartialOrder _≡_ (_≤_ {n})
≤-isPartialOrder = record
  { isPreorder = ≤-isPreorder
  ; antisym    = ≤-antisym
  }

≤-isTotalOrder : ∀ {n} → IsTotalOrder _≡_ (_≤_ {n})
≤-isTotalOrder = record
  { isPartialOrder = ≤-isPartialOrder
  ; total          = ≤-total
  }

≤-isDecTotalOrder : ∀ {n} → IsDecTotalOrder _≡_ (_≤_ {n})
≤-isDecTotalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  ; _≟_          = _≟_
  ; _≤?_         = _≤?_
  }

------------------------------------------------------------------------
-- Bundles

≤-preorder : ℕ → Preorder _ _ _
≤-preorder n = record
  { isPreorder = ≤-isPreorder {n}
  }

≤-poset : ℕ → Poset _ _ _
≤-poset n = record
  { isPartialOrder = ≤-isPartialOrder {n}
  }

≤-totalOrder : ℕ → TotalOrder _ _ _
≤-totalOrder n = record
  { isTotalOrder = ≤-isTotalOrder {n}
  }

≤-decTotalOrder : ℕ → DecTotalOrder _ _ _
≤-decTotalOrder n = record
  { isDecTotalOrder = ≤-isDecTotalOrder {n}
  }

------------------------------------------------------------------------
-- Properties of _<_
------------------------------------------------------------------------
-- Relational properties

<-irrefl : ∀ {n} → Irreflexive _≡_ (_<_ {n})
<-irrefl refl = ℕₚ.<-irrefl refl

<-asym : ∀ {n} → Asymmetric (_<_ {n})
<-asym = ℕₚ.<-asym

<-trans : ∀ {n} → Transitive (_<_ {n})
<-trans = ℕₚ.<-trans

<-cmp : ∀ {n} → Trichotomous _≡_ (_<_ {n})
<-cmp zero    zero    = tri≈ (λ())     refl  (λ())
<-cmp zero    (suc j) = tri< (s≤s z≤n) (λ()) (λ())
<-cmp (suc i) zero    = tri> (λ())     (λ()) (s≤s z≤n)
<-cmp (suc i) (suc j) with <-cmp i j
... | tri< i<j i≢j j≮i = tri< (s≤s i<j)         (i≢j ∘ suc-injective) (j≮i ∘ ℕₚ.≤-pred)
... | tri> i≮j i≢j j<i = tri> (i≮j ∘ ℕₚ.≤-pred) (i≢j ∘ suc-injective) (s≤s j<i)
... | tri≈ i≮j i≡j j≮i = tri≈ (i≮j ∘ ℕₚ.≤-pred) (cong suc i≡j)        (j≮i ∘ ℕₚ.≤-pred)

<-respˡ-≡ : ∀ {n} → (_<_ {n}) Respectsˡ _≡_
<-respˡ-≡ refl x≤y = x≤y

<-respʳ-≡ : ∀ {n} → (_<_ {n}) Respectsʳ _≡_
<-respʳ-≡ refl x≤y = x≤y

<-resp₂-≡ : ∀ {n} → (_<_ {n}) Respects₂ _≡_
<-resp₂-≡ = <-respʳ-≡ , <-respˡ-≡

<-irrelevant : ∀ {n} → Irrelevant (_<_ {n})
<-irrelevant = ℕₚ.<-irrelevant

------------------------------------------------------------------------
-- Structures

<-isStrictPartialOrder : ∀ {n} → IsStrictPartialOrder _≡_ (_<_ {n})
<-isStrictPartialOrder = record
  { isEquivalence = P.isEquivalence
  ; irrefl        = <-irrefl
  ; trans         = <-trans
  ; <-resp-≈      = <-resp₂-≡
  }

<-isStrictTotalOrder : ∀ {n} → IsStrictTotalOrder _≡_ (_<_ {n})
<-isStrictTotalOrder = record
  { isEquivalence = P.isEquivalence
  ; trans         = <-trans
  ; compare       = <-cmp
  }

------------------------------------------------------------------------
-- Bundles

<-strictPartialOrder : ℕ → StrictPartialOrder _ _ _
<-strictPartialOrder n = record
  { isStrictPartialOrder = <-isStrictPartialOrder {n}
  }

<-strictTotalOrder : ℕ → StrictTotalOrder _ _ _
<-strictTotalOrder n = record
  { isStrictTotalOrder = <-isStrictTotalOrder {n}
  }

------------------------------------------------------------------------
-- Other properties

<⇒≢ : ∀ {n} {i j : Fin n} → i < j → i ≢ j
<⇒≢ i<i refl = ℕₚ.n≮n _ i<i

≤∧≢⇒< : ∀ {n} {i j : Fin n} → i ≤ j → i ≢ j → i < j
≤∧≢⇒< {i = zero}  {zero}  _         0≢0     = contradiction refl 0≢0
≤∧≢⇒< {i = zero}  {suc j} _         _       = s≤s z≤n
≤∧≢⇒< {i = suc i} {suc j} (s≤s i≤j) 1+i≢1+j =
  s≤s (≤∧≢⇒< i≤j (1+i≢1+j ∘ (cong suc)))

------------------------------------------------------------------------
-- inject
------------------------------------------------------------------------

toℕ-inject : ∀ {n} {i : Fin n} (j : Fin′ i) →
             toℕ (inject j) ≡ toℕ j
toℕ-inject {i = suc i} zero    = refl
toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j)

------------------------------------------------------------------------
-- inject+
------------------------------------------------------------------------

toℕ-inject+ : ∀ {m} n (i : Fin m) → toℕ i ≡ toℕ (inject+ n i)
toℕ-inject+ n zero    = refl
toℕ-inject+ n (suc i) = cong suc (toℕ-inject+ n i)

------------------------------------------------------------------------
-- inject₁
------------------------------------------------------------------------

inject₁-injective : ∀ {n} {i j : Fin n} → inject₁ i ≡ inject₁ j → i ≡ j
inject₁-injective {i = zero}  {zero}  i≡j = refl
inject₁-injective {i = suc i} {suc j} i≡j =
  cong suc (inject₁-injective (suc-injective i≡j))

toℕ-inject₁ : ∀ {n} (i : Fin n) → toℕ (inject₁ i) ≡ toℕ i
toℕ-inject₁ zero    = refl
toℕ-inject₁ (suc i) = cong suc (toℕ-inject₁ i)

toℕ-inject₁-≢ : ∀ {n}(i : Fin n) → n ≢ toℕ (inject₁ i)
toℕ-inject₁-≢ (suc i) = toℕ-inject₁-≢ i ∘ ℕₚ.suc-injective

------------------------------------------------------------------------
-- inject₁ and lower₁

inject₁-lower₁ : ∀ {n} (i : Fin (suc n)) (n≢i : n ≢ toℕ i) →
                 inject₁ (lower₁ i n≢i) ≡ i
inject₁-lower₁ {zero}  zero     0≢0     = contradiction refl 0≢0
inject₁-lower₁ {suc n} zero     _       = refl
inject₁-lower₁ {suc n} (suc i)  n+1≢i+1 =
  cong suc (inject₁-lower₁ i  (n+1≢i+1 ∘ cong suc))

lower₁-inject₁′ : ∀ {n} (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) →
                  lower₁ (inject₁ i) n≢i ≡ i
lower₁-inject₁′ zero    _       = refl
lower₁-inject₁′ (suc i) n+1≢i+1 =
  cong suc (lower₁-inject₁′ i (n+1≢i+1 ∘ cong suc))

lower₁-inject₁ : ∀ {n} (i : Fin n) →
                 lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i
lower₁-inject₁ i = lower₁-inject₁′ i (toℕ-inject₁-≢ i)

lower₁-irrelevant : ∀ {n} (i : Fin (suc n)) n≢i₁ n≢i₂ →
             lower₁ {n} i n≢i₁ ≡ lower₁ {n} i n≢i₂
lower₁-irrelevant {zero}  zero     0≢0 _ = contradiction refl 0≢0
lower₁-irrelevant {suc n} zero     _   _ = refl
lower₁-irrelevant {suc n} (suc i)  _   _ =
  cong suc (lower₁-irrelevant i _ _)

------------------------------------------------------------------------
-- inject≤
------------------------------------------------------------------------

toℕ-inject≤ : ∀ {m n} (i : Fin m) (le : m ℕ.≤ n) →
                toℕ (inject≤ i le) ≡ toℕ i
toℕ-inject≤ {_} {suc n} zero    _  = refl
toℕ-inject≤ {_} {suc n} (suc i) le = cong suc (toℕ-inject≤ i (ℕₚ.≤-pred le))

inject≤-refl : ∀ {n} (i : Fin n) (n≤n : n ℕ.≤ n) → inject≤ i n≤n ≡ i
inject≤-refl {suc n} zero    _   = refl
inject≤-refl {suc n} (suc i) n≤n = cong suc (inject≤-refl i (ℕₚ.≤-pred n≤n))

inject≤-idempotent : ∀ {m n k} (i : Fin m)
                     (m≤n : m ℕ.≤ n) (n≤k : n ℕ.≤ k) (m≤k : m ℕ.≤ k) →
                     inject≤ (inject≤ i m≤n) n≤k ≡ inject≤ i m≤k
inject≤-idempotent {_} {suc n} {suc k} zero    _   _   _ = refl
inject≤-idempotent {_} {suc n} {suc k} (suc i) m≤n n≤k _ =
  cong suc (inject≤-idempotent i (ℕₚ.≤-pred m≤n) (ℕₚ.≤-pred n≤k) _)

------------------------------------------------------------------------
-- splitAt
------------------------------------------------------------------------

-- Fin (m + n) ≃ Fin m ⊎ Fin n

splitAt-inject+ : ∀ m n i → splitAt m (inject+ n i) ≡ inj₁ i
splitAt-inject+ (suc m) n zero = refl
splitAt-inject+ (suc m) n (suc i) rewrite splitAt-inject+ m n i = refl

splitAt-raise : ∀ m n i → splitAt m (raise {n} m i) ≡ inj₂ i
splitAt-raise zero    n i = refl
splitAt-raise (suc m) n i rewrite splitAt-raise m n i = refl

inject+-raise-splitAt : ∀ m n i → [ inject+ n , raise {n} m ] (splitAt m i) ≡ i
inject+-raise-splitAt zero    n i       = refl
inject+-raise-splitAt (suc m) n zero    = refl
inject+-raise-splitAt (suc m) n (suc i) = begin
  [ inject+ n , raise {n} (suc m) ] (splitAt (suc m) (suc i))  ≡⟨ [,]-map-commute (splitAt m i) ⟩
  [ suc ∘ (inject+ n) , suc ∘ (raise {n} m) ] (splitAt m i)    ≡˘⟨ [,]-∘-distr {f = suc} (splitAt m i) ⟩
  suc ([ inject+ n , raise {n} m ] (splitAt m i))              ≡⟨ cong suc (inject+-raise-splitAt m n i) ⟩
  suc i                                                        ∎
  where open ≡-Reasoning

------------------------------------------------------------------------
-- lift
------------------------------------------------------------------------

lift-injective : ∀ {m n} (f : Fin m → Fin n) →
                 (∀ {x y} → f x ≡ f y → x ≡ y) →
                 ∀ k {x y} → lift k f x ≡ lift k f y → x ≡ y
lift-injective f inj zero                    eq = inj eq
lift-injective f inj (suc k) {0F} {0F}       eq = refl
lift-injective f inj (suc k) {suc i} {suc y} eq = cong suc (lift-injective f inj k (suc-injective eq))

------------------------------------------------------------------------
-- _≺_
------------------------------------------------------------------------

≺⇒<′ : _≺_ ⇒ ℕ._<′_
≺⇒<′ (n ≻toℕ i) = ℕₚ.≤⇒≤′ (toℕ<n i)

<′⇒≺ : ℕ._<′_ ⇒ _≺_
<′⇒≺ {n} ℕ.≤′-refl = subst (_≺ suc n) (toℕ-fromℕ n)
                              (suc n ≻toℕ fromℕ n)
<′⇒≺ (ℕ.≤′-step m≤′n) with <′⇒≺ m≤′n
... | n ≻toℕ i = subst (_≺ suc n) (toℕ-inject₁ i) (suc n ≻toℕ _)

------------------------------------------------------------------------
-- pred
------------------------------------------------------------------------

<⇒≤pred : ∀ {n} {i j : Fin n} → j < i → j ≤ pred i
<⇒≤pred {i = suc i} {zero}  j<i       = z≤n
<⇒≤pred {i = suc i} {suc j} (s≤s j<i) =
  subst (_ ℕ.≤_) (sym (toℕ-inject₁ i)) j<i

------------------------------------------------------------------------
-- _ℕ-_
------------------------------------------------------------------------

toℕ‿ℕ- : ∀ n i → toℕ (n ℕ- i) ≡ n ∸ toℕ i
toℕ‿ℕ- n       zero     = toℕ-fromℕ n
toℕ‿ℕ- (suc n) (suc i)  = toℕ‿ℕ- n i

------------------------------------------------------------------------
-- _ℕ-ℕ_
------------------------------------------------------------------------

nℕ-ℕi≤n : ∀ n i → n ℕ-ℕ i ℕ.≤ n
nℕ-ℕi≤n n       zero     = ℕₚ.≤-refl
nℕ-ℕi≤n (suc n) (suc i)  = begin
  n ℕ-ℕ i  ≤⟨ nℕ-ℕi≤n n i ⟩
  n        ≤⟨ ℕₚ.n≤1+n n ⟩
  suc n    ∎
  where open ℕₚ.≤-Reasoning

------------------------------------------------------------------------
-- punchIn
------------------------------------------------------------------------

punchIn-injective : ∀ {m} i (j k : Fin m) →
                    punchIn i j ≡ punchIn i k → j ≡ k
punchIn-injective zero    _       _       refl      = refl
punchIn-injective (suc i) zero    zero    _         = refl
punchIn-injective (suc i) (suc j) (suc k) ↑j+1≡↑k+1 =
  cong suc (punchIn-injective i j k (suc-injective ↑j+1≡↑k+1))

punchInᵢ≢i : ∀ {m} i (j : Fin m) → punchIn i j ≢ i
punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective

------------------------------------------------------------------------
-- punchOut
------------------------------------------------------------------------

-- A version of 'cong' for 'punchOut' in which the inequality argument can be
-- changed out arbitrarily (reflecting the proof-irrelevance of that argument).

punchOut-cong : ∀ {n} (i : Fin (suc n)) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} → j ≡ k → punchOut i≢j ≡ punchOut i≢k
punchOut-cong zero {zero} {i≢j = 0≢0} = contradiction refl 0≢0
punchOut-cong zero {suc j} {zero} {i≢k = 0≢0} = contradiction refl 0≢0
punchOut-cong zero {suc j} {suc k} = suc-injective
punchOut-cong {suc n} (suc i) {zero} {zero} _ = refl
punchOut-cong {suc n} (suc i) {suc j} {suc k} = cong suc ∘ punchOut-cong i ∘ suc-injective

-- An alternative to 'punchOut-cong' in the which the new inequality argument is
-- specific. Useful for enabling the omission of that argument during equational
-- reasoning.

punchOut-cong′ : ∀ {n} (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) → punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
punchOut-cong′ i q = punchOut-cong i q

punchOut-injective : ∀ {m} {i j k : Fin (suc m)}
                     (i≢j : i ≢ j) (i≢k : i ≢ k) →
                     punchOut i≢j ≡ punchOut i≢k → j ≡ k
punchOut-injective {_}     {zero}   {zero}  {_}     0≢0 _   _     = contradiction refl 0≢0
punchOut-injective {_}     {zero}   {_}     {zero}  _   0≢0 _     = contradiction refl 0≢0
punchOut-injective {_}     {zero}   {suc j} {suc k} _   _   pⱼ≡pₖ = cong suc pⱼ≡pₖ
punchOut-injective {suc n} {suc i}  {zero}  {zero}  _   _    _    = refl
punchOut-injective {suc n} {suc i}  {suc j} {suc k} i≢j i≢k pⱼ≡pₖ =
  cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ))

punchIn-punchOut : ∀ {m} {i j : Fin (suc m)} (i≢j : i ≢ j) →
                   punchIn i (punchOut i≢j) ≡ j
punchIn-punchOut {_}     {zero}   {zero}  0≢0 = contradiction refl 0≢0
punchIn-punchOut {_}     {zero}   {suc j} _   = refl
punchIn-punchOut {suc m} {suc i}  {zero}  i≢j = refl
punchIn-punchOut {suc m} {suc i}  {suc j} i≢j =
  cong suc (punchIn-punchOut (i≢j ∘ cong suc))

punchOut-punchIn : ∀ {n} i {j : Fin n} → punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j
punchOut-punchIn zero {j} = refl
punchOut-punchIn (suc i) {zero} = refl
punchOut-punchIn (suc i) {suc j} = cong suc (begin
  punchOut (punchInᵢ≢i i j ∘ suc-injective ∘ sym ∘ cong suc)  ≡⟨ punchOut-cong i refl ⟩
  punchOut (punchInᵢ≢i i j ∘ sym)                             ≡⟨ punchOut-punchIn i ⟩
  j                                                           ∎)
  where open ≡-Reasoning

------------------------------------------------------------------------
-- Quantification
------------------------------------------------------------------------

module _ {n p} {P : Pred (Fin (suc n)) p} where

  ∀-cons : P zero → Π[ P ∘ suc ] → Π[ P ]
  ∀-cons z s zero    = z
  ∀-cons z s (suc i) = s i

  ∀-cons-⇔ : (P zero × Π[ P ∘ suc ]) ⇔ Π[ P ]
  ∀-cons-⇔ = equivalence (uncurry ∀-cons) < _$ zero , _∘ suc >

  ∃-here : P zero → ∃⟨ P ⟩
  ∃-here = zero ,_

  ∃-there : ∃⟨ P ∘ suc ⟩ → ∃⟨ P ⟩
  ∃-there = map suc id

  ∃-toSum : ∃⟨ P ⟩ → P zero ⊎ ∃⟨ P ∘ suc ⟩
  ∃-toSum ( zero , P₀ ) = inj₁ P₀
  ∃-toSum (suc f , P₁₊) = inj₂ (f , P₁₊)

  ⊎⇔∃ : (P zero ⊎ ∃⟨ P ∘ suc ⟩) ⇔ ∃⟨ P ⟩
  ⊎⇔∃ = equivalence [ ∃-here , ∃-there ] ∃-toSum

decFinSubset : ∀ {n p q} {P : Pred (Fin n) p} {Q : Pred (Fin n) q} →
               Decidable Q → (∀ {f} → Q f → Dec (P f)) → Dec (Q ⊆ P)
decFinSubset {zero} Q? P? = yes λ {}
decFinSubset {suc n} {P = P} {Q} Q? P?
  with Q? zero | ∀-cons {P = λ x → Q x → P x}
... | false because [¬Q0] | cons =
  map′ (λ f {x} → cons (⊥-elim ∘ invert [¬Q0]) (λ x → f {x}) x)
       (λ f {x} → f {suc x})
       (decFinSubset (Q? ∘ suc) P?)
... | true  because  [Q0] | cons =
  map′ (uncurry λ P0 rec {x} → cons (λ _ → P0) (λ x → rec {x}) x)
       < _$ invert [Q0] , (λ f {x} → f {suc x}) >
       (P? (invert [Q0]) ×-dec decFinSubset (Q? ∘ suc) P?)

any? : ∀ {n p} {P : Fin n → Set p} → Decidable P → Dec (∃ P)
any? {zero}  {P = _} P? = no λ { (() , _) }
any? {suc n} {P = P} P? = Dec.map ⊎⇔∃ (P? zero ⊎-dec any? (P? ∘ suc))

all? : ∀ {n p} {P : Pred (Fin n) p} →
       Decidable P → Dec (∀ f → P f)
all? P? = map′ (λ ∀p f → ∀p tt) (λ ∀p {x} _ → ∀p x)
               (decFinSubset U? (λ {f} _ → P? f))

private
  -- A nice computational property of `all?`:
  -- The boolean component of the result is exactly the
  -- obvious fold of boolean tests (`foldr _∧_ true`).
  note : ∀ {p} {P : Pred (Fin 3) p} (P? : Decidable P) →
         ∃ λ z → does (all? P?) ≡ z
  note P? = does (P? 0F) ∧ does (P? 1F) ∧ does (P? 2F) ∧ true
          , refl

-- If a decidable predicate P over a finite set is sometimes false,
-- then we can find the smallest value for which this is the case.

¬∀⟶∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
                 ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
¬∀⟶∃¬-smallest zero    P P? ¬∀P = contradiction (λ()) ¬∀P
¬∀⟶∃¬-smallest (suc n) P P? ¬∀P with P? zero
... | false because [¬P₀] = (zero , invert [¬P₀] , λ ())
... |  true because  [P₀] = map suc (map id (∀-cons (invert [P₀])))
  (¬∀⟶∃¬-smallest n (P ∘ suc) (P? ∘ suc) (¬∀P ∘ (∀-cons (invert [P₀]))))

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

¬∀⟶∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
          ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
¬∀⟶∃¬ n P P? ¬P = map id proj₁ (¬∀⟶∃¬-smallest n P P? ¬P)

-- The pigeonhole principle.

pigeonhole : ∀ {m n} → m ℕ.< n → (f : Fin n → Fin m) →
             ∃₂ λ i j → i ≢ j × f i ≡ f j
pigeonhole (s≤s z≤n)       f = contradiction (f zero) λ()
pigeonhole (s≤s (s≤s m≤n)) f with any? (λ k → f zero ≟ f (suc k))
... | yes (j , f₀≡fⱼ) = zero , suc j , (λ()) , f₀≡fⱼ
... | no  f₀≢fₖ with pigeonhole (s≤s m≤n) (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
...   | (i , j , i≢j , fᵢ≡fⱼ) =
  suc i , suc j , i≢j ∘ suc-injective ,
  punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ

------------------------------------------------------------------------
-- Categorical
------------------------------------------------------------------------

module _ {f} {F : Set f → Set f} (RA : RawApplicative F) where

  open RawApplicative RA

  sequence : ∀ {n} {P : Pred (Fin n) f} →
             (∀ i → F (P i)) → F (∀ i → P i)
  sequence {zero}  ∀iPi = pure λ()
  sequence {suc n} ∀iPi = ∀-cons <$> ∀iPi zero ⊛ sequence (∀iPi ∘ suc)

module _ {f} {F : Set f → Set f} (RF : RawFunctor F) where

  open RawFunctor RF

  sequence⁻¹ : ∀ {A : Set f} {P : Pred A f} →
               F (∀ i → P i) → (∀ i → F (P i))
  sequence⁻¹ F∀iPi i = (λ f → f i) <$> F∀iPi

------------------------------------------------------------------------
-- If there is an injection from a type to a finite set, then the type
-- has decidable equality.

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

  eq? : ∀ {n} → A ↣ Fin n → B.Decidable {A = A} _≡_
  eq? inj = Dec.via-injection inj _≟_

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

cmp              = <-cmp
{-# WARNING_ON_USAGE cmp
"Warning: cmp was deprecated in v0.15.
Please use <-cmp instead."
#-}
strictTotalOrder = <-strictTotalOrder
{-# WARNING_ON_USAGE strictTotalOrder
"Warning: strictTotalOrder was deprecated in v0.15.
Please use <-strictTotalOrder instead."
#-}

-- Version 0.16

to-from = toℕ-fromℕ
{-# WARNING_ON_USAGE to-from
"Warning: to-from was deprecated in v0.16.
Please use toℕ-fromℕ instead."
#-}
from-to          = fromℕ-toℕ
{-# WARNING_ON_USAGE from-to
"Warning: from-to was deprecated in v0.16.
Please use fromℕ-toℕ instead."
#-}
bounded = toℕ<n
{-# WARNING_ON_USAGE bounded
"Warning: bounded was deprecated in v0.16.
Please use toℕ<n instead."
#-}
prop-toℕ-≤ = toℕ≤pred[n]
{-# WARNING_ON_USAGE prop-toℕ-≤
"Warning: prop-toℕ-≤ was deprecated in v0.16.
Please use toℕ≤pred[n] instead."
#-}
prop-toℕ-≤′ = toℕ≤pred[n]′
{-# WARNING_ON_USAGE prop-toℕ-≤′
"Warning: prop-toℕ-≤′ was deprecated in v0.16.
Please use toℕ≤pred[n]′ instead."
#-}
inject-lemma = toℕ-inject
{-# WARNING_ON_USAGE inject-lemma
"Warning: inject-lemma was deprecated in v0.16.
Please use toℕ-inject instead."
#-}
inject+-lemma = toℕ-inject+
{-# WARNING_ON_USAGE inject+-lemma
"Warning: inject+-lemma was deprecated in v0.16.
Please use toℕ-inject+ instead."
#-}
inject₁-lemma = toℕ-inject₁
{-# WARNING_ON_USAGE inject₁-lemma
"Warning: inject₁-lemma was deprecated in v0.16.
Please use toℕ-inject₁ instead."
#-}
inject≤-lemma = toℕ-inject≤
{-# WARNING_ON_USAGE inject≤-lemma
"Warning: inject≤-lemma was deprecated in v0.16.
Please use toℕ-inject≤ instead."
#-}

-- Version 0.17

≤+≢⇒< = ≤∧≢⇒<
{-# WARNING_ON_USAGE ≤+≢⇒<
"Warning: ≤+≢⇒< was deprecated in v0.17.
Please use ≤∧≢⇒< instead."
#-}

-- Version 1.0

≤-irrelevance = ≤-irrelevant
{-# WARNING_ON_USAGE ≤-irrelevance
"Warning: ≤-irrelevance was deprecated in v1.0.
Please use ≤-irrelevant instead."
#-}
<-irrelevance = <-irrelevant
{-# WARNING_ON_USAGE <-irrelevance
"Warning: <-irrelevance was deprecated in v1.0.
Please use <-irrelevant instead."
#-}

-- Version 1.1

infixl 6 _+′_
_+′_ : ∀ {m n} (i : Fin m) (j : Fin n) → Fin (ℕ.pred m ℕ.+ n)
i +′ j = inject≤ (i + j) (ℕₚ.+-monoˡ-≤ _ (toℕ≤pred[n] i))
{-# WARNING_ON_USAGE _+′_
"Warning: _+′_ was deprecated in v1.1.
Please use `raise` or `inject+` from `Data.Fin` instead."
#-}

-- Version 1.2

fromℕ≤-toℕ = fromℕ<-toℕ
{-# WARNING_ON_USAGE fromℕ≤-toℕ
"Warning: fromℕ≤-toℕ was deprecated in v1.2.
Please use fromℕ<-toℕ instead."
#-}
toℕ-fromℕ≤ = toℕ-fromℕ<
{-# WARNING_ON_USAGE toℕ-fromℕ≤
"Warning: toℕ-fromℕ≤ was deprecated in v1.2.
Please use toℕ-fromℕ< instead."
#-}
fromℕ≤≡fromℕ≤″ = fromℕ<≡fromℕ<″
{-# WARNING_ON_USAGE fromℕ≤≡fromℕ≤″
"Warning: fromℕ≤≡fromℕ≤″ was deprecated in v1.2.
Please use fromℕ<≡fromℕ<″ instead."
#-}
toℕ-fromℕ≤″ = toℕ-fromℕ<″
{-# WARNING_ON_USAGE toℕ-fromℕ≤″
"Warning: toℕ-fromℕ≤″ was deprecated in v1.2.
Please use toℕ-fromℕ<″ instead."
#-}
isDecEquivalence = ≡-isDecEquivalence
{-# WARNING_ON_USAGE isDecEquivalence
"Warning: isDecEquivalence was deprecated in v1.2.
Please use ≡-isDecEquivalence instead."
#-}
preorder = ≡-preorder
{-# WARNING_ON_USAGE preorder
"Warning: preorder was deprecated in v1.2.
Please use ≡-preorder instead."
#-}
setoid = ≡-setoid
{-# WARNING_ON_USAGE setoid
"Warning: setoid was deprecated in v1.2.
Please use ≡-setoid instead."
#-}
decSetoid = ≡-decSetoid
{-# WARNING_ON_USAGE decSetoid
"Warning: decSetoid was deprecated in v1.2.
Please use ≡-decSetoid instead."
#-}


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

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
open import homotopy.Freudenthal
open import homotopy.IterSuspensionStable
open import homotopy.Pi2HSusp
open import homotopy.EM1HSpace
open import homotopy.EilenbergMacLane1

module homotopy.EilenbergMacLane where

private
  -- helper
  kle : (n : ℕ) → ⟨ S (S n) ⟩ ≤T ⟨ n ⟩ +2+ ⟨ n ⟩
  kle O = inl idp
  kle (S n) = ≤T-trans (≤T-ap-S (kle n))
                (≤T-trans (inl (! (+2+-βr ⟨ n ⟩ ⟨ n ⟩)))
                            (inr ltS))

-- EM(G,n) when G is π₁(A,a₀)
module EMImplicit {i} {X : Ptd i} {{_ : is-connected 0 (de⊙ X)}}
  {{X-level : has-level 1 (de⊙ X)}} (H-X : HSS X) where

  private
    A = de⊙ X
    a₀ = pt X

  ⊙EM : (n : ℕ) → Ptd i
  ⊙EM O = ⊙Ω X
  ⊙EM (S n) = ⊙Trunc ⟨ S n ⟩ (⊙Susp^ n X)

  module _ (n : ℕ) where
    EM = de⊙ (⊙EM n)

  EM-level : (n : ℕ) → has-level ⟨ n ⟩ (EM n)
  EM-level O = has-level-apply X-level _ _
  EM-level (S n) = Trunc-level

  instance
    EM-conn : (n : ℕ) → is-connected ⟨ n ⟩ (EM (S n))
    EM-conn n = Trunc-preserves-conn (⊙Susp^-conn' n)

  {-
  π (S k) (EM (S n)) (embase (S n)) == π k (EM n) (embase n)
  where k > 0 and n = S (S n')
  -}
  module Stable (k n : ℕ) (indexing : S k ≤ S (S n))
    where

    private
      SSn : ℕ
      SSn = S (S n)

      lte : ⟨ S k ⟩ ≤T ⟨ SSn ⟩
      lte = ⟨⟩-monotone-≤ $ indexing

      Skle : S k ≤ (S n) *2
      Skle = ≤-trans indexing (lemma n)
        where lemma : (n' : ℕ) → S (S n') ≤ (S n') *2
              lemma O = inl idp
              lemma (S n') = ≤-trans (≤-ap-S (lemma n')) (inr ltS)

    private
      module SS = Susp^StableSucc k (S n) Skle (⊙Susp^ (S n) X) {{⊙Susp^-conn' (S n)}}

    abstract
      stable : πS (S k) (⊙EM (S SSn)) ≃ᴳ πS k (⊙EM SSn)
      stable =
        πS (S k) (⊙EM (S SSn))
          ≃ᴳ⟨ πS-Trunc-fuse-≤-iso _ _ _ (≤T-ap-S lte) ⟩
        πS (S k) (⊙Susp^ SSn X)
          ≃ᴳ⟨ SS.stable ⟩
        πS k (⊙Susp^ (S n) X)
          ≃ᴳ⟨ πS-Trunc-fuse-≤-iso _ _ _ lte ⁻¹ᴳ ⟩
        πS k (⊙EM SSn)
          ≃ᴳ∎

  module BelowDiagonal where

    π₁ : (n : ℕ) → πS 0 (⊙EM (S (S n))) ≃ᴳ 0ᴳ
    π₁ n =
      contr-iso-0ᴳ (πS 0 (⊙EM (S (S n))))
        (connected-at-level-is-contr
          {{raise-level-≤T (≤T-ap-S (≤T-ap-S (-2≤T ⟨ n ⟩₋₂)))
                          (Trunc-level {n = 0})}})

    -- some clutter here arises from the definition of <;
    -- any simple way to avoid this?
    πS-below : (k n : ℕ) → (S k < n)
      → πS k (⊙EM n) ≃ᴳ 0ᴳ
    πS-below 0 .2 ltS = π₁ 0
    πS-below 0 .3 (ltSR ltS) = π₁ 1
    πS-below 0 (S (S n)) (ltSR (ltSR _)) = π₁ n
    πS-below (S k) ._ ltS =
      πS-below k _ ltS
      ∘eᴳ Stable.stable k k (inr ltS)
    πS-below (S k) ._ (ltSR ltS) =
      πS-below k _ (ltSR ltS)
      ∘eᴳ Stable.stable k (S k) (inr (ltSR ltS))
    πS-below (S k) ._ (ltSR (ltSR ltS)) =
      πS-below k _ (ltSR (ltSR ltS))
      ∘eᴳ Stable.stable k (S (S k)) (inr (ltSR (ltSR ltS)))
    πS-below (S k) (S (S (S n))) (ltSR (ltSR (ltSR lt))) =
      πS-below k _ (<-cancel-S (ltSR (ltSR (ltSR lt))))
      ∘eᴳ Stable.stable k n (inr (<-cancel-S (ltSR (ltSR (ltSR lt)))))

  module OnDiagonal where

    π₁ : πS 0 (⊙EM 1) ≃ᴳ πS 0 X
    π₁ = πS-Trunc-fuse-≤-iso 0 1 X ≤T-refl

    private
      module Π₂ = Pi2HSusp H-X

    π₂ : πS 1 (⊙EM 2) ≃ᴳ πS 0 X
    π₂ = Π₂.π₂-Susp
     ∘eᴳ πS-Trunc-fuse-≤-iso 1 2 (⊙Susp (de⊙ X)) ≤T-refl

    πS-diag : (n : ℕ) → πS n (⊙EM (S n)) ≃ᴳ πS 0 X
    πS-diag 0 = π₁
    πS-diag 1 = π₂
    πS-diag (S (S n)) = πS-diag (S n)
                    ∘eᴳ Stable.stable (S n) n ≤-refl

  module AboveDiagonal where

    πS-above : ∀ (k n : ℕ) → (n < S k)
      → πS k (⊙EM n) ≃ᴳ 0ᴳ
    πS-above k n lt =
      contr-iso-0ᴳ (πS k (⊙EM n))
        (inhab-prop-is-contr
          [ idp^ (S k) ]
          {{Trunc-preserves-level 0 (Ω^-level -1 (S k) _
            (raise-level-≤T (lemma lt) (EM-level n)))}})
      where lemma : {k n : ℕ} → n < k → ⟨ n ⟩ ≤T (⟨ k ⟩₋₂ +2+ -1)
            lemma ltS = inl (! (+2+-comm _ -1))
            lemma (ltSR lt) = ≤T-trans (lemma lt) (inr ltS)

  module Spectrum where

    private
      module Π₂ = Pi2HSusp H-X

    spectrum0 : ⊙Ω (⊙EM 1) ⊙≃ ⊙EM 0
    spectrum0 =
      ⊙Ω (⊙EM 1)
        ⊙≃⟨ ⊙Ω-⊙Trunc-comm 0 X ⟩
      ⊙Trunc 0 (⊙Ω X)
        ⊙≃⟨ ⊙unTrunc-equiv (⊙Ω X) ⟩
      ⊙Ω X ⊙≃∎

    spectrum1 : ⊙Ω (⊙EM 2) ⊙≃ ⊙EM 1
    spectrum1 =
      ⊙Ω (⊙EM 2)
        ⊙≃⟨ ⊙Ω-⊙Trunc-comm 1 (⊙Susp (de⊙ X)) ⟩
      ⊙Trunc 1 (⊙Ω (⊙Susp (de⊙ X)))
        ⊙≃⟨ Π₂.⊙eq ⟩
      ⊙EM 1 ⊙≃∎

    sconn : (n : ℕ) → is-connected ⟨ S n ⟩ (de⊙ (⊙Susp^ (S n) X))
    sconn n = ⊙Susp^-conn' (S n)

    module FS (n : ℕ) =
      FreudenthalEquiv ⟨ n ⟩₋₁ ⟨ S (S n) ⟩ (kle n)
        (⊙Susp^ (S n) X) {{sconn n}}

    Trunc-fmap-σloop-is-equiv : ∀ (n : ℕ)
      → is-equiv (Trunc-fmap {n = ⟨ S n ⟩} (σloop (⊙Susp^ n X)))
    Trunc-fmap-σloop-is-equiv O = snd (Π₂.eq ⁻¹)
    Trunc-fmap-σloop-is-equiv (S n) = snd (FS.eq n)

    spectrumSS : (n : ℕ)
      → ⊙Ω (⊙EM (S (S (S n)))) ⊙≃ ⊙EM (S (S n))
    spectrumSS n =
      ⊙Ω (⊙EM (S (S (S n))))
        ⊙≃⟨ ⊙Ω-⊙Trunc-comm ⟨ S (S n) ⟩ (⊙Susp^ (S (S n)) X) ⟩
      ⊙Trunc ⟨ S (S n) ⟩ (⊙Ω (⊙Susp^ (S (S n)) X))
        ⊙≃⟨ FS.⊙eq n ⊙⁻¹ ⟩
      ⊙EM (S (S n)) ⊙≃∎

    ⊙–>-spectrumSS : ∀ (n : ℕ)
      → ⊙–> (spectrumSS n) ◃⊙idf
        =⊙∘
        FS.⊙encodeN n ◃⊙∘
        ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S (S n) ⟩ (⊙Susp^ (S (S n)) X)) ◃⊙idf
    ⊙–>-spectrumSS n =
      ⊙–> (spectrumSS n) ◃⊙idf
        =⊙∘⟨ =⊙∘-in {gs = ⊙<– (FS.⊙eq n) ◃⊙∘
                          ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S (S n) ⟩ (⊙Susp^ (S (S n)) X)) ◃⊙idf} $
             ⊙λ= (⊙∘-unit-l _) ⟩
      ⊙<– (FS.⊙eq n) ◃⊙∘
      ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S (S n) ⟩ (⊙Susp^ (S (S n)) X)) ◃⊙idf
        =⊙∘₁⟨ 0 & 1 & FS.⊙<–-⊙eq n ⟩
      FS.⊙encodeN n ◃⊙∘
      ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S (S n) ⟩ (⊙Susp^ (S (S n)) X)) ◃⊙idf ∎⊙∘

    spectrum : (n : ℕ) → ⊙Ω (⊙EM (S n)) ⊙≃ ⊙EM n
    spectrum 0 = spectrum0
    spectrum 1 = spectrum1
    spectrum (S (S n)) = spectrumSS n

module EMImplicitMap {i} {j} {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
  {{_ : is-connected 0 (de⊙ X)}} {{_ : is-connected 0 (de⊙ Y)}}
  {{X-level : has-level 1 (de⊙ X)}} {{Y-level : has-level 1 (de⊙ Y)}}
  (H-X : HSS X) (H-Y : HSS Y) where

  ⊙EM-fmap : ∀ n → EMImplicit.⊙EM H-X n ⊙→ EMImplicit.⊙EM H-Y n
  ⊙EM-fmap O = ⊙Ω-fmap f
  ⊙EM-fmap (S n) = ⊙Trunc-fmap (⊙Susp^-fmap n f)

module SpectrumNatural {i} {X Y : Ptd i} (f : X ⊙→ Y)
  {{_ : is-connected 0 (de⊙ X)}} {{_ : is-connected 0 (de⊙ Y)}}
  {{X-level : has-level 1 (de⊙ X)}} {{Y-level : has-level 1 (de⊙ Y)}}
  (H-X : HSS X) (H-Y : HSS Y) where

  open EMImplicitMap f H-X H-Y

  open EMImplicit.Spectrum

  ⊙–>-spectrum0-natural :
    ⊙–> (spectrum0 H-Y) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap f) ◃⊙idf
    =⊙∘
    ⊙Ω-fmap f ◃⊙∘
    ⊙–> (spectrum0 H-X) ◃⊙idf
  ⊙–>-spectrum0-natural =
    ⊙–> (spectrum0 H-Y) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap f) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙expand (⊙–> (⊙unTrunc-equiv (⊙Ω Y)) ◃⊙∘
                            ⊙–> (⊙Ω-⊙Trunc-comm 0 Y) ◃⊙idf) ⟩
    ⊙–> (⊙unTrunc-equiv (⊙Ω Y)) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm 0 Y) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap f) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙–>-⊙Ω-⊙Trunc-comm-natural-=⊙∘ 0 f ⟩
    ⊙–> (⊙unTrunc-equiv (⊙Ω Y)) ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap f) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm (S (S ⟨-2⟩)) X) ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙–>-⊙unTrunc-equiv-natural-=⊙∘ (⊙Ω-fmap f) ⟩
    ⊙Ω-fmap f ◃⊙∘
    ⊙–> (⊙unTrunc-equiv (⊙Ω X)) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm (S (S ⟨-2⟩)) X) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙contract ⟩
    ⊙Ω-fmap f ◃⊙∘
    ⊙–> (spectrum0 H-X) ◃⊙idf ∎⊙∘

  ⊙–>-spectrum1-natural :
    ⊙–> (spectrum1 H-Y) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp-fmap (fst f))) ◃⊙idf
    =⊙∘
    ⊙Trunc-fmap f ◃⊙∘
    ⊙–> (spectrum1 H-X) ◃⊙idf
  ⊙–>-spectrum1-natural =
    ⊙–> (spectrum1 H-Y) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp-fmap (fst f))) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙expand (⊙–> (Pi2HSusp.⊙eq H-Y) ◃⊙∘
                            ⊙–> (⊙Ω-⊙Trunc-comm 1 (⊙Susp (de⊙ Y))) ◃⊙idf) ⟩
    ⊙–> (Pi2HSusp.⊙eq H-Y) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm 1 (⊙Susp (de⊙ Y))) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp-fmap (fst f))) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙–>-⊙Ω-⊙Trunc-comm-natural-=⊙∘ 1 (⊙Susp-fmap (fst f)) ⟩
    ⊙–> (Pi2HSusp.⊙eq H-Y) ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp-fmap (fst f))) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm 1 (⊙Susp (de⊙ X))) ◃⊙idf
      =⊙∘⟨ 0 & 2 & Pi2HSuspNaturality.⊙encodeN-natural f H-X H-Y ⟩
    ⊙Trunc-fmap f ◃⊙∘
    ⊙–> (Pi2HSusp.⊙eq H-X) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm (S (S (S ⟨-2⟩))) (⊙Susp (de⊙ X))) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙contract ⟩
    ⊙Trunc-fmap f ◃⊙∘
    ⊙–> (spectrum1 H-X) ◃⊙idf ∎⊙∘

  ⊙–>-spectrumSS-natural : ∀ (n : ℕ)
    → ⊙–> (spectrumSS H-Y n) ◃⊙∘
      ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp^-fmap (S (S n)) f)) ◃⊙idf
      =⊙∘
      ⊙Trunc-fmap (⊙Susp^-fmap (S n) f) ◃⊙∘
      ⊙–> (spectrumSS H-X n) ◃⊙idf
  ⊙–>-spectrumSS-natural n =
    ⊙–> (spectrumSS H-Y n) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp^-fmap (S (S n)) f)) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙–>-spectrumSS H-Y n ⟩
    FS.⊙encodeN H-Y n ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S (S n) ⟩ (⊙Susp^ (S (S n)) Y)) ◃⊙∘
    ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp^-fmap (S (S n)) f)) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙–>-⊙Ω-⊙Trunc-comm-natural-=⊙∘ ⟨ S (S n) ⟩ (⊙Susp^-fmap (S (S n)) f) ⟩
    FS.⊙encodeN H-Y n ◃⊙∘
    ⊙Trunc-fmap (⊙Ω-fmap (⊙Susp^-fmap (S (S n)) f)) ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S (S n) ⟩ (⊙Susp^ (S (S n)) X)) ◃⊙idf
      =⊙∘⟨ 0 & 2 & FreudenthalEquivNatural.⊙encodeN-natural
             ⟨ n ⟩₋₁ ⟨ S (S n) ⟩ (kle n)
             {X = ⊙Susp^ (S n) X} {Y = ⊙Susp^ (S n) Y} (⊙Susp^-fmap (S n) f)
             {{sconn H-X n}} {{sconn H-Y n}} ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap (S n) f) ◃⊙∘
    FS.⊙encodeN H-X n ◃⊙∘
    ⊙–> (⊙Ω-⊙Trunc-comm ⟨ S (S n) ⟩ (⊙Susp^ (S (S n)) X)) ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙–>-spectrumSS H-X n ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap (S n) f) ◃⊙∘
    ⊙–> (spectrumSS H-X n) ◃⊙idf ∎⊙∘

  abstract
    ⊙–>-spectrum-natural : ∀ (n : ℕ)
      → ⊙–> (spectrum H-Y n) ◃⊙∘
        ⊙Ω-fmap (⊙EM-fmap (S n)) ◃⊙idf
        =⊙∘
        ⊙EM-fmap n ◃⊙∘
        ⊙–> (spectrum H-X n) ◃⊙idf
    ⊙–>-spectrum-natural 0 = ⊙–>-spectrum0-natural
    ⊙–>-spectrum-natural 1 = ⊙–>-spectrum1-natural
    ⊙–>-spectrum-natural (S (S n)) = ⊙–>-spectrumSS-natural n

    ⊙<–-spectrum-natural : ∀ (n : ℕ)
      → ⊙<– (spectrum H-Y n) ◃⊙∘
        ⊙EM-fmap n ◃⊙idf
        =⊙∘
        ⊙Ω-fmap (⊙EM-fmap (S n)) ◃⊙∘
        ⊙<– (spectrum H-X n) ◃⊙idf
    ⊙<–-spectrum-natural n =
      ⊙<– (spectrum H-Y n) ◃⊙∘
      ⊙EM-fmap n ◃⊙idf
        =⊙∘⟨ 2 & 0 & !⊙∘ $ ⊙<–-inv-r-=⊙∘ (spectrum H-X n) ⟩
      ⊙<– (spectrum H-Y n) ◃⊙∘
      ⊙EM-fmap n ◃⊙∘
      ⊙–> (spectrum H-X n) ◃⊙∘
      ⊙<– (spectrum H-X n) ◃⊙idf
        =⊙∘⟨ 1 & 2 & !⊙∘ (⊙–>-spectrum-natural n) ⟩
      ⊙<– (spectrum H-Y n) ◃⊙∘
      ⊙–> (spectrum H-Y n) ◃⊙∘
      ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp^-fmap n f)) ◃⊙∘
      ⊙<– (spectrum H-X n) ◃⊙idf
        =⊙∘⟨ 0 & 2 & ⊙<–-inv-l-=⊙∘ (spectrum H-Y n) ⟩
      ⊙Ω-fmap (⊙Trunc-fmap (⊙Susp^-fmap n f)) ◃⊙∘
      ⊙<– (spectrum H-X n) ◃⊙idf ∎⊙∘

module EMExplicit {i} (G : AbGroup i) where
  module HSpace = EM₁HSpace G
  open EMImplicit
    {X = ⊙EM₁ (AbGroup.grp G)}
    {{EM₁-conn}}
    {{EM₁-level₁ (AbGroup.grp G)}}
    HSpace.H-⊙EM₁ public

  open BelowDiagonal public using (πS-below)

  πS-diag : (n : ℕ) → πS n (⊙EM (S n)) ≃ᴳ AbGroup.grp G
  πS-diag n = π₁-EM₁ (AbGroup.grp G) ∘eᴳ OnDiagonal.πS-diag n

  open AboveDiagonal public using (πS-above)

  abstract
    spectrum : (n : ℕ) → ⊙Ω (⊙EM (S n)) ⊙≃ ⊙EM n
    spectrum = Spectrum.spectrum

    spectrum-def : ∀ n → spectrum n == Spectrum.spectrum n
    spectrum-def n = idp

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definitions for Characters
------------------------------------------------------------------------

module Data.Char.Core where

open import Data.Nat using (ℕ)
open import Data.Bool using (Bool; true; false)

------------------------------------------------------------------------
-- The type

postulate
  Char : Set

{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}

------------------------------------------------------------------------
-- Primitive operations

primitive
  primCharToNat    : Char → ℕ
  primCharEquality : Char → Char → Bool
-- primShowChar is in Data.String.Core for break an import cycle.


text:
module Imports.Bool where

data Bool : Set where
  true false : Bool


text:
module AKS.Rational where

open import AKS.Rational.Base public
open import AKS.Rational.Properties public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
-- Andreas, 2017-12-03, issue #2826, reported by Snicksi, shrunk by sattlerc

data A : Set where
  a : A

data B : Set where
  b : (x : A) → B

foo : B → B
foo s with a
-- WAS: case splitting produces repeated variables in pattern
foo s | x = {!s!}

-- Expected: Something like the following
-- foo (b x₁) | x = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

--open import HoTT
open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose
import homotopy.3x3.To as To
import homotopy.3x3.From as From
open import homotopy.3x3.Common

module homotopy.3x3.FromTo2 {i} (d : Span^2 {i}) where

open Span^2 d
open M d hiding (Pushout^2)
open M (transpose d) using () renaming (module F₁∙ to F∙₁; f₁∙ to f∙₁;
                                        module F₃∙ to F∙₃; f₃∙ to f∙₃;
                                        v-h-span to h-v-span)
open M using (Pushout^2)

open To d
open From d

open import homotopy.3x3.FromToInit d

module M2 (c : A₂₂) where

  coh : ∀ {i} {A : Type i} {a b c d : A}
    {p q : a == b} (α : p == q)
    {v w : b == d} {β β' : w == v} (eqβ : β == β')
    {t u : a == c} {ε ε' : u == t} (eqε : ε == ε')
    {r s : c == d} (ζ : r == s)
    (γ : (q , v =□ t , s))
    (δ : (p , w =□ u , r))
    (eq : γ == δ ∙□-i/ ! β' / ε' / ∙□-o/ ! α / ζ /)
    → (α , β , γ =□□ δ , ε , ζ)
  coh idp {β = idp} idp {ε = idp} idp idp _ _ x = x

  end-lemma1 : ap (right ∘ f₃∙) (glue c) == ap (from ∘ i₄∙ ∘ f₃∙) (glue c) :> E∙₂Red.T-lhs c
  end-lemma1 =
    ap (right ∘ f₃∙) (glue c)
         =⟨ ap-∘ right f₃∙ (glue c) ⟩
    ap right (ap f₃∙ (glue c))
         =⟨ ap (ap right) (F₃∙.glue-β c) ⟩
    ap right (ap left (H₃₁ c) ∙ glue (f₃₂ c) ∙ ap right (H₃₃ c))
         =⟨ ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c) ⟩
    ap (right ∘ left) (H₃₁ c) ∙ ap right (glue (f₃₂ c)) ∙ ap (right ∘ right) (H₃₃ c)
         =⟨ ! (from-to-r-g (f₃₂ c)) |in-ctx (λ u → ap (right ∘ left) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)) ⟩
    ap (right ∘ left) (H₃₁ c) ∙ (ap (from ∘ i₄∙) (glue (f₃₂ c))) ∙ ap (right ∘ right) (H₃₃ c)
         =⟨ ! (ap-∙∙`∘`∘ (from ∘ i₄∙) left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)) ⟩
    ap (from ∘ i₄∙) (ap left (H₃₁ c) ∙ glue (f₃₂ c) ∙ ap right (H₃₃ c))
         =⟨ ! (ap (ap (from ∘ i₄∙)) (F₃∙.glue-β c)) ⟩
    ap (from ∘ i₄∙) (ap f₃∙ (glue c))
         =⟨ ∘-ap (from ∘ i₄∙) f₃∙ (glue c) ⟩
    ap (from ∘ i₄∙ ∘ f₃∙) (glue c) ∎

  lemma1 : ↓-='-out (apd (from-to-r ∘ f₃∙) (glue c)) == end-lemma1
  lemma1 =
    ↓-='-out (apd (from-to-r ∘ f₃∙) (glue c))

         =⟨ apd-∘'' from-to-r f₃∙ (glue c) (F₃∙.glue-β c) |in-ctx ↓-='-out ⟩

    ↓-='-out (↓-ap-out= (λ b → from (to (right b)) == right b) f₃∙ (glue c) (F₃∙.glue-β c) (apd from-to-r (ap left (H₃₁ c) ∙ glue (f₃₂ c) ∙ ap right (H₃₃ c))))

         =⟨ apd-∙∙`∘`∘ from-to-r left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c) |in-ctx (λ u → ↓-='-out (↓-ap-out= (λ b → from (to (right b)) == right b) f₃∙ (glue c) (F₃∙.glue-β c) u)) ⟩

    ↓-='-out (↓-ap-out= (λ b → from (to (right b)) == right b) f₃∙ (glue c) (F₃∙.glue-β c) (↓-ap-in _ _ (apd (λ _ → idp) (H₃₁ c)) ∙ᵈ apd from-to-r (glue (f₃₂ c)) ∙ᵈ ↓-ap-in _ _  (apd (λ _ → idp) (H₃₃ c))))

         =⟨ FromToR.glue-β (f₃₂ c) |in-ctx (λ u → ↓-='-out (↓-ap-out= (λ b → from (to (right b)) == right b) f₃∙ (glue c) (F₃∙.glue-β c)
                                                                      (↓-ap-in _ _ (apd (λ _ → idp) (H₃₁ c)) ∙ᵈ u ∙ᵈ ↓-ap-in _ _  (apd (λ _ → idp) (H₃₃ c))))) ⟩

    ↓-='-out (↓-ap-out= (λ b → from (to (right b)) == right b) f₃∙ (glue c) (F₃∙.glue-β c)
                        (↓-ap-in _ _ (apd (λ _ → idp) (H₃₁ c)) ∙ᵈ ↓-='-in (! (from-to-r-g (f₃₂ c))) ∙ᵈ ↓-ap-in _ _  (apd (λ _ → idp) (H₃₃ c))))

         =⟨ lemma-a _ f₃∙ (glue c) (F₃∙.glue-β c) _ ⟩

    ↓-='-out (↓-ap-in _ _ (apd (λ x → idp {a = right (left x)}) (H₃₁ c)) ∙ᵈ ↓-='-in (! (from-to-r-g (f₃₂ c))) ∙ᵈ ↓-ap-in _ _  (apd (λ _ → idp) (H₃₃ c)))
    ∙□-i/ ap-∘ right f₃∙ (glue c) ∙ ap (ap right) (F₃∙.glue-β c)
        / ! (ap (ap (from ∘ i₄∙)) (F₃∙.glue-β c)) ∙ ∘-ap (from ∘ i₄∙) f₃∙ (glue c) /

         =⟨ lemma-b (glue (f₃₂ c)) (apd (λ _ → idp) (H₃₁ c)) (! (from-to-r-g (f₃₂ c))) (apd (λ _ → idp) (H₃₃ c)) |in-ctx (λ u → u ∙□-i/ ap-∘ right f₃∙ (glue c) ∙ ap (ap right) (F₃∙.glue-β c)
                                      / ! (ap (ap (from ∘ i₄∙)) (F₃∙.glue-β c)) ∙ ∘-ap (from ∘ i₄∙) f₃∙ (glue c) /) ⟩

    (↓-='-out (apd (λ x → idp {a = right (left x)}) (H₃₁ c))
    ∙□h ((! (from-to-r-g (f₃₂ c)))
    ∙□h (↓-='-out (apd (λ _ → idp) (H₃₃ c)))))
    ∙□-i/ ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)
        / ! (ap-∙∙`∘`∘ (from ∘ i₄∙) left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)) /
    ∙□-i/ ap-∘ right f₃∙ (glue c) ∙ ap (ap right) (F₃∙.glue-β c)
        / ! (ap (ap (from ∘ i₄∙)) (F₃∙.glue-β c)) ∙ ∘-ap (from ∘ i₄∙) f₃∙ (glue c) /

         =⟨ coh3 |in-ctx (λ u → u
                                ∙□-i/ ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)
                                    / ! (ap-∙∙`∘`∘ (from ∘ i₄∙) left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)) /
                                ∙□-i/ ap-∘ right f₃∙ (glue c) ∙ ap (ap right) (F₃∙.glue-β c)
                                    / ! (ap (ap (from ∘ i₄∙)) (F₃∙.glue-β c)) ∙ ∘-ap (from ∘ i₄∙) f₃∙ (glue c) /) ⟩

    ((! (from-to-r-g (f₃₂ c))) |in-ctx (λ u → ap (right ∘ left) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))
    ∙□-i/ ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)
        / ! (ap-∙∙`∘`∘ (from ∘ i₄∙) left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)) /
    ∙□-i/ ap-∘ right f₃∙ (glue c) ∙ ap (ap right) (F₃∙.glue-β c)
        / ! (ap (ap (from ∘ i₄∙)) (F₃∙.glue-β c)) ∙ ∘-ap (from ∘ i₄∙) f₃∙ (glue c) /

         =⟨ coh' ⟩
    end-lemma1 ∎  where

      coh' : ∀ {i} {A : Type i} {x y : A} {a b c d e f g h : x == y} {p : a == b} {q : b == c}
        {r : c == d} {s : d == e} {t : e == f} {u : f == g} {v : g == h}
        → (s ∙□-i/ r / t / ∙□-i/ p ∙ q / u ∙ v /) == (a =⟨ p ⟩ b =⟨ q ⟩ c =⟨ r ⟩ d =⟨ s ⟩ e =⟨ t ⟩ f =⟨ u ⟩ g =⟨ v ⟩ h ∎)
      coh' {p = idp} {idp} {idp} {idp} {idp} {idp} {idp} = idp

      coh2 : ∀ {i j} {A : Type i} {B : Type j} {f : A → B} {x y : A} {p : x == y}
        → ↓-='-out (apd (λ x → idp {a = f x}) p) == idp {a = ap f p}
      coh2 {p = idp} = idp

      coh3 : (↓-='-out (apd (λ x → idp {a = right (left x)}) (H₃₁ c))
              ∙□h ((! (from-to-r-g (f₃₂ c)))
              ∙□h (↓-='-out (apd (λ _ → idp) (H₃₃ c))))) == ((! (from-to-r-g (f₃₂ c))) |in-ctx (λ u → ap (right ∘ left) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))
      coh3 =
        ↓-='-out (apd (λ x → idp {a = right (left x)}) (H₃₁ c))
        ∙□h ((! (from-to-r-g (f₃₂ c)))
        ∙□h (↓-='-out (apd (λ _ → idp) (H₃₃ c))))

             =⟨ coh2 {f = right ∘ left} {p = H₃₁ c} |in-ctx (λ u → u ∙□h ((! (from-to-r-g (f₃₂ c))) ∙□h (↓-='-out (apd (λ _ → idp) (H₃₃ c))))) ⟩

        idp {a = ap (right ∘ left) (H₃₁ c)} ∙□h ((! (from-to-r-g (f₃₂ c)))
            ∙□h (↓-='-out (apd (λ _ → idp) (H₃₃ c))))

             =⟨ coh2 {f = right ∘ right} {p = H₃₃ c} |in-ctx (λ u → idp {a = ap (right ∘ left) (H₃₁ c)} ∙□h ((! (from-to-r-g (f₃₂ c))) ∙□h u)) ⟩

        idp {a = ap (right ∘ left) (H₃₁ c)} ∙□h ((! (from-to-r-g (f₃₂ c))) ∙□h idp {a = ap (right ∘ right) (H₃₃ c)})

              =⟨ coh4 (ap (right ∘ left) (H₃₁ c)) (ap (right ∘ right) (H₃₃ c)) (! (from-to-r-g (f₃₂ c))) ⟩

        ((! (from-to-r-g (f₃₂ c))) |in-ctx (λ u → ap (right ∘ left) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c))) ∎  where

          coh4 : ∀ {i} {A : Type i} {x y z t : A} (p : x == y) (q : z == t) {s t : y == z} (r : s == t)
            → (idp {a = p} ∙□h (r ∙□h idp {a = q})) == (r |in-ctx (λ u → p ∙ u ∙ q))
          coh4 idp idp idp = idp

  end-lemma3 : ap (left ∘ f₁∙) (glue c) == ap (from ∘ i₀∙ ∘ f₁∙) (glue c)
  end-lemma3 =
    ap (left ∘ f₁∙) (glue c)
         =⟨ ap-∘ left f₁∙ (glue c) ⟩
    ap left (ap f₁∙ (glue c))
         =⟨ ap (ap left) (F₁∙.glue-β c) ⟩
    ap left (ap left (H₁₁ c) ∙ glue (f₁₂ c) ∙ ap right (H₁₃ c))
         =⟨ ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c) ⟩
    ap (left ∘ left) (H₁₁ c) ∙ ap left (glue (f₁₂ c)) ∙ ap (left ∘ right) (H₁₃ c)
         =⟨ ! (from-to-l-g (f₁₂ c)) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (left ∘ right) (H₁₃ c)) ⟩
    ap (left ∘ left) (H₁₁ c) ∙ (ap (from ∘ i₀∙) (glue (f₁₂ c))) ∙ ap (left ∘ right) (H₁₃ c)
         =⟨ ! (ap-∙∙`∘`∘ (from ∘ i₀∙) left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)) ⟩
    ap (from ∘ i₀∙) (ap left (H₁₁ c) ∙ glue (f₁₂ c) ∙ ap right (H₁₃ c))
         =⟨ ! (ap (ap (from ∘ i₀∙)) (F₁∙.glue-β c)) ⟩
    ap (from ∘ i₀∙) (ap f₁∙ (glue c))
         =⟨ ∘-ap (from ∘ i₀∙) f₁∙ (glue c) ⟩
    ap (from ∘ i₀∙ ∘ f₁∙) (glue c) ∎

  lemma3 : ↓-='-out (apd (from-to-l ∘ f₁∙) (glue c)) == end-lemma3
  lemma3 =
    ↓-='-out (apd (from-to-l ∘ f₁∙) (glue c))

      =⟨ apd-∘'' from-to-l f₁∙ (glue c) (F₁∙.glue-β c) |in-ctx ↓-='-out ⟩

    ↓-='-out (↓-ap-out= (λ b → from (to (left b)) == left b) f₁∙ (glue c) (F₁∙.glue-β c) (apd from-to-l (ap left (H₁₁ c) ∙ glue (f₁₂ c) ∙ ap right (H₁₃ c))))

      =⟨ lemma-a _ f₁∙ (glue c) (F₁∙.glue-β c) (apd from-to-l (ap left (H₁₁ c) ∙ glue (f₁₂ c) ∙ ap right (H₁₃ c))) ⟩

    ↓-='-out (apd from-to-l (ap left (H₁₁ c) ∙ glue (f₁₂ c) ∙ ap right (H₁₃ c)))
    ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /

      =⟨ apd-∙∙`∘`∘ from-to-l left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c) |in-ctx
         (λ u → ↓-='-out u ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /) ⟩

    ↓-='-out (↓-ap-in _ _ (apd (λ _ → idp) (H₁₁ c)) ∙ᵈ apd from-to-l (glue (f₁₂ c)) ∙ᵈ ↓-ap-in _ _ (apd (λ _ → idp) (H₁₃ c)))
    ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /

      =⟨ FromToL.glue-β (f₁₂ c) |in-ctx (λ u → ↓-='-out (↓-ap-in _ _ (apd (λ _ → idp) (H₁₁ c)) ∙ᵈ u ∙ᵈ ↓-ap-in _ _ (apd (λ _ → idp) (H₁₃ c)))
         ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /) ⟩

    ↓-='-out (↓-ap-in _ _ (apd (λ _ → idp) (H₁₁ c)) ∙ᵈ ↓-='-in (! (from-to-l-g (f₁₂ c))) ∙ᵈ ↓-ap-in _ _ (apd (λ _ → idp) (H₁₃ c)))
    ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /

      =⟨ lemma-b (glue (f₁₂ c)) (apd (λ _ → idp) (H₁₁ c)) (! (from-to-l-g (f₁₂ c))) (apd (λ _ → idp) (H₁₃ c))
         |in-ctx (λ u → u ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /) ⟩

    (↓-='-out (apd (λ _ → idp) (H₁₁ c)) ∙□h ((! (from-to-l-g (f₁₂ c))) ∙□h ↓-='-out (apd (λ _ → idp) (H₁₃ c))))
    ∙□-i/ ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c) / ! (ap-∙∙`∘`∘ (from ∘ i₀∙) left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)) /
    ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /

      =⟨ coh2 (left ∘ left) (left ∘ right) (H₁₁ c) (! (from-to-l-g (f₁₂ c))) (H₁₃ c) |in-ctx (λ u →
         u ∙□-i/ ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c) / ! (ap-∙∙`∘`∘ (from ∘ i₀∙) left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)) /
    ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /) ⟩

    ((! (from-to-l-g (f₁₂ c))) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (left ∘ right) (H₁₃ c)))
    ∙□-i/ ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c) / ! (ap-∙∙`∘`∘ (from ∘ i₀∙) left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)) /
    ∙□-i/ ap-∘ left f₁∙ (glue c) ∙ ap (ap left) (F₁∙.glue-β c) / ! (ap (ap (from ∘ to ∘ left)) (F₁∙.glue-β c)) ∙ ∘-ap (from ∘ to ∘ left) f₁∙ (glue c) /

      =⟨ coh3 ⟩

    end-lemma3 ∎  where

      coh2 : ∀ {i i' j} {A : Type i} {A' : Type i'} {B : Type j} (f : A → B) (f' : A' → B)
             {a b : A} {a' b' : A'} (p : a == b) {s s' : f b == f' a'} (q : s == s') (r : a' == b')
             → (↓-='-out (apd (λ x → idp) p) ∙□h (q ∙□h (↓-='-out (apd (λ _ → idp) r))))
               == (q |in-ctx (λ u → ap f p ∙ u ∙ ap f' r))
      coh2 f f' idp idp idp = idp

      coh3 : ∀ {i} {A : Type i} {x y : A} {a b c d e f g h : x == y} {p : a == b} {q : b == c}
        {r : c == d} {s : d == e} {t : e == f} {u : f == g} {v : g == h}
        → (s ∙□-i/ r / t / ∙□-i/ p ∙ q / u ∙ v /) == (a =⟨ p ⟩ b =⟨ q ⟩ c =⟨ r ⟩ d =⟨ s ⟩ e =⟨ t ⟩ f =⟨ u ⟩ g =⟨ v ⟩ h ∎)
      coh3 {p = idp} {idp} {idp} {idp} {idp} {idp} {idp} = idp

{- Lemma 2 -}

  lemma2-7 =
    ↓-='-out (ap↓ (ap from) (apd (glue {d = h-v-span}) (glue c)))

         =⟨ from-glue-glue-β c |in-ctx ↓-='-out ⟩

    ↓-='-out (↓-='-in (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                      ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                       ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /)
              ◃/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /)

         =⟨ thing _ (From.glue-β (left (f₁₂ c))) _ ⟩

    E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
    ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /
    ∙□-o/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) / ∎

  lemma2-6 =
    ap□ from (↓-='-out (apd (glue {d = h-v-span}) (glue c)))

         =⟨ ap□-↓-='-out-β _ _ from (apd (glue {d = h-v-span}) (glue c)) ⟩

    ↓-='-out (ap↓ (ap from) (apd (glue {d = h-v-span}) (glue c)))
    ∙□-i/ ∘-ap from (right ∘ f∙₃) (glue c) / ap-∘ from (left ∘ f∙₁) (glue c) /

         =⟨ lemma2-7 |in-ctx (λ u → (u ∙□-i/ ∘-ap from (right ∘ f∙₃) (glue c) / ap-∘ from (left ∘ f∙₁) (glue c) /)) ⟩

    E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
    ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /
    ∙□-o/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /
    ∙□-i/ ∘-ap from (right ∘ f∙₃) (glue c) / ap-∘ from (left ∘ f∙₁) (glue c) / ∎

  lemma2-5 =
    ap□ from (↓-='-out (apd (glue {d = h-v-span}) (glue c))
              ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)

         =⟨ ap□-∙□-i/ from _ (E₂∙Red.lhs-i c) _ ⟩

    ap□ from (↓-='-out (apd (glue {d = h-v-span}) (glue c)))
    ∙□-i/ ap (ap from) (E₂∙Red.lhs-i c) / ap (ap from) (E₂∙Red.rhs-i c) /

         =⟨ lemma2-6 |in-ctx (λ u → u ∙□-i/ ap (ap from) (E₂∙Red.lhs-i c) / ap (ap from) (E₂∙Red.rhs-i c) /) ⟩

    E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
    ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /
    ∙□-o/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /
    ∙□-i/ ∘-ap from (right ∘ f∙₃) (glue c) / ap-∘ from (left ∘ f∙₁) (glue c) /
    ∙□-i/ ap (ap from) (E₂∙Red.lhs-i c) / ap (ap from) (E₂∙Red.rhs-i c) / ∎

  lemma2'-1 =
    E₂∙Red.ap-ap-coh-lhs-i c from ∙ ap (ap from) (E₂∙Red.lhs-i c) ∙ ∘-ap from (right ∘ f∙₃) (glue c) ∙ E∙₂Red.lhs-o c

         =⟨ eq1 {f = ap from}
                {q = ! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))}
                { ! (F∙₃.glue-β c) |in-ctx (ap right)}
                {∘-ap right f∙₃ (glue c)}
                {p = E₂∙Red.ap-ap-coh-lhs-i c from}
                {∘-ap from (right ∘ f∙₃) (glue c)}
                {ap-∘ i∙₄ f∙₃ (glue c)}
                {F∙₃.glue-β c |in-ctx (ap i∙₄)}
                {ap-∙∙!`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c)}
                {I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))}
          ⟩

    (! (ap-∙∙!'`∘`∘ from (right ∘ left) (right ∘ right) (H₁₃ c) (ap right (glue (f₂₃ c))) (H₃₃ c))
     ∙ ap (ap from) (! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c)))
     ∙ (ap (ap from) (! (F∙₃.glue-β c) |in-ctx (ap right))
        ∙ (ap (ap from) (∘-ap right f∙₃ (glue c))
           ∙ ∘-ap from (right ∘ f∙₃) (glue c)
           ∙ ap-∘ i∙₄ f∙₃ (glue c))
        ∙ (F∙₃.glue-β c |in-ctx (ap i∙₄)))
     ∙ ap-∙∙!`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
    ∙ (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))

         =⟨ ap-∘^3-coh from right f∙₃ (glue c) |in-ctx (λ u →
    (! (ap-∙∙!'`∘`∘ from (right ∘ left) (right ∘ right) (H₁₃ c) (ap right (glue (f₂₃ c))) (H₃₃ c))
     ∙ ap (ap from) (! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c)))
     ∙ (ap (ap from) (! (F∙₃.glue-β c) |in-ctx (ap right))
        ∙ u
        ∙ (F∙₃.glue-β c |in-ctx (ap i∙₄)))
     ∙ ap-∙∙!`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
    ∙ (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))))
          ⟩

    (! (ap-∙∙!'`∘`∘ from (right ∘ left) (right ∘ right) (H₁₃ c) (ap right (glue (f₂₃ c))) (H₃₃ c))
     ∙ ap (ap from) (! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c)))
     ∙ (ap (ap from) (! (F∙₃.glue-β c) |in-ctx (ap right))
        ∙ ∘-ap from right (ap f∙₃ (glue c))
        ∙ (F∙₃.glue-β c |in-ctx (ap i∙₄)))
     ∙ ap-∙∙!`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
    ∙ (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))

         =⟨ ap-∘-ap-coh from right (F∙₃.glue-β c) |in-ctx (λ u →
    (! (ap-∙∙!'`∘`∘ from (right ∘ left) (right ∘ right) (H₁₃ c) (ap right (glue (f₂₃ c))) (H₃₃ c))
     ∙ ap (ap from) (! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c)))
     ∙ u
     ∙ ap-∙∙!`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
    ∙ (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))) ⟩

    (! (ap-∙∙!'`∘`∘ from (right ∘ left) (right ∘ right) (H₁₃ c) (ap right (glue (f₂₃ c))) (H₃₃ c))
     ∙ ap (ap from) (! (ap-∙∙!`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c)))
     ∙ ∘-ap from right (ap left (H₁₃ c) ∙ glue (f₂₃ c) ∙ ap right (! (H₃₃ c)))
     ∙ ap-∙∙!`∘`∘ i∙₄ left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c))
    ∙ (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))

         =⟨ ap-∘-ap-∙∙!`∘`∘-coh from right left right (H₁₃ c) (glue (f₂₃ c)) (H₃₃ c) |in-ctx (λ u →
             u ∙ (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))) ⟩

    (∘-ap from right (glue (f₂₃ c)) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))
    ∙ (I∙₄.glue-β (f₂₃ c) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))))

         =⟨ ∙-|in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c))) (∘-ap from right (glue (f₂₃ c))) (I∙₄.glue-β (f₂₃ c)) ⟩

    ((∘-ap from right (glue (f₂₃ c)) ∙ I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))) ∎

    where

      eq1 : ∀ {i j} {A : Type i} {B : Type j} {f : A → B} {a b c d : A}
        {q : a == b} {r : b == c} {s : c == d}
        {g h k l m n : B} {p : g == f a} {t : f d == h} {u : h == k}
        {v : k == l} {w : l == m} {x : m == n}
         → p ∙ ap f (_ =⟨ q ⟩ _ =⟨ r ⟩ _ =⟨ s ⟩ _ ∎) ∙ t
           ∙ (_ =⟨ u ⟩ _ =⟨ v ⟩ _ =⟨ w ⟩ _ =⟨ x ⟩ _ ∎)
         == (p ∙ ap f q ∙ (ap f r ∙ (ap f s ∙ t ∙ u) ∙ v) ∙ w) ∙ x
      eq1 {q = idp} {idp} {idp} {p = p} {idp} {idp} {idp} {idp} {idp} = ! (∙-unit-r (p ∙ idp))

  lemma2'-2 :
    E∙₂Red.rhs-o c
    ∙ ap-∘ from (left ∘ f∙₁) (glue c)
    ∙ ap (ap from) (E₂∙Red.rhs-i c)
    ∙ E₂∙Red.ap-ap-coh-rhs-i c from
    == (! (∘-ap from left (glue (f₂₁ c)) ∙ I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))
  lemma2'-2 =
    E∙₂Red.rhs-o c ∙ ap-∘ from (left ∘ f∙₁) (glue c) ∙ ap (ap from) (E₂∙Red.rhs-i c) ∙ E₂∙Red.ap-ap-coh-rhs-i c from

      =⟨ eq1 {f = ap from}
             {p = ! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))}
             { ! (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))}
             { ! (F∙₁.glue-β c) |in-ctx (λ u → ap i∙₀ u)}
             {∘-ap i∙₀ f∙₁ (glue c)}
             {ap-∘ from (left ∘ f∙₁) (glue c)}
             {ap-∘ left f∙₁ (glue c)}
             {F∙₁.glue-β c |in-ctx (ap left)}
             {ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)}
             {ap-!'∙∙`∘`∘ from (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₂₁ c))) (H₃₁ c)}
       ⟩

    (! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))))
    ∙ ((! (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)))
       ∙ ((! (F∙₁.glue-β c) |in-ctx (λ u → ap i∙₀ u))
          ∙ (∘-ap i∙₀ f∙₁ (glue c)
             ∙ ap-∘ from (left ∘ f∙₁) (glue c)
             ∙ ap (ap from) (ap-∘ left f∙₁ (glue c)))
          ∙ ap (ap from) (F∙₁.glue-β c |in-ctx (ap left)))
       ∙ ap (ap from) (ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
       ∙ ap-!'∙∙`∘`∘ from (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₂₁ c))) (H₃₁ c))

      =⟨ ap-∘^3-coh' from left f∙₁ (glue c)
         |in-ctx (λ u → (! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))))
    ∙ ((! (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)))
       ∙ ((! (F∙₁.glue-β c) |in-ctx (λ u → ap i∙₀ u))
          ∙ u
          ∙ ap (ap from) (F∙₁.glue-β c |in-ctx (ap left)))
       ∙ ap (ap from) (ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
       ∙ ap-!'∙∙`∘`∘ from (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₂₁ c))) (H₃₁ c))) ⟩

    (! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))))
    ∙ ((! (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)))
       ∙ ((! (F∙₁.glue-β c) |in-ctx (ap i∙₀))
          ∙ ap-∘ from left (ap f∙₁ (glue c))
          ∙ ap (ap from) (F∙₁.glue-β c |in-ctx (ap left)))
       ∙ ap (ap from) (ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
       ∙ ap-!'∙∙`∘`∘ from (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₂₁ c))) (H₃₁ c))

      =⟨ ap-∘-ap-coh' from left (F∙₁.glue-β c)
         |in-ctx (λ u → (! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))))
    ∙ ((! (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)))
       ∙ u
       ∙ ap (ap from) (ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
       ∙ ap-!'∙∙`∘`∘ from (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₂₁ c))) (H₃₁ c))) ⟩

    (! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))))
    ∙ ((! (ap-!∙∙`∘`∘ i∙₀ left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)))
       ∙ ap-∘ from left (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c))
       ∙ ap (ap from) (ap-!∙∙`∘`∘ left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c))
       ∙ ap-!'∙∙`∘`∘ from (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₂₁ c))) (H₃₁ c))

      =⟨ ap-∘-ap-!∙∙`∘`∘-coh from left left right (H₁₁ c) (glue (f₂₁ c)) (H₃₁ c)
         |in-ctx (λ u → (! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))) ∙ u) ⟩

    (! (I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → (! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))))
    ∙ (ap-∘ from left (glue (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)))

      =⟨ coh2 (glue (f₂₁ c)) (I∙₀.glue-β (f₂₁ c)) ⟩

    (! (∘-ap from left (glue (f₂₁ c)) ∙ I∙₀.glue-β (f₂₁ c)) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))) ∎

    where

      eq1 : ∀ {i j} {A : Type i} {B : Type j} {f : A → B} {a b c d e : B} {k l m n : A} {o : B}
         {p : a == b} {q : b == c} {r : c == d} {s : d == e} {t : e == f k} {u : k == l}
         {v : l == m} {w : m == n} {x : f n == o}
         → (_ =⟨ p ⟩ _ =⟨ q ⟩ _ =⟨ r ⟩ _ =⟨ s ⟩ _ ∎) ∙ t ∙ ap f (_ =⟨ u ⟩ _ =⟨ v ⟩ _ =⟨ w ⟩ _ ∎) ∙ x
         == (p ∙ (q ∙ ((r ∙ (s ∙ t ∙ ap f u) ∙ ap f v) ∙ ap f w ∙ x)))
      eq1 {p = idp} {idp} {idp} {idp} {t = t} {idp} {idp} {idp} {idp} = ! (∙-unit-r (t ∙ idp)) ∙ ! (∙-unit-r ((t ∙ idp) ∙ idp))

      coh2 : ∀ {i j k l} {A : Type i} {B : Type j} {C : Type k} {D : Type l}
        {a a' : A} (q : a == a') {h : A → B} {g : B → C} {f : (g (h a) == g (h a')) → D} {r : g (h a) == g (h a')} (p : ap (g ∘ h) q == r)
        → ((! p) |in-ctx f) ∙ (ap-∘ g h q |in-ctx f) == (! (∘-ap g h q ∙ p) |in-ctx f)
      coh2 idp p = ∙-unit-r _

  lemma2-4' =
    ap□ from (↓-='-out (apd (glue {d = h-v-span}) (glue c))
              ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
    ∙□-i/ E₂∙Red.ap-ap-coh-lhs-i c from / E₂∙Red.ap-ap-coh-rhs-i c from /

         =⟨ lemma2-5 |in-ctx (λ u → u ∙□-i/ E₂∙Red.ap-ap-coh-lhs-i c from / E₂∙Red.ap-ap-coh-rhs-i c from /) ⟩

    E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
    ∙□-i/ E∙₂Red.lhs-o c / E∙₂Red.rhs-o c /
    ∙□-o/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /
    ∙□-i/ ∘-ap from (right ∘ f∙₃) (glue c) / ap-∘ from (left ∘ f∙₁) (glue c) /
    ∙□-i/ ap (ap from) (E₂∙Red.lhs-i c) / ap (ap from) (E₂∙Red.rhs-i c) /
    ∙□-i/ E₂∙Red.ap-ap-coh-lhs-i c from / E₂∙Red.ap-ap-coh-rhs-i c from /

         =⟨ assoc (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /))
                   (E∙₂Red.lhs-o c) (∘-ap from (right ∘ f∙₃) (glue c)) (ap (ap from) (E₂∙Red.lhs-i c))
                   (E₂∙Red.ap-ap-coh-lhs-i c from) _ _ _ _ (From.glue-β (left (f₁₂ c))) _ ⟩

    E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
    ∙□-o/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /
    ∙□-i/ E₂∙Red.ap-ap-coh-lhs-i c from ∙ ap (ap from) (E₂∙Red.lhs-i c) ∙ ∘-ap from (right ∘ f∙₃) (glue c) ∙ E∙₂Red.lhs-o c
        / E∙₂Red.rhs-o c ∙ ap-∘ from (left ∘ f∙₁) (glue c) ∙ ap (ap from) (E₂∙Red.rhs-i c) ∙ E₂∙Red.ap-ap-coh-rhs-i c from /

         =⟨ ∙□-i/-rewrite (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
    ∙□-o/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /) lemma2'-1 lemma2'-2 ⟩ -- rewrite

    E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
    ∙□-o/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /
    ∙□-i/ (∘-ap from right (glue (f₂₃ c)) ∙ I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))
        / (! (∘-ap from left (glue (f₂₁ c)) ∙ I∙₀.glue-β (f₂₁ c))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c)) / ∎  where

      assoc : ∀ {i} {A : Type i} {a b b' c : A} {u u' : a == b} {v v1 v2 v3 v4 : b == c}
         {w w1 w2 w3 w4 : a == b'} {x x' : b' == c} (α : (u , v =□ w , x))
         (p1 : v1 == v) (p2 : v2 == v1) (p3 : v3 == v2) (p4 : v4 == v3)
         (q1 : w == w1) (q2 : w1 == w2) (q3 : w2 == w3) (q4 : w3 == w4)
         (r : u' == u) (s : x == x')
         → α ∙□-i/ p1 / q1 / ∙□-o/ r / s / ∙□-i/ p2 / q2 / ∙□-i/ p3 / q3 / ∙□-i/ p4 / q4 /
         == α ∙□-o/ r / s / ∙□-i/ p4 ∙ p3 ∙ p2 ∙ p1 / q1 ∙ q2 ∙ q3 ∙ q4 /
      assoc α idp idp idp idp idp idp idp idp idp idp = idp

  lemma2-4'' =
    E₂∙Red.ap-ap-coh c from (ap□ from (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                                       ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
                             ∙□-i/ E₂∙Red.ap-ap-coh-lhs-i c from / E₂∙Red.ap-ap-coh-rhs-i c from /)

         =⟨ lemma2-4' |in-ctx (E₂∙Red.ap-ap-coh c from) ⟩

    E₂∙Red.ap-ap-coh c from (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                            ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                             ∙□-o/ From.glue-β (left (f₁₂ c)) / ! (From.glue-β (right (f₃₂ c))) /
                             ∙□-i/ (∘-ap from right (glue (f₂₃ c)) ∙ I∙₄.glue-β (f₂₃ c)) |in-ctx (λ u → ap (left ∘ right) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))
                                 / (! (∘-ap from left (glue (f₂₁ c)) ∙ I∙₀.glue-β (f₂₁ c))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (right ∘ left) (H₃₁ c))/)

         =⟨ lemma (∘-ap from left (glue (f₂₁ c)) ∙ I∙₀.glue-β (f₂₁ c)) (From.glue-β (right (f₃₂ c))) (From.glue-β (left (f₁₂ c))) (∘-ap from right (glue (f₂₃ c)) ∙ I∙₄.glue-β (f₂₃ c))
                   (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                   ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /) ⟩

    ↓-='-out (apd (glue {d = v-h-span}) (glue c))
    ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /
    ∙□-o/ ∘-ap from left (glue (f₂₁ c)) ∙ I∙₀.glue-β (f₂₁ c) / ! (∘-ap from right (glue (f₂₃ c)) ∙ I∙₄.glue-β (f₂₃ c)) /
    ∙□-i/ (From.glue-β (right (f₃₂ c))) |in-ctx (λ u → ap (right ∘ left) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c))
        / (! (From.glue-β (left (f₁₂ c)))) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (left ∘ right) (H₁₃ c)) / ∎

  lemma2-4 =
    ap□ from (E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                            ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /))

         =⟨ E₂∙Red.ap-ap-coh-β c from (↓-='-out (apd (glue {d = h-v-span}) (glue c)) ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /) ⟩

    E₂∙Red.ap-ap-coh c from (ap□ from (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                                       ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
                             ∙□-i/ E₂∙Red.ap-ap-coh-lhs-i c from / E₂∙Red.ap-ap-coh-rhs-i c from /)
    ∙□-i/ E₂∙Red.ap-ap-coh-lhs-o c from / E₂∙Red.ap-ap-coh-rhs-o c from /

         =⟨ lemma2-4'' |in-ctx (λ u → u ∙□-i/ E₂∙Red.ap-ap-coh-lhs-o c from / E₂∙Red.ap-ap-coh-rhs-o c from /) ⟩

    ↓-='-out (apd (glue {d = v-h-span}) (glue c))
    ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /
    ∙□-o/ ∘-ap from left (glue (f₂₁ c)) ∙ I∙₀.glue-β (f₂₁ c) / ! (∘-ap from right (glue (f₂₃ c)) ∙ I∙₄.glue-β (f₂₃ c)) /
    ∙□-i/ (From.glue-β (right (f₃₂ c))) |in-ctx (λ u → ap (right ∘ left) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c))
        / (! (From.glue-β (left (f₁₂ c)))) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (left ∘ right) (H₁₃ c)) /
    ∙□-i/ E₂∙Red.ap-ap-coh-lhs-o c from / E₂∙Red.ap-ap-coh-rhs-o c from / ∎

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda


text:
module _ where

open import Common.Prelude
open import Common.Equality

record Functor (F : Set → Set) : Set₁ where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

open Functor {{...}} public

record Applicative (F : Set → Set) : Set₁ where
  field
    pure  : ∀ {A} → A → F A
    _<*>_ : ∀ {A B} → F (A → B) → F A → F B
    instance Fun : Functor F

  defaultApplicativeFunctor : Functor F
  fmap {{defaultApplicativeFunctor}} f x = pure f <*> x

open Applicative {{...}} public hiding (Fun)

-- Concrete instances --

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

vmap : ∀ {A B n} → (A → B) → Vec A n → Vec B n
vmap f [] = []
vmap f (x ∷ xs) = f x ∷ vmap f xs

it : ∀ {a} {A : Set a} {{_ : A}} → A
it {{x}} = x

pureV : ∀ {n A} → A → Vec A n
pureV {zero} _ = []
pureV {suc n} x = x ∷ pureV x

instance
  FunctorVec : ∀ {n} → Functor (λ A → Vec A n)
  fmap {{FunctorVec}} = vmap

  ApplicativeVec : ∀ {n} → Applicative (λ A → Vec A n)
  pure  {{ApplicativeVec}} x = pureV x
  _<*>_ {{ApplicativeVec}} []       []       = []
  _<*>_ {{ApplicativeVec}} (f ∷ fs) (x ∷ xs) = f x ∷ (fs <*> xs)
  Applicative.Fun ApplicativeVec = FunctorVec

-- In this case there are two candidates for Functor Vec:
--   FunctorVec and Applicative.Fun ApplicativeVec
-- but since they are equal everything works out.
testVec : ∀ {n} → Vec Nat n → Vec Nat n → Vec Nat n
testVec xs ys = fmap _+_ xs <*> ys

what : ∀ {n} → FunctorVec {n} ≡ it
what = refl


text:
module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

postulate
  String : Set
{-# BUILTIN STRING String #-}

primitive
  @0 ⦃ primShowNat ⦄ : Nat → String

-- Wrong modality for primitive primShowNat
--   Got:      instance, erased
--   Expected: visible, unrestricted
-- when checking that the type of the primitive function primShowNat
-- is Nat → String


text:
{-# OPTIONS --without-K #-}
module PathStructure.Sigma {a b} {A : Set a} {B : A → Set b} where

open import Equivalence
open import PathOperations
open import Transport
open import Types

ap₂-dep : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Set c}
  {x x′ : A} {y : B x} {y′ : B x′}
  (f : (a : A) (b : B a) → C) (p : x ≡ x′) (q : tr B p y ≡ y′) →
  f x y ≡ f x′ y′
ap₂-dep {B = B} f p q = J
  (λ x x′ p → (y : B x) (y′ : B x′) (q : tr B p y ≡ y′) → f x y ≡ f x′ y′)
  (λ x _ _ q → ap (f x) q)
  _ _ p _ _ q

ap₂-dep-eq : ∀ {a b c} {A : Set a} {B : A → Set b} {C : Set c}
  (f : (x : A) → B x → C)
  {x x′ : A} (p p′ : x ≡ x′) (pp : p ≡ p′)
  {y : B x} {y′ : B x′} (q : tr B p y ≡ y′) (q′ : tr B p′ y ≡ y′)
  (qq : tr (λ z → tr B z y ≡ y′) pp q ≡ q′) →
  ap₂-dep f p q ≡ ap₂-dep f p′ q′
ap₂-dep-eq {B = B} f {x = x} {x′ = x′} p p′ pp q q′ qq = J
  (λ p p′ pp → (y : B x) (y′ : B x′)
    (q : tr B p y ≡ y′) (q′ : tr B p′ y ≡ y′)
    (qq : tr (λ z → tr B z y ≡ y′) pp q ≡ q′) →
    ap₂-dep f p q ≡ ap₂-dep f p′ q′)
  (λ p _ _ q q′ qq → J
    (λ q q′ qq → ap₂-dep f p q ≡ ap₂-dep f p q′)
    (λ _ → refl)
    _ _ qq)
  _ _ pp _ _ _ _ qq

split-path : {x y : Σ A B} →
  x ≡ y → Σ (π₁ x ≡ π₁ y) (λ p → tr B p (π₂ x) ≡ π₂ y)
split-path {x = x} p = ap π₁ p , tr-∘ π₁ p (π₂ x) ⁻¹ · apd π₂ p

merge-path : {x y : Σ A B} →
  Σ (π₁ x ≡ π₁ y) (λ p → tr B p (π₂ x) ≡ π₂ y) → x ≡ y
merge-path pq = ap₂-dep _,_ (π₁ pq) (π₂ pq)

split-merge-eq : {x y : Σ A B} →
  (x ≡ y) ≃ Σ (π₁ x ≡ π₁ y) (λ p → tr B p (π₂ x) ≡ π₂ y)
split-merge-eq
  = split-path
  , (merge-path , λ pq → J
      (λ x x′ p → (y : B x) (y′ : B x′) (q : tr B p y ≡ y′) →
        split-path (merge-path (p , q)) ≡ p , q)
      (λ x y y′ q → J {A = B x}
        (λ _ _ q → split-path (merge-path (refl , q)) ≡ refl , q)
        (λ _ → refl) _ _ q)
      _ _ (π₁ pq) _ _ (π₂ pq))
  , (merge-path , J
      (λ _ _ p → merge-path (split-path p) ≡ p)
      (λ _ → refl) _ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive IO: simple bindings to Haskell types and functions
------------------------------------------------------------------------

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

module IO.Primitive where

open import Codata.Musical.Costring
open import Data.Char.Base
open import Data.String.Base
open import Foreign.Haskell

------------------------------------------------------------------------
-- The IO monad

open import Agda.Builtin.IO public using (IO)

infixl 1 _>>=_

postulate
  return : ∀ {a} {A : Set a} → A → IO A
  _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B

{-# COMPILE GHC return = \_ _ -> return    #-}
{-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
{-# COMPILE UHC return = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
{-# COMPILE UHC _>>=_  = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}

------------------------------------------------------------------------
-- Simple lazy IO

-- Note that the functions below produce commands which, when
-- executed, may raise exceptions.

-- Note also that the semantics of these functions depends on the
-- version of the Haskell base library. If the version is 4.2.0.0 (or
-- later?), then the functions use the character encoding specified by
-- the locale. For older versions of the library (going back to at
-- least version 3) the functions use ISO-8859-1.

{-# FOREIGN GHC import qualified Data.Text    #-}
{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# FOREIGN GHC import qualified System.IO    #-}
{-# FOREIGN GHC import qualified Control.Exception #-}

postulate
  getContents : IO Costring
  readFile    : String → IO Costring
  writeFile   : String → Costring → IO Unit
  appendFile  : String → Costring → IO Unit
  putStr      : Costring → IO Unit
  putStrLn    : Costring → IO Unit

  -- Reads a finite file. Raises an exception if the file path refers
  -- to a non-physical file (like "/dev/zero").

  readFiniteFile : String → IO String

{-# FOREIGN GHC
  readFiniteFile :: Data.Text.Text -> IO Data.Text.Text
  readFiniteFile f = do
    h <- System.IO.openFile (Data.Text.unpack f) System.IO.ReadMode
    Control.Exception.bracketOnError (return ()) (\_ -> System.IO.hClose h)
                                                 (\_ -> System.IO.hFileSize h)
    Data.Text.IO.hGetContents h

  fromColist :: MAlonzo.Code.Codata.Musical.Colist.AgdaColist a -> [a]
  fromColist MAlonzo.Code.Codata.Musical.Colist.Nil         = []
  fromColist (MAlonzo.Code.Codata.Musical.Colist.Cons x xs) =
    x : fromColist (MAlonzo.RTE.flat xs)

  toColist :: [a] -> MAlonzo.Code.Codata.Musical.Colist.AgdaColist a
  toColist []       = MAlonzo.Code.Codata.Musical.Colist.Nil
  toColist (x : xs) =
    MAlonzo.Code.Codata.Musical.Colist.Cons x (MAlonzo.RTE.Sharp (toColist xs))
#-}

{-# COMPILE GHC getContents    = fmap toColist getContents                          #-}
{-# COMPILE GHC readFile       = fmap toColist . readFile . Data.Text.unpack        #-}
{-# COMPILE GHC writeFile      = \x -> writeFile (Data.Text.unpack x) . fromColist  #-}
{-# COMPILE GHC appendFile     = \x -> appendFile (Data.Text.unpack x) . fromColist #-}
{-# COMPILE GHC putStr         = putStr . fromColist                                #-}
{-# COMPILE GHC putStrLn       = putStrLn . fromColist                              #-}
{-# COMPILE GHC readFiniteFile = readFiniteFile                        #-}
{-# COMPILE UHC getContents    = UHC.Agda.Builtins.primGetContents     #-}
{-# COMPILE UHC readFile       = UHC.Agda.Builtins.primReadFile        #-}
{-# COMPILE UHC writeFile      = UHC.Agda.Builtins.primWriteFile       #-}
{-# COMPILE UHC appendFile     = UHC.Agda.Builtins.primAppendFile      #-}
{-# COMPILE UHC putStr         = UHC.Agda.Builtins.primPutStr          #-}
{-# COMPILE UHC putStrLn       = UHC.Agda.Builtins.primPutStrLn        #-}
{-# COMPILE UHC readFiniteFile = UHC.Agda.Builtins.primReadFiniteFile  #-}


text:
module product where

open import Data.Nat using (ℕ; _*_)
open import lists using (List; foldr)

-- リストの要素の積
product : (List ℕ) → ℕ
product xs = foldr _*_ 1 xs

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue229 where

open import Common.Level

data Works a b : Set (lsuc a ⊔ lsuc b) where
  w : (A : Set a)(B : Set b) → Works a b

record Doesn'tWork a b : Set (lsuc a ⊔ lsuc b) where
  field
    A : Set a
    B : Set b

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Interaction/Highlighting/Generate.hs:469


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

module Data.List.Kleene where

open import Prelude
open import Data.Fin

mutual
  infixr 5 _&_ ∹_
  infixl 5 _⁺ _⋆
  record _⁺ {a} (A : Set a) : Set a where
    inductive
    constructor _&_
    field
      head : A
      tail : A ⋆

  data _⋆ {a} (A : Set a) : Set a where
    [] : A ⋆
    ∹_ : A ⁺ → A ⋆
open _⁺ public

mutual
  foldr⁺ : (A → B → B) → B → A ⁺ → B
  foldr⁺ f b (x & xs) = f x (foldr⋆ f b xs)

  foldr⋆ : (A → B → B) → B → A ⋆ → B
  foldr⋆ f b [] = b
  foldr⋆ f b (∹ xs) = foldr⁺ f b xs

length⋆ : A ⋆ → ℕ
length⋆ = foldr⋆ (const suc) zero

length⁺ : A ⁺ → ℕ
length⁺ = foldr⁺ (const suc) zero

mutual
  _!⁺_ : (xs : A ⁺) → Fin (length⁺ xs) → A
  xs !⁺ f0  = xs .head
  xs !⁺ fs i = xs .tail !⋆ i

  _!⋆_ : (xs : A ⋆) → Fin (length⋆ xs) → A
  (∹ xs) !⋆ i = xs !⁺ i

map⋆ : (A → B) → A ⋆ → B ⋆
map⋆ f = foldr⋆ (λ x xs → ∹ f x & xs) []

map⁺ : (A → B) → A ⁺ → B ⁺
map⁺ f (x & xs) = f x & map⋆ f xs

mutual
  _⋆++⋆_ : A ⋆ → A ⋆ → A ⋆
  [] ⋆++⋆ ys = ys
  (∹ xs) ⋆++⋆ ys = ∹ (xs ⁺++⋆ ys)

  _⁺++⋆_ : A ⁺ → A ⋆ → A ⁺
  head (xs ⁺++⋆ ys) = head xs
  tail (xs ⁺++⋆ ys) = tail xs ⋆++⋆ ys

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Lemma for `Constructive.Axiom.Properties.Base`

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

module Constructive.Axiom.Properties.Base.Lemma where

-- agda-stdlib
open import Data.Empty
open import Data.Nat
import Data.Nat.Properties as ℕₚ
open import Data.Product
open import Data.Sum as Sum
open import Data.Sum.Properties
open import Function.Base
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

-- agda-misc
open import Constructive.Combinators
open import Constructive.Common

-- lemma for `ℕ-llpo⇒mp∨`
ℕ≤-any-dec : ∀ {p} {P : ℕ → Set p} → DecU P → DecU (λ n → ∃ λ m → m ≤ n × P m)
ℕ≤-any-dec {P = P} P? zero with P? 0
... | inj₁  P0 = inj₁ (0 , ℕₚ.≤-refl , P0)
... | inj₂ ¬P0 = inj₂ λ {(m , m≤0 , Pm) → ¬P0 (subst P (ℕₚ.n≤0⇒n≡0 m≤0) Pm)}
ℕ≤-any-dec P? (suc n) with P? 0
... | inj₁  P0 = inj₁ (0 , (z≤n , P0))
... | inj₂ ¬P0 with ℕ≤-any-dec (P? ∘ suc) n
ℕ≤-any-dec {P = P} P? (suc n) | inj₂ ¬P0 | inj₁ (m , m≤n , Psm) =
  inj₁ (suc m , s≤s m≤n , Psm)
ℕ≤-any-dec {P = P} P? (suc n) | inj₂ ¬P0 | inj₂ ¬∃m→m≤n×Psm     = inj₂ f
  where
  f : (∃ λ m → m ≤ suc n × P m) → ⊥
  f (zero  , m≤sn  , Pm)  = ¬P0 Pm
  f (suc m , sm≤sn , Psm) = ¬∃m→m≤n×Psm (m , (ℕₚ.≤-pred sm≤sn , Psm))

private
  1+n≰0 : ∀ n → ¬ (suc n ≤ 0)
  1+n≰0 n ()

module _ {p} {P : ℕ → Set p} (P? : DecU P) where
  ℕ<-any-dec : DecU (λ n → ∃ λ m → m < n × P m)
  ℕ<-any-dec zero           = inj₂ λ {(m , m<0 , _) → 1+n≰0 m m<0}
  ℕ<-any-dec (suc n) with ℕ≤-any-dec P? n
  ... | inj₁ (m , m≤n , Pm) = inj₁ (m , s≤s m≤n , Pm)
  ... | inj₂ ¬∃m→m≤n×Pm     = inj₂ (contraposition f ¬∃m→m≤n×Pm)
    where
    f : (∃ λ m → suc m ≤ suc n × P m) → ∃ λ m → m ≤ n × P m
    f (m , sm≤sn , Pm) = m , (ℕₚ.≤-pred sm≤sn , Pm)

  ℕ≤-all-dec : DecU (λ n → ∀ m → m ≤ n → P m)
  ℕ≤-all-dec n with ℕ≤-any-dec (¬-DecU P?) n
  ... | inj₁ (m , m≤n , ¬Pm) = inj₂ λ ∀i→i≤n→Pi → ¬Pm (∀i→i≤n→Pi m m≤n)
  ... | inj₂ ¬∃m→m≤n×¬Pm     =
    inj₁ λ m m≤n → DecU⇒stable P? m λ ¬Pm → ¬∃m→m≤n×¬Pm (m , m≤n , ¬Pm)

module _ {p} {P : ℕ → Set p} (P? : DecU P) where
  ℕ<-all-dec : DecU (λ n → ∀ m → m < n → P m)
  ℕ<-all-dec n with ℕ<-any-dec (¬-DecU P?) n
  ... | inj₁ (m , m<n , ¬Pm) = inj₂ λ ∀i→i<n→Pi → ¬Pm (∀i→i<n→Pi m m<n)
  ... | inj₂ ¬∃m→m<n×¬Pm     =
    inj₁ λ m m<n → DecU⇒stable P? m λ ¬Pm → ¬∃m→m<n×¬Pm (m , m<n , ¬Pm)

-- lemma for llpo-ℕ⇒llpo
lemma₁ : ∀ {p} {P : ℕ → Set p} →
         (∀ m n → m ≢ n → P m ⊎ P n) →
         ∃ (λ n → ¬ P (2 * n)) → ∃ (λ n → ¬ P (suc (2 * n))) → ⊥
lemma₁ ∀mn→m≢n→Pm⊎Pn (m , ¬P2m) (n , ¬P1+2n) with
  ∀mn→m≢n→Pm⊎Pn (2 * m) (suc (2 * n)) (ℕₚ.even≢odd m n)
... | inj₁ P2m   = ¬P2m P2m
... | inj₂ P1+2n = ¬P1+2n P1+2n

parity : ℕ → ℕ ⊎ ℕ
parity zero          = inj₁ zero
parity (suc zero)    = inj₂ zero
parity (suc (suc n)) = Sum.map suc suc (parity n)

parity-even : ∀ n → parity (2 * n) ≡ inj₁ n
parity-even zero    = refl
parity-even (suc n) = begin
  parity (2 * (suc n))             ≡⟨ cong parity (ℕₚ.*-distribˡ-+ 2 1 n) ⟩
  parity (2 + 2 * n)               ≡⟨⟩
  Sum.map suc suc (parity (2 * n)) ≡⟨ cong (Sum.map suc suc) (parity-even n) ⟩
  Sum.map suc suc (inj₁ n)         ≡⟨⟩
  inj₁ (suc n)                     ∎
  where open ≡-Reasoning

parity-odd : ∀ n → parity (suc (2 * n)) ≡ inj₂ n
parity-odd zero    = refl
parity-odd (suc n) = begin
  parity (suc (2 * suc n))             ≡⟨ cong (parity ∘ suc) $ ℕₚ.*-distribˡ-+ 2 1 n ⟩
  parity (1 + (2 * 1 + 2 * n))         ≡⟨⟩
  parity (2 + (1 + 2 * n))             ≡⟨⟩
  Sum.map suc suc (parity (1 + 2 * n)) ≡⟨ cong (Sum.map suc suc) (parity-odd n) ⟩
  Sum.map suc suc (inj₂ n)             ≡⟨⟩
  inj₂ (suc n)                         ∎
  where open ≡-Reasoning

Sum-map-injective : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
                    {f : A → C} {g : B → D} →
                    (∀ {u v} → f u ≡ f v → u ≡ v) →
                    (∀ {u v} → g u ≡ g v → u ≡ v) → ∀ {x y} →
                    Sum.map f g x ≡ Sum.map f g y → x ≡ y
Sum-map-injective f-inj g-inj {inj₁ x} {inj₁ x₁} eq = cong inj₁ (f-inj (inj₁-injective eq))
Sum-map-injective f-ing g-inj {inj₂ y} {inj₂ y₁} eq = cong inj₂ (g-inj (inj₂-injective eq))

parity-injective : ∀ {m n} → parity m ≡ parity n → m ≡ n
parity-injective {zero}        {zero}        pm≡pn = refl
parity-injective {zero}        {suc (suc n)} pm≡pn with parity n
parity-injective {zero}        {suc (suc n)} () | inj₁ _
parity-injective {zero}        {suc (suc n)} () | inj₂ _
parity-injective {suc (suc m)} {zero}        pm≡pn with parity m
parity-injective {suc (suc m)} {zero}        () | inj₁ _
parity-injective {suc (suc m)} {zero}        () | inj₂ _
parity-injective {suc zero}    {suc zero}    pm≡pn = refl
parity-injective {suc zero}    {suc (suc n)} pm≡pn with parity n
parity-injective {suc zero}    {suc (suc n)} () | inj₁ _
parity-injective {suc zero}    {suc (suc n)} () | inj₂ _
parity-injective {suc (suc m)} {suc zero}    pm≡pn with parity m
parity-injective {suc (suc m)} {suc zero}    () | inj₁ _
parity-injective {suc (suc m)} {suc zero}    () | inj₂ _
parity-injective {suc (suc m)} {suc (suc n)} pm≡pn =
  cong (suc ∘ suc)
       (parity-injective
          (Sum-map-injective ℕₚ.suc-injective ℕₚ.suc-injective pm≡pn))

parity-even′ : ∀ {m n} → parity m ≡ inj₁ n → m ≡ 2 * n
parity-even′ {m} {n} eq = parity-injective (begin
    parity m       ≡⟨ eq ⟩
    inj₁ n         ≡⟨ sym $ parity-even n ⟩
    parity (2 * n) ∎)
  where open ≡-Reasoning

parity-odd′ : ∀ {m n} → parity m ≡ inj₂ n → m ≡ 1 + 2 * n
parity-odd′ {m} {n} eq = parity-injective (begin
  parity m           ≡⟨ eq ⟩
  inj₂ n             ≡⟨ sym $ parity-odd n ⟩
  parity (1 + 2 * n) ∎)
  where open ≡-Reasoning

mix : ℕ ⊎ ℕ → ℕ
mix = Sum.[ (λ n → 2 * n) , (λ n → 1 + 2 * n) ]

parity-mix : ∀ s → parity (mix s) ≡ s
parity-mix (inj₁ n) = parity-even n
parity-mix (inj₂ n) = parity-odd n

mix-parity : ∀ n → mix (parity n) ≡ n
mix-parity n = parity-injective (parity-mix (parity n))