text:
module TermShape where

open import Relation.Unary using (_∈_; _⊆_)
open import Size
open import Library
open import Terms
open import Substitution

-- Evaluation contexts.

data ECxt (Γ : Cxt) : (a b : Ty) → Set where
  appl  : ∀ {a b} (u : Tm Γ a)  → ECxt Γ (a →̂ b) b

-- Ehole Et E t ~~ Et = E[t]

data Ehole {Γ : Cxt} : {a b : Ty} → Tm Γ b → ECxt Γ a b → Tm Γ a → Set where
  appl  : ∀ {a b} {t : Tm Γ (a →̂ b)} (u : Tm Γ a)  → Ehole (app t u) (appl u) t

-- Evaluation contexts are closed under substitution.

substEC : ∀ {i vt Γ Δ a b} → (σ : RenSub {i} vt Γ Δ) → ECxt Γ a b → ECxt Δ a b
substEC σ (appl u) = appl (subst σ u)

substEh : ∀ {i vt Γ Δ a b} → (σ : RenSub {i} vt Γ Δ) → ∀ {E}{Et : Tm Γ b}{t : Tm Γ a} → (Eh : Ehole Et E t)
            → Ehole (subst σ Et) (substEC σ E) (subst σ t)
substEh σ (appl u) = appl (subst σ u)

mkEHole : ∀ {Γ} {a b} (E : ECxt Γ a b) {t} → ∃ λ E[t] → Ehole E[t] E t
mkEHole (appl u)  = _ , appl u

_[_] : ∀ {Γ} {a b} (E : ECxt Γ a b) (t : Tm Γ a) → Tm Γ b
E [ t ] = proj₁ (mkEHole E {t})

data ECxt* (Γ : Cxt) : Ty → Ty → Set where
  [] : ∀ {a} → ECxt* Γ a a
  _∷_ : ∀ {a₀ a₁ a₂} → ECxt Γ a₀ a₁ → ECxt* Γ a₁ a₂ → ECxt* Γ a₀ a₂

_[_]* : ∀ {Γ} {a b} (E : ECxt* Γ a b) (t : Tm Γ a) → Tm Γ b
[] [ t ]* = t
(E ∷ Es) [ t ]* = Es [ E [ t ] ]*

_++*_ : ∀ {Γ a b c} → ECxt* Γ a b → ECxt* Γ b c → ECxt* Γ a c
[] ++* ys = ys
(x ∷ xs) ++* ys = x ∷ (xs ++* ys)

_∷r_ : ∀ {Γ a b c} → ECxt* Γ a b → ECxt Γ b c → ECxt* Γ a c
xs ∷r x = xs ++* (x ∷ [])

data Ehole* {Γ : Cxt} : {a b : Ty} → Tm Γ b → ECxt* Γ a b → Tm Γ a → Set where
  [] : ∀ {a} {t : Tm Γ a} → Ehole* t [] t
  _∷_ : ∀ {a b c t} {E : ECxt Γ b c} {Es : ECxt* Γ a b} {EEst Est}
        → Ehole EEst E Est → Ehole* Est Es t → Ehole* EEst (Es ∷r E) t

-- Inductive definition of strong normalization.

-- Parameterized evaluation contexts

data PCxt {Γ : Cxt} (P : ∀{c} → Tm Γ c → Set) : {a b : Ty} → Tm Γ b → ECxt Γ a b → Tm Γ a → Set where

  appl  : ∀ {a b u}{t : Tm _ (a →̂ b)}
          → (𝒖 : P u)
          → PCxt P (app t u) (appl u) t

-- Parameterized neutral terms.

data PNe {Γ} (P : ∀{c} → Tm Γ c → Set) {b} : Tm Γ b → Set where

  var  : ∀ x                              → PNe P (var x)

  elim : ∀ {a} {t : Tm Γ a} {E Et}
         → (𝒏 : PNe P t) (𝑬𝒕 : PCxt P Et E t) → PNe P Et

-- Parametrized weak head reduction

infix 10 _/_⇒_

data _/_⇒_ {Γ} (P : ∀{c} → Tm Γ c → Set): ∀ {a} → Tm Γ a  → Tm Γ a → Set where

  β     : ∀ {a b}{t : Tm (a ∷ Γ) b}{u}
          → (𝒖 : P u)
          → P / (app (abs t) u) ⇒ subst0 u t

  cong  : ∀ {a b t t' Et Et'}{E : ECxt Γ a b}
          → (𝑬𝒕 : Ehole Et E t)
          → (𝑬𝒕' : Ehole Et' E t')
          → (t⇒ : P / t ⇒ t')
          → P / Et ⇒ Et'

-- Weak head reduction is deterministic.

detP⇒ : ∀ {a Γ} {P : ∀ {c} → Tm Γ c → Set} {t t₁ t₂ : Tm Γ a}
       → (t⇒₁ : P / t ⇒ t₁) (t⇒₂ : P / t ⇒ t₂) → t₁ ≡ t₂
{-
detP⇒ (β 𝒖) (β 𝒖₁) = ≡.refl
detP⇒ (β 𝒖) (cong (appl u) (appl .u) (cong () 𝑬𝒕' d'))
detP⇒ (cong (appl u) (appl .u) (cong () 𝑬𝒕' d)) (β 𝒖)
detP⇒ (cong (appl u) (appl .u) d) (cong (appl .u) (appl .u) d') = ≡.cong (λ t → app t u) (detP⇒ d d')
-}
detP⇒ (β _) (β _)                                              = ≡.refl
detP⇒ (β _) (cong (appl u) (appl .u) (cong () _ _))
detP⇒ (cong (appl u) (appl .u) (cong () _ _)) (β _)
detP⇒ (cong (appl u) (appl .u) x) (cong (appl .u) (appl .u) y) = ≡.cong (λ t → app t u) (detP⇒ x y)

-- Neutrals are closed under application.

pneApp : ∀{Γ a b}{P : ∀{c} → Tm Γ c → Set}{t : Tm Γ (a →̂ b)}{u : Tm Γ a} →
  PNe P t → P u → PNe P (app t u)
pneApp 𝒏 𝒖 = elim 𝒏 (appl 𝒖)

-- Functoriality of the notions wrt. P.

mapPCxt : ∀ {Γ} {P Q : ∀{c} → Tm Γ c → Set} (P⊆Q : ∀ {c}{t : Tm Γ c} → P t → Q t) {a b} {E : ECxt Γ a b}{Et t} → PCxt P Et E t -> PCxt Q Et E t
mapPCxt P⊆Q (appl u∈P) = appl (P⊆Q u∈P)

mapPNe : ∀ {Γ} {P Q : ∀{c} → Tm Γ c → Set} (P⊆Q : ∀ {c}{t : Tm Γ c} → P t → Q t) {a}{t : Tm Γ a} → PNe P t -> PNe Q t
mapPNe P⊆Q (var x) = var x
mapPNe P⊆Q (elim t∈Ne E∈SNh) = elim (mapPNe P⊆Q t∈Ne) (mapPCxt P⊆Q E∈SNh)

mapP⇒ : ∀ {Γ} {P Q : ∀{c} → Tm Γ c → Set} (P⊆Q : ∀ {c}{t : Tm Γ c} → P t → Q t) {a}{t t' : Tm Γ a} → P / t ⇒ t' → Q / t ⇒ t'
mapP⇒ P⊆Q (β t∈P) = β (P⊆Q t∈P)
mapP⇒ P⊆Q (cong Et Et' t→t') = cong Et Et' (mapP⇒ P⊆Q t→t')

_[_]⇒ : ∀ {Γ} {P : ∀{c} → Tm Γ c → Set} {a b} (E : ECxt Γ a b) {t₁ t₂ : Tm Γ a} → P / t₁ ⇒ t₂ → P / E [ t₁ ] ⇒ E [ t₂ ]
E [ t⇒ ]⇒ = cong (proj₂ (mkEHole E)) (proj₂ (mkEHole E)) t⇒

_[_]⇒* : ∀ {Γ} {P : ∀{c} → Tm Γ c → Set} {a b} (E : ECxt* Γ a b) {t₁ t₂ : Tm Γ a} → P / t₁ ⇒ t₂ → P / E [ t₁ ]* ⇒ E [ t₂ ]*
[]       [ t⇒ ]⇒* = t⇒
(E ∷ Es) [ t⇒ ]⇒* = Es [ E [ t⇒ ]⇒ ]⇒*

hole→≡ : ∀ {Γ a b}{Et t}{E : ECxt Γ a b} → (Es : Ehole Et E t) → Et ≡ E [ t ]
hole→≡ (appl u) = ≡.refl

lemma : ∀ {Γ b} {a} {t : Tm Γ a} (Es : ECxt* Γ a b)
         {b₁} {E : ECxt Γ b b₁}
         → E [ Es [ t ]* ] ≡ (Es ++* (E ∷ [])) [ t ]*
lemma [] = ≡.refl
lemma (x ∷ Es) = lemma Es

hole*→≡ : ∀ {Γ a b}{Et t}{E : ECxt* Γ a b} → (Es : Ehole* Et E t) → Et ≡ E [ t ]*
hole*→≡ [] = ≡.refl
hole*→≡ {t = t} (_∷_ {Es = Es} x Es₁) rewrite hole→≡ x | hole*→≡ Es₁ = lemma Es

++*-unit : ∀ {Γ a b} → (xs : ECxt* Γ a b) → xs ++* [] ≡ xs
++*-unit [] = ≡.refl
++*-unit (x ∷ xs) = ≡.cong (_∷_ x) (++*-unit xs)
++*-assoc : ∀ {Γ a b c d} → (xs : ECxt* Γ a b) → {ys : ECxt* Γ b c} → {zs : ECxt* Γ c d} → xs ++* (ys ++* zs) ≡ (xs ++* ys) ++* zs
++*-assoc [] = ≡.refl
++*-assoc (x ∷ xs) = ≡.cong (_∷_ x) (++*-assoc xs)

_++h*_ : ∀ {Γ a b c} {Es1 : ECxt* Γ a b} {Es2 : ECxt* Γ b c} → ∀ {t1 t2 t3} → Ehole* t2 Es1 t3 → Ehole* t1 Es2 t2  → Ehole* t1 (Es1 ++* Es2) t3
_++h*_ {Es1 = Es1} xs [] rewrite ++*-unit Es1      = xs
_++h*_ {Es1 = Es1} xs (_∷_ {E = E} {Es = Es} x ys) rewrite ++*-assoc Es1 {Es} {E ∷ []} = x ∷ (xs ++h* ys)

mkEhole* : ∀ {Γ} {a b} (E : ECxt* Γ a b) {t} → Ehole* (E [ t ]*) E t
mkEhole* [] = []
mkEhole* (E ∷ Es) {t} = (proj₂ (mkEHole E) ∷ []) ++h* mkEhole* Es

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
-- There was a bug with the new constraint machinery
-- where a type error could be ignored and checking
-- continued.
module LostTypeError where

postulate
  Wrap : (A : Set) (P : A → Set) → A → Set
  wrap : ∀ A (P : A → Set) (x : A) → P x → Wrap A P x
  A    : Set

data Box : Set where
  box : A → Box

data Dummy : Set where
  box : Dummy

postulate
  x y : A
  P   : Box → Set
  px  : P (box x)

bad : Wrap Box P (box y)
bad = wrap _ (λ a → P _) (box x) px

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

-- Also called "Girard's paradox" or "Russell's paradox".
module Miscellaneous.TypeInTypeInconsistency where

data ISet : Set where
  set : ∀{I : Set} → (I → ISet) → ISet

open import Functional
open import Logic.Predicate
open import Logic.Propositional
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Relator
open import Syntax.Function

_∉_ : ISet → ISet → Set
a ∉ set(b) = ∀{ib} → (a ≢ b(ib))

NotSelfContaining : ISet → Set
NotSelfContaining(a) = a ∉ a

NotSelfContainingSet : ISet
NotSelfContainingSet = set{∃(NotSelfContaining)} [∃]-witness

is-not-in : NotSelfContainingSet ∉ NotSelfContainingSet
is-not-in {[∃]-intro (set a) ⦃ proof ⦄} p = substitute₁ₗ(NotSelfContaining) p (\{_} → proof) {[∃]-intro (set a) ⦃ \{_} → proof ⦄} p

is-in : ¬(NotSelfContainingSet ∉ NotSelfContainingSet)
is-in p = p {[∃]-intro NotSelfContainingSet ⦃ \{proof} → p{proof} ⦄ } [≡]-intro

contradiction : ⊥
contradiction = is-in (\{proof} → is-not-in {proof})

{-

open import Data.Tuple as Tuple using ()
open import Logic.Predicate
open import Logic.Propositional
open import Functional
import      Structure.Relator.Names as Names
open import Structure.Relator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Relator.Proofs
open import Structure.Setoid using (Equiv)
open import Syntax.Transitivity

_≡_ : ISet → ISet → Set
_∈_ : ISet → ISet → Set
_∉_ : ISet → ISet → Set

set {Ia} a ≡ set {Ib} b = ∃{Obj = Ib → Ia}(f ↦ ∀{ib} → (a(f(ib)) ≡ b(ib))) ∧ ∃{Obj = Ia → Ib}(f ↦ ∀{ia} → (a(ia) ≡ b(f(ia))))
a ∈ set(b) = ∃(ib ↦ (a ≡ b(ib)))
_∉_ = (¬_) ∘₂ (_∈_)

instance
  [≡]-reflexivity : Reflexivity(_≡_)
  [≡]-reflexivity = intro p where
    p : Names.Reflexivity(_≡_)
    p {set a} = [∧]-intro ([∃]-intro id ⦃ p ⦄) ([∃]-intro id ⦃ p ⦄)

instance
  [≡]-symmetry : Symmetry(_≡_)
  [≡]-symmetry = intro p where
    p : Names.Symmetry(_≡_)
    p {set a}{set b} ([∧]-intro l r) = [∧]-intro ([∃]-map-proof (\eq {i} → p(eq{i})) r) (([∃]-map-proof (\eq {i} → p(eq{i})) l))

instance
  [≡]-transitivity : Transitivity(_≡_)
  [≡]-transitivity = intro p where
    p : Names.Transitivity(_≡_)
    p {set x} {set y} {set z} ([↔]-intro ([∃]-intro fyx ⦃ yx ⦄) ([∃]-intro fxy ⦃ xy ⦄)) ([↔]-intro ([∃]-intro fzy ⦃ zy ⦄) ([∃]-intro fyz ⦃ yz ⦄)) = [∧]-intro ([∃]-intro (fyx ∘ fzy) ⦃ p yx zy ⦄) ([∃]-intro (fyz ∘ fxy) ⦃ p xy yz ⦄)

instance
  [≡]-equivalence : Equivalence(_≡_)
  [≡]-equivalence = intro

instance
  [≡]-equiv : Equiv(ISet)
  Equiv._≡_         [≡]-equiv = (_≡_)
  Equiv.equivalence [≡]-equiv = [≡]-equivalence

instance
  [∈]-unaryOperatorₗ : ∀{b} → UnaryRelator(_∈ b)
  UnaryRelator.substitution ([∈]-unaryOperatorₗ {set b}) {a₁} {a₂} a1a2 = [∃]-map-proof (symmetry(_≡_) a1a2 🝖_)

instance
  [∈]-unaryOperatorᵣ : ∀{a} → UnaryRelator(a ∈_)
  UnaryRelator.substitution ([∈]-unaryOperatorᵣ {a}) {set b₁} {set b₂} ([∧]-intro _ ([∃]-intro fb1b2 ⦃ b1b2 ⦄)) ([∃]-intro ib₁ ⦃ p ⦄) = [∃]-intro (fb1b2(ib₁)) ⦃ p 🝖 b1b2 ⦄

instance
  [∈]-binaryOperator : BinaryRelator(_∈_)
  [∈]-binaryOperator = binaryRelator-from-unaryRelator

NotSelfContaining : ISet
NotSelfContaining = set{∃(a ↦ (a ∉ a))} [∃]-witness

NotSelfContaining-membership : ∀{x} → (x ∈ NotSelfContaining) ↔ (x ∉ x)
NotSelfContaining-membership = [↔]-intro l r where
  l : ∀{x} → (x ∈ NotSelfContaining) ← (x ∉ x)
  ∃.witness (l {x} xin) = [∃]-intro x ⦃ xin ⦄
  ∃.proof   (l {x} xin) = reflexivity(_≡_)

  r : ∀{x} → (x ∈ NotSelfContaining) → (x ∉ x)
  r {x} ([∃]-intro ([∃]-intro witness ⦃ nxinx ⦄) ⦃ p ⦄) xinx = nxinx(substitute₂(_∈_) p p xinx)

NotSelfContaining-self : (NotSelfContaining ∈ NotSelfContaining)
∃.witness NotSelfContaining-self = [∃]-intro NotSelfContaining ⦃ \{s@([∃]-intro ([∃]-intro _ ⦃ p ⦄) ⦃ b ⦄) → p(substitute₂(_∈_) b b s)} ⦄
∃.proof NotSelfContaining-self = [∧]-intro ([∃]-intro id ⦃ reflexivity(_≡_) ⦄) ([∃]-intro id ⦃ reflexivity(_≡_) ⦄)

paradox : ⊥
paradox = [↔]-to-[→] NotSelfContaining-membership NotSelfContaining-self NotSelfContaining-self
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Base
open import Spaces.Circle
open import Integers

module Spaces.LoopSpaceCircle where

-- Path fibration

path-fib : S¹ → Set
path-fib t = (t ≡ base)

tot-path-fib : Set
tot-path-fib = Σ S¹ path-fib

tot-path-fib-is-contr : is-contr tot-path-fib
tot-path-fib-is-contr = pathto-is-contr base

-- Universal cover

succ-path : ℤ ≡ ℤ
succ-path = eq-to-path succ-equiv

universal-cover : S¹ → Set
universal-cover = S¹-rec-nondep Set ℤ succ-path

tot-cover : Set
tot-cover = Σ S¹ universal-cover

-- Transport in the universal cover
loop-to-succ : (n : ℤ) → transport universal-cover loop n ≡ succ n
loop-to-succ n = ! (trans-ap (λ A → A) universal-cover loop n)
                 ∘ (ap (λ t → transport (λ A → A) t n)
                        (S¹-β-loop-nondep Set ℤ succ-path)
                 ∘ trans-id-eq-to-path succ-equiv n)

{- The flattening lemma

Here is an HIT declaration for the CW-complex of real numbers:

data ℝ : Set where
  z : ℤ → ℝ
  e : (n : ℤ) → z n ≡ z (succ n)

We want to show that [tot-cover] has the same introduction and elimination
rules.
-}

-- Introduction rules

R-z : ℤ → tot-cover
R-z n = (base , n)

R-e : (n : ℤ) → R-z n ≡ R-z (succ n)
R-e n = Σ-eq loop (loop-to-succ n)

-- Elimination rule
module Tot-cover-is-ℝ
  {i}
  (P : tot-cover → Set i)
  (z : (n : ℤ) → P (R-z n))
  (e : (n : ℤ) → transport P (R-e n) (z n) ≡ z (succ n)) where

  -- I redefine [R-e] and [e] to have something involving
  -- [transport universal-cover loop] instead of [succ]
  R-e' : (n : ℤ) → R-z n ≡ R-z (transport universal-cover loop n)
  R-e' n = Σ-eq loop refl

  e' : (n : ℤ) → transport P (R-e' n) (z n)
                 ≡ z (transport universal-cover loop n)
  e' n = (trans-totalpath universal-cover P {x = (base , n)}
                          {y = (base , transport universal-cover loop n)}
                          loop refl z
         ∘ move!-transp-left (λ z → P (base , z)) _ (loop-to-succ n)
           (z (succ n))
           (! (trans-totalpath universal-cover P {x = (base , n)}
                               {y = (base , succ n)} loop (loop-to-succ n) z)
            ∘ e n))
          ∘ apd z (! (loop-to-succ n))

  -- Now I can prove what I want by induction on the circle

  P-base : (t : universal-cover base) → P (base , t)
  P-base t = z t

  P-loop : (t : universal-cover base)
    → transport (λ x → (u : universal-cover x) → P (x , u)) loop P-base t
      ≡ P-base t
  P-loop t = transport (λ t → transport
                                (λ x → (u : universal-cover x) → P (x , u))
                                loop P-base t ≡ P-base t)
               (trans-trans-opposite universal-cover loop t)
               (! (trans-totalpath universal-cover P
                                   loop refl z)
               ∘ e' (transport universal-cover (! loop) t))

  P-R-rec : (x : S¹) → (t : universal-cover x) → P (x , t)
  P-R-rec = S¹-rec (λ x → (t : universal-cover x) → P (x , t))
                   P-base (funext P-loop)

  -- Here is the conclusion of the elimination rule
  R-rec : (t : tot-cover) → P t
  R-rec (x , y) = P-R-rec x y

-- We can now prove that [tot-cover] is contractible using [R-rec], that’s a
-- little tedious but not difficult

P-R-contr : (x : tot-cover) → Set _
P-R-contr x = R-z O ≡ x

R-contr-base : (n : ℤ) → P-R-contr (R-z n)
R-contr-base O = refl
R-contr-base (pos O) = R-e O
R-contr-base (pos (S y)) = R-contr-base (pos y) ∘ R-e (pos y)
R-contr-base (neg O) = ! (R-e (neg O))
R-contr-base (neg (S y)) = R-contr-base (neg y) ∘ ! (R-e (neg (S y)))

R-contr-loop : (n : ℤ)
  → transport P-R-contr (R-e n) (R-contr-base n) ≡ (R-contr-base (succ n))
R-contr-loop O = trans-cst≡id (R-e O) refl
R-contr-loop (pos O) = trans-cst≡id (R-e (pos O)) (R-e O)
R-contr-loop (pos (S y)) = trans-cst≡id (R-e (pos (S y)))
  (R-contr-base (pos y) ∘ R-e (pos y))
R-contr-loop (neg O) = trans-cst≡id (R-e (neg O))
  (! (R-e (neg O))) ∘ opposite-left-inverse (R-e (neg O))
R-contr-loop (neg (S y)) =
  ((trans-cst≡id (R-e (neg (S y))) (R-contr-base (neg y) ∘ ! (R-e (neg (S y))))
   ∘ concat-assoc (R-contr-base (neg y)) (! (R-e (neg (S y))))
                  (R-e (neg (S y))))
   ∘ (whisker-left (R-contr-base (neg y))
                   (opposite-left-inverse (R-e (neg (S y))))))
   ∘ refl-right-unit (R-contr-base (neg y))

R-contr : (x : tot-cover) → P-R-contr x
R-contr = Tot-cover-is-ℝ.R-rec P-R-contr R-contr-base R-contr-loop

tot-cover-is-contr : is-contr tot-cover
tot-cover-is-contr = (R-z O , λ x → ! (R-contr x))

-- We define now a fiberwise map between the two fibrations [path-fib]
-- and [universal-cover]
fiberwise-map : (x : S¹) → (path-fib x → universal-cover x)
fiberwise-map x p = transport universal-cover (! p) O

-- This induces an equivalence on the total spaces, because both total spaces
-- are contractible
total-is-equiv : is-equiv (total-map fiberwise-map)
total-is-equiv = contr-to-contr-is-equiv (total-map fiberwise-map)
                                         tot-path-fib-is-contr
                                         tot-cover-is-contr

-- Hence an equivalence fiberwise
fiberwise-map-is-equiv : (x : S¹) → is-equiv (fiberwise-map x)
fiberwise-map-is-equiv x = fiberwise-is-equiv fiberwise-map total-is-equiv x

-- We can then conclude that the based loop space of the circle is equivalent to
-- the type of the integers
ΩS¹≃ℤ : (base ≡ base) ≃ ℤ
ΩS¹≃ℤ = (fiberwise-map base , fiberwise-map-is-equiv base)

-- We can also deduce that the circle is 1-truncated

ΩS¹-is-set : is-set (base ≡ base)
ΩS¹-is-set = equiv-types-truncated _ (ΩS¹≃ℤ ⁻¹) ℤ-is-set

S¹-is-gpd : is-gpd S¹
S¹-is-gpd =
  S¹-rec _
    (S¹-rec _
      ΩS¹-is-set  -- [base ≡ base] is a set
      (π₁ (is-truncated-is-prop _ _ _)))
    (funext
      (S¹-rec _
        (π₁ (is-truncated-is-prop _ _ _))
        (prop-has-all-paths (≡-is-truncated _ (is-truncated-is-prop _)) _ _)))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Oscar.Prelude
open import Oscar.Class.Reflexivity
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity

module Oscar.Class.IsEquivalence where

record IsEquivalence
  {𝔬} {𝔒 : Ø 𝔬}
  {ℓ} (_≈_ : 𝔒 → 𝔒 → Ø ℓ)
  : Ø 𝔬 ∙̂ ℓ where
  constructor ∁
  field
    ⦃ `𝓡eflexivity ⦄ : Reflexivity.class _≈_
    ⦃ `𝓢ymmetry ⦄ : Symmetry.class _≈_
    ⦃ `𝓣ransitivity  ⦄ : Transitivity.class _≈_


text:
module AmbiguousName where

module A where
  postulate X : Set

module B where
  module A where
    postulate X : Set

open A renaming (X to Y)
open B

Z = A.X


text:
module Lib.Id where

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

cong : {A B : Set}(f : A -> B){x y : A} -> x ≡ y -> f x ≡ f y
cong f refl = refl

subst : {A : Set}(P : A -> Set){x y : A} -> x ≡ y -> P y -> P x
subst P refl px = px

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module inspect where

open import eq

-- From Norell's tutorial:

data Inspect {A : Set}(x : A) : Set where
  it : (y : A) -> x ≡ y -> Inspect x

inspect : {A : Set}(x : A) -> Inspect x
inspect x = it x refl

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


text:
open import HoTT
open import groups.Exactness
open import groups.HomSequence

module groups.ExactSequence where

is-exact-seq : ∀ {i} {G H : Group i}
  → HomSequence G H → Type i
is-exact-seq (_ ⊣|ᴳ) = Lift ⊤
is-exact-seq (_ →⟨ φ ⟩ᴳ _ ⊣|ᴳ) = Lift ⊤
is-exact-seq (_ →⟨ φ ⟩ᴳ _ →⟨ ψ ⟩ᴳ seq) =
  is-exact φ ψ × is-exact-seq (_ →⟨ ψ ⟩ᴳ seq)

ExactSequence : ∀ {i} (G H : Group i) → Type (lsucc i)
ExactSequence G H = Σ (HomSequence G H) is-exact-seq

{- equivalences preserve exactness -}

abstract
  seq-equiv-preserves-exact : ∀ {i₀ i₁} {G₀ H₀ : Group i₀} {G₁ H₁ : Group i₁}
    {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    → HomSeqEquiv seq₀ seq₁ ξG ξH
    → is-exact-seq seq₀ → is-exact-seq seq₁
  seq-equiv-preserves-exact ((_ ↓|ᴳ) , _) _ = lift tt
  seq-equiv-preserves-exact ((_ ↓⟨ _ ⟩ᴳ _ ↓|ᴳ) , _) _ = lift tt
  seq-equiv-preserves-exact
    ( (ξG ↓⟨ φ□ ⟩ᴳ _↓⟨_⟩ᴳ_ ξH {ξK} ψ□ seq-map)
    , (ξG-ise , ξH-ise , seq-map-ise))
    (φ₀-ψ₀-is-exact , ψ₀-seq₀-is-exact-seq) =
      equiv-preserves-exact
        φ□ ψ□ ξG-ise ξH-ise (is-seqᴳ-equiv.head seq-map-ise)
        φ₀-ψ₀-is-exact ,
      seq-equiv-preserves-exact
        ((ξH ↓⟨ ψ□ ⟩ᴳ seq-map) , (ξH-ise , seq-map-ise))
        ψ₀-seq₀-is-exact-seq

  seq-equiv-preserves'-exact : ∀ {i} {G₀ G₁ H₀ H₁ : Group i}
    {seq₀ : HomSequence G₀ H₀} {seq₁ : HomSequence G₁ H₁}
    {ξG : G₀ →ᴳ G₁} {ξH : H₀ →ᴳ H₁}
    → HomSeqEquiv seq₀ seq₁ ξG ξH
    → is-exact-seq seq₁ → is-exact-seq seq₀
  seq-equiv-preserves'-exact seq-equiv =
    seq-equiv-preserves-exact (HomSeqEquiv-inverse seq-equiv)

private
  exact-seq-index-type : ∀ {i} {G H : Group i} → ℕ → HomSequence G H → Type i
  exact-seq-index-type _ (G ⊣|ᴳ) = Lift ⊤
  exact-seq-index-type _ (G →⟨ φ ⟩ᴳ H ⊣|ᴳ) = Lift ⊤
  exact-seq-index-type O (G →⟨ φ ⟩ᴳ H →⟨ ψ ⟩ᴳ s) = is-exact φ ψ
  exact-seq-index-type (S n) (_ →⟨ _ ⟩ᴳ s) = exact-seq-index-type n s

abstract
  exact-seq-index : ∀ {i} {G H : Group i}
    → (n : ℕ) (seq : ExactSequence G H)
    → exact-seq-index-type n (fst seq)
  exact-seq-index _     ((G ⊣|ᴳ) , _) = lift tt
  exact-seq-index _     ((G →⟨ φ ⟩ᴳ H ⊣|ᴳ) , _) = lift tt
  exact-seq-index O     ((G →⟨ φ ⟩ᴳ H →⟨ ψ ⟩ᴳ seq) , ise-seq) = fst ise-seq
  exact-seq-index (S n) ((G →⟨ φ ⟩ᴳ H →⟨ ψ ⟩ᴳ seq) , ise-seq) =
    exact-seq-index n ((H →⟨ ψ ⟩ᴳ seq) , snd ise-seq)

{-
private
  exact-build-arg-type : ∀ {i} {G H : Group i} → HomSequence G H → List (Type i)
  exact-build-arg-type (G ⊣|) = nil
  exact-build-arg-type (G ⟨ φ ⟩→ H ⊣|) = nil
  exact-build-arg-type (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ s) =
    is-exact φ ψ :: exact-build-arg-type (H ⟨ ψ ⟩→ s)

  exact-build-helper : ∀ {i} {G H : Group i} (seq : HomSequence G H)
    → HList (exact-build-arg-type seq) → is-exact-seq seq
  exact-build-helper (G ⊣|) nil = exact-seq-zero
  exact-build-helper (G ⟨ φ ⟩→ H ⊣|) nil = exact-seq-one
  exact-build-helper (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ s) (ie :: ies) =
    exact-seq-more ie (exact-build-helper (H ⟨ ψ ⟩→ s) ies)

exact-build : ∀ {i} {G H : Group i} (seq : HomSequence G H)
  → hlist-curry-type (exact-build-arg-type seq) (λ _ → is-exact-seq seq)
exact-build seq = hlist-curry (exact-build-helper seq)

hom-seq-concat : ∀ {i} {G H K : Group i}
  → HomSequence G H → HomSequence H K → HomSequence G K
hom-seq-concat (G ⊣|) s₂ = s₂
hom-seq-concat (G ⟨ φ ⟩→ s₁) s₂ = G ⟨ φ ⟩→ (hom-seq-concat s₁ s₂)

abstract
  exact-concat : ∀ {i} {G H K L : Group i}
    {seq₁ : HomSequence G H} {φ : H →ᴳ K} {seq₂ : HomSequence K L}
    → is-exact-seq (hom-seq-snoc seq₁ φ) → is-exact-seq (H ⟨ φ ⟩→ seq₂)
    → is-exact-seq (hom-seq-concat seq₁ (H ⟨ φ ⟩→ seq₂))
  exact-concat {seq₁ = G ⊣|} exact-seq-one es₂ = es₂
  exact-concat {seq₁ = G ⟨ ψ ⟩→ H ⊣|} (exact-seq-more ex _) es₂ =
    exact-seq-more ex es₂
  exact-concat {seq₁ = G ⟨ ψ ⟩→ H ⟨ χ ⟩→ s} (exact-seq-more ex es₁) es₂ =
    exact-seq-more ex (exact-concat {seq₁ = H ⟨ χ ⟩→ s} es₁ es₂)
-}

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- The partiality monad
------------------------------------------------------------------------

module Category.Monad.Partiality where

open import Coinduction
open import Category.Monad
open import Data.Nat
open import Data.Bool

-- The partiality monad.

data _⊥ (A : Set) : Set where
  now   : (x : A) → A ⊥
  later : (x : ∞ (A ⊥)) → A ⊥

monad : RawMonad _⊥
monad = record
  { return = now
  ; _>>=_  = _>>=_
  }
  where
  _>>=_ : ∀ {A B} → A ⊥ → (A → B ⊥) → B ⊥
  now x   >>= f = f x
  later x >>= f = later (♯ ♭ x >>= f)

-- run x for n steps peels off at most n "later" constructors from x.

run_for_steps : ∀ {A} → A ⊥ → ℕ → A ⊥
run now   x for n     steps = now x
run later x for zero  steps = later x
run later x for suc n steps = run ♭ x for n steps

-- Is the computation done?

isNow : ∀ {A} → A ⊥ → Bool
isNow (now x)   = true
isNow (later x) = false

------------------------------------------------------------------------
-- Productivity checker workaround

-- The monad can be awkward to use, due to the limitations of guarded
-- coinduction. The following code provides a (limited) workaround.

infixl 1 _>>=_

data _⊥-prog : Set → Set₁ where
  now   : ∀ {A} (x : A) → A ⊥-prog
  later : ∀ {A} (x : ∞₁ (A ⊥-prog)) → A ⊥-prog
  _>>=_ : ∀ {A B} (x : A ⊥-prog) (f : A → B ⊥-prog) → B ⊥-prog

data _⊥-whnf : Set → Set₁ where
  now   : ∀ {A} (x : A) → A ⊥-whnf
  later : ∀ {A} (x : A ⊥-prog) → A ⊥-whnf

whnf : ∀ {A} → A ⊥-prog → A ⊥-whnf
whnf (now   x) = now x
whnf (later x) = later (♭₁ x)
whnf (x >>= f) with whnf x
whnf (x >>= f) | now   x′ = whnf (f x′)
whnf (x >>= f) | later x′ = later (x′ >>= f)

mutual

  value : ∀ {A} → A ⊥-whnf → A ⊥
  value (now   x) = now x
  value (later x) = later (♯ run x)

  run : ∀ {A} → A ⊥-prog → A ⊥
  run x = value (whnf x)

------------------------------------------------------------------------
-- Examples

module Examples where

  open import Relation.Nullary

  -- McCarthy's f91:

  f91′ : ℕ → ℕ ⊥-prog
  f91′ n with n ≤? 100
  ... | yes _ = later (♯₁ (f91′ (11 + n) >>= f91′))
  ... | no  _ = now (n ∸ 10)

  f91 : ℕ → ℕ ⊥
  f91 n = run (f91′ n)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module _ (A : Set) where

open import Issue1701.ModParamsToLose
module ParamA = Param A
open ParamA

failed : (A → A) → A → A
failed G = S.F
  module fails where
    module S = r A G


text:
{-# OPTIONS --universe-polymorphism #-}
module Reflection where

open import Common.Prelude hiding (Unit; module Unit) renaming (Nat to ℕ; module Nat to ℕ)
open import Common.Reflect

data _≡_ {a}{A : Set a}(x : A) : A → Set a where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

data Id {A : Set}(x : A) : (B : Set) → B → Set where
  course : Id x A x

primitive
  primTrustMe : ∀{a}{A : Set a}{x y : A} → x ≡ y

open import Common.Level

unEl : Type → Term
unEl (el _ t) = t

argᵛʳ : ∀{A} → A → Arg A
argᵛʳ = arg (arginfo visible relevant)

argʰʳ : ∀{A} → A → Arg A
argʰʳ = arg (arginfo hidden relevant)

el₀ : Term → Type
el₀ = el (lit 0)

el₁ : Term → Type
el₁ = el (lit 1)

set₀ : Type
set₀ = el₁ (sort (lit 0))

unCheck : Term → Term
unCheck (def x (_ ∷ _ ∷ arg _ t ∷ [])) = t
unCheck t = unknown

data Check {a}{A : Set a}(x : A) : Set where
  _is_of_ : (t t′ : Term) →
            Id (primTrustMe {x = unCheck t} {t′})
               (t′ ≡ t′) refl → Check x

`Check : QName
`Check = quote Check

test₁ : Check ({A : Set} → A → A)
test₁ = quoteGoal t in
        t is pi (argʰʳ set₀) (el₀ (pi (argᵛʳ (el₀ (var 0 []))) (el₀ (var 1 []))))
        of course

test₂ : (X : Set) → Check (λ (x : X) → x)
test₂ X = quoteGoal t in
          t is lam visible (var 0 []) of course

infixr 40 _`∷_

_`∷_ : Term → Term → Term
x `∷ xs = con (quote _∷_) (argᵛʳ x ∷ argᵛʳ xs ∷ [])
`[]     = con (quote []) []
`true   = con (quote true) []
`false  = con (quote false) []

test₃ : Check (true ∷ false ∷ [])
test₃ = quoteGoal t in
        t is `true `∷ `false `∷ `[] of course

`List : Term → Term
`List A = def (quote List) (argᵛʳ A ∷ [])
`ℕ      = def (quote ℕ) []

`Term : Term
`Term = def (quote Term) []
`Type : Term
`Type = def (quote Type) []
`Sort : Term
`Sort = def (quote Sort) []

test₄ : Check (List ℕ)
test₄ = quoteGoal t in
        t is `List `ℕ of course

test₅ : primQNameType (quote Term) ≡ set₀
test₅ = refl

-- TODO => test₆ : primQNameType (quote set₀) ≡ el unknown `Type ≢ el₀ `Type
test₆ : unEl (primQNameType (quote set₀)) ≡ `Type
test₆ = refl

test₇ : primQNameType (quote Sort.lit) ≡ el₀ (pi (argᵛʳ (el₀ `ℕ)) (el₀ `Sort))
test₇ = refl

mutual
  ℕdef : DataDef
  ℕdef = _

  test₈ : dataDef ℕdef ≡ primQNameDefinition (quote ℕ)
  test₈ = refl

test₉ : primDataConstructors ℕdef ≡ quote ℕ.zero ∷ quote ℕ.suc ∷ []
test₉ = refl

test₁₀ : primQNameDefinition (quote ℕ.zero) ≡ dataConstructor
test₁₀ = refl

postulate
  a : ℕ

test₁₁ : primQNameDefinition (quote a) ≡ axiom
test₁₁ = refl

test₁₂ : primQNameDefinition (quote primQNameDefinition) ≡ prim
test₁₂ = refl

record Unit : Set where

mutual
  UnitDef : RecordDef
  UnitDef = _

  test₁₃ : recordDef UnitDef ≡ primQNameDefinition (quote Unit)
  test₁₃ = refl

test₁₄ : Check 1
test₁₄ = quoteGoal t in
           t is con ( quote ℕ.suc ) (argᵛʳ (con (quote ℕ.zero) []) ∷ [])
           of course

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module tests.Mutual where

open import Prelude.IO
open import Prelude.String
open import Prelude.Unit

mutual
  data G : Set where
    GA : {g : G}(f : F g) -> G
    GB : G

  data F : G -> Set where
    FA : (g : G) -> F g
    FB : F GB

mutual
  incG : G -> G
  incG GB     = GA FB
  incG (GA f) = GA (incF f)

  incF : {g : G} -> F g -> F (incG g)
  incF FB     = FA (GA FB)
  incF (FA g) = FA (incG g)

mutual
  PrintF : {g : G} -> F g -> String
  PrintF FB = "FB"
  PrintF (FA g) = "(FA " +S+ PrintG g +S+ ")"

  PrintG : G -> String
  PrintG GB     = "GB"
  PrintG (GA f) = "(GA " +S+ PrintF f +S+ ")"

main : IO Unit
main =
    putStrLn (PrintF (FA (GA (FA GB)))) ,,
    putStrLn (PrintG (incG (GA (incF FB)))) ,, --
    return unit


text:
data A : Set where
  consA : A → A

A-false : {Y : Set} → A → Y
A-false (consA b) = A-false b

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

A-on-Nat : A → Nat → Nat
A-on-Nat σ zero = A-false σ
A-on-Nat σ (suc t) = suc (A-on-Nat σ t)

module _
  (any : {X : Set} → X)
  (P : Nat → Set)
  (p : (n : Nat) → P n → P (suc n))
  (eternity : (a : A) (n : Nat) → P (A-on-Nat (A-false a) n))
  where

  A-loop-term : (a : A) (n : Nat) → P (A-on-Nat a n)
  A-loop-term a zero = any
  A-loop-term a (suc n) = p _ (eternity _ n)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Core.Everything where

-- Basic primitives (some are from Agda.Primitive)
open import Cubical.Core.Primitives public

-- Definition of equivalences and Glue types
open import Cubical.Core.Glue public

-- Definition of cubical Identity types
open import Cubical.Core.Id

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Andreas, 2019-03-02, issue #3601 reported by 3abc

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

open import Agda.Primitive.Cubical renaming
  (primINeg to ~_; primIMin to _∧_; primTransp to transp)

open import Agda.Builtin.Cubical.Path

module _ (A : Set) (x y z t : A) (f : y ≡ z) (g : y ≡ x) (h : z ≡ t) where

  test : PathP (λ i → g i ≡ h i) f (transp (λ i → g i ≡ h i) i0 f)
  test k i = transp (λ i → g (i ∧ k) ≡ h (i ∧ k)) (~ k) f i

-- Should pass.
-- Problem was: Agda did not accept overapplied primTransp

  -- Also should pass.
  -- We had a problem with checking the sides at the right type.
  test2 : ∀ {ℓ} (i : I) {A : Partial i (Set ℓ)}
          → PartialP i (λ z → A z)
          → (r : IsOne i)
          → A r
  test2 i {A} u r = primPOr i i {A} u (λ o → u o) r


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax STLC | Λ

type
  N   : 0-ary
  _↣_ : 2-ary | r30

term
  app : α ↣ β  α  ->  β | _$_ l20
  lam : α.β  ->  α ↣ β | ƛ_ r10

theory
  (ƛβ) b : α.β  a : α |> app (lam(x.b[x]), a) = b[a]
  (ƛη) f : α ↣ β      |> lam (x. app(f, x))   = f
-}

module STLC.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import STLC.Signature
open import STLC.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution Λ:Syn
open import SOAS.Metatheory.SecondOrder.Equality Λ:Syn

private
  variable
    α β γ τ : ΛT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ Λ) α Γ → (𝔐 ▷ Λ) α Γ → Set where
  ƛβ : ⁅ α ⊩ β ⁆ ⁅ α ⁆̣ ▹ ∅ ⊢ (ƛ 𝔞⟨ x₀ ⟩) $ 𝔟 ≋ₐ 𝔞⟨ 𝔟 ⟩
  ƛη : ⁅ α ↣ β ⁆̣       ▹ ∅ ⊢      ƛ (𝔞 $ x₀) ≋ₐ 𝔞

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
open import bool
open import eq using (_≡_)
open import nat
open import nat-thms
open import z05-01-hc-slist2-base

module z05-01-hc-slist2-test where

data _R≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero R≤ n

  s≤s : ∀ {m n : ℕ}
    →     m R≤     n
      -------------
    → suc m R≤ suc n

≤-pred : ∀ {m n} → suc m R≤ suc n → m R≤ n
≤-pred (s≤s m≤n) = m≤n

_≤?_ : Decidable _R≤_
zero  ≤? _     = left z≤n
suc m ≤? zero  = right λ()
suc m ≤? suc n with m ≤? n
... | left  m≤n = left  (s≤s m≤n)
... | right m≰n = right λ x → m≰n (≤-pred x)

ℕ-Equivalence : Equivalence {X = ℕ} _≡_
ℕ-Equivalence = record
  { refl  = _≡_.refl
  ; sym   = λ x≡y → eq.sym x≡y
  ; trans = λ {_≡_.refl _≡_.refl → eq.trans _≡_.refl _≡_.refl} }

xR≤y→x≤y≡tt : ∀ {x y : ℕ} → x R≤ y → x ≤ y ≡ bool.𝔹.tt
xR≤y→x≤y≡tt {x} {y}  z≤n       = 0-≤ y
xR≤y→x≤y≡tt {x} {y} (s≤s xR≤y) = xR≤y→x≤y≡tt xR≤y

x≤y≡tt→xR≤y : ∀ {x y : ℕ} → x ≤ y ≡ bool.𝔹.tt → x R≤ y
x≤y≡tt→xR≤y  {zero} {_}         _ = z≤n
x≤y≡tt→xR≤y {suc x} {y} sucx≤y≡tt = {!!} -- TODO

R≤-total : (x y : ℕ) → Either (x R≤ y) (y R≤ x)
R≤-total zero     zero   = left z≤n
R≤-total zero    (suc y) = left z≤n
R≤-total (suc x)  zero   = right z≤n
R≤-total (suc x) (suc y) with R≤-total x y
... | left  l = left  (s≤s l)
... | right r = right (s≤s r)

x≡y→xR≤y : ∀ {x y : ℕ} → x ≡ y → x R≤ y
x≡y→xR≤y  {zero}        {_}        _ = z≤n
x≡y→xR≤y {suc x} {.(suc x)} _≡_.refl = s≤s (x≤y≡tt→xR≤y (≤-refl x))

ℕ-TotalOrder : TotalOrder {X = ℕ} _≡_ _R≤_
ℕ-TotalOrder = record
  { antisym     = λ x≤y y≤x → ≤-antisym (xR≤y→x≤y≡tt x≤y) (xR≤y→x≤y≡tt y≤x)
  ; trans       = λ {x} {y} {z} xR≤y yR≤z →
                    x≤y≡tt→xR≤y (≤-trans {x} {y} {z} (xR≤y→x≤y≡tt xR≤y) (xR≤y→x≤y≡tt yR≤z))
  ; total       = R≤-total
  ; reflexive   = x≡y→xR≤y
  ; equivalence = ℕ-Equivalence
  }

import z05-01-hc-slist2-list as SL
open   SL {ℕ}
          {_≡_}
          {_R≤_}
          _≤?_
          ℕ-TotalOrder

empty : OList ⟦ 0 ⟧ ⟦ 9 ⟧
empty = nil (≤-lift z≤n)

l-9 : OList ⟦ 0 ⟧ ⟦ 9 ⟧
l-9 = insert 9 empty (≤-lift z≤n) (≤-lift (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))))))

l-5-9 : OList ⟦ 0 ⟧ ⟦ 9 ⟧
l-5-9 = insert 5 l-9 (≤-lift z≤n) (≤-lift (s≤s (s≤s (s≤s (s≤s (s≤s z≤n))))))

l-1-5-9 : OList ⟦ 0 ⟧ ⟦ 9 ⟧
l-1-5-9 = insert 1 l-5-9 (≤-lift z≤n) (≤-lift (s≤s z≤n))

l-1-5-9' : OList ⊥ ⊤
l-1-5-9' = isort' (9 ∷ 1 ∷ 5 ∷ [])

-- cannot do because lower/upper indices different : l-1-5-9 ≡ l-1-5-9'
_ : toList l-1-5-9 ≡ toList l-1-5-9'
_ = eq.refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Data.Maybe.Primitive where
{-# IMPORT Data.Maybe #-}

-- In Agda 2.2.10 and below, there's no FFI binding for the stdlib
-- Maybe type, so we have to roll our own. This will change.

data #Maybe (X : Set) : Set where
  just : X → #Maybe X
  nothing : #Maybe X
{-# COMPILED_DATA #Maybe Data.Maybe.Maybe Data.Maybe.Just Data.Maybe.Nothing #-}

max_stars_repo_name: agda/agda-data-bindings

max_issues_repo_name: agda/agda-data-bindings

max_forks_repo_name: agda/agda-data-bindings


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection

macro
  printType : Term → TC ⊤
  printType hole = bindTC (inferType hole) λ t → typeError (termErr t ∷ [])

test1 : (a : Nat) → Nat
test1 = {! printType  !}

test2 : (a : Bool) → Bool
test2 = {! printType  !}


text:
module naturals where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- 1)
seven : ℕ
seven = suc (suc (suc (suc (suc (suc (suc zero))))))

{-# BUILTIN NATURAL ℕ #-}

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

-- 2)
_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc (suc (0 + 4)))
  ≡⟨⟩
    suc (suc (suc 4))
  ≡⟨⟩
    suc (suc 5)
  ≡⟨⟩
    suc 6
  ≡⟨⟩
    7
  ∎

_*_ : ℕ → ℕ → ℕ
zero * n  =  zero
(suc m) * n  =  n + (m * n)

-- 3)
_ : 3 * 4 ≡ 12
_ =
  begin
    3 * 4
  ≡⟨⟩
    4 + (2 * 4)
  ≡⟨⟩
    4 + (4 + (1 * 4))
  ≡⟨⟩
    4 + (4 + (4 + (0 * 4)))
  ≡⟨⟩
    4 + (4 + (4 + 0))
  ≡⟨⟩
    4 + (4 + (4))
  ≡⟨⟩
    12
  ∎

-- 4)
_^_ : ℕ → ℕ → ℕ
m ^ zero = suc zero
m ^ suc n = m * (m ^ n)

_ : 3 ^ 4 ≡ 81
_ =
  begin
    3 ^ 4
  ≡⟨⟩
    3 * (3 ^ 3)
  ≡⟨⟩
    3 * (3 * (3 ^ 2))
  ≡⟨⟩
    3 * (3 * (3 * (3 ^ 1)))
  ≡⟨⟩
    3 * (3 * (3 * (3 * (3 ^ 0))))
  ≡⟨⟩
    3 * (3 * (3 * (3 * 1)))
  ≡⟨⟩
    81
  ∎

_∸_ : ℕ → ℕ → ℕ
m ∸ zero   =  m
zero ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

-- 5)
_ : 5 ∸ 3 ≡ 2
_ =
  begin
    5 ∸ 3
  ≡⟨⟩
    4 ∸ 2
  ≡⟨⟩
    3 ∸ 1
  ≡⟨⟩
    2 ∸ 0
  ≡⟨⟩
    2
  ∎

_ : 3 ∸ 5 ≡ 0
_ =
  begin
    3 ∸ 5
  ≡⟨⟩
    2 ∸ 4
  ≡⟨⟩
    1 ∸ 3
  ≡⟨⟩
    0 ∸ 2
  ≡⟨⟩
    0
  ∎

infixl 6  _+_  _∸_
infixl 7  _*_

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

-- 6)
data Bin : Set where
  - : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc - = - I
inc (rest O) = rest I
inc (rest I) = (inc rest) O

to : ℕ → Bin
to zero = - O
to (suc n) = inc (to n)

from : Bin → ℕ
from - = 0
from (rest O) = 2 * from rest
from (rest I) = 2 * from rest + 1

max_stars_repo_name: aronerben/agda-playground

max_issues_repo_name: aronerben/agda-playground

max_forks_repo_name: aronerben/agda-playground


text:
{-# OPTIONS --copatterns --sized-types #-}
-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.conv:10 -v tc.conv.size:15 #-}
module Delay where

--open import Library
open import Size
open import Category.Monad
open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary public
import Relation.Binary.PreorderReasoning
module Pre = Relation.Binary.PreorderReasoning
open import Data.Product
-- Coinductive delay monad.

mutual

  data Delay (A : Set) (i : Size) : Set where
    now   : A → Delay A i
    later : ∞Delay A i → Delay A i

  record ∞Delay (A : Set) (i : Size) : Set where
    coinductive
    constructor delay
    field
      force : {j : Size< i} → Delay A j

open ∞Delay public

-- Smart constructor.

later! : ∀ {A i} → Delay A i → Delay A (↑ i)
later! x = later (delay x)

-- Monad instance.

module Bind where
  mutual
    _>>=_ : ∀ {i A B} → Delay A i → (A → Delay B i) → Delay B i
    now   x >>= f = f x
    later x >>= f = later (x ∞>>= f)

    _∞>>=_ :  ∀ {i A B} → ∞Delay A i → (A → Delay B i) → ∞Delay B i
    force (x ∞>>= f) = force x >>= f

delayMonad : ∀ {i} → RawMonad {f = lzero} (λ A → Delay A i)
delayMonad {i} = record
  { return = now
  ; _>>=_  = _>>=_ {i}
  } where open Bind

module _ {i : Size} where
  open module DelayMonad = RawMonad (delayMonad {i = i})
                           public renaming (_⊛_ to _<*>_)
open Bind public using (_∞>>=_)

-- Map for ∞Delay

_∞<$>_ : ∀ {i A B} (f : A → B) (∞a : ∞Delay A i) → ∞Delay B i
f ∞<$> ∞a = ∞a ∞>>= λ a → return (f a)
-- force (f ∞<$> ∞a) = f <$> force ∞a

-- Double bind

_=<<2_,_ : ∀ {i A B C} → (A → B → Delay C i) → Delay A i → Delay B i → Delay C i
f =<<2 x , y = x >>= λ a → y >>= λ b → f a b

-- Strong bisimilarity

mutual
  data _~_ {i : Size} {A : Set} : (a? b? : Delay A ∞) → Set where
    ~now   : ∀ a → now a ~ now a
    ~later : ∀ {a∞ b∞} (eq : _∞~_ {i} a∞ b∞) → later a∞ ~ later b∞

  record _∞~_ {i : Size} {A : Set} (a∞ b∞ : ∞Delay A ∞) : Set where
    coinductive
    constructor ~delay
    field
      ~force : {j : Size< i} → _~_ {j} (force a∞) (force b∞)

open _∞~_ public

-- Reflexivity

mutual
  ~refl  : ∀ {i A} (a? : Delay A ∞) → _~_ {i} a? a?
  ~refl (now a)    = ~now a
  ~refl (later a∞) = ~later (∞~refl a∞)

  ∞~refl : ∀ {i A} (a∞ : ∞Delay A ∞) → _∞~_ {i} a∞ a∞
  ~force (∞~refl a∞) = ~refl (force a∞)

-- Symmetry

mutual
  ~sym : ∀ {i A} {a? b? : Delay A ∞} → _~_ {i} a? b? → _~_ {i} b? a?
  ~sym (~now a)    = ~now a
  ~sym (~later eq) = ~later (∞~sym eq)

  ∞~sym : ∀ {i A} {a? b? : ∞Delay A ∞} → _∞~_ {i} a? b? → _∞~_ {i} b? a?
  ~force (∞~sym eq) = ~sym (~force eq)

-- Transitivity

mutual
  ~trans : ∀ {i A} {a? b? c? : Delay A ∞}
    (eq : _~_ {i} a? b?) (eq' : _~_ {i} b? c?) → _~_ {i} a? c?
  ~trans (~now a)    (~now .a)    = ~now a
  ~trans (~later eq) (~later eq') = ~later (∞~trans eq eq')

  ∞~trans : ∀ {i A} {a∞ b∞ c∞ : ∞Delay A ∞}
    (eq : _∞~_ {i} a∞ b∞) (eq' : _∞~_ {i} b∞ c∞) → _∞~_ {i} a∞ c∞
  ~force (∞~trans eq eq') = ~trans (~force eq) (~force eq')

-- Equality reasoning

~setoid : (i : Size) (A : Set) → Setoid lzero lzero
~setoid i A = record
  { Carrier       = Delay A ∞
  ; _≈_           = _~_ {i}
  ; isEquivalence = record
    { refl  = λ {a?} → ~refl a?
    ; sym   = ~sym
    ; trans = ~trans
    }
  }

module ~-Reasoning {i : Size} {A : Set} where
  open Pre (Setoid.preorder (~setoid i A)) public
--    using (begin_; _∎) (_≈⟨⟩_ to _~⟨⟩_; _≈⟨_⟩_ to _~⟨_⟩_)
    renaming (_≈⟨⟩_ to _≡⟨⟩_; _≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _~⟨_⟩_; begin_ to proof_)

∞~setoid : (i : Size) (A : Set) → Setoid lzero lzero
∞~setoid i A = record
  { Carrier       = ∞Delay A ∞
  ; _≈_           = _∞~_ {i}
  ; isEquivalence = record
    { refl  = λ {a?} → ∞~refl a?
    ; sym   = ∞~sym
    ; trans = ∞~trans
    }
  }

module ∞~-Reasoning {i : Size} {A : Set} where
  open Pre (Setoid.preorder (∞~setoid i A)) public
--    using (begin_; _∎) (_≈⟨⟩_ to _~⟨⟩_; _≈⟨_⟩_ to _~⟨_⟩_)
    renaming (_≈⟨⟩_ to _≡⟨⟩_; _≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _∞~⟨_⟩_; begin_ to proof_)

-- Congruence laws.

mutual
  bind-cong-l : ∀ {i A B} {a? b? : Delay A ∞} (eq : _~_ {i} a? b?)
    (k : A → Delay B ∞) → _~_ {i} (a? >>= k) (b? >>= k)
  bind-cong-l (~now a)    k = ~refl _
  bind-cong-l (~later eq) k = ~later (∞bind-cong-l eq k)

  ∞bind-cong-l : ∀ {i A B} {a∞ b∞ : ∞Delay A ∞} (eq : _∞~_ {i} a∞ b∞) →
    (k : A → Delay B ∞) →
    _∞~_ {i} (a∞ ∞>>= k)  (b∞ ∞>>= k)
  ~force (∞bind-cong-l eq k) = bind-cong-l (~force eq) k

_>>=l_ = bind-cong-l

mutual
  bind-cong-r : ∀ {i A B} (a? : Delay A ∞) {k l : A → Delay B ∞} →
    (h : ∀ a → _~_ {i} (k a) (l a)) → _~_ {i} (a? >>= k) (a? >>= l)
  bind-cong-r (now a)    h = h a
  bind-cong-r (later a∞) h = ~later (∞bind-cong-r a∞ h)

  ∞bind-cong-r : ∀ {i A B} (a∞ : ∞Delay A ∞) {k l : A → Delay B ∞} →
    (h : ∀ a → _~_ {i} (k a) (l a)) → _∞~_ {i} (a∞ ∞>>= k)  (a∞ ∞>>= l)
  ~force (∞bind-cong-r a∞ h) = bind-cong-r (force a∞) h

_>>=r_ = bind-cong-r

mutual
  bind-cong : ∀ {i A B}  {a? b? : Delay A ∞} (eq : _~_ {i} a? b?)
              {k l : A → Delay B ∞} (h : ∀ a → _~_ {i} (k a) (l a)) →
              _~_ {i} (a? >>= k) (b? >>= l)
  bind-cong (~now a)    h = h a
  bind-cong (~later eq) h = ~later (∞bind-cong eq h)

  ∞bind-cong : ∀ {i A B} {a∞ b∞ : ∞Delay A ∞} (eq : _∞~_ {i} a∞ b∞)
    {k l : A → Delay B ∞} (h : ∀ a → _~_ {i} (k a) (l a)) →
    _∞~_ {i} (a∞ ∞>>= k)  (b∞ ∞>>= l)
  ~force (∞bind-cong eq h) = bind-cong (~force eq) h

_~>>=_ = bind-cong

-- Monad laws.

mutual
  bind-assoc : ∀{i A B C}(m : Delay A ∞)
               {k : A → Delay B ∞}{l : B → Delay C ∞} →
               _~_ {i} ((m >>= k) >>= l)  (m >>= λ a → k a >>= l)
  bind-assoc (now a)    = ~refl _
  bind-assoc (later a∞) = ~later (∞bind-assoc a∞)

  ∞bind-assoc : ∀{i A B C}(a∞ : ∞Delay A ∞)
                {k : A → Delay B ∞}{l : B → Delay C ∞} →
                _∞~_ {i} ((a∞ ∞>>= λ a → k a) ∞>>= l) (a∞ ∞>>= λ a → k a >>= l)
  ~force (∞bind-assoc a∞) = bind-assoc (force a∞)

-- Termination/Convergence.  Makes sense only for Delay A ∞.

data _⇓_ {A : Set} : (a? : Delay A ∞) (a : A) → Set where
  now⇓   : ∀ {a} → now a ⇓ a
  later⇓ : ∀ {a} {a∞ : ∞Delay A ∞} → force a∞ ⇓ a → later a∞ ⇓ a

_⇓ : {A : Set} (x : Delay A ∞) → Set
x ⇓ = ∃ λ a → x ⇓ a

-- Monotonicity.

map⇓ : ∀ {A B} {a : A} {a? : Delay A ∞}
  (f : A → B) (a⇓ : a? ⇓ a) → (f <$> a?) ⇓ f a
map⇓ f now⇓        = now⇓
map⇓ f (later⇓ a⇓) = later⇓ (map⇓ f a⇓)

-- some lemmas about convergence
subst~⇓ : ∀{A}{t t' : Delay A ∞}{n : A} → t ⇓ n → t ~ t' → t' ⇓ n
subst~⇓ now⇓ (~now a) = now⇓
subst~⇓ (later⇓ p) (~later eq) = later⇓ (subst~⇓ p (~force eq))

-- this should also hold for weak bisimularity right?
{-
subst≈⇓ : ∀{A}{t t' : Delay A ∞}{n : A} → t ⇓ n → t ≈ t' → t' ⇓ n
subst≈⇓ = ?
-}

⇓>>= : ∀{A B}(f : A → Delay B ∞)
       {?a : Delay A ∞}{a : A} → ?a ⇓ a →
       {b : B} → (?a >>= f) ⇓ b → f a ⇓ b
⇓>>= f now⇓ q = q
⇓>>= f (later⇓ p) (later⇓ q) = ⇓>>= f p q

>>=⇓ : ∀{A B}(f : A → Delay B ∞)
       {?a : Delay A ∞}{a : A} → ?a ⇓ a →
       {b : B} → f a ⇓ b → (?a >>= f) ⇓ b
>>=⇓ f now⇓ q = q
>>=⇓ f (later⇓ p) q = later⇓ (>>=⇓ f p q)

-- handy when you can't pattern match like in a let definition
unlater : ∀{A}{∞a : ∞Delay A ∞}{a : A} → later ∞a ⇓ a → force ∞a ⇓ a
unlater (later⇓ p) = p

{-
mutual
  _⇓_ : {A : Set} {i : Size} (x : Delay A i) (a : A) → Set
  x ⇓ a = Terminates a x

  data Terminates {A : Set} {i : Size} (a : A) : Delay A i → Set where
    now   : now a ⇓ a
    later : ∀ {x : ∞Delay A i} → (force x {j = ?}) ⇓ a → later x ⇓ a

mutual

  cast : ∀ {A i} → Delay A i → (j : Size< ↑ i) → Delay A j
  cast (now x) j = now x
  cast (later x) j = {!later (∞cast x j)!}

  ∞cast : ∀ {A i} → ∞Delay A i → (j : Size< ↑ i) → ∞Delay A j
  ♭ (∞cast x j) {k} = cast {i = j} (♭ x) k
-}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module Cats.Adjunction where

open import Level using (suc ; _⊔_)

open import Cats.Category
open import Cats.Category.Cat.Facts.Product using (First ; Second)
open import Cats.Category.Fun using (Fun)
open import Cats.Category.Op using (_ᵒᵖ)
open import Cats.Category.Product.Binary using (_×_)
open import Cats.Category.Setoids using (Setoids)
open import Cats.Functor using (Functor ; _∘_)
open import Cats.Functor.Op using (Op)
open import Cats.Functor.Representable using (Hom[_])

open Functor

module _ {lo la l≈} {C D : Category lo la l≈} where

  private
    module Fun = Category (Fun ((C ᵒᵖ) × D) (Setoids la l≈))

  record Adjunction (F : Functor C D) (U : Functor D C)
    : Set (lo ⊔ suc la ⊔ suc l≈)
    where
    field
      iso : (Hom[ D ] ∘ First (Op F)) Fun.≅ (Hom[ C ] ∘ Second U)

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
-- Example usage of solver

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

open import Categories.Category
open import Categories.Functor renaming (id to idF)

module Experiment.Categories.Solver.Functor.Example
  {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′}
  (F : Functor 𝒞 𝒟)
  where

open Category 𝒟
open HomReasoning
open Functor F

open import Experiment.Categories.Solver.Functor F

module _ {A B C D E}
         (f : 𝒞 [ D , E ]) (g : 𝒞 [ C , D ]) (h : 𝒞 [ B , C ]) (i : 𝒞 [ A , B ]) where
  _ : F₁ (f 𝒞.∘ g 𝒞.∘ h) ∘ F₁ 𝒞.id ∘ F₁ i ∘ id ≈ F₁ (f 𝒞.∘ g) ∘ F₁ (h 𝒞.∘ i)
  _ = solve (:F₁ (∥-∥′ :∘ ∥-∥′ :∘ ∥-∥′) :∘ :F₁ :id :∘ :F₁ (∥-∥′) :∘ :id)
            (:F₁ (∥-∥′ :∘ ∥-∥′) :∘ :F₁ (∥-∥′ :∘ ∥-∥′))
            refl


text:
postulate
  P : (A : Set) → A → Set
  X : Set
  x : X

P' : (A : Set) → _

R : Set
R = P' _ x

P' = P

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; cong; cong₂; isEquivalence; setoid)
open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)

open import Data.Unit using (⊤; tt)
open import Agda.Builtin.FromNat using (Number)

open import Data.Product using (_,_)

module AKS.Rational.Properties where

open import AKS.Rational.Base using (ℚ; _+_; _*_; -_; _/_; _≟_)

open import Algebra.Structures {A = ℚ} _≡_ using
  ( IsCommutativeRing; IsRing; IsAbelianGroup
  ; IsGroup; IsMonoid; IsSemigroup; IsMagma
  )
open import Algebra.Definitions {A = ℚ} _≡_ using
  ( _DistributesOver_; _DistributesOverʳ_; _DistributesOverˡ_
  ; RightIdentity; LeftIdentity; Identity; Associative; Commutative
  ; RightInverse; LeftInverse; Inverse
  )
open import AKS.Algebra.Structures ℚ _≡_ using (IsNonZeroCommutativeRing; IsIntegralDomain; IsGCDDomain; IsDecField)
open import Algebra.Bundles using (Ring; CommutativeRing)
open import AKS.Algebra.Bundles using (NonZeroCommutativeRing; DecField)

open import AKS.Unsafe using (BOTTOM; ≢-irrelevant)

+-isMagma : IsMagma _+_
+-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong = cong₂ _+_
  }

+-assoc : Associative _+_
+-assoc = BOTTOM

+-isSemigroup : IsSemigroup _+_
+-isSemigroup = record
  { isMagma = +-isMagma
  ; assoc = +-assoc
  }

+-comm : Commutative _+_
+-comm = BOTTOM

+-identityˡ : LeftIdentity 0 _+_
+-identityˡ = BOTTOM

open import Algebra.FunctionProperties.Consequences.Propositional using (comm+idˡ⇒idʳ; comm+invˡ⇒invʳ; comm+distrˡ⇒distrʳ)

+-identityʳ : RightIdentity 0 _+_
+-identityʳ = BOTTOM -- comm+idˡ⇒idʳ +-comm +-identityˡ

+-identity : Identity 0 _+_
+-identity = +-identityˡ , +-identityʳ

+-isMonoid : IsMonoid _+_ 0
+-isMonoid = record
  { isSemigroup = +-isSemigroup
  ; identity = +-identity
  }

-‿inverseˡ : LeftInverse 0 -_ _+_
-‿inverseˡ = BOTTOM

-‿inverseʳ : RightInverse 0 -_ _+_
-‿inverseʳ = BOTTOM -- comm+invˡ⇒invʳ +-comm -‿inverseˡ

-‿inverse : Inverse 0 -_ _+_
-‿inverse = -‿inverseˡ , -‿inverseʳ

+-isGroup : IsGroup _+_ 0 -_
+-isGroup = record
  { isMonoid = +-isMonoid
  ; inverse = -‿inverse
  ; ⁻¹-cong = cong -_
  }

+-isAbelianGroup : IsAbelianGroup _+_ 0 -_
+-isAbelianGroup = record
  { isGroup = +-isGroup
  ; comm = +-comm
  }

*-isMagma : IsMagma _*_
*-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong = cong₂ _*_
  }

*-assoc : Associative _*_
*-assoc = BOTTOM

*-isSemigroup : IsSemigroup _*_
*-isSemigroup = record
  { isMagma = *-isMagma
  ; assoc = *-assoc
  }

*-comm : Commutative _*_
*-comm x y = BOTTOM

*-identityˡ : LeftIdentity 1 _*_
*-identityˡ x = BOTTOM

*-identityʳ : RightIdentity 1 _*_
*-identityʳ = BOTTOM -- comm+idˡ⇒idʳ *-comm *-identityˡ

*-identity : Identity 1 _*_
*-identity = *-identityˡ , *-identityʳ

*-isMonoid : IsMonoid _*_ 1
*-isMonoid = record
  { isSemigroup = *-isSemigroup
  ; identity = *-identity
  }

*-distribˡ-+ : _*_ DistributesOverˡ _+_
*-distribˡ-+ = BOTTOM

*-distribʳ-+ : _*_ DistributesOverʳ _+_
*-distribʳ-+ = BOTTOM -- comm+distrˡ⇒distrʳ *-comm *-distribˡ-+

*-distrib-+ : _*_ DistributesOver _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+

+-*-isRing : IsRing _+_ _*_ -_ 0 1
+-*-isRing = record
  { +-isAbelianGroup = +-isAbelianGroup
  ; *-isMonoid = *-isMonoid
  ; distrib = *-distrib-+
  }

+-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0 1
+-*-isCommutativeRing = record
  { isRing = +-*-isRing
  ; *-comm = *-comm
  }

+-*-isNonZeroCommutativeRing : IsNonZeroCommutativeRing _+_ _*_ -_ 0 1
+-*-isNonZeroCommutativeRing = record
  { isCommutativeRing = +-*-isCommutativeRing
  ; 0#≉1# = λ ()
  }

+-*-nonZeroCommutativeRing : NonZeroCommutativeRing 0ℓ 0ℓ
+-*-nonZeroCommutativeRing = record { isNonZeroCommutativeRing = +-*-isNonZeroCommutativeRing }

/-inverse : ∀ x y {y≢0} → x ≡ y * (x / y) {y≢0}
/-inverse x y {y≢0} = BOTTOM

open import AKS.Algebra.Consequences +-*-nonZeroCommutativeRing using (module Inverse⇒Field)

open Inverse⇒Field _≟_ ≡-irrelevant ≢-irrelevant _/_ /-inverse
  using (gcd)
  renaming (isField to +-*-/-isField; [field] to +-*-/-field) public

+-*-/-isDecField : IsDecField _≟_ _+_ _*_ -_ 0 1 _/_ gcd
+-*-/-isDecField = record { isField = +-*-/-isField }

+-*-/-decField : DecField 0ℓ 0ℓ
+-*-/-decField = record { isDecField = +-*-/-isDecField }

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
------------------------------------------------------------------------
-- Progress of CBV reductions in pure type systems (PTS)
------------------------------------------------------------------------

-- This module contains a variant of the "progress" theorem for PTS.
-- Progress says roughly that well-typed terms do not get stuck.
-- I.e. a well-typed term is either a value or it can take a CBV
-- reduction step.  Together with the subject reduction (aka
-- "preservation") theorem from Pts.Typing, progress ensures type
-- soundness.  For detials, see e.g.
--
--  * B. C. Pierce, TAPL (2002), pp. 95.
--
--  * A. Wright and M. Felleisen, "A Syntactic Approach to Type
--    Soundness" (1994).

module Pts.Typing.Progress where

open import Data.Product using (_,_; ∃; _×_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)

open import Pts.Typing
open import Pts.Reduction.Cbv
open import Pts.Reduction.Full

-- Definitions and lemmas are parametrized by a given PTS instance.
module _ {pts} where
  open PTS pts
  open Syntax
  open Ctx
  open Substitution using (_[_])
  open Typing pts

  -- A helper lemma: sorts are not product types.
  Π≢sort : ∀ {n s} {a : Term n} {b} → ¬ (Π a b ≡β sort s)
  Π≢sort Πab≡s =
    let _ , Πab→*c , s→*c       = ≡β⇒→β* Πab≡s
        _ , _ , _ , _ , Πa′b′≡c = Π-→β* Πab→*c
    in contradiction Πa′b′≡c (sort⇒¬Π (sort-→β* s→*c))
    where
      sort⇒¬Π : ∀ {n s a b} {c : Term n} → sort s ≡ c → ¬ (Π a b ≡ c)
      sort⇒¬Π refl ()

  -- A canonical forms lemma for dependent product values: closed
  -- values of product type are abstractions.
  Π-can : ∀ {f a b} → Val f → [] ⊢ f ∈ Π a b → ∃ λ a′ → ∃ λ t → f ≡ ƛ a′ t
  Π-can (sort s) s∈Πab =
    let _ , _ , Πab≡s′ = sort-gen s∈Πab
    in contradiction Πab≡s′ Π≢sort
  Π-can (Π c d)  Πcd∈Πab =
    let _ , _ , _ , _ , _ , _ , Πab≡s = Π-gen Πcd∈Πab
    in contradiction Πab≡s Π≢sort
  Π-can (ƛ a′ t) (ƛ a∈s t∈b)             = a′ , t , refl
  Π-can (ƛ a′ t) (conv λa′t∈c c∈s c≡Πab) = a′ , t , refl

  -- Progress: well-typed terms do not get stuck (under CBV reduction).
  prog : ∀ {a b} → [] ⊢ a ∈ b → Val a ⊎ (∃ λ a′ → a →v a′)
  prog (var () Γ-wf)
  prog (axiom a Γ-wf)  = inj₁ (sort _)
  prog (Π r a∈s₁ b∈s₂) = inj₁ (Π _ _)
  prog (ƛ t∈b Πab∈s)   = inj₁ (ƛ _ _)
  prog (f∈Πab · t∈a)   with prog f∈Πab
  prog (f∈Πab · t∈a)   | inj₁ u with prog t∈a
  prog (f∈Πab · t∈a)   | inj₁ u | inj₁ v with Π-can u f∈Πab
  ...| a′ , t′ , refl = inj₂ (_ , cont a′ t′ v)
  prog (f∈Πab · t∈a)   | inj₁ u | inj₂ (t′ , t→t′) = inj₂ (_ , u ·₂ t→t′)
  prog (f∈Πab · t∈a)   | inj₂ (f′ , f→f′) = inj₂ (_ , f→f′ ·₁ _)
  prog (conv a∈b₁ b₂∈s b₁≡b₂) = prog a∈b₁

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


text:
module Structure where
  -- Structures in meta-functions.
  module Function' where -- TODO: Temporary naming fix with tick
    module Properties ⦃ signature : Signature ⦄ where
      Type : Domain → Domain → Function → Formula
      Type(X)(Y)(f) = ∀ₛ(X)(x ↦ f(x) ∈ Y)

      Closed : Domain → Function → Formula
      Closed(S)(f) = Type(S)(S)(f)

      Injective'' : Domain → Function → Formula
      Injective''(A)(f) = ∀ₛ(A)(x ↦ ∀ₛ(A)(y ↦ (f(x) ≡ f(y)) ⟶ (x ≡ y)))

      Surjective'' : Domain → Domain → Function → Formula
      Surjective''(A)(B)(f) = ∀ₛ(B)(y ↦ ∃ₛ(A)(x ↦ f(x) ≡ y))

      Bijective'' : Domain → Domain → Function → Formula
      Bijective''(A)(B)(f) =
        Injective''(A)(f)
        ∧ Surjective''(A)(B)(f)

      Preserving₁'' : Domain → Function → Function → Function → Formula
      Preserving₁''(A)(f)(g₁)(g₂) = ∀ₛ(A)(x ↦ f(g₁(x)) ≡ g₂(f(x)))

      Preserving₂'' : Domain → Domain → Function → BinaryOperator → BinaryOperator → Formula
      Preserving₂''(A)(B)(f)(_▫₁_)(_▫₂_) = ∀ₛ(A)(x ↦ ∀ₛ(B)(y ↦ f(x ▫₁ y) ≡ (f(x) ▫₂ f(y))))

  module Relator where
    module Properties where
      Reflexivity : Domain → BinaryRelator → Formula
      Reflexivity(S)(_▫_) = ∀ₛ(S)(x ↦ x ▫ x)

      Irreflexivity : Domain → BinaryRelator → Formula
      Irreflexivity(S)(_▫_) = ∀ₛ(S)(x ↦ ¬(x ▫ x))

      Symmetry : Domain → BinaryRelator → Formula
      Symmetry(S)(_▫_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ (x ▫ y) ⟶ (y ▫ x)))

      Asymmetry : Domain → BinaryRelator → Formula
      Asymmetry(S)(_▫_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ (x ▫ y) ⟶ ¬(y ▫ x)))

      Antisymmetry : Domain → BinaryRelator → Formula
      Antisymmetry(S)(_▫_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ (x ▫ y)∧(y ▫ x) ⟶ (x ≡ y)))

      Transitivity : Domain → BinaryRelator → Formula
      Transitivity(S)(_▫_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ ∀ₛ(S)(z ↦ (x ▫ y)∧(y ▫ z) ⟶ (x ▫ z))))

      Equivalence : Domain → BinaryRelator → Formula
      Equivalence(S)(_▫_) =
        Reflexivity(S)(_▫_)
        ∧ Symmetry(S)(_▫_)
        ∧ Transitivity(S)(_▫_)

      SymmetricallyTotal : Domain → BinaryRelator → Formula
      SymmetricallyTotal(S)(_▫_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ (x ▫ y) ∨ (y ▫ x)))

  module Ordering where
    open Relator.Properties

    Minima : Domain → BinaryRelator → Domain → Formula
    Minima(S)(_≤_)(min) = ∀ₛ(S)(x ↦ min ≤ x)

    Maxima : Domain → BinaryRelator → Domain → Formula
    Maxima(S)(_≤_)(max) = ∀ₛ(S)(x ↦ x ≤ max)

    module _  ⦃ signature : Signature ⦄ where
      open Signature ⦃ ... ⦄

      lowerBounds : Domain → BinaryRelator → Domain → Domain
      lowerBounds(S)(_≤_)(Sₛ) = filter(S)(Minima(S)(_≤_))

      upperBounds : Domain → BinaryRelator → Domain → Domain
      upperBounds(S)(_≤_)(Sₛ) = filter(S)(Maxima(S)(_≤_))

      interval : Domain → BinaryRelator → Domain → Domain → Domain
      interval(S)(_≤_) (a)(b) = filter(S)(s ↦ (a ≤ s) ∧ (s ≤ b))

      Bounded : Domain → BinaryRelator → Domain → Domain → Formula
      Bounded(S)(_≤_) (a)(b) = ∀ₛ(S)(s ↦ (a ≤ s) ∧ (s ≤ b))

      Infima : Domain → BinaryRelator → Domain → Domain → Formula
      Infima(S)(_≤_)(Sₛ)(inf) = Maxima(lowerBounds(S)(_≤_)(Sₛ))(_≤_)(inf)

      Suprema : Domain → BinaryRelator → Domain → Domain → Formula
      Suprema(S)(_≤_)(Sₛ)(sup) = Minima(upperBounds(S)(_≤_)(Sₛ))(_≤_)(sup)

    module Weak where
      PartialOrder : Domain → BinaryRelator → Formula
      PartialOrder(S)(_≤_) =
        Reflexivity(S)(_≤_)
        ∧ Antisymmetry(S)(_≤_)
        ∧ Transitivity(S)(_≤_)

      TotalOrder : Domain → BinaryRelator → Formula
      TotalOrder(S)(_≤_) =
        PartialOrder(S)(_≤_)
        ∧ SymmetricallyTotal(S)(_≤_)

    module Strict where
      Order : Domain → BinaryRelator → Formula
      Order(S)(_<_) =
        Irreflexivity(S)(_<_)
        ∧ Asymmetry(S)(_<_)
        ∧ Transitivity(S)(_<_)

      Dense : Domain → BinaryRelator → Formula
      Dense(S)(_<_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ (x < y) ⟶ ∃ₛ(S)(z ↦ (x < z)∧(z < y))))

  module Operator where
    module Properties where
      AssociativityPattern : Domain → Domain → Domain → BinaryOperator → BinaryOperator → BinaryOperator → BinaryOperator → Formula
      AssociativityPattern(x)(y)(z)(_▫₁_)(_▫₂_)(_▫₃_)(_▫₄_) = (((x ▫₁ y) ▫₂ z) ≡ (x ▫₃ (y ▫₄ z)))

      DistributivityₗPattern : Domain → Domain → Domain → BinaryOperator → BinaryOperator → BinaryOperator → BinaryOperator → BinaryOperator → Formula
      DistributivityₗPattern(x)(y)(z)(_▫₁_)(_▫₂_)(_▫₃_)(_▫₄_)(_▫₅_) = (x ▫₁ (y ▫₂ z)) ≡ ((x ▫₃ y) ▫₄ (x ▫₅ z))

      DistributivityᵣPattern : Domain → Domain → Domain → BinaryOperator → BinaryOperator → BinaryOperator → BinaryOperator → BinaryOperator → Formula
      DistributivityᵣPattern(x)(y)(z)(_▫₁_)(_▫₂_)(_▫₃_)(_▫₄_)(_▫₅_) = ((x ▫₂ y) ▫₁ z) ≡ ((x ▫₃ z) ▫₄  (y ▫₅ z))

      Type : BinaryOperator → Domain → Domain → Domain → Formula
      Type(_▫_)(X)(Y)(Z) = ∀ₛ(X)(x ↦ ∀ₛ(Y)(y ↦ (x ▫ y) ∈ Z))

      Closed : Domain → BinaryOperator → Formula
      Closed(S)(_▫_) = Type(_▫_)(S)(S)(S)

      Commutativity : Domain → BinaryOperator → Formula
      Commutativity(S)(_▫_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ (x ▫ y) ≡ (y ▫ x)))

      Associativity : Domain → BinaryOperator → Formula
      Associativity(S)(_▫_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ ∀ₛ(S)(z ↦ AssociativityPattern(x)(y)(z)(_▫_)(_▫_)(_▫_)(_▫_))))

      Identityₗ : Domain → BinaryOperator → Domain → Formula
      Identityₗ(S)(_▫_)(id) = ∀ₛ(S)(x ↦ (id ▫ x) ≡ x)

      Identityᵣ : Domain → BinaryOperator → Domain → Formula
      Identityᵣ(S)(_▫_)(id) = ∀ₛ(S)(x ↦ (x ▫ id) ≡ x)

      Identity : Domain → BinaryOperator → Domain → Formula
      Identity(S)(_▫_)(id) = Identityₗ(S)(_▫_)(id) ∧ Identityᵣ(S)(_▫_)(id)

      Invertibleₗ : Domain → BinaryOperator → Domain → Formula
      Invertibleₗ(S)(_▫_)(id) = ∀ₛ(S)(x ↦ ∃ₛ(S)(x⁻¹ ↦ (x⁻¹ ▫ x) ≡ id))

      Invertibleᵣ : Domain → BinaryOperator → Domain → Formula
      Invertibleᵣ(S)(_▫_)(id) = ∀ₛ(S)(x ↦ ∃ₛ(S)(x⁻¹ ↦ (x ▫ x⁻¹) ≡ id))

      Invertible : Domain → BinaryOperator → Domain → Formula
      Invertible(S)(_▫_)(id) = ∀ₛ(S)(x ↦ ∃ₛ(S)(x⁻¹ ↦ ((x⁻¹ ▫ x) ≡ id) ∧ ((x ▫ x⁻¹) ≡ id)))

      Distributivityₗ : Domain → BinaryOperator → BinaryOperator → Formula
      Distributivityₗ(S)(_▫₁_)(_▫₂_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ ∀ₛ(S)(z ↦ DistributivityₗPattern(x)(y)(z)(_▫₁_)(_▫₂_)(_▫₁_)(_▫₂_)(_▫₁_))))

      Distributivityᵣ : Domain → BinaryOperator → BinaryOperator → Formula
      Distributivityᵣ(S)(_▫₁_)(_▫₂_) = ∀ₛ(S)(x ↦ ∀ₛ(S)(y ↦ ∀ₛ(S)(z ↦ DistributivityᵣPattern(x)(y)(z)(_▫₁_)(_▫₂_)(_▫₁_)(_▫₂_)(_▫₁_))))

      Distributivity : Domain → BinaryOperator → BinaryOperator → Formula
      Distributivity(S)(_▫₁_)(_▫₂_) = Distributivityₗ(S)(_▫₁_)(_▫₂_) ∧ Distributivityᵣ(S)(_▫₁_)(_▫₂_)

      Compatibility : Domain → Domain → BinaryOperator → BinaryOperator → Formula
      Compatibility(A)(B)(_▫₁_)(_▫₂_) = ∀ₛ(A)(a₁ ↦ ∀ₛ(A)(a₂ ↦ ∀ₛ(B)(b ↦ AssociativityPattern(a₁)(a₂)(b)(_▫₁_)(_▫₁_)(_▫₂_)(_▫₁_))))

      Semigroup : Domain → BinaryOperator → Formula
      Semigroup(S)(_▫_) =
        Closed(S)(_▫_)
        ∧ Associativity(S)(_▫_)

      Monoid : Domain → BinaryOperator → Formula
      Monoid(S)(_▫_) =
        Semigroup(S)(_▫_)
        ∧ ∃ₛ(S)(Identity(S)(_▫_))

      Group : Domain → BinaryOperator → Formula
      Group(S)(_▫_) =
        Monoid(S)(_▫_)
        ∧ ∀ₛ(S)(id ↦ Identity(S)(_▫_)(id) ⟶ Invertible(S)(_▫_)(id))

      CommutativeGroup : Domain → BinaryOperator → Formula
      CommutativeGroup(S)(_▫_) =
        Group(S)(_▫_)
        ∧ Commutativity(S)(_▫_)

      Rng : Domain → BinaryOperator → BinaryOperator → Formula
      Rng(S)(_▫₁_)(_▫₂_) =
        CommutativeGroup(S)(_▫₁_)
        ∧ Semigroup(S)(_▫₂_)
        ∧ Distributivity(S)(_▫₂_)(_▫₁_)

      Ring : Domain → BinaryOperator → BinaryOperator → Formula
      Ring(S)(_▫₁_)(_▫₂_) =
        CommutativeGroup(S)(_▫₁_)
        ∧ Monoid(S)(_▫₂_)
        ∧ Distributivity(S)(_▫₂_)(_▫₁_)

      module _  ⦃ signature : Signature ⦄ where
        open Signature ⦃ ... ⦄

        Field : Domain → BinaryOperator → BinaryOperator → Formula
        Field(S)(_▫₁_)(_▫₂_) =
          CommutativeGroup(S)(_▫₁_)
          ∧ ∀ₛ(S)(id₁ ↦ Identity(S)(_▫₁_)(id₁) ⟶ CommutativeGroup(S ∖ singleton(id₁))(_▫₂_))
          ∧ Distributivity(S)(_▫₂_)(_▫₁_)

        VectorSpace : Domain → Domain → BinaryOperator → BinaryOperator → BinaryOperator → BinaryOperator → Formula
        VectorSpace(V)(S)(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) =
          CommutativeGroup(V)(_+ᵥ_)
          ∧ Field(S)(_+ₛ_)(_⋅ₛ_)
          ∧ ∀ₛ(S)(id ↦ Identity(S)(_⋅ₛ_)(id) ⟶ Identityₗ(V)(_⋅ₛᵥ_)(id))
          ∧ Compatibility(S)(V)(_⋅ₛᵥ_)(_⋅ₛ_)
          ∧ ∀ₛ(S)(s ↦ ∀ₛ(V)(v₁ ↦ ∀ₛ(V)(v₂ ↦ DistributivityₗPattern(s)(v₁)(v₂)(_⋅ₛᵥ_)(_+ᵥ_)(_⋅ₛᵥ_)(_+ᵥ_)(_⋅ₛᵥ_))))
          ∧ ∀ₛ(S)(s₁ ↦ ∀ₛ(S)(s₂ ↦ ∀ₛ(V)(v ↦ DistributivityᵣPattern(s₁)(s₂)(v)(_⋅ₛᵥ_)(_+ᵥ_)(_⋅ₛᵥ_)(_+ᵥ_)(_⋅ₛᵥ_))))

  module Numeral where
    module Natural ⦃ signature : Signature ⦄ where
      open Signature ⦃ ... ⦄

      FormulaInduction : Domain → Domain → Function → (Domain → Formula) → Formula
      FormulaInduction(ℕ)(𝟎)(𝐒) (φ) = (φ(𝟎) ∧ ∀ₛ(ℕ)(n ↦ φ(n) ⟶ φ(𝐒(n)))) ⟶ ∀ₛ(ℕ)(φ)

      SetInduction : Domain → Domain → Function → Formula
      SetInduction(ℕ)(𝟎)(𝐒) = ∀ₗ(X ↦ ((𝟎 ∈ X) ∧ ∀ₛ(ℕ)(n ↦ (n ∈ X) ⟶ (𝐒(n) ∈ X))) ⟶ (ℕ ⊆ X))
      -- TODO: Can be expressed as ∀ₗ(X ↦ Inductive(X) ⟶ (ℕ ⊆ X))

      -- A set ℕ which can be constructed ℕ-inductively.
      Peano : Domain → Domain → Function → Formula
      Peano(ℕ)(𝟎)(𝐒) =
        (𝟎 ∈ ℕ)
        ∧ Function'.Properties.Closed(ℕ)(𝐒)
        ∧ Function'.Properties.Injective''(ℕ)(𝐒)
        ∧ ∀ₛ(ℕ)(n ↦ 𝐒(n) ≢ 𝟎)
        ∧ SetInduction(ℕ)(𝟎)(𝐒)

max_issues_repo_name: Lolirofle/stuff-in-agda


text:
module BasicIPC.Metatheory.Hilbert-TarskiConcreteGluedImplicit where

open import BasicIPC.Syntax.Hilbert public
open import BasicIPC.Semantics.TarskiConcreteGluedImplicit public

open ImplicitSyntax (_⊢_) public

-- Completeness with respect to a particular model.

module _ {{_ : Model}} where
  reify : ∀ {A w} → w ⊩ A → unwrap w ⊢ A
  reify {α P}   s = syn s
  reify {A ▻ B} s = syn s
  reify {A ∧ B} s = pair (reify (π₁ s)) (reify (π₂ s))
  reify {⊤}    s = unit

  reify⋆ : ∀ {Ξ w} → w ⊩⋆ Ξ → unwrap w ⊢⋆ Ξ
  reify⋆ {∅}     ∙        = ∙
  reify⋆ {Ξ , A} (ts , t) = reify⋆ ts , reify t

-- Additional useful equipment.

module _ {{_ : Model}} where
  ⟪K⟫ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A
  ⟪K⟫ {A} a = app ck (reify a) ⅋ K a

  ⟪S⟫′ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ = app cs (syn s₁) ⅋ λ s₂ →
                          app (app cs (syn s₁)) (syn s₂) ⅋ ⟪S⟫ s₁ s₂

  _⟪,⟫′_ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} a = app cpair (reify a) ⅋ _,_ a

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)   γ = lookup i γ
eval (app t u) γ = eval t γ ⟪$⟫ eval u γ
eval ci        γ = ci ⅋ I
eval ck        γ = ck ⅋ ⟪K⟫
eval cs        γ = cs ⅋ ⟪S⟫′
eval cpair     γ = cpair ⅋ _⟪,⟫′_
eval cfst      γ = cfst ⅋ π₁
eval csnd      γ = csnd ⅋ π₂
eval unit      γ = ∙

-- TODO: Correctness of evaluation with respect to conversion.

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { _⊩ᵅ_ = λ w P → unwrap w ⊢ α P
      }

-- Soundness with respect to the canonical model.

reflectᶜ : ∀ {A w} → unwrap w ⊢ A → w ⊩ A
reflectᶜ {α P}   t = t ⅋ t
reflectᶜ {A ▻ B} t = t ⅋ λ a → reflectᶜ (app t (reify a))
reflectᶜ {A ∧ B} t = reflectᶜ (fst t) , reflectᶜ (snd t)
reflectᶜ {⊤}    t = ∙

reflectᶜ⋆ : ∀ {Ξ w} → unwrap w ⊢⋆ Ξ → w ⊩⋆ Ξ
reflectᶜ⋆ {∅}     ∙        = ∙
reflectᶜ⋆ {Ξ , A} (ts , t) = reflectᶜ⋆ ts , reflectᶜ t

-- Reflexivity and transitivity.

refl⊩⋆ : ∀ {w} → w ⊩⋆ unwrap w
refl⊩⋆ = reflectᶜ⋆ refl⊢⋆

trans⊩⋆ : ∀ {w w′ w″} → w ⊩⋆ unwrap w′ → w′ ⊩⋆ unwrap w″ → w ⊩⋆ unwrap w″
trans⊩⋆ ts us = reflectᶜ⋆ (trans⊢⋆ (reify⋆ ts) (reify⋆ us))

-- Completeness with respect to all models, or quotation.

quot : ∀ {A Γ} → Γ ⊨ A → Γ ⊢ A
quot s = reify (s refl⊩⋆)

-- Normalisation by evaluation.

norm : ∀ {A Γ} → Γ ⊢ A → Γ ⊢ A
norm = quot ∘ eval

-- TODO: Correctness of normalisation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
open import Level hiding ( suc ; zero )
open import Algebra
module sym5n where

open import Symmetric
open import Data.Unit
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Relation.Nullary
open import Data.Empty
open import Data.Product

open import Gutil
open import Putil
open import Solvable using (solvable)
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open import Data.Fin
open import Data.Fin.Permutation hiding (_∘ₚ_)

infixr  200 _∘ₚ_
_∘ₚ_ = Data.Fin.Permutation._∘ₚ_

-- open import IO
open import Data.String hiding (toList)
open import Data.Unit
open import Agda.Builtin.String

sym5solvable : (n : ℕ) → String -- ¬ solvable (Symmetric 5)
sym5solvable n = FListtoStr (CommFListN 5 n) where

   open import Data.List using ( List ; [] ; _∷_ )
   open Solvable (Symmetric 5)

   open import FLutil
   open import Data.List.Fresh hiding ([_])
   open import Relation.Nary using (⌊_⌋)

   p0id :  FL→perm (zero :: zero :: zero :: (zero :: (zero :: f0))) =p= pid
   p0id = pleq _ _ refl

   open import Data.List.Fresh.Relation.Unary.Any
   open import FLComm

   stage4FList = CommFListN 5 0
   stage6FList = CommFListN 5 3

   -- stage5FList = {!!}
   -- s2=s3 :  CommFListN 5 2 ≡ CommFListN 5 3
   -- s2=s3 = refl

   FLtoStr : {n : ℕ} → (x : FL n) → String
   FLtoStr f0 = "f0"
   FLtoStr (x :: y) = primStringAppend ( primStringAppend (primShowNat (toℕ x)) " :: " ) (FLtoStr y)

   FListtoStr : {n : ℕ} → (x : FList n) → String
   FListtoStr [] = ""
   FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x))

open import Codata.Musical.Notation
open import Data.Maybe hiding (_>>=_)
open import Data.List
open import Data.Char
open import IO.Primitive
open import Codata.Musical.Costring

postulate
    getArgs : IO (List (List Char))
{-# FOREIGN GHC import qualified System.Environment #-}
{-# COMPILE GHC getArgs = System.Environment.getArgs #-}

charToDigit : Char → Maybe ℕ
charToDigit '0' = just ( 0)
charToDigit '1' = just ( 1)
charToDigit '2' = just ( 2)
charToDigit '3' = just ( 3)
charToDigit '4' = just ( 4)
charToDigit '5' = just ( 5)
charToDigit '6' = just ( 6)
charToDigit '7' = just ( 7)
charToDigit '8' = just ( 8)
charToDigit '9' = just ( 9)
charToDigit _   = nothing

getNumArg1 : (List (List Char)) → ℕ
getNumArg1 [] = 0
getNumArg1 ([] ∷ y) = 0
getNumArg1 ((x ∷ _) ∷ y) with charToDigit x
... | just n = n
... | nothing  = 0

--
-- CommFListN 5 x is too slow use compiler
-- agda --compile sym5n.agda
--

main : IO ⊤
main = getArgs >>= (λ x →  putStrLn $ toCostring $ sym5solvable $ getNumArg1 x )

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
-- Automatic solvers for equations over Gaussian Integers.
{-# OPTIONS --without-K --safe #-}

module GauInt.Solver where

import Algebra.Solver.Ring.Simple as Solver
import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
open import GauInt.Properties

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _+𝔾_ and _*𝔾_

module +-*-Solver =
  Solver (ACR.fromCommutativeRing +-*-commutativeRing) _≟_

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
module Agda.Builtin.Size where

{-# BUILTIN SIZEUNIV SizeU #-}
{-# BUILTIN SIZE     Size   #-}
{-# BUILTIN SIZELT   Size<_ #-}
{-# BUILTIN SIZESUC  ↑_     #-}
{-# BUILTIN SIZEINF  ω      #-}
{-# BUILTIN SIZEMAX  _⊔ˢ_  #-}


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

open import HoTT
open import homotopy.SuspSmash
open import homotopy.SuspSmashComm

module homotopy.IterSuspSmash where

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  Σ^∧-out : (n : ℕ) → ⊙Susp^ n X ∧ Y → Susp^ n (X ∧ Y)
  Σ^∧-out O = idf _
  Σ^∧-out (S n) = Susp-fmap (Σ^∧-out n) ∘ Σ∧-out (⊙Susp^ n X) Y

  private
    Σ^∧-out-pt : (n : ℕ) → Σ^∧-out n (pt (⊙Susp^ n X ⊙∧ Y)) == pt (⊙Susp^ n (X ⊙∧ Y))
    Σ^∧-out-pt O = idp
    Σ^∧-out-pt (S n) = idp

  ⊙Σ^∧-out : (n : ℕ) → ⊙Susp^ n X ⊙∧ Y ⊙→ ⊙Susp^ n (X ⊙∧ Y)
  ⊙Σ^∧-out n = Σ^∧-out n , Σ^∧-out-pt n

  ∧Σ^-out : (n : ℕ) → X ∧ ⊙Susp^ n Y → Susp^ n (X ∧ Y)
  ∧Σ^-out O = idf _
  ∧Σ^-out (S n) = Susp-fmap (∧Σ^-out n) ∘ ∧Σ-out X (⊙Susp^ n Y)

  private
    ∧Σ^-out-pt : (n : ℕ) → ∧Σ^-out n (pt (X ⊙∧ ⊙Susp^ n Y)) == pt (⊙Susp^ n (X ⊙∧ Y))
    ∧Σ^-out-pt O = idp
    ∧Σ^-out-pt (S n) = idp

  ⊙∧Σ^-out : (n : ℕ) → X ⊙∧ ⊙Susp^ n Y ⊙→ ⊙Susp^ n (X ⊙∧ Y)
  ⊙∧Σ^-out n = ∧Σ^-out n , ∧Σ^-out-pt n

private
  ⊙maybe-Susp^-flip-+ : ∀ {i} {X : Ptd i} (m n : ℕ) (b : Bool)
    → (m == 0 → b == false)
    → ⊙coe (⊙Susp^-+ m n {X}) ◃⊙∘
      ⊙maybe-Susp^-flip {X = ⊙Susp^ n X} m b ◃⊙idf
      =⊙∘
      ⊙maybe-Susp^-flip (m + n) b ◃⊙∘
      ⊙coe (⊙Susp^-+ m n) ◃⊙idf
  ⊙maybe-Susp^-flip-+ O O b h = =⊙∘-in idp
  ⊙maybe-Susp^-flip-+ O (S n) true h = ⊥-elim (Bool-true≠false (h idp))
  ⊙maybe-Susp^-flip-+ O (S n) false h = =⊙∘-in idp
  ⊙maybe-Susp^-flip-+ {X = X} (S m) n true h =
    ⊙coe (ap ⊙Susp (Susp^-+ m n)) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ m (⊙Susp^ n X)) ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ! p ⟩
    ⊙Susp-fmap (fst (⊙coe (⊙Susp^-+ m n))) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ m (⊙Susp^ n X)) ◃⊙idf
      =⊙∘⟨ =⊙∘-in $ ! $
           ⊙Susp-flip-natural (⊙coe (⊙Susp^-+ m n)) ⟩
    ⊙Susp-flip (⊙Susp^ (m + n) X) ◃⊙∘
    ⊙Susp-fmap (fst (⊙coe (⊙Susp^-+ m n))) ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & p ⟩
    ⊙Susp-flip (⊙Susp^ (m + n) X) ◃⊙∘
    ⊙coe (ap ⊙Susp (Susp^-+ m n)) ◃⊙idf ∎⊙∘
    where
    p : ⊙Susp-fmap (fst (⊙coe (⊙Susp^-+ m n {X}))) ==
        ⊙coe (ap ⊙Susp (Susp^-+ m n))
    p =
      ap (⊙Susp-fmap ∘ coe) (de⊙-⊙Susp^-+ m n {X}) ∙
      ! (⊙transport-⊙Susp (Susp^-+ m n)) ∙
      ⊙transport-⊙coe ⊙Susp (Susp^-+ m n)
  ⊙maybe-Susp^-flip-+ (S m) n false h = =⊙∘-in $ ! $ ⊙λ= $ ⊙∘-unit-l _

  ⊙maybe-Susp^-flip-comm : ∀ {i} {X : Ptd i} (m n : ℕ) (b : Bool)
    → (m == 0 → b == false)
    → (n == 0 → b == false)
    → ⊙coe (⊙Susp^-comm m n {X = X}) ◃⊙∘
      ⊙maybe-Susp^-flip {X = ⊙Susp^ n X} m b ◃⊙idf
      =⊙∘
      ⊙maybe-Susp^-flip {X = ⊙Susp^ m X} n b ◃⊙∘
      ⊙coe (⊙Susp^-comm m n) ◃⊙idf
  ⊙maybe-Susp^-flip-comm O O b h₁ h₂ = =⊙∘-in (! (⊙λ= (⊙∘-unit-l (⊙coe (⊙Susp^-comm 0 0)))))
  ⊙maybe-Susp^-flip-comm O (S _) true  h₁ h₂ = ⊥-elim (Bool-true≠false (h₁ idp))
  ⊙maybe-Susp^-flip-comm O (S _) false h₁ h₂ = =⊙∘-in (! (⊙λ= (⊙∘-unit-l _)))
  ⊙maybe-Susp^-flip-comm (S m) O true  h₁ h₂ = ⊥-elim (Bool-true≠false (h₂ idp))
  ⊙maybe-Susp^-flip-comm (S m) O false h₁ h₂ = =⊙∘-in (! (⊙λ= (⊙∘-unit-l _)))
  ⊙maybe-Susp^-flip-comm {X = X} (S m) (S n) true h₁ h₂ =
    ⊙coe (⊙Susp^-comm (S m) (S n)) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ m (⊙Susp^ (S n) X)) ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & p ⟩
    ⊙Susp-fmap (fst (⊙coe (⊙Susp^-comm m (S n) ∙ ⊙Susp^-comm 1 n))) ◃⊙∘
    ⊙Susp-flip (⊙Susp^ m (⊙Susp^ (S n) X)) ◃⊙idf
      =⊙∘⟨ =⊙∘-in $ ! $
           ⊙Susp-flip-natural (⊙coe (⊙Susp^-comm m (S n) ∙ ⊙Susp^-comm 1 n)) ⟩
    ⊙Susp-flip (⊙Susp^ n (⊙Susp^ (S m) X)) ◃⊙∘
    ⊙Susp-fmap (fst (⊙coe (⊙Susp^-comm m (S n) ∙ ⊙Susp^-comm 1 n))) ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ! p ⟩
    ⊙Susp-flip (⊙Susp^ n (⊙Susp^ (S m) X)) ◃⊙∘
    ⊙Susp^-swap (S m) (S n) ◃⊙idf ∎⊙∘
    where
    p : ⊙Susp^-swap (S m) (S n) {X} ==
        ⊙Susp-fmap (fst (⊙coe (⊙Susp^-comm m (S n) {X} ∙ ⊙Susp^-comm 1 n {⊙Susp^ m X})))
    p =
      ap ⊙coe (⊙Susp^-comm-S-S m n) ∙
      ! (⊙transport-⊙coe ⊙Susp (Susp^-comm m (S n) ∙ Susp^-comm 1 n)) ∙
      ⊙transport-⊙Susp (Susp^-comm m (S n) ∙ Susp^-comm 1 n) ∙
      ! (ap (⊙Susp-fmap ∘ coe) (ap2 _∙_ (de⊙-⊙Susp^-comm m (S n)) (de⊙-⊙Susp^-comm 1 n))) ∙
      ap (⊙Susp-fmap ∘ coe) (∙-ap de⊙ (⊙Susp^-comm m (S n)) (⊙Susp^-comm 1 n))
  ⊙maybe-Susp^-flip-comm (S m) (S n) false h₁ h₂ = =⊙∘-in (! (⊙λ= (⊙∘-unit-l _)))

⊙∧Σ-Σ^∧-out : ∀ {i} {j} (X : Ptd i) (Y : Ptd j) (m : ℕ)
  → ⊙Susp-fmap (∧Σ^-out X Y m) ◃⊙∘
    ⊙Σ∧-out X (⊙Susp^ m Y) ◃⊙idf
    =⊙∘
    ⊙Susp^-swap m 1 {X = X ⊙∧ Y} ◃⊙∘
    ⊙maybe-Susp^-flip m (odd m) ◃⊙∘
    ⊙Susp^-fmap m (⊙Σ∧-out X Y) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ X)) Y m ◃⊙idf
⊙∧Σ-Σ^∧-out X Y 0 =
  ⊙Susp-fmap (idf (X ∧ Y)) ◃⊙∘
  ⊙Σ∧-out X (⊙Susp^ 0 Y) ◃⊙idf
    =⊙∘⟨ 0 & 1 & ⊙Susp-fmap-idf _ ⟩
  ⊙Σ∧-out X (⊙Susp^ 0 Y) ◃⊙idf
    =⊙∘⟨ 0 & 0 & ⊙contract ⟩
  ⊙idf _ ◃⊙∘
  ⊙Σ∧-out X (⊙Susp^ 0 Y) ◃⊙idf
    =⊙∘₁⟨ 0 & 1 & ap ⊙coe (! (⊙Susp^-comm-0-l 1 (X ⊙∧ Y))) ⟩
  ⊙Susp^-swap 0 1 ◃⊙∘
  ⊙Σ∧-out X (⊙Susp^ 0 Y) ◃⊙idf
    =⊙∘⟨ 1 & 0 & ⊙contract ⟩
  ⊙Susp^-swap 0 1 ◃⊙∘
  ⊙idf _ ◃⊙∘
  ⊙Σ∧-out X (⊙Susp^ 0 Y) ◃⊙idf
    =⊙∘⟨ 3 & 0 & ⊙contract ⟩
  ⊙Susp^-swap 0 1 ◃⊙∘
  ⊙idf _ ◃⊙∘
  ⊙Σ∧-out X (⊙Susp^ 0 Y) ◃⊙∘
  ⊙idf _ ◃⊙idf ∎⊙∘
⊙∧Σ-Σ^∧-out X Y (S m) =
  ⊙Susp-fmap (∧Σ^-out X Y (S m)) ◃⊙∘
  ⊙Σ∧-out X (⊙Susp^ (S m) Y) ◃⊙idf
    =⊙∘⟨ 0 & 1 & ⊙Susp-fmap-seq-∘ (Susp-fmap (∧Σ^-out X Y m) ◃∘
                                   ∧Σ-out X (⊙Susp^ m Y) ◃idf) ⟩
  ⊙Susp^-fmap 2 (⊙∧Σ^-out X Y m) ◃⊙∘
  ⊙Susp-fmap (∧Σ-out X (⊙Susp^ m Y)) ◃⊙∘
  ⊙Σ∧-out X (⊙Susp^ (S m) Y) ◃⊙idf
    =⊙∘⟨ 1 & 2 & ⊙∧Σ-Σ∧-out X (⊙Susp^ m Y) ⟩
  ⊙Susp^-fmap 2 (⊙∧Σ^-out X Y m) ◃⊙∘
  ⊙Susp-flip (⊙Susp (X ∧ ⊙Susp^ m Y)) ◃⊙∘
  ⊙Susp-fmap (Σ∧-out X (⊙Susp^ m Y)) ◃⊙∘
  ⊙∧Σ-out (⊙Susp (de⊙ X)) (⊙Susp^ m Y) ◃⊙idf
    =⊙∘⟨ 0 & 2 & =⊙∘-in {gs = ⊙Susp-flip (⊙Susp (Susp^ m (X ∧ Y))) ◃⊙∘
                              ⊙Susp^-fmap 2 (⊙∧Σ^-out X Y m) ◃⊙idf} $
                 ! (⊙Susp-flip-natural (⊙Susp-fmap (∧Σ^-out X Y m))) ⟩
  ⊙Susp-flip (⊙Susp (Susp^ m (X ∧ Y))) ◃⊙∘
  ⊙Susp^-fmap 2 (⊙∧Σ^-out X Y m) ◃⊙∘
  ⊙Susp-fmap (Σ∧-out X (⊙Susp^ m Y)) ◃⊙∘
  ⊙∧Σ-out (⊙Susp (de⊙ X)) (⊙Susp^ m Y) ◃⊙idf
    =⊙∘⟨ 1 & 2 & ⊙Susp-fmap-seq-=⊙∘ (de⊙-seq-=⊙∘ (⊙∧Σ-Σ^∧-out X Y m)) ⟩
  ⊙Susp-flip (⊙Susp (Susp^ m (X ∧ Y))) ◃⊙∘
  ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm m 1))) ◃⊙∘
  ⊙Susp-fmap (fst (⊙maybe-Susp^-flip m (odd m))) ◃⊙∘
  ⊙Susp^-fmap (S m) (⊙Σ∧-out X Y) ◃⊙∘
  ⊙Susp-fmap (∧Σ^-out (⊙Susp (de⊙ X)) Y m) ◃⊙∘
  ⊙∧Σ-out (⊙Susp (de⊙ X)) (⊙Susp^ m Y) ◃⊙idf
    =⊙∘⟨ 0 & 2 & =⊙∘-in {gs = ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm m 1))) ◃⊙∘
                              ⊙Susp-flip (⊙Susp^ m (⊙Susp (X ∧ Y))) ◃⊙idf} $
                 ⊙Susp-flip-natural (⊙coe (⊙Susp^-comm m 1)) ⟩
  ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm m 1))) ◃⊙∘
  ⊙Susp-flip (⊙Susp^ m (⊙Susp (X ∧ Y))) ◃⊙∘
  ⊙Susp-fmap (fst (⊙maybe-Susp^-flip m (odd m))) ◃⊙∘
  ⊙Susp^-fmap (S m) (⊙Σ∧-out X Y) ◃⊙∘
  ⊙Susp-fmap (∧Σ^-out (⊙Susp (de⊙ X)) Y m) ◃⊙∘
  ⊙∧Σ-out (⊙Susp (de⊙ X)) (⊙Susp^ m Y) ◃⊙idf
    =⊙∘⟨ 4 & 2 & ⊙contract ⟩
  ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm m 1))) ◃⊙∘
  ⊙Susp-flip (⊙Susp^ m (⊙Susp (X ∧ Y))) ◃⊙∘
  ⊙Susp-fmap (fst (⊙maybe-Susp^-flip m (odd m))) ◃⊙∘
  ⊙Susp^-fmap (S m) (⊙Σ∧-out X Y) ◃⊙∘
  ⊙∧Σ^-out (⊙Susp (de⊙ X)) Y (S m) ◃⊙idf
    =⊙∘₁⟨ 0 & 1 & ! (⊙transport-⊙Susp (ap de⊙ (⊙Susp^-comm m 1))) ∙
                  ap (⊙transport ⊙Susp) (de⊙-⊙Susp^-comm m 1) ∙
                  ⊙transport-⊙coe ⊙Susp (Susp^-comm m 1) ∙
                  ap ⊙coe (! (⊙Susp^-comm-S-1 m {X ⊙∧ Y})) ⟩
  ⊙coe (⊙Susp^-comm (S m) 1) ◃⊙∘
  ⊙Susp-flip (⊙Susp^ m (⊙Susp (X ∧ Y))) ◃⊙∘
  ⊙Susp-fmap (fst (⊙maybe-Susp^-flip m (odd m))) ◃⊙∘
  ⊙Susp^-fmap (S m) (⊙Σ∧-out X Y) ◃⊙∘
  ⊙∧Σ^-out (⊙Susp (de⊙ X)) Y (S m) ◃⊙idf
    =⊙∘₁⟨ 2 & 1 & ap ⊙Susp-fmap (de⊙-⊙maybe-Susp^-flip m (odd m)) ⟩
  ⊙coe (⊙Susp^-comm (S m) 1) ◃⊙∘
  ⊙Susp-flip (⊙Susp^ m (⊙Susp (X ∧ Y))) ◃⊙∘
  ⊙Susp-fmap (maybe-Susp^-flip m (odd m)) ◃⊙∘
  ⊙Susp^-fmap (S m) (⊙Σ∧-out X Y) ◃⊙∘
  ⊙∧Σ^-out (⊙Susp (de⊙ X)) Y (S m) ◃⊙idf
    =⊙∘₁⟨ 2 & 1 & ⊙Susp-fmap-maybe-Susp^-flip m (odd m) (ap odd) ⟩
  ⊙coe (⊙Susp^-comm (S m) 1) ◃⊙∘
  ⊙Susp-flip (⊙Susp^ m (⊙Susp (X ∧ Y))) ◃⊙∘
  ⊙maybe-Susp-flip (⊙Susp^ m (⊙Susp (X ∧ Y))) (odd m) ◃⊙∘
  ⊙Susp^-fmap (S m) (⊙Σ∧-out X Y) ◃⊙∘
  ⊙∧Σ^-out (⊙Susp (de⊙ X)) Y (S m) ◃⊙idf
    =⊙∘⟨ 1 & 2 & ⊙maybe-Susp-flip-flip _ true (odd m) ⟩
  ⊙coe (⊙Susp^-comm (S m) 1) ◃⊙∘
  ⊙maybe-Susp-flip (⊙Susp^ m (⊙Susp (X ∧ Y))) (odd (S m)) ◃⊙∘
  ⊙Susp^-fmap (S m) (⊙Σ∧-out X Y) ◃⊙∘
  ⊙∧Σ^-out (⊙Susp (de⊙ X)) Y (S m) ◃⊙idf ∎⊙∘

module _ {i j} (X : Ptd i) (Y : Ptd j) where

  ⊙∧Σ^-Σ^∧-out : ∀ (m n : ℕ)
    → ⊙Susp^-fmap m (⊙∧Σ^-out X Y n) ◃⊙∘
      ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf
      =⊙∘
      ⊙coe (⊙Susp^-comm n m) ◃⊙∘
      ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
      ⊙Susp^-fmap n (⊙Σ^∧-out X Y m) ◃⊙∘
      ⊙∧Σ^-out (⊙Susp^ m X) Y n ◃⊙idf
  ⊙∧Σ^-Σ^∧-out O n =
    ⊙∧Σ^-out X Y n ◃⊙∘
    ⊙idf _ ◃⊙idf
      =⊙∘⟨ 1 & 1 & ⊙expand ⊙idf-seq ⟩
    ⊙∧Σ^-out X Y n ◃⊙idf
      =⊙∘⟨ 0 & 0 & !⊙∘ (⊙Susp^-fmap-idf n (X ⊙∧ Y)) ⟩
    ⊙Susp^-fmap n (⊙idf (X ⊙∧ Y)) ◃⊙∘
    ⊙∧Σ^-out X Y n ◃⊙idf
      =⊙∘₁⟨ 0 & 0 & ! (⊙maybe-Susp^-flip-false n) ⟩
    ⊙maybe-Susp^-flip n false ◃⊙∘
    ⊙Susp^-fmap n (⊙idf (X ⊙∧ Y)) ◃⊙∘
    ⊙∧Σ^-out X Y n ◃⊙idf
      =⊙∘₁⟨ 0 & 0 & ap ⊙coe (! (⊙Susp^-comm-0-r n _)) ⟩
    ⊙coe (⊙Susp^-comm n O) ◃⊙∘
    ⊙maybe-Susp^-flip n false ◃⊙∘
    ⊙Susp^-fmap n (⊙idf (X ⊙∧ Y)) ◃⊙∘
    ⊙∧Σ^-out X Y n ◃⊙idf ∎⊙∘
  ⊙∧Σ^-Σ^∧-out (S m) n =
    ⊙Susp^-fmap (S m) (⊙∧Σ^-out X Y n) ◃⊙∘
    ⊙Σ^∧-out X (⊙Susp^ n Y) (S m) ◃⊙idf
      =⊙∘⟨ 1 & 1 & ⊙expand (⊙Susp-fmap (Σ^∧-out X (⊙Susp^ n Y) m) ◃⊙∘
                            ⊙Σ∧-out (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf) ⟩
    ⊙Susp^-fmap (S m) (⊙∧Σ^-out X Y n) ◃⊙∘
    ⊙Susp-fmap (Σ^∧-out X (⊙Susp^ n Y) m) ◃⊙∘
    ⊙Σ∧-out (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙Susp-fmap-seq-=⊙∘ (de⊙-seq-=⊙∘ (⊙∧Σ^-Σ^∧-out m n)) ⟩
    ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm n m))) ◃⊙∘
    ⊙Susp-fmap (fst (⊙maybe-Susp^-flip n (and (odd m) (odd n)))) ◃⊙∘
    ⊙Susp-fmap (Susp^-fmap n (Σ^∧-out X Y m)) ◃⊙∘
    ⊙Susp-fmap (∧Σ^-out (⊙Susp^ m X) Y n) ◃⊙∘
    ⊙Σ∧-out (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf
      =⊙∘⟨ 3 & 2 & ⊙∧Σ-Σ^∧-out (⊙Susp^ m X) Y n ⟩
    ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm n m))) ◃⊙∘
    ⊙Susp-fmap (fst (⊙maybe-Susp^-flip n (and (odd m) (odd n)))) ◃⊙∘
    ⊙Susp-fmap (Susp^-fmap n (Σ^∧-out X Y m)) ◃⊙∘
    ⊙Susp^-swap n 1 ◃⊙∘
    ⊙maybe-Susp^-flip n (odd n) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ∧-out (⊙Susp^ m X) Y) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf
      =⊙∘⟨ 2 & 2 & !⊙∘ $ ⊙Susp^-swap-natural n 1 (⊙Σ^∧-out X Y m) ⟩
    ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm n m))) ◃⊙∘
    ⊙Susp-fmap (fst (⊙maybe-Susp^-flip n (and (odd m) (odd n)))) ◃⊙∘
    ⊙Susp^-swap n 1 ◃⊙∘
    ⊙Susp^-fmap n (⊙Susp-fmap (Σ^∧-out X Y m)) ◃⊙∘
    ⊙maybe-Susp^-flip n (odd n) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ∧-out (⊙Susp^ m X) Y) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf
      =⊙∘⟨ 3 & 2 & ⊙maybe-Susp^-flip-natural-=⊙∘ (⊙Susp-fmap (Σ^∧-out X Y m)) n (odd n) ⟩
    ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm n m))) ◃⊙∘
    ⊙Susp-fmap (fst (⊙maybe-Susp^-flip n (and (odd m) (odd n)))) ◃⊙∘
    ⊙Susp^-swap n 1 ◃⊙∘
    ⊙maybe-Susp^-flip n (odd n) ◃⊙∘
    ⊙Susp^-fmap n (⊙Susp-fmap (Σ^∧-out X Y m)) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ∧-out (⊙Susp^ m X) Y) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf
      =⊙∘₁⟨ 4 & 2 & ! $ ⊙Susp^-fmap-∘ n (⊙Susp-fmap (Σ^∧-out X Y m)) (⊙Σ∧-out (⊙Susp^ m X) Y) ⟩
    ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm n m))) ◃⊙∘
    ⊙Susp-fmap (fst (⊙maybe-Susp^-flip n (and (odd m) (odd n)))) ◃⊙∘
    ⊙Susp^-swap n 1 ◃⊙∘
    ⊙maybe-Susp^-flip n (odd n) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y (S m)) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙maybe-Susp^-flip-⊙Susp^-comm _ n 1 (and (odd m) (odd n)) ⟩
    ⊙Susp-fmap (coe (ap de⊙ (⊙Susp^-comm n m))) ◃⊙∘
    ⊙coe (⊙Susp^-comm n 1) ◃⊙∘
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙maybe-Susp^-flip n (odd n) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y (S m)) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ! (⊙transport-⊙Susp (ap de⊙ (⊙Susp^-comm n m))) ∙
                    ⊙transport-⊙coe ⊙Susp (ap de⊙ (⊙Susp^-comm n m)) ∙
                    ap (⊙coe ∘ ap ⊙Susp) (de⊙-⊙Susp^-comm n m) ⟩
    ⊙coe (ap ⊙Susp (Susp^-comm n m)) ◃⊙∘
    ⊙coe (⊙Susp^-comm n 1) ◃⊙∘
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙maybe-Susp^-flip n (odd n) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y (S m)) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf
      =⊙∘₁⟨ 0 & 2 & ! (=⊙∘-out (⊙coe-∙ (⊙Susp^-comm n 1) (ap ⊙Susp (Susp^-comm n m)))) ∙
                    ap ⊙coe (! (=ₛ-out (⊙Susp^-comm-S-r n m))) ⟩
    ⊙coe (⊙Susp^-comm n (S m)) ◃⊙∘
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙maybe-Susp^-flip n (odd n) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y (S m)) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙maybe-Susp^-flip-flip n (and (odd m) (odd n)) (odd n) ⟩
    ⊙coe (⊙Susp^-comm n (S m)) ◃⊙∘
    ⊙maybe-Susp^-flip n (xor (and (odd m) (odd n)) (odd n)) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y (S m)) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ap (⊙maybe-Susp^-flip n) (table (odd m) (odd n)) ⟩
    ⊙coe (⊙Susp^-comm n (S m)) ◃⊙∘
    ⊙maybe-Susp^-flip n (and (odd (S m)) (odd n)) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y (S m)) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp (de⊙ (⊙Susp^ m X))) Y n ◃⊙idf ∎⊙∘
    where
    table : ∀ (b c : Bool) → xor (and b c) c == and (negate b) c
    table true  true  = idp
    table true  false = idp
    table false true  = idp
    table false false = idp

  ⊙∧Σ^-Σ^∧-out' : ∀ (m n : ℕ)
    → ⊙Susp^-fmap n (⊙Σ^∧-out X Y m) ◃⊙∘
      ⊙∧Σ^-out (⊙Susp^ m X) Y n ◃⊙idf
      =⊙∘
      ⊙coe (⊙Susp^-comm m n) ◃⊙∘
      ⊙maybe-Susp^-flip m (and (odd m) (odd n)) ◃⊙∘
      ⊙Susp^-fmap m (⊙∧Σ^-out X Y n) ◃⊙∘
      ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf
  ⊙∧Σ^-Σ^∧-out' m n =
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y m) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp^ m X) Y n ◃⊙idf
      =⊙∘₁⟨ 0 & 0 & ! (⊙maybe-Susp^-flip-false n) ∙
                    ap (⊙maybe-Susp^-flip n) (! (xor-diag (and (odd m) (odd n)))) ⟩
    ⊙maybe-Susp^-flip n (xor (and (odd m) (odd n)) (and (odd m) (odd n))) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y m) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp^ m X) Y n ◃⊙idf
      =⊙∘⟨ 0 & 1 & !⊙∘ $ ⊙maybe-Susp^-flip-flip n (and (odd m) (odd n)) (and (odd m) (odd n)) ⟩
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y m) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp^ m X) Y n ◃⊙idf
      =⊙∘⟨ 1 & 0 & =⊙∘-in {gs = ⊙coe (! (⊙Susp^-comm n m)) ◃⊙∘
                                ⊙coe (⊙Susp^-comm n m) ◃⊙idf} $
           ap ⊙coe (! (!-inv-r (⊙Susp^-comm n m))) ∙
           =⊙∘-out (⊙coe-∙ (⊙Susp^-comm n m) (! (⊙Susp^-comm n m))) ⟩
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙coe (! (⊙Susp^-comm n m)) ◃⊙∘
    ⊙coe (⊙Susp^-comm n m) ◃⊙∘
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙Susp^-fmap n (⊙Σ^∧-out X Y m) ◃⊙∘
    ⊙∧Σ^-out (⊙Susp^ m X) Y n ◃⊙idf
      =⊙∘⟨ 2 & 4 & !⊙∘ $ ⊙∧Σ^-Σ^∧-out m n ⟩
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙coe (! (⊙Susp^-comm n m)) ◃⊙∘
    ⊙Susp^-fmap m (⊙∧Σ^-out X Y n) ◃⊙∘
    ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ap ⊙coe (⊙Susp^-comm-! n m) ⟩
    ⊙maybe-Susp^-flip n (and (odd m) (odd n)) ◃⊙∘
    ⊙coe (⊙Susp^-comm m n) ◃⊙∘
    ⊙Susp^-fmap m (⊙∧Σ^-out X Y n) ◃⊙∘
    ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf
      =⊙∘⟨ 0 & 2 & !⊙∘ $
           ⊙maybe-Susp^-flip-comm m n (and (odd m) (odd n))
             (ap (λ k → and (odd k) (odd n)))
             (λ p → ap (and (odd m) ∘ odd) p ∙ and-false-r (odd m)) ⟩
    ⊙coe (⊙Susp^-comm m n) ◃⊙∘
    ⊙maybe-Susp^-flip m (and (odd m) (odd n)) ◃⊙∘
    ⊙Susp^-fmap m (⊙∧Σ^-out X Y n) ◃⊙∘
    ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf ∎⊙∘

  ⊙Σ^∧Σ^-out-seq : ∀ (m n : ℕ) → (⊙Susp^ m X ⊙∧ ⊙Susp^ n Y) ⊙–→ ⊙Susp^ (m + n) (X ⊙∧ Y)
  ⊙Σ^∧Σ^-out-seq m n =
    ⊙coe (⊙Susp^-+ m n {X ⊙∧ Y}) ◃⊙∘
    ⊙Susp^-fmap m (⊙∧Σ^-out X Y n) ◃⊙∘
    ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf

  ⊙Σ^∧Σ^-out : ∀ (m n : ℕ) → ⊙Susp^ m X ⊙∧ ⊙Susp^ n Y ⊙→ ⊙Susp^ (m + n) (X ⊙∧ Y)
  ⊙Σ^∧Σ^-out m n = ⊙compose (⊙Σ^∧Σ^-out-seq m n)

  swap-⊙Σ^∧-out : ∀ (m : ℕ)
    → ⊙Susp^-fmap m (⊙∧-swap X Y) ◃⊙∘
      ⊙Σ^∧-out X Y m ◃⊙idf
      =⊙∘
      ⊙∧Σ^-out Y X m ◃⊙∘
      ⊙∧-swap (⊙Susp^ m X) Y ◃⊙idf
  swap-⊙Σ^∧-out O = =⊙∘-in $ ! $ ⊙λ= $ ⊙∘-unit-l (⊙∧-swap X Y)
  swap-⊙Σ^∧-out (S m) =
    ⊙Susp^-fmap (S m) (⊙∧-swap X Y) ◃⊙∘
    ⊙Σ^∧-out X Y (S m) ◃⊙idf
      =⊙∘⟨ 1 & 1 & ⊙expand (⊙Susp-fmap (Σ^∧-out X Y m) ◃⊙∘
                            ⊙Σ∧-out (⊙Susp^ m X) Y ◃⊙idf) ⟩
    ⊙Susp^-fmap (S m) (⊙∧-swap X Y) ◃⊙∘
    ⊙Susp-fmap (Σ^∧-out X Y m) ◃⊙∘
    ⊙Σ∧-out (⊙Susp^ m X) Y ◃⊙idf
      =⊙∘⟨ 0 & 2 &
           ⊙Susp-fmap-seq-=⊙∘ (de⊙-seq-=⊙∘ (swap-⊙Σ^∧-out m)) ⟩
    ⊙Susp-fmap (∧Σ^-out Y X m) ◃⊙∘
    ⊙Susp-fmap (∧-swap (⊙Susp^ m X) Y) ◃⊙∘
    ⊙Σ∧-out (⊙Susp^ m X) Y ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙swap-Σ∧-out (⊙Susp^ m X) Y ⟩
    ⊙Susp-fmap (∧Σ^-out Y X m) ◃⊙∘
    ⊙∧Σ-out Y (⊙Susp^ m X) ◃⊙∘
    ⊙∧-swap (⊙Susp (de⊙ (⊙Susp^ m X))) Y ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙contract ⟩
    ⊙∧Σ^-out Y X (S m) ◃⊙∘
    ⊙∧-swap (⊙Susp^ (S m) X) Y ◃⊙idf ∎⊙∘

  swap-⊙∧Σ^-out : ∀ (n : ℕ)
    → ⊙Susp^-fmap n (⊙∧-swap X Y) ◃⊙∘
      ⊙∧Σ^-out X Y n ◃⊙idf
      =⊙∘
      ⊙Σ^∧-out Y X n ◃⊙∘
      ⊙∧-swap X (⊙Susp^ n Y) ◃⊙idf
  swap-⊙∧Σ^-out O = =⊙∘-in $ ! $ ⊙λ= $ ⊙∘-unit-l (⊙∧-swap X Y)
  swap-⊙∧Σ^-out (S n) =
    ⊙Susp^-fmap (S n) (⊙∧-swap X Y) ◃⊙∘
    ⊙∧Σ^-out X Y (S n) ◃⊙idf
      =⊙∘⟨ 1 & 1 & ⊙expand (⊙Susp-fmap (∧Σ^-out X Y n) ◃⊙∘
                            ⊙∧Σ-out X (⊙Susp^ n Y) ◃⊙idf) ⟩
    ⊙Susp^-fmap (S n) (⊙∧-swap X Y) ◃⊙∘
    ⊙Susp-fmap (∧Σ^-out X Y n) ◃⊙∘
    ⊙∧Σ-out X (⊙Susp^ n Y) ◃⊙idf
      =⊙∘⟨ 0 & 2 &
           ⊙Susp-fmap-seq-=⊙∘ (de⊙-seq-=⊙∘ (swap-⊙∧Σ^-out n))⟩
    ⊙Susp-fmap (fst (⊙Σ^∧-out Y X n)) ◃⊙∘
    ⊙Susp-fmap (fst (⊙∧-swap X (⊙Susp^ n Y))) ◃⊙∘
    ⊙∧Σ-out X (⊙Susp^ n Y) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙swap-∧Σ-out X (⊙Susp^ n Y) ⟩
    ⊙Susp-fmap (fst (⊙Σ^∧-out Y X n)) ◃⊙∘
    ⊙Σ∧-out (⊙Susp^ n Y) X ◃⊙∘
    ⊙∧-swap X (⊙Susp (de⊙ (⊙Susp^ n Y))) ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙contract ⟩
    ⊙Σ^∧-out Y X (S n) ◃⊙∘
    ⊙∧-swap X (⊙Susp^ (S n) Y) ◃⊙idf ∎⊙∘

⊙Σ^∧Σ^-out-swap : ∀ {i} {j} (X : Ptd i) (Y : Ptd j) (m n : ℕ)
  → ⊙transport (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-swap X Y) ◃⊙∘
    ⊙Σ^∧Σ^-out X Y m n ◃⊙idf
    =⊙∘
    ⊙maybe-Susp^-flip (n + m) (and (odd n) (odd m)) ◃⊙∘
    ⊙Σ^∧Σ^-out Y X n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf
⊙Σ^∧Σ^-out-swap X Y m n =
  ⊙transport (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃⊙∘
  ⊙Susp^-fmap (m + n) (⊙∧-swap X Y) ◃⊙∘
  ⊙Σ^∧Σ^-out X Y m n ◃⊙idf
    =⊙∘⟨ 2 & 1 & ⊙expand (⊙Σ^∧Σ^-out-seq X Y m n) ⟩
  ⊙transport (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃⊙∘
  ⊙Susp^-fmap (m + n) (⊙∧-swap X Y) ◃⊙∘
  ⊙coe (⊙Susp^-+ m n) ◃⊙∘
  ⊙Susp^-fmap m (⊙∧Σ^-out X Y n) ◃⊙∘
  ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf
    =⊙∘⟨ 1 & 2 & =⊙∘-in {gs = ⊙coe (⊙Susp^-+ m n) ◃⊙∘
                              ⊙Susp^-fmap m (⊙Susp^-fmap n (⊙∧-swap X Y)) ◃⊙idf} $
         ! $ ⊙Susp^-+-natural m n (⊙∧-swap X Y) ⟩
  ⊙transport (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃⊙∘
  ⊙coe (⊙Susp^-+ m n) ◃⊙∘
  ⊙Susp^-fmap m (⊙Susp^-fmap n (⊙∧-swap X Y)) ◃⊙∘
  ⊙Susp^-fmap m (⊙∧Σ^-out X Y n) ◃⊙∘
  ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf
    =⊙∘⟨ 2 & 2 & ⊙Susp^-fmap-seq-=⊙∘ m $ swap-⊙∧Σ^-out X Y n ⟩
  ⊙transport (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃⊙∘
  ⊙coe (⊙Susp^-+ m n) ◃⊙∘
  ⊙Susp^-fmap m (⊙Σ^∧-out Y X n) ◃⊙∘
  ⊙Susp^-fmap m (⊙∧-swap X (⊙Susp^ n Y)) ◃⊙∘
  ⊙Σ^∧-out X (⊙Susp^ n Y) m ◃⊙idf
    =⊙∘⟨ 3 & 2 & swap-⊙Σ^∧-out X (⊙Susp^ n Y) m ⟩
  ⊙transport (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃⊙∘
  ⊙coe (⊙Susp^-+ m n) ◃⊙∘
  ⊙Susp^-fmap m (⊙Σ^∧-out Y X n) ◃⊙∘
  ⊙∧Σ^-out (⊙Susp^ n Y) X m ◃⊙∘
  ⊙∧-swap (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf
    =⊙∘⟨ 2 & 2 & ⊙∧Σ^-Σ^∧-out' Y X n m ⟩
  ⊙transport (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃⊙∘
  ⊙coe (⊙Susp^-+ m n) ◃⊙∘
  ⊙coe (⊙Susp^-comm n m) ◃⊙∘
  ⊙maybe-Susp^-flip n (and (odd n) (odd m)) ◃⊙∘
  ⊙Susp^-fmap n (⊙∧Σ^-out Y X m) ◃⊙∘
  ⊙Σ^∧-out Y (⊙Susp^ m X) n ◃⊙∘
  ⊙∧-swap (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf
    =⊙∘₁⟨ 0 & 1 & ⊙transport-⊙coe (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ⟩
  ⊙coe (ap (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n)) ◃⊙∘
  ⊙coe (⊙Susp^-+ m n) ◃⊙∘
  ⊙coe (⊙Susp^-comm n m) ◃⊙∘
  ⊙maybe-Susp^-flip n (and (odd n) (odd m)) ◃⊙∘
  ⊙Susp^-fmap n (⊙∧Σ^-out Y X m) ◃⊙∘
  ⊙Σ^∧-out Y (⊙Susp^ m X) n ◃⊙∘
  ⊙∧-swap (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf
    =⊙∘⟨ 0 & 3 & ⊙coe-seq-=ₛ p ⟩
  ⊙coe (⊙Susp^-+ n m) ◃⊙∘
  ⊙maybe-Susp^-flip n (and (odd n) (odd m)) ◃⊙∘
  ⊙Susp^-fmap n (⊙∧Σ^-out Y X m) ◃⊙∘
  ⊙Σ^∧-out Y (⊙Susp^ m X) n ◃⊙∘
  ⊙∧-swap (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf
    =⊙∘⟨ 0 & 2 & ⊙maybe-Susp^-flip-+ n m (and (odd n) (odd m))
           (ap (λ k → and (odd k) (odd m))) ⟩
  ⊙maybe-Susp^-flip (n + m) (and (odd n) (odd m)) ◃⊙∘
  ⊙coe (⊙Susp^-+ n m) ◃⊙∘
  ⊙Susp^-fmap n (⊙∧Σ^-out Y X m) ◃⊙∘
  ⊙Σ^∧-out Y (⊙Susp^ m X) n ◃⊙∘
  ⊙∧-swap (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf
    =⊙∘⟨ 1 & 3 & ⊙contract ⟩
  ⊙maybe-Susp^-flip (n + m) (and (odd n) (odd m)) ◃⊙∘
  ⊙Σ^∧Σ^-out Y X n m ◃⊙∘
  ⊙∧-swap (⊙Susp^ m X) (⊙Susp^ n Y) ◃⊙idf ∎⊙∘
  where
  p : ⊙Susp^-comm n m ◃∙
      ⊙Susp^-+ m n {Y ⊙∧ X} ◃∙
      ap (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃∎
      =ₛ
      ⊙Susp^-+ n m {Y ⊙∧ X} ◃∎
  p =
    ⊙Susp^-comm n m ◃∙
    ⊙Susp^-+ m n {Y ⊙∧ X} ◃∙
    ap (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃∎
      =ₛ⟨ 0 & 1 & expand (⊙Susp^-comm-seq n m) ⟩
    ⊙Susp^-+ n m ◃∙
    ap (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm n m) ◃∙
    ! (⊙Susp^-+ m n) ◃∙
    ⊙Susp^-+ m n ◃∙
    ap (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃∎
      =ₛ⟨ 2 & 2 & seq-!-inv-l (⊙Susp^-+ m n ◃∎) ⟩
    ⊙Susp^-+ n m ◃∙
    ap (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm n m) ◃∙
    ap (λ k → ⊙Susp^ k (Y ⊙∧ X)) (+-comm m n) ◃∎
      =ₛ⟨ 1 & 2 & ap-seq-=ₛ (λ k → ⊙Susp^ k (Y ⊙∧ X)) $
          =ₛ-in {s = +-comm n m ◃∙ +-comm m n ◃∎} {t = []} $
          set-path ℕ-level _ _ ⟩
    ⊙Susp^-+ n m ◃∎ ∎ₛ

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Everything
{-
open import Oscar.Prelude
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Symmetrical
open import Oscar.Data.Fin
open import Oscar.Data.Term
open import Oscar.Data.Substitunction
open import Oscar.Data.Proposequality
open import Oscar.Data.Surjcollation
open import Oscar.Data.Surjextenscollation
import Oscar.Class.HasEquivalence.ExtensionṖroperty
import Oscar.Class.HasEquivalence.Ṗroperty
import Oscar.Class.Symmetrical.ExtensionalUnifies
import Oscar.Class.Symmetrical.Unifies
import Oscar.Property.Setoid.Proposequality -- FIXME see fact1⋆ below; comment this out to observe confusing error messages
import Oscar.Property.Functor.SubstitunctionExtensionTerm
import Oscar.Class.Surjection.⋆
-}
module Test.Surjcollation {𝔭} (𝔓 : Ø 𝔭) where
  open Term 𝔓
  open Substitunction 𝔓

  module 𝓢 = Surjcollation Substitunction Proposequality
  module 𝓢̇ = Surjextenscollation Substitunction Proposextensequality

  fact1⋆ : ∀ {𝓃} (𝓈 𝓉 : Term 𝓃) → 𝓈 𝓢.⟹ 𝓉 ≈ 𝓉 𝓢.⟹ 𝓈
  fact1⋆ 𝓈 𝓉 = symmetrical 𝓈 𝓉
  -- fact1⋆ 𝓈 𝓉 = symmetrical ⦃ r = Oscar.Class.Symmetrical.Unifies.𝓢ymmetricalUnifies₀ ⦃ ! ⦄ ⦃ ! ⦄ ⦃ Oscar.Property.Setoid.Proposequality.𝓢ymmetryProposequality ⦄ ⦄ 𝓈 𝓉 -- FIXME I wish Agda would tell us that this is how the instances were resolved

  fact1⋆s : ∀ {N 𝓃} (𝓈 𝓉 : Terms N 𝓃) → 𝓈 𝓢.⟹ 𝓉 ≈ 𝓉 𝓢.⟹ 𝓈
  fact1⋆s 𝓈 𝓉 = symmetrical 𝓈 𝓉

  fact1 : ∀ {𝓃} (𝓈 𝓉 : Term 𝓃) → 𝓈 𝓢̇.⟹ 𝓉 ≈ 𝓉 𝓢̇.⟹ 𝓈
  fact1 𝓈 𝓉 = symmetrical 𝓈 𝓉


text:
-- Andreas, 2014-06-11, issue reported by Ulf
-- {-# OPTIONS -v tc.check.internal:100 -v tc.conv.elim:40 #-}

postulate
  Nat  : Set
  zero : Nat

module Projection where

  record _×_ (A B : Set) : Set where
    field fst : A
          snd : B
  open _×_

  postulate
    T    : (Nat × Nat → Nat) → Set
    foo  : T fst → Nat

  works : T fst → Nat
  works t with foo t
  works t | z = zero

module ProjectionLike where

  data _×_ (A B : Set) : Set where
    _,_ : A → B → A × B

  fst : {A B : Set} → A × B → A
  fst (x , y) = x

  postulate
    T    : (Nat × Nat → Nat) → Set
    foo  : T fst → Nat

  -- Error WAS::
  -- {A B : Set} → A × B → A != Nat × Nat → Nat because one is an
  -- implicit function type and the other is an explicit function type
  -- when checking that the type (t : T fst) → Nat → Nat of the
  -- generated with function is well-formed
  test : T fst → Nat
  test t with foo t
  test t | z = zero

-- Problem WAS:
-- It looks like CheckInternal doesn't handle projection-like functions
-- correctly. It works for actual projections (if you make _×_ a record)
-- and non-projection-like functions (if you make fst a postulate).

-- Should work without error.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Type(s) used (only) when calling out to Haskell via the FFI
------------------------------------------------------------------------

module Foreign.Haskell where

-- A unit type.

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}


text:
open import Prelude

module MJ.Classtable (c : ℕ) where

open import MJ.Classtable.Core c public


text:
module TermIsomorphism where

open import OscarPrelude

open import Term
open import VariableName
open import FunctionName
open import Arity
open import Vector

open import Data.Fin using (fromℕ ; toℕ ) renaming (raise to raiseFin)
open import Unify using (i ; leaf ; _fork_) renaming (Term to STerm ; AList to SAList)
open import UnifyProof2 using (mgu-c)

raiseSTerm : ∀ {m} n {o} → o ≡ n + m → STerm m → STerm o
raiseSTerm n refl (i x) = i (raiseFin n x)
raiseSTerm n o≡n+m leaf = leaf
raiseSTerm n refl (τ₁ fork τ₂) = raiseSTerm n refl τ₁ fork raiseSTerm n refl τ₂

max' : Nat → Nat → Nat
max' x y = if x >? y then x else y

aux-lemma-m<n : ∀ {m n : Nat} → IsTrue (lessNat m n) → n ≡ n - m + m
aux-lemma-m<n {zero} {zero} _ = refl
aux-lemma-m<n {zero} {suc _} _ = auto
aux-lemma-m<n {suc _} {zero} ()
aux-lemma-m<n {suc m} {suc n} m<n = by (aux-lemma-m<n {m} {n} m<n)

aux-lemma-m≮n,n≮m : ∀ {m n : Nat} → ¬ IsTrue (lessNat m n) → ¬ IsTrue (lessNat n m) → m ≡ n
aux-lemma-m≮n,n≮m {zero} {zero} m≮n n≮m = refl
aux-lemma-m≮n,n≮m {zero} {suc n} m≮n n≮m = ⊥-elim (m≮n true)
aux-lemma-m≮n,n≮m {suc m} {zero} m≮n n≮m = ⊥-elim (n≮m true)
aux-lemma-m≮n,n≮m {suc m} {suc n} m≮n n≮m = by (aux-lemma-m≮n,n≮m {m} {n} m≮n n≮m)

max-lemma-left : ∀ {m n : Nat} → max m n ≡ max m n - m + m
max-lemma-left {m} {n} with decBool (lessNat n m)
max-lemma-left {m} {n} | yes n<m = auto
max-lemma-left {m} {n} | no n≮m with decBool (lessNat m n)
max-lemma-left {m} {n} | no n≮m | (yes m<n) = aux-lemma-m<n m<n
max-lemma-left {m} {n} | no n≮m | (no m≮n)rewrite aux-lemma-m≮n,n≮m {m} {n} m≮n n≮m = auto

max-lemma-right : ∀ {m n : Nat} → max m n ≡ max m n - n + n
max-lemma-right {m} {n} with decBool (lessNat n m)
max-lemma-right {m} {n} | yes n<m = aux-lemma-m<n n<m
max-lemma-right {m} {n} | no n≮m with decBool (lessNat m n)
max-lemma-right {m} {n} | no n≮m | (yes m<n) = auto
max-lemma-right {m} {n} | no n≮m | (no m≮n)rewrite aux-lemma-m≮n,n≮m {m} {n} m≮n n≮m = auto

_⊕_ : ∃ STerm → ∃ STerm → ∃ STerm
_⊕_ (n₁ , τ₁) (n₂ , τ₂) = max n₁ n₂ , raiseSTerm (max n₁ n₂ - n₁) (max-lemma-left {n₁}) τ₁ fork raiseSTerm (max n₁ n₂ - n₂) (max-lemma-right {n₁}) τ₂

functionNameToSTerm : FunctionName → STerm 0
functionNameToSTerm ⟨ zero ⟩ = leaf
functionNameToSTerm ⟨ suc 𝑓 ⟩ = leaf fork functionNameToSTerm ⟨ 𝑓 ⟩

mutual

  termToSTerm : Term → ∃ STerm
  termToSTerm (variable x) = _ , i (fromℕ $ name x)
  termToSTerm (function 𝑓 τs) = (_ , functionNameToSTerm 𝑓) ⊕ termsToSTerm τs

  termsToSTerm : Terms → ∃ STerm
  termsToSTerm ⟨ ⟨ [] ⟩ ⟩ = 0 , leaf
  termsToSTerm ⟨ ⟨ τ ∷ τs ⟩ ⟩ = termToSTerm τ ⊕ termsToSTerm ⟨ ⟨ τs ⟩ ⟩

sTermToFunctionName : ∀ {n} → STerm n → Maybe FunctionName
sTermToFunctionName (i x) = nothing
sTermToFunctionName leaf = just ⟨ 0 ⟩
sTermToFunctionName (i x fork t₁) = nothing
sTermToFunctionName (leaf fork t₁) = sTermToFunctionName t₁ >>= (λ { ⟨ n ⟩ → just ⟨ suc n ⟩})
sTermToFunctionName ((t fork t₁) fork t₂) = nothing

mutual

  sTermToTerm : ∀ {n} → STerm n → Maybe Term
  sTermToTerm {n} (i x) = just $ variable ⟨ toℕ x ⟩
  sTermToTerm {n} leaf = just $ function ⟨ 0 ⟩ ⟨ ⟨ [] ⟩ ⟩
  sTermToTerm {n} (t₁ fork t₂) = sTermToFunctionName t₁ >>= λ 𝑓 → sTermToTerms t₂ >>= λ τs → just $ function 𝑓 τs

  sTermToTerms : ∀ {n} → STerm n → Maybe Terms
  sTermToTerms (i x) = nothing
  sTermToTerms leaf = just ⟨ ⟨ [] ⟩ ⟩
  sTermToTerms (x fork x₁) = sTermToTerm x >>= λ τ → sTermToTerms x₁ >>= λ τs → just ⟨ ⟨ τ ∷ vector (terms τs) ⟩ ⟩

term-round-trip : ∀ τ → sTermToTerm (snd $ termToSTerm τ) ≡ just τ
term-round-trip (variable ⟨ name₁ ⟩) = {!!}
term-round-trip (function x x₁) = {!!}

open import Relation.Binary.HeterogeneousEquality.Core as H
open import Data.Product
open import Data.Fin
open import Data.Sum
open import Data.Maybe.Base
open import Data.Empty

sTerm-round-trip : ∀ {n} → (t : STerm n) → (τ : Term) → just τ ≡ sTermToTerm t → snd (termToSTerm τ) H.≅ t
sTerm-round-trip (i x) (variable .(⟨ toℕ x ⟩)) refl = {!!}
sTerm-round-trip leaf (variable x) ()
sTerm-round-trip (i x fork t₁) (variable x₁) ()
sTerm-round-trip (t₁ fork t₂) (variable x) x₁ with sTermToFunctionName t₁ | sTermToTerms t₂
sTerm-round-trip (t₁ fork t₂) (variable x) () | nothing | ttt
sTerm-round-trip (t₁ fork t₂) (variable x₁) () | just x | nothing
sTerm-round-trip (t₁ fork t₂) (variable x₂) () | just x | (just x₁)
sTerm-round-trip t (function x x₁) x₂ = {!mgu-c!}

module Parameterized (Source : Nat → Set)
                     (Target : Nat → Set)
                     (let Sub : ∀ m n → Set
                          Sub m n = Source m → Target n)
 where

  _≐'_ : {m n : Nat} -> Sub m n → Sub m n -> Set
  f ≐' g = ∀ x -> f x ≡ g x

  Property' : (m : Nat) → Set₁
  Property' m = OscarPrelude.Σ (∀ {n} → (Sub m n) → Set) λ P → ∀ {m f g} -> f ≐' g -> P {m} f -> P g

{-
data AList : Set where
  anil : AList
  _asnoc_/_ : (σ : AList) (t' : Term) (x : VariableName) → AList

aListToSAList : AList → ∃
-}


text:
module _ where

open import Agda.Builtin.Unit
open import Imports.Issue5583 tt

_ : X
_ = it