text:
module PLDI14-List-of-Theorems where

-- List of theorems in PLDI submission
--
-- For hints about installation and execution, please refer
-- to README.agda.
--
-- Agda modules corresponding to definitions, lemmas and theorems
-- are listed here with the most important names. For example,
-- after this file type checks (C-C C-L), placing the cursor
-- on the purple "Base.Change.Algebra" and pressing M-. will
-- bring you to the file where change structures are defined.
-- The name for change structures in that file is
-- "ChangeAlgebra", given in the using-clause.

-- Definition 2.1 (Change structures)
open import Base.Change.Algebra using (ChangeAlgebra)
---- Carrier in record ChangeAlgebra                        --(a)
open Base.Change.Algebra.ChangeAlgebra   using (Change)     --(b)
open Base.Change.Algebra.ChangeAlgebra   using (update)     --(c)
open Base.Change.Algebra.ChangeAlgebra   using (diff)       --(d)
open Base.Change.Algebra.IsChangeAlgebra using (update-diff)--(e)

-- Definition 2.2 (Nil change)
-- IsChangeAlgebra.nil
open Base.Change.Algebra using (IsChangeAlgebra)

-- Lemma 2.3 (Behavior of nil)
-- IsChangeAlgebra.update-nil
open Base.Change.Algebra using (IsChangeAlgebra)

-- Lemma 2.5 (Behavior of derivatives on nil)
open import Base.Change.Equivalence using (deriv-zero)

-- Definition 2.4 (Derivatives)
open Base.Change.Algebra using (IsDerivative)

-- Definition 2.6 (Carrier set of function changes)
open Base.Change.Algebra.FunctionChanges

-- Definition 2.7 (Operations on function changes)
-- ChangeAlgebra.update FunctionChanges.changeAlgebra
-- ChangeAlgebra.diff   FunctionChanges.changeAlgebra
open Base.Change.Algebra.FunctionChanges using (changeAlgebraFun)

-- Theorem 2.8 (Function changes form a change structure)
-- (In Agda, the proof of Theorem 2.8 has to be included in the
-- definition of function changes, here
-- FunctionChanges.changeAlgebra.)
open Base.Change.Algebra.FunctionChanges using (changeAlgebraFun)

-- Theorem 2.9 (Incrementalization)
open Base.Change.Algebra.FunctionChanges using (incrementalization)

-- Theorem 2.10 (Nil changes are derivatives)
open Base.Change.Algebra.FunctionChanges using (nil-is-derivative)

-- Definition 3.1 (Domains)
import Parametric.Denotation.Value
open Parametric.Denotation.Value.Structure using (⟦_⟧Type)

-- Definition 3.2 (Environments)
open import Base.Denotation.Environment using (⟦_⟧Context)

-- Definition 3.3 (Evaluation)
import Parametric.Denotation.Evaluation
open Parametric.Denotation.Evaluation.Structure using (⟦_⟧Term)

-- Definition 3.4 (Changes)
-- Definition 3.5 (Change environments)
import Parametric.Change.Validity
open Parametric.Change.Validity.Structure using (change-algebra)
open Parametric.Change.Validity.Structure using (environment-changes)

-- Definition 3.6 (Change semantics)
-- Lemma 3.7 (Change semantics is the derivative of semantics)
import Parametric.Change.Specification
open Parametric.Change.Specification.Structure using (⟦_⟧Δ)
open Parametric.Change.Specification.Structure using (correctness)

-- Definition 3.8 (Erasure)
-- Lemma 3.9 (The erased version of a change is almost the same)
import Parametric.Change.Implementation
open Parametric.Change.Implementation.Structure using (_≈_)
open Parametric.Change.Implementation.Structure using (carry-over)

-- Lemma 3.10 (⟦ t ⟧Δ erases to Derive(t))
-- Theorem 3.11 (Correctness of differentiation)
import Parametric.Change.Correctness
open Parametric.Change.Correctness.Structure using (derive-correct-closed)
open Parametric.Change.Correctness.Structure using (main-theorem)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
open import Data.Product using ( proj₁ ; proj₂ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using
  ( _≡_ ; refl ; sym ; cong )
open import Relation.Unary using ( _⊆_ )
open import Web.Semantic.DL.ABox using ( ABox ; ⟨ABox⟩ ; Assertions )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ ; bnodes ; _,_ )
open import Web.Semantic.DL.Category.Object using ( Object ; IN ; fin ; iface )
open import Web.Semantic.DL.Category.Morphism using ( impl ; _≣_ ; _⊑_ ; _,_ )
open import Web.Semantic.DL.Category.Tensor using ( _⊗_ ; _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Properties.Tensor.Lemmas using
  ( tensor-up ; tensor-down ; tensor-resp-⊨a )
open import Web.Semantic.DL.Category.Wiring using
  ( wiring ; wires-≈ ; wires-≈⁻¹ ; identity ; id✓ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using
  ( Δ ; _⊨_≈_ ; ≈-refl ; ≈-refl′ ; ≈-trans )
open import Web.Semantic.Util using
  ( id ; _∘_ ; False ; elim ; inj⁻¹ ; _⊕_⊕_ ; inode ; bnode ; enode )

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

tensor-resp-wiring : ∀ (A₁ A₂ B₁ B₂ : Object S T) →
  (f₁ : IN B₁ → IN A₁) →
  (f₁✓ : Assertions (⟨ABox⟩ f₁ (iface B₁)) ⊆ Assertions (iface A₁)) →
  (f₂ : IN B₂ → IN A₂) →
  (f₂✓ : Assertions (⟨ABox⟩ f₂ (iface B₂)) ⊆ Assertions (iface A₂)) →
  (g : IN (B₁ ⊗ B₂) → IN (A₁ ⊗ A₂)) →
  (g✓ : Assertions (⟨ABox⟩ g (iface (B₁ ⊗ B₂))) ⊆ Assertions (iface (A₁ ⊗ A₂))) →
    (∀ x → inj₁ (f₁ x) ≡ g (inj₁ x)) →
      (∀ x → inj₂ (f₂ x) ≡ g (inj₂ x)) →
        ((wiring A₁ B₁ f₁ f₁✓ ⟨⊗⟩ wiring A₂ B₂ f₂ f₂✓) ≣
          (wiring (A₁ ⊗ A₂) (B₁ ⊗ B₂) g g✓))
tensor-resp-wiring A₁ A₂ B₁ B₂ f₁ f₁✓ f₂ f₂✓ g g✓ f₁≡g₁ f₂≡g₂ =
  (LHS⊑RHS , RHS⊑LHS) where

  LHS⊑RHS :
    wiring A₁ B₁ f₁ f₁✓ ⟨⊗⟩ wiring A₂ B₂ f₂ f₂✓ ⊑
      wiring (A₁ ⊗ A₂) (B₁ ⊗ B₂) g g✓
  LHS⊑RHS I I⊨STA I⊨F = (elim , I⊨RHS) where

    lemma : ∀ x → ⌊ I ⌋ ⊨ ind I (inode (g x)) ≈ ind I (enode x)
    lemma (inj₁ x) = ≈-trans ⌊ I ⌋
      (≈-refl′ ⌊ I ⌋ (cong (ind I ∘ inode) (sym (f₁≡g₁ x))))
      (wires-≈ f₁ (proj₂ (fin B₁) x)
        (tensor-up (wiring A₁ B₁ f₁ f₁✓) (wiring A₂ B₂ f₂ f₂✓) I I⊨F))
    lemma (inj₂ x) = ≈-trans ⌊ I ⌋
      (≈-refl′ ⌊ I ⌋ (cong (ind I ∘ inode) (sym (f₂≡g₂ x))))
      (wires-≈ f₂ (proj₂ (fin B₂) x)
        (tensor-down (wiring A₁ B₁ f₁ f₁✓) (wiring A₂ B₂ f₂ f₂✓) I I⊨F))

    I⊨RHS : bnodes I elim ⊨a impl (wiring (A₁ ⊗ A₂) (B₁ ⊗ B₂) g g✓)
    I⊨RHS = wires-≈⁻¹ g lemma (proj₁ (fin (B₁ ⊗ B₂)))

  RHS⊑LHS :
    wiring (A₁ ⊗ A₂) (B₁ ⊗ B₂) g g✓ ⊑
      wiring A₁ B₁ f₁ f₁✓ ⟨⊗⟩ wiring A₂ B₂ f₂ f₂✓
  RHS⊑LHS I I⊨STA I⊨F = (elim ∘ inj⁻¹ , I⊨LHS) where

    lemma₁ : ∀ x → ⌊ I ⌋ ⊨ ind I (inode (inj₁ (f₁ x))) ≈ ind I (enode (inj₁ x))
    lemma₁ x = ≈-trans ⌊ I ⌋
      (≈-refl′ ⌊ I ⌋ (cong (ind I ∘ inode) (f₁≡g₁ x)))
      (wires-≈ g (proj₂ (fin (B₁ ⊗ B₂)) (inj₁ x)) I⊨F)

    lemma₂ : ∀ x → ⌊ I ⌋ ⊨ ind I (inode (inj₂ (f₂ x))) ≈ ind I (enode (inj₂ x))
    lemma₂ x = ≈-trans ⌊ I ⌋
      (≈-refl′ ⌊ I ⌋ (cong (ind I ∘ inode) (f₂≡g₂ x)))
      (wires-≈ g (proj₂ (fin (B₁ ⊗ B₂)) (inj₂ x)) I⊨F)

    I⊨LHS : bnodes I (elim ∘ inj⁻¹) ⊨a impl (wiring A₁ B₁ f₁ f₁✓ ⟨⊗⟩ wiring A₂ B₂ f₂ f₂✓)
    I⊨LHS = tensor-resp-⊨a (wiring A₁ B₁ f₁ f₁✓) (wiring A₂ B₂ f₂ f₂✓) (bnodes I (elim ∘ inj⁻¹))
      (wires-≈⁻¹ f₁ lemma₁ (proj₁ (fin B₁))) (wires-≈⁻¹ f₂ lemma₂ (proj₁ (fin B₂)))

ext: agda

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module ParserC where

{-

  import Prelude
  import Equiv
  import Eq
  import Datoid
  import List
  import Bag

  open Prelude
  open Equiv
  open Eq
  open Datoid
  open List
  open Bag

  parserDatoid : (a, s : Datoid) -> Datoid
  parserDatoid a s = Bag (pairDatoid a (listDatoid s))

-- We use the following datatype instead of
--   type Parsing s a = [s] -> Bag (a, [s])
  data Parsing (s, a : Datoid) : Set1 where
    P :  (List (El s) -> El (parserDatoid a s)) -> Parsing s a

  private
    unP :  {s, a : Datoid} -> Parsing s a
        -> List (El s) -> El (parserDatoid a s)
    unP (P x) = x

    _<+>_ :  {a : Datoid} -> El (Bag a) -> El (Bag a) -> El (Bag a)
    _<+>_ {a} x y = bagElim (\bs -> El (Bag a)) ? y (\z zs ih -> insert z ih) x

    concatMap :  {a, b : Datoid} -> (El a -> El (Bag b)) -> El (Bag a)
              -> El (Bag b)
    concatMap {a} {b} f = bagElim (\bs -> El (Bag b)) ? empty (\x b ih -> f x <+> ih)

  symbol : {s : Datoid} -> Parsing s s
  symbol {s} = P symbol'
    where
    symbol' : List (El s) -> El (parserDatoid s s)
    symbol' nil       = empty
    symbol' (x :: xs) = insert (pair x xs) empty

  fail : {s, a : Datoid} -> Parsing s a
  fail = P (\ss -> empty)

  (+++) : {s, a : Datoid} -> Parsing s a -> Parsing s a -> Parsing s a
  P p +++ P q = P (\s -> p s <+> q s)

  return :  {s, a : Datoid} -> (x : El a) -> Parsing s a
  return = \x -> P (\s -> insert (pair x s) empty)

--  data Traverse (a : Datoid) : Set where
--    Empty  : Traverse a
--    Insert : (x : El a) -> (b : El (Bag a)) -> Traverse a

--  run : {a : Datoid} -> Traverse a -> El (Bag a)
--  traverse : {a : Datoid} -> El (Bag a) -> Traverse a
--  traverseTraverses
--    :  {a : Datoid} -> (b : El (Bag a)) -> run (traverse b) =^= b

-- insert : {a : Datoid} -> El a -> El (Bag a) -> El (Bag a)
-- pairDatoid : Datoid -> Datoid -> Datoid
--(empty {Bag (pairDatoid s (listDatoid s))})
--  bagElim
--    :  {a : Datoid}
--    -> (P : El (Bag a) -> Set)
--    -> P empty
--    -> ((x : El a) -> (b : El (Bag a)) -> P b -> P (insert x b))
--    -> (b : El (Bag a))
--    -> P b

  (>>=) : {s, a, b : Datoid}
        -> Parsing s a -> (El a -> Parsing s b) -> Parsing s b
  (>>=) {s} {a} {b} (P p) k
        = P (\s -> concatMap (\y -> unP (k (fst y)) (snd y)) (p s))

{-
  parserDatoid : (a, s : Datoid) -> Datoid
  parserDatoid a s = Bag (pairDatoid a (listDatoid s))

-- We use the following datatype instead of
--   type Parsing s a = [s] -> Bag (a, [s])
  data Parsing (s, a : Datoid) : Set1 where
    P :  (List (El s) -> El (parserDatoid a s))
      -> Parsing s a

-}

-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Test where

open import Level

infixl 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

J : {a b : Level} (A : Set a) (C : (x y : A) → x ≡ y → Set b)
    → ((x : A) → C x x refl)
    → (x y : A) (P : x ≡ y)
    → C x y P
J A C b x .x refl = b x

-- K : (A : Set) (x : A) (C : x ≡ x → Set)
--   → C refl
--   → (loop : x ≡ x)
--   → C loop
-- K A x C b p = {! p  !}

-- Lemma 2.1.1 (inversion of paths)
infix 6 ¬_
¬_ : {a : Level} {A : Set a} {x y : A} → x ≡ y → y ≡ x
¬_ {a} {A} {x} {y} p = J A D d x y p

  where
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = y ≡ x

    d : (x : A) → D x x refl
    d x = refl

-- Lemma 2.1.2 (concatenation of paths)
infixl 5 _∙_
_∙_ : {a : Level} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {a} {A} {x} {y} {z} p q = J {a} {a} A D d x y p z q

  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = (z : A) (q : y ≡ z) → x ≡ z

    -- base case
    d : (x : A) → D x x refl
    d x z q = J A E e x z q
      where
        -- the predicate
        E : (x z : A) (q : x ≡ z) → Set a
        E x z q = x ≡ z

        -- base case
        e : (x : A) → E x x refl
        e x = refl

-- Lemma 2.1.4.i (identity of path concatenation)
∙-identityʳ : {a : Level} {A : Set a} {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
∙-identityʳ {a} {A} {x} {y} p = J A D d x y p

  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = p ≡ p ∙ refl

    -- base case
    d : (x : A) → D x x refl
    d x = refl

∙-identityˡ : {a : Level} {A : Set a} {x y : A} (p : x ≡ y) → p ≡ refl ∙ p
∙-identityˡ {a} {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = p ≡ refl ∙ p

    -- base case
    d : (x : A) → D x x refl
    d x = refl

-- Lemma 2.1.4.ii (identity of path inversion)
¬-identityʳ : {a : Level} {A : Set a} {x y : A} (p : x ≡ y) → ¬ p ∙ p ≡ refl
¬-identityʳ {a} {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = ¬ p ∙ p ≡ refl

    -- base case
    d : (x : A) → D x x refl
    d x = refl

¬-identityˡ : {a : Level} {A : Set a} {x y : A} (p : x ≡ y) → p ∙ ¬ p ≡ refl
¬-identityˡ {a} {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set a
    D x y p = p ∙ ¬ p ≡ refl

    -- base case
    d : (x : A) → D x x refl
    d x = refl

-- Lemma 2.1.4.iii (involution of path inversion)
involution : {A : Set} {x y : A} (p : x ≡ y) → ¬ ¬ p ≡ p
involution {A} {x} {y} p = J A D d x y p
  where
    -- the predicate
    D : (x y : A) (p : x ≡ y) → Set
    D x y p = ¬ ¬ p ≡ p

    -- base case
    d : (x : A) → D x x refl
    d x = refl

-- Lemma 2.1.4.iv (associativity of path concatenation)
∙-assoc : {a : Level} {A : Set a} {w x y z : A}
  → (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
  → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
∙-assoc {a} {A} {w} {x} {y} {z} p q r = J A D d w x p y q z r
  where
    -- the predicate
    D : (w x : A) (p : w ≡ x) → Set a
    D w x p = (y : A) (q : x ≡ y)
            → (z : A) (r : y ≡ z)
            → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r

    -- base case
    d : (x : A) → D x x refl
    d x y q z r = J A E e x y q z r
      where
        -- the predicate
        E : (x y : A) (q : x ≡ y) → Set a
        E x y q = (z : A) (r : y ≡ z)
                → refl ∙ (q ∙ r) ≡ refl ∙ q ∙ r

        -- base case
        e : (x : A) → E x x refl
        e x z r = J A F f x z r
          where
            -- the predicate
            F : (y z : A) (r : y ≡ z) → Set a
            F y z r = refl ∙ (refl ∙ r) ≡ refl ∙ refl ∙ r

            -- base case
            f : (x : A) → F x x refl
            f x = {!   !}

max_stars_repo_name: erydo/agda-mode

max_issues_repo_name: erydo/agda-mode

max_forks_repo_name: erydo/agda-mode


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

module Definition.Typed.Consequences.Equality where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Fundamental.Reducibility

open import Tools.Product
import Tools.PropositionalEquality as PE

U≡A′ : ∀ {A Γ l} ([U] : Γ ⊩⟨ l ⟩U)
    → Γ ⊩⟨ l ⟩ U ≡ A / (U-intr [U])
    → A PE.≡ U
U≡A′ (noemb [U]) [U≡A] = [U≡A]
U≡A′ (emb 0<1 [U]) [U≡A] = U≡A′ [U] [U≡A]

-- If A is judgmentally equal to U, then A is propositionally equal to U.
U≡A : ∀ {A Γ}
    → Γ ⊢ U ≡ A
    → A PE.≡ U
U≡A {A} U≡A with reducibleEq U≡A
U≡A {A} U≡A | [U] , [A] , [U≡A] =
  U≡A′ (U-elim [U]) (irrelevanceEq [U] (U-intr (U-elim [U])) [U≡A])

ℕ≡A′ : ∀ {A Γ l} ([ℕ] : Γ ⊩⟨ l ⟩ℕ ℕ)
    → Γ ⊩⟨ l ⟩ ℕ ≡ A / (ℕ-intr [ℕ])
    → Whnf A
    → A PE.≡ ℕ
ℕ≡A′ (noemb x) [ℕ≡A] whnfA = whnfRed* [ℕ≡A] whnfA
ℕ≡A′ (emb 0<1 [ℕ]) [ℕ≡A] whnfA = ℕ≡A′ [ℕ] [ℕ≡A] whnfA

-- If A in WHNF is judgmentally equal to ℕ, then A is propositionally equal to ℕ.
ℕ≡A : ∀ {A Γ}
    → Γ ⊢ ℕ ≡ A
    → Whnf A
    → A PE.≡ ℕ
ℕ≡A {A} ℕ≡A whnfA with reducibleEq ℕ≡A
ℕ≡A {A} ℕ≡A whnfA | [ℕ] , [A] , [ℕ≡A] =
  ℕ≡A′ (ℕ-elim [ℕ]) (irrelevanceEq [ℕ] (ℕ-intr (ℕ-elim [ℕ])) [ℕ≡A]) whnfA

-- If A in WHNF is judgmentally equal to Empty, then A is propositionally equal to Empty.
Empty≡A′ : ∀ {A Γ l} ([Empty] : Γ ⊩⟨ l ⟩Empty Empty)
    → Γ ⊩⟨ l ⟩ Empty ≡ A / (Empty-intr [Empty])
    → Whnf A
    → A PE.≡ Empty
Empty≡A′ (noemb x) [Empty≡A] whnfA = whnfRed* [Empty≡A] whnfA
Empty≡A′ (emb 0<1 [Empty]) [Empty≡A] whnfA = Empty≡A′ [Empty] [Empty≡A] whnfA

Empty≡A : ∀ {A Γ}
    → Γ ⊢ Empty ≡ A
    → Whnf A
    → A PE.≡ Empty
Empty≡A {A} Empty≡A whnfA with reducibleEq Empty≡A
Empty≡A {A} Empty≡A whnfA | [Empty] , [A] , [Empty≡A] =
  Empty≡A′ (Empty-elim [Empty]) (irrelevanceEq [Empty] (Empty-intr (Empty-elim [Empty])) [Empty≡A]) whnfA

Unit≡A′ : ∀ {A Γ l} ([Unit] : Γ ⊩⟨ l ⟩Unit Unit)
    → Γ ⊩⟨ l ⟩ Unit ≡ A / (Unit-intr [Unit])
    → Whnf A
    → A PE.≡ Unit
Unit≡A′ (noemb x) [Unit≡A] whnfA = whnfRed* [Unit≡A] whnfA
Unit≡A′ (emb 0<1 [Unit]) [Unit≡A] whnfA = Unit≡A′ [Unit] [Unit≡A] whnfA

Unit≡A : ∀ {A Γ}
    → Γ ⊢ Unit ≡ A
    → Whnf A
    → A PE.≡ Unit
Unit≡A {A} Unit≡A whnfA with reducibleEq Unit≡A
Unit≡A {A} Unit≡A whnfA | [Unit] , [A] , [Unit≡A] =
  Unit≡A′ (Unit-elim [Unit]) (irrelevanceEq [Unit] (Unit-intr (Unit-elim [Unit])) [Unit≡A]) whnfA

ne≡A′ : ∀ {A K Γ l}
     → ([K] : Γ ⊩⟨ l ⟩ne K)
     → Γ ⊩⟨ l ⟩ K ≡ A / (ne-intr [K])
     → Whnf A
     → ∃ λ M → Neutral M × A PE.≡ M
ne≡A′ (noemb [K]) (ne₌ M D′ neM K≡M) whnfA =
  M , neM , (whnfRed* (red D′) whnfA)
ne≡A′ (emb 0<1 [K]) [K≡A] whnfA = ne≡A′ [K] [K≡A] whnfA

-- If A in WHNF is judgmentally equal to K, then there exists a M such that
-- A is propositionally equal to M.
ne≡A : ∀ {A K Γ}
    → Neutral K
    → Γ ⊢ K ≡ A
    → Whnf A
    → ∃ λ M → Neutral M × A PE.≡ M
ne≡A {A} neK ne≡A whnfA with reducibleEq ne≡A
ne≡A {A} neK ne≡A whnfA | [ne] , [A] , [ne≡A] =
  ne≡A′ (ne-elim neK [ne])
        (irrelevanceEq [ne] (ne-intr (ne-elim neK [ne])) [ne≡A]) whnfA

B≡A′ : ∀ {A F G Γ l} W ([W] : Γ ⊩⟨ l ⟩B⟨ W ⟩ ⟦ W ⟧ F ▹ G)
    → Γ ⊩⟨ l ⟩ ⟦ W ⟧ F ▹ G ≡ A / (B-intr W [W])
    → Whnf A
    → ∃₂ λ H E → A PE.≡ ⟦ W ⟧ H ▹ E
B≡A′ W (noemb [W]) (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) whnfA =
  F′ , G′ , whnfRed* D′ whnfA
B≡A′ W (emb 0<1 [W]) [W≡A] whnfA = B≡A′ W [W] [W≡A] whnfA

Π≡A′ : ∀ {A F G Γ l} → _
Π≡A′ {A} {F} {G} {Γ} {l} = B≡A′ {A} {F} {G} {Γ} {l} BΠ
Σ≡A′ : ∀ {A F G Γ l} → _
Σ≡A′ {A} {F} {G} {Γ} {l} = B≡A′ {A} {F} {G} {Γ} {l} BΣ

-- If A is judgmentally equal to Π F ▹ G, then there exists H and E such that
-- A is propositionally equal to  Π H ▹ E.
B≡A : ∀ {A F G Γ} W
    → Γ ⊢ ⟦ W ⟧ F ▹ G ≡ A
    → Whnf A
    → ∃₂ λ H E → A PE.≡ ⟦ W ⟧ H ▹ E
B≡A {A} W W≡A whnfA with reducibleEq W≡A
B≡A {A} W W≡A whnfA | [W] , [A] , [W≡A] =
  B≡A′ W (B-elim W [W]) (irrelevanceEq [W] (B-intr W (B-elim W [W])) [W≡A]) whnfA

Π≡A : ∀ {A F G Γ} → _
Π≡A {A} {F} {G} {Γ} = B≡A {A} {F} {G} {Γ} BΠ
Σ≡A : ∀ {A F G Γ} → _
Σ≡A {A} {F} {G} {Γ} = B≡A {A} {F} {G} {Γ} BΣ


text:
{-

Cubical Agda - A Dependently Typed PL with Univalence and HITs
==============================================================
                    Anders Mörtberg
       Every Proof Assistant - September 17, 2020

Link to slides: https://staff.math.su.se/anders.mortberg/slides/EPA2020.pdf

Link to video: https://vimeo.com/459020971

-}

-- To make Agda cubical add the following options
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Talks.EPA2020 where

-- The "Foundations" package contain a lot of important results (in
-- particular the univalence theorem)
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Int
open import Cubical.Data.Prod.Base

-- The interval in Cubical Agda is written I and the endpoints i0 and i1.

apply0 : (A : Type) (p : I → A) → A
apply0 A p = p i0

-- We omit the universe level ℓ for simplicity in this talk. In the
-- library everything is maximally universe polymorphic.

-- We can write functions out of the interval using λ-abstraction:
refl' : {A : Type} (x : A) → x ≡ x
refl' x = λ i → x
-- In fact, x ≡ y is short for PathP (λ _ → A) x y

refl'' : {A : Type} (x : A) → PathP (λ _ → A) x x
refl'' x = λ _ → x

-- In general PathP A x y has A : I → Type, x : A i0 and y : A i1
-- PathP = Dependent paths (Path over a Path)

-- We cannot pattern-match on interval variables as I is not inductively defined
-- foo : {A : Type} → I → A
-- foo r = {!r!}   -- Try typing C-c C-c

-- cong has a direct proof
cong' : {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong' f p i = f (p i)

-- function extensionality also has a direct proof.
-- It also has computational content: swap the arguments.
funExt' : {A B : Type} {f g : A → B} (p : (x : A) → f x ≡ g x) → f ≡ g
funExt' p i x = p x i

-- Transport is more complex as ≡ isn't inductively defined (so we
-- can't define it by pattern-matching on p)
transport' : {A B : Type} → A ≡ B → A → B
transport' p a = transp (λ i → p i) i0 a

-- This lets us define subst (which is called "transport" in the HoTT book)
subst' : {A : Type} (P : A → Type) {x y : A} (p : x ≡ y) → P x → P y
subst' P p pa = transport (λ i → P (p i)) pa

-- The transp operation reduces differently for different types
-- formers. For paths it reduces to another primitive operation called
-- hcomp.

-- We can also define the J eliminator (aka path induction)
J' : {A : Type} {B : A → Type} {x : A}
     (P : (z : A) → x ≡ z → Type)
     (d : P x refl) {y : A} (p : x ≡ y) → P y p
J' P d p = transport (λ i → P (p i) (λ j → p (i ∧ j))) d

-- So J is provable, but it doesn't satisfy computation rule
-- definitionally. This is almost never a problem in practice as the
-- cubical primitives satisfy many new definitional equalities.

-- Another key concept in HoTT/UF is the Univalence Axiom. In Cubical
-- Agda this is provable, we hence refer to it as the Univalence
-- Theorem.

-- The univalence theorem: equivalences of types give paths of types
ua' : {A B : Type} → A ≃ B → A ≡ B
ua' = ua

-- Any isomorphism of types gives rise to an equivalence
isoToEquiv' : {A B : Type} → Iso A B → A ≃ B
isoToEquiv' = isoToEquiv

-- And hence to a path
isoToPath' : {A B : Type} → Iso A B → A ≡ B
isoToPath' e = ua' (isoToEquiv' e)

-- ua satisfies the following computation rule
-- This suffices to be able to prove the standard formulation of univalence.
uaβ' : {A B : Type} (e : A ≃ B) (x : A)
     → transport (ua' e) x ≡ fst e x
uaβ' e x = transportRefl (equivFun e x)

-- Time for an example!

-- Booleans
data Bool : Type where
  false true : Bool

not : Bool → Bool
not false = true
not true  = false

notPath : Bool ≡ Bool
notPath = isoToPath' (iso not not rem rem)
  where
  rem : (b : Bool) → not (not b) ≡ b
  rem false = refl
  rem true  = refl

_ : transport notPath true ≡ false
_ = refl

-- Another example, integers:

sucPath : Int ≡ Int
sucPath = isoToPath' (iso sucInt predInt sucPred predSuc)

_ : transport sucPath (pos 0) ≡ pos 1
_ = refl

_ : transport (sucPath ∙ sucPath) (pos 0) ≡ pos 2
_ = refl

_ : transport (sym sucPath) (pos 0) ≡ negsuc 0
_ = refl

-----------------------------------------------------------------------------
-- Higher inductive types

-- The following definition of finite multisets is due to Vikraman
-- Choudhury and Marcelo Fiore.

infixr 5 _∷_

data FMSet (A : Type) : Type where
  [] : FMSet A
  _∷_ : (x : A) → (xs : FMSet A) → FMSet A
  comm : (x y : A) (xs : FMSet A) → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
--  trunc : (xs ys : FMSet A) (p q : xs ≡ ys) → p ≡ q

-- We need to add the trunc constructor for FMSets to be sets, omitted
-- here for simplicity.

_++_ : ∀ {A : Type} (xs ys : FMSet A) → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys
comm x y xs i ++ ys = comm x y (xs ++ ys) i
-- trunc xs zs p q i j ++ ys =
--   trunc (xs ++ ys) (zs ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j

unitr-++ : {A : Type} (xs : FMSet A) → xs ++ [] ≡ xs
unitr-++ [] = refl
unitr-++ (x ∷ xs) = cong (x ∷_) (unitr-++ xs)
unitr-++ (comm x y xs i) j = comm x y (unitr-++ xs j) i
-- unitr-++ (trunc xs ys x y i j) = {!!}

-- This is a special case of set quotients! Very useful for
-- programming and set level mathematics

data _/_ (A : Type) (R : A → A → Type) : Type where
  [_] : A → A / R
  eq/ : (a b : A) → R a b → [ a ] ≡ [ b ]
  trunc : (a b : A / R) (p q : a ≡ b) → p ≡ q

-- Proving that they are effective ((a b : A) → [ a ] ≡ [ b ] → R a b)
-- requires univalence for propositions.

-------------------------------------------------------------------------
-- Topological examples of things that are not sets

-- We can define the circle as the following simple data declaration:
data S¹ : Type where
  base : S¹
  loop : base ≡ base

-- We can write functions on S¹ using pattern-matching equations:
double : S¹ → S¹
double base = base
double (loop i) = (loop ∙ loop) i

helix : S¹ → Type
helix base     = Int
helix (loop i) = sucPathInt i

ΩS¹ : Type
ΩS¹ = base ≡ base

winding : ΩS¹ → Int
winding p = subst helix p (pos 0)

_ : winding (λ i → double ((loop ∙ loop) i)) ≡ pos 4
_ = refl

-- We can define the Torus as:
data Torus : Type where
  point : Torus
  line1 : point ≡ point
  line2 : point ≡ point
  square : PathP (λ i → line1 i ≡ line1 i) line2 line2

-- And prove that it is equivalent to two circle:
t2c : Torus → S¹ × S¹
t2c point        = (base , base)
t2c (line1 i)    = (loop i , base)
t2c (line2 j)    = (base , loop j)
t2c (square i j) = (loop i , loop j)

c2t : S¹ × S¹ → Torus
c2t (base   , base)   = point
c2t (loop i , base)   = line1 i
c2t (base   , loop j) = line2 j
c2t (loop i , loop j) = square i j

c2t-t2c : (t : Torus) → c2t (t2c t) ≡ t
c2t-t2c point        = refl
c2t-t2c (line1 _)    = refl
c2t-t2c (line2 _)    = refl
c2t-t2c (square _ _) = refl

t2c-c2t : (p : S¹ × S¹) → t2c (c2t p) ≡ p
t2c-c2t (base   , base)   = refl
t2c-c2t (base   , loop _) = refl
t2c-c2t (loop _ , base)   = refl
t2c-c2t (loop _ , loop _) = refl

-- Using univalence we get the following equality:
Torus≡S¹×S¹ : Torus ≡ S¹ × S¹
Torus≡S¹×S¹ = isoToPath' (iso t2c c2t t2c-c2t c2t-t2c)

windingTorus : point ≡ point → Int × Int
windingTorus l = ( winding (λ i → proj₁ (t2c (l i)))
                 , winding (λ i → proj₂ (t2c (l i))))

_ : windingTorus (line1 ∙ sym line2) ≡ (pos 1 , negsuc 0)
_ = refl

-- We have many more topological examples, including Klein bottle, RP^n,
-- higher spheres, suspensions, join, wedges, smash product:
open import Cubical.HITs.KleinBottle
open import Cubical.HITs.RPn
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.HITs.Susp
open import Cubical.HITs.Join
open import Cubical.HITs.Wedge
open import Cubical.HITs.SmashProduct

-- There's also a proof of the "3x3 lemma" for pushouts in less than
-- 200LOC. In HoTT-Agda this took about 3000LOC. For details see:
-- https://github.com/HoTT/HoTT-Agda/tree/master/theorems/homotopy/3x3
open import Cubical.HITs.Pushout

-- We also defined the Hopf fibration and proved that its total space
-- is S³ in about 300LOC:
open import Cubical.HITs.Hopf

-- There is also some integer cohomology:
open import Cubical.ZCohomology.Everything
-- To compute cohomology groups of various spaces we need a bunch of
-- interesting theorems: Freudenthal suspension theorem,
-- Mayer-Vietoris sequence...
open import Cubical.Homotopy.Freudenthal
open import Cubical.ZCohomology.MayerVietorisUnreduced

-------------------------------------------------------------------------
-- The structure identity principle

-- A more efficient version of finite multisets based on association lists
open import Cubical.HITs.AssocList.Base

-- data AssocList (A : Type) : Type where
--  ⟨⟩ : AssocList A
--  ⟨_,_⟩∷_ : (a : A) (n : ℕ) (xs : AssocList A) → AssocList A
--  per : (a b : A) (m n : ℕ) (xs : AssocList A)
--      → ⟨ a , m ⟩∷ ⟨ b , n ⟩∷ xs ≡ ⟨ b , n ⟩∷ ⟨ a , m ⟩∷ xs
--  agg : (a : A) (m n : ℕ) (xs : AssocList A)
--      → ⟨ a , m ⟩∷ ⟨ a , n ⟩∷ xs ≡ ⟨ a , m + n ⟩∷ xs
--  del : (a : A) (xs : AssocList A) → ⟨ a , 0 ⟩∷ xs ≡ xs
--  trunc : (xs ys : AssocList A) (p q : xs ≡ ys) → p ≡ q

-- Programming and proving is more complicated with AssocList compared
-- to FMSet. This kind of example occurs everywhere in programming and
-- mathematics: one representation is easier to work with, but not
-- efficient, while another is efficient but difficult to work with.

-- Solution: substitute using univalence
substIso : {A B : Type} (P : Type → Type) (e : Iso A B) → P A → P B
substIso P e = subst P (isoToPath e)

-- Can transport for example Monoid structure from FMSet to AssocList
-- this way, but the achieved Monoid structure is not very efficient
-- to work with. A better solution is to prove that FMSet and
-- AssocList are equal *as monoids*, but how to do this?

-- Solution: structure identity principle (SIP)
-- This is a very useful consequence of univalence
open import Cubical.Foundations.SIP

sip' : {ℓ : Level} {S : Type ℓ → Type ℓ} {ι : StrEquiv S ℓ}
       (θ : UnivalentStr S ι) (A B : TypeWithStr ℓ S) → A ≃[ ι ] B → A ≡ B
sip' = sip

-- The tricky thing is to prove that (S,ι) is a univalent structure.
-- Luckily we provide automation for this in the library, see for example:
open import Cubical.Algebra.Monoid.Base

-- Another cool application of the SIP: matrices represented as
-- functions out of pairs of Fin's and vectors are equal as abelian
-- groups:
open import Cubical.Algebra.Matrix

-- The end, back to slides!

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: module Structure.Sets.Relators where

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 Prelude.Monoid where

open import Prelude.Function
open import Prelude.Maybe
open import Prelude.List
open import Prelude.Semiring
open import Prelude.Applicative
open import Prelude.Functor

record Monoid {a} (A : Set a) : Set a where
  infixr 6 _<>_
  field
    mempty : A
    _<>_   : A → A → A

open Monoid {{...}} public

{-# DISPLAY Monoid.mempty _ = mempty #-}
{-# DISPLAY Monoid._<>_ _ a b = a <> b #-}

mconcat : ∀ {a} {A : Set a} {{MonA : Monoid A}} → List A → A
mconcat = foldr _<>_ mempty

--- Instances ---

instance
  MonoidList : ∀ {a} {A : Set a} → Monoid (List A)
  mempty {{MonoidList}} = []
  _<>_   {{MonoidList}} = _++_

  MonoidFun : ∀ {a b} {A : Set a} {B : A → Set b} {{_ : ∀ {x} → Monoid (B x)}} → Monoid (∀ x → B x)
  mempty {{MonoidFun}}     _ = mempty
  _<>_   {{MonoidFun}} f g x = f x <> g x

  MonoidMaybe : ∀ {a} {A : Set a} → Monoid (Maybe A)
  mempty {{MonoidMaybe}} = nothing
  _<>_   {{MonoidMaybe}} nothing  y = y
  _<>_   {{MonoidMaybe}} (just x) _ = just x

record Sum {a} (A : Set a) : Set a where
  constructor mkSum
  field getSum : A

open Sum public

instance
  MonoidSum : ∀ {a} {A : Set a} {{_ : Semiring A}} → Monoid (Sum A)
  getSum (mempty {{MonoidSum}})     = zro
  getSum (_<>_   {{MonoidSum}} x y) = getSum x + getSum y

record Product {a} (A : Set a) : Set a where
  constructor mkProduct
  field getProduct : A

open Product public

instance
  MonoidProduct : ∀ {a} {A : Set a} {{_ : Semiring A}} → Monoid (Product A)
  getProduct (mempty {{MonoidProduct}})     = one
  getProduct (_<>_   {{MonoidProduct}} x y) = getProduct x * getProduct y

record Const {a b} (A : Set a) (B : Set b) : Set a where
  constructor mkConst
  field getConst : A

open Const public

module _ {a b} {A : Set a} {{MonA : Monoid A}} where
  instance
    FunctorConst : Functor {a = b} (Const A)
    getConst (fmap {{FunctorConst}} f x) = getConst x

    ApplicativeConst : Applicative (Const A)
    getConst (pure  {{ApplicativeConst}} x)     = mempty
    getConst (_<*>_ {{ApplicativeConst}} wf wx) = getConst wf <> getConst wx

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.NProd where

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

open import Cubical.Data.Nat using (ℕ)

open import Cubical.Algebra.Group

private variable
  ℓ : Level

open GroupStr

NProd-Group : (G : (n : ℕ) → Type ℓ) → (Gstr : (n : ℕ) → GroupStr (G n)) → Group ℓ
fst (NProd-Group G Gstr) = (n : ℕ) → G n
1g (snd (NProd-Group G Gstr)) = λ n → 1g (Gstr n)
GroupStr._·_ (snd (NProd-Group G Gstr)) = λ f g n → Gstr n ._·_ (f n) (g n)
inv (snd (NProd-Group G Gstr)) = λ f n → (Gstr n).inv (f n)
isGroup (snd (NProd-Group G Gstr)) = makeIsGroup (isSetΠ (λ _ → is-set (Gstr _)))
                                                 (λ f g h → funExt λ n → ·Assoc (Gstr n) _ _ _)
                                                 (λ f → funExt λ n → ·IdR (Gstr n) _)
                                                 (λ f → funExt λ n → ·IdL (Gstr n) _)
                                                 (λ f → funExt λ n → ·InvR (Gstr n) _)
                                                  λ f → funExt λ n → ·InvL (Gstr n) _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- An abstraction: term-like things
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Context.Term-like
  {i u e} (Uni : IndexedUniverse i u e) where

import Axiom.Extensionality.Propositional as E
open import Data.Product
import deBruijn.Context.Basics          as Basics
import deBruijn.Context.Extension.Right as Right
open import Function.Base hiding (_∋_)
open import Level using (_⊔_)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open Basics Uni
open Right  Uni
open P.≡-Reasoning

------------------------------------------------------------------------
-- Term-like things

record Term-like ℓ : Set (i ⊔ u ⊔ e ⊔ Level.suc ℓ) where
  infix 3 _⊢_
  field
    _⊢_ : (Γ : Ctxt) → Type Γ → Set ℓ
    ⟦_⟧ : ∀ {Γ σ} → Γ ⊢ σ → Value Γ σ

  -- Equality of term-like things.

  record [⊢] : Set (i ⊔ u ⊔ e ⊔ ℓ) where
    constructor [_]
    field
      {Γ} : Ctxt
      {σ} : Type Γ
      t   : Γ ⊢ σ

  infix 4 _≅-⊢_

  _≅-⊢_ : ∀ {Γ₁ σ₁} (t₁ : Γ₁ ⊢ σ₁)
            {Γ₂ σ₂} (t₂ : Γ₂ ⊢ σ₂) → Set _
  t₁ ≅-⊢ t₂ = _≡_ {A = [⊢]} [ t₁ ] [ t₂ ]

  ≅-⊢-⇒-≡ : ∀ {Γ σ} {t₁ t₂ : Γ ⊢ σ} →
            t₁ ≅-⊢ t₂ → t₁ ≡ t₂
  ≅-⊢-⇒-≡ P.refl = P.refl

  -- Certain uses of substitutivity can be removed.

  drop-subst-⊢ :
    ∀ {a} {A : Set a} {x₁ x₂ : A} {Γ}
    (f : A → Type Γ) {t} (eq : x₁ ≡ x₂) →
    P.subst (λ x → Γ ⊢ f x) eq t ≅-⊢ t
  drop-subst-⊢ f P.refl = P.refl

  -- A congruence lemma.

  ⟦⟧-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁}
              {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
            t₁ ≅-⊢ t₂ → ⟦ t₁ ⟧ ≅-Value ⟦ t₂ ⟧
  ⟦⟧-cong P.refl = P.refl

-- Values are term-like.

Val : Term-like _
Val = record { _⊢_ = Value; ⟦_⟧ = id }

-- Variables are term-like.

Var : Term-like _
Var = record { _⊢_ = _∋_; ⟦_⟧ = lookup }

------------------------------------------------------------------------
-- Families of functions which, on the semantic side, correspond to
-- the application of a given context morphism

record [_⟶_] {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂)
             {Γ Δ : Ctxt} (ρ̂ : Γ ⇨̂ Δ) : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
  constructor _,_

  open Term-like T₁ renaming (_⊢_ to _⊢₁_; ⟦_⟧ to ⟦_⟧₁)
  open Term-like T₂ renaming (_⊢_ to _⊢₂_; ⟦_⟧ to ⟦_⟧₂)

  field
    function    : ∀ σ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂
    corresponds :
      ∀ σ (t : Γ ⊢₁ σ) → ⟦ t ⟧₁ /̂Val ρ̂ ≅-Value ⟦ function σ t ⟧₂

-- Functions which do not change the context or type.

[_⟶⁼_] : ∀ {t₁ t₂} → Term-like t₁ → Term-like t₂ → Set _
[ T₁ ⟶⁼ T₂ ] = ∀ {Γ} → [ T₁ ⟶ T₂ ] îd[ Γ ]

-- Projections. (The fields above have explicit σ's to avoid some
-- problems; the projections below have implicit σ's.)

infixl 9 _·_

_·_ : ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
      let open Term-like T₁ renaming (_⊢_ to _⊢₁_)
          open Term-like T₂ renaming (_⊢_ to _⊢₂_) in
      ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
      [ T₁ ⟶ T₂ ] ρ̂ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂
_·_ f = [_⟶_].function f _

corresponds :
  ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
  let open Term-like T₁ renaming (_⊢_ to _⊢₁_; ⟦_⟧ to ⟦_⟧₁)
      open Term-like T₂ renaming (⟦_⟧ to ⟦_⟧₂) in
  ∀ {Γ Δ : Ctxt} {ρ̂ : Γ ⇨̂ Δ} {σ}
  (f : [ T₁ ⟶ T₂ ] ρ̂) (t : Γ ⊢₁ σ) →
  ⟦ t ⟧₁ /̂Val ρ̂ ≅-Value ⟦ f · t ⟧₂
corresponds f = [_⟶_].corresponds f _

-- Weakening of variables (the successor function).

weaken∋ : ∀ {Γ} {σ : Type Γ} → [ Var ⟶ Var ] ŵk[ σ ]
weaken∋ = record
  { function    = λ _ → suc
  ; corresponds = λ _ _ → P.refl
  }

weaken∋[_] : ∀ {Γ} (σ : Type Γ) → [ Var ⟶ Var ] ŵk[ σ ]
weaken∋[ _ ] = weaken∋

-- Lifts a function on variables, f, to a function which leaves a
-- prefix of the context unchanged and otherwise behaves as f.

lift : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} →
       [ Var ⟶ Var ] ρ̂ → ∀ Γ⁺ → [ Var ⟶ Var ] (ρ̂ ↑̂⁺ Γ⁺)
lift             f ε        = f
lift {Γ} {Δ} {ρ̂} f (Γ⁺ ▻ σ) = record
  { function    = function
  ; corresponds = corr
  }
  where
  function : ∀ τ → Γ ++⁺ Γ⁺ ▻ σ ∋ τ →
             Δ ++⁺ (Γ⁺ ▻ σ) /̂⁺ ρ̂ ∋ τ /̂ ρ̂ ↑̂⁺ (Γ⁺ ▻ σ)
  function ._ zero    = zero
  function ._ (suc x) = suc (lift f Γ⁺ · x)

  abstract
    corr : ∀ τ (x : Γ ++⁺ Γ⁺ ▻ σ ∋ τ) →
           lookup x /̂Val ρ̂ ↑̂⁺ (Γ⁺ ▻ σ) ≅-Value lookup (function _ x)
    corr ._ zero    = P.refl
    corr ._ (suc x) = begin
      [ lookup x /̂Val ρ̂ ↑̂⁺ Γ⁺ /̂Val ŵk  ]  ≡⟨ /̂Val-cong (corresponds (lift f Γ⁺) x) P.refl ⟩
      [ lookup (lift f Γ⁺ · x) /̂Val ŵk ]  ≡⟨ P.refl ⟩
      [ lookup (suc (lift f Γ⁺ · x))   ]  ∎

------------------------------------------------------------------------
-- Equality for the functions introduced above

-- Note that the definition of equality does not take the
-- "corresponds" proof into account.

record [⟶] {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂)
           : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
  constructor [_]
  open Term-like T₁ renaming (_⊢_ to _⊢₁_)
  open Term-like T₂ renaming (_⊢_ to _⊢₂_)
  field
    {Γ Δ} : Ctxt
    {ρ̂}   : Γ ⇨̂ Δ
    f     : ∀ σ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂

[_]⟶ : ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂}
         {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} →
       [ T₁ ⟶ T₂ ] ρ̂ → [⟶] T₁ T₂
[ f ]⟶ = [ [_⟶_].function f ]

-- Equality is defined as a record type to make it possible to infer
-- ρ₁ and ρ₂ from a value of type ρ₁ ≅-⟶ ρ₂.

infix 4 _≅-⟶_

record _≅-⟶_
  {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂}
  {Γ₁ Δ₁ : Ctxt} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} (f₁ : [ T₁ ⟶ T₂ ] ρ̂₁)
  {Γ₂ Δ₂ : Ctxt} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} (f₂ : [ T₁ ⟶ T₂ ] ρ̂₂)
  : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
  constructor [_]
  field
    [f₁]⟶≡[f₂]⟶ : [ f₁ ]⟶ ≡ [ f₂ ]⟶

-- Some equational reasoning combinators.

module ≅-⟶-Reasoning
  {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂}
  where

  infix  3 _∎-⟶
  infixr 2 _≅-⟶⟨_⟩_

  _≅-⟶⟨_⟩_ : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁}
               {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂}
               {Γ₃ Δ₃} {ρ̂₃ : Γ₃ ⇨̂ Δ₃}
             (f₁ : [ T₁ ⟶ T₂ ] ρ̂₁) {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂}
                                   {f₃ : [ T₁ ⟶ T₂ ] ρ̂₃} →
             f₁ ≅-⟶ f₂ → f₂ ≅-⟶ f₃ → f₁ ≅-⟶ f₃
  _ ≅-⟶⟨ [ f₁≅f₂ ] ⟩ [ f₂≅f₃ ] = [ P.trans f₁≅f₂ f₂≅f₃ ]

  _∎-⟶ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (f : [ T₁ ⟶ T₂ ] ρ̂) → f ≅-⟶ f
  _ ∎-⟶ = [ P.refl ]

  sym-⟶ : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {f₁ : [ T₁ ⟶ T₂ ] ρ̂₁}
            {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂} →
          f₁ ≅-⟶ f₂ → f₂ ≅-⟶ f₁
  sym-⟶ [ f₁≅f₂ ] = [ P.sym f₁≅f₂ ]

open ≅-⟶-Reasoning public

-- A setoid for [_⟶_].

[_⟶_]-setoid : ∀ {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂) →
             ∀ {Γ Δ} → Γ ⇨̂ Δ → Setoid _ _
[ T₁ ⟶ T₂ ]-setoid ρ̂ = record
  { Carrier       = [ T₁ ⟶ T₂ ] ρ̂
  ; _≈_           = λ f₁ f₂ → f₁ ≅-⟶ f₂
  ; isEquivalence = record
    { refl  = _ ∎-⟶
    ; sym   = sym-⟶
    ; trans = λ p q → _ ≅-⟶⟨ p ⟩ q
    }
  }

-- A congruence lemma.

·-cong :
  ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
  let open Term-like T₁ renaming (_⊢_ to _⊢₁_; _≅-⊢_ to _≅-⊢₁_)
      open Term-like T₂ renaming (_⊢_ to _⊢₂_; _≅-⊢_ to _≅-⊢₂_) in
  ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {f₁ : [ T₁ ⟶ T₂ ] ρ̂₁} {t₁ : Γ₁ ⊢₁ σ₁}
    {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂} {t₂ : Γ₂ ⊢₁ σ₂} →
  f₁ ≅-⟶ f₂ → t₁ ≅-⊢₁ t₂ → f₁ · t₁ ≅-⊢₂ f₂ · t₂
·-cong {f₁ = _ , _} {f₂ = ._ , _} [ P.refl ] P.refl = P.refl

abstract

  -- Two variants of extensional equality (assuming ordinary
  -- extensional equality).

  extensional-equality₁ :
    ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
    let open Term-like T₁ renaming (_⊢_ to _⊢₁_)
        open Term-like T₂ renaming (_≅-⊢_ to _≅-⊢₂_)
    in
    E.Extensionality (i ⊔ u ⊔ e ⊔ t₁) (t₁ ⊔ t₂) →
    ∀ {Γ Δ₁} {ρ̂₁ : Γ ⇨̂ Δ₁} {f₁ : [ T₁ ⟶ T₂ ] ρ̂₁}
        {Δ₂} {ρ̂₂ : Γ ⇨̂ Δ₂} {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂} →
    ρ̂₁ ≅-⇨̂ ρ̂₂ → (∀ {σ} (t : Γ ⊢₁ σ) → f₁ · t ≅-⊢₂ f₂ · t) →
    f₁ ≅-⟶ f₂
  extensional-equality₁ {t₁} {t₂} {T₂ = T₂} ext P.refl f₁≅f₂ =
    [ P.cong [_] (ext₁ λ σ → ext₂ λ t → ≅-⊢₂-⇒-≡ (f₁≅f₂ t)) ]
    where
    open Term-like T₂ using () renaming (≅-⊢-⇒-≡ to ≅-⊢₂-⇒-≡)

    ext₁ : E.Extensionality (i ⊔ u ⊔ e) (t₁ ⊔ t₂)
    ext₁ = E.lower-extensionality t₁ Level.zero ext

    ext₂ : E.Extensionality t₁ t₂
    ext₂ = E.lower-extensionality (i ⊔ u ⊔ e) t₁ ext

  extensional-equality₂ :
    ∀ {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} →
    let open Term-like T₁ renaming (_≅-⊢_ to _≅-⊢₁_; _⊢_ to _⊢₁_)
        open Term-like T₂ renaming (_≅-⊢_ to _≅-⊢₂_)
    in
    E.Extensionality (i ⊔ u ⊔ e ⊔ t₁) (t₁ ⊔ t₂) →
    ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {f₁ : [ T₁ ⟶ T₂ ] ρ̂₁}
      {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {f₂ : [ T₁ ⟶ T₂ ] ρ̂₂} →
    ρ̂₁ ≅-⇨̂ ρ̂₂ →
    (∀ {σ₁} {t₁ : Γ₁ ⊢₁ σ₁} {σ₂} {t₂ : Γ₂ ⊢₁ σ₂} →
       t₁ ≅-⊢₁ t₂ → f₁ · t₁ ≅-⊢₂ f₂ · t₂) →
    f₁ ≅-⟶ f₂
  extensional-equality₂ {T₁ = T₁} ext P.refl f₁≅f₂ =
    extensional-equality₁ ext P.refl (λ t → f₁≅f₂ (P.refl {x = [ t ]}))
    where open Term-like T₁ using ([_])

  -- lift ∘ weaken∋ sort of commutes with a lifted version of itself.

  lift-weaken∋-lift-lift-weaken∋ :
    ∀ {Γ} σ Γ⁺ τ Γ⁺⁺ {υ} (x : Γ ++⁺ Γ⁺ ++⁺ Γ⁺⁺ ∋ υ) →
    lift weaken∋[ τ /̂ ŵk ↑̂⁺ Γ⁺ ] (Γ⁺⁺ /̂⁺ ŵk ↑̂⁺ Γ⁺) ·
         (lift (lift weaken∋[ σ ] Γ⁺) Γ⁺⁺ · x) ≅-∋
    lift (lift weaken∋[ σ ] (Γ⁺ ▻ τ)) (Γ⁺⁺ /̂⁺ ŵk) ·
         (lift weaken∋[ τ ] Γ⁺⁺ · x)
  lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ ε         x       = P.refl
  lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ (Γ⁺⁺ ▻ υ) zero    =
    zero-cong (/̂-↑̂⁺-/̂-ŵk-↑̂⁺ τ (ŵk ↑̂⁺ Γ⁺) Γ⁺⁺ υ)
  lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ (Γ⁺⁺ ▻ υ) (suc x) =
    suc-cong (/̂-↑̂⁺-/̂-ŵk-↑̂⁺ τ (ŵk ↑̂⁺ Γ⁺) Γ⁺⁺ υ)
             (lift-weaken∋-lift-lift-weaken∋ σ Γ⁺ τ Γ⁺⁺ x)

------------------------------------------------------------------------
-- Term-like t and [_⟶_] form a category

-- At least if we ignore the context morphism index.

-- Identity.

[id] : ∀ {t} {T : Term-like t} {Γ} → [ T ⟶ T ] îd[ Γ ]
[id] = record { function = λ _ → id; corresponds = λ _ _ → P.refl }

-- Composition.

infixl 9 _[∘]_

_[∘]_ : ∀ {t₁ t₂ t₃}
          {T₁ : Term-like t₁} {T₂ : Term-like t₂} {T₃ : Term-like t₃}
          {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
        [ T₂ ⟶ T₃ ] ρ̂₂ → [ T₁ ⟶ T₂ ] ρ̂₁ → [ T₁ ⟶ T₃ ] (ρ̂₁ ∘̂ ρ̂₂)
_[∘]_ {T₁ = T₁} {T₂} {T₃} {ρ̂₁ = ρ̂₁} {ρ̂₂} f g = record
  { function    = λ _ → _·_ f ∘ _·_ g
  ; corresponds = corr
  }
  where
  open P.≡-Reasoning
  open Term-like T₁ renaming (⟦_⟧ to ⟦_⟧₁; _⊢_ to _⊢₁_)
  open Term-like T₂ renaming (⟦_⟧ to ⟦_⟧₂)
  open Term-like T₃ renaming (⟦_⟧ to ⟦_⟧₃)

  abstract
    corr : ∀ σ (t : _ ⊢₁ σ) →
           ⟦ t ⟧₁ /̂Val ρ̂₁ ∘̂ ρ̂₂ ≅-Value ⟦ f · (g · t) ⟧₃
    corr = λ σ t → begin
      [ ⟦ t ⟧₁ /̂Val ρ̂₁ ∘̂ ρ̂₂ ]  ≡⟨ /̂Val-cong (corresponds g t) P.refl ⟩
      [ ⟦ g · t ⟧₂ /̂Val ρ̂₂  ]  ≡⟨ corresponds f (g · t) ⟩
      [ ⟦ f · (g · t) ⟧₃    ]  ∎

-- [id] and _[∘]_ preserve equality.

[id]-cong :
  ∀ {t} {T : Term-like t} {Γ₁ Γ₂} →
  Γ₁ ≅-Ctxt Γ₂ → [id] {T = T} {Γ = Γ₁} ≅-⟶ [id] {T = T} {Γ = Γ₂}
[id]-cong P.refl = [ P.refl ]

private
 module Dummy {t₁ t₂} {T₁ : Term-like t₁} {T₂ : Term-like t₂} where

  [∘]-cong : ∀ {t₃} {T₃ : Term-like t₃}
               {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
               {f₁₁ : [ T₁ ⟶ T₂ ] ρ̂₁₁} {f₂₁ : [ T₂ ⟶ T₃ ] ρ̂₂₁}
               {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂}
               {f₁₂ : [ T₁ ⟶ T₂ ] ρ̂₁₂} {f₂₂ : [ T₂ ⟶ T₃ ] ρ̂₂₂} →
             f₁₁ ≅-⟶ f₁₂ → f₂₁ ≅-⟶ f₂₂ → f₂₁ [∘] f₁₁ ≅-⟶ f₂₂ [∘] f₁₂
  [∘]-cong {f₁₁ = _ , _} {f₂₁ = _ , _} {f₁₂ = ._ , _} {f₂₂ = ._ , _}
           [ P.refl ] [ P.refl ] = [ P.refl ]

  -- [id] is a left and right identity of _[∘]_, which is associative.

  [id]-[∘] : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
             (f : [ T₁ ⟶ T₂ ] ρ̂) → [id] [∘] f ≅-⟶ f
  [id]-[∘] f = [ P.refl ]

  [∘]-[id] : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
             (f : [ T₁ ⟶ T₂ ] ρ̂) → f [∘] [id] ≅-⟶ f
  [∘]-[id] f = [ P.refl ]

  [∘]-[∘] :
    ∀ {t₃ t₄} {T₃ : Term-like t₃} {T₄ : Term-like t₄}
      {Γ Δ Ε Ζ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {ρ̂₃ : Ε ⇨̂ Ζ}
    (f₃ : [ T₃ ⟶ T₄ ] ρ̂₃) (f₂ : [ T₂ ⟶ T₃ ] ρ̂₂)
    (f₁ : [ T₁ ⟶ T₂ ] ρ̂₁) →
    f₃ [∘] (f₂ [∘] f₁) ≅-⟶ (f₃ [∘] f₂) [∘] f₁
  [∘]-[∘] f₃ f₂ f₁ = [ P.refl ]

open Dummy public

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
module Logic.Propositional.Proofs.Structures where

import      Data.Tuple as Tuple
import      Lvl
open import Functional
open import Logic
open import Logic.Propositional
import      Logic.Propositional.Theorems as Theorems
open import Structure.Operator.Properties
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

open import Logic.Propositional.Equiv public

private variable ℓ ℓ₁ ℓ₂ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable T A B : Type{ℓ}

instance
  [→]-reflexivity : Reflexivity{ℓ₂ = ℓ}(_→ᶠ_)
  [→]-reflexivity = intro Theorems.[→]-reflexivity

instance
  [→]-transitivity : Transitivity{ℓ₂ = ℓ}(_→ᶠ_)
  [→]-transitivity = intro Theorems.[→]-transitivity

module _ where
  [←]-reflexivity : Reflexivity{ℓ₂ = ℓ}(_←_)
  [←]-reflexivity = intro Theorems.[→]-reflexivity

module _ where
  [←]-transitivity : Transitivity{ℓ₂ = ℓ}(_←_)
  [←]-transitivity = intro (swap Theorems.[→]-transitivity)

instance
  [↔]-antisymmetry : Antisymmetry{ℓ₂ = ℓ}(_→ᶠ_)(_↔_)
  [↔]-antisymmetry = intro(swap [↔]-intro)

open import Structure.Relator
open import Structure.Function
open import Structure.Operator
module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {P : T → Type{ℓ}} where
  relator-function₁ : UnaryRelator(P) ↔ Function ⦃ equiv-B = [↔]-equiv ⦄ (P)
  UnaryRelator.substitution (Tuple.left  relator-function₁ (intro congruence))   xy = [↔]-to-[→] (congruence xy)
  Function.congruence       (Tuple.right relator-function₁ (intro substitution)) xy = [↔]-intro (substitution(symmetry(_≡_) xy)) (substitution xy)

module _ ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ {P : A → B → Type{ℓ}} where
  relator-function₂ : BinaryRelator(P) ↔ BinaryOperator ⦃ equiv-B = [↔]-equiv ⦄ (P)
  BinaryRelator.substitution (Tuple.left  relator-function₂ (intro congruence))   xy1 xy2 = [↔]-to-[→] (congruence xy1 xy2)
  BinaryOperator.congruence  (Tuple.right relator-function₂ (intro substitution)) xy1 xy2 = [↔]-intro (substitution(symmetry(_≡_) xy1) (symmetry(_≡_) xy2)) (substitution xy1 xy2)

{- TODO: Maybe a general Equiv and Transitivity for (_↔_) is possible with indexed relation structures? What I mean by indexed:
test : ∀{ℓ₁ ℓ₂}{T : TYPE ℓ₁}{ℓ : T → Lvl.Level} → ((x : T) → TYPE(ℓ x)) → TYPE ℓ₂

test2 : TYPE Lvl.𝟎
test2 = test{T = Lvl.Level}{ℓ = Lvl.𝐒} (\ℓ → TYPE ℓ)

instead of:

test : ∀{ℓ₁ ℓ₂}{T : TYPE ℓ₁}{ℓ : Lvl.Level} → TYPE ℓ → TYPE ℓ₂

Then all special cases for (_→_) and (_↔_) would finally be redundant. Also, substitution could be a special case of congruence, so *Relator would be special cases of *Operator
-}

instance
  [∧]-symmetry : Symmetry{ℓ₂ = ℓ}(_∧_)
  [∧]-symmetry = intro Theorems.[∧]-symmetry

instance
  [∨]-symmetry : Symmetry{ℓ₂ = ℓ}(_∨_)
  [∨]-symmetry = intro Theorems.[∨]-symmetry

instance
  [∧][↔]-sub : (_∧_) ⊆₂ (_↔_ {ℓ₁}{ℓ₂})
  [∧][↔]-sub = intro Theorems.[∧]-to-[↔]

instance
  [∧][→]-sub : (_∧_) ⊆₂ (_→ᶠ_ {ℓ₁}{ℓ₂})
  [∧][→]-sub = intro Theorems.[∧]-to-[→]

instance
  [∧][←]-sub : (_∧_) ⊆₂ (_←_ {ℓ₁}{ℓ₂})
  [∧][←]-sub = intro Theorems.[∧]-to-[←]

instance
  [∧][∨]-sub : (_∧_) ⊆₂ (_∨_ {ℓ₁}{ℓ₂})
  [∧][∨]-sub = intro Theorems.[∧]-to-[∨]

instance
  [∧]-associativity : Associativity ⦃ [↔]-equiv ⦄ (_∧_ {ℓ})
  [∧]-associativity = intro Theorems.[∧]-associativity

instance
  [∧]-operator : BinaryOperator ⦃ [↔]-equiv{ℓ₁} ⦄ ⦃ [↔]-equiv{ℓ₂} ⦄ ⦃ [↔]-equiv ⦄ (_∧_)
  BinaryOperator.congruence [∧]-operator = Theorems.[∧]-map-[↔]

instance
  [∨]-operator : BinaryOperator ⦃ [↔]-equiv{ℓ₁} ⦄ ⦃ [↔]-equiv{ℓ₂} ⦄ ⦃ [↔]-equiv ⦄ (_∨_)
  BinaryOperator.congruence [∨]-operator = Theorems.[∨]-map-[↔]

instance
  [→]-operator : BinaryOperator ⦃ [↔]-equiv{ℓ₁} ⦄ ⦃ [↔]-equiv{ℓ₂} ⦄ ⦃ [↔]-equiv ⦄ (_→ᶠ_)
  BinaryOperator.congruence [→]-operator = Theorems.[→]-map-[↔]

instance
  [↔]-operator : BinaryOperator ⦃ [↔]-equiv{ℓ₁} ⦄ ⦃ [↔]-equiv{ℓ₂} ⦄ ⦃ [↔]-equiv ⦄ (_↔_)
  BinaryOperator.congruence [↔]-operator = Theorems.[↔]-map-[↔]


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

module Examples.Sorting.Parallel where

open import Examples.Sorting.Parallel.Comparable

open import Calf costMonoid
open import Calf.Types.Nat
open import Calf.Types.List

open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
open import Data.Product using (_,_)
open import Data.Nat using (z≤n; s≤s)

test/forward  = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ 10 ∷ 11 ∷ 12 ∷ 13 ∷ 14 ∷ 15 ∷ 16 ∷ []
test/backward = 16 ∷ 15 ∷ 14 ∷ 13 ∷ 12 ∷ 11 ∷ 10 ∷ 9 ∷ 8 ∷ 7 ∷ 6 ∷ 5 ∷ 4 ∷ 3 ∷ 2 ∷ 1 ∷ []
test/shuffled = 4 ∷ 8 ∷ 12 ∷ 16 ∷ 13 ∷ 3 ∷ 5 ∷ 14 ∷ 9 ∷ 6 ∷ 7 ∷ 10 ∷ 11 ∷ 1 ∷ 2 ∷ 15 ∷ []

module Ex/InsertionSort where
  import Examples.Sorting.Parallel.InsertionSort NatComparable as Sort

  list' = list nat

  ex/insert : cmp (F list')
  ex/insert = Sort.insert 3 (1 ∷ 2 ∷ 4 ∷ [])

  ex/sort : cmp (F list')
  ex/sort = Sort.sort (1 ∷ 5 ∷ 3 ∷ 1 ∷ 2 ∷ [])

  ex/sort/forward : cmp (F list')
  ex/sort/forward = Sort.sort test/forward  -- cost: 15 , 15

  ex/sort/backward : cmp (F list')
  ex/sort/backward = Sort.sort test/backward  -- cost: 120 , 120

  ex/sort/shuffled : cmp (F list')
  ex/sort/shuffled = Sort.sort test/shuffled  -- cost: 76 , 76

module Ex/MergeSort where
  import Examples.Sorting.Parallel.MergeSort NatComparable as Sort

  list' = list nat

  ex/split : cmp (F Sort.pair)
  ex/split = Sort.split (6 ∷ 2 ∷ 8 ∷ 3 ∷ 1 ∷ 8 ∷ 5 ∷ [])

  ex/merge : cmp (F list')
  ex/merge = Sort.merge (2 ∷ 3 ∷ 6 ∷ 8 ∷ [] , 1 ∷ 5 ∷ 8 ∷ [])

  ex/sort : cmp (F list')
  ex/sort = Sort.sort (1 ∷ 5 ∷ 3 ∷ 1 ∷ 2 ∷ [])

  ex/sort/forward : cmp (F list')
  ex/sort/forward = Sort.sort test/forward  -- cost: 32, 15

  ex/sort/backward : cmp (F list')
  ex/sort/backward = Sort.sort test/backward  -- cost: 32, 15

  ex/sort/shuffled : cmp (F list')
  ex/sort/shuffled = Sort.sort test/shuffled  -- cost: 47, 26

module Ex/MergeSortPar where
  import Examples.Sorting.Parallel.MergeSortPar NatComparable as Sort

  list' = list nat

  ex/split : cmp (F Sort.pair)
  ex/split = Sort.split (6 ∷ 2 ∷ 8 ∷ 3 ∷ 1 ∷ 8 ∷ 5 ∷ [])

  ex/splitMid : cmp (F Sort.triple)
  ex/splitMid = Sort.splitMid test/forward (s≤s z≤n)

  ex/splitBy : cmp (F Sort.pair)
  ex/splitBy = Sort.splitBy test/forward 5

  ex/merge : cmp (F list')
  ex/merge = Sort.merge (2 ∷ 3 ∷ 6 ∷ 8 ∷ [] , 1 ∷ 5 ∷ 8 ∷ [])

  ex/sort : cmp (F list')
  ex/sort = Sort.sort (1 ∷ 5 ∷ 3 ∷ 1 ∷ 2 ∷ [])

  ex/sort/forward : cmp (F list')
  ex/sort/forward = Sort.sort test/forward  -- cost: 40, 21

  ex/sort/backward : cmp (F list')
  ex/sort/backward = Sort.sort test/backward  -- cost: 40, 21

  ex/sort/shuffled : cmp (F list')
  ex/sort/shuffled = Sort.sort test/shuffled  -- cost: 43, 17

module SortEquivalence (M : Comparable) where
  open Comparable M
  open import Examples.Sorting.Parallel.Core M

  import Examples.Sorting.Parallel.InsertionSort M as ISort
  import Examples.Sorting.Parallel.MergeSort     M as MSort
  import Examples.Sorting.Parallel.MergeSortPar  M as PSort

  isort≡msort : ◯ (ISort.sort ≡ MSort.sort)
  isort≡msort = IsSort⇒≡ ISort.sort ISort.sort/correct MSort.sort MSort.sort/correct

  msort≡psort : ◯ (MSort.sort ≡ PSort.sort)
  msort≡psort = IsSort⇒≡ MSort.sort MSort.sort/correct PSort.sort PSort.sort/correct

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Day3 where

open import Data.String as String
open import Data.Maybe
open import Foreign.Haskell using (Unit)
open import Data.List as List hiding (fromMaybe)
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
import Data.Nat.Show as ℕs
open import Data.Char
open import Data.Vec as Vec renaming (_>>=_ to _VV=_ ; toList to VecToList)
open import Data.Product
open import Relation.Nullary
open import Data.Nat.Properties
open import Data.Bool.Base
open import AocIO
open import AocUtil
open import AocVec
open import Relation.Binary.PropositionalEquality
open import EvenOdd

printUsage : String → IO Unit
printUsage name = printString ("Usage: " String.++ name String.++ " NUMBER\n(NUMBER > 0)")

sqr : (l : ℕ) → Σ[ k ∈ ℕ ] (k ≡ l * l)
sqr l = l * l , refl

first-larger-odd-square : {m : ℕ} → (n : ℕ) → suc m ≡ n → Σ[ k ∈ ℕ ] (n ≤ (k * k) × Odd k)
first-larger-odd-square {m} n n-is-suc = helper 1 m n-is-suc oddOne
  where
    helper : (m diff : ℕ) → (m + diff) ≡ n → Odd m → Σ[ k ∈ ℕ ] (n ≤ (k * k) × Odd k)
    helper m (suc (suc diff)) p m-is-odd with sqr m
    ... | (m² , m²≡m*m) with n ≤? m²
    ... | yes n≤m² rewrite m²≡m*m = m , n≤m² , m-is-odd
    ... | no _ = helper (suc (suc m)) diff rewr-p (oddSuc m-is-odd)
      where
        rewr-p : suc (suc m + diff) ≡ n
        rewr-p with (+-suc m diff) | (+-suc m (suc diff))
        ... | s | t rewrite (sym s) | t = p
    helper m zero p m-is-odd rewrite (+-identityʳ m) with (sqr m)
    ... | (m² , q) = m , (my-proof n refl) , m-is-odd
      where
        my-proof : (k : ℕ) → k ≡ n → n ≤ m * m
        my-proof k p₁ rewrite sym p₁ with k
        ... | zero = z≤n
        ... | suc kk rewrite p with (m≤m+n kk (kk * suc kk))
        ... | kk≤kk+junk = s≤s kk≤kk+junk
    helper zero (suc zero) p ()
    helper (suc zero) (suc zero) p m-is-odd rewrite sym p = 3 , (s≤s (s≤s z≤n) , oddSuc oddOne)
    helper (suc (suc m)) (suc zero) p m-is-odd = (suc (suc m)) , my-proof n refl , m-is-odd
      where
        my-proof : (k : ℕ) → k ≡ n → n ≤ suc (suc (m + suc (suc (m + m * suc (suc m)))))
        my-proof k p₁ rewrite sym p₁ with k
        ... | zero = z≤n
        -- we replace with p and get an expression 1 + m ≤ suc (suc m + junk)
        -- +-comm m 1 turns 1 + m into suc m
        -- sym +-suc turns m + suc junk into suc (m + junk) to match the number on the other side
        -- finally we cancel suc on both sides and use m ≤ m + junk
        ... | suc kk rewrite sym p | +-comm m 1 | +-suc m (suc (m + m * suc (suc m))) = s≤s (s≤s (s≤s (m≤m+n m (suc (m + m * suc (suc m))))))

oddness : ∀ {n} → Odd n → ℕ
oddness oddOne = 1
oddness (oddSuc v) = suc (oddness v)

ring-for-square# : {m : ℕ} → (n : ℕ) → suc m ≡ n → Σ[ k ∈ ℕ ] Odd k × ℕ
ring-for-square# zero ()
ring-for-square# (suc n) p with (first-larger-odd-square (suc n) (cong suc refl))
... | k , proj₄ , k-odd = k , k-odd , (oddness k-odd)

ring-corners : {m : ℕ} → Odd m → ℕ × ℕ × ℕ × ℕ × ℕ
ring-corners oddOne = 1 , (1 , (1 , 1 , 1))
ring-corners {(suc (suc n))} (oddSuc _)  = (n * n) , ((proj₁ first-corner) , ((proj₁ second-corner) , ((proj₁ third-corner) , (proj₁ fourth-corner))))
  where
    first-corner : Σ[ k ∈ ℕ ] k ≡ suc ((n * n) + n)
    first-corner = suc (n * n + n) , refl
    second-corner : Σ[ k ∈ ℕ ] k ≡ suc (suc ((n * n) + n + n))
    second-corner = (suc (suc (n * n + n + n))) , refl
    third-corner : Σ[ k ∈ ℕ ] k ≡ suc (suc (suc ((n * n) + n + n + n)))
    third-corner = suc (suc (suc (n * n + n + n + n))) , refl
    fourth-corner : Σ[ k ∈ ℕ ] k ≡ suc (suc (n + suc (suc (n + n * suc (suc n)))))
    fourth-corner = sqr (suc (suc n))
    ring-length : Σ[ k ∈ ℕ ] k ≡ (2 * (suc (suc n))) + (2 * n)
    ring-length = (2 * (suc (suc n)) + 2 * n) , refl
    -- proof that fourth-corner = ring-length + prev-fourth-corner
    ring-length-proof : {m l : ℕ} → m ≡ suc (suc (n + suc (suc (n + n * suc (suc n))))) → l ≡ (2 * (suc (suc n))) + (2 * n) →  l + (n * n) ≡ m
    ring-length-proof p q rewrite p | q = cong suc (cong suc my-proof)
      where
        halp : n + n + (n + n) ≡ n + n + n + n
        halp = begin
           n + n + (n + n)
           ≡⟨ sym (+-assoc (n + n) n n) ⟩
           n + n + n + n ∎
          where
            open ≡-Reasoning
        halp-again : n * n + (n + n + n + n) ≡ n * n + n + n + n + n
        halp-again with +-assoc (n * n) (n + n + n) n
        ... | p₁  rewrite sym p₁ with +-assoc (n * n) (n + n) n
        ... | p₂ rewrite sym p₂ with +-assoc (n * n) n n
        ... | p₃ rewrite sym p₃ = refl
        my-proof : n + suc (suc (n + 0)) + (n + (n + 0)) + n * n ≡ n + suc (suc (n + n * suc (suc n)))
        my-proof rewrite +-identityʳ n | +-*-suc n (suc n) | +-*-suc n n with +-comm n (suc (suc n)) | +-comm n (suc (suc (n + (n + (n + n * n)))))
        ... | p₁ | p₂ rewrite p₁ | p₂ with +-comm n (n + n * n) | +-comm n (n + n * n + n) | +-comm n (n * n) | +-comm (n + n + (n + n)) (n * n)
        ... | p₃ | p₄ | p₅ | p₆ rewrite p₃ | p₄ | p₅ | p₆ | halp | halp-again = cong suc (cong suc refl)
    -- Here I'd like a proof that the distance between the corners add up to the length

abs-diff : (n m : ℕ) → ℕ
abs-diff zero m = m
abs-diff (suc n) zero = suc n
abs-diff (suc n) (suc m) = abs-diff n m

min-5 : (a b c d e : ℕ) → ℕ
min-5 a b c d e with a ⊓ b | c ⊓ d
... | min-ab | min-cd with min-ab ⊓ min-cd
... | min-abcd = min-abcd ⊓ e

dist-to-closest-ring-corner : {k : ℕ} → (n : ℕ) → suc k ≡ n → ℕ
dist-to-closest-ring-corner zero ()
dist-to-closest-ring-corner (suc k) p with (ring-for-square# (suc k) p) | (suc k)
... | corner-root , corner-root-odd , ring# | n with ring-corners corner-root-odd
... | c₀ , c₁ , c₂ , c₃ , c₄ with abs-diff n c₀ | abs-diff n c₁ | abs-diff n c₂ | abs-diff n c₃ | abs-diff n c₄
... | n-c₀ | n-c₁ | n-c₂ | n-c₃ | n-c₄ = min-5 n-c₀ n-c₁ n-c₂ n-c₃ n-c₄

dist-to-center : {k : ℕ} → (n : ℕ) → suc k ≡ n → ℕ
dist-to-center zero ()
dist-to-center (suc k) p with (ring-for-square# (suc k) p) | (suc k)
... | corner-root , corner-root-odd , ring# | n with dist-to-closest-ring-corner (suc k) refl
... | dist = abs-diff dist (2 * (pred ring#))

infixr 5 _+++_

_+++_ : String → String → String
_+++_ s1 s2 = s1 String.++ " " String.++ s2

print-corners : {k : ℕ} → (n : ℕ) → suc k ≡ n → IO Unit
print-corners zero ()
print-corners (suc k) p with (ring-for-square# (suc k) p) | (suc k)
... | corner-root , corner-root-odd , ring# | n with ring-corners corner-root-odd
... | c₀ , c₁ , c₂ , c₃ , c₄ with abs-diff n c₀ | abs-diff n c₁ | abs-diff n c₂ | abs-diff n c₃ | abs-diff n c₄
... | n-c₀ | n-c₁ | n-c₂ | n-c₃ | n-c₄ with ℕs.show n-c₀ | ℕs.show n-c₁ | ℕs.show n-c₂ | ℕs.show n-c₃ | ℕs.show n-c₄ | ℕs.show corner-root | ℕs.show ring#
... | s0 | s1 | s2 | s3 | s4 | s5 | s6 = printString (s0 +++ s1 +++ s2 +++ s3 +++ s4 +++ "==" +++ s5 +++ s6)

main : IO Unit
main = mainBuilder main'
  where
    main' : String → (List String) → IO Unit
    main' name (numS ∷ []) with (unsafeParseNat (String.toList numS))
    ... | 0 = printUsage name
    ... | (suc n) =  printString (ℕs.show (dist-to-center (suc n) (cong suc refl)))
    main' name _ = printUsage name


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

open import HoTT

module experimental.NConnected where

  lemma₁ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {n : ℕ₋₂}
    → is-connected n A → is-connected (S n) B
    → has-conn-fibers n f
  lemma₁ f cA cB = λ b → Σ-conn cA (λ a → path-conn cB)

  lemma₂ : ∀ {i} {A B C : Type i}
    → (f : A → B) (g : B → C) {n : ℕ₋₂}
    → has-conn-fibers n (g ∘ f)
    → has-conn-fibers (S n) g
    → has-conn-fibers n f
  lemma₂ f g {n} cA cB b =
    equiv-preserves-conn (eqv b idp ⁻¹) (lemma₁-f′ (g b) (b , idp))
      where
        f′ : ∀ c → hfiber (g ∘ f) c → hfiber g c
        f′ c (a , p) = (f a , p)

        -- We first show [∀ b → is-connected n (hfiber (f′ (g b) (b , idp))) ]
        lemma₁-f′ : ∀ c → has-conn-fibers n (f′ c)
        lemma₁-f′ c = lemma₁ (f′ c) (cA c) (cB c)

        -- The remaining shows [hfiber (f′ (g b) (b , idp))]
        -- is the same as [hfiber f b]
        to : ∀ b p → hfiber f b → hfiber (f′ (g b)) (b , p)
        to ._ p (a , idp) = ((a , p) , idp)

        from′ : ∀ b a → f a == b → hfiber f b
        from′ ._ a idp = (a , idp)

        from : ∀ b p → hfiber (f′ (g b)) (b , p) → hfiber f b
        from b p ((a , q) , r) = from′ b a (fst= r)

        from-to : ∀ b p x → from b p (to b p x) == x
        from-to ._ p (a , idp) = idp

        to-from : ∀ b p x → to b p (from b p x) == x
        to-from b p ((a , q) , r) =
            to b p (from b p ((a , q) , r))
              =⟨ pair=-η r |in-ctx (λ r → to b p (from b p ((a , q) , r))) ⟩
            to b p (from b p ((a , q) , pair= (fst= r) (snd= r)))
              =⟨ lemma b p a q (fst= r) (snd= r) ⟩
            ((a , q) , pair= (fst= r) (snd= r))
              =⟨ ! (pair=-η r) |in-ctx (λ r → ((a , q) , r)) ⟩
            ((a , q) , r)
              ∎
          where
            lemma : ∀ b p a (q : g (f a) == g b)
              → (r : f a == b) (s : q == p [ (λ b′ → g b′ == g b) ↓ r ])
              → to b p (from b p ((a , q) , pair= r s)) == ((a , q) , pair= r s)
            lemma ._ ._ a q idp idp = idp

        eqv : ∀ b p → hfiber f b ≃ hfiber (f′ (g b)) (b , p)
        eqv b p = equiv (to b p) (from b p) (to-from b p) (from-to b p)

  lemma₃ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
    → A ≃ Σ B (hfiber f)
  lemma₃ {A = A} {B} f = equiv to from to-from from-to
    where
      to : A → Σ B (hfiber f)
      to a = (f a , (a , idp))

      from : Σ B (hfiber f) → A
      from (_ , (a , p)) = a

      to-from : ∀ s → to (from s) == s
      to-from (._ , (a , idp)) = idp

      from-to : ∀ a → from (to a) == a
      from-to a = idp

{-
∘-conn : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  → (f : A → B) → (g : B → C) → {n : ℕ₋₂}
  → has-conn-fibers n f
  → has-conn-fibers n g
  → has-conn-fibers n (g ∘ f)
∘-conn f g {⟨-2⟩} cf cg c = -2-conn _
∘-conn f g {S n } cf cg c =
  Trunc-rec
    {P = is-connected (hfiber (g ∘ f) c)}
    (prop-has-level-S n (is-connected-is-prop n A))
    (λ c )
    (cg c)
-}

{-
  lemma₃-path : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
    → A == Σ B (hfiber f)
  lemma₃-path = λ f → ua (lemma₃ f)
-}

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with a single relation
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Reasoning.Base.Single
  {a ℓ} {A : Set a} (_∼_ : Rel A ℓ)
  (refl : Reflexive _∼_) (trans : Transitive _∼_)
  where

------------------------------------------------------------------------
-- Reasoning combinators

-- Re-export combinators from partial reasoning

open import Relation.Binary.Reasoning.Base.Partial _∼_ trans public
  hiding (_∎⟨_⟩)

-- Redefine the terminating combinator now that we have reflexivity

infix  3 _∎

_∎ : ∀ x → x IsRelatedTo x
x ∎ = relTo refl


text:
{-# OPTIONS --universe-polymorphism #-}
module Issue227 where

open import Common.Level

data D (a p b : Level) (A : Set a) (P : A → Set p) : Set (p ⊔ a ⊔ b) where
  d : ((x : A) → P x) → D a p b A P

-- Unsolved trivial constraint: Set (a ⊔ p) =< Set (p ⊔ a).

OK : ∀ {a} {A : Set a} → (A → Set) → A → Set _
OK P = P

NotOK : ∀ {a} {A : Set a} → (P : A → Set) → A → Set _
NotOK P = P

-- Unsolved constraint:
-- \/ (Set (a ⊔ suc zero)) (Set (a ⊔ suc zero)) = \/ (Set (a ⊔ suc zero)) (Set (a ⊔ suc zero))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Induction principles for the total natural numbers inductive predicate
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.Type where

open import FOTC.Base hiding ( succ₁ )

------------------------------------------------------------------------------
-- We define succ₁ outside an abstract block.

succ₁ : D → D
succ₁ n = succ · n

module ConstantAndUnaryFunction where

  -- N using the constant succ.
  data N : D → Set where
    nzero : N zero
    nsucc : ∀ {n} → N n → N (succ · n)

  N-ind : (A : D → Set) →
          A zero →
          (∀ {n} → A n → A (succ · n)) →
          ∀ {n} → N n → A n
  N-ind A A0 h nzero      = A0
  N-ind A A0 h (nsucc Nn) = h (N-ind A A0 h Nn)

  -- N using the unary function succ₁.
  data N₁ : D → Set where
    nzero₁ : N₁ zero
    nsucc₁ : ∀ {n} → N₁ n → N₁ (succ₁ n)

  N-ind₁ : (A : D → Set) →
           A zero →
           (∀ {n} → A n → A (succ₁ n)) →
           ∀ {n} → N₁ n → A n
  N-ind₁ A A0 h nzero₁      = A0
  N-ind₁ A A0 h (nsucc₁ Nn) = h (N-ind₁ A A0 h Nn)

  ----------------------------------------------------------------------------
  -- From N/N₁ to N₁/N.

  N→N₁ : ∀ {n} → N n → N₁ n
  N→N₁ nzero          = nzero₁
  N→N₁ (nsucc {n} Nn) = nsucc₁ (N→N₁ Nn)

  N₁→N : ∀ {n} → N₁ n → N n
  N₁→N nzero₁           = nzero
  N₁→N (nsucc₁ {n} N₁n) = nsucc (N₁→N N₁n)

  ----------------------------------------------------------------------------
  -- From N-ind → N-ind₁.
  N-ind₁' : (A : D → Set) →
            A zero →
            (∀ {n} → A n → A (succ₁ n)) →
            ∀ {n} → N₁ n → A n
  N-ind₁' A A0 h Nn₁ = N-ind A A0 h' (N₁→N Nn₁)
    where
    h' : ∀ {n} → A n → A (succ · n)
    h' {n} An = h An

  ----------------------------------------------------------------------------
  -- From N-ind₁ → N-ind.
  N-ind' : (A : D → Set) →
           A zero →
           (∀ {n} → A n → A (succ · n)) →
           ∀ {n} → N n → A n
  N-ind' A A0 h Nn = N-ind₁ A A0 h' (N→N₁ Nn)
    where
    h' : ∀ {n} → A n → A (succ₁ n)
    h' {n} An = h An

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

module AdditionalHypotheis where

  data N : D → Set where
    nzero : N zero
    nsucc : ∀ {n} → N n → N (succ₁ n)

  -- The induction principle generated by Coq 8.4pl4 when we define
  -- the data type N in Prop.
  N-ind₁ : (A : D → Set) →
           A zero →
           (∀ {n} → N n → A n → A (succ₁ n)) →
           ∀ {n} → N n → A n
  N-ind₁ A A0 h nzero      = A0
  N-ind₁ A A0 h (nsucc Nn) = h Nn (N-ind₁ A A0 h Nn)

  -- The induction principle removing the hypothesis N n from the
  -- inductive step (see Martin-Löf 1971, p. 190).
  N-ind₂ : (A : D → Set) →
            A zero →
           (∀ {n} → A n → A (succ₁ n)) →
           ∀ {n} → N n → A n
  N-ind₂ A A0 h nzero      = A0
  N-ind₂ A A0 h (nsucc Nn) = h (N-ind₂ A A0 h Nn)

  ----------------------------------------------------------------------------
  -- N-ind₂ from N-ind₁.
  N-ind₂' : (A : D → Set) →
            A zero →
            (∀ {n} → A n → A (succ₁ n)) →
            ∀ {n} → N n → A n
  N-ind₂' A A0 h = N-ind₁ A A0 (λ _ → h)

  ----------------------------------------------------------------------------
  -- N-ind₁ from N-ind₂.
  N-ind₁' : (A : D → Set) →
            A zero →
            (∀ {n} → N n → A n → A (succ₁ n)) →
            ∀ {n} → N n → A n
  N-ind₁' A A0 h {n} Nn = ∧-proj₂ (N-ind₂ B B0 h' Nn)
    where
    B : D → Set
    B n = N n ∧ A n

    B0 : B zero
    B0 = nzero , A0

    h' : ∀ {m} → B m → B (succ₁ m)
    h' (Nm , Am) = nsucc Nm , h Nm Am

------------------------------------------------------------------------------
-- References
--
-- Martin-Löf, P. (1971). Hauptsatz for the Intuitionistic Theory of
-- Iterated Inductive Definitions. In: Proceedings of the Second
-- Scandinavian Logic Symposium. Ed. by Fenstad,
-- J. E. Vol. 63. Studies in Logic and the Foundations of
-- Mathematics. North-Holland Publishing Company, pp. 179–216.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Identity

module HoTT.Homotopy where

open variables
private variable f g : A → B

-- Lemma 2.4.3
~-natural : (α : f ~ g) {x y : A} (p : x == y) → α x ∙ ap g p == ap f p ∙ α y
~-natural α {x} refl rewrite α x = refl

~-natural-id : (α : f ~ id) {x y : A} (p : x == y) → α x ∙ p == ap f p ∙ α y
~-natural-id α {x} refl rewrite α x = refl

-- Corollary 2.4.4
~-natural-comm : {f : A → A} (α : f ~ id) → α ∘ f ~ ap f ∘ α
~-natural-comm {f = f} α x = cancelᵣ (α (f x) ∙ₗ ap-id (α x) ⁻¹ ∙ ~-natural α (α x))

module ~-Reasoning where
  _~⟨_⟩_ : (f : Π A P) {g h : Π A P} → f ~ g → g ~ h → f ~ h
  x ~⟨ α ⟩ β = α ∙ₕ β
  infixr 2 _~⟨_⟩_

  _∎ : (f : Π A P) → f ~ f
  _ ∎ = reflₕ
  infix 3 _∎

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module UniDB.Morph.Unit where

open import UniDB.Spec

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

data Unit : MOR where
  unit : {γ : Dom} → Unit γ γ

instance
  iUpUnit : Up Unit
  _↑₁ {{iUpUnit}} unit = unit
  _↑_ {{iUpUnit}} unit δ = unit
  ↑-zero {{iUpUnit}} unit = refl
  ↑-suc {{iUpUnit}} unit δ = refl

  iIdmUnit : Idm Unit
  idm {{iIdmUnit}} _ = unit

  iCompUnit : Comp Unit
  _⊙_ {{iCompUnit}} unit unit = unit

  iUpIdmUnit : UpIdm Unit
  idm-↑₁ {{iUpIdmUnit}} = refl

module _ {T : STX} {{vrT : Vr T}} where

  instance
    iLkUnit :  Lk T Unit
    lk {{iLkUnit}} unit = vr {T = T}

    iLkUpUnit : {{wkT : Wk T}} {{wkVrT : WkVr T}} → LkUp T Unit
    lk-↑₁-zero {{iLkUpUnit}} unit  = refl
    lk-↑₁-suc {{iLkUpUnit}} unit i = sym (wk₁-vr {T = T} i)

    iLkIdmUnit : LkIdm T Unit
    lk-idm {{iLkIdmUnit}} i = refl

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Functor.Base where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Sigma

open import Cubical.Categories.Category

private
  variable
    ℓC ℓC' ℓD ℓD' : Level

record Functor (C : Category ℓC ℓC') (D : Category ℓD ℓD') :
         Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
  no-eta-equality

  open Category

  field
    F-ob  : C .ob → D .ob
    F-hom : {x y : C .ob} → C [ x , y ] → D [ F-ob x , F-ob y ]
    F-id  : {x : C .ob} → F-hom (C .id) ≡ D .id {x = F-ob x}
    F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ])
          → F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)

  isFull = (x y : _) (F[f] : D [ F-ob x , F-ob y ]) → ∃[ f ∈ C [ x , y ] ] F-hom f ≡ F[f]
  isFaithful = (x y : _) (f g : C [ x , y ]) → F-hom f ≡ F-hom g → f ≡ g
  isEssentiallySurj = (d : D .ob) → Σ[ c ∈ C .ob ] CatIso D (F-ob c) d

private
  variable
    ℓ ℓ' : Level
    C D E : Category ℓ ℓ'

open Category
open Functor

-- Helpful notation

-- action on objects
infix 30 _⟅_⟆
_⟅_⟆ : (F : Functor C D)
     → C .ob
     → D .ob
_⟅_⟆ = F-ob

-- action on morphisms
infix 30 _⟪_⟫ -- same infix level as on objects since these will never be used in the same context
_⟪_⟫ : (F : Functor C D)
     → ∀ {x y}
     → C [ x , y ]
     → D [(F ⟅ x ⟆) , (F ⟅ y ⟆)]
_⟪_⟫ = F-hom

-- Functor constructions

𝟙⟨_⟩ : ∀ (C : Category ℓ ℓ') → Functor C C
𝟙⟨ C ⟩ .F-ob x    = x
𝟙⟨ C ⟩ .F-hom f   = f
𝟙⟨ C ⟩ .F-id      = refl
𝟙⟨ C ⟩ .F-seq _ _ = refl

-- functor composition
funcComp : ∀ (G : Functor D E) (F : Functor C D) → Functor C E
(funcComp G F) .F-ob c    = G ⟅ F ⟅ c ⟆ ⟆
(funcComp G F) .F-hom f   = G ⟪ F ⟪ f ⟫ ⟫
(funcComp G F) .F-id      = cong (G ⟪_⟫) (F .F-id) ∙ G .F-id
(funcComp G F) .F-seq f g = cong (G ⟪_⟫) (F .F-seq _ _) ∙ G .F-seq _ _

infixr 30 funcComp
syntax funcComp G F = G ∘F F

_^opF : Functor C D → Functor (C ^op) (D ^op)
(F ^opF) .F-ob      = F .F-ob
(F ^opF) .F-hom     = F .F-hom
(F ^opF) .F-id      = F .F-id
(F ^opF) .F-seq f g = F .F-seq g f

max_stars_repo_name: FernandoLarrain/cubical


text:
module Prelude.Monoid where

open import Prelude.Function
open import Prelude.Maybe

open import Prelude.List

open import Prelude.Semiring
open import Prelude.Semigroup public

open import Prelude.Applicative
open import Prelude.Functor
open import Prelude.Equality

open import Prelude.Variables

record Monoid {a} (A : Set a) : Set a where
  field
    {{super}} : Semigroup A
    mempty : A
open Monoid {{...}} public hiding (super)

{-# DISPLAY Monoid.mempty _ = mempty #-}

record Monoid/Laws {ℓ} (A : Set ℓ) : Set ℓ where
  field
    overlap {{super}} : Monoid A
    left-identity : (e : A) → mempty <> e ≡ e
    right-identity : (e : A) → e <> mempty ≡ e
    -- Using Semigroup/Laws instance creates inference problems
    -- Maby we can do this in a better way?
    monoid-assoc : (a b c : A) → (a <> b) <> c ≡ a <> (b <> c)
open Monoid/Laws {{...}} public hiding (super)

mconcat : ∀ {a} {A : Set a} {{MonA : Monoid A}} → List A → A
mconcat = foldr _<>_ mempty

--- Instances ---

instance

  MonoidList : ∀ {a} {A : Set a} → Monoid (List A)
  Monoid.super MonoidList = it
  mempty {{MonoidList}} = []

  MonoidFun : ∀ {a b} {A : Set a} {B : A → Set b} {{_ : ∀ {x} → Monoid (B x)}} → Monoid (∀ x → B x)
  Monoid.super (MonoidFun {a} {b} {A} {B} {{SG}}) =
    SemigroupFun {a} {b} {A} {B} {{Monoid.super SG}}
  mempty {{MonoidFun}} _ = mempty

  MonoidMaybe : ∀ {a} {A : Set a} → Monoid (Maybe A)
  Monoid.super MonoidMaybe = it
  mempty {{MonoidMaybe}} = nothing

  -- Temporarily here, better version comes in the list update
  Monoid/LawsList : Monoid/Laws (List A)
  Monoid/Laws.super Monoid/LawsList = it
  left-identity {{Monoid/LawsList}} _ = refl
  right-identity {{Monoid/LawsList}} [] = refl
  right-identity {{Monoid/LawsList}} (x ∷ xs) =
    cong (x ∷_) (right-identity xs)
  monoid-assoc {{Monoid/LawsList}} [] ys zs = refl
  monoid-assoc {{Monoid/LawsList}} (x ∷ xs) ys zs =
    cong (x ∷_) (monoid-assoc xs ys zs)

record Sum {a} (A : Set a) : Set a where
  constructor mkSum
  field getSum : A
open Sum public

instance
  SemigroupSum : ∀ {a} {A : Set a} {{_ : Semiring A}} → Semigroup (Sum A)
  getSum (_<>_   {{SemigroupSum}} x y) = getSum x + getSum y

  MonoidSum : ∀ {a} {A : Set a} {{_ : Semiring A}} → Monoid (Sum A)
  Monoid.super MonoidSum = it
  getSum (mempty {{MonoidSum}}) = zro

record Product {a} (A : Set a) : Set a where
  constructor mkProduct
  field getProduct : A

open Product public

instance
  SemigroupProduct : ∀ {a} {A : Set a} {{_ : Semiring A}} → Semigroup (Product A)
  getProduct (_<>_   {{SemigroupProduct}} x y) = getProduct x * getProduct y

  MonoidProduct : ∀ {a} {A : Set a} {{_ : Semiring A}} → Monoid (Product A)
  Monoid.super MonoidProduct = it
  getProduct (mempty {{MonoidProduct}}) = one

record Const {a b} (A : Set a) (B : Set b) : Set a where
  constructor mkConst
  field getConst : A

open Const public

module _ {a b} {A : Set a} {{MonA : Monoid A}} where
  instance
    FunctorConst : Functor {a = b} (Const A)
    getConst (fmap {{FunctorConst}} f x) = getConst x

    ApplicativeConst : Applicative (Const A)
    getConst (pure  {{ApplicativeConst}} x)     = mempty
    getConst (_<*>_ {{ApplicativeConst}} wf wx) = getConst wf <> getConst wx

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 #-}

module T where

open import Level
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; subst; module ≡-Reasoning)
open import Data.Nat using (ℕ; _+_)
open import Data.Fin using (Fin)

data Exp : Set where
  ONE   : Exp
  PLUS  : Exp → Exp → Exp

val : Exp → ℕ
val ONE           = 1
val (PLUS e₁ e₂)  = val e₁ + val e₂

data eqExp : Exp → Exp → Set where
  idExp    : {e : Exp} → eqExp e e
  transExp : {e₁ e₂ e₃ : Exp} → (eqExp e₁ e₂) → (eqExp e₂ e₃) → (eqExp e₁ e₃)

val≡ : {e₁ e₂ : Exp} → (eqExp e₁ e₂) → (val e₁ ≡ val e₂)
val≡ idExp = refl
val≡ (transExp α₁ α₂) = trans (val≡ α₁) (val≡ α₂)

trans-assoc : {A : Set} {x y z w : A} → (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) →
  trans (trans p q) r ≡ trans p (trans q r)
trans-assoc refl refl refl = refl

subst-trans : (P : ℕ → Set) (p : (n : ℕ) → P n) {e₁ e₂ e₃ : Exp} →
              (α : eqExp e₁ e₂) (β : eqExp e₂ e₃) (v : P (val e₁)) →
              subst P (trans (val≡ α) (val≡ β)) v ≡
              subst P (val≡ β) (subst P (val≡ α) v)
subst-trans P p idExp β v = refl
subst-trans P p (transExp α₁ α₂) β v =
  begin (subst P (trans (trans (val≡ α₁) (val≡ α₂)) (val≡ β)) v
         ≡⟨ cong (λ x → subst P x v)
                 (trans-assoc (val≡ α₁) (val≡ α₂) (val≡ β))  ⟩
         subst P (trans (val≡ α₁) (trans (val≡ α₂) (val≡ β))) v
         ≡⟨ refl ⟩
         subst P (trans (val≡ α₁) (val≡ (transExp α₂ β))) v
         ≡⟨  subst-trans P p α₁ (transExp α₂ β) v ⟩
         subst P (val≡ (transExp α₂ β)) (subst P (val≡ α₁) v)
         ≡⟨ refl ⟩
         subst P (trans (val≡ α₂) (val≡ β)) (subst P (val≡ α₁) v)
         ≡⟨ subst-trans P p α₂ β (subst P (val≡ α₁) v) ⟩
         subst P (val≡ β) (subst P (val≡ α₂) (subst P (val≡ α₁) v))
         ≡⟨ cong (λ x → subst P (val≡ β) x) (sym (subst-trans P p α₁ α₂ v)) ⟩
         subst P (val≡ β) (subst P (trans (val≡ α₁) (val≡ α₂)) v)
         ≡⟨ refl ⟩
         subst P (val≡ β) (subst P (val≡ (transExp α₁ α₂)) v) ∎)
  where open ≡-Reasoning

pr : {P : ℕ → Set} {p : (n : ℕ) → P n} {e₁ e₂ : Exp} {α : eqExp e₁ e₂} →
    subst P (val≡ α) (p (val e₁)) ≡ p (val e₂)
pr {P} {p} {e} {.e} {idExp} = refl
pr {P} {p} {e₁} {e₃} {transExp {e₂ = e₂} α β} =
  begin (subst P (val≡ (transExp α β)) (p (val e₁))
           ≡⟨ refl ⟩
         subst P (trans (val≡ α) (val≡ β)) (p (val e₁))
           ≡⟨ subst-trans P p α β (p (val e₁)) ⟩
         subst P (val≡ β) (subst P (val≡ α) (p (val e₁)))
           ≡⟨ cong (λ x → subst P (val≡ β) x) (pr {P} {p} {e₁} {e₂} {α}) ⟩
         subst P (val≡ β) (p (val e₂))
           ≡⟨ pr {P} {p} {e₂} {e₃} {β} ⟩
         p (val e₃) ∎)
  where open ≡-Reasoning

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-

This file contains:
- Some basic properties of Rijke finite types.

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

module Cubical.Data.FinType.Properties where

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

open import Cubical.HITs.SetTruncation

open import Cubical.Data.Nat
open import Cubical.Data.FinSet
open import Cubical.Data.FinSet.Constructors
open import Cubical.Data.FinType.Base

private
  variable
    ℓ ℓ' : Level
    n : ℕ
    X : Type ℓ
    Y : Type ℓ'

EquivPresIsFinType : (n : ℕ) → X ≃ Y → isFinType n X → isFinType n Y
EquivPresIsFinType 0 e = EquivPresIsFinSet (isoToEquiv (setTruncIso (equivToIso e)))
EquivPresIsFinType (suc n) e (p , q) .fst = EquivPresIsFinType 0 e p
EquivPresIsFinType (suc n) e (p , q) .snd a b =
  EquivPresIsFinType n (invEquiv (congEquiv (invEquiv e))) (q _ _)

isFinSet→isFinType : (n : ℕ) → isFinSet X → isFinType n X
isFinSet→isFinType 0 p = EquivPresIsFinSet (invEquiv (setTruncIdempotent≃ (isFinSet→isSet p))) p
isFinSet→isFinType (suc n) p .fst = isFinSet→isFinType 0 p
isFinSet→isFinType (suc n) p .snd a b = isFinSet→isFinType n (isFinSet≡ (_ , p) _ _)

isPathConnected→isFinType0 : isContr ∥ X ∥₂ → isFinType 0 X
isPathConnected→isFinType0 p = isContr→isFinSet p


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monoidal.Braided where

open import Level
open import Level using (_⊔_)

open import Categories.Category

open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation using (_∘₁_) renaming (_≡_ to _≡ⁿ_)

open import Categories.Monoidal.Helpers
open import Categories.Monoidal.Braided.Helpers

open import Categories.Monoidal

record Braided {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where
  private module C = Category C
  private module M = Monoidal M
  open C hiding (id; identityˡ; identityʳ; assoc)
  open M

  open MonoidalHelperFunctors C ⊗ id
  open BraidedHelperFunctors C ⊗ id

  field
    braid : NaturalIsomorphism x⊗y y⊗x

  open Braiding identityˡ identityʳ assoc braid

  field
    -- NB: Triangle is redundant, proof coming soon...
    .hexagon₁ : (Hexagon1SideB ∘₁ (Hexagon1TopB ∘₁ Hexagon1TopA)) ≡ⁿ (Hexagon1BottomB ∘₁ (Hexagon1BottomA ∘₁ Hexagon1SideA))
    .hexagon₂ : (Hexagon2SideB ∘₁ (Hexagon2TopB ∘₁ Hexagon2TopA)) ≡ⁿ (Hexagon2BottomB ∘₁ (Hexagon2BottomA ∘₁ Hexagon2SideA))

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module DaraisPhoas where

open import Agda.Primitive using (_⊔_)

module Prelude where

  infixr 3 ∃𝑠𝑡
  infixl 5 _∨_
  infixr 20 _∷_

  data 𝔹 : Set where
    T : 𝔹
    F : 𝔹

  data _∨_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    Inl : A → A ∨ B
    Inr : B → A ∨ B

  syntax ∃𝑠𝑡 A (λ x → B) = ∃ x ⦂ A 𝑠𝑡 B
  data ∃𝑠𝑡 {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
    ⟨∃_,_⟩ : ∀ (x : A) → B x → ∃ x ⦂ A 𝑠𝑡 B x

  data ⟬_⟭ {ℓ} (A : Set ℓ) : Set ℓ where
    [] : ⟬ A ⟭
    _∷_ : A → ⟬ A ⟭ → ⟬ A ⟭

open Prelude

infixr 15 _⟨→⟩_
data type : Set where
  ⟨ℕ⟩   : type
  _⟨→⟩_ : type → type → type

infixl 15 _⟨∙⟩_
data exp-phoas (var : type → ⟬ type ⟭ → Set) : ∀ (Γ : ⟬ type ⟭) (τ : type) → Set where
  Var : ∀ {Γ τ}
    (x : var τ Γ)
    → exp-phoas var Γ τ
  ⟨λ⟩ : ∀ {Γ τ₁ τ₂}
    (e : var τ₁ (τ₁ ∷ Γ) → exp-phoas var (τ₁ ∷ Γ) τ₂)
    → exp-phoas var Γ (τ₁ ⟨→⟩ τ₂)
  _⟨∙⟩_ : ∀ {Γ τ₁ τ₂}
    (e₁ : exp-phoas var Γ (τ₁ ⟨→⟩ τ₂))
    (e₂ : exp-phoas var Γ τ₁)
    → exp-phoas var Γ τ₂

infix 10 _∈_
data _∈_ {ℓ} {A : Set ℓ} (x : A) : ∀ (xs : ⟬ A ⟭) → Set ℓ where
  Z : ∀ {xs} → x ∈ x ∷ xs
  S : ∀ {x′ xs} → x ∈ xs → x ∈ x′ ∷ xs

infix 10 _⊢_
data _⊢_ : ∀ (Γ : ⟬ type ⟭) (τ : type) → Set where
  Var : ∀ {Γ τ}
    (x : τ ∈ Γ)
    → Γ ⊢ τ
  ⟨λ⟩ : ∀ {Γ τ₁ τ₂}
    (e : τ₁ ∷ Γ ⊢ τ₂)
    → Γ ⊢ τ₁ ⟨→⟩ τ₂
  _⟨∙⟩_ : ∀ {Γ τ₁ τ₂}
    (e₁ : Γ ⊢ τ₁ ⟨→⟩ τ₂)
    (e₂ : Γ ⊢ τ₁)
    → Γ ⊢ τ₂

⟦_⟧₁ : ∀ {Γ τ} (e : exp-phoas _∈_ Γ τ) → Γ ⊢ τ
⟦ Var x ⟧₁ = Var x
⟦ ⟨λ⟩ e ⟧₁ = ⟨λ⟩ ⟦ e Z ⟧₁
⟦ e₁ ⟨∙⟩ e₂ ⟧₁ = ⟦ e₁ ⟧₁ ⟨∙⟩ ⟦ e₂ ⟧₁

⟦_⟧₂ : ∀ {Γ τ} (e : Γ ⊢ τ) → exp-phoas _∈_ Γ τ
⟦ Var x ⟧₂ = Var x
⟦ ⟨λ⟩ e ⟧₂ = ⟨λ⟩ (λ _ → ⟦ e ⟧₂)
⟦ e₁ ⟨∙⟩ e₂ ⟧₂ = ⟦ e₁ ⟧₂ ⟨∙⟩ ⟦ e₂ ⟧₂

Ch : type
Ch =  (⟨ℕ⟩ ⟨→⟩ ⟨ℕ⟩) ⟨→⟩ ⟨ℕ⟩ ⟨→⟩ ⟨ℕ⟩

twoDB : [] ⊢ Ch
twoDB = ⟨λ⟩ (⟨λ⟩ (Var (S Z) ⟨∙⟩ (Var (S Z) ⟨∙⟩ Var Z)))

twoPH : exp-phoas _∈_ [] Ch
twoPH = ⟨λ⟩ (λ f → ⟨λ⟩ (λ x → Var f ⟨∙⟩ (Var f ⟨∙⟩ Var x)))

{-
/Users/wadler/sf/src/extra/DaraisPhoas.agda:82,9-60
⟨ℕ⟩ ⟨→⟩ ⟨ℕ⟩ != ⟨ℕ⟩ of type type
when checking that the expression
⟨λ⟩ (λ f → ⟨λ⟩ (λ x → Var f ⟨∙⟩ (Var f ⟨∙⟩ Var x))) has type
exp-phoas _∈_ [] Ch
-}


text:
module All where

open import Prelude
open import T
open import SubstTheory
open import DynTheory
open import Progress
open import HT
open import Examples
open import Eq
open import DenotCommutes

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
{-
Problem #53
Given premises:
    (all x)[(F x) -> (some y)((F y) & (G x y))]    justification = 1.0

Ultimate epistemic interests:
    (all x)[(F x) -> (some y)(some z)((G x y) & (G y z))]    interest = 1.0
-}

open import Prelude

postulate
  U : Set
  F : U → Set
  G : U → U → Set

record Premise {x : U} (Fx : F x) : Set where
  field
    pY : U
    pF : F pY
    pG : G x pY

open Premise

record Conclusion {x : U} (Fx : F x) : Set where
  field
    cY : U
    cZ : U
    cGxy : G x cY
    cGyz : G cY cZ

open Conclusion

premise = ∀ x → (Fx : F x) → Premise Fx
conclusion = ∀ x → (Fx : F x) → Conclusion Fx

proof1 : premise → conclusion
proof1 p x Fx =
  record
  { cY = _
  ; cZ = _
  ; cGxy = pG p1
  ; cGyz = pG p2 }
  where
  p1 = p x Fx
  p2 = p (pY p1) (pF p1)

{-
postulate
  U : Set
  F : U → Set
  G : U → U → Set

∃ : ∀ {a b} {A : Set a} (B : A → Set b) → Set (a ⊔ b)
∃ = Σ _

premise = ∀ x → F x → ∃ λ y → (F y × G x y)
conclusion = ∀ x → F x → ∃ λ y → ∃ λ z → (G x y × G y z)

pY : premise → ∀ x → F x → _
pY p x Fx = fst (p x Fx)

pF : premise → ∀ x → F x → F y -- y is not in scope!
pF p x Fx = {!fst (snd (p x Fx))!}

pG : premise → ∀ x → F x → _
pG p x Fx = {!snd (snd (p x Fx))!}

proof1 : premise → conclusion
proof1 p x Fx = y , z , Gxy , Gyz
  where
    y : U
    y = {!!}

    z : U
    z = {!!}

    Gxy : G x y
    Gxy = {!!}

    Gyz : G y z
    Gyz = {!!}
-}


text:
module Issue384 where

postulate
  D : (A : Set) → A → Set

data I : Set where
  i : I

D′ : (A : Set) → A → I → Set
D′ A x i = D A x

postulate
  Q : (A : Set) → A → Set
  q : ∀ j A (x : A) → D′ A x j → Q A x

  A : Set
  x : A
  d : D A x

  P : (A : Set) → A → Set
  p : P (Q _ _) (q _ _ _ d)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue168 where

postulate X : Set

open import Issue168b
open Membership X

postulate
  P : Nat → Set
  lemma : ∀ n → P (id n)

foo : P zero
foo = lemma _

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- List Literals
------------------------------------------------------------------------

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

module Data.List.Literals where

open import Agda.Builtin.FromString
open import Data.Unit
open import Agda.Builtin.Char
open import Agda.Builtin.List
open import Data.String.Base using (toList)

isString : IsString (List Char)
isString = record
  { Constraint = λ _ → ⊤
  ; fromString = λ s → toList s
  }


text:
------------------------------------------------------------------------------
-- The relation of divisibility on partial natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.Divisibility.By0 where

open import FOTC.Base
open import FOTC.Data.Nat

infix 4 _∣_

------------------------------------------------------------------------------
-- The relation of divisibility (the symbol is '\mid' not '|')
--
-- It seems there is not agreement about if 0∣0:
--
-- Hardy and Wright 1975, p. 1: 0∤0
--
-- Knuth 1977, p. 40: 0∤0
--
-- Agda standard library 0.8.1: 0|0
--
-- Coq 8.4pl4: 0∣0
--
-- Isabelle2014: 0∣0

-- In our definition 0∣0, which is used to prove properties of the gcd
-- as it is in GHC ≥ 7.2.1, where gcd 0 0 = 0 (see
-- http://hackage.haskell.org/trac/ghc/ticket/3304).

-- Note that @k@ should be a total natural number.
_∣_ : D → D → Set
m ∣ n = ∃[ k ] N k ∧ n ≡ k * m
{-# ATP definition _∣_ #-}

------------------------------------------------------------------------------
-- References:
--
-- Hardy, G. H. and Wright, E. M. (1975). An Introduction to the
-- Theory of Numbers. 4th ed. Oxford University Press.
--
-- Knuth, Donald E. (1997). The Art of Computer Programming. 3rd
-- ed. Vol. 1. Fundamental Algorithms. Addison-Wesley Professional.


text:
------------------------------------------------------------------------
-- Compiler correctness
------------------------------------------------------------------------

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

module Lambda.Partiality-monad.Inductive.Compiler-correctness where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
open import Maybe equality-with-J as Maybe
open import Monad equality-with-J
open import Vec.Function equality-with-J

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Monad

open import Lambda.Compiler
open import Lambda.Partiality-monad.Inductive.Interpreter
open import Lambda.Partiality-monad.Inductive.Virtual-machine
open import Lambda.Syntax
open import Lambda.Virtual-machine

private
  module C = Closure Code
  module T = Closure Tm

-- Compiler correctness.

mutual

  ⟦⟧-correct :
    ∀ {n} t {ρ : T.Env n} {c s} {k : ℕ → T.Value → M C.Value} {n} →
    (∀ v → steps ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≳[ n ]
           λ n → run (k n v)) →
    steps ⟨ comp t c , s , comp-env ρ ⟩ ≳[ n ]
    λ n → run (⟦ t ⟧′ ρ n >>= k n)
  ⟦⟧-correct (con i) {ρ} {c} {s} {k} hyp =
    steps ⟨ con i ∷ c , s , comp-env ρ ⟩                     ≳⟨ step⇓ ⟩
    steps ⟨ c , val (comp-val (T.con i)) ∷ s , comp-env ρ ⟩  ≳⟨ hyp (T.con i) ⟩
    (λ n → run (k n (T.con i)))                              ≡⟨ sym now->>= ⟩≳
    (λ n → run (⟦ con i ⟧′ ρ n >>= k n))                     ∎≳

  ⟦⟧-correct (var x) {ρ} {c} {s} {k} hyp =
    steps ⟨ var x ∷ c , s , comp-env ρ ⟩                 ≳⟨ step⇓ ⟩
    steps ⟨ c , val (comp-val (ρ x)) ∷ s , comp-env ρ ⟩  ≳⟨ hyp (ρ x) ⟩
    (λ n → run (k n (ρ x)))                              ≡⟨ sym now->>= ⟩≳
    (λ n → run (⟦ var x ⟧′ ρ n >>= k n))                 ∎≳

  ⟦⟧-correct (ƛ t) {ρ} {c} {s} {k} hyp =
    steps ⟨ clo (comp t (ret ∷ [])) ∷ c , s , comp-env ρ ⟩   ≳⟨ step⇓ ⟩
    steps ⟨ c , val (comp-val (T.ƛ t ρ)) ∷ s , comp-env ρ ⟩  ≳⟨ hyp (T.ƛ t ρ) ⟩
    (λ n → run (k n (T.ƛ t ρ)))                              ≡⟨ sym now->>= ⟩≳
    (λ n → run (⟦ ƛ t ⟧′ ρ n >>= k n))                       ∎≳

  ⟦⟧-correct (t₁ · t₂) {ρ} {c} {s} {k} {n} hyp =
    steps ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩     ≳⟨ (⟦⟧-correct t₁ {n = n} λ v₁ → ⟦⟧-correct t₂ λ v₂ → ∙-correct v₁ v₂ hyp) ⟩

    (λ n → run (⟦ t₁ ⟧′ ρ n >>= λ v₁ →
                ⟦ t₂ ⟧′ ρ n >>= λ v₂ →
                (v₁ ∙ v₂) n >>= k n))                          ≡⟨ cong (λ f → run (⟦ t₁ ⟧′ ρ n >>= f))
                                                                       (⟨ext⟩ λ v₁ → Monad.associativity tr (⟦ t₂ ⟧′ ρ n) _ _) ⟩≳
    (λ n → run (⟦ t₁ ⟧′ ρ n >>= λ v₁ →
               (⟦ t₂ ⟧′ ρ n >>= λ v₂ → (v₁ ∙ v₂) n) >>= k n))  ≡⟨ cong MaybeT.run $ Monad.associativity tr (⟦ t₁ ⟧′ ρ n) _ _ ⟩≳

    (λ n → run (⟦ t₁ · t₂ ⟧′ ρ n >>= k n))                     ∎≳
    where
    tr = Monad-transformer.transform (Maybe.monad-transformer ext)

  ∙-correct :
    ∀ {n} v₁ v₂ {ρ : T.Env n} {c s} {k : ℕ → T.Value → M C.Value} {n} →
    (∀ v → steps ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≳[ n ]
           λ n → run (k n v)) →
    steps ⟨ app ∷ c
          , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s
          , comp-env ρ
          ⟩ ≳[ n ]
    λ n → run ((v₁ ∙ v₂) n >>= k n)
  ∙-correct (T.con i) v₂ {ρ} {c} {s} {k} hyp =
    steps ⟨ app ∷ c
          , val (comp-val v₂) ∷ val (C.con i) ∷ s
          , comp-env ρ
          ⟩                                        ≳⟨⟩

    const (run fail)                               ≡⟨ sym now->>= ⟩≳

    (λ n → run ((T.con i ∙ v₂) n >>= k n))         ∎≳

  ∙-correct (T.ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} {zero} hyp =
    steps ⟨ app ∷ c
          , val (comp-val v₂) ∷ val (comp-val (T.ƛ t₁ ρ₁)) ∷ s
          , comp-env ρ
          ⟩                                   ≡⟨ refl ⟩≳

    const never                               ≡⟨ sym never->>= ⟩≳

    const (never >>= _)                       ≡⟨ cong (_>>= maybe (MaybeT.run ∘ k 0) (return nothing) ⦂ (_ ⊥ → _)) (sym never->>=) ⟩≳

    (λ n → run ((T.ƛ t₁ ρ₁ ∙ v₂) n >>= k n))  ∎≳

  ∙-correct (T.ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} {suc n} hyp = later (
    steps ⟨ app ∷ c
          , val (comp-val v₂) ∷
            val (comp-val (T.ƛ t₁ ρ₁)) ∷ s
          , comp-env ρ
          ⟩ ∘ suc                                         ≳⟨⟩

    steps ⟨ comp t₁ (ret ∷ [])
          , ret c (comp-env ρ) ∷ s
          , cons (comp-val v₂) (comp-env ρ₁)
          ⟩                                               ∀≡⟨ (λ n → cong (λ ρ′ → steps ⟨ comp t₁ (ret ∷ []) , ret c (comp-env ρ) ∷ s , ρ′ ⟩ n) $
                                                                          sym comp-cons) ⟩≳
    steps ⟨ comp t₁ (ret ∷ [])
          , ret c (comp-env ρ) ∷ s
          , comp-env (cons v₂ ρ₁)
          ⟩                                               ≳⟨ (⟦⟧-correct t₁ {n = n} λ v →

        steps ⟨ ret ∷ []
              , val (comp-val v) ∷ ret c (comp-env ρ) ∷ s
              , comp-env (cons v₂ ρ₁)
              ⟩                                                ≳⟨ step⇓ ⟩

        steps ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩        ≳⟨ hyp v ⟩

        (λ n → run (k n v))                                    ≳⟨ step⇓ ⟩

        (λ n → run (k (suc n) v))                              ∎≳) ⟩

    (λ n → run (⟦ t₁ ⟧′ (cons v₂ ρ₁) n >>= k (suc n)))    ≳⟨⟩

    (λ n → run ((T.ƛ t₁ ρ₁ ∙ v₂) (suc n) >>= k (suc n)))  ∎≳)

-- Note that the equality that is used here is syntactic.

correct :
  ∀ t →
  wrap (exec ⟨ comp t [] , [] , nil ⟩) ≡
  (⟦ t ⟧ nil >>= λ v → return (comp-val v))
correct t =
  wrap (exec ⟨ comp t [] , [] , nil ⟩)                     ≡⟨ cong (λ ρ → wrap (exec ⟨ comp t [] , [] , ρ ⟩)) $ sym comp-nil ⟩

  wrap (exec ⟨ comp t [] , [] , comp-env nil ⟩)            ≡⟨⟩

  wrap (⨆ (stepsˢ ⟨ comp t [] , [] , comp-env nil ⟩))      ≡⟨ cong wrap (≳→⨆≡⨆ 0 $ ⟦⟧-correct t λ v →
                                                                                const (MaybeT.run (return (comp-val v))) ∎≳) ⟩
  wrap (⨆ (⟦ t ⟧ˢ nil >>=ˢ λ v →
           constˢ (MaybeT.run (return (comp-val v)))))     ≡⟨ cong (λ s → wrap (⨆ s))
                                                                   (_↔_.to equality-characterisation-increasing (λ _ → refl)) ⟩
  wrap (⨆ (maybe (λ v → MaybeT.run (return (comp-val v)))
                 (return nothing)
             ∗-inc
           ⟦ t ⟧ˢ nil))                                    ≡⟨ cong wrap (sym ⨆->>=) ⟩∎

  (⟦ t ⟧ nil >>= λ v → return (comp-val v))                ∎

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module BHeap.Properties {A : Set}(_≤_ : A → A → Set)  where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import BHeap _≤_
open import Data.List
open import Data.Nat
open import Data.Sum
open import Nat.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import List.Properties A
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality

lemma-merge-lf : {b : Bound}(tot≤ : Total _≤_)(h : BHeap b) → merge tot≤ h lf ≡ h
lemma-merge-lf _ lf = refl
lemma-merge-lf _ (nd b≤x l r) = refl

lemma-merge# : {b : Bound}(tot≤ : Total _≤_)(l r : BHeap b) → # (merge tot≤ l r) ≡ # l + # r
lemma-merge# _ lf r = refl
lemma-merge# tot≤ l lf rewrite lemma-merge-lf tot≤ l | +id (# l) = refl
lemma-merge# tot≤ (nd {x = y} x≤y l r) (nd {x = y'} x≤y' l' r')
    with tot≤ y y'
... | inj₁ y≤y' rewrite lemma-merge# tot≤ l r = refl
... | inj₂ y'≤y rewrite lemma-merge# tot≤ l' r' | +assoc (# l + # r) (# l' + # r') = refl

lemma-merge≤′ : {b : Bound}{x : A}(tot≤ : Total _≤_)(b≤x : LeB b (val x))(l r : BHeap (val x)) → suc (# (merge tot≤ l r)) ≤′ # (nd b≤x l r)
lemma-merge≤′ tot≤ b≤x l r rewrite lemma-merge# tot≤ l r = ≤′-refl

lemma-merge∼ : {b : Bound}(tot≤ : Total _≤_)(l r : BHeap b) → flatten (merge tot≤ l r) ∼ (flatten l ++ flatten r)
lemma-merge∼ _ lf r = refl∼
lemma-merge∼ tot≤ l lf rewrite lemma-merge-lf tot≤ l | ++id (flatten l) = refl∼
lemma-merge∼ tot≤ (nd {x = y} b≤x l r) (nd {x = y'} b≤y' l' r')
    with tot≤ y y'
... | inj₁ y≤y' = lemma++∼r (∼x /head /head (lemma-merge∼ tot≤ l r))
... | inj₂ y'≤y = trans∼ (lemma++∼l {xs = y' ∷ (y ∷ flatten l ++ flatten r)} (lemma-merge∼ tot≤ l' r')) (∼x /head (lemma++/ {xs = y ∷ flatten l ++ flatten r}) refl∼)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Andreas, 2012-10-30 Sections
-- Reported by guillaume.brunerie, Oct 24 2012
module Issue735 where

import Common.Level
open import Common.Prelude using (Nat; zero; suc)

{- I often want to use something like sections in Coq. I usually use
parametrized modules but this has at least two issues that Coq does
not have:

1) I need to give a name to the module, and there is often no
   meaningful name to be given

2) It exports the module, so I cannot define a module in another file
   with the same name

I guess I can workaround 2) by declaring the module private, but this
will mean that everything will be indented further (again) and I
really want to avoid that.

I think this can easily be fixed by adding a kind of anonymous
modules.  An anonymous module would be declared by naming it `_`, and
the following code

  module _ params where
    declarations

would be translated to:

  private
    module Fresh params where
      declarations

  open Fresh public

where Fresh is a new name. -}

-- Andreas: this translation is not necessary, because Agda
-- has a concept of sections internally (in Abstract syntax).

-- However, the translation and the actual implementation should
-- have the same semantics, except that a name 'Fresh' is never generated.

-- An empty section with no parameters

module _ where

-- A section with a non-hidden parameter

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

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

-- A section with all hidden parameters

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

  _++_ : List A → List A → List A
  []       ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

  module _ (default : A) where

    head : List A → A
    head  []     = default
    head (x ∷ _) = x

test : List Nat
test = head 1 [] ∷ ((2 ∷ []) ++ (3 ∷ []))


text:
module ImpossiblePattern where

f : ?
f (_ _) = ?

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Issue2959.M Set

r : R
r = ?

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Example of a nested recursive function using the Agda standard
-- library
------------------------------------------------------------------------------

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

-- From: Ana Bove and Venanzio Capretta. Nested general recursion and
-- partiality in type theory. vol 2152 LNCS. 2001.

module FOT.FOTC.Program.Nest.NestSL where

open import Data.Nat renaming (suc to succ)
open import Relation.Binary.PropositionalEquality

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

{-# TERMINATING #-}
nest : ℕ → ℕ
nest 0        = 0
nest (succ n) = nest (nest n)

{-# TERMINATING #-}
nest-x≡0 : ∀ n → nest n ≡ zero
nest-x≡0 zero     = refl
nest-x≡0 (succ n) = nest-x≡0 (nest n)