text:
{-# OPTIONS --sized-types --without-K #-}
module DepM 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

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

Fam₂ : {I : Set} → (I → Set) → Set₁
Fam₂ {I} J = (i : I) → J i → 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

-- | 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)

-- | Dependent polynomials
record DPoly
  {I : Set} -- ^ Outer index
  {J : Set} -- ^ Inner index
  : 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
⟦_⟧ : {I : Set} {J : Set} →
    DPoly {I} {J} →
    (X : Fam J) →  -- ^ Parameter
    (Fam I)
⟦_⟧ {I} {N} (dpoly A s E p t) X =
  Σ' s (λ a →
  Π' p (λ e →
    X (t e)
  ) a )

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

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

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

Rel₂ : {I : Set} → (X Y : I → Set) → Set₁
Rel₂ {I} X Y = (i : I) → X i → Y i → Set

-- | Lifting to relations
⟦_⟧'' : ∀ {I} (P : DPoly {I} {I}) {X Y} → Rel₂ X Y → Rel₂ (⟦ P ⟧ X) (⟦ P ⟧ Y)
⟦ dpoly A s E p t ⟧'' {X} {Y} R i x y =
  ∃ λ a → ∃ λ α → ∃ λ β → Σ[ q ∈ (i ≡ s a) ]
    (subst (⟦ dpoly A s E p t ⟧ X) q x ≡ ins a α
    × (subst (⟦ dpoly A s E p t ⟧ Y) q y) ≡ ins a β
    × ∀ u → R (t (proj₁ u)) (α u) (β u))

[_]_≡₂_ : ∀{I} {X : I → Set} → Rel₂ X X
[ i ] x ≡₂ y = x ≡ y

eq-preserving : ∀ {I P X} (i : I) (x y : ⟦ P ⟧ X i) →
                x ≡ y → ⟦ P ⟧'' (λ i → _≡_) i x y
eq-preserving i x y x≡y = {!!}

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

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
{-# OPTIONS --without-K --safe #-}
module Util.Vec where

open import Data.Vec public
open import Data.Vec.Relation.Unary.All as All public using (All ; [] ; _∷_)
open import Data.Vec.Relation.Unary.Any as Any public using (Any ; here ; there)
open import Data.Vec.Membership.Propositional public using (_∈_)

open import Data.Nat as ℕ using (_≤_)
open import Level using (_⊔_)
open import Relation.Binary using (Rel)

open import Util.Prelude

import Data.Nat.Properties as ℕ

max : ∀ {n} → Vec ℕ n → ℕ
max = foldr _ ℕ._⊔_ 0

max-weaken : ∀ {n} x (xs : Vec ℕ n) → max xs ≤ max (x ∷ xs)
max-weaken _ _ = ℕ.n≤m⊔n _ _

max-maximal : ∀ {n} (xs : Vec ℕ n) → All (_≤ max xs) xs
max-maximal [] = []
max-maximal (x ∷ xs)
  = ℕ.m≤m⊔n _ _
  ∷ All.map (λ x≤max → ℕ.≤-trans x≤max (max-weaken x xs)) (max-maximal xs)

All→∈→P : ∀ {α β} {A : Set α} {P : A → Set β} {n} {xs : Vec A n}
  → All P xs
  → ∀ {x}
  → x ∈ xs
  → P x
All→∈→P (px ∷ allP) (here refl) = px
All→∈→P (px ∷ allP) (there x∈xs) = All→∈→P allP x∈xs

max-maximal-∈ : ∀ {n x} {xs : Vec ℕ n} → x ∈ xs → x ≤ max xs
max-maximal-∈ = All→∈→P (max-maximal _)

data All₂ {α} {A : Set α} {ρ} (R : Rel A ρ)
  : ∀ {n} → Vec A n → Vec A n → Set (α ⊔ ρ) where
  [] : All₂ R [] []
  _∷_ : ∀ {n x y} {xs ys : Vec A n}
    → R x y
    → All₂ R xs ys
    → All₂ R (x ∷ xs) (y ∷ ys)

All₂-tabulate⁺ : ∀ {α} {A : Set α} {ρ} {R : Rel A ρ} {n} {f g : Fin n → A}
  → (∀ x → R (f x) (g x))
  → All₂ R (tabulate f) (tabulate g)
All₂-tabulate⁺ {n = zero} p = []
All₂-tabulate⁺ {n = suc n} p = p zero ∷ All₂-tabulate⁺ (λ x → p (suc x))

All₂-tabulate⁻ : ∀ {α} {A : Set α} {ρ} {R : Rel A ρ} {n} {f g : Fin n → A}
  → All₂ R (tabulate f) (tabulate g)
  → ∀ x → R (f x) (g x)
All₂-tabulate⁻ [] ()
All₂-tabulate⁻ (fzRgz ∷ all) zero = fzRgz
All₂-tabulate⁻ (fzRgz ∷ all) (suc x) = All₂-tabulate⁻ all x

ext: agda

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
{-# OPTIONS --safe #-}
module Cubical.Functions.Implicit where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

implicit≃Explicit : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
  → ({a : A} → B a) ≃ ((a : A) → B a)
implicit≃Explicit = isoToEquiv isom
  where
  isom : Iso _ _
  Iso.fun isom f a = f
  Iso.inv isom f = f _
  Iso.rightInv isom f = funExt λ _ → refl
  Iso.leftInv isom f = implicitFunExt refl

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module hello-world-dep where

open import Data.Nat using (ℕ; zero; suc)

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

infixr 5 _∷_

max_stars_repo_name: avieor/agda-demos

max_issues_repo_name: avieor/agda-demos

max_forks_repo_name: avieor/agda-demos


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

open import Base

module Homotopy.PushoutDef where

record pushout-diag (i : Level) : Set (suc i) where
  constructor diag_,_,_,_,_
  field
    A : Set i
    B : Set i
    C : Set i
    f : C → A
    g : C → B

pushout-diag-raw-eq : ∀ {i} {A A' : Set i} (p : A ≡ A')
  {B B' : Set i} (q : B ≡ B') {C C' : Set i} (r : C ≡ C')
  {f : C → A} {f' : C' → A'} (s : f' ◯ transport _ r ≡ transport _ p ◯ f)
  {g : C → B} {g' : C' → B'} (t : transport _ q ◯ g ≡ g' ◯ transport _ r)
  → (diag A , B , C , f , g) ≡ (diag A' , B' , C' , f' , g')
pushout-diag-raw-eq refl refl refl refl refl = refl

pushout-diag-eq : ∀ {i} {A A' : Set i} (p : A ≃ A')
  {B B' : Set i} (q : B ≃ B') {C C' : Set i} (r : C ≃ C')
  {f : C → A} {f' : C' → A'} (s : (a : C) →  f' (π₁ r a) ≡ (π₁ p) (f a))
  {g : C → B} {g' : C' → B'} (t : (b : C) → (π₁ q) (g b) ≡ g' (π₁ r b))
  → (diag A , B , C , f , g) ≡ (diag A' , B' , C' , f' , g')
pushout-diag-eq p q r {f} {f'} s {g} {g'} t = pushout-diag-raw-eq
  (eq-to-path p)
  (eq-to-path q)
  (eq-to-path r)
  (funext (λ a → ap f' (trans-id-eq-to-path r a)
                     ∘ (s a ∘ ! (trans-id-eq-to-path p (f a)))))
  (funext (λ b → trans-id-eq-to-path q (g b)
                     ∘ (t b ∘ ap g' (! (trans-id-eq-to-path r b)))))

module Pushout {i} {d : pushout-diag i} where

  open pushout-diag d

  private
    data #pushout : Set i where
      #left : A → #pushout
      #right : B → #pushout

  pushout : Set _
  pushout = #pushout

  left : A → pushout
  left = #left

  right : B → pushout
  right = #right

  postulate  -- HIT
    glue : (c : C) → left (f c) ≡ right (g c)

  pushout-rec : ∀ {l} (P : pushout → Set l) (left* : (a : A) → P (left a))
    (right* : (b : B) → P (right b))
    (glue* : (c : C) → transport P (glue c) (left* (f c)) ≡ right* (g c))
    → (x : pushout) → P x
  pushout-rec P left* right* glue* (#left y) = left* y
  pushout-rec P left* right* glue* (#right y) = right* y

  postulate  -- HIT
    pushout-β-glue : ∀ {l} (P : pushout → Set l) (left* : (a : A) → P (left a))
      (right* : (b : B) → P (right b))
      (glue* : (c : C) → transport P (glue c) (left* (f c)) ≡ right* (g c))
      (c : C)
        → apd (pushout-rec {l} P left* right* glue*) (glue c) ≡ glue* c

  pushout-rec-nondep : ∀ {l} (D : Set l) (left* : A → D) (right* : B → D)
    (glue* : (c : C) → left* (f c) ≡ right* (g c)) → (pushout → D)
  pushout-rec-nondep D left* right* glue* (#left y) = left* y
  pushout-rec-nondep D left* right* glue* (#right y) = right* y

  postulate  -- HIT
    pushout-β-glue-nondep : ∀ {l} (D : Set l) (left* : A → D) (right* : B → D)
      (glue* : (c : C) → left* (f c) ≡ right* (g c)) (c : C)
      → ap (pushout-rec-nondep D left* right* glue*) (glue c) ≡ glue* c

open Pushout public hiding (pushout)

pushout : ∀ {i} (d : pushout-diag i) → Set i
pushout d = Pushout.pushout {_} {d}

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- {-# OPTIONS -v tc.term.exlam:100 -v extendedlambda:100 -v int2abs.reifyterm:100 -v tc.with:100 -v tc.mod.apply:100 #-}
module Issue778b (Param : Set) where

open import Issue778M Param

data D : (Nat → Nat) → Set where
  d : D pred → D pred

-- Ulf, 2013-11-11: With the fix to issue 59 that inlines with functions,
-- this no longer termination checks. The problem is having a termination
-- path going through a with-expression (the variable x in this case).
{-# TERMINATING #-}
test : (f : Nat → Nat) → D f → Nat
test .pred (d x) = bla
  where bla : Nat
        bla with (d x)  -- Andreas, 2014-11-06 "with x" has been outlawed.
        ... | (d (d y)) = test pred y


text:
{-# OPTIONS --exact-split #-}

module ExactSplitParity where

data Bool : Set where
  true false : Bool

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

parity : ℕ → ℕ → Bool
parity zero          zero          = true
parity zero          (suc zero)    = false
parity zero          (suc (suc n)) = parity zero n
parity (suc zero)    zero          = false
parity (suc (suc m)) zero          = parity m zero
parity (suc m)       (suc n)       = parity m n

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Data.Fin.Subset.Disjoint.Properties where

open import Data.Nat
open import Data.Vec as Vec hiding (_++_; _∈_)
open import Data.List as List hiding (zipWith; foldr)
open import Data.Bool
open import Data.Bool.Properties
open import Data.Product
open import Data.Sum
open import Data.Empty hiding (⊥)
open import Relation.Binary.PropositionalEquality

open import Data.Fin hiding (_-_)
open import Data.Fin.Subset
open import Data.Fin.Subset.Properties
open import Data.Fin.Subset.Disjoint

module _ where

  _-_ : ∀ {n} → (l r : Subset n) → Subset n
  l - r = zipWith _⊝_ l r
    module Subtract where
      _⊝_ = (λ l r → if r then false else l)

  q-p∪p : ∀ {n}{p q : Subset n} → q ⊆ p → (p - q) ∪ q ≡ p
  q-p∪p {p = []} {[]} s = refl
  q-p∪p {p = x ∷ p} {outside ∷ q} s rewrite ∨-identityʳ x =
    cong₂ _∷_ refl (q-p∪p (drop-∷-⊆ s))
  q-p∪p {p = outside ∷ p} {true ∷ q} s with s here
  ... | ()
  q-p∪p {p = true ∷ p} {true ∷ q} s = cong₂ _∷_ refl (q-p∪p (drop-∷-⊆ s))

  ⊆-∪-cong : ∀ {n}{x y x' y' : Subset n} → x ⊆ x' → y ⊆ y' → (x ∪ y) ⊆ (x' ∪ y')
  ⊆-∪-cong p q t with x∈p∪q⁻ _ _ t
  ... | inj₁ z = p⊆p∪q _ (p z)
  ... | inj₂ z = q⊆p∪q _ _ (q z)

-- properties of disjoint subsets x ◆ y
module _ where

  ◆-tail : ∀ {n} x y {xs ys : Subset n} → (x ∷ xs) ◆ (y ∷ ys) → xs ◆ ys
  ◆-tail _ _ p (x , x∈xs) = p (suc x , there x∈xs)

  ◆-comm : ∀ {n} {x y : Subset n} → x ◆ y → y ◆ x
  ◆-comm {x = x}{y} = subst Empty (∩-comm x y)

  ◆-⊆-left : ∀ {n}{x y z : Subset n} → x ⊆ y → y ◆ z → x ◆ z
  ◆-⊆-left w d (e , e∈x∩z) = let (e∈x , e∈z) = (x∈p∩q⁻ _ _ e∈x∩z) in d (e , x∈p∩q⁺ ((w e∈x) , e∈z))

  ◆-⊆-right : ∀ {n}{x y z : Subset n} → x ⊆ z → y ◆ z → y ◆ x
  ◆-⊆-right w d = ◆-comm (◆-⊆-left w (◆-comm d))

  ◆-∉ : ∀ {n}{x y : Subset n}{i} → x ◆ y → i ∈ x → i ∉ y
  ◆-∉ {y = outside ∷ y} p here = λ ()
  ◆-∉ {y = inside ∷ y} p here = λ _ → p (zero , here)
  ◆-∉ {y = _ ∷ ys} p (there {y = y} q) (there z) =
    ◆-∉ (λ where (i , i∈ys) → p (suc i , there i∈ys)) q z

  ⊆-◆ : ∀ {n}{x y z : Subset n} → x ⊆ y → x ◆ z → x ⊆ y - z
  ⊆-◆ {x = .(true ∷ _)} {_ ∷ _} {outside ∷ zs} p x◆z here with p here
  ... | here = here
  ⊆-◆ {x = .(true ∷ _)} {_ ∷ _} {inside  ∷ zs} p x◆z here = ⊥-elim (◆-∉ x◆z here here)
  ⊆-◆ {x = .(_ ∷ _)} {y ∷ ys} {z ∷ zs} p x◆z (there i∈x) =
    there (⊆-◆ (drop-∷-⊆ p) (◆-tail _ z x◆z) i∈x)

  ◆-∪ : ∀ {n}{x y z : Subset n} → x ◆ y → x ◆ z → x ◆ (y ∪ z)
  ◆-∪ x◆y x◆z (i , i∈x∩y∪z) with x∈p∪q⁻ _ _ (proj₂ (x∈p∩q⁻ _ _ i∈x∩y∪z))
  ... | inj₁ i∈y = x◆y (i , (x∈p∩q⁺ (proj₁ (x∈p∩q⁻ _ _ i∈x∩y∪z) , i∈y)))
  ... | inj₂ i∈z = x◆z (i , (x∈p∩q⁺ (proj₁ (x∈p∩q⁻ _ _ i∈x∩y∪z) , i∈z)))

  ◆-- : ∀ {n}(x y : Subset n) → x ◆ (y - x)
  ◆-- xs ys (zero , p) with x∈p∩q⁻ _ _ p
  ◆-- (.true ∷ _) (outside ∷ _) (zero , p) | here , ()
  ◆-- (.true ∷ _) (true ∷ _)    (zero , p) | here , ()
  ◆-- (_ ∷ xs) (_ ∷ ys) (suc e , there p) = ◆-- xs ys (e , p)

  ◆-⊥ : ∀ {n} {x : Subset n} → x ◆ ⊥
  ◆-⊥ (i , snd) = ∉⊥ (subst (λ s → i ∈ s) (proj₂ ∩-zero _) snd)

-- properties of disjoint unions z of xs (xs ⨄ z)
module _ where

  -- append for disjoint disjoint-unions of subsets
  ++-⨄ : ∀ {n}{xs ys}{x y : Subset n} → xs ⨄ x → ys ⨄ y → (x ◆ y) → (xs ++ ys) ⨄ (x ∪ y)
  ++-⨄ {x = x}{y} [] q d rewrite ∪-identityˡ y = q
  ++-⨄ {y = y} (_∷_ {x = x}{z} x◆z xs⊎y) ys⊎z x∪z⊎y rewrite ∪-assoc x z y =
    (◆-∪ x◆z (◆-⊆-left (p⊆p∪q z) x∪z⊎y)) ∷ (++-⨄ xs⊎y ys⊎z (◆-⊆-left (q⊆p∪q x z) x∪z⊎y))

  ⨄-trans : ∀ {n}{xs ys}{x y : Subset n} → xs ⨄ x → (x ∷ ys) ⨄ y → (xs ++ ys) ⨄ (x ∪ y)
  ⨄-trans {x = x}{y} xs▰x (_∷_ {y = z} x◆y ys▰y) rewrite sym (∪-assoc x x z) =
    subst (λ x → _ ⨄ (x ∪ z)) (sym (∪-idem x)) (++-⨄ xs▰x ys▰y x◆y)


text:
------------------------------------------------------------------------------
-- The FOTC streams of total natural numbers type
------------------------------------------------------------------------------

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

-- N.B. This module is re-exported by FOTC.Data.Stream.

module FOT.FOTC.Data.Nat.Stream.Type where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- The FOTC streams type (co-inductive predicate for total streams).

-- Functional for the StreamN predicate.
-- StreamNF : (D → Set) → D → Set
-- StreamNF P ns = ∃[ n' ] ∃[ ns' ] N n' ∧ P ns' ∧ ns ≡ n' ∷ ns'

-- Stream is the greatest fixed-point of StreamF (by Stream-out and
-- Stream-coind).

postulate StreamN : D → Set

postulate
-- StreamN is a post-fixed point of StreamNF, i.e.
--
-- StreamN ≤ StreamNF StreamN.
  StreamN-out : ∀ {ns} → StreamN ns →
                ∃[ n' ] ∃[ ns' ] N n' ∧ StreamN ns' ∧ ns ≡ n' ∷ ns'
{-# ATP axiom StreamN-out #-}

-- StreamN is the greatest post-fixed point of StreamNF, i.e.
--
-- ∀ P. P ≤ StreamNF P ⇒ P ≤ StreamN.
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  StreamN-coind :
    ∀ (A : D → Set) {ns} →
    -- A is post-fixed point of StreamNF.
    (A ns → ∃[ n' ] ∃[ ns' ] N n' ∧ A ns' ∧ ns ≡ n' ∷ ns') →
    -- StreamN is greater than A.
    A ns → StreamN ns

-- Because a greatest post-fixed point is a fixed-point, then the
-- StreamN predicate is also a pre-fixed point of the functional
-- StreamNF, i.e.
--
-- StreamNF StreamN ≤ StreamN.
StreamN-in : ∀ {ns} →
             ∃[ n' ] ∃[ ns' ] N n' ∧ StreamN ns' ∧ ns ≡ n' ∷ ns' →
             StreamN ns
StreamN-in {ns} h = StreamN-coind A h' h
  where
  A : D → Set
  A ns = ∃[ n' ] ∃[ ns' ] N n' ∧ StreamN ns' ∧ ns ≡ n' ∷ ns'

  h' : A ns → ∃[ n' ] ∃[ ns' ] N n' ∧ A ns' ∧ ns ≡ n' ∷ ns'
  h' (_ , _ , Nn' , SNns' , prf) = _ , _ , Nn' , (StreamN-out SNns') , prf

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Data.Bool.Truth where

open import Data.Empty
open import Data.Unit
open import Level
open import Data.Bool.Base

T : Bool → Type
T true  = ⊤
T false = ⊥

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Examples involving simple λ-calculi
------------------------------------------------------------------------

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

module README.Lambda where

------------------------------------------------------------------------
-- An untyped λ-calculus with constants

-- Some developments from "Operational Semantics Using the Partiality
-- Monad" by Danielsson, implemented using both the quotient
-- inductive-inductive partiality monad, and the delay monad.
--
-- These developments to a large extent mirror developments in
-- "Coinductive big-step operational semantics" by Leroy and Grall.

-- The syntax of, and a type system for, the untyped λ-calculus with
-- constants.

import Lambda.Syntax

-- Most of a virtual machine.

import Lambda.Virtual-machine

-- A compiler.

import Lambda.Compiler

-- A definitional interpreter.

import Lambda.Partiality-monad.Inductive.Interpreter
import Lambda.Delay-monad.Interpreter

-- A type soundness result.

import Lambda.Partiality-monad.Inductive.Type-soundness
import Lambda.Delay-monad.Type-soundness

-- A virtual machine.

import Lambda.Partiality-monad.Inductive.Virtual-machine
import Lambda.Delay-monad.Virtual-machine

-- Compiler correctness.

import Lambda.Partiality-monad.Inductive.Compiler-correctness
import Lambda.Delay-monad.Compiler-correctness

------------------------------------------------------------------------
-- An untyped λ-calculus without constants

-- A variant of the development above. The development above uses a
-- well-scoped variant of the untyped λ-calculus with constants. This
-- development does not use constants. This means that the interpreter
-- cannot crash, so the type soundness result has been omitted.

import Lambda.Simplified.Syntax
import Lambda.Simplified.Virtual-machine
import Lambda.Simplified.Compiler
import Lambda.Simplified.Partiality-monad.Inductive.Interpreter
import Lambda.Simplified.Delay-monad.Interpreter
import Lambda.Simplified.Partiality-monad.Inductive.Virtual-machine
import Lambda.Simplified.Delay-monad.Virtual-machine
import Lambda.Simplified.Partiality-monad.Inductive.Compiler-correctness
import Lambda.Simplified.Delay-monad.Compiler-correctness

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module powerset where

open import level
open import list
open import bool
open import product
open import empty
open import unit
open import sum
open import eq
open import functions renaming (id to id-set) public

-- Extensionality will be used when proving equivalences of morphisms.
postulate ext-set : ∀{l1 l2 : level} → extensionality {l1} {l2}
-- These are isomorphisms, but Agda has no way to prove these as
-- equivalences.  They are consistent to adopt as equivalences by
-- univalence:
postulate ⊎-unit-r : ∀{X : Set} → (X ⊎ ⊥) ≡ X
postulate ⊎-unit-l : ∀{X : Set} → (⊥ ⊎ X) ≡ X
postulate ∧-unit : ∀{ℓ}{A : Set ℓ} → A ≡ ((⊤ {ℓ}) ∧ A)
postulate ∧-sym : ∀{ℓ}{A B : Set ℓ} → (A ∧ B) ≡ (B ∧ A)
postulate ∧-unit-r : ∀{ℓ}{A : Set ℓ} → A ≡ (A ∧ (⊤ {ℓ}))
postulate ∧-assoc : ∀{ℓ}{A B C : Set ℓ} →  (A ∧ (B ∧ C)) ≡ ((A ∧ B) ∧ C)

ℙ : {X : Set} → (X → 𝔹) → Set
ℙ {X} S = (X → 𝔹) → 𝔹

_∪_ : {X : Set}{S : X → 𝔹} → ℙ S → ℙ S → ℙ S
(s₁ ∪ s₂) x = (s₁ x) || (s₂ x)

_∩_ : {X : Set}{S : X → 𝔹} → ℙ S → ℙ S → ℙ S
(s₁ ∩ s₂) x = (s₁ x) && (s₂ x)

_×S_ : {X Y : Set} → (S₁ : X → 𝔹) → (S₂ : Y → 𝔹) →  (X × Y) → 𝔹
_×S_ S₁ S₂ (a , b) = (S₁ a) && (S₂ b)

π₁ : ∀{X Y : Set} → ((Σ X (λ x → Y) → 𝔹) → 𝔹) → ((X → 𝔹) → 𝔹)
π₁ P S = P (λ x → S (fst x))

π₂ : ∀{X Y : Set} → ((Σ X (λ x → Y) → 𝔹) → 𝔹) → ((Y → 𝔹) → 𝔹)
π₂ P S = P (λ x → S (snd x))

i₁ : {X Y : Set}{S₁ : X → 𝔹}{S₂ : Y → 𝔹} → ℙ S₁ → (((X × Y) → 𝔹) → 𝔹)
i₁ {X}{Y}{S₁}{S₂} P S = {!!}

i₂ : {X Y : Set}{S₁ : X → 𝔹}{S₂ : Y → 𝔹} → ℙ S₂ → ℙ (S₁ ×S S₂)
i₂ {X}{Y}{S₁}{S₂} P _ = P S₂

cp-ar : {X Y Z : Set}{S₁ : X → 𝔹}{S₂ : Y → 𝔹}{S₃ : Z → 𝔹} → (ℙ S₁ → ℙ S₃) → (ℙ S₂ → ℙ S₃) → ℙ (S₁ ×S S₂) → ℙ S₃
cp-ar {X}{Y}{Z}{S₁}{S₂}{S₃} f g P S = (f (π₁ P) S) || (g (π₂ P) S)

cp-diag₁ : {X Y Z : Set}{S₁ : X → 𝔹}{S₂ : Y → 𝔹}{S₃ : Z → 𝔹}{f : ℙ S₁ → ℙ S₃}{g : ℙ S₂ → ℙ S₃} → cp-ar {X}{Y}{Z}{S₁}{S₂}{S₃ = S₃} f g ∘ (i₁ {X}{Y}{S₁}{S₂}) ≡ f
cp-diag₁ {X}{Y}{Z}{S₁}{S₂}{S₃}{f}{g} = ext-set (λ {x} → ext-set (λ {S} → {!!}))

-- cp-diag₂ : {X Y Z : Set}{f : Z → X}{g : Z → Y} → cp-ar f g ∘ i₂ ≡ ℙₐ g
-- cp-diag₂ {X}{Y}{Z}{f}{g} = refl

-- co-curry : {A B C : Set} → ((A × B) → C) → ℙ (B → C) → ℙ A
-- co-curry {A}{B}{C} f = ℙₐ {A}{B → C} (curry f)

-- co-uncurry : {A B C : Set} → (A → B → C) → ℙ C → ℙ (A × B)
-- co-uncurry {A}{B}{C} f = ℙₐ {A × B} {C} (uncurry f)

-- liftℙ : {A B : Set} → (A → ℙ B) → ℙ A → ℙ B
-- liftℙ {A} f s b = ∀(a : A) → (s a) × (f a b)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module Numeral.Integer.Relation.Order where

open import Functional
import      Lvl
import      Numeral.Natural.Relation.Order as ℕ
open import Numeral.Integer
open import Numeral.Integer.Oper
open import Relator.Ordering
open import Type

-- Inequalities/Comparisons
data _≤_ : ℤ → ℤ → Type{Lvl.𝟎} where
  neg-neg : ∀{a b} → (a ℕ.≤ b) → (−𝐒ₙ(b)) ≤ (−𝐒ₙ(a))
  neg-pos : ∀{a b} → (−𝐒ₙ(a)) ≤ (+ₙ b)
  pos-pos : ∀{a b} → (a ℕ.≤ b) → (+ₙ a)   ≤ (+ₙ b)

_<_ : ℤ → ℤ → Type
_<_ = (_≤_) ∘ 𝐒

open From-[≤][<] (_≤_)(_<_) public

module _ where
  open import Structure.Relator.Properties

  instance
    [≤][−𝐒ₙ]-sub : (swap(_≤_) on₂ (−𝐒ₙ_)) ⊆₂ (ℕ._≤_)
    _⊆₂_.proof [≤][−𝐒ₙ]-sub (neg-neg p) = p

  instance
    [≤][+ₙ]-sub : ((_≤_) on₂ (+ₙ_)) ⊆₂ (ℕ._≤_)
    _⊆₂_.proof [≤][+ₙ]-sub (pos-pos p) = p

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:
module Data.Real.Base where

import Prelude
import Data.Rational
import Data.Nat as Nat
import Data.Bits
import Data.Bool
import Data.Maybe
import Data.Integer
import Data.List
import Data.Real.Gauge

open Prelude
open Data.Rational hiding (_-_; !_!)
open Data.Bits
open Data.Bool
open Data.List
open Data.Integer
       hiding   (-_; _+_; _≥_; _≤_; _>_; _<_; _==_)
       renaming ( _*_ to _*'_ )
open Nat using (Nat; zero; suc)
open Data.Real.Gauge using (Gauge)

Base  = Rational

bitLength : Int -> Int
bitLength x = pos (nofBits ! x !) - pos 1

approxBase : Base -> Gauge -> Base
approxBase x e = help err
  where
    num = numerator   e
    den = denominator e

    err = bitLength (den - pos 1) - bitLength num

    help : Int -> Base
    help (pos (suc n)) = round (x * fromNat k) % pos k
      where
        k = shiftL 1 (suc n)
    help (pos zero) = x
    help (neg n) = fromInt $ (round $ x / fromInt k) *' k
      where
        k = pos (shiftL 1 ! neg n !)

powers : Nat -> Base -> List Base
powers n x = iterate n (_*_ x) x

sumBase : List Base -> Base
sumBase xs = foldr _+_ (fromNat 0) xs

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text: module Structure.Topology.Proofs where