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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Numbers.Integers.Integers
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Subtraction
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.Naturals.Exponentiation
open import Numbers.Primes.PrimeNumbers
open import Maybe
open import Semirings.Definition
import Semirings.Solver

open module NatSolver = Semirings.Solver ℕSemiring multiplicationNIsCommutative

module LectureNotes.NumbersAndSets.Lecture1 where

a-Na : (a : ℕ) → a -N' a ≡ yes 0
a-Na zero = refl
a-Na (succ a) = a-Na a

-N''lemma : (a b : ℕ) → (a<b : a ≤N b) → b -N' a ≡ yes (subtractionNResult.result (-N a<b))
-N''lemma zero (succ b) (inl x) = refl
-N''lemma (succ a) (succ b) (inl x) = -N''lemma a b (inl (canRemoveSuccFrom<N x))
-N''lemma a b (inr x) rewrite x | a-Na b = ans
  where
    ans : yes 0 ≡ yes (subtractionNResult.result (-N (inr (refl {x = b}))))
    ans with -N (inr (refl {x = b}))
    ans | record { result = result ; pr = pr } with result
    ans | record { result = result ; pr = pr } | zero = refl
    ans | record { result = result ; pr = pr } | succ bl = exFalso (cannotAddAndEnlarge'' pr)

-N'' : (a b : ℕ) (a<b : a ≤N b) → ℕ
-N'' a b a<b with -N''lemma a b a<b
... | bl with b -N' a
-N'' a b a<b | bl | yes x = x

n3Bigger : (n : ℕ) → (n ≡ 0) || (n ≤N n ^N 3)
n3Bigger n = exponentiationIncreases n 2

n3Bigger' : (n : ℕ) → n ≤N n ^N 3
n3Bigger' zero = inr refl
n3Bigger' (succ n) with n3Bigger (succ n)
n3Bigger' (succ n) | inr f = f

-- How to use the semiring solver
-- The process is very mechanical; I haven't yet worked out how to do reflection,
-- so there's quite a bit of transcribing expressions into the Expr form.
-- The first two arguments to from-to-by are totally mindless in construction.
proof : (n : ℕ) → ((n *N n) +N ((2 *N n) +N 1)) ≡ (n +N 1) *N (n +N 1)
proof n =
  from plus (times (const n) (const n)) (plus (times (succ (succ zero)) (const n)) (succ zero))
  to times (plus (const n) (succ zero)) (plus (const n) (succ zero))
  by
    applyEquality (λ i → succ (n *N n) +N (n +N i)) ((from (const n) to (plus (const n) zero) by refl))

ext: agda


text:
------------------------------------------------------------------------------
-- Induction principles for Tree and Forest
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Mirror.Induction.InductionPrinciples where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Program.Mirror.Type

------------------------------------------------------------------------------
-- These induction principles *not cover* the mutual structure of the
-- types Tree and Rose (Bertot and Casterán, 2004, p. 401).

-- Induction principle for Tree.
Tree-ind : (A : D → Set) →
           (∀ d {ts} → Forest ts → A (node d ts)) →
           ∀ {t} → Tree t → A t
Tree-ind A h (tree d Fts) = h d Fts

-- Induction principle for Forest.
Forest-ind : (A : D → Set) →
             A [] →
             (∀ {t ts} → Tree t → Forest ts → A ts → A (t ∷ ts)) →
             ∀ {ts} → Forest ts → A ts
Forest-ind A A[] h fnil           = A[]
Forest-ind A A[] h (fcons Tt Fts) = h Tt Fts (Forest-ind A A[] h Fts)

------------------------------------------------------------------------------
-- References
--
-- Bertot, Yves and Castéran, Pierre (2004). Interactive Theorem
-- Proving and Program Development. Coq’Art: The Calculus of Inductive
-- Constructions. Springer.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Polynomial.Simple.Solver where

open import Polynomial.Expr public
open import Polynomial.Simple.AlmostCommutativeRing public hiding (-raw-almostCommutative⟶)
open import Data.Vec hiding (_⊛_)
open import Algebra.Solver.Ring.AlmostCommutativeRing using (-raw-almostCommutative⟶)
open import Polynomial.Parameters
open import Function
open import Data.Maybe
open import Data.Vec.N-ary
open import Data.Bool using (Bool; true; false; T; if_then_else_)
open import Data.Empty using (⊥-elim)

module Ops {ℓ₁ ℓ₂} (ring : AlmostCommutativeRing ℓ₁ ℓ₂) where
  open AlmostCommutativeRing ring

  zero-homo : ∀ x → T (is-just (0≟ x)) → 0# ≈ x
  zero-homo x _ with 0≟ x
  zero-homo x _ | just p = p
  zero-homo x () | nothing

  homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂
  homo = record
    { coeffs = record
      { coeffs = AlmostCommutativeRing.rawRing ring
      ; Zero-C = λ x → is-just (0≟ x)
      }
    ; ring = record
      { isAlmostCommutativeRing = record
          { isCommutativeSemiring = isCommutativeSemiring
          ; -‿cong = -‿cong
          ; -‿*-distribˡ = -‿*-distribˡ
          ; -‿+-comm = -‿+-comm
          }
      }
    ; morphism = -raw-almostCommutative⟶ _
    ; Zero-C⟶Zero-R = zero-homo
    }

  ⟦_⟧ : ∀ {n} → Expr Carrier n → Vec Carrier n → Carrier
  ⟦ Κ x ⟧ ρ = x
  ⟦ Ι x ⟧ ρ = lookup ρ x
  ⟦ x ⊕ y ⟧ ρ = ⟦ x ⟧ ρ + ⟦ y ⟧ ρ
  ⟦ x ⊗ y ⟧ ρ = ⟦ x ⟧ ρ * ⟦ y ⟧ ρ
  ⟦ ⊝ x ⟧ ρ = - ⟦ x ⟧ ρ
  ⟦ x ⊛ i ⟧ ρ = ⟦ x ⟧ ρ ^ i

  open import Polynomial.NormalForm.Definition (Homomorphism.coeffs homo)
  open import Polynomial.NormalForm.Operations (Homomorphism.coeffs homo)

  norm : ∀ {n} → Expr Carrier n → Poly n
  norm = go
    where
    go : ∀ {n} → Expr Carrier n → Poly n
    go (Κ x) = κ x
    go (Ι x) = ι x
    go (x ⊕ y) = go x ⊞ go y
    go (x ⊗ y) = go x ⊠ go y
    go (⊝ x) = ⊟ go x
    go (x ⊛ i) = go x ⊡ i

  ⟦_⇓⟧ : ∀ {n} → Expr Carrier n → Vec Carrier n → Carrier
  ⟦ expr ⇓⟧ = ⟦ norm expr ⟧ₚ where

    open import Polynomial.NormalForm.Semantics homo
      renaming (⟦_⟧ to ⟦_⟧ₚ)

  correct : ∀ {n} (expr : Expr Carrier n) ρ → ⟦ expr ⇓⟧ ρ ≈ ⟦ expr ⟧ ρ
  correct {n = n} = go
    where
    open import Polynomial.Homomorphism homo

    go : ∀ (expr : Expr Carrier n) ρ → ⟦ expr ⇓⟧ ρ ≈ ⟦ expr ⟧ ρ
    go (Κ x) ρ = κ-hom x ρ
    go (Ι x) ρ = ι-hom x ρ
    go (x ⊕ y) ρ = ⊞-hom (norm x) (norm y) ρ ⟨ trans ⟩ (go x ρ ⟨ +-cong ⟩ go y ρ)
    go (x ⊗ y) ρ = ⊠-hom (norm x) (norm y) ρ ⟨ trans ⟩ (go x ρ ⟨ *-cong ⟩ go y ρ)
    go (⊝ x) ρ = ⊟-hom (norm x) ρ ⟨ trans ⟩ -‿cong (go x ρ)
    go (x ⊛ i) ρ = ⊡-hom (norm x) i ρ ⟨ trans ⟩ pow-cong i (go x ρ)

  open import Relation.Binary.Reflection setoid Ι ⟦_⟧ ⟦_⇓⟧ correct public

open import Data.Nat using (ℕ)
open import Data.Product

solve : ∀ {ℓ₁ ℓ₂}
      → (ring : AlmostCommutativeRing ℓ₁ ℓ₂)
      → (n : ℕ)
      → (f : N-ary n (Expr (AlmostCommutativeRing.Carrier ring) n) (Expr (AlmostCommutativeRing.Carrier ring) n × Expr (AlmostCommutativeRing.Carrier ring) n))
      → Eqʰ n (AlmostCommutativeRing._≈_ ring) (curryⁿ (Ops.⟦_⇓⟧ ring  (proj₁ (Ops.close ring n f)))) (curryⁿ (Ops.⟦_⇓⟧ ring (proj₂ (Ops.close ring n f))))
      → Eq  n (AlmostCommutativeRing._≈_ ring) (curryⁿ (Ops.⟦_⟧ ring (proj₁ (Ops.close ring n f)))) (curryⁿ (Ops.⟦_⟧ ring (proj₂ (Ops.close ring n f))))
solve ring = solve′
  where
  open Ops ring renaming (solve to solve′)
{-# INLINE solve #-}

_⊜_ : ∀ {ℓ₁ ℓ₂}
    → (ring : AlmostCommutativeRing ℓ₁ ℓ₂)
    → (n : ℕ)
    → Expr (AlmostCommutativeRing.Carrier ring) n
    → Expr (AlmostCommutativeRing.Carrier ring) n
    → Expr (AlmostCommutativeRing.Carrier ring) n × Expr (AlmostCommutativeRing.Carrier ring) n
_⊜_ _ _ = _,_
{-# INLINE _⊜_ #-}

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
------------------------------------------------------------------------
-- A class of algebraic structures, based on non-recursive simple
-- types, satisfies the property that isomorphic instances of a
-- structure are equal (assuming univalence)
------------------------------------------------------------------------

-- In fact, isomorphism and equality are basically the same thing, and
-- the main theorem can be instantiated with several different
-- "universes", not only the one based on simple types.

-- This module is similar to
-- Univalence-axiom.Isomorphism-is-equality.Simple, but the
-- definitions of isomorphism used below are perhaps closer to the
-- "standard" ones. Carrier types also live in Type rather than Type₁
-- (at the cost of quite a bit of lifting).

-- This module has been developed in collaboration with Thierry
-- Coquand.

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

open import Equality

module Univalence-axiom.Isomorphism-is-equality.Simple.Variant
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq as B using (_↔_)
open Derived-definitions-and-properties eq
  renaming (lower-extensionality to lower-ext)
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq hiding (id; _∘_)
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence using (_⇔_; module _⇔_)
open import Preimage eq
open import Prelude as P hiding (id)
open import Univalence-axiom eq

------------------------------------------------------------------------
-- Universes with some extra stuff

-- A record type packing up some assumptions.

record Assumptions : Type₃ where
  field

    -- Univalence at three different levels.

    univ  : Univalence (# 0)
    univ₁ : Univalence (# 1)
    univ₂ : Univalence (# 2)

  abstract

    -- Extensionality.

    ext : Extensionality (# 1) (# 1)
    ext = dependent-extensionality univ₂ univ₁

    ext₀ : Extensionality (# 0) (# 0)
    ext₀ = dependent-extensionality univ₁ univ

-- Universes with some extra stuff.

record Universe : Type₃ where
  field

    -- Codes for something.

    U : Type₁

    -- Interpretation of codes.

    El : U → Type → Type₁

    -- A predicate, possibly specifying what it means for a bijection
    -- to be an isomorphism between two elements.

    Is-isomorphism : ∀ a {B C} → B ↔ C → El a B → El a C → Type₁

    -- El a, seen as a predicate, respects equivalences (assuming
    -- univalence).

    resp : Assumptions → ∀ a {B C} → B ≃ C → El a B → El a C

    -- The resp function respects identities (assuming univalence).

    resp-id : (ass : Assumptions) →
              ∀ a {B} (x : El a B) → resp ass a Eq.id x ≡ x

  -- An alternative definition of Is-isomorphism, (possibly) defined
  -- using univalence.

  Is-isomorphism′ : Assumptions →
                    ∀ a {B C} → B ↔ C → El a B → El a C → Type₁
  Is-isomorphism′ ass a B↔C x y = resp ass a (Eq.↔⇒≃ B↔C) x ≡ y

  field

    -- Is-isomorphism and Is-isomorphism′ are isomorphic (assuming
    -- univalence).

    isomorphism-definitions-isomorphic :
      (ass : Assumptions) →
      ∀ a {B C} (B↔C : B ↔ C) {x y} →
      Is-isomorphism a B↔C x y ↔ Is-isomorphism′ ass a B↔C x y

  -- Another alternative definition of Is-isomorphism, defined using
  -- univalence.

  Is-isomorphism″ : Assumptions →
                    ∀ a {B C} → B ↔ C → El a B → El a C → Type₁
  Is-isomorphism″ ass a B↔C x y =
    subst (El a) (≃⇒≡ univ (Eq.↔⇒≃ B↔C)) x ≡ y
    where open Assumptions ass

  abstract

    -- Every element is isomorphic to itself, transported along the
    -- isomorphism.

    isomorphic-to-itself :
      (ass : Assumptions) → let open Assumptions ass in
      ∀ a {B C} (B↔C : B ↔ C) x →
      Is-isomorphism′ ass a B↔C x
        (subst (El a) (≃⇒≡ univ (Eq.↔⇒≃ B↔C)) x)
    isomorphic-to-itself ass a B↔C x =
      transport-theorem (El a) (resp ass a) (resp-id ass a)
                        univ (Eq.↔⇒≃ B↔C) x
      where open Assumptions ass

    -- Is-isomorphism and Is-isomorphism″ are isomorphic (assuming
    -- univalence).

    isomorphism-definitions-isomorphic₂ :
      (ass : Assumptions) →
      ∀ a {B C} (B↔C : B ↔ C) {x y} →
      Is-isomorphism a B↔C x y ↔ Is-isomorphism″ ass a B↔C x y
    isomorphism-definitions-isomorphic₂ ass a B↔C {x} {y} =
      Is-isomorphism      a B↔C x y  ↝⟨ isomorphism-definitions-isomorphic ass a B↔C ⟩
      Is-isomorphism′ ass a B↔C x y  ↝⟨ ≡⇒↝ _ $ cong (λ z → z ≡ y) $ isomorphic-to-itself ass a B↔C x ⟩□
      Is-isomorphism″ ass a B↔C x y  □

------------------------------------------------------------------------
-- A universe-indexed family of classes of structures

module Class (Univ : Universe) where

  open Universe Univ

  -- Codes for structures.

  Code : Type₃
  Code =
    -- A code.
    Σ U λ a →

    -- A proposition.
    (C : Set (# 0)) → El a ⌞ C ⌟ → Σ Type₁ λ P →
      -- The proposition should be propositional (assuming
      -- univalence).
      Assumptions → Is-proposition P

  -- Interpretation of the codes. The elements of "Instance c" are
  -- instances of the structure encoded by c.

  Instance : Code → Type₁
  Instance (a , P) =
    -- A carrier set.
    Σ (Set (# 0)) λ C →

    -- An element.
    Σ (El a ⌞ C ⌟) λ x →

    -- The element should satisfy the proposition.
    proj₁ (P C x)

  -- The carrier type.

  Carrier : ∀ c → Instance c → Type
  Carrier _ I = ⌞ proj₁ I ⌟

  -- The "element".

  element : ∀ c (I : Instance c) → El (proj₁ c) (Carrier c I)
  element _ I = proj₁ (proj₂ I)

  -- One can prove that two instances of a structure are equal by
  -- proving that the carrier types and "elements" (suitably
  -- transported) are equal (assuming univalence).

  instances-equal↔ :
    Assumptions →
    ∀ c {I₁ I₂} →
    (I₁ ≡ I₂) ↔
    ∃ λ (C-eq : Carrier c I₁ ≡ Carrier c I₂) →
      subst (El (proj₁ c)) C-eq (element c I₁) ≡ element c I₂
  instances-equal↔ ass (a , P)
                   {(C₁ , S₁) , x₁ , p₁} {(C₂ , S₂) , x₂ , p₂} =

    ((C₁ , λ {_ _} → S₁) , x₁ , p₁) ≡ ((C₂ , λ {_ _} → S₂) , x₂ , p₂)  ↔⟨ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ bij ⟩

    ((C₁ , x₁) , ((λ {_ _} → S₁) , p₁)) ≡
    ((C₂ , x₂) , ((λ {_ _} → S₂) , p₂))                                ↝⟨ inverse $ ignore-propositional-component prop ⟩

    ((C₁ , x₁) ≡ (C₂ , x₂))                                            ↝⟨ inverse B.Σ-≡,≡↔≡ ⟩□

    (∃ λ (C-eq : C₁ ≡ C₂) → subst (El a) C-eq x₁ ≡ x₂)                 □

    where
    bij : Instance (a , P) ↔
          Σ (Σ Type (El a)) λ { (C , x) →
          Σ (Is-set C) λ S → proj₁ (P (C , S) x) }
    bij =
      (Σ (Σ Type Is-set) λ { (C , S) →
         Σ (El a C) λ x → proj₁ (P (C , S) x) })    ↝⟨ inverse Σ-assoc ⟩

      (Σ Type λ C → Σ (Is-set C) λ S →
         Σ (El a C) λ x → proj₁ (P (C , S) x))      ↝⟨ ∃-cong (λ _ → ∃-comm) ⟩

      (Σ Type λ C → Σ (El a C) λ x →
         Σ (Is-set C) λ S → proj₁ (P (C , S) x))    ↝⟨ Σ-assoc ⟩□

      (Σ (Σ Type (El a)) λ { (C , x) →
         Σ (Is-set C) λ S → proj₁ (P (C , S) x) })  □

    prop : Is-proposition
             (Σ (Is-set C₂) λ S₂ → proj₁ (P (C₂ , S₂) x₂))
    prop =
      Σ-closure 1
        (H-level-propositional (Assumptions.ext₀ ass) 2)
        (λ S₂ → proj₂ (P (C₂ , S₂) x₂) ass)

  -- Structure isomorphisms.

  Isomorphic : ∀ c → Instance c → Instance c → Type₁
  Isomorphic (a , _) ((C₁ , _) , x₁ , _) ((C₂ , _) , x₂ , _) =
    Σ (C₁ ↔ C₂) λ C₁↔C₂ → Is-isomorphism a C₁↔C₂ x₁ x₂

  abstract

    -- The type of isomorphisms between two instances of a structure
    -- is isomorphic to the type of equalities between the same
    -- instances (assuming univalence).
    --
    -- In short, isomorphism is isomorphic to equality.

    isomorphic↔equal :
      Assumptions →
      ∀ c {I₁ I₂} → Isomorphic c I₁ I₂ ↔ (I₁ ≡ I₂)
    isomorphic↔equal ass c {I₁} {I₂} =

      (∃ λ (C-eq : Carrier c I₁ ↔ Carrier c I₂) →
         Is-isomorphism (proj₁ c) C-eq (element c I₁) (element c I₂))    ↝⟨ ∃-cong (λ C-eq → isomorphism-definitions-isomorphic₂
                                                                                ass (proj₁ c) C-eq) ⟩
      (∃ λ (C-eq : Carrier c I₁ ↔ Carrier c I₂) →
         subst (El (proj₁ c)) (≃⇒≡ univ (Eq.↔⇒≃ C-eq)) (element c I₁) ≡
         element c I₂)                                                   ↝⟨ Σ-cong (Eq.↔↔≃ ext₀ (proj₂ (proj₁ I₁))) (λ _ → _ □) ⟩

      (∃ λ (C-eq : Carrier c I₁ ≃ Carrier c I₂) →
         subst (El (proj₁ c)) (≃⇒≡ univ C-eq) (element c I₁) ≡
         element c I₂)                                                   ↝⟨ inverse $
                                                                              Σ-cong (≡≃≃ univ) (λ C-eq → ≡⇒↝ _ $ sym $
                                                                                cong (λ eq → subst (El (proj₁ c)) eq (element c I₁) ≡
                                                                                element c I₂)
                                                                                (_≃_.left-inverse-of (≡≃≃ univ) C-eq)) ⟩
      (∃ λ (C-eq : Carrier c I₁ ≡ Carrier c I₂) →
         subst (El (proj₁ c)) C-eq (element c I₁) ≡ element c I₂)        ↝⟨ inverse $ instances-equal↔ ass c ⟩□

      (I₁ ≡ I₂)                                                          □

      where open Assumptions ass

    -- The first part of the from component of the preceding lemma is
    -- extensionally equal to a simple function. (The codomain of the
    -- second part is propositional whenever El (proj₁ c) applied to
    -- either carrier type is a set.)

    proj₁-from-isomorphic↔equal :
      ∀ ass c {I J} (I≡J : I ≡ J) →
      proj₁ (_↔_.from (isomorphic↔equal ass c) I≡J) ≡
      _≃_.bijection (≡⇒≃ (cong (proj₁ ∘ proj₁) I≡J))
    proj₁-from-isomorphic↔equal ass (a , P) I≡J =
      let A = Instance (a , P)
          B = Σ (∃ (El a)) λ { (C , x) →
                ∃ λ (S : Is-set C) → proj₁ (P (C , S) x) }
      in

      cong (_≃_.bijection ∘ ≡⇒≃) (
        proj₁ (Σ-≡,≡←≡ (proj₁ (Σ-≡,≡←≡ (cong {B = B}
          (λ { ((C , S) , x , p) → (C , x) , S , p }) I≡J))))            ≡⟨ cong (proj₁ ∘ Σ-≡,≡←≡) $ proj₁-Σ-≡,≡←≡ _ ⟩
        proj₁ (Σ-≡,≡←≡ (cong proj₁ (cong {B = B}
          (λ { ((C , S) , x , p) → (C , x) , S , p }) I≡J)))             ≡⟨ cong (proj₁ ∘ Σ-≡,≡←≡) $
                                                                              cong-∘ {B = B} proj₁
                                                                                (λ { ((C , S) , x , p) → (C , x) , S , p }) _ ⟩
        proj₁ (Σ-≡,≡←≡ (cong {A = A}
          (λ { ((C , S) , x , p) → C , x }) I≡J))                        ≡⟨ proj₁-Σ-≡,≡←≡ _ ⟩
        cong proj₁ (cong {A = A} (λ { ((C , S) , x , p) → C , x }) I≡J)  ≡⟨ cong-∘ {A = A} proj₁ (λ { ((C , S) , x , p) → C , x }) _ ⟩∎
        cong (proj₁ ∘ proj₁) I≡J                                         ∎)

    -- The type of (lifted) isomorphisms between two instances of a
    -- structure is equal to the type of equalities between the same
    -- instances (assuming univalence).
    --
    -- In short, isomorphism is equal to equality.

    isomorphic≡equal :
      Assumptions →
      ∀ c {I₁ I₂} → Isomorphic c I₁ I₂ ≡ (I₁ ≡ I₂)
    isomorphic≡equal ass c {I₁} {I₂} =
      ≃⇒≡ univ₁ $ Eq.↔⇒≃ (isomorphic↔equal ass c)
      where open Assumptions ass

------------------------------------------------------------------------
-- A universe of non-recursive, simple types

-- Codes for types.

infixr 20 _⊗_
infixr 15 _⊕_
infixr 10 _⇾_

data U : Type₁ where
  id prop     : U
  k           : Type → U
  _⇾_ _⊕_ _⊗_ : U → U → U

-- Interpretation of types.

El : U → Type₁ → Type₁
El id      B = B
El prop    B = Proposition (# 0)
El (k A)   B = ↑ _ A
El (a ⇾ b) B = El a B → El b B
El (a ⊕ b) B = El a B ⊎ El b B
El (a ⊗ b) B = El a B × El b B

-- El a preserves equivalences (assuming extensionality).

cast : Extensionality (# 1) (# 1) →
       ∀ a {B C} → B ≃ C → El a B ≃ El a C
cast ext id      B≃C = B≃C
cast ext prop    B≃C = Eq.id
cast ext (k A)   B≃C = Eq.id
cast ext (a ⇾ b) B≃C = →-cong ext (cast ext a B≃C) (cast ext b B≃C)
cast ext (a ⊕ b) B≃C = cast ext a B≃C ⊎-cong cast ext b B≃C
cast ext (a ⊗ b) B≃C = cast ext a B≃C ×-cong cast ext b B≃C

abstract

  -- The cast function respects identities (assuming extensionality).

  cast-id : (ext : Extensionality (# 1) (# 1)) →
            ∀ a {B} → cast ext a (Eq.id {A = B}) ≡ Eq.id
  cast-id ext id      = refl _
  cast-id ext prop    = refl _
  cast-id ext (k A)   = refl _
  cast-id ext (a ⇾ b) = Eq.lift-equality ext $ cong _≃_.to $
                          cong₂ (→-cong ext) (cast-id ext a) (cast-id ext b)
  cast-id ext (a ⊗ b) = Eq.lift-equality ext $ cong _≃_.to $
                          cong₂ _×-cong_ (cast-id ext a) (cast-id ext b)
  cast-id ext (a ⊕ b) =
    cast ext a Eq.id ⊎-cong cast ext b Eq.id  ≡⟨ cong₂ _⊎-cong_ (cast-id ext a) (cast-id ext b) ⟩
    Eq.⟨ [ inj₁ , inj₂ ] , _ ⟩                ≡⟨ Eq.lift-equality ext (apply-ext ext [ refl ∘ inj₁ , refl ∘ inj₂ ]) ⟩∎
    Eq.id                                     ∎

-- The property of being an isomorphism between two elements.

Is-isomorphism : ∀ a {B C} → B ↔ C → El a B → El a C → Type₁
Is-isomorphism id      B↔C = λ x y → _↔_.to B↔C x ≡ y
Is-isomorphism prop    B↔C = λ { (P , _) (Q , _) → ↑ _ (P ⇔ Q) }
Is-isomorphism (k A)   B↔C = λ x y → x ≡ y
Is-isomorphism (a ⇾ b) B↔C = Is-isomorphism a B↔C →-rel
                             Is-isomorphism b B↔C
Is-isomorphism (a ⊕ b) B↔C = Is-isomorphism a B↔C ⊎-rel
                             Is-isomorphism b B↔C
Is-isomorphism (a ⊗ b) B↔C = Is-isomorphism a B↔C ×-rel
                             Is-isomorphism b B↔C

-- Another definition of "being an isomorphism" (defined using
-- extensionality).

Is-isomorphism′ : Extensionality (# 1) (# 1) →
                  ∀ a {B C} → B ↔ C → El a B → El a C → Type₁
Is-isomorphism′ ext a B↔C x y = _≃_.to (cast ext a (Eq.↔⇒≃ B↔C)) x ≡ y

abstract

  -- The two definitions of "being an isomorphism" are "isomorphic"
  -- (in bijective correspondence), assuming univalence.

  isomorphism-definitions-isomorphic :
    (ass : Assumptions) → let open Assumptions ass in
    ∀ a {B C} (B↔C : B ↔ C) {x y} →
    Is-isomorphism a B↔C x y ↔ Is-isomorphism′ ext a B↔C x y

  isomorphism-definitions-isomorphic ass id B↔C {x} {y} =

    (_↔_.to B↔C x ≡ y)  □

  isomorphism-definitions-isomorphic ass prop B↔C {P} {Q} =

    ↑ _ (proj₁ P ⇔ proj₁ Q)  ↝⟨ B.↑↔ ⟩

    (proj₁ P ⇔ proj₁ Q)      ↝⟨ Eq.⇔↔≃ ext₀ (proj₂ P) (proj₂ Q) ⟩

    (proj₁ P ≃ proj₁ Q)      ↔⟨ inverse $ ≡≃≃ univ ⟩

    (proj₁ P ≡ proj₁ Q)      ↝⟨ ignore-propositional-component (H-level-propositional ext₀ 1) ⟩□

    (P ≡ Q)                □

    where open Assumptions ass

  isomorphism-definitions-isomorphic ass (k A) B↔C {x} {y} =

    (x ≡ y) □

  isomorphism-definitions-isomorphic ass (a ⇾ b) B↔C {f} {g} =
    let B≃C = Eq.↔⇒≃ B↔C in

    (∀ x y → Is-isomorphism a B↔C x y →
             Is-isomorphism b B↔C (f x) (g y))                     ↝⟨ ∀-cong ext (λ _ → ∀-cong ext λ _ →
                                                                        →-cong ext (isomorphism-definitions-isomorphic ass a B↔C)
                                                                                (isomorphism-definitions-isomorphic ass b B↔C)) ⟩
    (∀ x y → to (cast ext a B≃C) x ≡ y →
             to (cast ext b B≃C) (f x) ≡ g y)                      ↝⟨ inverse $ ∀-cong ext (λ x →
                                                                        ∀-intro (λ y _ → to (cast ext b B≃C) (f x) ≡ g y) ext) ⟩
    (∀ x → to (cast ext b B≃C) (f x) ≡ g (to (cast ext a B≃C) x))  ↔⟨ Eq.extensionality-isomorphism ext ⟩

    (to (cast ext b B≃C) ∘ f ≡ g ∘ to (cast ext a B≃C))            ↝⟨ inverse $ ∘from≡↔≡∘to ext (cast ext a B≃C) ⟩□

    (to (cast ext b B≃C) ∘ f ∘ from (cast ext a B≃C) ≡ g)          □

    where
    open _≃_
    open Assumptions ass

  isomorphism-definitions-isomorphic ass (a ⊕ b) B↔C {inj₁ x} {inj₁ y} =
    let B≃C = Eq.↔⇒≃ B↔C in

    Is-isomorphism a B↔C x y                 ↝⟨ isomorphism-definitions-isomorphic ass a B↔C ⟩

    (to (cast ext a B≃C) x ≡ y)              ↝⟨ B.≡↔inj₁≡inj₁ ⟩□

    (inj₁ (to (cast ext a B≃C) x) ≡ inj₁ y)  □

    where
    open _≃_
    open Assumptions ass

  isomorphism-definitions-isomorphic ass (a ⊕ b) B↔C {inj₂ x} {inj₂ y} =
    let B≃C = Eq.↔⇒≃ B↔C in

    Is-isomorphism b B↔C x y                 ↝⟨ isomorphism-definitions-isomorphic ass b B↔C ⟩

    (to (cast ext b B≃C) x ≡ y)              ↝⟨ B.≡↔inj₂≡inj₂ ⟩□

    (inj₂ (to (cast ext b B≃C) x) ≡ inj₂ y)  □

    where
    open _≃_
    open Assumptions ass

  isomorphism-definitions-isomorphic ass (a ⊕ b) B↔C {inj₁ x} {inj₂ y} =

    ⊥                  ↝⟨ B.⊥↔uninhabited ⊎.inj₁≢inj₂ ⟩□

    (inj₁ _ ≡ inj₂ _)  □

  isomorphism-definitions-isomorphic ass (a ⊕ b) B↔C {inj₂ x} {inj₁ y} =

    ⊥                  ↝⟨ B.⊥↔uninhabited (⊎.inj₁≢inj₂ ∘ sym) ⟩□

    (inj₂ _ ≡ inj₁ _)  □

  isomorphism-definitions-isomorphic ass (a ⊗ b) B↔C {x , u} {y , v} =
    let B≃C = Eq.↔⇒≃ B↔C in

    Is-isomorphism  a B↔C x y × Is-isomorphism  b B↔C u v        ↝⟨ isomorphism-definitions-isomorphic ass a B↔C ×-cong
                                                                    isomorphism-definitions-isomorphic ass b B↔C ⟩
    (to (cast ext a B≃C) x ≡ y × to (cast ext b B≃C) u ≡ v)      ↝⟨ ≡×≡↔≡ ⟩□

    ((to (cast ext a B≃C) x , to (cast ext b B≃C) u) ≡ (y , v))  □

    where
    open _≃_
    open Assumptions ass

-- The universe above is a "universe with some extra stuff".

simple : Universe
simple = record
  { U              = U
  ; El             = λ a → El a ∘ ↑ _
  ; Is-isomorphism = λ a B↔C → Is-isomorphism a (↑-cong B↔C)
  ; resp           = λ ass a → _≃_.to ∘ cast (ext ass) a ∘ ↑-cong
  ; resp-id        = λ ass a x → cong (λ f → _≃_.to f x) (
                       cast (ext ass) a (↑-cong Eq.id)  ≡⟨ cong (cast (ext ass) a) $ Eq.lift-equality (ext ass) (refl _) ⟩
                       cast (ext ass) a Eq.id           ≡⟨ cast-id (ext ass) a ⟩∎
                       Eq.id                            ∎)
  ; isomorphism-definitions-isomorphic = λ ass a B↔C {x y} →
      Is-isomorphism a (↑-cong B↔C) x y                        ↝⟨ isomorphism-definitions-isomorphic ass a (↑-cong B↔C) ⟩
      (_≃_.to (cast (ext ass) a (Eq.↔⇒≃ (↑-cong B↔C))) x ≡ y)  ↝⟨ ≡⇒↝ _ $ cong (λ eq → _≃_.to (cast (ext ass) a eq) x ≡ y) $
                                                                    Eq.lift-equality (ext ass) (refl _) ⟩□
      (_≃_.to (cast (ext ass) a (↑-cong (Eq.↔⇒≃ B↔C))) x ≡ y)  □
  }
  where open Assumptions

-- Let us use this universe in the examples below.

open Class simple

------------------------------------------------------------------------
-- An example: monoids

monoid : Code
monoid =
  -- Binary operation.
  (id ⇾ id ⇾ id) ⊗

  -- Identity.
  id ,

  λ { (_ , M-set) (_∙_ , e) →

      (-- Left and right identity laws.
       (∀ x → (e ∙ x) ≡ x) ×
       (∀ x → (x ∙ e) ≡ x) ×

       -- Associativity.
       (∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z))) ,

       -- The laws are propositional (assuming extensionality).
      λ ass → let open Assumptions ass in
        ×-closure 1  (Π-closure ext 1 λ _ →
                      ↑-closure 2 M-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      ↑-closure 2 M-set)
                     (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 M-set)) }

-- The interpretation of the code is reasonable.

Instance-monoid :

  Instance monoid
    ≡
  Σ (Set (# 0)) λ { (M , _) →
  Σ ((↑ _ M → ↑ _ M → ↑ _ M) × ↑ _ M) λ { (_∙_ , e) →
  (∀ x → (e ∙ x) ≡ x) ×
  (∀ x → (x ∙ e) ≡ x) ×
  (∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z)) }}

Instance-monoid = refl _

-- The notion of isomorphism that we get is also reasonable.

Isomorphic-monoid :
  ∀ {M₁} {S₁ : Is-set M₁} {_∙₁_ e₁ laws₁}
    {M₂} {S₂ : Is-set M₂} {_∙₂_ e₂ laws₂} →

  Isomorphic monoid ((M₁ , S₁) , (_∙₁_ , e₁) , laws₁)
                    ((M₂ , S₂) , (_∙₂_ , e₂) , laws₂)
    ≡
  Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
  (∀ x y → to x ≡ y → ∀ u v → to u ≡ v → to (x ∙₁ u) ≡ (y ∙₂ v)) ×
  to e₁ ≡ e₂

Isomorphic-monoid = refl _

-- Note that this definition of isomorphism is isomorphic to a more
-- standard one (assuming extensionality).

Isomorphism-monoid-isomorphic-to-standard :
  Extensionality (# 1) (# 1) →
  ∀ {M₁} {S₁ : Is-set M₁} {_∙₁_ e₁ laws₁}
    {M₂} {S₂ : Is-set M₂} {_∙₂_ e₂ laws₂} →

  Isomorphic monoid ((M₁ , S₁) , (_∙₁_ , e₁) , laws₁)
                    ((M₂ , S₂) , (_∙₂_ , e₂) , laws₂)
    ↔
  Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
  (∀ x y → to (x ∙₁ y) ≡ (to x ∙₂ to y)) ×
  to e₁ ≡ e₂

Isomorphism-monoid-isomorphic-to-standard ext
  {M₁} {S₁} {_∙₁_} {e₁} {M₂ = M₂} {_∙₂_ = _∙₂_} {e₂} =

  (Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
   (∀ x y → to x ≡ y → ∀ u v → to u ≡ v → to (x ∙₁ u) ≡ (y ∙₂ v)) ×
   to e₁ ≡ e₂)                                                       ↝⟨ inverse $ ∃-cong (λ _ →
                                                                          (∀-cong ext λ _ → ∀-intro (λ _ _ → _) ext) ×-cong (_ □)) ⟩
  (Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
   (∀ x u v → to u ≡ v → to (x ∙₁ u) ≡ (to x ∙₂ v)) ×
   to e₁ ≡ e₂)                                                       ↝⟨ inverse $ ∃-cong (λ _ →
                                                                          (∀-cong ext λ _ → ∀-cong ext λ _ → ∀-intro (λ _ _ → _) ext)
                                                                            ×-cong
                                                                          (_ □)) ⟩□
  (Σ (M₁ ↔ M₂) λ M₁↔M₂ → let open _↔_ (↑-cong M₁↔M₂) in
   (∀ x u → to (x ∙₁ u) ≡ (to x ∙₂ to u)) ×
   to e₁ ≡ e₂)                                                       □

------------------------------------------------------------------------
-- An example: posets

poset : Code
poset =
  -- The ordering relation.
  (id ⇾ id ⇾ prop) ,

  λ { (P , P-set) Le →

    let _≤_ : ↑ _ P → ↑ _ P → Type
        _≤_ x y = proj₁ (Le x y)
    in

     -- Reflexivity.
    ((∀ x → x ≤ x) ×

     -- Transitivity.
     (∀ x y z → x ≤ y → y ≤ z → x ≤ z) ×

     -- Antisymmetry.
     (∀ x y → x ≤ y → y ≤ x → x ≡ y)) ,

    λ ass → let open Assumptions ass in
      ×-closure 1  (Π-closure (lower-ext (# 0) _ ext) 1 λ _ →
                    proj₂ (Le _ _))
      (×-closure 1 (Π-closure ext                     1 λ _ →
                    Π-closure ext                     1 λ _ →
                    Π-closure (lower-ext (# 0) _ ext) 1 λ _ →
                    Π-closure ext₀                    1 λ _ →
                    Π-closure ext₀                    1 λ _ →
                    proj₂ (Le _ _))
                   (Π-closure ext                     1 λ _ →
                    Π-closure ext                     1 λ _ →
                    Π-closure (lower-ext _ (# 0) ext) 1 λ _ →
                    Π-closure (lower-ext _ (# 0) ext) 1 λ _ →
                    ↑-closure 2 P-set)) }

-- The interpretation of the code is reasonable.

Instance-poset :

  Instance poset
    ≡
  Σ (Set (# 0)) λ { (P , _) →
  Σ (↑ _ P → ↑ _ P → Proposition (# 0)) λ Le →
  let _≤_ : ↑ _ P → ↑ _ P → Type
      _≤_ x y = proj₁ (Le x y)
  in
  (∀ x → x ≤ x) ×
  (∀ x y z → x ≤ y → y ≤ z → x ≤ z) ×
  (∀ x y → x ≤ y → y ≤ x → x ≡ y) }

Instance-poset = refl _

-- The notion of isomorphism that we get is also reasonable. It is the
-- usual notion of "order isomorphism".

Isomorphic-poset :
  ∀ {P₁} {S₁ : Is-set P₁} {Le₁ laws₁}
    {P₂} {S₂ : Is-set P₂} {Le₂ laws₂} →
  let _≤₁_ : ↑ _ P₁ → ↑ _ P₁ → Type
      _≤₁_ x y = proj₁ (Le₁ x y)

      _≤₂_ : ↑ _ P₂ → ↑ _ P₂ → Type
      _≤₂_ x y = proj₁ (Le₂ x y)
  in

  Isomorphic poset ((P₁ , S₁) , Le₁ , laws₁) ((P₂ , S₂) , Le₂ , laws₂)
    ≡
  Σ (P₁ ↔ P₂) λ P₁↔P₂ → let open _↔_ (↑-cong P₁↔P₂) in
  ∀ a b → to a ≡ b → ∀ c d → to c ≡ d → ↑ _ ((a ≤₁ c) ⇔ (b ≤₂ d))

Isomorphic-poset = refl _

------------------------------------------------------------------------
-- An example: discrete fields

-- Discrete fields.

discrete-field : Code
discrete-field =
  -- Addition.
  (id ⇾ id ⇾ id) ⊗

  -- Zero.
  id ⊗

  -- Multiplication.
  (id ⇾ id ⇾ id) ⊗

  -- One.
  id ⊗

  -- Minus.
  (id ⇾ id) ⊗

  -- Multiplicative inverse (a partial operation).
  (id ⇾ k ⊤ ⊕ id) ,

  λ { (_ , F-set) (_+_ , 0# , _*_ , 1# , -_ , _⁻¹) →

       -- Associativity.
      ((∀ x y z → (x + (y + z)) ≡ ((x + y) + z)) ×
       (∀ x y z → (x * (y * z)) ≡ ((x * y) * z)) ×

       -- Commutativity.
       (∀ x y → (x + y) ≡ (y + x)) ×
       (∀ x y → (x * y) ≡ (y * x)) ×

       -- Distributivity.
       (∀ x y z → (x * (y + z)) ≡ ((x * y) + (x * z))) ×

       -- Identity laws.
       (∀ x → (x + 0#) ≡ x) ×
       (∀ x → (x * 1#) ≡ x) ×

       -- Zero and one are distinct.
       0# ≢ 1# ×

       -- Inverse laws.
       (∀ x → (x + (- x)) ≡ 0#) ×
       (∀ x → (x ⁻¹) ≡ inj₁ (lift tt) → x ≡ 0#) ×
       (∀ x y → (x ⁻¹) ≡ inj₂ y → (x * y) ≡ 1#)) ,

      λ ass → let open Assumptions ass in
        ×-closure 1  (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
        (×-closure 1 (Π-closure (lower-ext (# 0) (# 1) ext) 1 λ _ →
                      ⊥-propositional)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)
                     (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 F-set)))))))))) }

-- The interpretation of the code is reasonable.

Instance-discrete-field :

  Instance discrete-field
    ≡
  Σ (Set (# 0)) λ { (F , _) →
  Σ ((↑ _ F → ↑ _ F → ↑ _ F) × ↑ _ F × (↑ _ F → ↑ _ F → ↑ _ F) ×
     ↑ _ F × (↑ _ F → ↑ _ F) × (↑ _ F → ↑ (# 1) ⊤ ⊎ ↑ _ F))
    λ { (_+_ , 0# , _*_ , 1# , -_ , _⁻¹) →
  (∀ x y z → (x + (y + z)) ≡ ((x + y) + z)) ×
  (∀ x y z → (x * (y * z)) ≡ ((x * y) * z)) ×
  (∀ x y → (x + y) ≡ (y + x)) ×
  (∀ x y → (x * y) ≡ (y * x)) ×
  (∀ x y z → (x * (y + z)) ≡ ((x * y) + (x * z))) ×
  (∀ x → (x + 0#) ≡ x) ×
  (∀ x → (x * 1#) ≡ x) ×
  0# ≢ 1# ×
  (∀ x → (x + (- x)) ≡ 0#) ×
  (∀ x → (x ⁻¹) ≡ inj₁ (lift tt) → x ≡ 0#) ×
  (∀ x y → (x ⁻¹) ≡ inj₂ y → (x * y) ≡ 1#) }}

Instance-discrete-field = refl _

-- The notion of isomorphism that we get is also reasonable.

Isomorphic-discrete-field :
  ∀ {F₁} {S₁ : Is-set F₁} {_+₁_ 0₁ _*₁_ 1₁ -₁_ _⁻¹₁ laws₁}
    {F₂} {S₂ : Is-set F₂} {_+₂_ 0₂ _*₂_ 1₂ -₂_ _⁻¹₂ laws₂} →

  Isomorphic discrete-field
    ((F₁ , S₁) , (_+₁_ , 0₁ , _*₁_ , 1₁ , -₁_ , _⁻¹₁) , laws₁)
    ((F₂ , S₂) , (_+₂_ , 0₂ , _*₂_ , 1₂ , -₂_ , _⁻¹₂) , laws₂)
    ≡
  Σ (F₁ ↔ F₂) λ F₁↔F₂ → let open _↔_ (↑-cong F₁↔F₂) in
  (∀ x y → to x ≡ y → ∀ u v → to u ≡ v → to (x +₁ u) ≡ (y +₂ v)) ×
  to 0₁ ≡ 0₂ ×
  (∀ x y → to x ≡ y → ∀ u v → to u ≡ v → to (x *₁ u) ≡ (y *₂ v)) ×
  to 1₁ ≡ 1₂ ×
  (∀ x y → to x ≡ y → to (-₁ x) ≡ (-₂ y)) ×
  (∀ x y → to x ≡ y →
     ((λ _ _ → lift tt ≡ lift tt) ⊎-rel (λ u v → to u ≡ v))
       (x ⁻¹₁) (y ⁻¹₂))

Isomorphic-discrete-field = refl _

------------------------------------------------------------------------
-- An example: vector spaces over discrete fields

-- Vector spaces over a particular discrete field.

vector-space : Instance discrete-field → Code
vector-space ((F , _) , (_+F_ , _ , _*F_ , 1F , _ , _) , _) =
  -- Addition.
  (id ⇾ id ⇾ id) ⊗

  -- Scalar multiplication.
  (k F ⇾ id ⇾ id) ⊗

  -- Zero vector.
  id ⊗

  -- Additive inverse.
  (id ⇾ id) ,

  λ { (_ , V-set) (_+_ , _*_ , 0V , -_) →

       -- Associativity.
      ((∀ u v w → (u + (v + w)) ≡ ((u + v) + w)) ×
       (∀ x y v → (x * (y * v)) ≡ ((x *F y) * v)) ×

       -- Commutativity.
       (∀ u v → (u + v) ≡ (v + u)) ×

       -- Distributivity.
       (∀ x u v → (x * (u + v)) ≡ ((x * u) + (x * v))) ×
       (∀ x y v → ((x +F y) * v) ≡ ((x * v) + (y * v))) ×

       -- Identity laws.
       (∀ v → (v + 0V) ≡ v) ×
       (∀ v → (1F * v) ≡ v) ×

       -- Inverse law.
       (∀ v → (v + (- v)) ≡ 0V)) ,

      λ ass → let open Assumptions ass in
        ×-closure 1  (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 V-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 V-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 V-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 V-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      Π-closure ext 1 λ _ →
                      ↑-closure 2 V-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      ↑-closure 2 V-set)
        (×-closure 1 (Π-closure ext 1 λ _ →
                      ↑-closure 2 V-set)
                     (Π-closure ext 1 λ _ →
                      ↑-closure 2 V-set))))))) }

-- The interpretation of the code is reasonable.

Instance-vector-space :
  ∀ {F} {S : Is-set F} {_+F_ 0F _*F_ 1F -F_ _⁻¹F laws} →

  Instance (vector-space
              ((F , S) , (_+F_ , 0F , _*F_ , 1F , -F_ , _⁻¹F) , laws))
    ≡
  Σ (Set (# 0)) λ { (V , _) →
  Σ ((↑ _ V → ↑ _ V → ↑ _ V) × (↑ _ F → ↑ _ V → ↑ _ V) × ↑ _ V ×
     (↑ _ V → ↑ _ V))
    λ { (_+_ , _*_ , 0V , -_) →
  (∀ u v w → (u + (v + w)) ≡ ((u + v) + w)) ×
  (∀ x y v → (x * (y * v)) ≡ ((x *F y) * v)) ×
  (∀ u v → (u + v) ≡ (v + u)) ×
  (∀ x u v → (x * (u + v)) ≡ ((x * u) + (x * v))) ×
  (∀ x y v → ((x +F y) * v) ≡ ((x * v) + (y * v))) ×
  (∀ v → (v + 0V) ≡ v) ×
  (∀ v → (1F * v) ≡ v) ×
  (∀ v → (v + (- v)) ≡ 0V) }}

Instance-vector-space = refl _

-- The notion of isomorphism that we get is also reasonable.

Isomorphic-vector-space :
  ∀ {F V₁} {S₁ : Is-set V₁} {_+₁_ _*₁_ 0₁ -₁_ laws₁}
      {V₂} {S₂ : Is-set V₂} {_+₂_ _*₂_ 0₂ -₂_ laws₂} →

  Isomorphic (vector-space F)
             ((V₁ , S₁) , (_+₁_ , _*₁_ , 0₁ , -₁_) , laws₁)
             ((V₂ , S₂) , (_+₂_ , _*₂_ , 0₂ , -₂_) , laws₂)
    ≡
  Σ (V₁ ↔ V₂) λ V₁↔V₂ → let open _↔_ (↑-cong V₁↔V₂) in
  (∀ a b → to a ≡ b → ∀ u v → to u ≡ v → to (a +₁ u) ≡ (b +₂ v)) ×
  (∀ x y →    x ≡ y → ∀ u v → to u ≡ v → to (x *₁ u) ≡ (y *₂ v)) ×
  to 0₁ ≡ 0₂ ×
  (∀ u v → to u ≡ v → to (-₁ u) ≡ (-₂ v))

Isomorphic-vector-space = refl _

------------------------------------------------------------------------
-- An example: sets equipped with fixpoint operators

set-with-fixpoint-operator : Code
set-with-fixpoint-operator =
  (id ⇾ id) ⇾ id ,

  λ { (_ , F-set) fix →

     -- The fixpoint operator property.
    (∀ f → f (fix f) ≡ fix f) ,

    λ ass → let open Assumptions ass in
      Π-closure ext 1 λ _ →
      ↑-closure 2 F-set }

-- The usual unfolding lemmas.

Instance-set-with-fixpoint-operator :

  Instance set-with-fixpoint-operator
    ≡
  Σ (Set (# 0)) λ { (F , _) →
  Σ ((↑ _ F → ↑ _ F) → ↑ _ F) λ fix →
  ∀ f → f (fix f) ≡ fix f }

Instance-set-with-fixpoint-operator = refl _

Isomorphic-set-with-fixpoint-operator :
  ∀ {F₁} {S₁ : Is-set F₁} {fix₁ law₁}
    {F₂} {S₂ : Is-set F₂} {fix₂ law₂} →

  Isomorphic set-with-fixpoint-operator
             ((F₁ , S₁) , fix₁ , law₁) ((F₂ , S₂) , fix₂ , law₂)
    ≡
  Σ (F₁ ↔ F₂) λ F₁↔F₂ → let open _↔_ (↑-cong F₁↔F₂) in
  ∀ f g → (∀ x y → to x ≡ y → to (f x) ≡ g y) → to (fix₁ f) ≡ fix₂ g

Isomorphic-set-with-fixpoint-operator = refl _

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module LogicalFramework.Existential where

module LF where
  postulate
    D : Set

    -- Disjunction.
    _∨_  : Set → Set → Set
    inj₁ : {A B : Set} → A → A ∨ B
    inj₂ : {A B : Set} → B → A ∨ B
    case : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C

    -- The existential quantifier type on D.
    ∃       : (A : D → Set) → Set
    _,_     : {A : D → Set}(t : D) → A t → ∃ A
    ∃-proj₁ : {A : D → Set} → ∃ A → D
    ∃-proj₂ : {A : D → Set}(h : ∃ A) → A (∃-proj₁ h)
    ∃-elim  : {A : D → Set}{B : Set} → ∃ A → (∀ {x} → A x → B) → B

  syntax ∃ (λ x → e) = ∃[ x ] e

  module FOL-Examples where
    -- Using the projections.
    ∃∀₁ : {A : D → D → Set} → ∃[ x ](∀ y → A x y) → ∀ y → ∃[ x ] A x y
    ∃∀₁ h y = ∃-proj₁ h , (∃-proj₂ h) y

    ∃∨₁ : {A B : D → Set} → ∃[ x ](A x ∨ B x) → (∃[ x ] A x) ∨ (∃[ x ] B x)
    ∃∨₁ h = case (λ Ax → inj₁ (∃-proj₁ h , Ax))
                 (λ Bx → inj₂ (∃-proj₁ h , Bx))
                 (∃-proj₂ h)

    -- Using the elimination.
    ∃∀₂ : {A : D → D → Set} → ∃[ x ](∀ y → A x y) → ∀ y → ∃[ x ] A x y
    ∃∀₂ h y = ∃-elim h (λ {x} ah → x , ah y)

    ∃∨₂ : {A B : D → Set} → ∃[ x ](A x ∨ B x) → (∃[ x ] A x) ∨ (∃[ x ] B x)
    ∃∨₂ h = ∃-elim h (λ {x} ah → case (λ Ax → inj₁ (x , Ax))
                                      (λ Bx → inj₂ (x , Bx))
                                      ah)

  module NonFOL-Examples where

    -- Using the projections.
    non-FOL₁ : {A : D → Set} → ∃ A → D
    non-FOL₁ h = ∃-proj₁ h

    -- Using the elimination.
    non-FOL₂ : {A : D → Set} → ∃ A → D
    non-FOL₂ h = ∃-elim h (λ {x} _ → x)

module Inductive where

  open import Common.FOL.FOL

  -- The existential proyections.
  ∃-proj₁ : ∀ {A} → ∃ A → D
  ∃-proj₁ (x , _) = x

  ∃-proj₂ : ∀ {A} → (h : ∃ A) → A (∃-proj₁ h)
  ∃-proj₂ (_ , Ax) = Ax

  -- The existential elimination.
  ∃-elim : {A : D → Set}{B : Set} → ∃ A → (∀ {x} → A x → B) → B
  ∃-elim (_ , Ax) h = h Ax

  module FOL-Examples where
    -- Using the projections.
    ∃∀₁ : {A : D → D → Set} → ∃[ x ](∀ y → A x y) → ∀ y → ∃[ x ] A x y
    ∃∀₁ h y = ∃-proj₁ h , (∃-proj₂ h) y

    ∃∨₁ : {A B : D → Set} → ∃[ x ](A x ∨ B x) → (∃[ x ] A x) ∨ (∃[ x ] B x)
    ∃∨₁ h = case (λ Ax → inj₁ (∃-proj₁ h , Ax))
                 (λ Bx → inj₂ (∃-proj₁ h , Bx))
                 (∃-proj₂ h)

    -- Using the elimination.
    ∃∀₂ : {A : D → D → Set} → ∃[ x ](∀ y → A x y) → ∀ y → ∃[ x ] A x y
    ∃∀₂ h y = ∃-elim h (λ {x} ah → x , ah y)

    ∃∨₂ : {A B : D → Set} → ∃[ x ](A x ∨ B x) → (∃[ x ] A x) ∨ (∃[ x ] B x)
    ∃∨₂ h = ∃-elim h (λ {x} ah → case (λ Ax → inj₁ (x , Ax))
                                      (λ Bx → inj₂ (x , Bx))
                                      ah)

    -- Using pattern matching.
    ∃∀₃ : {A : D → D → Set} → ∃[ x ](∀ y → A x y) → ∀ y → ∃[ x ] A x y
    ∃∀₃ (x , Ax) y = x , Ax y

    ∃∨₃ : {A B : D → Set} → ∃[ x ](A x ∨ B x) → (∃[ x ] A x) ∨ (∃[ x ] B x)
    ∃∨₃ (x , inj₁ Ax) = inj₁ (x , Ax)
    ∃∨₃ (x , inj₂ Bx) = inj₂ (x , Bx)

  module NonFOL-Examples where

    -- Using the projections.
    non-FOL₁ : {A : D → Set} → ∃ A → D
    non-FOL₁ h = ∃-proj₁ h

    -- Using the elimination.
    non-FOL₂ : {A : D → Set} → ∃ A → D
    non-FOL₂ h = ∃-elim h (λ {x} _ → x)

    -- Using the pattern matching.
    non-FOL₃ : {A : D → Set} → ∃ A → D
    non-FOL₃ (x , _) = x


text:
module Prelude where

open import Agda.Primitive public
  using (_⊔_)
  renaming (lsuc to ↑_)

-- Built-in implication.

id : ∀ {ℓ} {X : Set ℓ} → X → X
id x = x

const : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → X → Y → X
const x y = x

flip : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
       (X → Y → Z) → Y → X → Z
flip P y x = P x y

ap : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
     (X → Y → Z) → (X → Y) → X → Z
ap f g x = f x (g x)

infixr 9 _∘_
_∘_ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
      (Y → Z) → (X → Y) → X → Z
f ∘ g = λ x → f (g x)

refl→ : ∀ {ℓ} {X : Set ℓ} → X → X
refl→ = id

trans→ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
          (X → Y) → (Y → Z) → X → Z
trans→ = flip _∘_

-- Built-in verum.

open import Agda.Builtin.Unit public
  using (⊤)
  renaming (tt to ∙)

-- Falsum.

data ⊥ : Set where

{-# HASKELL data AgdaEmpty #-}
{-# COMPILED_DATA ⊥ MAlonzo.Code.Data.Empty.AgdaEmpty #-}

elim⊥ : ∀ {ℓ} {X : Set ℓ} → ⊥ → X
elim⊥ ()

-- Negation.

infix 3 ¬_
¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ X = X → ⊥

_↯_ : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → X → ¬ X → Y
p ↯ ¬p = elim⊥ (¬p p)

-- Built-in equality.

open import Agda.Builtin.Equality public
  using (_≡_ ; refl)

infix 4 _≢_
_≢_ : ∀ {ℓ} {X : Set ℓ} → X → X → Set ℓ
x ≢ x′ = ¬ (x ≡ x′)

trans : ∀ {ℓ} {X : Set ℓ} {x x′ x″ : X} → x ≡ x′ → x′ ≡ x″ → x ≡ x″
trans refl refl = refl

sym : ∀ {ℓ} {X : Set ℓ} {x x′ : X} → x ≡ x′ → x′ ≡ x
sym refl = refl

subst : ∀ {ℓ ℓ′} {X : Set ℓ} → (P : X → Set ℓ′) →
        ∀ {x x′} → x ≡ x′ → P x → P x′
subst P refl p = p

cong : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → (f : X → Y) →
       ∀ {x x′} → x ≡ x′ → f x ≡ f x′
cong f refl = refl

cong² : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} → (f : X → Y → Z) →
        ∀ {x x′ y y′} → x ≡ x′ → y ≡ y′ → f x y ≡ f x′ y′
cong² f refl refl = refl

cong³ : ∀ {ℓ ℓ′ ℓ″ ℓ‴} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} {A : Set ℓ‴} →
        (f : X → Y → Z → A) →
        ∀ {x x′ y y′ z z′} → x ≡ x′ → y ≡ y′ → z ≡ z′ → f x y z ≡ f x′ y′ z′
cong³ f refl refl refl = refl

-- Equational reasoning with built-in equality.

module ≡-Reasoning {ℓ} {X : Set ℓ} where
  infix 1 begin_
  begin_ : ∀ {x x′ : X} → x ≡ x′ → x ≡ x′
  begin p = p

  infixr 2 _≡⟨⟩_
  _≡⟨⟩_ : ∀ (x {x′} : X) → x ≡ x′ → x ≡ x′
  x ≡⟨⟩ p = p

  infixr 2 _≡⟨_⟩_
  _≡⟨_⟩_ : ∀ (x {x′ x″} : X) → x ≡ x′ → x′ ≡ x″ → x ≡ x″
  x ≡⟨ p ⟩ q = trans p q

  infix 3 _∎
  _∎ : ∀ (x : X) → x ≡ x
  x ∎ = refl

open ≡-Reasoning public

-- Constructive existence.

infixl 5 _,_
record Σ {ℓ ℓ′} (X : Set ℓ) (Y : X → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  constructor _,_
  field
    π₁ : X
    π₂ : Y π₁

open Σ public

-- Conjunction.

infixr 2 _∧_
_∧_ : ∀ {ℓ ℓ′} → Set ℓ → Set ℓ′ → Set (ℓ ⊔ ℓ′)
X ∧ Y = Σ X (λ x → Y)

-- Disjunction.

infixr 1 _∨_
data _∨_ {ℓ ℓ′} (X : Set ℓ) (Y : Set ℓ′) : Set (ℓ ⊔ ℓ′) where
  ι₁ : X → X ∨ Y
  ι₂ : Y → X ∨ Y

{-# HASKELL type AgdaEither _ _ x y = Either x y #-}
{-# COMPILED_DATA _∨_ MAlonzo.Code.Data.Sum.AgdaEither Left Right #-}

elim∨ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
        X ∨ Y → (X → Z) → (Y → Z) → Z
elim∨ (ι₁ x) f g = f x
elim∨ (ι₂ y) f g = g y

-- Equivalence.

infix 3 _↔_
_↔_ : ∀ {ℓ ℓ′} → (X : Set ℓ) (Y : Set ℓ′) → Set (ℓ ⊔ ℓ′)
X ↔ Y = (X → Y) ∧ (Y → X)

infix 3 _↮_
_↮_ : ∀ {ℓ ℓ′} → (X : Set ℓ) (Y : Set ℓ′) → Set (ℓ ⊔ ℓ′)
X ↮ Y = ¬ (X ↔ Y)

refl↔ : ∀ {ℓ} {X : Set ℓ} → X ↔ X
refl↔ = refl→ , refl→

trans↔ : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″} →
          X ↔ Y → Y ↔ Z → X ↔ Z
trans↔ (P , Q) (P′ , Q′) = trans→ P P′ , trans→ Q′ Q

sym↔ : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → X ↔ Y → Y ↔ X
sym↔ (P , Q) = Q , P

antisym→ : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} →
            ((X → Y) ∧ (Y → X)) ≡ (X ↔ Y)
antisym→ = refl

≡→↔ : ∀ {ℓ} {X Y : Set ℓ} → X ≡ Y → X ↔ Y
≡→↔ refl = refl↔

-- Equational reasoning with equivalence.

module ↔-Reasoning where
  infix 1 begin↔_
  begin↔_ : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → X ↔ Y → X ↔ Y
  begin↔ P = P

  infixr 2 _↔⟨⟩_
  _↔⟨⟩_ : ∀ {ℓ ℓ′} → (X : Set ℓ) → {Y : Set ℓ′} → X ↔ Y → X ↔ Y
  X ↔⟨⟩ P = P

  infixr 2 _≡→↔⟨⟩_
  _≡→↔⟨⟩_ : ∀ {ℓ} → (X : Set ℓ) → {Y : Set ℓ} → X ≡ Y → X ↔ Y
  X ≡→↔⟨⟩ P = ≡→↔ P

  infixr 2 _↔⟨_⟩_
  _↔⟨_⟩_ : ∀ {ℓ ℓ′ ℓ″} → (X : Set ℓ) → {Y : Set ℓ′} {Z : Set ℓ″} →
            X ↔ Y → Y ↔ Z → X ↔ Z
  X ↔⟨ P ⟩ Q = trans↔ P Q

  infix 3 _∎↔
  _∎↔ : ∀ {ℓ} → (X : Set ℓ) → X ↔ X
  X ∎↔ = refl↔

open ↔-Reasoning public

-- Booleans.

open import Agda.Builtin.Bool public
  using (Bool ; false ; true)

elimBool : ∀ {ℓ} {X : Set ℓ} → Bool → X → X → X
elimBool false z s = z
elimBool true  z s = s

-- Conditionals.

data Maybe {ℓ} (X : Set ℓ) : Set ℓ where
  nothing : Maybe X
  just    : X → Maybe X

{-# HASKELL type AgdaMaybe _ x = Maybe x #-}
{-# COMPILED_DATA Maybe MAlonzo.Code.Data.Maybe.Base.AgdaMaybe Just Nothing #-}

elimMaybe : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → Maybe X → Y → (X → Y) → Y
elimMaybe nothing  z f = z
elimMaybe (just x) z f = f x

-- Naturals.

open import Agda.Builtin.Nat public
  using (Nat ; zero ; suc)

elimNat : ∀ {ℓ} {X : Set ℓ} → Nat → X → (Nat → X → X) → X
elimNat zero    z f = z
elimNat (suc n) z f = f n (elimNat n z f)

-- Decidability.

data Dec {ℓ} (X : Set ℓ) : Set ℓ where
  yes : X → Dec X
  no  : ¬ X → Dec X

mapDec : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} →
         (X → Y) → (Y → X) → Dec X → Dec Y
mapDec f g (yes x) = yes (f x)
mapDec f g (no ¬x) = no (λ y → g y ↯ ¬x)

⌊_⌋Dec : ∀ {ℓ} {X : Set ℓ} → Dec X → Bool
⌊ yes x ⌋Dec = true
⌊ no ¬x ⌋Dec = false

max_stars_repo_name: mietek/nbe-correctness

max_issues_repo_name: mietek/nbe-correctness

max_forks_repo_name: mietek/nbe-correctness


text:
-- Andreas, 2014-01-08, following Maxime Denes 2014-01-06

-- This file demonstrates that size-based termination does
-- not lead to incompatibility with HoTT.

{-# OPTIONS --sized-types #-}

open import Common.Size
open import Common.Equality

data Empty : Set where

data Box : Size → Set where
  wrap : ∀ i → (Empty → Box i) → Box (↑ i)

-- Box is inhabited at each stage > 0:

gift : ∀ {i} → Empty → Box i
gift ()

box : ∀ {i} → Box (↑ i)
box {i} = wrap i gift

-- wrap has an inverse:

unwrap : ∀ i → Box (↑ i) → (Empty → Box i)
unwrap .i (wrap i f) = f

-- There is an isomorphism between (Empty → Box ∞) and (Box ∞)
-- but none between (Empty → Box i) and (Box i).
-- We only get the following, but it is not sufficient to
-- produce the loop.

postulate iso : ∀ i → (Empty → Box i) ≡ Box (↑ i)

-- Since Agda's termination checker uses the structural order
-- in addition to sized types, we need to conceal the subterm.

conceal : {A : Set} → A → A
conceal x = x

mutual
  loop : ∀ i → Box i → Empty
  loop .(↑ i) (wrap i x) = loop' (↑ i) (Empty → Box i) (iso i) (conceal x)

  -- We would like to write  loop' i  instead of  loop' (↑ i)
  -- but this is ill-typed.  Thus, we cannot achieve something
  -- well-founded wrt. to sized types.

  loop' : ∀ i A → A ≡ Box i → A → Empty
  loop' i .(Box i) refl x = loop i x

-- The termination checker complains here, rightfully!

bug : Empty
bug = loop ∞ box

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- 2014-05-27 Jesper and Andreas

postulate
  A : Set
  R : A → A → Set

{-# BUILTIN REWRITE R #-}
{-# REWRITE R #-}

-- Expected error:
-- R  does not target rewrite relation
-- when checking the pragma REWRITE R

max_stars_repo_name: larrytheliquid/agda


text:
open import FRP.JS.Nat using ( ℕ ; suc ; _+_ ) renaming ( _≟_ to _≟=_ )
open import FRP.JS.List using ( List ; [] ; _∷_ ; [_] ; _++_ ; map ; foldr ; foldl ; build ; _≟[_]_ )
open import FRP.JS.Bool using ( Bool ; not )
open import FRP.JS.QUnit using ( TestSuite ; ok ; ok! ; test ; _,_ )

module FRP.JS.Test.List where

infixr 2 _≟_

_≟_ : List ℕ → List ℕ → Bool
xs ≟ ys = xs ≟[ _≟=_ ] ys

tests : TestSuite
tests =
  ( test "≟"
    ( ok "[] ≟ []" ([] ≟ [])
    , ok "[] ≟ [0]" (not ([] ≟ (0 ∷ [])))
    , ok "[0] ≟ []" (not ((0 ∷ []) ≟ []))
    , ok "[0] ≟ [0]" ((0 ∷ []) ≟ (0 ∷ []))
    , ok "[] ≟ [0,1]" (not ([] ≟ (0 ∷ 1 ∷ [])))
    , ok "[0,1] ≟ []" (not ((0 ∷ 1 ∷ []) ≟ []))
    , ok "[1] ≟ [0,1]" (not ((1 ∷ []) ≟ (0 ∷ 1 ∷ [])))
    , ok "[0] ≟ [0,1]" (not ((0 ∷ []) ≟ (0 ∷ 1 ∷ [])))
    , ok "[0,1] ≟ [0,1]" ((0 ∷ 1 ∷ []) ≟ (0 ∷ 1 ∷ [])) )
  , test "[_]"
    ( ok "[1] ≟ 1 ∷ []" ([ 1 ] ≟ 1 ∷ [])
    , ok "[1] ≟ [0]" (not ([ 1 ] ≟ [ 0 ])) )
  , test "++"
    ( ok "[] ++ []" ([] ++ [] ≟ [])
    , ok "[] ++ [1]" ([] ++ [ 1 ] ≟ [ 1 ])
    , ok "[0] ++ []" ([ 0 ] ++ [] ≟ [ 0 ])
    , ok "[0] ++ [1]" ([ 0 ] ++ [ 1 ] ≟ 0 ∷ [ 1 ])
    , ok "[0] ++ [1] ++ [2]" ([ 0 ] ++ [ 1 ] ++ [ 2 ] ≟ (0 ∷ 1 ∷ [ 2 ])) )
  , test "foldl"
    ( ok "foldl + []" (foldl _+_ 0 [] ≟= 0)
    , ok "foldl + [1]" (foldl _+_ 0 [ 1 ] ≟= 1)
    , ok "foldl + [1,2]" (foldl _+_ 0 (1 ∷ [ 2 ]) ≟= 3) )
  , test "foldr"
    ( ok "foldr + []" (foldr _+_ 0 [] ≟= 0)
    , ok "foldr + [1]" (foldr _+_ 0 [ 1 ] ≟= 1)
    , ok "foldr + [1,2]" (foldr _+_ 0 (1 ∷ [ 2 ]) ≟= 3) )
  , test "map"
    ( ok "map suc []" (map suc [] ≟ [])
    , ok "map suc [1]" (map suc [ 1 ] ≟ [ 2 ])
    , ok "map suc [1,2]" (map suc (1 ∷ [ 2 ]) ≟ 2 ∷ [ 3 ]) )
  , test "build"
    ( ok "build suc 0" (build suc 0 ≟ [])
    , ok "build suc 1" (build suc 1 ≟ [ 1 ])
    , ok "build suc 2" (build suc 2 ≟ 1 ∷ [ 2 ]) ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module Numeral.Natural.Oper.Summation.Proofs where

import      Lvl
open import Data.List
open import Data.List.Functions
open import Data.List.Equiv.Id
open import Numeral.Natural
open import Structure.Function
open import Structure.Operator.Field
open import Structure.Operator.Monoid
open import Structure.Operator
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T A B : Type{ℓ}
private variable _▫_ : T → T → T

open        Data.List.Functions.LongOper
open import Data.List.Proofs
open import Functional as Fn using (_$_ ; _∘_ ; const)
import      Function.Equals as Fn
open import Lang.Instance
import      Numeral.Natural.Oper.Summation
open import Numeral.Natural.Oper.Summation.Range
open import Numeral.Natural.Oper.Summation.Range.Proofs
open import Numeral.Natural.Relation.Order
import      Structure.Function.Names as Names
open import Structure.Operator.Properties
open import Structure.Operator.Proofs.Util
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ monoid : Monoid{T = T}(_▫_) ⦄ where
  open Numeral.Natural.Oper.Summation {I = ℕ} ⦃ monoid = monoid ⦄
  open Monoid(monoid) using (id) renaming (binary-operator to [▫]-binary-operator)
  open import Relator.Equals.Proofs.Equiv {T = ℕ}

  private variable f g : ℕ → T
  private variable x a b c k n : ℕ
  private variable r r₁ r₂ : List(ℕ)

  ∑-empty : (∑(∅) f ≡ id)
  ∑-empty = reflexivity(Equiv._≡_ equiv)

  ∑-prepend : (∑(prepend x r) f ≡ f(x) ▫ ∑(r) f)
  ∑-prepend = reflexivity(Equiv._≡_ equiv)

  ∑-postpend : (∑(postpend x r) f ≡ ∑(r) f ▫ f(x))
  ∑-postpend {x = x} {r = ∅} {f = f} =
    ∑(postpend x empty) f 🝖[ _≡_ ]-[]
    ∑(prepend x empty) f  🝖[ _≡_ ]-[]
    f(x) ▫ (∑(empty) f)   🝖[ _≡_ ]-[]
    f(x) ▫ id             🝖[ _≡_ ]-[ identityᵣ(_▫_)(id) ]
    f(x)                  🝖[ _≡_ ]-[ identityₗ(_▫_)(id) ]-sym
    id ▫ f(x)             🝖[ _≡_ ]-[]
    (∑(empty) f) ▫ f(x)   🝖-end
  ∑-postpend {x = x} {r = r₀ ⊰ r} {f = f} =
    f(r₀) ▫ ∑(postpend x r) f  🝖[ _≡_ ]-[ congruence₂ᵣ(_▫_)(f(r₀)) (∑-postpend {x = x}{r = r}{f = f}) ]
    f(r₀) ▫ (∑(r) f ▫ f(x))    🝖[ _≡_ ]-[ associativity(_▫_) {f(r₀)}{∑(r) f}{f(x)} ]-sym
    (f(r₀) ▫ ∑(r) f) ▫ f(x)    🝖-end

  ∑-compose : ∀{f : ℕ → T}{g : ℕ → ℕ} → (∑(r) (f ∘ g) ≡ ∑(map g r) f)
  ∑-compose {r = r}{f = f}{g = g} =
    ∑(r) (f ∘ g)                  🝖[ _≡_ ]-[]
    foldᵣ(_▫_) id (map(f ∘ g) r)   🝖[ _≡_ ]-[ congruence₁(foldᵣ(_▫_) id) ⦃ foldᵣ-function ⦄ (map-preserves-[∘] {f = f}{g = g}{x = r}) ]
    foldᵣ(_▫_) id (map f(map g r)) 🝖[ _≡_ ]-[]
    ∑(map g r) f                  🝖-end

  ∑-singleton : (∑(singleton(a)) f ≡ f(a))
  ∑-singleton = identityᵣ ⦃ equiv ⦄ (_▫_)(id)

  ∑-concat : (∑(r₁ ++ r₂) f ≡ ∑(r₁) f ▫ ∑(r₂) f)
  ∑-concat {empty}        {r₂} {f} = symmetry(_≡_) (identityₗ(_▫_)(id))
  ∑-concat {prepend x r₁} {r₂} {f} =
    f(x) ▫ ∑(r₁ ++ r₂) f      🝖[ _≡_ ]-[ congruence₂ᵣ(_▫_)(f(x)) (∑-concat {r₁}{r₂}{f}) ]
    f(x) ▫ (∑(r₁) f ▫ ∑ r₂ f) 🝖[ _≡_ ]-[ associativity(_▫_) {x = f(x)}{y = ∑(r₁) f}{z = ∑(r₂) f} ]-sym
    (f(x) ▫ ∑(r₁) f) ▫ ∑ r₂ f 🝖-end

  ∑-const-id : (∑(r) (const id) ≡ id)
  ∑-const-id {empty}       = reflexivity(Equiv._≡_ equiv)
  ∑-const-id {prepend x r} =
    ∑(prepend x r) (const id) 🝖[ _≡_ ]-[]
    id ▫ (∑(r) (const id))    🝖[ _≡_ ]-[ identityₗ(_▫_)(id) ]
    ∑(r) (const id)           🝖[ _≡_ ]-[ ∑-const-id {r} ]
    id                        🝖-end

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  private variable f g : ℕ → T
  private variable k n : ℕ
  private variable x a b c : T
  private variable r r₁ r₂ : List(ℕ)
  private variable _+_ _⋅_ : T → T → T

  module _ ⦃ monoid : Monoid(_+_) ⦄ ⦃ comm : Commutativity(_+_) ⦄ where
    open Numeral.Natural.Oper.Summation {I = ℕ} ⦃ monoid = monoid ⦄
    open Monoid(monoid) using (id) renaming (binary-operator to [+]-binary-operator)
    open import Relator.Equals.Proofs.Equiv {T = ℕ}

    ∑-add : (∑(r) f + ∑(r) g ≡ ∑(r) (x ↦ f(x) + g(x)))
    ∑-add {∅}      {f} {g} = identityₗ(_+_)(id)
    ∑-add {r₀ ⊰ r} {f} {g} =
      ∑(prepend r₀ r) f + ∑(prepend r₀ r) g    🝖[ _≡_ ]-[]
      (f(r₀) + ∑(r) f) + (g(r₀) + ∑(r) g)      🝖[ _≡_ ]-[ One.associate-commute4 {a = f(r₀)}{b = ∑(r) f}{c = g(r₀)}{d = ∑(r) g} (commutativity(_+_){∑(r) f}{g(r₀)}) ]
      (f(r₀) + g(r₀)) + (∑(r) f + ∑(r) g)      🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(f(r₀) + g(r₀)) (∑-add {r} {f} {g}) ]
      (f(r₀) + g(r₀)) + ∑(r) (x ↦ f(x) + g(x)) 🝖[ _≡_ ]-[]
      ∑(prepend r₀ r) (x ↦ f(x) + g(x))        🝖-end

  module _ ⦃ monoid : Monoid(_+_) ⦄ ⦃ distₗ : Distributivityₗ(_⋅_)(_+_) ⦄ ⦃ absorᵣ : Absorberᵣ(_⋅_)(Monoid.id monoid) ⦄ where
    open Numeral.Natural.Oper.Summation {I = ℕ} ⦃ monoid = monoid ⦄
    open Monoid(monoid) using (id) renaming (binary-operator to [+]-binary-operator)
    open import Relator.Equals.Proofs.Equiv {T = ℕ}

    ∑-scalar-multₗ : (∑(r) (x ↦ c ⋅ f(x)) ≡ c ⋅ (∑(r) f))
    ∑-scalar-multₗ {empty}        {c} {f} = symmetry(_≡_) (absorberᵣ(_⋅_)(id))
    ∑-scalar-multₗ {prepend r₀ r} {c} {f} =
      (c ⋅ f(r₀)) + ∑(r) (x ↦ c ⋅ f(x)) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(c ⋅ f(r₀)) (∑-scalar-multₗ {r}{c}{f}) ]
      (c ⋅ f(r₀)) + (c ⋅ (∑(r) f))      🝖[ _≡_ ]-[ distributivityₗ(_⋅_)(_+_) {c}{f(r₀)}{∑(r) f} ]-sym
      c ⋅ (f(r₀) + (∑(r) f))            🝖-end

  module _ ⦃ monoid : Monoid(_+_) ⦄ ⦃ distᵣ : Distributivityᵣ(_⋅_)(_+_) ⦄ ⦃ absorₗ : Absorberₗ(_⋅_)(Monoid.id monoid) ⦄ where
    open Numeral.Natural.Oper.Summation {I = ℕ} ⦃ monoid = monoid ⦄
    open Monoid(monoid) using (id) renaming (binary-operator to [+]-binary-operator)
    open import Relator.Equals.Proofs.Equiv {T = ℕ}

    ∑-scalar-multᵣ : (∑(r) (x ↦ f(x) ⋅ c) ≡ (∑(r) f) ⋅ c)
    ∑-scalar-multᵣ {empty}        {f} {c} = symmetry(_≡_) (absorberₗ(_⋅_)(id))
    ∑-scalar-multᵣ {prepend r₀ r} {f} {c} =
      (f(r₀) ⋅ c) + ∑(r) (x ↦ f(x) ⋅ c) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(f(r₀) ⋅ c) (∑-scalar-multᵣ {r}{f}{c}) ]
      (f(r₀) ⋅ c) + ((∑(r) f) ⋅ c)      🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_+_) {f(r₀)}{∑(r) f}{c} ]-sym
      (f(r₀) + (∑(r) f)) ⋅ c            🝖-end

  module _ ⦃ field-structure : Field(_+_)(_⋅_) ⦄ where
    open Field(field-structure)
    open Numeral.Natural.Oper.Summation {I = ℕ} ⦃ monoid = [+]-monoid ⦄

open import Relator.Equals hiding (_≡_)
open import Relator.Equals.Proofs.Equiv
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Structure
open Numeral.Natural.Oper.Summation {I = ℕ} ⦃ monoid = [+]-monoid ⦄ -- TODO: Generalize all the proofs

private variable f g : ℕ → ℕ
private variable x a b c k n : ℕ
private variable r r₁ r₂ : List(ℕ)

∑-const : (∑(r) (const c) ≡ c ⋅ length(r))
∑-const {empty}      {c} = reflexivity(_≡_)
∑-const {prepend x r}{c} = congruence₂ᵣ(_+_)(c) (∑-const {r}{c})

-- TODO: Σ-const-id is a generalization of this
∑-zero : (∑(r) (const 𝟎) ≡ 𝟎)
∑-zero {r} = ∑-const {r}{𝟎}

-- TODO: map-binaryOperator is on the equality setoid, which blocks the generalization of this
instance
  ∑-binaryOperator : BinaryOperator ⦃ equiv-A₂ = Fn.[⊜]-equiv ⦄ (∑)
  BinaryOperator.congruence ∑-binaryOperator {r₁}{r₂}{f}{g} rr fg =
    ∑(r₁) f  🝖[ _≡_ ]-[]
    foldᵣ(_+_) 𝟎 (map f(r₁))  🝖[ _≡_ ]-[ congruence₁(foldᵣ(_+_) 𝟎) (congruence₂(map) ⦃ map-binaryOperator ⦄ fg rr) ]
    foldᵣ(_+_) 𝟎 (map g(r₂))  🝖[ _≡_ ]-[]
    ∑(r₂) g  🝖-end

∑-mult : ∀{r₁ r₂}{f g} → ((∑(r₁) f) ⋅ (∑(r₂) g) ≡ ∑(r₁) (x ↦ ∑(r₂) (y ↦ f(x) ⋅ g(y))))
∑-mult {empty}        {_} {f} {g} = [≡]-intro
∑-mult {prepend x₁ r₁} {empty} {f} {g} =
  𝟎                                                 🝖[ _≡_ ]-[ ∑-zero {r = prepend x₁ r₁} ]-sym
  ∑(prepend x₁ r₁) (x ↦ 𝟎)                          🝖[ _≡_ ]-[ congruence₂ᵣ(∑)(prepend x₁ r₁) (Fn.intro(\{x} → ∑-empty {f = y ↦ f(x) ⋅ g(y)})) ]-sym
  ∑(prepend x₁ r₁) (x ↦ ∑(empty) (y ↦ f(x) ⋅ g(y))) 🝖-end
∑-mult {prepend x₁ r₁} {prepend x₂ r₂} {f} {g} =
  (∑(prepend x₁ r₁) f) ⋅ (∑(prepend x₂ r₂) g)                                                               🝖[ _≡_ ]-[]
  (f(x₁) + (∑(r₁) f)) ⋅ (g(x₂) + (∑(r₂) g))                                                                 🝖[ _≡_ ]-[ OneTypeTwoOp.cross-distribute {a = f(x₁)}{b = ∑(r₁) f}{c = g(x₂)}{d = ∑(r₂) g} ]
  ((f(x₁) ⋅ g(x₂)) + ((∑(r₁) f) ⋅ g(x₂))) + ((f(x₁) ⋅ (∑(r₂) g)) + ((∑(r₁) f) ⋅ (∑(r₂) g)))                 🝖[ _≡_ ]-[ One.associate-commute4 {a = f(x₁) ⋅ g(x₂)}{b = (∑(r₁) f) ⋅ g(x₂)}{c = f(x₁) ⋅ (∑(r₂) g)}{d = (∑(r₁) f) ⋅ (∑(r₂) g)} (commutativity(_+_) {(∑(r₁) f) ⋅ g(x₂)}{f(x₁) ⋅ (∑(r₂) g)}) ]
  ((f(x₁) ⋅ g(x₂)) + (f(x₁) ⋅ (∑(r₂) g))) + (((∑(r₁) f) ⋅ g(x₂)) + ((∑(r₁) f) ⋅ (∑(r₂) g)))                 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_) ((f(x₁) ⋅ g(x₂)) + (f(x₁) ⋅ (∑(r₂) g))) p ]
  ((f(x₁) ⋅ g(x₂)) + (f(x₁) ⋅ (∑(r₂) g))) + (∑(r₁) (x ↦ (f(x) ⋅ g(x₂)) + (∑(r₂) (y ↦ f(x) ⋅ g(y)))))        🝖[ _≡_ ]-[ congruence₂ₗ(_+_) (∑(r₁) (x ↦ (f(x) ⋅ g(x₂)) + (∑(r₂) (y ↦ f(x) ⋅ g(y))))) (congruence₂ᵣ(_+_)(f(x₁) ⋅ g(x₂)) (∑-scalar-multₗ {r = r₂}{c = f(x₁)}{f = g})) ]-sym
  ((f(x₁) ⋅ g(x₂)) + (∑(r₂) (y ↦ f(x₁) ⋅ g(y)))) + (∑(r₁) (x ↦ (f(x) ⋅ g(x₂)) + (∑(r₂) (y ↦ f(x) ⋅ g(y))))) 🝖[ _≡_ ]-[]
  (∑(prepend x₂ r₂) (y ↦ f(x₁) ⋅ g(y))) + (∑(r₁) (x ↦ ∑(prepend x₂ r₂) (y ↦ f(x) ⋅ g(y))))                  🝖[ _≡_ ]-[]
  ∑(prepend x₁ r₁) (x ↦ ∑(prepend x₂ r₂) (y ↦ f(x) ⋅ g(y)))                                                 🝖-end
  where
    p =
      ((∑(r₁) f) ⋅ g(x₂)) + ((∑(r₁) f) ⋅ (∑(r₂) g))                 🝖[ _≡_ ]-[ distributivityₗ(_⋅_)(_+_) {x = ∑(r₁) f}{y = g(x₂)}{z = ∑(r₂) g} ]-sym
      (∑(r₁) f) ⋅ (g(x₂) + (∑(r₂) g))                               🝖[ _≡_ ]-[ ∑-scalar-multᵣ {r = r₁}{f = f}{c = g(x₂) + (∑(r₂) g)} ]-sym
      ∑(r₁) (x ↦ f(x) ⋅ (g(x₂) + (∑(r₂) g)))                        🝖[ _≡_ ]-[ congruence₂ᵣ(∑) r₁ (Fn.intro(\{x} → distributivityₗ(_⋅_)(_+_) {x = f(x)}{y = g(x₂)}{z = ∑(r₂) g})) ]
      ∑(r₁) (x ↦ (f(x) ⋅ g(x₂)) + (f(x) ⋅ (∑(r₂) g)))               🝖[ _≡_ ]-[ congruence₂ᵣ(∑) r₁ (Fn.intro(\{x} → congruence₂ᵣ(_+_) (f(x) ⋅ g(x₂)) (∑-scalar-multₗ {r = r₂}{c = f(x)}{f = g}))) ]-sym
      ∑(r₁) (x ↦ (f(x) ⋅ g(x₂)) + (∑(r₂) (y ↦ f(x) ⋅ g(y))))        🝖-end

∑-swap-nested : ∀{f : ℕ → ℕ → _}{r₁ r₂} → (∑(r₁) (a ↦ ∑(r₂) (b ↦ f(a)(b))) ≡ ∑(r₂) (b ↦ ∑(r₁) (a ↦ f(a)(b))))
∑-swap-nested {f} {empty}         {empty}         = [≡]-intro
∑-swap-nested {f} {empty}         {prepend x  r₂} =
  ∑(∅)(a ↦ ∑(x ⊰ r₂) (b ↦ f(a)(b)))  🝖[ _≡_ ]-[]
  𝟎                                  🝖[ _≡_ ]-[ ∑-zero {x ⊰ r₂} ]-sym
  ∑(x ⊰ r₂) (b ↦ 𝟎)                  🝖[ _≡_ ]-[]
  ∑(x ⊰ r₂) (b ↦ ∑(∅) (a ↦ f(a)(b))) 🝖-end
∑-swap-nested {f} {prepend x  r₁} {empty}         =
  ∑(x ⊰ r₁) (a ↦ ∑(∅) (b ↦ f(a)(b))) 🝖[ _≡_ ]-[]
  ∑(x ⊰ r₁) (b ↦ 𝟎)                  🝖[ _≡_ ]-[ ∑-zero {x ⊰ r₁} ]
  𝟎                                  🝖[ _≡_ ]-[]
  ∑(∅) (b ↦ ∑(x ⊰ r₁) (a ↦ f(a)(b))) 🝖-end
∑-swap-nested {f} {prepend x₁ r₁} {prepend x₂ r₂} =
  ∑(x₁ ⊰ r₁) (a ↦ ∑(x₂ ⊰ r₂) (b ↦ f(a)(b)))                                                       🝖[ _≡_ ]-[]
  ∑(x₁ ⊰ r₁) (a ↦ f(a)(x₂) + ∑(r₂) (b ↦ f(a)(b)))                                                 🝖[ _≡_ ]-[]
  (f(x₁)(x₂) + ∑(r₂) (b ↦ f(x₁)(b))) + ∑(r₁) (a ↦ f(a)(x₂) + ∑(r₂) (b ↦ f(a)(b)))                 🝖[ _≡_ ]-[]
  (f(x₁)(x₂) + ∑(r₂) (b ↦ f(x₁)(b))) + (∑(r₁) (a ↦ f(a)(x₂) + ∑(r₂) (b ↦ f(a)(b))))               🝖[ _≡_ ]-[ associativity(_+_) {x = f(x₁)(x₂)}{y = ∑(r₂) (b ↦ f(x₁)(b))} ]
  f(x₁)(x₂) + (∑(r₂) (b ↦ f(x₁)(b)) + (∑(r₁) (a ↦ f(a)(x₂) + ∑(r₂) (b ↦ f(a)(b)))))               🝖[ _≡_ ]-[]
  f(x₁)(x₂) + (∑(r₂) (b ↦ f(x₁)(b)) + (∑(r₁) (a ↦ ∑(x₂ ⊰ r₂) (b ↦ f(a)(b)))))                     🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(f(x₁)(x₂)) (congruence₂ᵣ(_+_)(∑(r₂) (b ↦ f(x₁)(b))) (∑-swap-nested {f}{r₁}{x₂ ⊰ r₂})) ]
  f(x₁)(x₂) + (∑(r₂) (b ↦ f(x₁)(b)) + (∑(x₂ ⊰ r₂) (b ↦ ∑(r₁) (a ↦ f(a)(b)))))                     🝖[ _≡_ ]-[]
  f(x₁)(x₂) + (∑(r₂) (b ↦ f(x₁)(b)) + (∑(r₁) (a ↦ f(a)(x₂)) + (∑(r₂) (b ↦ ∑(r₁) (a ↦ f(a)(b)))))) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(f(x₁)(x₂)) (symmetry(_≡_) (associativity(_+_) {x = ∑(r₂) (b ↦ f(x₁)(b))}{y = ∑(r₁) (a ↦ f(a)(x₂))})) ]
  f(x₁)(x₂) + ((∑(r₂) (b ↦ f(x₁)(b)) + ∑(r₁) (a ↦ f(a)(x₂))) + (∑(r₂) (b ↦ ∑(r₁) (a ↦ f(a)(b))))) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(f(x₁)(x₂)) (congruence₂(_+_) (commutativity(_+_) {∑(r₂) (b ↦ f(x₁)(b))}{∑(r₁) (a ↦ f(a)(x₂))}) (symmetry(_≡_) (∑-swap-nested {f}{r₁}{r₂}))) ]
  f(x₁)(x₂) + ((∑(r₁) (a ↦ f(a)(x₂)) + ∑(r₂) (b ↦ f(x₁)(b))) + ∑(r₁) (a ↦ ∑(r₂) (b ↦ f(a)(b))))   🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(f(x₁)(x₂)) (associativity(_+_) {x = ∑(r₁) (a ↦ f(a)(x₂))}{y = ∑(r₂) (b ↦ f(x₁)(b))}) ]
  f(x₁)(x₂) + (∑(r₁) (a ↦ f(a)(x₂)) + (∑(r₂) (b ↦ f(x₁)(b)) + ∑(r₁) (a ↦ ∑(r₂) (b ↦ f(a)(b)))))   🝖[ _≡_ ]-[]
  f(x₁)(x₂) + (∑(r₁) (a ↦ f(a)(x₂)) + (∑(x₁ ⊰ r₁) (a ↦ ∑(r₂) (b ↦ f(a)(b)))))                     🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(f(x₁)(x₂)) (congruence₂ᵣ(_+_)(∑(r₁) (a ↦ f(a)(x₂))) (∑-swap-nested {f}{x₁ ⊰ r₁}{r₂})) ]
  f(x₁)(x₂) + (∑(r₁) (a ↦ f(a)(x₂)) + (∑(r₂) (b ↦ ∑(x₁ ⊰ r₁) (a ↦ f(a)(b)))))                     🝖[ _≡_ ]-[]
  f(x₁)(x₂) + (∑(r₁) (a ↦ f(a)(x₂)) + (∑(r₂) (b ↦ f(x₁)(b) + ∑(r₁) (a ↦ f(a)(b)))))               🝖[ _≡_ ]-[ associativity(_+_) {x = f(x₁)(x₂)}{y = ∑(r₁) (a ↦ f(a)(x₂))} ]-sym
  (f(x₁)(x₂) + ∑(r₁) (a ↦ f(a)(x₂))) + (∑(r₂) (b ↦ f(x₁)(b) + ∑(r₁) (a ↦ f(a)(b))))               🝖[ _≡_ ]-[]
  ∑(x₂ ⊰ r₂) (b ↦ f(x₁)(b) + ∑(r₁) (a ↦ f(a)(b)))                                                 🝖[ _≡_ ]-[]
  ∑(x₂ ⊰ r₂) (b ↦ ∑(x₁ ⊰ r₁) (a ↦ f(a)(b)))                                                       🝖-end

∑-zero-range : (∑(a ‥ a) f ≡ 𝟎)
∑-zero-range {a}{f} = congruence₁ (r ↦ ∑(r) f) (Range-empty{a})

∑-single-range : (∑(a ‥ 𝐒(a)) f ≡ f(a))
∑-single-range {𝟎}  {f} = reflexivity(_≡_)
∑-single-range {𝐒 a}{f} =
  ∑ (map 𝐒(a ‥ 𝐒(a))) f       🝖[ _≡_ ]-[ ∑-compose ⦃ monoid = [+]-monoid ⦄ {r = a ‥ 𝐒(a)}{f}{𝐒} ]-sym
  ∑ (a ‥ 𝐒(a)) (x ↦ f(𝐒(x)))  🝖[ _≡_ ]-[ ∑-single-range {a}{f ∘ 𝐒} ]
  f(𝐒(a))                     🝖-end

∑-step-range : (∑(𝐒(a) ‥ 𝐒(b)) f ≡ ∑(a ‥ b) (f ∘ 𝐒))
∑-step-range {a}{b}{f} = symmetry(_≡_) (∑-compose {r = a ‥ b}{f = f}{g = 𝐒})

∑-stepₗ-range : ⦃ _ : (a < b) ⦄ → (∑(a ‥ b) f ≡ f(a) + ∑(𝐒(a) ‥ b) f)
∑-stepₗ-range {𝟎}   {𝐒 b} {f} ⦃ succ ab ⦄ = reflexivity(_≡_)
∑-stepₗ-range {𝐒 a} {𝐒 b} {f} ⦃ succ ab ⦄ =
  ∑(𝐒(a) ‥ 𝐒(b)) f                                🝖[ _≡_ ]-[ ∑-step-range {a}{b}{f} ]
  ∑(a ‥ b) (f ∘ 𝐒)                                🝖[ _≡_ ]-[ ∑-stepₗ-range {a}{b}{f ∘ 𝐒} ]
  (f ∘ 𝐒)(a) + ∑(𝐒(a) ‥ b) (f ∘ 𝐒)                🝖[ _≡_ ]-[ congruence₂(_+_) (reflexivity(_≡_) {x = f(𝐒(a))}) (symmetry(_≡_) (∑-step-range {𝐒 a}{b}{f})) ]
  f(𝐒(a)) + ∑(𝐒(𝐒(a)) ‥ 𝐒(b)) f                   🝖-end
  where instance _ = ab

-- ∑-stepᵣ-range : ⦃ _ : (a < 𝐒(b)) ⦄ → (∑(a ‥ 𝐒(b)) f ≡ ∑(a ‥ b) f + f(b))
-- ∑-stepᵣ-range = ?

-- ∑-add-range : (∑(a ‥ a + b) f ≡ ∑(𝟎 ‥ b) (f ∘ (_+ a)))

∑-trans-range : ⦃ ab : (a ≤ b) ⦄ ⦃ bc : (b < c) ⦄ → (∑(a ‥ b) f + ∑(b ‥ c) f ≡ ∑(a ‥ c) f)
∑-trans-range {a}{b}{c} {f} =
  ∑(a ‥ b) f + ∑(b ‥ c) f 🝖[ _≡_ ]-[ ∑-concat{r₁ = a ‥ b}{r₂ = b ‥ c}{f = f} ]-sym
  ∑((a ‥ b) ++ (b ‥ c)) f 🝖[ _≡_ ]-[ congruence₁(r ↦ ∑(r) f) (Range-concat{a}{b}{c}) ]
  ∑(a ‥ c) f              🝖-end

-- TODO: Formulate ∑({(x,y). a ≤ x ≤ y ≤ b}) f ≡ ∑(a ‥ b) (x ↦ ∑(a ‥ x) (y ↦ f(x)(y))) ≡ ∑(a ‥ b) (x ↦ ∑(x ‥ b) (y ↦ f(x)(y))) ≡ ... and first prove a theorem stating that the order of a list does not matter
-- ∑-nested-dependent-range : ∀{f : ℕ → ℕ → _}{a b} → ?

∑-of-succ : (∑(r) (𝐒 ∘ f) ≡ (∑(r) f) + length(r))
∑-of-succ {empty}      {f} = [≡]-intro
∑-of-succ {prepend x r}{f} =
  ∑(x ⊰ r) (𝐒 ∘ f)                 🝖[ _≡_ ]-[]
  𝐒(f(x)) + ∑(r) (𝐒 ∘ f)           🝖[ _≡_ ]-[]
  𝐒(f(x) + ∑(r) (𝐒 ∘ f))           🝖[ _≡_ ]-[ congruence₁(𝐒) (congruence₂ᵣ(_+_)(f(x)) (∑-of-succ {r}{f})) ]
  𝐒(f(x) + ((∑(r) f) + length(r))) 🝖[ _≡_ ]-[ congruence₁(𝐒) (symmetry(_≡_) (associativity(_+_) {x = f(x)}{y = ∑(r) f}{z = length(r)})) ]
  𝐒((f(x) + (∑(r) f)) + length(r)) 🝖[ _≡_ ]-[]
  𝐒((∑(x ⊰ r) f) + length(r))      🝖[ _≡_ ]-[]
  (∑(x ⊰ r) f) + 𝐒(length(r))      🝖[ _≡_ ]-[]
  (∑(x ⊰ r) f) + length(x ⊰ r)     🝖-end

∑-even-sum : (∑(𝟎 ‥₌ n) (k ↦ 2 ⋅ k) ≡ n ⋅ 𝐒(n))
∑-even-sum {𝟎}   = [≡]-intro
∑-even-sum {𝐒 n} =
  ∑(𝟎 ‥₌ 𝐒(n)) (k ↦ 2 ⋅ k)                       🝖[ _≡_ ]-[]
  (2 ⋅ 𝟎) + ∑(1 ‥₌ 𝐒(n)) (k ↦ 2 ⋅ k)             🝖[ _≡_ ]-[]
  𝟎 + ∑(1 ‥₌ 𝐒(n)) (k ↦ 2 ⋅ k)                   🝖[ _≡_ ]-[]
  ∑(1 ‥₌ 𝐒(n)) (k ↦ 2 ⋅ k)                       🝖[ _≡_ ]-[]
  ∑(map 𝐒(𝟎 ‥₌ n)) (k ↦ 2 ⋅ k)                   🝖[ _≡_ ]-[ ∑-step-range {a = 𝟎}{b = 𝐒 n}{f = 2 ⋅_} ]
  ∑(𝟎 ‥₌ n) (k ↦ 2 ⋅ 𝐒(k))                       🝖[ _≡_ ]-[]
  ∑(𝟎 ‥₌ n) (k ↦ 2 + (2 ⋅ k))                    🝖[ _≡_ ]-[ ∑-add {r = 0 ‥₌ n}{f = const 2}{g = 2 ⋅_} ]-sym
  ∑(𝟎 ‥₌ n) (const(2)) + ∑(𝟎 ‥₌ n) (k ↦ (2 ⋅ k)) 🝖[ _≡_ ]-[ congruence₂(_+_) (∑-const {r = 0 ‥₌ n}{c = 2}) (∑-even-sum {n}) ]
  (2 ⋅ length(𝟎 ‥₌ n)) + (n ⋅ 𝐒(n))              🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(n ⋅ 𝐒(n)) (congruence₂ᵣ(_⋅_)(2) (Range-length-zero {𝐒(n)})) ]
  (2 ⋅ 𝐒(n)) + (n ⋅ 𝐒(n))                        🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_+_) {x = 2}{y = n}{z = 𝐒(n)} ]-sym
  (2 + n) ⋅ 𝐒(n)                                 🝖[ _≡_ ]-[]
  𝐒(𝐒(n)) ⋅ 𝐒(n)                                 🝖[ _≡_ ]-[ commutativity(_⋅_) {𝐒(𝐒(n))}{𝐒(n)} ]
  𝐒(n) ⋅ 𝐒(𝐒(n))                                 🝖[ _≡_ ]-end

∑-odd-sum : (∑(𝟎 ‥ n) (k ↦ 𝐒(2 ⋅ k)) ≡ n ^ 2)
∑-odd-sum {𝟎}   = [≡]-intro
∑-odd-sum {𝐒 n} =
  ∑(𝟎 ‥ 𝐒(n)) (k ↦ 𝐒(2 ⋅ k))               🝖[ _≡_ ]-[]
  ∑(𝟎 ‥₌ n) (k ↦ 𝐒(2 ⋅ k))                 🝖[ _≡_ ]-[ ∑-of-succ {r = 𝟎 ‥ 𝐒(n)}{f = 2 ⋅_} ]
  ∑(𝟎 ‥₌ n) (k ↦ 2 ⋅ k) + length(𝟎 ‥ 𝐒(n)) 🝖[ _≡_ ]-[ congruence₂(_+_) (∑-even-sum {n}) (Range-length-zero {𝐒(n)}) ]
  (n ⋅ 𝐒(n)) + 𝐒(n)                        🝖[ _≡_ ]-[ [⋅]-with-[𝐒]ₗ {x = n}{y = 𝐒(n)} ]-sym
  𝐒(n) ⋅ 𝐒(n)                              🝖[ _≡_ ]-[]
  𝐒(n) ^ 2                                 🝖-end

open import Numeral.Natural.Combinatorics

module _ where
  open import Data.List.Relation.Membership using (_∈_ ; use ; skip)

  mapDep : ∀{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → (l : List(A)) → ((elem : A) → ⦃ _ : (elem ∈ l) ⦄ → B) → List(B)
  mapDep ∅ _ = ∅
  mapDep (elem ⊰ l) f = (f elem ⦃ use [≡]-intro ⦄) ⊰ (mapDep l (\x → f x ⦃ _∈_.skip infer ⦄))

  -- ∑dep : (r : List(ℕ)) → ((i : ℕ) → ⦃ _ : (i ∈ r) ⦄ → ℕ) → ℕ

  -- ∑dep-test : ∑dep ∅ id ≡ 0

-- Also called: The binomial theorem
{-
binomial-power : ∀{n}{a b} → ((a + b) ^ n ≡ ∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ^ (n −₀ i)) ⋅ (b ^ i)))
binomial-power {𝟎}   {a} {b} =
  (a + b) ^ 𝟎                                         🝖[ _≡_ ]-[]
  1                                                   🝖[ _≡_ ]-[]
  1 ⋅ 1 ⋅ 1                                           🝖[ _≡_ ]-[]
  𝑐𝐶(𝟎)(𝟎) ⋅ (a ^ 𝟎) ⋅ (b ^ 𝟎)                        🝖[ _≡_ ]-[]
  𝑐𝐶(𝟎)(𝟎) ⋅ (a ^ (𝟎 −₀ 𝟎)) ⋅ (b ^ 𝟎)                 🝖[ _≡_ ]-[]
  ∑(𝟎 ‥₌ 𝟎) (i ↦ 𝑐𝐶(𝟎)(i) ⋅ (a ^ (𝟎 −₀ i)) ⋅ (b ^ 𝟎)) 🝖-end
binomial-power {𝐒 n} {a} {b} = {!!}
{-  (a + b) ^ 𝐒(n)                                                                                🝖[ _≡_ ]-[]
  (a + b) ⋅ ((a + b) ^ n)                                                                                🝖[ _≡_ ]-[ congruence₂ᵣ(_⋅_)(a + b) (binomial-power{n}{a}{b}) ]
  (a + b) ⋅ (∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ^ i) ⋅ (b ^ (n −₀ i))))                                                           🝖[ _≡_ ]-[ {!!} ]
  (a ⋅ (∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ^ i) ⋅ (b ^ (n −₀ i))))) + (b ⋅ (∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ^ i) ⋅ (b ^ (n −₀ i))))) 🝖[ _≡_ ]-[ {!!} ]

  a ⋅ (b ^ 𝐒(n)) ⋅ ∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(𝐒(n))(𝐒(i)) ⋅ (a ^ i) ⋅ (b ^ (n −₀ i)))                                                🝖[ _≡_ ]-[ {!!} ]
  (b ^ 𝐒(n)) ⋅ ∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(𝐒(n))(𝐒(i)) ⋅ a ⋅ (a ^ i) ⋅ (b ^ (n −₀ i)))                                                🝖[ _≡_ ]-[ {!!} ]
  (b ^ 𝐒(n)) ⋅ ∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(𝐒(n))(𝐒(i)) ⋅ (a ^ 𝐒(i)) ⋅ (b ^ (n −₀ i)))                                                 🝖[ _≡_ ]-[]
  (b ^ 𝐒(n)) ⋅ ∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(𝐒(n))(𝐒(i)) ⋅ (a ^ 𝐒(i)) ⋅ (b ^ (𝐒(n) −₀ 𝐒(i))))                                            🝖[ _≡_ ]-[ {!!} ]
  (b ^ 𝐒(n)) ⋅ ∑(1 ‥₌ 𝐒(n)) (i ↦ 𝑐𝐶(𝐒(n))(i) ⋅ (a ^ i) ⋅ (b ^ (𝐒(n) −₀ i)))                                  🝖[ _≡_ ]-[]
  (1 ⋅ 1 ⋅ (b ^ 𝐒(n))) ⋅ ∑(1 ‥₌ 𝐒(n)) (i ↦ 𝑐𝐶(𝐒(n))(i) ⋅ (a ^ i) ⋅ (b ^ (𝐒(n) −₀ i)))                        🝖[ _≡_ ]-[]
  (𝑐𝐶(𝐒(n))(𝟎) ⋅ (a ^ 𝟎) ⋅ (b ^ (𝐒(n) −₀ 𝟎))) ⋅ ∑(1 ‥₌ 𝐒(n)) (i ↦ 𝑐𝐶(𝐒(n))(i) ⋅ (a ^ i) ⋅ (b ^ (𝐒(n) −₀ i))) 🝖[ _≡_ ]-[ {!!} ]
  ∑(𝟎 ‥₌ 𝐒(n)) (i ↦ 𝑐𝐶(𝐒(n))(i) ⋅ (a ^ i) ⋅ (b ^ (𝐒(n) −₀ i)))                                               🝖-end-}
  where
    left : _ ≡ _
    left =
      a ⋅ (∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ^ (n −₀ i)) ⋅ (b ^ i)))                                               🝖[ _≡_ ]-[ {!!} ]
      ∑(𝟎 ‥₌ n) (i ↦ a ⋅ 𝑐𝐶(n)(i) ⋅ (a ^ (n −₀ i)) ⋅ (b ^ i))                                                 🝖[ _≡_ ]-[ {!!} ]
      ∑(𝟎 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ⋅ (a ^ (n −₀ i))) ⋅ (b ^ i))                                               🝖[ _≡_ ]-[ {!!} ]
      (𝑐𝐶(n)(𝟎) ⋅ (a ⋅ (a ^ (n −₀ 𝟎))) ⋅ (b ^ 𝟎)) + ∑(1 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ⋅ (a ^ (n −₀ i))) ⋅ (b ^ i)) 🝖[ _≡_ ]-[ {!!} ]
      (1 ⋅ (a ^ 𝐒(n)) ⋅ 1) + ∑(1 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ⋅ (a ^ (n −₀ i))) ⋅ (b ^ i))                        🝖[ _≡_ ]-[ {!!} ]
      (1 ⋅ (a ^ 𝐒(n))) + ∑(1 ‥₌ n) (i ↦ 𝑐𝐶(n)(i) ⋅ (a ⋅ (a ^ (n −₀ i))) ⋅ (b ^ i))                            🝖-end
-- TODO: Maybe need another variant of ∑ where the index has a proof of it being in the range? And it is in this case used for a ⋅ (a ^ (n −₀ i)) ≡ a ^ (𝐒(n) −₀ i)
-}

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 --cubical --no-import-sorts --no-exact-split --safe #-}

module Cubical.Data.InfNat.Properties where

open import Cubical.Data.Nat as ℕ using (ℕ)
open import Cubical.Data.InfNat.Base
open import Cubical.Core.Primitives
open import Cubical.Foundations.Prelude
open import Cubical.Relation.Nullary
open import Cubical.Data.Unit
open import Cubical.Data.Empty

fromInf-def : ℕ → ℕ+∞ → ℕ
fromInf-def n ∞ = n
fromInf-def _ (fin n) = n

fin-inj : (n m : ℕ) → fin n ≡ fin m → n ≡ m
fin-inj x _ eq = cong (fromInf-def x) eq

discreteInfNat : Discrete ℕ+∞
discreteInfNat ∞ ∞ = yes (λ i → ∞)
discreteInfNat ∞ (fin _) = no λ p → subst (caseInfNat ⊥ Unit) p tt
discreteInfNat (fin _) ∞ = no λ p → subst (caseInfNat Unit ⊥) p tt
discreteInfNat (fin n) (fin m) with ℕ.discreteℕ n m
discreteInfNat (fin n) (fin m) | yes p = yes (cong fin p)
discreteInfNat (fin n) (fin m) | no ¬p = no (λ p → ¬p (fin-inj n m p))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Category
open import Oscar.Class.Congruity
open import Oscar.Class.Functor
open import Oscar.Class.HasEquivalence
open import Oscar.Class.IsCategory
open import Oscar.Class.IsFunctor
open import Oscar.Class.IsPrecategory
open import Oscar.Class.IsPrefunctor
open import Oscar.Class.Precategory
open import Oscar.Class.Prefunctor
open import Oscar.Class.Reflexivity
open import Oscar.Class.Surjection
open import Oscar.Class.Smap
open import Oscar.Class.Surjextensionality
open import Oscar.Class.Surjidentity
open import Oscar.Class.Surjtranscommutativity
open import Oscar.Class.Transassociativity
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transitivity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Transrightidentity
open import Oscar.Class.[IsExtensionB]
open import Oscar.Data.¶
open import Oscar.Data.Proposequality
open import Oscar.Data.Substitunction
open import Oscar.Data.Term
open import Oscar.Data.Vec
import Oscar.Property.Setoid.Proposequality
import Oscar.Property.Setoid.Proposextensequality
import Oscar.Property.Category.ExtensionProposextensequality
import Oscar.Property.Category.Function
import Oscar.Class.Congruity.Proposequality
import Oscar.Class.HasEquivalence.Substitunction
import Oscar.Class.Surjection.⋆
import Oscar.Class.Reflexivity.Function

module Oscar.Property.Functor.SubstitunctionExtensionTerm where

module _ {𝔭} {𝔓 : Ø 𝔭} where

  open Substitunction 𝔓
  open Term 𝔓

  private

    mutual

      𝓼urjectivitySubstitunctionExtensionTerm : Smap!.type Substitunction (Extension Term)
      𝓼urjectivitySubstitunctionExtensionTerm σ (i x) = σ x
      𝓼urjectivitySubstitunctionExtensionTerm σ leaf = leaf
      𝓼urjectivitySubstitunctionExtensionTerm σ (τ₁ fork τ₂) = 𝓼urjectivitySubstitunctionExtensionTerm σ τ₁ fork 𝓼urjectivitySubstitunctionExtensionTerm σ τ₂
      𝓼urjectivitySubstitunctionExtensionTerm σ (function p τs) = function p (𝓼urjectivitySubstitunctionExtensionTerms σ τs)

      𝓼urjectivitySubstitunctionExtensionTerms : ∀ {N} → Smap.type Substitunction (Extension $ Terms N) surjection surjection
      𝓼urjectivitySubstitunctionExtensionTerms σ ∅ = ∅
      𝓼urjectivitySubstitunctionExtensionTerms σ (τ , τs) = 𝓼urjectivitySubstitunctionExtensionTerm σ τ , 𝓼urjectivitySubstitunctionExtensionTerms σ τs

  instance

    𝓢urjectivitySubstitunctionExtensionTerm : Smap!.class Substitunction (Extension Term)
    𝓢urjectivitySubstitunctionExtensionTerm .⋆ _ _ = 𝓼urjectivitySubstitunctionExtensionTerm

    𝓢urjectivitySubstitunctionExtensionTerms : ∀ {N} → Smap!.class Substitunction (Extension $ Terms N)
    𝓢urjectivitySubstitunctionExtensionTerms .⋆ _ _ = 𝓼urjectivitySubstitunctionExtensionTerms

  instance

    𝓣ransitivitySubstitunction : Transitivity.class Substitunction
    𝓣ransitivitySubstitunction .⋆ f g = smap g ∘ f

    [IsExtensionB]Term : [IsExtensionB] Term
    [IsExtensionB]Term = ∁

    [IsExtensionB]Terms : ∀ {N} → [IsExtensionB] (Terms N)
    [IsExtensionB]Terms = ∁

  private

    mutual
      𝓼urjextensionalitySubstitunctionExtensionTerm : Surjextensionality!.TYPE Substitunction _≈_ (Extension Term) _≈_
      𝓼urjextensionalitySubstitunctionExtensionTerm p (i x) = p x
      𝓼urjextensionalitySubstitunctionExtensionTerm p leaf = ∅
      𝓼urjextensionalitySubstitunctionExtensionTerm p (s fork t) = congruity₂ _fork_ (𝓼urjextensionalitySubstitunctionExtensionTerm p s) (𝓼urjextensionalitySubstitunctionExtensionTerm p t)
      𝓼urjextensionalitySubstitunctionExtensionTerm p (function fn ts) = congruity (function fn) (𝓼urjextensionalitySubstitunctionExtensionTerms p ts)

      𝓼urjextensionalitySubstitunctionExtensionTerms : ∀ {N} → Surjextensionality!.TYPE Substitunction Proposextensequality (Extension $ Terms N) Proposextensequality
      𝓼urjextensionalitySubstitunctionExtensionTerms p ∅ = ∅
      𝓼urjextensionalitySubstitunctionExtensionTerms p (t , ts) = congruity₂ _,_ (𝓼urjextensionalitySubstitunctionExtensionTerm p t) (𝓼urjextensionalitySubstitunctionExtensionTerms p ts)

  instance

    𝓢urjextensionalitySubstitunction : Surjextensionality!.class Substitunction Proposextensequality (Extension Term) Proposextensequality
    𝓢urjextensionalitySubstitunction .⋆ _ _ _ _ = 𝓼urjextensionalitySubstitunctionExtensionTerm

    𝓢urjextensionalitySubstitunctions : ∀ {N} → Surjextensionality!.class Substitunction Proposextensequality (Extension $ Terms N) Proposextensequality
    𝓢urjextensionalitySubstitunctions .⋆ _ _ _ _ = 𝓼urjextensionalitySubstitunctionExtensionTerms

  private

    mutual

      𝓼urjtranscommutativitySubstitunctionExtensionTerm : Surjtranscommutativity.type Substitunction (Extension Term) Proposextensequality smap transitivity transitivity
      𝓼urjtranscommutativitySubstitunctionExtensionTerm _ _ (i _) = !
      𝓼urjtranscommutativitySubstitunctionExtensionTerm _ _ leaf = !
      𝓼urjtranscommutativitySubstitunctionExtensionTerm _ _ (τ₁ fork τ₂) = congruity₂ _fork_ (𝓼urjtranscommutativitySubstitunctionExtensionTerm _ _ τ₁) (𝓼urjtranscommutativitySubstitunctionExtensionTerm _ _ τ₂)
      𝓼urjtranscommutativitySubstitunctionExtensionTerm f g (function fn ts) = congruity (function fn) (𝓼urjtranscommutativitySubstitunctionExtensionTerms f g ts)

      𝓼urjtranscommutativitySubstitunctionExtensionTerms : ∀ {N} → Surjtranscommutativity.type Substitunction (Extension $ Terms N) Proposextensequality smap transitivity transitivity
      𝓼urjtranscommutativitySubstitunctionExtensionTerms _ _ ∅ = !
      𝓼urjtranscommutativitySubstitunctionExtensionTerms _ _ (τ , τs) = congruity₂ _,_ (𝓼urjtranscommutativitySubstitunctionExtensionTerm _ _ τ) (𝓼urjtranscommutativitySubstitunctionExtensionTerms _ _ τs)

  instance

    𝓢urjtranscommutativitySubstitunctionExtensionTerm : Surjtranscommutativity.class Substitunction (Extension Term) Proposextensequality smap transitivity transitivity
    𝓢urjtranscommutativitySubstitunctionExtensionTerm .⋆ = 𝓼urjtranscommutativitySubstitunctionExtensionTerm

    𝓢urjtranscommutativitySubstitunctionExtensionTerms : ∀ {N} → Surjtranscommutativity.class Substitunction (Extension $ Terms N) Proposextensequality smap transitivity transitivity
    𝓢urjtranscommutativitySubstitunctionExtensionTerms .⋆ = 𝓼urjtranscommutativitySubstitunctionExtensionTerms

  instance

    𝓣ransassociativitySubstitunction : Transassociativity!.class Substitunction _≈_
    𝓣ransassociativitySubstitunction .⋆ f g h = surjtranscommutativity g h ∘ f

    𝓣ransextensionalitySubstitunction : Transextensionality!.class Substitunction _≈_
    𝓣ransextensionalitySubstitunction .⋆ {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = surjextensionality g₁≡̇g₂ $ f₂ x

    IsPrecategorySubstitunction : IsPrecategory Substitunction _≈_ transitivity
    IsPrecategorySubstitunction = ∁

    IsPrefunctorSubstitunctionExtensionTerm : IsPrefunctor Substitunction _≈_ transitivity (Extension Term) _≈_ transitivity smap
    IsPrefunctorSubstitunctionExtensionTerm = ∁

    IsPrefunctorSubstitunctionExtensionTerms : ∀ {N} → IsPrefunctor Substitunction _≈_ transitivity (Extension $ Terms N) _≈_ transitivity smap
    IsPrefunctorSubstitunctionExtensionTerms = ∁

    𝓡eflexivitySubstitunction : Reflexivity.class Substitunction
    𝓡eflexivitySubstitunction .⋆ = i

  private

    mutual

      𝓼urjidentitySubstitunctionExtensionTerm : Surjidentity.type Substitunction (Extension Term) _≈_ smap ε ε
      𝓼urjidentitySubstitunctionExtensionTerm (i x) = ∅
      𝓼urjidentitySubstitunctionExtensionTerm leaf = ∅
      𝓼urjidentitySubstitunctionExtensionTerm (s fork t) = congruity₂ _fork_ (𝓼urjidentitySubstitunctionExtensionTerm s) (𝓼urjidentitySubstitunctionExtensionTerm t)
      𝓼urjidentitySubstitunctionExtensionTerm (function fn ts) = congruity (function fn) (𝓼urjidentitySubstitunctionExtensionTerms ts)

      𝓼urjidentitySubstitunctionExtensionTerms : ∀ {N} → Surjidentity.type Substitunction (Extension $ Terms N) _≈_ smap ε ε
      𝓼urjidentitySubstitunctionExtensionTerms ∅ = ∅
      𝓼urjidentitySubstitunctionExtensionTerms (t , ts) = congruity₂ _,_ (𝓼urjidentitySubstitunctionExtensionTerm t) (𝓼urjidentitySubstitunctionExtensionTerms ts)

  instance

    𝓢urjidentitySubstitunctionExtensionTerm : Surjidentity.class Substitunction (Extension Term) _≈_ smap ε ε
    𝓢urjidentitySubstitunctionExtensionTerm .⋆ = 𝓼urjidentitySubstitunctionExtensionTerm

    𝓢urjidentitySubstitunctionExtensionTerms : ∀ {N} → Surjidentity.class Substitunction (Extension $ Terms N) _≈_ smap ε ε
    𝓢urjidentitySubstitunctionExtensionTerms .⋆ = 𝓼urjidentitySubstitunctionExtensionTerms

    𝓣ransleftidentitySubstitunction : Transleftidentity!.class Substitunction _≈_
    𝓣ransleftidentitySubstitunction .⋆ {f = f} = surjidentity ∘ f

    𝓣ransrightidentitySubstitunction : Transrightidentity!.class Substitunction _≈_
    𝓣ransrightidentitySubstitunction .⋆ _ = !

    IsCategorySubstitunction : IsCategory Substitunction _≈_ ε transitivity
    IsCategorySubstitunction = ∁

    IsFunctorSubstitunctionExtensionTerm : IsFunctor Substitunction _≈_ ε transitivity (Extension Term) _≈_ ε transitivity smap
    IsFunctorSubstitunctionExtensionTerm = ∁

    IsFunctorSubstitunctionExtensionTerms : ∀ {N} → IsFunctor Substitunction _≈_ ε transitivity (Extension $ Terms N) _≈_ ε transitivity smap
    IsFunctorSubstitunctionExtensionTerms = ∁

module _ {𝔭} (𝔓 : Ø 𝔭) where

  open Substitunction 𝔓
  open Term 𝔓

  PrecategorySubstitunction : Precategory _ _ _
  PrecategorySubstitunction = ∁ Substitunction _≈_ transitivity

  PrefunctorSubstitunctionExtensionTerm : Prefunctor _ _ _ _ _ _
  PrefunctorSubstitunctionExtensionTerm = ∁ Substitunction _≈_ transitivity (Extension Term) _≈_ transitivity smap

  CategorySubstitunction : Category _ _ _
  CategorySubstitunction = ∁ Substitunction _≈_ ε transitivity

  FunctorSubstitunctionExtensionTerm : Functor _ _ _ _ _ _
  FunctorSubstitunctionExtensionTerm = ∁ Substitunction _≈_ ε transitivity (Extension Term) _≈_ ε transitivity smap

  module _ (N : ¶) where

    FunctorSubstitunctionExtensionTerms : Functor _ _ _ _ _ _
    FunctorSubstitunctionExtensionTerms = ∁ Substitunction _≈_ ε transitivity (Extension $ Terms N) _≈_ ε transitivity smap


text:
{-

Eilenberg–Mac Lane type K(G, 1)

-}

{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.EilenbergMacLane1.Properties where

open import Cubical.HITs.EilenbergMacLane1.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Sigma

open import Cubical.Algebra.Group.Base

open import Cubical.HITs.PropositionalTruncation as PropTrunc using (∥_∥; ∣_∣; squash)
open import Cubical.HITs.SetTruncation as SetTrunc using (∥_∥₂; ∣_∣₂; squash₂)

-- Type quotients

private
  variable
    ℓG ℓ : Level

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

  open Group G

  elimEq : {B : EM₁ G → Type ℓ}
           (Bprop : (x : EM₁ G) → isProp (B x))
           {x y : EM₁ G}
           (eq : x ≡ y)
           (bx : B x)
           (by : B y) →
           PathP (λ i → B (eq i)) bx by
  elimEq {B = B} Bprop {x = x} =
    J (λ y eq → ∀ bx by → PathP (λ i → B (eq i)) bx by) (λ bx by → Bprop x bx by)

  elimProp : {B : EM₁ G → Type ℓ}
             → ((x : EM₁ G) → isProp (B x))
             → B embase
             → (x : EM₁ G)
             → B x
  elimProp Bprop b embase = b
  elimProp Bprop b (emloop g i) = elimEq Bprop (emloop g) b b i
  elimProp Bprop b (emcomp g h i j) =
    isSet→isSetDep (λ x → isProp→isSet (Bprop x))
    (emloop g) (emloop (g + h)) (λ j → embase) (emloop h) (emcomp g h)
    (λ i → elimEq Bprop (emloop g) b b i)
    (λ i → elimEq Bprop (emloop (g + h)) b b i)
    (λ j → b) (λ j → elimEq Bprop (emloop h) b b j) i j
  elimProp Bprop b (emsquash x y p q r s i j k) =
    isOfHLevel→isOfHLevelDep 3 (λ x → isSet→isGroupoid (isProp→isSet (Bprop x)))
    _ _ _ _ (λ j k → g (r j k)) (λ j k → g (s j k)) (emsquash x y p q r s) i j k
    where
      g = elimProp Bprop b

  elimProp2 : {C : EM₁ G → EM₁ G → Type ℓ}
            → ((x y : EM₁ G) → isProp (C x y))
            → C embase embase
            → (x y : EM₁ G)
            → C x y
  elimProp2 Cprop c = elimProp (λ x → isPropΠ (λ y → Cprop x y))
                               (elimProp (λ y → Cprop embase y) c)

  elimSet : {B : EM₁ G → Type ℓ}
          → ((x : EM₁ G) → isSet (B x))
          → (b : B embase)
          → ((g : Carrier) → PathP (λ i → B (emloop g i)) b b)
          → (x : EM₁ G)
          → B x
  elimSet Bset b bloop embase = b
  elimSet Bset b bloop (emloop g i) = bloop g i
  elimSet Bset b bloop (emcomp g h i j) =
    isSet→isSetDep Bset (emloop g) (emloop (g + h)) (λ j → embase) (emloop h) (emcomp g h)
      (bloop g) (bloop (g + h)) refl (bloop h) i j
  elimSet Bset b bloop (emsquash x y p q r s i j k) =
    isOfHLevel→isOfHLevelDep 3 (λ x → isSet→isGroupoid (Bset x))
      _ _ _ _ (λ j k → g (r j k)) (λ j k → g (s j k)) (emsquash x y p q r s) i j k
    where
      g = elimSet Bset b bloop

  elim : {B : EM₁ G → Type ℓ}
       → ((x : EM₁ G) → isGroupoid (B x))
       → (b : B embase)
       → (bloop : (g : Carrier) → PathP (λ i → B (emloop g i)) b b)
       → ((g h : Carrier) → SquareP (λ i j → B (emcomp g h i j))
            (bloop g) (bloop (g + h)) (λ j → b) (bloop h))
       → (x : EM₁ G)
       → B x
  elim Bgpd b bloop bcomp embase = b
  elim Bgpd b bloop bcomp (emloop g i) = bloop g i
  elim Bgpd b bloop bcomp (emcomp g h i j) = bcomp g h i j
  elim Bgpd b bloop bcomp (emsquash x y p q r s i j k) =
     isOfHLevel→isOfHLevelDep 3 Bgpd
      _ _ _ _ (λ j k → g (r j k)) (λ j k → g (s j k)) (emsquash x y p q r s) i j k
    where
      g = elim Bgpd b bloop bcomp

  rec : {B : Type ℓ}
      → isGroupoid B
      → (b : B)
      → (bloop : Carrier → b ≡ b)
      → ((g h : Carrier) → Square (bloop g) (bloop (g + h)) refl (bloop h))
      → (x : EM₁ G)
      → B
  rec Bgpd = elim (λ _ → Bgpd)

  rec' : {B : Type ℓ}
      → isGroupoid B
      → (b : B)
      → (bloop : Carrier → b ≡ b)
      → ((g h : Carrier) → (bloop g) ∙ (bloop h) ≡ bloop (g + h))
      → (x : EM₁ G)
      → B
  rec' Bgpd b bloop p = rec Bgpd b bloop sq
    where
      module _ (g h : Carrier) where
        abstract
          sq : Square (bloop g) (bloop (g + h)) refl (bloop h)
          sq =
            transport (sym (Square≡doubleComp (bloop g) (bloop (g + h)) refl (bloop h)))
                      (refl ∙∙ bloop g ∙∙ bloop h
                        ≡⟨ doubleCompPath-elim refl (bloop g) (bloop h) ⟩
                      (refl ∙ bloop g) ∙ bloop h
                        ≡⟨ cong (_∙ bloop h) (sym (lUnit (bloop g))) ⟩
                      bloop g ∙ bloop h
                        ≡⟨ p g h ⟩
                      bloop (g + h) ∎)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical