text:
-- Inductively constructed substitution maps
module SOAS.ContextMaps.Inductive {T : Set} where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Sorting
open import SOAS.Families.Core {T}
open import SOAS.Variable

private
  variable
    α : T
    Γ Δ : Ctx
    𝒳 𝒴 : Familyₛ

-- A list of terms in context Δ for every variable in context Γ
data Sub (𝒳 : Familyₛ) : Ctx → Ctx → Set where
  •   : Sub 𝒳 ∅ Δ
  _◂_ : 𝒳 α Δ → Sub 𝒳 Γ Δ → Sub 𝒳 (α ∙ Γ) Δ

infixl 120 _◂_

infix 150 _⟩
pattern _⟩ t  = t ◂ •

-- Functorial mapping
Sub₁ : (f : 𝒳 ⇾̣ 𝒴) → Sub 𝒳 Γ Δ → Sub 𝒴 Γ Δ
Sub₁ f • = •
Sub₁ f (x ◂ σ) = f x ◂ Sub₁ f σ

-- Conversion between inductive substitutions and context maps
module _ {𝒳 : Familyₛ} where
  index : Sub 𝒳 Γ Δ → Γ ~[ 𝒳 ]↝ Δ
  index • ()
  index (t ◂ σ) new = t
  index (t ◂ σ) (old v) = index σ v

  tabulate : Γ ~[ 𝒳 ]↝ Δ → Sub 𝒳 Γ Δ
  tabulate {Γ = ∅} σ = •
  tabulate {Γ = α ∙ Γ} σ = σ new ◂ tabulate (σ ∘ old)

  ix∘tab≈id : (σ : Γ ~[ 𝒳 ]↝ Δ) (v : ℐ α Γ)
         → index (tabulate σ) v ≡ σ v
  ix∘tab≈id {Γ = α ∙ Γ} σ new = refl
  ix∘tab≈id {Γ = α ∙ Γ} σ (old v) = ix∘tab≈id (σ ∘ old) v

  tab∘ix≈id : (σ : Sub 𝒳 Γ Δ) → tabulate (index σ) ≡ σ
  tab∘ix≈id • = refl
  tab∘ix≈id (x ◂ σ) rewrite tab∘ix≈id σ = refl

-- Naturality conditions
tabulate-nat : (f : 𝒳 ⇾̣ 𝒴)(σ : Γ ~[ 𝒳 ]↝ Δ)
          → tabulate {𝒴} (f ∘ σ) ≡ Sub₁ f (tabulate {𝒳} σ)
tabulate-nat {Γ = ∅} f σ = refl
tabulate-nat {Γ = α ∙ Γ} f σ = cong (f (σ new) ◂_) (tabulate-nat f (σ ∘ old))

index-nat : (f : 𝒳 ⇾̣ 𝒴)(σ : Sub 𝒳 Γ Δ)(v : ℐ α Γ)
          → index (Sub₁ f σ) v ≡ f (index σ v)
index-nat f (x ◂ σ) new     = refl
index-nat f (x ◂ σ) (old v) = index-nat f σ v


text:
------------------------------------------------------------------------------
-- The division program is correct
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- This module proves the correctness of the division program using
-- repeated subtraction (Dybjer 1985).

module FOTC.Program.Division.CorrectnessProofI where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.PropertiesI

import FOTC.Data.Nat.Induction.NonAcc.WF-I
open module WFInd = FOTC.Data.Nat.Induction.NonAcc.WF-I.WFInd

open import FOTC.Program.Division.Division
open import FOTC.Program.Division.ResultI
open import FOTC.Program.Division.Specification
open import FOTC.Program.Division.TotalityI

------------------------------------------------------------------------------
-- The division program is correct when the dividend is less than the
-- divisor.
div-x<y-correct : ∀ {i j} → N i → N j → i < j → divSpec i j (div i j)
div-x<y-correct Ni Nj i<j = div-x<y-N i<j , div-x<y-resultCorrect Ni Nj i<j

-- The division program is correct when the dividend is greater or
-- equal than the divisor.
div-x≮y-correct : ∀ {i j} → N i → N j →
                  (∀ {i'} → N i' → i' < i → divSpec i' j (div i' j)) →
                  j > zero →
                  i ≮ j →
                  divSpec i j (div i j)
div-x≮y-correct {i} {j} Ni Nj ah j>0 i≮j =
  div-x≮y-N ih i≮j , div-x≮y-resultCorrect Ni Nj ih i≮j

  where
  -- The inductive hypothesis on i ∸ j.
  ih : divSpec (i ∸ j) j (div (i ∸ j) j)
  ih = ah {i ∸ j}
          (∸-N Ni Nj)
          (x≥y→y>0→x∸y<x Ni Nj (x≮y→x≥y Ni Nj i≮j) j>0)

------------------------------------------------------------------------------
-- The division program is correct.

-- We do the well-founded induction on i and we keep j fixed.
divCorrect : ∀ {i j} → N i → N j → j > zero → divSpec i j (div i j)
divCorrect {j = j} Ni Nj j>0 = <-wfind A ih Ni
  where
  A : D → Set
  A d = divSpec d j (div d j)

  -- The inductive step doesn't use the variable i (nor Ni). To make
  -- this clear we write down the inductive step using the variables m
  -- and n.
  ih : ∀ {n} → N n → (∀ {m} → N m → m < n → A m) → A n
  ih {n} Nn ah =
    case (div-x<y-correct Nn Nj) (div-x≮y-correct Nn Nj ah j>0) (x<y∨x≮y Nn Nj)

------------------------------------------------------------------------------
-- References
--
-- Dybjer, Peter (1985). Program Verification in a Logical Theory of
-- Constructions. In: Functional Programming Languages and Computer
-- Architecture. Ed. by Jouannaud,
-- Jean-Pierre. Vol. 201. LNCS. Appears in revised form as Programming
-- Methodology Group Report 26, University of Gothenburg and Chalmers
-- University of Technology, June 1986. Springer, pp. 334–349.

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module UniversePolymorphicFunctor where

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

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

infixl 6 _⊔_

record IsEquivalence {a ℓ} {A : Set a}
                     (_≈_ : A → A → Set ℓ) : Set (a ⊔ ℓ) where
  field
    refl  : ∀ {x} → x ≈ x
    sym   : ∀ {i j} → i ≈ j → j ≈ i
    trans : ∀ {i j k} → i ≈ j → j ≈ k → i ≈ k

record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : Set c
    _≈_           : Carrier → Carrier → Set ℓ
    isEquivalence : IsEquivalence _≈_

  open IsEquivalence isEquivalence public

infixr 0 _⟶_

record _⟶_ {f₁ f₂ t₁ t₂}
           (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
           Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  infixl 5 _⟨$⟩_
  field
    _⟨$⟩_ : Setoid.Carrier From → Setoid.Carrier To
    cong  : ∀ {x y} →
            Setoid._≈_ From x y → Setoid._≈_ To (_⟨$⟩_ x) (_⟨$⟩_ y)

open _⟶_ public

id : ∀ {a₁ a₂} {A : Setoid a₁ a₂} → A ⟶ A
id = record { _⟨$⟩_ = λ x → x; cong = λ x≈y → x≈y }

infixr 9 _∘_

_∘_ : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
        {b₁ b₂} {B : Setoid b₁ b₂}
        {c₁ c₂} {C : Setoid c₁ c₂} →
      B ⟶ C → A ⟶ B → A ⟶ C
f ∘ g = record
  { _⟨$⟩_ = λ x → f ⟨$⟩ (g ⟨$⟩ x)
  ; cong  = λ x≈y → cong f (cong g x≈y)
  }

_⇨_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Setoid _ _
From ⇨ To = record
  { Carrier       = From ⟶ To
  ; _≈_           = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
  ; isEquivalence = record
    { refl  = λ {f} → cong f
    ; sym   = λ f∼g x∼y → To.sym (f∼g (From.sym x∼y))
    ; trans = λ f∼g g∼h x∼y → To.trans (f∼g From.refl) (g∼h x∼y)
    }
  }
  where
  open module From = Setoid From using () renaming (_≈_ to _≈₁_)
  open module To   = Setoid To   using () renaming (_≈_ to _≈₂_)

record Functor {f₁ f₂ f₃ f₄}
               (F : Setoid f₁ f₂ → Setoid f₃ f₄) :
               Set (suc (f₁ ⊔ f₂) ⊔ f₃ ⊔ f₄) where
  field
    map : ∀ {A B} → (A ⇨ B) ⟶ (F A ⇨ F B)

    identity : ∀ {A} →
      let open Setoid (F A ⇨ F A) in
      map ⟨$⟩ id ≈ id

    composition : ∀ {A B C} (f : B ⟶ C) (g : A ⟶ B) →
      let open Setoid (F A ⇨ F C) in
      map ⟨$⟩ (f ∘ g) ≈ (map ⟨$⟩ f) ∘ (map ⟨$⟩ g)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- Andreas, 2011-04-15
-- {-# OPTIONS -v tc.meta:20 #-}
module SameMeta where

infix 10 _≡_

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

infixr 5 _×_ _,_

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

postulate A : Set

same : let X : A -> A -> A -> A × A
           X = _
       in {x y z : A} -> X x y y ≡ (x , y)
                       × X x x y ≡ X x y y
same = refl , refl
-- second equation triggers pruning of second variable of X
-- which makes the first equation linear and solvable

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Function.Isomorphism where

open import Cubical.Foundations.Equiv using (isoToEquiv) public
open import Cubical.Foundations.Isomorphism using (Iso; section; retract; isoToPath; iso) public
open import Level
open import Path
open import Function
open import Data.Sigma
open import Relation.Binary

open Iso public

infix 4 _⇔_
_⇔_ = Iso

sym-⇔ : (A ⇔ B) → (B ⇔ A)
fun (sym-⇔ A⇔B) = inv A⇔B
inv (sym-⇔ A⇔B) = fun A⇔B
leftInv (sym-⇔ A⇔B) = rightInv A⇔B
rightInv (sym-⇔ A⇔B) = leftInv A⇔B

refl-⇔ : A ⇔ A
fun refl-⇔ x = x
inv refl-⇔ x = x
leftInv refl-⇔ x = refl
rightInv refl-⇔  x = refl

trans-⇔ : A ⇔ B → B ⇔ C → A ⇔ C
fun      (trans-⇔ A⇔B B⇔C) = fun B⇔C ∘ fun A⇔B
inv      (trans-⇔ A⇔B B⇔C) = inv A⇔B ∘ inv B⇔C
leftInv  (trans-⇔ A⇔B B⇔C) x = cong (inv A⇔B) (leftInv B⇔C _) ; leftInv A⇔B _
rightInv (trans-⇔ A⇔B B⇔C) x = cong (fun B⇔C) (rightInv A⇔B _) ; rightInv B⇔C _

iso-Σ : {B : A → Type b} {C : A → Type c} → (∀ x → B x ⇔ C x) → Σ A B ⇔ Σ A C
iso-Σ B⇔C .fun (x , xs) = x , B⇔C x .fun xs
iso-Σ B⇔C .inv (x , xs) = x , B⇔C x .inv xs
iso-Σ B⇔C .rightInv (x , xs) i .fst = x
iso-Σ B⇔C .rightInv (x , xs) i .snd = B⇔C x .rightInv xs i
iso-Σ B⇔C .leftInv (x , xs) i .fst = x
iso-Σ B⇔C .leftInv (x , xs) i .snd = B⇔C x .leftInv xs i

⇔-equiv : Equivalence (Type a) a
Equivalence._≋_ ⇔-equiv = _⇔_
Equivalence.sym ⇔-equiv = sym-⇔
Equivalence.refl ⇔-equiv = refl-⇔
Equivalence.trans ⇔-equiv = trans-⇔

open import HLevels
open import Equiv

iso⇔equiv : isSet A → (A ⇔ B) ⇔ (A ≃ B)
iso⇔equiv isSetA .fun = isoToEquiv
iso⇔equiv isSetA .inv = equivToIso
iso⇔equiv isSetA .rightInv x i .fst = x .fst
iso⇔equiv isSetA .rightInv x i .snd = isPropIsEquiv (x .fst) (isoToEquiv (equivToIso x) .snd) (x .snd) i
iso⇔equiv isSetA .leftInv x i .fun = x .fun
iso⇔equiv isSetA .leftInv x i .inv = x .inv
iso⇔equiv isSetA .leftInv x i .rightInv = x .rightInv
iso⇔equiv isSetA .leftInv x i .leftInv y = isSetA _ y (equivToIso (isoToEquiv x) .leftInv y) (x .leftInv y) i

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Andreas, 2015-05-06, issue reported by Nisse

postulate
  _ : Set

postulate
  _ : Set

-- Error message WAS: "Multiple definitions of _."
-- BUT: If the first occurrence of _ is accepted, then the second one
-- should also be accepted.

-- Error NOW: "Invalid name: _"

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
module hott.equivalence where

open import hott.equivalence.alternative public
open import hott.equivalence.core public
open import hott.equivalence.properties public
open import hott.equivalence.inverse public
-- open import hott.equivalence.coind public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
-- Andreas, 2016-08-04, issue #964
-- Allow open metas and interaction points in imported files

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v import:100 #-}
-- {-# OPTIONS -v meta.postulate:20 #-}
-- {-# OPTIONS -v tc.meta:25 #-}

-- Andreas, 2016-10-09, while working on issue #2223:
--
-- This module is an example that we can be in a context
-- that is shorter than the current section.
-- Typically, this would be the empty context.
--
-- {-# OPTIONS -v tc.constr.add:45 #-}

open import Common.Level

module Common.Issue964.UnsolvedMetas (A : Set₁) where

meta : Level
meta = {!!}  -- unsolved interaction point

module M (B : Set) where

  meta2 : Set meta
  meta2 = _  -- unsolved meta

  module N (C D : meta2) where

    meta3 : meta2
    meta3 = Set

-- EOF


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Homomorphism.Properties (Σ : Signature) where

open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Homomorphism.Base Σ
open import Fragment.Algebra.Homomorphism.Setoid Σ

open import Level using (Level)
open import Relation.Binary using (Setoid)

private
  variable
    a b c d ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
    A : Algebra {a} {ℓ₁}
    B : Algebra {b} {ℓ₂}
    C : Algebra {c} {ℓ₃}
    D : Algebra {d} {ℓ₄}

id-unitˡ : ∀ {f : A ⟿ B} → id ⊙ f ≗ f
id-unitˡ {B = B} = Setoid.refl ∥ B ∥/≈

id-unitʳ : ∀ {f : A ⟿ B} → f ⊙ id ≗ f
id-unitʳ {B = B} = Setoid.refl ∥ B ∥/≈

⊙-assoc : ∀ (h : C ⟿ D) (g : B ⟿ C) (f : A ⟿ B)
          → (h ⊙ g) ⊙ f ≗ h ⊙ (g ⊙ f)
⊙-assoc {D = D} _ _ _ = Setoid.refl ∥ D ∥/≈

⊙-congˡ : ∀ (h : B ⟿ C) (f g : A ⟿ B)
          → f ≗ g
          → h ⊙ f ≗ h ⊙ g
⊙-congˡ h _ _ f≗g = ∣ h ∣-cong f≗g

⊙-congʳ : ∀ (h : A ⟿ B) (f g : B ⟿ C)
          → f ≗ g
          → f ⊙ h ≗ g ⊙ h
⊙-congʳ _ _ _ f≗g = f≗g

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Environments (heterogeneous collections)
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Star.Environment {ℓ} (Ty : Set ℓ) where

open import Level
open import Data.Star.List
open import Data.Star.Decoration
open import Data.Star.Pointer as Pointer hiding (lookup)
open import Data.Unit
open import Function hiding (_∋_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

-- Contexts, listing the types of all the elements in an environment.

Ctxt : Set ℓ
Ctxt = List Ty

-- Variables (de Bruijn indices); pointers into environments.

infix 4 _∋_

_∋_ : Ctxt → Ty → Set ℓ
Γ ∋ σ = Any (const (Lift ℓ ⊤)) (σ ≡_) Γ

vz : ∀ {Γ σ} → Γ ▻ σ ∋ σ
vz = this refl

vs : ∀ {Γ σ τ} → Γ ∋ τ → Γ ▻ σ ∋ τ
vs = that _

-- Environments. The T function maps types to element types.

Env : ∀ {e} → (Ty → Set e) → (Ctxt → Set (ℓ ⊔ e))
Env T Γ = All T Γ

-- A safe lookup function for environments.

lookup : ∀ {Γ σ} {T : Ty → Set} → Γ ∋ σ → Env T Γ → T σ
lookup i ρ with Pointer.lookup i ρ
... | result refl x = x


text:
-- | Stuff regarding isomorphisms and isomorphic data structures.
module Isomorphisms where

open import Function
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
open ≡-Reasoning

record IsIso {A B : Set} (f : A → B) : Set where
  field
    inv : B → A
    isLeftInv : (a : A) → inv (f a) ≡ a
    isRightInv : (b : B) → f (inv b) ≡ b

iso-comp : {A B C : Set} → {f : A → B} → {g : B → C} →
           IsIso f → IsIso g → IsIso (g ∘ f)
iso-comp {A} {B} {C} {f} {g} if ig =
  record { inv = IsIso.inv if ∘ IsIso.inv ig
         ; isLeftInv = λ a →
           begin
             (IsIso.inv if ∘ IsIso.inv ig) ((g ∘ f) a)
           ≡⟨ refl ⟩
             (IsIso.inv if (IsIso.inv ig (g (f a))))
           ≡⟨ cong (λ x → IsIso.inv if x) (IsIso.isLeftInv ig (f a)) ⟩
             (IsIso.inv if (f a))
           ≡⟨ IsIso.isLeftInv if a ⟩
             a
           ∎
         ; isRightInv = λ c →
           begin
             (g ∘ f) ((IsIso.inv if ∘ IsIso.inv ig) c)
           ≡⟨ refl ⟩
             g (f ((IsIso.inv if) ((IsIso.inv ig) c)))
           ≡⟨ cong (λ x → g x) (IsIso.isRightInv if (IsIso.inv ig c)) ⟩
             g ((IsIso.inv ig) c)
           ≡⟨ IsIso.isRightInv ig c ⟩
             c
           ∎
         }

iso-rev : {A B : Set} → {f : A → B} → (I : IsIso f) →
          IsIso (IsIso.inv I)
iso-rev {A} {B} {f} I =
  record { inv = f
         ; isLeftInv = IsIso.isRightInv I
         ; isRightInv = IsIso.isLeftInv I }

record Iso (A B : Set) : Set where
  field
    iso : A → B
    indeedIso : IsIso iso

iso-trans : {A B C : Set} → Iso A B → Iso B C → Iso A C
iso-trans I₁ I₂ =
  record { iso = Iso.iso I₂ ∘ Iso.iso I₁
         ; indeedIso = iso-comp (Iso.indeedIso I₁) (Iso.indeedIso I₂) }

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A binary representation of natural numbers
------------------------------------------------------------------------

module Data.Bin where

open import Data.Nat as Nat
  using (ℕ; zero; z≤n; s≤s) renaming (suc to 1+_)
open Nat.≤-Reasoning
import Data.Nat.Properties as NP
open import Data.Digit
open import Data.Fin as Fin using (Fin; zero) renaming (suc to 1+_)
open import Data.Fin.Properties as FP using (_+′_)
open import Data.List as List hiding (downFrom)
open import Function
open import Data.Product
open import Algebra
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; sym)
open import Relation.Nullary
private
  module BitOrd = StrictTotalOrder (FP.strictTotalOrder 2)

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

-- A representation of binary natural numbers in which there is
-- exactly one representative for every number.

-- The function toℕ below defines the meaning of Bin.

infix 8 _1#

-- bs stands for the binary number 1<reverse bs>, which is positive.

Bin⁺ : Set
Bin⁺ = List Bit

data Bin : Set where
  -- Zero.
  0#  : Bin
  -- bs 1# stands for the binary number 1<reverse bs>.
  _1# : (bs : Bin⁺) → Bin

------------------------------------------------------------------------
-- Conversion functions

-- Converting to a list of bits starting with the _least_ significant
-- one.

toBits : Bin → List Bit
toBits 0#      = [ 0b ]
toBits (bs 1#) = bs ++ [ 1b ]

-- Converting to a natural number.

toℕ : Bin → ℕ
toℕ = fromDigits ∘ toBits

-- Converting from a list of bits, starting with the _least_
-- significant one.

fromBits : List Bit → Bin
fromBits []              = 0#
fromBits (b        ∷ bs) with fromBits bs
fromBits (b        ∷ bs) | bs′ 1# = (b ∷ bs′) 1#
fromBits (zero     ∷ bs) | 0#     = 0#
fromBits (1+ zero  ∷ bs) | 0#     = [] 1#
fromBits (1+ 1+ () ∷ bs) | _

-- Converting from a natural number.

fromℕ : ℕ → Bin
fromℕ n = fromBits $ proj₁ $ toDigits 2 n

------------------------------------------------------------------------
-- (Bin, _≡_, _<_) is a strict total order

infix 4 _<_

-- Order relation. Wrapped so that the parameters can be inferred.

data _<_ (b₁ b₂ : Bin) : Set where
  less : (lt : (Nat._<_ on toℕ) b₁ b₂) → b₁ < b₂

private
  <-trans : Transitive _<_
  <-trans (less lt₁) (less lt₂) = less (NP.<-trans lt₁ lt₂)

  asym : ∀ {b₁ b₂} → b₁ < b₂ → ¬ b₂ < b₁
  asym {b₁} {b₂} (less lt) (less gt) = tri⟶asym cmp lt gt
    where cmp = StrictTotalOrder.compare NP.strictTotalOrder

  irr : ∀ {b₁ b₂} → b₁ < b₂ → b₁ ≢ b₂
  irr lt eq = asym⟶irr (PropEq.resp₂ _<_) sym asym eq lt

  irr′ : ∀ {b} → ¬ b < b
  irr′ lt = irr lt refl

  ∷∙ : ∀ {b₁ b₂ bs₁ bs₂} →
       bs₁ 1# < bs₂ 1# → (b₁ ∷ bs₁) 1# < (b₂ ∷ bs₂) 1#
  ∷∙ {b₁} {b₂} {bs₁} {bs₂} (less lt) = less (begin
      1 + (m₁ + n₁ * 2)  ≤⟨ ≤-refl {x = 1} +-mono
                              (≤-pred (FP.bounded b₁) +-mono ≤-refl) ⟩
      1 + (1  + n₁ * 2)  ≡⟨ refl ⟩
            suc n₁ * 2   ≤⟨ lt *-mono ≤-refl ⟩
                n₂ * 2   ≤⟨ n≤m+n m₂ (n₂ * 2) ⟩
           m₂ + n₂ * 2   ∎
    )
    where
    open Nat; open NP
    open DecTotalOrder decTotalOrder renaming (refl to ≤-refl)
    m₁ = Fin.toℕ b₁;   m₂ = Fin.toℕ b₂
    n₁ = toℕ (bs₁ 1#); n₂ = toℕ (bs₂ 1#)

  ∙∷ : ∀ {b₁ b₂ bs} →
       Fin._<_ b₁ b₂ → (b₁ ∷ bs) 1# < (b₂ ∷ bs) 1#
  ∙∷ {b₁} {b₂} {bs} lt = less (begin
    1 + (m₁  + n * 2)  ≡⟨ sym (+-assoc 1 m₁ (n * 2)) ⟩
    (1 + m₁) + n * 2   ≤⟨ lt +-mono ≤-refl ⟩
         m₂  + n * 2   ∎)
    where
    open Nat; open NP
    open DecTotalOrder decTotalOrder renaming (refl to ≤-refl)
    open CommutativeSemiring commutativeSemiring using (+-assoc)
    m₁ = Fin.toℕ b₁; m₂ = Fin.toℕ b₂; n = toℕ (bs 1#)

  1<[23] : ∀ {b} → [] 1# < (b ∷ []) 1#
  1<[23] {b} = less (NP.n≤m+n (Fin.toℕ b) 2)

  1<2+ : ∀ {bs b} → [] 1# < (b ∷ bs) 1#
  1<2+ {[]}     = 1<[23]
  1<2+ {b ∷ bs} = <-trans 1<[23] (∷∙ {b₁ = b} (1<2+ {bs}))

  0<1 : 0# < [] 1#
  0<1 = less (s≤s z≤n)

  0<+ : ∀ {bs} → 0# < bs 1#
  0<+ {[]}     = 0<1
  0<+ {b ∷ bs} = <-trans 0<1 1<2+

  compare⁺ : Trichotomous (_≡_ on _1#) (_<_ on _1#)
  compare⁺ []         []         = tri≈ irr′ refl irr′
  compare⁺ []         (b ∷ bs)   = tri<       1<2+  (irr 1<2+) (asym 1<2+)
  compare⁺ (b ∷ bs)   []         = tri> (asym 1<2+) (irr 1<2+ ∘ sym) 1<2+
  compare⁺ (b₁ ∷ bs₁) (b₂ ∷ bs₂) with compare⁺ bs₁ bs₂
  ... | tri<  lt ¬eq ¬gt = tri<       (∷∙ lt)  (irr (∷∙ lt)) (asym (∷∙ lt))
  ... | tri> ¬lt ¬eq  gt = tri> (asym (∷∙ gt)) (irr (∷∙ gt) ∘ sym) (∷∙ gt)
  compare⁺ (b₁ ∷ bs) (b₂ ∷ .bs) | tri≈ ¬lt refl ¬gt with BitOrd.compare b₁ b₂
  compare⁺ (b  ∷ bs) (.b ∷ .bs) | tri≈ ¬lt refl ¬gt | tri≈ ¬lt′ refl ¬gt′ =
    tri≈ irr′ refl irr′
  ... | tri<  lt′ ¬eq ¬gt′ = tri<       (∙∷ lt′)  (irr (∙∷ lt′)) (asym (∙∷ lt′))
  ... | tri> ¬lt′ ¬eq  gt′ = tri> (asym (∙∷ gt′)) (irr (∙∷ gt′) ∘ sym) (∙∷ gt′)

  compare : Trichotomous _≡_ _<_
  compare 0#       0#       = tri≈ irr′ refl irr′
  compare 0#       (bs₂ 1#) = tri<       0<+  (irr 0<+) (asym 0<+)
  compare (bs₁ 1#) 0#       = tri> (asym 0<+) (irr 0<+ ∘ sym) 0<+
  compare (bs₁ 1#) (bs₂ 1#) = compare⁺ bs₁ bs₂

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record
  { Carrier            = Bin
  ; _≈_                = _≡_
  ; _<_                = _<_
  ; isStrictTotalOrder = record
    { isEquivalence = PropEq.isEquivalence
    ; trans         = <-trans
    ; compare       = compare
    ; <-resp-≈      = PropEq.resp₂ _<_
    }
  }

------------------------------------------------------------------------
-- (Bin, _≡_) is a decidable setoid

decSetoid : DecSetoid _ _
decSetoid = StrictTotalOrder.decSetoid strictTotalOrder

infix 4 _≟_

_≟_ : Decidable {A = Bin} _≡_
_≟_ = DecSetoid._≟_ decSetoid

------------------------------------------------------------------------
-- Arithmetic

-- Power of two.

infixr 8 2^_

2^_ : ℕ → Bin⁺
2^ 0    = []
2^ 1+ n = 0b ∷ 2^ n

-- Base 2 logarithm (rounded downwards).

⌊log₂_⌋ : Bin⁺ → ℕ
⌊log₂ (b ∷ bs) ⌋ = 1+ ⌊log₂ bs ⌋
⌊log₂ []       ⌋ = 0

-- Multiplication by 2.

infix 7 _*2 _*2+1

_*2 : Bin → Bin
0#      *2 = 0#
(bs 1#) *2 = (0b ∷ bs) 1#

_*2+1 : Bin → Bin
0#      *2+1 = [] 1#
(bs 1#) *2+1 = (1b ∷ bs) 1#

-- Division by 2, rounded downwards.

⌊_/2⌋ : Bin → Bin
⌊ 0#          /2⌋ = 0#
⌊ [] 1#       /2⌋ = 0#
⌊ (b ∷ bs) 1# /2⌋ = bs 1#

-- Addition.

Carry : Set
Carry = Bit

addBits : Carry → Bit → Bit → Carry × Bit
addBits c b₁ b₂ with c +′ (b₁ +′ b₂)
... | zero          = (0b , 0b)
... | 1+ zero       = (0b , 1b)
... | 1+ 1+ zero    = (1b , 0b)
... | 1+ 1+ 1+ zero = (1b , 1b)
... | 1+ 1+ 1+ 1+ ()

addCarryToBitList : Carry → List Bit → List Bit
addCarryToBitList zero      bs             = bs
addCarryToBitList (1+ zero) []             = 1b ∷ []
addCarryToBitList (1+ zero) (zero    ∷ bs) = 1b ∷ bs
addCarryToBitList (1+ zero) (1+ zero ∷ bs) = 0b ∷ addCarryToBitList 1b bs
addCarryToBitList (1+ 1+ ()) _
addCarryToBitList _ ((1+ 1+ ()) ∷ _)

addBitLists : Carry → List Bit → List Bit → List Bit
addBitLists c []         bs₂        = addCarryToBitList c bs₂
addBitLists c bs₁        []         = addCarryToBitList c bs₁
addBitLists c (b₁ ∷ bs₁) (b₂ ∷ bs₂) with addBits c b₁ b₂
... | (c' , b') = b' ∷ addBitLists c' bs₁ bs₂

infixl 6 _+_

_+_ : Bin → Bin → Bin
m + n = fromBits (addBitLists 0b (toBits m) (toBits n))

-- Multiplication.

infixl 7 _*_

_*_ : Bin → Bin → Bin
0#                 * n = 0#
[]              1# * n = n
-- (b + 2 * bs 1#) * n = b * n + 2 * (bs 1# * n)
(b        ∷ bs) 1# * n with bs 1# * n
(b        ∷ bs) 1# * n | 0#     = 0#
(zero     ∷ bs) 1# * n | bs' 1# = (0b ∷ bs') 1#
(1+ zero  ∷ bs) 1# * n | bs' 1# = n + (0b ∷ bs') 1#
((1+ 1+ ()) ∷ _) 1# * _ | _

-- Successor.

suc : Bin → Bin
suc n = [] 1# + n

-- Division by 2, rounded upwards.

⌈_/2⌉ : Bin → Bin
⌈ n /2⌉ = ⌊ suc n /2⌋

-- Predecessor.

pred : Bin⁺ → Bin
pred []              = 0#
pred (zero     ∷ bs) = pred bs *2+1
pred (1+ zero  ∷ bs) = (zero ∷ bs) 1#
pred (1+ 1+ () ∷ bs)

-- downFrom n enumerates all numbers from n - 1 to 0. This function is
-- linear in n. Analysis: fromℕ takes linear time, and the preds used
-- take amortised constant time (to see this, let the cost of a pred
-- be 2, and put 1 debit on every bit which is 1).

downFrom : ℕ → List Bin
downFrom n = helper n (fromℕ n)
  where
  helper : ℕ → Bin → List Bin
  helper zero   0#      = []
  helper (1+ n) (bs 1#) = n′ ∷ helper n n′
    where n′ = pred bs
  -- Impossible cases:
  helper zero   (_ 1#)  = []
  helper (1+ _) 0#      = []

------------------------------------------------------------------------
-- Tests

-- The tests below have been commented out since (at least one version
-- of) Agda is too slow or memory-hungry to type check them.

{-
-- The tests below are run when this module is type checked.

-- First some test helpers:

private

  testLimit : ℕ
  testLimit = 5

  nats : List ℕ
  nats = List.downFrom testLimit

  nats⁺ : List ℕ
  nats⁺ = filter (λ n → decToBool (Nat._≤?_ 1 n)) nats

  natPairs : List (ℕ × ℕ)
  natPairs = zip nats (reverse nats)

  _=[_]_ : (ℕ → ℕ) → List ℕ → (Bin → Bin) → Set
  f =[ ns ] g = map f ns ≡ map (toℕ ∘ g ∘ fromℕ) ns

  _=[_]₂_ : (ℕ → ℕ → ℕ) → List (ℕ × ℕ) → (Bin → Bin → Bin) → Set
  f =[ ps ]₂ g =
    map (uncurry f) ps ≡ map (toℕ ∘ uncurry (g on fromℕ)) ps

-- And then the tests:

private

  test-*2+1 : (λ n → Nat._+_ (Nat._*_ n 2) 1) =[ nats ] _*2+1
  test-*2+1 = refl

  test-*2 : (λ n → Nat._*_ n 2) =[ nats ] _*2
  test-*2 = refl

  test-⌊_/2⌋ : Nat.⌊_/2⌋ =[ nats ] ⌊_/2⌋
  test-⌊_/2⌋ = refl

  test-+ : Nat._+_ =[ natPairs ]₂ _+_
  test-+ = refl

  test-* : Nat._*_ =[ natPairs ]₂ _*_
  test-* = refl

  test-suc : 1+_ =[ nats ] suc
  test-suc = refl

  test-⌈_/2⌉ : Nat.⌈_/2⌉ =[ nats ] ⌈_/2⌉
  test-⌈_/2⌉ = refl

  drop-1# : Bin → Bin⁺
  drop-1# 0#      = []
  drop-1# (bs 1#) = bs

  test-pred : Nat.pred =[ nats⁺ ] (pred ∘ drop-1#)
  test-pred = refl

  test-downFrom : map toℕ (downFrom testLimit) ≡
                  List.downFrom testLimit
  test-downFrom = refl
-}


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

open import HoTT
open import homotopy.EM1HSpace
open import homotopy.EilenbergMacLane
open import homotopy.EilenbergMacLane1
open import homotopy.EM1HSpace
open import homotopy.EM1HSpaceAssoc

module homotopy.EilenbergMacLaneFunctor where

open EMExplicit

module _ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where

  private
    module φ = GroupHom φ

    EM₁-fmap-hom : G →ᴳ Ω^S-group 0 (⊙EM₁ H)
    EM₁-fmap-hom = group-hom f f-preserves-comp
      where
        f : Group.El G → embase' H == embase
        f g = emloop (φ.f g)
        f-preserves-comp : ∀ g₁ g₂ → f (Group.comp G g₁ g₂) == f g₁ ∙ f g₂
        f-preserves-comp g₁ g₂ =
          emloop (φ.f (Group.comp G g₁ g₂))
            =⟨ ap emloop (φ.pres-comp g₁ g₂) ⟩
          emloop (Group.comp H (φ.f g₁) (φ.f g₂))
            =⟨ emloop-comp' H (φ.f g₁) (φ.f g₂) ⟩
          emloop (φ.f g₁) ∙ emloop (φ.f g₂) =∎

    module EM₁FmapRec =
      EM₁Level₁Rec {G = G} {C = EM₁ H}
                  {{EM₁-level₁ H {⟨-2⟩}}}
                  embase
                  EM₁-fmap-hom

  abstract
    EM₁-fmap : EM₁ G → EM₁ H
    EM₁-fmap = EM₁FmapRec.f

    EM₁-fmap-embase-β : EM₁-fmap embase ↦ embase
    EM₁-fmap-embase-β = EM₁FmapRec.embase-β
    {-# REWRITE EM₁-fmap-embase-β #-}

    EM₁-fmap-emloop-β : ∀ g → ap EM₁-fmap (emloop g) == emloop (φ.f g)
    EM₁-fmap-emloop-β = EM₁FmapRec.emloop-β

  ⊙EM₁-fmap : ⊙EM₁ G ⊙→ ⊙EM₁ H
  ⊙EM₁-fmap = EM₁-fmap , idp

module _ {i j k} {G : Group i} {H : Group j} {K : Group k} (ψ : H →ᴳ K) (φ : G →ᴳ H) where

  EM₁-fmap-∘ : EM₁-fmap (ψ ∘ᴳ φ) ∼ EM₁-fmap ψ ∘ EM₁-fmap φ
  EM₁-fmap-∘ =
    EM₁-set-elim
      {P = λ x → EM₁-fmap (ψ ∘ᴳ φ) x == EM₁-fmap ψ (EM₁-fmap φ x)}
      {{λ x → has-level-apply (EM₁-level₁ K) _ _}}
      idp $
    λ g → ↓-='-in' $
    ap (EM₁-fmap ψ ∘ EM₁-fmap φ) (emloop g)
      =⟨ ap-∘ (EM₁-fmap ψ) (EM₁-fmap φ) (emloop g) ⟩
    ap (EM₁-fmap ψ) (ap (EM₁-fmap φ) (emloop g))
      =⟨ ap (ap (EM₁-fmap ψ)) (EM₁-fmap-emloop-β φ g) ⟩
    ap (EM₁-fmap ψ) (emloop (GroupHom.f φ g))
      =⟨ EM₁-fmap-emloop-β ψ (GroupHom.f φ g) ⟩
    emloop (GroupHom.f (ψ ∘ᴳ φ) g)
      =⟨ ! (EM₁-fmap-emloop-β (ψ ∘ᴳ φ) g) ⟩
    ap (EM₁-fmap (ψ ∘ᴳ φ)) (emloop g) =∎

  ⊙EM₁-fmap-∘ : ⊙EM₁-fmap (ψ ∘ᴳ φ) ⊙∼ ⊙EM₁-fmap ψ ⊙∘ ⊙EM₁-fmap φ
  ⊙EM₁-fmap-∘ = EM₁-fmap-∘ , idp

module _ {i} (G : Group i) where

  EM₁-fmap-idhom : EM₁-fmap (idhom G) ∼ idf (EM₁ G)
  EM₁-fmap-idhom =
    EM₁-set-elim
      {P = λ x → EM₁-fmap (idhom G) x == x}
      {{λ x → has-level-apply (EM₁-level₁ G) (EM₁-fmap (idhom G) x) x}}
      idp $
    λ g → ↓-='-in' $ ! $
    ap (EM₁-fmap (idhom G)) (emloop g)
      =⟨ EM₁-fmap-emloop-β (idhom G) g ⟩
    emloop g
      =⟨ ! (ap-idf (emloop g)) ⟩
    ap (idf (EM₁ G)) (emloop g) =∎

  ⊙EM₁-fmap-idhom : ⊙EM₁-fmap (idhom G) ⊙∼ ⊙idf (⊙EM₁ G)
  ⊙EM₁-fmap-idhom = EM₁-fmap-idhom , idp

module _ {i j} (G : Group i) (H : Group j) where

  EM₁-fmap-cst-hom : EM₁-fmap (cst-hom {G = G} {H = H}) ∼ cst embase
  EM₁-fmap-cst-hom =
    EM₁-set-elim
      {P = λ x → EM₁-fmap cst-hom x == embase}
      {{λ x → has-level-apply (EM₁-level₁ H) (EM₁-fmap cst-hom x) embase}}
      idp $
    λ g → ↓-app=cst-in' $ ! $
    ap (EM₁-fmap cst-hom) (emloop g)
      =⟨ EM₁-fmap-emloop-β cst-hom g ⟩
    emloop (Group.ident H)
      =⟨ emloop-ident ⟩
    idp =∎

  ⊙EM₁-fmap-cst-hom : ⊙EM₁-fmap (cst-hom {G = G} {H = H}) ⊙∼ ⊙cst
  ⊙EM₁-fmap-cst-hom = EM₁-fmap-cst-hom , idp

module _ {i j} (G : AbGroup i) (H : AbGroup j) (φ : G →ᴬᴳ H) where

  ⊙EM-fmap : ∀ n → ⊙EM G n ⊙→ ⊙EM H n
  ⊙EM-fmap = EMImplicitMap.⊙EM-fmap (⊙EM₁-fmap φ) (EM₁HSpace.H-⊙EM₁ G) (EM₁HSpace.H-⊙EM₁ H)

  EM-fmap : ∀ n → EM G n → EM H n
  EM-fmap n = fst (⊙EM-fmap n)

module _ {i} (G H : AbGroup i) (φ : AbGroup.grp G →ᴳ AbGroup.grp H) where

  private
    module SN = SpectrumNatural
      {X = ⊙EM₁ (AbGroup.grp G)} {Y = ⊙EM₁ (AbGroup.grp H)}
      (⊙EM₁-fmap φ)
      {{EM₁-conn}} {{EM₁-conn}}
      {{EM₁-level₁ (AbGroup.grp G)}} {{EM₁-level₁ (AbGroup.grp H)}}
      (EM₁HSpace.H-⊙EM₁ G) (EM₁HSpace.H-⊙EM₁ H)

  abstract
    {-
      checking this definition is very slow for some
      mysterious reason (unification maybe?)
    -}
    ⊙–>-spectrum-natural : ∀ (n : ℕ)
      → ⊙–> (spectrum H n) ◃⊙∘
        ⊙Ω-fmap (⊙EM-fmap G H φ (S n)) ◃⊙idf
        =⊙∘
        ⊙EM-fmap G H φ n ◃⊙∘
        ⊙–> (spectrum G n) ◃⊙idf
    ⊙–>-spectrum-natural n =
      ⊙–> (spectrum H n) ◃⊙∘
      ⊙Ω-fmap (⊙EM-fmap G H φ (S n)) ◃⊙idf
        =⊙∘₁⟨ 0 & 1 & ap ⊙–> (spectrum-def H n) ⟩
      ⊙–> (Spectrum.spectrum H n) ◃⊙∘
      ⊙Ω-fmap (⊙EM-fmap G H φ (S n)) ◃⊙idf
        =⊙∘⟨ SN.⊙–>-spectrum-natural n ⟩
      ⊙EM-fmap G H φ n ◃⊙∘
      ⊙–> (Spectrum.spectrum G n) ◃⊙idf
        =⊙∘₁⟨ 1 & 1 & ap ⊙–> (! (spectrum-def G n)) ⟩
      ⊙EM-fmap G H φ n ◃⊙∘
      ⊙–> (spectrum G n) ◃⊙idf ∎⊙∘

    {-
      derived from `⊙–>-spectrum-natural` instead of from
      `SN.⊙<–-spectrum-natural n` since that circumvents
      the slowness issue for this definition.
    -}
    ⊙<–-spectrum-natural : ∀ (n : ℕ)
      → ⊙<– (spectrum H n) ◃⊙∘
        ⊙EM-fmap G H φ n ◃⊙idf
        =⊙∘
        ⊙Ω-fmap (⊙EM-fmap G H φ (S n)) ◃⊙∘
        ⊙<– (spectrum G n) ◃⊙idf
    ⊙<–-spectrum-natural n =
      ⊙<– (spectrum H n) ◃⊙∘
      ⊙EM-fmap G H φ n ◃⊙idf
        =⊙∘⟨ 2 & 0 & !⊙∘ $ ⊙<–-inv-r-=⊙∘ (spectrum G n) ⟩
      ⊙<– (spectrum H n) ◃⊙∘
      ⊙EM-fmap G H φ n ◃⊙∘
      ⊙–> (spectrum G n) ◃⊙∘
      ⊙<– (spectrum G n) ◃⊙idf
        =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙–>-spectrum-natural n ⟩
      ⊙<– (spectrum H n) ◃⊙∘
      ⊙–> (spectrum H n) ◃⊙∘
      ⊙Ω-fmap (⊙EM-fmap G H φ (S n)) ◃⊙∘
      ⊙<– (spectrum G n) ◃⊙idf
        =⊙∘⟨ 0 & 2 & ⊙<–-inv-l-=⊙∘ (spectrum H n) ⟩
      ⊙Ω-fmap (⊙EM-fmap G H φ (S n)) ◃⊙∘
      ⊙<– (spectrum G n) ◃⊙idf ∎⊙∘

module _ {i j k} (G : AbGroup i) (H : AbGroup j) (K : AbGroup k) (ψ : H →ᴬᴳ K) (φ : G →ᴬᴳ H) where

  private
    module G = AbGroup G
    module H = AbGroup H
    module K = AbGroup K

  ⊙EM-fmap-∘ : ∀ n → ⊙EM-fmap G K (ψ ∘ᴳ φ) n == ⊙EM-fmap H K ψ n ⊙∘ ⊙EM-fmap G H φ n
  ⊙EM-fmap-∘ O =
    ⊙Ω-fmap (⊙EM₁-fmap (ψ ∘ᴳ φ))
      =⟨ ap ⊙Ω-fmap (⊙λ= (⊙EM₁-fmap-∘ ψ φ)) ⟩
    ⊙Ω-fmap (⊙EM₁-fmap ψ ⊙∘ ⊙EM₁-fmap φ)
      =⟨ ⊙Ω-fmap-∘ (⊙EM₁-fmap ψ) (⊙EM₁-fmap φ) ⟩
    ⊙Ω-fmap (⊙EM₁-fmap ψ) ⊙∘ ⊙Ω-fmap (⊙EM₁-fmap φ) =∎
  ⊙EM-fmap-∘ (S n) =
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM₁-fmap (ψ ∘ᴳ φ)))
      =⟨ ap (⊙Trunc-fmap ∘ ⊙Susp^-fmap n) (⊙λ= (⊙EM₁-fmap-∘ ψ φ)) ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM₁-fmap ψ ⊙∘ ⊙EM₁-fmap φ))
      =⟨ ap ⊙Trunc-fmap (⊙Susp^-fmap-∘ n (⊙EM₁-fmap ψ) (⊙EM₁-fmap φ)) ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM₁-fmap ψ) ⊙∘ ⊙Susp^-fmap n (⊙EM₁-fmap φ))
      =⟨ ! (⊙λ= (⊙Trunc-fmap-⊙∘ (⊙Susp^-fmap n (⊙EM₁-fmap ψ)) (⊙Susp^-fmap n (⊙EM₁-fmap φ)))) ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM₁-fmap ψ)) ⊙∘ ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM₁-fmap φ)) =∎

  EM-fmap-∘ : ∀ n → EM-fmap G K (ψ ∘ᴳ φ) n == EM-fmap H K ψ n ∘ EM-fmap G H φ n
  EM-fmap-∘ n = ap fst (⊙EM-fmap-∘ n)

module _ {i} (G : AbGroup i) where

  private
    module G = AbGroup G
  open EM₁HSpace G using (mult; mult-emloop-β)

  EM₁-neg : EM₁ G.grp → EM₁ G.grp
  EM₁-neg = EM₁-fmap (inv-hom G)

  ⊙EM₁-neg : ⊙EM₁ G.grp ⊙→ ⊙EM₁ G.grp
  ⊙EM₁-neg = ⊙EM₁-fmap (inv-hom G)

  abstract
    EM₁-neg-emloop-β : ∀ g → ap EM₁-neg (emloop g) == ! (emloop g)
    EM₁-neg-emloop-β g =
      ap EM₁-neg (emloop g)
        =⟨ EM₁-fmap-emloop-β (inv-hom G) g ⟩
      emloop (G.inv g)
        =⟨ emloop-inv g ⟩
      ! (emloop g) =∎

    EM₁-neg-! : ∀ (p : embase' G.grp == embase)
      → ap EM₁-neg p == ! p
    EM₁-neg-! p =
      transport (λ q → ap EM₁-neg q == ! q)
                (<–-inv-r (emloop-equiv G.grp) p) $
      EM₁-neg-emloop-β (<– (emloop-equiv G.grp) p)

    ⊙Ω-fmap-⊙EM₁-neg : ⊙Ω-fmap ⊙EM₁-neg == ⊙Ω-!
    ⊙Ω-fmap-⊙EM₁-neg = ⊙λ=' EM₁-neg-! $ prop-has-all-paths-↓
      {{has-level-apply (has-level-apply (EM₁-level₁ G.grp {n = -2}) _ _) _ _}}

    EM₁-neg-inv-l : ∀ (x : EM₁ G.grp)
      → mult (EM₁-neg x) x == embase
    EM₁-neg-inv-l =
      EM₁-set-elim
        {P = λ x → mult (EM₁-neg x) x == embase}
        {{λ x → has-level-apply (EM₁-level₁ G.grp) _ _}}
        idp $ λ g →
      ↓-='-in-=ₛ $ !ₛ $
      ap (λ x → mult (EM₁-neg x) x) (emloop g) ◃∙
      idp ◃∎
        =ₛ⟨ 1 & 1 & expand [] ⟩
      ap (λ x → mult (EM₁-neg x) x) (emloop g) ◃∎
        =ₛ₁⟨ ! (ap2-diag (λ x y → mult (EM₁-neg x) y) (emloop g)) ⟩
      ap2 (λ x y → mult (EM₁-neg x) y) (emloop g) (emloop g) ◃∎
        =ₛ⟨ ap2-out (λ x y → mult (EM₁-neg x) y) (emloop g) (emloop g) ⟩
      ap (λ x → mult (EM₁-neg x) embase) (emloop g) ◃∙
      ap (λ y → y) (emloop g) ◃∎
        =ₛ₁⟨ 1 & 1 & ap-idf (emloop g) ⟩
      ap (λ x → mult (EM₁-neg x) embase) (emloop g) ◃∙
      emloop g ◃∎
        =ₛ₁⟨ 0 & 1 & ap-∘ (λ x → mult x embase) EM₁-neg (emloop g) ⟩
      ap (λ x → mult x embase) (ap EM₁-neg (emloop g)) ◃∙
      emloop g ◃∎
        =ₛ₁⟨ 0 & 1 & ap (ap (λ x → mult x embase)) (EM₁-neg-emloop-β g) ⟩
      ap (λ x → mult x embase) (! (emloop g)) ◃∙
      emloop g ◃∎
        =ₛ₁⟨ 0 & 1 & ap-! (λ x → mult x embase) (emloop g) ⟩
      ! (ap (λ x → mult x embase) (emloop g)) ◃∙
      emloop g ◃∎
        =ₛ₁⟨ 0 & 1 & ap ! (mult-emloop-β g embase) ⟩
      ! (emloop g) ◃∙
      emloop g ◃∎
        =ₛ₁⟨ !-inv-l (emloop g) ⟩
      idp ◃∎
        =ₛ₁⟨ 1 & 0 & ! (ap-cst embase (emloop g)) ⟩
      idp ◃∙
      ap (cst embase) (emloop g) ◃∎ ∎ₛ

    EM₁-neg-inv-r : ∀ (x : EM₁ G.grp)
      → mult x (EM₁-neg x) == embase
    EM₁-neg-inv-r =
      EM₁-set-elim
        {P = λ x → mult x (EM₁-neg x) == embase}
        {{λ x → has-level-apply (EM₁-level₁ G.grp) _ _}}
        idp $ λ g →
      ↓-='-in-=ₛ $ !ₛ $
      ap (λ x → mult x (EM₁-neg x)) (emloop g) ◃∙
      idp ◃∎
        =ₛ⟨ 1 & 1 & expand [] ⟩
      ap (λ x → mult x (EM₁-neg x)) (emloop g) ◃∎
        =ₛ₁⟨ ! (ap2-diag (λ x y → mult x (EM₁-neg y)) (emloop g)) ⟩
      ap2 (λ x y → mult x (EM₁-neg y)) (emloop g) (emloop g) ◃∎
        =ₛ⟨ ap2-out (λ x y → mult x (EM₁-neg y)) (emloop g) (emloop g) ⟩
      ap (λ x → mult x embase) (emloop g) ◃∙
      ap EM₁-neg (emloop g) ◃∎
        =ₛ₁⟨ 0 & 1 & mult-emloop-β g embase ⟩
      emloop g ◃∙
      ap EM₁-neg (emloop g) ◃∎
        =ₛ₁⟨ 1 & 1 & EM₁-neg-emloop-β g ⟩
      emloop g ◃∙
      ! (emloop g) ◃∎
        =ₛ₁⟨ !-inv-r (emloop g) ⟩
      idp ◃∎
        =ₛ₁⟨ 1 & 0 & ! (ap-cst embase (emloop g)) ⟩
      idp ◃∙
      ap (λ _ → embase) (emloop g) ◃∎ ∎ₛ

  EM-neg : ∀ (n : ℕ) → EM G n → EM G n
  EM-neg n = EM-fmap G G (inv-hom G) n

  ⊙EM-neg : ∀ (n : ℕ) → ⊙EM G n ⊙→ ⊙EM G n
  ⊙EM-neg n = ⊙EM-fmap G G (inv-hom G) n

  private
    -- superseded by Susp-flip-EM-neg
    EM-neg-2=Trunc-fmap-Susp-flip : EM-neg 2 ∼ Trunc-fmap Susp-flip
    EM-neg-2=Trunc-fmap-Susp-flip =
      Trunc-elim {{λ t → =-preserves-level (EM-level G 2)}} $
      Susp-elim
        {P = λ s → EM-neg 2 [ s ]₂ == Trunc-fmap Susp-flip [ s ]₂}
        (ap [_]₂ (merid embase))
        (ap [_]₂ (! (merid embase))) $
      λ x → ↓-='-in-=ₛ $
      ap [_]₂ (merid embase) ◃∙
      ap (Trunc-fmap Susp-flip ∘ [_]₂) (merid x) ◃∎
        =ₛ₁⟨ 1 & 1 & ap-∘ [_]₂ Susp-flip (merid x) ⟩
      ap [_]₂ (merid embase) ◃∙
      ap [_]₂ (ap Susp-flip (merid x)) ◃∎
        =ₛ₁⟨ 1 & 1 & ap (ap [_]₂) (SuspFlip.merid-β x) ⟩
      ap [_]₂ (merid embase) ◃∙
      ap [_]₂ (! (merid x)) ◃∎
        =ₛ₁⟨ 0 & 1 & ap (ap [_]₂) (! (!-! (merid embase))) ⟩
      ap [_]₂ (! (! (merid embase))) ◃∙
      ap [_]₂ (! (merid x)) ◃∎
        =ₛ⟨ ap-seq-=ₛ [_]₂ (∙-!-seq (merid x ◃∙ ! (merid embase) ◃∎)) ⟩
      ap [_]₂ (! (η x)) ◃∎
        =ₛ₁⟨ ap-! [_]₂ (η x) ⟩
      ! (ap [_]₂ (η x)) ◃∎
        =ₛ₁⟨ cancels-inverse (ap [_]₂ (η x)) (ap [_]₂ (η (EM₁-neg x))) $
             ap [_]₂ (η x) ∙ ap [_]₂ (η (EM₁-neg x))
               =⟨ ∙-ap [_]₂ (η x) (η (EM₁-neg x)) ⟩
             ap [_]₂ (η x ∙ η (EM₁-neg x))
               =⟨ ap (<– (=ₜ-equiv [ north ]₂ [ north ]₂)) $
                  ! $ comp x (EM₁-neg x) ⟩
             ap [_]₂ (η (mult x (EM₁-neg x)))
               =⟨ ap (ap [_]₂ ∘ η) (EM₁-neg-inv-r x) ⟩
             ap [_]₂ (η embase)
               =⟨ ap (ap [_]₂) (!-inv-r (merid embase)) ⟩
             idp =∎ ⟩
      ap [_]₂ (η (EM₁-neg x)) ◃∎
        =ₛ⟨ ap-seq-∙ [_]₂ (merid (EM₁-neg x) ◃∙ ! (merid embase) ◃∎) ⟩
      ap [_]₂ (merid (EM₁-neg x)) ◃∙
      ap [_]₂ (! (merid embase)) ◃∎
        =ₛ₁⟨ 0 & 1 & ap (ap [_]₂) (! (SuspFmap.merid-β EM₁-neg x)) ⟩
      ap [_]₂ (ap (Susp-fmap EM₁-neg) (merid x)) ◃∙
      ap [_]₂ (! (merid embase)) ◃∎
        =ₛ₁⟨ 0 & 1 & ∘-ap [_]₂ (Susp-fmap EM₁-neg) (merid x) ⟩
      ap (EM-neg 2 ∘ [_]₂) (merid x) ◃∙
      ap [_]₂ (! (merid embase)) ◃∎ ∎ₛ
      where
      open EM₁HSpaceAssoc G using (η; H-⊙EM₁; H-⊙EM₁-assoc; H-EM₁-assoc-coh-unit-l-r-pentagon)
      open import homotopy.Pi2HSuspCompose H-⊙EM₁ H-⊙EM₁-assoc H-EM₁-assoc-coh-unit-l-r-pentagon
        using (comp)
      cancels-inverse : ∀ {i} {A : Type i} {x y : A}
        (p : x == y) (q : y == x) → p ∙ q == idp → ! p == q
      cancels-inverse p@idp q@.idp idp = idp

    ⊙EM-neg-2=⊙Trunc-fmap-⊙Susp-flip : ⊙EM-neg 2 == ⊙Trunc-fmap (⊙Susp-flip (⊙EM₁ G.grp))
    ⊙EM-neg-2=⊙Trunc-fmap-⊙Susp-flip =
      ⊙λ=' {X = ⊙EM G 2} {Y = ⊙EM G 2} EM-neg-2=Trunc-fmap-Susp-flip $
      ↓-idf=cst-in $
      =ₛ-out $ !ₛ $
      ap [_]₂ (merid embase) ◃∙
      ap [_]₂ (! (merid embase)) ◃∎
        =ₛ⟨ ap-seq-=ₛ [_]₂ (seq-!-inv-r (merid (embase' G.grp) ◃∎)) ⟩
      [] ∎ₛ

    ⊙to-alt-EM : ∀ n → ⊙EM G (S (S n)) ⊙≃ ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ n (⊙EM G 2))
    ⊙to-alt-EM n =
      (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ⊙⁻¹ ⊙∘e
      ⊙coe-equiv (ap (⊙Trunc (⟨ n ⟩₋₂ +2+ 2)) (! (⊙Susp^-+ n 1))) ⊙∘e
      ⊙coe-equiv (ap (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n)) ⊙∘e
      ⊙coe-equiv (ap (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂))

    ⊙–>-⊙to-alt-EM : ∀ n →
      ⊙–> (⊙to-alt-EM n) ◃⊙idf
      =⊙∘
      ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
      ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
      ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
      ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
    ⊙–>-⊙to-alt-EM n =
      ⊙–> (⊙to-alt-EM n) ◃⊙idf
        =⊙∘⟨ =⊙∘-in idp ⟩
      ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
      ⊙coe (ap (⊙Trunc (⟨ n ⟩₋₂ +2+ 2)) (! (⊙Susp^-+ n 1))) ◃⊙∘
      ⊙coe (ap (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n)) ◃⊙∘
      ⊙coe (ap (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂)) ◃⊙idf
        =⊙∘₁⟨ 1 & 1 & ! (⊙transport-⊙coe (⊙Trunc (⟨ n ⟩₋₂ +2+ 2)) (! (⊙Susp^-+ n 1))) ∙
                      ⊙transport-⊙Trunc (! (⊙Susp^-+ n 1)) ⟩
      ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
      ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
      ⊙coe (ap (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n)) ◃⊙∘
      ⊙coe (ap (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂)) ◃⊙idf
        =⊙∘₁⟨ 2 & 1 & ! $ ⊙transport-⊙coe (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ⟩
      ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
      ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
      ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
      ⊙coe (ap (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂)) ◃⊙idf
        =⊙∘₁⟨ 3 & 1 & ! $ ⊙transport-⊙coe (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ⟩
      ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
      ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
      ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
      ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf ∎⊙∘

  ⊙EM-neg=⊙Trunc-fmap-⊙Susp-flip : ∀ (n : ℕ)
    → ⊙EM-neg (S (S n)) == ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n (⊙EM₁ G.grp)))
  ⊙EM-neg=⊙Trunc-fmap-⊙Susp-flip n =
    equiv-is-inj
      (post⊙∘-is-equiv (⊙to-alt-EM n))
      (⊙EM-neg (S (S n)))
      (⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n (⊙EM₁ G.grp)))) $
    =⊙∘-out {fs = ⊙–> (⊙to-alt-EM n) ◃⊙∘ ⊙EM-neg (S (S n)) ◃⊙idf}
            {gs = ⊙–> (⊙to-alt-EM n) ◃⊙∘ ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n (⊙EM₁ G.grp))) ◃⊙idf} $
    ⊙–> (⊙to-alt-EM n) ◃⊙∘
    ⊙EM-neg (S (S n)) ◃⊙idf
      =⊙∘⟨ 0 & 1 & ⊙–>-⊙to-alt-EM n ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙∘
    ⊙EM-neg (S (S n)) ◃⊙idf
      =⊙∘⟨ 3 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘
             (+2+-comm 2 ⟨ n ⟩₋₂)
             (λ k → ⊙Trunc-fmap {n = k} (⊙Susp^-fmap (S n) ⊙EM₁-neg)) ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap (S n) ⊙EM₁-neg) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
      =⊙∘⟨ 2 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘
             (+-comm 1 n)
             (λ l → ⊙Trunc-fmap (⊙Susp^-fmap l ⊙EM₁-neg)) ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap (n + 1) ⊙EM₁-neg) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙Trunc-fmap-seq-=⊙∘ $
           =⊙∘-in {fs = ⊙coe (! (⊙Susp^-+ n 1)) ◃⊙∘ ⊙Susp^-fmap (n + 1) ⊙EM₁-neg ◃⊙idf}
                  {gs = ⊙Susp^-fmap n (⊙Susp-fmap EM₁-neg) ◃⊙∘ ⊙coe (! (⊙Susp^-+ n 1)) ◃⊙idf} $
           ! $ ⊙Susp^-+-natural' n 1 ⊙EM₁-neg ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Susp-fmap EM₁-neg)) ◃⊙∘
    ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙Susp^-⊙Trunc-equiv-natural' (⊙Susp-fmap EM₁-neg) 2 n ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM-neg 2)) ◃⊙∘
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ap (⊙Trunc-fmap ∘ ⊙Susp^-fmap n) $
                    ⊙EM-neg-2=⊙Trunc-fmap-⊙Susp-flip ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Trunc-fmap (⊙Susp-flip (⊙EM₁ G.grp)))) ◃⊙∘
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
      =⊙∘⟨ 0 & 2 & !⊙∘ $ ⊙Susp^-⊙Trunc-equiv-natural' (⊙Susp-flip _) 2 n ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Susp-flip (⊙EM₁ G.grp))) ◃⊙∘
    ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
      =⊙∘₁⟨ 3 & 1 & p ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙Susp-flip (⊙EM₁ G.grp))) ◃⊙∘
    ⊙Trunc-fmap {n = ⟨ n ⟩₋₂ +2+ 2} (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙Trunc-fmap (⊙coe (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n))) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
      =⊙∘⟨ 1 & 3 & ⊙Trunc-fmap-seq-=⊙∘ $
           ⊙Susp^-fmap n (⊙Susp-flip (⊙EM₁ G.grp)) ◃⊙∘
           ⊙coe (! (⊙Susp^-+ n 1)) ◃⊙∘
           ⊙coe (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n)) ◃⊙idf
             =⊙∘⟨ 3 & 0 & ⊙contract ⟩
           ⊙Susp^-fmap n (⊙Susp-flip (⊙EM₁ G.grp)) ◃⊙∘
           ⊙coe (! (⊙Susp^-+ n 1)) ◃⊙∘
           ⊙coe (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n)) ◃⊙∘
           ⊙coe (⊙Susp^-+ 1 n {⊙EM₁ G.grp}) ◃⊙idf
             =⊙∘⟨ 1 & 3 & !⊙∘ $ ⊙coe-seq-∙ (⊙Susp^-comm-seq 1 n) ⟩
           ⊙Susp^-fmap n (⊙Susp-flip (⊙EM₁ G.grp)) ◃⊙∘
           ⊙coe (⊙Susp^-comm 1 n) ◃⊙idf
             =⊙∘⟨ ⊙Susp^-comm-flip 0 n (⊙EM₁ G.grp) ⟩
           ⊙coe (⊙Susp^-comm 1 n) ◃⊙∘
           ⊙Susp-flip (⊙Susp^ 0 (⊙Susp^ n (⊙EM₁ G.grp))) ◃⊙idf
             =⊙∘⟨ 0 & 1 & ⊙coe-seq-∙ (⊙Susp^-comm-seq 1 n) ⟩
           ⊙coe (! (⊙Susp^-+ n 1)) ◃⊙∘
           ⊙coe (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n)) ◃⊙∘
           ⊙coe (⊙Susp^-+ 1 n {⊙EM₁ G.grp}) ◃⊙∘
           ⊙Susp-flip (⊙Susp^ 0 (⊙Susp^ n (⊙EM₁ G.grp))) ◃⊙idf
             =⊙∘⟨ 2 & 1 & ⊙expand ⊙idf-seq ⟩
           ⊙coe (! (⊙Susp^-+ n 1)) ◃⊙∘
           ⊙coe (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n)) ◃⊙∘
           ⊙Susp-flip (⊙Susp^ 0 (⊙Susp^ n (⊙EM₁ G.grp))) ◃⊙idf ∎⊙∘ ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙Trunc-fmap (⊙coe (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n))) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n (⊙EM₁ G.grp))) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙idf
      =⊙∘⟨ 3 & 2 & ⊙transport-natural-=⊙∘
                     (+2+-comm 2 ⟨ n ⟩₋₂)
                     (λ k → ⊙Trunc-fmap {n = k} (⊙Susp-flip (⊙Susp^ n (⊙EM₁ G.grp)))) ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙Trunc-fmap (⊙coe (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n))) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n (⊙EM₁ G.grp))) ◃⊙idf
      =⊙∘₁⟨ 2 & 1 & ! p ⟩
    ⊙<– (⊙Susp^-⊙Trunc-equiv (⊙Susp (EM₁ G.grp)) 2 n) ◃⊙∘
    ⊙Trunc-fmap (⊙coe (! (⊙Susp^-+ n 1))) ◃⊙∘
    ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ◃⊙∘
    ⊙transport (λ k → ⊙Trunc k (⊙Susp^ (S n) (⊙EM₁ G.grp))) (+2+-comm 2 ⟨ n ⟩₋₂) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n (⊙EM₁ G.grp))) ◃⊙idf
      =⊙∘⟨ 0 & 4 & !⊙∘ $ ⊙–>-⊙to-alt-EM n ⟩
    ⊙–> (⊙to-alt-EM n) ◃⊙∘
    ⊙Trunc-fmap (⊙Susp-flip (⊙Susp^ n (⊙EM₁ G.grp))) ◃⊙idf ∎⊙∘
    where
    p : ⊙transport (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ==
        ⊙Trunc-fmap (⊙coe (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n)))
    p =
      ⊙transport-⊙coe (λ l → ⊙Trunc (⟨ n ⟩₋₂ +2+ 2) (⊙Susp^ l (⊙EM₁ G.grp))) (+-comm 1 n) ∙
      ap ⊙coe (ap-∘ (⊙Trunc (⟨ n ⟩₋₂ +2+ 2)) (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n)) ∙
      ! (⊙transport-⊙coe (⊙Trunc (⟨ n ⟩₋₂ +2+ 2)) (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n))) ∙
      ⊙transport-⊙Trunc (ap (λ l → ⊙Susp^ l (⊙EM₁ G.grp)) (+-comm 1 n))

module _ {i} (G : AbGroup i) where

  private
    module G = AbGroup G

  ⊙EM-fmap-idhom : ∀ (n : ℕ)
    → ⊙EM-fmap G G (idhom G.grp) n == ⊙idf (⊙EM G n)
  ⊙EM-fmap-idhom O =
    ⊙Ω-fmap (⊙EM₁-fmap (idhom G.grp))
      =⟨ ap ⊙Ω-fmap (⊙λ= (⊙EM₁-fmap-idhom G.grp)) ⟩
    ⊙Ω-fmap (⊙idf (⊙EM₁ G.grp))
      =⟨ ⊙Ω-fmap-idf ⟩
    ⊙idf _ =∎
  ⊙EM-fmap-idhom (S n) =
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM₁-fmap (idhom G.grp)))
      =⟨ ap (⊙Trunc-fmap ∘ ⊙Susp^-fmap n) (⊙λ= (⊙EM₁-fmap-idhom G.grp)) ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙idf (⊙EM₁ G.grp)))
      =⟨ ap ⊙Trunc-fmap (=⊙∘-out (⊙Susp^-fmap-idf n (⊙EM₁ G.grp))) ⟩
    ⊙Trunc-fmap (⊙idf (⊙Susp^ n (⊙EM₁ G.grp)))
      =⟨ ⊙λ= ⊙Trunc-fmap-⊙idf ⟩
    ⊙idf _ =∎

  EM-fmap-idhom : ∀ (n : ℕ)
    → EM-fmap G G (idhom G.grp) n == idf (EM G n)
  EM-fmap-idhom n = ap fst (⊙EM-fmap-idhom n)

module _ {i} {j} (G : AbGroup i) (H : AbGroup j) where

  ⊙EM-fmap-cst-hom : ∀ (n : ℕ)
    → ⊙EM-fmap G H cst-hom n == ⊙cst
  ⊙EM-fmap-cst-hom O =
    ⊙Ω-fmap (⊙EM₁-fmap cst-hom)
      =⟨ ap ⊙Ω-fmap (⊙λ= (⊙EM₁-fmap-cst-hom (AbGroup.grp G) (AbGroup.grp H))) ⟩
    ⊙Ω-fmap ⊙cst
      =⟨ ⊙Ω-fmap-cst ⟩
    ⊙cst =∎
  ⊙EM-fmap-cst-hom (S n) =
    ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM₁-fmap cst-hom))
      =⟨ ap (⊙Trunc-fmap ∘ ⊙Susp^-fmap n) (⊙λ= (⊙EM₁-fmap-cst-hom (AbGroup.grp G) (AbGroup.grp H))) ⟩
    ⊙Trunc-fmap (⊙Susp^-fmap n ⊙cst)
      =⟨ ap ⊙Trunc-fmap (⊙Susp^-fmap-cst n) ⟩
    ⊙Trunc-fmap ⊙cst
      =⟨ ⊙λ= ⊙Trunc-fmap-cst ⟩
    ⊙cst =∎

  EM-fmap-cst-hom : ∀ (n : ℕ)
    → EM-fmap G H cst-hom n == cst (pt (⊙EM H n))
  EM-fmap-cst-hom n = ap fst (⊙EM-fmap-cst-hom n)

transport-EM : ∀ {i} {G H : AbGroup i}
  (p : G == H) (n : ℕ)
  → transport (λ K → EM K n) p == EM-fmap G H (coeᴬᴳ p) n
transport-EM {G = G} idp n = ! $
  EM-fmap G G (coeᴳ idp) n
    =⟨ ap (λ φ → EM-fmap G G φ n) (coeᴳ-idp (AbGroup.grp G)) ⟩
  EM-fmap G G (idhom (AbGroup.grp G)) n
    =⟨ EM-fmap-idhom G n ⟩
  idf (EM G n) =∎

transport-EM-uaᴬᴳ : ∀ {i} (G H : AbGroup i)
  (iso : G ≃ᴬᴳ H) (n : ℕ)
  → transport (λ K → EM K n) (uaᴬᴳ G H iso) == EM-fmap G H (–>ᴳ iso) n
transport-EM-uaᴬᴳ G H iso n =
  transport (λ K → EM K n) (uaᴬᴳ G H iso)
    =⟨ transport-EM (uaᴬᴳ G H iso) n ⟩
  EM-fmap G H (coeᴬᴳ (uaᴬᴳ G H iso)) n
    =⟨ ap (λ p → EM-fmap G H p n) (coeᴬᴳ-β G H iso) ⟩
  EM-fmap G H (–>ᴳ iso) n =∎

⊙transport-⊙EM : ∀ {i} {G H : AbGroup i}
  (p : G == H) (n : ℕ)
  → ⊙transport (λ K → ⊙EM K n) p == ⊙EM-fmap G H (coeᴬᴳ p) n
⊙transport-⊙EM {G = G} p@idp n = ! $
  ⊙EM-fmap G G (coeᴳ idp) n
    =⟨ ap (λ φ → ⊙EM-fmap G G φ n) (coeᴳ-idp (AbGroup.grp G)) ⟩
  ⊙EM-fmap G G (idhom (AbGroup.grp G)) n
    =⟨ ⊙EM-fmap-idhom G n ⟩
  ⊙idf (⊙EM G n) =∎

⊙transport-⊙EM-uaᴬᴳ : ∀ {i} (G H : AbGroup i)
  (iso : G ≃ᴬᴳ H) (n : ℕ)
  → ⊙transport (λ K → ⊙EM K n) (uaᴬᴳ G H iso) == ⊙EM-fmap G H (–>ᴳ iso) n
⊙transport-⊙EM-uaᴬᴳ G H iso n =
  ⊙transport (λ K → ⊙EM K n) (uaᴬᴳ G H iso)
    =⟨ ⊙transport-⊙EM (uaᴬᴳ G H iso) n ⟩
  ⊙EM-fmap G H (coeᴬᴳ (uaᴬᴳ G H iso)) n
    =⟨ ap (λ p → ⊙EM-fmap G H p n) (coeᴬᴳ-β G H iso) ⟩
  ⊙EM-fmap G H (–>ᴳ iso) n =∎

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --guardedness #-}

module Issue728 where

open import Common.MAlonzo using () renaming (main to mainDefault)

main = mainDefault


text:
module Pi-.Everything where
open import Pi-.Syntax      -- Syntax of Pi-
open import Pi-.Opsem       -- Abstract machine semantics of Pi-
open import Pi-.AuxLemmas   -- Some auxiliary lemmas about opsem for forward/backward deterministic proof
open import Pi-.NoRepeat    -- Forward/backward deterministic lemmas and Non-repeating lemma
open import Pi-.Invariants  -- Some invariants about abstract machine semantics
open import Pi-.Eval        -- Evaluator for Pi-
open import Pi-.Interp      -- Big-step intepreter for Pi-
open import Pi-.Properties  -- Properties of Pi-
open import Pi-.Examples    -- Examples
open import Pi-.Category    -- Pi- Category


text:
module Data.List.Exts where

open import Class.Equality
open import Class.Monad
open import Class.Functor
open import Data.Bool hiding (_≟_)
open import Data.List
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Maybe.Instance
open import Data.Nat using (ℕ; zero; suc; _⊔_)
open import Data.Product
open import Relation.Nullary
open import Relation.Unary

private
  variable
    A : Set

lookupMaybe : ∀ {a} {A : Set a} -> ℕ -> List A -> Maybe A
lookupMaybe n [] = nothing
lookupMaybe zero (x ∷ l) = just x
lookupMaybe (suc n) (x ∷ l) = lookupMaybe n l

findIndexList : {A : Set} {P : A -> Set} -> Decidable P -> List A -> Maybe ℕ
findIndexList P? [] = nothing
findIndexList P? (x ∷ v) with P? x
... | yes p = just 0
... | no ¬p = suc <$> findIndexList P? v

dropHeadIfAny : ∀ {a} {A : Set a} -> List A -> List A
dropHeadIfAny [] = []
dropHeadIfAny (x ∷ l) = l

-- inverse to intercalate
{-# TERMINATING #-}
splitMulti : ∀ {A : Set} {{_ : Eq A}} -> A -> List A -> List (List A)
splitMulti a [] = []
splitMulti a l@(x ∷ xs) with break (a ≟_) l
... | fst , snd = fst ∷ splitMulti a (dropHeadIfAny snd)

takeEven : ∀ {a} {A : Set a} -> List A -> List A
takeEven [] = []
takeEven (x ∷ []) = []
takeEven (x ∷ x₁ ∷ l) = x₁ ∷ takeEven l

maximum : List ℕ → ℕ
maximum [] = 0
maximum (x ∷ l) = x ⊔ maximum l

mapWithIndex : ∀ {a b} {A : Set a} {B : Set b} → (ℕ → A → B) → List A → List B
mapWithIndex f l = zipWith f (upTo (length l)) l

isInit : ⦃ EqB A ⦄ → List A → List A → Bool
isInit [] l' = true
isInit (x ∷ l) [] = false
isInit (x ∷ l) (x₁ ∷ l') = x ≣ x₁ ∧ isInit l l'

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-# OPTIONS --rewriting --prop #-}

open import common
open import syntx
open import derivability
open import structuralrules
open import typingrules
open import typetheories

module _ where

{- Π-Types + a dependent type -}

module _ where
  TypingRuleΠ : TypingRule (TTDer ◇) ([] , (0 , Ty) , (1 , Ty)) Ty
  TypingRuleΠ = Ty ([] , Ty []
                       , Ty ([] , (sym 0 [] / apr T 0 [])))

  ΠUEl-TT1 : TypeTheory
  ΠUEl-TT1 = ◇ , TypingRuleΠ

  TypingRuleλ : TypingRule (TTDer ΠUEl-TT1) ([] , (0 , Ty) , (1 , Ty) , (1 , Tm)) Tm
  TypingRuleλ = Tm ([] , Ty []
                       , Ty ([] , (sym 0 [] / apr T 0 []))
                       , Tm ([] , (sym 1 [] / apr T 1 []))
                            (sym   1 ([] ,    sym   0 []) /
                             apr T 1 ([] ,0Tm apr T 0 [])))
                   (sym   3 ([] ,    sym   2 [] ,    sym   1 ([] ,    var last)) /
                    apr T 3 ([] ,0Ty apr T 2 [] ,1Ty apr T 1 ([] ,0Tm apr S (var 0) ([] , apr T 2 []))))

  ΠUEl-TT2 : TypeTheory
  ΠUEl-TT2 = ΠUEl-TT1 , TypingRuleλ

  TypingRuleapp : TypingRule (TTDer ΠUEl-TT2) ([] , (0 , Ty) , (1 , Ty) , (0 , Tm) , (0 , Tm)) Tm
  TypingRuleapp = Tm ([] , Ty []
                         , Ty ([] , (sym 0 [] / apr T 0 []))
                         , Tm [] (sym 3 ([] ,    sym 1 [] ,    sym 0 ([] ,    var last)) /
                                  apr T 3 ([] ,0Ty apr T 1 [] ,1Ty apr T 0 ([] ,0Tm apr S (var 0) ([] , apr T 1 []))))
                         , Tm [] (sym 2 [] / apr T 2 []))
                     (sym 2 ([] ,    sym 0 []) /
                      apr T 2 ([] ,0Tm apr T 0 []))

  ΠUEl-TT3 : TypeTheory
  ΠUEl-TT3 = ΠUEl-TT2 , TypingRuleapp

  TypingRuleBeta : EqualityRule (TTDer ΠUEl-TT3) ([] , (0 , Ty) , (1 , Ty) , (1 , Tm) , (0 , Tm)) Tm
  TypingRuleBeta = Tm= ([] , Ty []
                           , Ty ([] , sym 0 [] / apr T 0 [])
                           , Tm ([] , sym 1 [] / apr T 1 [])
                                (sym 1 ([] ,    sym 0 []) /
                                 apr T 1 ([] ,0Tm apr T 0 []))
                           , Tm [] (sym 2 [] / apr T 2 []))
                       (sym 2 ([] , sym 0 []) <:
                         sym 4 ([] , sym 3 []
                                   , sym 2 ([] , var last)
                                   , sym 5 ([] , sym 3 [] , sym 2 ([] , var last) , sym 1 ([] , var last))
                                   , sym 0 []) /
                         apr T 4 ([]
                           ,0Ty apr T 3 []
                           ,1Ty apr T 2 ([] ,0Tm apr S (var 0) ([] ,0Ty apr T 3 []))
                           ,0Tm apr T 5 ([] ,0Ty apr T 3 []
                                            ,1Ty apr T 2 ([] ,0Tm apr S (var zero) ([] ,0Ty apr T 3 []))
                                            ,1Tm apr T 1 ([] ,0Tm apr S (var zero) ([] ,0Ty apr T 3 []))) {-{{((tt , (tt , tt)) , ((tt , refl) , tt)) , ((tt , refl) , (refl , tt)) , tt}}-}
                           ,0Tm apr T 0 []) {-{{((((tt , (tt , tt)) , ((tt , refl) , tt)) , (tt , (refl , tt))) , (tt , (refl , tt))) , tt}}-}
                        // sym 1 ([] , sym 0 [])
                         / apr T 1 ([] ,0Tm apr T 0 []))

  ΠUEl-TT4 : TypeTheory
  ΠUEl-TT4 = ΠUEl-TT3 ,= TypingRuleBeta

  TypingRuleEta : EqualityRule (TTDer ΠUEl-TT4) ([] , (0 , Ty) , (1 , Ty) , (0 , Tm)) Tm
  TypingRuleEta = Tm= ([] , Ty []
                          , Ty ([] , sym 0 [] / apr T 0 [])
                          , Tm [] (sym 4 ([] , sym 1 [] , sym 0 ([] , var last))
                                 / apr T 4 ([] ,0Ty apr T 1 [] ,1Ty apr T 0 ([] ,0Tm apr S (var 0) ([] ,0Ty apr T 1 [])))))
                      (sym 5 ([] , sym 2 [] , sym 1 ([] , var last))
                      <: sym 0 []
                      /  apr T 0 []
                      // sym 4 ([] , sym 2 [] , sym 1 ([] , var last) , sym 3 ([] , sym 2 [] , sym 1 ([] , var last) , sym 0 [] , var last))
                      /  apr T 4 ([] ,0Ty apr T 2 []
                                     ,1Ty apr T 1 ([] ,0Tm apr S (var 0) ([] ,0Ty apr T 2 []))
                                     ,1Tm apr T 3 ([] ,0Ty apr T 2 []
                                                      ,1Ty apr T 1 ([] ,0Tm apr S (var 0) ([] ,0Ty apr T 2 []))
                                                      ,0Tm apr T 0 []
                                                      ,0Tm apr S (var 0) ([] ,0Ty apr T 2 []))))

  ΠUEl-TT5 : TypeTheory
  ΠUEl-TT5 = ΠUEl-TT4 ,= TypingRuleEta

  TypingRuleU : TypingRule (TTDer ΠUEl-TT5) [] Ty
  TypingRuleU = Ty []

  ΠUEl-TT6 : TypeTheory
  ΠUEl-TT6 = ΠUEl-TT5 , TypingRuleU

  TypingRuleEl : TypingRule (TTDer ΠUEl-TT6) ([] , (0 , Tm)) Ty
  TypingRuleEl = Ty ([] , Tm [] (sym 0 [] / apr T 0 []))

  ΠUEl-TT : TypeTheory
  ΠUEl-TT = ΠUEl-TT6 , TypingRuleEl

-- {- Natural numbers -}

-- module _ where
--   TypingRuleℕ : TypingRule (TTDer ◇) [] Ty
--   TypingRuleℕ = Ty []

--   ℕ-TT0 : TypeTheory
--   ℕ-TT0 = ◇ , TypingRuleℕ

--   TypingRule0 : TypingRule (TTDer ℕ-TT0) [] Tm
--   TypingRule0 = Tm [] (sym 0 [] / apr T 0 [])

--   ℕ-TT1 : TypeTheory
--   ℕ-TT1 = ℕ-TT0 , TypingRule0

--   TypingRuleS : TypingRule (TTDer ℕ-TT1) ([] , (0 , Tm)) Tm
--   TypingRuleS = Tm ([] , Tm [] (sym 1 [] / apr T 1 []))
--                    (sym 2 [] / apr T 2 [])

--   ℕ-TT2 : TypeTheory
--   ℕ-TT2 = ℕ-TT1 , TypingRuleS

--   TypingRuleℕ-elim : TypingRule (TTDer ℕ-TT2) ([] , (1 , Ty) , (0 , Tm) , (2 , Tm) , (0 , Tm)) Tm
--   TypingRuleℕ-elim = Tm ([] , Ty ([] , sym 2 [] / apr T 2 [])
--                             , Tm [] (sym 0 ([] , sym 2 []) / apr T 0 ([] ,0Tm apr T 2 []))
--                             , Tm ([] , sym 4 [] / apr T 4 []
--                                      , sym 2 ([] , sym 0 []) / apr T 2 ([] ,0Tm apr T 0 []))
--                                  (sym 3 ([] , sym 4 ([] , sym 1 [])) /
--                                   apr T 3 ([] ,0Tm apr T 4 ([] ,0Tm apr T 1 [])))
--                             , Tm [] (sym 5 [] / apr T 5 []))
--                         (sym 3 ([] , (sym 0 [])) / apr T 3 ([] ,0Tm apr T 0 []))

--   ℕ-TT3 : TypeTheory
--   ℕ-TT3 = ℕ-TT2 , TypingRuleℕ-elim

--   TypingRuleℕ0-β : EqualityRule (TTDer ℕ-TT3) ([] , (1 , Ty) , (0 , Tm) , (2 , Tm)) Tm
--   TypingRuleℕ0-β = Tm= ([] , Ty ([] , (sym 3 [] / apr T 3 []))
--                            , Tm [] (sym 0 ([] , sym 3 []) / apr T 0 ([] ,0Tm apr T 3 []))
--                            , Tm ([] , (sym 5 [] / apr T 5 [])
--                                     , (sym 2 ([] , sym 0 []) / apr T 2 ([] ,0Tm apr T 0 [])))
--                                 (sym 3 ([] , sym 5 ([] , sym 1 [])) / apr T 3 ([] ,0Tm apr T 5 ([] ,0Tm apr T 1 []))))
--                        (sym 2 ([] , sym 5 []) <: sym 3 ([] , sym 2 ([] , var last) , sym 1 [] , sym 0 ([] , var (prev last) , var last) , sym 5 [])
--                                                  / apr T 3 ([] ,1Ty apr T 2 ([] ,0Tm apr S (var 0) ([] ,0Ty apr T 6 []))
--                                                                ,0Tm apr T 1 []
--                                                                ,2Tm apr T 0 ([] ,0Tm apr S (var 1) ([] ,0Ty apr T 6 [])
--                                                                                ,0Tm apr S (var 0) ([] ,0Ty apr T 2 ([] ,0Tm apr S (var 1) ([] ,0Ty apr T 6 []))))
--                                                                ,0Tm apr T 5 [])
--                                                  // sym 1 []
--                                                  / apr T 1 [])

--   ℕ-TT4 : TypeTheory
--   ℕ-TT4 = ℕ-TT3 ,= TypingRuleℕ0-β

--   TypingRuleℕS-β : EqualityRule (TTDer ℕ-TT4) ([] , (1 , Ty) , (0 , Tm) , (2 , Tm) , (0 , Tm)) Tm
--   TypingRuleℕS-β = Tm= ([] , Ty ([] , (sym 3 [] / apr T 3 []))
--                            , Tm [] (sym 0 ([] , sym 3 []) / apr T 0 ([] ,0Tm apr T 3 []))
--                            , Tm ([] , (sym 5 [] / apr T 5 [])
--                                     , (sym 2 ([] , sym 0 []) / apr T 2 ([] ,0Tm apr T 0 [])))
--                                 (sym 3 ([] , sym 5 ([] , sym 1 [])) / apr T 3 ([] ,0Tm apr T 5 ([] ,0Tm apr T 1 [])))
--                            , Tm [] (sym 6 [] / apr T 6 []))
--                        (sym 3 ([] , sym 5 ([] , sym 0 []))
--                          <: sym 4 ([] , sym 3 ([] , var last) , sym 2 [] , sym 1 ([] , var (prev last) , var last) , sym 5 ([] , sym 0 []))
--                          / apr T 4 ([] ,1Ty apr T 3 ([] ,0Tm apr S (var 0) ([] ,0Ty apr T 7 [])) ,0Tm apr T 2 [] ,2Tm apr T 1 ([] ,0Tm apr S (var 1) ([] ,0Ty apr T 7 []) ,0Tm (apr S (var 0) ([] ,0Ty apr T 3 ([] ,0Tm apr S (var 1) ([] ,0Ty apr T 7 []))))) ,0Tm apr T 5 ([] ,0Tm apr T 0 []))
--                          // sym 1 ([] , sym 0 [] , sym 4 ([] , sym 3 ([] , var last) , sym 2 [] , sym 1 ([] , var (prev last) , var last) , sym 0 []))
--                          / apr T 1 ([] ,0Tm apr T 0 [] ,0Tm apr T 4 ([] ,1Ty apr T 3 ([] ,0Tm apr S (var 0) ([] ,0Ty apr T 7 [])) ,0Tm apr T 2 [] ,2Tm apr T 1 ([] ,0Tm apr S (var 1) ([] ,0Ty apr T 7 []) ,0Tm (apr S (var 0) ([] ,0Ty apr T 3 ([] ,0Tm apr S (var 1) ([] ,0Ty apr T 7 []))))) ,0Tm apr T 0 [])))

--   ℕ-TT5 : TypeTheory
--   ℕ-TT5 = ℕ-TT4 ,= TypingRuleℕS-β

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


text:
-- agad-modeの使い方
-- https://agda.readthedocs.io/en/latest/tools/emacs-mode.html
{-# OPTIONS --without-K --safe #-}
module Learn.Interactive where

-- ロード
-- タイプチェックする
-- C-c C-l
-- Ctrlを押しながら、cを押して次にlを押す
-- このとき、ソース内に"?"が存在すればそれをゴールにする
-- ゴールには番号が振られる

-- 型推論する
-- C-c C-d

-- 評価する
-- C-c C-n

-- 終了させる
-- C-c C-x C-q
-- Ctrlを押しながら、c、x、qと押す

-- 再スタートさせる
-- C-c C-x C-r

----------------------------------------------------------------------------
-- ゴールへの操作
-- ゴール内に値を書いてからゴールにカーソルを合わせ実行する。

-- 与える
-- C-c C-SPC
-- Ctrlを押しながら、cを押して次にスペースを押す
-- 型が合っていればゴールは消える

-- リファイン
-- C-c C-r
-- 何もない状態で行うと関数ならラムダ、レコード型ならコンストラクタを挿入する
-- ゴールに関数がある場合、関数の引数をゴールにする

-- ケーススプリット
-- C-c C-c
-- ゴール内に変数を書く、またはC-c C-cして出てきた入力枠に変数を入力すると
-- その変数でパターンマッチングを行う

-- ゴールの型を確認する
-- C-c C-t

-- 環境を確認する
-- C-c C-e

----------------------------------------------------------------------------
-- 自然数
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- 等価性
infix 3 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

-- 足し算
-- 右辺に?と書いてC-c C-l(ロード)する
-- モジュールは無視で
module Step1 where
  _+_ : ℕ → ℕ → ℕ
  m + n = {!   !}

-- ゴールに"m"と入力する
module Step2 where
  _+_ : ℕ → ℕ → ℕ
  m + n = {! m  !}

--　ゴールにカーソルを合わせ C-c C-c (ケーススプリット)する
module Step3 where
  _+_ : ℕ → ℕ → ℕ
  zero + n = {!   !}
  suc m + n = {!   !}

-- インデントを整える
module Step4 where
  _+_ : ℕ → ℕ → ℕ
  zero  + n = {!   !}
  suc m + n = {!   !}

-- ゴール内に右辺値を書く
module Step5 where
  _+_ : ℕ → ℕ → ℕ
  zero  + n = {! zero  !}
  suc m + n = {!   !}

-- ゴールにカーソルを合わせ C-c C-SPC (Give)する
module Step6 where
  _+_ : ℕ → ℕ → ℕ
  zero  + n = zero
  suc m + n = {!   !}

-- もう一方のゴールも同様にする
-- このときmは再帰的な呼び出しをするときに小さくなっている
_+_ : ℕ → ℕ → ℕ
zero  + n = zero
suc m + n = suc (m + n)

-- +の結合性
-- 証明したい型を書く。右辺を?にしてゴールにする
module Assoc1 where
  +-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
  +-assoc m n o = {!   !}

-- このとき+の定義から+の左の変数で帰納するとよいとわかる
-- 単一の変数であるならばパターンマッチングできるのでmを選びゴールに書く
module Assoc2 where
  +-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
  +-assoc m n o = {! m  !}

-- C-c C-cする
-- ここで +-assoc zero n o の右辺のゴールでC-c C-tすると　zero ≡ zero とわかる
-- 同じ形ならreflが使えるのでreflをC-c C-SPCする
module Assoc3 where
  +-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
  +-assoc zero    n o = refl
  +-assoc (suc m) n o = {!   !}

-- 次に +-assoc (suc m) n o の右辺でC-c C-tすると
-- suc ((m + n) + o) ≡ suc (m + (n + o)) とわかる
-- 両辺に同じ関数（suc）が掛かっているのでcongが使える
-- congとゴール内に書く
module Assoc4 where
  +-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
  +-assoc zero    n o = refl
  +-assoc (suc m) n o = {!cong   !}

-- C-c C-rするとゴールが分かれる
-- 前はsucを与える
module Assoc5 where
  +-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
  +-assoc zero    n o = refl
  +-assoc (suc m) n o = cong suc {!   !}

-- 後ろは+-assoc m n oの型と同じなのでそれを与える
-- これで証明終了
module Assoc6 where
  +-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
  +-assoc zero    n o = refl
  +-assoc (suc m) n o = cong suc (+-assoc m n o)


text:
module Ual.Both where

infix 10 _∧_
record _∧_ (A B : Set) : Set where
  field
    andL : A
    andR : B

max_stars_repo_name: brunoczim/ual

max_issues_repo_name: brunoczim/ual

max_forks_repo_name: brunoczim/ual


text:
{-# OPTIONS --without-K #-}
open import Function
open import Data.Zero
open import Relation.Binary.PropositionalEquality.NP
open import Explore.Zero
import Explore.Universe.Type
import Explore.Universe
open import Function.Extensionality
open import Type.Identities
open import HoTT
open Equivalences

module Explore.Universe.Base
  (open Explore.Universe.Type {𝟘})
  (u : U) where

open Explore.Universe 𝟘

open FromKit 𝟘ⁱ (λ {{ua}}{{_}} → 𝟘ˢ-ok {{ua}}) 𝟘ˡ 𝟘ᶠ
             (λ {{ua}} → Σᵉ𝟘-ok {{ua}})
             Πᵉ𝟘-ok (λ {ℓ₀ ℓ₁} ℓᵣ → ⟦𝟘ᵉ⟧ {ℓ₀} {ℓ₁} {ℓᵣ} {_≡_})
             (const 𝟙ᵁ) (λ {{ua}} {{fext}} v → equiv (λ _ ()) _ (λ f → λ= (λ())) (λ _ → refl))
             u public

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
-- Andreas, 2019-02-23, re #3578, less reduction in the unifier.
-- Non-interactive version of interaction/Issue635c.agda.

-- {-# OPTIONS -v tc.lhs.unify:50 #-}

open import Common.Bool
open import Common.Equality
open import Common.Product

test : (p : Bool × Bool) → proj₁ p ≡ true → Set
test _ refl = Bool

-- Tests that the unifier does the necessary weak head reduction.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Fragment.Examples.Semigroup.Arith.Functions where

open import Fragment.Examples.Semigroup.Arith.Base

-- Fully dynamic associativity

+-dyn-assoc₁ : ∀ {f : ℕ → ℕ} {m n o} → (f m + n) + o ≡ f m + (n + o)
+-dyn-assoc₁ = fragment SemigroupFrex +-semigroup

+-dyn-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → ((f m + n) + o) + g p ≡ f m + (n + (o + g p))
+-dyn-assoc₂ = fragment SemigroupFrex +-semigroup

+-dyn-assoc₃ : ∀ {f g h : ℕ → ℕ} {m n o p q} → (f m + n) + g o + (p + h q) ≡ f m + (n + g o + p) + h q
+-dyn-assoc₃ = fragment SemigroupFrex +-semigroup

*-dyn-assoc₁ : ∀ {f : ℕ → ℕ} {m n o} → (f m * n) * o ≡ f m * (n * o)
*-dyn-assoc₁ = fragment SemigroupFrex *-semigroup

*-dyn-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → ((f m * n) * o) * g p ≡ f m * (n * (o * g p))
*-dyn-assoc₂ = fragment SemigroupFrex *-semigroup

*-dyn-assoc₃ : ∀ {f g h : ℕ → ℕ} {m n o p q} → (f m * n) * g o * (p * h q) ≡ f m * (n * g o * p) * h q
*-dyn-assoc₃ = fragment SemigroupFrex *-semigroup

-- Partially static associativity

+-sta-assoc₁ : ∀ {f : ℕ → ℕ} {m} → (m + 2) + (3 + f 0) ≡ m + (5 + f 0)
+-sta-assoc₁ = fragment SemigroupFrex +-semigroup

+-sta-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → (((f m + g n) + 5) + o) + p ≡ f m + (g n + (2 + (3 + (o + p))))
+-sta-assoc₂ = fragment SemigroupFrex +-semigroup

+-sta-assoc₃ : ∀ {f : ℕ → ℕ} {m n o p} → f (n + m) + (n + 2) + (3 + (o + p)) ≡ f (n + m) + (((n + 1) + (4 + o)) + p)
+-sta-assoc₃ = fragment SemigroupFrex +-semigroup

*-sta-assoc₁ : ∀ {f : ℕ → ℕ} {m} → (m * 2) * (3 * f 0) ≡ m * (6 * f 0)
*-sta-assoc₁ = fragment SemigroupFrex *-semigroup

*-sta-assoc₂ : ∀ {f g : ℕ → ℕ} {m n o p} → (((f m * g n) * 6) * o) * p ≡ f m * (g n * (2 * (3 * (o * p))))
*-sta-assoc₂ = fragment SemigroupFrex *-semigroup

*-sta-assoc₃ : ∀ {f : ℕ → ℕ} {m n o p} → f (n + m) * (n * 4) * (3 * (o * p)) ≡ f (n + m) * (((n * 2) * (6 * o)) * p)
*-sta-assoc₃ = fragment SemigroupFrex *-semigroup


text:
-- Abstract definitions can't be projection-like
module Issue447 where

postulate
  I : Set
  R : I → Set

module M (i : I) (r : R i) where

  abstract

    P : Set₂
    P = Set₁

    p : P
    p = Set


text:
module Rationals where

open import Nats renaming (_+_ to _:+:_; _*_ to _:*:_)
open import Equality
open import Data.Product
open import Agda.Builtin.TrustMe

infixl 7 _÷_
infixr 5 _→ℕ
infixr 7 _÷_↓_
infixr 7 _÷_↑_
infixl 6 _+_

data ℚ : Set where
  _÷_ : (a b : ℕ) → ℚ

_→ℕ : {a : ℕ} → ℚ → ∃ (λ m → m ≡ a)
_→ℕ {a} _ = a , refl

-- of course.
_÷_↓_ : ∀ a b n → (a :*: n ÷ (b :*: n)) ≡ a ÷ b
_ ÷ _ ↓ _ = primTrustMe

_÷_↑_ : ∀ a b n → a ÷ b ≡ (a :*: n ÷ (b :*: n))
a ÷ b ↑ n = sym (a ÷ b ↓ n)

_+_ : ℚ → ℚ → ℚ
a ÷ c + b ÷ d = (a :*: d :+: b :*: c) ÷ (c :*: d)

_*_ : ℚ → ℚ → ℚ
(a ÷ c) * (b ÷ d) = a :*: b ÷ (c :*: d)

_/_ : ℚ → ℚ → ℚ
(a ÷ c) / (b ÷ d) = a :*: d ÷ (c :*: b)


text:
module Implicits.Resolution.Infinite.Expressiveness where

open import Prelude hiding (Bool)

open import Data.Fin.Substitution
open import Data.List
open import Data.List.Any
open Membership-≡

open import Extensions.ListFirst
open import SystemF.Everything as F using ()

open import Implicits.Resolution.Ambiguous.Resolution as A
open import Implicits.Resolution.Deterministic.Resolution as D
open import Implicits.Resolution.Infinite.Resolution as I
open import Implicits.Syntax
open import Implicits.Substitutions

module Deterministic⊆Infinite where

  complete : ∀ {ν} {a : Type ν} {Δ : ICtx ν} → Δ D.⊢ᵣ a → Δ I.⊢ᵣ a
  complete (r-simp x r↓a) = r-simp (proj₁ $ first⟶∈ x) (lem r↓a)
    where
      lem : ∀ {ν} {Δ : ICtx ν} {r a} → Δ D.⊢ r ↓ a → Δ I.⊢ r ↓ a
      lem (i-simp a) = i-simp a
      lem (i-iabs x₁ x₂) = i-iabs (complete x₁) (lem x₂)
      lem (i-tabs b x₁) = i-tabs b (lem x₁)
  complete (r-iabs ρ₁ x) = r-iabs (complete x)
  complete (r-tabs x) = r-tabs (complete x)

module Deterministic⊂Infinite where

  open import Implicits.Resolution.Deterministic.Incomplete as Inc

  -- We gave an example of a query that the det rules could not resolve
  --   ((Int ⇒ Bool) List.∷ Bool List.∷ List.[]) ⊢ᵣ Bool
  -- Here we derive it for the Infinite rules, to prove that we are strictly
  -- more expressive
  infinite-can : Δ I.⊢ᵣ Bool
  infinite-can = r-simp (there (here refl)) p
    where
      p : Δ I.⊢ Bool ↓ tc 0
      p = i-simp (tc 0)

module Infinite⇔Ambiguous
  (nf : ∀ {ν n} {Γ : F.Ctx ν n} {t a} → Γ F.⊢ t ∈ a → ∃ λ (t₂ : F.Term ν n) → Γ F.⊢ t₂ ⇑ a)
  where

  open import Implicits.Resolution.Ambiguous.SystemFEquiv hiding (equivalent)
  open import Implicits.Resolution.Infinite.NormalFormEquiv hiding (equivalent)
  open import Implicits.Resolution.Embedding.Lemmas
  open import Function.Equivalence

  sound : ∀ {ν} {a : Type ν} {Δ : ICtx ν} → Δ I.⊢ᵣ a → Δ A.⊢ᵣ a
  sound (r-simp x p) = lem p (r-ivar x)
    where
      lem : ∀ {ν} {Δ : ICtx ν} {a τ} → Δ I.⊢ a ↓ τ → Δ A.⊢ᵣ a → Δ A.⊢ᵣ (simpl τ)
      lem (i-simp τ) ⊢y = ⊢y
      lem (i-iabs ⊢a b↓τ) ⊢b = lem b↓τ (r-iapp ⊢b (sound ⊢a))
      lem (i-tabs b a) ⊢y = lem a (r-tapp b ⊢y)
  sound (r-iabs p) = r-iabs (sound p)
  sound (r-tabs p) = r-tabs (sound p)

  complete : ∀ {ν} {a : Type ν} {Δ : ICtx ν} → Δ A.⊢ᵣ a → Δ I.⊢ᵣ a
  complete {a = a} p = subst₂ (λ Δ r → Δ I.⊢ᵣ r) (ctx→← _) (tp→← a) (from-⇑ (proj₂ (nf (to-⊢ p))))

  equivalent : ∀ {ν} (Δ : ICtx ν) r → Δ I.⊢ᵣ r ⇔ Δ A.⊢ᵣ r
  equivalent Δ r = equivalence sound complete


text:
module Issue493 where

module M where
  postulate A B C : Set

open M using (A) hiding (B)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Fields.Fields
open import Setoids.Setoids
open import Sets.EquivalenceRelations

module Fields.FieldOfFractions.Field {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where

open import Fields.FieldOfFractions.Ring I

fieldOfFractions : Field fieldOfFractionsRing
Field.allInvertible fieldOfFractions (record { num = fst ; denom = b }) prA = (record { num = b ; denom = fst ; denomNonzero = ans }) , need
  where
    abstract
      open Setoid S
      open Equivalence eq
      need : ((b * fst) * Ring.1R R) ∼ ((fst * b) * Ring.1R R)
      need = Ring.*WellDefined R (Ring.*Commutative R) reflexive
      ans : fst ∼ Ring.0R R → False
      ans pr = prA need'
        where
          need' : (fst * Ring.1R R) ∼ (b * Ring.0R R)
          need' = transitive (Ring.*WellDefined R pr reflexive) (transitive (transitive (Ring.*Commutative R) (Ring.timesZero R)) (symmetric (Ring.timesZero R)))
Field.nontrivial fieldOfFractions pr = IntegralDomain.nontrivial I (symmetric (transitive (symmetric (Ring.timesZero R)) (transitive (Ring.*Commutative R) (transitive pr (Ring.identIsIdent R)))))
  where
    open Setoid S
    open Equivalence eq
    pr' : (Ring.0R R) * (Ring.1R R) ∼ (Ring.1R R) * (Ring.1R R)
    pr' = pr


text:
module Data.List.Combinatorics.Proofs where

import      Lvl
open import Data
open import Data.List
open import Data.List.Combinatorics
open import Data.List.Functions hiding (skip) renaming (module LongOper to List)
open        Data.List.Functions.LongOper
open import Data.List.Relation.Permutation
open import Data.List.Relation.Quantification
open import Data.List.Relation.Quantification.Proofs
open import Data.List.Relation.Sublist
open import Data.List.Relation.Sublist.Proofs
open import Data.List.Proofs
open import Data.List.Equiv.Id
open import Data.List.Proofs.Length
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
import      Data.Tuple.Raiseᵣ as Tuple₊
import      Data.Tuple.Raiseᵣ.Functions as Tuple₊
open import Functional
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Combinatorics
open import Numeral.Natural.Combinatorics.Proofs
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Multiplication
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function
open import Structure.Operator
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T A B : Type{ℓ}
private variable l l₁ l₂ : List(T)
private variable x : T
private variable n k : ℕ

sublists₊-contains-sublists : AllElements (_⊑ l) (sublists₊(l))
sublists₊-contains-sublists {l = ∅} = ∅
sublists₊-contains-sublists {l = x ⊰ l} with sublists₊(l) | sublists₊-contains-sublists {l = l}
... | ∅       | _       = use [⊑]-minimum ⊰ ∅
... | sx ⊰ sl | px ⊰ pl = use [⊑]-minimum ⊰ skip px ⊰ use px ⊰ p pl where
  p : ∀{x : T}{l}{sl} → AllElements (_⊑ l) sl → AllElements (_⊑ (x ⊰ l)) (concatMap(y ↦ y ⊰ (x ⊰ y) ⊰ ∅) sl)
  p {sl = ∅}     ∅            = ∅
  p {sl = _ ⊰ _} (sll ⊰ alsl) = (skip sll) ⊰ (use sll) ⊰ (p alsl)

{-
sublists₊-contains-all-nonempty-sublists : ∀{x}{l₁ l₂ : List(T)} → (x ⊰ l₁ ⊑ l₂) → ExistsElement (_≡ x ⊰ l₁) (sublists(l₂))
sublists₊-contains-all-nonempty-sublists {l₁ = l₁} {prepend x l₂} (use p) = ⊰ (• {!!})
sublists₊-contains-all-nonempty-sublists {l₁ = l₁} {prepend x l₂} (skip p) = ⊰ (⊰ {!sublists₊-contains-all-nonempty-sublists ?!})

sublists-contains-all-sublists : ∀{l₁ l₂ : List(T)} → (l₁ ⊑ l₂) → ExistsElement (_≡ l₁) (sublists(l₂))
sublists-contains-all-sublists {l₁ = ∅} {∅} _⊑_.empty = • [≡]-intro
sublists-contains-all-sublists {l₁ = ∅} {prepend x l₂} (skip sub) = • [≡]-intro
sublists-contains-all-sublists {l₁ = prepend x l₁} {prepend .x l₂} (use sub) = ⊰ (⊰ {!!})
sublists-contains-all-sublists {l₁ = prepend x l₁} {prepend x₁ l₂} (skip sub) = {!!}
-}

permutes-insertedEverywhere : AllElements (_permutes (x ⊰ l)) (insertedEverywhere x l)
permutes-insertedEverywhere {x = x} {∅}     = _permutes_.prepend _permutes_.empty ⊰ ∅
permutes-insertedEverywhere {x = x} {y ⊰ l} = reflexivity(_permutes_) ⊰ AllElements-mapᵣ(y List.⊰_) (p ↦ trans (_permutes_.prepend p) _permutes_.swap) (permutes-insertedEverywhere {x = x} {l})

{-
AllElements-insertedEverywhere-function : ∀{P : List(T) → Type{ℓ}} → (∀{l₁ l₂}{x} → (l₁ permutes l₂) → (P(x ⊰ l₁) → P(x ⊰ l₂))) → (∀{l₁ l₂} → (l₁ permutes l₂) → (P(l₁) → P(l₂))) → (∀{l₁ l₂ : List(T)} → (l₁ permutes l₂) → (AllElements P (insertedEverywhere x l₁) → AllElements P (insertedEverywhere x l₂)))
AllElements-insertedEverywhere-function _ pperm {l₁ = ∅}      {∅}       _permutes_.empty   p@(_ ⊰ _) = p
AllElements-insertedEverywhere-function t pperm {l₁ = x ⊰ l₁} {.x ⊰ l₂} (_permutes_.prepend perm) (p ⊰ pl) =
  pperm (_permutes_.prepend (_permutes_.prepend perm)) p ⊰
  {!AllElements-insertedEverywhere-function t pperm {l₁ = l₁} {l₂} perm!} -- TODO: Probably needs more assumptions
  -- AllElements-insertedEverywhere-function {l₁ = l₁} {l₂} pperm perm (AllElements-without-map {!!} {!!} pl)
  -- AllElements-map (x List.⊰_) (\{l} → {!!}) (AllElements-insertedEverywhere-function {l₁ = l₁} {l₂} pperm perm {!!})
AllElements-insertedEverywhere-function _ pperm {l₁ = x ⊰ .(x₁ ⊰ _)} {x₁ ⊰ .(x ⊰ _)} _permutes_.swap (p₁ ⊰ p₂ ⊰ pl) =
  pperm (trans _permutes_.swap (_permutes_.prepend _permutes_.swap)) p₂ ⊰
  pperm (trans (_permutes_.prepend _permutes_.swap) _permutes_.swap) p₁ ⊰
  {!!}
AllElements-insertedEverywhere-function t pperm (trans perm₁ perm₂) = AllElements-insertedEverywhere-function t pperm perm₂ ∘ AllElements-insertedEverywhere-function t pperm perm₁
-}

permutations-contains-permutations : AllElements (_permutes l) (permutations(l))
permutations-contains-permutations {l = ∅}         = _permutes_.empty ⊰ ∅
permutations-contains-permutations {l = x ⊰ ∅}     = _permutes_.prepend _permutes_.empty ⊰ ∅
permutations-contains-permutations {l = x ⊰ y ⊰ l} = AllElements-concatMap(insertedEverywhere x) (perm ↦ AllElements-of-transitive-binary-relationₗ (_permutes_.prepend perm) permutes-insertedEverywhere) (permutations-contains-permutations {l = y ⊰ l})

sublists₊-length : length(sublists₊ l) ≡ (2 ^ (length l)) −₀ 1
sublists₊-length {l = ∅} = [≡]-intro
sublists₊-length {l = x ⊰ l} =
  length(sublists₊ (x ⊰ l))                                                               🝖[ _≡_ ]-[]
  length(singleton(x) ⊰ foldᵣ (prev ↦ rest ↦ (prev ⊰ (x ⊰ prev) ⊰ rest)) ∅ (sublists₊ l)) 🝖[ _≡_ ]-[]
  𝐒(length(foldᵣ (prev ↦ rest ↦ (prev ⊰ (x ⊰ prev) ⊰ rest)) ∅ (sublists₊ l)))             🝖[ _≡_ ]-[ [≡]-with(𝐒) (length-foldᵣ {l = sublists₊(l)}{init = ∅}{f = (prev ↦ rest ↦ (prev ⊰ (x ⊰ prev) ⊰ rest))}{g = const(𝐒 ∘ 𝐒)} [≡]-intro) ]
  𝐒(foldᵣ (prev ↦ rest ↦ 𝐒(𝐒(rest))) 𝟎 (sublists₊ l))                                     🝖[ _≡_ ]-[ [≡]-with(𝐒) (foldᵣ-constant-[+]ᵣ{l = sublists₊ l}{init = 𝟎}) ]
  𝐒(2 ⋅ length(sublists₊ l))     🝖[ _≡_ ]-[ [≡]-with(𝐒 ∘ (2 ⋅_)) (sublists₊-length {l = l}) ]
  𝐒(2 ⋅ (2 ^ (length l) −₀ 1))   🝖[ _≡_ ]-[ [≡]-with(𝐒) (distributivityₗ(_⋅_)(_−₀_) {2}{2 ^ length(l)}{1}) ]
  𝐒((2 ⋅ (2 ^ (length l))) −₀ 2) 🝖[ _≡_ ]-[]
  𝐒((2 ^ 𝐒(length l)) −₀ 2)      🝖[ _≡_ ]-[]
  𝐒((2 ^ length(x ⊰ l)) −₀ 2)    🝖[ _≡_ ]-[ [↔]-to-[→] [−₀][𝐒]ₗ-equality ([^]ₗ-strictly-growing {0}{0}{𝐒(length l)} [≤]-with-[𝐒]) ]-sym
  𝐒(2 ^ length(x ⊰ l)) −₀ 2      🝖[ _≡_ ]-[]
  (2 ^ length (x ⊰ l)) −₀ 1      🝖-end

sublists-length : length(sublists l) ≡ 2 ^ (length l)
sublists-length {l = l} =
  length(sublists l)      🝖[ _≡_ ]-[]
  length(∅ ⊰ sublists₊ l) 🝖[ _≡_ ]-[]
  𝐒(length(sublists₊ l))  🝖[ _≡_ ]-[ [≡]-with(𝐒) (sublists₊-length {l = l}) ]
  𝐒((2 ^ length(l)) −₀ 1) 🝖[ _≡_ ]-[ [↔]-to-[→] [−₀][𝐒]ₗ-equality ([^]ₗ-growing {2}{0}{length l} (\()) [≤]-minimum) ]-sym
  𝐒(2 ^ length(l)) −₀ 1   🝖[ _≡_ ]-[]
  2 ^ length(l)           🝖-end

combinations-length : length(combinations k l) ≡ 𝑐𝐶(length(l))(k)
combinations-length {0}   {l = _} = [≡]-intro
combinations-length {𝐒 k} {l = ∅} = [≡]-intro
combinations-length {1}   {l = x ⊰ l} =
  length(combinations 1 (x ⊰ l))    🝖[ _≡_ ]-[]
  length(x ⊰ l)                     🝖[ _≡_ ]-[]
  𝐒(length l)                       🝖[ _≡_ ]-[ 𝑐𝐶-singleton-subsets ]-sym
  𝐒(𝑐𝐶 (length l) 1)                🝖[ _≡_ ]-[]
  1 + 𝑐𝐶 (length l) 1               🝖[ _≡_ ]-[]
  𝑐𝐶 (length l) 0 + 𝑐𝐶 (length l) 1 🝖[ _≡_ ]-[]
  𝑐𝐶 (𝐒(length l)) 1                🝖[ _≡_ ]-[]
  𝑐𝐶 (length(x ⊰ l)) 1              🝖-end
combinations-length {𝐒(𝐒 k)} {l = x ⊰ l} =
  length(combinations (𝐒(𝐒 k)) (x ⊰ l))                                       🝖[ _≡_ ]-[]
  length(map (x ,_) (combinations (𝐒 k) l) ++ combinations (𝐒(𝐒 k)) l)        🝖[ _≡_ ]-[ length-[++] {l₁ = map (x ,_) (combinations (𝐒 k) l)}{l₂ = combinations (𝐒(𝐒 k)) l} ]
  length(map (x ,_) (combinations (𝐒 k) l)) + length(combinations (𝐒(𝐒 k)) l) 🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(length(combinations (𝐒(𝐒 k)) l)) (length-map{f = (x ,_)}{x = combinations (𝐒 k) l}) ]
  length(combinations (𝐒 k) l) + length(combinations (𝐒(𝐒 k)) l)              🝖[ _≡_ ]-[ congruence₂(_+_) (combinations-length {𝐒 k} {l = l}) (combinations-length {𝐒(𝐒 k)} {l = l}) ]
  𝑐𝐶(length(l))(𝐒 k) + 𝑐𝐶(length(l))(𝐒(𝐒 k))                                  🝖[ _≡_ ]-[]
  𝑐𝐶 (length(x ⊰ l)) (𝐒(𝐒 k))                                                 🝖-end

repeatableCombinations-length : length(repeatableCombinations k l) ≡ 𝑐𝐶((length(l) + k) −₀ 1)(k)
repeatableCombinations-length {0}      {l = _} = [≡]-intro
repeatableCombinations-length {1}      {l = x ⊰ l} = [≡]-intro
repeatableCombinations-length {𝐒 k}    {l = ∅} = symmetry(_≡_) (𝑐𝐶-larger-subsets{k}{𝐒(k)} (reflexivity(_≤_)))
repeatableCombinations-length {𝐒(𝐒 k)} {l = x ⊰ l} =
  length (repeatableCombinations (𝐒(𝐒 k)) (x ⊰ l))                                                        🝖[ _≡_ ]-[]
  length(map(x ,_) (repeatableCombinations (𝐒 k) (x ⊰ l)) ++ repeatableCombinations(𝐒(𝐒 k)) l)            🝖[ _≡_ ]-[ length-[++] {l₁ = map(x ,_) (repeatableCombinations (𝐒 k) (x ⊰ l))}{l₂ = repeatableCombinations(𝐒(𝐒 k)) l} ]
  length(map(x ,_) (repeatableCombinations (𝐒 k) (x ⊰ l))) + length(repeatableCombinations(𝐒(𝐒 k)) l)     🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(length(repeatableCombinations(𝐒(𝐒 k)) l)) (length-map {f = x ,_}{x = repeatableCombinations (𝐒 k) (x ⊰ l)}) ]
  length(repeatableCombinations (𝐒 k) (x ⊰ l))             + length(repeatableCombinations(𝐒(𝐒 k)) l)     🝖[ _≡_ ]-[ congruence₂(_+_) (repeatableCombinations-length{k = 𝐒 k}{l = x ⊰ l}) (repeatableCombinations-length{k = 𝐒(𝐒 k)}{l = l}) ]
  𝑐𝐶((length(x ⊰ l) + 𝐒(k)) −₀ 1)(𝐒(k))                    + 𝑐𝐶((length(l) + 𝐒(𝐒(k))) −₀ 1)(𝐒(𝐒(k)))      🝖[ _≡_ ]-[]
  𝑐𝐶((length(x ⊰ l) + 𝐒(𝐒 k)) −₀ 1) (𝐒(𝐒 k))                                                              🝖-end

tuples-length : length(tuples n l) ≡ length(l) ^ n
tuples-length {0} = [≡]-intro
tuples-length {1} = [≡]-intro
tuples-length {𝐒(𝐒(n))}{l = ∅} = [≡]-intro
tuples-length {𝐒(𝐒(n))}{l = x ⊰ l} =
  length(tuples(𝐒(𝐒(n))) (x ⊰ l))                                                   🝖[ _≡_ ]-[]
  length(concatMap(y ↦ map (y Tuple₊.⊰_) (tuples (𝐒(n)) (x ⊰ l))) (x ⊰ l))          🝖[ _≡_ ]-[ length-concatMap {l = x ⊰ l}{f = y ↦ map (y Tuple₊.⊰_) (tuples (𝐒(n)) (x ⊰ l))} ]
  foldᵣ((_+_) ∘ length ∘ (y ↦ map (y Tuple₊.⊰_) (tuples (𝐒(n)) (x ⊰ l)))) 𝟎 (x ⊰ l) 🝖[ _≡_ ]-[ foldᵣ-function₊-raw {l₁ = x ⊰ l}{a₁ = 𝟎} (\{a b} → [≡]-with(_+ b) (length-map{f = a Tuple₊.⊰_}{x = tuples (𝐒(n)) (x ⊰ l)})) [≡]-intro [≡]-intro ]
  foldᵣ((_+_) ∘ length ∘ (y ↦ tuples (𝐒(n)) (x ⊰ l))) 𝟎 (x ⊰ l)                     🝖[ _≡_ ]-[]
  foldᵣ(const(length(tuples (𝐒(n)) (x ⊰ l)) +_)) 𝟎 (x ⊰ l)                          🝖[ _≡_ ]-[ foldᵣ-constant-[+]ₗ{l = x ⊰ l} {init = 𝟎}{step = length(tuples (𝐒(n)) (x ⊰ l))} ]
  length(x ⊰ l) ⋅ length(tuples(𝐒(n)) (x ⊰ l))                                      🝖[ _≡_ ]-[ congruence₂ᵣ(_⋅_) (length(x ⊰ l)) (tuples-length {𝐒(n)} {l = x ⊰ l}) ]
  length(x ⊰ l) ⋅ (length(x ⊰ l) ^ 𝐒(n))                                            🝖[ _≡_ ]-[]
  length(x ⊰ l) ^ 𝐒(𝐒(n))                                                           🝖-end

rotations-length : length(rotations l) ≡ length(l)
rotations-length{l = l} = length-accumulateIterate₀{f = rotateₗ(1)}{init = l}

insertedEverywhere-contents-length : AllElements(p ↦ length(p) ≡ 𝐒(length(l))) (insertedEverywhere x l)
insertedEverywhere-contents-length = AllElements-fn (Function.congruence ⦃ _ ⦄ Proofs.permutes-length-function) permutes-insertedEverywhere

insertedEverywhere-length : length(insertedEverywhere x l) ≡ 𝐒(length(l))
insertedEverywhere-length {x = x} {∅}     = [≡]-intro
insertedEverywhere-length {x = x} {a ⊰ l} =
  length(insertedEverywhere x (a ⊰ l))                                  🝖[ _≡_ ]-[]
  length((x ⊰ a ⊰ l) ⊰ (map (List.prepend a) (insertedEverywhere x l))) 🝖[ _≡_ ]-[]
  𝐒(length(map (List.prepend a) (insertedEverywhere x l)))              🝖[ _≡_ ]-[ [≡]-with(𝐒) (length-map{f = List.prepend a}{x = insertedEverywhere x l}) ]
  𝐒(length(insertedEverywhere x l))                                     🝖[ _≡_ ]-[ [≡]-with(𝐒) (insertedEverywhere-length {x = x} {l}) ]
  𝐒(𝐒(length(l)))                                                       🝖[ _≡_ ]-[]
  𝐒(length(a ⊰ l))                                                      🝖-end

permutation-length : AllElements(p ↦ length p ≡ length l) (permutations l)
permutation-length{l = l} = AllElements-fn (Function.congruence ⦃ _ ⦄ Proofs.permutes-length-function) (permutations-contains-permutations{l = l})

{-permutations-length : length(permutations l) ≡ length(l) !
permutations-length {l = ∅}         = [≡]-intro
permutations-length {l = x ⊰ ∅}     = [≡]-intro
permutations-length {l = x ⊰ y ⊰ l} =
  length(permutations(x ⊰ y ⊰ l))                                🝖[ _≡_ ]-[]
  length(concatMap(insertedEverywhere x) (permutations(y ⊰ l)))  🝖[ _≡_ ]-[ length-concatMap{l = permutations(y ⊰ l)}{f = insertedEverywhere x} ]
  foldᵣ (_+_ ∘ length ∘ insertedEverywhere x) 𝟎 (permutations (y ⊰ l)) 🝖[ _≡_ ]-[ {!!} ]
  foldᵣ (_+_ ∘ length) 𝟎 (map (insertedEverywhere x) (permutations (y ⊰ l))) 🝖[ _≡_ ]-[ {!!} ]
  𝐒(𝐒(length l)) ⋅ (𝐒(length l) ⋅ (length(l)!)) 🝖[ _≡_ ]-[]
  length(x ⊰ y ⊰ l)! 🝖-end
-}
{-permutations-length {l = x ⊰ y ⊰ l} with permutations(y ⊰ l) | permutations-length {l = y ⊰ l}
... | ∅       | p = {!!}
... | z ⊰ pyl | p =
  length(foldᵣ((_++_) ∘ insertedEverywhere x) ∅ (z ⊰ pyl))                            🝖[ _≡_ ]-[]
  length(insertedEverywhere x z ++ foldᵣ((_++_) ∘ insertedEverywhere x) ∅ pyl)        🝖[ _≡_ ]-[ length-[++] {l₁ = insertedEverywhere x z}{l₂ = foldᵣ((_++_) ∘ insertedEverywhere x) ∅ pyl} ]
  length(insertedEverywhere x z) + length(foldᵣ((_++_) ∘ insertedEverywhere x) ∅ pyl) 🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(length(foldᵣ((_++_) ∘ insertedEverywhere x) ∅ pyl)) (insertedEverywhere-length {x = x}{l = z}) ]
  𝐒(length z)                    + length(foldᵣ((_++_) ∘ insertedEverywhere x) ∅ pyl) 🝖[ _≡_ ]-[ {!!} ]
  𝐒(𝐒(length l)) ⋅ 𝐒(length pyl)                                                      🝖[ _≡_ ]-[ congruence₂ᵣ(_⋅_)(𝐒(𝐒(length l))) p ]
  𝐒(𝐒(length l)) ⋅ (𝐒(length l) ⋅ (length(l) !))                                      🝖-end-}
{- TODO: Proof of above
length(concatMap (insertedEverywhere x) (permutations(y ⊰ l)))
foldᵣ((_+_) ∘ length ∘ (insertedEverywhere x)) (permutations(y ⊰ l))
foldᵣ((_+_) ∘ 𝐒 ∘ length) (permutations(y ⊰ l))
foldᵣ((_+_) ∘ 𝐒) (map length(permutations(y ⊰ l)))
foldᵣ((_+_) ∘ 𝐒) (map (const(length(y ⊰ l))) (permutations(y ⊰ l))) -- from permutation-length when map function yields the same value for every element in the list
foldᵣ((_+_) ∘ 𝐒 ∘ const(length(y ⊰ l))) (permutations(y ⊰ l))
foldᵣ((_+_) ∘ const(𝐒 ∘ length(y ⊰ l))) (permutations(y ⊰ l))
𝐒(length(y ⊰ l)) ⋅ length(permutations(y ⊰ l))
𝐒(length(y ⊰ l)) ⋅ (length(y ⊰ l) !)
-}

{-  length(permutations (x ⊰ y ⊰ l))                                    🝖[ _≡_ ]-[ {!!} ]
  -- length(concatMap (insertedEverywhere x) (permutations(y ⊰ l)))      🝖[ _≡_ ]-[ length-concatMap {l = permutations(y ⊰ l)}{f = insertedEverywhere x} ]
  -- foldᵣ (_+_ ∘ length ∘ insertedEverywhere x) 𝟎 (permutations(y ⊰ l)) 🝖[ _≡_ ]-[ {!length-foldᵣ {l = permutations(y ⊰ l)}{init = 𝟎}!} ]
  𝐒(𝐒(length l)) ⋅ (𝐒(length l) ⋅ (length(l) !))                      🝖[ _≡_ ]-[]
  (length(x ⊰ y ⊰ l) !)                                               🝖-end
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --type-in-type #-}

open import Function
open import Data.Nat.Base
open import Data.Bool.Base
open import Data.Product

{-# NO_POSITIVITY_CHECK #-}
record IFix {I : Set} (F : (I -> Set) -> I -> Set) (i : I) : Set where
  constructor wrap
  field unwrap : F (IFix F) i
open IFix

data Expr : Set -> Set where
  Lit  : ℕ -> Expr ℕ
  Inc  : Expr ℕ -> Expr ℕ
  IsZ  : Expr ℕ -> Expr Bool
  Pair : ∀ {A B} -> Expr A -> Expr B -> Expr (A × B)
  Fst  : ∀ {A B} -> Expr (A × B) -> Expr A
  Snd  : ∀ {A B} -> Expr (A × B) -> Expr B

-- As usually the pattern vector of a Scott-encoded data type encodes pattern-matching.
ExprF′ : (Set -> Set) -> Set -> Set
ExprF′
  = λ Rec I
  -> (R : Set -> Set)
  -> (ℕ -> R ℕ)
  -> (Rec ℕ -> R ℕ)
  -> (Rec ℕ -> R Bool)
  -> (∀ {A B} -> Rec A -> Rec B -> R (A × B))
  -> (∀ {A B} -> Rec (A × B) -> R A)
  -> (∀ {A B} -> Rec (A × B) -> R B)
  -> R I

Expr′ : Set -> Set
Expr′ = IFix ExprF′

expr-to-expr′ : ∀ {A} -> Expr A -> Expr′ A
expr-to-expr′ (Lit x)    = wrap λ R lit inc isZ pair fst snd -> lit x
expr-to-expr′ (Inc x)    = wrap λ R lit inc isZ pair fst snd -> inc (expr-to-expr′ x)
expr-to-expr′ (IsZ x)    = wrap λ R lit inc isZ pair fst snd -> isZ (expr-to-expr′ x)
expr-to-expr′ (Pair x y) = wrap λ R lit inc isZ pair fst snd -> pair (expr-to-expr′ x) (expr-to-expr′ y)
expr-to-expr′ (Fst p)    = wrap λ R lit inc isZ pair fst snd -> fst (expr-to-expr′ p)
expr-to-expr′ (Snd p)    = wrap λ R lit inc isZ pair fst snd -> snd (expr-to-expr′ p)

{-# TERMINATING #-}
expr′-to-expr : ∀ {A} -> Expr′ A -> Expr A
expr′-to-expr e =
  unwrap
    e
    Expr
    Lit
    (Inc ∘ expr′-to-expr)
    (IsZ ∘ expr′-to-expr)
    (λ x y -> Pair (expr′-to-expr x) (expr′-to-expr y))
    (Fst ∘ expr′-to-expr)
    (Snd ∘ expr′-to-expr)

isZero : ℕ -> Bool
isZero zero    = true
isZero (suc _) = false

{-# TERMINATING #-}
evalExpr′ : ∀ {A} -> Expr′ A -> A
evalExpr′ e =
  unwrap
    e
    id
    id
    (suc ∘ evalExpr′)
    (isZero ∘ evalExpr′)
    (λ x y -> (evalExpr′ x , evalExpr′ y))
    (proj₁ ∘ evalExpr′)
    (proj₂ ∘ evalExpr′)

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus