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

module Data.Rational.SternBrocot where

open import Prelude
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Data.Bits renaming (Bits to ℚ⁺; [] to 1ℚ; 0∷_ to lℚ; 1∷_ to rℚ)
open import Data.Bits.Equatable

-- ⟦_⇓⟧ : ℚ⁺ → (ℕ × ℕ)
-- ⟦ 1ℚ ⇓⟧ = 1 , 1
-- ⟦ lℚ x ⇓⟧ = let p , q = ⟦ x ⇓⟧ in p , p ℕ.+ q
-- ⟦ rℚ x ⇓⟧ = let p , q = ⟦ x ⇓⟧ in p ℕ.+ q , q

-- module TerminationProofs where
--   Tᴮ⇒≡ : {n m : ℕ} → n ≡ m → T (n ℕ.≡ᴮ m)
--   Tᴮ⇒≡ {n} {m} n≡m = subst (λ n′ → T (n ℕ.≡ᴮ n′)) n≡m (ℕ.complete-== n)

--   lift-suc-≡ : ∀ {n m} s → m ≡ n → T (n ℕ.≡ᴮ s) → T (m ℕ.≡ᴮ s)
--   lift-suc-≡ {n} {m} s  m≡n p = Tᴮ⇒≡ (m≡n ; ℕ.sound-== (n) s p)

--   lemma₁ : ∀ a m → a ℕ.+ m ℕ.+ zero ≡ m ℕ.+ a
--   lemma₁ a m = ℕ.+-idʳ (a ℕ.+ m) ; ℕ.+-comm a m

--   lemma₂ : ∀ n a m → n ℕ.+ m ℕ.+ suc a ≡ n ℕ.+ suc m ℕ.+ a
--   lemma₂ n a m = ℕ.+-assoc n m (suc a) ; cong (n ℕ.+_) (ℕ.+-suc m a) ; sym (ℕ.+-assoc n (suc m) a)

--   lemma₃ : ∀ n a → n ℕ.+ a ℕ.+ zero ≡ n ℕ.+ zero ℕ.+ a
--   lemma₃ n a = ℕ.+-idʳ (n ℕ.+ a) ; cong (ℕ._+ a) (sym (ℕ.+-idʳ n))

-- _+1/_+1 : ℕ → ℕ → ℚ⁺
-- n +1/ m +1 = go zero n m (n ℕ.+ m)
--   where
--   go : (a n m s : ℕ) → ℚ⁺
--   go a zero    (suc m) (suc s) = lℚ (go zero a m s)
--   go a (suc n) (suc m) (suc s) = go (suc a) n m s
--   go a (suc n) zero    (suc s) = rℚ (go zero n a s)
--   go _ _       _       _       = 1ℚ

euclidian : ℕ → ℕ → ℕ → ℚ⁺
euclidian n m zero    = 1ℚ
euclidian n m (suc s) =
  if n ℕ.≡ᴮ m
  then 1ℚ
  else if n ℕ.<ᴮ m
  then lℚ (euclidian n (m ℕ.∸ (1 ℕ.+ n)) s)
  else rℚ (euclidian (n ℕ.∸ (1 ℕ.+ m)) m s)

normalise-suc : ℕ → ℕ → ℚ⁺
normalise-suc n m = euclidian n m (n ℕ.+ m)

ℚ : Type
ℚ = ℚ⁺

import Data.Rational.Unnormalised as F
open import Data.Rational.Unnormalised using (_/suc_; _/_)
import Data.Integer as ℤ
open import Data.Integer using (ℤ; ⁺; ⁻suc; ⁻)
open import Data.Bits.Fold

zer : (ℕ × ℕ) → (ℕ × ℕ)
zer (p , q) = p , suc p ℕ.+ q

one : (ℕ × ℕ) → (ℕ × ℕ)
one (p , q) = suc p ℕ.+ q , q

fraction : ℚ → (ℕ × ℕ)
fraction = foldr-bits zer one (0 , 0)

⟦_⇓⟧ : ℚ → F.ℚ
⟦ 1ℚ ⇓⟧ = ⁺ 0 F./suc 0
⟦ lℚ xs ⇓⟧ = let n , d = fraction xs in ⁻suc n /suc d
⟦ rℚ xs ⇓⟧ = let n , d = fraction xs in ⁺ (suc n) /suc d

⟦_⇑⟧ : F.ℚ → ℚ
⟦ ⁺ zero /suc den-pred ⇑⟧ = 1ℚ
⟦ ⁺ (suc x) /suc den-pred ⇑⟧ = rℚ (normalise-suc x den-pred)
⟦ ⁻suc x /suc den-pred ⇑⟧ = lℚ (normalise-suc x den-pred)

-- open import Path.Reasoning

-- n≢sn+d : ∀ n d → (n ℕ.≡ᴮ suc (n ℕ.+ d)) ≡ false
-- n≢sn+d zero d = refl
-- n≢sn+d (suc n) d = n≢sn+d n d

-- n<sn+d : ∀ n d → (n ℕ.<ᴮ suc (n ℕ.+ d)) ≡ true
-- n<sn+d zero d = refl
-- n<sn+d (suc n) d = n<sn+d n d

-- n+d-n≡d : ∀ n d → n ℕ.+ d ℕ.∸ n ≡ d
-- n+d-n≡d zero d = refl
-- n+d-n≡d (suc n) d = n+d-n≡d n d

-- euclidian-term-helper : ∀ n d s₁ s₂ → (n ℕ.+ d ℕ.≤ s₁) → (n ℕ.+ d ℕ.≤ s₂) → euclidian n d s₁ ≡ euclidian n d s₂
-- euclidian-term-helper zero zero zero zero p₁ p₂ = refl
-- euclidian-term-helper zero zero zero (suc s₂) p₁ p₂ = refl
-- euclidian-term-helper zero zero (suc s₁) zero p₁ p₂ = refl
-- euclidian-term-helper zero zero (suc s₁) (suc s₂) p₁ p₂ = refl
-- euclidian-term-helper zero (suc d) (suc s₁) (suc s₂) p₁ p₂ = cong lℚ (euclidian-term-helper zero d s₁ s₂ (ℕ.p≤p d s₁ p₁) (ℕ.p≤p d s₂ p₂))
-- euclidian-term-helper (suc n) zero (suc s₁) (suc s₂) p₁ p₂ = cong rℚ (euclidian-term-helper n zero s₁ s₂ (ℕ.p≤p (n ℕ.+ zero) s₁ p₁) (ℕ.p≤p (n ℕ.+ zero) s₂ p₂))
-- euclidian-term-helper (suc n) (suc d) (suc s₁) (suc s₂) p₁ p₂ with n ℕ.≡ᴮ d | n ℕ.<ᴮ d
-- euclidian-term-helper (suc n) (suc d) (suc s₁) (suc s₂) p₁ p₂ | false | false = cong rℚ (euclidian-term-helper (n ℕ.∸ suc d) (suc d) s₁ s₂ {!!} {!!})
-- euclidian-term-helper (suc n) (suc d) (suc s₁) (suc s₂) p₁ p₂ | false | true  = cong lℚ (euclidian-term-helper (suc n) (d ℕ.∸ suc n) s₁ s₂ {!!} {!!})
-- euclidian-term-helper (suc n) (suc d) (suc s₁) (suc s₂) p₁ p₂ | true  | _ = refl

-- norm-l : ∀ n d → normalise-suc n (suc n ℕ.+ d) ≡ lℚ (normalise-suc n d)
-- norm-l n d =
--   normalise-suc n (suc n ℕ.+ d) ≡⟨⟩
--   euclidian n (suc n ℕ.+ d) (n ℕ.+ (suc n ℕ.+ d)) ≡⟨ cong (euclidian n (suc n ℕ.+ d)) (ℕ.+-suc n (n ℕ.+ d)) ⟩
--   euclidian n (suc n ℕ.+ d) (suc n ℕ.+ (n ℕ.+ d)) ≡⟨⟩
--   (if n ℕ.≡ᴮ suc (n ℕ.+ d) then 1ℚ else
--        if n ℕ.<ᴮ suc (n ℕ.+ d) then lℚ (euclidian n (n ℕ.+ d ℕ.∸ n) (n ℕ.+ (n ℕ.+ d))) else rℚ (euclidian (n ℕ.∸ suc (suc (n ℕ.+ d))) (suc (n ℕ.+ d)) (n ℕ.+ (n ℕ.+ d)))) ≡⟨ cong (if_then 1ℚ else if n ℕ.<ᴮ suc (n ℕ.+ d) then lℚ (euclidian n (n ℕ.+ d ℕ.∸ n) (n ℕ.+ (n ℕ.+ d))) else rℚ (euclidian (n ℕ.∸ suc (suc (n ℕ.+ d))) (suc (n ℕ.+ d)) (n ℕ.+ (n ℕ.+ d)))) (n≢sn+d n d) ⟩
--   (if n ℕ.<ᴮ suc (n ℕ.+ d) then
--        lℚ (euclidian n (n ℕ.+ d ℕ.∸ n) (n ℕ.+ (n ℕ.+ d))) else
--        rℚ (euclidian (n ℕ.∸ suc (suc (n ℕ.+ d))) (suc (n ℕ.+ d)) (n ℕ.+ (n ℕ.+ d)))) ≡⟨ cong (if_then lℚ ((euclidian n (n ℕ.+ d ℕ.∸ n) (n ℕ.+ (n ℕ.+ d)))) else rℚ ((euclidian (n ℕ.∸ suc (suc (n ℕ.+ d))) (suc (n ℕ.+ d)) (n ℕ.+ (n ℕ.+ d))))) (n<sn+d n d) ⟩
--   lℚ (euclidian n (n ℕ.+ d ℕ.∸ n) (n ℕ.+ (n ℕ.+ d))) ≡⟨ cong (λ ndn → lℚ (euclidian n ndn (n ℕ.+ (n ℕ.+ d)))) (n+d-n≡d n d) ⟩
--   lℚ (euclidian n d (n ℕ.+ (n ℕ.+ d))) ≡⟨ {!!} ⟩
--   lℚ (euclidian n d (n ℕ.+ d)) ≡⟨⟩
--   lℚ (normalise-suc n d) ∎

-- ℚ-retract′ : ∀ x → normalise-suc (fst (fraction x)) (snd (fraction x)) ≡ x
-- ℚ-retract′ 1ℚ = refl
-- ℚ-retract′ (rℚ x) = {!!}
-- ℚ-retract′ (lℚ x) = let n , d = fraction x in
--   normalise-suc n (suc (n ℕ.+ d)) ≡⟨ {!!} ⟩
--   lℚ x ∎

-- ℚ-retract : ∀ x → ⟦ ⟦ x ⇓⟧ ⇑⟧ ≡ x
-- ℚ-retract 1ℚ = refl
-- ℚ-retract (lℚ x) = cong lℚ (ℚ-retract′ x)
-- ℚ-retract (rℚ x) = cong rℚ (ℚ-retract′ x)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module _ where

record ⊤ : Set where
  instance
    constructor tt

data Nat : Set where
  suc  : Nat → Nat

NZ : Nat → Set
NZ (suc _) = ⊤

postulate
  A : ∀ n → {{_ : NZ n}} → Set

B : ∀ n (nz : NZ n) → Set
B (suc n) nz = A (suc n)

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Nat where

data Rel (A : Set) : Set1 where
  rel : (A -> A -> Set) -> Rel A

_is_than_ : {A : Set} -> A -> Rel A -> A -> Set
x is rel f than y = f x y

data Acc {A : Set} (less : Rel A) (x : A) : Set where
  acc : ((y : A) -> x is less than y -> Acc less y) -> Acc less x

data WO {A : Set} (less : Rel A) : Set where
  wo : ((x : A) -> Acc less x) -> WO less

data False : Set where
data True : Set where
  tt : True

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

data ∏ {A : Set} (f : A -> Set) : Set where
  ∏I : ((z : A) -> f z) -> ∏ f

ltNat : Nat -> Nat -> Set
ltNat Z Z = False
ltNat Z (S n) = True
ltNat (S m) (S n) = ltNat m n
ltNat (S m) Z = False

ltNatRel : Rel Nat
ltNatRel = rel ltNat

postulate woltNat : WO ltNatRel

idN : Nat -> Nat
idN x = x

id  : {A : Set} -> A -> A
id x = x

down1 : Nat -> Nat
down1 Z = Z
down1 (S n) = down1 n

-- measure down1 = (woNat, id)
-- For a function f : (x:A) -> B(x)
-- f(p) = ... f(x1) ... f(x2)
-- measure_set : Set
-- measure_rel : Rel measure_set
-- measure_ord : WO measure_rel
-- measure_fun : A -> measure_set
-- For j-th call of f in i-th clause of f:
-- measure_i_j_hint : xj is measure_rel than p

data Measure : Set1 where
  μ : {M : Set} -> {rel : Rel M} -> (ord : WO rel) -> Measure

{-
down1_measure_set : Set
down1_measure_set = Nat
down1_measure_rel : Rel down1_measure_set
down1_measure_rel = ltNatRel
down1_measure_ord : WO measure_rel
down1_measure_ord = woltNat
-}
down1-measure : Measure
down1-measure = μ woltNat

down1-2-1-hint : (n : Nat) -> n is ltNatRel than (S n)
down1-2-1-hint Z = tt
down1-2-1-hint (S n) = down1-2-1-hint n

{-
down2 : Nat -> Nat
down2 Z = Z
down2 (S n) = down2 (idN n)

down3 : Nat -> Nat
down3 Z = Z
down3 (S n) = down3 (id n)

plus : Nat -> Nat -> Nat
plus Z n = n
plus (S m) n = S(plus m n)
-}


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

postulate
  tac : {A : Set} (x : A) → Term → TC ⊤

data D : Set where
  con : {@(tactic tac true) y : Bool} → D

-- WAS: Internal error in Serialize/Instances/Internal for MetaV case
-- SHOULD: succeed

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

Pointed structure: X ↦ X

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Foundations.Univalence
open import Cubical.Relation.ZigZag.Base
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Structures.Pointed

private
  variable
    ℓ : Level

-- Structured relations

PointedRelStr : StrRel PointedStructure ℓ
PointedRelStr R = R

pointedSuitableRel : SuitableStrRel {ℓ = ℓ} PointedStructure PointedRelStr
pointedSuitableRel .quo _ _ _ = isContrSingl _
pointedSuitableRel .symmetric _ r = r
pointedSuitableRel .transitive _ _ r r' = ∣ _ , r , r' ∣
pointedSuitableRel .set setX = setX
pointedSuitableRel .prop propR = propR

pointedRelMatchesEquiv : StrRelMatchesEquiv {ℓ = ℓ} PointedRelStr PointedEquivStr
pointedRelMatchesEquiv _ _ _ = idEquiv _

pointedRelAction : StrRelAction {ℓ = ℓ} PointedRelStr
pointedRelAction .actStr f = f
pointedRelAction .actStrId _ = refl
pointedRelAction .actRel α = α

pointedPositiveRel : PositiveStrRel {ℓ = ℓ} pointedSuitableRel
pointedPositiveRel .act = pointedRelAction
pointedPositiveRel .reflexive x = ∣ refl ∣
pointedPositiveRel .detransitive R R' rr' = rr'
pointedPositiveRel .quo R = isoToIsEquiv isom
  where
  open Iso
  isom : Iso _ _
  isom .fun = _
  isom .inv q = q
  isom .rightInv = elimProp (λ _ → squash/ _ _) (λ _ → refl)
  isom .leftInv = elimProp (λ _ → squash/ _ _) (λ _ → refl)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Issue #4115 reported by Guillaume Brunerie

{-# OPTIONS --prop #-}

data Unit : Set where
  tt : Unit

postulate
  P : Prop

{-# TERMINATING #-}
p : P
p = p

works : Unit → P
works b = p

-- WAS: Agda loops during injectivity analysis of `loops`
loops : Unit → P
loops tt = p


text:
module Data.Boolean.Stmt.Proofs where

import      Lvl
open import Data.Boolean
open import Data.Boolean.Proofs hiding (bivalence ; disjointness)
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.Boolean.Stmt
open import Functional
open import Logic.Propositional as Logic using (⊥ ; _∨_ ; _∧_ ; ¬_ ; _↔_ ; [⊤]-intro ; [↔]-intro ; [⊥]-elim)
open import Relator.Equals
open import Type

-- A boolean operation is either true or false
bivalence : ∀{a} → (IsTrue(a) ∨ IsFalse(a))
bivalence {𝑇} = Logic.[∨]-introₗ [⊤]-intro
bivalence {𝐹} = Logic.[∨]-introᵣ [⊤]-intro

-- A boolean operation is not both true and false at the same time
disjointness : ∀{a} → IsTrue(a) → IsFalse(a) → ⊥
disjointness {𝑇} [⊤]-intro ()
disjointness {𝐹} () [⊤]-intro

module IsTrue where
  [𝑇]-intro : IsTrue(𝑇)
  [𝑇]-intro = [⊤]-intro

  [𝐹]-elim : ¬ IsTrue(𝐹)
  [𝐹]-elim ()

  [∧]-intro : ∀{a b} → IsTrue(a) → IsTrue(b) → IsTrue(a && b)
  [∧]-intro {𝑇} {b} ta tb = tb
  [∧]-intro {𝐹} {b} ta tb = ta

  [∨]-introₗ : ∀{a b} → IsTrue(a) → IsTrue(a || b)
  [∨]-introₗ {_}{𝑇} _ = [⊤]-intro
  [∨]-introₗ {_}{𝐹} = id

  [∨]-introᵣ : ∀{a b} → IsTrue(b) → IsTrue(a || b)
  [∨]-introᵣ {𝑇}{_} _ = [⊤]-intro
  [∨]-introᵣ {𝐹}{_} = id

  [∧]-elimₗ : ∀{a b} → IsTrue(a && b) → IsTrue(a)
  [∧]-elimₗ {𝑇}{𝑇} [⊤]-intro = [⊤]-intro
  [∧]-elimₗ {𝑇}{𝐹} ()
  [∧]-elimₗ {𝐹}{𝑇} ()
  [∧]-elimₗ {𝐹}{𝐹} ()

  [∧]-elimᵣ : ∀{a b} → IsTrue(a && b) → IsTrue(b)
  [∧]-elimᵣ {𝑇}{𝑇} [⊤]-intro = [⊤]-intro
  [∧]-elimᵣ {𝑇}{𝐹} ()
  [∧]-elimᵣ {𝐹}{𝑇} ()
  [∧]-elimᵣ {𝐹}{𝐹} ()

  [∨]-elim : ∀{ℓ₂}{φ : Type{ℓ₂}}{a b} → (IsTrue(a) → φ) → (IsTrue(b) → φ) → IsTrue(a || b) → φ
  [∨]-elim {_}{_}{𝑇}{𝑇} f _ [⊤]-intro = f [⊤]-intro
  [∨]-elim {_}{_}{𝑇}{𝐹} f _ [⊤]-intro = f [⊤]-intro
  [∨]-elim {_}{_}{𝐹}{𝑇} _ f [⊤]-intro = f [⊤]-intro
  [∨]-elim {_}{_}{𝐹}{𝐹} _ f ()

  [¬]-intro : ∀{a} → IsFalse(a) → IsTrue(! a)
  [¬]-intro {𝐹} fa = [⊤]-intro

  [¬]-elim : ∀{a} → IsTrue(! a) → IsFalse(a)
  [¬]-elim {𝑇} ()
  [¬]-elim {𝐹} [⊤]-intro = [⊤]-intro

  [→?]-intro : ∀{a b} → (IsTrue a → IsTrue b) → IsTrue (a →? b)
  [→?]-intro {𝑇} {𝑇} _   = [⊤]-intro
  [→?]-intro {𝑇} {𝐹} tab = tab [⊤]-intro
  [→?]-intro {𝐹} {𝑇} _   = [⊤]-intro
  [→?]-intro {𝐹} {𝐹} _   = [⊤]-intro

  [→?]-elim : ∀{a b} → IsTrue (a →? b) → (IsTrue a → IsTrue b)
  [→?]-elim {𝑇} {𝑇} tab ta = [⊤]-intro

  [←?]-intro : ∀{a b} → (IsTrue b → IsTrue a) → IsTrue (a ←? b)
  [←?]-intro {𝑇} {𝑇} tba = [⊤]-intro
  [←?]-intro {𝑇} {𝐹} tba = [⊤]-intro
  [←?]-intro {𝐹} {𝑇} tba = tba [⊤]-intro
  [←?]-intro {𝐹} {𝐹} tba = [⊤]-intro

  [←?]-elim : ∀{a b} → IsTrue (a ←? b) → (IsTrue b → IsTrue a)
  [←?]-elim {𝑇} {𝑇} tab tb = [⊤]-intro

  [==]-intro : ∀{a b} → (IsTrue b → IsTrue a) → (IsTrue a → IsTrue b) → IsTrue(a == b)
  [==]-intro {𝑇} {𝑇} ba ab = [⊤]-intro
  [==]-intro {𝑇} {𝐹} ba ab = ab [⊤]-intro
  [==]-intro {𝐹} {𝑇} ba ab = ba [⊤]-intro
  [==]-intro {𝐹} {𝐹} ba ab = [⊤]-intro

  [==]-elimₗ : ∀{a b} → IsTrue(a == b) → (IsTrue b → IsTrue a)
  [==]-elimₗ {𝑇} {𝑇} tab tb = [⊤]-intro

  [==]-elimᵣ : ∀{a b} → IsTrue(a == b) → (IsTrue a → IsTrue b)
  [==]-elimᵣ {𝑇} {𝑇} tab ta = [⊤]-intro

  [!]-intro : ∀{a b} → (IsTrue a → IsTrue b) → (IsTrue a → IsTrue(not b)) → IsTrue(not a)
  [!]-intro {𝑇} {𝑇} tab tanb = tanb [⊤]-intro
  [!]-intro {𝑇} {𝐹} tab tanb = tab [⊤]-intro
  [!]-intro {𝐹} {𝑇} tab tanb = [⊤]-intro
  [!]-intro {𝐹} {𝐹} tab tanb = [⊤]-intro

  [!]-elim : ∀{a b} → IsTrue a → IsTrue(not a) → IsTrue b
  [!]-elim {𝑇} {𝑇} ta tnb = [⊤]-intro
  [!]-elim {𝑇} {𝐹} ta tnb = tnb
  [!]-elim {𝐹} {𝑇} ta tnb = [⊤]-intro
  [!]-elim {𝐹} {𝐹} ta tnb = ta

  is-𝑇 : ∀{a} → IsTrue(a) ↔ (a ≡ 𝑇)
  is-𝑇 {a} = [↔]-intro (l{a}) (r{a}) where
    r : ∀ {a} → IsTrue(a) → (a ≡ 𝑇)
    r {𝑇} _ = [≡]-intro
    r {𝐹} ()

    l : ∀ {a} → IsTrue(a) ← (a ≡ 𝑇)
    l [≡]-intro = [⊤]-intro

  preserves-[&&][∧] : ∀{a b} → IsTrue(a && b) ↔ IsTrue(a) ∧ IsTrue(b)
  preserves-[&&][∧] = [↔]-intro
    (\{(Logic.[∧]-intro l r) → [∧]-intro l r})
    (proof ↦ Logic.[∧]-intro ([∧]-elimₗ proof) ([∧]-elimᵣ proof))

  preserves-[||][∨] : ∀{a b} → IsTrue(a || b) ↔ IsTrue(a) ∨ IsTrue(b)
  preserves-[||][∨] = [↔]-intro
    (Logic.[∨]-elim [∨]-introₗ [∨]-introᵣ)
    ([∨]-elim Logic.[∨]-introₗ Logic.[∨]-introᵣ)

  preserves-[!][¬] : ∀{a} → IsTrue(! a) ↔ (¬ IsTrue(a))
  preserves-[!][¬] {a} = [↔]-intro (l{a}) (r{a}) where
    l : ∀{a} → IsTrue(! a) ← (¬ IsTrue(a))
    l {𝐹} _ = [⊤]-intro
    l {𝑇} f = [⊥]-elim (f [⊤]-intro)

    r : ∀{a} → IsTrue(! a) → (¬ IsTrue(a))
    r {𝑇} () _
    r {𝐹} _ ()

module IsFalse where
  [∧]-introₗ : ∀{a b} → IsFalse(a) → IsFalse(a && b)
  [∧]-introₗ {_}{𝑇} = id
  [∧]-introₗ {_}{𝐹} _ = [⊤]-intro

  [∧]-introᵣ : ∀{a b} → IsFalse(b) → IsFalse(a && b)
  [∧]-introᵣ {𝑇}{_} = id
  [∧]-introᵣ {𝐹}{_} _ = [⊤]-intro

  [∨]-intro : ∀{a b} → IsFalse(a) → IsFalse(b) → IsFalse(a || b)
  [∨]-intro {𝑇} fa fb = fa
  [∨]-intro {𝐹} fa fb = fb

  [¬]-intro : ∀{a} → IsTrue(a) → IsFalse(! a)
  [¬]-intro = id

  [¬]-elim : ∀{a} → IsFalse(! a) → IsTrue(a)
  [¬]-elim = id

  is-𝐹 : ∀{a} → IsFalse(a) ↔ (a ≡ 𝐹)
  is-𝐹 {a} = [↔]-intro (l{a}) (r{a}) where
    r : ∀{a} → IsFalse(a) → (a ≡ 𝐹)
    r {𝑇} ()
    r {𝐹} _ = [≡]-intro

    l : ∀{a} → IsFalse(a) ← (a ≡ 𝐹)
    l [≡]-intro = [⊤]-intro

true-false-opposites : ∀{a} → IsTrue(a) ↔ (¬ IsFalse(a))
true-false-opposites {𝑇} = [↔]-intro (const [⊤]-intro) (const id)
true-false-opposites {𝐹} = [↔]-intro (_$    [⊤]-intro) const

false-true-opposites : ∀{a} → IsFalse(a) ↔ (¬ IsTrue(a))
false-true-opposites {𝑇} = [↔]-intro (_$    [⊤]-intro) const
false-true-opposites {𝐹} = [↔]-intro (const [⊤]-intro) (const id)

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:
-- Andreas, 2017-05-15, issue 2585, reported by Martin Stone Davis
-- Information about whether a function uses copatterns
-- needs to be added already while function is defines.
-- Otherwise, clauses might fail to check due to missing eta.

{-# OPTIONS --postfix-projections #-}

open import Agda.Builtin.Equality

record Super : Set₁ where
  eta-equality
  field
    set : Set

record Sub : Set₁ where
  eta-equality
  field
    super1 : Super
    super2 : Super
    super1=2 : super1 ≡ super2

postulate
  X : Set

works : Sub
works .Sub.super1 = record { set = X }
works .Sub.super2 .Super.set = X
works .Sub.super1=2 = refl

test : Sub
test .Sub.super1 .Super.set = X
test .Sub.super2 .Super.set = X
test .Sub.super1=2 = refl

-- Should pass


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Various forms of induction for natural numbers
------------------------------------------------------------------------

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

module Induction.Nat where

open import Function
open import Data.Nat
open import Data.Nat.Properties using (≤⇒≤′)
open import Data.Fin using (_≺_)
open import Data.Fin.Properties
open import Data.Product
open import Data.Unit
open import Induction
open import Induction.WellFounded as WF
open import Level using (Lift)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary

------------------------------------------------------------------------
-- Ordinary induction

Rec : ∀ ℓ → RecStruct ℕ ℓ ℓ
Rec ℓ P zero    = Lift ℓ ⊤
Rec ℓ P (suc n) = P n

recBuilder : ∀ {ℓ} → RecursorBuilder (Rec ℓ)
recBuilder P f zero    = _
recBuilder P f (suc n) = f n (recBuilder P f n)

rec : ∀ {ℓ} → Recursor (Rec ℓ)
rec = build recBuilder

------------------------------------------------------------------------
-- Complete induction

CRec : ∀ ℓ → RecStruct ℕ ℓ ℓ
CRec ℓ P zero    = Lift ℓ ⊤
CRec ℓ P (suc n) = P n × CRec ℓ P n

cRecBuilder : ∀ {ℓ} → RecursorBuilder (CRec ℓ)
cRecBuilder P f zero    = _
cRecBuilder P f (suc n) = f n ih , ih
  where ih = cRecBuilder P f n

cRec : ∀ {ℓ} → Recursor (CRec ℓ)
cRec = build cRecBuilder

------------------------------------------------------------------------
-- Complete induction based on _<′_

<′-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
<′-Rec = WfRec _<′_

mutual

  <′-wellFounded : WellFounded _<′_
  <′-wellFounded n = acc (<′-wellFounded′ n)

  <′-wellFounded′ : ∀ n → <′-Rec (Acc _<′_) n
  <′-wellFounded′ zero     _ ()
  <′-wellFounded′ (suc n) .n ≤′-refl       = <′-wellFounded n
  <′-wellFounded′ (suc n)  m (≤′-step m<n) = <′-wellFounded′ n m m<n

module _ {ℓ} where
  open WF.All <′-wellFounded ℓ public
    renaming ( wfRecBuilder to <′-recBuilder
             ; wfRec        to <′-rec
             )
    hiding (wfRec-builder)

------------------------------------------------------------------------
-- Complete induction based on _<_

<-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
<-Rec = WfRec _<_

<-wellFounded : WellFounded _<_
<-wellFounded = Subrelation.wellFounded ≤⇒≤′ <′-wellFounded

module _ {ℓ} where
  open WF.All <-wellFounded ℓ public
    renaming ( wfRecBuilder to <-recBuilder
             ; wfRec        to <-rec
             )
    hiding (wfRec-builder)

------------------------------------------------------------------------
-- Complete induction based on _≺_

≺-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
≺-Rec = WfRec _≺_

≺-wellFounded : WellFounded _≺_
≺-wellFounded = Subrelation.wellFounded ≺⇒<′ <′-wellFounded

module _ {ℓ} where
  open WF.All ≺-wellFounded ℓ public
    renaming ( wfRecBuilder to ≺-recBuilder
             ; wfRec        to ≺-rec
             )
    hiding (wfRec-builder)

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

private

 module Examples where

  -- Doubles its input.

  twice : ℕ → ℕ
  twice = rec _ λ
    { zero    _       → zero
    ; (suc n) twice-n → suc (suc twice-n)
    }

  -- Halves its input (rounding downwards).
  --
  -- The step function is mentioned in a proof below, so it has been
  -- given a name. (The mutual keyword is used to avoid having to give
  -- a type signature for the step function.)

  mutual

    half₁-step = λ
      { zero          _                → zero
      ; (suc zero)    _                → zero
      ; (suc (suc n)) (_ , half₁n , _) → suc half₁n
      }

    half₁ : ℕ → ℕ
    half₁ = cRec _ half₁-step

  -- An alternative implementation of half₁.

  mutual

    half₂-step = λ
      { zero          _   → zero
      ; (suc zero)    _   → zero
      ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl))
      }

    half₂ : ℕ → ℕ
    half₂ = <′-rec _ half₂-step

  -- The application half₁ (2 + n) is definitionally equal to
  -- 1 + half₁ n. Perhaps it is instructive to see why.

  half₁-2+ : ∀ n → half₁ (2 + n) ≡ 1 + half₁ n
  half₁-2+ n = begin

    half₁ (2 + n)                                                         ≡⟨⟩

    cRec _ half₁-step (2 + n)                                             ≡⟨⟩

    half₁-step (2 + n) (cRecBuilder _ half₁-step (2 + n))                 ≡⟨⟩

    half₁-step (2 + n)
      (let ih = cRecBuilder _ half₁-step (1 + n) in
       half₁-step (1 + n) ih , ih)                                        ≡⟨⟩

    half₁-step (2 + n)
      (let ih = cRecBuilder _ half₁-step n in
       half₁-step (1 + n) (half₁-step n ih , ih) , half₁-step n ih , ih)  ≡⟨⟩

    1 + half₁-step n (cRecBuilder _ half₁-step n)                         ≡⟨⟩

    1 + cRec _ half₁-step n                                               ≡⟨⟩

    1 + half₁ n                                                           ∎

    where open ≡-Reasoning

  -- The application half₂ (2 + n) is definitionally equal to
  -- 1 + half₂ n. Perhaps it is instructive to see why.

  half₂-2+ : ∀ n → half₂ (2 + n) ≡ 1 + half₂ n
  half₂-2+ n = begin

    half₂ (2 + n)                                               ≡⟨⟩

    <′-rec _ half₂-step (2 + n)                                 ≡⟨⟩

    half₂-step (2 + n) (<′-recBuilder _ half₂-step (2 + n))     ≡⟨⟩

    1 + <′-recBuilder _ half₂-step (2 + n) n (≤′-step ≤′-refl)  ≡⟨⟩

    1 + Some.wfRecBuilder _ half₂-step (2 + n)
          (<′-wellFounded (2 + n)) n (≤′-step ≤′-refl)          ≡⟨⟩

    1 + Some.wfRecBuilder _ half₂-step (2 + n)
          (acc (<′-wellFounded′ (2 + n))) n (≤′-step ≤′-refl)   ≡⟨⟩

    1 + half₂-step n
          (Some.wfRecBuilder _ half₂-step n
             (<′-wellFounded′ (2 + n) n (≤′-step ≤′-refl)))     ≡⟨⟩

    1 + half₂-step n
          (Some.wfRecBuilder _ half₂-step n
             (<′-wellFounded′ (1 + n) n ≤′-refl))               ≡⟨⟩

    1 + half₂-step n
          (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩

    1 + half₂-step n (<′-recBuilder _ half₂-step n)             ≡⟨⟩

    1 + <′-rec _ half₂-step n                                   ≡⟨⟩

    1 + half₂ n                                                 ∎

    where open ≡-Reasoning

  -- Some properties that the functions above satisfy, proved using
  -- cRec.

  half₁-+₁ : ∀ n → half₁ (twice n) ≡ n
  half₁-+₁ = cRec _ λ
    { zero          _                        → refl
    ; (suc zero)    _                        → refl
    ; (suc (suc n)) (_ , half₁twice-n≡n , _) →
        cong (suc ∘ suc) half₁twice-n≡n
    }

  half₂-+₁ : ∀ n → half₂ (twice n) ≡ n
  half₂-+₁ = cRec _ λ
    { zero          _                        → refl
    ; (suc zero)    _                        → refl
    ; (suc (suc n)) (_ , half₁twice-n≡n , _) →
        cong (suc ∘ suc) half₁twice-n≡n
    }

  -- Some properties that the functions above satisfy, proved using
  -- <′-rec.

  half₁-+₂ : ∀ n → half₁ (twice n) ≡ n
  half₁-+₂ = <′-rec _ λ
    { zero          _   → refl
    ; (suc zero)    _   → refl
    ; (suc (suc n)) rec →
        cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
    }

  half₂-+₂ : ∀ n → half₂ (twice n) ≡ n
  half₂-+₂ = <′-rec _ λ
    { zero          _   → refl
    ; (suc zero)    _   → refl
    ; (suc (suc n)) rec →
        cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
    }

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

rec-builder      = recBuilder
{-# WARNING_ON_USAGE rec-builder
"Warning: rec-builder was deprecated in v0.15.
Please use recBuilder instead."
#-}
cRec-builder     = cRecBuilder
{-# WARNING_ON_USAGE cRec-builder
"Warning: cRec-builder was deprecated in v0.15.
Please use cRecBuilder instead."
#-}
<′-rec-builder   = <′-recBuilder
{-# WARNING_ON_USAGE <′-rec-builder
"Warning: <′-rec-builder was deprecated in v0.15.
Please use <′-recBuilder instead."
#-}
<-rec-builder    = <-recBuilder
{-# WARNING_ON_USAGE <-rec-builder
"Warning: <-rec-builder was deprecated in v0.15.
Please use <-recBuilder instead."
#-}
≺-rec-builder    = ≺-recBuilder
{-# WARNING_ON_USAGE ≺-rec-builder
"Warning: ≺-rec-builder was deprecated in v0.15.
Please use ≺-recBuilder instead."
#-}
<′-well-founded  = <′-wellFounded
{-# WARNING_ON_USAGE <′-well-founded
"Warning: <′-well-founded was deprecated in v0.15.
Please use <′-wellFounded instead."
#-}
<′-well-founded′ = <′-wellFounded′
{-# WARNING_ON_USAGE <′-well-founded′
"Warning: <′-well-founded′ was deprecated in v0.15.
Please use <′-wellFounded′ instead."
#-}
<-well-founded   = <-wellFounded
{-# WARNING_ON_USAGE <-well-founded
"Warning: <-well-founded was deprecated in v0.15.
Please use <-wellFounded instead."
#-}
≺-well-founded   = ≺-wellFounded
{-# WARNING_ON_USAGE ≺-well-founded
"Warning: ≺-well-founded was deprecated in v0.15.
Please use ≺-wellFounded instead."
#-}


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

open import Categories.Category

-- Reasoning facilities about morphism equivalences (not necessarily 'squares')

module Categories.Morphism.Reasoning {o ℓ e} (C : Category o ℓ e) where

open import Categories.Morphism.Reasoning.Core C public
open import Categories.Morphism.Reasoning.Iso C public

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

module WithoutK where

open import Common.Level

-- Propositional equality.

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

-- The J rule.

J : {A : Set} (P : {x y : A} → x ≡ y → Set) →
    (∀ x → P (refl x)) →
    ∀ {x y} (x≡y : x ≡ y) → P x≡y
J P p (refl x) = p x

-- Christine Paulin-Mohring's version of the J rule.

J′ : {A : Set} {x : A} (P : {y : A} → x ≡ y → Set) →
     P (refl x) →
     ∀ {y} (x≡y : x ≡ y) → P x≡y
J′ P p (refl x) = p

-- A variant of _≡_.

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

-- We normalise before checking index well-formedness.

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x _ = x

id : {A : Set} {x y : A} → const x y ≡′ const y x → x ≡′ y
id refl = refl

-- We can handle more complicated indices as well.

data ⊥ : Set where

data Bool : Set where
  true false : Bool

true≢false : true ≡ false → ⊥
true≢false ()

data D : Set where
  c₀ : D
  c₂ : (i₁ i₂ : D) → D

f : ∀ {x y z} → x ≡ y → c₂ y c₀ ≡ c₂ c₀ z → x ≡ z
f x≡y (refl .(c₂ c₀ c₀)) = x≡y

-- The indices can contain literals.

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}

g : 2 ≡ 3 → 3 ≡ 5
g ()

h : ∀ {n} → 2 ≡ suc n → n ≡ 1
h (refl .2) = refl _


text:
------------------------------------------------------------------------------
-- Testing Agda internal term: @Pi _ (NoAbs _ _)@
------------------------------------------------------------------------------

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

-- After the patch
--
-- Wed Sep 21 04:50:43 COT 2011  ulfn@chalmers.se
--   * got rid of the Fun constructor in internal syntax (using Pi _ (NoAbs _ _) instead)
--
-- Agda is using @Pi _ (NoAbs _ _)@ for the non-dependent
-- functions. We test some translations of non-dependent functions.

module Agda.InternalTerms.PiNoAbsTerm where

postulate
  _↔_ : Set → Set → Set
  D   : Set
  A   : Set

postulate foo₁ : ((x : D) → A) → A
{-# ATP prove foo₁ #-}

postulate foo₂ : A → ((x : D) → A)
{-# ATP prove foo₂ #-}

postulate foo₃ : ((x : D) → A) ↔ A
{-# ATP prove foo₃ #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Everything where

import Generics.Prelude
import Generics.Telescope
import Generics.Telescope.Equality
import Generics.Desc
import Generics.All
import Generics.HasDesc
import Generics.Accessibility
import Generics.Helpers
import Generics.Reflection

import Generics.Mu
import Generics.Mu.All
import Generics.Mu.Elim
import Generics.Mu.Fold
import Generics.Mu.Conversion

import Generics.Constructions.Case
import Generics.Constructions.Cong
import Generics.Constructions.DecEq
import Generics.Constructions.Elim
import Generics.Constructions.Fold
import Generics.Constructions.Mu
import Generics.Constructions.Recursion
import Generics.Constructions.Show

import Generics

-- Work In Progress
---------------------------------

-- import Generics.Mu.NoConfusion
-- import Generics.Constructions.Injective

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
------------------------------------------------------------------------------
-- Fair properties
------------------------------------------------------------------------------

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

module FOTC.Program.ABP.Fair.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.Stream.Type
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the Fair
-- predicate is also a pre-fixed point of the functional FairF, i.e.
--
-- FairF Fair ≤ Fair (see FOTC.Program.ABP.Fair).
Fair-in : ∀ {os} → ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ Fair os' →
          Fair os
Fair-in h = Fair-coind A h' h
  where
  A : D → Set
  A os = ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ Fair os'

  h' : ∀ {os} → A os → ∃[ ft ] ∃[ os' ] F*T ft ∧ os ≡ ft ++ os' ∧ A os'
  h' (ft , os' , FTft , prf , Fos') = ft , os' , FTft , prf , Fair-out Fos'

head-tail-Fair : ∀ {os} → Fair os → os ≡ T ∷ tail₁ os ∨ os ≡ F ∷ tail₁ os
head-tail-Fair {os} Fos with Fair-out Fos
... | .(T ∷ []) , os' , f*tnil , h , Fos' = inj₁ prf₃
  where
  prf₁ : os ≡ T ∷ [] ++ os'
  prf₁ = os              ≡⟨ h ⟩
         (T ∷ []) ++ os' ≡⟨ ++-∷ T [] os' ⟩
         T ∷ [] ++ os'   ∎

  prf₂ : tail₁ os ≡ [] ++ os'
  prf₂ = tail₁ os              ≡⟨ tailCong prf₁ ⟩
         tail₁ (T ∷ [] ++ os') ≡⟨ tail-∷ T ([] ++ os') ⟩
         [] ++ os'             ∎

  prf₃ : os ≡ T ∷ tail₁ os
  prf₃ = os             ≡⟨ prf₁ ⟩
         T ∷ [] ++ os'  ≡⟨ ∷-rightCong (sym prf₂) ⟩
         T ∷ tail₁ os   ∎

... | .(F ∷ ft) , os' , f*tcons {ft} FTft , h , Fos' =
  inj₂ prf₃
  where
  prf₁ : os ≡ F ∷ ft ++ os'
  prf₁ = os              ≡⟨ h ⟩
         (F ∷ ft) ++ os' ≡⟨ ++-∷ F ft os' ⟩
         F ∷ ft ++ os'   ∎

  prf₂ : tail₁ os ≡ ft ++ os'
  prf₂ = tail₁ os              ≡⟨ tailCong prf₁ ⟩
         tail₁ (F ∷ ft ++ os') ≡⟨ tail-∷ F (ft ++ os') ⟩
         ft ++ os'             ∎

  prf₃ : os ≡ F ∷ tail₁ os
  prf₃ = os             ≡⟨ prf₁ ⟩
         F ∷ ft ++ os'  ≡⟨ ∷-rightCong (sym prf₂) ⟩
         F ∷ tail₁ os   ∎

tail-Fair : ∀ {os} → Fair os → Fair (tail₁ os)
tail-Fair {os} Fos with Fair-out Fos
... | .(T ∷ []) , os' , f*tnil , h , Fos' =
  subst Fair (sym prf₂) Fos'
  where
  prf₁ : os ≡ T ∷ os'
  prf₁ = os              ≡⟨ h ⟩
         (T ∷ []) ++ os' ≡⟨ ++-∷ T [] os' ⟩
         T ∷ [] ++ os'   ≡⟨ ∷-rightCong (++-leftIdentity os') ⟩
         T ∷ os'         ∎

  prf₂ : tail₁ os ≡ os'
  prf₂ = tail₁ os        ≡⟨ tailCong prf₁ ⟩
         tail₁ (T ∷ os') ≡⟨ tail-∷ T os' ⟩
         os'             ∎

... | .(F ∷ ft) , os' , f*tcons {ft} FTft , h , Fos' =
    subst Fair (sym prf₂) (Fair-in (ft , os' , FTft , refl , Fos'))
  where
  prf₁ : os ≡ F ∷ ft ++ os'
  prf₁ = os              ≡⟨ h ⟩
         (F ∷ ft) ++ os' ≡⟨ ++-∷ F ft os' ⟩
         F ∷ ft ++ os'   ∎

  prf₂ : tail₁ os ≡ ft ++ os'
  prf₂ = tail₁ os              ≡⟨ tailCong prf₁ ⟩
         tail₁ (F ∷ ft ++ os') ≡⟨ tail-∷ F (ft ++ os') ⟩
         ft ++ os'             ∎

Fair→Stream : ∀ {os} → Fair os → Stream os
Fair→Stream Fos = Stream-coind A h Fos
  where
  A : D → Set
  A xs = Fair xs

  h : ∀ {os} → A os → ∃[ o' ] ∃[ os' ] os ≡ o' ∷ os' ∧ A os'
  h {os} As with head-tail-Fair As
  ... | inj₁ prf = T , tail₁ os , prf , tail-Fair As
  ... | inj₂ prf = F , tail₁ os , prf , tail-Fair As

F*T→List : ∀ {xs} → F*T xs → List xs
F*T→List f*tnil              = lcons T lnil
F*T→List (f*tcons {ft} FTft) = lcons F (F*T→List FTft)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Table-related properties
------------------------------------------------------------------------

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

module Data.Table.Properties where

open import Data.Table
open import Data.Table.Relation.Binary.Equality

open import Data.Bool using (true; false; if_then_else_)
open import Data.Nat using (zero; suc)
open import Data.Empty using (⊥-elim)
open import Data.Fin using (Fin; suc; zero; _≟_; punchIn)
import Data.Fin.Properties as FP
open import Data.Fin.Permutation as Perm using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
open import Data.List as L using (List; _∷_; [])
open import Data.List.Relation.Unary.Any using (here; there; index)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Product as Product using (Σ; ∃; _,_; proj₁; proj₂)
open import Data.Vec as V using (Vec; _∷_; [])
import Data.Vec.Properties as VP
open import Function using (_∘_; flip)
open import Function.Inverse using (Inverse)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; sym; cong)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)

------------------------------------------------------------------------
-- select

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

  -- Selecting from any table is the same as selecting from a constant table.

  select-const : ∀ {n} (z : A) (i : Fin n) t →
                 select z i t ≗ select z i (replicate (lookup t i))
  select-const z i t j with j ≟ i
  ... | yes _ = refl
  ... | no  _ = refl

  -- Selecting an element from a table then looking it up is the same as looking
  -- up the index in the original table

  select-lookup : ∀ {n x i} (t : Table A n) →
                  lookup (select x i t) i ≡ lookup t i
  select-lookup {i = i} t with i ≟ i
  ... | yes _  = refl
  ... | no i≢i = contradiction refl i≢i

  -- Selecting an element from a table then removing the same element produces a
  -- constant table

  select-remove : ∀ {n x} i (t : Table A (suc n)) →
                  remove i (select x i t) ≗ replicate {n = n} x
  select-remove i t j with punchIn i j ≟ i
  ... | yes p = contradiction p (FP.punchInᵢ≢i _ _)
  ... | no ¬p = refl

------------------------------------------------------------------------
-- permute

  -- Removing an index 'i' from a table permuted with 'π' is the same as
  -- removing the element, then permuting with 'π' minus 'i'.

  remove-permute : ∀ {m n} (π : Permutation (suc m) (suc n))
                   i (t : Table A (suc n)) →
                   remove (π ⟨$⟩ˡ i) (permute π t)
                   ≗ permute (Perm.remove (π ⟨$⟩ˡ i) π) (remove i t)
  remove-permute π i t j = P.cong (lookup t) (Perm.punchIn-permute′ π i j)

------------------------------------------------------------------------
-- fromList

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

  fromList-∈ : ∀ {xs : List A} (i : Fin (L.length xs)) → lookup (fromList xs) i ∈ xs
  fromList-∈ {[]}     ()
  fromList-∈ {x ∷ xs} zero    = here refl
  fromList-∈ {x ∷ xs} (suc i) = there (fromList-∈ i)

  index-fromList-∈ : ∀ {xs i} → index (fromList-∈ {xs} i) ≡ i
  index-fromList-∈ {[]}     {()}
  index-fromList-∈ {x ∷ xs} {zero}  = refl
  index-fromList-∈ {x ∷ xs} {suc i} = cong suc index-fromList-∈

  fromList-index : ∀ {xs} {x : A} (x∈xs : x ∈ xs) → lookup (fromList xs) (index x∈xs) ≡ x
  fromList-index (here px)    = sym px
  fromList-index (there x∈xs) = fromList-index x∈xs

------------------------------------------------------------------------
-- There exists an isomorphism between tables and vectors.

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

  ↔Vec : Inverse (≡-setoid A n) (P.setoid (Vec A n))
  ↔Vec = record
    { to = record { _⟨$⟩_ = toVec ; cong = VP.tabulate-cong }
    ; from = P.→-to-⟶ fromVec
    ; inverse-of = record
      { left-inverse-of  = VP.lookup∘tabulate ∘ lookup
      ; right-inverse-of = VP.tabulate∘lookup
      }
    }

------------------------------------------------------------------------
-- Other

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

  lookup∈ : ∀ {xs : List A} (i : Fin (L.length xs)) → ∃ λ x → x ∈ xs
  lookup∈ i = _ , fromList-∈ i


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

open import HoTT
open import homotopy.FinWedge
open import homotopy.Bouquet
open import groups.SphereEndomorphism
open import cohomology.Theory

module cohomology.RephraseSubFinCoboundary (OT : OrdinaryTheory lzero) where

open OrdinaryTheory OT
open import cohomology.SphereEndomorphism cohomology-theory
open import cohomology.Sphere OT
open import cohomology.SubFinBouquet OT

abstract
  rephrase-in-degree : ∀ n {I : ℕ} {JA JB : Type₀}
    (JB-ac : has-choice 0 JB lzero)
    (JB-dec : has-dec-eq JB)
    {J} (p : Fin J ≃ Coprod JA JB)
    (f : ⊙FinBouquet I (S n) ⊙→ ⊙Susp (⊙Bouquet JB n)) g
    → GroupIso.f (C-FinBouquet-diag (S n) I)
        (CEl-fmap (ℕ-to-ℤ (S n)) f
          (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Bouquet JB n))
            (GroupIso.g (C-SubFinBouquet-diag n JB-ac (–> p)) g)))
    ∼ λ <I → Group.subsum-r (C2 0) (–> p)
          (λ b → Group.exp (C2 0) (g b) (⊙SphereS-endo-degree n (⊙Susp-fmap (⊙bwproj JB-dec b) ⊙∘ f ⊙∘ ⊙fwin <I)))
  rephrase-in-degree n {I} {JA} {JB} JB-ac JB-dec {J} p f g <I =
    GroupIso.f (C-FinBouquet-diag (S n) I)
      (CEl-fmap (ℕ-to-ℤ (S n)) f
        (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Bouquet JB n))
          (GroupIso.g (C-SubFinBouquet-diag n JB-ac (–> p)) g)))
      <I
      =⟨ ap
          (λ g → GroupIso.f (C-FinBouquet-diag (S n) I)
            (CEl-fmap (ℕ-to-ℤ (S n)) f
              (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Bouquet JB n))
                g)) <I)
          (inverse-C-SubFinBouquet-diag-β n JB-ac JB-dec p g) ⟩
    GroupIso.f (C-FinBouquet-diag (S n) I)
      (CEl-fmap (ℕ-to-ℤ (S n)) f
        (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Bouquet JB n))
          (Group.subsum-r (C (ℕ-to-ℤ n) (⊙Bouquet JB n)) (–> p)
            (λ b → CEl-fmap (ℕ-to-ℤ n) (⊙bwproj JB-dec b)
              (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                (GroupIso.g (C-Sphere-diag n) (g b)))))))
      <I
      =⟨ ap (λ g → GroupIso.f (C-FinBouquet-diag (S n) I) g <I) $
          GroupHom.pres-subsum-r
            (C-fmap (ℕ-to-ℤ (S n)) f ∘ᴳ GroupIso.g-hom (C-Susp (ℕ-to-ℤ n) (⊙Bouquet JB n)))
            (–> p)
            (λ b → CEl-fmap (ℕ-to-ℤ n) (⊙bwproj JB-dec b)
              (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                (GroupIso.g (C-Sphere-diag n) (g b)))) ⟩
    GroupIso.f (C-FinBouquet-diag (S n) I)
      (Group.subsum-r (C (ℕ-to-ℤ (S n)) (⊙FinBouquet I (S n))) (–> p)
        (λ b → CEl-fmap (ℕ-to-ℤ (S n)) f
          (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Bouquet JB n))
            (CEl-fmap (ℕ-to-ℤ n) (⊙bwproj JB-dec b)
              (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                (GroupIso.g (C-Sphere-diag n) (g b)))))))
      <I
      =⟨ ap
          (λ f → GroupIso.f (C-FinBouquet-diag (S n) I)
            (Group.subsum-r (C (ℕ-to-ℤ (S n)) (⊙FinBouquet I (S n))) (–> p) f) <I)
          (λ= λ b → ap (CEl-fmap (ℕ-to-ℤ (S n)) f) $
            C-Susp-fmap' (ℕ-to-ℤ n) (⊙bwproj JB-dec b) □$ᴳ
              CEl-fmap (ℕ-to-ℤ n) ⊙lift (GroupIso.g (C-Sphere-diag n) (g b))) ⟩
    GroupIso.f (C-FinBouquet-diag (S n) I)
      (Group.subsum-r (C (ℕ-to-ℤ (S n)) (⊙FinBouquet I (S n))) (–> p)
        (λ b → CEl-fmap (ℕ-to-ℤ (S n)) f
          (CEl-fmap (ℕ-to-ℤ (S n)) (⊙Susp-fmap (⊙bwproj JB-dec b))
            (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
              (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                (GroupIso.g (C-Sphere-diag n) (g b)))))))
      <I
      =⟨ C-FinBouquet-diag-β (S n) I
          (Group.subsum-r (C (ℕ-to-ℤ (S n)) (⊙FinBouquet I (S n))) (–> p)
            (λ b → CEl-fmap (ℕ-to-ℤ (S n)) f
              (CEl-fmap (ℕ-to-ℤ (S n)) (⊙Susp-fmap (⊙bwproj JB-dec b))
                (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
                  (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                    (GroupIso.g (C-Sphere-diag n) (g b)))))))
          <I ⟩
    GroupIso.f (C-Sphere-diag (S n))
      (CEl-fmap (ℕ-to-ℤ (S n)) ⊙lower
        (CEl-fmap (ℕ-to-ℤ (S n)) (⊙fwin <I)
          (Group.subsum-r (C (ℕ-to-ℤ (S n)) (⊙FinBouquet I (S n))) (–> p)
            (λ b → CEl-fmap (ℕ-to-ℤ (S n)) f
              (CEl-fmap (ℕ-to-ℤ (S n)) (⊙Susp-fmap (⊙bwproj JB-dec b))
                (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
                  (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                    (GroupIso.g (C-Sphere-diag n) (g b)))))))))
      =⟨ GroupHom.pres-subsum-r
          (  GroupIso.f-hom (C-Sphere-diag (S n))
          ∘ᴳ C-fmap (ℕ-to-ℤ (S n)) ⊙lower
          ∘ᴳ C-fmap (ℕ-to-ℤ (S n)) (⊙fwin <I))
          (–> p)
          (λ b → CEl-fmap (ℕ-to-ℤ (S n)) f
            (CEl-fmap (ℕ-to-ℤ (S n)) (⊙Susp-fmap (⊙bwproj JB-dec b))
              (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
                (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                  (GroupIso.g (C-Sphere-diag n) (g b)))))) ⟩
    Group.subsum-r (C2 0) (–> p)
      (λ b → GroupIso.f (C-Sphere-diag (S n))
        (CEl-fmap (ℕ-to-ℤ (S n)) ⊙lower
          (CEl-fmap (ℕ-to-ℤ (S n)) (⊙fwin <I)
            (CEl-fmap (ℕ-to-ℤ (S n)) f
              (CEl-fmap (ℕ-to-ℤ (S n)) (⊙Susp-fmap (⊙bwproj JB-dec b))
                (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
                  (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                    (GroupIso.g (C-Sphere-diag n) (g b)))))))))
      =⟨ ap (Group.subsum-r (C2 0) (–> p))
          (λ= λ b → ap (GroupIso.f (C-Sphere-diag (S n)) ∘ CEl-fmap (ℕ-to-ℤ (S n)) ⊙lower) $
              ∘-CEl-fmap (ℕ-to-ℤ (S n)) (⊙fwin <I) f _
            ∙ ∘-CEl-fmap (ℕ-to-ℤ (S n)) (f ⊙∘ ⊙fwin <I) (⊙Susp-fmap (⊙bwproj JB-dec b)) _
            ∙ CEl-fmap-⊙Sphere-endo-η (ℕ-to-ℤ (S n)) n
                (⊙Susp-fmap (⊙bwproj JB-dec b) ⊙∘ f ⊙∘ ⊙fwin <I)
                (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
                  (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                    (GroupIso.g (C-Sphere-diag n) (g b))))) ⟩
    Group.subsum-r (C2 0) (–> p)
      (λ b → GroupIso.f (C-Sphere-diag (S n))
        (CEl-fmap (ℕ-to-ℤ (S n)) ⊙lower
          (Group.exp (C (ℕ-to-ℤ (S n)) (⊙Sphere (S n)))
            (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
              (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                (GroupIso.g (C-Sphere-diag n) (g b))))
            (⊙SphereS-endo-degree n (⊙Susp-fmap (⊙bwproj JB-dec b) ⊙∘ f ⊙∘ ⊙fwin <I)))))
      =⟨ ap (Group.subsum-r (C2 0) (–> p))
          (λ= λ b →
            GroupHom.pres-exp
              (GroupIso.f-hom (C-Sphere-diag (S n)) ∘ᴳ C-fmap (ℕ-to-ℤ (S n)) ⊙lower)
              (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
                (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                  (GroupIso.g (C-Sphere-diag n) (g b))))
              (⊙SphereS-endo-degree n (⊙Susp-fmap (⊙bwproj JB-dec b) ⊙∘ f ⊙∘ ⊙fwin <I))) ⟩
    Group.subsum-r (C2 0) (–> p)
      (λ b → Group.exp (C2 0)
        (GroupIso.f (C-Sphere-diag n)
          (–> (CEl-Susp (ℕ-to-ℤ n) (⊙Lift (⊙Sphere n)))
            (CEl-fmap (ℕ-to-ℤ (S n)) (⊙lift {j = lzero} ⊙∘ ⊙Susp-fmap {Y = ⊙Sphere n} ⊙lower)
              (CEl-fmap (ℕ-to-ℤ (S n)) ⊙lower
                (<– (CEl-Susp (ℕ-to-ℤ n) (⊙Sphere n))
                  (CEl-fmap (ℕ-to-ℤ n) ⊙lift
                    (GroupIso.g (C-Sphere-diag n) (g b))))))))
        (⊙SphereS-endo-degree n (⊙Susp-fmap (⊙bwproj JB-dec b) ⊙∘ f ⊙∘ ⊙fwin <I)))
      =⟨ ap (Group.subsum-r (C2 0) (–> p))
          (λ= λ b → ap (λ g → Group.exp (C2 0) g (⊙SphereS-endo-degree n (⊙Susp-fmap (⊙bwproj JB-dec b) ⊙∘ f ⊙∘ ⊙fwin <I))) $
            ap (GroupIso.f (C-Sphere-diag n) ∘ –> (CEl-Susp (ℕ-to-ℤ n) (⊙Lift (⊙Sphere n))))
              ( CEl-fmap-∘ (ℕ-to-ℤ (S n)) ⊙lift (⊙Susp-fmap {Y = ⊙Sphere n} ⊙lower) _
              ∙ ap (CEl-fmap (ℕ-to-ℤ (S n)) (⊙Susp-fmap {Y = ⊙Sphere n} ⊙lower))
                  ( ∘-CEl-fmap (ℕ-to-ℤ (S n)) ⊙lift ⊙lower _
                  ∙ CEl-fmap-idf (ℕ-to-ℤ (S n)) _))
            ∙ ap (GroupIso.f (C-Sphere-diag n))
                ( (C-Susp-fmap (ℕ-to-ℤ n) ⊙lower □$ᴳ _)
                ∙ ap (CEl-fmap (ℕ-to-ℤ n) ⊙lower) (GroupIso.f-g (C-Susp (ℕ-to-ℤ n) (⊙Sphere n)) _)
                ∙ ∘-CEl-fmap (ℕ-to-ℤ n) ⊙lower ⊙lift _
                ∙ CEl-fmap-idf (ℕ-to-ℤ n) _)
            ∙ GroupIso.f-g (C-Sphere-diag n) (g b)) ⟩
    Group.subsum-r (C2 0) (–> p)
      (λ b → Group.exp (C2 0) (g b)
        (⊙SphereS-endo-degree n (⊙Susp-fmap (⊙bwproj JB-dec b) ⊙∘ f ⊙∘ ⊙fwin <I)))
      =∎

  {- the version specialzied to [Fin J]. -}
  rephrase-in-degree' : ∀ n {I J : ℕ} (f : ⊙FinBouquet I (S n) ⊙→ ⊙Susp (⊙FinBouquet J n)) g
    → GroupIso.f (C-FinBouquet-diag (S n) I)
        (CEl-fmap (ℕ-to-ℤ (S n)) f
          (<– (CEl-Susp (ℕ-to-ℤ n) (⊙FinBouquet J n))
            (GroupIso.g (C-FinBouquet-diag n J) g)))
    ∼ λ <I → Group.sum (C2 0)
          (λ <J → Group.exp (C2 0) (g <J) (⊙SphereS-endo-degree n (⊙Susp-fmap (⊙fwproj <J) ⊙∘ f ⊙∘ ⊙fwin <I)))
  rephrase-in-degree' n {I} {J} f g =
    rephrase-in-degree n {I} {JA = Empty} {JB = Fin J}
      (Fin-has-choice 0 lzero) Fin-has-dec-eq (⊔₁-Empty (Fin J) ⁻¹) f g

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- Pointwise products of binary relations
------------------------------------------------------------------------

module Relation.Binary.Product.Pointwise where

open import Data.Function
open import Data.Product
open import Data.Sum
open import Relation.Nullary.Product
open import Relation.Binary

private
 module Dummy {a₁ a₂ : Set} where

  infixr 2 _×-Rel_

  _×-Rel_ : Rel a₁ → Rel a₂ → Rel (a₁ × a₂)
  ∼₁ ×-Rel ∼₂ = (∼₁ on₁ proj₁) -×- (∼₂ on₁ proj₂)

  -- Some properties which are preserved by ×-Rel (under certain
  -- assumptions).

  _×-reflexive_ : ∀ {≈₁ ∼₁ ≈₂ ∼₂} →
                  ≈₁ ⇒ ∼₁ → ≈₂ ⇒ ∼₂ → (≈₁ ×-Rel ≈₂) ⇒ (∼₁ ×-Rel ∼₂)
  refl₁ ×-reflexive refl₂ = λ x≈y →
    (refl₁ (proj₁ x≈y) , refl₂ (proj₂ x≈y))

  _×-refl_ : ∀ {∼₁ ∼₂} →
             Reflexive ∼₁ → Reflexive ∼₂ → Reflexive (∼₁ ×-Rel ∼₂)
  refl₁ ×-refl refl₂ = (refl₁ , refl₂)

  ×-irreflexive₁ :
    ∀ {≈₁ <₁ ≈₂ <₂} →
    Irreflexive ≈₁ <₁ → Irreflexive (≈₁ ×-Rel ≈₂) (<₁ ×-Rel <₂)
  ×-irreflexive₁ ir = λ x≈y x<y → ir (proj₁ x≈y) (proj₁ x<y)

  ×-irreflexive₂ :
    ∀ {≈₁ <₁ ≈₂ <₂} →
    Irreflexive ≈₂ <₂ → Irreflexive (≈₁ ×-Rel ≈₂) (<₁ ×-Rel <₂)
  ×-irreflexive₂ ir = λ x≈y x<y → ir (proj₂ x≈y) (proj₂ x<y)

  _×-symmetric_ : ∀ {∼₁ ∼₂} →
                  Symmetric ∼₁ → Symmetric ∼₂ → Symmetric (∼₁ ×-Rel ∼₂)
  sym₁ ×-symmetric sym₂ = λ x∼y → sym₁ (proj₁ x∼y) , sym₂ (proj₂ x∼y)

  _×-transitive_ : ∀ {∼₁ ∼₂} →
                   Transitive ∼₁ → Transitive ∼₂ →
                   Transitive (∼₁ ×-Rel ∼₂)
  trans₁ ×-transitive trans₂ = λ x∼y y∼z →
    trans₁ (proj₁ x∼y) (proj₁ y∼z) ,
    trans₂ (proj₂ x∼y) (proj₂ y∼z)

  _×-antisymmetric_ : ∀ {≈₁ ≤₁ ≈₂ ≤₂} →
                      Antisymmetric ≈₁ ≤₁ → Antisymmetric ≈₂ ≤₂ →
                      Antisymmetric (≈₁ ×-Rel ≈₂) (≤₁ ×-Rel ≤₂)
  antisym₁ ×-antisymmetric antisym₂ = λ x≤y y≤x →
    ( antisym₁ (proj₁ x≤y) (proj₁ y≤x)
    , antisym₂ (proj₂ x≤y) (proj₂ y≤x) )

  ×-asymmetric₁ : ∀ {<₁ ∼₂} → Asymmetric <₁ → Asymmetric (<₁ ×-Rel ∼₂)
  ×-asymmetric₁ asym₁ = λ x<y y<x → asym₁ (proj₁ x<y) (proj₁ y<x)

  ×-asymmetric₂ : ∀ {∼₁ <₂} → Asymmetric <₂ → Asymmetric (∼₁ ×-Rel <₂)
  ×-asymmetric₂ asym₂ = λ x<y y<x → asym₂ (proj₂ x<y) (proj₂ y<x)

  _×-≈-respects₂_ : ∀ {≈₁ ∼₁ ≈₂ ∼₂} →
                    ∼₁ Respects₂ ≈₁ → ∼₂ Respects₂ ≈₂ →
                    (∼₁ ×-Rel ∼₂) Respects₂ (≈₁ ×-Rel ≈₂)
  _×-≈-respects₂_ {≈₁ = ≈₁} {∼₁ = ∼₁} {≈₂ = ≈₂} {∼₂ = ∼₂}
                  resp₁ resp₂ =
    (λ {x y z} → resp¹ {x} {y} {z}) ,
    (λ {x y z} → resp² {x} {y} {z})
    where
    ∼ = ∼₁ ×-Rel ∼₂

    resp¹ : ∀ {x} → (∼ x) Respects (≈₁ ×-Rel ≈₂)
    resp¹ y≈y' x∼y = proj₁ resp₁ (proj₁ y≈y') (proj₁ x∼y) ,
                     proj₁ resp₂ (proj₂ y≈y') (proj₂ x∼y)

    resp² : ∀ {y} → (flip₁ ∼ y) Respects (≈₁ ×-Rel ≈₂)
    resp² x≈x' x∼y = proj₂ resp₁ (proj₁ x≈x') (proj₁ x∼y) ,
                     proj₂ resp₂ (proj₂ x≈x') (proj₂ x∼y)

  ×-total : ∀ {∼₁ ∼₂} →
            Symmetric ∼₁ → Total ∼₁ → Total ∼₂ → Total (∼₁ ×-Rel ∼₂)
  ×-total {∼₁ = ∼₁} {∼₂ = ∼₂} sym₁ total₁ total₂ = total
    where
    total : Total (∼₁ ×-Rel ∼₂)
    total x y with total₁ (proj₁ x) (proj₁ y)
                 | total₂ (proj₂ x) (proj₂ y)
    ... | inj₁ x₁∼y₁ | inj₁ x₂∼y₂ = inj₁ (     x₁∼y₁ , x₂∼y₂)
    ... | inj₁ x₁∼y₁ | inj₂ y₂∼x₂ = inj₂ (sym₁ x₁∼y₁ , y₂∼x₂)
    ... | inj₂ y₁∼x₁ | inj₂ y₂∼x₂ = inj₂ (     y₁∼x₁ , y₂∼x₂)
    ... | inj₂ y₁∼x₁ | inj₁ x₂∼y₂ = inj₁ (sym₁ y₁∼x₁ , x₂∼y₂)

  _×-decidable_ : ∀ {∼₁ ∼₂} →
                  Decidable ∼₁ → Decidable ∼₂ → Decidable (∼₁ ×-Rel ∼₂)
  dec₁ ×-decidable dec₂ = λ x y →
    dec₁ (proj₁ x) (proj₁ y)
      ×-dec
    dec₂ (proj₂ x) (proj₂ y)

  -- Some collections of properties which are preserved by ×-Rel.

  _×-isEquivalence_ : ∀ {≈₁ ≈₂} →
                      IsEquivalence ≈₁ → IsEquivalence ≈₂ →
                      IsEquivalence (≈₁ ×-Rel ≈₂)
  _×-isEquivalence_ {≈₁ = ≈₁} {≈₂ = ≈₂} eq₁ eq₂ = record
    { refl  = λ {x} →
              _×-refl_        {∼₁ = ≈₁} {∼₂ = ≈₂}
                              (refl  eq₁) (refl  eq₂) {x}
    ; sym   = λ {x y} →
              _×-symmetric_   {∼₁ = ≈₁} {∼₂ = ≈₂}
                              (sym   eq₁) (sym   eq₂) {x} {y}
    ; trans = λ {x y z} →
              _×-transitive_  {∼₁ = ≈₁} {∼₂ = ≈₂}
                              (trans eq₁) (trans eq₂) {x} {y} {z}
    }
    where open IsEquivalence

  _×-isPreorder_ : ∀ {≈₁ ∼₁ ≈₂ ∼₂} →
                   IsPreorder ≈₁ ∼₁ → IsPreorder ≈₂ ∼₂ →
                   IsPreorder (≈₁ ×-Rel ≈₂) (∼₁ ×-Rel ∼₂)
  _×-isPreorder_ {∼₁ = ∼₁} {∼₂ = ∼₂} pre₁ pre₂ = record
    { isEquivalence = isEquivalence pre₁ ×-isEquivalence
                      isEquivalence pre₂
    ; reflexive     = λ {x y} →
                      _×-reflexive_  {∼₁ = ∼₁} {∼₂ = ∼₂}
                                     (reflexive pre₁) (reflexive pre₂)
                                     {x} {y}
    ; trans         = λ {x y z} →
                      _×-transitive_ {∼₁ = ∼₁} {∼₂ = ∼₂}
                                     (trans pre₁) (trans pre₂)
                                     {x} {y} {z}
    ; ∼-resp-≈      = ∼-resp-≈ pre₁ ×-≈-respects₂ ∼-resp-≈ pre₂
    }
    where open IsPreorder

  _×-isDecEquivalence_ : ∀ {≈₁ ≈₂} →
                         IsDecEquivalence ≈₁ → IsDecEquivalence ≈₂ →
                         IsDecEquivalence (≈₁ ×-Rel ≈₂)
  eq₁ ×-isDecEquivalence eq₂ = record
    { isEquivalence = isEquivalence eq₁ ×-isEquivalence
                      isEquivalence eq₂
    ; _≟_           = _≟_ eq₁ ×-decidable _≟_ eq₂
    }
    where open IsDecEquivalence

  _×-isPartialOrder_ : ∀ {≈₁ ≤₁ ≈₂ ≤₂} →
                       IsPartialOrder ≈₁ ≤₁ → IsPartialOrder ≈₂ ≤₂ →
                       IsPartialOrder (≈₁ ×-Rel ≈₂) (≤₁ ×-Rel ≤₂)
  _×-isPartialOrder_ {≤₁ = ≤₁} {≤₂ = ≤₂} po₁ po₂ = record
    { isPreorder = isPreorder po₁ ×-isPreorder isPreorder po₂
    ; antisym    = λ {x y} →
                   _×-antisymmetric_ {≤₁ = ≤₁} {≤₂ = ≤₂}
                                     (antisym po₁) (antisym po₂)
                                     {x} {y}
    }
    where open IsPartialOrder

  _×-isStrictPartialOrder_ :
    ∀ {≈₁ <₁ ≈₂ <₂} →
    IsStrictPartialOrder ≈₁ <₁ → IsStrictPartialOrder ≈₂ <₂ →
    IsStrictPartialOrder (≈₁ ×-Rel ≈₂) (<₁ ×-Rel <₂)
  _×-isStrictPartialOrder_ {<₁ = <₁} {≈₂ = ≈₂} {<₂ = <₂} spo₁ spo₂ =
    record
      { isEquivalence = isEquivalence spo₁ ×-isEquivalence
                        isEquivalence spo₂
      ; irrefl        = λ {x y} →
                        ×-irreflexive₁ {<₁ = <₁} {≈₂ = ≈₂} {<₂ = <₂}
                                       (irrefl spo₁) {x} {y}
      ; trans         = λ {x y z} →
                        _×-transitive_ {∼₁ = <₁} {∼₂ = <₂}
                                       (trans spo₁) (trans spo₂)
                                       {x} {y} {z}
      ; <-resp-≈      = <-resp-≈ spo₁ ×-≈-respects₂ <-resp-≈ spo₂
      }
    where open IsStrictPartialOrder

open Dummy public

-- "Packages" (e.g. setoids) can also be combined.

_×-preorder_ : Preorder → Preorder → Preorder
p₁ ×-preorder p₂ = record
  { isPreorder = isPreorder p₁ ×-isPreorder isPreorder p₂
  } where open Preorder

_×-setoid_ : Setoid → Setoid → Setoid
s₁ ×-setoid s₂ = record
  { isEquivalence = isEquivalence s₁ ×-isEquivalence isEquivalence s₂
  } where open Setoid

_×-decSetoid_ : DecSetoid → DecSetoid → DecSetoid
s₁ ×-decSetoid s₂ = record
  { isDecEquivalence = isDecEquivalence s₁ ×-isDecEquivalence
                       isDecEquivalence s₂
  } where open DecSetoid

_×-poset_ : Poset → Poset → Poset
s₁ ×-poset s₂ = record
  { isPartialOrder = isPartialOrder s₁ ×-isPartialOrder
                     isPartialOrder s₂
  } where open Poset

_×-strictPartialOrder_ :
  StrictPartialOrder → StrictPartialOrder → StrictPartialOrder
s₁ ×-strictPartialOrder s₂ = record
  { isStrictPartialOrder = isStrictPartialOrder s₁
                             ×-isStrictPartialOrder
                           isStrictPartialOrder s₂
  } where open StrictPartialOrder

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Common.Prelude hiding (tt)

instance
  tt : ⊤
  tt = record{}

NonZero : Nat → Set
NonZero zero    = ⊥
NonZero (suc _) = ⊤

pred′ : (n : Nat) {{_ : NonZero n}} → Nat
pred′ zero {{}}
pred′ (suc n) = n

test : (n : Nat) {{x y : NonZero n}} → Nat
test n = pred′ n


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Data.Empty using (⊥-elim)
open import Data.Product
open import Data.Sum

open import Relation.Nullary
open import Relation.Unary using (_∈_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym; subst)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_)

open import Function.Base using (case_of_)

open import Common

module Compliance {ℙ : Set} (message : Message ℙ)
  where

open import Action message
open import SessionType message
open import Transitions message
open import Session message
open import Progress message

data   Compliance : Session -> Set
record ∞Compliance (S : Session) : Set where
  constructor delay_
  coinductive
  field force : Compliance S
open ∞Compliance public

data Compliance where
  win#def : ∀{T S} (w : Win T) (def : Defined S) -> Compliance (T # S)
  out#inp : ∀{f g} (W : Witness f) (F : ∀{x} (!x : x ∈ dom f) -> ∞Compliance (f x .force # g x .force)) -> Compliance (out f # inp g)
  inp#out : ∀{f g} (W : Witness g) (F : ∀{x} (!x : x ∈ dom g) -> ∞Compliance (f x .force # g x .force)) -> Compliance (inp f # out g)

subject-reduction : ∀{S S'} -> Compliance S -> Reduction S S' -> ∞Compliance S'
force (subject-reduction (win#def (out U) def) (sync {I _} (out !x) s)) = ⊥-elim (U _ !x)
force (subject-reduction (inp#out _ F) (sync inp (out !x))) = F !x .force
force (subject-reduction (out#inp _ F) (sync (out !x) inp)) = F !x .force

subject-reduction* : ∀{S S'} -> Compliance S -> Reductions S S' -> ∞Compliance S'
force (subject-reduction* comp ε) = comp
subject-reduction* comp (red ◅ reds) = subject-reduction* (subject-reduction comp red .force) reds

compliance->progress : ∀{S} -> Compliance S -> Progress S
compliance->progress (win#def w def) = win#def w def
compliance->progress (out#inp W F) = out#inp W
compliance->progress (inp#out W F) = inp#out W

compliance->defined : ∀{T S} -> Compliance (T # S) -> Defined T × Defined S
compliance->defined (win#def (out _) def) = out , def
compliance->defined (out#inp _ _)         = out , inp
compliance->defined (inp#out _ _)         = inp , out

compliance-sound : ∀{S} -> Compliance S -> ComplianceS S
compliance-sound comp reds = progress-sound (compliance->progress (subject-reduction* comp reds .force))

compliance-complete : ∀{S} -> ComplianceS S -> ∞Compliance S
force (compliance-complete {T # S} spec) with spec ε
... | inj₁ (win#def w def) = win#def w def
... | inj₂ (_ , sync inp (out !x)) =
  inp#out (_ , !x) λ !x -> compliance-complete λ reds -> spec (sync inp (out !x) ◅ reds)
... | inj₂ (_ , sync (out !x) inp) =
  out#inp (_ , !x) λ !x -> compliance-complete λ reds -> spec (sync (out !x) inp ◅ reds)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module +-mono-< where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

open import Relations using (_<_; z<s; s<s)
open import <-trans using (<-trans)

+-monoʳ-< : ∀ (n p q : ℕ)
  → p < q
    -------------
  → n + p < n + q
+-monoʳ-< zero    p q p<q = p<q
+-monoʳ-< (suc n) p q p<q = s<s (+-monoʳ-< n p q p<q)

+-monoˡ-< : ∀ (m n p : ℕ)
  → m < n
    -------------
  → m + p < n + p
+-monoˡ-< m n p m<n rewrite +-comm m p | +-comm n p = +-monoʳ-< p m n m<n

+-mono-< : ∀ (m n p q : ℕ)
  → m < n
  → p < q
    -------------
  → m + p < n + q
+-mono-< m n p q m<n p<q = <-trans (+-monoˡ-< m n p m<n) (+-monoʳ-< n p q p<q)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Everything where

-- Basic cubical prelude
open import Cubical.Foundations.Prelude public

-- Definition of Identity types and definitions of J, funExt,
-- univalence and propositional truncation using Id instead of Path
open import Cubical.Foundations.Id
  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ )
  renaming ( _≃_           to EquivId
           ; EquivContr    to EquivContrId
           ; J             to JId
           ; ap            to apId
           ; equivFun      to equivFunId
           ; equivCtr      to equivCtrId
           ; fiber          to fiberId
           ; funExt        to funExtId
           ; isContr       to isContrId
           ; isProp        to isPropId
           ; isSet         to isSetId
           ; isEquiv       to isEquivId
           ; equivIsEquiv  to equivIsEquivId
           ; refl           to reflId
           ; ∥_∥           to propTruncId
           ; ∣_∣           to incId
           ; isPropIsContr to isPropIsContrId
           ; isPropIsEquiv to isPropIsEquivId
           )

open import Cubical.Foundations.GroupoidLaws public
open import Cubical.Foundations.CartesianKanOps public
open import Cubical.Foundations.Function public
open import Cubical.Foundations.Equiv public
open import Cubical.Foundations.Equiv.Properties public
open import Cubical.Foundations.PathSplitEquiv public
open import Cubical.Foundations.BiInvEquiv public
open import Cubical.Foundations.FunExtEquiv public
open import Cubical.Foundations.HLevels public
open import Cubical.Foundations.Path public
open import Cubical.Foundations.Transport public
open import Cubical.Foundations.Univalence public
open import Cubical.Foundations.UnivalenceId public
open import Cubical.Foundations.GroupoidLaws public
open import Cubical.Foundations.Isomorphism public
open import Cubical.Foundations.Logic
open import Cubical.Foundations.HoTT-UF

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Prelude.String where

open import Agda.Primitive
open import Prelude.Unit
open import Prelude.Char
open import Prelude.Bool
open import Prelude.Nat
open import Prelude.List
open import Prelude.Maybe
open import Prelude.Equality
open import Prelude.Equality.Unsafe
open import Prelude.Decidable
open import Prelude.Ord
open import Prelude.Function
open import Prelude.Monad
open import Prelude.Semiring

open import Agda.Builtin.String public
open import Agda.Builtin.FromString public

unpackString = primStringToList
packString   = primStringFromList

unpackString-inj : ∀ {x y} → unpackString x ≡ unpackString y → x ≡ y
unpackString-inj {x} p with unpackString x
unpackString-inj refl | ._ = unsafeEqual

infixr 5 _&_
_&_ = primStringAppend

parseNat : String → Maybe Nat
parseNat = parseNat′ ∘ unpackString
  where
    pDigit : Char → Maybe Nat
    pDigit c =
      if isDigit c then just (charToNat c - charToNat '0')
                   else nothing

    pNat : Nat → List Char → Maybe Nat
    pNat n [] = just n
    pNat n (c ∷ s) = pDigit c >>= λ d → pNat (n * 10 + d) s

    parseNat′ : List Char → Maybe Nat
    parseNat′ [] = nothing
    parseNat′ (c ∷ s) = pDigit c >>= λ d → pNat d s

-- Eq --

instance
  EqString : Eq String
  _==_ {{EqString}} x y with primStringEquality x y
  ... | true  = yes unsafeEqual
  ... | false = no  unsafeNotEqual

-- Ord --

instance
  OrdString : Ord String
  OrdString = OrdBy unpackString-inj

  OrdLawsString : Ord/Laws String
  OrdLawsString = OrdLawsBy unpackString-inj

-- Overloaded literals --

instance
  StringIsString : IsString String
  IsString.Constraint StringIsString _ = ⊤
  IsString.fromString StringIsString s = s

  ListIsString : IsString (List Char)
  IsString.Constraint ListIsString _ = ⊤
  IsString.fromString ListIsString s = unpackString s

-- Monoid --

instance
  open import Prelude.Monoid
  MonoidString : Monoid String
  mempty {{MonoidString}} = ""
  _<>_   {{MonoidString}} = primStringAppend

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-# OPTIONS --cubical-compatible #-}
module Common.IO where

open import Agda.Builtin.IO public
open import Common.Bool
open import Common.Char
open import Common.Nat
open import Common.String
open import Common.Unit
open import Common.Float

infixl 1 _>>=_

postulate
  return  : ∀ {a} {A : Set a} → A → IO A
  _>>=_   : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B

{-# COMPILE GHC return = \_ _ -> return #-}
{-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-}
{-# COMPILE UHC return = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
{-# COMPILE UHC _>>=_ = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
{-# COMPILE JS return =
    function(u0) { return function(u1) { return function(x) { return function(cb) { cb(x); }; }; }; } #-}
{-# COMPILE JS _>>=_ =
  function(u0) { return function(u1) { return function(u2) { return function(u3) {
    return function(x) { return function(y) { return function(cb) {
      x(function (xx) { y(xx)(cb); });
  }; }; };
  }; }; }; }
#-}

{-# FOREIGN GHC import qualified Data.Text.IO #-}

postulate
  putStr     : String -> IO Unit

{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE UHC putStr = UHC.Agda.Builtins.primPutStr #-}
{-# COMPILE JS putStr = function (x) { return function(cb) { process.stdout.write(x); cb(0); }; } #-}

printChar : Char -> IO Unit
printChar c = putStr (charToStr c)

putStrLn   : String -> IO Unit
putStrLn s = putStr s >>= \_ -> putStr "\n"

printNat : Nat -> IO Unit
printNat n = putStr (natToString n)

printBool : Bool -> IO Unit
printBool true = putStr "true"
printBool false = putStr "false"

printFloat : Float -> IO Unit
printFloat f = putStr (floatToString f)

infixr 2 _<$>_
_<$>_ : {A B : Set}(f : A -> B)(m : IO A) -> IO B
f <$> x = x >>= λ y -> return (f y)

infixr 0 bind
bind : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
bind m f = m >>= f

infixr 0 then
then : ∀ {a b} {A : Set a} {B : Set b} -> IO A -> IO B -> IO B
then m f = m >>= λ _ -> f

syntax bind e (\ x -> f) = x <- e , f
syntax then e f          = e ,, f


text:
module OpenModuleShortHand where

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

module List (Elem : Set) where

  data List : Set where
    []   : List
    _::_ : Elem -> List -> List

open List Nat

{- This means
open module _ = List Nat
-}

xs : List
xs = zero :: (suc zero :: [])


text:
module classify-tests where

open import lib
open import classify
open import syntax-util

test = check-beta-inequiv (mlam "a" (mlam "b" (mvar "a"))) (mlam "a" (mlam "b" (mvar "b")))

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Displayed where

open import Data.Product using (Σ ; Σ-syntax ; _,_)
open import Level using (_⊔_ ; suc)
open import Relation.Binary using
  (Setoid ; IsEquivalence ; Rel ; REL ; _Preserves₂_⟶_⟶_)

open import Cats.Category

record DisplayedCategory {lo la l≈} (C : Category lo la l≈) lo′ la′ l≈′
  : Set (lo ⊔ la ⊔ l≈ ⊔ suc (lo′ ⊔ la′ ⊔ l≈′)) where
  infixr  9  _∘_
  infix   4  _≈[_]_
  infixr  -1 _⇒[_]_

  Base = C
  module Base = Category Base
  private
    module C = Category C

  field
    Obj : (c : C.Obj) → Set lo′
    _⇒[_]_ : ∀ {a b} (a⁺ : Obj a) (f : a C.⇒ b) (b⁺ : Obj b) → Set la′
    _≈[_]_ : ∀ {a b} {f g : a C.⇒ b} {a⁺ : Obj a} {b⁺ : Obj b}
      → a⁺ ⇒[ f ] b⁺
      → f C.≈ g
      → a⁺ ⇒[ g ] b⁺
      → Set l≈′
    id : ∀ {a} {a⁺ : Obj a} → a⁺ ⇒[ C.id ] a⁺
    _∘_ : ∀ {a b c} {a⁺ : Obj a} {b⁺ : Obj b} {c⁺ : Obj c}
      → {f : b C.⇒ c} {g : a C.⇒ b}
      → (f⁺ : b⁺ ⇒[ f ] c⁺) (g⁺ : a⁺ ⇒[ g ] b⁺)
      → a⁺ ⇒[ f C.∘ g ] c⁺
    ≈-refl : ∀ {a b} {f : a C.⇒ b} {a⁺ : Obj a} {b⁺ : Obj b} {f⁺ : a⁺ ⇒[ f ] b⁺}
      → f⁺ ≈[ C.≈.refl ] f⁺
    ≈-sym : ∀ {a b} {f g : a C.⇒ b} {f≈g : f C.≈ g} {a⁺ : Obj a} {b⁺ : Obj b}
      → {f⁺ : a⁺ ⇒[ f ] b⁺} {g⁺ : a⁺ ⇒[ g ] b⁺}
      → f⁺ ≈[ f≈g ] g⁺
      → g⁺ ≈[ C.≈.sym f≈g ] f⁺
    ≈-trans : ∀ {a b}
      → {f g h : a C.⇒ b} {f≈g : f C.≈ g} {g≈h : g C.≈ h}
      → {a⁺ : Obj a} {b⁺ : Obj b}
      → {f⁺ : a⁺ ⇒[ f ] b⁺} {g⁺ : a⁺ ⇒[ g ] b⁺} {h⁺ : a⁺ ⇒[ h ] b⁺}
      → f⁺ ≈[ f≈g ] g⁺ → g⁺ ≈[ g≈h ] h⁺
      → f⁺ ≈[ C.≈.trans f≈g g≈h ] h⁺
    ∘-resp : ∀ {a b c} {f g : b C.⇒ c} {h i : a C.⇒ b}
      → {f≈g : f C.≈ g} {h≈i : h C.≈ i}
      → {a⁺ : Obj a} {b⁺ : Obj b} {c⁺ : Obj c}
      → {f⁺ : b⁺ ⇒[ f ] c⁺} {g⁺ : b⁺ ⇒[ g ] c⁺}
      → {h⁺ : a⁺ ⇒[ h ] b⁺} {i⁺ : a⁺ ⇒[ i ] b⁺}
      → f⁺ ≈[ f≈g ] g⁺
      → h⁺ ≈[ h≈i ] i⁺
      → f⁺ ∘ h⁺ ≈[ C.∘-resp f≈g h≈i ] g⁺ ∘ i⁺
    id-r : ∀ {a b} {f : a C.⇒ b} {a⁺ : Obj a} {b⁺ : Obj b} {f⁺ : a⁺ ⇒[ f ] b⁺}
      → f⁺ ∘ id ≈[ C.id-r ] f⁺
    id-l : ∀ {a b} {f : a C.⇒ b} {a⁺ : Obj a} {b⁺ : Obj b} {f⁺ : a⁺ ⇒[ f ] b⁺}
      → id ∘ f⁺ ≈[ C.id-l ] f⁺
    assoc : ∀ {a b c d} {f : c C.⇒ d} {g : b C.⇒ c} {h : a C.⇒ b}
      → {a⁺ : Obj a} {b⁺ : Obj b} {c⁺ : Obj c} {d⁺ : Obj d}
      → {f⁺ : c⁺ ⇒[ f ] d⁺} {g⁺ : b⁺ ⇒[ g ] c⁺} {h⁺ : a⁺ ⇒[ h ] b⁺}
      → (f⁺ ∘ g⁺) ∘ h⁺ ≈[ C.assoc ] f⁺ ∘ (g⁺ ∘ h⁺)

module BuildTotal
  {lo la l≈} {C : Category lo la l≈} {lo′ la′ l≈′}
  (D : DisplayedCategory C lo′ la′ l≈′)
  where

  infixr  9  _∘_
  infix   4  _≈_
  infixr  -1 _⇒_

  private
    module C = Category C
    module D = DisplayedCategory D

  Obj : Set (lo ⊔ lo′)
  Obj = Σ[ c ∈ C.Obj ] D.Obj c

  _⇒_ : (a b : Obj) → Set (la ⊔ la′)
  (a , a⁺) ⇒ (b , b⁺) = Σ[ f ∈ a C.⇒ b ] (a⁺ D.⇒[ f ] b⁺)

  _≈_ : ∀ {a b} → Rel (a ⇒ b) (l≈ ⊔ l≈′)
  (f , f⁺) ≈ (g , g⁺) = Σ[ f≈g ∈ f C.≈ g ] f⁺ D.≈[ f≈g ] g⁺

  id : ∀ {a} → a ⇒ a
  id = C.id , D.id

  _∘_ : ∀ {a b c} → b ⇒ c → a ⇒ b → a ⇒ c
  (f , f⁺) ∘ (g , g⁺) = (f C.∘ g) , (f⁺ D.∘ g⁺)

  equiv : ∀ {a b} → IsEquivalence (_≈_ {a} {b})
  equiv = record
    { refl = C.≈.refl , D.≈-refl
    ; sym = λ where
        (f≈g , f⁺≈g⁺) → C.≈.sym f≈g , D.≈-sym f⁺≈g⁺
    ; trans = λ where
        (f≈g , f⁺≈g⁺) (g≈h , g⁺≈h⁺) → C.≈.trans f≈g g≈h , D.≈-trans f⁺≈g⁺ g⁺≈h⁺
    }

  ∘-resp : ∀ {a b c} → (_∘_ {a} {b} {c} Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_)
  ∘-resp (f≈g , f⁺≈g⁺) (h≈i , h⁺≈i⁺) = C.∘-resp f≈g h≈i , D.∘-resp f⁺≈g⁺ h⁺≈i⁺

  id-r : ∀ {a b} {f : a ⇒ b} → f ∘ id ≈ f
  id-r = C.id-r , D.id-r

  id-l : ∀ {a b} {f : a ⇒ b} → id ∘ f ≈ f
  id-l = C.id-l , D.id-l

  assoc : ∀ {a b c d} {f : c ⇒ d} {g : b ⇒ c} {h : a ⇒ b}
    → (f ∘ g) ∘ h ≈ f ∘ (g ∘ h)
  assoc = C.assoc , D.assoc

  Total : Category (lo ⊔ lo′) (la ⊔ la′) (l≈ ⊔ l≈′)
  Total = record
    { Obj = Obj
    ; _⇒_ = _⇒_
    ; _≈_ = _≈_
    ; id = id
    ; _∘_ = _∘_
    ; equiv = equiv
    ; ∘-resp = ∘-resp
    ; id-r = id-r
    ; id-l = id-l
    ; assoc = assoc
    }

open BuildTotal public using (Total)

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
module EqTest where

import Common.Level

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

data Maybe (a : Set) : Set where
  just    : a -> Maybe a
  nothing : Maybe a

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

_≟_ : (x y : ℕ) -> Maybe (x ≡ y)
suc m  ≟ suc n with m ≟ n
suc .n ≟ suc n |    just refl = just refl
suc m  ≟ suc n |    nothing   = nothing
zero   ≟ suc _ = nothing
suc m  ≟ zero  = nothing
zero   ≟ zero  = just refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Issue477b where

record D where
  field A : Set


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

open import Categories.Category

-- BinaryCoproducts -- a category with all binary coproducts
-- Cocartesian -- a category with all coproducts

-- since most of the work is dual to Categories.Category.Cartesian, so the idea
-- in this module is to make use of duality
module Categories.Category.Cocartesian {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

private
  module 𝒞 = Category 𝒞
  open Category 𝒞
  open HomReasoning
  variable
    A B C D : Obj
    f g h i : A ⇒ B

open import Categories.Object.Initial 𝒞
open import Categories.Object.Coproduct 𝒞
open import Categories.Object.Duality 𝒞
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Symmetric
open import Categories.Category.Cartesian 𝒞.op
open import Categories.Morphism 𝒞
open import Categories.Morphism.Properties 𝒞
open import Categories.Morphism.Duality 𝒞
open import Categories.Morphism.Reasoning 𝒞

open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.Functor.Bifunctor

record BinaryCoproducts : Set (levelOfTerm 𝒞) where

  infixr 6 _+_
  infixr 7 _+₁_

  field
    coproduct : ∀ {A B} → Coproduct A B

  module coproduct {A} {B} = Coproduct (coproduct {A} {B})

  _+_ : Obj → Obj → Obj
  A + B = coproduct.A+B {A} {B}

  open coproduct
    using (i₁; i₂; [_,_]; inject₁; inject₂; []-cong₂)
    renaming (unique to +-unique; η to +-η; g-η to +-g-η)
    public

  module Dual where
    op-binaryProducts : BinaryProducts
    op-binaryProducts = record { product = coproduct→product coproduct }

    module op-binaryProducts = BinaryProducts op-binaryProducts

  open Dual

  +-comm : A + B ≅ B + A
  +-comm = op-≅⇒≅ (op-binaryProducts.×-comm)

  +-assoc : A + B + C ≅ (A + B) + C
  +-assoc = op-≅⇒≅ (op-binaryProducts.×-assoc)

  _+₁_ : A ⇒ B → C ⇒ D → A + C ⇒ B + D
  _+₁_ = op-binaryProducts._⁂_

  open op-binaryProducts
    using ()
    renaming ( ⟨⟩-congʳ     to []-congʳ
             ; ⟨⟩-congˡ     to []-congˡ
             ; assocˡ       to +-assocʳ
             ; assocʳ       to +-assocˡ
             ; swap         to +-swap
             ; first        to +-first
             ; second       to +-second
             ; π₁∘⁂         to +₁∘i₁
             ; π₂∘⁂         to +₁∘i₂
             ; ⁂-cong₂      to +₁-cong₂
             ; ⁂∘⟨⟩         to []∘+₁
             ; ⁂∘⁂          to +₁∘+₁
             ; ⟨⟩∘          to ∘[]
             ; first↔second to +-second↔first
             ; swap∘⁂       to +₁∘+-swap
             ; swap∘swap    to +-swap∘swap
             )
    public

  -- since op-×- has type Bifunctor 𝒞.op 𝒞.op 𝒞.op,
  -- need to rewrap in order to type check
  -+- : Bifunctor 𝒞 𝒞 𝒞
  -+- = record
    { F₀           = op-×-.F₀
    ; F₁           = op-×-.F₁
    ; identity     = op-×-.identity
    ; homomorphism = op-×-.homomorphism
    ; F-resp-≈     = op-×-.F-resp-≈
    }
    where op-×- = op-binaryProducts.-×-
          module op-×- = Functor op-×-

  -+_ : Obj → Functor 𝒞 𝒞
  -+_ = appʳ -+-

  _+- : Obj → Functor 𝒞 𝒞
  _+- = appˡ -+-

record Cocartesian : Set (levelOfTerm 𝒞) where
  field
    initial    : Initial
    coproducts : BinaryCoproducts

  module initial    = Initial initial
  module coproducts = BinaryCoproducts coproducts

  open initial
    renaming (! to ¡; !-unique to ¡-unique; !-unique₂ to ¡-unique₂)
    public
  open coproducts hiding (module Dual) public

  module Dual where
    open coproducts.Dual public

    op-cartesian : Cartesian
    op-cartesian = record
      { terminal = ⊥⇒op⊤ initial
      ; products = op-binaryProducts
      }

    module op-cartesian = Cartesian op-cartesian

  open Dual

  ⊥+A≅A : ⊥ + A ≅ A
  ⊥+A≅A = op-≅⇒≅ (op-cartesian.⊤×A≅A)

  A+⊥≅A : A + ⊥ ≅ A
  A+⊥≅A = op-≅⇒≅ (op-cartesian.A×⊤≅A)

  open op-cartesian
    using ()
    -- both are natural isomorphism
    renaming (⊤×--id to ⊥+--id; -×⊤-id to -+⊥-id)
    public

  +-monoidal : Monoidal 𝒞
  +-monoidal = record
    { ⊗                    = -+-
    ; unit                 = unit
    ; unitorˡ              = ⊥+A≅A
    ; unitorʳ              = A+⊥≅A
    ; associator           = ≅.sym +-assoc
    ; unitorˡ-commute-from = ⟺ unitorˡ-commute-to
    ; unitorˡ-commute-to   = ⟺ unitorˡ-commute-from
    ; unitorʳ-commute-from = ⟺ unitorʳ-commute-to
    ; unitorʳ-commute-to   = ⟺ unitorʳ-commute-from
    ; assoc-commute-from   = ⟺ assoc-commute-to
    ; assoc-commute-to     = ⟺ assoc-commute-from
    -- the proof idea of triangle is that the opposite triangle is obtained for free,
    -- but notice that triangle and the opposite triangle form isomorphism.
    ; triangle             = λ {X Y} →
                               Iso-≈ triangle
                                     (Iso-∘ ([ X +- ]-resp-Iso (Iso-swap (iso ⊥+A≅A)))
                                            (iso +-assoc))
                                     ([ -+ Y ]-resp-Iso (Iso-swap (iso A+⊥≅A)))
    ; pentagon             = λ {X Y Z W} →
                               Iso-≈ pentagon
                                     (Iso-∘ ([ X +- ]-resp-Iso (iso +-assoc))
                                     (Iso-∘ (iso +-assoc)
                                            ([ -+ W ]-resp-Iso (iso +-assoc))))
                                     (Iso-∘ (iso +-assoc) (iso +-assoc))
    }
    where op-monoidal = op-cartesian.monoidal
          open Monoidal op-monoidal
          open _≅_

  module +-monoidal = Monoidal +-monoidal

  +-symmetric : Symmetric +-monoidal
  +-symmetric = record
    { braided     = record
      { braiding = record
        { F⇒G = record
          { η           = λ _ → +-swap
          ; commute     = λ _ → ⟺ +₁∘+-swap
          ; sym-commute = λ _ → +₁∘+-swap
          }
        ; F⇐G = record
          { η           = λ _ → +-swap
          ; commute     = λ _ → ⟺ +₁∘+-swap
          ; sym-commute = λ _ → +₁∘+-swap
          }
        ; iso = λ _ → iso +-comm
        }
      ; hexagon₁ = braided.hexagon₂
      ; hexagon₂ = braided.hexagon₁
      }
    ; commutative = commutative
    }
    where op-symmetric = op-cartesian.symmetric
          open Symmetric op-symmetric
          open _≅_

  -- we don't open this module publicly in order to prevent introducing conflicts
  -- with Cartesian category
  module +-symmetric = Symmetric +-symmetric

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

data D : Set where
  @0 c : D

data P (x : D) : Set where

record R : Set where
  field
    f : P c


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

open import Level using (Level)

open import Data.List using (List; sum) renaming ([] to []ᴸ; _∷_ to _∷ᴸ_)
open import Data.Nat using (ℕ; _+_; zero; suc)
open import Data.Vec using (Vec; _++_; take; drop) renaming ([] to []ⱽ; _∷_ to _∷ⱽ_)
open import Data.Product as Prod using (∃; ∃₂; _×_; _,_)

module FLA.Data.VectorList where

-- At the moment, `VectorList` is named `RList` in the Haskell code.
data VectorList (A : Set) : List ℕ → Set where
  []ⱽᴸ  : VectorList A []ᴸ
  _∷ⱽᴸ_ : {n : ℕ} {ns : List ℕ} → Vec A n → VectorList A ns
                                → VectorList A (n ∷ᴸ ns)
infixr 5 _∷ⱽᴸ_

concat : {A : Set} {ns : List ℕ} → VectorList A ns → Vec A (sum ns)
concat []ⱽᴸ = []ⱽ
concat (v ∷ⱽᴸ vs) = v ++ concat vs

-- We will want to use split to split a VectorList
split : {ℓ : Level} {A : Set ℓ} → {m n : ℕ} → Vec A (m + n) → Vec A m × Vec A n
split {ℓ} {A} {zero} {n} v = []ⱽ , v
split {ℓ} {A} {suc m} {n} (v ∷ⱽ vs) = let v₁ , v₂ = split vs in v ∷ⱽ v₁ , v₂

-- split' : {ℓ : Level} {A : Set ℓ} → {m n : ℕ} → Vec A (m + n) → Vec A m × Vec A n
-- split' {ℓ} {A} {m} {n} v = (take v , drop v)

-- Hmm, this will be hard to translate to Haskell, since we match on ns
splitToVectorList : {A : Set} → (ns : List ℕ) → Vec A (sum ns) → VectorList A ns
splitToVectorList []ᴸ v = []ⱽᴸ
splitToVectorList (_ ∷ᴸ ns) v = let v₁ , v₂ = split v in
                                v₁ ∷ⱽᴸ (splitToVectorList ns v₂)

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


text:
module Issue477 where

data D where
  c : D

max_stars_repo_name: asr/agda-kanso


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

import Data.String.Base as String
{-# BUILTIN FROMSTRING String.toList #-}
open import Data.Nat using (ℕ; zero; suc)
open import Data.Bool using (Bool; true; false)
open import Data.Unit using (⊤; tt)
open import Data.Fin using (Fin; zero; suc) renaming (#_ to #'_)
open import Data.Product using (_,_)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
open import Data.String
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

import Level as L

open import PiCalculus.Syntax
open Scoped
open import PiCalculus.Semantics
open import PiCalculus.LinearTypeSystem.Algebras
open import PiCalculus.LinearTypeSystem.Algebras.Linear using (Linear)
open import PiCalculus.LinearTypeSystem.Algebras.Shared using (Shared)
open import PiCalculus.LinearTypeSystem.Algebras.Graded using (Graded)

module PiCalculus.Examples where
open Raw

variable
  n : ℕ

raw : Raw
raw = ⦅ν "x"⦆ (("x" ⦅ "y" ⦆ 𝟘) ∥ ("x" ⟨ "a" ⟩ 𝟘))

scoped : Scoped 1
scoped = ν (((#' 0) ⦅⦆ 𝟘) ⦃ "y" ⦄ ∥ ((#' 0) ⟨ #' 1 ⟩ 𝟘)) ⦃ "x" ⦄

_ : Conversion.fromRaw ("a" ∷ []) raw ≡ scoped
_ = refl

channel-over-channel₀ : Raw
channel-over-channel₀ = ⦅ν "x"⦆
                        ( ("x" ⦅ "r" ⦆ "r" ⦅ "p" ⦆ 𝟘)
                        ∥ (⦅ν "z"⦆ ("x" ⟨ "z" ⟩ "z" ⟨ "y" ⟩ 𝟘)))

channel-over-channel₁ : Raw
channel-over-channel₁ = ⦅ν "x"⦆ ⦅ν "z"⦆
                        ( ("x" ⦅ "r" ⦆ "r" ⦅ "p" ⦆ 𝟘)
                        ∥ ("x" ⟨ "z" ⟩ "z" ⟨ "y" ⟩ 𝟘))

channel-over-channel₂ : Raw
channel-over-channel₂ = ⦅ν "z"⦆ ⦅ν "x"⦆
                        ( ("x" ⦅ "r" ⦆ "r" ⦅ "p" ⦆ 𝟘)
                        ∥ ("x" ⟨ "z" ⟩ "z" ⟨ "y" ⟩ 𝟘))

channel-over-channel₃ : Raw
channel-over-channel₃ = ⦅ν "z"⦆ ⦅ν "x"⦆
                        ( ("z" ⦅ "p" ⦆ 𝟘)
                        ∥ ("z" ⟨ "y" ⟩ 𝟘))

channel-over-channel₄ : Raw
channel-over-channel₄ = ⦅ν "z"⦆ ⦅ν "x"⦆
                        (𝟘 ∥ 𝟘)

channel-over-channel₅ : Raw
channel-over-channel₅ = ⦅ν "z"⦆ ⦅ν "x"⦆ 𝟘

channel-over-channel₆ : Raw
channel-over-channel₆ = ⦅ν "z"⦆ 𝟘

channel-over-channel₇ : Raw
channel-over-channel₇ = 𝟘

_!_≅_ : ∀ {n} → Vec Name n → Raw → Raw → Set
_!_≅_ = Conversion.map₂ _≅_

_!_⇒_ : ∀ {n} → Vec Name n → Raw → Raw → Set
_!_⇒_ = Conversion.map₂ _⇒_

_ : ("y" ∷ []) ! channel-over-channel₀ ≅ channel-over-channel₁
_ = _ , ν-cong cong-symm stop scope-ext ((λ ()) , (λ ()) , tt)

_ : ("y" ∷ []) ! channel-over-channel₁ ≅ channel-over-channel₂
_ = _ , stop scope-scope-comm

_ : ("y" ∷ []) ! channel-over-channel₂ ⇒ channel-over-channel₃
_ = _ , res res comm

_ : ("y" ∷ []) ! channel-over-channel₃ ⇒ channel-over-channel₄
_ = _ , res res comm

_ : ("y" ∷ []) ! channel-over-channel₄ ≅ channel-over-channel₅
_ = _ , ν-cong ν-cong stop comp-end

_ : ("y" ∷ []) ! channel-over-channel₅ ≅ channel-over-channel₆
_ = _ , ν-cong stop scope-end

_ : ("y" ∷ []) ! channel-over-channel₆ ≅ channel-over-channel₇
_ = _ , stop scope-end

module Shared-Graded-Linear where
  data Grading : Set where
    sha gra lin : Grading

  pattern 0∙ = false
  pattern 1∙ = true

  QUANTIFIERS : Algebras
  Algebras.Idx QUANTIFIERS = Grading
  Algebras.∃Idx QUANTIFIERS = sha
  Algebras.Usage QUANTIFIERS sha = ⊤
  Algebras.Usage QUANTIFIERS gra = ℕ
  Algebras.Usage QUANTIFIERS lin = Bool
  Algebras.UsageAlgebra QUANTIFIERS sha = Shared
  Algebras.UsageAlgebra QUANTIFIERS gra = Graded
  Algebras.UsageAlgebra QUANTIFIERS lin = Linear

  open Algebras QUANTIFIERS hiding (ℓᵢ;ℓₒ;ℓ∅;ℓ#;0∙;1∙)
  open import PiCalculus.LinearTypeSystem QUANTIFIERS
  open import PiCalculus.LinearTypeSystem.ContextLemmas QUANTIFIERS

  _!_；[_]_⊢_▹_ : Vec Name n → PreCtx n → (idxs : Idxs n) → Ctx idxs → Raw → Ctx idxs → Set
  ctx ! γ ；[ idxs ] Γ ⊢ P ▹ Δ = Conversion.map (λ P' → γ ；[ idxs ] Γ ⊢ P' ▹ Δ) ctx P

  ω∙ : ⊤ ²
  ω∙ = tt , tt

  ℓ# : Bool ²
  ℓ# = true , true

  ℓᵢ : Bool ²
  ℓᵢ = true , false

  ℓₒ : Bool ²
  ℓₒ = false , true

  ℓ∅ : Bool ²
  ℓ∅ = false , false

  instance
    name : Name
    name = ""

  _ : ([] -, "y") ! [] -, 𝟙 ；[ [] -, sha ] [] -, ω∙ ⊢ channel-over-channel₀ ▹ ε
  _ = ν C[ 𝟙 ； ω∙ ] ℓᵢ {lin} 1∙
      (((here ) ⦅⦆ (here ⦅⦆ 𝟘)) ∥
            (ν 𝟙 ω∙ {lin} 1∙
                  ((there here) ⟨ here ⟩ (here ⟨ there there here ⟩ 𝟘))))

  _ : [] -, 𝟙 ；[ [] -, sha ] [] -, ω∙ ⊢ ν (((#' 0) ⟨ #' 1 ⟩ 𝟘) ∥ ((#' 0) ⦅⦆ 𝟘)) ▹ ε
  _ = ν 𝟙 ω∙ {lin} 1∙ ((# 0 ⟨ # 1 ⟩ 𝟘) ∥ (# 0 ⦅⦆ 𝟘))

  p : Scoped 1
  p = ν (((#' 0) ⦅⦆ ((#' 0) ⦅⦆ 𝟘)) ∥ (ν ((#' 1) ⟨ #' 0 ⟩ (#' 0) ⟨ #' 2 ⟩ 𝟘)))

  _ : [] -, 𝟙 ；[ [] -, sha ] [] -, ω∙ ⊢ p ▹ ε
  _ = ν C[ 𝟙 ； ω∙ ] {lin} ℓᵢ {lin} 1∙ (
           (here ⦅⦆ (here ⦅⦆ 𝟘)) ∥ (ν 𝟙 ω∙ 1∙ (there here ⟨ here ⟩ (here ⟨ there there here ⟩ 𝟘))))

  P : Scoped 2
  P = (ν (suc zero ⟨ zero ⟩ zero ⟨ suc (suc zero) ⟩ 𝟘)) ∥ (zero ⦅⦆ zero ⦅⦆ 𝟘)

  ⊢P : ∀ {n} → [] -, 𝟙 -, C[ C[ 𝟙 ； ω∙ ] ； ℓᵢ ] ；[ [] -, sha -, gra ] [] -, ω∙ -, (suc n , suc n) ⊢ P ▹ [] -, ω∙ -, (n , n)
  ⊢P = ν 𝟙 ω∙ {lin} 1∙ ((there here) ⟨ here ⟩ (here ⟨ there there here ⟩ 𝟘)) ∥ (here ⦅⦆ (here ⦅⦆ 𝟘))

  ⊢P∥P : [] -, 𝟙 ；[ [] -, sha ] [] -, ω∙ ⊢ ν (P ∥ P) ▹ ε
  ⊢P∥P = ν C[ 𝟙 ； ω∙ ] ℓᵢ 2 (⊢P ∥ ⊢P)

  sync : ∀ {n} → Fin n → Fin n → Fin n → Scoped n
  sync i0 i1 o =
    i0 ⦅⦆
    suc i1 ⦅⦆
    suc (suc o) ⟨ suc zero ⟩
    suc (suc o) ⟨ zero ⟩ 𝟘

  send : ∀ {n} → Fin n → Scoped n
  send c = ν (suc c ⟨ zero ⟩ 𝟘)

  recv : ∀ {n} → Fin n → Scoped n
  recv c = c ⦅⦆ (suc c ⦅⦆ 𝟘)

  example : Scoped 0
  example = ν ( (send zero)
              ∥ ν ( (send zero)
                  ∥ ν ( recv zero
                      ∥ sync (#' 2) (#' 1) (#' 0))))

  ⊢-send : ∀ {n} {γ : PreCtx n} {idxs : Idxs n} {Γ : Ctx idxs} {k l}
         → γ -, C[_；_] {idx = lin} (C[_；_] {idx = sha} 𝟙 ω∙) ℓ∅ ；[ idxs -, gra ] Γ -, (k , suc l) ⊢ send zero ▹ Γ -, (k , l)
  ⊢-send = ν _ _ 0∙ (there here ⟨ here ⟩ 𝟘)

  ⊢-recv : ∀ {n} {γ : PreCtx n} {idxs : Idxs n} {Γ : Ctx idxs} {t : Type} {k l}
         → γ -, (C[_；_] {idx = lin} t ℓ∅) ；[ idxs -, gra ] Γ -, (suc (suc l) , k) ⊢ recv zero ▹ Γ -, (l , k)
  ⊢-recv = here ⦅⦆ (there here ⦅⦆ 𝟘)

  ⊢-sync : ∀ {n} {γ : PreCtx n} {idxs : Idxs n} {Γ : Ctx idxs} {t : Type} {lx rx ly ry lz rz}
         → γ -, C[_；_] {idx = lin} t ℓ∅ -, C[ t ； ℓ∅ ] -, C[ t ； ℓ∅ ]
         ；[ idxs -, gra -, gra -, gra ]
         Γ -, (suc lx , rx) -, (suc ly , ry) -, (lz , suc (suc rz)) ⊢ sync (#' 2) (#' 1) (#' 0) ▹ Γ -, (lx , rx) -, (ly , ry) -, (lz , rz)
  ⊢-sync = (there (there here)) ⦅⦆
           (there (there here)) ⦅⦆
           (there (there here)) ⟨ there here ⟩
           (there (there here)) ⟨ here ⟩ 𝟘

  _ : [] ； [] ⊢ example ▹ []
  _ = ν _ _ _ ( ⊢-send
    ∥ ν _ _ _ ( ⊢-send
    ∥ ν _ _ _ ( ⊢-recv
    ∥ ⊢-sync )))

module Linear where
  QUANTIFIERS : Algebras
  Algebras.Idx QUANTIFIERS = ⊤
  Algebras.∃Idx QUANTIFIERS = tt
  Algebras.Usage QUANTIFIERS _ = Bool
  Algebras.UsageAlgebra QUANTIFIERS _ = Linear

  open Algebras QUANTIFIERS
  open import PiCalculus.LinearTypeSystem QUANTIFIERS
  open import PiCalculus.LinearTypeSystem.ContextLemmas QUANTIFIERS

  _ : [] -, C[ 𝟙 ； ℓᵢ ] -, 𝟙 ； [] -, ℓ# -, ℓ# ∋[ #' 1 ] C[ 𝟙 ； ℓᵢ ] ； ℓᵢ ▹ [] -, ℓₒ -, ℓ#
  _ = there here

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi