text:
open import Prelude renaming (_++_ to _++-List_)
open import Data.Maybe using (Maybe; just; nothing; maybe; From-just)
open import Data.Fin using (Fin; toℕ) renaming (inject+ to finject; raise to fraise; zero to fzero; suc to fsuc)
open import Data.List.All as A
open import Data.Vec using (Vec; _∷_; [])

open import Data.Nat renaming (decTotalOrder to decTotalOrder-ℕ)
open import Relation.Binary using (module DecTotalOrder)

module RW.Language.Instantiation where

  open import RW.Language.RTerm
  open import RW.Language.FinTerm

  --------------------------------------------------
  -- Monadic Boilerplate

  open import RW.Utils.Monads
  open Monad {{...}}

  _<$>_ : ∀{a b}{A : Set a}{B : Set b}
        → (A → B) → Maybe A → Maybe B
  _ <$> nothing  = nothing
  f <$> (just x) = just (f x)

  _<*>_ : ∀{a b}{A : Set a}{B : Set b}
        → Maybe (A → B) → Maybe A → Maybe B
  just f <*> just x = just (f x)
  _      <*> _      = nothing

  {-
  mapM : {A B : Set} → (A → Maybe B) → List A → Maybe (List B)
  mapM f = Prelude.foldr
           (λ a → maybe (λ x → flip _∷_ x <$> f a) nothing)
           (just [])
  -}

  -------------------------------------------------
  -- Partial Substitutions
  --
  --   The complexity annotations might require
  --   a slight notational introduction.
  --
  --   If a variable name overlaps one in the corresponding type signature,
  --   this is intentional.
  --
  --   Sₜ is defined by (S t), module RW.Language.RTermUtils.
  --   #Fvₜ is defined by length (Fv t), where Fv is also in RTermUtils.
  --

  X : ℕ → Set
  X = Vec (Maybe (RTerm ⊥))

  -- O(n)
  empty-X : {n : ℕ} → X n
  empty-X {zero}  = []
  empty-X {suc n} = nothing ∷ empty-X

  -- O(n)
  lookup-X : {n : ℕ} → Fin n → X n → Maybe (RTerm ⊥)
  lookup-X fz     (x ∷ _) = x
  lookup-X (fs i) (_ ∷ s) = lookup-X i s

  -- Let n be the number of free variables, and Sₜ be the size of our term t.
  -- We'll denote by #Fvₜ the number of free variables actually occuring in t.
  --
  -- O(Sₜ + n × # Fvₜ)
  --
  -- Still, on the average case, we can expect that each (i ∈ Fin n) will
  -- occur in a (FinTerm n), therefore # Fvₜ ≥ n. So, we have,
  --
  --             # Fvₜ ≥ n
  -- ⇒       n × # Fvₜ ≥ n²
  -- ⇒  Sₜ + n × # Fvₜ ≥ Sₜ + n²
  --
  -- For calculational purposes, then, we might consider that apply-X function
  -- have a complexity of O(n²).
  {-# TERMINATING #-}
  apply-X : {n : ℕ} → X n → FinTerm n → Maybe (RTerm ⊥)
  apply-X s (ovar x) = lookup-X x s
  apply-X s (ivar n) = just (ivar n)
  apply-X s (rlit l) = just (rlit l)
  apply-X s (rlam t) = rlam <$> apply-X s t
  apply-X s (rapp n ts) = rapp n <$> mapM (apply-X s) ts

  -- The worst case of extending a partial substitution is
  -- asking to extend the last index on an already defined
  -- term, that is, n recursive calls on the last branch and
  -- finishing on the branch marked (§). comparing (t ≟-RTerm u)
  -- is O(min(Sₜ , Sᵤ)).
  --
  -- Therefore,
  --
  -- O(n + min(Sₜ , Sᵤ))
  extend-X : {n : ℕ} → Fin n → RTerm ⊥ → X n → Maybe (X n)
  extend-X fz t (nothing ∷ s) = just (just t ∷ s)
  extend-X fz t (just t′ ∷ s) with t ≟-RTerm t′
  ...| yes _ = just (just t ∷ s) -- (§)
  ...| no  _ = nothing
  extend-X (fs i) t (mt ∷ s) = _∷_ mt <$> extend-X i t s

  ------------------------------
  -- * Instantiation

  -- Taking a close look to instAcc, we can see that the only real operation it performs
  -- is extend-X, on the first branch. The rest is pretty much traversing down the term
  -- with a possibility of failing (nothing).
  --
  -- Assuming (t : FinTerm n), Sₜ is the size of t and #Fvₜ is the number of
  -- free variables in t.
  --
  -- instAcc t j empty ∈ O(Sₜ + #Fvₜ × (n + min(Sₜ , Sⱼ)ᴬ ))
  --
  -- [ᴬ]: This is not really the size of t, but of the corresponding term sent to extend,
  --      which is ALWAYS smaller than or equal to Sₜ.
  --
  -- Without loss of generality, let's assume that the subterms of t are always
  -- smaller than their corresponding counterparts in j, allowing us
  -- to simplify min(Sₜ , Sⱼ) to Sₜ.
  --
  -- O(Sₜ + #Fvₜ × (n + Sₜ))
  -- O(Sₜ + #Fvₜ × Sₜ + #Fvₜ × n)
  -- O(Sₜ × (#Fvₜ + 1) + #Fvₜ × n)
  --
  -- Making the same assumption as before, that #Fvₜ ≈ n in the average scenario,
  --
  -- O(Sₜ × (n + 1) + n²)
  -- O(n² + Sₜ × n + Sₜ) ≈ O(n²).

  mutual
    instAcc : {n : ℕ} → FinTerm n → RTerm ⊥ → X n → Maybe (X n)
    instAcc (ovar x) t s = extend-X x t s
    {- we need to allow ivar's to match whatever. If we end up
       giving a false positive, Agda typechecker will spot it.

       TODO: maybe there's a better workaround, but it would require
             a re-engineering of our AST, by providing explicit and
             implicit ovar's. Or, a RTerm (A ⊎ A) would suffice.
    instAcc (ivar n) (ivar m) s with n ≟-ℕ m
    ...| yes _ = just s
    ...| no  _ = nothing
    -}
    instAcc (ivar _) _ s = just s
    instAcc (rlit l) (rlit k) s with l ≟-Lit k
    ...| yes _ = just s
    ...| no  _ = nothing
    instAcc (rlam t) (rlam u) s = instAcc t u s
    instAcc (rapp n ts) (rapp m us) s with n ≟-RTermName m
    ...| no  _ = nothing
    ...| yes _ = instAcc* ts us s
    instAcc _ _ _ = nothing

    instAcc* : {n : ℕ} → List (FinTerm n) → List (RTerm ⊥) → X n → Maybe (X n)
    instAcc* [] [] s = just s
    instAcc* [] (_ ∷ _) _ = nothing
    instAcc* (_ ∷ _) [] _ = nothing
    instAcc* (x ∷ xs) (y ∷ ys) s = instAcc x y s >>= instAcc* xs ys

  -- This is just a call to instAcc with an aditional n steps performed to generate
  -- empty-X.
  --
  -- Keeping our degree of freedom Sₜ, we have
  -- inst ∈ O(n² + (Sₜ + 1) × n + Sₜ)
  --
  inst : {n : ℕ} → FinTerm n → RTerm ⊥ → Maybe (X n)
  inst t u = instAcc t u empty-X

  ----------------------------------
  -- * Interface

  RSubst : Set
  RSubst = List (ℕ × RTerm ⊥)

  private
    X2RSubst0 : {n : ℕ} → X n → Maybe RSubst
    X2RSubst0 {.zero} []            = just []
    X2RSubst0 {suc n} (just x ∷ s)  = _∷_ (suc n , x) <$> X2RSubst0 s
    X2RSubst0 {suc _} (nothing ∷ _) = nothing

  X2RSubst : {n : ℕ} → X n → Maybe RSubst
  X2RSubst x = reverse <$> (X2RSubst0 x)

  _++ₓ_ : {n : ℕ} → X n → X n → Maybe (X n)
  []       ++ₓ []       = just []
  (x ∷ xs) ++ₓ (y ∷ ys) with x | y
  ...| nothing | just y' = _∷_ y <$> (xs ++ₓ ys)
  ...| just x' | nothing = _∷_ x <$> (xs ++ₓ ys)
  ...| nothing | nothing = nothing
  ...| just x' | just y' with x' ≟-RTerm y'
  ...| no _  = nothing
  ...| yes _ = _∷_ x <$> (xs ++ₓ ys)

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
{-

ℚ is a Field

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.Field.Instances.QuoQ where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Int.MoreInts.QuoInt
  using    (ℤ ; spos ; sneg ; pos ; neg ; signed ; posneg ; isSetℤ ; 0≢1-ℤ)
  renaming (_·_ to _·ℤ_ ; -_ to -ℤ_
           ; ·-zeroˡ to ·ℤ-zeroˡ
           ; ·-identityʳ to ·ℤ-identityʳ)
open import Cubical.HITs.SetQuotients as SetQuot
open import Cubical.HITs.Rationals.QuoQ
  using    (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)

open import Cubical.Algebra.Field
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRingSolver.Reflection
open import Cubical.Algebra.CommRing.Instances.QuoInt
open import Cubical.Algebra.CommRing.Instances.QuoQ

open import Cubical.Relation.Nullary

-- It seems there are bugs when applying ring solver to explicit ring.
-- The following is a work-around.
private
  module Helpers {ℓ : Level}(𝓡 : CommRing ℓ) where
    open CommRingStr (𝓡 .snd)

    helper1 : (x y : 𝓡 .fst) → (x · y) · 1r ≡ 1r · (y · x)
    helper1 = solve 𝓡

    helper2 : (x y : 𝓡 .fst) → ((- x) · (- y)) · 1r ≡ 1r · (y · x)
    helper2 = solve 𝓡

-- A rational number is zero if and only if its numerator is zero

a/b≡0→a≡0 : (x : ℤ × ℕ₊₁) → [ x ] ≡ 0 → x .fst ≡ 0
a/b≡0→a≡0 (a , b) a/b≡0 = sym (·ℤ-identityʳ a) ∙ a·1≡0·b ∙ ·ℤ-zeroˡ (ℕ₊₁→ℤ b)
  where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
        a·1≡0·b = effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ a/b≡0

a≡0→a/b≡0 : (x : ℤ × ℕ₊₁) → x .fst ≡ 0 → [ x ] ≡ 0
a≡0→a/b≡0 (a , b) a≡0 = eq/ _ _ a·1≡0·b
  where a·1≡0·b : a ·ℤ 1 ≡ 0 ·ℤ (ℕ₊₁→ℤ b)
        a·1≡0·b = (λ i → a≡0 i ·ℤ 1) ∙ ·ℤ-zeroˡ {s = spos} 1 ∙ sym (·ℤ-zeroˡ (ℕ₊₁→ℤ b))

-- ℚ is a field

open CommRingStr (ℚCommRing .snd)
open Units        ℚCommRing
open Helpers      ℤCommRing

hasInverseℚ : (q : ℚ) → ¬ q ≡ 0 → Σ[ p ∈ ℚ ] q · p ≡ 1
hasInverseℚ = SetQuot.elimProp (λ q → isPropΠ (λ _ → inverseUniqueness q))
  (λ x x≢0 → let a≢0 = λ a≡0 → x≢0 (a≡0→a/b≡0 x a≡0) in inv-helper x a≢0 , inv·-helper x a≢0)
  where
  inv-helper : (x : ℤ × ℕ₊₁) → ¬ x .fst ≡ 0 → ℚ
  inv-helper (signed spos (suc a) , b) _ = [ ℕ₊₁→ℤ b , 1+ a ]
  inv-helper (signed sneg (suc a) , b) _ = [ -ℤ ℕ₊₁→ℤ b , 1+ a ]
  inv-helper (signed spos zero , _) a≢0 = Empty.rec (a≢0 refl)
  inv-helper (signed sneg zero , _) a≢0 = Empty.rec (a≢0 (sym posneg))
  inv-helper (posneg i , _) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))

  inv·-helper : (x : ℤ × ℕ₊₁)(a≢0 : ¬ x .fst ≡ 0) → [ x ] · inv-helper x a≢0 ≡ 1
  inv·-helper (signed spos zero , b) a≢0 = Empty.rec (a≢0 refl)
  inv·-helper (signed sneg zero , b) a≢0 = Empty.rec (a≢0 (sym posneg))
  inv·-helper (posneg i , b) a≢0 = Empty.rec (a≢0 (λ j → posneg (i ∧ ~ j)))
  inv·-helper (signed spos (suc a) , b) _ = eq/ _ _ (helper1 (pos (suc a)) (ℕ₊₁→ℤ b))
  inv·-helper (signed sneg (suc a) , b) _ = eq/ _ _ (helper2 (pos (suc a)) (ℕ₊₁→ℤ b))

0≢1-ℚ : ¬ Path ℚ 0 1
0≢1-ℚ p = 0≢1-ℤ (effective (λ _ _ → isSetℤ _ _) isEquivRel∼ _ _ p)

-- The instance

ℚField : Field ℓ-zero
ℚField = makeFieldFromCommRing ℚCommRing hasInverseℚ 0≢1-ℚ

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Absurd where

open import Prelude

absurd : {A : Set} -> Empty -> A
absurd x = {!!}

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


text:
module Ethambda.Common where

open import Eth.Prelude

infixr 3 _<<_
infixr 3 _<d>_

export
_<d>_ : String -> String -> String
v <d> w =
  if isNullStr v
  then v
  else v ++ " " ++ " " ++ w

export
ShowS : Type
ShowS = String -> String

export
_<d_ : String -> ShowS -> ShowS
s <d c = (s <.>) . c

max_stars_repo_name: fredefox/ethambda-agda

max_issues_repo_name: fredefox/ethambda-agda

max_forks_repo_name: fredefox/ethambda-agda


text:
{-

The James Construction,
  also known as James Reduced Product

A very fundamental and useful construction in classical homotopy theory.
It can be seen as the free A∞-monoid constructed out of a given type,
namely the "correct higher version" of free monoid that is meaningful for all types,
instead of only h-Sets.

Referrence:
  Guillaume Brunerie,
  "The James construction and π₄(𝕊³) in homotopy type theory"
  (https://arxiv.org/abs/1710.10307)

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.James.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed

private
  variable
    ℓ ℓ' : Level

module _
  ((X , x₀) : Pointed ℓ) where

  infixr 5 _∷_

  -- The James Construction

  data James : Type ℓ where
    []   : James
    _∷_  : X → James → James
    unit : (xs : James) → xs ≡ x₀ ∷ xs

  James∙ : Pointed ℓ
  James∙ = James , []

-- Basic operations on James construction, imitating those in Cubical.Data.List.Base

module _
  {X∙@(X , x₀) : Pointed ℓ} where

  infixr 5 _++_
  infixl 5 _∷ʳ_

  [_] : X → James X∙
  [ x ] = x ∷ []

  _++_ : James X∙ → James X∙ → James X∙
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ xs ++ ys
  (unit xs i) ++ ys = unit (xs ++ ys) i

  ++₀ : (xs : James X∙) → xs ≡ xs ++ [ x₀ ]
  ++₀ [] = unit []
  ++₀ (x ∷ xs) i = x ∷ ++₀ xs i
  ++₀ (unit xs i) j = unit (++₀ xs j) i

  rev : James X∙ → James X∙
  rev [] = []
  rev (x ∷ xs) = rev xs ++ [ x ]
  rev (unit xs i) = ++₀ (rev xs) i

  _∷ʳ_ : James X∙ → X → James X∙
  xs ∷ʳ x = xs ++ x ∷ []

map : {X : Pointed ℓ}{Y : Pointed ℓ'} → (X →∙ Y) → James X → James Y
map f [] = []
map f (x ∷ xs) = f .fst x ∷ map f xs
map f (unit xs i) = (unit (map f xs) ∙ (λ i → f .snd (~ i) ∷ map f xs)) i

map∙ : {X : Pointed ℓ}{Y : Pointed ℓ'} → (X →∙ Y) → James∙ X →∙ James∙ Y
map∙ f .fst = map f
map∙ f .snd = refl


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

module Compilation.Data where

open import Context
open import Type.Core

open import Function
open import Data.Product
open import Data.List.Base

infixr 6 _⇒ᶜ_

{- Note [Type denotations]
The denotation of a System Fωμ type is an Agda type that somehow corresponds to the original type.
For System Fωμ types we'll be using simple and straightforward denotations. For example, we map

    π ⋆ (Var vz ⇒ Var vz)

to

    (A : Set) -> A -> A

and

    Lam (Var vz) ∙ (π ⋆ (Var vz ⇒ Var vz))

to

    (λ x -> x) ((A : Set) -> A -> A)

which computes to

    (A : Set) -> A -> A

The latter is due to the fact that we map System Fωμ lambdas to Agda lambdas and System Fωμ
applications to Agda applications and hence get type normalization of denotations for free.
-}

{- Note [Kind denotations]
Of course before taking denotations of System Fωμ types, we need to be able to take denotations
of System Fωμ kinds. We map a System Fωμ `⋆` to an Agda `Set` and a System Fωμ `_⇒ᵏ_` to an Agda
`_->_`. For example the denotation of

  (⋆ ⇒ᵏ ⋆) ⇒ᵏ ⋆

is

  (Set -> Set) -> Set
-}

-- | The Agda meaning of a kind.
⟦_⟧ᵏ : Kind -> Set
⟦ ⋆      ⟧ᵏ = Set
⟦ σ ⇒ᵏ τ ⟧ᵏ = ⟦ σ ⟧ᵏ -> ⟦ τ ⟧ᵏ

-- | The Agda meaning of a System Fωμ type in an environment.
evalᵗ : ∀ {Θ σ} -> Env ⟦_⟧ᵏ Θ -> Θ ⊢ᵗ σ -> ⟦ σ ⟧ᵏ
evalᵗ ρ (Var v) = lookupᵉ v ρ                      -- Look up a variable in the current context.
evalᵗ ρ (Lam β) = λ A -> evalᵗ (ρ ▷ A) β           -- Map a System Fωμ lambda to an Agda lambda.
evalᵗ ρ (φ ∙ α) = evalᵗ ρ φ (evalᵗ ρ α)            -- Map a System Fωμ application to an Agda application.
evalᵗ ρ (α ⇒ β) = evalᵗ ρ α -> evalᵗ ρ β           -- Map a System Fωμ arrow to an Agda arrow.
evalᵗ ρ (π σ β) = (A : ⟦ σ ⟧ᵏ) -> evalᵗ (ρ ▷ A) β  -- Map a System Fωμ `all` to an Agda `∀`.
evalᵗ ρ (μ ψ α) = IFix (evalᵗ ρ ψ) (evalᵗ ρ α)     -- Map a System Fωμ `ifix` to an Agda `IFix`.

-- | The Agda meaning of a closed System Fωμ type.
⟦_⟧ᵗ : ∀ {σ} -> Type⁽⁾ σ -> ⟦ σ ⟧ᵏ
⟦_⟧ᵗ = evalᵗ ∅

{- Note [Representing data types]
We represent a single data type as a list of constructor types. Each constructor type is defined in
a non-empty context where the first bound variable is for handling recursion and other variables are
parameters of the data type (there can be none). Each constructor type is a sequence of `_⇒ᶜ_`
that ends in `endᶜ` where `endᶜ` is a placeholder that will later be substituted either for
a type being defined or a type we eliminate the data type into or the unit type,
depending on how we denote constructors (there are multiple ways).

Consider the `list` data type. Its pattern functor binds two variables:

1. one responsible for recursion
2. one for the type of the elements stored in a list

Since we define constructors in contexts, the list constructors are defined in

    ε ▻ (⋆ ⇒ ⋆) ▻ ⋆

(the parens are for clarity, they're not really needed). The types of the constructors are

    1. List A                 -- The type of the `nil` constructor.
    2. A -> List A -> List A  -- The type of the `cons` constructor.

and we translate them to

    1. endᶜ
    2. Var vz ⇒ᶜ Var (vs vz) ∙ Var vz ⇒ᶜ endᶜ

A more interesting example is

    data InterList (A B : Set) : Set where
      InterNil  : InterList A B
      InterCons : A -> B -> InterList B A -> InterList A B

The types of its constructors are described as

    1. endᶜ
    2. Var (vs vz) ⇒ᶜ Var vz ⇒ᶜ Var (vs vs vz) ∙ Var vz ∙ Var (vs vz) ⇒ᶜ endᶜ

Below we define the data type that describes constructors and some basic functions over it.
-}

-- | The type of a constructor is of the `σ₁ ⇒ … ⇒ σₙ ⇒ end` form
-- where each `σ` is a type of kind `⋆`.
data Cons Θ : Set where
  endᶜ : Cons Θ
  _⇒ᶜ_ : (α : Star Θ) -> (ξ : Cons Θ) -> Cons Θ

-- | Convert the type of a constructor to an actual type of kind `⋆`.
--
-- > consToType (α₁ ⇒ᶜ … ⇒ᶜ αₙ ⇒ᶜ endᶜ) β = α₁ ⇒ … ⇒ αₙ ⇒ β
consToType : ∀ {Θ} -> Cons Θ -> Star Θ -> Star Θ
consToType  endᶜ    β = β
consToType (α ⇒ᶜ ξ) β = α ⇒ consToType ξ β

-- | Rename the type of a constructor.
renᶜ : ∀ {Θ Ξ} -> Θ ⊆ Ξ -> Cons Θ -> Cons Ξ
renᶜ ι  endᶜ    = endᶜ
renᶜ ι (α ⇒ᶜ ξ) = renᵗ ι α ⇒ᶜ renᶜ ι ξ

-- The family we use as an example in docs below.
module ProdTreeTree where
  mutual
    data ProdTree (A : Set) (B : Set) : Set where
      Prod : Tree (A × B) -> ProdTree A B

    data Tree (A : Set) : Set where
      Leaf : A -> Tree A
      Fork : ProdTree A A -> Tree A

  open import Data.Nat.Base
  open import Data.Bool.Base

  private
    example : ProdTree ℕ Bool
    example
      = Prod ∘ Fork ∘ Prod ∘ Fork ∘ Prod ∘ Leaf
      $ ( ( 0
          , false
          )
        , ( 1
          , true
          )
        )
      , ( ( 2
          , false
          )
        , (3
          , true
          )
        )

-- | A data description is parameterized by a context of contexts of kinds. Inner contexts are those
-- single data types are defined in. Outer contexts are needed in order to allow to define mutually
-- recursive data types. I.e. each element of an outer context is an inner context, in which
-- a single data type is defined.
--
-- A single data type is described as a list of described constructors. The context of each
-- constructor consists of
--
--   1. all the data types being defined (because we allow mutually recursive data types)
--   2. the particular inner context of the data type that the constructor constructs
--
-- For example, consider the `ProdTree`/`Tree` family of data types defined above
--
-- Since there are two data types in this family, the length of the outer context is 2.
-- Since `ProdTree` is parameterized by two types, it's inner context is `ε ▻ ⋆ ▻ ⋆`.
-- Since `Tree` is parameterized by one type, it's inner context is `ε ▻ ⋆`.
-- I.e. the context this whole family is defined in, is
--
-- > ε ▻ (ε ▻ ⋆ ▻ ⋆) ▻ (ε ▻ ⋆)
--
-- The context that the constructor of `ProdTree` is defined in, consists of
--
--     1. References to both `ProdTree` and `Tree` which have the `⋆ ⇒ᵏ ⋆ ⇒ᵏ ⋆` and  `⋆ ⇒ᵏ ⋆`
--        kinds respectively.
--     2. The inner context of `ProdTree` which has two parameters `A` and `B`, each of kind `⋆`.
--
-- hence the final context is
--
-- > ε ▻ {- ProdTree :: -} (⋆ ⇒ᵏ ⋆ ⇒ᵏ ⋆) ▻ {- Tree :: -} (⋆ ⇒ᵏ ⋆) ▻ {- A :: -} ⋆ ▻ {- B :: -} ⋆
--
-- (things in `{- … -}` are comments that assign names to variables for clarity).
--
-- Analogously, the context that the constructors of Tree` are defined in, is
--
-- > ε ▻ {- ProdTree :: -} (⋆ ⇒ᵏ ⋆ ⇒ᵏ ⋆) ▻ {- Tree :: -} (⋆ ⇒ᵏ ⋆) ▻ {- A :: -} ⋆
--
-- I.e. the same as the one of `ProdTree`, except we bind only one type parameter, because `Tree`
-- has only one type parameter.
record Data Ξ (Θs : Con Conᵏ) : Set where
  constructor PackData
  field constructors : Seq (λ Θ -> List (Cons (Ξ ▻▻ mapᶜ (λ Θᵢ -> conToKind Θᵢ ⋆) Θs ▻▻ Θ))) Θs

Data⁺ : Con Conᵏ -> Set
Data⁺ Θs = ∀ {Ξ} -> Data Ξ Θs

module prodTreeTree where
  -- The encoded `ProdTree`/`Tree` family from the above looks like this:
  -- (`∀ Q -> (A -> B -> Q) -> Q` is the Scott-encoded `A × B`)
  prodTreeTree : Data⁺ (ε ▻ (ε ▻ ⋆ ▻ ⋆) ▻ (ε ▻ ⋆))
  prodTreeTree
    = PackData
    $ ø
    ▶ ( -- `Tree (∀ Q -> (A -> B -> Q) -> Q) -> ProdTree A B`
        Var (vs vs vz) ∙ π ⋆ ((Var (vs vs vz) ⇒ Var (vs vz) ⇒ Var vz) ⇒ Var vz) ⇒ᶜ endᶜ
      ∷ []
      )
    ▶ ( -- `A -> Tree A`
        Var vz ⇒ᶜ endᶜ
      ∷ -- `ProdTree A A -> Tree A`
        Var (vs vs vz) ∙ Var vz ∙ Var vz ⇒ᶜ endᶜ
      ∷ []
      )

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
-- Issue reported by Christian Sattler on 2019-12-02

postulate
  M : Set
  m₀ : M
  D : Set
  d : D
  Y : (m : M) (a : D) → Set
  y : Y m₀ d
  R' : M → Set

data X : M → Set where
  conX : X m₀

R : M → Set
R = R'

postulate
  felt :
      (m : M)
      (f : X m → D)
      (g : (x : X m) → Y m (f x))
    → R m -- No error if R unfolded to R'.

module _ (m : M) where
  foo : R m
  foo = felt _ f g where
    f : X _ → D -- No error if signature of f given as _.
    f conX = d

    g : (x : X _) → Y _ (f x)
    g conX = y -- Accepted if y given as hole filler.

-- WAS: error:
--   d != f conX of type D
--   when checking that the expression y has type Y m₀ (f conX)
-- SHOULD: succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Functions used in googology

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

module Math.Googology.Function where

-- agda-stdlib
open import Data.Nat
open import Data.Nat.GeneralisedArithmetic
open import Function

-- Ackermann function.
-- ack m n = Ack(m, n)
ack : ℕ → ℕ → ℕ
ack 0       n       = 1 + n
ack (suc m) zero    = ack m 1
ack (suc m) (suc n) = ack m (ack (suc m) n)

-- Hyperoperation.
-- H n a b ≡ Hₙ(a, b)
H : ℕ → ℕ → ℕ → ℕ
H 0                     a b       = 1 + b
H 1                     a 0       = a
H 1                     a (suc b) = H 0 a (H 1 a b)
H 2                     a 0       = 0
H 2                     a (suc b) = H 1 a (H 2 a b)
H (suc (suc (suc _)))   a 0       = 1
H (suc n@(suc (suc _))) a (suc b) = H n a (H (suc n) a b)

-- Knuth's up-arrow notation.
-- a ↑[ n ] b =`a ↑ⁿ b`
_↑[_]_ : ℕ → ℕ → ℕ → ℕ
a ↑[ n ] b = H (2 + n) a b

infixr 8 _↑_ _↑↑_ _↑↑↑_ _↑↑↑↑_

-- Exponentiation.
_↑_ : ℕ → ℕ → ℕ
_↑_ a b = a ↑[ 1 ] b

-- Tetration.
_↑↑_ : ℕ → ℕ → ℕ
_↑↑_ a b = a ↑[ 2 ] b

-- Pentation.
_↑↑↑_ : ℕ → ℕ → ℕ
_↑↑↑_ a b = a ↑[ 3 ] b

-- Hexation.
_↑↑↑↑_ : ℕ → ℕ → ℕ
_↑↑↑↑_ a b = a ↑[ 4 ] b

-- Heptation.
_↑↑↑↑↑_ : ℕ → ℕ → ℕ
_↑↑↑↑↑_ a b = a ↑[ 5 ] b

-- Graham's number.
graham's-number : ℕ
graham's-number = go 64 where
  go : ℕ → ℕ
  go 0       = 4
  go (suc n) = 3 ↑[ go n ] 3

-- Fast-growing hierarchy
FGHℕ[_][_] : ℕ → ℕ → ℕ
FGHℕ[ zero  ][ x ] = suc x
FGHℕ[ suc n ][ x ] = fold x FGHℕ[ n ][_] x

FGHω : ℕ → ℕ
FGHω n = FGHℕ[ n ][ n ]


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise equality for containers
------------------------------------------------------------------------

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

module Data.Container.Relation.Binary.Pointwise where

open import Data.Product using (_,_; Σ-syntax; -,_; proj₁; proj₂)
open import Function
open import Level using (_⊔_)
open import Relation.Binary using (REL; _⇒_)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; subst; cong)

open import Data.Container.Core using (Container; ⟦_⟧)

-- Equality, parametrised on an underlying relation.

module _ {s p} (C : Container s p) where

  record Pointwise {x y e} {X : Set x} {Y : Set y} (R : REL X Y e)
                   (cx : ⟦ C ⟧ X) (cy : ⟦ C ⟧ Y) : Set (s ⊔ p ⊔ e) where
    constructor _,_
    field shape    : proj₁ cx ≡ proj₁ cy
          position : ∀ p → R (proj₂ cx p) (proj₂ cy (subst _ shape p))

module _ {s p} {C : Container s p} {x y} {X : Set x} {Y : Set y}
         {ℓ ℓ′} {R : REL X Y ℓ} {R′ : REL X Y ℓ′}
         where

  map : R ⇒ R′ → Pointwise C R ⇒ Pointwise C R′
  map R⇒R′ (s , f) = s , R⇒R′ ∘ f


text:
{-# OPTIONS --cubical #-}

F : Set → Set
F A = A

record R : Set₁ where
  field
    A : Set

r : Set → R
r A = λ where
  .R.A → A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module CF.Examples.Ex1 where

open import Function
open import Data.Bool
open import Data.Product
open import Data.List
open import Data.List.Relation.Unary.All
open import Data.Nat
open import Data.String

open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad.Possibly
open import Relation.Ternary.Data.Allstar
open import Relation.Ternary.Data.Bigstar hiding ([_])

open import CF.Types
open import CF.Syntax as Src
open import CF.Contexts.Lexical

open import JVM.Transform.Assemble
open import JVM.Printer
import JVM.Printer.Jasmin as J

ex₁ : Closed (Src.Block void)
ex₁ = (
  Src.while (
    Src.bool true ∙⟨ ∙-idˡ ⟩ Src.block
    -- int j = true
    (Src.bool true ≔⟨ ∙-idˡ ⟩ Possibly.possibly ∼-all (
      Src.ifthenelse
        -- if j
        (var
          ∙⟨ overlaps ∙-idˡ ⟩
          -- then
          Src.block (
            -- int i = j
            var ≔⟨ consˡ ∙-idˡ ⟩
            Possibly.possibly ∼-all (
              -- j := j
              Src.asgn (vars ∙⟨ overlaps ∙-idˡ ⟩ var) ⍮⟨ ∙-idʳ ⟩
              Src.run unit ⍮⟨ ∙-idʳ ⟩
              emp))
          -- else
          ∙⟨ overlaps ∙-idˡ ⟩
          Src.block (
            -- int i = j
            var ≔⟨ consˡ ∙-idˡ ⟩
            Possibly.possibly ∼-none (
              Src.run unit ⍮⟨ ∙-idʳ ⟩
              emp))
          )
        Src.⍮⟨ ∙-idʳ ⟩ emp
    ))) Src.⍮⟨ ∙-idʳ ⟩ emp)

open import IO as IO
open import Codata.Musical.Notation

open import CF.Compile

main = IO.run (putStrLn test)
  where
    test = Show.showBytecode $ proj₂ $ exec-extractor $ extract (proj₂ $ compile ex₁)

-- Uncomment this instead of the above main to output Jasmin code.
-- You can assemble this using Jasmin so that you can run the output with java.
-- Disclaimer: the jasmin compiler pass is not verified.
-- main = IO.run (putStrLn (J.unlines $ J.Jasmin.out proc))
--   where
--   proc = procedure "ex1" (proj₂ $ compile ex₁)


text:
{-# OPTIONS --prop --allow-unsolved-metas #-}

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

data _≃_ {α}{A : Set α}(a : A) : ∀ {B} → B → Prop where
  refl̃ : a ≃ a

data ⊥ : Set where

data Con  : Set
data Con~ : Con → Con → Prop
data Ty   : Con → Set
data Ty~  : ∀ {Γ₀ Γ₁} → Con~ Γ₀ Γ₁ → Ty Γ₀ → Ty Γ₁ → Prop

data Con where
data Con~ where

data Ty where
  U  : ∀ {Γ} → Ty Γ

data Ty~ where
  U~  : ∀ {Γ₀ Γ₁ Γ₀₁} → Ty~ {Γ₀}{Γ₁} Γ₀₁ U U

Conᴹ  : Con → Set
Con~ᴹ : ∀ {Γ₀ Γ₁} → Con~ Γ₀ Γ₁ → Conᴹ Γ₀ ≡ Conᴹ Γ₁
Tyᴹ   : ∀ {Γ} → Ty Γ → Conᴹ Γ → Set
Ty~ᴹ  : ∀ {Γ₀ Γ₁ Γ₀₁ A₀ A₁} → Ty~ {Γ₀}{Γ₁} Γ₀₁ A₀ A₁ → Tyᴹ A₀ ≃ Tyᴹ A₁
Conᴹ  ()
Con~ᴹ ()

Tyᴹ U γ = ⊥

-- offending line: if I comment this out, the internal error goes away
-- If I use Set instead of Prop everywhere, the error also goes away
Ty~ᴹ U~ = {!!}


text:
module PushArgument where
open import ScopeState
open import Data.List.NonEmpty
open import Data.List
open import ParseTree
open import Data.Nat
open import AgdaHelperFunctions
open import Data.Unit
open import Data.String hiding (toVec)
open import Data.Bool
open import Data.Product
open import Data.Maybe
open import ExpressionChanging hiding (makeInstruction)
open import ParseTreeOperations
open import Data.Vec hiding (_>>=_)
open import Data.Fin
open import Relation.Nullary
open import Data.Nat.Properties
open import Data.String using (_++_)

data ArgType : Set where
  explicit : ArgType
  present : ArgType
  absent : ArgType
-- if matches is false then an expected implicit argument has been omitted
matches : Expr -> Expr -> ArgType
matches expectedType argument
  with isImplicit expectedType | isImplicit argument
matches expectedType argument | false | false = explicit
--expected explicit but found implicit, actually an error
matches expectedType argument | false | true = explicit
matches expectedType argument | true | false = absent
matches expectedType argument | true | true = present
-- n is the argument to be pushed, so there must be another argument to switch
-- it with
makeIns : {n : ℕ} -> Vec Expr (suc n) -> Fin n -> (List Expr -> List Expr)
makeIns (x ∷ x₁) _ [] = []
makeIns (x ∷ y ∷ list) zero (z ∷ []) with matches x z
makeIns (x ∷ y ∷ list) zero (z ∷ []) | explicit = newHole ∷ []
makeIns (x ∷ y ∷ list) zero (z ∷ []) | present = implicit newHole ∷ []
makeIns (x ∷ y ∷ list) zero (z ∷ []) | absent with matches y z
makeIns (x ∷ y ∷ list) zero (z ∷ []) | absent | explicit = newHole ∷ []
makeIns (x ∷ y ∷ list) zero (z ∷ []) | absent | present = z ∷ []
makeIns (x ∷ y ∷ list) zero (z ∷ []) | absent | absent = z ∷ []
makeIns (a ∷ b ∷ list) zero (y ∷ z ∷ list2) with
  matches a y
makeIns (a ∷ b ∷ list) zero (y ∷ z ∷ list2) | absent = y ∷ z ∷ list2
makeIns (a ∷ b ∷ list) zero (y ∷ z ∷ list2) | _ with matches b z
makeIns (a ∷ b ∷ list) zero (y ∷ z ∷ list2) | _ | explicit = z ∷ y ∷ list2
makeIns (a ∷ b ∷ list) zero (y ∷ z ∷ list2) | _ | present = z ∷ y ∷ list2
makeIns (a ∷ b ∷ list) zero (y ∷ z ∷ list2) | _ | absent = y ∷ z ∷ list2
makeIns (x ∷ x₁) (suc n) (y ∷ list) with matches x y
makeIns (x ∷ x₁) (suc n) (y ∷ list) | explicit = y ∷ makeIns x₁ n list
makeIns (x ∷ x₁) (suc n) (y ∷ list) | present = y ∷ makeIns x₁ n list
makeIns (x ∷ x₁) (suc n) (y ∷ list) | absent = makeIns x₁ n (y ∷ list)

makeInstruction : TypeSignature -> ℕ -> (makeIns : {n : ℕ} -> Vec Expr (suc n) -> Fin n -> (List Expr -> List Expr)) -> ScopeState (List⁺ Expr -> List⁺ Expr)
makeInstruction (typeSignature funcName funcType) argNo f
  with toVec (typeToList funcType)
... | c = do
    newFin <- makeFin2 c argNo
    return $ function $ f c newFin
    where function : (List Expr -> List Expr) -> (List⁺ Expr -> List⁺ Expr)
          function f (ident identifier₁ ∷ tail₁)
              with sameId identifier₁ funcName
          function f (ident identifier₁ ∷ tail₁) | false =
            (ident identifier₁ ∷ tail₁)
          function f (ident identifier₁ ∷ tail₁) | true =
              ident identifier₁ ∷ f tail₁
          function f list = list

pushInstruction : TypeSignature -> ℕ -> ScopeState (List⁺ Expr -> List⁺ Expr)
pushInstruction t n = makeInstruction t n makeIns

--Data.List.NonEmpty.fromVec
pushTypeIfApplicable : {n : ℕ} -> Vec Expr (suc n)  -> Fin n -> ScopeState (Vec Expr (suc n))
pushTypeIfApplicable (namedArgument (typeSignature funcName funcType) {b} {bef1} {aft1} ∷ namedArgument (typeSignature funcName₁ funcType₁) {b2} {bef2} {aft2} ∷ v) zero =
        if sameName funcName funcName₁
         then fail "Can't switch two arguments of the same name, to avoid anything changing meaning"
         else if funcName doesNotAppearInExp funcType₁
                then (return $  namedArgument (typeSignature funcName₁ funcType₁) {b2} {bef2} {aft2} ∷ namedArgument (typeSignature funcName funcType) {b} {bef1} {aft1} ∷ v)
                else fail "The next argument depends on the one being pushed"
pushTypeIfApplicable (namedArgument (typeSignature funcName funcType) {b} {bef} {aft} ∷ x ∷ v) zero = if funcName doesNotAppearInExp x
                      then return $  x ∷ namedArgument (typeSignature funcName funcType) {b} {bef} {aft} ∷ v
                      else fail "The next argument depends on the one being pushed"
pushTypeIfApplicable (x ∷ x₁ ∷ v) zero = return $  x₁ ∷ x ∷ v
pushTypeIfApplicable (x ∷ v) (suc f) = do
        newRest <- pushTypeIfApplicable v f
        return $ x ∷ newRest

pushArgument : List ParseTree -> (funcID : ℕ) -> (whichArgument : ℕ) -> ScopeState (List ParseTree)
pushArgument code funcId whichArgument = doForArgument code funcId whichArgument pushTypeIfApplicable pushInstruction


text:
-- {-# OPTIONS -v tc.cover.splittree:10 -v tc.cc.splittree:10  #-}
module Issue106 where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ -> ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

_+_ : ℕ -> ℕ -> ℕ
zero + m = m
suc n + m = suc (n + m)

record ⊤ : Set where

data C : ℕ -> Set where
  c : C 0

data D : Set where
  d : forall s (x : C s) (xs : D) -> D

f : D -> ℕ -> ⊤
f (d zero c x) (suc n) = f (d 0 c x) n
f (d .zero c x) n      = f x (suc n)

g : D -> ℕ -> ⊤
g (d .zero c x) (suc n) = g (d zero c x) n
g (d .zero c x) n       = g x (suc n)

h : D -> ℕ -> ⊤
h (d .zero c x) (suc n) = h (d 0 c x) n
h (d .zero c x) n       = h x (suc n)

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Data where

data D
  (A : Set)
  : Set

data D A
  where

  c
    : D A

data E
  (B : Set)
  : Set
  where

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


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

module WithoutK10 where

data Unit : Set where
  unit : Unit

data D {A : Set} (f : Unit → A) : A → Set where
  d : ∀ {x} → D f x

Foo : ∀ {A} {x : A} → D (let f = λ { unit → x } in f) x → Set₁
Foo d = Set


text:
{-

Index a structure S by the type variable: X ↦ X → S X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Relational.UnaryOp where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Foundations.Univalence
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.Relation.Binary.Base
open import Cubical.Relation.ZigZag.Base
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.PropositionalTruncation as Trunc

open import Cubical.Structures.NAryOp

private
  variable
    ℓ ℓ₁ ℓ₁' : Level

-- Structured relations

preservesSetsUnaryFun : {S : Type ℓ → Type ℓ₁}
  → preservesSets S → preservesSets (NAryFunStructure 1 S)
preservesSetsUnaryFun p setX = isSetΠ λ _ → p setX

UnaryFunRelStr : {S : Type ℓ → Type ℓ₁} {ℓ₁' : Level}
  → StrRel S ℓ₁' → StrRel (NAryFunStructure 1 S) (ℓ-max ℓ ℓ₁')
UnaryFunRelStr ρ R f g =
  ∀ {x y} → R x y → ρ R (f x) (g y)

open BinaryRelation
open isEquivRel
open isQuasiEquivRel
open SuitableStrRel

private
  composeWith[_] : {A : Type ℓ} (R : EquivPropRel A ℓ)
    → compPropRel (R .fst) (quotientPropRel (R .fst .fst)) .fst ≡ graphRel [_]
  composeWith[_] R =
    funExt₂ λ a t →
    hPropExt squash (squash/ _ _)
      (Trunc.rec (squash/ _ _) (λ {(b , r , p) → eq/ a b r ∙ p }))
      (λ p → ∣ a , R .snd .reflexive a , p ∣)

unaryFunSuitableRel : {S : Type ℓ → Type ℓ₁} (p : preservesSets S) {ρ : StrRel S ℓ₁'}
  → SuitableStrRel S ρ
  → SuitableStrRel (NAryFunStructure 1 S) (UnaryFunRelStr ρ)
unaryFunSuitableRel pres {ρ} θ .quo (X , f) R h .fst =
  f₀ ,
  λ {x} → J (λ y p → ρ (graphRel [_]) (f x) (f₀ y)) (θ .quo (X , f x) R (href x) .fst .snd)
  where
  href = h ∘ R .snd .reflexive

  f₀ : _
  f₀ [ x ] = θ .quo (X , f x) R (href x) .fst .fst
  f₀ (eq/ x₀ x₁ r i) = path i
    where
    path : θ .quo (X , f x₀) R (href x₀) .fst .fst ≡ θ .quo (X , f x₁) R (href x₁) .fst .fst
    path =
      cong fst
        (θ .quo (X , f x₀) R (href x₀) .snd
          ( θ .quo (X , f x₁) R (href x₁) .fst .fst
          , subst
            (λ T → ρ T (f x₀) (θ .quo (X , f x₁) R (href x₁) .fst .fst))
            (composeWith[_] R)
            (θ .transitive (R .fst) (quotientPropRel (R .fst .fst))
              (h r)
              (θ .quo (X , f x₁) R (href x₁) .fst .snd))
          ))
  f₀ (squash/ _ _ p q j i) =
    pres squash/ _ _ (cong f₀ p) (cong f₀ q) j i
unaryFunSuitableRel pres {ρ} θ .quo (X , f) R h .snd (f' , c) =
  Σ≡Prop
    (λ _ → isPropImplicitΠ λ _ → isPropImplicitΠ λ _ → isPropΠ λ _ →
      θ .prop (λ _ _ → squash/ _ _) _ _)
    (funExt
      (elimProp (λ _ → pres squash/ _ _)
        (λ x → cong fst (θ .quo (X , f x) R (href x) .snd (f' [ x ] , c refl)))))
  where
  href = h ∘ R .snd .reflexive
unaryFunSuitableRel pres {ρ} θ .symmetric R h {x} {y} r = θ .symmetric R (h r)
unaryFunSuitableRel pres {ρ} θ .transitive R R' h h' {x} {z} =
  Trunc.rec
    (θ .prop (λ _ _ → squash) _ _)
    (λ {(y , r , r') → θ .transitive R R' (h r) (h' r')})
unaryFunSuitableRel pres {ρ} θ .prop propR f g =
  isPropImplicitΠ λ x →
  isPropImplicitΠ λ y →
  isPropΠ λ _ → θ .prop propR (f x) (g y)

unaryFunRelMatchesEquiv : {S : Type ℓ → Type ℓ₁}
  (ρ : StrRel S ℓ₁') {ι : StrEquiv S ℓ₁'}
  → StrRelMatchesEquiv ρ ι
  → StrRelMatchesEquiv (UnaryFunRelStr ρ) (UnaryFunEquivStr ι)
unaryFunRelMatchesEquiv ρ μ (X , f) (Y , g) e =
  compEquiv (isoToEquiv isom) (equivPi λ _ → μ _ _ e)
  where
  open Iso

  isom : Iso _ _
  isom .fun h x = h refl
  isom .inv k {x} = J (λ y _ → ρ (graphRel (e .fst)) (f x) (g y)) (k x)
  isom .rightInv k i x = JRefl (λ y _ → ρ (graphRel (e .fst)) (f x) (g y)) (k x) i
  isom .leftInv h =
    implicitFunExt λ {x} →
    implicitFunExt λ {y} →
    funExt λ p →
    J (λ y p →  isom .inv (isom .fun h) p ≡ h p)
      (funExt⁻ (isom .rightInv (isom .fun h)) x)
      p

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module Bound.Total.Order {A : Set}(_≤_ : A → A → Set)  where

open import Bound.Total A

data LeB : Bound → Bound → Set where
  lebx : {b : Bound}
                   → LeB bot b
  lexy : {x y : A}
                   → x ≤ y
                   → LeB (val x) (val y)
  lext : {b : Bound}
                   → LeB b top

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import LogicalFormulae
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Rings.Definition
open import Rings.Homomorphisms.Definition
open import Rings.IntegralDomains.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations

module Fields.FieldOfFractions.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) where

open import Fields.FieldOfFractions.Setoid I
open import Fields.FieldOfFractions.Ring I

embedIntoFieldOfFractions : A → fieldOfFractionsSet
embedIntoFieldOfFractions a = record { num = a ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }

homIntoFieldOfFractions : RingHom R fieldOfFractionsRing embedIntoFieldOfFractions
RingHom.preserves1 homIntoFieldOfFractions = Equivalence.reflexive (Setoid.eq S)
RingHom.ringHom homIntoFieldOfFractions {a} {b} = Equivalence.transitive (Setoid.eq S) (Ring.*WellDefined R (Equivalence.reflexive (Setoid.eq S)) (Ring.identIsIdent R)) (Ring.*Commutative R)
GroupHom.groupHom (RingHom.groupHom homIntoFieldOfFractions) {x} {y} = need
  where
    open Setoid S
    open Equivalence eq
    need : ((x + y) * (Ring.1R R * Ring.1R R)) ∼ (Ring.1R R * ((x * Ring.1R R) + (Ring.1R R * y)))
    need = transitive (transitive (Ring.*WellDefined R reflexive (Ring.identIsIdent R)) (transitive (Ring.*Commutative R) (transitive (Ring.identIsIdent R) (Group.+WellDefined (Ring.additiveGroup R) (symmetric (transitive (Ring.*Commutative R) (Ring.identIsIdent R))) (symmetric (Ring.identIsIdent R)))))) (symmetric (Ring.identIsIdent R))
GroupHom.wellDefined (RingHom.groupHom homIntoFieldOfFractions) x=y = transitive (Ring.*Commutative R) (Ring.*WellDefined R reflexive x=y)
  where
    open Equivalence (Setoid.eq S)

homIntoFieldOfFractionsIsInj : SetoidInjection S fieldOfFractionsSetoid embedIntoFieldOfFractions
SetoidInjection.wellDefined homIntoFieldOfFractionsIsInj x=y = transitive (Ring.*Commutative R) (Ring.*WellDefined R reflexive x=y)
  where
    open Equivalence (Setoid.eq S)
SetoidInjection.injective homIntoFieldOfFractionsIsInj x~y = transitive (symmetric identIsIdent) (transitive *Commutative (transitive x~y identIsIdent))
  where
    open Ring R
    open Setoid S
    open Equivalence eq


text:
{-

This file contains:

- Properties of 2-groupoid truncations

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.2GroupoidTruncation.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.HITs.2GroupoidTruncation.Base

rec2GroupoidTrunc : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (gB : is2Groupoid B) → (A → B) → (∥ A ∥₂ → B)
rec2GroupoidTrunc gB f ∣ x ∣₂ = f x
rec2GroupoidTrunc gB f (squash₂ _ _ _ _ _ _ t u i j k l) =
  gB _ _ _ _ _ _
    (λ m n o → rec2GroupoidTrunc gB f (t m n o))
    (λ m n o → rec2GroupoidTrunc gB f (u m n o))
    i j k l

g2TruncFib : ∀ {ℓ ℓ'} {A : Type ℓ} (P : A → Type ℓ')
             {a b : A} (sPb : is2Groupoid (P b))
             {p q : a ≡ b} {r s : p ≡ q} {u v : r ≡ s} (w : u ≡ v) {a1 : P a} {b1 : P b}
             {p1 : PathP (λ i → P (p i)) a1 b1}
             {q1 : PathP (λ i → P (q i)) a1 b1}
             {r1 : PathP (λ i → PathP (λ j → P (r i j)) a1 b1) p1 q1}
             {s1 : PathP (λ i → PathP (λ j → P (s i j)) a1 b1) p1 q1}
             (u1 : PathP (λ i → PathP (λ j → PathP (λ k → P (u i j k)) a1 b1) p1 q1) r1 s1)
             (v1 : PathP (λ i → PathP (λ j → PathP (λ k → P (v i j k)) a1 b1) p1 q1) r1 s1)
           → PathP (λ i → PathP (λ j → PathP (λ k → PathP (λ l → P (w i j k l)) a1 b1) p1 q1) r1 s1) u1 v1
g2TruncFib {A} P {a} {b} sPb {p} {q} {r} {s} {u} {v} w
           {a1} {b1} {p1} {q1} {r1} {s1} u1 v1 i j k l
  = hcomp (λ m → λ { (i = i0) → u1 j k l
                   ; (i = i1) → v1 j k l
                   ; (j = i0) → r1 k l
                   ; (j = i1) → s1 k l
                   ; (k = i0) → p1 l
                   ; (k = i1) → q1 l
                   ; (l = i0) → a1
                   ; (l = i1) → sPb b1 b1 refl refl refl refl L refl m i j k
                   })
          (Lb i j k l)
  where
  L : Path (Path (b1 ≡ b1) refl refl) refl refl
  L i j k = comp (λ l → P (w i j k l))
                 (λ l → λ { (i = i0) → u1 j k l
                          ; (i = i1) → v1 j k l
                          ; (j = i0) → r1 k l
                          ; (j = i1) → s1 k l
                          ; (k = i0) → p1 l
                          ; (k = i1) → q1 l
                          })
                 a1
  Lb : PathP (λ i → PathP (λ j → PathP (λ k → PathP (λ l → P (w i j k l)) a1 (L i j k)) p1 q1) r1 s1) u1 v1
  Lb i j k l = fill (λ l → P (w i j k l))
                    (λ l → λ { (i = i0) → u1 j k l
                             ; (i = i1) → v1 j k l
                             ; (j = i0) → r1 k l
                             ; (j = i1) → s1 k l
                             ; (k = i0) → p1 l
                             ; (k = i1) → q1 l
                             })
                    (inS a1) l

g2TruncElim : ∀ {ℓ ℓ'} (A : Type ℓ) (B : ∥ A ∥₂ → Type ℓ')
                    (bG : (x : ∥ A ∥₂) → is2Groupoid (B x))
                    (f : (x : A) → B ∣ x ∣₂) (x : ∥ A ∥₂) → B x
g2TruncElim A B bG f ∣ x ∣₂ = f x
g2TruncElim A B bG f (squash₂ x y p q r s u v i j k l) =
  g2TruncFib {A = ∥ A ∥₂} B {x} {y} (bG y) {p} {q} {r} {s} {u} {v}
               (squash₂ x y p q r s u v)
               {g2TruncElim A B bG f x}
               {g2TruncElim A B bG f y}
               {λ i → g2TruncElim A B bG f (p i)}
               {λ i → g2TruncElim A B bG f (q i)}
               {λ i j → g2TruncElim A B bG f (r i j)}
               {λ i j → g2TruncElim A B bG f (s i j)}
               (λ i j k → g2TruncElim A B bG f (u i j k))
               (λ i j k → g2TruncElim A B bG f (v i j k))
               i j k l

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import LogicalFormulae

module Decidable.Sets {a : _} (A : Set a) where

DecidableSet : Set a
DecidableSet = (a b : A) → ((a ≡ b) || ((a ≡ b) → False))


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

open import Axiom.Extensionality.Propositional

module FLA.Axiom.Extensionality.Propositional where

-- Since (dependent) extensionality is not allowed in standard Agda, we
-- postulate it here. In the standard library, the Extensionality term is
-- given in the type, which is then often named `ext` as an input to the
-- function. However this is cumberson, as anything using extensionality now
-- needs to take extensionality as an argument. If this library was
-- converted to cubical Agda we could prove extensionality directly,
-- although we would lose UIP.
postulate
  extensionality : ∀ {α β} → Extensionality α β

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


text:
------------------------------------------------------------------------
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Props.DistributiveLattice
         (dl : DistributiveLattice)
         where

open DistributiveLattice dl
import Algebra.Props.Lattice as L; open L lattice public
open import Algebra.Structures
import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Data.Function
open import Data.Product

∨-∧-distrib : _∨_ DistributesOver _∧_
∨-∧-distrib = ∨-∧-distribˡ , ∨-∧-distribʳ
  where
  ∨-∧-distribˡ : _∨_ DistributesOverˡ _∧_
  ∨-∧-distribˡ x y z = begin
    x ∨ y ∧ z          ≈⟨ ∨-comm _ _ ⟩
    y ∧ z ∨ x          ≈⟨ ∨-∧-distribʳ _ _ _ ⟩
    (y ∨ x) ∧ (z ∨ x)  ≈⟨ ∨-comm _ _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _ ⟩
    (x ∨ y) ∧ (x ∨ z)  ∎

∧-∨-distrib : _∧_ DistributesOver _∨_
∧-∨-distrib = ∧-∨-distribˡ , ∧-∨-distribʳ
  where
  ∧-∨-distribˡ : _∧_ DistributesOverˡ _∨_
  ∧-∨-distribˡ x y z = begin
    x ∧ (y ∨ z)                ≈⟨ sym (proj₂ absorptive _ _) ⟨ ∧-pres-≈ ⟩ refl ⟩
    (x ∧ (x ∨ y)) ∧ (y ∨ z)    ≈⟨ (refl ⟨ ∧-pres-≈ ⟩ ∨-comm _ _) ⟨ ∧-pres-≈ ⟩ refl ⟩
    (x ∧ (y ∨ x)) ∧ (y ∨ z)    ≈⟨ ∧-assoc _ _ _ ⟩
    x ∧ ((y ∨ x) ∧ (y ∨ z))    ≈⟨ refl ⟨ ∧-pres-≈ ⟩ sym (proj₁ ∨-∧-distrib _ _ _) ⟩
    x ∧ (y ∨ x ∧ z)            ≈⟨ sym (proj₁ absorptive _ _) ⟨ ∧-pres-≈ ⟩ refl ⟩
    (x ∨ x ∧ z) ∧ (y ∨ x ∧ z)  ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩
    x ∧ y ∨ x ∧ z              ∎

  ∧-∨-distribʳ : _∧_ DistributesOverʳ _∨_
  ∧-∨-distribʳ x y z = begin
    (y ∨ z) ∧ x    ≈⟨ ∧-comm _ _ ⟩
    x ∧ (y ∨ z)    ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
    x ∧ y ∨ x ∧ z  ≈⟨ ∧-comm _ _ ⟨ ∨-pres-≈ ⟩ ∧-comm _ _ ⟩
    y ∧ x ∨ z ∧ x  ∎

-- The dual construction is also a distributive lattice.

∧-∨-isDistributiveLattice : IsDistributiveLattice _≈_ _∧_ _∨_
∧-∨-isDistributiveLattice = record
  { isLattice    = ∧-∨-isLattice
  ; ∨-∧-distribʳ = proj₂ ∧-∨-distrib
  }

∧-∨-distributiveLattice : DistributiveLattice
∧-∨-distributiveLattice = record
  { _∧_                   = _∨_
  ; _∨_                   = _∧_
  ; isDistributiveLattice = ∧-∨-isDistributiveLattice
  }

max_issues_repo_name: larrytheliquid/Lemmachine


text:
even : ℕ → Bool
odd  : ℕ → Bool

even zero    = true
even (suc n) = odd n

odd zero    = false
odd (suc n) = even n

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
{-
Please do not move this file. Changes should only be made if necessary.

This file contains pointers to the code examples and main results from the paper:

Internalizing Representation Independence with Univalence

Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner

Preprint: https://arxiv.org/abs/2009.05547

-}
{-# OPTIONS --safe #-}
module Cubical.Papers.RepresentationIndependence where

-- 2.1
import Agda.Builtin.Cubical.Path               as Path
import Cubical.Foundations.Prelude             as Prelude
-- 2.2
import Cubical.Foundations.Univalence          as Univalence
import Cubical.Foundations.HLevels             as HLevels
import Cubical.Foundations.Equiv               as Equivalences
import Cubical.Data.Sigma.Properties           as Sigma
-- 2.3
import Cubical.HITs.PropositionalTruncation    as PropositionalTruncation
import Cubical.HITs.Cost.Base                  as CostMonad
import Cubical.HITs.SetQuotients               as SetQuotients
import Cubical.HITs.Rationals.QuoQ             as SetQuoQ
import Cubical.HITs.Rationals.SigmaQ           as SigmaQ
-- 3.1
import Cubical.Foundations.SIP                 as SIP
import Cubical.Structures.Axioms               as Axioms
import Cubical.Algebra.Semigroup.Base          as Semigroup
open import Cubical.Data.Sigma.Base
-- 3.2
import Cubical.Structures.Pointed              as PointedStr
import Cubical.Structures.Constant             as ConstantStr
import Cubical.Structures.Product              as ProductStr
import Cubical.Structures.Function             as FunctionStr
import Cubical.Structures.Maybe                as MaybeStr
import Cubical.Foundations.Structure           as Structure
import Cubical.Structures.Auto                 as Auto
open import Cubical.Data.Maybe.Base
-- 4.1
import Cubical.Data.Vec.Base                   as Vector
import Cubical.Algebra.Matrix                  as Matrices
import Cubical.Data.FinData.Base               as Finite
open import Cubical.Algebra.AbGroup.Base
open import Cubical.Data.Bool.Base
-- 4.2
import Cubical.Structures.Queue                as Queues
import Cubical.Data.Queue.Truncated2List       as BatchedQueues
-- 5.1
import Cubical.Relation.Binary.Base            as BinRel
import Cubical.Relation.ZigZag.Base            as QER
import Cubical.Relation.ZigZag.Applications.MultiSet
                                               as MultiSets
-- 5.2
import Cubical.Foundations.RelationalStructure as RelStructure
import Cubical.Structures.Relational.Function  as RelFunction

-------------------------------------------------------------------------
-- 2. Programming in Cubical Type Theory
-- 2.1 Equalities as Paths
-- 2.2 Univalence
-- 2.3 Higher Inductive Types
-------------------------------------------------------------------------

-- 2.1 Equalities as Paths
open Path using (PathP) public
open Prelude using (_≡_ ; refl ; cong ; funExt
                        ; transport ; subst ; J) public

-- 2.2 Univalence
open Univalence using (ua ; uaβ) public

-- Sets and Propositions
open Prelude using (isProp ; isSet) public
open HLevels using (isPropΠ) public
open Prelude using (isContr) public

-- Equivalences and Isomorphisms
open Equivalences using (isEquiv ; _≃_) public
open Equivalences renaming (fiber to preim) public
open Sigma using (ΣPath≃PathΣ) public
open Equivalences renaming (propBiimpl→Equiv to prop≃) public

-- 2.3 Higher Inductive Types
-- Propositional Truncation
open PropositionalTruncation using (∥_∥ ; map) public
open CostMonad using (Cost ; Cost≡ ; _>>=_ ; return
                           ; fib ; fibTail) public
-- Computation
_ : fib 20 ≡ (6765 , PropositionalTruncation.∣ 21890 ∣)
_ = refl

_ : fibTail 20 ≡ (6765 , PropositionalTruncation.∣ 19 ∣)
_ = refl

-- Set Quotients
open SetQuotients using (_/_ ; setQuotUniversal) public
-- Rational Numbers
open SetQuoQ using (_∼_ ; ℚ) public
open SigmaQ renaming (ℚ to ℚ') public

-------------------------------------------------------------------------
-- 3. The Structure Identity Principle
-- 3.1 Structures
-- 3.2 Building Strucutres
-------------------------------------------------------------------------

-- 3.1 Structures
open SIP using (TypeWithStr ; StrEquiv ; _≃[_]_
                            ; UnivalentStr ; SIP ; sip) public

-- the last two terms above correspond to lemma 3.3
-- and corollary 3.4 respectively
open Axioms using ( AxiomsStructure ; AxiomsEquivStr
                  ; axiomsUnivalentStr ; transferAxioms) public

-- Monoids are defined using records and Σ-types in the library

RawMonoidStructure : Type → Type
RawMonoidStructure X = X × (X → X → X)

MonoidAxioms : (M : Type) → RawMonoidStructure M → Type
MonoidAxioms M (e , _·_) = Semigroup.IsSemigroup _·_
                         × ((x : M) → (x · e ≡ x) × (e · x ≡ x))

MonoidStructure : Type → Type
MonoidStructure = AxiomsStructure RawMonoidStructure MonoidAxioms

Monoid : Type₁
Monoid = TypeWithStr ℓ-zero MonoidStructure

MonoidEquiv : (M N : Monoid) → fst M ≃ fst N → Type
MonoidEquiv (_ , (εᴹ , _·_) , _) (_ , (εᴺ , _∗_) , _) (φ , _) =
  (φ εᴹ ≡ εᴺ) × (∀ x y → φ (x · y) ≡ (φ x) ∗ (φ y))

-- 3.2 Building Structures
-- Constant and Pointed Structures
open PointedStr using (PointedStructure ; PointedEquivStr
                                        ; pointedUnivalentStr) public
open ConstantStr using (ConstantStructure ; ConstantEquivStr
                                          ; constantUnivalentStr) public

-- Product Structures
open ProductStr using (ProductStructure ; ProductEquivStr
                                        ; productUnivalentStr) public

-- Function Structures
open FunctionStr using (FunctionEquivStr) public

-- Maybe Structures
open MaybeStr using (MaybeEquivStr) public

-- Transport Structures
open Structure using (EquivAction) public
open SIP using (TransportStr ; TransportStr→UnivalentStr
                             ; UnivalentStr→TransportStr) public
open Structure using (EquivAction→StrEquiv) public
open FunctionStr using (FunctionEquivStr+) public

-- Monoids Revisited

RawMonoid : Type₁
RawMonoid = TypeWithStr _ RawMonoidStructure

Monoid→RawMonoid : Monoid → RawMonoid
Monoid→RawMonoid (A , r , _) = (A , r)

RawMonoidEquivStr = Auto.AutoEquivStr RawMonoidStructure

rawMonoidUnivalentStr : UnivalentStr _ RawMonoidEquivStr
rawMonoidUnivalentStr = Auto.autoUnivalentStr RawMonoidStructure

isPropMonoidAxioms : (M : Type) (s : RawMonoidStructure M) → isProp (MonoidAxioms M s)
isPropMonoidAxioms M (e , _·_) =
  HLevels.isPropΣ
    (Semigroup.isPropIsSemigroup _·_)
    (λ α → isPropΠ λ _ →
      HLevels.isProp×
        (Semigroup.IsSemigroup.is-set α _ _)
        (Semigroup.IsSemigroup.is-set α _ _))

MonoidEquivStr : StrEquiv MonoidStructure ℓ-zero
MonoidEquivStr = AxiomsEquivStr RawMonoidEquivStr MonoidAxioms

monoidUnivalentStr : UnivalentStr MonoidStructure MonoidEquivStr
monoidUnivalentStr = axiomsUnivalentStr _ isPropMonoidAxioms rawMonoidUnivalentStr

MonoidΣPath : (M N : Monoid) → (M ≃[ MonoidEquivStr ] N) ≃ (M ≡ N)
MonoidΣPath = SIP monoidUnivalentStr

InducedMonoid : (M : Monoid) (N : RawMonoid) (e : M .fst ≃ N .fst)
                → RawMonoidEquivStr (Monoid→RawMonoid M) N e → Monoid
InducedMonoid M N e r =
  Axioms.inducedStructure rawMonoidUnivalentStr M N (e , r)

InducedMonoidPath : (M : Monoid) (N : RawMonoid) (e : M .fst ≃ N .fst)
                    (E : RawMonoidEquivStr (Monoid→RawMonoid M) N e)
                    → M ≡ InducedMonoid M N e E
InducedMonoidPath M N e E =
  MonoidΣPath M (InducedMonoid M N e E) .fst (e , E)

-- Automation
open Auto using (Transp[_] ; AutoEquivStr ; autoUnivalentStr) public
module _ (A : Type) (Aset : isSet A) where
 RawQueueEquivStr =
   AutoEquivStr (λ (X : Type) → X × (A → X → X) × (X → Transp[ Maybe (X × A) ]))

-------------------------------------------------------------------------
-- 4. Representation Independence through the SIP
-- 4.1 Matrices
-- 4.2 Queues
-------------------------------------------------------------------------

-- 4.1 Matrices
open Vector using (Vec) public
open Finite using (Fin ; _==_) public
open Matrices using (VecMatrix ; FinMatrix ; FinMatrix≡VecMatrix
                                           ; FinMatrix≃VecMatrix) public
open Matrices.FinMatrixAbGroup using (addFinMatrix ; addFinMatrixComm) public

-- example (not in the library)
open import Cubical.Data.Int renaming (Int to ℤ ; isSetInt to isSetℤ) hiding (-_)

ℤ-AbGroup : AbGroup ℓ-zero
ℤ-AbGroup = makeAbGroup {G = ℤ} 0 _+_ -_ isSetℤ +-assoc (λ x _ → x) rem +-comm
    where
    -_ : ℤ → ℤ
    - x = 0 - x
    rem : (x : ℤ) → x + (- x) ≡ 0
    rem x =  +-comm x (pos 0 - x) Prelude.∙ minusPlus x 0

module experiment where
  open Prelude

  M : FinMatrix ℤ 2 2
  M i j = if i == j then 1 else 0

  N : FinMatrix ℤ 2 2
  N i j = if i == j then 0 else 1

  replaceGoal : {A B : Type} {x y : A} → (e : A ≃ B)
                (h : invEq e (equivFun e x) ≡ invEq e (equivFun e y)) → x ≡ y
  replaceGoal e h = sym (retEq e _) ∙∙ h ∙∙ retEq e _

  _ : addFinMatrix ℤ-AbGroup M N ≡ (λ _ _ → 1)
  _ = replaceGoal (FinMatrix≃VecMatrix) refl

-- 4.2 Queues
open Queues.Queues-on using (RawQueueStructure ; QueueAxioms) public
open BatchedQueues.Truncated2List renaming (Q to BatchedQueueHIT)
                                  using (Raw-1≡2 ; WithLaws) public

-------------------------------------------------------------------------
-- 5. Structured Equivalences from Structured Relations
-- 5.1 Quasi-Equivalence Relations
-- 5.2 Structured Relations
-------------------------------------------------------------------------

-- 5.1 Quasi-Equivalence Relations
--Lemma (5.1)
open BinRel using (idPropRel ; invPropRel
                             ; compPropRel ; graphRel) public
-- Definitions (5.2) and (5.3)
open QER using (isZigZagComplete ; isQuasiEquivRel) public
-- Lemma (5.4)
open QER.QER→Equiv using (Thm ; bwd≡ToRel) public
-- Multisets
open MultiSets renaming (AList to AssocList) public
open MultiSets.Lists&ALists using (addIfEq ; R ; φ ; ψ
                                           ; List/Rᴸ≃AList/Rᴬᴸ) public
open MultiSets.Lists&ALists.L using (insert ; union ; count)
open MultiSets.Lists&ALists.AL using (insert ; union ; count)

-- 5.2 Structured Relations
open RelStructure using (StrRel) public
-- Definition (5.6)
open RelStructure using (SuitableStrRel) public
-- Theorem (5.7)
open RelStructure using (structuredQER→structuredEquiv) public
-- Definition (5.9)
open RelStructure using (StrRelAction) public
-- Lemma (5.10)
open RelStructure using (strRelQuotientComparison) public
-- Definition (5.11)
open RelStructure using (PositiveStrRel) public
-- Theorem (5.12)
open RelFunction using (functionSuitableRel) public
-- Multisets
-- (main is applying 5.7 to the example)
open MultiSets.Lists&ALists using (multisetShape ; isStructuredR ; main ; List/Rᴸ≡AList/Rᴬᴸ)
                            renaming ( hasAssociativeUnion to unionAssocAxiom
                                     ; LQassoc to LUnionAssoc
                                     ; ALQassoc to ALUnionAssoc) public

max_stars_repo_name: LuuBluum/cubical

max_issues_repo_name: LuuBluum/cubical

max_forks_repo_name: LuuBluum/cubical


text:
open import Nat
open import Prelude
open import Hazelnut-core

module Hazelnut-sensible where
  -- theorem 1: action sensibility
  synthmovelem : {Γ : ·ctx} {e e' : ê} {t : τ̇} {δ : direction} →
                 (e + move δ +>e e') →
                 (Γ ⊢ e ◆e => t) →
                 (Γ ⊢ e' ◆e => t)
  synthmovelem EMAscFirstChild d2 = d2
  synthmovelem EMAscParent1 d2 = d2
  synthmovelem EMAscParent2 d2 = d2
  synthmovelem EMAscNextSib d2 = d2
  synthmovelem EMAscPrevSib d2 = d2
  synthmovelem EMLamFirstChild d2 = d2
  synthmovelem EMLamParent d2 = d2
  synthmovelem EMPlusFirstChild d2 = d2
  synthmovelem EMPlusParent1 d2 = d2
  synthmovelem EMPlusParent2 d2 = d2
  synthmovelem EMPlusNextSib d2 = d2
  synthmovelem EMPlusPrevSib d2 = d2
  synthmovelem EMApFirstChild d2 = d2
  synthmovelem EMApParent1 d2 = d2
  synthmovelem EMApParent2 d2 = d2
  synthmovelem EMApNextSib d2 = d2
  synthmovelem EMApPrevSib d2 = d2
  synthmovelem EMFHoleFirstChild d2 = d2
  synthmovelem EMFHoleParent d2 = d2

  -- movements preserve analytic types up to erasure. this lemma seems
  -- silly because all it seems to do in each case is return the second
  -- derivation D. the pattern matching here, though, constrains what that
  -- derivation may be in each case, and is therefore actually
  -- non-trivial. it's just that most of the work is happening in the
  -- implicit arguments.
  anamovelem : {Γ : ·ctx} {δ : direction} {e e' : ê} {t : τ̇}
            (p : e + move δ +>e e') →
            (Γ ⊢ e ◆e <= t) →
            (Γ ⊢ e' ◆e <= t)
  anamovelem EMAscFirstChild d2 = d2
  anamovelem EMAscParent1 d2 = d2
  anamovelem EMAscParent2 d2 = d2
  anamovelem EMAscNextSib d2 = d2
  anamovelem EMAscPrevSib d2 = d2
  anamovelem EMLamFirstChild d2 = d2
  anamovelem EMLamParent d2 = d2
  anamovelem EMPlusFirstChild d2 = d2
  anamovelem EMPlusParent1 d2 = d2
  anamovelem EMPlusParent2 d2 = d2
  anamovelem EMPlusNextSib d2 = d2
  anamovelem EMPlusPrevSib d2 = d2
  anamovelem EMApFirstChild d2 = d2
  anamovelem EMApParent1 d2 = d2
  anamovelem EMApParent2 d2 = d2
  anamovelem EMApNextSib d2 = d2
  anamovelem EMApPrevSib d2 = d2
  anamovelem EMFHoleFirstChild d2 = d2
  anamovelem EMFHoleParent d2 = d2

  mutual
    -- if an action transforms an zexp in a synthetic posistion to another
    -- zexp, they have the same type up erasure of focus.
    actsense1 : {Γ : ·ctx} {e e' : ê} {t t' : τ̇} {α : action} →
                (Γ ⊢ e => t ~ α ~> e' => t') →
                (Γ ⊢ (e  ◆e) => t) →
                 Γ ⊢ (e' ◆e) => t'
    actsense1 (SAMove x) D2 = synthmovelem x D2
    actsense1 SADel D2 = SEHole
    actsense1 SAConAsc D2 = SAsc (ASubsume D2 TCRefl)
    actsense1 (SAConVar p) D2 = SVar p
    actsense1 (SAConLam p) D2 = SAsc (ALam p (ASubsume SEHole TCRefl))
    actsense1 SAConAp1 D2 = SAp D2 (ASubsume SEHole TCHole1)
    actsense1 SAConAp2 D2 = SApHole D2 (ASubsume SEHole TCRefl)
    actsense1 (SAConAp3 x) D2 = SApHole (SFHole D2) (ASubsume SEHole TCRefl)
    actsense1 SAConArg D2 = SApHole SEHole (ASubsume D2 TCHole2)
    actsense1 SAConNumlit D2 = SNum
    actsense1 (SAConPlus1 TCRefl) D2 = SPlus (ASubsume D2 TCRefl) (ASubsume SEHole TCHole1)
    actsense1 (SAConPlus1 TCHole2) D2 = SPlus (ASubsume D2 TCHole1) (ASubsume SEHole TCHole1)
    actsense1 (SAConPlus2 x) D2 = SPlus (ASubsume (SFHole D2) TCHole1) (ASubsume SEHole TCHole1)
    actsense1 (SAFinish x) D2 = x
    actsense1 (SAZipAsc1 x) (SAsc D2) = SAsc (actsense2 x D2)
    actsense1 (SAZipAsc2 x x₁) _ = SAsc x₁
    actsense1 (SAZipAp1 x D1 x₁) D2 = SAp (actsense1 D1 x) x₁
    actsense1 (SAZipAp2 x D1 x₁) D2 = SApHole (actsense1 D1 x) x₁
    actsense1 (SAZipAp3 x x₁) (SAp D2 x₃)     with synthunicity x D2
    ... | refl = SAp x (actsense2 x₁ x₃)
    actsense1 (SAZipAp3 x x₁) (SApHole D2 x₂) with synthunicity x D2
    ... | ()
    actsense1 (SAZipAp4 x x₁) (SAp D2 x₂)     with synthunicity x D2
    ... | ()
    actsense1 (SAZipAp4 x x₁) (SApHole D2 x₂)  = SApHole x (actsense2 x₁ x₂)
    actsense1 (SAZipPlus1 x) (SPlus x₁ x₂) = SPlus (actsense2 x x₁) x₂
    actsense1 (SAZipPlus2 x) (SPlus x₁ x₂) = SPlus x₁ (actsense2 x x₂)
    actsense1 (SAZipHole1 x D1 x₁) D2 = SFHole (actsense1 D1 x)
    actsense1 (SAZipHole2 x D1) D2 = SEHole

    -- if an action transforms an zexp in an analytic posistion to another
    -- zexp, they have the same type up erasure of focus.
    actsense2  : {Γ : ·ctx} {e e' : ê} {t : τ̇} {α : action} →
                  (Γ ⊢ e ~ α ~> e' ⇐ t) →
                  (Γ ⊢ (e ◆e) <= t) →
                  (Γ ⊢ (e' ◆e) <= t)
    actsense2 (AASubsume x act p) D2 = ASubsume (actsense1 act x) p
    actsense2 (AAMove x) D2 = anamovelem x D2
    actsense2 AADel _ = ASubsume SEHole TCHole1
    actsense2 AAConAsc D2 = ASubsume (SAsc D2) TCRefl
    actsense2 (AAConVar x₁ p) D2 = ASubsume (SFHole (SVar p)) TCHole1
    actsense2 (AAConLam1 p) (ASubsume SEHole TCHole1) = ALam p (ASubsume SEHole TCHole1)
    actsense2 (AAConLam2 p n~) (ASubsume SEHole TCRefl) = abort (n~ TCHole2)
    actsense2 (AAConLam2 p x₁) (ASubsume SEHole TCHole1) = ASubsume (SFHole (SAsc (ALam p (ASubsume SEHole TCRefl)))) TCHole1
    actsense2 (AAConLam2 p n~) (ASubsume SEHole TCHole2) = abort (n~ TCHole2)
    actsense2 (AAConNumlit _) _ = ASubsume (SFHole SNum) TCHole1
    actsense2 (AAFinish x) _ = x
    actsense2 (AAZipLam _ _ ) (ASubsume () _)

    actsense2 (AAZipLam x₁ (AASubsume {p = p} x₂ x₃ x₄)) (ALam x₅ D2) = ALam x₅ (actsense2 (AASubsume {p = p} x₂ x₃ x₄) D2)
    actsense2 (AAZipLam x₁ (AAMove x₂)) (ALam x₃ D2) = ALam x₃ (anamovelem x₂ D2)
    actsense2 (AAZipLam x₁ AADel) (ALam x₂ D2) = ALam x₂ (ASubsume SEHole TCHole1)
    actsense2 (AAZipLam x₁ AAConAsc) (ALam x₂ (ASubsume x₃ x₄)) = ALam x₂ (ASubsume (SAsc (ASubsume x₃ x₄)) TCRefl)
    actsense2 (AAZipLam x₁ AAConAsc) (ALam x₂ (ALam x₃ D2)) = ALam x₂ (ASubsume (SAsc (ALam x₃ D2)) TCRefl)
    actsense2 (AAZipLam x₁ (AAConVar x₃ p)) (ALam x₄ D2) = ALam x₄ (ASubsume (SFHole (SVar p)) TCHole1)
    actsense2 (AAZipLam x₁ (AAConLam1 x₃)) (ALam x₄ D2) = ALam x₄ (ALam x₃ (ASubsume SEHole TCHole1))
    actsense2 (AAZipLam x₁ (AAConLam2 x₃ x₄)) (ALam x₅ D2) = ALam x₅ (ASubsume (SFHole (SAsc (ALam x₃ (ASubsume SEHole TCRefl))))
                                                                        TCHole1)
    actsense2 (AAZipLam x₁ (AAConNumlit x₂)) (ALam x₃ D2) = ALam x₃ (ASubsume (SFHole SNum) TCHole1)
    actsense2 (AAZipLam x₁ (AAFinish x₂)) (ALam x₃ D2) = ALam x₃ x₂
    actsense2 (AAZipLam x₁ (AAZipLam x₃ D1)) (ALam x₄ (ASubsume () x₆))
    actsense2 (AAZipLam x₁ (AAZipLam x₃ D1)) (ALam x₄ (ALam x₅ D2)) = ALam x₄ (ALam x₃ (actsense2 D1 D2))


text:
--{-# OPTIONS --allow-unsolved-metas #-}

module StateSizedIO.GUI.Prelude where

open import Size public renaming (Size to AgdaSize)

open import Data.Nat.Base public
open import Data.Bool.Base hiding (_≟_) public
open import Data.List.Base public

open import Function public
open import Data.Integer.Base public hiding (_*_; _+_; _-_; _⊓_; _⊔_; pred; suc;_≤_)
open import Agda.Builtin.Equality public
open import Data.Product public using (_×_; _,_)

open import NativeIO public

open import StateSizedIO.GUI.WxBindingsFFI public
open import StateSizedIO.GUI.VariableList public

open import SizedIO.Base public
open import StateSizedIO.GUI.BaseStateDependent public

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
-- Andreas, 2019-08-20, issue #4012
-- unquoteDef and unquoteDecl should respect `private`

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.List

data D : Set where
  c : D

module M where

  private

    unquoteDecl g = do
      ty ← quoteTC D
      _  ← declareDef (arg (arg-info visible relevant) g) ty
      qc ← quoteTC c
      defineFun g (clause [] qc ∷ [])

open M

test = g

-- Expect failure.
-- g is private in M, thus, should not be in scope


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

{-
Imports everything that is not imported by something else.
This is not supposed to be used anywhere, this is just a simple way to
do `make all'

This file is intentionally named index.agda so that
Agda will generate index.html.
-}

module index where

-- import Spaces.IntervalProps
-- import Algebra.F2NotCommutative
import homotopy.LoopSpaceCircle
import homotopy.HopfJunior
import homotopy.Hopf
import homotopy.CoverClassification
import homotopy.AnyUniversalCoverIsPathSet
import homotopy.PathSetIsInital
-- import Spaces.LoopSpaceDecidableWedgeCircles
-- import Homotopy.PullbackIsPullback
-- import Homotopy.PushoutIsPushout
-- import Homotopy.Truncation
-- import Sets.QuotientUP
-- import Spaces.PikSn
-- import Homotopy.VanKampen

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Data.List    using (List; _∷_; [])
open import Data.Product using (_×_; _,_; Σ)
open import Data.Unit    using (⊤; tt)
open import Relation.Binary.PropositionalEquality using (_≡_)

module SystemT where

  data _∈_ {A : Set} : (x : A) (l : List A) → Set where -- type \in
    i0 : {x : A} {xs : List A} → x ∈ (x ∷ xs)
    iS : {x y : A} {xs : List A} → x ∈ xs → x ∈ (y ∷ xs)

  data TType : Set where
    base  : TType
    _⟶_ : TType → TType → TType

  Context = List TType
  _,,_ : Context → TType → Context
  Γ ,, τ = τ ∷ Γ

  infixr 10 _⟶_
  infixr 9 _,,_
  infixr 8 _⊢_

  data _⊢_ (Γ : Context) : TType → Set where
    -- Some constant of the base type whose type is immediate.
    c : Γ ⊢ base
    -- Variable.
    var : {τ : TType} → τ ∈ Γ → Γ ⊢ τ
    -- Function introduction.
    lam : {τ₁ τ₂ : TType} → Γ ,, τ₁ ⊢ τ₂ → Γ ⊢ τ₁ ⟶ τ₂
    -- Function application.
    app : {τ₁ τ₂ : TType} → (Γ ⊢ τ₁ ⟶ τ₂) → Γ ⊢ τ₁ → Γ ⊢ τ₂

  module Semantics (B : Set) (elB : B) where

    -- Interpretation of System T types to Agda types.
    ⟦_⟧t : TType → Set
    ⟦ base ⟧t = B
    ⟦ τ₁ ⟶ τ₂ ⟧t = ⟦ τ₁ ⟧t → ⟦ τ₂ ⟧t

    -- Interpretation of System T contexts to Agda types.
    ⟦_⟧c : Context → Set
    ⟦ [] ⟧c = ⊤
    ⟦ τ ∷ Γ ⟧c = ⟦ Γ ⟧c × ⟦ τ ⟧t

    -- Interpretation of terms.
    ⟦_⟧ : {Γ : Context} {τ : TType} → (Γ ⊢ τ) → ⟦ Γ ⟧c → ⟦ τ ⟧t
    ⟦ c ⟧ γ = elB
    ⟦ var x ⟧ γ = {!  !}
    ⟦ lam e ⟧ γ x = {!   !}
    ⟦ app e₁ e₂ ⟧ γ = {!   !}

max_stars_repo_name: ayberkt/system-t-normalization

max_issues_repo_name: ayberkt/system-t-normalization

max_forks_repo_name: ayberkt/system-t-normalization


text:
{-# OPTIONS --universe-polymorphism #-}
-- {-# OPTIONS --verbose tc.records.ifs:15 #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.term.args.ifs:15 #-}

module 05-equality-std1 where

open import Relation.Binary using (IsDecEquivalence; module IsDecEquivalence; Reflexive; module DecSetoid)
open import Data.Bool using (false; true; decSetoid)
open DecSetoid decSetoid using (isDecEquivalence)

open module IsDecEquivalenceWithImplicits = IsDecEquivalence {{...}} using (_≟_)

test = false ≟ true

test2 : ∀ {a ℓ} {A : Set a} {_≈_} → {{ide : IsDecEquivalence {a} {ℓ} {A} _≈_}} →
        Reflexive _≈_
test2 = IsDecEquivalenceWithImplicits.refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Thesis.SIRelBigStep.DenSem where

open import Data.Nat
open import Data.Product
open import Thesis.SIRelBigStep.Syntax

open import Data.Nat

⟦_⟧Type : Type → Set
⟦ σ ⇒ τ ⟧Type = ⟦ σ ⟧Type → ⟦ τ ⟧Type
⟦ nat ⟧Type = ℕ
⟦ pair τ1 τ2 ⟧Type = ⟦ τ1 ⟧Type × ⟦ τ2 ⟧Type

import Base.Denotation.Environment
module Den = Base.Denotation.Environment Type ⟦_⟧Type
open import Base.Data.DependentList

⟦_⟧Const : ∀ {τ} → Const τ → ⟦ τ ⟧Type
⟦ lit n ⟧Const = n

⟦_⟧Primitive : ∀ {τ} → Primitive τ → ⟦ τ ⟧Type
⟦ succ ⟧Primitive = suc
⟦ add ⟧Primitive = λ { (n1 , n2) → n1 + n2}

⟦_⟧Term : ∀ {Γ τ} → Term Γ τ → Den.⟦ Γ ⟧Context → ⟦ τ ⟧Type
⟦_⟧SVal : ∀ {Γ τ} → SVal Γ τ → Den.⟦ Γ ⟧Context → ⟦ τ ⟧Type
⟦ var x ⟧SVal ρ = Den.⟦ x ⟧Var ρ
⟦ abs t ⟧SVal ρ = λ v → ⟦ t ⟧Term (v • ρ)
⟦ cons sv1 sv2 ⟧SVal ρ = ⟦ sv1 ⟧SVal ρ , ⟦ sv2 ⟧SVal ρ
⟦ const c ⟧SVal ρ = ⟦ c ⟧Const

⟦ val sv ⟧Term ρ = ⟦ sv ⟧SVal ρ
⟦ app s t ⟧Term ρ = ⟦ s ⟧SVal ρ (⟦ t ⟧SVal ρ)
⟦ lett s t ⟧Term ρ = ⟦ t ⟧Term ((⟦ s ⟧Term ρ) • ρ)
⟦ primapp vs vt ⟧Term ρ = ⟦ vs ⟧Primitive (⟦ vt ⟧SVal ρ)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
-- Subtyping is no longer supported for irrelevance.

f : {A B : Set} → (.A → B) → A → B
f g = λ .x → g x

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

postulate X : Set
variable x : X

data C : Σ X (λ x → x ≡ x) → Set where
  mkC :
    let
      eq : x ≡ x  -- don't generalize over x at eq
      eq = refl {x = x}
    in
    C (x , eq)

max_stars_repo_name: sseefried/agda


text:
module Sets.IterativeUSet where

open import Data renaming (Empty to EmptyType)
open import Functional
import      Lvl
import      Lvl.Decidable as Lvl
open import Structure.Setoid renaming (_≡_ to _≡ₛ_)
open import Syntax.Function
open import Type
open import Type.Dependent

private variable ℓ ℓₒ ℓₑ ℓ₁ ℓ₂ : Lvl.Level
private variable T Indexₗ Indexᵣ : Type{ℓ}
private variable a b c x y z : T

-- A model of constructive set theory with atoms/urelements (CZFU) by iterative sets.
-- The definition states that an instance of IUset is either an atom or a set.
-- An atom is an instance of the atoms/urelements.
-- A set is an instance of a set container which is a function from a type of indices (which depends on the set) to an IUset. The function should be interpreted as pointing to every element of the set, and the image of this function is how a single set is represented.
module _ (T : Type{ℓₒ}) ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {ℓ} where
  data IUset : Type{Lvl.𝐒(ℓ) Lvl.⊔ ℓₒ}
  SetContainer : Type{Lvl.𝐒(ℓ) Lvl.⊔ ℓₒ}
  SetContainer = Σ(Type{ℓ}) (_→ᶠ IUset)
  data IUset where
    atom : T → IUset
    set  : SetContainer → IUset

module _ {T : Type{ℓₒ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {ℓ} where
  pattern setc {Index} elem = set(intro Index elem)

  module SetContainer where
    -- The projection of the index type for a set container.
    Index : (SC : SetContainer(T){ℓ}) → Type.of(Σ.left SC)
    Index = Σ.left

    -- The projection of the elements' function for a set container.
    elem : (SC : SetContainer(T){ℓ}) → Type.of(Σ.right SC)
    elem = Σ.right

  -- The projection of the index type for an IUset's set container if it is a set.
  -- It is non-existant otherwise (modeled by the empty type with no inhabitants).
  Index : IUset(T){ℓ} → Type{ℓ}
  Index (atom x) = EmptyType
  Index (set SC) = SetContainer.Index SC

  -- The projection of the elements' function for an IUset's set container it if it a set.
  -- It is non-existant otherwise (modeled by the empty function which is interpreted as the empty set).
  elem : (A : IUset(T){ℓ}) → (Index(A) → IUset(T){ℓ})
  elem (atom _) ()
  elem (set SC) = SetContainer.elem SC

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  open import Functional
  open import Logic.Propositional
  open import Logic.Propositional.Theorems
  open import Logic.Predicate

  private variable SC SCₗ SCᵣ : SetContainer(T) ⦃ equiv ⦄ {ℓ}

  -- The predicate stating that an IUset is a set.
  data IsSet {ℓ} : IUset(T){ℓ} → Type{Lvl.of(T) Lvl.⊔ Lvl.𝐒(ℓ)} where
    intro : IsSet(set(SC))

  -- The predicate stating that an IUset is an atom.
  data IsAtom {ℓ} : IUset(T){ℓ} → Type{Lvl.of(T) Lvl.⊔ Lvl.𝐒(ℓ)} where
    intro : IsAtom(atom(x))

  data _≡_ {ℓ₁ ℓ₂} : IUset(T){ℓ₁} → IUset(T){ℓ₂} → Type{Lvl.𝐒(ℓ₁ Lvl.⊔ ℓ₂) Lvl.⊔ ℓₑ Lvl.⊔ Lvl.of(T)}
  data _⊆_ {ℓ₁ ℓ₂} : IUset(T){ℓ₁} → IUset(T){ℓ₂} → Type{Lvl.𝐒(ℓ₁ Lvl.⊔ ℓ₂) Lvl.⊔ ℓₑ Lvl.⊔ Lvl.of(T)}

  _⊇_ : IUset(T){ℓ₁} → IUset(T){ℓ₂} → Type
  A ⊇ B = B ⊆ A

  -- Equality is either equivalence on its atoms or by definition the antisymmetric property of the subset relation.
  data _≡_ where
    atom : (a ≡ₛ b) → (atom a ≡ atom b)
    set  : (set SCₗ ⊇ set SCᵣ) → (set SCₗ ⊆ set SCᵣ) → (set SCₗ ≡ set SCᵣ)

  -- Set membership is the existence of an index in the set that points to a set equal element to the element.
  -- Note: This is never satisfied for an atom on the right.
  data _∈_ {ℓ₁ ℓ₂} (x : IUset(T){ℓ₁}) : IUset(T){ℓ₂} → Type{Lvl.𝐒(ℓ₁ Lvl.⊔ ℓ₂) Lvl.⊔ ℓₑ Lvl.⊔ Lvl.of(T)} where
    set : ∃{Obj = SetContainer.Index(SC)} (i ↦ x ≡ SetContainer.elem(SC) i) → (x ∈ set SC)
  [∈]-proof : (x ∈ set SC) → ∃{Obj = SetContainer.Index(SC)} (i ↦ x ≡ SetContainer.elem(SC) i)
  [∈]-proof (set p) = p
  [∈]-index : (x ∈ set SC) → SetContainer.Index(SC)
  [∈]-index (set ([∃]-intro i)) = i
  [∈]-elem : (p : (x ∈ set SC)) → (x ≡ SetContainer.elem(SC) ([∈]-index p))
  [∈]-elem (set ([∃]-intro _ ⦃ p ⦄)) = p

  -- Set subset is a mapping between the indices such that they point to the same element in both sets.
  -- Note: This is never satisfied for an atom on the right.
  data _⊆_ where
    set : (map : SetContainer.Index(SCₗ) → SetContainer.Index(SCᵣ)) → (∀{i} → (SetContainer.elem(SCₗ) i ≡ SetContainer.elem(SCᵣ) (map i))) → (set SCₗ ⊆ set SCᵣ)
  [⊆]-map : (set SCₗ ⊆ set SCᵣ) → (SetContainer.Index(SCₗ) → SetContainer.Index(SCᵣ))
  [⊆]-map (set map _) = map
  [⊆]-proof : (p : (set SCₗ ⊆ set SCᵣ)) → (∀{i} → (SetContainer.elem(SCₗ) i ≡ SetContainer.elem(SCᵣ) ([⊆]-map p i)))
  [⊆]-proof (set _ p) = p

  -- The binary relation of non-membership.
  _∉_ : IUset(T){ℓ₁} → IUset(T){ℓ₂} → Type
  a ∉ B = ¬(a ∈ B)

  -- The predicate stating that an IUset contains no elements (in other words, is empty).
  Empty : ∀{ℓ₁ ℓ₂ : Lvl.Level} → IUset(T){ℓ₂} → Type
  Empty{ℓ₁}(A) = ∀{x : IUset(T){ℓ₁}} → (x ∉ A)

  open import Logic.Classical

  private variable A B C : IUset(T) ⦃ equiv ⦄ {ℓ}

  instance
    -- An IUset is exclusively either an atom or a set.
    atom-xor-set : IsAtom(A) ⊕ IsSet(A)
    atom-xor-set {A = atom _} = [⊕]-introₗ intro \()
    atom-xor-set {A = set  _} = [⊕]-introᵣ intro \()

  instance
    IsAtom-classical : Classical₁(IsAtom{ℓ})
    IsAtom-classical = classical-from-xorₗ

  instance
    IsSet-classical : Classical₁(IsSet{ℓ})
    IsSet-classical = classical-from-xorᵣ

  -- An IUset containing something is always a set.
  set-if-membership : (x ∈ A) → IsSet(A)
  set-if-membership (set _) = intro

  -- An IUset which is an atom is always "empty" when interpreted as a set.
  atom-is-empty : IsAtom(A) → Empty{ℓ}(A)
  atom-is-empty p = contrapositiveᵣ set-if-membership ([⊕]-not-left atom-xor-set p)

  open import Functional
  open import Structure.Relator.Equivalence
  open import Structure.Relator.Properties

  [≡]-reflexivity-raw : (A ≡ A)
  [⊆]-reflexivity-raw : (set SC ⊆ set SC)
  [⊇]-reflexivity-raw : (set SC ⊇ set SC)
  [⊇]-reflexivity-raw = [⊆]-reflexivity-raw

  {-# TERMINATING #-} -- TODO: Passed the termination checker before Agda 2.6.2-caeadac-dirty
  [≡]-reflexivity-raw {A = atom x} = atom(reflexivity(_≡ₛ_))
  [≡]-reflexivity-raw {A = set x}  = set [⊇]-reflexivity-raw [⊆]-reflexivity-raw

  [⊆]-reflexivity-raw {SC = SC} = set id \{i} → [≡]-reflexivity-raw {A = SetContainer.elem(SC)(i)}

  [≡]-transitivity-raw : (A ≡ B) → (B ≡ C) → (A ≡ C)
  [⊆]-transitivity-raw : (A ⊆ B) → (B ⊆ C) → (A ⊆ C)
  [⊇]-transitivity-raw : (A ⊇ B) → (B ⊇ C) → (A ⊇ C)
  [⊇]-transitivity-raw {A = A}{B = B}{C = C} ab bc = [⊆]-transitivity-raw {A = C}{B = B}{C = A} bc ab

  [≡]-transitivity-raw (atom ab)  (atom bc) = atom (transitivity(_≡ₛ_) ab bc)
  [≡]-transitivity-raw (set lab rab) (set lbc rbc) = set ([⊇]-transitivity-raw lab lbc) ([⊆]-transitivity-raw rab rbc)

  [⊆]-transitivity-raw (set {SCₗ = SC₁} {SCᵣ = SC₂} mapₗ pₗ) (set {SCᵣ = SC₃} mapᵣ pᵣ) = set (mapᵣ ∘ mapₗ) \{i} → [≡]-transitivity-raw {A = SetContainer.elem(SC₁) i}{B = SetContainer.elem(SC₂)(mapₗ i)} {C = SetContainer.elem(SC₃)(mapᵣ(mapₗ i))} pₗ pᵣ

  instance
    [≡]-reflexivity : Reflexivity(_≡_ {ℓ})
    [≡]-reflexivity = intro [≡]-reflexivity-raw
  instance
    [⊆]-reflexivity : Reflexivity{T = SetContainer(T){ℓ}} ((_⊆_) on₂ set)
    [⊆]-reflexivity = intro [⊆]-reflexivity-raw
  instance
    [⊇]-reflexivity : Reflexivity{T = SetContainer(T){ℓ}} ((_⊇_) on₂ set)
    [⊇]-reflexivity = intro [⊇]-reflexivity-raw
  instance
    [≡]-symmetry : Symmetry(_≡_ {ℓ})
    Symmetry.proof [≡]-symmetry (atom ab) = atom (symmetry(_≡ₛ_) ab)
    Symmetry.proof [≡]-symmetry (set l r) = set r l
  instance
    [⊆]-antisymmetry : Antisymmetry(_⊆_ {ℓ})(_≡_)
    Antisymmetry.proof [⊆]-antisymmetry l@(set _ _) r@(set _ _) = set r l
  instance
    [⊇]-antisymmetry : Antisymmetry(_⊇_ {ℓ})(_≡_)
    Antisymmetry.proof [⊇]-antisymmetry l@(set _ _) r@(set _ _) = set l r
  instance
    [≡]-transitivity : Transitivity(_≡_ {ℓ})
    [≡]-transitivity = intro [≡]-transitivity-raw
  instance
    [⊆]-transitivity : Transitivity(_⊆_ {ℓ})
    [⊆]-transitivity = intro [⊆]-transitivity-raw
  instance
    [⊇]-transitivity : Transitivity(_⊇_ {ℓ})
    [⊇]-transitivity = intro [⊇]-transitivity-raw
  instance
    [≡]-equivalence : Equivalence(_≡_ {ℓ})
    [≡]-equivalence = intro
  instance
    Iset-equiv : Equiv(IUset(T){ℓ})
    Equiv._≡_ Iset-equiv = _≡_
    Equiv.equivalence Iset-equiv = [≡]-equivalence

  [≡]-to-[⊆] : (set SCₗ ≡ set SCᵣ) → (set SCₗ ⊆ set SCᵣ)
  [≡]-to-[⊆] (set l r) = r

  [≡]-to-[⊇] : (set SCₗ ≡ set SCᵣ) → (set SCₗ ⊇ set SCᵣ)
  [≡]-to-[⊇] (set l r) = l

  [∈]-of-elem : ∀{A : IUset(T){ℓ}}{ia : Index(A)} → (elem(A)(ia) ∈ A)
  [∈]-of-elem {A = setc {Index} elem} {ia} = set ([∃]-intro ia ⦃ [≡]-reflexivity-raw ⦄)

  [⊆]-membership : ((_⊆_ on₂ set) SCₗ SCᵣ) ← (∀{x : IUset(T)} → (x ∈ set SCₗ) → (x ∈ set SCᵣ))
  [⊆]-membership {SCₗ = SCₗ} {SCᵣ = SCᵣ} proof = set
    (ia    ↦ [∃]-witness ([∈]-proof(proof {elem(set SCₗ)(ia)} ([∈]-of-elem {A = set SCₗ}))))
    (\{ia} → [∃]-proof   ([∈]-proof(proof {elem(set SCₗ)(ia)} ([∈]-of-elem {A = set SCₗ}))))

module Oper ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  open import Data renaming (Empty to EmptyType)
  open import Data.Boolean
  open import Data.Boolean.Stmt
  open import Data.Either as Either using (_‖_)
  open import Functional
  open import Logic
  open import Logic.Classical
  open import Type.Dependent
  open import Type.Dependent.Functions
  open import Type.Properties.Decidable
  open import Type.Properties.Decidable.Proofs
  open import Syntax.Function
  instance _ = classical-to-decidable

  -- TODO: Many of these operations are simply copy-pasted from Sets.IterativeSet with small modifications.

  -- The operation converting an IUset from a lower universe level to a higher universe level.
  IUset-level-up : let _ = ℓ₁ in IUset(T){ℓ₂} → IUset(T){ℓ₁ Lvl.⊔ ℓ₂}
  IUset-level-up          (atom x) = atom x
  IUset-level-up {ℓ₁}{ℓ₂} (setc {Index} elem) = setc {Lvl.Up{ℓ₁}{ℓ₂}(Index)} \{(Lvl.up i) → IUset-level-up{ℓ₁}{ℓ₂}(elem(i))}

  -- The empty set, consisting of no elements.
  -- Index is the empty type, which means that there are no objects pointing to elements in the set.
  ∅ : IUset(T){ℓ}
  ∅ = setc empty

  -- Lifts an unary operation on set containers to an unary operation on IUsets.
  set-operator₁ : (SetContainer(T){ℓ₁} → SetContainer(T){ℓ₂}) → (IUset(T){ℓ₁} → IUset(T){ℓ₂})
  set-operator₁ op (atom _) = ∅
  set-operator₁ op (set  A) = set (op A)

  -- Lifts a binary operation on set containers to a binary operation on IUsets.
  set-operator₂ : (SetContainer(T){ℓ} → SetContainer(T){ℓ} → SetContainer(T){ℓ}) → (IUset(T){ℓ} → IUset(T){ℓ} → IUset(T){ℓ})
  set-operator₂ op (atom _) (atom _) = ∅
  set-operator₂ op (atom _) (set  B) = set B
  set-operator₂ op (set  A) (atom _) = set A
  set-operator₂ op (set  A) (set  B) = set (op A B)

  -- Filters a set to only contain set elements.
  sets-of : IUset(T){ℓ} → IUset(T){ℓ}
  sets-of{ℓ} = set-operator₁(A ↦ intro (Σ(SetContainer.Index(A)) (ia ↦ Lvl.Convert(IsSet(SetContainer.elem(A)(ia))){ℓ})) \{(intro ia p) → SetContainer.elem(A)(ia)})

  -- Filters a set to only contain atomic elements.
  atoms-of : IUset(T){ℓ} → IUset(T){ℓ}
  atoms-of{ℓ} = set-operator₁(A ↦ intro (Σ(SetContainer.Index(A)) (ia ↦ Lvl.Convert(IsAtom(SetContainer.elem(A)(ia))){ℓ})) \{(intro ia p) → SetContainer.elem(A)(ia)})

  -- The singleton set, consisting of one element.
  -- Index is the unit type, which means that there are a single object pointing to a single element in the set.
  singleton : IUset(T){ℓ} → IUset(T){ℓ}
  singleton = setc{Index = Unit} ∘ const

  -- The pair set, consisting of two elements.
  -- Index is the boolean type, which means that there are two objects pointing to two elements in the set.
  pair : IUset(T){ℓ} → IUset(T){ℓ} → IUset(T){ℓ}
  pair A B = setc{Index = Lvl.Up(Bool)} ((if_then B else A) ∘ Lvl.Up.obj)

  -- The union operator.
  -- Index(A ∪ B) is the either type of two indices, which means that both objects from the A and the B index point to elements in the set.
  _∪_ : IUset(T){ℓ} → IUset(T){ℓ} → IUset(T){ℓ}
  A ∪ B = setc{Index = Index(A) ‖ Index(B)} (Either.map1 (elem(A)) (elem(B)))
  -- _∪_ = set-operator₂([ℰ]-map₂ Either.map1)

  -- The big union operator.
  -- Index(⋃ A) is the dependent sum type of an Index(A) and the index of the element this index points to.
  ⋃ : IUset(T){ℓ} → IUset(T){ℓ}
  ⋃ A = setc{Index = Σ(Index(A)) (ia ↦ Index(elem(A)(ia)))} (\{(intro ia i) → elem(elem(A)(ia))(i)})

  indexFilter : (A : IUset(T){ℓ}) → (Index(A) → Stmt{ℓ}) → IUset(T){ℓ}
  indexFilter A P = setc{Index = Σ(Index(A)) P} (elem(A) ∘ Σ.left)

  filter : (A : IUset(T){ℓ}) → (IUset(T){ℓ} → Stmt{ℓ}) → IUset(T){ℓ}
  filter{ℓ} A P = indexFilter A (P ∘ elem(A))

  indexFilterBool : (A : IUset(T){ℓ}) → (Index(A) → Bool) → IUset(T){ℓ}
  indexFilterBool A f = indexFilter A (Lvl.Up ∘ IsTrue ∘ f)

  filterBool : (A : IUset(T){ℓ}) → (IUset(T){ℓ} → Bool) → IUset(T){ℓ}
  filterBool A f = indexFilterBool A (f ∘ elem(A))

  map : (IUset(T){ℓ} → IUset(T){ℓ}) → (IUset(T){ℓ} → IUset(T){ℓ})
  map f(A) = setc{Index = Index(A)} (f ∘ elem(A))

  -- The power set operator.
  -- Index(℘(A)) is a function type. An instance of such a function represents a subset, and essentially maps every element in A to a boolean which is interpreted as "in the subset of not".
  -- Note: This only works properly in a classical setting. Trying to use indexFilter instead result in universe level problems.
  ℘ : IUset(T){ℓ} → IUset(T){ℓ}
  ℘(A) = setc{Index = Index(A) → Bool} (indexFilterBool A)

  -- The set of ordinal numbers of the first order.
  ω : IUset(T){ℓ}
  ω = setc{Index = Lvl.Up ℕ} (N ∘ Lvl.Up.obj) where
    open import Numeral.Natural
    N : ℕ → IUset(T){ℓ}
    N(𝟎)    = ∅
    N(𝐒(n)) = N(n) ∪ singleton(N(n))

  module Proofs where
    open import Data.Boolean
    open import Data.Tuple as Tuple using ()
    open import Logic.Propositional
    open import Logic.Predicate
    open import Structure.Function
    open import Structure.Relator.Properties

    instance
      atom-function : Function(atom{T = T}{ℓ})
      Function.congruence atom-function = atom

    {-instance
      set-function : Function(set{T = T}{ℓ})
      Function.congruence set-function = ?
    -}

    -- If there is an element in the empty set, then there exists an instance of the empty type by definition, and that is false by definition.
    ∅-membership : ∀{x : IUset(T){ℓ₁}} → (x ∉ ∅ {ℓ₂})
    ∅-membership (set())

    -- There is a bijection between (A ‖ B) and ∃{Lvl.Up Bool}(\{(Lvl.up 𝐹) → A ; (Lvl.up 𝑇) → B}).
    pair-membership : ∀{a b x : IUset(T){ℓ}} → (x ∈ pair a b) ↔ (x ≡ a)∨(x ≡ b)
    Tuple.left (pair-membership {x = x}) ([∨]-introₗ p) = set ([∃]-intro (Lvl.up 𝐹) ⦃ p ⦄)
    Tuple.left (pair-membership {x = x}) ([∨]-introᵣ p) = set ([∃]-intro (Lvl.up 𝑇) ⦃ p ⦄)
    Tuple.right pair-membership (set ([∃]-intro (Lvl.up 𝐹) ⦃ atom p ⦄)) = [∨]-introₗ (atom p)
    Tuple.right pair-membership (set ([∃]-intro (Lvl.up 𝑇) ⦃ atom p ⦄)) = [∨]-introᵣ (atom p)
    Tuple.right pair-membership (set ([∃]-intro (Lvl.up 𝐹) ⦃ set l r ⦄)) = [∨]-introₗ (set l r)
    Tuple.right pair-membership (set ([∃]-intro (Lvl.up 𝑇) ⦃ set l r ⦄)) = [∨]-introᵣ (set l r)

    -- There is a bijection between (A) and ∃{Unit}(\{<> → A}).
    singleton-membership : ∀{a x : IUset(T){ℓ}} → (x ∈ singleton(a)) ↔ (x ≡ a)
    Tuple.left singleton-membership xin = set ([∃]-intro <> ⦃ xin ⦄)
    Tuple.right singleton-membership (set ([∃]-intro _ ⦃ eq ⦄)) = eq

    [∪]-membership : ∀{A B x : IUset(T){ℓ}} → (x ∈ (A ∪ B)) ↔ (x ∈ A)∨(x ∈ B)
    Tuple.left [∪]-membership ([∨]-introₗ (set ([∃]-intro ia))) = set ([∃]-intro (Either.Left  ia))
    Tuple.left [∪]-membership ([∨]-introᵣ (set ([∃]-intro ib))) = set ([∃]-intro (Either.Right ib))
    Tuple.right ([∪]-membership {A = set x}) (set ([∃]-intro ([∨]-introₗ ia))) = [∨]-introₗ (set ([∃]-intro ia))
    {-# CATCHALL #-}
    Tuple.right ([∪]-membership {B = set x}) (set ([∃]-intro ([∨]-introᵣ ib))) = [∨]-introᵣ (set ([∃]-intro ib))

    [⊆]-with-elem : ∀{SCₗ SCᵣ : SetContainer(T){ℓ}} → (xy : set SCₗ ⊆ set SCᵣ) → ∀{ix} → (elem (set SCₗ) ix ≡ elem (set SCᵣ) ([⊆]-map xy ix))
    [⊆]-with-elem (set map proof) {ix} = proof{ix}

{-
    open import Lang.Inspect
    import      Relator.Equals as Equals
    import      Relator.Equals.Proofs.Equivalence as Equals
    [⋃]-membership : ∀{A x : IUset(T){ℓ}} → (x ∈ (⋃ A)) ↔ ∃(a ↦ (a ∈ A) ∧ (x ∈ a))
    Tuple.left ([⋃]-membership {A = A@(set _)}) ([∃]-intro a@(set _) ⦃ [∧]-intro aA xa ⦄) with elem A ([∈]-index aA) | [∈]-elem aA | inspect ⦃ Equals.[≡]-equiv ⦄ (elem A) ([∈]-index aA)
    ... | set _ | (set aA-mapₗ aA-mapᵣ) | intro pp = set ([∃]-intro (intro ([∈]-index aA) (Equals.[≡]-substitutionₗ pp {f = Index} ([⊆]-map aA-mapᵣ ([∈]-index xa)))) ⦃ [≡]-transitivity-raw ([∈]-elem xa) ([⊆]-with-elem ([≡]-to-[⊆] ([≡]-transitivity-raw ([∈]-elem aA) ([≡]-transitivity-raw (sub₂(Equals._≡_)(_≡_) pp) {!!}))) {[∈]-index xa}) ⦄)
    Tuple.right ([⋃]-membership {A = A@(atom _)}) (set ([∃]-intro (intro iA ia))) = {!!}
    ∃.witness (Tuple.right ([⋃]-membership {A = A@(set _)}) (set ([∃]-intro (intro iA ia)))) = elem(A) iA
    ∃.proof (Tuple.right ([⋃]-membership {A = A@(set _)}) (set ([∃]-intro (intro iA ia) ⦃ proof ⦄))) = [∧]-intro ([∈]-of-elem {A = A}) {!set([∃]-intro ia ⦃ proof ⦄)!}
-}

{-  Σ.left  (∃.witness (Tuple.left ([⋃]-membership {A = A} {x}) ([∃]-intro a ⦃ [∧]-intro ([∃]-intro iA) _ ⦄))) = iA
  Σ.right (∃.witness (Tuple.left ([⋃]-membership {A = A} {x}) ([∃]-intro a ⦃ [∧]-intro ([∃]-intro iA ⦃ aA ⦄) ([∃]-intro ia) ⦄))) = _⊆_.map (_≡_.right aA) ia

  ∃.proof (Tuple.left ([⋃]-membership {A = A} {x}) ([∃]-intro a ⦃ [∧]-intro ([∃]-intro iA ⦃ aA ⦄) ([∃]-intro ia ⦃ xa ⦄) ⦄)) = [≡]-transitivity-raw xa ([⊆]-with-elem (sub₂(_≡_)(_⊆_) aA) {ia})

  ∃.witness (Tuple.right ([⋃]-membership {A = A} {x}) ([∃]-intro (intro iA ia) ⦃ proof ⦄)) = elem(A)(iA)
  Tuple.left (∃.proof (Tuple.right ([⋃]-membership {A = A} {x}) ([∃]-intro (intro iA ia) ⦃ proof ⦄))) = [∈]-of-elem {A = A}
  ∃.witness (Tuple.right (∃.proof (Tuple.right ([⋃]-membership {A = A} {x}) ([∃]-intro (intro iA ia) ⦃ proof ⦄)))) = ia
  ∃.proof (Tuple.right (∃.proof (Tuple.right ([⋃]-membership {A = A} {x}) ([∃]-intro (intro iA ia) ⦃ proof ⦄)))) = proof
-}

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 treeThms where

open import lib

-- simple Tree type storing natural numbers
data Tree : Set where
  Node : ℕ → Tree → Tree → Tree
  Leaf : Tree

mirror : Tree → Tree
mirror (Node x t1 t2) = Node x (mirror t2) (mirror t1)
mirror Leaf = Leaf

mirror-mirror : ∀ (t : Tree) → mirror (mirror t) ≡ t
mirror-mirror Leaf = refl
mirror-mirror (Node x t1 t2) rewrite mirror-mirror t2 | mirror-mirror t1 = refl

size : Tree → ℕ
size (Node x t t₁) = 1 + size t + size t₁
size Leaf = 1

height : Tree → ℕ
height (Node x t t₁) = 1 + (max (height t) (height t₁))
height Leaf = 0

numLeaves : Tree → ℕ
numLeaves (Node x t t₁) = numLeaves t + numLeaves t₁
numLeaves Leaf = 1

perfect : ℕ → Tree
perfect zero = Leaf
perfect (suc n) = Node 1 (perfect n) (perfect n)

-- I found I needed the +0 theorem from nat-thms.agda in the IAL
perfect-numLeaves : ∀(n : ℕ) → numLeaves (perfect n) ≡ 2 pow n
perfect-numLeaves zero = refl
perfect-numLeaves (suc n) rewrite +0 (2 pow n) |  perfect-numLeaves n  = refl

perfect-size : ∀(n : ℕ) → suc (size (perfect n)) ≡ 2 pow (suc n)
perfect-size zero = refl
perfect-size (suc n) rewrite  sym (perfect-size n) | +0 (size(perfect n)) | sym (+suc(size(perfect n))(size(perfect n)))= refl

-- helper lemma I found I needed below
max-same : ∀ (n : ℕ) → max n n ≡ n
max-same n rewrite <-irrefl n = refl

perfect-height : ∀(n : ℕ) → height (perfect n) ≡ n
perfect-height zero = refl
perfect-height (suc n) rewrite max-same (height(perfect n)) | perfect-height n = refl

numNodes : Tree → ℕ
numNodes (Node x t1 t2) = 1 + numNodes t1 + numNodes t2
numNodes Leaf = 0

-- flatten a tree into a list of all the values stored at the nodes
prefixFlatten : Tree → 𝕃 ℕ
prefixFlatten (Node x t1 t2) = x :: prefixFlatten t1 ++ prefixFlatten t2
prefixFlatten Leaf = []

-- I found I needed a theorem from list-thms.agda in the IAL
length-flatten : ∀(t : Tree) → numNodes t ≡ length (prefixFlatten t)
length-flatten (Node x t1 t2) rewrite length-++(prefixFlatten t1) (prefixFlatten t2) | length-flatten t1 | length-flatten t2 = refl
length-flatten Leaf = refl


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Sigma
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.Reflection renaming (returnTC to return; bindTC to _>>=_)

_>>_ : ∀ {a} {b} {A : Set a} {B : Set b}
     → TC A → TC B → TC B
x >> y = x >>= λ _ → y

macro
  false-oh-no-actually-true : Term → TC ⊤
  false-oh-no-actually-true goal = do
    runSpeculative (do
      unify goal (con (quote false) [])
      return (tt , false))
    unify goal (con (quote true) [])

  false-yes-really-false : Term → TC ⊤
  false-yes-really-false goal =
    runSpeculative (do
      unify goal (con (quote false) [])
      return (tt , true))

test₁ : Bool
test₁ = false-oh-no-actually-true

_ : test₁ ≡ true
_ = refl

test₂ : Bool
test₂ = false-yes-really-false

_ : test₂ ≡ false
_ = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda