text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Environments
--
-- This module defines the meaning of contexts, that is,
-- the type of environments that fit a context, together
-- with operations and properties of these operations.
--
-- This module is parametric in the syntax and semantics
-- of types, so it can be reused for different calculi
-- and models.
------------------------------------------------------------------------

module Base.Denotation.Environment
    (Type : Set)
    {ℓ}
    (⟦_⟧Type : Type → Set ℓ)
  where

open import Relation.Binary.PropositionalEquality

open import Base.Syntax.Context Type
open import Base.Denotation.Notation
open import Base.Data.DependentList as DependentList

private
  instance
    meaningOfType : Meaning Type
    meaningOfType = meaning ⟦_⟧Type

⟦_⟧Context : Context → Set ℓ
⟦_⟧Context = DependentList ⟦_⟧Type

instance
  meaningOfContext : Meaning Context
  meaningOfContext = meaning ⟦_⟧Context

-- VARIABLES

-- Denotational Semantics

⟦_⟧Var : ∀ {Γ τ} → Var Γ τ → ⟦ Γ ⟧ → ⟦ τ ⟧
⟦ this ⟧Var (v • ρ) = v
⟦ that x ⟧Var (v • ρ) = ⟦ x ⟧Var ρ

instance
  meaningOfVar : ∀ {Γ τ} → Meaning (Var Γ τ)
  meaningOfVar = meaning ⟦_⟧Var

-- WEAKENING

-- Remove a variable from an environment

⟦_⟧≼ : ∀ {Γ₁ Γ₂} → (Γ′ : Γ₁ ≼ Γ₂) → ⟦ Γ₂ ⟧ → ⟦ Γ₁ ⟧
⟦ ∅ ⟧≼ ∅ = ∅
⟦ keep τ • Γ′ ⟧≼ (v • ρ) = v • ⟦ Γ′ ⟧≼ ρ
⟦ drop τ • Γ′ ⟧≼ (v • ρ) = ⟦ Γ′ ⟧≼ ρ

instance
  meaningOf≼ : ∀ {Γ₁ Γ₂} → Meaning (Γ₁ ≼ Γ₂)
  meaningOf≼ = meaning ⟦_⟧≼

-- Properties

⟦∅≼Γ⟧-∅ : ∀ {Γ} ρ → ⟦ ∅≼Γ {Γ = Γ} ⟧≼ ρ ≡ ∅
⟦∅≼Γ⟧-∅ {∅} ∅ = refl
⟦∅≼Γ⟧-∅ {x • Γ} (v • ρ) = ⟦∅≼Γ⟧-∅ ρ

⟦⟧-≼-trans : ∀ {Γ₃ Γ₁ Γ₂} → (Γ′ : Γ₁ ≼ Γ₂) (Γ″ : Γ₂ ≼ Γ₃) →
   ∀ (ρ : ⟦ Γ₃ ⟧) → ⟦_⟧ {{meaningOf≼}} (≼-trans Γ′ Γ″) ρ ≡ ⟦_⟧ {{meaningOf≼}} Γ′ (⟦_⟧ {{meaningOf≼}} Γ″ ρ)
⟦⟧-≼-trans Γ′ ∅ ∅ = refl
⟦⟧-≼-trans (keep τ • Γ′) (keep .τ • Γ″) (v • ρ) = cong₂ _•_ refl (⟦⟧-≼-trans Γ′ Γ″ ρ)
⟦⟧-≼-trans (drop τ • Γ′) (keep .τ • Γ″) (v • ρ) = ⟦⟧-≼-trans Γ′ Γ″ ρ
⟦⟧-≼-trans Γ′ (drop τ • Γ″) (v • ρ) = ⟦⟧-≼-trans Γ′ Γ″ ρ

⟦⟧-≼-refl : ∀ {Γ : Context} →
  ∀ (ρ : ⟦ Γ ⟧) → ⟦_⟧ {{meaningOf≼}} ≼-refl ρ ≡ ρ
⟦⟧-≼-refl {∅} ∅ = refl
⟦⟧-≼-refl {τ • Γ} (v • ρ) = cong₂ _•_ refl (⟦⟧-≼-refl ρ)

-- SOUNDNESS of variable lifting

weaken-var-sound : ∀ {Γ₁ Γ₂ τ} (Γ′ : Γ₁ ≼ Γ₂) (x : Var Γ₁ τ) →
  ∀ (ρ : ⟦ Γ₂ ⟧) → ⟦_⟧ {{meaningOfVar}} (weaken-var Γ′ x) ρ ≡ ⟦_⟧ {{meaningOfVar}} x ( ⟦_⟧ {{meaningOf≼}} Γ′  ρ)
weaken-var-sound ∅ () ρ
weaken-var-sound (keep τ • Γ′) this (v • ρ) = refl
weaken-var-sound (keep τ • Γ′) (that x) (v • ρ) = weaken-var-sound Γ′ x ρ
weaken-var-sound (drop τ • Γ′) this (v • ρ) = weaken-var-sound Γ′ this ρ
weaken-var-sound (drop τ • Γ′) (that x) (v • ρ) = weaken-var-sound Γ′ (that x) ρ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Comonads
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

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

module Category.Comonad where

open import Level
open import Function

private
  variable
    a b c f : Level
    A : Set a
    B : Set b
    C : Set c

record RawComonad (W : Set f → Set f) : Set (suc f) where

  infixl 1 _=>>_ _=>=_
  infixr 1 _<<=_ _=<=_

  field
    extract : W A → A
    extend  : (W A → B) → (W A → W B)

  duplicate : W A → W (W A)
  duplicate = extend id

  liftW : (A → B) → W A → W B
  liftW f = extend (f ∘′ extract)

  _=>>_ : W A → (W A → B) → W B
  _=>>_ = flip extend

  _=>=_ : (W A → B) → (W B → C) → W A → C
  f =>= g = g ∘′ extend f

  _<<=_ : (W A → B) → W A → W B
  _<<=_ = extend

  _=<=_ : (W B → C) → (W A → B) → W A → C
  _=<=_ = flip _=>=_

ext: agda


text:
------------------------------------------------------------------------
-- Alternative definitions of weak bisimilarity
------------------------------------------------------------------------

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

open import Prelude

module Delay-monad.Bisimilarity.Alternative {a} {A : Type a} where

open import Equality.Propositional as E
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity
open import Delay-monad.Termination

-- An alternative definition of weak bisimilarity (discussed by
-- Capretta in "General Recursion via Coinductive Types", and
-- basically the one used in the paper "Partiality, Revisited: The
-- Partiality Monad as a Quotient Inductive-Inductive Type" by
-- Altenkirch, Danielsson and Kraus).
--
-- This definition is pointwise logically equivalent to the one above,
-- see Delay-monad.Partial-order.≈⇔≈₂.

infix 4 _≈₂_

_≈₂_ : Delay A ∞ → Delay A ∞ → Type a
x ≈₂ y = ∀ z → x ⇓ z ⇔ y ⇓ z

-- If A is a set, then this alternative definition of weak
-- bisimilarity is propositional (assuming extensionality), unlike _≈_
-- (see Delay-monad.Bisimilarity.¬-≳≈-propositional).

≈₂-propositional :
  E.Extensionality a a →
  Is-set A → ∀ {x y} → Is-proposition (x ≈₂ y)
≈₂-propositional ext A-set =
  Π-closure ext 1 λ _ →
  ⇔-closure ext 1 (Terminates-propositional A-set)
                  (Terminates-propositional A-set)

-- Another alternative definition of weak bisimilarity, basically the
-- one given by Capretta in "General Recursion via Coinductive Types".

infix 4 [_]_≈₃_ [_]_≈₃′_ _≈₃_

mutual

  data [_]_≈₃_ (i : Size) : Delay A ∞ → Delay A ∞ → Type a where
    both-terminate : ∀ {x y v} → x ⇓ v → y ⇓ v → [ i ] x ≈₃ y
    later          : ∀ {x y} →
                     [ i ] force x ≈₃′ force y →
                     [ i ] later x ≈₃  later y

  record [_]_≈₃′_ (i : Size) (x y : Delay A ∞) : Type a where
    coinductive
    field
      force : {j : Size< i} → [ j ] x ≈₃ y

open [_]_≈₃′_ public

_≈₃_ : Delay A ∞ → Delay A ∞ → Type a
_≈₃_ = [ ∞ ]_≈₃_

-- If A is inhabited, then this definition is not propositional.

¬-≈₃-propositional : A → ¬ (∀ {x y} → Is-proposition (x ≈₃ y))
¬-≈₃-propositional x =
  (∀ {x y} → Is-proposition (x ≈₃ y))  ↝⟨ (λ prop → prop) ⟩
  Is-proposition (y ≈₃ y)              ↝⟨ (_$ _) ∘ (_$ _) ⟩
  proof₁ ≡ proof₂                      ↝⟨ (λ ()) ⟩□
  ⊥                                    □
  where
  y : Delay A ∞
  y = later λ { .force → now x }

  proof₁ : y ≈₃ y
  proof₁ = both-terminate (laterʳ now) (laterʳ now)

  proof₂ : y ≈₃ y
  proof₂ = later λ { .force → both-terminate now now }

-- The last definition of weak bisimilarity given above is pointwise
-- logically equivalent to _≈_. Note that the proof is
-- size-preserving.
--
-- (Given suitable notions of extensionality the two definitions are
-- not pointwise isomorphic, because given such assumptions there is
-- only one proof of never ≈₃ never, but multiple proofs of
-- never ≈ never. However, there is no Agda proof of this claim in
-- this module.)

≈⇔≈₃ : ∀ {i x y} → [ i ] x ≈ y ⇔ [ i ] x ≈₃ y
≈⇔≈₃ = record { to = to; from = from }
  where
  mutual

    laterˡ′ : ∀ {i x x′ y} →
              x′ ≡ force x →
              [ i ] x′      ≈₃ y →
              [ i ] later x ≈₃ y
    laterˡ′ eq (both-terminate x⇓ y⇓) = both-terminate
                                          (laterʳ (subst (_⇓ _) eq x⇓))
                                          y⇓
    laterˡ′ eq (later p)              = later (laterˡ″ eq p)

    laterˡ″ : ∀ {i x x′ y} →
              later x′ ≡ x →
              [ i ] force x′ ≈₃′ y →
              [ i ] x        ≈₃′ y
    force (laterˡ″ refl p) = laterˡ′ refl (force p)

  mutual

    laterʳ′ : ∀ {i x y y′} →
              y′ ≡ force y →
              [ i ] x ≈₃ y′ →
              [ i ] x ≈₃ later y
    laterʳ′ eq (both-terminate x⇓ y⇓) = both-terminate
                                          x⇓
                                          (laterʳ (subst (_⇓ _) eq y⇓))
    laterʳ′ eq (later p)              = later (laterʳ″ eq p)

    laterʳ″ : ∀ {i x y y′} →
              later y′ ≡ y →
              [ i ] x ≈₃′ force y′ →
              [ i ] x ≈₃′ y
    force (laterʳ″ refl p) = laterʳ′ refl (force p)

  to : ∀ {i x y} → [ i ] x ≈ y → [ i ] x ≈₃ y
  to now        = both-terminate now now
  to (later  p) = later λ { .force → to (force p) }
  to (laterˡ p) = laterˡ′ refl (to p)
  to (laterʳ p) = laterʳ′ refl (to p)

  from⇓ : ∀ {i x y v} → x ⇓ v → y ⇓ v → [ i ] x ≈ y
  from⇓ now        now        = now
  from⇓ p          (laterʳ q) = laterʳ (from⇓ p q)
  from⇓ (laterʳ p) q          = laterˡ (from⇓ p q)

  from : ∀ {i x y} → [ i ] x ≈₃ y → [ i ] x ≈ y
  from (both-terminate x⇓v y⇓v) = from⇓ x⇓v y⇓v
  from (later p)                = later λ { .force → from (force p) }

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
open import prelude

-- Copied pretty much verbatim

data Term : Set where
  true : Term
  false : Term
  if_then_else_end : Term → Term → Term → Term

data Value : Term → Set where
  true : Value true
  false :  Value false

data _⟶_ : Term → Term → Set where

  E─IfTrue : ∀ {t₂ t₃} →

    -----------------------------------
    if true then t₂ else t₃ end ⟶ t₂

  E─IfFalse : ∀ {t₂ t₃} →

    -----------------------------------
    if false then t₂ else t₃ end ⟶ t₃

  E─IfCong : ∀ {t₁ t₁′ t₂ t₃} →

    (t₁ ⟶ t₁′) →
    ----------------------------------------------------------
    (if t₁ then t₂ else t₃ end ⟶ if t₁′ then t₂ else t₃ end)

data Redex  : Term → Set where

  redex : ∀ {t t′} →

    t ⟶ t′ →
    --------
    Redex(t)

-- Proving that every term is a value or a redex

data ValueOrRedex : Term → Set where

  value : ∀ {t} →

    (Value(t)) →
    ---------------
    ValueOrRedex(t)

  redex : ∀ {t t′} →

    t ⟶ t′ →
    ---------------
    ValueOrRedex(t)

valueOrRedex : (t : Term) → ValueOrRedex(t)
valueOrRedex true = value true
valueOrRedex false = value false
valueOrRedex if t₀ then t₁ else t₂ end = helper (valueOrRedex t₀) where

  helper : ∀ {t₀ t₁ t₂} → ValueOrRedex(t₀) → ValueOrRedex(if t₀ then t₁ else t₂ end)
  helper (value true) = redex E─IfTrue
  helper (value false) = redex E─IfFalse
  helper (redex r) = redex (E─IfCong r)

-- From which we get some of the theorems in the book

NormalForm : Term → Set
NormalForm(t) = Redex(t) → FALSE

thm357 : ∀ {t} → Value(t) → NormalForm(t)
thm357 true (redex ())
thm357 false (redex ())

thm358 : ∀ {t} → NormalForm(t) → Value(t)
thm358 {t} nf = helper (valueOrRedex t) nf where

  helper : ∀ {t} → ValueOrRedex(t) → NormalForm(t) → Value(t)
  helper (value v) nf = v
  helper (redex r) nf = CONTRADICTION (nf (redex r))

-- But also we can buid an interpreter.

data _⟶*_ : Term → Term → Set where

  done : ∀ {t} →

    --------
    t ⟶* t

  redex : ∀ {t t′ t″} →

    t ⟶ t′ →
    t′ ⟶* t″ →
    ----------
    t ⟶* t″

-- An interpreter result

data Result  : Term → Set where

  result : ∀ {t t′} →

    t ⟶* t′ →
    Value(t′) →
    ---------
    Result(t)

-- The interpreter just calls `valueOrRedex` until it is a value.
-- This might bot terminate!

{-# NON_TERMINATING #-}
interp : (t : Term) → Result(t)
interp t = helper₂ (valueOrRedex t) where

  helper₁ : ∀ {t t′} → (t ⟶ t′) → Result(t′) → Result(t)
  helper₁ r (result s v) = result (redex r s) v

  helper₂ : ∀ {t} → ValueOrRedex(t) → Result(t)
  helper₂ (value v)          = result done v
  helper₂ (redex {t} {t′} r) = helper₁ r (interp t′)

-- Examples

not : Term → Term
not(t) = if t then false else true end

_and_ : Term → Term → Term
s and t = if s then t else false end

_or_ : Term → Term → Term
s or t = if s then true else t end

ex : Term
ex = (true and false) or (not true)

-- Try normalizing (CTRL-C CTRL-N) `interp ex`
-- you get told the result but also the derivation tree for every step!
-- ```
-- result
-- (redex (E─IfCong E─IfTrue)
--  (redex E─IfFalse
--   (redex E─IfTrue
--    done)))
-- false
-- ```

max_stars_repo_name: asajeffrey/tapl

max_issues_repo_name: asajeffrey/tapl

max_forks_repo_name: asajeffrey/tapl


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Polynomials.Multivariate.Base where

open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly public

{-

The Multivariate Polynomials of size n over a CommRing A is a CommRing.
This version is define as an instance of the more general constructions of gradedRing.
This done by defing Poly A n = ⊕HIT_{Vec A n} A where ⊕HIT is the HIT direct sum.
Then raising the _·_ to Poly A n.

See :
-}

open import Cubical.Algebra.GradedRing.DirectSumHIT

{-

This is define very shortly as a CommRing Instances calling a general makeGradedRing functions.
And by proving the additional properties that the _·_ is commutative.
Hence the absence of real Base and Properties files.

Some more properties that are comming from the definition using the ⊕HIT
can be found in the DirectSumHIT file such as eliminator.

-}

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import HoTT
open import cohomology.Exactness
open import cohomology.Theory

module cohomology.Sn {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT

C-Sphere-≠ : (n : ℤ) (m : ℕ) → (n ≠ ℕ-to-ℤ m)
  → C n (⊙Lift (⊙Sphere m)) == Lift-Unit-group
C-Sphere-≠ n O neq = C-dimension n neq
C-Sphere-≠ n (S m) neq =
  C n (⊙Lift (⊙Sphere (S m)))
    =⟨ ! $ ⊙Susp-⊙Lift (⊙Sphere m) |in-ctx C n ⟩
  C n (⊙Susp (⊙Lift (⊙Sphere m)))
    =⟨ ! (succ-pred n) |in-ctx (λ k → C k (⊙Susp (⊙Lift (⊙Sphere m)))) ⟩
  C (succ (pred n)) (⊙Susp (⊙Lift (⊙Sphere m)))
    =⟨ group-ua (C-Susp (pred n) (⊙Lift (⊙Sphere m))) ⟩
  C (pred n) (⊙Lift (⊙Sphere m))
    =⟨ C-Sphere-≠ (pred n) m (λ p → neq (pred-injective n (ℕ-to-ℤ (S m)) p)) ⟩
  Lift-Unit-group
    ∎

C-Sphere-diag : (m : ℕ) → C (ℕ-to-ℤ m) (⊙Lift (⊙Sphere m)) == C 0 (⊙Lift ⊙S⁰)
C-Sphere-diag O = idp
C-Sphere-diag (S m) =
  C (ℕ-to-ℤ (S m)) (⊙Lift (⊙Sphere (S m)))
    =⟨ ! $ ⊙Susp-⊙Lift (⊙Sphere m) |in-ctx C (ℕ-to-ℤ (S m)) ⟩
  C (ℕ-to-ℤ (S m)) (⊙Susp (⊙Lift (⊙Sphere m)))
    =⟨ group-ua (C-Susp (ℕ-to-ℤ m) (⊙Lift (⊙Sphere m))) ⟩
  C (ℕ-to-ℤ m) (⊙Lift (⊙Sphere m))
    =⟨ C-Sphere-diag m ⟩
  C 0 (⊙Lift ⊙S⁰)
    ∎

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors
------------------------------------------------------------------------

module Data.Vec where

open import Category.Applicative
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.List as List using (List)
open import Data.Product as Prod using (∃; ∃₂; _×_; _,_)
open import Function
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

------------------------------------------------------------------------
-- Types

infixr 5 _∷_

data Vec {a} (A : Set a) : ℕ → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

infix 4 _∈_

data _∈_ {a} {A : Set a} : A → {n : ℕ} → Vec A n → Set a where
  here  : ∀ {n} {x}   {xs : Vec A n} → x ∈ x ∷ xs
  there : ∀ {n} {x y} {xs : Vec A n} (x∈xs : x ∈ xs) → x ∈ y ∷ xs

infix 4 _[_]=_

data _[_]=_ {a} {A : Set a} :
            {n : ℕ} → Vec A n → Fin n → A → Set a where
  here  : ∀ {n}     {x}   {xs : Vec A n} → x ∷ xs [ zero ]= x
  there : ∀ {n} {i} {x y} {xs : Vec A n}
          (xs[i]=x : xs [ i ]= x) → y ∷ xs [ suc i ]= x

------------------------------------------------------------------------
-- Some operations

head : ∀ {a n} {A : Set a} → Vec A (1 + n) → A
head (x ∷ xs) = x

tail : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
tail (x ∷ xs) = xs

[_] : ∀ {a} {A : Set a} → A → Vec A 1
[ x ] = x ∷ []

infixr 5 _++_

_++_ : ∀ {a m n} {A : Set a} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

infixl 4 _⊛_

_⊛_ : ∀ {a b n} {A : Set a} {B : Set b} →
      Vec (A → B) n → Vec A n → Vec B n
[]       ⊛ _        = []
(f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs)

replicate : ∀ {a n} {A : Set a} → A → Vec A n
replicate {n = zero}  x = []
replicate {n = suc n} x = x ∷ replicate x

applicative : ∀ {a n} → RawApplicative (λ (A : Set a) → Vec A n)
applicative = record
  { pure = replicate
  ; _⊛_  = _⊛_
  }

map : ∀ {a b n} {A : Set a} {B : Set b} →
      (A → B) → Vec A n → Vec B n
map f xs = replicate f ⊛ xs

zipWith : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c} →
          (A → B → C) → Vec A n → Vec B n → Vec C n
zipWith _⊕_ xs ys = replicate _⊕_ ⊛ xs ⊛ ys

zip : ∀ {a b n} {A : Set a} {B : Set b} →
      Vec A n → Vec B n → Vec (A × B) n
zip = zipWith _,_

unzip : ∀ {a b n} {A : Set a} {B : Set b} →
        Vec (A × B) n → Vec A n × Vec B n
unzip []              = [] , []
unzip ((x , y) ∷ xys) = Prod.map (_∷_ x) (_∷_ y) (unzip xys)

foldr : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → A → B n → B (suc n)) →
        B zero →
        Vec A m → B m
foldr b _⊕_ n []       = n
foldr b _⊕_ n (x ∷ xs) = x ⊕ foldr b _⊕_ n xs

foldr₁ : ∀ {a} {A : Set a} {m} →
         (A → A → A) → Vec A (suc m) → A
foldr₁ _⊕_ (x ∷ [])     = x
foldr₁ _⊕_ (x ∷ y ∷ ys) = x ⊕ foldr₁ _⊕_ (y ∷ ys)

foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → B n → A → B (suc n)) →
        B zero →
        Vec A m → B m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs

foldl₁ : ∀ {a} {A : Set a} {m} →
         (A → A → A) → Vec A (suc m) → A
foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs

concat : ∀ {a m n} {A : Set a} →
         Vec (Vec A m) n → Vec A (n * m)
concat []         = []
concat (xs ∷ xss) = xs ++ concat xss

splitAt : ∀ {a} {A : Set a} m {n} (xs : Vec A (m + n)) →
          ∃₂ λ (ys : Vec A m) (zs : Vec A n) → xs ≡ ys ++ zs
splitAt zero    xs                = ([] , xs , refl)
splitAt (suc m) (x ∷ xs)          with splitAt m xs
splitAt (suc m) (x ∷ .(ys ++ zs)) | (ys , zs , refl) =
  ((x ∷ ys) , zs , refl)

take : ∀ {a} {A : Set a} m {n} → Vec A (m + n) → Vec A m
take m xs          with splitAt m xs
take m .(ys ++ zs) | (ys , zs , refl) = ys

drop : ∀ {a} {A : Set a} m {n} → Vec A (m + n) → Vec A n
drop m xs          with splitAt m xs
drop m .(ys ++ zs) | (ys , zs , refl) = zs

group : ∀ {a} {A : Set a} n k (xs : Vec A (n * k)) →
        ∃ λ (xss : Vec (Vec A k) n) → xs ≡ concat xss
group zero    k []                  = ([] , refl)
group (suc n) k xs                  with splitAt k xs
group (suc n) k .(ys ++ zs)         | (ys , zs , refl) with group n k zs
group (suc n) k .(ys ++ concat zss) | (ys , ._ , refl) | (zss , refl) =
  ((ys ∷ zss) , refl)

-- Splits a vector into two "halves".

split : ∀ {a n} {A : Set a} → Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋
split []           = ([]     , [])
split (x ∷ [])     = (x ∷ [] , [])
split (x ∷ y ∷ xs) = Prod.map (_∷_ x) (_∷_ y) (split xs)

reverse : ∀ {a n} {A : Set a} → Vec A n → Vec A n
reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []

sum : ∀ {n} → Vec ℕ n → ℕ
sum = foldr _ _+_ 0

toList : ∀ {a n} {A : Set a} → Vec A n → List A
toList []       = List.[]
toList (x ∷ xs) = List._∷_ x (toList xs)

fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)
fromList List.[]         = []
fromList (List._∷_ x xs) = x ∷ fromList xs

-- Snoc.

infixl 5 _∷ʳ_

_∷ʳ_ : ∀ {a n} {A : Set a} → Vec A n → A → Vec A (1 + n)
[]       ∷ʳ y = [ y ]
(x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y)

initLast : ∀ {a n} {A : Set a} (xs : Vec A (1 + n)) →
           ∃₂ λ (ys : Vec A n) (y : A) → xs ≡ ys ∷ʳ y
initLast {n = zero}  (x ∷ [])         = ([] , x , refl)
initLast {n = suc n} (x ∷ xs)         with initLast xs
initLast {n = suc n} (x ∷ .(ys ∷ʳ y)) | (ys , y , refl) =
  ((x ∷ ys) , y , refl)

init : ∀ {a n} {A : Set a} → Vec A (1 + n) → Vec A n
init xs         with initLast xs
init .(ys ∷ʳ y) | (ys , y , refl) = ys

last : ∀ {a n} {A : Set a} → Vec A (1 + n) → A
last xs         with initLast xs
last .(ys ∷ʳ y) | (ys , y , refl) = y

infixl 1 _>>=_

_>>=_ : ∀ {a b m n} {A : Set a} {B : Set b} →
        Vec A m → (A → Vec B n) → Vec B (m * n)
xs >>= f = concat (map f xs)

infixl 4 _⊛*_

_⊛*_ : ∀ {a b m n} {A : Set a} {B : Set b} →
       Vec (A → B) m → Vec A n → Vec B (m * n)
fs ⊛* xs = fs >>= λ f → map f xs

-- Interleaves the two vectors.

infixr 5 _⋎_

_⋎_ : ∀ {a m n} {A : Set a} →
      Vec A m → Vec A n → Vec A (m +⋎ n)
[]       ⋎ ys = ys
(x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs)

-- A lookup function.

lookup : ∀ {a n} {A : Set a} → Fin n → Vec A n → A
lookup zero    (x ∷ xs) = x
lookup (suc i) (x ∷ xs) = lookup i xs

-- An inverse of flip lookup.

tabulate : ∀ {n a} {A : Set a} → (Fin n → A) → Vec A n
tabulate {zero}  f = []
tabulate {suc n} f = f zero ∷ tabulate (f ∘ suc)

-- Update.

infixl 6 _[_]≔_

_[_]≔_ : ∀ {a n} {A : Set a} → Vec A n → Fin n → A → Vec A n
[]       [ ()    ]≔ y
(x ∷ xs) [ zero  ]≔ y = y ∷ xs
(x ∷ xs) [ suc i ]≔ y = x ∷ xs [ i ]≔ y

-- Generates a vector containing all elements in Fin n. This function
-- is not placed in Data.Fin because Data.Vec depends on Data.Fin.
--
-- The implementation was suggested by Conor McBride ("Fwd: how to
-- count 0..n-1", http://thread.gmane.org/gmane.comp.lang.agda/2554).

allFin : ∀ n → Vec (Fin n) n
allFin _ = tabulate id


text:
module Data.Union.Relation.Binary.Subtype where

open import Data.List using (List)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)

open import Data.Union using (Union; here; there; inj)

open import Function using (_∘_; id)

open import Relation.Binary.PropositionalEquality using () renaming (refl to refl≡)

open import Level using (Level; _⊔_)

-- ----------------------------------------------------------------------
-- Subtyping

private
  variable
    a b c d f : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d

    F : A → Set f
    ts ts′ : List A

infix 4 _≼_ _,_⊢_≼_

_≼_ : Set a → Set b → Set (a ⊔ b)
A ≼ B = A → B

_,_⊢_≼_ : (A : Set a) → (F : A → Set b) → List A → List A → Set (a ⊔ b)
A , F ⊢ ts ≼ ts′ = Union A F ts ≼ Union A F ts′

refl : A ≼ A
refl = id

trans : A ≼ B → B ≼ C → A ≼ C
trans A≼B B≼C = B≼C ∘ A≼B

generalize : ts ⊆ ts′ → A , F ⊢ ts ≼ ts′
generalize ts⊆ts′ (here x) = inj (ts⊆ts′ (here refl≡)) x
generalize ts⊆ts′ (there x) = generalize (ts⊆ts′ ∘ there) x

function : C ≼ A → B ≼ D → (A → B) ≼ (C → D)
function C≼A B≼D f = B≼D ∘ f ∘ C≼A

coerce : A ≼ B → A → B
coerce = id

max_stars_repo_name: johnyob/agda-union

max_issues_repo_name: johnyob/agda-union

max_forks_repo_name: johnyob/agda-union


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

module lib.types.Suspension.Trunc where

open import lib.Basics
open import lib.NType2
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Truncation

open import lib.types.Suspension.Core

module _ {i} (A : Type i) (m : ℕ₋₂) where

  module SuspTruncSwap =
    SuspRec
      {C = Trunc (S m) (Susp A)}
      [ north ]
      [ south ]
      (Trunc-rec
        {B = [ north ] == [ south ]}
        {{has-level-apply (Trunc-level {n = S m}) [ north ] [ south ]}}
        (λ x → ap [_] (merid x)))

  Susp-Trunc-swap : Susp (Trunc m A) → Trunc (S m) (Susp A)
  Susp-Trunc-swap = SuspTruncSwap.f

  Susp-Trunc-swap-Susp-fmap-trunc : ∀ (s : Susp A) →
    Susp-Trunc-swap (Susp-fmap [_] s) == [ s ]
  Susp-Trunc-swap-Susp-fmap-trunc =
    Susp-elim
      idp
      idp $
    λ a → ↓-='-in' $ ! $
    ap (Susp-Trunc-swap ∘ Susp-fmap [_]) (merid a)
      =⟨ ap-∘ Susp-Trunc-swap (Susp-fmap [_]) (merid a) ⟩
    ap Susp-Trunc-swap (ap (Susp-fmap [_]) (merid a))
      =⟨ ap (ap Susp-Trunc-swap) (SuspFmap.merid-β [_] a) ⟩
    ap Susp-Trunc-swap (merid [ a ])
      =⟨ SuspTruncSwap.merid-β [ a ] ⟩
    ap [_] (merid a) =∎

abstract
  Susp-Trunc-swap-natural : ∀ {i} {j} {A : Type i} {B : Type j} (f : A → B) (m : ℕ₋₂)
    → Susp-Trunc-swap B m ∘ Susp-fmap (Trunc-fmap f) ∼
      Trunc-fmap (Susp-fmap f) ∘ Susp-Trunc-swap A m
  Susp-Trunc-swap-natural {A = A} {B} f m =
    Susp-elim
      idp
      idp $
    Trunc-elim {{λ t → ↓-level (=-preserves-level Trunc-level)}} $ λ s →
    ↓-='-in' $
    ap (Trunc-fmap (Susp-fmap f) ∘ Susp-Trunc-swap A m) (merid [ s ])
      =⟨ ap-∘ (Trunc-fmap (Susp-fmap f)) (Susp-Trunc-swap A m) (merid [ s ]) ⟩
    ap (Trunc-fmap (Susp-fmap f)) (ap (Susp-Trunc-swap A m) (merid [ s ]))
      =⟨ ap (ap (Trunc-fmap (Susp-fmap f))) (SuspTruncSwap.merid-β A m [ s ]) ⟩
    ap (Trunc-fmap (Susp-fmap f)) (ap [_] (merid s))
      =⟨ ∘-ap (Trunc-fmap (Susp-fmap f)) [_] (merid s) ⟩
    ap ([_] ∘ Susp-fmap f) (merid s)
      =⟨ ap-∘ [_] (Susp-fmap f) (merid s) ⟩
    ap [_] (ap (Susp-fmap f) (merid s))
      =⟨ ap (ap [_]) (SuspFmap.merid-β f s) ⟩
    ap [_] (merid (f s))
      =⟨ ! (SuspTruncSwap.merid-β B m [ f s ]) ⟩
    ap (Susp-Trunc-swap B m) (merid [ f s ])
      =⟨ ap (ap (Susp-Trunc-swap B m)) (! (SuspFmap.merid-β (Trunc-fmap f) [ s ])) ⟩
    ap (Susp-Trunc-swap B m) (ap (Susp-fmap (Trunc-fmap f)) (merid [ s ]))
      =⟨ ∘-ap (Susp-Trunc-swap B m) (Susp-fmap (Trunc-fmap f)) (merid [ s ]) ⟩
    ap (Susp-Trunc-swap B m ∘ Susp-fmap (Trunc-fmap f)) (merid [ s ]) =∎

⊙Susp-Trunc-swap : ∀ {i} (A : Type i) (m : ℕ₋₂)
  → ⊙Susp (Trunc m A) ⊙→ ⊙Trunc (S m) (⊙Susp A)
⊙Susp-Trunc-swap A m = Susp-Trunc-swap A m , idp

abstract
  ⊙Susp-Trunc-swap-natural : ∀ {i} {j} {A : Type i} {B : Type j} (f : A → B) (m : ℕ₋₂)
    → ⊙Susp-Trunc-swap B m ⊙∘ ⊙Susp-fmap (Trunc-fmap f) ==
      ⊙Trunc-fmap (⊙Susp-fmap f) ⊙∘ ⊙Susp-Trunc-swap A m
  ⊙Susp-Trunc-swap-natural f m = ⊙λ=' (Susp-Trunc-swap-natural f m) idp

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Weakening {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Weakening of valid types by one.
wk1ᵛ : ∀ {A F Γ l}
      ([Γ] : ⊩ᵛ Γ)
      ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
    → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
    → Γ ∙ F ⊩ᵛ⟨ l ⟩ wk1 A / (VPack _ _ (V∙ [Γ] [F]))
wk1ᵛ {A} [Γ] [F] [A] ⊢Δ [σ] =
  let [σA] = proj₁ ([A] ⊢Δ (proj₁ [σ]))
      [σA]′ = irrelevance′ (PE.sym (subst-wk A)) [σA]
  in  [σA]′
  ,   (λ [σ′] [σ≡σ′] →
         irrelevanceEq″ (PE.sym (subst-wk A))
                        (PE.sym (subst-wk A))
                        [σA] [σA]′
                        (proj₂ ([A] ⊢Δ (proj₁ [σ])) (proj₁ [σ′]) (proj₁ [σ≡σ′])))

-- Weakening of valid type equality by one.
wk1Eqᵛ : ∀ {A B F Γ l}
         ([Γ] : ⊩ᵛ Γ)
         ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
         ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
         ([A≡B] : Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A])
       → Γ ∙ F ⊩ᵛ⟨ l ⟩ wk1 A ≡ wk1 B / (VPack _ _ (V∙ [Γ] [F])) / wk1ᵛ {A} {F} [Γ] [F] [A]
wk1Eqᵛ {A} {B} [Γ] [F] [A] [A≡B] ⊢Δ [σ] =
  let [σA] = proj₁ ([A] ⊢Δ (proj₁ [σ]))
      [σA]′ = irrelevance′ (PE.sym (subst-wk A)) [σA]
  in  irrelevanceEq″ (PE.sym (subst-wk A))
                     (PE.sym (subst-wk B))
                     [σA] [σA]′
                     ([A≡B] ⊢Δ (proj₁ [σ]))

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

open import HoTT

{- Move (parts of) faces of a cube around -}

module lib.cubical.elims.CubeMove where

square-push-rb : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ b : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} (p₁₋ : a₁₀ == b) (q : b == a₁₁)
  → Square p₀₋ p₋₀ p₋₁ (p₁₋ ∙ q)
  → Square p₀₋ p₋₀ (p₋₁ ∙' ! q) p₁₋
square-push-rb idp idp sq = sq

private
  right-from-front-lemma : ∀ {i} {A : Type i}
    {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
    {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
    {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
    {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

    {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
    {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
    (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) -- right

    {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
    {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
    {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
    {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ (p₋₀₁ ∙ idp)} -- top
    {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ (p₋₁₁ ∙ idp)} -- bottom
    {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ (square-push-rb p₋₀₁ idp sq₋₀₋)
           (square-push-rb p₋₁₁ idp sq₋₁₋) (sq₁₋₋ ⊡h' !□h hid-square)
    → Cube sq₋₋₀ (sq₋₋₁ ⊡h hid-square) sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  right-from-front-lemma ids cu = cu

cube-right-from-front : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ b₀ b₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁}
  {p₋₀₁ : a₀₀₁ == b₀} {q₋₀₁ : b₀ == a₁₀₁}
  {r : b₀ == b₁}
  {p₋₁₁ : a₀₁₁ == b₁} {q₋₁₁ : b₁ == a₁₁₁}
  {p₁₋₁ : a₁₀₁ == a₁₁₁}
  (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ r) -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ (p₋₀₁ ∙ q₋₀₁)} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ (p₋₁₁ ∙ q₋₁₁)} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  (sq' : Square r q₋₀₁ q₋₁₁ p₁₋₁)
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ (square-push-rb p₋₀₁ q₋₀₁ sq₋₀₋)
         (square-push-rb p₋₁₁ q₋₁₁ sq₋₁₋) (sq₁₋₋ ⊡h' !□h sq')
  → Cube sq₋₋₀ (sq₋₋₁ ⊡h sq') sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
cube-right-from-front sq₋₋₁ ids cu = right-from-front-lemma sq₋₋₁ cu

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
-- test termination using structured orders

module TerminationTupledAckermann where

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

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

-- addition in tupled form

add : Nat × Nat -> Nat
add (zero   , m) = m
add (succ n , m) = succ (add (n , m))

-- ackermann in tupled form

ack : Nat × Nat -> Nat
ack (zero   , y)      = succ y
ack (succ x , zero)   = ack (x , succ zero)
ack (succ x , succ y) = ack (x , ack (succ x , y))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

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

module homotopy.EilenbergMacLane where

-- EM(G,n) when G is π₁(A,a₀)
module EMImplicit {i} (A : Type i) (cA : is-connected 0 A)
  (gA : has-level 1 A) (A-H : HSS A) where

  private
    a₀ = HSS.e A-H
    X = ⊙[ A , a₀ ]

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

  module _ (n : ℕ) where
    EM = fst (⊙EM n)
    embase = snd (⊙EM n)

  EM-level : (n : ℕ) → has-level ⟨ n ⟩ (fst (⊙EM n))
  EM-level O = gA a₀ a₀
  EM-level (S n) = Trunc-level

  EM-conn : (n : ℕ) → is-connected ⟨ n ⟩ (EM (S n))
  EM-conn n = Trunc-preserves-conn ⟨ S n ⟩
                  (transport (λ t → is-connected t (fst (⊙Susp^ n X)))
                    (+2+0 ⟨ n ⟩₋₂) (⊙Susp^-conn n cA))

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

    private
      SSn : ℕ
      SSn = S (S n)

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

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

    private
      module SS = Susp^StableSucc X cA k (S n) Skle

    abstract
      stable : πS (S k) (⊙EM (S SSn))
             == πS k (⊙EM SSn)
      stable =
        πS (S k) (⊙EM (S SSn))
          =⟨ πS-below-trunc _ _ _ (≤T-ap-S lte) ⟩
        πS (S k) (⊙Susp^ SSn X)
          =⟨ SS.stable ⟩
        πS k (⊙Susp^ (S n) X)
          =⟨ ! (πS-below-trunc _ _ _ lte) ⟩
        πS k (⊙EM SSn) ∎

  module BelowDiagonal where

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

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

  module OnDiagonal where

    π₁ : πS 0 (⊙EM 1) == πS 0 X
    π₁ = πS-below-trunc 0 1 X ≤T-refl

    private
      module Π₂ = Pi2HSusp A gA cA A-H

    π₂ : πS 1 (⊙EM 2) == πS 0 X
    π₂ =
      πS-below-trunc 1 2 (⊙Susp X) ≤T-refl
      ∙ Π₂.π₂-Suspension

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

  module AboveDiagonal where

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

  module Spectrum where

    private
      module Π₂ = Pi2HSusp A gA cA A-H

    spectrum0 : ⊙Ω (⊙EM 1) == ⊙EM 0
    spectrum0 =
      ⊙Ω (⊙EM 1)
        =⟨ ⊙ua (⊙≃-in (Trunc=-equiv _ _) idp) ⟩
      ⊙Trunc 0 (⊙Ω X)
        =⟨ ⊙ua (⊙≃-in (unTrunc-equiv _ (gA a₀ a₀)) idp) ⟩
      ⊙Ω X ∎

    spectrum1 : ⊙Ω (⊙EM 2) == ⊙EM 1
    spectrum1 =
      ⊙Ω (⊙EM 2)
        =⟨ ⊙ua (⊙≃-in (Trunc=-equiv _ _) idp) ⟩
      ⊙Trunc 1 (⊙Ω (⊙Susp X))
        =⟨ Π₂.⊙main-lemma ⟩
      X
        =⟨ ! (⊙ua (⊙≃-in (unTrunc-equiv _ gA) idp)) ⟩
      ⊙EM 1 ∎

    private
      sconn : (n : ℕ) → is-connected ⟨ S n ⟩ (fst (⊙Susp^ (S n) X))
      sconn n = transport (λ t → is-connected t (fst (⊙Susp^ (S n) X)))
                          (+2+0 ⟨ n ⟩₋₁) (⊙Susp^-conn (S n) cA)

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

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

    spectrumSS : (n : ℕ)
      → ⊙Ω (⊙EM (S (S (S n)))) == ⊙EM (S (S n))
    spectrumSS n =
      ⊙Ω (⊙EM (S (S (S n))))
        =⟨ ⊙ua (⊙≃-in (Trunc=-equiv _ _) idp) ⟩
      ⊙Trunc ⟨ S (S n) ⟩ (⊙Ω (⊙Susp^ (S (S n)) X))
        =⟨ ! (FS.⊙path n) ⟩
      ⊙EM (S (S n)) ∎

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

module EMExplicit {i} (G : Group i) (G-abelian : is-abelian G) where
  module K₁ = EM₁ G
  module HSpace = EM₁HSpace G G-abelian
  open EMImplicit K₁.EM₁ K₁.EM₁-conn K₁.emlevel HSpace.H-EM₁ public

  open BelowDiagonal public using (πS-below)

  πS-diag : (n : ℕ) → πS n (⊙EM (S n)) == G
  πS-diag n = OnDiagonal.πS-diag n ∙ K₁.π₁.π₁-iso

  open AboveDiagonal public using (πS-above)
  open Spectrum public using (spectrum)


text:
-- Andreas, 2015-07-13  Better parse errors for illegal type signatures

A : Set where B = C


text:
-- Andreas, 2019-08-10, weird error for naked ellipsis

...

-- Error (weird):
-- Missing type signature for left hand side ...
-- when scope checking the declaration
--   ...

-- When following the suggestion to give a type signature,
--
--   ... : Set
--
-- Agda says:
-- The ellipsis ... cannot have a type signature
-- <EOF><ERROR>

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Cubical.Relation.Binary.Extensionality where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Data.Sigma
open import Cubical.Relation.Binary.Base

module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where

  ≡→≺Equiv : (x y : A) → x ≡ y → ∀ z → (z ≺ x) ≃ (z ≺ y)
  ≡→≺Equiv _ _ p z = substEquiv (z ≺_) p

  isWeaklyExtensional : Type _
  isWeaklyExtensional = ∀ {x y} → isEquiv (≡→≺Equiv x y)

  isPropIsWeaklyExtensional : isProp isWeaklyExtensional
  isPropIsWeaklyExtensional = isPropImplicitΠ2 λ _ _ → isPropIsEquiv _


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Magma.Submagma where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Algebra
open import Cubical.Algebra.Magma.Morphism

open import Cubical.Relation.Unary
open import Cubical.Relation.Unary.Subtype

record IsSubmagma {c ℓ} (M : Magma c) (Member : Pred ⟨ M ⟩ ℓ) : Type (ℓ-max c ℓ) where
  constructor issubmagma

  private module M = Magma M

  field
    closed : M._•_ Preserves₂ Member

  Carrier : Type _
  Carrier = Subtype Member

  _•_ : Op₂ Carrier
  (x , subx) • (y , suby) = x M.• y , closed subx suby

  is-set : isSet Carrier
  is-set = isSetSubtype Member M.is-set

  isMagma : IsMagma Carrier _•_
  isMagma = record { is-set = is-set }

  magma : Magma _
  magma = record { isMagma = isMagma }

  open Magma magma using (set) public

record Submagma {c} (M : Magma c) ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  constructor mksubmagma

  field
    Member : Pred ⟨ M ⟩ ℓ
    isSubmagma : IsSubmagma M Member

  open IsSubmagma isSubmagma public

instance
  SubmagmaCarrier : ∀ {c ℓ} {M : Magma c} → HasCarrier (Submagma M ℓ) _
  SubmagmaCarrier = record { ⟨_⟩ = Submagma.Carrier }

module _ {ℓ} (M : Magma ℓ) where
  open Magma M

  ∅-isSubmagma : IsSubmagma M ∅
  ∅-isSubmagma = record { closed = λ () }

  ∅-submagma : Submagma M _
  ∅-submagma = record { isSubmagma = ∅-isSubmagma }

  U-isSubmagma : IsSubmagma M U
  U-isSubmagma = record {} -- trivial

  U-submagma : Submagma M _
  U-submagma = record { isSubmagma = U-isSubmagma }

isPropIsSubmagma : ∀ {c ℓ} {M : Magma c} {Member : Pred ⟨ M ⟩ ℓ} → isProp (IsSubmagma M Member)
isPropIsSubmagma {Member = Member} (issubmagma a) (issubmagma b) =
  cong issubmagma ((isPropImplicitΠ λ _ → isPropImplicitΠ λ _ → isPropΠ2 λ _ _ → isProp[ Member ] _) a b)


text:
-- Andreas, 2016-09-09 issue #2168 reported by Nisse
-- {-# OPTIONS -v tc.cover.splittree:30 -v tc.cc:40 #-}

open import Common.Equality

data Unit : Set where
  unit : Unit

data Bool : Set where
  true false : Bool

f : Unit → Bool → Bool
f unit true = false
f = λ _ _ → true

-- Testing definitional equality:

f-1 : f unit true ≡ false
f-1 = refl

f-2 : f unit false ≡ true
f-2 = refl


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

open import Relation.Binary.PropositionalEquality as P

data Phantom {i} {A : Set i} (a : A) : Set where
  phantom : Phantom a

module _ where
  private
    data #Σ-aux (A : Set) (B : A → Set) : Set where
      #pair : (x : A) → B x → #Σ-aux A B

  Σ : (A : Set) → (A → Set) → Set
  Σ A B = #Σ-aux A B

  pair : ∀ {A : Set} {B : A → Set} (x : A) → B x → Σ A B
  pair = #pair

  module ΣElim {A} {B} {S : Σ A B → Set}
    (pair* : ∀(a : A) (b : B a) → S (pair a b))
    where
      f-aux : Phantom pair* → (x : Σ A B) → S x
      f-aux x (#pair a b) = pair* a b

      f : (x : Σ A B) → S x
      f = f-aux phantom

open ΣElim public renaming (f to Σ-elim)

Σ-rec : ∀ {A} {B} {S : Set} → ((x : A) → B x → S) → Σ A B → S
Σ-rec f = Σ-elim f

isΣ-hom : ∀ {A B} {S : Set} (α : (a : A) → B a → S) →
          (Σ A B → S) → Set
isΣ-hom α f = ∀ a b → f (pair a b) ≡ α a b

Σ-rec-unique : ∀ {A B S} {α : (a : A) → B a → S} {f : Σ A B → S} → isΣ-hom α f →
               ∀ x → f x ≡ Σ-rec α x
Σ-rec-unique f-hom = Σ-elim f-hom

π₁ : ∀ {A B} → Σ A B → A
π₁ = Σ-rec (λ a _ → a)

π₂ : ∀ {A B} → (x : Σ A B) → B (π₁ x)
π₂ = Σ-elim (λ a b → b)

record ΣRecStruct (A : Set) (B : A → Set) : Set₁ where
  field
    Carrier : Set
    inj : (a : A) → B a → Carrier
    rec : ∀{S : Set} → ((a : A) → B a → S) → Carrier → S
    rec-hom : ∀ {S : Set} (α : (a : A) → B a → S) →
                 (∀ a b → rec α (inj a b) ≡ α a b)
    rec-unique : ∀ {S : Set} {α : (a : A) → B a → S} {f : Carrier → S} →
                 (∀ a b → f (inj a b) ≡ α a b) →
                 ∀ x → f x ≡ rec α x
-- open ΣRecStruct public

Σ-ΣRecStruct : ∀ A B → ΣRecStruct A B
Σ-ΣRecStruct A B = record
  { Carrier = Σ A B
  ; inj = pair
  ; rec = Σ-rec
  ; rec-hom = λ α a b → refl
  ; rec-unique = Σ-rec-unique
  }

ΣRecStruct-HasInduction : ∀{A B} → ΣRecStruct A B → Set₁
ΣRecStruct-HasInduction {A} {B} R =
  ∀ {S : Carrier → Set} (inj* : ∀(a : A) (b : B a) → S (inj a b)) →
  (x : Carrier) → S x
  where open ΣRecStruct R

-- I don't think that this is provable without resorting to π₂.
-- But I also conjecture that internally the negation is neither
-- provable.
∀ΣRecStruct-haveInduction : ∀{A B} (R : ΣRecStruct A B) →
                            ΣRecStruct-HasInduction R
∀ΣRecStruct-haveInduction R {S} inj* x = {!!}
  where
    open ΣRecStruct R

    S-aux : Set
    S-aux = Σ Carrier S

    f : Carrier → S-aux
    f = rec (λ a b → pair (inj a b) (inj* a b))

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

open import Fragment.Equational.Theory

module Fragment.Equational.FreeExtension.Synthetic (Θ : Theory) where

open import Fragment.Algebra.Signature
open import Fragment.Algebra.Algebra (Σ Θ) using (Algebra)
open import Fragment.Equational.Model Θ
open import Fragment.Equational.Coproduct Θ
open import Fragment.Equational.FreeExtension.Base Θ
open import Fragment.Algebra.Free (Σ Θ) hiding (_~_)
open import Fragment.Algebra.Homomorphism (Σ Θ)
open import Fragment.Algebra.Quotient (Σ Θ)
open import Fragment.Setoid.Morphism using (_↝_)

open import Level using (Level; _⊔_)
open import Function using (_∘_)

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Product using (proj₁; proj₂)
open import Data.Vec using (Vec; []; _∷_; map)
open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
  using (Pointwise; []; _∷_)

open import Relation.Binary using (Setoid; IsEquivalence)
import Relation.Binary.Reasoning.Setoid as Reasoning
import Relation.Binary.PropositionalEquality as PE

private
  variable
    a b ℓ₁ ℓ₂ ℓ₃ : Level

  module _ (A : Model {a} {ℓ₁}) (n : ℕ) where

    Terms : Algebra
    Terms = Free (Atoms ∥ A ∥/≈ n)

    open module T = Setoid Algebra.∥ Terms ∥/≈ renaming (_≈_ to _~_) using ()

    ∣inl∣ : ∥ A ∥ → T.Carrier
    ∣inl∣ x = atom (sta x)

    infix 4 _≈_

    data _≈_ : T.Carrier → T.Carrier → Set (a ⊔ ℓ₁) where
      refl     : ∀ {x} → x ≈ x
      sym      : ∀ {x y} → x ≈ y → y ≈ x
      trans    : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
      inherit  : ∀ {x y} → x ~ y → x ≈ y
      evaluate : ∀ {n xs} → (f : ops (Σ Θ) n)
                 → term f (map ∣inl∣ xs) ≈ ∣inl∣ (A ⟦ f ⟧ xs)
      cong     : ∀ {n} → (f : ops (Σ Θ) n)
                 → ∀ {xs ys} → Pointwise _≈_ xs ys
                 → term f xs ≈ term f ys
      axiom    : ∀ {n} → (eq : eqs Θ n) → (θ : Env Terms n)
                 → ∣ inst Terms θ ∣ (proj₁ (Θ ⟦ eq ⟧ₑ))
                   ≈ ∣ inst Terms θ ∣ (proj₂ (Θ ⟦ eq ⟧ₑ))

    ≈-isEquivalence : IsEquivalence _≈_
    ≈-isEquivalence = record { refl  = refl
                             ; sym   = sym
                             ; trans = trans
                             }

    instance
      ≈-isDenom : IsDenominator Terms _≈_
      ≈-isDenom = record { isEquivalence = ≈-isEquivalence
                         ; isCompatible  = cong
                         ; isCoarser     = inherit
                         }

    module N = Setoid (∥ Terms ∥/ _≈_)

    Syn-models : Models (Terms / _≈_)
    Syn-models eq θ = begin
        ∣ inst (Terms / _≈_) θ ∣ lhs
      ≈⟨ N.sym (lemma {x = lhs}) ⟩
        ∣ inst Terms θ ∣ lhs
      ≈⟨ axiom eq θ ⟩
        ∣ inst Terms θ ∣ rhs
      ≈⟨ lemma {x = rhs} ⟩
        ∣ inst (Terms / _≈_) θ ∣ rhs
      ∎
      where open Reasoning (∥ Terms ∥/ _≈_)

            lhs = proj₁ (Θ ⟦ eq ⟧ₑ)
            rhs = proj₂ (Θ ⟦ eq ⟧ₑ)

            lemma = inst-universal (Terms / _≈_) θ
                      {h = (inc Terms _≈_) ⊙ (inst Terms θ) }
                      (λ x → PE.refl)

    Syn-isModel : IsModel (∥ Terms ∥/ _≈_)
    Syn-isModel = record { isAlgebra = Terms / _≈_ -isAlgebra
                         ; models    = Syn-models
                         }

    Syn : Model
    Syn = record { ∥_∥/≈   = ∥ Terms ∥/ _≈_
                 ; isModel = Syn-isModel
                 }

    ∣inl∣-cong : Congruent ≈[ A ] _≈_ ∣inl∣
    ∣inl∣-cong p = inherit (atom (sta p))

    ∣inl∣-hom : Homomorphic ∥ A ∥ₐ ∥ Syn ∥ₐ ∣inl∣
    ∣inl∣-hom f xs = evaluate f

    ∣inl∣⃗ : ∥ A ∥/≈ ↝ ∥ Syn ∥/≈
    ∣inl∣⃗ = record { ∣_∣      = ∣inl∣
                    ; ∣_∣-cong = ∣inl∣-cong
                    }

    inl : ∥ A ∥ₐ ⟿ ∥ Syn ∥ₐ
    inl = record { ∣_∣⃗    = ∣inl∣⃗
                 ; ∣_∣-hom = ∣inl∣-hom
                 }

    inr : ∥ J n ∥ₐ ⟿ ∥ Syn ∥ₐ
    inr = interp Syn (λ n → atom (dyn n))

    module _
      (X : Model {b} {ℓ₂})
      (f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ)
      (g : ∥ J n ∥ₐ ⟿ ∥ X ∥ₐ)
      where

      private module X = Setoid ∥ X ∥/≈
      open Reasoning ∥ X ∥/≈

      resid : Terms ⟿ ∥ X ∥ₐ
      resid = subst ∥ X ∥ₐ ∣ f ∣⃗ (λ n → ∣ g ∣ (atom (dyn n)))

      ∣resid∣-map-∣inl∣ : ∀ {m} {xs : Vec ∥ A ∥ m}
                          → Pointwise ≈[ X ]
                                      (map ∣ resid ∣ (map ∣inl∣ xs))
                                      (map ∣ f ∣ xs)
      ∣resid∣-map-∣inl∣ {xs = []}     = []
      ∣resid∣-map-∣inl∣ {xs = x ∷ xs} = X.refl ∷ ∣resid∣-map-∣inl∣

      mutual
        ∣resid∣-args-cong : ∀ {m} {xs ys : Vec ∥ Syn ∥ m}
                            → Pointwise _≈_ xs ys
                            → Pointwise ≈[ X ] (map ∣ resid ∣ xs)
                                               (map ∣ resid ∣ ys)
        ∣resid∣-args-cong []       = []
        ∣resid∣-args-cong (p ∷ ps) = ∣resid∣-cong p ∷ ∣resid∣-args-cong ps

        ∣resid∣-cong : Congruent _≈_ ≈[ X ] ∣ resid ∣
        ∣resid∣-cong refl        = X.refl
        ∣resid∣-cong (sym p)     = X.sym (∣resid∣-cong p)
        ∣resid∣-cong (trans p q) = X.trans (∣resid∣-cong p) (∣resid∣-cong q)
        ∣resid∣-cong (inherit p) = ∣ resid ∣-cong p
        ∣resid∣-cong (evaluate {xs = xs} op) = begin
            ∣ resid ∣ (term op (map ∣inl∣ xs))
          ≈⟨ X.sym (∣ resid ∣-hom op (map ∣inl∣ xs)) ⟩
            X ⟦ op ⟧ (map ∣ resid ∣ (map ∣inl∣ xs))
          ≈⟨ (X ⟦ op ⟧-cong) ∣resid∣-map-∣inl∣ ⟩
            X ⟦ op ⟧ (map ∣ f ∣ xs)
          ≈⟨ ∣ f ∣-hom op xs ⟩
            ∣ f ∣ (A ⟦ op ⟧ xs)
          ∎
        ∣resid∣-cong (cong f {xs = xs} {ys = ys} ps) = begin
            ∣ resid ∣ (term f xs)
          ≈⟨ X.sym (∣ resid ∣-hom f xs) ⟩
            X ⟦ f ⟧ (map ∣ resid ∣ xs)
          ≈⟨ (X ⟦ f ⟧-cong) (∣resid∣-args-cong ps) ⟩
            X ⟦ f ⟧ (map ∣ resid ∣ ys)
          ≈⟨ ∣ resid ∣-hom f ys ⟩
            ∣ resid ∣ (term f ys)
          ∎
        ∣resid∣-cong (axiom eq θ) = begin
            ∣ resid ∣ (∣ inst Terms θ ∣ lhs)
          ≈⟨ inst-assoc Terms θ resid {lhs} ⟩
            ∣ inst ∥ X ∥ₐ (∣ resid ∣ ∘ θ) ∣ lhs
          ≈⟨ ∥ X ∥ₐ-models eq (∣ resid ∣ ∘ θ) ⟩
            ∣ inst ∥ X ∥ₐ (∣ resid ∣ ∘ θ) ∣ rhs
          ≈⟨ X.sym (inst-assoc Terms θ resid {rhs}) ⟩
            ∣ resid ∣ (∣ inst Terms θ ∣ rhs)
          ∎
          where lhs = proj₁ (Θ ⟦ eq ⟧ₑ)
                rhs = proj₂ (Θ ⟦ eq ⟧ₑ)

      _[_,_] : ∥ Syn ∥ₐ ⟿ ∥ X ∥ₐ
      _[_,_] = factor Terms _≈_ resid ∣resid∣-cong

    module _
      {X : Model {b} {ℓ₂}}
      {f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ}
      {g : ∥ J n ∥ₐ ⟿ ∥ X ∥ₐ}
      where

      private module X = Setoid ∥ X ∥/≈
      open Reasoning ∥ X ∥/≈

      commute₁ : X [ f , g ] ⊙ inl ≗ f
      commute₁ = X.refl

      mutual
        map-commute₂ : ∀ {m} {xs : Vec ∥ J n ∥ m}
                       → Pointwise ≈[ X ]
                                   (map ∣ X [ f , g ] ⊙ inr ∣ xs)
                                   (map ∣ g ∣ xs)
        map-commute₂ {xs = []}     = []
        map-commute₂ {xs = x ∷ xs} = commute₂ ∷ map-commute₂

        commute₂ : X [ f , g ] ⊙ inr ≗ g
        commute₂ {atom (dyn _)} = X.refl
        commute₂ {term op xs}    = begin
            ∣ X [ f , g ] ⊙ inr ∣ (term op xs)
          ≈⟨ X.sym (∣ X [ f , g ] ⊙ inr ∣-hom op xs) ⟩
            X ⟦ op ⟧ (map ∣ X [ f , g ] ⊙ inr ∣ xs)
          ≈⟨ (X ⟦ op ⟧-cong) map-commute₂ ⟩
            X ⟦ op ⟧ (map ∣ g ∣ xs)
          ≈⟨ ∣ g ∣-hom op xs ⟩
            ∣ g ∣ (term op xs)
          ∎

      module _
        {h : ∥ Syn ∥ₐ ⟿ ∥ X ∥ₐ}
        (c₁ : h ⊙ inl ≗ f)
        (c₂ : h ⊙ inr ≗ g)
        where

        mutual
          map-universal : ∀ {m} {xs : Vec ∥ Syn ∥ m}
                          → Pointwise ≈[ X ]
                                      (map ∣ X [ f , g ] ∣ xs)
                                      (map ∣ h ∣ xs)
          map-universal {xs = []}     = []
          map-universal {xs = x ∷ xs} = universal ∷ map-universal

          universal : X [ f , g ] ≗ h
          universal {atom (sta x)} = X.sym c₁
          universal {atom (dyn x)} = begin
              ∣ X [ f , g ] ∣ (atom (dyn x))
            ≈⟨ commute₂ ⟩
              ∣ g ∣ (atom (dyn x))
            ≈⟨ X.sym c₂ ⟩
              ∣ h ∣ (atom (dyn x))
            ∎
          universal {term op xs}   = begin
              ∣ X [ f , g ] ∣ (term op xs)
            ≈⟨ X.sym (∣ X [ f , g ] ∣-hom op xs) ⟩
              X ⟦ op ⟧ (map ∣ X [ f , g ] ∣ xs)
            ≈⟨ (X ⟦ op ⟧-cong) map-universal ⟩
              X ⟦ op ⟧ (map ∣ h ∣ xs)
            ≈⟨ ∣ h ∣-hom op xs ⟩
              ∣ h ∣ (term op xs)
            ∎

    isFrex : IsCoproduct A (J n) Syn
    isFrex =
      record { inl       = inl
             ; inr       = inr
             ; _[_,_]    = _[_,_]
             ; commute₁  = λ {_ _ X f g} → commute₁ {X = X} {f} {g}
             ; commute₂  = λ {_ _ X f g} → commute₂ {X = X} {f} {g}
             ; universal = λ {_ _ X f g h} → universal {X = X} {f} {g} {h}
             }

SynFrex : FreeExtension
SynFrex = record { _[_]        = Syn
                 ; _[_]-isFrex = isFrex
                 }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-# OPTIONS -v tc.with.display:30 #-}
-- {-# OPTIONS -v tc.with.strip:30 #-}

open import Common.Product
open import Common.Prelude
open import Common.Equality

postulate
  p : Nat → Nat

-- g : Nat → Nat × Nat
-- g x .proj₁ with p x
-- g x .proj₁ | 0 = 1
-- g x .proj₁ | suc y = 0
-- g x .proj₂ = suc x

-- h : Nat → Nat × Nat
-- h x .proj₁ with p x
-- h x .proj₁ | 0 = 1
-- proj₁ (h x) | suc y = 0
-- h x .proj₂ = suc x

f : Nat → Nat × Nat
f x .proj₁ with p x
... | 0 = 1
... | suc y = 0
f x .proj₂ = suc x

test : f 0 ≡ (0 , 1)
test = refl

-- EXPECTED ERROR:
-- f 0 .proj₁ | p 0 != zero of type Nat
-- when checking that the expression refl has type f 0 ≡ (0 , 1)


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

open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules
open import Sets ℕ eqdecℕ

{- PS-contexts -}
module CaTT.Ps-contexts where

  {- Rules for PS-contexts -}
  data _⊢ps_#_ : Pre-Ctx → ℕ → Pre-Ty → Set₁ where
    pss : (nil :: (O , ∗)) ⊢ps O # ∗
    psd : ∀ {Γ f A x y} → Γ ⊢ps f # (⇒ A (Var x) (Var y)) → Γ ⊢ps y # A
    pse : ∀ {Γ x A y z C t Tt} → Γ ⊢ps x # A  →  y == length Γ → z == S (length Γ) → C == ⇒ A (Var x) (Var y) → z == t → C == Tt → ((Γ :: (y , A)) :: (z , C)) ⊢ps t # Tt

  data _⊢ps : Pre-Ctx → Set₁ where
    ps : ∀ {Γ x} → Γ ⊢ps x # ∗ → Γ ⊢ps

  psd↓ : ∀ {Γ f A x y z} → (Γ⊢ps₁ : Γ ⊢ps f # (⇒ A (Var x) (Var z))) → (Γ⊢ps₂ : Γ ⊢ps f # (⇒ A (Var y) (Var z))) → (p : x == y) → transport p Γ⊢ps₁ == Γ⊢ps₂ → psd Γ⊢ps₁ == psd Γ⊢ps₂
  psd↓ Γ⊢ps₁ .Γ⊢ps₁ idp idp = idp

  pse↓ : ∀ {Γ A B C x y a f z} → (Γ⊢ps₁ : Γ ⊢ps x # A) (a= : a == length Γ) (f= : f == S (length Γ)) (B= : B == ⇒ A (Var x) (Var a)) (z= : f == z) (C= : B == C)
                                → (Γ⊢ps₂ : Γ ⊢ps y # A) (a=' : a == length Γ) (f=' : f == S (length Γ)) (B=' : B == ⇒ A (Var y) (Var a)) (z=' : f == z) (C=' : B == C)
                                → (p : x == y)  → transport p Γ⊢ps₁ == Γ⊢ps₂ → (pse Γ⊢ps₁ a= f= B= z= C=) == (pse Γ⊢ps₂ a=' f=' B=' z=' C=')
  pse↓ _ _ _ _ _ _ _ _ _ _ _ _ idp idp = ap⁶ pse idp (is-prop-has-all-paths (is-setℕ _ _) _ _)
                                                      (is-prop-has-all-paths (is-setℕ _ _) _ _)
                                                      (is-prop-has-all-paths (eqdec-is-set eqdec-PreTy _ _) _ _)
                                                      (is-prop-has-all-paths (is-setℕ _ _) _ _)
                                                      (is-prop-has-all-paths (eqdec-is-set eqdec-PreTy _ _) _ _)

  ps↓ : ∀ {Γ x y} → (Γ⊢ps₁ : Γ ⊢ps x # ∗) → (Γ⊢ps₂ : Γ ⊢ps y # ∗)
                  → (p : x == y)  → transport {B = λ z → Γ ⊢ps z # ∗} p Γ⊢ps₁ == Γ⊢ps₂ → (ps Γ⊢ps₁) == (ps Γ⊢ps₂)
  ps↓ _ _ idp idp = idp

  {- PS-contexts define valid contexts -}
  Γ⊢ps→Γ⊢ : ∀ {Γ} → Γ ⊢ps → Γ ⊢C
  Γ⊢psx:A→Γ⊢x:A : ∀ {Γ x A} → Γ ⊢ps x # A → Γ ⊢t (Var x) # A

  Γ⊢ps→Γ⊢ (ps Γ⊢psx) = Γ⊢t:A→Γ⊢ (Γ⊢psx:A→Γ⊢x:A Γ⊢psx)
  Γ⊢psx:A→Γ⊢x:A pss = var (cc ec (ob ec) idp) (inr (idp , idp))
  Γ⊢psx:A→Γ⊢x:A (psd Γ⊢psf:x⇒y) with Γ⊢t:A→Γ⊢A (Γ⊢psx:A→Γ⊢x:A Γ⊢psf:x⇒y)
  Γ⊢psx:A→Γ⊢x:A (psd Γ⊢psf:x⇒y) | ar _ Γ⊢y:A = Γ⊢y:A
  Γ⊢psx:A→Γ⊢x:A (pse Γ⊢psx:A idp idp idp idp idp) with (cc (Γ⊢t:A→Γ⊢ (Γ⊢psx:A→Γ⊢x:A Γ⊢psx:A)) (Γ⊢t:A→Γ⊢A (Γ⊢psx:A→Γ⊢x:A Γ⊢psx:A)) idp)
  ...                          | Γ,y:A⊢ = var (cc Γ,y:A⊢ (ar (wkt (Γ⊢psx:A→Γ⊢x:A Γ⊢psx:A) Γ,y:A⊢) (var Γ,y:A⊢ (inr (idp , idp)))) idp) (inr (idp , idp))

  Γ⊢psx:A→Γ⊢ : ∀ {Γ x A} → Γ ⊢ps x # A → Γ ⊢C
  Γ⊢psx:A→Γ⊢ Γ⊢psx:A = Γ⊢t:A→Γ⊢ (Γ⊢psx:A→Γ⊢x:A Γ⊢psx:A)

  -- some renamings so that useful lemmas are faster to write
  -- TODO restrict these as local names
  psv : ∀ {Γ x A} → Γ ⊢ps x # A → Γ ⊢C --psvalid
  psv Γ⊢ps = Γ⊢psx:A→Γ⊢ Γ⊢ps

  psvar : ∀ {Γ x A} → Γ ⊢ps x # A → Γ ⊢t (Var x) # A
  psvar Γ⊢psx = Γ⊢psx:A→Γ⊢x:A Γ⊢psx

  ps-ctx : Set₁
  ps-ctx = Σ Pre-Ctx (λ Γ → Γ ⊢ps)

  {- Eric's trick : is a src-var -}
  srcᵢ-var : ∀ {Γ x A} → ℕ → Γ ⊢ps x # A → list ℕ
  srcᵢ-var i pss = if i ≡ 0 then nil else (nil :: 0)
  srcᵢ-var i (psd Γ⊢psx) = srcᵢ-var i Γ⊢psx
  srcᵢ-var i (pse {Γ = Γ} {A = A} Γ⊢psx idp idp idp idp idp) with dec-≤ i (S (dim A))
  ... | inl i≤SdimA = srcᵢ-var i Γ⊢psx
  ... | inr SdimA<i = (srcᵢ-var i Γ⊢psx :: length Γ) :: (S (length Γ))

  drop : ∀ {i} {A : Set i} → list A → list A
  drop nil = nil
  drop (l :: a) = l

  tgtᵢ-var : ∀ {Γ x A} → ℕ → Γ ⊢ps x # A → list ℕ
  tgtᵢ-var i pss = if i ≡ 0 then nil else (nil :: 0)
  tgtᵢ-var i (psd Γ⊢psx) = tgtᵢ-var i Γ⊢psx
  tgtᵢ-var i (pse {Γ = Γ} {A = A} Γ⊢psx idp idp idp idp idp) with dec-≤ i (S (dim A))
  ... | inl i≤SdimA = if i ≡ S (dim A) then drop(tgtᵢ-var i Γ⊢psx) :: length Γ else tgtᵢ-var i Γ⊢psx
  ... | inr SdimA<i = (tgtᵢ-var i Γ⊢psx :: length Γ) :: (S (length Γ))

  src-var : (Γ : ps-ctx) → set
  src-var (Γ , ps Γ⊢psx) = set-of-list (srcᵢ-var (dimC Γ) Γ⊢psx)

  tgt-var : (Γ : ps-ctx) → set
  tgt-var (Γ , ps Γ⊢psx) = set-of-list (tgtᵢ-var (dimC Γ) Γ⊢psx)

  dim-psx-not-𝔻0 : ∀ {Γ x A} → (Γ⊢ps : Γ ⊢ps x # A) → (Γ ≠ (nil :: (0 , ∗))) → 0 < dimC Γ
  dim-psx-not-𝔻0 {.(nil :: (0 , ∗))} {.0} {.∗} pss Γ≠𝔻0 = ⊥-elim (Γ≠𝔻0 idp)
  dim-psx-not-𝔻0 {Γ} {x} {A} (psd Γ⊢psx) Γ≠𝔻0 = dim-psx-not-𝔻0 Γ⊢psx Γ≠𝔻0
  dim-psx-not-𝔻0 {_} {x} {A} (pse {Γ = Γ} Γ⊢psx idp idp idp idp idp) Γ+≠𝔻0 = ≤T (S≤ (0≤ _)) (m≤max (max (dimC Γ) _) (dim A))

  dim-ps-not-𝔻0 : ∀ {Γ} → (Γ⊢ps : Γ ⊢ps) → (Γ ≠ (nil :: (0 , ∗))) → 0 < dimC Γ
  dim-ps-not-𝔻0 (ps Γ⊢psx) Γ≠𝔻0 = dim-psx-not-𝔻0 Γ⊢psx Γ≠𝔻0

  dim-dangling : ∀ {Γ x A} → Γ ⊢ps x # A → dim A ≤ dimC Γ
  dim-dangling pss = 0≤ _
  dim-dangling (psd Γ⊢psf) = Sn≤m→n≤m (dim-dangling Γ⊢psf)
  dim-dangling (pse {Γ = Γ} Γ⊢psx idp idp idp idp idp) = m≤max (max (dimC Γ) _) _

  {- Definition of a few ps-contexts and their source and target in the theory CaTT -}
  -- It is not necessary to define the pre contexts, as they can be infered with the derivation tree. We do it just as a sanity check
  Pre-Γc : Pre-Ctx
  Pre-Γc = ((((nil :: (0 , ∗)) :: (1 , ∗)) :: (2 , ⇒ ∗ (Var 0) (Var 1))) :: (3 , ∗)) :: (4 , ⇒ ∗ (Var 1) (Var 3))

  Pre-Γw : Pre-Ctx
  Pre-Γw = ((((((nil :: (0 , ∗)) :: (1 , ∗)) :: (2 , ⇒ ∗ (Var 0) (Var 1))) :: (3 , ⇒ ∗ (Var 0) (Var 1))) :: (4 , ⇒ (⇒ ∗ (Var 0) (Var 1)) (Var 2) (Var 3))) :: (5 , ∗)) :: (6 , ⇒ ∗ (Var 1) (Var 5))

  Pre-Γ₁ : Pre-Ctx
  Pre-Γ₁ = ((nil :: (0 , ∗)) :: (1 , ∗)) :: (2 , ⇒ ∗ (Var 0) (Var 1))

  Pre-Γ₂ : Pre-Ctx
  Pre-Γ₂ = ((((nil :: (0 , ∗)) :: (1 , ∗)) :: (2 , ⇒ ∗ (Var 0) (Var 1))) :: (3 , ⇒ ∗ (Var 0) (Var 1))) :: (4 , ⇒ (⇒ ∗ (Var 0) (Var 1)) (Var 2) (Var 3))

  Γc⊢ps : Pre-Γc ⊢ps
  Γc⊢ps = ps (psd (pse (psd (pse pss idp idp idp idp idp)) idp idp idp idp idp))

  Γw⊢ps : Pre-Γw ⊢ps
  Γw⊢ps = ps (psd (pse (psd (psd (pse (pse pss idp idp idp idp idp) idp idp idp idp idp))) idp idp idp idp idp))

  Γ₁⊢ps : Pre-Γ₁ ⊢ps
  Γ₁⊢ps = ps (psd (pse pss idp idp idp idp idp))

  Γ₂⊢ps : Pre-Γ₂ ⊢ps
  Γ₂⊢ps = ps (psd (psd (pse (pse pss idp idp idp idp idp) idp idp idp idp idp)))

  Γc : ps-ctx
  Γc = _ , Γc⊢ps

  Γw : ps-ctx
  Γw = _ , Γw⊢ps

  Γ₁ : ps-ctx
  Γ₁ = _ , Γ₁⊢ps

  Γ₂ : ps-ctx
  Γ₂ = _ , Γ₂⊢ps

  src-Γc : src-var Γc ≗ singleton 0
  src-Γc = (λ _ x → x) , λ _ x → x

  tgt-Γc : tgt-var Γc ≗ singleton 3
  tgt-Γc = (λ _ x → x) , λ _ x → x

  src-Γ₁ : src-var Γ₁ ≗ singleton 0
  src-Γ₁ = (λ _ x → x) , λ _ x → x

  tgt-Γ₁ : tgt-var Γ₁ ≗ singleton 1
  tgt-Γ₁ = (λ _ x → x) , λ _ x → x

  src-Γ₂ : src-var Γ₂ ≗ set-of-list (((nil :: 0) :: 1) :: 2)
  src-Γ₂ = (λ _ x → x) , λ _ x → x

  tgt-Γ₂ : tgt-var Γ₂ ≗ set-of-list (((nil :: 0) :: 1) :: 3)
  tgt-Γ₂ = (λ _ x → x) , λ _ x → x

  src-Γw : src-var Γw ≗ set-of-list (((((nil :: 0) :: 1) :: 2) :: 5) :: 6)
  src-Γw = (λ _ x → x) , λ _ x → x

  tgt-Γw : tgt-var Γw ≗ set-of-list (((((nil :: 0) :: 1) :: 3) :: 5) :: 6)
  tgt-Γw = (λ _ x → x) , λ _ x → x

-- TODO : cleanup and unite these two lemmas
  x∉ : ∀ {Γ x} → Γ ⊢C → length Γ ≤ x → (∀ {A} → ¬ (Γ ⊢t (Var x) # A))
  x∉ (cc Γ⊢ _ idp) l≤x (var _ (inl x∈Γ)) = x∉ Γ⊢ (Sn≤m→n≤m l≤x) (var Γ⊢ x∈Γ)
  x∉ (cc Γ⊢ _ idp) l≤x (var _ (inr (idp , idp))) = Sn≰n _ l≤x

  l∉ : ∀ {Γ x} → Γ ⊢C → length Γ ≤ x → ¬ (x ∈ Γ)
  l∉ (cc Γ⊢ _ idp) l≤x (inl x∈Γ) = l∉ Γ⊢ (Sn≤m→n≤m l≤x) x∈Γ
  l∉ (cc Γ⊢ _ idp) l≤x (inr idp) = Sn≰n _ l≤x

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


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

module Fragment.Tactic.Fragment where

open import Reflection hiding (name; Type; _≟_)
open import Reflection.Term using (_≟_)

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

open import Data.Bool using (Bool; _∨_; true; false; if_then_else_)
open import Data.Nat using (ℕ)
open import Data.List using (List; []; _∷_; map; sum; length)
open import Data.Vec using (fromList)
open import Data.Product using (_×_; _,_)
open import Data.Unit using (⊤; tt)
open import Data.String using (String; _++_)
open import Data.Maybe using (Maybe; just; nothing)

open import Fragment.Tactic.Utils

open import Fragment.Equational.Theory
open import Fragment.Equational.Model
open import Fragment.Equational.FreeExtension hiding (reduce)
open import Fragment.Algebra.Signature
import Fragment.Algebra.Free as Free

read-goal : List (Arg Term) → TC (Term × List (Arg Term))
read-goal (vArg x ∷ xs) = return (x , xs)
read-goal (_ ∷ xs)      = read-goal xs
read-goal []            = typeError (strErr "failed to read goal" ∷ [])

read-goals : List (Arg Term) → TC (Term × Term)
read-goals xs = do (fst , xs) ← read-goal xs
                   (snd , _) ← read-goal xs
                   return (fst , snd)

extract-goals : Term → TC (Term × Term)
extract-goals (var _ args)  = read-goals args
extract-goals (con _ args)  = read-goals args
extract-goals (def _ args)  = read-goals args
extract-goals (meta _ args) = read-goals args
extract-goals t             =
  typeError (strErr "can't read goals from" ∷ termErr t ∷ [])

record Operator : Set where
  constructor operator
  field
    name       : Name
    normalised : Term
    arity      : ℕ

open Operator

record CoreCtx : Set where
  field
    signature : Term
    theory    : Term
    model     : Term
    carrier   : Term
    frex      : Term

record GlobalCtx : Set where
  field
    core      : CoreCtx
    operators : List Operator

    telescope : List (Arg String)
    lhs       : Term
    rhs       : Term

  open CoreCtx core public

pattern modelType Θ a ℓ = def (quote Model) (vArg Θ ∷ hArg a ∷ hArg ℓ ∷ [])

ctx : Name → Term → Term → TC GlobalCtx
ctx frex model goal
  = do τ ← inferType model
       γ ← inferType goal

       signature ← extract-Σ τ
       theory ← extract-Θ τ
       carrier ← normalise (def (quote ∥_∥) (vra theory ∷ vra model ∷ []))

       let core = record { signature = signature
                         ; theory    = theory
                         ; model     = model
                         ; carrier   = carrier
                         ; frex      = def frex []
                         }

       operators ← extract-ops core

       (inner , telescope) ← strip-telescope γ
       (lhs , rhs) ← extract-goals inner

       return (record { core      = core
                      ; operators = operators
                      ; telescope = telescope
                      ; lhs       = lhs
                      ; rhs       = rhs
                      })

  where modelErr : ∀ {a} {A : Set a} → Term → String → TC A
        modelErr t err =
          typeError ( termErr t
                    ∷ strErr "isn't a"
                    ∷ nameErr (quote Model)
                    ∷ strErr ("(" ++ err ++ ")")
                    ∷ []
                    )

        extract-Σ : Term → TC Term
        extract-Σ (modelType Θ _ _) = normalise (def (quote Theory.Σ) (vra Θ ∷ []))
        extract-Σ t                 = modelErr t "when extracting the signature"

        extract-Θ : Term → TC Term
        extract-Θ (modelType Θ _ _) = normalise Θ
        extract-Θ t                 = modelErr t "when extracting the theory"

        extract-arity : CoreCtx → Name → TC ℕ
        extract-arity ctx op
          = do τ ← inferType (def (quote _⟦_⟧_)
                                  ( vra (CoreCtx.theory ctx)
                                  ∷ vra (CoreCtx.model ctx)
                                  ∷ vra (con op [])
                                  ∷ []
                                  ))
               α ← extract-type-arg τ
               vec-len α

        extract-interp : CoreCtx → Name → ℕ → TC Term
        extract-interp ctx op arity
          = do let t = def (quote _⟦_⟧_)
                           ( vra (CoreCtx.theory ctx)
                           ∷ vra (CoreCtx.model ctx)
                           ∷ vra (con op [])
                           ∷ []
                           )
               normalise (n-ary arity (apply t (vra (vec (debrujin arity)) ∷ [])))

        extract-ops : CoreCtx → TC (List Operator)
        extract-ops ctx
          = do ops ← normalise (def (quote ops) (vra (CoreCtx.signature ctx) ∷ []))
               symbols ← extract-constructors ops
               arities ← listTC (map (extract-arity ctx) symbols)
               interps ← listTC (mapList (map (extract-interp ctx) symbols) arities)
               return (mapList (mapList (map operator symbols) interps) arities)

record FoldCtx {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor foldCtx
  field
    global : GlobalCtx

    f : Term → B → A × B
    g : Operator → List A → A
    ε : B

  open GlobalCtx global public

mutual

  map-fold : ∀ {a b} {A : Set a} {B : Set b}
             → FoldCtx A B → List (Arg Term) → B → TC (List A × B)
  map-fold ctx [] acc = return ([] , acc)
  map-fold ctx (vArg x ∷ xs) acc
    = do (x , acc) ← fold-acc ctx x acc
         (xs , acc) ← map-fold ctx xs acc
         return (x ∷ xs , acc)
  map-fold ctx (_ ∷ xs) acc = map-fold ctx xs acc

  fold-inner : ∀ {a b} {A : Set a} {B : Set b}
                → FoldCtx A B → Operator → Term → B → TC (List A × B)
  fold-inner ctx op (var _ args)     acc = map-fold ctx (ekat (arity op) args) acc
  fold-inner ctx op (con _ args)     acc = map-fold ctx (ekat (arity op) args) acc
  fold-inner ctx op (def _ args)     acc = map-fold ctx (ekat (arity op) args) acc
  fold-inner ctx op (meta _ args)    acc = map-fold ctx (ekat (arity op) args) acc
  fold-inner ctx op (pat-lam _ args) acc = map-fold ctx (ekat (arity op) args) acc
  fold-inner _ _ t _ = typeError (termErr t ∷ strErr "has no arguments" ∷ [])

  fold-acc : ∀ {a b} {A : Set a} {B : Set b} → FoldCtx A B → Term → B → TC (A × B)
  fold-acc ctx t acc
    = do op? ← find (λ x → prefix (arity x) (normalised x) t) (FoldCtx.operators ctx)
         resolve op?
    where resolve : Maybe Operator → TC _
          resolve (just op)
            = do (args , acc) ← fold-inner ctx op t acc
                 return ((FoldCtx.g ctx) op args , acc)
          resolve nothing = return ((FoldCtx.f ctx) t acc)

fold : ∀ {a b} {A : Set a} {B : Set b} → FoldCtx A B → Term → TC (A × B)
fold ctx t = fold-acc ctx t (FoldCtx.ε ctx)

fold-⊤ : ∀ {a} {A : Set a} → GlobalCtx
         → (Term → A) → (Operator → List A → A) → Term → TC A
fold-⊤ ctx f g t
  = do (x , _) ← fold (foldCtx ctx (λ x _ → (f x , tt)) g tt) t
       return x

accumulate : ∀ {a} {A : Set a} → GlobalCtx
             → (Term → A → A) → A → Term → TC A
accumulate ctx f ε t
  = do (_ , acc) ← fold (foldCtx ctx (λ x acc → (tt , f x acc)) (λ _ _ → tt) ε) t
       return acc

leaves : GlobalCtx → Term → TC ℕ
leaves ctx = fold-⊤ ctx (λ _ → 1) (λ _ → sum)

mutual
  argsOpen : Term → List (Arg Term) → TC Bool
  argsOpen τ [] = return false
  argsOpen τ (vArg x ∷ xs)
    = do head ← isOpen τ x
         tail ← argsOpen τ xs
         return (head ∨ tail)
  argsOpen τ (_ ∷ xs) = argsOpen τ xs

  isOpen : Term → Term → TC Bool
  isOpen τ t@(var _ _)  = hasType τ t
  isOpen τ t@(meta _ _) = hasType τ t
  isOpen τ (con c args) = argsOpen τ args
  isOpen τ (def f args) = argsOpen τ args
  isOpen τ unknown      = return true
  isOpen τ _            = return false

findOpen : GlobalCtx → List Term → Term → TC (List Term)
findOpen ctx ε t = flatten (accumulate ctx binding (return ε) t)
  where binding : Term → TC (List Term) → TC (List Term)
        binding t env
          = do env ← env
               let τ = CoreCtx.carrier (GlobalCtx.core ctx)
               open? ← isOpen τ t
               if open? then return (insert env t)
                        else return env

buildSyntax : GlobalCtx → List Term → Term → TC Term
buildSyntax ctx env t = fold-⊤ ctx buildInj buildTerm t
  where bt : Term
        bt = def (quote Free.BT)
                 ( vra (GlobalCtx.signature ctx)
                 ∷ vra (GlobalCtx.carrier ctx)
                 ∷ vra (lit (nat (length env)))
                 ∷ []
                 )

        buildAtom : Term → Term
        buildAtom t =
          con (quote Free.Term.atom)
              ( hra (GlobalCtx.signature ctx)
              ∷ hra unknown
              ∷ hra bt
              ∷ vra t
              ∷ []
              )

        buildDyn : ℕ → Term
        buildDyn n =
          con (quote Free.BT.dyn)
              ( hra (GlobalCtx.signature ctx)
              ∷ hra unknown
              ∷ hra (GlobalCtx.carrier ctx)
              ∷ hra (lit (nat (length env)))
              ∷ vra (fin n)
              ∷ []
              )

        buildSta : Term → Term
        buildSta t =
          con (quote Free.BT.sta)
              ( hra (GlobalCtx.signature ctx)
              ∷ hra unknown
              ∷ hra (GlobalCtx.carrier ctx)
              ∷ hra (lit (nat (length env)))
              ∷ vra t
              ∷ []
              )

        buildInj : Term → Term
        buildInj t with indexOf env t
        ...           | just n  = buildAtom (buildDyn n)
        ...           | nothing = buildAtom (buildSta t)

        buildTerm : Operator → List Term → Term
        buildTerm op xs =
          con (quote Free.Term.term)
               ( hra (GlobalCtx.signature ctx)
               ∷ hra unknown
               ∷ hra bt
               ∷ hra (lit (nat (arity op)))
               ∷ vra (con (name op) [])
               ∷ vra (vec (fromList xs))
               ∷ []
               )

environment : List Term → Term
environment env = vec (fromList env)

macro
  fragment : Name → Term → Term → TC ⊤
  fragment frex model goal
    = do ctx ← ctx frex model goal
         env ← findOpen ctx [] (GlobalCtx.lhs ctx)
         env ← findOpen ctx env (GlobalCtx.rhs ctx)
         lhs ← buildSyntax ctx env (GlobalCtx.lhs ctx)
         rhs ← buildSyntax ctx env (GlobalCtx.rhs ctx)
         let n = length env
         let frex = def (quote FreeExtension._[_])
                        ( hra (GlobalCtx.theory ctx)
                        ∷ vra (GlobalCtx.frex ctx)
                        ∷ vra (GlobalCtx.model ctx)
                        ∷ vra (lit (nat n))
                        ∷ []
                        )
         let setoid = def (quote ∥_∥/≈)
                          ( hra (GlobalCtx.theory ctx)
                          ∷ vra frex
                          ∷ []
                          )
         let p = def (quote Setoid.refl) (vra setoid ∷ [])
         let frexify = def (quote frexify)
                           ( vra (GlobalCtx.theory ctx)
                           ∷ vra (GlobalCtx.frex ctx)
                           ∷ vra (GlobalCtx.model ctx)
                           ∷ vra (vec (fromList env))
                           ∷ hra lhs
                           ∷ hra rhs
                           ∷ vra p
                           ∷ []
                           )
         frexify ← restore-telescope (GlobalCtx.telescope ctx) frexify
         unify frexify goal


text:
module Issue580 where

record Bad : Set₁ where
  private field A : Set


text:
postulate
  Wrap : Set → Set
  instance wrap : {A : Set} → A → Wrap A

postulate
  I : Set
  P : I → Set

HO = ∀ {i} {{p : P i}} → P i

postulate
  X : {{ho : HO}} → Set
  Y : {{ho : Wrap HO}} → Set

Works : Set
Works = X

-- Debug output shows messed up deBruijn indices in unwrapped target: P p instead of P i
Fails : Set
Fails = Y

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- Most of a virtual machine
------------------------------------------------------------------------

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

module Lambda.Virtual-machine where

open import Equality.Propositional
open import Prelude

open import Vec.Function equality-with-J

open import Lambda.Syntax

------------------------------------------------------------------------
-- Instruction set

mutual

  -- Instructions.

  data Instr (n : ℕ) : Type where
    var : (x : Fin n) → Instr n
    con : (i : ℕ) → Instr n
    clo : (c : Code (suc n)) → Instr n
    app : Instr n
    ret : Instr n

  -- Code.

  Code : ℕ → Type
  Code n = List (Instr n)

-- Environments and values.

open Closure Code

------------------------------------------------------------------------
-- Stacks and states

-- Stacks.

data StackElement : Type where
  val : (v : Value) → StackElement
  ret : ∀ {n} (c : Code n) (ρ : Env n) → StackElement

Stack : Type
Stack = List StackElement

-- States.

data State : Type where
  ⟨_,_,_⟩ : ∀ {n} (c : Code n) (s : Stack) (ρ : Env n) → State

pattern ⟨_∣_,_,_⟩ n c s ρ = ⟨_,_,_⟩ {n} c s ρ

------------------------------------------------------------------------
-- A kind of small-step semantics for the virtual machine

-- The result of running the VM one step.

data Result : Type where
  continue : (s : State) → Result
  done     : (v : Value) → Result
  crash    : Result

-- A single step of the computation.

step : State → Result
step ⟨ var x  ∷ c ,                          s , ρ ⟩ = continue ⟨ c  , val (ρ x)    ∷ s ,        ρ  ⟩
step ⟨ con i  ∷ c ,                          s , ρ ⟩ = continue ⟨ c  , val (con i)  ∷ s ,        ρ  ⟩
step ⟨ clo c′ ∷ c ,                          s , ρ ⟩ = continue ⟨ c  , val (ƛ c′ ρ) ∷ s ,        ρ  ⟩
step ⟨ app    ∷ c , val v ∷ val (ƛ c′ ρ′) ∷  s , ρ ⟩ = continue ⟨ c′ , ret c ρ      ∷ s , cons v ρ′ ⟩
step ⟨ ret    ∷ c , val v ∷ ret c′ ρ′     ∷  s , ρ ⟩ = continue ⟨ c′ , val v        ∷ s ,        ρ′ ⟩
step ⟨ zero ∣ []  ,                 val v ∷ [] , ρ ⟩ = done v
step _                                               = crash

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Class.Equality where

open import Data.Bool using (Bool; if_then_else_)
open import Data.List
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality

record Eq (A : Set) : Set where
  field
    _≟_ : (x y : A) -> Dec (x ≡ y)

open Eq {{...}} public

record EqB (A : Set) : Set where
  field
    _≣_ : (x y : A) -> Bool

  decCase_of_default_ : ∀ {b} {B : Set b} -> A -> List (A × B) -> B -> B
  decCase a of [] default d = d
  decCase a of x ∷ xs default d = if a ≣ proj₁ x then proj₂ x else (decCase a of xs default d)

open EqB {{...}} public

Eq→EqB : ∀ {A} -> {{_ : Eq A}} -> EqB A
Eq→EqB = record { _≣_ = λ x y -> ⌊ x ≟ y ⌋ }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.RPn where

open import Cubical.HITs.RPn.Base public


text: module bstd.bign where

max_stars_repo_name: semenov-vladyslav/bstd

max_issues_repo_name: semenov-vladyslav/bstd

max_forks_repo_name: semenov-vladyslav/bstd


text:
-- {-# OPTIONS -v tc.lhs.unify:100 #-}
-- Reported by project member adamgundry, 2012-10-26

-- I was trying to extend Conor's KIPLING technique (Outrageous but
-- Meaningful Coincidences, WGP 2010) which depends on indexing a
-- syntax by functions, when I hit this problem:

module Issue738 where

open import Common.Equality

data U : Set where
  a : U
  b : U

-- works, with explicit equality:

module Param where

  data D (f : U → U) : Set where
    da : (f ≡ λ x → a) → D f
    db : (f ≡ λ x → b) → D f

  app : ∀ {A B : Set}{f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
  app refl x = refl

  fu : D (λ x → a) → Set
  fu (da refl) = U
  fu (db p) with app p a
  ... | ()

-- original formulation:

module Index where

  data Foo : (U -> U) -> Set where
    mka : Foo (\ x -> a)
    mkb : Foo (\ x -> b)

  foo : Foo (\ x -> a) -> Set
  foo mka = ?

-- This gives the error message:

-- -- Cannot decide whether there should be a case for the constructor
-- -- mkb, since the unification gets stuck on unifying the inferred
-- -- indices
-- --   [λ x → b]
-- -- with the expected indices
-- --   [λ x → a]
-- -- when checking the definition of foo

-- But these indices cannot be unified (a and b are constants) so it
-- should be possible to exclude this case.  Could we improve the
-- unifier to notice this?

-- Andreas, 2012-10-29 No, because if the domain type is empty,
-- these two lambdas cannot be disunified


text:
module Functors where

open import Library
open import Categories
open Cat

record Fun {a b c d} (C : Cat {a}{b})(D : Cat {c}{d}) : Set (a ⊔ b ⊔ c ⊔ d)
  where
  constructor functor
  field OMap  : Obj C → Obj D
        HMap  : ∀{X Y} → Hom C X Y → Hom D (OMap X) (OMap Y)
        fid   : ∀{X} → HMap (iden C {X}) ≅ iden D {OMap X}
        fcomp : ∀{X Y Z}{f : Hom C Y Z}{g : Hom C X Y} →
                HMap (comp C f g) ≅ comp D (HMap f) (HMap g)
open Fun

IdF : ∀{a b}(C : Cat {a}{b}) → Fun C C
IdF C = record{OMap = id;HMap = id;fid = refl;fcomp = refl}

_○_ : ∀{a b c d e f}{C : Cat {a}{b}}{D : Cat {c}{d}}{E : Cat {e}{f}} →
      Fun D E → Fun C D → Fun C E
_○_ {C = C}{D}{E} F G = record{
  OMap  = OMap F ∘ OMap G;
  HMap   = HMap F ∘ HMap G;
  fid    =
    proof
    HMap F (HMap G (iden C))
    ≅⟨ cong (HMap F) (fid G) ⟩
    HMap F (iden D)
    ≅⟨ fid F ⟩
    iden E
    ∎;
  fcomp  = λ {_}{_}{_}{f}{g} →
    proof
    HMap F (HMap G (comp C f g))
    ≅⟨ cong (HMap F) (fcomp G)  ⟩
    HMap F (comp D (HMap G f) (HMap G g))
    ≅⟨ fcomp F ⟩
    comp E (HMap F (HMap G f)) (HMap F (HMap G g))
    ∎}
infix 10 _○_

FunctorEq : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}(F G : Fun C D) →
            OMap F ≅ OMap G →
            (λ {X Y} → HMap F {X}{Y}) ≅ (λ {X}{Y} → HMap G {X}{Y}) → F ≅ G
FunctorEq (functor fo fh _ _) (functor .fo .fh _ _) refl refl =
  cong₂ (functor fo fh)
        (iext λ _ → ir _ _)
        (iext λ _ → iext λ _ → iext λ _ → iext λ _ → iext λ _ → ir _ _)

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
open import Oscar.Prelude
open import Oscar.Class.Successor₀
open import Oscar.Class.Injectivity
open import Oscar.Data.¶
open import Oscar.Data.Vec
open import Oscar.Data.Proposequality
import Oscar.Property.Thickandthin.FinFinProposequalityMaybeProposequality

module Oscar.Class.Injectivity.Vec where

instance

  𝓘njection₂Vec : ∀ {N} {𝔭} {𝔓 : ¶ → Ø 𝔭} → 𝓘njection₂ (λ (x : 𝔓 N) (_ : Vec⟨ 𝔓 ⟩ N) → Vec⟨ 𝔓 ⟩ (⇑₀ N))
  𝓘njection₂Vec .𝓘njection₂.injection₂ = _,_

  [𝓘njectivity₂,₀,₁]Vec : ∀ {N} {𝔭} {𝔓 : ¶ → Ø 𝔭} → [𝓘njectivity₂,₀,₁] (λ (x : 𝔓 N) (_ : Vec⟨ 𝔓 ⟩ N) → Vec⟨ 𝔓 ⟩ (⇑₀ N)) Proposequality Proposequality
  [𝓘njectivity₂,₀,₁]Vec = ∁

  𝓘njectivity₂,₀,₁Vec :   ∀ {N} {𝔭} {𝔓 : ¶ → Ø 𝔭} → 𝓘njectivity₂,₀,₁   (λ (x : 𝔓 N) (_ : Vec⟨ 𝔓 ⟩ N) → Vec⟨ 𝔓 ⟩ (⇑₀ N)) Proposequality Proposequality
  𝓘njectivity₂,₀,₁Vec .𝓘njectivity₂,₀,₁.injectivity₂,₀,₁ ∅ = ∅

  [𝓘njectivity₂,₀,₂]Vec : ∀ {N} {𝔭} {𝔓 : ¶ → Ø 𝔭} → [𝓘njectivity₂,₀,₂] (λ (x : 𝔓 N) (_ : Vec⟨ 𝔓 ⟩ N) → Vec⟨ 𝔓 ⟩ (⇑₀ N)) Proposequality Proposequality
  [𝓘njectivity₂,₀,₂]Vec = ∁

  𝓘njectivity₂,₀,₂Vec : ∀ {N} {𝔭} {𝔓 : ¶ → Ø 𝔭} → 𝓘njectivity₂,₀,₂ (λ (x : 𝔓 N) (_ : Vec⟨ 𝔓 ⟩ N) → Vec⟨ 𝔓 ⟩ (⇑₀ N)) Proposequality Proposequality
  𝓘njectivity₂,₀,₂Vec .𝓘njectivity₂,₀,₂.injectivity₂,₀,₂ ∅ = ∅


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

-- Exact category (https://ncatlab.org/nlab/show/exact+category)
-- is a regular category
-- in which every internal equivalence is a kernel pair

module Categories.Category.Exact where

open import Level

open import Categories.Category.Core
open import Categories.Diagram.Pullback
open import Categories.Category.Cocartesian
open import Categories.Object.Coproduct
open import Categories.Morphism
open import Categories.Category.Complete.Finitely using (FinitelyComplete)
open import Categories.Diagram.Coequalizer
open import Categories.Diagram.KernelPair

open import Categories.Category.Regular
open import Categories.Morphism.Regular

open import Categories.Object.InternalRelation

record Exact {o ℓ e : Level} (𝒞 : Category o ℓ e) : Set (suc (o ⊔ ℓ ⊔ e)) where
  open Category 𝒞
  open Pullback
  open Coequalizer
  open Equivalence

  field
    regular    : Regular 𝒞
    quotient   : ∀ {X : Obj} (E : Equivalence 𝒞 X) → Coequalizer 𝒞 (R.p₁ E) (R.p₂ E)
    effective  : ∀ {X : Obj} (E : Equivalence 𝒞 X) → IsPullback 𝒞 (R.p₁ E) (R.p₂ E)
      (arr (quotient E)) (arr (quotient E))


text:
module VecS where

open import Data.Empty
open import Data.Product hiding (map)
open import Data.Sum
open import Data.Vec
open import Data.Nat
open import Data.Bool
open import Data.Nat.Properties

import Homotopy as Pi

------------------------------------------------------------------------------

data B : Set where
  ZERO  : B
  ONE   : B
  PLUS  : B → B → B
  TIMES : B → B → B
  DUAL  : B → B

data BVAL : B → Set where
  UNIT   : BVAL ONE
  LEFT   : {b₁ b₂ : B} → BVAL b₁ → BVAL (PLUS b₁ b₂)
  RIGHT  : {b₁ b₂ : B} → BVAL b₂ → BVAL (PLUS b₁ b₂)
  PAIR   : {b₁ b₂ : B} → BVAL b₁ → BVAL b₂ → BVAL (TIMES b₁ b₂)
  FLIP   : {b : B} → BVAL b → BVAL (DUAL b)

data Iso : {b₁ b₂ : B} → BVAL b₁ → BVAL b₂ → Set where
  unite₊  : {b : B} {v : BVAL b} → Iso (RIGHT {ZERO} {b} v) v
  uniti₊  : {b : B} {v : BVAL b} → Iso v (RIGHT {ZERO} {b} v)
  swap₊1  : {b₁ b₂ : B} {v₁ : BVAL b₁} → Iso (LEFT {b₁} {b₂} v₁) (RIGHT {b₂} {b₁} v₁)
  swap₊2  : {b₁ b₂ : B} {v₂ : BVAL b₂} → Iso (RIGHT {b₁} {b₂} v₂) (LEFT {b₂} {b₁} v₂)
  assocl₊1 : {b₁ b₂ b₃ : B} {v₁ : BVAL b₁} →
             Iso (LEFT {b₁} {PLUS b₂ b₃} v₁) (LEFT {PLUS b₁ b₂} {b₃} (LEFT {b₁} {b₂} v₁))
  assocl₊2 : {b₁ b₂ b₃ : B} {v₂ : BVAL b₂} →
             Iso (RIGHT {b₁} {PLUS b₂ b₃} (LEFT {b₂} {b₃} v₂)) (LEFT {PLUS b₁ b₂} {b₃} (RIGHT {b₁} {b₂} v₂))
  assocl₊3 : {b₁ b₂ b₃ : B} {v₃ : BVAL b₃} →
             Iso (RIGHT {b₁} {PLUS b₂ b₃} (RIGHT {b₂} {b₃} v₃)) (RIGHT {PLUS b₁ b₂} {b₃} v₃)
  assocr₊1 : {b₁ b₂ b₃ : B} {v₁ : BVAL b₁} →
             Iso (LEFT {PLUS b₁ b₂} {b₃} (LEFT {b₁} {b₂} v₁)) (LEFT {b₁} {PLUS b₂ b₃} v₁)
  assocr₊2 : {b₁ b₂ b₃ : B} {v₂ : BVAL b₂} →
             Iso (LEFT {PLUS b₁ b₂} {b₃} (RIGHT {b₁} {b₂} v₂)) (RIGHT {b₁} {PLUS b₂ b₃} (LEFT {b₂} {b₃} v₂))
  assocr₊3 : {b₁ b₂ b₃ : B} {v₃ : BVAL b₃} →
             Iso (RIGHT {PLUS b₁ b₂} {b₃} v₃) (RIGHT {b₁} {PLUS b₂ b₃} (RIGHT {b₂} {b₃} v₃))
  unite⋆  : {b : B} {v : BVAL b} → Iso (PAIR UNIT v) v
  uniti⋆  : {b : B} {v : BVAL b} → Iso v (PAIR UNIT v)
  swap⋆   : {b₁ b₂ : B} {v₁ : BVAL b₁} {v₂ : BVAL b₂} → Iso (PAIR v₁ v₂) (PAIR v₂ v₁)
  assocl⋆ : {b₁ b₂ b₃ : B} {v₁ : BVAL b₁} {v₂ : BVAL b₂} {v₃ : BVAL b₃} →
            Iso (PAIR v₁ (PAIR v₂ v₃)) (PAIR (PAIR v₁ v₂) v₃)
  assocr⋆ : {b₁ b₂ b₃ : B} {v₁ : BVAL b₁} {v₂ : BVAL b₂} {v₃ : BVAL b₃} →
            Iso (PAIR (PAIR v₁ v₂) v₃) (PAIR v₁ (PAIR v₂ v₃))
  dist1   : {b₁ b₂ b₃ : B} {v₁ : BVAL b₁} {v₃ : BVAL b₃} →
            Iso (PAIR (LEFT {b₁} {b₂} v₁) v₃) (LEFT {TIMES b₁ b₃} {TIMES b₂ b₃} (PAIR v₁ v₃))
  dist2   : {b₁ b₂ b₃ : B} {v₂ : BVAL b₂} {v₃ : BVAL b₃} →
            Iso (PAIR (RIGHT {b₁} {b₂} v₂) v₃) (RIGHT {TIMES b₁ b₃} {TIMES b₂ b₃} (PAIR v₂ v₃))
  factor1 : {b₁ b₂ b₃ : B} {v₁ : BVAL b₁} {v₃ : BVAL b₃} →
            Iso (LEFT {TIMES b₁ b₃} {TIMES b₂ b₃} (PAIR v₁ v₃)) (PAIR (LEFT {b₁} {b₂} v₁) v₃)
  factor2 : {b₁ b₂ b₃ : B} {v₂ : BVAL b₂} {v₃ : BVAL b₃} →
            Iso (RIGHT {TIMES b₁ b₃} {TIMES b₂ b₃} (PAIR v₂ v₃)) (PAIR (RIGHT {b₁} {b₂} v₂) v₃)
  id⟷   : {b : B} {v : BVAL b} → Iso v v
  sym    : {b₁ b₂ : B} {v₁ : BVAL b₁} {v₂ : BVAL b₂} → Iso v₁ v₂ → Iso v₂ v₁
  VSEMI  : {b₁ b₂ b₃ : B} {v₁ : BVAL b₁} {v₂ : BVAL b₂} {v₃ : BVAL b₃} →
           Iso v₁ v₂ → Iso v₂ v₃ → Iso v₁ v₃
  VPLUS1  : {b₁ b₂ b₃ b₄ : B} {v₁ : BVAL b₁} {v₂ : BVAL b₂} {v₃ : BVAL b₃} {v₄ : BVAL b₄} →
           Iso v₁ v₃ → Iso v₂ v₄ → Iso (LEFT {b₁} {b₂} v₁) (LEFT {b₃} {b₄} v₃)
  VPLUS2  : {b₁ b₂ b₃ b₄ : B} {v₁ : BVAL b₁} {v₂ : BVAL b₂} {v₃ : BVAL b₃} {v₄ : BVAL b₄} →
           Iso v₁ v₃ → Iso v₂ v₄ → Iso (RIGHT {b₁} {b₂} v₂) (RIGHT {b₃} {b₄} v₄)
  VTIMES : {b₁ b₂ b₃ b₄ : B} {v₁ : BVAL b₁} {v₂ : BVAL b₂} {v₃ : BVAL b₃} {v₄ : BVAL b₄} →
           Iso v₁ v₃ → Iso v₂ v₄ → Iso (PAIR v₁ v₂) (PAIR v₃ v₄)
  refe⋆   : {b : B} {v : BVAL b} → Iso (FLIP (FLIP v)) v
  refi⋆   : {b : B} {v : BVAL b} → Iso v (FLIP (FLIP v))
  rile⋆   : {b : B} {v : BVAL b} → Iso (PAIR v (PAIR v (FLIP v))) v
  rili⋆   : {b : B} {v : BVAL b} → Iso v (PAIR v (PAIR v (FLIP v)))

------------------------------------------------------------------------------
-- Pi combinators

-- embed pi into the values with duals

liftT : Pi.B → B
liftT Pi.ZERO = ZERO
liftT Pi.ONE = ONE
liftT (Pi.PLUS b₁ b₂) = PLUS (liftT b₁) (liftT b₂)
liftT (Pi.TIMES b₁ b₂) = TIMES (liftT b₁) (liftT b₂)

lift : {b : Pi.B} → Pi.BVAL b → BVAL (liftT b)
lift Pi.UNIT = UNIT
lift (Pi.LEFT v) = LEFT (lift v)
lift (Pi.RIGHT v) = RIGHT (lift v)
lift (Pi.PAIR v₁ v₂) = PAIR (lift v₁) (lift v₂)

embed : {b₁ b₂ : Pi.B} → Pi.Id_B (b₁ , b₂) → Pi.BVAL b₁ → BVAL (TIMES (DUAL (liftT b₁)) (liftT b₂))
embed c v = PAIR (FLIP (lift v)) (lift (Pi.eval c v))

-- the idea would be that:
--   if   eval pi-combinator v = v'
-- then we would have a proof that
--   (embed pi-combinator v , v) ~iso~ v'

pibool : Pi.B
pibool = Pi.PLUS Pi.ONE Pi.ONE

pitrue : Pi.BVAL pibool
pitrue = Pi.LEFT Pi.UNIT

ex1 : BVAL (TIMES (DUAL (PLUS ONE ONE)) (PLUS ONE ONE))
ex1 = embed {pibool} {pibool} Pi.swap₊  pitrue
-- ex1 = PAIR (FLIP (LEFT UNIT)) (RIGHT UNIT)

-- Check: PAIR (PAIR (FLIP (LEFT UNIT)) (RIGHT UNIT)) (LEFT UNIT) ~ RIGHT UNIT

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets
------------------------------------------------------------------------

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

module Data.Fin where

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Data.Fin.Base public

------------------------------------------------------------------------
-- Publicly re-export queries

open import Data.Fin.Properties public
  using (_≟_; _≤?_; _<?_)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Function setoids and related constructions
------------------------------------------------------------------------

module Function.Equality where

open import Function as Fun using (_on_)
open import Level
import Relation.Binary as B
import Relation.Binary.Indexed as I

------------------------------------------------------------------------
-- Functions which preserve equality

record Π {f₁ f₂ t₁ t₂}
         (From : B.Setoid f₁ f₂)
         (To : I.Setoid (B.Setoid.Carrier From) t₁ t₂) :
         Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  open I using (_=[_]⇒_)
  infixl 5 _⟨$⟩_
  field
    _⟨$⟩_ : (x : B.Setoid.Carrier From) → I.Setoid.Carrier To x
    cong  : B.Setoid._≈_ From =[ _⟨$⟩_ ]⇒ I.Setoid._≈_ To

open Π public

infixr 0 _⟶_

_⟶_ : ∀ {f₁ f₂ t₁ t₂} → B.Setoid f₁ f₂ → B.Setoid t₁ t₂ → Set _
From ⟶ To = Π From (B.Setoid.indexedSetoid To)

-- Identity and composition.

id : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂} → A ⟶ A
id = record { _⟨$⟩_ = Fun.id; cong = Fun.id }

infixr 9 _∘_

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

-- Constant equality-preserving function.

const : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂}
          {b₁ b₂} {B : B.Setoid b₁ b₂} →
        B.Setoid.Carrier B → A ⟶ B
const {B = B} b = record
  { _⟨$⟩_ = Fun.const b
  ; cong  = Fun.const (B.Setoid.refl B)
  }

------------------------------------------------------------------------
-- Function setoids

-- Dependent.

setoid : ∀ {f₁ f₂ t₁ t₂}
         (From : B.Setoid f₁ f₂) →
         I.Setoid (B.Setoid.Carrier From) t₁ t₂ →
         B.Setoid _ _
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 = B.Setoid From using () renaming (_≈_ to _≈₁_)
  open module To = I.Setoid To   using () renaming (_≈_ to _≈₂_)

-- Non-dependent.

infixr 0 _⇨_

_⇨_ : ∀ {f₁ f₂ t₁ t₂} → B.Setoid f₁ f₂ → B.Setoid t₁ t₂ → B.Setoid _ _
From ⇨ To = setoid From (B.Setoid.indexedSetoid To)

-- A variant of setoid which uses the propositional equality setoid
-- for the domain, and a more convenient definition of _≈_.

≡-setoid : ∀ {f t₁ t₂} (From : Set f) → I.Setoid From t₁ t₂ → B.Setoid _ _
≡-setoid From To = record
  { Carrier       = (x : From) → Carrier x
  ; _≈_           = λ f g → ∀ x → f x ≈ g x
  ; isEquivalence = record
    { refl  = λ {f} x → refl
    ; sym   = λ f∼g x → sym (f∼g x)
    ; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x)
    }
  } where open I.Setoid To

-- Parameter swapping function.

flip : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂}
         {b₁ b₂} {B : B.Setoid b₁ b₂}
         {c₁ c₂} {C : B.Setoid c₁ c₂} →
       A ⟶ B ⇨ C → B ⟶ A ⇨ C
flip {B = B} f = record
  { _⟨$⟩_ = λ b → record
    { _⟨$⟩_ = λ a → f ⟨$⟩ a ⟨$⟩ b
    ; cong  = λ a₁≈a₂ → cong f a₁≈a₂ (B.Setoid.refl B) }
  ; cong  = λ b₁≈b₂ a₁≈a₂ → cong f a₁≈a₂ b₁≈b₂
  }


text:
{-

Eilenberg–Mac Lane type K(G, 1)

-}

{-# OPTIONS --cubical --no-import-sorts --safe  --experimental-lossy-unification #-}
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.GroupoidLaws
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma
open import Cubical.Data.Empty renaming (rec to ⊥-rec) hiding (elim)

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

open import Cubical.Algebra.AbGroup.Base

open import Cubical.Functions.Morphism

private
  variable
    ℓG ℓ : Level

module _ ((G , str) : Group ℓG) where

  open GroupStr str

  elimGroupoid :
   {B : EM₁ (G , str) → Type ℓ}
          → ((x : EM₁ (G , str)) → isGroupoid (B x))
          → (b : B embase)
          → (bloop : ((g : G) → PathP (λ i → B (emloop g i)) b b))
          → ((g h : G) → PathP (λ i → PathP (λ j → B (emcomp g h j i))
                                 (bloop g i) (bloop (g · h) i)) (λ _ → b) (bloop h))
          → (x : EM₁ (G , str))
          → B x
  elimGroupoid Bgroup b bloop bcomp embase = b
  elimGroupoid Bgroup b bloop bcomp (emloop x i) = bloop x i
  elimGroupoid Bgroup b bloop bcomp (emcomp g h j i) = bcomp g h i j
  elimGroupoid {B = B} Bgroup b bloop bcomp (emsquash g h p q r s i j k) = help i j k
    where
    help : PathP (λ i → PathP (λ j → PathP (λ k → B (emsquash g h p q r s i j k))
                 (elimGroupoid Bgroup b bloop bcomp g)
                 (elimGroupoid Bgroup b bloop bcomp h))
                 (λ k → elimGroupoid Bgroup b bloop bcomp (p k))
                 λ k → elimGroupoid Bgroup b bloop bcomp (q k))
                 (λ j k → elimGroupoid Bgroup b bloop bcomp (r j k))
                 λ j k → elimGroupoid Bgroup b bloop bcomp (s j k)
    help = toPathP (isOfHLevelPathP' 1 (isOfHLevelPathP' 2 (Bgroup _) _ _) _ _ _ _)

  elimSet : {B : EM₁ (G , str) → Type ℓ}
          → ((x : EM₁ (G , str)) → isSet (B x))
          → (b : B embase)
          → ((g : G) → PathP (λ i → B (emloop g i)) b b)
          → (x : EM₁ (G , str))
          → 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→SquareP
      (λ i j → Bset (emcomp g h i j))
      (λ j → bloop g j) (λ j → bloop (g · h) j)
      (λ i → b) (λ i → bloop h i)
      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

  elimProp : {B : EM₁ (G , str) → Type ℓ}
             → ((x : EM₁ (G , str)) → isProp (B x))
             → B embase
             → (x : EM₁ (G , str))
             → B x
  elimProp Bprop b x =
    elimSet
      (λ x → isProp→isSet (Bprop x))
      b
      (λ g → isProp→PathP (λ i → Bprop ((emloop g) i)) b b)
      x

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

  elim : {B : EM₁ (G , str) → Type ℓ}
       → ((x : EM₁ (G , str)) → isGroupoid (B x))
       → (b : B embase)
       → (bloop : (g : G) → PathP (λ i → B (emloop g i)) b b)
       → ((g h : G) → SquareP (λ i j → B (emcomp g h i j))
            (bloop g) (bloop (g · h)) (λ j → b) (bloop h))
       → (x : EM₁ (G , str))
       → 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 : G → b ≡ b)
      → ((g h : G) → Square (bloop g) (bloop (g · h)) refl (bloop h))
      → (x : EM₁ (G , str))
      → B
  rec Bgpd = elim (λ _ → Bgpd)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical