text:
{-# OPTIONS --no-unicode #-} -- turn off automatic unicode insertion

module 02-agda-start where

-------------------------------------------------------------------------------------------------------
-- ADDITIONAL RESOURCES |
-------------------------
-- допълнителни ресурси:
-- https://github.com/pigworker/CS410-17 - курс (има и домашни) с видео лекции, добър лектор
-- ^ има още много repo-та които си струват разглеждане
-- един от хората измислили Applicative бтв, както и with-abstraction, което ще видим по-късно

-- https://plfa.github.io/ - книга с подробни обяснения и описания, има и упражнения, втората част се занимава с имплементиране на ламбда смятане

-------------------------------------------------------------------------------------------------------
-- CHEATSHEETS |
----------------
-- SPACEMACS CHEATSHEET:
-- <SPC> h <SPC> -- search for help, including agda's help

-- <SPC> <TAB> - go to previous buffer -- helpful to go back after looking at help
-- <SPC> z x -/= - decrease/increase font size

-- normal emacs agda bindings:
-- https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#keybindings
-- spacemacs agda layer bindings (but also can open them with <SPC> h <SPC> inside spacemacs):
-- https://github.com/syl20bnr/spacemacs/tree/master/layers/%2Blang/agda#key-bindings

-- AGDA CHEATSHEET (descending importance):
-- <SPC> m l - reload file

-- <SPC> m , - (in goal) show context and goal

-- <SPC> m . - (in goal) show type of expression in goal. if goal is empty agda will ask for an expression to type

-- <SPC> m c - case split on goal contents
--             if goal is empty, will ask for what to split on

-- <SPC> m r - introduce constructor (if non-ambiguous)
--             can also introduce constructors, lambdas, record constructors
--             if there's a function in the goal it will "introduce" it with its arguments as new goals

-- <SPC> m <SPC> - when in a goal, replace the goal with the expression currently in the goal
--               if the goal is empty, agda will ask for an expression to insert
--               obviously only works if types match

-- <SPC> m a - (invoke "agsy") agda try your best to figure this out!
--             you can add names to a goal to give hints to agda, e.g. if you want to use a function "f"

-- <SPC> m x r - restart agda

-- <SPC> u <SPC> u <other-command> - kindly ask agda to evaluate and desugar everything as much as it can when executing <other-command>

-- <SPC> m f - go to next goal

-- <SPC> m n - compute an expression

-- <SPC> m h - when in a hole, compute what the type of a helper function you need here would be

-------------------------------------------------------------------------------------------------------
-- EXERCISE |
-------------

-- a haskell type declaration
--data List a
--  = Nil
--  | Cons a (List a)
--

-- same thing but in agda
--data List (A : Set) : Set where
--  Nil : List A
--  Cons : A -> List A -> List A

-- X : Y - "X is of type Y"
-- Set is the "kind" of types
-- it's safe to just read it as "Type" instead

-- identity function, with an explicit type as an argument
-- in agda we don't have (and don't need) "implicit polymorphic types"
-- like how in haskell when we write a -> a we actually mean "for all a (a -> a)"
-- so instead we "simulate" it by taking a type as an argument
id' : (A : Set) -> A -> A
id' _ x = x

-- we can also have it implicitly inferred, by using {} to specify the argument
-- agda doesn't have global type inference (because it's not decidable in general) - you always need to write top level signatures
id : {A : Set} -> A -> A
id x = x

-- a data type definition
-- it has no constructors
-- therefore it cannot be constructed!
-- this is an encoding of "falsity" exactly because you can't make values (proofs) of it
-- called Zero because it contains 0 values
data Zero : Set where -- ⊥

-- therefore if you are handed something of Zero
-- you can try to inspect it, to show that it's not possible for it to exist!
-- this is "efq"
naughtE : {A : Set} -> Zero -> A
naughtE ()
--      ^ this bit is special syntax for "impossible case" - not the same thing as () in haskell

-- a record type - "dual" in some sense to a data type
-- very similar to a struct in C:
-- in order to construct a record type, you need to give values for all its fields
-- this record has *no* fields, therefore to construct it you need to give *no values*
-- and it is therefore very easy to construct
-- it encodes "trivial truth" in logic, exactly because you don't need any assumptions to create it
-- the "constructor <>" syntax introduces a convenient way to create values from this type, instead of using record syntax
-- called One because it contains one value
record One : Set where -- unit/top/⊤
  constructor <>

-- an example value from One
one : One
one = <>

-- an example value constructed with record syntax
one' : One
one' = record {} -- no values to give!

-- example of a record type with some actual fields!
--record Student : Set where
--  field
--    fn : Number -- these types don't actually exist yet, but let's assume they do
--    name : String
--
--georgi : Student
--georgi =
--  record
--    { fn = {!81248!}
--    ; name = {!"Georgi"!}
--    }

-- boolean values - to construct a Two we either use the ff or the tt constructor
-- called Two because it has two values
data Two : Set where
  ff : Two
  tt : Two

-- an example of "mixfix" syntax
-- we can define a function with three arguments
-- the _s are where we would place arguments
if_then_else_ : {A : Set} -> Two -> A -> A -> A
if ff then t else e = e
if tt then t else e = t

-- we can write ordinary functions that return types, based on some value!
-- this function "promotes" the boolean *values* to their "corresponding" *logical types*
-- e.g. we convert the boolean "false" to our encoding of falsity - the type Zero
IsTrue : Two -> Set
IsTrue ff = Zero
IsTrue tt = One

_ : IsTrue tt
_ = <>

-- a sum type - it's either the left thing or the right thing
-- Either in haskell
-- as a logical construction it's a proof of either a or either b
data _+_ (A B : Set) : Set where -- A || B
  inl : A -> A + B
  inr : B -> A + B

_ : Zero + One
_ = inr <>

-- two-tuples defined as a record
-- a logical encoding for proof of *both* a *and* b
-- (a, b) in haskell
-- we will instead get this as a special case from our next construction
--record _*_ (A B : Set) : Set where -- A && B
--  constructor _,_
--  field
--    fst : A
--    snd : B

-- a **dependent two-tuple** - called a sigma type in books
-- **the type of the second field can depend on the value of the first**
-- this is an encoding of "exists" quantifiers-
-- to prove (constructively) ∃x.P(x), you must give me a x₀, and then prove that P(x₀)
-- which is effectively a two-tuple of a value x, and a proof P x
record _><_ (A : Set) (P : A -> Set) : Set where
  constructor _,_
  field
    fst : A
    snd : P fst

infixr 15 _><_
open _><_

-- an example of a dependent tuple
-- we give a value, and then show proof that the value satisfies our predicate "IsTrue"
-- ofcourse, if we give the value ff, we would not be able to construct this, because we cannot prove Zero
_ : Two >< IsTrue
_ = tt , <>

-- another example of construction of a sigma type
--data Nat : Set where
--  zero : Nat
--  suc : Nat -> Nat
--
--three : Nat
--three = suc (suc (suc zero))
--
--Even : Nat -> Set
--Even zero = One
--Even (suc zero) = Zero
--Even (suc (suc x)) = Even x
--
--twoIsEven : Nat >< Even
--twoIsEven = (suc (suc zero)) , <>

-- and now we can get our regular 2-tuples for free as a special case of sigma types
-- in which the second argument doesn't depend on the first (notice how our lambda ignores its argument)
_*_ : (A B : Set) -> Set
A * B = A >< \_ -> B
infixr 15 _*_

-- we can encode Either using a sigma type with Two as our left type!
-- to construct an Either
-- you must either use tt (the "left" constructor) in which case our if then else will compute to A, therefore we must give an A
-- or you must either use ff (the "right" constructor) in which case our if then else will compute to B, therefore we must give a B
Either : (A B : Set) -> Set
Either A B = Two >< \b -> if b then A else' B
  where
  -- note: I used another version of if_then_else, because our original one had arguments that are **values of some type**, i.e. (x : A), for some A : Set,
  -- but here we're actually using the **A itself** as an argument, and our original function handle this
  -- this one is **polymorphic over levels** (similar to kind polymorphism in haskell) - it works for both (x : A) and for (A : Set) and for a lot of other stuff
  if_then_else'_ : forall {l} -> {A : Set l} -> Two -> A -> A -> A
  if ff then t else' e = e
  if tt then t else' e = t

-- an example of a function using _*_
-- and a theorem at the same time
-- if you know that A * B is true, then you can also prove B * A (so some kind of symmetry/commutativity)
*-theorem1 : {A B : Set} -> A * B -> B * A
*-theorem1 (x , y) = y , x

-- peano-encoded natural numbers
data Nat : Set where
  zero : Nat
  suc : Nat -> Nat -- a recursive case in a constructor
{-# BUILTIN NATURAL Nat #-} -- pragma allows us to write literals, e.g. 2 to mean (suc (suc zero)), and also to compile these to Integer, if we compile to haskell

-- traditional left-recursive peano nat addition
-- how you define your functions has great repercussions!
-- because all your proofs will now have to look at the left argument of n +N m in order to proceed!
_+N_ : Nat -> Nat -> Nat
zero +N m = m
suc n +N m = suc (n +N m)

infixr 30 _+N_

-- an equality type
-- to show that x == y for some values x and y
-- you can do only one thing: show that x and y are actually the same value (by using the refl constructor)
-- this "syntactic equality" is internal to agda, but you can think of it as basically "the same structure" (when you look at e.g. constructors)
data _==_ {A : Set} : A -> A -> Set where
  refl : {x : A} -> x == x

infix 20 _==_
{-# BUILTIN EQUALITY _==_ #-} -- allows us to use rewrites for this equality type

-- a proof that 2 is equal to 2
-- since 2 is the same syntactic object (suc (suc zero)) as itself, we can use refl
twoIsTwo : 2 == 2
twoIsTwo = refl

-- similarly, in this case 1 +N 1 is not immediately the same thing as 2
-- but agda automatically applies (beta-reduces) the definition of +N as much as possible,
-- and can calculate that they are actually the same!
onePlusOneIsTwo : (1 +N 1) == 2
onePlusOneIsTwo = refl

-- another way to define == where the x is a parameter instead
--data _=='_ {A : Set} (x : A) -> A -> Set where
--  refl : x == x

-- a proof demonstrating how to use ==
-- this states that if you have two proofs of x and y being equal
-- then the proofs themselves are equal to one another!
==-unique : {A : Set} {x y : A} (p1 p2 : x == y) -> p1 == p2
==-unique refl refl = refl
-- note that this is not always true, and it is an active area of research (homotopy type theory),
-- which might provide solutions to problems in constructive mathematics
-- in it, you cannot prove this theorem, and indeed, there are p1 and p2 there, which *are not* equal to each other

-- ap allows us to "apply a function to both sides of an equality"
-- i.e. on a piece of paper we automatically assume this, because f is a function
ap : {A B : Set} {x y : A} (f : A -> B) -> x == y -> f x == f y
ap f refl = refl

-- this proof doesn't need to look at n at all, because we have a case for 0 +N _ in the definition of +N
-- and agda can automatically compute it
+N-left-zero : (n : Nat) -> 0 +N n == n
+N-left-zero n = refl

-- but it is not the same in this case!
-- and thus we use recursion to prove this
+N-right-zero : (n : Nat) -> n +N 0 == n
+N-right-zero zero = refl
+N-right-zero (suc n') = ap suc (+N-right-zero n')
-- another alternative to the last case would be to use "rewrite"
-- the rewrite declaration allows us to "rewrite" our goal by using an equality provided by us
-- i.e. if we have a goal that has some x's in it, and we have a proof (p : x == y)
-- then rewrite p will change all the x's into y's in our goal

+N-assoc : (n m k : Nat) -> (n +N m) +N k == n +N (m +N k)
+N-assoc zero m k = refl
+N-assoc (suc n) m k rewrite +N-assoc n m k = refl

---- EXERCISES ==
--
---- EXERCISE: == is symmetric
--==-symm : {A : Set} {x y : A} -> x == y -> y == x
--==-symm = ?
--
---- EXERCISE: == is transitive
--==-trans : {A : Set} {x y z : A} -> x == y -> y == z -> x == z
--==-trans = ?
--
---- EXERCISES Nats
--
---- EXERCISE: suc is injective
--suc-inj : {n m : Nat} -> suc n == suc m -> n == m
--suc-inj = ?

data _<=_ : Nat -> Nat -> Set where
  ozero : {n : Nat} -> zero <= n
  osuc : {n m : Nat} -> n <= m -> suc n <= suc m

-- TODO: show some inequalities

---- EXERCISE: <=-refl
--<=-refl : (n : Nat) -> n <= n
--<=-refl n = ?
--
---- EXERCISE: <=-trans
--<=-trans : {n m k : Nat} -> n <= m -> m <= k -> n <= k
--<=-trans = ?
--
---- EXERCISE: suc n is not less than or equal to n
--suc-suc-not-<= : {n : Nat} -> suc n <= n -> Zero
--suc-suc-not-<= = ?
--
---- EXERCISE: <= proofs are unique
---- use ap or rewrite!
--<=-unique : {n m : Nat} -> (p1 p2 : n <= m) -> p1 == p2
--<=-unique = ?
--
---- lists
--
--data List (A : Set) : Set where
--  [] : List A
--  _,-_ : A -> List A -> List A
--
--infixr 50 _,-_
--
---- EXERCISE:
---- Define list appending
---- HINT: look at +N if you haven't done this before
--_+L_ : {A : Set} -> List A -> List A -> List A
--xs +L ys = ?
--
--infixr 30 _+L_
--
---- EXERCISE:
---- +L is a monoid - with what left and right unit?
---- i.e. for what x is it true that for any xs:
---- x +L xs == xs and xs +L x == xs
---- TODO: delete []
--+L-left-id : {A : Set} (xs : List A) -> [] +L xs == xs
--+L-left-id = ?
--
--+L-right-id : {A : Set} (xs : List A) -> xs +L [] == xs
--+L-right-id = ?
--
---- EXERCISE:
---- +L is associative
---- HINT: look at +N-assoc
--+L-assoc : {A : Set} (xs ys zs : List A) -> (xs +L ys) +L zs == xs +L (ys +L zs)
--+L-assoc = ?
--
---- EXERCISE: list map
---- define map for lists - apply a function to every argument
--map : {A B : Set} -> (A -> B) -> List A -> List B
--map = ?
--
---- EXERICSE: mapping id is the same as just id
--map-id-is-id : {A : Set} -> (xs : List A) -> map id xs == xs
--map-id-is-id = ?
---- Note: we apply the argument to avoid extensionality issues
--
---- left-to-right composition
--_<<_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
--(f << g) x = ?
--
---- EXERCISE: mapping a composition is the same as composing mappings
---- <SPC> u <SPC> u <other-command>
---- might be useful here
--map-compose : {A B C : Set} (f : B -> C) (g : A -> B) (xs : List A) -> map (f << g) xs == (map f << map g) xs
--map-compose = ?
--
---- EXERCISE: mapping after appending is the same as first mapping and then appending
--map-distrib-+L : {A B : Set} (f : A -> B) (xs ys : List A) -> map f (xs +L ys) == map f xs +L map f ys
--map-distrib-+L = ?
--
---- EXERCISE: length-indexed lists - vectors
---- "lists that know their length"
--
--data Vector (A : Set) : Nat -> Set where
--  [] : Vector A zero -- the empty vector has a length of 0
--  _,-_ : {n : Nat} -> A -> Vector A n -> Vector A (suc n) -- if we cons an element to a vector of length n, we get a vector of length (suc n)
--
---- EXERCISE: We can now define a safe head and tail - you can't call them with []
---- Compare this to the default ones in haskell, that can throw exceptions
--vhead : {A : Set} {n : Nat} -> Vector A (suc n) -> A
--vhead = ?
--
--vtail : {A : Set} {n : Nat} -> Vector A (suc n) -> Vector A n
--vtail = ?
--
---- EXERCISE: We can also define "safe" take, that does not "overshoot"
---- Note how we don't need to pass n explicitly, because n <= m holds this information already
--vtake : {A : Set} {n m : Nat} -> n <= m -> Vector A m -> Vector A n
--vtake = ?
--
---- EXERCISE: Our zip is also "safe" in that we don't lose any information from either vector
--vzip : {A B : Set} {n : Nat} -> Vector A n -> Vector B n -> Vector (A * B) n
--vzip = ?
--
---- EXERCISE: Append vectors
---- What type should this function have?
---- _+V_ : ?
--
---- EXERCISE: We can split a vector if we know its size is a sum of two numbers
---- N.B.! you need to pattern match on the left number here, because otherwise agda doesn't know
---- what cases could be possible for the vector
--vsplit : {A : Set} (n m : Nat) -> Vector A (n +N m) -> Vector A n * Vector A m
--vsplit = ?
--
---- EXERCISE: Appending two vectors and then splitting them should yield the original two vectors!
---- What type should this have?
---- vsplit-+V-id : ?
--
---- EXERCISE: you can also suc on the right in +N
--+N-right-suc : (n m : Nat) -> suc (n +N m) == n +N suc m
--+N-right-suc = ?
--
---- EXERCISE: +N is commutative
---- prove lemmas if something seems too hard!
---- you'll need to prove a lemma for the recursive case
---- HINT:
---- use ==-symm and +N-right-zero in the base case
---- and +N-right-suc in the recursive case (+ rewrite or ap + ==-trans)
--+N-commut : (n m : Nat) -> n +N m == m +N n
--+N-commut = ?
--
---- EXERCISE: multiplication
---- use addition
--_*N_ : Nat -> Nat -> Nat
--n *N m = ?
--infixr 40 _*N_
--
---- EXERCISE: multiplication right identity
--*N-right-id : (n : Nat) -> n *N 1 == n
--*N-right-id = ?
--
---- EXERCISE: multiplication distributes over addition
---- HINT: use rewrite and ==-symm + +N-assoc in the recursive case
--*N-distrib-+N : (n m k : Nat) -> (n +N m) *N k == n *N k +N m *N k
--*N-distrib-+N = ?
--
---- EXERCISE: multiplication is associative
---- HINT: user *N-+N-distrib and rewrite
--*N-assoc : (n m k : Nat) -> (n *N m) *N k == n *N (m *N k)
--*N-assoc = ?


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

open import Prelude

module Syntax where

data Con           : (n : ℕ) → Set
Ctx : Set
Ctx = Σ ℕ Con
data Ty            : Ctx → Set
data Tm            : {Γ : Ctx} (A : Ty Γ) → Set
data Sub           : Ctx → Ctx → Set

𝔻 : (n : ℕ) → Con n
dangling : {n : ℕ} (Γ : Con n) → Sub (n , Γ) (n , 𝔻 n)

_[_]T : ∀ {Γ Δ} (A : Ty Γ) (σ : Sub Δ Γ) → Ty Δ
_[_]tm : ∀ {Γ Δ} {A : Ty Γ} (t : Tm A) (σ : Sub Δ Γ)  → Tm (A [ σ ]T)

_≃_ : ∀ (Γ Δ : Ctx) {γ : Sub Δ Γ} {δ : Sub Γ Δ} → Set

-- Type theory for globular sets
data Con where
  Start     : Con (O)
  Ext       : ∀ {n : ℕ} (Γ : Con (n)) → Con (S n)
  Drop      : ∀ {n : ℕ} (Γ : Con (S n)) → Con n

Ext' : Ctx → Ctx
Ext' Γ = (S (fst Γ) , Ext (snd Γ))

data Ty where
  ⇒/_         : ∀ {n} {Δ} (σ : Sub Δ (n , 𝔻 n)) → Ty Δ

data Sub where
  id          : ∀ {Γ} → Sub Γ Γ
  _∘_         : ∀ {Γ Δ Θ} (δ : Sub Θ Δ) (γ : Sub Δ Γ) → Sub Θ Γ
  Drop        : ∀ {n} (Γ : Con (S n)) → Sub (S n , Γ) (n , Drop Γ)
  Drop-       : ∀ {n} (Γ : Con (S n)) → Sub (n , Drop Γ) (S n , Γ)
  π₁          : ∀ (Γ : Ctx) → Sub (Ext' Γ) Γ
  _,_         : ∀ {Γ Δ} (γ : Sub Δ Γ) (a : Tm ((⇒/ (dangling (snd Γ))) [ γ ]T))  → Sub Δ (Ext' Γ)

data Tm where
--  π₂ : ∀ {Γ} (A : Ty Γ) → Tm {Γ , A} (A [ π₁ ]T)

postulate
  -- category structure
  idl : ∀ {Γ Δ} {γ : Sub Δ Γ} → (γ ∘ id) == γ
  idr : ∀ {Γ Δ} {γ : Sub Δ Γ} → (id ∘ γ) == γ
  assoc : ∀ {Γ Δ Θ Φ} {γ : Sub Δ Γ} {δ : Sub Θ Δ} {θ : Sub Φ Θ} → (θ ∘ (δ ∘ γ)) == ((θ ∘ δ) ∘ γ)
  -- skeleton
  iso : ∀ {n} {Γ : Con (S n)} → ((S n , Γ) ≃ (n , (Drop Γ))) {Drop- Γ} {Drop Γ}

𝔻 O = Start
𝔻 (S n) = Ext (𝔻 n)

dangling Start = id
dangling (Ext Γ) = {!!}
dangling (Drop Γ) = {!!}

_≃_ Γ Δ {γ} {δ} = {!((γ ∘ δ) == id) ^ ((δ ∘ γ) == id)!}

_[_]T {Γ} {Δ} (⇒/ σ₁) σ = ⇒/ (σ ∘ σ₁)

_[_]tm = {!!}

ext: agda

max_stars_repo_name: ThiBen/catt

max_issues_repo_name: thibautbenjamin/catt

max_forks_repo_name: thibautbenjamin/catt


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

module Algebra.Construct.Dyck where

open import Prelude
open import Algebra
open import Data.Nat using (_+_)
import Data.Nat.Properties as ℕ
open import Agda.Builtin.Nat using (_-_)

record Bal : Type₀ where
  constructor _⟩⟨_
  field
    left  : ℕ
    right : ℕ
open Bal public

infix 4.5 _⟩-⟨_ _⟩⟨_ _+⟨_⟩+_ _+⟨⟩+_

_⟩-⟨_ : ℕ → ℕ → Bal
zero  ⟩-⟨ m     = zero  ⟩⟨ m
suc n ⟩-⟨ zero  = suc n ⟩⟨ zero
suc n ⟩-⟨ suc m = n ⟩-⟨ m

_+⟨_⟩+_ : ℕ → Bal → ℕ → Bal
x +⟨ z ⟩+ y = right z + x ⟩⟨ left z  + y

_+⟨⟩+_ : Bal → Bal → Bal
x +⟨⟩+ y = left x +⟨ right x ⟩-⟨ left y ⟩+ right y

mempty : Bal
mempty = 0 ⟩⟨ 0

diff-zeroʳ : ∀ n → n ⟩-⟨ zero ≡ n ⟩⟨ zero
diff-zeroʳ zero    = refl
diff-zeroʳ (suc n) = refl

invert : Bal → Bal
invert (x ⟩⟨ y) = y ⟩⟨ x

diff-inv : ∀ x y → invert (x ⟩-⟨ y) ≡ y ⟩-⟨ x
diff-inv zero  zero = refl
diff-inv zero (suc y) = refl
diff-inv (suc x) zero = refl
diff-inv (suc x) (suc y) = diff-inv x y

open import Path.Reasoning

add-inv : ∀ x y → (x +⟨⟩+ y) ≡ invert (invert y +⟨⟩+ invert x)
add-inv (xl ⟩⟨ xr) (yl ⟩⟨ yr) = cong₂ _⟩⟨_ (cong (_+ xl) (cong left (diff-inv xr yl))) (cong (_+ yr) (cong right (diff-inv xr yl)))

0+⟨⟩ : ∀ x → mempty +⟨⟩+ x ≡ x
0+⟨⟩ (zero   ⟩⟨ xr) i = zero ⟩⟨ xr
0+⟨⟩ (suc xl ⟩⟨ xr) i = suc (ℕ.+-idʳ xl i) ⟩⟨ xr

⟨⟩+0 : ∀ x → x +⟨⟩+ mempty ≡ x
⟨⟩+0 (xl ⟩⟨ zero  ) i = xl ⟩⟨ zero
⟨⟩+0 (xl ⟩⟨ suc xr) i = xl ⟩⟨ suc (ℕ.+-idʳ xr i)

diff-sub : ∀ x y → left (x ⟩-⟨ y) ≡ x - y
diff-sub zero zero = refl
diff-sub zero (suc y) = refl
diff-sub (suc x) zero = refl
diff-sub (suc x) (suc y) = diff-sub x y

diff-subʳ : ∀ x y → right (x ⟩-⟨ y) ≡ y - x
diff-subʳ zero zero = refl
diff-subʳ zero (suc y) = refl
diff-subʳ (suc x) zero = refl
diff-subʳ (suc x) (suc y) = diff-subʳ x y

minus-plus : ∀ x y z → x - y - z ≡ x - (y + z)
minus-plus x zero z = refl
minus-plus zero (suc y) zero = refl
minus-plus zero (suc y) (suc z) = refl
minus-plus (suc x) (suc y) z = minus-plus x y z

lhs″ : ∀ zl xr yl yr → (zl - ((xr - yl) + yr)) + (yl - xr) ≡ ((zl - yr) + yl) - xr
lhs″ zl zero zero yr = refl
lhs″ zl zero (suc yl) yr = refl
lhs″ zl (suc xr) zero yr = ℕ.+-idʳ _ ; (cong (zl -_) (ℕ.+-comm (suc xr) yr) ; sym (minus-plus zl yr (suc xr))) ; sym (cong (_- suc xr) (ℕ.+-idʳ (zl - yr)))
lhs″ zero (suc xr) (suc yl) zero = lhs″ zero xr yl zero
lhs″ zero (suc xr) (suc yl) (suc yr) = lhs″ zero xr yl (suc yr)
lhs″ (suc zl) (suc xr) (suc yl) zero = lhs″ (suc zl) xr yl zero ; cong (_- xr) (sym (ℕ.+-suc zl yl))
lhs″ (suc zl) (suc xr) (suc yl) (suc yr) = cong (_+ (yl - xr)) (cong (suc zl -_) (ℕ.+-suc (xr - yl) yr)) ; lhs″ zl (suc xr) (suc yl) yr

rhs‴ : ∀ x y z → x + y - z ≡ x - (z - y) + (y - z)
rhs‴ zero zero zero = refl
rhs‴ zero zero (suc z) = refl
rhs‴ zero (suc y) zero = refl
rhs‴ (suc x) zero zero = refl
rhs‴ (suc x) (suc y) zero = refl
rhs‴ zero (suc y) (suc z) = rhs‴ zero y z
rhs‴ (suc x) zero (suc z) = cong (_- z) (ℕ.+-idʳ x) ; sym (ℕ.+-idʳ (x - z))
rhs‴ (suc x) (suc y) (suc z) = cong (_- z) (ℕ.+-suc x y) ; rhs‴ (suc x) y z

rhs″ : ∀ xr yl yr zl → ((xr - yl) + yr) - zl ≡ xr - (zl - yr + yl) + (yr - zl)
rhs″ (suc xr) (suc yl) yr zl = rhs″ xr yl yr zl ; cong (λ zy → suc xr - zy + (yr - zl)) (sym (ℕ.+-suc (zl - yr) yl))
rhs″ zero zero zero zero = refl
rhs″ zero zero zero (suc zl) = refl
rhs″ zero zero (suc yr) zero = refl
rhs″ zero zero (suc yr) (suc zl) = rhs″ zero zero yr zl
rhs″ zero (suc yl) zero zero = refl
rhs″ zero (suc yl) zero (suc zl) = refl
rhs″ zero (suc yl) (suc yr) zero = refl
rhs″ zero (suc yl) (suc yr) (suc zl) = rhs″ zero (suc yl) yr zl
rhs″ (suc xr) zero zero zero = refl
rhs″ (suc xr) zero (suc yr) zero = refl
rhs″ (suc xr) zero zero     (suc zl) = cong (_- zl) (ℕ.+-idʳ xr) ; cong (xr -_) (sym (ℕ.+-idʳ zl)) ; sym (ℕ.+-idʳ (xr - (zl + zero)))
rhs″ (suc xr) zero (suc yr) (suc zl) = cong (_- zl) (ℕ.+-suc xr yr) ;  rhs‴ (suc xr) yr zl ; sym (cong (λ zy → suc xr - zy + (yr - zl)) (ℕ.+-idʳ (zl - yr)))

⟨⟩-assoc : Associative _+⟨⟩+_
⟨⟩-assoc (xl ⟩⟨ xr ) (yl ⟩⟨ yr ) (zl ⟩⟨ zr) = cong₂ _⟩⟨_ lhs rhs
  where

  lhs′ : ∀ xr yl yr zl → right (left (xr ⟩-⟨ yl) + yr ⟩-⟨ zl) + right (xr ⟩-⟨ yl) ≡ right (xr ⟩-⟨ right (yr ⟩-⟨ zl) + yl)
  lhs′ xr yl yr zl =
    right (left (xr ⟩-⟨ yl) + yr ⟩-⟨ zl) + right (xr ⟩-⟨ yl) ≡⟨ cong₂ _+_ (diff-subʳ (left (xr ⟩-⟨ yl) + yr) zl) (diff-subʳ xr yl) ⟩
    (zl - (left (xr ⟩-⟨ yl) + yr)) + (yl - xr) ≡⟨ cong (λ xy → (zl - (xy + yr)) + (yl - xr)) (diff-sub xr yl) ⟩
    (zl - ((xr - yl) + yr)) + (yl - xr) ≡⟨ lhs″ zl xr yl yr ⟩
    ((zl - yr) + yl) - xr ≡˘⟨ cong (λ yz → (yz + yl) - xr) (diff-subʳ yr zl) ⟩
    (right (yr ⟩-⟨ zl) + yl) - xr ≡˘⟨ diff-subʳ xr _ ⟩
    right (xr ⟩-⟨ right (yr ⟩-⟨ zl) + yl) ∎

  lhs : right (left (xr ⟩-⟨ yl) + yr ⟩-⟨ zl) + (right (xr ⟩-⟨ yl) + xl) ≡ right (xr ⟩-⟨ right (yr ⟩-⟨ zl) + yl) + xl
  lhs = sym (ℕ.+-assoc _ (right (xr ⟩-⟨ yl)) xl) ; cong (_+ xl) (lhs′ xr yl yr zl)

  rhs′ : ∀ xr yl yr zl → left (left (xr ⟩-⟨ yl) + yr ⟩-⟨ zl) ≡ left (xr ⟩-⟨ right (yr ⟩-⟨ zl) + yl) + left (yr ⟩-⟨ zl)
  rhs′ xr yl yr zl =
    left (left (xr ⟩-⟨ yl) + yr ⟩-⟨ zl) ≡⟨ diff-sub _ zl ⟩
    left (xr ⟩-⟨ yl) + yr - zl ≡⟨ cong (_- zl) (cong (_+ yr) (diff-sub xr yl)) ⟩
    (xr - yl) + yr - zl ≡⟨ rhs″ xr yl yr zl ⟩
    (xr - ((zl - yr) + yl)) + (yr - zl) ≡˘⟨ cong (λ yz → (xr - (yz + yl)) + (yr - zl)) (diff-subʳ yr zl) ⟩
    (xr - (right (yr ⟩-⟨ zl) + yl)) + (yr - zl) ≡˘⟨ cong₂ _+_ (diff-sub xr _) (diff-sub yr zl) ⟩
    left (xr ⟩-⟨ right (yr ⟩-⟨ zl) + yl) + left (yr ⟩-⟨ zl) ∎

  rhs : left (left (xr ⟩-⟨ yl) + yr ⟩-⟨ zl) + zr ≡ left (xr ⟩-⟨ right (yr ⟩-⟨ zl) + yl) + (left (yr ⟩-⟨ zl) + zr)
  rhs = cong (_+ zr) (rhs′ xr yl yr zl) ; ℕ.+-assoc (left (xr ⟩-⟨ right (yr ⟩-⟨ zl) + yl)) (left (yr ⟩-⟨ zl)) zr

semigroupBal : Semigroup _
semigroupBal .Semigroup.𝑆 = Bal
semigroupBal .Semigroup._∙_ = _+⟨⟩+_
semigroupBal .Semigroup.assoc = ⟨⟩-assoc

monoidBal : Monoid _
Monoid.𝑆 monoidBal = Bal
Monoid._∙_ monoidBal = _+⟨⟩+_
Monoid.ε monoidBal = mempty
Monoid.assoc monoidBal = ⟨⟩-assoc
Monoid.ε∙ monoidBal = 0+⟨⟩
Monoid.∙ε monoidBal = ⟨⟩+0

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Structure.Operator.Monoid.Invertible where

open import Functional
import      Lvl
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Type

private variable ℓ ℓₗ ℓₑ : Lvl.Level
private variable T : Type{ℓ}
private variable _⨞_ : T → T → Type{ℓₗ}

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) where
  -- Generalizes the following examples in ℕ:
  -- • Lesser than or equal: (5+? = 8)  ⇔ (5 ≤ 8)
  -- • Divides             : (5*? = 10) ⇔ (5 ∣ 10)
  record InverseRelationᵣ(_⨞_ : T → T → Type{ℓₗ}) : Type{Lvl.of(T) Lvl.⊔ ℓₑ Lvl.⊔ ℓₗ} where
    constructor intro
    field proof : ∀{x y} → (x ⨞ y) ↔ ∃(z ↦ x ▫ z ≡ y)

  module _ ⦃ invRel : InverseRelationᵣ{ℓₗ}(_⨞_) ⦄ where
    record InverseOperatorᵣ (_⋄_ : (x : T) → (y : T) → . ⦃ inv : (y ⨞ x) ⦄ → T) : Type{Lvl.of(T) Lvl.⊔ ℓₑ Lvl.⊔ ℓₗ} where
      constructor intro
      field proof : ∀{x y} ⦃ inv : (y ⨞ x) ⦄ → (x ⋄ y ≡ [∃]-witness([↔]-to-[→] (InverseRelationᵣ.proof invRel) inv))

{-
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) where
  InverseRelationₗ = InverseRelationᵣ(swap(_▫_))

  module _ ⦃ invRel : InverseRelationₗ{ℓₗ}(_⨞_) ⦄ where
    InverseOperatorₗ = InverseOperatorᵣ -- TODO: Is this correct?
-}

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 map-compose where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning
open import Function using (_∘_)
open import lists using (List; []; _∷_; map)

postulate
  -- 外延性の公理
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

-- 外延性の公理を用いた証明のための補助定理
lemma : ∀ {A B C : Set} → (f : A → B) → (g : B → C) → (x : List A)
  → map (g ∘ f) x ≡ (map g ∘ map f) x
lemma f g []       = refl
lemma f g (x ∷ xs) =
  begin
    map (g ∘ f) (x ∷ xs)
  ≡⟨⟩
    (g ∘ f) x ∷ map (g ∘ f) xs
  ≡⟨ cong ((g ∘ f) x ∷_) (lemma f g xs) ⟩
    (g ∘ f) x ∷ (map g ∘ map f) xs
  ≡⟨⟩
    (map g ∘ map f) (x ∷ xs)
  ∎

-- mapの分配法則の証明
map-compose : ∀ {A B C : Set} → (f : A → B) → (g : B → C)
  → map (g ∘ f) ≡ map g ∘ map f
map-compose f g = extensionality (lemma f g)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-# OPTIONS --guardedness #-}
module induction-ex where

open import Relation.Binary.PropositionalEquality
open import Size
open import Data.Bool

data List (A : Set ) : Set where
    [] : List A
    _∷_ : A → List A → List A

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

add : Nat → Nat → Nat
add zero x = x
add (suc x) y = suc ( add x y )

_++_ : {A : Set} → List A → List A → List A
[] ++ y = y
(x ∷ t) ++ y = x ∷ ( t ++ y )

test1 = (zero ∷ []) ++ (zero ∷ [])

length : {A : Set } → List A → Nat
length [] = zero
length (_ ∷ t)  = suc ( length t )

lemma1 : {A : Set} → (x y : List A ) → length ( x ++ y ) ≡ add (length x) (length y)
lemma1 [] y = refl
lemma1 (x ∷ t) y = cong ( λ k → suc k ) lemma2  where
   lemma2 : length (t ++ y) ≡ add (length t) (length y)
   lemma2 = lemma1 t y

-- record List1 ( A : Set  ) : Set where
--    inductive
--    field
--       nil : List1 A
--       cons : A → List1 A → List1 A
--
-- record List2 ( A : Set  ) : Set where
--    coinductive
--    field
--       nil : List2 A
--       cons : A → List2 A → List2 A

data SList (i : Size) (A : Set) : Set where
  []' : SList i A
  _∷'_ : {j : Size< i} (x : A) (xs : SList j A) → SList i A

map : ∀{i A B} → (A → B) → SList i A → SList i B
map f []' = []'
map f ( x ∷' xs)= f x ∷' map f xs

foldr : ∀{i} {A B : Set} → (A → B → B) → B → SList i A → B
foldr c n []' = n
foldr c n (x ∷' xs) = c x (foldr c n xs)

any : ∀{i A} → (A → Bool) → SList i A → Bool
any p xs = foldr _∨_ false (map p xs)

-- Sappend : {A : Set } {i j : Size } → SList i A → SList j A → SList {!!} A
-- Sappend []' y = y
-- Sappend (x ∷' x₁) y =  _∷'_  {?}  x (Sappend x₁ y)

language : { Σ : Set } → Set
language {Σ} = List Σ → Bool

record Lang (i : Size) (A : Set) : Set where
  coinductive
  field
    ν : Bool
    δ : ∀{j : Size< i} → A → Lang j A

open Lang

∅ : ∀ {i A}  → Lang i A
ν ∅   = false
δ ∅ _ = ∅

∅' :  {i : Size } { A : Set }  → Lang i A
∅' {i} {A}  = record { ν = false ; δ = lemma3 } where
    lemma3 : {j : Size< i} → A → Lang j A
    lemma3 {j} _ = {!!}

∅l : {A : Set } → language {A}
∅l _ = false

ε : ∀ {i A} → Lang i A
ν ε   = true
δ ε _ = ∅

εl : {A : Set } → language {A}
εl [] = true
εl (_ ∷ _)  = false

_+_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (a + b)   = ν a   ∨  ν b
δ (a + b) x = δ a x + δ b x

Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Union {Σ} A B x = (A x ) ∨ (B x)

_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A
ν (a · b)   = ν a ∧ ν b
δ (a · b) x = if (ν a) then ((δ a x · b ) + (δ b x )) else ( δ a x · b )

split : {Σ : Set} → (List Σ → Bool)
      → ( List Σ → Bool) → List Σ → Bool
split x y  [] = x [] ∨ y []
split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Concat {Σ} A B = split A B

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
-- An ATP hint must be used with functions.

-- This error is detected by Syntax.Translation.ConcreteToAbstract.

module ATPBadHint1 where

data Bool : Set where
  false true : Bool

{-# ATP hint false #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
{-
  Given a type A with a UARel and a family B over A,
  a SubstRel on B is a family of functions a ≅ a' → B a ≃ B a' path-equal to transport in that family.

  Any SubstRel gives rise to a DUARel in which b and b' are related over p when the transport of b along p is
  equial to b'.
-}

{-# OPTIONS --safe #-}
module Cubical.Displayed.Subst where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence

open import Cubical.Displayed.Base

private
  variable
    ℓA ℓ≅A ℓB : Level

record SubstRel {A : Type ℓA} {ℓ≅A : Level} (𝒮-A : UARel A ℓ≅A) (B : A → Type ℓB)
  : Type (ℓ-max (ℓ-max ℓA ℓB) ℓ≅A)
  where

  no-eta-equality
  constructor substrel
  open UARel 𝒮-A

  field
    act : {a a' : A} → a ≅ a' → B a ≃ B a'
    uaˢ : {a a' : A} (p : a ≅ a') (b : B a) → subst B (≅→≡ p) b ≡ equivFun (act p) b

  uaˢ⁻ : {a a' : A} (p : a ≅ a') (b : B a') → subst B (sym (≅→≡ p)) b ≡ invEq (act p) b
  uaˢ⁻ p b =
    subst B (sym (≅→≡ p)) b
      ≡⟨ cong (subst B (sym (≅→≡ p))) (sym (retEq (act p) b)) ⟩
    subst B (sym (≅→≡ p)) (equivFun (act p) (invEq (act p) b))
      ≡⟨ cong (subst B (sym (≅→≡ p))) (sym (uaˢ p (invEq (act p) b))) ⟩
    subst B (sym (≅→≡ p)) (subst B (≅→≡ p) (invEq (act p) b))
      ≡⟨ pathToIso (cong B (≅→≡ p)) .Iso.leftInv (invEq (act p) b) ⟩
    invEq (act p) b
    ∎

Subst→DUA : {A : Type ℓA} {ℓ≅A : Level} {𝒮-A : UARel A ℓ≅A} {B : A → Type ℓB}
  → SubstRel 𝒮-A B → DUARel 𝒮-A B ℓB
DUARel._≅ᴰ⟨_⟩_ (Subst→DUA 𝒮ˢ-B) b p b' =
  equivFun (SubstRel.act 𝒮ˢ-B p) b ≡ b'
DUARel.uaᴰ (Subst→DUA {𝒮-A = 𝒮-A} {B = B} 𝒮ˢ-B) b p b' =
  equivFun (SubstRel.act 𝒮ˢ-B p) b ≡ b'
    ≃⟨ invEquiv (compPathlEquiv (sym (SubstRel.uaˢ 𝒮ˢ-B p b))) ⟩
  subst B (≅→≡ p) b ≡ b'
    ≃⟨ invEquiv (PathP≃Path (λ i → B (≅→≡ p i)) b b') ⟩
  PathP (λ i → B (UARel.≅→≡ 𝒮-A p i)) b b'
  ■
  where
  open UARel 𝒮-A

max_stars_repo_name: jespercockx/cubical

max_issues_repo_name: jespercockx/cubical

max_forks_repo_name: jespercockx/cubical


text:
-- Andreas, 2018-10-15, issue #3262 reported by Guillaume Brunerie
--
-- Missing with clauses should be reported close to problem location
-- not just at the type signature of the function which has this problem.

data T : Set where
  a b c : T

f : T → Set
f a = ?
f b = ?
f c with c | c
... | _ = ?

-- Should trigger the "missing with clauses" error
-- at the lhs with the "with".

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

postulate
  Nat : Set
  Fin : Nat → Set
  Foo : (n : Nat) → Fin n → Set
  Bar : ∀ {n m} → Foo n m → Set

variable
  n : Nat
  m : Fin _
  k : Foo _ m
  l : Foo n m

open import Agda.Builtin.Equality

postulate
  goal-type-error : Bar k

foo : Bar _
foo = goal-type-error _ _

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2017-07-11, issue #2639 reported by nad
--
-- Unsolvable size constraints were added to the constraint set
-- each time the size solver ran.  This lead to exponentially
-- many size constraints.

-- {-# OPTIONS -v tc.size.solve:40 #-}

module Issue2639 (A : Set) where

open import Agda.Builtin.Nat
open import Agda.Builtin.Size

open import Issue2639.DR A

postulate
  P : {i : Size} → D i → Set

F : Set₁
F = Set
  where

  -- This postulate creates an unsolved size constraint.
  postulate
    unused : P a

  G : Nat → Set → Set₁
  G zero = λ { _ → Set }
  G (suc zero) = λ { _ → Set }
  G (suc (suc zero)) = λ { _ → Set }
  G (suc (suc (suc zero))) = λ { _ → Set }
  G (suc (suc (suc (suc zero)))) = λ { _ → Set }
  G _ = λ { _ → Set }


text:
-- Andreas, 2012-04-18
module Issue611 where

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

data Bool : Set where
  true false : Bool

T : Bool -> Set
T true  = {x : Bool} -> Nat
T false = {x : Bool} -> Bool

data D (b : Bool) : Set where
  c : T b -> D b

d : D false
d = c {_} true

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Finitary.Permutation where

open import Data.Nat
open import Data.Fin
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
open import Function.Inverse as Inv using (Inverse)
import Function.Equality as F
open import Function.LeftInverse using (_LeftInverseOf_)
open import Data.Finitary
open import Data.Vec as Vec using (Vec)
open import Data.Vec.Distinct as Distinct using (Distinct)
open import Data.Product hiding (swap)

Permutation : ℕ → Set
Permutation n = Finitary (P.setoid (Fin n)) n

identity : ∀ {n} → Permutation n
identity = Inv.id

swap : ∀ {n} → Fin n → Fin n → Permutation n
swap {n} i j = record {
         to = P.→-to-⟶ swap′
       ; from = P.→-to-⟶ swap′
       ; inverse-of = record {
           left-inverse-of = swap′-involutive
         ; right-inverse-of = swap′-involutive
           }
         }
         where
           open import Data.Fin.Properties as FinP
           open import Relation.Nullary
           open import Data.Empty using (⊥-elim)
           swap′ : Fin n → Fin n
           swap′ k with k FinP.≟ i
           swap′ k | yes k≡i = j
           swap′ k | no ¬p with k FinP.≟ j
           swap′ k | no ¬p | yes k≡j = i
           swap′ k | no ¬p | no ¬p₁ = k

           swap′-involutive : ∀ k → swap′ (swap′ k) ≡ k
           swap′-involutive k with k FinP.≟ i
           swap′-involutive k | yes k≡i with k≡i | j FinP.≟ i
           swap′-involutive _ | yes k≡i | P.refl | yes j≡i = j≡i
           swap′-involutive _ | yes k≡i | P.refl | no j≢i with j FinP.≟ j
           swap′-involutive _ | yes k≡i | P.refl | no j≢i | yes j≡j = P.refl
           swap′-involutive _ | yes k≡i | P.refl | no j≢i | no j≢j = ⊥-elim (j≢j P.refl)
           swap′-involutive k | no k≢i with k FinP.≟ j
           swap′-involutive k | no k≢i | yes k≡j with k≡j | i FinP.≟ i
           swap′-involutive k | no k≢i | yes k≡j | P.refl | yes P.refl = P.refl
           swap′-involutive k | no k≢i | yes k≡j | P.refl | no i≢i = ⊥-elim (i≢i P.refl)
           swap′-involutive k | no k≢i | no k≢j = lemma k≢i k≢j
             where
               open P.≡-Reasoning
               lemma : ∀ {k} → k ≢ i → k ≢ j → swap′ k ≡ k
               lemma {k} k≢i k≢j with k FinP.≟ i
               lemma k≢i k≢j | yes k≡i  = ⊥-elim (k≢i k≡i)
               lemma {k} k≢i k≢j | no ¬k≡i with k FinP.≟ j
               lemma {k} k≢i k≢j | no ¬k≡i | yes k≡j = ⊥-elim (k≢j k≡j)
               lemma {k} k≢i k≢j | no ¬k≡i | no ¬p = P.refl

shift : ∀ {n} → Permutation n → Permutation (ℕ.suc n)
shift {n} p = record {
         to = P.→-to-⟶ (shift′ Perm.to)
       ; from = P.→-to-⟶ (shift′ Perm.from)
       ; inverse-of = record {
           left-inverse-of = shift′-inverse-of Perm.left-inverse-of
         ; right-inverse-of = shift′-inverse-of Perm.right-inverse-of
       }
    }
    where
      module Perm = Inverse p
      shift′ : P.setoid (Fin n) F.⟶ P.setoid (Fin n) → Fin (ℕ.suc n) → Fin (ℕ.suc n)
      shift′ f Fin.zero = Fin.zero
      shift′ f (Fin.suc i) = Fin.suc (f F.⟨$⟩ i)
      shift′-inverse-of : ∀ {from : P.setoid (Fin n) F.⟶ P.setoid (Fin n)}{to : P.setoid (Fin n) F.⟶ P.setoid (Fin n)} → from LeftInverseOf to → (P.→-to-⟶ (shift′ from)) LeftInverseOf (P.→-to-⟶ (shift′ to))
      shift′-inverse-of inv Fin.zero = P.refl
      shift′-inverse-of inv (Fin.suc i) = P.cong Fin.suc (inv i)

Perm→Distinct : ∀ {n} → Permutation n → ∃ λ (xs : Vec (Fin n) n) → Distinct xs
Perm→Distinct {n} p = , xs-distinct
  where
    open Inverse p renaming (to to f)
    open import Data.Vec.Properties

    xs-distinct : Distinct (Vec.tabulate (f F.⟨$⟩_))
    xs-distinct = P.subst Distinct (P.sym (tabulate-allFin _))
                  (Distinct.map injection (Distinct.allFin n))

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


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

syntax STLC | Λ

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

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

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

module STLC.Signature where

open import SOAS.Context

-- Type declaration
data ΛT : Set where
  N   : ΛT
  _↣_ : ΛT → ΛT → ΛT
infixr 30 _↣_

open import SOAS.Syntax.Signature ΛT public
open import SOAS.Syntax.Build ΛT public

-- Operator symbols
data Λₒ : Set where
  appₒ lamₒ : {α β : ΛT} → Λₒ

-- Term signature
Λ:Sig : Signature Λₒ
Λ:Sig = sig λ
  { (appₒ {α}{β}) → (⊢₀ α ↣ β) , (⊢₀ α) ⟼₂ β
  ; (lamₒ {α}{β}) → (α ⊢₁ β) ⟼₁ α ↣ β
  }

open Signature Λ:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
f : {A B : Set} → (@0 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:
-- Andreas, 2017-04-13, issue #2494, reported by identicalsnowflake
-- Consecutive hidden record fields confused the implicit argument insertion
-- due to lack of names in NamedArg.

-- {-# OPTIONS -v tc.lhs:30 #-}
-- {-# OPTIONS -v tc.term.args:100 #-}

postulate
  Red Blue : Set

record Colors : Set where
  field
    {{red}}  : Red
    {{blue}} : Blue

f : Colors → Red
f record { blue = blue } = blue


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Metavariables used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Meta where

import Data.Nat.Properties as ℕₚ
open import Function
open import Relation.Nullary.Decidable using (map′)
open import Relation.Binary
import Relation.Binary.Construct.On as On
open import Relation.Binary.PropositionalEquality

open import Agda.Builtin.Reflection public
  using (Meta) renaming (primMetaToNat to toℕ)

open import Agda.Builtin.Reflection.Properties public
  renaming (primMetaToNatInjective to toℕ-injective)

-- Equality of metas is decidable.

_≈_ : Rel Meta _
_≈_ = _≡_ on toℕ

_≈?_ : Decidable _≈_
_≈?_ = On.decidable toℕ _≡_ ℕₚ._≟_

infix 4 _≟_
_≟_ : DecidableEquality Meta
m ≟ n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n)


text:
module Thesis.SIRelBigStep.SemEquiv where

open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import Thesis.SIRelBigStep.Syntax public
open import Thesis.SIRelBigStep.OpSem
open import Thesis.SIRelBigStep.DenSem

⟦_⟧Val : ∀ {τ} → Val τ → ⟦ τ ⟧Type
⟦_⟧Env : ∀ {Γ} → ⟦ Γ ⟧Context → Den.⟦ Γ ⟧Context

⟦ ∅ ⟧Env = ∅
⟦ v • ρ ⟧Env = ⟦ v ⟧Val • ⟦ ρ ⟧Env

⟦ closure t ρ ⟧Val = λ v → (⟦ t ⟧Term) (v • ⟦ ρ ⟧Env)
⟦ natV n ⟧Val = n
⟦ pairV v1 v2 ⟧Val = ⟦ v1 ⟧Val , ⟦ v2 ⟧Val

↦-sound : ∀ {Γ τ} ρ (x : Var Γ τ) →
  Den.⟦ x ⟧Var ⟦ ρ ⟧Env ≡ ⟦ ⟦ x ⟧Var ρ ⟧Val
↦-sound (px • ρ) this = refl
↦-sound (px • ρ) (that x) = ↦-sound ρ x

eval-const-sound : ∀ {τ} (c : Const τ) → ⟦ c ⟧Const ≡ ⟦ eval-const c ⟧Val
eval-const-sound (lit n) = refl

eval-primitive-sound : ∀ {σ τ} (p : Primitive (σ ⇒ τ)) v → ⟦ p ⟧Primitive ⟦ v ⟧Val ≡ ⟦ eval-primitive p v ⟧Val
eval-primitive-sound succ (natV n) = refl
eval-primitive-sound add (pairV (natV n1) (natV n2)) = refl

eval-sound : ∀ {Γ τ} ρ (sv : SVal Γ τ) →
   ⟦ sv ⟧SVal ⟦ ρ ⟧Env ≡ ⟦ eval sv ρ ⟧Val
eval-sound ρ (var x) = ↦-sound ρ x
eval-sound ρ (abs t) = refl
eval-sound ρ (cons sv1 sv2) rewrite eval-sound ρ sv1 | eval-sound ρ sv2 = refl
eval-sound ρ (const c) = eval-const-sound c

-- Check it's fine to use i 0 in the derivations for app
↓-sv-1-step : ∀ {Γ τ ρ v} {n} {sv : SVal Γ τ} →
  ρ ⊢ val sv ↓[ i' n ] v →
  n ≡ 0
↓-sv-1-step (val sv) = refl

↓-sound : ∀ {Γ τ ρ v hasIdx} {n : Idx hasIdx} {t : Term Γ τ} →
  ρ ⊢ t ↓[ n ] v →
  ⟦ t ⟧Term ⟦ ρ ⟧Env ≡ ⟦ v ⟧Val
↓-sound (val sv) = eval-sound _ sv
↓-sound (app _ _ ↓₁ ↓₂ ↓′) rewrite ↓-sound ↓₁ | ↓-sound ↓₂ | ↓-sound ↓′ = refl
↓-sound (lett n1 n2 vsv s t ↓ ↓₁) rewrite ↓-sound ↓ | ↓-sound ↓₁ = refl
↓-sound {ρ = ρ} (primapp p sv) rewrite eval-sound ρ sv = eval-primitive-sound p (eval sv ρ)

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:
------------------------------------------------------------------------
-- Applicative functors
------------------------------------------------------------------------

-- Note that currently the applicative functor laws are not included
-- here.

module Category.Applicative where

open import Data.Unit
open import Category.Applicative.Indexed

RawApplicative : (Set → Set) → Set₁
RawApplicative F = RawIApplicative {I = ⊤} (λ _ _ → F)

module RawApplicative {F : Set → Set} (app : RawApplicative F) where
  open RawIApplicative app public

max_issues_repo_name: larrytheliquid/Lemmachine


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

module Cubical.Algebra.CommAlgebra.FreeCommAlgebra where

open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base public
open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Prod.Properties where

open import Cubical.Core.Everything

open import Cubical.Data.Prod.Base
open import Cubical.Data.Sigma

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

private
  variable
    ℓ ℓ' : Level
    A B  : Type ℓ

-- Swapping is an equivalence

swap : A × B → B × A
swap (x , y) = (y , x)

swap-invol : (xy : A × B) → swap (swap xy) ≡ xy
swap-invol (_ , _) = refl

isEquivSwap : (A : Type ℓ) (B : Type ℓ') → isEquiv (λ (xy : A × B) → swap xy)
isEquivSwap A B = isoToIsEquiv (iso swap swap swap-invol swap-invol)

swapEquiv : (A : Type ℓ) (B : Type ℓ') → A × B ≃ B × A
swapEquiv A B = (swap , isEquivSwap A B)

swapEq : (A : Type ℓ) (B : Type ℓ') → A × B ≡ B × A
swapEq A B = ua (swapEquiv A B)

private
  open import Cubical.Data.Nat

  -- As × is defined as a datatype this computes as expected
  -- (i.e. "C-c C-n test1" reduces to (2 , 1)). If × is implemented
  -- using Sigma this would be "transp (λ i → swapEq ℕ ℕ i) i0 (1 , 2)"
  test : ℕ × ℕ
  test = transp (λ i → swapEq ℕ ℕ i) i0 (1 , 2)

  testrefl : test ≡ (2 , 1)
  testrefl = refl

-- equivalence between the sigma-based definition and the inductive one
A×B≡A×ΣB : A × B ≡ A ×Σ B
A×B≡A×ΣB = isoToPath (iso (λ { (a , b) → (a , b)})
                          (λ { (a , b) → (a , b)})
                          (λ _ → refl)
                          (λ { (a , b) → refl }))

-- truncation for products
hLevelProd : (n : ℕ) → isOfHLevel n A → isOfHLevel n B → isOfHLevel n (A × B)
hLevelProd {A = A} {B = B} n h1 h2 =
  let h : isOfHLevel n (A ×Σ B)
      h = isOfHLevelΣ n h1 (λ _ → h2)
  in transport (λ i → isOfHLevel n (A×B≡A×ΣB {A = A} {B = B} (~ i))) h

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Example use case for a trie: a wee generic lexer
------------------------------------------------------------------------

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

module README.Data.Trie.NonDependent where

------------------------------------------------------------------------
-- Introduction

-- A Trie is a tree of values indexed by words in a finite language. It
-- allows users to quickly compute the Brzozowski derivative of that
-- little mapping from words to values.

-- In the most general case, values can depend upon the list of characters
-- that constitutes the path leading to them. Here however we consider a
-- non-dependent case (cf. README.Trie.Dependent for a dependent use case).

-- We can recognize keywords by storing the list of characters they
-- correspond to as paths in a Trie and the constructor they are decoded
-- to as the tree's values.

-- E.g.
-- [     .      ] is a root
-- [  -- m -->  ] is an m-labeled edge and is followed when reading 'm'
-- [    (X)     ] is a value leaf storing constructor X

--                     --> -- m --> -- m --> -- a --> (LEMMA)
--                    /
--       -- l --> -- e --> -- t --> (LET)
--      /
--     /    -- u --> -- t --> -- u --> -- a --> -- l --> (MUTUAL)
--    /    /
--  .< -- m --> -- o --> -- d --> -- u --> -- l --> -- e --> (MODULE)
--    \
--     -- w --> -- h --> -- e --> -- r --> -- e --> (WHERE)
--                           \
--                            --> -- n --> (WHEN)

-- after reading 'w', we get the derivative:

--  . -- h --> -- e --> -- r --> -- e --> (WHERE)
--                 \
--                  --> -- n --> (WHEN)

open import Level
open import Data.Unit
open import Data.Bool
open import Data.Char        as Char
import Data.Char.Properties  as Char
open import Data.List        as List using (List; []; _∷_)
open import Data.List.Fresh  as List# using (List#; []; _∷#_)
open import Data.Maybe       as Maybe
open import Data.Product     as Prod
open import Data.String      as String using (String)
open import Data.These       as These

open import Function using (case_of_; _$_; _∘′_; id; _on_)
open import Relation.Nary
open import Relation.Binary using (Rel)
open import Relation.Nullary.Negation using (¬?)

open import Data.Trie Char.<-strictTotalOrder-≈
open import Data.AVL.Value

------------------------------------------------------------------------
-- Generic lexer

record Lexer t : Set (suc t) where
  field
  -- Our lexer is parametrised over the type of tokens
    Tok : Set t

  -- Keywords are distinguished strings associated to tokens
  Keyword : Set t
  Keyword = String × Tok

  -- Two keywords are considered distinct if the strings are not equal
  Distinct : Rel Keyword 0ℓ
  Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋

  field

  -- We ask users to provide us with a fresh list of keywords to guarantee
  -- that no two keywords share the same string representation
    keywords : List# Keyword Distinct

  -- Some characters are special: they are separators, breaking a string
  -- into a list of tokens. Some are associated to a token value
  -- (e.g. parentheses) others are not (e.g. space)
    breaking : Char → ∃ λ b → if b then Maybe Tok else Lift _ ⊤

  -- Finally, strings which are not decoded as keywords are coerced
  -- using a function to token values.
    default  : String → Tok

module _ {t} (L : Lexer t) where
  open Lexer L

  tokenize : String → List Tok
  tokenize = start ∘′ String.toList where

   mutual

    -- A Trie is defined for an alphabet of strictly ordered letters (here
    -- we have picked Char for letters and decided to use the strict total
    -- order induced by their injection into ℕ as witnessed by the statement
    -- open import Data.Trie Char.strictTotalOrder earlier in this file).

    -- It is parametrised by a set of Values indexed over list of letters.
    -- Because we focus on the non-dependent case, we pick the constant
    -- family of Value uniformly equal to Tok. It is trivially compatible
    -- with the notion of equality underlying the strict total order on Chars.

    Keywords : Set _
    Keywords = Trie (const _ Tok) _

    -- We build a trie from the association list so that we may easily
    -- compute the successive derivatives obtained by eating the
    -- characters one by one

    init : Keywords
    init = fromList $ List.map (Prod.map₁ String.toList) $ proj₁ $ List#.toList keywords

    -- Kickstart the tokeniser with an empty accumulator and the initial
    -- trie.
    start : List Char → List Tok
    start = loop [] init

    -- The main loop
    loop : (acc  : List Char)  → -- chars read so far in this token
           (toks : Keywords)   → -- keyword candidates left at this point
           (input : List Char) → -- list of chars to tokenize
           List Tok
    -- Empty input: finish up, check whether we have a non-empty accumulator
    loop acc toks []         = push acc []
    -- At least one character
    loop acc toks (c ∷ cs)   = case breaking c of λ where
      -- if we are supposed to break on this character, we do
      (true , m)  → push acc $ maybe′ _∷_ id m $ start cs
      -- otherwise we see whether it leads to a recognized keyword
      (false , _) → case lookupValue (c ∷ []) toks of λ where
        -- if so we can forget about the current accumulator and
        -- restart the tokenizer on the rest of the input
        (just tok) → tok ∷ start cs
        -- otherwise we record the character we read in the accumulator,
        -- compute the derivative of the map of keyword candidates and
        -- keep going with the rest of the input
        nothing    → loop (c ∷ acc) (lookupTrie c toks) cs

    -- Grab the accumulator and, unless it is empty, push it on top of
    -- the decoded list of tokens
    push : List Char → List Tok → List Tok
    push [] ts = ts
    push cs ts = default (String.fromList (List.reverse cs)) ∷ ts

------------------------------------------------------------------------
-- Concrete instance

-- A small set of keywords for a language with expressions of the form
-- `let x = e in b`.

module LetIn where

  data TOK : Set where
    LET EQ IN : TOK
    LPAR RPAR : TOK
    ID : String → TOK

  keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋)
  keywords =  ("let" , LET)
           ∷# ("="   , EQ)
           ∷# ("in"  , IN)
           ∷# []

  -- Breaking characters: spaces (thrown away) and parentheses (kept)
  breaking : Char → ∃ (λ b → if b then Maybe TOK else Lift 0ℓ ⊤)
  breaking c = if isSpace c then true , nothing else parens c where

    parens : Char → _
    parens '(' = true , just LPAR
    parens ')' = true , just RPAR
    parens _   = false , _

  default : String → TOK
  default = ID

letIn : Lexer 0ℓ
letIn = record { LetIn }

open import Agda.Builtin.Equality

-- A test case:

open LetIn
_ : tokenize letIn "fix f x = let b = fix f in (f b) x"
  ≡ ID "fix"
  ∷ ID "f"
  ∷ ID "x"
  ∷ EQ
  ∷ LET
  ∷ ID "b"
  ∷ EQ
  ∷ ID "fix"
  ∷ ID "f"
  ∷ IN
  ∷ LPAR
  ∷ ID "f"
  ∷ ID "b"
  ∷ RPAR
  ∷ ID "x"
  ∷ []
_ = refl


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

open import Fragment.Equational.Theory

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

open import Fragment.Algebra.Algebra (Σ Θ) using (Algebra)
open import Fragment.Algebra.Homomorphism (Σ Θ)
open import Fragment.Algebra.Free (Σ Θ)
open import Fragment.Equational.Model Θ
open import Fragment.Equational.Coproduct Θ
open import Fragment.Equational.FreeExtension.Base Θ
open import Fragment.Equational.FreeExtension.Synthetic Θ using (SynFrex)

open import Level using (Level)
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec)
open import Relation.Binary using (Setoid)
import Relation.Binary.Reasoning.Setoid as Reasoning

private
  variable
    a ℓ₁ : Level

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

  open FreeExtension X renaming (_[_] to _[_]₁; _[_]-isFrex to _[_]₁-isFrex)
  open FreeExtension Y renaming (_[_] to _[_]₂; _[_]-isFrex to _[_]₂-isFrex)

  open IsCoproduct (A [ n ]₁-isFrex)
    renaming (inl to inl₁; inr to inr₁; _[_,_] to _[_,_]₁; commute₁ to commute₁₁; commute₂ to commute₂₁)
  open IsCoproduct (A [ n ]₂-isFrex)
    renaming (inl to inl₂; inr to inr₂; _[_,_] to _[_,_]₂; commute₁ to commute₁₂; commute₂ to commute₂₂)
    using ()

  to : ∥ A [ n ]₂ ∥ₐ ⟿ ∥ A [ n ]₁ ∥ₐ
  to = (A [ n ]₁) [ inl₁ , inr₁ ]₂

  from : ∥ A [ n ]₁ ∥ₐ ⟿ ∥ A [ n ]₂ ∥ₐ
  from = (A [ n ]₂) [ inl₂ , inr₂ ]₁

  inv : to ⊙ from ≗ id
  inv = begin
      to ⊙ from
    ≈⟨ ≗-sym {f = (A [ n ]₁) [ inl₁ , inr₁ ]₁} {g = to ⊙ from} (universal {h = to ⊙ from} c₁ c₂) ⟩
      (A [ n ]₁) [ inl₁ , inr₁ ]₁
    ≈⟨ universal {h = id} (id-unitˡ {f = inl₁}) (id-unitˡ {f = inr₁}) ⟩
      id
    ∎
    where c₁ : (to ⊙ from) ⊙ inl₁ ≗ inl₁
          c₁ = begin
              (to ⊙ from) ⊙ inl₁
            ≈⟨ ⊙-assoc to from inl₁ ⟩
              to ⊙ (from ⊙ inl₁)
            ≈⟨ ⊙-congˡ to (from ⊙ inl₁) inl₂ (commute₁₁ {f = inl₂} {g = inr₂}) ⟩
              to ⊙ inl₂
            ≈⟨ commute₁₂ {X = A [ n ]₁} {f = inl₁} {g = inr₁} ⟩
              inl₁
            ∎
            where open Reasoning (∥ A ∥ₐ ⟿ ∥ A [ n ]₁ ∥ₐ /≗)

          c₂ : (to ⊙ from) ⊙ inr₁ ≗ inr₁
          c₂ = begin
              (to ⊙ from) ⊙ inr₁
            ≈⟨ ⊙-assoc to from inr₁ ⟩
              to ⊙ (from ⊙ inr₁)
            ≈⟨ ⊙-congˡ to (from ⊙ inr₁) inr₂ (commute₂₁ {f = inl₂} {g = inr₂}) ⟩
              to ⊙ inr₂
            ≈⟨ commute₂₂ {X = A [ n ]₁} {f = inl₁} {g = inr₁} ⟩
              inr₁
            ∎
            where open Reasoning (∥ J n ∥ₐ ⟿ ∥ A [ n ]₁ ∥ₐ /≗)

          open Reasoning (∥ A [ n ]₁ ∥ₐ ⟿ ∥ A [ n ]₁ ∥ₐ /≗)

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

  open FreeExtension X renaming (_[_] to _[_]₁)
  open FreeExtension Y renaming (_[_] to _[_]₂)

  iso : ∥ A [ n ]₁ ∥ₐ ≃ ∥ A [ n ]₂ ∥ₐ
  iso = record { _⃗   = to Y X A n
               ; _⃖   = from Y X A n
               ; invˡ = inv Y X A n
               ; invʳ = inv X Y A n
               }

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

  open FreeExtension X
  open FreeExtension SynFrex renaming (_[_] to _[_]ₛ; _[_]-isFrex to _[_]ₛ-isFrex)

  open IsCoproduct (A [ n ]-isFrex)
  open IsCoproduct (A [ n ]ₛ-isFrex) renaming (_[_,_] to _[_,_]ₛ) using ()

  open Setoid ∥ A [ n ] ∥/≈ renaming (_≈_ to _≋_)
  open Setoid ∥ A ∥/≈ using (_≈_)

  norm = to X SynFrex A n
  syn = from X SynFrex A n

  reduce : (θ : Env ∥ A ∥ₐ n) → ∥ A [ n ]ₛ ∥ₐ ⟿ ∥ A ∥ₐ
  reduce θ = A [ id , interp A θ ]ₛ

  module _ (Γ : Vec ∥ A ∥ n) where

    private

      θ : Env ∥ A ∥ₐ n
      θ = env {A = ∥ A ∥ₐ} Γ

    frexify : ∀ {lhs rhs : Term (BT ∥ A ∥ n)}
              → ∣ norm ∣ lhs ≋ ∣ norm ∣ rhs
              → ∣ reduce θ ∣ lhs ≈ ∣ reduce θ ∣ rhs
    frexify {lhs = lhs} {rhs = rhs} p = begin
        ∣ reduce θ ∣ lhs
      ≈⟨ Setoid.sym ∥ A ∥/≈ (∣ reduce θ ∣-cong (inv SynFrex X A n {x = lhs})) ⟩
        ∣ reduce θ ∣ (∣ syn ∣ (∣ norm ∣ lhs))
      ≈⟨ ∣ reduce θ ∣-cong (∣ syn ∣-cong p) ⟩
        ∣ reduce θ ∣ (∣ syn ∣ (∣ norm ∣ rhs))
      ≈⟨ ∣ reduce θ ∣-cong (inv SynFrex X A n {x = rhs}) ⟩
        ∣ reduce θ ∣ rhs
      ∎
      where open Reasoning ∥ A ∥/≈

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

postulate
  _↦_ : {A : Set} → A → A → Set
  idr : {A : Set} {a : A} → a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

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

postulate
  A B C : Set
  g : A → B → C

f : A × B → C
f (x , y) = g x y

postulate
  D : Set
  P : (A → B → C) → D
  res : D
  rew : P (λ x y → g x y) ↦ res
  {-# REWRITE rew #-}

test : P (λ x y → f (x , y)) ↦ res
test = idr


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category

module Categories.Object.Coproduct {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level
open import Categories.Opposite

import Categories.Object.Product as ProductObject
module Op× = ProductObject op

-- Borrowed from Dan Doel's definition of coproducts
record Coproduct (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    A+B : Obj
    i₁ : A ⇒ A+B
    i₂ : B ⇒ A+B
    [_,_] : ∀ {C} → (A ⇒ C) → (B ⇒ C) → (A+B ⇒ C)

    .commute₁ : ∀ {C} {f : A ⇒ C} {g : B ⇒ C} → [ f , g ] ∘ i₁ ≡ f
    .commute₂ : ∀ {C} {f : A ⇒ C} {g : B ⇒ C} → [ f , g ] ∘ i₂ ≡ g
    .universal : ∀ {C} {f : A ⇒ C} {g : B ⇒ C} {h : A+B ⇒ C}
               → h ∘ i₁ ≡ f
               → h ∘ i₂ ≡ g
               → [ f , g ] ≡ h

  .g-η : ∀ {C} {f : A+B ⇒ C} → [ f ∘ i₁ , f ∘ i₂ ] ≡ f
  g-η = universal Equiv.refl Equiv.refl

  .η : [ i₁ , i₂ ] ≡ id
  η = universal identityˡ identityˡ

  .[]-cong₂ : ∀ {C} → {f f′ : A ⇒ C} {g g′ : B ⇒ C} → f ≡ f′ → g ≡ g′ → [ f , g ] ≡ [ f′ , g′ ]
  []-cong₂ f≡f′ g≡g′ =
    universal (trans commute₁ (sym f≡f′)) (trans commute₂ (sym g≡g′))
    where open Equiv

record BinCoproducts : Set (suc o ⊔ ℓ ⊔ e) where
  field
    _+_ : (A B : Obj) -> Obj
    i₁ : {A B : Obj} -> A ⇒ (A + B)
    i₂ : {A B : Obj} -> B ⇒ (A + B)
    [_,_] : {A B : Obj} -> ∀ {C} → (A ⇒ C) → (B ⇒ C) → ((A + B) ⇒ C)

    .commute₁ : {A B : Obj} -> ∀ {C} {f : A ⇒ C} {g : B ⇒ C} → [ f , g ] ∘ i₁ ≡ f
    .commute₂ : {A B : Obj} -> ∀ {C} {f : A ⇒ C} {g : B ⇒ C} → [ f , g ] ∘ i₂ ≡ g
    .universal : {A B : Obj} -> ∀ {C} {f : A ⇒ C} {g : B ⇒ C} {h : (A + B) ⇒ C}
               → h ∘ i₁ ≡ f
               → h ∘ i₂ ≡ g
               → [ f , g ] ≡ h

coproduct→product : ∀ {A B} → Coproduct A B → Op×.Product A B
coproduct→product A+B = record
  { A×B = A+B.A+B
  ; π₁ = A+B.i₁
  ; π₂ = A+B.i₂
  ; ⟨_,_⟩ = A+B.[_,_]
  ; commute₁ = A+B.commute₁
  ; commute₂ = A+B.commute₂
  ; universal = A+B.universal
  }
  where
  module A+B = Coproduct A+B

product→coproduct : ∀ {A B} → Op×.Product A B → Coproduct A B
product→coproduct A×B = record
  { A+B = A×B.A×B
  ; i₁ = A×B.π₁
  ; i₂ = A×B.π₂
  ; [_,_] = A×B.⟨_,_⟩
  ; commute₁ = A×B.commute₁
  ; commute₂ = A×B.commute₂
  ; universal = A×B.universal
  }
  where
  module A×B = Op×.Product A×B

open import Categories.Morphisms

Commutative : ∀ {A B} → (p₁ : Coproduct A B) (p₂ : Coproduct B A) → _≅_ C (Coproduct.A+B p₁) (Coproduct.A+B p₂)
Commutative p₁ p₂ = opⁱ (Op×.Commutative (coproduct→product p₂) (coproduct→product p₁))

Associative : ∀ {X Y Z} (p₁ : Coproduct X Y) (p₂ : Coproduct Y Z) (p₃ : Coproduct X (Coproduct.A+B p₂)) (p₄ : Coproduct (Coproduct.A+B p₁) Z) → _≅_ C (Coproduct.A+B p₃) (Coproduct.A+B p₄)
Associative p₁ p₂ p₃ p₄ = reverseⁱ C (opⁱ (Op×.Associative (coproduct→product p₁) (coproduct→product p₂) (coproduct→product p₃) (coproduct→product p₄)))

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

record NoEta : Set where
  no-eta-equality
  constructor _,_
  field fst : Nat
        snd : Nat

open NoEta

data ⊥ : Set where

soft-fail : (a : NoEta) (x : Nat) → (fst a , x) ≡ a → ⊥
soft-fail a x ()  -- Should be yellow (not sure if empty)

loop : ⊥
loop = soft-fail (0 , 0) 0 refl


text:
module NotStrictlyPositive where

data False : Set where

data Not (A : Set) : Set where
  not : (A -> False) -> Not A

data Neg (A : Set) : Set where
  neg : Not A -> Neg A

data Bad : Set where
  bad : Neg Bad -> Bad


text:
------------------------------------------------------------------------
-- Some properties that hold for Erased do not hold for every
-- topological modality
------------------------------------------------------------------------

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

open import Equality

module Erased.Counterexamples
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import Bijection eq using (_↔_)
open import Equality.Decision-procedures eq
open import Equivalence.Path-split eq
open import Function-universe eq hiding (_∘_)
open import Erased.Stability eq
open import H-level eq
open import H-level.Closure eq

private
  variable
    a b ℓ ℓ′ p : Level
    A          : Type a

-- The zero modality.
--
-- This modality is taken from "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

Zero : Type ℓ → Type ℓ
Zero _ = ↑ _ ⊤

-- A type A is Zero-stable if Zero A implies A.

Zero-stable : Type ℓ → Type ℓ
Zero-stable A = Zero A → A

-- A type is Zero-modal if it is contractible.
--
-- This definition is based on "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

Zero-modal : Type ℓ → Type ℓ
Zero-modal = Contractible

-- Zero-modal types are Zero-stable.

Zero-modal→Zero-stable : Zero-modal A → Zero-stable A
Zero-modal→Zero-stable m _ = proj₁ m

-- A type A has Zero-stable equality if x ≡ y is Zero-stable for all
-- values x and y of type A.

Zero-stable-≡ : Type a → Type a
Zero-stable-≡ = For-iterated-equality 1 Zero-stable

-- A type A has Zero-modal equality if x ≡ y is Zero-modal for all
-- values x and y of type A.

Zero-modal-≡ : Type a → Type a
Zero-modal-≡ = For-iterated-equality 1 Zero-modal

-- The zero modality is a Σ-closed reflective subuniverse.
--
-- This proof is based on "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

Zero-modality : Σ-closed-reflective-subuniverse ℓ
Zero-modality {ℓ = ℓ} = λ where
    .◯                      → Zero
    .η                      → return
    .Is-modal               → Zero-modal
    .Is-modal-propositional → λ ext → H-level-propositional ext 0
    .Is-modal-◯             → ↑-closure 0 ⊤-contractible
    .Is-modal-respects-≃    → H-level-cong _ 0
    .extendable-along-η     → extendable
    .Σ-closed               → Σ-closure 0
  where
  open Σ-closed-reflective-subuniverse

  return : A → Zero A
  return = _

  extendable :
    {A B : Type ℓ} →
    Zero-modal B →
    Is-∞-extendable-along-[ return {A = A} ] (λ (_ : Zero A) → B)
  extendable cB zero    = _
  extendable cB (suc n) =
      (λ g → (λ _ → proj₁ cB) , (λ x → proj₂ cB (g x)))
    , (λ _ _ → extendable (⇒≡ 0 cB) n)

-- The zero modality is topological (for all universe levels).
--
-- This result is based on "Modalities in Homotopy Type Theory" by
-- Rijke, Shulman and Spitters.

Zero-topological : Topological ℓ′ (Zero-modality {ℓ = ℓ})
Zero-topological {ℓ′ = ℓ′} {ℓ = ℓ} =
    ↑ ℓ′ ⊤
  , (λ _ → ⊥)
  , (λ _ → ⊥-propositional)
  , (λ _ → record { to = to; from = from })
  where
  open Σ-closed-reflective-subuniverse Zero-modality

  to :
    Zero-modal A →
    ↑ ℓ′ ⊤ → Is-∞-extendable-along-[ η ] (λ _ → A)
  to cA _ zero    = _
  to cA _ (suc n) =
      (λ _ → (λ _ → proj₁ cA) , (λ ()))
    , (λ _ _ → to (⇒≡ 0 cA) _ n)

  from :
    (↑ ℓ′ ⊤ → Is-∞-extendable-along-[ η ] (λ _ → A)) →
    Zero-modal A
  from {A = A} ext =
      inh
    , (λ x →
         ext _ 2 .proj₂ (const inh) (const x) .proj₁ ⊥-elim .proj₁ _)
    where
    inh : A
    inh = ext _ 1 .proj₁ ⊥-elim .proj₁ _

-- It is not the case that Zero ⊥ is isomorphic to ⊥.
--
-- Compare with Erased.Level-1.Erased-⊥↔⊥.

¬[Zero-⊥↔⊥] : ¬ (Zero (⊥ {ℓ = ℓ}) ↔ ⊥ {ℓ = ℓ})
¬[Zero-⊥↔⊥] hyp =
         $⟨ _ ⟩
  ↑ _ ⊤  ↝⟨ hyp ⟩
  ⊥      ↝⟨ ⊥↔⊥ ⟩□
  ⊥₀     □

-- It is not the case that Zero A implies ¬ ¬ A for all types A.
--
-- Compare with Erased.Stability.Erased→¬¬.

¬[Zero→¬¬] : ¬ ({A : Type a} → Zero A → ¬ ¬ A)
¬[Zero→¬¬] hyp =
          $⟨ _ ⟩
  Zero ⊥  ↝⟨ hyp ⟩
  ¬ ¬ ⊥   ↝⟨ ⊥-elim ∘ (_$ ⊥-elim) ⟩□
  ⊥       □

-- It is not the case that, for all types A, if A is stable for
-- double-negation, then A is Zero-stable.
--
-- Compare with Erased.Stability.¬¬-stable→Stable.

¬[¬¬-stable→Zero-stable] :
  ¬ ({A : Type a} → (¬ ¬ A → A) → Zero-stable A)
¬[¬¬-stable→Zero-stable] hyp =
                $⟨ ⊥-elim ∘ (_$ ⊥-elim) ⟩
  (¬ ¬ ⊥ → ⊥)   ↝⟨ hyp ⟩
  (Zero ⊥ → ⊥)  ↝⟨ _$ _ ⟩
  ⊥             ↔⟨ ⊥↔⊥ ⟩□
  ⊥₀            □

-- It is not the case that, for all types A, if A is decided, then A
-- is Zero-stable.
--
-- Compare with Erased.Stability.Dec→Stable.

¬[Dec→Zero-stable] : ¬ ({A : Type a} → Dec A → Zero-stable A)
¬[Dec→Zero-stable] hyp =
                $⟨ inj₂ ⊥-elim ⟩
  Dec ⊥         ↝⟨ hyp ⟩
  (Zero ⊥ → ⊥)  ↝⟨ _$ _ ⟩
  ⊥             ↔⟨ ⊥↔⊥ ⟩□
  ⊥₀            □

-- It is not the case that, for all types A, if equality is decidable
-- for A, then equality for A is Zero-stable.

¬[Decidable-equality→Zero-stable-≡] :
  ¬ ({A : Type a} → Decidable-equality A → Zero-stable-≡ A)
¬[Decidable-equality→Zero-stable-≡] {a = a} hyp =
                                                            $⟨ ↑.Dec._≟_ Bool._≟_ ⟩
  Decidable-equality (↑ a Bool)                             ↝⟨ (λ dec → hyp dec _ _) ⟩
  (Zero (lift true ≡ lift false) → lift true ≡ lift false)  ↝⟨ _$ _ ⟩
  lift true ≡ lift false                                    ↝⟨ Bool.true≢false ∘ cong lower ⟩□
  ⊥₀                                                        □

-- It is not the case that, for all types A, if equality is decidable
-- for A, then equality for A is Zero-modal.
--
-- Compare with
-- Erased.Stability.[]-cong₁.Decidable-equality→Very-stable-≡.

¬[Decidable-equality→Zero-modal-≡] :
  ¬ ({A : Type a} → Decidable-equality A → Zero-modal-≡ A)
¬[Decidable-equality→Zero-modal-≡] {a = a} =
  ({A : Type a} →
   Decidable-equality A → Zero-modal-≡ A)   ↝⟨ (implicit-∀-cong _ $ ∀-cong _ λ _ → ∀-cong _ λ _ → ∀-cong _ λ _ →
                                                Zero-modal→Zero-stable) ⟩
  ({A : Type a} →
   Decidable-equality A → Zero-stable-≡ A)  ↝⟨ ¬[Decidable-equality→Zero-stable-≡] ⟩□

  ⊥                                         □

-- It is not the case that the empty types are Zero-modal.
--
-- Compare with Erased.Stability.Very-stable-⊥.

¬[Zero-modal-⊥] : ¬ Zero-modal (⊥ {ℓ = ℓ})
¬[Zero-modal-⊥] =
  Contractible ⊥  ↝⟨ proj₁ ⟩
  ⊥               ↔⟨ ⊥↔⊥ ⟩□
  ⊥₀              □

-- It is not the case that, for any type A and type family P over A,
-- if A is Zero-modal, then W A P is Zero-modal.
--
-- Compare with Erased.Stability.[]-cong₂-⊔₁.Very-stable-W, which is
-- proved under the assumption of function extensionality.

¬[Zero-modal-W] :
  ¬ ({A : Type a} {P : A → Type p} → Zero-modal A → Zero-modal (W A P))
¬[Zero-modal-W] hyp =                   $⟨ ↑-closure 0 ⊤-contractible ⟩
  Zero-modal (↑ _ ⊤)                    ↝⟨ hyp ⟩
  Zero-modal (W (↑ _ ⊤) (λ _ → ↑ _ ⊤))  ↝⟨ proj₁ ⟩
  W (↑ _ ⊤) (λ _ → ↑ _ ⊤)               ↝⟨ inhabited⇒W-empty _ ⟩□
  ⊥                                     □

-- It is not the case that, for all types A and B, if equality is
-- Zero-stable for A and B, then equality is Zero-stable for A ⊎ B.
--
-- Compare with Erased.Stability.Stable-≡-⊎.

¬[Zero-stable-≡-⊎] :
  ¬ ({A : Type a} {B : Type b} →
     Zero-stable-≡ A →
     Zero-stable-≡ B →
     Zero-stable-≡ (A ⊎ B))
¬[Zero-stable-≡-⊎] hyp =                         $⟨ (λ _ _ _ → refl _)
                                                  , (λ _ _ _ → refl _)
                                                  ⟩
  Zero-stable-≡ (↑ _ ⊤) × Zero-stable-≡ (↑ _ ⊤)  ↝⟨ uncurry hyp ⟩
  Zero-stable-≡ (↑ _ ⊤ ⊎ ↑ _ ⊤)                  ↝⟨ (_$ _) ∘ (_$ _) ∘ (_$ _) ⟩
  inj₁ _ ≡ inj₂ _                                ↝⟨ ⊎.inj₁≢inj₂ ⟩□
  ⊥                                              □

-- It is not the case that, for all types A and B, if equality is
-- Zero-modal for A and B, then equality is Zero-modal for A ⊎ B.
--
-- Compare with Erased.Stability.[]-cong₂-⊔₂.Very-stable-≡-⊎.

¬[Zero-modal-≡-⊎] :
  ¬ ({A : Type a} {B : Type b} →
     Zero-modal-≡ A →
     Zero-modal-≡ B →
     Zero-modal-≡ (A ⊎ B))
¬[Zero-modal-≡-⊎] hyp =                        $⟨ (λ _ _ → +⇒≡ (mono₁ 0 (↑-closure 0 ⊤-contractible)))
                                                , (λ _ _ → +⇒≡ (mono₁ 0 (↑-closure 0 ⊤-contractible)))
                                                ⟩
  Zero-modal-≡ (↑ _ ⊤) × Zero-modal-≡ (↑ _ ⊤)  ↝⟨ uncurry hyp ⟩
  Zero-modal-≡ (↑ _ ⊤ ⊎ ↑ _ ⊤)                 ↝⟨ proj₁ ∘ (_$ _) ∘ (_$ _) ⟩
  inj₁ _ ≡ inj₂ _                              ↝⟨ ⊎.inj₁≢inj₂ ⟩□
  ⊥                                            □

-- It is not the case that, for all types A, if equality is
-- Zero-stable for A, then equality is Zero-stable for List A.
--
-- Compare with Erased.Stability.Stable-≡-List.

¬[Zero-stable-≡-List] :
  ¬ ({A : Type a} → Zero-stable-≡ A → Zero-stable-≡ (List A))
¬[Zero-stable-≡-List] hyp =     $⟨ (λ _ _ _ → refl _) ⟩
  Zero-stable-≡ (↑ _ ⊤)         ↝⟨ hyp ⟩
  Zero-stable-≡ (List (↑ _ ⊤))  ↝⟨ (_$ _) ∘ (_$ _) ∘ (_$ _) ⟩
  [] ≡ _ ∷ []                   ↝⟨ List.[]≢∷ ⟩□
  ⊥                             □

-- It is not the case that, for all types A, if equality is Zero-modal
-- for A, then equality is Zero-modal for List A.
--
-- Compare with Erased.Stability.[]-cong₁.Very-stable-≡-List.

¬[Zero-modal-≡-List] :
  ¬ ({A : Type a} → Zero-modal-≡ A → Zero-modal-≡ (List A))
¬[Zero-modal-≡-List] hyp =     $⟨ (λ _ _ → +⇒≡ (mono₁ 0 (↑-closure 0 ⊤-contractible))) ⟩
  Zero-modal-≡ (↑ _ ⊤)         ↝⟨ hyp ⟩
  Zero-modal-≡ (List (↑ _ ⊤))  ↝⟨ proj₁ ∘ (_$ _) ∘ (_$ _) ⟩
  [] ≡ _ ∷ []                  ↝⟨ List.[]≢∷ ⟩□
  ⊥                            □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Base.Prelude.Bool where

open import Data.Bool using (Bool; true; false; if_then_else_) renaming (_∧_ to _∧ᵖ_; _∨_ to _∨ᵖ_; not to notᵖ)
open import Base.Free using (Free; pure; _>>=_)

𝔹 : (Shape : Set) → (Shape → Set) → Set
𝔹 _ _ = Bool

True : ∀ {S P} → Free S P (𝔹 S P)
True = pure true

False : ∀ {S P} → Free S P (𝔹 S P)
False = pure false

_∧_ : ∀ {S P} → Free S P (𝔹 S P) → Free S P (𝔹 S P) → Free S P (𝔹 S P)
mx ∧ my = mx >>= λ x → if x then my else False

_∨_ : ∀ {S P} → Free S P (𝔹 S P) → Free S P (𝔹 S P) → Free S P (𝔹 S P)
mx ∨ my = mx >>= λ x → if x then True else my

not : ∀ {S P} → Free S P (𝔹 S P) → Free S P (𝔹 S P)
not mb = mb >>= λ b → pure (notᵖ b)

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
data D (A : Set) : Set where
  c₁ : D A

_ : (@0 A : Set) → D A
_ = λ A → c₁ {A = A}

_ : (@0 A : Set) → D A
_ = λ A → D.c₁ {A = A}

record R (A : Set) : Set where
  constructor c₂
  field
    f : A → A

  g : A → A
  g x = f (f x)

open R public

_ : (@0 A : Set) → (A → A) → R A
_ = λ A → c₂ {A = A}

_ : (@0 A : Set) → R A → A → A
_ = λ A → f {A = A}

_ : (@0 A : Set) → R A → A → A
_ = λ A → R.f {A = A}

_ : (A : Set) → R A → A → A
_ = λ A → g {A = A}

_ : (A : Set) → R A → A → A
_ = λ A → R.g {A = A}

open module R′ (A : Set) (r : R A) = R {A = A} r
  renaming (f to f′; g to g′)

_ : (A : Set) → R A → A → A
_ = λ A → f′ {A = A}

_ : (A : Set) → R A → A → A
_ = λ A → R′.f {A = A}

_ : (A : Set) → R A → A → A
_ = λ A → g′ A

_ : (A : Set) → R A → A → A
_ = λ A → R′.g A


text:
{-# OPTIONS --without-K #-}
module function.isomorphism.lift where

open import level
open import equality
open import function.isomorphism.core

-- lifting is an isomorphism
lift-iso : ∀ {i} j (X : Set i) → X ≅ ↑ j X
lift-iso j X = iso lift lower (λ _ → refl) (λ _ → refl)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-

Inductive eliminators to establish properties of all finite sets directly

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

module Cubical.Data.FinSet.Induction where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.HITs.PropositionalTruncation as Prop
open import Cubical.HITs.SetTruncation as Set

open import Cubical.Data.Nat
  renaming (_+_ to _+ℕ_) hiding (elim)
open import Cubical.Data.Unit
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sum

open import Cubical.Data.Fin renaming (Fin to Finℕ)
open import Cubical.Data.SumFin
open import Cubical.Data.FinSet.Base
open import Cubical.Data.FinSet.Properties
open import Cubical.Data.FinSet.Constructors

private
  variable
    ℓ ℓ' : Level

-- definitions mimicking that of natural numbers

module _
  {ℓ : Level} where

  𝟘 : FinSet ℓ
  𝟘 = ⊥* , 0 , ∣ uninhabEquiv Empty.rec* Empty.rec ∣

  𝟙 : FinSet ℓ
  𝟙 = Unit* , isContr→isFinSet (isContrUnit*)

  _+_ : FinSet ℓ → FinSet ℓ → FinSet ℓ
  X + Y = X .fst ⊎ Y .fst , isFinSet⊎ X Y

  -- 𝔽in can be seen as a universe polymorphic version of SumFin
  𝔽in : ℕ → FinSet ℓ
  𝔽in 0 = 𝟘
  𝔽in (suc n) = 𝟙 + 𝔽in n

  -- useful properties

  𝟘≃Empty : 𝟘 .fst ≃ ⊥
  𝟘≃Empty = uninhabEquiv rec* (λ x → x)

  𝟙≃Unit : 𝟙 .fst ≃ Unit
  𝟙≃Unit = isContr→≃Unit (isContrUnit*)

  * : {n : ℕ} → 𝔽in (suc n) .fst
  * = inl tt*

  𝔽in≃Fin : (n : ℕ) → 𝔽in n .fst ≃ Fin n
  𝔽in≃Fin 0 = 𝟘≃Empty
  𝔽in≃Fin (suc n) = ⊎-equiv 𝟙≃Unit (𝔽in≃Fin n)

  𝔽in≃Finℕ : (n : ℕ) → 𝔽in n .fst ≃ Finℕ n
  𝔽in≃Finℕ n = 𝔽in≃Fin n ⋆ SumFin≃Fin n

  -- 𝔽in preserves addition

  𝟘+X≡X : {X : FinSet ℓ} → 𝟘 + X ≡ X
  𝟘+X≡X {X = X} i .fst = ua (⊎-swap-≃ ⋆ ⊎-equiv (idEquiv (X .fst)) 𝟘≃Empty ⋆ ⊎-⊥-≃) i
  𝟘+X≡X {X = X} i .snd =
    isProp→PathP {B = λ i → isFinSet (𝟘+X≡X {X = X} i .fst)}
                 (λ _ → isPropIsFinSet) ((𝟘 + X) .snd) (X .snd) i

  𝔽in1≡𝟙 : 𝔽in 1 ≡ 𝟙
  𝔽in1≡𝟙 i .fst = ua (⊎-equiv (idEquiv (𝟙 .fst)) 𝟘≃Empty ⋆ ⊎-⊥-≃) i
  𝔽in1≡𝟙 i .snd =
    isProp→PathP {B = λ i → isFinSet (𝔽in1≡𝟙 i .fst)}
                 (λ _ → isPropIsFinSet) (𝔽in 1 .snd) (𝟙 .snd) i

  𝔽in+ : (m n : ℕ) → 𝔽in m + 𝔽in n ≡ 𝔽in (m +ℕ n)
  𝔽in+ 0 n = 𝟘+X≡X
  𝔽in+ (suc m) n i .fst = (ua (⊎-assoc-≃) ∙ (λ i → (𝟙 + 𝔽in+ m n i) .fst)) i
  𝔽in+ (suc m) n i .snd =
    isProp→PathP {B = λ i → isFinSet (𝔽in+ (suc m) n i .fst)}
                 (λ _ → isPropIsFinSet) ((𝔽in (suc m) + 𝔽in n) .snd) (𝔽in (suc m +ℕ n) .snd) i

-- every finite sets are merely equal to some 𝔽in

∣≡𝔽in∣ : (X : FinSet ℓ) → ∥ Σ[ n ∈ ℕ ] X ≡ 𝔽in n ∥
∣≡𝔽in∣ X = Prop.map (λ (n , p) → n , path X (n , p)) (isFinSet→isFinSet' (X .snd))
  where
    path : (X : FinSet ℓ) → ((n , _) : isFinOrd (X .fst)) → X ≡ 𝔽in n
    path X (n , p) i .fst = ua (p ⋆ invEquiv (𝔽in≃Fin n)) i
    path X (n , p) i .snd =
      isProp→PathP {B = λ i → isFinSet (path X (n , p) i .fst)}
                   (λ _ → isPropIsFinSet) (X .snd) (𝔽in n .snd) i

-- the eliminators

module _
  (P : FinSet ℓ → Type ℓ')
  (h : (X : FinSet ℓ) → isProp (P X)) where

  module _
    (p : (n : ℕ) → P (𝔽in n)) where

    elimProp : (X : FinSet ℓ) → P X
    elimProp X = Prop.rec (h X) (λ (n , q) → transport (λ i → P (q (~ i))) (p n)) (∣≡𝔽in∣ X)

  module _
    (p0 : P 𝟘)
    (p1 : {X : FinSet ℓ} → P X → P (𝟙 + X)) where

    elimProp𝔽in : (n : ℕ) → P (𝔽in n)
    elimProp𝔽in 0 = p0
    elimProp𝔽in (suc n) = p1 (elimProp𝔽in n)

    elimProp𝟙+ : (X : FinSet ℓ) → P X
    elimProp𝟙+ = elimProp elimProp𝔽in

  module _
    (p0 : P 𝟘)(p1 : P 𝟙)
    (p+ : {X Y : FinSet ℓ} → P X → P Y → P (X + Y)) where

    elimProp+ : (X : FinSet ℓ) → P X
    elimProp+ = elimProp𝟙+ p0 (λ p → p+ p1 p)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module Data.List.Combinatorics where

import      Lvl
open import Data
open import Data.List
open import Data.List.Functions
open        Data.List.Functions.LongOper
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Raiseᵣ as Tuple₊ using (_^_)
import      Data.Tuple.Raiseᵣ.Functions as Tuple₊
open import Functional
open import Numeral.Natural
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

-- A list of all non-empty sublists of the specified list.
-- The corresponding counting function is `(2 ^ n) − 1` where `n` is the length of the list.
-- Note:
--   In the inductive case, all of these are permutations of each other:
--   • `foldᵣ (prev ↦ rest ↦ (prev ⊰ (x ⊰ prev) ⊰ rest)) ∅ (sublists₊ l)` (This is used because of its "natural" order)
--   • `foldᵣ (prev ↦ rest ↦ ((x ⊰ prev) ⊰ prev ⊰ rest)) ∅ (sublists₊ l)`
--   • `(map (x ⊰_) (sublists₊ l)) ++ (sublists₊ l)`
--   • `(sublists₊ l) ++ (map (x ⊰_) (sublists₊ l))`
-- Examples:
--   sublists₊ []        = []
--   sublists₊ [1]       = [[1]]
--   sublists₊ [1,2]     = [[1],[2],[1,2]]
--   sublists₊ [1,2,3]   = [[1],[2],[1,2],[3],[1,3],[2,3],[1,2,3]]
--   sublists₊ [1,2,3,4] = [[1],[2],[1,2],[3],[1,3],[2,3],[1,2,3],[4],[1,4],[2,4],[1,2,4],[3,4],[1,3,4],[2,3,4],[1,2,3,4]]
sublists₊ : List(T) → List(List(T))
sublists₊ ∅       = ∅
sublists₊ (x ⊰ l) = singleton(x) ⊰ concatMap(y ↦ (y ⊰ (x ⊰ y) ⊰ ∅)) (sublists₊ l)

-- A list of all sublists of the specified list.
-- This is also the list of all subsets when the given list is a set (distinct elements).
-- The corresponding counting function is `2 ^ n` where `n` is the length of the list.
-- Examples:
--   sublists []        = [[]]
--   sublists [1]       = [[],[1]]
--   sublists [1,2]     = [[],[1],[2],[1,2]]
--   sublists [1,2,3]   = [[],[1],[2],[1,2],[3],[1,3],[2,3],[1,2,3]]
--   sublists [1,2,3,4] = [[],[1],[2],[1,2],[3],[1,3],[2,3],[1,2,3],[4],[1,4],[2,4],[1,2,4],[3,4],[1,3,4],[2,3,4],[1,2,3,4]]
sublists : List(T) → List(List(T))
sublists(l) = ∅ ⊰ sublists₊(l)

-- A list of all combinations of the specified size of the specified list.
-- The corresponding counting function is `𝑐𝐶(n,k)` where `n` is the length of the specified "multiset".
-- All subsets of size `n` from the set `l`.
-- Every unique subset of size n up to set equality.
-- This is also a list of all sublists of the specified size of the specified list.
-- Alternative definition that does not pass the termination checker:
--   combinations : ℕ → List(T) → List(List(T))
--   combinations 0         _ = ∅
--   combinations _         ∅ = ∅
--   combinations 1         l = map singleton l
--   combinations (𝐒(𝐒(n))) l = concat(map f(tails l)) where
--     f : List(T) → List(List(T))
--     f ∅      = ∅
--     f(x ⊰ l) = map (x ⊰_) (combinations (𝐒(n)) l)
-- Examples:
--   combinations _ []          = []
--   combinations 0 [a,b,c,...] = [[]]              when the list is non-empty
--   combinations 1 [a,b,c,...] = [[a],[b],[c],...] when the list is non-empty
--   combinations n l           = []  when (n ≥ length(l))
--   combinations n l           = [l] when (n = length(l))
--   combinations 2 [a,b,c]     = [[a,b],[a,c],[b,c]]
--   combinations 2 [a,b,c,d]   = [[a,b],[a,c],[a,d],[b,c],[b,d],[c,d]]
--   combinations 2 [a,b,c,d,e] = [[a,b],[a,c],[a,d],[a,e],[b,c],[b,d],[b,e],[c,d],[c,e],[d,e]]
--   combinations 3 [a,b,c,d]   = [[a,b,c],[a,b,d],[a,c,d],[b,c,d]]
--   combinations 3 [a,b,c,d,e] = [[a,b,c],[a,b,d],[a,b,e],[a,c,d],[a,c,e],[a,d,e],[b,c,d],[b,c,e],[b,d,e],[c,d,e]]
--   combinations 4 [a,b,c,d,e] = [[a,b,c,d],[a,b,c,e],[a,b,d,e],[a,c,d,e],[b,c,d,e]]
combinations : (k : ℕ) → List(T) → List(T ^ k)
combinations 0         _         = singleton(<>)
combinations (𝐒(_))    ∅         = ∅
combinations 1         l@(_ ⊰ _) = l
combinations (𝐒(𝐒(k))) (x ⊰ l)   = (map(x ,_) (combinations (𝐒(k)) l)) ++ (combinations(𝐒(𝐒(k))) l)

-- The corresponding counting function is `𝑐𝐶(n + k − 1 , k)` where `n` is the length of the specified "multiset".
-- Examples:
--   repeatableCombinations _ []          = []
--   repeatableCombinations 0 [a,b,c,...] = [[]]              when the list is non-empty
--   repeatableCombinations 1 [a,b,c,...] = [[a],[b],[c],...] when the list is non-empty
--   repeatableCombinations n [a]         = [repeat n a]
--   repeatableCombinations 2 [a,b]       = [[a,a],[a,b],[b,b]]
--   repeatableCombinations 2 [a,b,c]     = [[a,a],[a,b],[a,c],[b,b],[b,c],[c,c]]
--   repeatableCombinations 3 [a,b]       = [[a,a,a],[a,a,b],[a,b,b],[b,b,b]]
--   repeatableCombinations 3 [a,b,c]     = [[a,a,a],[a,a,b],[a,a,c],[a,b,b],[a,b,c],[a,c,c],[b,b,b],[b,b,c],[b,c,c],[c,c,c]]
--   repeatableCombinations 4 [a,b]       = [[a,a,a,a],[a,a,a,b],[a,a,b,b],[a,b,b,b],[b,b,b,b]]
--   repeatableCombinations 4 [a,b,c]     = [[a,a,a,a],[a,a,a,b],[a,a,a,c],[a,a,b,b],[a,a,b,c],[a,a,c,c],[a,b,b,b],[a,b,b,c],[a,b,c,c],[a,c,c,c],[b,b,b,b],[b,b,b,c],[b,b,c,c],[b,c,c,c],[c,c,c,c]]
repeatableCombinations : (k : ℕ) → List(T) → List(T ^ k)
repeatableCombinations 0         _         = singleton(<>)
repeatableCombinations (𝐒(_))    ∅         = ∅
repeatableCombinations 1         l@(_ ⊰ _) = l
repeatableCombinations (𝐒(𝐒(k))) (x ⊰ l)   = (map (x ,_) (repeatableCombinations (𝐒(k)) (x ⊰ l))) ++ (repeatableCombinations (𝐒(𝐒(k))) l)

-- A list of all tuples of length `n` from the "multiset" `l`.
-- Every tuple combination of length `n`.
-- The corresponding counting function is `k ^ n` where `k` is the length of the list.
-- Examples:
--   tuples 0 [a]     = [()]
--   tuples 1 [a]     = [a]
--   tuples 2 [a]     = [(a,a)]
--   tuples 0 [a,b]   = [()]
--   tuples 1 [a,b]   = [a,b]
--   tuples 2 [a,b]   = [(a,a) , (a,b) , (b,a) , (b,b)]
--   tuples 0 [a,b,c] = [()]
--   tuples 1 [a,b,c] = [a,b,c]
--   tuples 2 [a,b,c] = [(a,a) , (a,b) , (a,c) , (b,a) , (b,b) , (b,c) , (c,a) , (c,b), (c,c)]
tuples : (n : ℕ) → List(T) → List(T ^ n)
tuples 0           = const(singleton(<>))
tuples 1           = id
tuples (𝐒(𝐒(n))) l = concatMap(x ↦ map (Tuple₊.prepend x) (tuples (𝐒(n)) l)) l

-- A list of all rotations of a list.
-- Examples:
--   rotations []        = []
--   rotations [a]       = [[a]]
--   rotations [a,b]     = [[a,b] , [b,a]]
--   rotations [a,b,c]   = [[a,b,c] , [b,c,a] , [c,a,b]]
--   rotations [a,b,c,d] = [[a,b,c,d] , [b,c,d,a] , [c,d,a,b] , [d,a,b,c]]
rotations : List(T) → List(List(T))
rotations l = accumulateIterate₀(length l) (rotateₗ(1)) l

-- Accumulated `insertAt` for every position of the given list.
-- Examples:
--   insertedEverywhere i []        = [[i]]
--   insertedEverywhere i [a]       = [[i,a],[a,i]]
--   insertedEverywhere i [a,b]     = [[i,a,b],[a,i,b],[a,b,i]]
--   insertedEverywhere i [a,b,c]   = [[i,a,b,c],[a,i,b,c],[a,b,i,c],[a,b,c,i]]
--   insertedEverywhere i [a,b,c,d] = [[i,a,b,c,d],[a,i,b,c,d],[a,b,i,c,d],[a,b,c,i,d],[a,b,c,d,i]
insertedEverywhere : T → List(T) → List(List(T))
insertedEverywhere i ∅       = singleton(singleton i)
insertedEverywhere i (x ⊰ l) = (i ⊰ x ⊰ l) ⊰ (map (prepend x) (insertedEverywhere i l))

-- Every reordering of the list's elements.
-- Examples:
--   permutations []        = [[]]
--   permutations [a]       = [[a]]
--   permutations [a,b]     = [[a,b],[b,a]]
--   permutations [a,b,c]   = [[a,b,c],[b,a,c],[b,c,a],[a,c,b],[c,a,b],[c,b,a]]
--   permutations [a,b,c,d] = [[a,b,c,d],[b,a,c,d],[b,c,a,d],[b,c,d,a],[a,c,b,d],[c,a,b,d],[c,b,a,d],[c,b,d,a],[a,c,d,b],[c,a,d,b],[c,d,a,b],[c,d,b,a],[a,b,d,c],[b,a,d,c],[b,d,a,c],[b,d,c,a],[a,d,b,c],[d,a,b,c],[d,b,a,c],[d,b,c,a],[a,d,c,b],[d,a,c,b],[d,c,a,b],[d,c,b,a]]
permutations : List(T) → List(List(T))
permutations ∅               = singleton(∅)
permutations (x ⊰ ∅)         = singleton(singleton x)
permutations (x ⊰ l@(_ ⊰ _)) = concatMap (insertedEverywhere x) (permutations l)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --rewriting #-}
module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data D (A : Set) : Set₁ where
  c₁ : D A
  c₂ : Set → D A

f : {A : Set} → D A → Set
f c₁ = Bool
f (c₂ X) = X

postulate
  rew : (A : Set) → c₁ {A} ≡ c₂ A

-- This rewrite rule is rejected because the A on the lhs of the rule
-- only appears in a parameter position, but parameters are erased.
-- Reconstructing the parameter would only be possible if we had
-- access to the type during reduction, but we don't.
{-# REWRITE rew #-}

boom : f {Bool} c₁ ≡ Bool
boom = refl


text:
module Tactic.Reflection.Quote where

open import Prelude
open import Builtin.Reflection
open import Builtin.Float
open import Tactic.Reflection.Quote.Class public
open import Tactic.Deriving.Quotable
open import Container.Traversable

--- Instances ---

private
  QuoteLit : {A : Set} → (A → Literal) → Quotable A
  ` {{QuoteLit f}} x = lit (f x)

-- Primitive types --

instance
  QuotableNat    = QuoteLit nat
  QuotableWord64 = QuoteLit word64
  QuotableFloat  = QuoteLit float
  QuotableString = QuoteLit string
  QuotableChar   = QuoteLit char
  QuotableName   = QuoteLit name

-- Standard data types --

unquoteDecl QuotableBool       = deriveQuotable QuotableBool       (quote Bool)
unquoteDecl QuotableList       = deriveQuotable QuotableList       (quote List)
unquoteDecl QuotableMaybe      = deriveQuotable QuotableMaybe      (quote Maybe)
unquoteDecl QuotableEither     = deriveQuotable QuotableEither     (quote Either)

instance
  QuotableΣ : ∀ {a b} {A : Set a} {B : A → Set b} {{_ : Quotable A}} {{_ : {x : A} → Quotable (B x)}} → Quotable (Σ A λ a → B a)
  QuotableΣ = record { ` = λ { (x , y) → con (quote _,_) ((vArg (` x)) ∷ vArg (` y) ∷ [])} }

unquoteDecl Quotable⊤          = deriveQuotable Quotable⊤          (quote ⊤)
unquoteDecl Quotable⊥          = deriveQuotable Quotable⊥          (quote ⊥)
unquoteDecl Quotable≡          = deriveQuotable Quotable≡          (quote _≡_)
unquoteDecl QuotableComparison = deriveQuotable QuotableComparison (quote Comparison)
unquoteDecl QuotableLessNat    = deriveQuotable QuotableLessNat    (quote LessNat)
unquoteDecl QuotableInt        = deriveQuotable QuotableInt        (quote Int)

-- The reflection machinery can't deal with computational irrelevance (..)
-- unquoteDecl QuotableFin        = deriveQuotable QuotableFin        (quote Fin)
-- unquoteDecl QuotableVec        = deriveQuotable QuotableVec        (quote Vec)

instance
  QuotableFin : ∀ {n} → Quotable (Fin n)
  ` {{QuotableFin}} zero    = con (quote Fin.zero) []
  ` {{QuotableFin}} (suc i) = con (quote Fin.suc) (vArg (` i) ∷ [])

  QuotableVec : ∀ {a} {A : Set a} {n} {{_ : Quotable A}} → Quotable (Vec A n)
  ` {{QuotableVec}} []       = con (quote Vec.[]) []
  ` {{QuotableVec}} (x ∷ xs) = con (quote Vec._∷_) (vArg (` x) ∷ vArg (` xs) ∷ [])

-- Reflection types --

instance
  QuotableMeta : Quotable Meta
  ` {{QuotableMeta}} x = lit (meta x)

private
  deriveQuotableTermTypes : Vec Name _ → TC ⊤
  deriveQuotableTermTypes is = do
    let ts : Vec Name _
        ts = quote Term ∷ quote Clause ∷ quote Sort ∷ []
        its = ⦇ is , ts ⦈
    traverse (uncurry declareQuotableInstance) its
    traverse (uncurry defineQuotableInstance)  its
    pure _

unquoteDecl QuotableVisibility QuotableRelevance QuotableArgInfo
            QuotableArg QuotableAbs QuotableLiteral = do
  deriveQuotable QuotableVisibility (quote Visibility)
  deriveQuotable QuotableRelevance  (quote Relevance)
  deriveQuotable QuotableArgInfo    (quote ArgInfo)
  deriveQuotable QuotableArg        (quote Arg)
  deriveQuotable QuotableAbs        (quote Abs)
  deriveQuotable QuotableLiteral    (quote Literal)

{-# TERMINATING #-}
unquoteDecl QuotablePattern QuotableTerm QuotableClause QuotableSort = do
  deriveQuotable QuotablePattern (quote Pattern)
  deriveQuotableTermTypes (QuotableTerm ∷ QuotableClause ∷ QuotableSort ∷ [])

quoteList : List Term → Term
quoteList = foldr (λ x xs → con (quote List._∷_) (vArg x ∷ vArg xs ∷ [])) (con (quote List.[]) [])

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
-- This combination should not be allowed:

{-# OPTIONS --safe --guardedness --sized-types #-}

-- note that `--safe` turns off `--guardedness` and `--sized-types`,
-- hence `--guardedness --sized-types --safe` works, but does not
-- mean the above combination

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Data.Product using ( ∃ ; _×_ )
open import FRP.LTL.RSet.Core using ( RSet ; _[_,_⟩ )
open import FRP.LTL.Time using ( _≤_ )

module FRP.LTL.RSet.Until where

infixr 2 _U_

_U_ : RSet → RSet → RSet
(A U B) t = ∃ λ u → (t ≤ u) × (A [ t , u ⟩) × B u

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
open import Data.Product using ( proj₁ ; proj₂ )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _,_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; on-bnode ; bnodes ; _,_ ; ⊨a-resp-≲ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Properties.Composition.Lemmas using
  ( compose-left ; compose-right ; compose-resp-⊨a )
open import Web.Semantic.DL.Category.Properties.Tensor.Lemmas using
  ( tensor-up ; tensor-down ; tensor-resp-⊨a )
open import Web.Semantic.DL.Category.Object using ( Object ; IN ; fin )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; BN ; impl ; _⊑_ ; _≣_ ; _,_ )
open import Web.Semantic.DL.Category.Tensor using ( _⊗_ ; _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Unit using ( I )
open import Web.Semantic.DL.Category.Wiring using
  ( wires-≈ ; wires-≈⁻¹ ; assoc )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using
  ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-refl′ ; ≈-sym )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( ≲-refl )
open import Web.Semantic.Util using
  ( _∘_ ; False ; ⊎-assoc ; ⊎-assoc⁻¹
  ; _⊕_⊕_ ; inode ; bnode ; enode ; left ; right ; up ; down )

module Web.Semantic.DL.Category.Properties.Tensor.AssocNatural
  {Σ : Signature} {S T : TBox Σ} where

assoc-natural : ∀ {A₁ A₂ A₃ B₁ B₂ B₃ : Object S T}
  (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) (F₃ : A₃ ⇒ B₃) →
    (((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) ∙ assoc B₁ B₂ B₃ ≣
      assoc A₁ A₂ A₃ ∙ (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)))
assoc-natural {A₁} {A₂} {A₃} {B₁} {B₂} {B₃} F₁ F₂ F₃ = (LHS⊑RHS , RHS⊑LHS) where

  LHS⊑RHS : ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) ∙ assoc B₁ B₂ B₃ ⊑
    assoc A₁ A₂ A₃ ∙ (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃))
  LHS⊑RHS J J⊨STA J⊨LHS = (f , J⊨RHS) where

    f : (False ⊕ (IN A₁ ⊎ (IN A₂ ⊎ IN A₃)) ⊕ (BN F₁ ⊎ (BN F₂ ⊎ BN F₃))) → Δ ⌊ J ⌋
    f (inode ())
    f (bnode x) = ind J (inode (⊎-assoc⁻¹ x))
    f (enode v) = ind J (bnode (inode (⊎-assoc⁻¹ v)))

    lemma₁ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (left (up (up x))) ≈
        on-bnode f (ind J) (right (up x))
    lemma₁ (inode x) = ≈-refl ⌊ J ⌋
    lemma₁ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₁ (enode y) = wires-≈ ⊎-assoc⁻¹
      (proj₂ (fin (B₁ ⊗ (B₂ ⊗ B₃))) (inj₁ y))
      (compose-right ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) (assoc B₁ B₂ B₃) J J⊨LHS)

    lemma₂ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (left (up (down x))) ≈
        on-bnode f (ind J) (right (down (up x)))
    lemma₂ (inode x) = ≈-refl ⌊ J ⌋
    lemma₂ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₂ (enode y) = wires-≈ ⊎-assoc⁻¹
      (proj₂ (fin (B₁ ⊗ (B₂ ⊗ B₃))) (inj₂ (inj₁ y)))
      (compose-right ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) (assoc B₁ B₂ B₃) J J⊨LHS)

    lemma₃ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (left (down x)) ≈
        on-bnode f (ind J) (right (down (down x)))
    lemma₃ (inode x) = ≈-refl ⌊ J ⌋
    lemma₃ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₃ (enode y) = wires-≈ ⊎-assoc⁻¹
      (proj₂ (fin (B₁ ⊗ (B₂ ⊗ B₃))) (inj₂ (inj₂ y)))
      (compose-right ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) (assoc B₁ B₂ B₃) J J⊨LHS)

    J⊨RHS : bnodes J f ⊨a impl (assoc A₁ A₂ A₃ ∙ (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)))
    J⊨RHS = compose-resp-⊨a (assoc A₁ A₂ A₃) (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)) (bnodes J f)
      (wires-≈⁻¹ ⊎-assoc⁻¹ (λ x → ≈-refl ⌊ J ⌋) (proj₁ (fin (A₁ ⊗ (A₂ ⊗ A₃)))))
      (tensor-resp-⊨a F₁ (F₂ ⟨⊗⟩ F₃) (right * bnodes J f)
        (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₁) (impl F₁)
          (tensor-up F₁ F₂ (up * left * J)
            (tensor-up (F₁ ⟨⊗⟩ F₂) F₃ (left * J)
              (compose-left ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) (assoc B₁ B₂ B₃) J J⊨LHS))))
        (tensor-resp-⊨a F₂ F₃ (down * right * bnodes J f)
          (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₂) (impl F₂)
            (tensor-down F₁ F₂ (up * left * J)
              (tensor-up (F₁ ⟨⊗⟩ F₂) F₃ (left * J)
                (compose-left ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) (assoc B₁ B₂ B₃) J J⊨LHS))))
          (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₃) (impl F₃)
            (tensor-down (F₁ ⟨⊗⟩ F₂) F₃ (left * J)
              (compose-left ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) (assoc B₁ B₂ B₃) J J⊨LHS)))))

  RHS⊑LHS : assoc A₁ A₂ A₃ ∙ (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)) ⊑
    ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) ∙ assoc B₁ B₂ B₃
  RHS⊑LHS J J⊨STA J⊨RHS = (f , J⊨LHS) where

    f : (((BN F₁ ⊎ BN F₂) ⊎ BN F₃) ⊕ ((IN B₁ ⊎ IN B₂) ⊎ IN B₃) ⊕ False) → Δ ⌊ J ⌋
    f (inode v) = ind J (bnode (enode (⊎-assoc v)))
    f (bnode y) = ind J (enode (⊎-assoc y))
    f (enode ())

    lemma₀ : ∀ x →
      ⌊ J ⌋ ⊨ ind J (enode (⊎-assoc (⊎-assoc⁻¹ x))) ≈ ind J (enode x)
    lemma₀ (inj₁ x) = ≈-refl ⌊ J ⌋
    lemma₀ (inj₂ (inj₁ x)) = ≈-refl ⌊ J ⌋
    lemma₀ (inj₂ (inj₂ y)) = ≈-refl ⌊ J ⌋

    lemma₁ : ∀ x → ⌊ J ⌋ ⊨ ind J (right (up x)) ≈
      on-bnode f (ind J) (left (up (up x)))
    lemma₁ (inode x) = ≈-sym ⌊ J ⌋ (wires-≈ ⊎-assoc⁻¹
      (proj₂ (fin (A₁ ⊗ (A₂ ⊗ A₃))) (inj₁ x))
      (compose-left (assoc A₁ A₂ A₃) (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)) J J⊨RHS))
    lemma₁ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₁ (enode y) = ≈-refl ⌊ J ⌋

    lemma₂ : ∀ x → ⌊ J ⌋ ⊨ ind J (right (down (up x))) ≈
      on-bnode f (ind J) (left (up (down x)))
    lemma₂ (inode x) = ≈-sym ⌊ J ⌋ (wires-≈ ⊎-assoc⁻¹
      (proj₂ (fin (A₁ ⊗ (A₂ ⊗ A₃))) (inj₂ (inj₁ x)))
      (compose-left (assoc A₁ A₂ A₃) (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)) J J⊨RHS))
    lemma₂ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₂ (enode y) = ≈-refl ⌊ J ⌋

    lemma₃ : ∀ x → ⌊ J ⌋ ⊨ ind J (right (down (down x))) ≈
      on-bnode f (ind J) (left (down x))
    lemma₃ (inode x) = ≈-sym ⌊ J ⌋ (wires-≈ ⊎-assoc⁻¹
      (proj₂ (fin (A₁ ⊗ (A₂ ⊗ A₃))) (inj₂ (inj₂ x)))
      (compose-left (assoc A₁ A₂ A₃) (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)) J J⊨RHS))
    lemma₃ (bnode v) = ≈-refl ⌊ J ⌋
    lemma₃ (enode y) = ≈-refl ⌊ J ⌋

    J⊨LHS : bnodes J f ⊨a impl (((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) ∙ assoc B₁ B₂ B₃)
    J⊨LHS = compose-resp-⊨a ((F₁ ⟨⊗⟩ F₂) ⟨⊗⟩ F₃) (assoc B₁ B₂ B₃) (bnodes J f)
      (tensor-resp-⊨a (F₁ ⟨⊗⟩ F₂) F₃ (left * bnodes J f)
        (tensor-resp-⊨a F₁ F₂ (up * left * bnodes J f)
          (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₁) (impl F₁)
            (tensor-up F₁ (F₂ ⟨⊗⟩ F₃) (right * J)
              (compose-right (assoc A₁ A₂ A₃) (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)) J J⊨RHS)))
          (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₂) (impl F₂)
            (tensor-up F₂ F₃ (down * right * J)
              (tensor-down F₁ (F₂ ⟨⊗⟩ F₃) (right * J)
                (compose-right (assoc A₁ A₂ A₃) (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)) J J⊨RHS)))))
       (⊨a-resp-≲ (≲-refl ⌊ J ⌋ , lemma₃) (impl F₃)
         (tensor-down F₂ F₃ (down * right * J)
           (tensor-down F₁ (F₂ ⟨⊗⟩ F₃) (right * J)
             (compose-right (assoc A₁ A₂ A₃) (F₁ ⟨⊗⟩ (F₂ ⟨⊗⟩ F₃)) J J⊨RHS)))))
      (wires-≈⁻¹ ⊎-assoc⁻¹ lemma₀ (proj₁ (fin (B₁ ⊗ (B₂ ⊗ B₃)))))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
{-# OPTIONS --allow-unsolved-metas #-}
module ExtractDependent where
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.String

apply : (A : Set) -> (B : A -> Set) ->
            ((x : A) -> B x) -> (a : A) -> B a
apply A B f a = f a

applySameName : (A : Set) -> (A : Set) -> (B : A -> Set) ->
             (h : Set) -> (h : (x : A) -> B x) -> (a : A) -> B a
applySameName C A B g f a = f a

-- TODO : Try same test with {A} {B} once the parser can handle that.
applyImp : {A : Set} -> {B : A -> Set} ->
            ((x : A) -> B x) -> (y : A) -> B y
applyImp f a = f a

applyImpSameName : {A : Set} -> {A : Set} -> {B : A -> Set} ->
             (h : Set) -> (h : (x : A) -> B x) -> (a : A) -> B a
applyImpSameName A B h = B h


text:
module FizzBuzz where

{-# IMPORT Data.Word #-}
{-# IMPORT FizzBuzz #-}

open import Data.Nat
open import IO.Primitive
open import Foreign.Haskell

postulate
  ℕ′ : Set
  zero′ : ℕ′
  suc′ : ℕ′ → ℕ′

{-# COMPILED_TYPE ℕ′ Data.Word.Word32 #-}
{-# COMPILED zero′ 0 #-}
{-# COMPILED suc′ succ #-}

fromℕ : ℕ → ℕ′
fromℕ zero = zero′
fromℕ (suc n) = suc′ (fromℕ n)

postulate FizzBuzz : ℕ′ → IO Unit
{-# COMPILED FizzBuzz FizzBuzz.fizzBuzz #-}

main : IO Unit
main = FizzBuzz (fromℕ 10000)

max_stars_repo_name: Taneb/AgdaCBuzz

max_issues_repo_name: Taneb/AgdaCBuzz

max_forks_repo_name: Taneb/AgdaCBuzz