text:
{-# OPTIONS --copatterns --sized-types --without-K #-}
module Poly where

open import Level using (Level)
open import Data.Product
open import Data.Nat
open import Data.Fin
open import Data.Unit
open import Data.Empty
open import Data.Vec hiding (_∈_; [_])
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Sum
open import Size

infixr 2 _and_

Fam : Set → Set₁
Fam I = I → Set

Fam₂ : Set → Set → Set₁
Fam₂ I J = I → J → Set

-- | Morphisms between families
MorFam : {I : Set} (P₁ P₂ : Fam I) → Set
MorFam {I} P₁ P₂ = (x : I) → P₁ x → P₂ x

_⇒_ = MorFam

compMorFam : {I : Set} {P₁ P₂ P₃ : Fam I} →
             MorFam P₁ P₂ → MorFam P₂ P₃ → MorFam P₁ P₃
compMorFam f₁ f₂ a = f₂ a ∘ f₁ a

_⊚_ = compMorFam

-- | Reindexing of families
_* : {I J : Set} → (I → J) → Fam J → Fam I
(u *) P = P ∘ u

-- | Reindexing on morphisms of families
_*₁ : {I J : Set} → (u : I → J) →
      {P₁ P₂ : Fam J} → (P₁ ⇒ P₂) → (u *) P₁ ⇒ (u *) P₂
(u *₁) f i = f (u i)

-- | This notation for Π-types is more useful for our purposes here.
Π : (A : Set) (P : Fam A) → Set
Π A P = (x : A) → P x

_and_ = _×_

-- | Fully general Σ-type, which we need to interpret the interpretation
-- of families of containers as functors for inductive types.
data Σ' {A B : Set} (f : A → B) (P : Fam A) : B → Set where
  ins : (a : A) → P a → Σ' f P (f a)

p₁' : {A B : Set} {u : A → B} {P : Fam A} {b : B} →
      Σ' u P b → A
p₁' (ins a _) = a

p₂' : {A B : Set} {u : A → B} {P : Fam A} {b : B} →
      (x : Σ' u P b) → P (p₁' x)
p₂' (ins _ x) = x

p₌' : {A B : Set} {u : A → B} {P : Fam A} {b : B} →
      (x : Σ' u P b) → u (p₁' x) ≡ b
p₌' (ins _ _) = refl

ins' : {A B : Set} {u : A → B} {P : Fam A} →
       (a : A) → (b : B) → u a ≡ b → P a → Σ' u P b
ins' a ._ refl x = ins a x

Σ'-eq : {A B : Set} {f : A → B} {P : Fam A} →
        (a a' : A) (x : P a) (x' : P a')
        (a≡a' : a ≡ a') (x≡x' : subst P a≡a' x ≡ x') →
        subst (Σ' f P) (cong f a≡a') (ins a x) ≡ ins a' x'
Σ'-eq a .a x .x refl refl = refl

Σ-eq : {a b : Level} {A : Set a} {B : A → Set b} →
       (a a' : A) (x : B a) (x' : B a')
       (a≡a' : a ≡ a') (x≡x' : subst B a≡a' x ≡ x') →
       (a , x) ≡ (a' , x')
Σ-eq a .a x .x refl refl = refl

×-eq : {ℓ : Level} {A : Set ℓ} {B : Set ℓ} →
       (a a' : A) (b b' : B) →
       a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
×-eq a .a b .b refl refl = refl

×-eqˡ : {A B : Set} {a a' : A} {b b' : B} → (a , b) ≡ (a' , b') → a ≡ a'
×-eqˡ refl = refl

×-eqʳ : {A B : Set} {a a' : A} {b b' : B} → (a , b) ≡ (a' , b') → b ≡ b'
×-eqʳ refl = refl

-- | Comprehension
⟪_⟫ : {I : Set} → Fam I → Set
⟪_⟫ {I} B = Σ I B

⟪_⟫² : {I J : Set} → (J → Fam I) → Fam J
⟪_⟫² {I} B j = Σ I (B j)

π : {I : Set} → (B : Fam I) → ⟪ B ⟫ → I
π B = proj₁

_⊢₁_ : {I : Set} {A : Fam I} → (i : I) → A i → ⟪ A ⟫
i ⊢₁ a = (i , a)

_,_⊢₂_ : {I : Set} {A : Fam I} {B : Fam ⟪ A ⟫} →
         (i : I) → (a : A i) → B (i , a) → ⟪ B ⟫
i , a ⊢₂ b = ((i , a) , b)

-- Not directly definable...
-- record Π' {A B : Set} (u : A → B) (P : A → Set) : B → Set where
--  field
--    app : (a : A) → Π' u P (u a) → P a

-- | ... but this does the job.
Π' : {I J : Set} (u : I → J) (P : Fam I) → Fam J
Π' {I} u P j = Π (∃ λ i → u i ≡ j) (λ { (i , _) → P i})

Π'' : {I J : Set} (u : I → J) (j : J) (P : Fam (∃ λ i → u i ≡ j)) → Set
Π'' {I} u j P = Π (∃ λ i → u i ≡ j) P

-- | Application for fully general Π-types.
app : {I J : Set} {u : I → J} {P : Fam I} →
      (u *) (Π' u P) ⇒ P
app i f = f (i , refl)

-- | Abstraction for fully general Π-types.
abs : {I J : Set} {u : I → J} {P : Fam I} →
      ((i : I) → P i) → ((j : J) → Π' u P j)
abs {u = u} f .(u i) (i , refl) = f i

-- | Abstraction for fully general Π-types.
abs' : {I J : Set} {u : I → J} {P : Fam I} {X : Fam J} →
      ((u *) X ⇒ P) → (X ⇒ Π' u P)
abs' {u = u} f .(u i) x (i , refl) = f i x

-- | Abstraction for fully general Π-types.
abs'' : {I J : Set} {u : I → J} {P : Fam I} →
        (j : J) → ((i : I) → u i ≡ j → P i) → Π' u P j
abs'' j f (i , p) = f i p

abs₃ : {I J : Set} {u : I → J} (j : J) {P : Fam (Σ I (λ i → u i ≡ j))} →
       ((i : I) → (p : u i ≡ j) → P (i , p)) → Π'' u j P
abs₃ j f (i , p) = f i p

-- | Functorial action of Π'
Π'₁ : {I J : Set} {u : I → J} {P Q : Fam I} →
        (f : P ⇒ Q) → (Π' u P ⇒ Π' u Q)
Π'₁ {u = u} f .(u i) g (i , refl) = f i (app i g)

-- | Turn morphism into a family
toFam : ∀ {A B : Set} → (h : B → A) → Fam A
toFam {A} {B} h a = Σ[ b ∈ B ] (h b ≡ a)

-- | Turn family into a morphism
fromFam : ∀ {A B : Set} → (X : Fam A) → (Σ A X → A)
fromFam {A} {B} X = proj₁

-- | Set comprehension
record ⟪_⟫' {A : Set} (φ : A → Set) : Set where
  constructor elem
  field
    a : A
    .isElem : φ a

inc : {A : Set} {φ : A → Set} → ⟪ φ ⟫' → A
inc (elem a isElem) = a

compr-syntax : (A : Set) (φ : A → Set) → Set
compr-syntax A = ⟪_⟫'

syntax compr-syntax A (λ x → φ) = ⟪ x ∈ A ∥ φ ⟫

compr-syntax' : {A : Set} (φ ψ : A → Set) → Set
compr-syntax' φ ψ = ⟪ (λ a → φ a and ψ a) ⟫'

syntax compr-syntax' φ (λ x → ψ) = ⟪ x ∈ φ ∥ ψ ⟫'

-- | Subsets of A
Sub : Set → Set₁
Sub A = Σ[ φ ∈ (A → Set) ] ⟪ φ ⟫'

_∈_ : {A : Set} → A → (φ : A → Set) → Set
x ∈ φ = φ x

_⊆_ : {A : Set} → (φ₁ φ₂ : A → Set) → Set
φ₁ ⊆ φ₂ = φ₁ ⇒ φ₂

_≅_ : {A : Set} → (φ₁ φ₂ : A → Set) → Set
φ₁ ≅ φ₂ = (φ₁ ⊆ φ₂) × (φ₂ ⊆ φ₁)

predToFam : {I A : Set} → (A → I) → (A → Set) → Fam I
predToFam {I} {A} h φ = Σ' h φ

-- | Dependent polynomials
record DPoly
  {I : Set} -- ^ Global index of constructed type
--  {N : Set}      -- ^ Index set for parameters
--  {J : N → Set}  -- ^ Index of each parameter
  {J : Set}
  : Set₁ where
  constructor dpoly
  field
    -- J ←t- E -p→ A -s→ I
    A : Set  -- ^ Labels
    s : A → I
    E : Set
    p : E → A
    t : E → J

-- | Interpretation of polynomial as functor
T : {I : Set} {J : Set} →
    DPoly {I} {J} →
    (X : Fam J) →  -- ^ Parameter
    (Fam I)
T {I} {N} (dpoly A s E p t) X =
  Σ' s     (λ a →
  Π' p (λ e →
    X (t e)
  ) a )

-- | Functorial action of T
T₁ : {I : Set} {J : Set} →
     (C : DPoly {I} {J}) →
     {X Y : J → Set} →
     (f : (j : J) → X j → Y j)
     (i : I) → T C X i → T C Y i
T₁ {I} {J} (dpoly A s E p t) {X} {Y} f .(s a) (ins a v) =
  ins a (Π'₁ ((t *₁) f) a v)

-- | Dependent, multivariate polynomials
record DMPoly
  {I : Set} -- ^ Global index of constructed type
  {N : Set}      -- ^ Index set for parameters
  {J : N → Set}  -- ^ Index of each parameter
  : Set₁ where
  constructor dpoly₁
  field
    -- J ←t- E -p→ A -s→ I
    A₁ : Set  -- ^ Labels
    s₁ : A₁ → I
    E₁ : N → Set
    p₁ : (n : N) → E₁ n → A₁
    t₁ : (n : N) → E₁ n → J n

-- | Create multiparameter polynomial
paramPoly : {I : Set} {N : Set} {J : N → Set} →
            DMPoly {I} {N} {J} →
            DPoly {I} {Σ N J}
paramPoly {I} {N} (dpoly₁ A₁ s₁ E₁ p₁ t₁) =
  dpoly
    A₁
    s₁
    ⟪ E₁ ⟫
    (λ {(n , e) → p₁ n e})
    (λ {(n , e) → (n , t₁ n e)})

-- | Functor on product category for multivariate polynomials.
TM : {I : Set} {N : Set} {J : N → Set} →
     DMPoly {I} {N} {J} →
     (X : (n : N) → J n → Set) →
     (I → Set)
TM P X = T (paramPoly P) (λ {(n , j) → X n j})

{-
----- Example: Vectors seen fixed point of (A, X) ↦ Σ z ⊤ + Σ s (A × X)
------   in the second variable. Here, z is the zero map, s the successor and
------   A is implicitely weakend.

Vec-Cons = Fin 2

Vec-Loc-Ind : Vec-Cons → Set
Vec-Loc-Ind zero    = ⊤
Vec-Loc-Ind (suc x) = ℕ

Vars : Set
Vars = Fin 2

Var-Types : Vars → Set
Var-Types zero    = ⊤
Var-Types (suc m) = ℕ

C : DPoly {ℕ} {Vars} {Var-Types}
C = dpoly ⟪ Vec-Loc-Ind ⟫ f Dom pp g
  where
    f : ⟪ Vec-Loc-Ind ⟫ → ℕ
    f (zero  , tt) = 0
    f (suc _ , k) = suc k

    -- | Domain exponents
    Dom' : Vars → Fam Vec-Cons
    Dom' _    zero = ⊥
    Dom' _    (suc _) = ℕ

    Dom : Vars → Set
    Dom zero = ⟪ Dom' zero ⟫
    Dom (suc n) = ⟪ Dom' (suc n) ⟫

    pp : (n : Vars) → Dom n → ⟪ Vec-Loc-Ind ⟫
    pp zero    (zero , ())
    pp (suc n) (zero , ())
    pp zero    (suc c , k) = suc c ⊢₁ k
    pp (suc n) (suc c , k) = suc c ⊢₁ k

    Params : Vars → ⟪ Vec-Loc-Ind ⟫ → Set
    Params x       (zero    , _) = ⊥
    Params zero    ((suc a) , k) = ⊤
    Params (suc x) ((suc a) , k) = ⊤

    g : (n : Vars) → Dom n → Var-Types n
    g zero    (zero , ())
    g (suc n) (zero , ())
    g zero    (suc c , k) = tt
    g (suc n) (suc c , k) = k

F : ((m : Vars) → Var-Types m → Set) → (ℕ → Set)
F = T C

-- Fix the variables, so that we can apply F.
Fix-Vars : Set → (ℕ → Set) → (p : Vars) → Var-Types p → Set
Fix-Vars A _ zero    _ = A
Fix-Vars A X (suc n)   = X

-- | Algebra structure on vectors, using the functor F.
in-vec : ∀ {A} → (n : ℕ) → F (Fix-Vars A (Vec A)) n → Vec A n
in-vec {A} .0       (ins (zero    , tt) _) = []
in-vec {A} .(suc k) (ins ((suc i) , k)  v) = a ∷ x
  where
    a : A
    a = app (suc i ⊢₁ k) (v zero)

    x : Vec A k
    x = app (suc i ⊢₁ k) (v (suc zero))

-- | Recursion for F-algebras
rec-vec : {A : Set} {X : ℕ → Set} →
          ((n : ℕ) → F (Fix-Vars A X) n → X n) →
          (n : ℕ) → Vec A n → X n
rec-vec {A} {X} u .0 [] = u 0 (ins (zero ⊢₁ tt) v₀)
  where
    v₀ : Π Vars (λ n → Π' (p C n) (λ e → Fix-Vars A X n (t C n e)) (zero ⊢₁ tt))
    v₀ zero = abs'' (zero ⊢₁ tt) q₀
      where
        q₀ : (i : E C zero) → p C zero i ≡ zero ⊢₁ tt → A
        q₀ (zero  , ()) p
        q₀ (suc d , _) ()
    v₀ (suc n) = abs'' (zero ⊢₁ tt) q₁
      where
        q₁ : (d : E C (suc n)) → p C (suc n) d ≡ zero ⊢₁ tt → X (t C (suc n) d)
        q₁ (zero  , ()) p
        q₁ (suc d , _) ()

rec-vec {A} {X} f (suc k) (a ∷ x) = f (suc k) (ins (suc zero ⊢₁ k) v')
  where
    v' : Π Vars     (λ n →
         Π' (p C n) (λ e →
         Fix-Vars A X n (t C n e)) (suc zero ⊢₁ k))
    v' zero = abs'' (suc zero ⊢₁ k) q₀
      where
        q₀ : (d : E C zero) → p C zero d ≡ suc zero ⊢₁ k → A
        q₀ d p = a
    v' (suc n) = abs'' (suc zero ⊢₁ k) q₁
      where
        q₁ : (d : E C (suc n)) →
             p C (suc n) d ≡ suc zero ⊢₁ k → X (t C (suc n) d)
        q₁ (zero  , ()) p
        q₁ (suc .zero , .k) refl = rec-vec f k x

--- Example 2: Partial streams

record ℕ∞ : Set where
  coinductive
  field
    pred∞ : ⊤ ⊎ ℕ∞
open ℕ∞

suc∞ : ℕ∞ → ℕ∞
pred∞ (suc∞ n) = inj₂ n

PS-Vars : Set
PS-Vars = Fin 2

PS-Types : PS-Vars → Set
PS-Types zero = ⊤
PS-Types (suc n) = ℕ∞

PS-C : DPoly {ℕ∞} {PS-Vars} {PS-Types}
PS-C = dpoly ℕ∞ id Codom codom-dep var-reidx
  where
    Codom : PS-Vars → Set
    Codom _ = ℕ∞

    codom-dep : (n : PS-Vars) → Codom n → ℕ∞
    codom-dep _ = suc∞

    var-reidx : (n : PS-Vars) → Codom n → PS-Types n
    var-reidx zero _ = tt
    var-reidx (suc v) = id

PS-F : ((m : PS-Vars) → PS-Types m → Set) → (ℕ∞ → Set)
PS-F = T PS-C

-- Fix the variables, so that we can apply F.
PS-Fix-Vars : Set → Fam ℕ∞ → (p : PS-Vars) → Fam (PS-Types p)
PS-Fix-Vars A _ zero    _ = A
PS-Fix-Vars A X (suc n)   = X

record PStr {i : Size} (A : Set) (n : ℕ∞) : Set where
  coinductive
  field
    out : ∀ {j : Size< i} → PS-F (PS-Fix-Vars A (PStr {j} A)) n
open PStr

P-hd : ∀ {A} {n : ℕ∞} → PStr A (suc∞ n) → A
P-hd {A} {n} s = q (out s)
  where
    q : PS-F (PS-Fix-Vars A (PStr A)) (suc∞ n) → A
    q (ins .(suc∞ n) v) = app n (v zero)

P-tl : ∀ {A} {n : ℕ∞} → PStr A (suc∞ n) → PStr A n
P-tl {A} {n} s = q (out s)
  where
    q : PS-F (PS-Fix-Vars A (PStr A)) (suc∞ n) → PStr A n
    q (ins .(suc∞ n) v) = app n (v (suc zero))

P-corec : {A : Set} {X : Fam ℕ∞} →
          (c : X ⇒ PS-F (PS-Fix-Vars A X)) →
          (∀{i} → X ⇒ PStr {i} A)
out (P-corec {A} {X} c n x) {j} = ins n (h n x)
  where
    h : (n : ℕ∞) → X n →
        Π PS-Vars     (λ v →
        Π' (p PS-C v) (λ e →
        PS-Fix-Vars A (PStr {j} A) v (t PS-C v e)) n)
    h n x zero  = abs'' n (q n x)
      where
        q : (n : ℕ∞) → (X n) → (d : E PS-C zero) → p PS-C zero d ≡ n → A
        q .(suc∞ n) x n refl = r (c (suc∞ n) x)
          where
            r : PS-F (PS-Fix-Vars A X) (suc∞ n) → A
            r (ins .(suc∞ n) ch) = app n (ch zero)

    h n x (suc v) = abs'' n (q n x)
      where
        q : (n : ℕ∞) → (X n) →
            (i : E PS-C (suc v)) →
            p PS-C (suc v) i ≡ n →
            PStr {j} A (t PS-C (suc v) i)
        q .(suc∞ k) x k refl = P-corec c k (r (c (suc∞ k) x))
          where
            r : PS-F (PS-Fix-Vars A X) (suc∞ k) → X k
            r (ins .(suc∞ k) ch) = app k (ch (suc zero))

------- End examples --------

-}

-- | Non-dependent polynomials in one variable
record Poly : Set₁ where
  constructor poly
  field
    Sym : Set
    Arit : Set
    f : Arit → Sym
open Poly

-- | Interpretation as functors
⟦_⟧ : Poly → Set → Set
⟦ poly A B f ⟧ X = Σ A ((Π' f) (λ e → X))

⟦_⟧₁ : {P : Poly} {A B : Set} → (A → B) → (⟦ P ⟧ A → ⟦ P ⟧ B)
⟦_⟧₁ {poly Sym Arit f} {A} {B} f₁ (a , v) = (a , abs'' a (v' a v))
  where
    v' : (a' : Sym) (v' : Π' f (λ e → A) a') (b : Arit) → f b ≡ a' → B
    v' ._ v' b refl = f₁ (app b v')

-- | Lifting to predicates
⟦_⟧' : (p : Poly) → ∀ {X} → Fam X → Fam (⟦ p ⟧ X)
⟦ poly A B f ⟧' P (s , α) = ∀ (x : toFam f s) → P (α x)

-- | Lifting to relations
⟦_⟧'' : (p : Poly) → ∀ {X Y} → Fam₂ X Y → Fam₂ (⟦ p ⟧ X) (⟦ p ⟧ Y)
⟦ poly A B f ⟧'' P (s₁ , α₁) (s₂ , α₂) =
  Σ[ e ∈ (s₁ ≡ s₂) ] (∀ (x : toFam f s₁) →
    P (α₁ x) (α₂ (proj₁ x , trans (proj₂ x) e)))

eq-preserving : ∀ {p X} (x y : ⟦ p ⟧ X) → x ≡ y → ⟦ p ⟧'' _≡_ x y
eq-preserving {p} x .x refl = refl , q
  where
    lem : ∀ {X : Set} {x y : X} (e : x ≡ y) → trans e refl ≡ e
    lem refl = refl

    q : (z : toFam (f p) (proj₁ x)) →
        proj₂ x z ≡ proj₂ x (proj₁ z , trans (proj₂ z) refl)
    q (s , e) = cong (λ u → proj₂ x (s , u)) (sym (lem e))

-- | Final coalgebras for non-dependent polynomials
record M {i : Size} (P : Poly) : Set where
  coinductive
  field
    ξ : ∀ {j : Size< i} → ⟦ P ⟧ (M {j} P)
open M

ξ'  : ∀ {P} → M P → ⟦ P ⟧ (M P)
ξ' x = ξ x

mutual
  -- | Equality for M types is given by bisimilarity
  record _~_ {P : Poly} (x y : M P) : Set where
    coinductive
    field
      ~pr : ⟦ P ⟧'' _~_ (ξ' x) (ξ' y)
open _~_ public

IsBisim : ∀{p X Y} → (X → ⟦ p ⟧ X) → (Y → ⟦ p ⟧ Y) → Fam₂ X Y → Set
IsBisim {p} f g _R_ = ∀ x y → x R y → ⟦ p ⟧'' _R_ (f x) (g y)

root : ∀ {P} → M P → Sym P
root = proj₁ ∘ ξ'

corec-M : ∀ {P : Poly} {X : Set} → (X → ⟦ P ⟧ X) → (∀{i} → X → M {i} P)
ξ (corec-M {poly Sym Arit f} {X} c x) {j} = (c₁ , abs'' c₁ (v x))
  where
    c₁ = proj₁ (c x)

    v : (x : X) (b : Arit) → f b ≡ proj₁ (c x) → M {j} (poly Sym Arit f)
    v x b p = corec-M c (proj₂ (c x) (b , p))

Bisim→~ : ∀{p X Y} {f : X → ⟦ p ⟧ X} {g : Y → ⟦ p ⟧ Y} {_R_} →
          IsBisim f g _R_ → ∀ x y → x R y → corec-M f x ~ corec-M g y
~pr (Bisim→~ isBisim x y xRy) with isBisim x y xRy
~pr (Bisim→~ {p} {X} {Y} {f} {g} isBisim x y xRy) | (e , β) =
  (e , (λ z →
    Bisim→~ isBisim
            (proj₂ (f x) z)
            (proj₂ (g y) (proj₁ z , trans (proj₂ z) e))
            (β z)))

{-
corec-M-hom : {P : Poly} {X : Set}
              (c : X → ⟦ P ⟧ X) →
              (x : X) → ξ' (corec-M c x) R~ ⟦ corec-M c ⟧₁ (c x)
sym≡  (corec-M-hom c x) = refl
arit~ (corec-M-hom {poly A B f} {X} c x) =
  abs₃ (proj₁ (c x)) {!!} -- (pr x (c x) refl refl)
  where
    P = poly A B f

    pr : (x : X)
         (x' : ⟦ P ⟧ X)
         (p₀ : x' ≡ c x)
         (p : proj₁ (ξ' (corec-M c x)) ≡ proj₁ (⟦ corec-M c ⟧₁ x'))
         (b : B)
         (p₁ : f b ≡ proj₁ (ξ' (corec-M c x))) →
--         (p₁ : f b ≡ proj₁ x') →
         arit~-pr (ξ' (corec-M c x)) (⟦ corec-M c ⟧₁ x') p (b , p₁)
    pr x₁ (._ , ._) refl p₁ b p₂ = {!!}
-}

record PolyHom (P₁ P₂ : Poly) : Set where
  constructor polyHom
  field
    SymMor : Sym P₁ → Sym P₂
    AritMor : (SymMor *) (toFam (f P₂)) ⇒ toFam (f P₁)

coalg : {P₁ P₂ : Poly} →
        PolyHom P₁ P₂ →
        (∀ X → ⟦ P₁ ⟧ X → ⟦ P₂ ⟧ X)
coalg {poly Sym₁ Arit₁ f₁} {poly Sym₂ Arit₂ f₂} (polyHom α β) X (a , v)
  = (α a , abs'' (α a) (v' a v))
    where
      v' : (a : Sym₁) (v :  Π' f₁ (λ e → X) a) (b : Arit₂) → f₂ b ≡ α a → X
      v' a v b p = v (β a (b , p))

-- | Functoriality
M₁ : ∀ {P₁ P₂} → PolyHom P₁ P₂ → M P₁ → M P₂
M₁ {P₁} h = corec-M (coalg h (M P₁) ∘ ξ')

-- | Product of maps
_⊗_ : {A B C D : Set} → (A → B) → (C → D) → (A × C → B × D)
(f ⊗ g) x = ((f (proj₁ x)) , (g (proj₂ x)))

⊗-eq : {A B C : Set} {f : A → C} {g : B → C}
       (a : A) (b : B) (p : f a ≡ g b)→
       (f ⊗ g) (a , b) ≡ (g b , g b)
⊗-eq {f = f} {g} a b p = ×-eq (f a) (g b) (g b) (g b) p refl

-- | Extend polynomial by index
I-poly : Poly → Set → Poly
I-poly P I = poly (Sym P × I) (Arit P × I) (f P ⊗ id)

_⋊_ = I-poly

{-
-- | Projects away the I from M (P × I)
u₁ : ∀ {i} → (P : Poly) (I : Set) → M (I-poly I P) → M {i} P
ξ (u₁ P I x) {j} = q (ξ x)
  where
    q : R (I-poly I P) (M (I-poly I P)) → ⟦ P ⟧ (M {j} P)
    q (s , v) = (proj₁ s , abs'' (proj₁ s) (r (s , v)))
      where
        r : (u : R (I-poly I P) (M (I-poly I P))) (a : Arit P) →
            f P a ≡ proj₁ (proj₁ u) → M {j} P
        r ((.(f P a) , i) , v) a refl = u₁ P I (app (a , i) v)
-}

-- | Forget changes of dependencies of a polynomial in one variable.
simple : {I : Set} → DPoly {I} {I} → Poly
simple C = poly (DPoly.A C) (DPoly.E C) (DPoly.p C)

↓_ = simple

module MTypes {I : Set} (C : DPoly {I} {I}) where
  open DPoly C
  P = ↓ C

  idx : M P → I
  idx = s ∘ root

  inj : (X : I → Set) → ⟪ T C X ⟫ → ⟦ ↓ C ⟧ ⟪ X ⟫
  inj X (.(s a) , (ins a v)) = (a , abs'' a (u a v))
    where
      u : (a' : A)
          (v' : Π' p (λ e → X (t e)) a')
          (b : E) →
          f (↓ C) b ≡ a' →
          ⟪ X ⟫
      u ._ v' b refl = (t b , app b v')

  -- | Applies r corecursively, thus essentially constructs an element of
  -- M (P × I) where the second component is given by r.
  u₁ : M P → M (P ⋊ I)
  u₁ = M₁ (polyHom α β)
    where
      α : Sym (↓ C) → Sym ((↓ C) ⋊ I)
      α = < id , s >

      β : (α *) (toFam (f P ⊗ id)) ⇒ toFam p
      β ._ ((b , ._) , refl) = (b , refl)

  K : ⟦ P ⋊ I ⟧ (M (P ⋊ I)) → ⟦ P ⋊ I ⟧ (M (P ⋊ I) × E)
  K (a , v) = (a , abs'' a (v' a v))
    where
      v' : (a : Sym (P ⋊ I))
           (v : Π' (f (P ⋊ I)) (λ e → M (P ⋊ I)) a)
           (bi : Arit (P ⋊ I)) →
           f (P ⋊ I) bi ≡ a →
           M (P ⋊ I) × E
      v' ._ v₁ bi refl = (v₁ (bi , refl) , proj₁ bi)

  φ : M (P ⋊ I) × Arit P → M (P ⋊ I)
  φ = corec-M c
    where
      h : ⟦ P ⋊ I ⟧ (M (P ⋊ I)) × Arit P → ⟦ P ⋊ I ⟧ (M (P ⋊ I) × Arit P)
      h (((a , i) , v) , b) =
        ((a , t b) ,
          abs'' (a , t b) (v' (a , t b) b v))
        where
          v' : (ai' : Sym (P ⋊ I))
               (b : Arit P)
               (v :  Π' (f (P ⋊ I)) (λ _ →
                     M (P ⋊ I)) (proj₁ ai' , i))
               (i : Arit (P ⋊ I)) →
               f (P ⋊ I) i ≡ ai' →
               M (P ⋊ I) × Arit P
          v' ._ b v₁ (b₁ , _) refl = (app (b₁ , i) v₁ , b)

      c :  M (P ⋊ I) × Arit P →
           ⟦ P ⋊ I ⟧ (M (P ⋊ I) × Arit P)
      c = h ∘ (ξ' ⊗ id)

  ψ : M (P ⋊ I) → M (P ⋊ I)
  ψ = corec-M c
    where
      c : M (P ⋊ I) → ⟦ P ⋊ I ⟧ (M (P ⋊ I))
      c = ⟦ φ ⟧₁ ∘ K ∘ ξ'

  u₂ : M P → M (P ⋊ I)
  u₂ = ψ ∘ u₁

{-
{-
-- | Same as u₂???
u₂' : ∀ {I} (C : DPoly {I}) →
      M (↓ C) → M (↓ C ⋊ I)
u₂' {I} C x = M₁ (polyHom α β) x
  where
    α : Sym (↓ C) → Sym ((↓ C) ⋊ I)
    α a = (a , t C {!!}) -- (root x)) -- (s C (root x)))

    β : (α *) (toFam (f (↓ C) ⊗ id)) ⇒ toFam (p C tt)
    β ._ ((a , ._) , refl) = (a , refl)

φ : {I : Set} (C : DPoly {I}) {i : Size} →
    M {i} (↓ C ⋊ I) × Arit (↓ C) → M {i} (↓ C ⋊ I)
ξ (φ {I} C (x , b)) {j} = q (ξ x)
  where
    m : ⟦ ↓ C ⋊ I ⟧ (M {j} (↓ C ⋊ I)) → Sym (↓ C ⋊ I)
    m ((a , i) , v) = (a , (t C b))

    q : ⟦ ↓ C ⋊ I ⟧ (M {j} (↓ C ⋊ I)) →
        ⟦ ↓ C ⋊ I ⟧ (M {j} (↓ C ⋊ I))
    q u = (m u , abs'' (m u) (v' u))
      where
        v' : (u : ⟦ ↓ C ⋊ I ⟧ (M {j} (↓ C ⋊ I)))
             (b : Arit (↓ C ⋊ I)) →
             f (↓ C ⋊ I) b ≡ m u →
             M {j} (↓ C ⋊ I)
        v' ((._ , i) , v) (b , ._) refl = φ C ((app (b , i) v) , b)

ψ : {I : Set} (C : DPoly {I}) {i : Size} →
    M {i} (↓ C ⋊ I) → M {i} (↓ C ⋊ I)
ξ (ψ {I} C x) {j} = q (ξ x)
  where
    q : ⟦ ↓ C ⋊ I ⟧ (M {j} (↓ C ⋊ I)) →
        ⟦ ↓ C ⋊ I ⟧ (M {j} (↓ C ⋊ I))
    q (a , v) = (a , abs'' a (v' (a , v)))
      where
        v' : (u' : ⟦ ↓ C ⋊ I ⟧ (M {j} (↓ C ⋊ I)))
             (a' : Arit (↓ C ⋊ I)) →
             f (↓ C ⋊ I) a' ≡ proj₁ u' →
             M {j} (↓ C ⋊ I)
        v' (._ , v) a' refl = φ C (app a' v , proj₁ a')

u₂ : ∀ {i} {I} (C : DPoly {I}) →
     M (↓ C) → M {i} (↓ C ⋊ I)
u₂ C = ψ C ∘ u₁ C
-}

  Vφ : (i : I) → (M P → Set)
  Vφ i x = (s (root x) ≡ i) × (u₁ x ≡ u₂ x)

--V' : {I : Set} (C : DPoly {I} {I}) → Fam I
--V' C = ⟪ Vφ C ⟫²

{-
lem₂ : {I : Set} {C : DPoly {I} {I}} →
       (x : M (↓ C))
       (b : E C)
       (v : Π' (p C) (λ e → M (↓ C)) (p C b)) →
       ξ' x ≡ (_ , v) →
       u₁ C x ≡ u₂ C x →
       u₁ C (app b v) ≡ u₂ C (app b v)
lem₂ {I} {C} x b v pr≡ u₁≡u₂ = {!!}
  where
    w : (x : ⟦ ↓ C ⟧ (M (↓ C)))
        (b : E C)
        (v : Π' (p C) (λ e → M (↓ C)) (p C b)) →
        x ≡ (_ , v) →
        u₁ C (app b v) ≡ u₂ C (app b v)
    w ._ b v refl = {!!}

--    bar : ξ' (u₁ C x) ≡ ⟦ ↓ C ⟧₁ u₁ (M₁

lem₁ : {I : Set} {C : DPoly {I} {I}} →
       (x : M (↓ C))
       (b : E C)
       (v : Π' (p C) (λ e → M (↓ C)) (p C b)) →
       ξ' x ≡ (_ , v) →
       u₁ C x ≡ u₂ C x →
       s C (root (app b v)) ≡ t C b
lem₁ x b v pr≡ u₁≡u₂ = {!!}

{-
ξV  : ∀ {I} {C : DPoly {I} {I}} →
      V' C ⇒ T C (V' C)
ξV {C = dpoly A s E p t} .(s (proj₁ (ξ x))) (x , refl , u₁≡u₂)
  = ins (root x) (abs'' (root x) (v' (root x) (proj₂ (ξ' x)) refl))
  where
    C = dpoly A s E p t

    v' : (a : A)
         (v : Π' p (λ e → M (↓ C)) a)
         (q : ξ' x ≡ (a , v))
         (b : E) →
         p b ≡ a →
         Σ (M (↓ C)) (Vφ C (t b))
    v' .(p b) v q b refl =
      (app b v
      , lem₁ x b v q u₁≡u₂
      , (lem₂ x b v q u₁≡u₂))
-}

-}

  V' : M P → Set
  V' x = u₁ x ≡ u₂ x

  Φ : (M P → Set) → (M P → Set)
  Φ U x =
    let (a , v) = ξ' x
    in Π'' (f P) a (λ {(b , pr) →
       Σ[ y ∈ M P ] (
         U y and
         idx y ≡ t b and
         q b (a , v) pr y ) })
    where
      q : (b : E) (u : ⟦ P ⟧ (M P)) → f P b ≡ proj₁ u → M P → Set
      q b (._ , v) refl y = app b v ≡ y

{-
      q : (b : E) (u : ⟦ P ⟧ (M P)) → f P b ≡ proj₁ u →
          (j : I) → U' j → Set
      q b (._ , v) refl .(idx y) (ins y z) = app b v ≡ y
-}

{-
  V'-postFP : V' ⊆ Φ V'
  V'-postFP x x∈V' (b , fb≡ξx₁) = (r b (ξ' x) fb≡ξx₁ , {!!})
    where
      r : (b₁ : E) (u : ⟦ P ⟧ (M P)) →
          f P b₁ ≡ proj₁ u →
          predToFam idx V' (t b₁)
      r b₁ (._ , v) refl = r' b₁ (app b₁ v)
        where
          r' : (b₂ : E) (x' : M P) → predToFam idx V' (t b₂)
          r' b₂ x' = ins ? {!!}
-}
  V'-final : (U : M P → Set) → U ⊆ Φ U → U ⊆ V'
  V'-final = {!!}

  -- | This predicate on M (↓ C) ensures that we can define a map
  -- V → s a ≡ ⟦ ↓ C ⟧ (i × (t *) V.
  record V-pred (i : I) (x : M P) : Set where
    coinductive
    field
      -- | For ξ x = (a , v), we require s a = i
      sigma-idx : s (proj₁ (ξ x)) ≡ i
      -- | For ξ x = (a , v), we require ∀ b with p b = a that
      -- idx (v b) = s a and v b ∈ V (t b)
      reidx : Π'' (f P) (proj₁ (ξ x))
              (λ {(e , eq) → idx ((proj₂ (ξ x)) (e , eq)) ≡ t e
                             × V-pred (t e) ((proj₂ (ξ x)) (e , eq)) })
  open V-pred

{-
V : {I : Set} (C : DPoly {I} {I}) → Fam I
V C i = Σ (M (↓ C)) (V-pred C i)

Σ≡₁ : {I : Set} {A : Fam I} → {x y : Σ I A} → x ≡ y → proj₁ x ≡ proj₁ y
Σ≡₁ {x = i , a} {.i , .a} refl = refl

foofoo : {I : Set} {A : Fam I} → (x y : Σ I A) →
         (p : x ≡ y) → A (proj₁ y)
foofoo x .x refl = proj₂ x

Σ≡₂ : {I : Set} {A : Fam I} → {x y : Σ I A} →
        (p : x ≡ y) → foofoo x y p ≡ proj₂ y
Σ≡₂ {x = i , a} {.i , .a} refl = refl

out-V : {I : Set} {C : DPoly {I} {I}} →
        V C ⇒ T C (V C)
out-V {I} {C = dpoly A s E p t} i (x , v-proof)
  = foo i v-proof (sigma-idx v-proof)
  where
    P : DPoly
    P = dpoly A s E p t

    u : ⟦ ↓ P ⟧ (M (↓ P))
    u = ξ x

--    uaie : (u' : ⟦ ↓ P ⟧ (M (↓ P))) → f (↓ P) e ≡ proj₁ u' → A → Set
--    uaie u' pr = Π' (p tt) (λ e → V-pred P (t e) ((proj₂ u') (e , {!!})))

    foo : (i' : I) → V-pred P i' x → s (proj₁ u) ≡ i' → T P (V P) i'
    foo .(s (proj₁ u)) pr refl =
      ins (proj₁ u) (v'' u refl)
      where
        v'' : (u' : ⟦ ↓ P ⟧ (M (↓ P))) →
              u' ≡ ξ x →
              Π' p (λ e → V P (t e)) (proj₁ u')
        v'' (.(p e) , v) u'=ξx (e , refl) = (x' , {!!}) -- bar x {!v!} {!!} {!!} pr)
          where
            x' : M (↓ P)
            x' = v (e , refl)

            aiu = proj₂ (reidx pr (e , {!!}))

            bar : (x' : M (↓ P))
                  (v₁ : Π' (f (↓ P)) (λ e₁ → M (↓ P)) (proj₁ (ξ x'))) →
                  v₁ ≡ proj₂ (ξ x') →
                  (q : f (↓ P) e ≡ proj₁ (ξ x')) →
                  V-pred P (s (proj₁ (ξ x'))) x' → V-pred P (t e) (v₁ (e , q))
            bar x'' .(proj₂ (ξ x'')) refl q pr' = proj₂ (reidx pr' (e , q))

            tu : s (root (proj₂ (ξ x) (e , Σ≡₁ u'=ξx))) ≡ t e
            tu = proj₁ (reidx pr (e , Σ≡₁ u'=ξx))

{-
            bar : (v₁ : Π' (f (↓ P)) (λ e₁ → M (↓ P)) (proj₁ (ξ x))) →
                  v₁ ≡ proj₂ (ξ x) →
                  V-pred P (t e) x'
            bar ._ refl = proj₂ (reidx pr ?)
-}
            tiu : V-pred P (t e) (proj₂ (ξ x) (e , Σ≡₁ u'=ξx))
            tiu = proj₂ (reidx pr (e , Σ≡₁ u'=ξx))

-- Want out-s : M (↓ C ⋊ I) → T C (M {i} (↓ C ⋊ I))

T' : {I : Set} →
     DPoly {I} {I} →
     (X : I → Set) →  -- ^ Parameter
     (I → Set)
T' C X = T C {!!}

{-
out-s' : ∀ {i} {I} {C : DPoly {I}} →
         M (↓ C ⋊ I) → T' C (M {i} (↓ C ⋊ I))
out-s' = ?
-}

-- | Candidate for R C
out-s : ∀ {i} {I} {C : DPoly {I}} →
        M (↓ C ⋊ I) → ⟦ ↓ C ⟧ (M {i} (↓ C ⋊ I))
out-s {i} {I} {C} x = (q (ξ x) , abs'' (q (ξ x)) (h (ξ x)))
  where
    q : ⟦ ↓ C ⋊ I ⟧ (M {i} (↓ C ⋊ I)) → Sym (↓ C)
    q (a , _) = proj₁ a

    h : (u : ⟦ ↓ C ⋊ I ⟧ (M {i} (↓ C ⋊ I)))
        (a : Arit (↓ C)) →
        f (↓ C) a ≡ q u → M {i} (↓ C ⋊ I)
    h ((._ , b) , v') a refl = app (a , b) v'
-}
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An abstraction of various forms of recursion/induction
------------------------------------------------------------------------

-- The idea underlying Induction.* comes from Epigram 1, see Section 4
-- of "The view from the left" by McBride and McKinna.

-- Note: The types in this module can perhaps be easier to understand
-- if they are normalised. Note also that Agda can do the
-- normalisation for you.

module Induction where

open import Level
open import Relation.Unary

-- A RecStruct describes the allowed structure of recursion. The
-- examples in Induction.Nat should explain what this is all about.

RecStruct : ∀ {a} → Set a → (ℓ₁ ℓ₂ : Level) → Set _
RecStruct A ℓ₁ ℓ₂ = Pred A ℓ₁ → Pred A ℓ₂

-- A recursor builder constructs an instance of a recursion structure
-- for a given input.

RecursorBuilder : ∀ {a ℓ₁ ℓ₂} {A : Set a} → RecStruct A ℓ₁ ℓ₂ → Set _
RecursorBuilder Rec = ∀ P → Rec P ⊆′ P → Universal (Rec P)

-- A recursor can be used to actually compute/prove something useful.

Recursor : ∀ {a ℓ₁ ℓ₂} {A : Set a} → RecStruct A ℓ₁ ℓ₂ → Set _
Recursor Rec = ∀ P → Rec P ⊆′ P → Universal P

-- And recursors can be constructed from recursor builders.

build : ∀ {a ℓ₁ ℓ₂} {A : Set a} {Rec : RecStruct A ℓ₁ ℓ₂} →
        RecursorBuilder Rec →
        Recursor Rec
build builder P f x = f x (builder P f x)

-- We can repeat the exercise above for subsets of the type we are
-- recursing over.

SubsetRecursorBuilder : ∀ {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} →
                        Pred A ℓ₁ → RecStruct A ℓ₂ ℓ₃ → Set _
SubsetRecursorBuilder Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ Rec P

SubsetRecursor : ∀ {a ℓ₁ ℓ₂ ℓ₃} {A : Set a} →
                 Pred A ℓ₁ → RecStruct A ℓ₂ ℓ₃ → Set _
SubsetRecursor Q Rec = ∀ P → Rec P ⊆′ P → Q ⊆′ P

subsetBuild : ∀ {a ℓ₁ ℓ₂ ℓ₃}
                {A : Set a} {Q : Pred A ℓ₁} {Rec : RecStruct A ℓ₂ ℓ₃} →
              SubsetRecursorBuilder Q Rec →
              SubsetRecursor Q Rec
subsetBuild builder P f x q = f x (builder P f x q)

ext: agda


text:
-- {-# OPTIONS -v tc.constr.add:45 #-}

module _ where

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

==_] : ∀ {a} {A : Set a} (x : A) → x ≡ x
== x ] = refl

[ : ∀ {a} {A : Set a} (x : A) {y : A} → x ≡ y → A
[ x refl = x

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

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

infixr 5 _∷[_]_
pattern _∷[_]_ x n xs = _∷_ {n} x xs

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

  id : A → A
  id x = x

  len : ∀ {n} → Vec A n → Nat
  len {n} _ = n

  module _ {b} {B : Set b} where

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

    const : A → B → A
    const x _ = x

    _!>_ : A → B → B
    _ !> x = x

module SomeParameters {a} (n : Nat) (A : Set a) (xs : Vec A n) (ys : Vec A (n * 2)) where

  simpleRefine : Vec A n → Nat
  simpleRefine []            = [ n == 0 ]
  simpleRefine (x ∷[ m ] xs) = [ n == suc m ]

  moreComplex : Vec A n → Nat
  moreComplex [] = 0
  moreComplex (z ∷ zs) with map id xs
  moreComplex (z ∷ zs) | x ∷ [] = [ n == 1 ] + [ 2 == len ys ]
  moreComplex (z ∷ zs) | x ∷ x₁ ∷[ k ] xs′ with [ n == 2 + k ] !> map id zs
  moreComplex (z ∷ zs) | x ∷ x₁ ∷ xs′ | z₁ ∷ [] = [ n == 2 ]
  moreComplex (z ∷ zs) | x ∷ x₁ ∷ xs′ | z₁ ∷ z₂ ∷[ k ] zs′ =
    let n+_ = λ m → [ n == 3 + k ] + m
        n+k = n+ k
    in case [ n+k == 3 + k + k ] of λ i →
       let n+i = [ n == 3 + k ] + i in
       case map id zs′ of λ where
         []              → [ (n+ i) == 3 + i ] + [ n+k == 3 ] + [ n+i == 3 + i ]
         (z₃ ∷[ j ] zs″) →
           let _ = [ n      == 4 + j ]
               _ = [ k      == 1 + j ]
               _ = [ n+k    == 4 + j + (1 + j) ]
               _ = [ (n+ i) == 4 + j + i ]
           in
           [ (len xs′) == 2 + j ] +
           [ (len ys) == (4 + j) * 2 ]

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module FT-Fin where

import Data.Fin as F
import Data.Nat as N

open import FT
open import FT-Nat using (toℕ)

------------------------------------------------------------------
-- Finite Types and the natural numbers are intimately related.
--
toFin : (b : FT) → F.Fin (N.suc (toℕ b))
toFin b = F.fromℕ (toℕ b)

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Cats.Category.Cat.Facts where

open import Cats.Category.Cat.Facts.Initial public using (hasInitial)
open import Cats.Category.Cat.Facts.Terminal public using (hasTerminal)
open import Cats.Category.Cat.Facts.Product public using (hasBinaryProducts)
open import Cats.Category.Cat.Facts.Exponential public using (hasExponentials)

open import Cats.Category.Cat using (Cat)
open import Cats.Category.Constructions.Product using (HasFiniteProducts)
open import Cats.Category.Constructions.CCC using (IsCCC)

instance
  hasFiniteProducts : ∀ lo la l≈ → HasFiniteProducts (Cat lo la l≈)
  hasFiniteProducts _ _ _ = record {}

  isCCC : ∀ l → IsCCC (Cat l l l)
  isCCC _ = record {}

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:
open import Preliminaries

module Focusing where

  data Tp : Set where
    b : Tp
    _⇒'_ : Tp → Tp → Tp
    _×'_ : Tp → Tp → Tp

  Ctx = List Tp

  data _∈_ : Tp → Ctx → Set where
    i0 : ∀ {Γ τ} → τ ∈ τ :: Γ
    iS : ∀ {Γ τ τ1} → τ ∈ Γ → τ ∈ τ1 :: Γ

  -- datatype of focused proofs for negative fragment of intuitionistic logic
  data _,,_|-_ : Ctx → Maybe Tp → Tp → Set where

  -- focus and init

    focus : ∀ {Γ A P} →

          A ∈ Γ → Γ ,, (Some A) |- P
          -------------------------- focus
          → Γ ,, None |- P

    init : ∀ {Γ P} →

         ------------------ init
         Γ ,, (Some P) |- P

  -- synchronous rules

    arr-l : ∀ {Γ A B P} →

          Γ ,, None |- A → Γ ,, (Some B) |- P
          ----------------------------------- impl-left
          → Γ ,, (Some (A ⇒' B)) |- P

    conj-l1 : ∀ {Γ A B P} →

            Γ ,, (Some A) |- P
            --------------------------- conj-left1
            → Γ ,, (Some (A ×' B)) |- P
    conj-l2 : ∀ {Γ A B P} →

            Γ ,, (Some B) |- P
            --------------------------- conj-left2
            → Γ ,, (Some (A ×' B)) |- P

  -- asynchronous rules

    arr-r : ∀ {Γ A B} →

          (A :: Γ) ,, None |- B
          ----------------------- impl-right
          → Γ ,, None |- (A ⇒' B)

    conj-r : ∀ {Γ A B} →

           Γ ,, None |- A → Γ ,, None |- B
           ------------------------------- conj-right
           → Γ ,, None |- (A ×' B)

  -- examples

  i : ∀ {A} → [] ,, None |- (A ⇒' A)
  i = arr-r (focus i0 init)

  #2 : ∀ {A B} → [] ,, None |- (A ⇒' (B ⇒' B))
  #2 = arr-r (arr-r (focus i0 init))

  k : ∀ {A B} → [] ,, None |- (A ⇒' (B ⇒' A))
  k = arr-r (arr-r (focus (iS i0) init))

  s : ∀ {A B C} → [] ,, None |- ((A ⇒' (B ⇒' C)) ⇒' ((A ⇒' B) ⇒' (A ⇒' C)))
  s = arr-r (arr-r (arr-r (focus (iS (iS i0)) (arr-l (focus i0 init) (arr-l (focus (iS i0) (arr-l (focus i0 init) init)) init)))))

  #5 : ∀ {A B} → [] ,, None |- (A ⇒' (B ⇒' (A ×' B)))
  #5 = arr-r (arr-r (conj-r (focus (iS i0) init) (focus i0 init)))

  #6 : ∀ {A B} → [] ,, None |- (A ⇒' (A ×' (B ⇒' B)))
  #6 = arr-r (conj-r (focus i0 init) (arr-r (focus i0 init)))

  mp : ∀ {A B} → [] ,, None |- ((A ×' (A ⇒' B)) ⇒' B)
  mp = arr-r (focus i0 (conj-l2 (arr-l (focus i0 (conj-l1 init)) init)))

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Groups
open import Fields.Fields
open import Fields.Orders.Total.Definition
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Addition
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Semirings.Definition
open import Groups.Homomorphisms.Definition
open import Rings.Homomorphisms.Definition
open import Groups.Lemmas
open import Orders.Total.Definition

module Fields.CauchyCompletion.PartiallyOrderedRing {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

private
  lemma3 : {c d : _} {C : Set c} {S : Setoid {c} {d} C} {_+_ : C → C → C} (G : Group S _+_) → ({x y : C} → Setoid._∼_ S (x + y) (y + x)) → (x y z : C) → Setoid._∼_ S (((Group.inverse G x) + y) + (x + z)) (y + z)
  lemma3 {S = S} {_+_ = _+_} G ab x y z = transitive +Associative (+WellDefined (transitive (ab {inverse x + y}) (transitive +Associative (transitive (+WellDefined invRight reflexive) identLeft))) reflexive)
    where
      open Setoid S
      open Equivalence (Setoid.eq S)
      open Group G

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Ring R
open Group additiveGroup
open Field F

open import Fields.Lemmas F
open import Rings.Orders.Partial.Lemmas pRing
open import Rings.Orders.Total.Lemmas order
open import Fields.Orders.Lemmas {F = F} {pRing} (record { oRing = order })
open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Addition order F
open import Fields.CauchyCompletion.Multiplication order F
open import Fields.CauchyCompletion.Approximation order F
open import Fields.CauchyCompletion.Group order F
open import Fields.CauchyCompletion.Ring order F
open import Fields.CauchyCompletion.Comparison order F
open import Fields.CauchyCompletion.Setoid order F
open import Groups.Homomorphisms.Lemmas CInjectionGroupHom
open import Setoids.Orders.Total.Lemmas (TotallyOrderedRing.total order)

private
  productPositives : (a b : A) → (injection 0R) <Cr a → (injection 0R) <Cr b → (injection 0R) <Cr (a * b)
  productPositives a b record { e = eA ; 0<e = 0<eA ; N = Na ; property = prA } record { e = eB ; 0<e = 0<eB ; N = Nb ; property = prB } = record { e = eA * eB ; 0<e = orderRespectsMultiplication 0<eA 0<eB ; N = Na +N Nb ; property = ans }
    where
      ans : (m : ℕ) → Na +N Nb <N m → ((eA * eB) + index (CauchyCompletion.elts (injection 0R)) m) < (a * b)
      ans m <m = <WellDefined (symmetric (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight)) reflexive (ringMultiplyPositives 0<eA 0<eB (<WellDefined (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight) reflexive (prA m (inequalityShrinkLeft <m))) (<WellDefined (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight) reflexive (prB m (inequalityShrinkRight <m))))

  productPositives' : (a b : CauchyCompletion) (interA interB : A) → (0R < interA) → (0R < interB) → (interA r<C a) → (interB r<C b) → (interA * interB) r<C (a *C b)
  productPositives' a b interA interB 0<iA 0<iB record { e = interA' ; 0<e = 0<interA' ; N = Na ; pr = prA } record { e = interB' ; 0<e = 0<interB' ; N = Nb ; pr = prB } = record { e = interA' * interB' ; 0<e = orderRespectsMultiplication 0<interA' 0<interB' ; N = Na +N Nb ; pr = ans }
    where
      ans : (m : ℕ) → (Na +N Nb <N m) → ((interA * interB) + (interA' * interB')) < index (CauchyCompletion.elts (a *C b)) m
      ans m <m rewrite indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _*_ {m} = <Transitive (<WellDefined identRight (symmetric *DistributesOver+) (<WellDefined reflexive (+WellDefined *Commutative *Commutative) (<WellDefined reflexive (+WellDefined (symmetric *DistributesOver+) (symmetric *DistributesOver+)) (<WellDefined groupIsAbelian (transitive (transitive groupIsAbelian (transitive (symmetric +Associative) (+WellDefined *Commutative (transitive groupIsAbelian (transitive (+WellDefined reflexive *Commutative) (symmetric +Associative)))))) +Associative) (orderRespectsAddition (<WellDefined identRight reflexive (ringAddInequalities (orderRespectsMultiplication 0<iB 0<interA') (orderRespectsMultiplication 0<interB' 0<iA))) ((interA * interB) + (interA' * interB'))))))) (ringMultiplyPositives (<WellDefined identRight reflexive (ringAddInequalities 0<iA 0<interA')) (<WellDefined identRight reflexive (ringAddInequalities 0<iB 0<interB')) (prA m (inequalityShrinkLeft <m)) (prB m (inequalityShrinkRight <m)))

  <COrderRespectsMultiplication : (a b : CauchyCompletion) → (injection 0R <C a) → (injection 0R <C b) → (injection 0R <C (a *C b))
  <COrderRespectsMultiplication a b record { i = interA ; a<i = 0<interA ; i<b = interA<a } record { i = interB ; a<i = 0<interB ; i<b = interB<b } = record { i = interA * interB ; a<i = productPositives interA interB 0<interA 0<interB ; i<b = productPositives' a b interA interB (<CCollapsesL 0R _ 0<interA) (<CCollapsesL 0R _ 0<interB) interA<a interB<b }

  cOrderRespectsAdditionLeft' : (a : CauchyCompletion) (b : A) (c : A) → (a <Cr b) → (a +C injection c) <C (injection b +C injection c)
  cOrderRespectsAdditionLeft' a b c record { e = e ; 0<e = 0<e ; N = N ; property = pr } = <CWellDefined {a +C injection c} {a +C injection c} {injection (b + c)} {(injection b) +C (injection c)} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {a +C injection c}) (GroupHom.groupHom (RingHom.groupHom CInjectionRingHom)) (<CRelaxR (record { e = e ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (transitive (symmetric +Associative) (+WellDefined reflexive (ans m))) reflexive (orderRespectsAddition (pr m N<m) c) }))
    where
      ans : (m : ℕ) → (index (CauchyCompletion.elts a) m + c) ∼ index (apply _+_ (CauchyCompletion.elts a) (constSequence c)) m
      ans m rewrite indexAndApply (CauchyCompletion.elts a) (constSequence c) _+_ {m} | indexAndConst c m = reflexive

  l1 : (a : A) (b : CauchyCompletion) → a r<C b → 0R r<C (b +C injection (inverse a))
  l1 a b record { e = e ; 0<e = 0<e ; N = N ; pr = pr } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive groupIsAbelian (transitive +Associative (+WellDefined invLeft reflexive))) (ans m) (orderRespectsAddition (pr m N<m) (inverse a)) }
    where
      ans : (m : ℕ) → (index (CauchyCompletion.elts b) m + inverse a) ∼ index (CauchyCompletion.elts (b +C injection (inverse a))) m
      ans m rewrite indexAndApply (CauchyCompletion.elts b) (constSequence (inverse a)) _+_ {m} | indexAndConst (inverse a) m = reflexive

  l1' : (a : A) (b : CauchyCompletion) → 0R r<C (b +C injection a) → (inverse a) r<C b
  l1' a b record { e = e ; 0<e = 0<e ; N = N ; pr = pr } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive (+WellDefined identLeft reflexive) groupIsAbelian) (symmetric (ans m)) (orderRespectsAddition (pr m N<m) (inverse a)) }
    where
      ans : (m : ℕ) → (index (CauchyCompletion.elts b) m) ∼ (index (CauchyCompletion.elts (b +C injection a)) m + inverse a)
      ans m rewrite indexAndApply (CauchyCompletion.elts b) (constSequence a) _+_ {m} | indexAndConst a m = transitive (symmetric identRight) (transitive (+WellDefined reflexive (symmetric invRight)) +Associative)

  l2 : (a : CauchyCompletion) (b : A) → a <Cr b → 0R r<C (injection b +C (-C a))
  l2 a b record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invRight)) groupIsAbelian) (ans m) (orderRespectsAddition (property m N<m) (inverse (index (CauchyCompletion.elts a) m))) }
    where
      ans : (m : ℕ) → (b + inverse (index (CauchyCompletion.elts a) m)) ∼ index (CauchyCompletion.elts (injection b +C (-C a))) m
      ans m rewrite indexAndApply (CauchyCompletion.elts (injection b)) (CauchyCompletion.elts (-C a)) _+_ {m} | indexAndConst b m | mapAndIndex (CauchyCompletion.elts a) inverse m = reflexive

  l2' : (a : CauchyCompletion) (b : A) → 0R r<C (injection b +C a) → (-C a) <Cr b
  l2' a b record { e = e ; 0<e = 0<e ; N = N ; pr = pr } = record { e = e ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (+WellDefined identLeft reflexive) (ans m) (orderRespectsAddition (pr m N<m) (index (CauchyCompletion.elts (-C a)) m)) }
    where
      ans : (m : ℕ) → (index (CauchyCompletion.elts (injection b +C a)) m + index (map inverse (CauchyCompletion.elts a)) m) ∼ b
      ans m rewrite indexAndApply (CauchyCompletion.elts (injection b)) (CauchyCompletion.elts a) _+_ {m} | indexAndConst b m | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) = transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)

  invInj : (i : A) → Setoid._∼_ cauchyCompletionSetoid (injection (inverse i) +C injection i) (injection 0R)
  invInj i = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (inverse i) +C injection i) }} {record { converges = CauchyCompletion.converges ((-C (injection i)) +C injection i) }} {record { converges = CauchyCompletion.converges (injection 0R) }} (Group.+WellDefinedLeft CGroup {record { converges = CauchyCompletion.converges (injection (inverse i)) }} {record { converges = CauchyCompletion.converges (injection i)}} {record { converges = CauchyCompletion.converges (-C (injection i)) }} homRespectsInverse) (Group.invLeft CGroup {injection i})

  cOrderMove : (a b : A) (c : CauchyCompletion) → (injection a +C c) <Cr b → a r<C (injection b +C (-C c))
  cOrderMove a b c record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts (injection a)) (CauchyCompletion.elts c) _+_ {m})) reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst a m)) invRight) identRight)))) groupIsAbelian)) (transitive (+WellDefined (identityOfIndiscernablesLeft _∼_ reflexive (indexAndConst b m)) (identityOfIndiscernablesRight _∼_ reflexive (mapAndIndex (CauchyCompletion.elts c) inverse m))) (identityOfIndiscernablesLeft _∼_ reflexive (indexAndApply (CauchyCompletion.elts (injection b)) (CauchyCompletion.elts (-C c)) _+_ {m}))) (orderRespectsAddition (property m N<m) (inverse (index (CauchyCompletion.elts c) m))) }

  cOrderMove' : (a b : A) (c : CauchyCompletion) → (injection a +C (-C c)) <Cr b → a r<C (injection b +C c)
  cOrderMove' a b c pr = r<CWellDefinedRight _ _ _ (Group.+WellDefinedRight CGroup {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges (-C (-C c)) }} {record {converges = CauchyCompletion.converges c }} (invTwice CGroup record { converges = CauchyCompletion.converges c })) (cOrderMove a b (-C c) pr)

  cOrderMove'' : (a : CauchyCompletion) (b c : A) → (a +C (-C injection b)) <Cr c → a <Cr (b + c)
  cOrderMove'' a b c record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts a) _ _+_ {m})) reflexive) (transitive (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (transitive (identityOfIndiscernablesLeft _∼_ reflexive (mapAndIndex _ inverse m)) (inverseWellDefined additiveGroup (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst b m)))) reflexive) invLeft))) identRight)))) groupIsAbelian (orderRespectsAddition (property m N<m) b) }

  cOrderRespectsAdditionLeft'' : (a b : A) (c : CauchyCompletion) → (a < b) → (injection a +C c) <C (injection b +C c)
  cOrderRespectsAdditionLeft'' a b c a<b with halve charNot2 (b + inverse a)
  ... | b-a/2 , prDiff with approximateAbove c b-a/2 (halvePositive' prDiff (moveInequality a<b))
  ... | aboveC , (c<aboveC ,, aboveC-C<e) = record { i = a + aboveC ; a<i = <CRelaxR' (SetoidPartialOrder.<WellDefined <COrder (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges c }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection aboveC +C injection a) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection aboveC) }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} (GroupHom.groupHom CInjectionGroupHom))) (cOrderRespectsAdditionLeft' c aboveC a c<aboveC)) ; i<b = cOrderMove' _ _ _ (<CRelaxR' (<CTransitive (<CRelaxR t) (<CInherited u))) }
    where
      g : ((injection aboveC +C (-C c)) +C injection a) <C ((injection b-a/2) +C (injection a))
      g = cOrderRespectsAdditionLeft' _ _ a (<CRelaxR' aboveC-C<e)
      g' : ((injection aboveC +C (-C c)) +C injection a) <C (injection (b-a/2 + a))
      g' = <CWellDefined (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((injection aboveC +C (-C c)) +C injection a) }}) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }} {record { converges = CauchyCompletion.converges (injection b-a/2 +C injection a) }} (GroupHom.groupHom CInjectionGroupHom)) g
      t : (injection (a + aboveC) +C (-C c)) <Cr (b-a/2 + a)
      t = <CRelaxR' (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (((injection aboveC) +C (-C c)) +C injection a) }} {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC) +C (-C c)) }} (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection aboveC +C (-C c)) }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (((injection a) +C (injection aboveC)) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((injection (a + aboveC)) +C (-C c)) }} (Group.+Associative CGroup {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges (injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }}) (Group.+WellDefinedLeft CGroup {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} (GroupHom.groupHom CInjectionGroupHom))))) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }}) g')
      lemm : 0R < b-a/2
      lemm = halvePositive' prDiff (moveInequality a<b)
      u : (b-a/2 + a) < b
      u = <WellDefined (transitive (+WellDefined (symmetric prDiff) reflexive) (transitive groupIsAbelian (transitive +Associative (transitive (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive) groupIsAbelian)))) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) (orderRespectsAddition (<WellDefined identLeft (transitive (transitive +Associative (transitive (+WellDefined (transitive groupIsAbelian (+WellDefined reflexive (symmetric (invTwice additiveGroup b-a/2)))) reflexive) (symmetric +Associative))) (+WellDefined reflexive (symmetric (invContravariant additiveGroup)))) (orderRespectsAddition lemm (b + inverse a))) (a + inverse b-a/2))

  cOrderRespectsAdditionLeft''Flip : (a b : A) (c : CauchyCompletion) → (a < b) → (c +C injection a) <C (c +C injection b)
  cOrderRespectsAdditionLeft''Flip a b c a<b = <CWellDefined ((Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges c }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges c }}) (cOrderRespectsAdditionLeft'' a b c a<b)

  cOrderRespectsAdditionLeft''' : (a b : CauchyCompletion) (c : A) → (a <C b) → (a +C injection c) <C (b +C injection c)
  cOrderRespectsAdditionLeft''' a b c record { i = i ; a<i = a<i ; i<b = i<b } = <CTransitive (cOrderRespectsAdditionLeft' a i c a<i) (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C injection i) }} {record { converges = CauchyCompletion.converges (injection i +C injection c) }} (GroupHom.groupHom CInjectionGroupHom) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges (injection i) }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}) (flip<C' {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C b) }} (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((-C b) +C injection (inverse c)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} (Group.+WellDefinedRight CGroup {record { converges = CauchyCompletion.converges (-C b) }} {record { converges = CauchyCompletion.converges (injection (inverse c)) }} {record { converges = CauchyCompletion.converges (-C (injection c)) }} homRespectsInverse) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} (invContravariant CGroup {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}))) homRespectsInverse' (cOrderRespectsAdditionLeft' (-C b) (inverse i) (inverse c) (flipR<C i<b)))))

  cOrderRespectsAdditionRightZero : (a : CauchyCompletion) → (0R r<C a) → (c : CauchyCompletion) → c <C (a +C c)
  cOrderRespectsAdditionRightZero a record { e = e ; 0<e = 0<e ; N = N1 ; pr = pr } c with halve charNot2 e
  ... | e/2 , prE/2 with approximateAbove c e/2 (halvePositive' prE/2 0<e)
  ... | c+ , (c<c+ ,, c+<c+e/2) with approximateBelow (a +C c) e/2 (halvePositive' prE/2 0<e)
  ... | α , (α<a+c ,, a+c<α+e/2) with totality c+ α
  ... | inl (inl c+<α) = record { i = α ; a<i = <CRelaxR' (<CTransitive (<CRelaxR c<c+) (<CInherited c+<α)) ; i<b = α<a+c }
  -- The remaining cases can't actually happen, but it's easier to go this way
  ... | inr c+=α = record { i = α ; a<i = <CrWellDefinedRight c _ _ c+=α c<c+ ; i<b = α<a+c }
  ... | inl (inr α<c+) with cOrderMove'' (a +C c) α e/2 (<CRelaxR' a+c<α+e/2)
  ... | record { e = f ; 0<e = 0<f ; N = M ; property = pr2 } with CauchyCompletion.converges c e/2 (halvePositive' prE/2 0<e)
  ... | N3 , pr4 = record { i = α ; a<i = record { e = f ; 0<e = 0<f ; N = u ; property = ans } ; i<b = α<a+c }
    where
      u : ℕ
      u = succ ((N1 +N M) +N N3)
      help : (m : ℕ) → u <N m → index (CauchyCompletion.elts c) m < (e/2 + index (CauchyCompletion.elts c) u)
      help m size with pr4 {m} {u} (lessTransitive (le (N1 +N M) refl) size) (le (N1 +N M) refl)
      ... | bl with totality 0G (index (CauchyCompletion.elts c) m + inverse (index (CauchyCompletion.elts c) u))
      ... | inl (inl 0<t) = <WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive (orderRespectsAddition bl (index (CauchyCompletion.elts c) u))
      ... | inl (inr cm-cU<0) = <Transitive (<WellDefined (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invLeft)) identRight) reflexive (orderRespectsAddition cm-cU<0 (index (CauchyCompletion.elts c) u))) (orderRespectsAddition (halvePositive' prE/2 0<e) (index (CauchyCompletion.elts c) u))
      ... | inr (0=t) = <WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive (orderRespectsAddition bl (index (CauchyCompletion.elts c) u))
      ans : (m : ℕ) → u <N m → (f + index (CauchyCompletion.elts c) m) < α
      ans m size = <Transitive (<WellDefined reflexive +Associative (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (<Transitive (<WellDefined reflexive (transitive (+WellDefined (symmetric (transitive (+WellDefined (transitive identLeft (symmetric prE/2)) reflexive) (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invRight)) identRight))) reflexive) (symmetric +Associative)) (help m size)) (<WellDefined reflexive (transitive groupIsAbelian (transitive (symmetric +Associative) (+WellDefined reflexive groupIsAbelian))) (orderRespectsAddition (pr u (le (M +N N3) (applyEquality succ (transitivity (additionNIsCommutative _ N1) (Semiring.+Associative ℕSemiring N1 M _))))) (inverse e/2 + index (CauchyCompletion.elts c) u)))) f))) (<WellDefined (transitive groupIsAbelian (transitive +Associative (+WellDefined groupIsAbelian (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts c) _+_ {u}))))) (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invRight)) identRight) (orderRespectsAddition (pr2 u (le (N1 +N N3) (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring N1 _ _)) (transitivity (applyEquality (N1 +N_) (additionNIsCommutative N3 M)) (Semiring.+Associative ℕSemiring N1 _ _)))))) (inverse e/2)))

  cOrderRespectsAdditionLeft : (a : CauchyCompletion) (b : A) (c : CauchyCompletion) → (a <Cr b) → (a +C c) <C (injection b +C c)
  cOrderRespectsAdditionLeft a b c a<b = <CWellDefined {record { converges = CauchyCompletion.converges (a +C c) }}{record { converges = CauchyCompletion.converges (a +C c) }}{record { converges = CauchyCompletion.converges (((-C a) +C injection b) +C (a +C c)) }}{record { converges = CauchyCompletion.converges (injection b +C c) }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (a +C c)}}) (lemma3 CGroup (λ {x} {y} → Ring.groupIsAbelian CRing {x} {y}) a (injection b) c) (cOrderRespectsAdditionRightZero ((-C a) +C injection b) (r<CWellDefinedLeft (inverse b + b) 0R ((-C a) +C injection b) invLeft (<CRelaxL' (<CWellDefined {record { converges = CauchyCompletion.converges (injection (inverse b) +C injection b) }}{record { converges = CauchyCompletion.converges (injection (inverse b + b)) }}{record { converges = CauchyCompletion.converges ((-C a) +C injection b) }}{record { converges = CauchyCompletion.converges ((-C a) +C injection b) }} (GroupHom.groupHom' CInjectionGroupHom) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((-C a) +C injection b) }}) (cOrderRespectsAdditionLeft''' _ _ b (<CRelaxL (flip<CR a<b)))))) (a +C c))

  lemma2 : (a b : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid (Group.inverse CGroup ((-C a) +C (-C b))) (a +C b)
  lemma2 a b = tr {record { converges = CauchyCompletion.converges (-C ((-C a) +C (-C b))) }} {record { converges = CauchyCompletion.converges ((-C (-C b)) +C (-C (-C a))) }} {record { converges = CauchyCompletion.converges (a +C b) }} (invContravariant CGroup {record { converges = CauchyCompletion.converges (-C a) }} {record { converges = CauchyCompletion.converges (-C b) }}) (tr {record { converges = CauchyCompletion.converges ((-C (-C b)) +C (-C (-C a))) }} {record { converges = CauchyCompletion.converges (b +C a) }} {record { converges = CauchyCompletion.converges (a +C b) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (-C (-C b)) }} {record { converges = CauchyCompletion.converges (-C (-C a)) }} {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges a }} (invTwice CGroup b) (invTwice CGroup a)) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges a }}))
    where
      open Setoid cauchyCompletionSetoid
      open Equivalence (Setoid.eq cauchyCompletionSetoid) renaming (transitive to tr)

  cOrderRespectsAdditionRight : (a : A) (b : CauchyCompletion) (c : CauchyCompletion) → (a r<C b) → (injection a +C c) <C (b +C c)
  cOrderRespectsAdditionRight a b c a<b = <CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (Group.inverse CGroup (injection (inverse a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (Group.inverse CGroup ((-C injection a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection a +C c) }} (inverseWellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse a) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((-C (injection a)) +C (-C c)) }} (Group.+WellDefinedLeft CGroup {record { converges = CauchyCompletion.converges (injection (inverse a)) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (-C (injection a)) }} homRespectsInverse)) (lemma2 (injection a) c)) (lemma2 b c) (flip<C (cOrderRespectsAdditionLeft _ _ (Group.inverse CGroup c) (flipR<C a<b)))

  cOrderRespectsAddition : (a b : CauchyCompletion) → (a <C b) → (c : CauchyCompletion) → (a +C c) <C (b +C c)
  cOrderRespectsAddition a b record { i = i ; a<i = a<i ; i<b = i<b } c = SetoidPartialOrder.<Transitive <COrder (cOrderRespectsAdditionLeft a i c a<i) (cOrderRespectsAdditionRight i b c i<b)

CpOrderedRing : PartiallyOrderedRing CRing <COrder
PartiallyOrderedRing.orderRespectsAddition CpOrderedRing {a} {b} = cOrderRespectsAddition a b
PartiallyOrderedRing.orderRespectsMultiplication CpOrderedRing {a} {b} 0<a 0<b = <COrderRespectsMultiplication a b 0<a 0<b


text:
{-# OPTIONS --cubical-compatible --show-implicit #-}
-- {-# OPTIONS -v tc.data:100 #-}
module WithoutK9 where

module Eq {A : Set} (x : A) where

  data _≡_ : A → Set where
    refl : _≡_ x

open Eq

module Bad {A : Set} {x : A} where

  module E = Eq x

  weak-K : {y : A} (p q : E._≡_ y) (α β : p ≡ q) → α ≡ β
  weak-K refl .refl refl refl = refl


text:
module Generate where

open import Data.List
open import Data.Fin hiding (_+_)
open import Data.Nat
open import Data.Product
open import Data.Bool
open import Function using (_∘_ ; _$_ ; _∋_ ; id ; case_return_of_ ; flip )
open import Function.Injection hiding (_∘_)
open import Function.Surjection hiding (_∘_)
open import Function.Bijection hiding (_∘_)
open import Function.LeftInverse hiding (_∘_)
open import Relation.Binary using (Setoid ; Decidable)
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary.Negation
open import Relation.Nullary
open import Function.Equality using (_⟶_ ;  _⟨$⟩_ ; Π )
open import Reflection
open import Level

open import Serializer
open import Helper.Fin
open import Helper.CodeGeneration

open import Serializer.Bool
open import Serializer.Fin
open import With hiding (subst) --  ; _+_ ; A)

open Serializer.Serializer {{...}}
--open Serializer.Serializer {{Fin 2}}

-------------------------
-- Generic from/to term's.

data Test : Set where
  A : Bool -> Test
  B : Bool -> Test
  C : Bool -> Test
  D : Bool -> Test

conSize : (n : Name) -> Term
conSize n with (definition n)
conSize n | constructor′ with (type n)
conSize n | constructor′ | el (lit n₁) (pi (arg i (el s t)) t₂) = def (quote size) [ a1 t ]
conSize n | constructor′ | el _ _ = quoteTerm 0
conSize n | _ = quoteTerm 0

sumTerms : List Name -> Term
sumTerms [] = quoteTerm 0
sumTerms (x ∷ ls) = def (quote _+_) (a (conSize x) ∷ a (sumTerms ls) ∷ [])

cons`` : (n : Name) -> List (_×_ Name (_×_ (List Name) (List Name)))
cons`` n = zipWith _,_ (cons n) (zipWith _,_ (inits (cons n)) (drop 1 (tails (cons n))))

{-
fromTest : Test -> Fin 4
fromTest (A z) = +₁ 2 (2 + 0) (fromBool z)
fromTest (B z) = +₂ 2 2 (fromBool z)

toTest : Fin 4 -> Test
toTest x = (Helper.Fin.[ (λ z₁ → A (toBool z₁)) , (λ z₁ → B (toBool z₁)) ] (⨁ 2 2 x))
-}

{-
fromTest : Test -> Fin 6
fromTest (A x) = +₁ 4 2 (+₁ 2 2 (from x))
fromTest (B x) = +₁ 4 2 (+₂ 2 2 (from x))
fromTest (C x) = +₂ 4 2 (from x)

toTest : Fin 6 -> Test
toTest x = Helper.Fin.[ (\y -> Helper.Fin.[ (\z -> A $ to z) , (\z -> B $ to z) ] (⨁ 2 2 y) ) , (\y -> C $ to y) ] (⨁ 4 2 x)
-}

cons` : Name -> List (_×_ Name (_×_ (List Name) (List Name)))
cons` n = zipWith _,_ (reverse (cons n)) (zipWith _,_ (inits (reverse (cons n))) (Data.List.map reverse (drop 1 (tails (reverse (cons n))))))

{-# TERMINATING #-}
genFrom : (n : Name)  -> FunctionDef
genFrom n = fun-def (t0 $ fun_type) clauses
  where
    fun_type = pi (a ∘ t0 $ def n []) (abs "_" (t0 (def (quote Fin) [ a (sumTerms (cons n)) ])))

    construct : (_×_ Name (_×_ (List Name) (List Name))) -> Term
    construct (c , [] , []) = (def (quote from) [ a (var 0 []) ])
    construct (c , x ∷ xs , []) = def (quote +₂) ((a (sumTerms (x ∷ xs))) ∷ (a (conSize c)) ∷ (a (construct (c , ([] , [])))) ∷ [])
    construct (c , xs , y ∷ ys) = def (quote +₁) ((a (sumTerms (c ∷ (xs ++ ys)))) ∷ (a (conSize y)) ∷ (a (construct (c , (xs , ys)))) ∷ [])

    clauses = Data.List.map (\{ (c , xs) -> clause [ a $ con c [ a (var "_") ] ] (construct (c , xs))}) (cons` n)

unquoteDecl fromTest = genFrom (quote Test)

genTo : (n : Name)  -> FunctionDef
genTo n = fun-def (t0 $ fun_type) clauses
  where
    fun_type = pi (a (t0 (def (quote Fin) [ a (sumTerms (cons n)) ]))) (abs "_" (t0 $ def n []))

    match : List Name -> Term
    match [] = unknown
    match (x ∷ []) = con x [ a (def (quote to) [ a (var 0 []) ]) ]
    match (x ∷ x₁ ∷ cons) = def (quote [_,_])
          ( (a (lam visible (abs "_" (match (x₁ ∷ cons))))) -- (a (lam visible (abs "_" (con x [ a (def (quote to) [ a (var 0 []) ]) ]))))
          ∷ (a (lam visible (abs "_" (con x [ a (def (quote to) [ a (var 0 []) ]) ]))))
          ∷ (a (def (quote ⨁) ((a (sumTerms (x₁ ∷ cons))) ∷ (a (quoteTerm 2)) ∷ (a (var 0 [])) ∷ [])))
          ∷ [])

    clauses = [ clause [ a (var "_") ] (match (cons n)) ]

unquoteDecl toTest = genTo (quote Test)

makePresEq : {T : Set} {n : ℕ} -> (T -> (Fin n)) -> setoid T ⟶ setoid (Fin n)
makePresEq f = record { _⟨$⟩_ = f ; cong = (\{ {i} {.i} refl → refl }) }

genPresEq' : (n : Name) -> Term
genPresEq' n = def (quote makePresEq) [ a (def (quote fromTest) []) ] -- [(a (genFrom' n))]
  where
    setoidFrom = def (quote setoid) [(a (def n []))]
    setoidTo = def (quote setoid) [(a (def (quote Fin) [ a (sumTerms (cons n)) ]))]
    fun_type1 = t0 (def (quote _⟶_) ( (a setoidFrom) ∷ (a setoidTo) ∷ []))

genPresEq : (n : Name) -> FunctionDef
genPresEq n = fun-def fun_type1 [(clause [] (genPresEq' n) ) ]
  where
    setoidFrom = def (quote setoid) [(a (def n []))]
    setoidTo = def (quote setoid) [(a (def (quote Fin) [ a (sumTerms (cons n)) ]))]
    fun_type1 = t0 (def (quote _⟶_) ( (a setoidFrom) ∷ (a setoidTo) ∷ []))

unquoteDecl genTest = genPresEq (quote Test)

t2 : {x y : Bool} → fromBool x ≡ fromBool y → x ≡ y
t2 = Bijective.injective (Bijection.bijective (bijection {Bool}))

bijection' : Term
bijection' = quoteTerm t2

refl' : Term
refl' = pat-lam [ clause ( (a1 (var "d1")) ∷ (a1 (dot)) ∷ ( a (con (quote refl) []) ) ∷ []) (con (quote refl) []) ] []

x₁≡x₂' : Term
x₁≡x₂' = def (quote _≡_) ((a $ var 1 []) ∷ (a $ var 0 []) ∷ [])

+-eq₁' : Term -> Term
+-eq₁' t = (def (quote +-eq₁) [ a t ])

+-eq₂' : ℕ -> ℕ -> Term -> Term
+-eq₂' n1 n2 t = (def (quote +-eq₂) ( a1 (lit (nat n1)) ∷ a1 (lit (nat n2)) ∷ a t ∷ [] ) )

¬+-eq₁' : Term
¬+-eq₁' = def (quote ¬+-eq₁) []

¬+-eq₂' : Term
¬+-eq₂' = def (quote ¬+-eq₂) []

_$'_ : Term -> Term -> Term
x $' y = def (quote _$_) ((a x) ∷ (a y) ∷ [])

contradiction' : Term -> Term -> Term
contradiction' t1 t2 = def (quote contradiction) ( (a t1) ∷ (a t2) ∷ [] )

genInjective : (n : Name) -> FunctionDef
genInjective n = fun-def fun_type1 [ (clause [] ( pat-lam (clauses 0 (var 0 []) (indexed_cons)) [] )) ]
  where
    fun_type1 = t0 (def (quote Injective) [ (a (def (quote genTest) [])) ] )

    ncons = (length (cons n))
    indexed_cons = zipWith (_,_) (cons n) ((downFrom (length (cons n))))

    clause'' : Name -> Name -> Term -> Clause
    clause'' l r t = clause ( (a1 $ con l [ a (var "x") ]) ∷ (a1 $ con r [ a (var "y") ]) ∷ (a (var "p")) ∷ [] ) t

    clause' : ℕ -> Term -> (_×_ Name ℕ) -> (_×_ Name ℕ) -> Clause
    clause' n t (n1 , i1) (n2 , i2) with (Data.Nat.compare i1 i2)
    clause' n t (n1 , i1) (n2 , ._) | less .i1 k = clause'' n1 n2 (contradiction' (t) ¬+-eq₁')
    clause' n t (n1 , ℕ.zero) (n2 , .0) | equal .0 = clause'' n1 n2 (with' x₁≡x₂' (bijection' $' (t)) refl')
    clause' n t (n1 , ℕ.suc i1) (n2 , .(ℕ.suc i1)) | equal .(ℕ.suc i1) = clause'' n1 n2 (with' x₁≡x₂' (bijection' $' (+-eq₂' ((ncons ∸ n ∸ 1) * 2) 2 (t))) refl')
    clause' n t (n1 , ._) (n2 , i2) | greater .i2 k = clause'' n1 n2 (contradiction' (t) ¬+-eq₂')

    clauses : ℕ -> Term -> List (_×_ Name ℕ) -> List Clause
    clauses n t [] = []
    clauses n t (x ∷ cs) = (Data.List.map (clause' n t x) (x ∷ cs)) ++ (Data.List.map ((flip (clause' n t)) x) cs) ++ (clauses (ℕ.suc n) (+-eq₁' t) cs) -- Data.List.map clause' c

unquoteDecl testInjective = genInjective (quote Test)

makePresEqTo : {T : Set} {n : ℕ} -> ((Fin n) -> T) -> setoid (Fin n) ⟶ setoid T
makePresEqTo f = record { _⟨$⟩_ = f ; cong = (\{ {i} {.i} refl → refl }) }

genPresEqTo' : (n : Name) -> Term
genPresEqTo' n = def (quote makePresEqTo) [ a (def (quote toTest) []) ]
  where
    setoidTo = def (quote setoid) [(a (def n []))]
    setoidFrom = def (quote setoid) [(a (def (quote Fin) [ a (sumTerms (cons n)) ]))]
    fun_type1 = t0 (def (quote _⟶_) ( (a setoidFrom) ∷ (a setoidTo) ∷ []))

genPresEqTo : (n : Name) -> FunctionDef
genPresEqTo n = fun-def infer_type [ (clause [] (genPresEqTo' n) ) ]

unquoteDecl genTestTo = genPresEqTo (quote Test)

Fin+' : ℕ -> ℕ -> Term
Fin+' n1 n2 = def (quote Fin+) ((a (lit (nat n1))) ∷ (a (lit (nat n2))) ∷ (a $ var 0 []) ∷ [])

⨁' : ℕ -> ℕ -> Term
⨁' n1 n2 = def (quote ⨁) ((a (lit (nat n1))) ∷ (a (lit (nat n2))) ∷ (a $ var 0 []) ∷ [])

x₂≡x₁' : Term
x₂≡x₁' = def (quote _≡_) ( (a $ var 0 []) ∷ (a $ var 1 []) ∷ [])

right-inverse-of' : Term
right-inverse-of' = quoteTerm (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (bijection {Bool}))))

fromToBool' : Term
fromToBool' = (def (quote fromBool) (arg (arg-info visible relevant) (def (quote toBool) (arg (arg-info visible relevant) (var 0 []) ∷ [])) ∷ []))

matchFin+ : Term -> Term -> Term
matchFin+ t1 t2 = pat-lam ((clause ( (a1 (dot)) ∷ (a (con (quote is+₁) [ a $ (var "u") ])) ∷ []) t1) ∷ (clause ( (a1 (dot)) ∷ (a (con (quote is+₂) [ a $ (var "u") ])) ∷ []) t2) ∷ []) []

step2 : Term
step2 = rewrite'' x₂≡x₁' (quoteTerm fromToBool') (quoteTerm (right-inverse-of' $' var 0 [])) refl'

⨁'' : ℕ -> ℕ -> Term
⨁'' m1 m2 = With.subst (quoteTerm (⨁' 1337 2)) (lit (nat 1337)) (lit (nat m1))

genRightInv' : (List Name) -> Term
genRightInv' [] = unknown
genRightInv' (x ∷ []) = step2
genRightInv' (x ∷ x₁ ∷ cons) = with'' (Fin+' l 2) (⨁'' l 2) (matchFin+ (genRightInv' (x₁ ∷ cons)) step2)
  where
    l = (length (x₁ ∷ cons) * 2)

right-inverse-of : genTestTo RightInverseOf genTest
right-inverse-of x = unquote (genRightInv' (cons (quote Test)))

{-
from-bijection : Bijection (setoid Test) (setoid (Fin 6))
from-bijection = record {
    to = genTest
  ; bijective = record {
      injective = testInjective
    ; surjective = record {
        from = genTestTo
      ; right-inverse-of = right-inverse-of
      }
    }
  }

instance
  serializerTest : Serializer Test
  serializerTest = record {
    size = 6 ;
    from = fromTest ;
    to = toTest ;
    bijection = from-bijection
    }
-}

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


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

module library.Basics where

open import library.Base public
open import library.PathGroupoid public
open import library.PathFunctor public
open import library.NType public
open import library.Equivalences public
open import library.Univalence public
open import library.Funext public
open import library.PathOver public

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import FRP.JS.Nat using ( ℕ ; _*_ )
open import FRP.JS.Bool using ( Bool )
open import FRP.JS.String using ( String )
open import FRP.JS.RSet using ( ⟦_⟧ ; ⟨_⟩ )
open import FRP.JS.Behaviour using ( Beh )
open import FRP.JS.Delay using ( Delay ) renaming
  ( _≟_ to _≟d_ ; _≠_ to _≠d_ ; _≤_ to _≤d_ ; _<_ to _<d_ ; _+_ to _+d_ ; _∸_ to _∸d_ )

module FRP.JS.Time where

open import FRP.JS.Time.Core public using ( Time ; epoch )

_≟_ : Time → Time → Bool
epoch t ≟ epoch u = t ≟d u

{-# COMPILED_JS _≟_ function(d) { return function(e) { return d === e; }; } #-}

_≠_ : Time → Time → Bool
epoch t ≠ epoch u = t ≠d u

{-# COMPILED_JS _≠_ function(d) { return function(e) { return d !== e; }; } #-}

_≤_ : Time → Time → Bool
epoch t ≤ epoch u = t ≤d u

{-# COMPILED_JS _≤_ function(d) { return function(e) { return d <= e; }; } #-}

_<_ : Time → Time → Bool
epoch t < epoch u = t <d u

{-# COMPILED_JS _<_ function(d) { return function(e) { return d < e; }; } #-}

_+_ : Time → Delay → Time
epoch t + d = epoch (t +d d)

{-# COMPILED_JS _+_ function(d) { return function(e) { return d + e; }; } #-}

_∸_ : Time → Time → Delay
epoch t ∸ epoch u = t ∸d u

{-# COMPILED_JS _∸_ function(d) { return function(e) { return Math.min(0, d - e); }; } #-}

postulate
  toUTCString : Time → String
  every : Delay → ⟦ Beh ⟨ Time ⟩ ⟧

{-# COMPILED_JS toUTCString function(t) { return require("agda.frp").date(t).toUTCString(); } #-}
{-# COMPILED_JS every function(d) { return function(t) { return require("agda.frp").every(d); }; } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module Lib.Logic where

infix 30 _∨_
infix 40 _∧_
infix 50 ¬_

data _∨_ (A B : Set) : Set where
  inl : A -> A ∨ B
  inr : B -> A ∨ B

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

data   False : Set where
record True  : Set where

¬_ : Set -> Set
¬ A = A -> False

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Lexicographic induction
------------------------------------------------------------------------

module Induction.Lexicographic where

open import Induction
open import Data.Product

-- The structure of lexicographic induction.

_⊗_ : ∀ {a b} → RecStruct a → RecStruct b → RecStruct (a × b)
_⊗_ RecA RecB P (x , y) =
  -- Either x is constant and y is "smaller", ...
  RecB (λ y' → P (x , y')) y
    ×
  -- ...or x is "smaller" and y is arbitrary.
  RecA (λ x' → ∀ y' → P (x' , y')) x

-- Constructs a recursor builder for lexicographic induction.

[_⊗_] : ∀ {a} {RecA : RecStruct a} → RecursorBuilder RecA →
        ∀ {b} {RecB : RecStruct b} → RecursorBuilder RecB →
        RecursorBuilder (RecA ⊗ RecB)
[_⊗_] {RecA = RecA} recA {RecB = RecB} recB P f (x , y) =
  (p₁ x y p₂x , p₂x)
  where
  p₁ : ∀ x y →
       RecA (λ x' → ∀ y' → P (x' , y')) x →
       RecB (λ y' → P (x , y')) y
  p₁ x y x-rec = recB (λ y' → P (x , y'))
                      (λ y y-rec → f (x , y) (y-rec , x-rec))
                      y

  p₂ : ∀ x → RecA (λ x' → ∀ y' → P (x' , y')) x
  p₂ = recA (λ x → ∀ y → P (x , y))
            (λ x x-rec y → f (x , y) (p₁ x y x-rec , x-rec))

  p₂x = p₂ x

------------------------------------------------------------------------
-- Example

private

  open import Data.Nat
  open import Induction.Nat as N

  -- The Ackermann function à la Rózsa Péter.

  ackermann : ℕ → ℕ → ℕ
  ackermann m n = build [ N.rec-builder ⊗ N.rec-builder ]
                        AckPred ack (m , n)
    where
    AckPred : ℕ × ℕ → Set
    AckPred _ = ℕ

    ack : ∀ p → (N.Rec ⊗ N.Rec) AckPred p → AckPred p
    ack (zero  , n)     _                   = 1 + n
    ack (suc m , zero)  (_         , ackm•) = ackm• 1
    ack (suc m , suc n) (ack[1+m]n , ackm•) = ackm• ack[1+m]n

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- Products (variants for Set₁)
------------------------------------------------------------------------

-- I want universe polymorphism.

module Data.Product1 where

open import Data.Function
open import Relation.Nullary

infixr 4 _,_
infixr 2 _×₀₁_ _×₁₀_ _×₁₁_

------------------------------------------------------------------------
-- Definition

data Σ₀₁ (a : Set) (b : a → Set₁) : Set₁ where
  _,_ : (x : a) (y : b x) → Σ₀₁ a b

data Σ₁₀ (a : Set₁) (b : a → Set) : Set₁ where
  _,_ : (x : a) (y : b x) → Σ₁₀ a b

data Σ₁₁ (a : Set₁) (b : a → Set₁) : Set₁ where
  _,_ : (x : a) (y : b x) → Σ₁₁ a b

∃₀₁ : {A : Set} → (A → Set₁) → Set₁
∃₀₁ = Σ₀₁ _

∃₁₀ : {A : Set₁} → (A → Set) → Set₁
∃₁₀ = Σ₁₀ _

∃₁₁ : {A : Set₁} → (A → Set₁) → Set₁
∃₁₁ = Σ₁₁ _

_×₀₁_ : Set → Set₁ → Set₁
A ×₀₁ B = Σ₀₁ A (λ _ → B)

_×₁₀_ : Set₁ → Set → Set₁
A ×₁₀ B = Σ₁₀ A (λ _ → B)

_×₁₁_ : Set₁ → Set₁ → Set₁
A ×₁₁ B = Σ₁₁ A (λ _ → B)

------------------------------------------------------------------------
-- Functions

proj₀₁₁ : ∀ {a b} → Σ₀₁ a b → a
proj₀₁₁ (x , y) = x

proj₀₁₂ : ∀ {a b} → (p : Σ₀₁ a b) → b (proj₀₁₁ p)
proj₀₁₂ (x , y) = y

proj₁₀₁ : ∀ {a b} → Σ₁₀ a b → a
proj₁₀₁ (x , y) = x

proj₁₀₂ : ∀ {a b} → (p : Σ₁₀ a b) → b (proj₁₀₁ p)
proj₁₀₂ (x , y) = y

proj₁₁₁ : ∀ {a b} → Σ₁₁ a b → a
proj₁₁₁ (x , y) = x

proj₁₁₂ : ∀ {a b} → (p : Σ₁₁ a b) → b (proj₁₁₁ p)
proj₁₁₂ (x , y) = y

map₀₁ : ∀ {A B P Q} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ₀₁ A P → Σ₀₁ B Q
map₀₁ f g p = (f (proj₀₁₁ p) , g (proj₀₁₂ p))

map₁₀ : ∀ {A B P Q} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ₁₀ A P → Σ₁₀ B Q
map₁₀ f g p = (f (proj₁₀₁ p) , g (proj₁₀₂ p))

map₁₁ : ∀ {A B P Q} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ₁₁ A P → Σ₁₁ B Q
map₁₁ f g p = (f (proj₁₁₁ p) , g (proj₁₁₂ p))


text: module Categories.Pushout where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Prelude

module Implicits.Syntax.MetaType where

open import Implicits.Syntax.Type

mutual
  data MetaSimpleType (m ν : ℕ) : Set where
    tvar : Fin ν → MetaSimpleType m ν
    mvar : Fin m → MetaSimpleType m ν
    _→'_ : (a b : MetaType m ν) → MetaSimpleType m ν
    tc   : ℕ → MetaSimpleType m ν

  data MetaType (m ν : ℕ) : Set where
    _⇒_ : (a b : MetaType m ν) → MetaType m ν
    ∀'  : MetaType m (suc ν) → MetaType m ν
    simpl : MetaSimpleType m ν → MetaType m ν

s-tvar : ∀ {ν m} → Fin ν → MetaType m ν
s-tvar n = simpl (tvar n)

s-mvar : ∀ {ν m} → Fin m → MetaType m ν
s-mvar n = simpl (mvar n)

s-tc : ∀ {ν m} → ℕ → MetaType m ν
s-tc c = simpl (tc c)

mutual
  to-smeta : ∀ {m ν} → SimpleType ν → MetaSimpleType m ν
  to-smeta (tc x) = (tc x)
  to-smeta (tvar n) = (tvar n)
  to-smeta (a →' b) = (to-meta a) →' (to-meta b)

  to-meta : ∀ {m ν} → Type ν → MetaType m ν
  to-meta (simpl x) = simpl (to-smeta x)
  to-meta (a ⇒ b) = (to-meta a) ⇒ (to-meta b)
  to-meta (∀' a) = ∀' (to-meta a)

mutual
  from-smeta : ∀ {ν} → MetaSimpleType zero ν → SimpleType ν
  from-smeta (tvar x) = tvar x
  from-smeta (mvar ())
  from-smeta (tc c) = tc c
  from-smeta (a →' b) = from-meta a →' from-meta b

  from-meta : ∀ {ν} → MetaType zero ν → Type ν
  from-meta (simpl τ) = simpl (from-smeta τ)
  from-meta (a ⇒ b) = from-meta a ⇒ from-meta b
  from-meta (∀' x) = ∀' (from-meta x)

is-m∀' : ∀ {m ν} → MetaType m ν → Set
is-m∀' (simpl x) = ⊥
is-m∀' (a ⇒ b) = ⊥
is-m∀' (∀' x) = ⊤