text:
module plfa-exercises.Practice5 where

open import Data.Nat using (ℕ; zero; suc)
open import Data.String using (String; _≟_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import plfa.part1.Isomorphism using (_≲_)

Id : Set
Id = String

infix  5  ƛ_⇒_ μ_⇒_
infixl 7  _·_
infix  8  `suc_
infix  9  `_

data Term : Set where
  `_                      :  Id → Term
  ƛ_⇒_                    :  Id → Term → Term
  _·_                     :  Term → Term → Term
  `zero                   :  Term
  `suc_                   :  Term → Term
  case_[zero⇒_|suc_⇒_]    :  Term → Term → Id → Term → Term
  μ_⇒_                    :  Id → Term → Term

--ƛ "x" ⇒ `suc `zero

one = `suc `zero
two = `suc one

plus : Term
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
         case ` "m"
           [zero⇒ ` "n"
           |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]

--plus · two · two

twoᶜ : Term
twoᶜ =  ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")

plusᶜ : Term
plusᶜ =  ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
         ` "m" · ` "s" · (` "n" · ` "s" · ` "z")

sucᶜ : Term
sucᶜ = ƛ "n" ⇒ `suc (` "n")

----- Little detour into the same definitions but working in Agda
--plus c                    one           two
--(λ m n s z → m s (n s z)) (λ s z → s z) (λ s z → s (s z)) suc zero

Nat : Set₁
Nat = ∀ {A : Set} → (A → A) → A → A

--my_two : ∀ {A : Set} → (A → A) → A → A
my_two : Nat
my_two = (λ s z → s (s z))

--my_four : ∀ {A : Set} → (A → A) → A → A
my_four : Nat
my_four = (λ s z → s (s (s (s z))))

--(λ m n s z → m s (n s z)) my_two my_four
--my_add : ∀ {A : Set} → ((A → A) → A → A) → ((A → A) → A → A) → (A → A) → A → A
my_add : Nat → Nat → Nat
my_add = (λ m n s z → m s (n s z))
--my_add = (λ m n s → (m s) ∘ (n s))

-- my_add my_two my_four   ≡   λ s z → s (s (s (s (s (s z)))))

six : ℕ
six = my_add my_two my_four suc zero
--six = 6

--my_mul : ∀ {A : Set} → ((A → A) → A → A) → ((A → A) → A → A) → (A → A) → A → A
my_mul : Nat → Nat → Nat
my_mul = (λ m n s z → m (n s) z)
--my_mul = (λ m n s → m (n s))

--my_mul my_two my_four  ≡  λ s z → s (s (s (s (s (s (s (s z)))))))
eight_true : my_mul my_two my_four suc zero ≡ 8
eight_true = refl
----- End of detour

-- Exercises
mult : Term
mult = μ "*" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
         case ` "m"
           [zero⇒ `zero
           |suc "m" ⇒ plus · (` "*" · ` "m" · ` "n") · ` "n" ]

multᶜ : Term
multᶜ =  ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
         ` "m" · (` "n" · ` "s") · ` "z"
--- End Exercises

data Value : Term → Set where
  V-ƛ : ∀ {x N} → Value (ƛ x ⇒ N)
  V-zero : Value `zero
  V-suc : ∀ {V} → Value V → Value (`suc V)

-- Notice that this only works if we are working with _closed_ terms.
-- Open terms require more care

infix 9 _[_:=_]

-- Wrote them partly by myself
_[_:=_] : Term → Id → Term → Term
(` x) [ x' := V ] with x ≟ x'
... | yes _ = V
... | no _  = ` x
(ƛ x ⇒ M) [ x' := V ] with x ≟ x'
... | yes _ = ƛ x ⇒ M
... | no _  = ƛ x ⇒ (M [ x' := V ])
(M · N) [ x := V ] = (M [ x := V ]) · (N [ x := V ])
`zero [ _ := _ ] = `zero
(`suc M) [ x := V ] = `suc (M [ x := V ])
(case n [zero⇒ M |suc n' ⇒ N ]) [ x := V ] with x ≟ n'
... | yes _ = case (n [ x := V ]) [zero⇒ (M [ x := V ]) |suc n' ⇒ N ]
... | no _  = case (n [ x := V ]) [zero⇒ (M [ x := V ]) |suc n' ⇒ (N [ x := V ]) ]
(μ f ⇒ M) [ x := V ] with f ≟ x
... | yes _ = μ f ⇒ M
... | no _  = μ f ⇒ (M [ x := V ])

-- (ƛ "y" ⇒ ` "x" · (ƛ "x" ⇒ ` "x")) [ "x" := `zero ]

infix 4 _—→_

data _—→_ : Term → Term → Set where

  ξ-·₁ : ∀ {L L′ M}
    → L —→ L′
      -----------------
    → L · M —→ L′ · M

  ξ-·₂ : ∀ {V M M′}
    → Value V
    → M —→ M′
      -----------------
    → V · M —→ V · M′

  β-ƛ : ∀ {x N V}
    → Value V
      ------------------------------
    → (ƛ x ⇒ N) · V —→ N [ x := V ]

  ξ-suc : ∀ {M M′}
    → M —→ M′
      ------------------
    → `suc M —→ `suc M′

  ξ-case : ∀ {x L L′ M N}
    → L —→ L′
      -----------------------------------------------------------------
    → case L [zero⇒ M |suc x ⇒ N ] —→ case L′ [zero⇒ M |suc x ⇒ N ]

  β-zero : ∀ {x M N}
      ----------------------------------------
    → case `zero [zero⇒ M |suc x ⇒ N ] —→ M

  β-suc : ∀ {x V M N}
    → Value V
      ---------------------------------------------------
    → case `suc V [zero⇒ M |suc x ⇒ N ] —→ N [ x := V ]

  β-μ : ∀ {x M}
      ------------------------------
    → μ x ⇒ M —→ M [ x := μ x ⇒ M ]

_ : (ƛ "x" ⇒ `suc (`suc (` "x"))) · (`suc `zero) —→ `suc (`suc (`suc `zero))
_ = β-ƛ (V-suc V-zero)

_ : (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")  —→  (ƛ "x" ⇒ ` "x")
_ = β-ƛ V-ƛ

_ : (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")  —→  (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")
_ = ξ-·₁ (β-ƛ V-ƛ)

_ : twoᶜ · sucᶜ · `zero  —→  (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero
_ = ξ-·₁ (β-ƛ V-ƛ)

--- Detour
t : ∀ {A B : Set} → A → B → A
t = λ x y → x -- true
f : ∀ {A B : Set} → A → B → B
f = λ x y → y -- false
--is0 : ∀ {A : Set} → ((A → A → A → A) → (A → A → A) → A → A → A) → A → A → A
--is0 {A} = λ n → n (λ x → f {A}) (t {A})
--is0 : ∀ {A B : Set} → ((A → A → A → A) → (A → A → A) → A → A → A) → (A → A) → A → A
--is0 {A} {B} = λ n → n (λ x → f {A} {B}) (t {A} {B})

-- is0 {ℕ} (λ s z → z)   -- returns true
-- is0 (λ s z → s z) -- returns false
--- End detour

infix  2 _—↠_
infix  1 begin_
infixr 2 _—→⟨_⟩_ _—→⟨⟩_
infix  3 _∎

data _—↠_ : Term → Term → Set where
  _∎ : ∀ M
      ---------
    → M —↠ M

  _—→⟨_⟩_ : ∀ L {M N}
    → L —→ M
    → M —↠ N
      ---------
    → L —↠ N

begin_ : ∀ {M N}
  → M —↠ N
    ------
  → M —↠ N
begin M—↠N = M—↠N

_—→⟨⟩_ : ∀ L {N}
  → L —↠ N
    ---------
  → L —↠ N
_—→⟨⟩_ l l—↠n = l—↠n

trans : ∀ {L M N}
      → L —↠ M
      → M —↠ N
      → L —↠ N
trans (m ∎) m—↠n = m—↠n
trans (l —→⟨ l—→o ⟩ o—↠m) m—↠n = l —→⟨ l—→o ⟩ (trans o—↠m m—↠n)

_ : (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")  —↠  (ƛ "x" ⇒ ` "x")
_ =
  begin
    (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
    (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")                   —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x")                                     —→⟨ β-ƛ V-ƛ ⟩
    ƛ "x" ⇒ ` "x"
  ∎

data _—↠′_ : Term → Term → Set where

  step′ : ∀ {M N}
    → M —→ N
      -------
    → M —↠′ N

  refl′ : ∀ {M}
      -------
    → M —↠′ M

  trans′ : ∀ {L M N}
    → L —↠′ M
    → M —↠′ N
      -------
    → L —↠′ N

↠≲—↠′ : ∀ t t' → (t —↠ t') ≲ (t —↠′ t')
↠≲—↠′ t t' = record {
   to      = to
 ; from    = from
 ; from∘to = from∘to
 }
 where
    to : ∀ {t t'} → t —↠ t' → t —↠′ t'
    to (m ∎) = refl′ {m}
    to (l —→⟨ l—→m ⟩ m—↠n) = trans′ {l} (step′ l—→m) (to m—↠n)

    from : ∀ {t t'} → t —↠′ t' → t —↠ t'
    from (step′ {m} {n} m—→n) = m —→⟨ m—→n ⟩ n ∎
    from (refl′ {m}) = m ∎
    from (trans′ {l} {m} {n} l—↠′m m—↠′n) =
      trans (from l—↠′m) (from m—↠′n)

    from∘to : ∀ {l n} (x : l —↠ n) → from (to x) ≡ x
    from∘to (n ∎) = refl
    from∘to (l —→⟨ l—→m ⟩ m—↠n) = cong (l —→⟨ l—→m ⟩_) (from∘to m—↠n)

    --to∘from : ∀ {l n} (x : l —↠′ n) → to (from x) ≡ x
    --to∘from (step′ {m} {n} m—→n) = ?
    ---- here lies the problem:
    ----   to (from (step′ m—→n)) ≡ step′ m—→n
    ---- is converted into:
    ----   trans′ (step′ m—→n) refl′ ≡ step′ m—→n
    ---- which cannot be true :/, both are constructors, both
    ---- create the same type. Lesson, always make sure your data
    ---- definitions make unique elements
    --to∘from = ?

_ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero
_ = begin
  twoᶜ · sucᶜ · `zero                                       —→⟨⟩  -- def
  (ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) · sucᶜ · `zero  —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
  (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero                   —→⟨ β-ƛ V-zero ⟩
  sucᶜ · (sucᶜ · `zero)                                     —→⟨⟩
  (ƛ "n" ⇒ `suc (` "n")) · ((ƛ "n" ⇒ `suc (` "n")) · `zero) —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
  (ƛ "n" ⇒ `suc (` "n")) · `suc `zero                       —→⟨ β-ƛ (V-suc V-zero) ⟩
  `suc `suc `zero  ∎

oneᶜ : Term
oneᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · ` "z"

_ : plusᶜ · oneᶜ · oneᶜ · sucᶜ · `zero —↠ `suc `suc `zero
_ = begin
  plusᶜ · oneᶜ · oneᶜ · sucᶜ · `zero                                           —→⟨⟩
  plusᶜ · oneᶜ · oneᶜ · sucᶜ · `zero                                           —→⟨⟩
  (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
         ` "m" · ` "s" · (` "n" · ` "s" · ` "z")) · oneᶜ · oneᶜ · sucᶜ · `zero —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
  (ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
         oneᶜ · ` "s" · (` "n" · ` "s" · ` "z")) · oneᶜ · sucᶜ · `zero         —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
  (ƛ "s" ⇒ ƛ "z" ⇒ oneᶜ · ` "s" · (oneᶜ  · ` "s" · ` "z")) · sucᶜ · `zero      —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
  (ƛ "z" ⇒ oneᶜ · sucᶜ  · (oneᶜ  · sucᶜ · ` "z")) · `zero                      —→⟨ β-ƛ V-zero ⟩
  oneᶜ · sucᶜ  · (oneᶜ  · sucᶜ · `zero)                                        —→⟨⟩
  (ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · ` "z") · sucᶜ  · (oneᶜ  · sucᶜ · `zero)             —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
  (ƛ "z" ⇒ sucᶜ · ` "z") · (oneᶜ  · sucᶜ · `zero)                              —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
  (ƛ "z" ⇒ sucᶜ · ` "z") · ((ƛ "z" ⇒ sucᶜ · ` "z") · `zero)                    —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
  (ƛ "z" ⇒ sucᶜ · ` "z") · (sucᶜ · `zero)                                      —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
  (ƛ "z" ⇒ sucᶜ · ` "z") · (`suc `zero)                                        —→⟨ β-ƛ (V-suc V-zero) ⟩
  sucᶜ · (`suc `zero)                                                          —→⟨ β-ƛ (V-suc V-zero) ⟩
  `suc `suc `zero ∎


text:
module Ag13 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using ()
  renaming (contradiction to ¬¬-intro)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Ag09 using (_⇔_)

data Bool : Set where
  true  : Bool
  false : Bool

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

T→≡ : ∀ (b : Bool) → T b → b ≡ true
T→≡ true tt   =  refl
T→≡ false ()

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl  =  tt

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

infix 4 _≤_

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero)
¬s≤z ()

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s ¬m≤n (s≤s m≤n) = ¬m≤n m≤n

_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
zero  ≤? n                   =  yes z≤n
suc m ≤? zero                =  no ¬s≤z
suc m ≤? suc n with m ≤? n
...               | yes m≤n  =  yes (s≤s m≤n)
...               | no ¬m≤n  =  no (¬s≤s ¬m≤n)

ext: agda

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

useful-lemma : ∀ {a} {A : Set a} → A
useful-lemma = useful-lemma

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --without-K --copatterns --sized-types #-}
open import lib.Basics
open import lib.PathGroupoid
open import lib.types.Paths
open import lib.Funext
open import Size

{-
-- | Coinductive delay type. This is the functor νπ̂ : Set → Set arising
-- as the fixed point of π̂(H) = π ∘ ⟨Id, H⟩, where π : Set × Set → Set
-- with π(X, Y) = X.
record D (S : Set) : Set where
  coinductive
  field
    force : S
open D

-- | Action of D on morphisms
D₁ : ∀ {X Y} → (X → Y) → D X → D Y
force (D₁ f x) = f (force x)

-- | D lifted to dependent functions
↑D₁ : ∀ {A} → (B : A → Set) → ((x : A) → B x) → (y : D A) → D (B (force y))
force (↑D₁ B f y) = f (force y)

D-intro : ∀ {H : Set → Set} → (∀ {X} → H X → X) → (∀ {X} → H X → D X)
force (D-intro f x) = f x

D-intro2 : ∀ {X S : Set} → (X → S) → X → D S
force (D-intro2 f x) = f x

postulate
  -- | We'll need coinduction to prove such equalities in the future, or prove
  -- it from univalence.
  D-coind : ∀ {S} {x y : D S} → force x == force y → x == y

D-coind2 : ∀ {S} {x y : D S} → D (force x == force y) → x == y
D-coind2 p = D-coind (force p
-}

module _ where
  private
    mutual
      data #D (A : Set) (P : Set) : Set where
        #p : #D-aux A P → (Unit → Unit) → #D A P

      data #D-aux (A : Set) (P : Set) : Set where
        #now : A → #D-aux A P
        #later : P → #D-aux A P

  D : Set → Set → Set
  D A X = #D A X

  now : ∀ {A X} → A → D A X
  now a = #p (#now a) _

  later : ∀ {A X} → X → D A X
  later x = #p (#later x) _

  D₁ : ∀ {A P₁ P₂} → (P₁ → P₂) → (D A P₁ → D A P₂)
  D₁ f (#p (#now a) _)   = now a
  D₁ f (#p (#later x) _) = later (f x)

  record P {i : Size} (A : Set) : Set where
    coinductive
    field
      #force : ∀ {j : Size< i} → D A (P {j} A)
  open P

  force : ∀ {A} → P A → D A (P A)
  force x = #force x

  P-intro : ∀ {A X : Set} → (X → D A X) → (X → P A)
  P-intro {A} {X} f = P-intro'
    where
      P-intro' : ∀ {i} → X → P {i} A
      #force (P-intro' x) {j} = D₁ (P-intro' {j}) (f x)

  postulate  -- HIT
    weak~ : ∀{A X : Set} → (force* : X → D A X) →
            (x : X) → (later x == force* x)

  -- | Extra module for recursion using sized types.
  -- This is convenient, as we can use the functor D in the definition, which
  -- in turn simplifies proofs.
  module DRec {A B : Set} {P' Y : Set}
    (now* : A → D B Y)
    (later* : P A → D B Y)
    (force* : Y → D B Y)
    (weak~* : (x : P A) → (later* x == force x))
    where
      f : D A P' → D B Y
      f = f-aux phantom where
        f-aux : Phantom weak~* → D A P' → D B Y
        f-aux phantom (#p (#now a) _)   = now* a
        f-aux phantom (#p (#later x) _) = later* x

      postulate      -- HIT
        weak~-β : (x : P') → ap f (weak~ force* x) == weak~* x

{-
  module PElim {A X} {S : D A X → Set}
    (now* : (a : A) → S (now a))
    (later* : (x : X) → S (later x))
    (force*₁ : (x : X) → D A X)
    (force*₂ : (x : X) → S (force*₁ x))
    (weak~* : (x : X) → -- (x_rec : S
              (later* x == (force*₂ x) [ S ↓ (weak~ force*₁ x) ]))
    where
      f : (x : D A X) → S x
      f = f-aux phantom
        where
          f-aux : Phantom weak~* → (x : D A X) → S x
          f-aux phantom (#p (#now a) _)   = now* a
          f-aux phantom (#p (#later x) _) = later* x
-}
--      postulate      -- HIT
--        weak~-β : (x : X) → apd f (weak~ force*₁ x) == weak~* x

{-
      weak~-β₂ : (x : ∞P A) →
                 apd f (weak~ x) == weak~* x (↑D₁ S f x)
                  -- transport (weak~* x) g-is-D₁f (↑D₁ S f x)
      weak~-β₂ = ?
-}

open DRec public renaming (f to D-rec)
{-
open PElim public
  renaming (f to P-elim; g to ∞P-elim; f-homomorphism to P-elim-hom;
           weak~-β to elim-weak~-β)

-}

module Bla where

⊥ : ∀ {A} → P A
⊥ = P-intro later unit

-- | Copairing of morphisms
[_,_] : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  (l : A → C) (r : B → C) → (x : Coprod A B) → C
[ f , g ] x = match x withl f withr g

id-D : ∀ {A} → D A (P A) → D A (P A)
id-D {A} = D-rec now later force (weak~ force)
           --(idf A) (idf (P A)) (λ x → force x) (weak~ (λ x → force x))

D₁-force : ∀ {A P₁ P₂} → (force* : P₁ → D A P₁) → (f : P₁ → P₂) → (x : P₁)
           → later (f x) == D₁ f (force* x)
D₁-force force* f x =
  later (f x)
    =⟨ idp ⟩
  D₁ f (later x)
    =⟨ weak~ force* x |in-ctx (D₁ f) ⟩
  D₁ f (force* x)
    ∎

-- | Direct definition of bind
bind : ∀ {A B} → (A → P B) → (P A → P B)
bind {A} {B} f x = P-intro {X = P A ⊔ P B} [ u , v ] (inl x)
  where
    elim-A : A → D B (P A ⊔ P B)
    elim-A a =
      D-rec now
            (later ∘ inr)
            (D₁ inr ∘ force)
            (D₁-force force inr)
            (force (f a))

    u : P A → D B (P A ⊔ P B)
    u x = D-rec
          elim-A
          (later ∘ inl)
          (later ∘ inl) -- this should be force ...
          (λ _ → idp)
          (force x)

    v : P B → D B (P A ⊔ P B)
    v = D₁ inr ∘ force

{-
-- | Copairing of morphisms
[_,_] : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  (l : A → C) (r : B → C) → (x : Coprod A B) → C
[ f , g ] x = match x withl f withr g

-- | Inverse of [now, later] à la Lambek,
-- given by extending id + D ([now, later]) : A ⊔ D(A ⊔ ∞P A) → A ⊔ ∞P A.
out : ∀ {A} → P A → A ⊔ ∞P A
out {A} = P-rec inl force (λ _ → idp)
    -- (inr ∘ D₁ [ now , later ]) resp-weak~
    where
      resp-weak~ : (x : D (A ⊔ ∞P A)) →
                   (inr ∘ D₁ [ now , later ]) x == force x
      resp-weak~ x =
        (inr ∘ D₁ [ now , later ]) x
          =⟨ {!!} ⟩
        inr (D₁ [ now , later ] x)
          =⟨ {!!} ⟩
        force x
          ∎

⊥' : ∀ {A} → ∞P A

⊥ : ∀ {A} → P A
⊥ = later (D-intro (λ _ → {!!}) unit)

force ⊥' = {!!} -- ⊥

-- | Action of P on morphisms
P₁ : ∀ {A B} → (A → B) → (P A → P B)
P₁ f = P-rec (now ∘ f) later weak~

-- | Unit for the monad
η : ∀ {A} → A → P A
η = now

-- | Monad multiplication
μ : ∀ {A} → P (P A) → P A
μ {A} = P-rec (idf (P A)) later weak~

-- | Direct definition of bind
bind : ∀ {A B} → (A → P B) → (P A → P B)
bind {A} {B} f = P-rec f later weak~

η-natural : ∀ {A B} → (f : A → B) →
            η ∘ f == P₁ f ∘ η
η-natural f = λ=-nondep (λ x → idp)
  where
n    open FunextNonDep

μ-natural : ∀ {A B} → (f : A → B) →
            μ ∘ P₁ (P₁ f) == P₁ f ∘ μ
μ-natural {A} f = λ=-nondep q
  where
    open FunextNonDep

    T : P (P A) → Set
    T x = μ ( P₁ (P₁ f) x) == P₁ f (μ x)

    =-later : (x : ∞P (P A)) → D (T (force x)) → T (later x)
    =-later x p = transport T (! (weak~ x)) (force p)

    r : (x : ∞P (P A)) → (p : D (T (force x))) →
        (=-later x p) == (force p) [ T ↓ (weak~ x) ]
    r x p = trans-↓ T (weak~ x) (force p)

    q : (x : P (P A)) → μ ( P₁ (P₁ f) x) == P₁ f (μ x)
    q = P-elim {S = λ x → μ ( P₁ (P₁ f) x) == P₁ f (μ x)}
        (λ a → idp) =-later r

-- | Termination predicate on P A
data _↓_ {A} (x : P A) : A → Set where
  now↓ : (a : A) → now a == x → x ↓ a
  later↓ : (a : A) → (u : ∞P A) → (later u == x) → (force u) ↓ a → x ↓ a

mutual
  -- | Weak bisimilarity proofs
  data ~proof {A} (x y : P A) : Set where
    terminating : (a : A) → x ↓ a → y ↓ a → ~proof x y
    -- A bit awkward, but otherwise we cannot pattern matching on ~proof
    step : (u v : ∞P A) → (later u == x) → (later v == y) → force u ~ force v →
           ~proof x y

  -- | Weak bisimilarity for P A
  record _~_ {A} (x y : P A) : Set where
    coinductive
    field
      out~ : ~proof x y
open _~_

terminate→=now : ∀{A} → (a : A) → (x : P A) → x ↓ a → now a == x
terminate→=now a x (now↓ .a na=x) = na=x
terminate→=now a x (later↓ .a u lu=x fu↓a) =
  now a
    =⟨ terminate→=now a (force u) fu↓a ⟩
  force u
    =⟨ ! (weak~ u) ⟩
  later u
    =⟨ lu=x ⟩
  x
    ∎

lemma : ∀{A} → (a : A) → (x y : P A) → x ↓ a → y ↓ a → x == y
lemma a x y x↓a y↓a =
  x
    =⟨ ! (terminate→=now a x x↓a) ⟩
  now a
    =⟨ terminate→=now a y y↓a ⟩
  y
    ∎

inr-inj : ∀ {i} {A B : Set i} →
          (x y : B) → Path {i} {A ⊔ B} (inr x) (inr y) → x == y
inr-inj x .x idp = idp

later-inj : ∀ {A} → (u v : ∞P A) → later u == later v → u == v
later-inj u v p = inr-inj u v lem
  where
    lem : inr u == inr v
    lem = transport (λ z → inr u == P-out z) {later u} {later v} p idp

-- | Weak bisimilarity implies equality for P A
~→= : ∀{A} → (x y : P A) → x ~ y → x == y
~→= {A} x y = P-elim {S = λ x' → x' ~ y → x' == y} now-= later-= weak~-= x
  where
    now-= : (a : A) → now a ~ y → now a == y
    now-= a p = lem (out~ p)
      where
        lem : ~proof (now a) y → now a == y
        lem (terminating b (now↓ .b nb=na) y↓b) =
          now a
            =⟨ ! nb=na ⟩
          now b
            =⟨ terminate→=now b y y↓b ⟩
          y
            ∎
        lem (terminating b (later↓ .b u () now_a↓b) y↓b)
        lem (step u v () x₂ x₃)

    later-= : (u : ∞P A) →
              D (force u ~ y → force u == y) → later u ~ y → later u == y
    later-= u p later_u~y = lem (out~ later_u~y)
      where
        lem : ~proof (later u) y → later u == y
        lem (terminating a later_u↓a y↓a) = lemma a (later u) y later_u↓a y↓a
        lem (step u' v later_u'=later_u later_v=y force_u'~force_v) =
          later u
            =⟨ weak~ u ⟩
          force u
            =⟨ force p force_u~y ⟩
          y ∎
          where
            force_u'=force_u : force u' == force u
            force_u'=force_u =
              force u'
                =⟨ later-inj u' u later_u'=later_u |in-ctx force ⟩
              force u
                ∎

            y=force_v : y == force v
            y=force_v =
              y
                =⟨ ! later_v=y ⟩
              later v
                =⟨ weak~ v ⟩
              force v
                ∎

            force_u~y : force u ~ y
            force_u~y = transport
                   (λ z → z ~ y)
                   force_u'=force_u
                   (transport! (λ z → force u' ~ z) y=force_v force_u'~force_v)

    weak~-= : (u : ∞P A) (p : D (force u ~ y → force u == y)) →
              (later-= u p)
                == (force p) [ (λ x' → x' ~ y → x' == y) ↓ (weak~ u) ]
    weak~-= u p = {!!}
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Group where

open import Cubical.Algebra.Group.Base public
open import Cubical.Algebra.Group.Properties public
open import Cubical.Algebra.Group.Morphism public
open import Cubical.Algebra.Group.MorphismProperties public
open import Cubical.Algebra.Group.Algebra public
open import Cubical.Algebra.Group.Action public
-- open import Cubical.Algebra.Group.Higher public
-- open import Cubical.Algebra.Group.EilenbergMacLane1 public
open import Cubical.Algebra.Group.Semidirect public
open import Cubical.Algebra.Group.Notation public

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --without-K #-}
module Sigma {a b} {A : Set a} {B : A → Set b} where

open import Equivalence
open import Types

-- Projections for the positive sigma.
π₁′ : (p : Σ′ A B) → A
π₁′ p = split (λ _ → A) (λ a _ → a) p

π₂′ : (p : Σ′ A B) → B (π₁′ p)
π₂′ p = split (λ p → B (π₁′ p)) (λ _ b → b) p

-- Induction principle for the negative sigma.
split′ : ∀ {p} (P : Σ A B → Set p)
  (f : (a : A) (b : B a) → P (a , b)) → ∀ z → P z
split′ P f p = f (π₁ p) (π₂ p)

Σ→Σ′ : Σ A B → Σ′ A B
Σ→Σ′ p = π₁ p , π₂ p

Σ′→Σ : Σ′ A B → Σ A B
Σ′→Σ = split _ _,_

Σ≃Σ′ : Σ A B ≃ Σ′ A B
Σ≃Σ′
  = Σ→Σ′
  , (Σ′→Σ , split
      (λ p → Σ→Σ′ (Σ′→Σ p) ≡ p)
      (λ _ _ → refl))
  , (Σ′→Σ , λ _ → refl)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


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

module Multidimensional.Data.NNat.Base where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Unit
open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.Data.Bool

open import Cubical.Relation.Nullary

open import Multidimensional.Data.Extra.Nat
open import Multidimensional.Data.Dir
open import Multidimensional.Data.DirNum

data N (r : ℕ) : Type₀ where
  bn : DirNum r → N r
  xr : DirNum r → N r → N r

-- should define induction principle for N r

-- we have 2ⁿ "unary" constructors, analogous to BNat with 2¹ (b0 and b1)
-- rename n to r
-- this likely introduces inefficiencies compared
-- to BinNat, with the max? check etc.
sucN : ∀ {n} → N n → N n
sucN {zero} (bn tt) = xr tt (bn tt)
sucN {zero} (xr tt x) = xr tt (sucN x)
sucN {suc n} (bn (↓ , ds)) = (bn (↑ , ds))
sucN {suc n} (bn (↑ , ds)) with max? ds
... | no _ = (bn (↓ , next ds))
... | yes _ = xr (zero-n (suc n)) (bn (one-n (suc n)))
sucN {suc n} (xr d x) with max? d
... | no _ = xr (next d) x
... | yes _ = xr (zero-n (suc n)) (sucN x)

sucnN : {r : ℕ} → (n : ℕ) → (N r → N r)
sucnN n = iter n sucN

doubleN : (r : ℕ) → N r → N r
doubleN zero (bn tt) = bn tt
doubleN zero (xr d x) = sucN (sucN (doubleN zero x))
doubleN (suc r) (bn x) with zero-n? x
... | yes _    = bn x
            -- bad:
... | no _ = caseBool (bn (doubleDirNum (suc r) x)) (xr (zero-n (suc r)) (bn x)) (doubleable-n? x)
-- ... | no _  | doubleable  = {!bn (doubleDirNum x)!}
-- ... | no _  | notdoubleable = xr (zero-n (suc r)) (bn x)
doubleN (suc r) (xr x x₁) = sucN (sucN (doubleN (suc r) x₁))

doublesN : (r : ℕ) → ℕ → N r → N r
doublesN r zero m = m
doublesN r (suc n) m = doublesN r n (doubleN r m)

N→ℕ : (r : ℕ) (x : N r) → ℕ
N→ℕ zero (bn tt) = zero
N→ℕ zero (xr tt x) = suc (N→ℕ zero x)
N→ℕ (suc r) (bn x) = DirNum→ℕ x
N→ℕ (suc r) (xr d x) = sucn (DirNum→ℕ d) (doublesℕ (suc r) (N→ℕ (suc r) x))

ℕ→N : (r : ℕ) → (n : ℕ) → N r
ℕ→N r zero = bn (zero-n r)
ℕ→N zero (suc n) = xr tt (ℕ→N zero n)
ℕ→N (suc r) (suc n) = sucN (ℕ→N (suc r) n)

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
{-# OPTIONS --safe #-}
module Cubical.Homotopy.HSpace where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.HLevels
open import Cubical.HITs.S1
open import Cubical.HITs.Sn

record HSpace {ℓ : Level} (A : Pointed ℓ) : Type ℓ where
  constructor HSp
  field
    μ : typ A → typ A → typ A
    μₗ : (x : typ A) → μ (pt A) x ≡ x
    μᵣ : (x : typ A) → μ x (pt A) ≡ x
    μₗᵣ : μₗ (pt A) ≡ μᵣ (pt A)

record AssocHSpace {ℓ : Level} {A : Pointed ℓ} (e : HSpace A) : Type ℓ where
  constructor AssocHSp
  field
    μ-assoc : (x y z : _)
      → HSpace.μ e (HSpace.μ e x y) z ≡ HSpace.μ e x (HSpace.μ e y z)

    μ-assoc-filler : (y z : typ A)
      → PathP (λ i → HSpace.μ e (HSpace.μₗ e y i) z
                    ≡ HSpace.μₗ e (HSpace.μ e y z) i)
               (μ-assoc (pt A) y z)
               refl

-- Instances
open HSpace
open AssocHSpace

-- S¹
S1-HSpace : HSpace (S₊∙ 1)
μ S1-HSpace = _·_
μₗ S1-HSpace x = refl
μᵣ S1-HSpace base = refl
μᵣ S1-HSpace (loop i) = refl
μₗᵣ S1-HSpace x = refl

S1-AssocHSpace : AssocHSpace S1-HSpace
μ-assoc S1-AssocHSpace base _ _ = refl
μ-assoc S1-AssocHSpace (loop i) x y j = h x y j i
  where
  h : (x y : S₊ 1) → cong (_· y) (rotLoop x) ≡ rotLoop (x · y)
  h = wedgeconFun _ _ (λ _ _ → isOfHLevelPath 2 (isGroupoidS¹ _ _) _ _)
        (λ x → refl)
        (λ { base → refl ; (loop i) → refl})
        refl
μ-assoc-filler S1-AssocHSpace _ _ = refl

max_stars_repo_name: FernandoLarrain/cubical


text:
module Prelude.Equality.Unsafe where

open import Prelude.Equality
open import Prelude.Empty
open import Prelude.Erased

open import Agda.Builtin.TrustMe

-- unsafeEqual {x = x} {y = y} evaluates to refl if x and y are
-- definitionally equal.
unsafeEqual : ∀ {a} {A : Set a} {x y : A} → x ≡ y
unsafeEqual = primTrustMe

{-# DISPLAY primTrustMe = [erased] #-}

-- Used in decidable equality for primitive types (String, Char and Float)
unsafeNotEqual : ∀ {a} {A : Set a} {x y : A} → ¬ (x ≡ y)
unsafeNotEqual _ = erase-⊥ trustme
  where postulate trustme : ⊥

-- Erase an equality proof. Throws away the actual proof
-- and replaces it by unsafeEqual.
eraseEquality : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y
eraseEquality _ = unsafeEqual

unsafeCoerce : ∀ {a} {A : Set a} {B : Set a} → A → B
unsafeCoerce {A = A} {B} x with unsafeEqual {x = A} {y = B}
unsafeCoerce x | refl = x

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

module Definition.Conversion.Lift where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.Conversion
open import Definition.Conversion.Whnf
open import Definition.Conversion.Soundness
open import Definition.Conversion.Weakening
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Fundamental.Reducibility
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Reduction

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Lifting of algorithmic equality of types from WHNF to generic types.
liftConv : ∀ {A B Γ}
          → Γ ⊢ A [conv↓] B
          → Γ ⊢ A [conv↑] B
liftConv A<>B =
  let ⊢A , ⊢B = syntacticEq (soundnessConv↓ A<>B)
      whnfA , whnfB = whnfConv↓ A<>B
  in  [↑] _ _ (id ⊢A) (id ⊢B) whnfA whnfB A<>B

-- Lifting of algorithmic equality of terms from WHNF to generic terms.
liftConvTerm : ∀ {t u A Γ}
             → Γ ⊢ t [conv↓] u ∷ A
             → Γ ⊢ t [conv↑] u ∷ A
liftConvTerm t<>u =
  let ⊢A , ⊢t , ⊢u = syntacticEqTerm (soundnessConv↓Term t<>u)
      whnfA , whnfT , whnfU = whnfConv↓Term t<>u
  in  [↑]ₜ _ _ _ (id ⊢A) (id ⊢t) (id ⊢u) whnfA whnfT whnfU t<>u

mutual
  -- Helper function for lifting from neutrals to generic terms in WHNF.
  lift~toConv↓′ : ∀ {t u A A′ Γ l}
                → Γ ⊩⟨ l ⟩ A′
                → Γ ⊢ A′ ⇒* A
                → Γ ⊢ t ~ u ↓ A
                → Γ ⊢ t [conv↓] u ∷ A
  lift~toConv↓′ (Uᵣ′ .⁰ 0<1 ⊢Γ) D ([~] A D₁ whnfB k~l)
                rewrite PE.sym (whnfRed* D Uₙ) =
    let _ , ⊢t , ⊢u = syntacticEqTerm (conv (soundness~↑ k~l) (subset* D₁))
    in  univ ⊢t ⊢u (ne ([~] A D₁ Uₙ k~l))
  lift~toConv↓′ (ℕᵣ D) D₁ ([~] A D₂ whnfB k~l)
                rewrite PE.sym (whrDet* (red D , ℕₙ) (D₁ , whnfB)) =
    ℕ-ins ([~] A D₂ ℕₙ k~l)
  lift~toConv↓′ (Emptyᵣ D) D₁ ([~] A D₂ whnfB k~l)
                rewrite PE.sym (whrDet* (red D , Emptyₙ) (D₁ , whnfB)) =
    Empty-ins ([~] A D₂ Emptyₙ k~l)
  lift~toConv↓′ (Unitᵣ D) D₁ ([~] A D₂ whnfB k~l)
                rewrite PE.sym (whrDet* (red D , Unitₙ) (D₁ , whnfB)) =
    Unit-ins ([~] A D₂ Unitₙ k~l)
  lift~toConv↓′ (ne′ K D neK K≡K) D₁ ([~] A D₂ whnfB k~l)
                rewrite PE.sym (whrDet* (red D , ne neK) (D₁ , whnfB)) =
    let _ , ⊢t , ⊢u = syntacticEqTerm (soundness~↑ k~l)
        A≡K = subset* D₂
    in  ne-ins (conv ⊢t A≡K) (conv ⊢u A≡K) neK ([~] A D₂ (ne neK) k~l)
  lift~toConv↓′ (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) D₁ ([~] A D₂ whnfB k~l)
                rewrite PE.sym (whrDet* (red D , Πₙ) (D₁ , whnfB)) =
    let ⊢ΠFG , ⊢t , ⊢u = syntacticEqTerm (soundness~↓ ([~] A D₂ Πₙ k~l))
        ⊢F , ⊢G = syntacticΠ ⊢ΠFG
        neT , neU = ne~↑ k~l
        ⊢Γ = wf ⊢F
        var0 = neuTerm ([F] (step id) (⊢Γ ∙ ⊢F)) (var 0) (var (⊢Γ ∙ ⊢F) here)
                       (refl (var (⊢Γ ∙ ⊢F) here))
        0≡0 = lift~toConv↑′ ([F] (step id) (⊢Γ ∙ ⊢F)) (var-refl (var (⊢Γ ∙ ⊢F) here) PE.refl)
        k∘0≡l∘0 = lift~toConv↑′ ([G] (step id) (⊢Γ ∙ ⊢F) var0)
                                (app-cong (wk~↓ (step id) (⊢Γ ∙ ⊢F) ([~] A D₂ Πₙ k~l))
                                          0≡0)
    in  η-eq ⊢t ⊢u (ne neT) (ne neU)
             (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ x)
                       (wkSingleSubstId _)
                       k∘0≡l∘0)
  lift~toConv↓′ (Σᵣ′ F G D ⊢F ⊢G Σ≡Σ [F] [G] G-ext) D₁ ([~] A″ D₂ whnfA t~u)
                rewrite PE.sym (whrDet* (red D , Σₙ) (D₁ , whnfA)) {- Σ F ▹ G ≡ A -} =
    let neT , neU = ne~↑ t~u
        t~u↓ = [~] A″ D₂ Σₙ t~u
        ⊢ΣFG , ⊢t , ⊢u = syntacticEqTerm (soundness~↓ t~u↓)
        ⊢F , ⊢G = syntacticΣ ⊢ΣFG
        ⊢Γ = wf ⊢F

        wkId = wk-id F
        wkLiftId = PE.cong (λ x → x [ fst _ ]) (wk-lift-id G)

        wk[F] = [F] id ⊢Γ
        wk⊢fst = PE.subst (λ x → _ ⊢ _ ∷ x) (PE.sym wkId) (fstⱼ ⊢F ⊢G ⊢t)
        wkfst≡ = PE.subst (λ x → _ ⊢ _ ≡ _ ∷ x) (PE.sym wkId) (fst-cong ⊢F ⊢G (refl ⊢t))
        wk[fst] = neuTerm wk[F] (fstₙ neT) wk⊢fst wkfst≡
        wk[Gfst] = [G] id ⊢Γ wk[fst]

        wkfst~ = PE.subst (λ x → _ ⊢ _ ~ _ ↑ x) (PE.sym wkId) (fst-cong t~u↓)
        wksnd~ = PE.subst (λ x → _ ⊢ _ ~ _ ↑ x) (PE.sym wkLiftId) (snd-cong t~u↓)
    in  Σ-η ⊢t ⊢u (ne neT) (ne neU)
            (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ x) wkId
                      (lift~toConv↑′ wk[F] wkfst~))
            (PE.subst (λ x → _ ⊢ _ [conv↑] _ ∷ x) wkLiftId
                      (lift~toConv↑′ wk[Gfst] wksnd~))
  lift~toConv↓′ (emb 0<1 [A]) D t~u = lift~toConv↓′ [A] D t~u

  -- Helper function for lifting from neutrals to generic terms.
  lift~toConv↑′ : ∀ {t u A Γ l}
                → Γ ⊩⟨ l ⟩ A
                → Γ ⊢ t ~ u ↑ A
                → Γ ⊢ t [conv↑] u ∷ A
  lift~toConv↑′ [A] t~u =
    let B , whnfB , D = whNorm′ [A]
        t~u↓ = [~] _ (red D) whnfB t~u
        neT , neU = ne~↑ t~u
        _ , ⊢t , ⊢u = syntacticEqTerm (soundness~↓ t~u↓)
    in  [↑]ₜ _ _ _ (red D) (id ⊢t) (id ⊢u) whnfB
             (ne neT) (ne neU) (lift~toConv↓′ [A] (red D) t~u↓)

-- Lifting of algorithmic equality of terms from neutrals to generic terms in WHNF.
lift~toConv↓ : ∀ {t u A Γ}
             → Γ ⊢ t ~ u ↓ A
             → Γ ⊢ t [conv↓] u ∷ A
lift~toConv↓ ([~] A₁ D whnfB k~l) =
  lift~toConv↓′ (reducible (proj₁ (syntacticRed D))) D ([~] A₁ D whnfB k~l)

-- Lifting of algorithmic equality of terms from neutrals to generic terms.
lift~toConv↑ : ∀ {t u A Γ}
             → Γ ⊢ t ~ u ↑ A
             → Γ ⊢ t [conv↑] u ∷ A
lift~toConv↑ t~u =
  lift~toConv↑′ (reducible (proj₁ (syntacticEqTerm (soundness~↑ t~u)))) t~u


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

open import Types
open import Functions

module Paths where

-- Identity type
infix 4 _≡_  -- \equiv

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

_==_ = _≡_

_≢_ : ∀ {i} {A : Set i} → (A → A → Set i)
x ≢ y = ¬ (x ≡ y)

-- -- This should not be provable
-- K : {A : Set} → (x : A) → (p : x ≡ x) → p ≡ refl x
-- K .x (refl x) = refl

-- Composition and opposite of paths

infixr 8 _∘_  -- \o

_∘_ : ∀ {i} {A : Set i} {x y z : A} → (x ≡ y → y ≡ z → x ≡ z)
refl ∘ q = q

-- Composition with the opposite definitional behaviour
_∘'_ : ∀ {i} {A : Set i} {x y z : A} → (x ≡ y → y ≡ z → x ≡ z)
q ∘' refl = q

! : ∀ {i} {A : Set i} {x y : A} → (x ≡ y → y ≡ x)
! refl = refl

-- Equational reasoning combinator

infix  2 _∎
infixr 2 _≡⟨_⟩_

_≡⟨_⟩_ : ∀ {i} {A : Set i} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ p1 ⟩ p2 = p1 ∘ p2

_∎ : ∀ {i} {A : Set i} (x : A) → x ≡ x
_∎ _ = refl

-- Obsolete, for retrocompatibility only
infixr 2 _≡⟨_⟩∎_
_≡⟨_⟩∎_ : ∀ {i} {A : Set i} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
_≡⟨_⟩∎_ = _≡⟨_⟩_

-- Transport and ap

ap : ∀ {i j} {A : Set i} {B : Set j} (f : A → B) {x y : A}
  → (x ≡ y → f x ≡ f y)
ap f refl = refl

-- Make equational reasoning much more readable
syntax ap f p = p |in-ctx f

transport : ∀ {i j} {A : Set i} (P : A → Set j) {x y : A}
  → (x ≡ y → P x → P y)
transport P refl t = t

apd : ∀ {i j} {A : Set i} {P : A → Set j} (f : (a : A) → P a) {x y : A}
  → (p : x ≡ y) → transport P p (f x) ≡ f y
apd f refl = refl

apd! : ∀ {i j} {A : Set i} {P : A → Set j} (f : (a : A) → P a) {x y : A}
  → (p : x ≡ y) → f x ≡ transport P (! p) (f y)
apd! f refl = refl

-- Paths in Sigma types

module _ {i j} {A : Set i} {P : A → Set j} where

  ap2 : ∀ {k} {Q : Set k} (f : (a : A) → P a → Q)
    {x y : A} (p : x ≡ y) {u : P x} {v : P y}
    (q : transport P p u ≡ v) → f x u ≡ f y v
  ap2 f refl refl = refl

  Σ-eq : {x y : A} (p : x ≡ y) {u : P x} {v : P y}
    (q : transport P p u ≡ v) → (x , u) ≡ (y , v)
  Σ-eq = ap2 _,_

  -- Same as [Σ-eq] but with only one argument
  total-Σ-eq : {xu yv : Σ A P}
    (q : Σ (π₁ xu ≡ π₁ yv) (λ p → transport P p (π₂ xu) ≡ (π₂ yv)))
    → xu ≡ yv
  total-Σ-eq (p , q) = Σ-eq p q

  base-path : {x y : Σ A P} (p : x ≡ y) → π₁ x ≡ π₁ y
  base-path = ap π₁

  trans-base-path : {x y : Σ A P} (p : x ≡ y)
    → transport P (base-path p) (π₂ x) ≡ π₂ y
  trans-base-path {_} {._} refl = refl

  fiber-path : {x y : Σ A P} (p : x ≡ y)
    → transport P (base-path p) (π₂ x) ≡ π₂ y
  fiber-path {x} {.x} refl = refl

  abstract
    base-path-Σ-eq : {x y : A} (p : x ≡ y) {u : P x} {v : P y}
      (q : transport P p u ≡ v) → base-path (Σ-eq p q) ≡ p
    base-path-Σ-eq refl refl = refl

    fiber-path-Σ-eq : {x y : A} (p : x ≡ y) {u : P x} {v : P y}
      (q : transport P p u ≡ v)
      → transport (λ t → transport P t u ≡ v) (base-path-Σ-eq p q)
                  (fiber-path (Σ-eq p q))
        ≡ q
    fiber-path-Σ-eq refl refl = refl

    Σ-eq-base-path-fiber-path : {x y : Σ A P} (p : x ≡ y)
      → Σ-eq (base-path p) (fiber-path p) ≡ p
    Σ-eq-base-path-fiber-path {x} {.x} refl = refl

-- Some of the ∞-groupoid structure

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

  concat-assoc : {x y z t : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ t)
    → (p ∘ q) ∘ r ≡ p ∘ (q ∘ r)
  concat-assoc refl _ _ = refl

  -- [refl-left-unit] for _∘_ and [refl-right-unit] for _∘'_ are definitional

  refl-right-unit : {x y : A} (q : x ≡ y) → q ∘ refl ≡ q
  refl-right-unit refl = refl

  refl-left-unit : {x y : A} (q : x ≡ y) → refl ∘' q ≡ q
  refl-left-unit refl = refl

  opposite-left-inverse : {x y : A} (p : x ≡ y) → (! p) ∘ p ≡ refl
  opposite-left-inverse refl = refl

  opposite-right-inverse : {x y : A} (p : x ≡ y) → p ∘ (! p) ≡ refl
  opposite-right-inverse refl = refl

  -- This is useless in the presence of ap & equation reasioning combinators
  whisker-left : {x y z : A} (p : x ≡ y) {q r : y ≡ z}
    → (q ≡ r → p ∘ q ≡ p ∘ r)
  whisker-left p refl = refl

  -- This is useless in the presence of ap & equation reasioning combinators
  whisker-right : {x y z : A} (p : y ≡ z) {q r : x ≡ y}
    → (q ≡ r → q ∘ p ≡ r ∘ p)
  whisker-right p refl = refl

  anti-whisker-right : {x y z : A} (p : y ≡ z) {q r : x ≡ y}
    → (q ∘ p ≡ r ∘ p → q ≡ r)
  anti-whisker-right refl {q} {r} h =
    ! (refl-right-unit q) ∘ (h ∘ refl-right-unit r)

  anti-whisker-left : {x y z : A} (p : x ≡ y) {q r : y ≡ z}
    → (p ∘ q ≡ p ∘ r → q ≡ r)
  anti-whisker-left refl h = h

  -- [opposite-concat …] gives a result of the form [opposite (concat …) ≡ …],
  -- and so on
  opposite-concat : {x y z : A} (p : x ≡ y) (q : y ≡ z) → ! (p ∘ q) ≡ ! q ∘ ! p
  opposite-concat refl q = ! (refl-right-unit (! q))

  concat-opposite : {x y z : A} (q : y ≡ z) (p : x ≡ y) → ! q ∘ ! p ≡ ! (p ∘ q)
  concat-opposite q refl = refl-right-unit (! q)

  opposite-opposite : {x y : A} (p : x ≡ y) → ! (! p) ≡ p
  opposite-opposite refl = refl

-- Reduction rules for transport

module _ {i} {A : Set i} where
  -- This first part is about transporting something in a known fibration. In
  -- the names, [x] represents the variable of the fibration, [a] is a constant
  -- term, [A] is a constant type, and [f] and [g] are constant functions.

  trans-id≡cst : {a b c : A} (p : b ≡ c) (q : b ≡ a)
    → transport (λ x → x ≡ a) p q ≡ (! p) ∘ q
  trans-id≡cst refl q = refl

  trans-cst≡id : {a b c : A} (p : b ≡ c) (q : a ≡ b)
    → transport (λ x → a ≡ x) p q ≡ q ∘ p
  trans-cst≡id refl q = ! (refl-right-unit q)

  trans-app≡app : ∀ {j} {B : Set j} (f g : A → B) {x y : A} (p : x ≡ y)
    (q : f x ≡ g x)
    → transport (λ x → f x ≡ g x) p q ≡ ! (ap f p) ∘ (q ∘ ap g p)
  trans-app≡app f g refl q = ! (refl-right-unit q)

  trans-move-app≡app : ∀ {j} {B : Set j} (f g : A → B) {x y : A} (p : x ≡ y)
    (q : f x ≡ g x) {r : f y ≡ g y}
    → (q ∘ ap g p ≡ ap f p ∘ r → transport (λ x → f x ≡ g x) p q ≡ r)
  trans-move-app≡app f g refl q h = ! (refl-right-unit q) ∘ h

  trans-cst≡app : ∀ {j} {B : Set j} (a : B) (f : A → B) {x y : A} (p : x ≡ y)
    (q : a ≡ f x)
    → transport (λ x → a ≡ f x) p q ≡ q ∘ ap f p
  trans-cst≡app a f refl q = ! (refl-right-unit q)

  trans-app≡cst : ∀ {j} {B : Set j} (f : A → B) (a : B) {x y : A} (p : x ≡ y)
    (q : f x ≡ a)
    → transport (λ x → f x ≡ a) p q ≡ ! (ap f p) ∘ q
  trans-app≡cst f a refl q = refl

  trans-id≡app : (f : A → A) {x y : A} (p : x ≡ y) (q : x ≡ f x)
    → transport (λ x → x ≡ f x) p q ≡ ! p ∘ (q ∘ ap f p)
  trans-id≡app f refl q = ! (refl-right-unit q)

  trans-app≡id : (f : A → A) {x y : A} (p : x ≡ y) (q : f x ≡ x)
    → transport (λ x → f x ≡ x) p q ≡ ! (ap f p) ∘ (q ∘ p)
  trans-app≡id f refl q = ! (refl-right-unit q)

  trans-id≡id : {x y : A} (p : x ≡ y) (q : x ≡ x)
    → transport (λ x → x ≡ x) p q ≡ ! p ∘ (q ∘ p)
  trans-id≡id refl q = ! (refl-right-unit _)

  trans-cst : ∀ {j} {B : Set j} {x y : A} (p : x ≡ y) (q : B)
    → transport (λ _ → B) p q ≡ q
  trans-cst refl q = refl

  trans-Π2 : ∀ {j k} (B : Set j) (P : (x : A) (y : B) → Set k)
    {b c : A} (p : b ≡ c) (q : (y : B) → P b y) (a : B)
    → transport (λ x → ((y : B) → P x y)) p q a
      ≡ transport (λ u → P u a) p (q a)
  trans-Π2 B P refl q a = refl

  trans-Π2-dep : ∀ {j k} (B : A → Set j) (P : (x : A) (y : B x) → Set k)
    {a₁ a₂ : A} (p : a₁ ≡ a₂) (q : (y : B a₁) → P a₁ y) (b : B a₂)
    → transport (λ x → ((y : B x) → P x y)) p q b
      ≡ transport (uncurry P) (! (Σ-eq (! p) $ refl)) (q (transport B (! p) b))
  trans-Π2-dep B P refl q b = refl

  trans-→-trans : ∀ {j k} (B : A → Set j) (P : A → Set k)
    {b c : A} (p : b ≡ c) (q : B b → P b) (a : B b)
    → transport (λ x → B x → P x) p q (transport B p a)
      ≡ transport P p (q a)
  trans-→-trans B P refl q a = refl

  trans-→ : ∀ {j k} (B : A → Set j) (P : A → Set k)
    {b c : A} (p : b ≡ c) (q : B b → P b) (a : B c)
    → transport (λ x → B x → P x) p q a
      ≡ transport P p (q $ transport B (! p) a)
  trans-→ B P refl q a = refl

  -- This second part is about transporting something along a known path

  trans-diag : ∀ {j} (P : A → A → Set j) {x y : A} (p : x ≡ y) (q : P x x)
    → transport (λ x → P x x) p q ≡ transport (λ z → P z y) p (transport (P x) p q)
  trans-diag P refl q = refl

  trans-concat : ∀ {j} (P : A → Set j) {x y z : A} (p : y ≡ z) (q : x ≡ y)
    (u : P x)
    → transport P (q ∘ p) u ≡ transport P p (transport P q u)
  trans-concat P p refl u = refl

  compose-trans : ∀ {j} (P : A → Set j) {x y z : A} (p : y ≡ z) (q : x ≡ y)
    (u : P x)
    →  transport P p (transport P q u) ≡ transport P (q ∘ p) u
  compose-trans P p refl u = refl

  trans-ap : ∀ {j k} {B : Set j} (P : B → Set k) (f : A → B)
    {x y : A} (p : x ≡ y) (u : P (f x))
    → transport P (ap f p) u ≡ transport (P ◯ f) p u
  trans-ap P f refl u = refl

  -- Unreadable, should be removed
  trans-totalpath : ∀ {j k} (P : A → Set j) (Q : Σ A P → Set k) {x y : Σ A P}
    (p : π₁ x ≡ π₁ y) (q : transport P p (π₂ x) ≡ π₂ y)
    (f : (t : P (π₁ x)) → Q (π₁ x , t))
    → transport Q (Σ-eq p q) (f (π₂ x)) ≡
        transport (λ x' → Q (π₁ y , x')) q
          (transport (λ x' → (t : P x') → Q (x' , t)) p f
            (transport P p (π₂ x)))
  trans-totalpath P Q {(x₁ , x₂)} {(y₁ , y₂)} p q f =
    trans-totalpath' P Q {x₁} {y₁} {x₂} {y₂} p q f where

    trans-totalpath' : ∀ {j k} (P : A → Set j) (Q : Σ A P → Set k) {x₁ y₁ : A}
      {x₂ : P x₁} {y₂ : P y₁}
      (p : x₁ ≡ y₁) (q : transport P p (x₂) ≡ y₂) (f : (t : P x₁) → Q (x₁ , t))
      → transport Q (Σ-eq p q) (f x₂) ≡
          transport (λ x' → Q (y₁ , x')) q
            (transport (λ x' → (t : P x') → Q (x' , t)) p f
              (transport P p x₂))
    trans-totalpath' P Q refl refl f = refl

  -- This third part is about various other convenient properties

  trans-trans-opposite : ∀ {j} (P : A → Set j) {x y : A} (p : x ≡ y) (u : P y)
    → transport P p (transport P (! p) u) ≡ u
  trans-trans-opposite P refl u = refl

  trans-opposite-trans : ∀ {j} (P : A → Set j) {x y : A} (p : x ≡ y) (u : P x)
    → transport P (! p) (transport P p u) ≡ u
  trans-opposite-trans P refl u = refl

  ap-dep-trivial : ∀ {j} {B : Set j} (f : A → B) {x y : A} (p : x ≡ y)
    → ap f p ≡ ! (trans-cst p (f x)) ∘ apd f p
  ap-dep-trivial f refl = refl

  homotopy-naturality : ∀ {j} {B : Set j} (f g : A → B)
    (p : (x : A) → f x ≡ g x) {x y : A} (q : x ≡ y)
    → ap f q ∘ p y ≡ p x ∘ ap g q
  homotopy-naturality f g p refl = ! (refl-right-unit _)

  homotopy-naturality-toid : (f : A -> A) (p : (x : A) → f x ≡ x)
    {x y : A} (q : x ≡ y) → ap f q ∘ p y ≡ p x ∘ q
  homotopy-naturality-toid f p refl = ! (refl-right-unit _)

  homotopy-naturality-fromid : (g : A -> A) (p : (x : A) → x ≡ g x)
    {x y : A} (q : x ≡ y) → q ∘ p y ≡ p x ∘ ap g q
  homotopy-naturality-fromid g p refl = ! (refl-right-unit _)

  opposite-ap : ∀ {j} {B : Set j} (f : A → B) {x y : A} (p : x ≡ y)
    → ! (ap f p) ≡ ap f (! p)
  opposite-ap f refl = refl

  ap-opposite : ∀ {j} {B : Set j} (f : A → B) {x y : A} (p : x ≡ y)
    → ap f (! p) ≡ ! (ap f p)
  ap-opposite f refl = refl

  concat-ap : ∀ {j} {B : Set j} (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
    → ap f p ∘ ap f q ≡ ap f (p ∘ q)
  concat-ap f refl _ = refl

  ap-concat : ∀ {j} {B : Set j} (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
    → ap f (p ∘ q) ≡ ap f p ∘ ap f q
  ap-concat f refl _ = refl

  compose-ap : ∀ {j k} {B : Set j} {C : Set k} (g : B → C) (f : A → B)
    {x y : A} (p : x ≡ y) → ap g (ap f p) ≡ ap (g ◯ f) p
  compose-ap f g refl = refl

  ap-compose : ∀ {j k} {B : Set j} {C : Set k} (g : B → C) (f : A → B)
    {x y : A} (p : x ≡ y) → ap (g ◯ f) p ≡ ap g (ap f p)
  ap-compose f g refl = refl

  ap-cst : ∀ {j} {B : Set j} (b : B) {x y : A} (p : x ≡ y)
    → ap (cst b) p ≡ refl
  ap-cst b refl = refl

  ap-id : {u v : A} (p : u ≡ v) → ap (id A) p ≡ p
  ap-id refl = refl

  app-trans : ∀ {j k} (B : A → Set j) (C : A → Set k) (f : ∀ x → B x → C x)
    {x y} (p : x ≡ y) (a : B x)
    → f y (transport B p a) ≡ transport C p (f x a)
  app-trans B C f refl a = refl

  -- Move functions
  -- These functions are used when the goal is to show that path is a
  -- concatenation of two other paths, and that you want to prove it by moving a
  -- path to the other side
  --
  -- The first [left/right] is the side (with respect to ≡) where will be the
  -- path after moving (“after” means “after replacing the conclusion of the
  -- proposition by its premisse”), and the second [left/right] is the side
  -- (with respect to ∘) where the path is (and will still be)
  -- If you want to prove something of the form [p ≡ q ∘ r] by moving [q] or [r]
  -- to the left,  use the functions move-left-on-left  and move-left-on-right
  -- If you want to prove something of the form [p ∘ q ≡ r] by moving [p] or [q]
  -- to the right, use the functions move-right-on-left and move-right-on-right
  -- Add a [0] after [move] if the big path is constant, a [1] if the other
  -- small path is constant and then a [!] if the path you will move is an
  -- opposite.
  --
  -- I’m not sure all of these functions are useful, but it can’t hurt to have
  -- them.

  move-left-on-left : {x y z : A} (p : x ≡ z) (q : x ≡ y) (r : y ≡ z)
    → ((! q) ∘ p ≡ r → p ≡ q ∘ r)
  move-left-on-left p refl r h = h

  move-left-on-right : {x y z : A} (p : x ≡ z) (q : x ≡ y) (r : y ≡ z)
    → (p ∘ (! r) ≡ q → p ≡ q ∘ r)
  move-left-on-right p q refl h = ! (refl-right-unit p)
                                      ∘ (h ∘ ! (refl-right-unit q))

  move-right-on-left : {x y z : A} (p : x ≡ y) (q : y ≡ z) (r : x ≡ z)
    → (q ≡ (! p) ∘ r → p ∘ q ≡ r)
  move-right-on-left refl q r h = h

  move-right-on-right : {x y z : A} (p : x ≡ y) (q : y ≡ z) (r : x ≡ z)
    → (p ≡ r ∘ (! q) → p ∘ q ≡ r)
  move-right-on-right p refl r h = refl-right-unit p
                                       ∘ (h ∘ refl-right-unit r)

  move!-left-on-left : {x y z : A} (p : x ≡ z) (q : y ≡ x) (r : y ≡ z)
    → (q ∘ p ≡ r → p ≡ (! q) ∘ r)
  move!-left-on-left p refl r h = h

  move!-left-on-right : {x y z : A} (p : x ≡ z) (q : x ≡ y) (r : z ≡ y)
    → (p ∘ r ≡ q → p ≡ q ∘ (! r))
  move!-left-on-right p q refl h = ! (refl-right-unit p)
                                       ∘ (h ∘ ! (refl-right-unit q))

  move!-right-on-left : {x y z : A} (p : y ≡ x) (q : y ≡ z) (r : x ≡ z)
    → (q ≡ p ∘ r → (! p) ∘ q ≡ r)
  move!-right-on-left refl q r h = h

  move!-right-on-right : {x y z : A} (p : x ≡ y) (q : z ≡ y) (r : x ≡ z)
    → (p ≡ r ∘ q → p ∘ (! q) ≡ r)
  move!-right-on-right p refl r h = refl-right-unit p
                                        ∘ (h ∘ refl-right-unit r)

  move0-left-on-left : {x y : A} (q : x ≡ y) (r : y ≡ x)
    → (! q ≡ r → refl ≡ q ∘ r)
  move0-left-on-left refl r h = h

  move0-left-on-right : {x y : A} (q : x ≡ y) (r : y ≡ x)
    → (! r ≡ q → refl ≡ q ∘ r)
  move0-left-on-right q refl h = h ∘ ! (refl-right-unit q)

  move0-right-on-left : {x y : A} (p : x ≡ y) (q : y ≡ x)
    → (q ≡ ! p → p ∘ q ≡ refl)
  move0-right-on-left refl q h = h

  move0-right-on-right : {x y : A} (p : x ≡ y) (q : y ≡ x)
    → (p ≡ ! q → p ∘ q ≡ refl)
  move0-right-on-right p refl h = refl-right-unit p ∘ h

  move0!-left-on-left : {x y : A} (q : y ≡ x) (r : y ≡ x)
    → (q ≡ r → refl ≡ (! q) ∘ r)
  move0!-left-on-left refl r h = h

  move0!-left-on-right : {x y : A} (q : x ≡ y) (r : x ≡ y)
    → (r ≡ q → refl ≡ q ∘ (! r))
  move0!-left-on-right q refl h = h ∘ ! (refl-right-unit q)

  move0!-right-on-left : {x y : A} (p : y ≡ x) (q : y ≡ x)
    → (q ≡ p → (! p) ∘ q ≡ refl)
  move0!-right-on-left refl q h = h

  move0!-right-on-right : {x y : A} (p : x ≡ y) (q : x ≡ y)
    → (p ≡ q → p ∘ (! q) ≡ refl)
  move0!-right-on-right p refl h = refl-right-unit p ∘ h

  move1-left-on-left : {x y : A} (p : x ≡ y) (q : x ≡ y)
    → ((! q) ∘ p ≡ refl → p ≡ q)
  move1-left-on-left p refl h = h

  move1-left-on-right : {x y : A} (p : x ≡ y) (r : x ≡ y)
    → (p ∘ (! r) ≡ refl → p ≡ r)
  move1-left-on-right p refl h = ! (refl-right-unit p) ∘ h

  move1-right-on-left : {x y : A} (p : x ≡ y) (r : x ≡ y)
    → (refl ≡ (! p) ∘ r → p ≡ r)
  move1-right-on-left refl r h = h

  move1-right-on-right : {x y : A} (q : x ≡ y) (r : x ≡ y)
    → (refl ≡ r ∘ (! q) → q ≡ r)
  move1-right-on-right refl r h = h ∘ refl-right-unit r

  move1!-left-on-left : {x y : A} (p : x ≡ y) (q : y ≡ x)
    → (q ∘ p ≡ refl → p ≡ ! q)
  move1!-left-on-left p refl h = h

  move1!-left-on-right : {x y : A} (p : x ≡ y) (r : y ≡ x)
    → (p ∘ r ≡ refl → p ≡ ! r)
  move1!-left-on-right p refl h = ! (refl-right-unit p) ∘ h

  move1!-right-on-left : {x y : A} (p : y ≡ x) (r : x ≡ y)
    → (refl ≡ p ∘ r → ! p ≡ r)
  move1!-right-on-left refl r h = h

  move1!-right-on-right : {x y : A} (q : y ≡ x) (r : x ≡ y)
    → (refl ≡ r ∘ q → ! q ≡ r)
  move1!-right-on-right refl r h = h ∘ refl-right-unit r

  move-transp-left : ∀ {j} (P : A → Set j) {x y : A} (u : P y) (p : x ≡ y)
    (v : P x)
    → transport P (! p) u ≡ v → u ≡ transport P p v
  move-transp-left P _ refl _ p = p

  move-transp-right : ∀ {j} (P : A → Set j) {x y : A} (p : y ≡ x) (u : P y)
    (v : P x)
    → u ≡ transport P (! p) v → transport P p u ≡ v
  move-transp-right P refl _ _ p = p

  move!-transp-left : ∀ {j} (P : A → Set j) {x y : A} (u : P y) (p : y ≡ x)
    (v : P x)
    → transport P p u ≡ v → u ≡ transport P (! p) v
  move!-transp-left P _ refl _ p = p

  move!-transp-right : ∀ {j} (P : A → Set j) {x y : A} (p : x ≡ y) (u : P y)
    (v : P x)
    → u ≡ transport P p v → transport P (! p) u ≡ v
  move!-transp-right P refl _ _ p = p

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Andreas, 2016-10-09, issue #2223

-- The level constraint solver needs to combine constraints
-- from different contexts and modules.
-- The parameter refinement broke this test case.

-- {-# OPTIONS -v tc.with.top:25 #-}
-- {-# OPTIONS -v tc.conv.nat:40 #-}
-- {-# OPTIONS -v tc.constr.add:45 #-}

open import Common.Level

module _ (a ℓ : Level) where

  mutual
    X : Level
    X = _

    data D : Set (lsuc a) where
      c : Set X → D  -- X <= a

    test : Set₁
    test with (lsuc ℓ) -- failed
    ... | _ = Set
    -- test = Set -- works

      where
        data C : Set (lsuc X) where
          c : Set a → C -- a <= X

-- Should solve all metas.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Data.Nat.Order where

open import Prelude
open import Data.Nat.Properties
open import Relation.Binary

<-trans : Transitive _<_
<-trans {zero} {suc y} {suc z} x<y y<z = tt
<-trans {suc x} {suc y} {suc z} x<y y<z = <-trans {x} {y} {z} x<y y<z

<-asym : Asymmetric _<_
<-asym {suc x} {suc y} x<y y<x = <-asym {x} {y} x<y y<x

<-irrefl : Irreflexive _<_
<-irrefl {suc x} = <-irrefl {x = x}

<-conn : Connected _<_
<-conn {zero} {zero} x≮y y≮x = refl
<-conn {zero} {suc y} x≮y y≮x = ⊥-elim (x≮y tt)
<-conn {suc x} {zero} x≮y y≮x = ⊥-elim (y≮x tt)
<-conn {suc x} {suc y} x≮y y≮x = cong suc (<-conn x≮y y≮x)

≤-antisym : Antisymmetric _≤_
≤-antisym {zero} {zero} x≤y y≤x = refl
≤-antisym {suc x} {suc y} x≤y y≤x = cong suc (≤-antisym x≤y y≤x)

ℕ-≰⇒> : ∀ x y → ¬ (x ≤ y) → y < x
ℕ-≰⇒> x y x≰y with y <ᴮ x
... | false = x≰y tt
... | true = tt

ℕ-≮⇒≥ : ∀ x y → ¬ (x < y) → y ≤ x
ℕ-≮⇒≥ x y x≮y with x <ᴮ y
... | false = tt
... | true = x≮y tt

totalOrder : TotalOrder ℕ ℓzero ℓzero
totalOrder .TotalOrder.strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder._<_ = _<_
totalOrder .TotalOrder.strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder.trans {x} {y} {z} = <-trans {x} {y} {z}
totalOrder .TotalOrder.strictPartialOrder .StrictPartialOrder.strictPreorder .StrictPreorder.irrefl {x} = <-irrefl {x = x}
totalOrder .TotalOrder.strictPartialOrder .StrictPartialOrder.conn = <-conn
totalOrder .TotalOrder.partialOrder .PartialOrder.preorder .Preorder._≤_ = _≤_
totalOrder .TotalOrder.partialOrder .PartialOrder.preorder .Preorder.refl {x} = ≤-refl x
totalOrder .TotalOrder.partialOrder .PartialOrder.preorder .Preorder.trans {x} {y} {z} = ≤-trans x y z
totalOrder .TotalOrder.partialOrder .PartialOrder.antisym = ≤-antisym
totalOrder .TotalOrder._<?_ x y = T? (x <ᴮ y)
totalOrder .TotalOrder.≰⇒> {x} {y} = ℕ-≰⇒> x y
totalOrder .TotalOrder.≮⇒≥ {x} {y} = ℕ-≮⇒≥ x y

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.Block     as Block
import      LibraBFT.Impl.Consensus.ConsensusTypes.BlockData as BlockData
import      LibraBFT.Impl.Types.BlockInfo                    as BlockInfo
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Encode                                      as Encode
open import Util.Prelude

module LibraBFT.Impl.Consensus.Liveness.ProposalGenerator where

ensureHighestQuorumCertM : Round → LBFT (Either ErrLog QuorumCert)

generateNilBlockM : Round → LBFT (Either ErrLog Block)
generateNilBlockM round =
  ensureHighestQuorumCertM round ∙?∙ (ok ∘ Block.newNil round)

generateProposalM : Instant → Round → LBFT (Either ErrLog BlockData)
generateProposalM _now round = do
  lrg ← use (lProposalGenerator ∙ pgLastRoundGenerated)
  ifD lrg <?ℕ round
    then (do
      lProposalGenerator ∙ pgLastRoundGenerated ∙= round
      ensureHighestQuorumCertM round ∙?∙ λ hqc -> do
        payload ← ifD BlockInfo.hasReconfiguration (hqc ^∙ qcCertifiedBlock)
                      -- IMPL-DIFF : create a fake TX
                      then pure (Encode.encode 0) -- (Payload [])
                      else pure (Encode.encode 0) -- use pgTxnManager <*> use (rmEpochState ∙ esEpoch) <*> pure round
        use (lRoundManager ∙ pgAuthor) >>= λ where
          nothing       → bail fakeErr -- ErrL (here ["lRoundManager.pgAuthor", "Nothing"])
          (just author) →
            ok (BlockData.newProposal payload author round {-pure blockTimestamp <*>-} hqc))
    else bail fakeErr
-- where
--  here t = "ProposalGenerator" ∷ "generateProposal" ∷ t

ensureHighestQuorumCertM round = do
  hqc ← use (lBlockStore ∙ bsHighestQuorumCert)
  ifD‖ (hqc ^∙ qcCertifiedBlock ∙ biRound) ≥?ℕ round ≔
       bail fakeErr {- ErrL (here [ "given round is lower than hqc round"
                                  , show (hqc^.qcCertifiedBlock.biRound) ]) -}
     ‖ hqc ^∙ qcEndsEpoch ≔
       bail fakeErr {-ErrEpochEndedNoProposals (here ["further proposals not allowed"])-}
     ‖ otherwise≔
       ok hqc
-- where
--  here t = "ProposalGenerator":"ensureHighestQuorumCertM":lsR round:t


text:
open import Relation.Binary.Core

module BubbleSort.Everything {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BubbleSort.Correctness.Order _≤_ tot≤ trans≤
open import BubbleSort.Correctness.Permutation _≤_ tot≤

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Equivalence.Strong where

-- Strong equivalence of categories.  Same as ordinary equivalence in Cat.
-- May not include everything we'd like to think of as equivalences, namely
-- the full, faithful functors that are essentially surjective on objects.

open import Level
open import Relation.Binary using (IsEquivalence; module IsEquivalence)
open import Function using () renaming (_∘_ to _∙_)

open import Categories.Category
open import Categories.Functor hiding (equiv)
open import Categories.NaturalIsomorphism as NI hiding (equiv)
open import Categories.NaturalTransformation as NT hiding (id; equiv)
open import Categories.Morphisms using (Iso; module Iso)

record WeakInverse {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (F : Functor C D) (G : Functor D C) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    F∘G≅id : NaturalIsomorphism (F ∘ G) id
    G∘F≅id : NaturalIsomorphism (G ∘ F) id
  F∘G⇒id = NaturalIsomorphism.F⇒G F∘G≅id
  id⇒F∘G = NaturalIsomorphism.F⇐G F∘G≅id
  G∘F⇒id = NaturalIsomorphism.F⇒G G∘F≅id
  id⇒G∘F = NaturalIsomorphism.F⇐G G∘F≅id
  .F∘G-iso : _
  F∘G-iso = NaturalIsomorphism.iso F∘G≅id
  .F∘G-isoˡ : _
  F∘G-isoˡ = λ x → Iso.isoˡ {C = D} (F∘G-iso x)
  .F∘G-isoʳ : _
  F∘G-isoʳ = λ x → Iso.isoʳ {C = D} (F∘G-iso x)
  .G∘F-iso : _
  G∘F-iso = NaturalIsomorphism.iso G∘F≅id
  .G∘F-isoˡ : _
  G∘F-isoˡ = λ x → Iso.isoˡ {C = C} (G∘F-iso x)
  .G∘F-isoʳ : _
  G∘F-isoʳ = λ x → Iso.isoʳ {C = C} (G∘F-iso x)

record StrongEquivalence {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    F : Functor C D
    G : Functor D C
    weak-inverse : WeakInverse F G
  open WeakInverse weak-inverse public

module Equiv where
  refl : ∀ {o ℓ e} {C : Category o ℓ e} → StrongEquivalence C C
  refl = record
    { F = id
    ; G = id
    ; weak-inverse = record
      { F∘G≅id = IsEquivalence.refl NI.equiv
      ; G∘F≅id = IsEquivalence.refl NI.equiv
      }
    }

  sym : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → StrongEquivalence C D → StrongEquivalence D C
  sym Inv = record
    { F = Inv.G
    ; G = Inv.F
    ; weak-inverse = record
      { F∘G≅id = Inv.G∘F≅id
      ; G∘F≅id = Inv.F∘G≅id
      }
    }
    where
    module Inv = StrongEquivalence Inv

  trans : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃} {C₁ : Category o₁ ℓ₁ e₁} {C₂ : Category o₂ ℓ₂ e₂} {C₃ : Category o₃ ℓ₃ e₃} → StrongEquivalence C₁ C₂ → StrongEquivalence C₂ C₃ → StrongEquivalence C₁ C₃
  trans {C₁ = C₁} {C₂} {C₃} A B = record
    { F = B.F ∘ A.F
    ; G = A.G ∘ B.G
    ; weak-inverse = record
      { F∘G≅id = IsEquivalence.trans NI.equiv ((B.F ⓘˡ A.F∘G≅id) ⓘʳ B.G) B.F∘G≅id
      ; G∘F≅id = IsEquivalence.trans NI.equiv ((A.G ⓘˡ B.G∘F≅id) ⓘʳ A.F) A.G∘F≅id
      }
    }
    where
    module A = StrongEquivalence A
    module B = StrongEquivalence B

equiv : ∀ {o ℓ e} → IsEquivalence (StrongEquivalence {o} {ℓ} {e})
equiv = record { refl = Equiv.refl; sym = Equiv.sym; trans = Equiv.trans }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.S1 where

open import Cubical.HITs.S1.Base public

-- open import Cubical.HITs.S1.Properties public

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Sets.IterativeSet.Relator.Proofs where

import      Lvl
open import Data
open import Data.Boolean
open import Data.Boolean.Proofs
open import Data.Boolean.Stmt
open import Data.Boolean.Stmt.Proofs
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using ()
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Relator.Equals using () renaming (_≡_ to Id ; [≡]-intro to intro)
open import Sets.IterativeSet.Relator
open import Sets.IterativeSet
open import Structure.Setoid using (Equiv)
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Relator
open import Syntax.Function
open import Syntax.Transitivity
open import Type
open import Type.Dependent

module _ where
  private variable {ℓ ℓ₁ ℓ₂} : Lvl.Level
  open Iset

  instance
    [≡][⊆]-sub : (_≡_) ⊆₂ (_⊆_ {ℓ₁}{ℓ₂})
    [≡][⊆]-sub = intro [∧]-elimᵣ

  instance
    [≡][⊇]-sub : (_≡_) ⊆₂ (_⊇_ {ℓ₁}{ℓ₂})
    [≡][⊇]-sub = intro [∧]-elimₗ

  [≡]-reflexivity-raw : ∀{A : Iset{ℓ}} → (A ≡ A)
  [⊆]-reflexivity-raw : ∀{A : Iset{ℓ}} → (A ⊆ A)
  [⊇]-reflexivity-raw : ∀{A : Iset{ℓ}} → (A ⊇ A)

  [≡]-reflexivity-raw {A = A} = [∧]-intro [⊇]-reflexivity-raw [⊆]-reflexivity-raw
  [⊆]-reflexivity-raw {A = set elem} = intro id (\{i} → [≡]-reflexivity-raw {A = elem(i)})
  [⊇]-reflexivity-raw = [⊆]-reflexivity-raw

  [≡]-symmetry-raw : ∀{A B : Iset{ℓ}} → (A ≡ B) → (B ≡ A)
  [≡]-symmetry-raw {A = A}{B = B} ([∧]-intro l r) = [∧]-intro r l

  [≡]-transitivity-raw : ∀{A B C : Iset{ℓ}} → (A ≡ B) → (B ≡ C) → (A ≡ C)
  [⊆]-transitivity-raw : ∀{A B C : Iset{ℓ}} → (A ⊆ B) → (B ⊆ C) → (A ⊆ C)
  [⊇]-transitivity-raw : ∀{A B C : Iset{ℓ}} → (A ⊇ B) → (B ⊇ C) → (A ⊇ C)

  Tuple.left  ([≡]-transitivity-raw {A = A}{B = B}{C = C} ab bc) = [⊇]-transitivity-raw(Tuple.left ab) (Tuple.left bc)
  Tuple.right ([≡]-transitivity-raw {A = A}{B = B}{C = C} ab bc) = [⊆]-transitivity-raw(Tuple.right ab) (Tuple.right bc)

  _⊆_.map   ([⊆]-transitivity-raw {A = A} {B = B} {C = C} ab bc) = _⊆_.map bc ∘ _⊆_.map ab
  _⊆_.proof ([⊆]-transitivity-raw {A = set elemA} {B = set elemB} {C = set elemC} ab bc) {ia} = [≡]-transitivity-raw {A = elemA(ia)}{B = elemB (_⊆_.map ab ia)} {C = elemC((_⊆_.map bc)((_⊆_.map ab)(ia)))} (_⊆_.proof ab {ia}) (_⊆_.proof bc)

  [⊇]-transitivity-raw {A = A} {B = B} {C = C} ab bc = [⊆]-transitivity-raw {A = C}{B = B}{C = A} bc ab

  instance
    [≡]-reflexivity : Reflexivity(_≡_ {ℓ})
    [≡]-reflexivity = intro [≡]-reflexivity-raw
  instance
    [⊆]-reflexivity : Reflexivity(_⊆_ {ℓ})
    [⊆]-reflexivity = intro [⊆]-reflexivity-raw
  instance
    [⊇]-reflexivity : Reflexivity(_⊇_ {ℓ})
    [⊇]-reflexivity = intro [⊇]-reflexivity-raw
  instance
    [≡]-symmetry : Symmetry(_≡_ {ℓ})
    [≡]-symmetry = intro [≡]-symmetry-raw
  instance
    [⊆]-antisymmetry : Antisymmetry(_⊆_ {ℓ})(_≡_)
    [⊆]-antisymmetry = intro (swap [∧]-intro)
  instance
    [⊇]-antisymmetry : Antisymmetry(_⊇_ {ℓ})(_≡_)
    [⊇]-antisymmetry = intro [∧]-intro
  instance
    [≡]-transitivity : Transitivity(_≡_ {ℓ})
    [≡]-transitivity = intro [≡]-transitivity-raw
  instance
    [⊆]-transitivity : Transitivity(_⊆_ {ℓ})
    [⊆]-transitivity = intro [⊆]-transitivity-raw
  instance
    [⊇]-transitivity : Transitivity(_⊇_ {ℓ})
    [⊇]-transitivity = intro [⊇]-transitivity-raw
  instance
    [≡]-equivalence : Equivalence(_≡_ {ℓ})
    [≡]-equivalence = intro
  instance
    Iset-equiv : Equiv(Iset{ℓ})
    Equiv._≡_ Iset-equiv = _≡_
    Equiv.equivalence Iset-equiv = [≡]-equivalence

  Iset-induction : ∀{P : Iset{ℓ₁} → Stmt{ℓ₂}} ⦃ _ : UnaryRelator(P) ⦄ → (∀{A : Iset{ℓ₁}} → (∀{a} → (a ∈ A) → P(a)) → P(A)) → (∀{A : Iset{ℓ₁}} → P(A))
  Iset-induction {P = P} p = Iset-index-induction (\{A} pp → p{A} (\{a} aA → substitute₁ₗ(P) ([∃]-proof aA) (pp{[∃]-witness aA})))

  [∈]-of-elem : ∀{A : Iset{ℓ}}{ia : Index(A)} → (elem(A)(ia) ∈ A)
  ∃.witness ([∈]-of-elem {ia = ia}) = ia
  ∃.proof    [∈]-of-elem = [≡]-reflexivity-raw

  Iset-intro-self-equality : ∀{A : Iset{ℓ}} → (set{Index = Index(A)}(elem(A)) ≡ A)
  _⊆_.map   (Tuple.left  Iset-intro-self-equality) = id
  _⊆_.map   (Tuple.right Iset-intro-self-equality) = id
  _⊆_.proof (Tuple.left  Iset-intro-self-equality) = [≡]-reflexivity-raw
  _⊆_.proof (Tuple.right Iset-intro-self-equality) = [≡]-reflexivity-raw

  [⊆]-with-elem : ∀{x y : Iset{ℓ}} → (xy : x ⊆ y) → ∀{ix} → (elem x ix ≡ elem y (_⊆_.map xy ix))
  [⊆]-with-elem xy {ix} = _⊆_.proof xy {ix}

  [⊆]-membership : ∀{A : Iset{ℓ}}{B : Iset{ℓ}} → (∀{x : Iset{ℓ}} → (x ∈ A) → (x ∈ B)) ↔ (A ⊆ B)
  [⊆]-membership {A = A}{B = B} = [↔]-intro l r where
    l : (∀{x} → (x ∈ A) → (x ∈ B)) ← (A ⊆ B)
    ∃.witness (l AB {x} xa) = _⊆_.map AB (∃.witness xa)
    ∃.proof   (l AB {x} xa) = [≡]-transitivity-raw (∃.proof xa) (_⊆_.proof AB)

    r : (∀{x} → (x ∈ A) → (x ∈ B)) → (A ⊆ B)
    _⊆_.map   (r proof) ia = [∃]-witness (proof{x = elem(A)(ia)} ([∈]-of-elem {A = A}))
    _⊆_.proof (r proof) {ia} = [∃]-proof (proof([∈]-of-elem {A = A}))

  [⊇]-membership : ∀{A : Iset{ℓ}}{B : Iset{ℓ}} → (∀{x : Iset{ℓ}} → (x ∈ A) ← (x ∈ B)) ↔ (A ⊇ B)
  [⊇]-membership {A = A}{B = B} = [⊆]-membership {A = B}{B = A}

  [≡]-membership : ∀{A : Iset{ℓ}}{B : Iset{ℓ}} → (∀{x : Iset{ℓ}} → (x ∈ A) ↔ (x ∈ B)) ↔ (A ≡ B)
  Tuple.left  (Tuple.left ([≡]-membership {A = A} {B = B}) ab) = [↔]-to-[←] [⊇]-membership (Tuple.left ab)
  Tuple.right (Tuple.left ([≡]-membership {A = A} {B = B}) ab) = [↔]-to-[←] [⊆]-membership (Tuple.right ab)
  Tuple.left  (Tuple.right ([≡]-membership {A = A} {B = B}) xaxb) = [↔]-to-[→] [⊇]-membership ([↔]-to-[←] xaxb)
  Tuple.right (Tuple.right ([≡]-membership {A = A} {B = B}) xaxb) = [↔]-to-[→] [⊆]-membership ([↔]-to-[→] xaxb)

  [∈]ₗ-unaryRelation-raw : ∀{A₁ A₂ B : Iset{ℓ}} → (A₁ ≡ A₂) → (A₁ ∈ B) → (A₂ ∈ B)
  ∃.witness ([∈]ₗ-unaryRelation-raw pa ([∃]-intro i ⦃ p ⦄)) = i
  ∃.proof ([∈]ₗ-unaryRelation-raw pa ([∃]-intro i ⦃ p ⦄)) = [≡]-transitivity-raw ([≡]-symmetry-raw pa) p

  [∈]-binaryRelation-raw : ∀{A₁ A₂ B₁ B₂ : Iset{ℓ}} → (A₁ ≡ A₂) → (B₁ ≡ B₂) → ((A₁ ∈ B₁) → (A₂ ∈ B₂))
  [∈]-binaryRelation-raw {B₂ = B₂} pa pb = [∈]ₗ-unaryRelation-raw {B = B₂} pa ∘ [↔]-to-[←] [⊆]-membership (sub₂(_≡_)(_⊆_) pb)

  instance
    [∈]-binaryRelation : BinaryRelator(_∈_ {ℓ})
    [∈]-binaryRelation = intro [∈]-binaryRelation-raw

  instance
    [⊆]-binaryRelator : BinaryRelator(_⊆_ {ℓ}{ℓ})
    BinaryRelator.substitution [⊆]-binaryRelator p1 p2 ps = sub₂(_≡_)(_⊇_) p1 🝖 ps 🝖 sub₂(_≡_)(_⊆_) p2

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 Pi-Calculus where

-- Local modules ---------------------------------------------------------------

open import Common
     using (Id)

-- π-process definition --------------------------------------------------------

data π-process : Set where
   recv_from_∙_ : Id → Id → π-process → π-process       -- Receive
   send_to_∙_   : Id → Id → π-process → π-process       -- Send
   _||_         : π-process → π-process → π-process     -- Composition
   ν_∙_         : Id → π-process → π-process            -- Restriction
   !_           : π-process → π-process                 -- Repetition
   Zero         : π-process                             -- Inactivity

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


text:
------------------------------------------------------------------------
-- Properties of combinatorial functions on integers
------------------------------------------------------------------------

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

module Math.Combinatorics.IntegerFunction.Properties where

open import Data.Nat as ℕ hiding (_*_; _+_; _≤_; _<_)
import Data.Nat.Properties as ℕₚ
open import Data.Integer as ℤ
import Data.Integer.Properties as ℤₚ
open import Relation.Binary.PropositionalEquality
open import Function.Base

import Math.Combinatorics.Function as ℕF
import Math.Combinatorics.Function.Properties as ℕFₚ
open import Math.Combinatorics.IntegerFunction
import Math.Combinatorics.IntegerFunction.Properties.Lemma as Lemma

------------------------------------------------------------------------
-- Properties of [-1]^_

[-1]^[1+n]≡-1*[-1]^n : ∀ n → [-1]^ (ℕ.suc n) ≡ -1ℤ * [-1]^ n
[-1]^[1+n]≡-1*[-1]^n zero              = refl
[-1]^[1+n]≡-1*[-1]^n (ℕ.suc zero)      = refl
[-1]^[1+n]≡-1*[-1]^n (ℕ.suc (ℕ.suc n)) = [-1]^[1+n]≡-1*[-1]^n n

[-1]^[m+n]≡[-1]^m*[-1]^n : ∀ m n → [-1]^ (m ℕ.+ n) ≡ [-1]^ m * [-1]^ n
[-1]^[m+n]≡[-1]^m*[-1]^n zero              n = sym $ ℤₚ.*-identityˡ $ [-1]^ n
[-1]^[m+n]≡[-1]^m*[-1]^n (ℕ.suc zero)      n = [-1]^[1+n]≡-1*[-1]^n n
[-1]^[m+n]≡[-1]^m*[-1]^n (ℕ.suc (ℕ.suc m)) n = [-1]^[m+n]≡[-1]^m*[-1]^n m n

-- TODO: [-1]^n≡-1∨[-1]^n≡1

[-1]^[2*n]≡1 : ∀ n → [-1]^ (2 ℕ.* n) ≡ + 1
[-1]^[2*n]≡1 zero      = refl
[-1]^[2*n]≡1 (ℕ.suc n) = begin-equality
  [-1]^ (2 ℕ.* ℕ.suc n) ≡⟨ cong ([-1]^_) $ ℕₚ.*-distribˡ-+ 2 1 n ⟩
  [-1]^ (2 ℕ.+ 2 ℕ.* n) ≡⟨⟩
  [-1]^ (2 ℕ.* n)       ≡⟨ [-1]^[2*n]≡1 n ⟩
  + 1                   ∎
  where open ℤₚ.≤-Reasoning

[-1]^[1+2*n]≡-1 : ∀ n → [-1]^ (1 ℕ.+ 2 ℕ.* n) ≡ -1ℤ
[-1]^[1+2*n]≡-1 n = begin-equality
  [-1]^ (1 ℕ.+ 2 ℕ.* n) ≡⟨ [-1]^[1+n]≡-1*[-1]^n (2 ℕ.* n) ⟩
  -1ℤ * [-1]^ (2 ℕ.* n) ≡⟨ cong (-1ℤ *_) $ [-1]^[2*n]≡1 n ⟩
  -1ℤ * + 1             ∎
  where open ℤₚ.≤-Reasoning

------------------------------------------------------------------------
-- Properties of permutation

P[n,0]≡1 : ∀ n → P n 0 ≡ (+ 1)
P[n,0]≡1 (+ n)      = refl
P[n,0]≡1 (-[1+ n ]) = refl

P[n,1]≡n : ∀ n → P n 1 ≡ n
P[n,1]≡n (+ n)      = cong (+_) $ ℕFₚ.P[n,1]≡n n
P[n,1]≡n (-[1+ n ]) = begin-equality
  -1ℤ * + ℕF.Poch (ℕ.suc n) 1
    ≡⟨ cong (λ v → -1ℤ * + v) $ ℕFₚ.Poch[n,1]≡n (ℕ.suc n) ⟩
  -1ℤ * (+ (ℕ.suc n))
    ≡⟨ ℤₚ.-1*n≡-n (+ (ℕ.suc n)) ⟩
  - (+ ℕ.suc n)
    ∎
  where open ℤₚ.≤-Reasoning

module _ where
  open ℤₚ.≤-Reasoning

  P[-n,k]≡[-1]^k*ℕPoch[n,k] : ∀ n k → P (- (+ n)) k ≡ [-1]^ k * + ℕF.Poch n k
  P[-n,k]≡[-1]^k*ℕPoch[n,k] zero      zero      = refl
  P[-n,k]≡[-1]^k*ℕPoch[n,k] zero      (ℕ.suc k) = sym $ ℤₚ.*-zeroʳ ([-1]^ ℕ.suc k)
  P[-n,k]≡[-1]^k*ℕPoch[n,k] (ℕ.suc n) k         = refl

  P[-n,2*k]≡ℕPoch[n,2*k] : ∀ n k → P (- (+ n)) (2 ℕ.* k) ≡ + ℕF.Poch n (2 ℕ.* k)
  P[-n,2*k]≡ℕPoch[n,2*k] n k = begin-equality
    P (- (+ n)) (2 ℕ.* k) ≡⟨ P[-n,k]≡[-1]^k*ℕPoch[n,k] n (2 ℕ.* k) ⟩
    [-1]^ (2 ℕ.* k) * p   ≡⟨ cong (_* p) $ [-1]^[2*n]≡1 k ⟩
    1ℤ * p                ≡⟨ ℤₚ.*-identityˡ p ⟩
    p                     ∎
    where p = + ℕF.Poch n (2 ℕ.* k)

  P[-n,1+2*k]≡-ℕPoch[n,1+2*k] : ∀ n k →
    P (- (+ n)) (1 ℕ.+ 2 ℕ.* k) ≡ - (+ ℕF.Poch n (1 ℕ.+ 2 ℕ.* k))
  P[-n,1+2*k]≡-ℕPoch[n,1+2*k] n k = begin-equality
    P (- (+ n)) (1 ℕ.+ 2 ℕ.* k) ≡⟨ P[-n,k]≡[-1]^k*ℕPoch[n,k] n (1 ℕ.+ 2 ℕ.* k) ⟩
    [-1]^ (1 ℕ.+ 2 ℕ.* k) * p   ≡⟨ cong (_* p) $ [-1]^[1+2*n]≡-1 k ⟩
    -1ℤ * p                     ≡⟨ ℤₚ.-1*n≡-n p ⟩
    - p                         ∎
    where p = + ℕF.Poch n (1 ℕ.+ 2 ℕ.* k)

  0≤n∧n<k⇒P[n,k]≡0 : ∀ {n k} → 0ℤ ≤ n → n < + k → P n k ≡ + 0
  0≤n∧n<k⇒P[n,k]≡0 {+_ n} {k} 0≤n (+<+ n<k) = cong (+_) $ ℕFₚ.n<k⇒P[n,k]≡0 n<k

  P[1+n,1+k]≡[1+n]*P[n,k] : ∀ n k → P (ℤ.suc n) (ℕ.suc k) ≡ ℤ.suc n * P n k
  P[1+n,1+k]≡[1+n]*P[n,k] (+ n)            k = begin-equality
    + (ℕ.suc n ℕ.* ℕF.P n k) ≡⟨ sym $ ℤₚ.pos-distrib-* (ℕ.suc n) (ℕF.P n k) ⟩
    + (ℕ.suc n) * + ℕF.P n k ≡⟨⟩
    ℤ.suc (+ n) * + ℕF.P n k ∎
  P[1+n,1+k]≡[1+n]*P[n,k] (-[1+ 0 ])       k = refl
  P[1+n,1+k]≡[1+n]*P[n,k] (-[1+ ℕ.suc n ]) k = begin-equality
    [-1]^ (ℕ.suc k) * + ℕF.Poch (ℕ.suc n) (ℕ.suc k)
      ≡⟨⟩
    [-1]^ (ℕ.suc k) * + (ℕ.suc n ℕ.* p)
      ≡⟨ cong (_* + (ℕ.suc n ℕ.* p)) $ [-1]^[1+n]≡-1*[-1]^n k ⟩
    -1ℤ * [-1]^ k * + (ℕ.suc n ℕ.* p)
      ≡⟨ sym $ cong (-1ℤ * [-1]^ k *_) $ ℤₚ.pos-distrib-* (ℕ.suc n) p ⟩
    -1ℤ * [-1]^ k * (+ ℕ.suc n * + p)
      ≡⟨ Lemma.lemma₁ -1ℤ ([-1]^ k) (+ ℕ.suc n) (+ p) ⟩
    -1ℤ * + ℕ.suc n * ([-1]^ k * + p)
      ≡⟨ cong (_* ([-1]^ k * + p)) $ ℤₚ.-1*n≡-n (+ ℕ.suc n) ⟩
    -[1+ n ] * ([-1]^ k * + p)
      ∎
    where p = ℕF.Poch (ℕ.suc (ℕ.suc n)) k

  P[n,1+k]≡n*P[n-1,k] : ∀ n k → P n (ℕ.suc k) ≡ n * P (n - 1ℤ) k
  P[n,1+k]≡n*P[n-1,k] n k = begin-equality
    P n (ℕ.suc k)                  ≡⟨ cong (λ v → P v (ℕ.suc k)) $ Lemma.lemma₂ n ⟩
    P (1ℤ + (n - 1ℤ)) (ℕ.suc k)    ≡⟨ P[1+n,1+k]≡[1+n]*P[n,k] (n - 1ℤ) k ⟩
    (1ℤ + (n - 1ℤ)) * P (n - 1ℤ) k ≡⟨ sym $ cong (_* P (n - 1ℤ) k) $ Lemma.lemma₂ n ⟩
    n * P (n - 1ℤ) k               ∎

  P-split : ∀ (m : ℕ) (n : ℤ) (o : ℕ) → P ((+ m) + n) (m ℕ.+ o) ≡ P ((+ m) + n) m * P n o
  P-split zero      n o = begin-equality
    P (0ℤ + n) o         ≡⟨ cong (λ v → P v o) $ ℤₚ.+-identityˡ n ⟩
    P n o                ≡⟨ sym $ ℤₚ.*-identityˡ (P n o) ⟩
    1ℤ * P n o           ≡⟨ sym $ cong (_* P n o) $ P[n,0]≡1 (0ℤ + n) ⟩
    P (0ℤ + n) 0 * P n o ∎
  P-split (ℕ.suc m) n o = begin-equality
    P (ℤ.suc (+ m) + n) (ℕ.suc (m ℕ.+ o))
      ≡⟨ cong (λ v → P v (ℕ.suc (m ℕ.+ o))) $ ℤₚ.+-assoc 1ℤ (+ m) n ⟩
    P (ℤ.suc (+ m + n)) (ℕ.suc (m ℕ.+ o))
      ≡⟨ P[1+n,1+k]≡[1+n]*P[n,k] (+ m + n) (m ℕ.+ o) ⟩
    ℤ.suc (+ m + n) * P (+ m + n) (m ℕ.+ o)
      ≡⟨ cong (ℤ.suc (+ m + n) *_) $ P-split m n o ⟩
    ℤ.suc (+ m + n) * (P (+ m + n) m * P n o)
      ≡⟨ sym $ ℤₚ.*-assoc (ℤ.suc (+ m + n)) (P (+ m + n) m) (P n o) ⟩
    ℤ.suc (+ m + n) * P (+ m + n) m * P n o
      ≡⟨ sym $ cong (_* P n o) $ P[1+n,1+k]≡[1+n]*P[n,k] (+ m + n) m ⟩
    P (ℤ.suc (+ m + n)) (ℕ.suc m) * P n o
      ≡⟨ sym $ cong (λ v → P v (ℕ.suc m) * P n o) $ ℤₚ.+-assoc 1ℤ (+ m) n ⟩
    P (+ (ℕ.suc m) + n) (ℕ.suc m) * P n o
      ∎

  P-split-minus : ∀ m n o → P m (n ℕ.+ o) ≡ P m n * P (m - + n) o
  P-split-minus m n o = begin-equality
    P m (n ℕ.+ o)         ≡⟨ cong (λ v → P v (n ℕ.+ o)) m≡n+p ⟩
    P (+ n + p) (n ℕ.+ o) ≡⟨ P-split n p o ⟩
    P (+ n + p) n * P p o ≡⟨ sym $ cong (λ v → P v n * P p o) $ m≡n+p ⟩
    P m n * P (m - + n) o ∎
    where
    p = m - + n
    m≡n+p : m ≡ + n + (m - + n)
    m≡n+p = Lemma.lemma₃ m (+ n)


text:
data Unit : Set where
  unit : Unit

F : Unit → Set₁
F unit = Set

data D (u : Unit) (f : F u) : Set where

variable
  u : Unit
  f : F u
  d : D u f

postulate
  P : {u : Unit} {f : F u} → D u f → Set
  p : P d

p' : (u : Unit) (f : F u) (d : D u f) → P d
p' u f d = p {u} {f}  {d}


text:
module Not-named-according-to-the-Haskell-lexical-syntax where

postulate
  IO : Set -> Set

{-# BUILTIN IO IO #-}
{-# COMPILE GHC IO = type IO #-}

postulate
  return : {A : Set} -> A -> IO A

{-# COMPILE GHC return = \ _ -> return :: a -> IO a #-}

data Unit : Set where
  unit : Unit

{-# COMPILE GHC Unit = data () (()) #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module NotNot where
  open import Basics

  open import lib.NType2

  {-
    The definitions here follow Penon's paper "Infinitesimaux et Intuitionisme".
  -}

  -- Since double negation is always proposition valued, we just define it that way
  -- for convenience.
  ¬¬ : ∀ {i} (A : Type i) → PropT i
  ¬¬ A = ¬ (¬ A), ¬¬-is-a-prop
    where
      ¬¬-is-a-prop : ∀ {i} {A : Type i} → (¬ (¬ A)) is-a-prop
      ¬¬-is-a-prop = mapping-into-prop-is-a-prop (λ _ → False holds-is-a-prop)

  continue : ∀ {i j} {A : Type i} {B : A → Type j}
             (a : A) → ((a : A) → B a) → B a
  continue a f = f a

  -- When trying to prove a negation from a double negation,
  -- You may remove the double negation.
  ¬¬-elim : ∀ {i j} {A : Type i} (B : (¬¬ A) holds → Type j)
            (f : (a : A) → ¬ (B (continue a)))
            → (nna : (¬¬ A) holds) → ¬ (B nna)
  ¬¬-elim {A = A} B f nna b =
    nna (λ a → (f a) b')
    where
      b' : {a : A} → B (continue a)
      b' {a} = transport B (prop-path (snd (¬¬ A)) nna (continue a)) b
  ¬¬-elim' : ∀ {i j} {A : Type i} {B : (¬¬ A) holds → Type j}
            (f : (a : A) → ¬ (B (continue a)))
            → (nna : (¬¬ A) holds) → ¬ (B nna)
  ¬¬-elim' {B = B} f nna = ¬¬-elim B f nna

  syntax ¬¬-elim B (λ a → t) nna = un¬¬ nna -as- a -in t in-family B
  syntax ¬¬-elim'  (λ a → t) nna = un¬¬ nna -as- a -in t

  -- The "neighbor relation"
  -- a is the neighbor of b (a ≈ b) if a is not distinct from b (¬¬ (a == b))
  infix 30 _≈_
  _≈_ : ∀ {i} {A : Type i} (a b : A) → PropT i
  a ≈ b = ¬¬ (a == b)

  refl≈ : ∀ {i} {A : Type i} {a : A} → a ≈ a holds
  refl≈ = λ nnp → nnp refl

  trans≈ : ∀ {i} {A : Type i} {a b c : A}
           → a ≈ b holds
           → b ≈ c holds
           → a ≈ c holds
  trans≈ nnp nnq =
    un¬¬ nnp -as- p -in
      un¬¬ nnq -as- q -in
        (λ npq → npq (p ∙ q))

  -- The "neighborhood" of a point of a type is the subtype of all its neighbors.
  nbhd-prop : ∀ {i} {A} (a : A) → SubtypeProp A i
  nbhd-prop a = (λ b → a ≈ b holds) , (λ b → a ≈ b holds-is-a-prop)

  nbhd : ∀ {i} {A : Type i} (a : A)
         → Type i
  nbhd  {i} {A} a = Subtype (nbhd-prop a)

  -- The total space neighborhood bundle is the sum of all neighborhoods.
  nbhd-space : ∀ {i} (A : Type i) → Type i
  nbhd-space A = Σ A \(a : A) → nbhd a

  private -- We give the neighborhood space a nickname
    N = nbhd-space

  germ : ∀ {i j} {A : Type i} {B : Type j} -- The germ of
         → (f : A → B) -- a function f
         → (a : A) -- at a point a
         → nbhd a → nbhd (f a) -- is a function of this type
  germ f a (d , nnp) =
    f d ,
      (un¬¬ nnp -as- p -in
        (λ ne → ne (ap f p))
      in-family (λ _ → ¬ (f a == f d)))

  chain-rule : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
                       {f : A → B} {g : B → C} (a : A)
                       → germ (g ∘ f) a == (germ g (f a)) ∘ (germ f a)
  chain-rule {f = f} {g = g} a =
    λ= $ λ {(d , p) →
      Subtype=-out (nbhd-prop (g (f a))) -- It suffices to prove the first terms are equal,
        refl -- which they are judgementally.
    }

  -- A map is etale if all its germs are equivalences.
  _is-etale : ∀ {i j} {A : Type i} {B : Type j}
          (f : A → B) → Type (lmax i j)
  f is-etale = ∀ a → (germ f a) is-an-equiv

  {- Some universe level error
  ∘-is-etale : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
               {f : A → B} {g : B → C}
               (p : f is-etale) (q : g is-etale)
               → (g ∘ f) is-etale
  ∘-is-etale {i}{j}{k}{A}{B}{C} {f = f} {g = g} p q =
    λ a →     transport (λ (φ : nbhd a → nbhd (g (f (a)))) → φ is-an-equiv)
      {x = (germ g (f a)) ∘ (germ f a)} {y = germ (g ∘ f) a}
      (chain-rule a) (((q (f a)) ∘ise (p a)) )
  -}

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of pretty printing
------------------------------------------------------------------------

module README.Text.Pretty where

open import Size

open import Data.Bool.Base
open import Data.List.Base as List
open import Data.List.NonEmpty as List⁺
open import Data.Nat.Base
open import Data.Product
open import Data.String.Base hiding (parens; _<+>_)
open import Data.Vec.Base as Vec
open import Function.Base

-- We import the pretty printer and pass 80 to say that we do not want to
-- have lines longer than 80 characters
open import Text.Pretty 80

open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- A small declarative programming language
------------------------------------------------------------------------

-- We define a small programming language where definitions are
-- introduced by providing a non-empty list of equations with:
-- * the same number of patterns on the LHS
-- * a term on the RHS of each equation

-- A pattern is either a variable or a constructor applied to a
-- list of subpatterns

data Pattern (i : Size) : Set where
  var : String → Pattern i
  con : ∀ {j : Size< i} → String → List (Pattern j) → Pattern i

-- A term is either a (bound) variable, the application of a
-- named definition / constructor to a list of arguments or a
-- lambda abstraction

data Term (i : Size) : Set where
  var : String → Term i
  app : ∀ {j : Size< i} → String → List (Term j) → Term i
  lam : ∀ {j : Size< i} → String → Term j → Term i

-- As explained before, a definitions is given by a list of equations

infix 1 _by_
record Def : Set where
  constructor _by_
  field name      : String
        {arity}   : ℕ
        equations : List⁺ (Vec (Pattern _) arity × (Term _))

------------------------------------------------------------------------
-- A pretty printer for this language
------------------------------------------------------------------------

-- First we print patterns. We only wrap a pattern in parentheses if it
-- is compound: i.e. if it is a constructor applied to a non-empty list
-- of subpatterns
-- Lists of patterns are printed separated by a single space.

prettyPattern  : ∀ {i} → Pattern i → Doc
prettyPatterns : ∀ {i} → List (Pattern i) → Doc

prettyPattern (var v)    = text v
prettyPattern (con c []) = text c
prettyPattern (con c ps) = parens $ text c <+> prettyPatterns ps

prettyPatterns = hsep ∘ List.map prettyPattern

-- Next we print terms. The Bool argument tells us whether we are on
-- the RHS of an application (in which case it is sensible to wrap
-- complex subterms in parentheses).

prettyTerm : ∀ {i} → Bool → Term i → Doc
prettyTerm l (var v)    = text v
prettyTerm l (app f []) = text f
prettyTerm l (app f es) = if l then parens else id
  $ text f <+> sep (List.map (prettyTerm true) es)
prettyTerm l (lam x b)  = if l then parens else id
  $ text "λ" <+> text x <> text "." <+> prettyTerm false b

-- We now have all the pieces to print definitions.
-- We print the equations below each other by using vcat.
--
-- The LHS is printed as follows: the name of the function followed by
-- the space-separated list of patterns (if any) and then an equal sign.
--
-- The RHS is printed as a term which is *not* on the RHS of an application.
--
-- Finally we can layout the definition in two different manners:
-- * either LHS followed by RHS
-- * or LHS followed and the RHS as a relative block (indented by 2 spaces)
--   on the next line

prettyDef : Def → Doc
prettyDef (fun by eqs) =
  vcat $ List⁺.toList $ flip List⁺.map eqs $ uncurry $ λ ps e →
  let lhs = text fun <+> (case ps of λ where
              [] → text "="
              _  → prettyPatterns (Vec.toList ps) <+> text "=")
      rhs = prettyTerm false e
  in lhs <+> rhs <|> lhs $$ (spaces 2 <> rhs)

-- The pretty printer is obtained by using the renderer.

pretty : Def → String
pretty = render ∘ prettyDef

------------------------------------------------------------------------
-- Some examples
------------------------------------------------------------------------

-- Our first example is the identity function defined as a λ-abstraction

`id : Def
`id = "id" by ([] , lam "x" (var "x")) ∷ []

_ : pretty `id ≡ "id = λ x. x"
_ = refl

-- If we were to assume that this definition also takes a level (a) and
-- a Set at that level (A) as arguments, we can have a slightly more complex
-- definition like so.

`explicitid : Def
`explicitid = "id" by (var "a" ∷ var "A" ∷ [] , lam "x" (var "x")) ∷ []

_ : pretty `explicitid ≡ "id a A = λ x. x"
_ = refl

-- A more complex example: boolFilter, a function that takes a boolean
-- predicate and a list as arguments and returns a list containing only
-- the values that satisfy the predicate.
-- We use nil and con for [] and _∷_ as our little toy language does not
-- support infix notations.

`filter : Def
`filter = "boolFilter"
  by ( var "P?" ∷ con "nil" [] ∷ []
     , app "nil" []
     )
   ∷ ( var "P?" ∷ con "con" (var "x" ∷ var "xs" ∷ []) ∷ []
     , let rec = app "filter" (var "P?" ∷ var "xs" ∷ []) in
       app "if" (app "P?" (var "x" ∷ [])
         ∷ app "con" (var "x" ∷ rec ∷ [])
         ∷ rec
         ∷ [])
     )
   ∷ []

_ : pretty `filter ≡
  "boolFilter P? nil = nil
\ \boolFilter P? (con x xs) = if (P? x) (con x (filter P? xs)) (filter P? xs)"
_ = refl

-- We can once more revisit this example with its more complex counterpart:
-- boolFilter taking its level and set arguments explicitly (idem for the
-- list constructors nil and con).
-- This time laying out the second equation on a single line would produce a
-- string larger than 80 characters long. So the pretty printer decides to
-- make the RHS a relative block indented by 2 spaces.

`explicitfilter : Def
`explicitfilter = "boolFilter"
  by ( var "a" ∷ var "A" ∷ var "P?" ∷ con "nil" [] ∷ []
     , app "nil" (var "a" ∷ var "A" ∷ [])
     )
   ∷ ( var "a" ∷ var "A" ∷ var "P?" ∷ con "con" (var "x" ∷ var "xs" ∷ []) ∷ []
     , let rec = app "filter" (var "a" ∷ var "A" ∷ var "P?" ∷ var "xs" ∷ []) in
       app "if" (app "P?" (var "x" ∷ [])
         ∷ app "con" (var "a" ∷ var "A" ∷ var "x" ∷ rec ∷ [])
         ∷ rec
         ∷ [])
     )
   ∷ []

_ : pretty `explicitfilter
  ≡ "boolFilter a A P? nil = nil a A
\   \boolFilter a A P? (con x xs) =
\   \  if (P? x) (con a A x (filter a A P? xs)) (filter a A P? xs)"
_ = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Automatic solvers for equations over naturals
------------------------------------------------------------------------

-- See README.Nat for examples of how to use this solver

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

module Data.Nat.Tactic.RingSolver where

open import Agda.Builtin.Reflection

open import Data.Maybe.Base using (just; nothing)
open import Data.Nat.Base using (zero; suc)
open import Data.Nat.Properties
open import Level using (0ℓ)
open import Data.Unit using (⊤)
open import Relation.Binary.PropositionalEquality

import Tactic.RingSolver as Solver
import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _+_ and _*_

ring : ACR.AlmostCommutativeRing 0ℓ 0ℓ
ring = ACR.fromCommutativeSemiring *-+-commutativeSemiring
  λ { zero → just refl; _ → nothing }

macro
  solve-∀ : Term → TC ⊤
  solve-∀ = Solver.solve-∀-macro (quote ring)

macro
  solve : Term → Term → TC ⊤
  solve n = Solver.solve-macro n (quote ring)


text:
module Data.List.Categorical where

import Lvl
open import Functional
open import Function.Equals
open import Data.List
open import Data.List.Functions
open import Data.List.Proofs
open import Data.List.Equiv.Id
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Setoid using (intro)
open import Structure.Function
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Type
open import Type.Category

private variable ℓ : Lvl.Level

instance
  map-functor : Functor{ℓ}(List)
  Functor.map ⦃ map-functor ⦄ = map
  _⊜_.proof (Function.congruence (Functor.map-function ⦃ map-functor ⦄) {x = f} {y = g} (intro proof)) = map-function-raw proof
  _⊜_.proof (Functor.op-preserving ⦃ map-functor ⦄) = map-preserves-[∘]
  _⊜_.proof (Functor.id-preserving ⦃ map-functor ⦄) = map-preserves-id

instance
  concatMap-monad : Monad{ℓ}(List)
  Monad.η   ⦃ concatMap-monad ⦄ _ = singleton
  Monad.ext ⦃ concatMap-monad ⦄   = concatMap
  _⊜_.proof (Function.congruence (Monad.ext-function ⦃ concatMap-monad ⦄) (intro proof)) {x} = concatMap-function-raw (proof) {x}
  Monad.ext-inverse    ⦃ concatMap-monad ⦄ = intro concatMap-singleton
  Monad.ext-identity   ⦃ concatMap-monad ⦄ = intro (identityᵣ(_++_)(∅))
  Monad.ext-distribute ⦃ concatMap-monad ⦄ {f = f}{g = g} = intro (\{x} → concatMap-[∘] {f = f}{g = g}{x = x})


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import Util.Prelude

module LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-0 where

enabled : Bool
enabled = true


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

module DiscriminationRules where

open import Data.Bool.Base
open import Data.List
open import Data.Nat
open import Relation.Binary.PropositionalEquality

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

true≢false : true ≢ false
true≢false ()

0≠suc : ∀ {n} → 0 ≢ suc n
0≠suc ()

[]≢x∷xs : {A : Set}{x : A}{xs : List A} → [] ≢ x ∷ xs
[]≢x∷xs ()

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Everything where

import Prelude
import Stack

import Syntax
import Semantics

import Convertibility
import Correctness

max_stars_repo_name: mietek/nbe-correctness

max_issues_repo_name: mietek/nbe-correctness

max_forks_repo_name: mietek/nbe-correctness