text:
{- Conatural number properties (Tesla Ice Zhang et al., Feb. 2019)

This file defines operations and properties on conatural numbers:

- Infinity (∞).

- Proof that ∞ + 1 is equivalent to ∞.

- Proof that conatural is an hSet.

- Bisimulation on conatural

- Proof that bisimulation is equivalent to equivalence (Coinductive Proof
  Principle).

- Proof that this bisimulation is prop valued

The standard library also defines bisimulation on conaturals:

https://github.com/agda/agda-stdlib/blob/master/src/Codata/Conat/Bisimilarity.agda
-}

{-# OPTIONS --cubical --safe --guardedness #-}
module Cubical.Codata.Conat.Properties where

open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Empty

open import Cubical.Core.Everything

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

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq
open import Cubical.Codata.Conat.Base

Unwrap-prev : Conat′ → Type₀
Unwrap-prev  zero   = Unit
Unwrap-prev (suc _) = Conat

unwrap-prev : (n : Conat′) -> Unwrap-prev n
unwrap-prev  zero   = _
unwrap-prev (suc x) = x

private -- tests
  𝟘 = conat zero
  𝟙  = succ 𝟘
  𝟚  = succ 𝟙

  succ𝟙≡𝟚 : succ 𝟙 ≡ 𝟚
  succ𝟙≡𝟚 i = 𝟚

  pred𝟚≡𝟙 : unwrap-prev (force 𝟚) ≡ 𝟙
  pred𝟚≡𝟙 i = 𝟙

∞ : Conat
force ∞ = suc ∞

∞+1≡∞ : succ ∞ ≡ ∞
force (∞+1≡∞ _) = suc ∞

∞+2≡∞ : succ (succ ∞) ≡ ∞
∞+2≡∞ = (cong succ ∞+1≡∞) ∙ ∞+1≡∞

_+_ : Conat → Conat → Conat
_+′_ : Conat′ → Conat → Conat′

force (x + y) = force x +′ y
zero +′ y = force y
suc x +′ y = suc (x + y)

n+∞≡∞ : ∀ n → n + ∞ ≡ ∞
n+′∞≡∞′ : ∀ n → n +′ ∞ ≡ suc ∞

force (n+∞≡∞ n i) = n+′∞≡∞′ (force n) i
n+′∞≡∞′ zero = refl
n+′∞≡∞′ (suc n) = λ i → suc (n+∞≡∞ n i)

∞+∞≡∞ : ∞ + ∞ ≡ ∞
force (∞+∞≡∞ i) = suc (∞+∞≡∞ i)

conat-absurd : ∀ {y : Conat} {ℓ} {Whatever : Type ℓ} → zero ≡ suc y → Whatever
conat-absurd eq = ⊥-elim (transport (cong diag eq) tt)
  where
  diag : Conat′ → Type₀
  diag zero = Unit
  diag (suc _) = ⊥

module IsSet where
  ≡-stable  : {x y : Conat} → Stable (x ≡ y)
  ≡′-stable : {x y : Conat′} → Stable (x ≡ y)

  force (≡-stable ¬¬p i) = ≡′-stable (λ ¬p → ¬¬p (λ p → ¬p (cong force p))) i
  ≡′-stable {zero}  {zero}  ¬¬p′ = refl
  ≡′-stable {suc x} {suc y} ¬¬p′ =
     cong′ suc (≡-stable λ ¬p → ¬¬p′ λ p → ¬p (cong pred′′ p))
  ≡′-stable {zero}  {suc y} ¬¬p′ = ⊥-elim (¬¬p′ conat-absurd)
  ≡′-stable {suc x} {zero}  ¬¬p′ = ⊥-elim (¬¬p′ λ p → conat-absurd (sym p))

  isSetConat : isSet Conat
  isSetConat _ _ = Stable≡→isSet (λ _ _ → ≡-stable) _ _

  isSetConat′ : isSet Conat′
  isSetConat′ m n p′ q′ = cong (cong force) (isSetConat (conat m) (conat n) p q)
    where p = λ where i .force → p′ i
          q = λ where i .force → q′ i

module Bisimulation where
  open IsSet using (isSetConat)

  record _≈_ (x y : Conat) : Type₀
  data _≈′_ (x y : Conat′) : Type₀
  _≈′′_ : Conat′ → Conat′ → Type₀
  zero  ≈′′ zero  = Unit
  suc x ≈′′ suc y = x ≈ y
  -- So impossible proofs are preserved
  x ≈′′ y = ⊥

  record _≈_ x y where
    coinductive
    field prove : force x ≈′ force y

  data _≈′_  x y where
    con : x ≈′′ y → x ≈′ y

  open _≈_ public

  bisim : ∀ {x y} → x ≈ y → x ≡ y
  bisim′ : ∀ {x y} → x ≈′ y → x ≡ y

  bisim′ {zero} {zero} (con tt) = refl
  bisim′ {zero} {suc x} (con ())
  bisim′ {suc x} {zero} (con ())
  bisim′ {suc x} {suc y} (con eq) i = suc (bisim eq i)
  force (bisim eq i) = bisim′ (prove eq) i

  misib : ∀ {x y} → x ≡ y → x ≈ y
  misib′ : ∀ {x y} → x ≡ y → x ≈′ y

  misib′ {zero} {zero} _ = con tt
  misib′ {zero} {suc x} = conat-absurd
  misib′ {suc x} {zero} p = conat-absurd (sym p)
  -- misib′ {suc x} {suc y} p = con λ where .prove → misib′ (cong pred′ p)
  misib′ {suc x} {suc y} p = con (misib (cong pred′′ p))
  prove (misib x≡y) = misib′ (cong force x≡y)

  iso″ : ∀ {x y} → (p : x ≈ y) → misib (bisim p) ≡ p
  iso′ : ∀ {x y} → (p : x ≈′ y) → misib′ (bisim′ p) ≡ p

  iso′ {zero} {zero} (con p) = refl
  iso′ {zero} {suc x} (con ())
  iso′ {suc x} {zero} (con ())
  iso′ {suc x} {suc y} (con p) = cong con (iso″ p)
  prove (iso″ p i) = iso′ (prove p) i

  osi : ∀ {x y} → (p : x ≡ y) → bisim (misib p) ≡ p
  osi p = isSetConat _ _ _ p

  path≃bisim : ∀ {x y} → (x ≡ y) ≃ (x ≈ y)
  path≃bisim = isoToEquiv (iso misib bisim iso″ osi)

  path≡bisim : ∀ {x y} → (x ≡ y) ≡ (x ≈ y)
  path≡bisim = ua path≃bisim

  isProp≈ : ∀ {x y} → isProp (x ≈ y)
  isProp≈ = subst isProp path≡bisim (isSetConat _ _)

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Generic.Test.DeriveEq where

open import Generic.Main

open import Data.Vec using (Vec) renaming ([] to []ᵥ; _∷_ to _∷ᵥ_)

module DeriveEqStar where
  open import Relation.Binary
  open import Relation.Binary.Construct.Closure.ReflexiveTransitive

  instance StarEq : ∀ {i t} {I : Set i} {T : Rel I t} {i j}
                      {{iEq : Eq I}} {{tEq : ∀ {i j} -> Eq (T i j)}} -> Eq (Star T i j)
  unquoteDef StarEq = deriveEqTo StarEq (quote Star)

module DeriveEqVec where
  instance VecEq : ∀ {n α} {A : Set α} {{aEq : Eq A}} -> Eq (Vec A n)
  unquoteDef VecEq = deriveEqTo VecEq (quote Vec)

  xs : Vec ℕ 3
  xs = 2 ∷ᵥ 4 ∷ᵥ 1 ∷ᵥ []ᵥ

  test₁ : xs ≟ xs ≡ yes refl
  test₁ = refl

  test₂ : xs ≟ (2 ∷ᵥ 4 ∷ᵥ 2 ∷ᵥ []ᵥ) ≡ no _
  test₂ = refl

module DeriveEqD where
  data D {α β} (A : Set α) (B : A -> Set β) : ∀ {n x} -> Vec (B x) n -> ℕ -> Set (α ⊔ β) where
    c₁ : ∀ {x n} (ys : Vec (B x) n) m -> .A -> D A B ys m
    c₂ : ∀ {x n m y} {ys zs : Vec (B x) n}
       -> D A B (y ∷ᵥ ys) 0 -> Vec A m -> D A B ys (suc n) -> D A B zs n

  -- `VecEq` is in scope.
  instance DEq : ∀ {α β} {A : Set α} {B : A -> Set β} {n m x} {ys : Vec (B x) n}
                   {{aEq : Eq A}} {{bEq : ∀ {x} -> Eq (B x)}} -> Eq (D A B ys m)
  unquoteDef DEq = deriveEqTo DEq (quote D)

-- -- Seems like the problem is that irrelevance and metavariables resolution do not play well.
-- module DeriveEqE where
--   data E {α} (A : Set α) : ∀ {n} -> .(Vec A n) -> Set α where
--     c₁ : ∀ {n} -> .(xs : Vec A n) -> E A xs

--   instance EEq : ∀ {α n} {A : Set α} .{xs : Vec A n} -> Eq (E A xs)
--   unquoteDef EEq = deriveEqTo EEq (quote E)
--   -- Variable xs is declared irrelevant, so it cannot be used here
--   -- when checking that the expression xs has type _B_76 A _ n₁ _ n₁

module DeriveEqF where
  data F {α} (A : Set α) : Set α where
    c₁ : ∀ {n} -> .(Vec A n) -> F A

  instance FEq : ∀ {α} {A : Set α} -> Eq (F A)
  unquoteDef FEq = deriveEqTo FEq (quote F)

ext: agda

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" in multiple Setoids.
------------------------------------------------------------------------

-- Example use:
--
--   open import Data.Maybe.Properties
--   open import Data.Maybe.Relation.Binary.Equality
--   open import Relation.Binary.Reasoning.MultiSetoid
--
--   begin⟨ S ⟩
--     x ≈⟨ drop-just (begin⟨ setoid S ⟩
--          just x ≈⟨ justx≈mz ⟩
--          mz     ≈⟨ mz≈justy ⟩
--          just y ∎)⟩
--     y ≈⟨ y≈z ⟩
--     z ∎

-- Note this module is not reimplemented in terms of `Reasoning.Setoid`
-- as this introduces unsolved metas as the underlying base module
-- `Base.Single` does not require `_≈_` be symmetric.

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

module Relation.Binary.Reasoning.MultiSetoid where

open import Function.Base using (flip)
open import Level using (_⊔_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

import Relation.Binary.Reasoning.Setoid as EqR

------------------------------------------------------------------------
-- Combinators that take the current setoid as an explicit argument.

module _ {c ℓ} (S : Setoid c ℓ) where
  open Setoid S

  data IsRelatedTo (x y : _) : Set (c ⊔ ℓ) where
    relTo : (x∼y : x ≈ y) → IsRelatedTo x y

  infix 1 begin⟨_⟩_

  begin⟨_⟩_ : ∀ {x y} → IsRelatedTo x y → x ≈ y
  begin⟨_⟩_ (relTo eq) = eq

------------------------------------------------------------------------
-- Combinators that take the current setoid as an implicit argument.

module _ {c ℓ} {S : Setoid c ℓ} where

  open Setoid S renaming (_≈_ to _≈_)

  infixr 2 step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_
  infix 3 _∎

  step-≈ : ∀ x {y z} → IsRelatedTo S y z → x ≈ y → IsRelatedTo S x z
  step-≈ x (relTo y∼z) x∼y = relTo (trans x∼y y∼z)

  step-≈˘ : ∀ x {y z} → IsRelatedTo S y z → y ≈ x → IsRelatedTo S x z
  step-≈˘ x y∼z x≈y = step-≈ x y∼z (sym x≈y)

  step-≡ : ∀ x {y z} → IsRelatedTo S y z → x ≡ y → IsRelatedTo S x z
  step-≡ _ x∼z P.refl = x∼z

  step-≡˘ : ∀ x {y z} → IsRelatedTo S y z → y ≡ x → IsRelatedTo S x z
  step-≡˘ _ x∼z P.refl = x∼z

  _≡⟨⟩_ : ∀ x {y} → IsRelatedTo S x y → IsRelatedTo S x y
  _ ≡⟨⟩ x∼y = x∼y

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

  syntax step-≈  x y∼z x≈y = x ≈⟨  x≈y ⟩ y∼z
  syntax step-≈˘ x y∼z y≈x = x ≈˘⟨ y≈x ⟩ y∼z
  syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
  syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z


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

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Function
open import Data.Unit
open import Data.List as List
open import Data.Char
open import Data.Nat as ℕ
open import Data.Product
open import Data.String
open import Relation.Nullary using (Dec; yes; no)
open import Category.Functor

open import Reflection

open import Optics.Functorial

module Optics.Reflection where

 private
  tcMapM : {A B : Set} → (A → TC B) → List A → TC (List B)
  tcMapM f [] = return []
  tcMapM f (x ∷ xs) = do
    y ← f x
    ys ← tcMapM f xs
    return (y ∷ ys)

  count : ℕ → List ℕ
  count 0       = []
  count (suc n) = 0 ∷ List.map suc (count n)

  List-last : {A : Set} → A → List A → A
  List-last d []       = d
  List-last d (x ∷ []) = x
  List-last d (x ∷ xs) = List-last d xs

  ai : {A : Set} → A → Arg A
  ai x = arg (arg-info visible relevant) x

  record MetaLens : Set where
    constructor ml
    field
      mlName : Name
      mlType : Type
      mkDef  : Term

  -- Example call:
  -- Let:
  -- > record Test : Set where
  -- >   constructor test
  -- >   field
  -- >     firstField  : ℕ
  -- >     secondField : Maybe String
  --
  -- Then; consider the call:
  --
  -- > go Test test [x , y] 2 secondField
  --
  -- What we want to generate is:
  --
  --
  -- > secondField : Lens Name (Maybe String)
  -- > secondField = lens (λ { F rf f (test x y)
  -- >                     → (RawFunctor._<$>_ rf)
  -- >                       (λ y' → test x y') (f y)
  -- >                     })
  --
  -- Which is captured by the MetaLens
  go : Name → Name → List String → ℕ → (Name × Arg Name) → TC MetaLens
  go rec cName vars curr (lensName , (arg _ fld)) = do
     -- Get the type of the field; in our case: Mabe String
     tyFld    ← (getType fld >>= parseTy)
     -- compute the full lens type: Lens Test (Maybe String)
     let finalTy = def (quote Lens) (ai (def rec []) ∷ ai tyFld ∷ [])
     -- compute the clause of the lens:
     return (ml lensName finalTy genTerm)
   where
     parseTy : Type → TC Type
     parseTy (pi _ (abs _ t)) = parseTy t
     parseTy (var (suc x) i)  = return (var x i)
     parseTy r                = return r

     -- We might be at field 0; but our de Bruijn index depends
     -- on the total of fields
     curr' : ℕ
     curr' = List.length vars ∸ suc curr

     testxy : Pattern
     testxy = Pattern.con cName (List.map (ai ∘ Pattern.var) vars)

     myabs : Term → Term
     myabs t = pat-lam (Clause.clause (ai (Pattern.var "F") ∷ ai (Pattern.var "rf") ∷ ai (Pattern.var "f") ∷ ai testxy ∷ []) t ∷ []) []

     myvar : ℕ → List (Arg Term) → Term
     myvar n args = var (List.length vars + n) args

     RawFunctor-<$>-var2 : Term → Term → Term
     RawFunctor-<$>-var2 testxy' fy =
       let rawf = quote RawFunctor._<$>_
        in def rawf (ai (myvar 1 []) ∷ (ai testxy') ∷ (ai fy) ∷ [])

     f-varN : Term
     f-varN = myvar 0 (ai (var curr' []) ∷ [])

     xy' : List (Arg Term)
     xy' = let xs = reverse (count (List.length vars))
            in List.map (λ m → ai (var (suc+set0 m) [])) xs
       where
         suc+set0 : ℕ → ℕ
         suc+set0 m = case m ℕ.≟ curr' of
                        λ { (no _) → suc m
                          ; (yes _) → zero
                          }

     testxy' : Term
     testxy' = lam visible (abs "y'" (con cName xy'))

     -- We will now generate the RHS of second field: lens (λ { F rf ⋯
     genTerm : Term
     genTerm = con (quote lens) (ai (myabs (RawFunctor-<$>-var2 testxy' f-varN)) ∷ [])

  mkLensFrom : Name → Definition → List Name → TC (List MetaLens)
  mkLensFrom rec (record-type c fs) lnames = do
    let xs = count (List.length fs)
    let vars = List.map (flip Data.String.replicate 'v' ∘ suc) xs
    tcMapM (uncurry (go rec c vars)) (List.zip xs (List.zip lnames fs))
  mkLensFrom _ _ _ = typeError (strErr "Not a record" ∷ [])

  defineLens : MetaLens → TC ⊤
  defineLens (ml n ty trm)
    = do -- typeError (nameErr n ∷ strErr "%%" ∷ termErr ty ∷ strErr "%%" ∷ termErr trm ∷ [])
         declareDef (arg (arg-info visible relevant) n) ty
         defineFun n (Clause.clause [] trm ∷ [])

 mkLens : Name → List Name → TC ⊤
 mkLens rec lenses = do
   r ← getDefinition rec
   res ← mkLensFrom rec r lenses
   tcMapM defineLens res
   return tt
  -- usage will be: unquoteDecl = mkLens RecordName

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

syntax CommRing | CR

type
  * : 0-ary

term
  zero : * | 𝟘
  add  : *  *  ->  * | _⊕_ l20
  one  : * | 𝟙
  mult : *  *  ->  * | _⊗_ l30
  neg  : *  ->  * | ⊖_ r50

theory
  (𝟘U⊕ᴸ) a |> add (zero, a) = a
  (𝟘U⊕ᴿ) a |> add (a, zero) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
  (𝟙U⊗ᴸ) a |> mult (one, a) = a
  (𝟙U⊗ᴿ) a |> mult (a, one) = a
  (⊗A) a b c |> mult (mult(a, b), c) = mult (a, mult(b, c))
  (⊗D⊕ᴸ) a b c |> mult (a, add (b, c)) = add (mult(a, b), mult(a, c))
  (⊗D⊕ᴿ) a b c |> mult (add (a, b), c) = add (mult(a, c), mult(b, c))
  (𝟘X⊗ᴸ) a |> mult (zero, a) = zero
  (𝟘X⊗ᴿ) a |> mult (a, zero) = zero
  (⊖N⊕ᴸ) a |> add (neg (a), a) = zero
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = zero
  (⊗C) a b |> mult(a, b) = mult(b, a)
-}

module CommRing.Signature where

open import SOAS.Context

open import SOAS.Common

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

-- Operator symbols
data CRₒ : Set where
  zeroₒ addₒ oneₒ multₒ negₒ : CRₒ

-- Term signature
CR:Sig : Signature CRₒ
CR:Sig = sig λ
  {  zeroₒ  → ⟼₀ *
  ;  addₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  oneₒ   → ⟼₀ *
  ;  multₒ  → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  negₒ   → (⊢₀ *) ⟼₁ *
  }

open Signature CR:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module examplesPaperJFP.Console where

open import  examplesPaperJFP.NativeIOSafe
open import  examplesPaperJFP.BasicIO hiding (main)
open import  examplesPaperJFP.ConsoleInterface public

IOConsole : Set → Set
IOConsole = IO ConsoleInterface

--IOConsole+ : Set → Set
--IOConsole+ = IO+ ConsoleInterface

translateIOConsoleLocal : (c : ConsoleCommand) → NativeIO (ConsoleResponse c)
translateIOConsoleLocal (putStrLn s)  =  nativePutStrLn s
translateIOConsoleLocal getLine       =  nativeGetLine

translateIOConsole : {A : Set} → IOConsole A → NativeIO A
translateIOConsole = translateIO translateIOConsoleLocal

main : NativeIO Unit
main = nativePutStrLn "Console"

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
open import Signature
import Program

-- | Herbrand model that takes the distinction between inductive
-- and coinductive clauses into account.
module Herbrand (Σ : Sig) (V : Set) (P : Program.Program Σ V) where

open import Function
open import Data.Empty
open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Sum as Sum
open import Relation.Unary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality hiding ([_])

open import Program Σ V
open import Terms Σ

mutual
  record Herbrand-ν (t : T∞ ⊥) : Set where
    coinductive
    field
      bw-closed :
        (∀ (i : dom-ν P) {σ} →
           (t ~ app∞ σ (χ (geth-ν P i))) →
           ∀ (j : dom (getb-ν P i)) →
           (app∞ σ (χ (get (getb-ν P i) j))) ∈ Herbrand-ν)
        ⊎ (t ∈ Herbrand-μ)

  data Herbrand-μ : T∞ ⊥ → Set where
    fw-closed : (t : T∞ ⊥) → (t ∈ Herbrand-μ) → (i : dom-μ P) (σ : Subst∞ V ⊥) →
                t ≡ app∞ σ (χ (geth-μ P i)) → (j : dom (getb-μ P i)) →
                Herbrand-μ (app∞ σ (χ (get (getb-μ P i) j)))
    coind-μ : {t : T∞ ⊥} → t ∈ Herbrand-ν → Herbrand-μ t

open Herbrand-ν public

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Bool.Base where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

-- Obtain the booleans
open import Agda.Builtin.Bool public

infixr 6 _and_
infixr 5 _or_

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

_or_ : Bool → Bool → Bool
false or false = false
false or true  = true
true  or false = true
true  or true  = true

_and_ : Bool → Bool → Bool
false and false = false
false and true  = false
true  and false = false
true  and true  = true

caseBool : ∀ {ℓ} → {A : Type ℓ} → (a0 aS : A) → Bool → A
caseBool att aff true  = att
caseBool att aff false = aff

_≟_ : Discrete Bool
false ≟ false = yes refl
false ≟ true  = no λ p → subst (caseBool ⊥ Bool) p true
true  ≟ false = no λ p → subst (caseBool Bool ⊥) p true
true  ≟ true  = yes refl

Dec→Bool : ∀ {ℓ} {A : Type ℓ} → Dec A → Bool
Dec→Bool (yes p) = true
Dec→Bool (no ¬p) = false


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.QuotientRing where

open import Cubical.Foundations.Prelude

open import Cubical.HITs.SetQuotients hiding (_/_)

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.QuotientRing renaming (_/_ to _/Ring_) hiding (asRing)

private
  variable
    ℓ : Level

_/_ : (R : CommRing ℓ) → (I : IdealsIn R) → CommRing ℓ
R / I =
  fst asRing , commringstr _ _ _ _ _
                 (iscommring (RingStr.isRing (snd asRing))
                             (elimProp2 (λ _ _ → squash/ _ _)
                                        commEq))
   where
       asRing = (CommRing→Ring R) /Ring (CommIdeal→Ideal I)
       _·/_ : fst asRing → fst asRing → fst asRing
       _·/_ = RingStr._·_ (snd asRing)
       commEq : (x y : fst R) → ([ x ] ·/ [ y ]) ≡ ([ y ] ·/ [ x ])
       commEq x y i = [ CommRingStr.·Comm (snd R) x y i ]

[_]/ : {R : CommRing ℓ} {I : IdealsIn R} → (a : fst R) → fst (R / I)
[ a ]/ = [ a ]

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


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

module RingSolving where

open import Data.Nat hiding (_≟_)
open import Data.Nat.Properties hiding (_≟_)
import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality
open import Agda.Builtin.Equality.Rewrite
open import Function
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)

module _ (A : Set) where
  infixr 5 _+H_
  infixr 6 _*H_

  infixr 5 _:+_
  infixr 6 _:*_

  infixr 5 _+A_
  infixr 6 _*A_

  postulate
    #0 : A
    #1 : A
    _+A_ : A → A → A
    _*A_ : A → A → A

  data Poly : Set where
    con : A → Poly
    var : Poly
    _:+_ : Poly → Poly → Poly
    _:*_ : Poly → Poly → Poly

  data Horner : Set where
    PC : A → Horner
    PX : A → Horner → Horner

  scalMapHorner : (A → A) → Horner → Horner
  scalMapHorner f (PC x) = PC (f x)
  scalMapHorner f (PX x xs) = PX (f x) (scalMapHorner f xs)

  postulate
    extensionality : {S : Set}{T : S -> Set}
                    {f g : (x : S) -> T x} ->
                    ((x : S) -> f x ≡ g x) ->
                    f ≡ g

  postulate
    +A-id-l : ∀ m → #0 +A m ≡ m
    *A-id-l : ∀ m → #1 *A m ≡ m
    +A-id-r : ∀ m → m +A #0 ≡ m
    *A-id-r : ∀ m → m *A #1 ≡ m
    +A-assoc : ∀ m n p → (m +A n) +A p ≡ m +A n +A p
    *A-assoc : ∀ m n p → (m *A n) *A p ≡ m *A n *A p
    +A-comm : ∀ m n → m +A n ≡ n +A m
    *A-comm : ∀ m n → m *A n ≡ n *A m
    *A-+A-distrib : ∀ m n p → m *A (n +A p) ≡ m *A n +A m *A p
    *A-annhiliate-r : ∀ m → m *A #0 ≡ #0
    *A-annhiliate-l : ∀ m → #0 *A m ≡ #0

  *A-+A-distrib′ : ∀ m n p → (m +A n) *A p ≡ m *A p +A n *A p
  *A-+A-distrib′ m n p =
    begin
      (m +A n) *A p ≡⟨ *A-comm (m +A n) p ⟩
      p *A (m +A n) ≡⟨ *A-+A-distrib p m n ⟩
      p *A m +A p *A n ≡⟨ cong₂ (_+A_) (*A-comm p m) (*A-comm p n) ⟩
      m *A p +A n *A p
    ∎
    where open ≡-Reasoning

  {-# REWRITE +A-id-l *A-id-l +A-id-r *A-id-r *A-annhiliate-r *A-annhiliate-l +A-assoc *A-assoc *A-+A-distrib #-}

  _+H_ : Horner → Horner → Horner
  _+H_ (PC x) (PC y) = PC (x +A y)
  _+H_ (PC x) (PX y ys) = PX (x +A y) ys
  _+H_ (PX x xs) (PC y) = PX (x +A y) xs
  _+H_ (PX x xs) (PX y ys) = PX (x +A y) (_+H_ xs ys)

  is-lt : (m : ℕ) → (n : ℕ) → n ⊔ (m Data.Nat.+ suc n) ≡ m Data.Nat.+ suc n
  is-lt m n = m≤n⇒m⊔n≡n $
    begin
      n                    ≤⟨ n≤1+n n ⟩
      suc n                ≤⟨ m≤n+m (suc n) m ⟩
      m Data.Nat.+ suc n
    ∎
    where open ≤-Reasoning

  _*H_ : Horner  → Horner → Horner
  _*H_ (PC x) y = scalMapHorner (x *A_) y
  _*H_ (PX x xs) y = (scalMapHorner (x *A_) y) +H (PX #0 (xs *H y))

  evaluate : Horner → A → A
  evaluate (PC x) v = x
  evaluate (PX x xs) v = x +A (v *A evaluate xs v)

  varH : Horner
  varH = PX #0 $ PC #1

  conH : A → Horner
  conH = PC

  construct : Poly → A → A
  construct (con x) a = x
  construct var a = a
  construct (p :+ p2) a = construct p a +A construct p2 a
  construct (p :* p2) a = construct p a *A construct p2 a

  normalize : Poly → Horner
  normalize (con x) = conH x
  normalize var = varH
  normalize (x :+ y) = normalize x +H normalize y
  normalize (x :* y) = normalize x *H normalize y

  swap : ∀ m n j k → (m +A n) +A (j +A k) ≡ (m +A j) +A (n +A k)
  swap m n j k =
    begin
      (m +A n) +A (j +A k)  ≡⟨ +A-assoc m n (j +A k) ⟩
      m +A (n +A (j +A k))  ≡⟨ cong (m +A_) $ sym $ +A-assoc n j k ⟩
      m +A ((n +A j) +A k)  ≡⟨ cong (\ φ → m +A (φ +A k)) $ +A-comm n j ⟩
      m +A ((j +A n) +A k)  ≡⟨ cong (m +A_) $ +A-assoc j n k ⟩
      m +A (j +A (n +A k))  ≡⟨ sym $ +A-assoc m j (n +A k) ⟩
      (m +A j) +A (n +A k)
    ∎
    where open Eq.≡-Reasoning

  swap2-+A : ∀ m n p → m +A (n +A p) ≡ n +A (m +A p)
  swap2-+A m n p =
    begin
      m +A (n +A p)  ≡⟨ +A-assoc m n p ⟩
      (m +A n) +A p  ≡⟨ cong ( _+A p) $ +A-comm m n ⟩
      (n +A m) +A p  ≡⟨ sym $ +A-assoc n m p ⟩
      n +A (m +A p)
    ∎
    where open Eq.≡-Reasoning

  swap2-*A : ∀ m n p → m *A (n *A p) ≡ n *A (m *A p)
  swap2-*A m n p  =
    begin
      m *A (n *A p)  ≡⟨ *A-assoc m n p ⟩
      (m *A n) *A p  ≡⟨ cong ( _*A p) $ *A-comm m n ⟩
      (n *A m) *A p  ≡⟨ sym $ *A-assoc n m p ⟩
      n *A (m *A p)
    ∎
    where open Eq.≡-Reasoning

  +A-+H-homo : ∀ j k a → evaluate j a +A evaluate k a ≡ evaluate (j +H k) a
  +A-+H-homo (PC x) (PC x₁) a = refl
  +A-+H-homo (PC x) (PX x₁ k) a = refl
  +A-+H-homo (PX x x₁) (PC x₂) a =
    begin
      x +A ((a *A evaluate x₁ a) +A x₂)  ≡⟨ cong (x +A_) $ +A-comm (a *A evaluate x₁ a) x₂ ⟩
      x +A (x₂ +A (a *A evaluate x₁ a))
    ∎
    where open Eq.≡-Reasoning
  +A-+H-homo (PX x x₁) (PX x₂ y) a rewrite +A-+H-homo x₁ y a =
    begin
      (x +A (a *A evaluate x₁ a)) +A (x₂ +A (a *A evaluate y a))  ≡⟨ swap x (a *A evaluate x₁ a) x₂ (a *A evaluate y a) ⟩
      (x +A x₂) +A ((a *A evaluate x₁ a) +A (a *A evaluate y a))  ≡⟨ cong (\φ → (x +A x₂) +A φ) (sym $ *A-+A-distrib a (evaluate x₁ a) (evaluate y a)) ⟩
      (x +A x₂) +A (a *A (evaluate x₁ a +A evaluate y a))         ≡⟨ cong (\φ → (x +A x₂) +A (a *A φ)) (+A-+H-homo x₁ y a) ⟩
      (x +A x₂) +A (a *A evaluate (x₁ +H y) a)
    ∎
    where open Eq.≡-Reasoning

  scale-evaluate : ∀ x k a → x *A evaluate k a ≡ evaluate (scalMapHorner (x *A_) k) a
  scale-evaluate x (PC x₁) a = refl
  scale-evaluate x (PX x₁ k) a =
    begin
      x *A evaluate (PX x₁ k) a                                 ≡⟨⟩
      x *A (x₁ +A (a *A evaluate k a))                          ≡⟨ *A-+A-distrib x x₁ (a *A evaluate k a) ⟩
      (x *A x₁) +A (x *A (a *A evaluate k a))                   ≡⟨ cong ((x *A x₁) +A_) $ swap2-*A x a $ evaluate k a ⟩
      (x *A x₁) +A (a *A (x *A evaluate k a))                   ≡⟨ cong (\ φ → (x *A x₁) +A (a *A φ)) $ scale-evaluate x k a ⟩
      (x *A x₁) +A (a *A evaluate (scalMapHorner (x *A_) k) a)  ≡⟨⟩
      evaluate (PX (x *A x₁) (scalMapHorner (x *A_) k)) a       ≡⟨⟩
      evaluate (scalMapHorner (x *A_) (PX x₁ k)) a
    ∎
    where open Eq.≡-Reasoning

  *A-*H-homo : ∀ j k a → evaluate j a *A evaluate k a ≡ evaluate (j *H k) a
  *A-*H-homo (PC x) k a = scale-evaluate x k a
  *A-*H-homo (PX x j) k a =
    begin
      evaluate (PX x j) a *A evaluate k a             ≡⟨⟩
      (x +A a *A evaluate j a) *A evaluate k a        ≡⟨ *A-+A-distrib′ x (a *A evaluate j a) (evaluate k a) ⟩
      x *A (evaluate k a) +A (a *A evaluate j a) *A evaluate k a        ≡⟨ cong₂ _+A_ (scale-evaluate x k a) (cong (a *A_) (*A-*H-homo j k a)) ⟩
      evaluate (scalMapHorner (_*A_ x) k) a +A evaluate (PX #0 (j *H k)) a ≡⟨ +A-+H-homo (scalMapHorner (_*A_ x) k) (PX #0 (j *H k)) a ⟩
      evaluate (scalMapHorner (_*A_ x) k +H PX #0 (j *H k)) a ≡⟨⟩
      evaluate (PX x j *H k) a
    ∎
    where open Eq.≡-Reasoning

  isoToConstruction : (x : Poly) → (a : A) → construct x a ≡ evaluate (normalize x) a
  isoToConstruction (con x) a = refl
  isoToConstruction var a = refl
  isoToConstruction (x :+ y) a
    rewrite isoToConstruction x a
          | isoToConstruction y a
          | +A-+H-homo (normalize x) (normalize y) a
          = refl
  isoToConstruction (x :* y) a
    rewrite isoToConstruction x a
          | isoToConstruction y a
          | *A-*H-homo (normalize x) (normalize y) a
          = refl

  solve : (x y : Poly) → normalize x ≡ normalize y → (a : A) → construct x a ≡ construct y a
  solve x y eq a =
    begin
      construct x a            ≡⟨ isoToConstruction x a ⟩
      evaluate (normalize x) a  ≡⟨ cong (\φ → evaluate φ a) eq ⟩
      evaluate (normalize y) a  ≡⟨ sym $ isoToConstruction y a ⟩
      construct y a
    ∎
    where open Eq.≡-Reasoning

  test-a : Poly
  test-a = (var :+ con #1) :* (var :+ con #1)

  test-b : Poly
  test-b = var :* var :+ two :* var :+ con #1
    where
      two = con #1 :+ con #1

  blah : (x : A) → (x +A #1) *A (x +A #1) ≡ (x *A x) +A (#1 +A #1) *A x +A #1
  blah x = solve test-a test-b refl x

max_stars_repo_name: dominiquedevriese/reviews

max_issues_repo_name: dominiquedevriese/reviews

max_forks_repo_name: dominiquedevriese/reviews


text:
import      Lvl
open import Data.Boolean
open import Type

module Data.List.Sorting.Functions {ℓ} {T : Type{ℓ}} (_≤?_ : T → T → Bool) where

open import Data.List
import      Data.List.Functions as List

-- Inserts an element to a sorted list so that the resulting list is still sorted.
insert : T → List(T) → List(T)
insert x ∅       = List.singleton(x)
insert x (y ⊰ l) = if(x ≤? y) then (x ⊰ y ⊰ l) else (y ⊰ insert x l)

-- Merges two sorted lists so that the resulting list is still sorted.
merge : List(T) → List(T) → List(T)
merge = List.foldᵣ insert

-- Merges a list of sorted lists so that the resulting list is still sorted.
mergeAll : List(List(T)) → List(T)
mergeAll = List.foldᵣ merge ∅

open import Data.Tuple
open import Data.Option
import      Data.Option.Functions as Option

-- Extracts a smallest element from a list.
extractMinimal : List(T) → Option(T ⨯ List(T))
extractMinimal ∅               = None
extractMinimal (x ⊰ ∅)         = Some(x , ∅)
extractMinimal (x ⊰ l@(_ ⊰ _)) = Option.map(\{(la , las) → if(x ≤? la) then (x , l) else (la , x ⊰ las)}) (extractMinimal l)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Types where

-- Universe levels

postulate  -- Universe levels
  Level : Set
  zero : Level
  suc : Level → Level
  max : Level → Level → Level

{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO zero #-}
{-# BUILTIN LEVELSUC suc #-}
{-# BUILTIN LEVELMAX max #-}

-- Empty type

data ⊥ {i} : Set i where  -- \bot

abort : ∀ {i j} {P : ⊥ {i} → Set j} → ((x : ⊥) → P x)
abort ()

abort-nondep : ∀ {i j} {A : Set j} → (⊥ {i} → A)
abort-nondep ()

¬ : ∀ {i} (A : Set i) → Set i
¬ A = A → ⊥ {zero}

-- Unit type

record unit {i} : Set i where
  constructor tt

⊤ = unit  -- \top

-- Booleans

data bool {i} : Set i where
  true : bool
  false : bool

-- Dependent sum

record Σ {i j} (A : Set i) (P : A → Set j) : Set (max i j) where  -- \Sigma
  constructor _,_
  field
    π₁ : A       -- \pi\_1
    π₂ : P (π₁)  -- \pi\_2
open Σ public

-- Disjoint sum

data _⊔_ {i j} (A : Set i) (B : Set j) : Set (max i j) where  -- \sqcup
  inl : A → A ⊔ B
  inr : B → A ⊔ B

-- Product
_×_ : ∀ {i j} (A : Set i) (B : Set j) → Set (max i j)  -- \times
A × B = Σ A (λ _ → B)

-- Dependent product
Π : ∀ {i j} (A : Set i) (P : A → Set j) → Set (max i j)
Π A P = (x : A) → P x

-- Natural numbers

data ℕ : Set where  -- \bn
  O : ℕ
  S : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO O #-}
{-# BUILTIN SUC S #-}

-- Truncation index (isomorphic to the type of integers ≥ -2)

data ℕ₋₂ : Set where
  ⟨-2⟩ : ℕ₋₂
  S : (n : ℕ₋₂) → ℕ₋₂

⟨-1⟩ : ℕ₋₂
⟨-1⟩ = S ⟨-2⟩

⟨0⟩ : ℕ₋₂
⟨0⟩ = S ⟨-1⟩

_-1 : ℕ → ℕ₋₂
O -1 = ⟨-1⟩
(S n) -1 = S (n -1)

⟨_⟩ : ℕ → ℕ₋₂
⟨ n ⟩ = S (n -1)

⟨1⟩ = ⟨ 1 ⟩
⟨2⟩ = ⟨ 2 ⟩

_+2+_ : ℕ₋₂ → ℕ₋₂ → ℕ₋₂
⟨-2⟩ +2+ n = n
S m +2+ n = S (m +2+ n)

-- Integers

data ℤ : Set where  -- \bz
  O : ℤ
  pos : (n : ℕ) → ℤ
  neg : (n : ℕ) → ℤ

-- Lifting

record lift {i} (j : Level) (A : Set i) : Set (max i j) where
  constructor ↑  -- \u
  field
    ↓ : A  -- \d
open lift public

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------------
-- Auxiliary properties of the McCarthy 91 function
------------------------------------------------------------------------------

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

module FOTC.Program.McCarthy91.AuxiliaryPropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP using ( x<y→y≤z→x<z )
open import FOTC.Data.Nat.PropertiesATP
  using ( +-N
        ; ∸-N
        )
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.Inequalities.PropertiesATP
  using ( x<x+1 )
open import FOTC.Program.McCarthy91.ArithmeticATP
open import FOTC.Program.McCarthy91.McCarthy91

------------------------------------------------------------------------------
--- Auxiliary properties

postulate x>100→x<f₉₁-x+11 : ∀ {n} → N n → n > 100' → n < f₉₁ n + 11'
{-# ATP prove x>100→x<f₉₁-x+11 +-N ∸-N x<y→y≤z→x<z x<x+1 x+1≤x∸10+11 #-}

-- Case n ≡ 100 can be proved automatically
postulate f₉₁-100 : f₉₁ 100' ≡ 91'
{-# ATP prove f₉₁-100 100+11>100 100+11∸10>100 101≡100+11∸10 91≡100+11∸10∸10 #-}

postulate  f₉₁x+11<f₉₁x+11 : ∀ n →
                             n ≯ 100' →
                             f₉₁ (n + 11') < f₉₁ (f₉₁ (n + 11')) + 11' →
                             f₉₁ (n + 11') < f₉₁ n + 11'
{-# ATP prove f₉₁x+11<f₉₁x+11 #-}

postulate f₉₁-x≯100-helper : ∀ m n →
                             m ≯ 100' →
                             f₉₁ (m + 11') ≡ n →
                             f₉₁ n ≡ 91' →
                             f₉₁ m ≡ 91'
{-# ATP prove f₉₁-x≯100-helper #-}

postulate
  f₉₁-110 : f₉₁ (99' + 11') ≡ 100'
  f₉₁-109 : f₉₁ (98' + 11') ≡ 99'
  f₉₁-108 : f₉₁ (97' + 11') ≡ 98'
  f₉₁-107 : f₉₁ (96' + 11') ≡ 97'
  f₉₁-106 : f₉₁ (95' + 11') ≡ 96'
  f₉₁-105 : f₉₁ (94' + 11') ≡ 95'
  f₉₁-104 : f₉₁ (93' + 11') ≡ 94'
  f₉₁-103 : f₉₁ (92' + 11') ≡ 93'
  f₉₁-102 : f₉₁ (91' + 11') ≡ 92'
  f₉₁-101 : f₉₁ (90' + 11') ≡ 91'
{-# ATP prove f₉₁-110 99+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-109 98+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-108 97+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-107 96+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-106 95+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-105 94+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-104 93+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-103 92+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-102 91+11>100 x+11∸10≡Sx #-}
{-# ATP prove f₉₁-101 90+11>100 x+11∸10≡Sx #-}

postulate
  f₉₁-99 : f₉₁ 99' ≡ 91'
  f₉₁-98 : f₉₁ 98' ≡ 91'
  f₉₁-97 : f₉₁ 97' ≡ 91'
  f₉₁-96 : f₉₁ 96' ≡ 91'
  f₉₁-95 : f₉₁ 95' ≡ 91'
  f₉₁-94 : f₉₁ 94' ≡ 91'
  f₉₁-93 : f₉₁ 93' ≡ 91'
  f₉₁-92 : f₉₁ 92' ≡ 91'
  f₉₁-91 : f₉₁ 91' ≡ 91'
  f₉₁-90 : f₉₁ 90' ≡ 91'
{-# ATP prove f₉₁-99 f₉₁-x≯100-helper f₉₁-110 f₉₁-100 #-}
{-# ATP prove f₉₁-98 f₉₁-x≯100-helper f₉₁-109 f₉₁-99 #-}
{-# ATP prove f₉₁-97 f₉₁-x≯100-helper f₉₁-108 f₉₁-98 #-}
{-# ATP prove f₉₁-96 f₉₁-x≯100-helper f₉₁-107 f₉₁-97 #-}
{-# ATP prove f₉₁-95 f₉₁-x≯100-helper f₉₁-106 f₉₁-96 #-}
{-# ATP prove f₉₁-94 f₉₁-x≯100-helper f₉₁-105 f₉₁-95 #-}
{-# ATP prove f₉₁-93 f₉₁-x≯100-helper f₉₁-104 f₉₁-94 #-}
{-# ATP prove f₉₁-92 f₉₁-x≯100-helper f₉₁-103 f₉₁-93 #-}
{-# ATP prove f₉₁-91 f₉₁-x≯100-helper f₉₁-102 f₉₁-92 #-}
{-# ATP prove f₉₁-90 f₉₁-x≯100-helper f₉₁-101 f₉₁-91 #-}

f₉₁-x≡y : ∀ {m n o} → f₉₁ m ≡ n → o ≡ m → f₉₁ o ≡ n
f₉₁-x≡y h refl = h

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

plus : Nat -> Nat -> Nat
plus = {!   !}

function1 : (x : Nat) -> (y : Nat) -> Nat
function1 x y = plus x y

pickTheFirst :  Nat -> Bool -> Nat
pickTheFirst x y = x

function2 :  Nat -> Bool -> Nat
function2 x y = pickTheFirst x y


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

open import Base
open import Algebra.Groups
open import Integers
open import Homotopy.Truncation
open import Homotopy.Pointed
open import Homotopy.PathTruncation
open import Homotopy.Connected

-- Definitions and properties of homotopy groups
module Homotopy.HomotopyGroups {i} where

-- Loop space
Ω : (X : pType i) → pType i
Ω X = ⋆[ ⋆ X ≡ ⋆ X , refl ]

Ω-pregroup : (X : pType i) → pregroup i
Ω-pregroup X = record
  { carrier       = (⋆ X) ≡ (⋆ X)
  ; _∙_           = _∘_
  ; e             = refl
  ; _′            = !
  ; assoc         = concat-assoc
  ; right-unit    = refl-right-unit
  ; left-unit     = λ _ → refl
  ; right-inverse = opposite-right-inverse
  ; left-inverse  = opposite-left-inverse
  }

Ωⁿ-pregroup : (n : ℕ) ⦃ ≢0 : n ≢ O ⦄ (X : pType i) → pregroup i
Ωⁿ-pregroup O ⦃ ≢0 ⦄ X = abort-nondep (≢0 refl)
Ωⁿ-pregroup 1 X = Ω-pregroup X
Ωⁿ-pregroup (S (S n)) X = Ωⁿ-pregroup (S n) (Ω X)

-- Homotopy groups
πⁿ-group : (n : ℕ) ⦃ >0 : n ≢ O ⦄ (X : pType i) → group i
πⁿ-group n X = π₀-pregroup (Ωⁿ-pregroup n X)

fundamental-group : (X : pType i) → group i
fundamental-group X = πⁿ-group 1 ⦃ ℕ-S≢O 0 ⦄ X

-- Homotopy groups of loop space
πⁿ-group-from-πⁿΩ : (n : ℕ) ⦃ ≢0 : n ≢ 0 ⦄ (X : pType i)
  → πⁿ-group (S n) X ≡ πⁿ-group n (Ω X)
πⁿ-group-from-πⁿΩ O ⦃ ≢0 ⦄ X = abort-nondep (≢0 refl)
πⁿ-group-from-πⁿΩ 1 X = refl
πⁿ-group-from-πⁿΩ (S (S n)) X = refl

-- Homotopy groups of spaces of a given h-level
abstract
  truncated-πⁿ-group : (n : ℕ) ⦃ ≢0 : n ≢ 0 ⦄ (X : pType i)
    (p : is-truncated (n -1) ∣ X ∣)
    → πⁿ-group n X ≡ unit-group
  truncated-πⁿ-group O ⦃ ≢0 ⦄ X p = abort-nondep (≢0 refl)
  truncated-πⁿ-group 1 X p =
    unit-group-unique _
      (proj refl ,
      π₀-extend ⦃ p = λ x → truncated-is-truncated-S _ (π₀-is-set _ _ _) ⦄
        (λ x → ap proj (π₁ (p _ _ _ _))))
  truncated-πⁿ-group (S (S n)) X p =
    truncated-πⁿ-group (S n) (Ω X) (λ x y → p _ _ x y)

Ωⁿ : (n : ℕ) (X : pType i) → pType i
Ωⁿ 0 X = X
Ωⁿ (S n) X = Ω (Ωⁿ n X)

πⁿ : (n : ℕ) (X : pType i) → pType i
πⁿ n X = τ⋆ ⟨0⟩ (Ωⁿ n X)

other-πⁿ : (n : ℕ) (X : pType i) → pType i
other-πⁿ n X = Ωⁿ n (τ⋆ ⟨ n ⟩ X)

ap-Ω-equiv : (X Y : pType i) (e : X ≃⋆ Y)
  → Ω X ≃⋆ Ω Y
ap-Ω-equiv X Y e = transport (λ u → Ω X ≃⋆ Ω u) (pType-eq e) (id-equiv⋆ _)

τ⋆Ω-is-Ωτ⋆S : (n : ℕ₋₂) (X : pType i)
  → τ⋆ n (Ω X) ≃⋆ Ω (τ⋆ (S n) X)
τ⋆Ω-is-Ωτ⋆S n X = (τ-path-equiv-path-τ-S , refl)

τ⋆kΩⁿ-is-Ωⁿτ⋆n+k : (k n : ℕ) (X : pType i)
  → τ⋆ ⟨ k ⟩ (Ωⁿ n X) ≃⋆ Ωⁿ n (τ⋆ ⟨ n + k ⟩ X)
τ⋆kΩⁿ-is-Ωⁿτ⋆n+k k O X = id-equiv⋆ _
τ⋆kΩⁿ-is-Ωⁿτ⋆n+k k (S n) X =
  equiv-compose⋆ (τ⋆Ω-is-Ωτ⋆S _ _) (ap-Ω-equiv _ _
    (equiv-compose⋆ (τ⋆kΩⁿ-is-Ωⁿτ⋆n+k (S k) n _)
      (transport (λ u → Ωⁿ n (τ⋆ ⟨ n + S k ⟩ X) ≃⋆ Ωⁿ n (τ⋆ ⟨ u ⟩ X))
        (+S-is-S+ n k) (id-equiv⋆ _))))

πⁿ-is-other-πⁿ : (n : ℕ) (X : pType i) → πⁿ n X ≃⋆ other-πⁿ n X
πⁿ-is-other-πⁿ n X =
  transport (λ u → πⁿ n X ≃⋆ Ωⁿ n (τ⋆ ⟨ u ⟩ X)) (+0-is-id n)
    (τ⋆kΩⁿ-is-Ωⁿτ⋆n+k 0 n X)

contr-is-contr-Ω : (X : pType i) → (is-contr⋆ X → is-contr⋆ (Ω X))
contr-is-contr-Ω X p = ≡-is-truncated ⟨-2⟩ p

contr-is-contr-Ωⁿ : (n : ℕ) (X : pType i) → (is-contr⋆ X) → is-contr⋆ (Ωⁿ n X)
contr-is-contr-Ωⁿ O X p = p
contr-is-contr-Ωⁿ (S n) X p = contr-is-contr-Ω _ (contr-is-contr-Ωⁿ n X p)

connected-other-πⁿ : (k n : ℕ) (lt : k < S n) (X : pType i)
  → (is-connected⋆ ⟨ n ⟩ X → is-contr⋆ (other-πⁿ k X))
connected-other-πⁿ k n lt X p =
  contr-is-contr-Ωⁿ k _ (connected⋆-lt k n lt X p)

connected-πⁿ : (k n : ℕ) (lt : k < S n) (X : pType i)
  → (is-connected⋆ ⟨ n ⟩ X → is-contr⋆ (πⁿ k X))
connected-πⁿ k n lt X p =
  equiv-types-truncated _ (π₁ (πⁿ-is-other-πⁿ k X) ⁻¹)
                       (connected-other-πⁿ k n lt X p)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda


text:
{-# OPTIONS -W ignore #-}
module Issue2596b where

-- This warning will be ignored
{-# REWRITE #-}

-- but this error will still be raised
f : Set
f = f

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module hott.level.sets.core where

open import sum
open import equality.core
open import sets.unit
open import sets.empty
open import hott.level.core

⊤-contr : ∀ {i} → contr (⊤ {i})
⊤-contr = tt , λ { tt → refl }

⊥-prop : ∀ {i} → h 1 (⊥ {i})
⊥-prop x _ = ⊥-elim x

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --without-K #-}
module equality.core where

open import sum
open import level using ()
open import function.core

infix 4 _≡_

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

sym : ∀ {i} {A : Set i} {x y : A}
    → x ≡ y → y ≡ x
sym refl = refl

_·_ : ∀ {i}{X : Set i}{x y z : X}
    → x ≡ y → y ≡ z → x ≡ z
refl · p = p
infixl 9 _·_

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

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

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

subst₂ : ∀ {i j k} {A : Set i}{x x' : A}
         {B : Set j}{y y' : B}
       → (C : A → B → Set k)
       → x ≡ x' → y ≡ y'
       → C x y → C x' y'
subst₂ C refl refl = id

singleton : ∀ {i}{A : Set i} → A → Set i
singleton {A = A} a = Σ A λ a' → a ≡ a'

singleton' : ∀ {i}{A : Set i} → A → Set i
singleton' {A = A} a = Σ A λ a' → a' ≡ a

J' : ∀ {i j}{X : Set i}{x : X}
   → (P : (y : X) → x ≡ y → Set j)
   → P x refl
   → (y : X)
   → (p : x ≡ y)
   → P y p
J' P u y refl = u

J : ∀ {i j}{X : Set i}
  → (P : (x y : X) → x ≡ y → Set j)
  → ((x : X) → P x x refl)
  → (x y : X)
  → (p : x ≡ y)
  → P x y p
J P u x y p = J' (P x) (u x) y p

max_stars_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
-- The ATP pragma with the role <hint> can be used with functions.

module ATPHint where

postulate
  D : Set

data _≡_ (x : D) : D → Set where
  refl : x ≡ x

sym : ∀ {m n} → m ≡ n → n ≡ m
sym refl = refl
{-# ATP hint sym #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

open import Agda.Builtin.Bool

data D : Bool → Set where
  true  : D true
  false : D false

F : @0 D false → Set₁
F false = Set


text:
------------------------------------------------------------------------
-- Abstract well-formed typing contexts
------------------------------------------------------------------------

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

module Data.Context.WellFormed where

open import Level using (suc; _⊔_; Lift; lift)
open import Data.Fin using (Fin)
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (ℕ)
open import Data.Unit using (⊤; tt)
open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
open import Data.Vec.Relation.Unary.All.Properties using (gmap)
open import Relation.Binary using (REL)
open import Relation.Unary using (Pred)

open import Data.Context

------------------------------------------------------------------------
-- Abstract well-formed typing

-- An abtract well-formedness judgment _⊢_wf : Wf Tp Tm is a binary
-- relation which, in a given Tp-context, asserts the well-formedness
-- of Tm-terms.

Wf : ∀ {t₁ t₂} → Pred ℕ t₁ → Pred ℕ t₂ → ∀ ℓ → Set (t₁ ⊔ t₂ ⊔ suc ℓ)
Wf Tp Tm ℓ = ∀ {n} → REL (Ctx Tp n) (Tm n) ℓ

------------------------------------------------------------------------
-- Abstract well-formed typing contexts and context extensions.
--
-- A well-formed typing context (Γ wf) is a context Γ in which every
-- participating T-type is well-formed.

module ContextFormation {t ℓ} {T : Pred ℕ t} (_⊢_wf : Wf T T ℓ) where

  infix  4 _wf _⊢_wfExt
  infixr 5 _∷_

  -- Well-formed typing contexts and context extensions.

  data _wf : ∀ {n} → Ctx T n → Set (t ⊔ ℓ) where
    []  :                                              [] wf
    _∷_ : ∀ {n t} {Γ : Ctx T n} → Γ ⊢ t wf → Γ wf → t ∷ Γ wf

  data _⊢_wfExt {m} (Γ : Ctx T m) : ∀ {n} → CtxExt T m n → Set (t ⊔ ℓ) where
    []  : Γ ⊢ [] wfExt
    _∷_ : ∀ {n t} {Δ : CtxExt T m n} →
          (Δ ++ Γ) ⊢ t wf → Γ ⊢ Δ wfExt → Γ ⊢ t ∷ Δ wfExt

  -- Inversions.

  wf-∷₁ : ∀ {n} {Γ : Ctx T n} {a} → a ∷ Γ wf → Γ ⊢ a wf
  wf-∷₁ (a-wf ∷ _) = a-wf

  wf-∷₂ : ∀ {n} {Γ : Ctx T n} {a} → a ∷ Γ wf → Γ wf
  wf-∷₂ (_ ∷ Γ-wf) = Γ-wf

  wfExt-∷₁ : ∀ {m n} {Γ : Ctx T m} {Δ : CtxExt T m n} {a} →
             Γ ⊢ a ∷ Δ wfExt → (Δ ++ Γ) ⊢ a wf
  wfExt-∷₁ (a-wf ∷ _) = a-wf

  wfExt-∷₂ : ∀ {m n} {Γ : Ctx T m} {Δ : CtxExt T m n} {a} →
             Γ ⊢ a ∷ Δ wfExt → Γ ⊢ Δ wfExt
  wfExt-∷₂ (_ ∷ Γ-wf) = Γ-wf

  -- Operations on well-formed contexts that require weakening of
  -- well-formedness judgments.

  record WellFormedWeakenOps (typeExtension : Extension T)
                             : Set (suc (t ⊔ ℓ)) where

    private module C = WeakenOps typeExtension
    open C hiding (lookup; extLookup)

    -- Weakening of well-formedness judgments.

    field wf-weaken : ∀ {n} {Γ : Ctx T n} {a b} → Γ ⊢ a wf → Γ ⊢ b wf →
                      (a ∷ Γ) ⊢ weaken b wf

    -- Convert a well-formed context (extension) to its All representation.

    toAll : ∀ {n} {Γ : Ctx T n} → Γ wf → All (λ t → Γ ⊢ t wf) (toVec Γ)
    toAll []            = []
    toAll (t-wf ∷ Γ-wf) =
      wf-weaken t-wf t-wf ∷ gmap (wf-weaken t-wf) (toAll Γ-wf)

    extToAll : ∀ {m n} {Γ : Ctx T m} {Δ : CtxExt T m n} →
               All (λ t → Γ ⊢ t wf) (toVec Γ) → Γ ⊢ Δ wfExt →
               All (λ a → (Δ ++ Γ) ⊢ a wf) (toVec (Δ ++ Γ))
    extToAll ts-wf []               = ts-wf
    extToAll ts-wf (t-wf ∷ Δ-wfExt) =
      wf-weaken t-wf t-wf ∷ gmap (wf-weaken t-wf) (extToAll ts-wf Δ-wfExt)

    -- Lookup the well-formedness proof of a variable in a context.

    lookup : ∀ {n} {Γ : Ctx T n} → Γ wf → (x : Fin n) → Γ ⊢ (C.lookup Γ x) wf
    lookup Γ-wf x = All.lookup x (toAll Γ-wf)

    extLookup : ∀ {m n} {Γ : Ctx T m} {Δ : CtxExt T m n} →
                All (λ t → Γ ⊢ t wf) (toVec Γ) → Γ ⊢ Δ wfExt →
                ∀ x → (Δ ++ Γ) ⊢ (C.lookup (Δ ++ Γ) x) wf
    extLookup ts-wf Γ-wf x = All.lookup x (extToAll ts-wf Γ-wf)

------------------------------------------------------------------------
-- Trivial well-formedness.
--
-- This module provides a trivial well-formedness relation and the
-- corresponding trivially well-formed contexts.  This is useful when
-- implmenting typed substitutions on types that either lack or do not
-- necessitate a notion of well-formedness.

module ⊤-WellFormed {ℓ} {T : Pred ℕ ℓ} (typeExtension : Extension T) where

  infix  4 _⊢_wf

  -- Trivial well-formedness.

  _⊢_wf : Wf T T ℓ
  _ ⊢ _ wf = Lift ℓ ⊤

  open ContextFormation _⊢_wf public

  -- Trivial well-formedness of contexts and context extensions.

  ctx-wf : ∀ {n} (Γ : Ctx T n) → Γ wf
  ctx-wf []      = []
  ctx-wf (a ∷ Γ) = lift tt ∷ ctx-wf Γ

  ctx-wfExt : ∀ {m n} (Δ : CtxExt T m n) {Γ : Ctx T m} → Γ ⊢ Δ wfExt
  ctx-wfExt []      = []
  ctx-wfExt (a ∷ Δ) = lift tt ∷ ctx-wfExt Δ

  module ⊤-WfWeakenOps where

    wfWeakenOps : WellFormedWeakenOps typeExtension
    wfWeakenOps = record { wf-weaken = λ _ _ → lift tt }

    open WellFormedWeakenOps public

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


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

module Definition.Typed.Properties where

open import Definition.Untyped
open import Definition.Typed

open import Tools.Empty using (⊥; ⊥-elim)
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Escape context extraction

wfTerm : ∀ {Γ A t} → Γ ⊢ t ∷ A → ⊢ Γ
wfTerm (ℕⱼ ⊢Γ) = ⊢Γ
wfTerm (Emptyⱼ ⊢Γ) = ⊢Γ
wfTerm (Unitⱼ ⊢Γ) = ⊢Γ
wfTerm (Πⱼ F ▹ G) = wfTerm F
wfTerm (var ⊢Γ x₁) = ⊢Γ
wfTerm (lamⱼ F t) with wfTerm t
wfTerm (lamⱼ F t) | ⊢Γ ∙ F′ = ⊢Γ
wfTerm (g ∘ⱼ a) = wfTerm a
wfTerm (zeroⱼ ⊢Γ) = ⊢Γ
wfTerm (sucⱼ n) = wfTerm n
wfTerm (natrecⱼ F z s n) = wfTerm z
wfTerm (Emptyrecⱼ A e) = wfTerm e
wfTerm (starⱼ ⊢Γ) = ⊢Γ
wfTerm (conv t A≡B) = wfTerm t
wfTerm (Σⱼ a ▹ a₁) = wfTerm a
wfTerm (prodⱼ F G a a₁) = wfTerm a
wfTerm (fstⱼ _ _ a) = wfTerm a
wfTerm (sndⱼ _ _ a) = wfTerm a

wf : ∀ {Γ A} → Γ ⊢ A → ⊢ Γ
wf (ℕⱼ ⊢Γ) = ⊢Γ
wf (Emptyⱼ ⊢Γ) = ⊢Γ
wf (Unitⱼ ⊢Γ) = ⊢Γ
wf (Uⱼ ⊢Γ) = ⊢Γ
wf (Πⱼ F ▹ G) = wf F
wf (Σⱼ F ▹ G) = wf F
wf (univ A) = wfTerm A

wfEqTerm : ∀ {Γ A t u} → Γ ⊢ t ≡ u ∷ A → ⊢ Γ
wfEqTerm (refl t) = wfTerm t
wfEqTerm (sym t≡u) = wfEqTerm t≡u
wfEqTerm (trans t≡u u≡r) = wfEqTerm t≡u
wfEqTerm (conv t≡u A≡B) = wfEqTerm t≡u
wfEqTerm (Π-cong F F≡H G≡E) = wfEqTerm F≡H
wfEqTerm (app-cong f≡g a≡b) = wfEqTerm f≡g
wfEqTerm (β-red F t a) = wfTerm a
wfEqTerm (η-eq F f g f0≡g0) = wfTerm f
wfEqTerm (suc-cong n) = wfEqTerm n
wfEqTerm (natrec-cong F≡F′ z≡z′ s≡s′ n≡n′) = wfEqTerm z≡z′
wfEqTerm (natrec-zero F z s) = wfTerm z
wfEqTerm (natrec-suc n F z s) = wfTerm n
wfEqTerm (Emptyrec-cong A≡A' e≡e') = wfEqTerm e≡e'
wfEqTerm (η-unit e e') = wfTerm e
wfEqTerm (Σ-cong F _ _) = wf F
wfEqTerm (fst-cong _ _ a) = wfEqTerm a
wfEqTerm (snd-cong _ _ a) = wfEqTerm a
wfEqTerm (Σ-η _ _ x _ _ _) = wfTerm x
wfEqTerm (Σ-β₁ F G x x₁) = wfTerm x
wfEqTerm (Σ-β₂ F G x x₁) = wfTerm x

wfEq : ∀ {Γ A B} → Γ ⊢ A ≡ B → ⊢ Γ
wfEq (univ A≡B) = wfEqTerm A≡B
wfEq (refl A) = wf A
wfEq (sym A≡B) = wfEq A≡B
wfEq (trans A≡B B≡C) = wfEq A≡B
wfEq (Π-cong F F≡H G≡E) = wf F
wfEq (Σ-cong F x₁ x₂) = wf F

-- Reduction is a subset of conversion

subsetTerm : ∀ {Γ A t u} → Γ ⊢ t ⇒ u ∷ A → Γ ⊢ t ≡ u ∷ A
subsetTerm (natrec-subst F z s n⇒n′) =
  natrec-cong (refl F) (refl z) (refl s) (subsetTerm n⇒n′)
subsetTerm (natrec-zero F z s) = natrec-zero F z s
subsetTerm (natrec-suc n F z s) = natrec-suc n F z s
subsetTerm (Emptyrec-subst A n⇒n′) =
  Emptyrec-cong (refl A) (subsetTerm n⇒n′)
subsetTerm (app-subst t⇒u a) = app-cong (subsetTerm t⇒u) (refl a)
subsetTerm (β-red A t a) = β-red A t a
subsetTerm (conv t⇒u A≡B) = conv (subsetTerm t⇒u) A≡B
subsetTerm (fst-subst F G x) = fst-cong F G (subsetTerm x)
subsetTerm (snd-subst F G x) = snd-cong F G (subsetTerm x)
subsetTerm (Σ-β₁ F G x x₁) = Σ-β₁ F G x x₁
subsetTerm (Σ-β₂ F G x x₁) = Σ-β₂ F G x x₁

subset : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A ≡ B
subset (univ A⇒B) = univ (subsetTerm A⇒B)

subset*Term : ∀ {Γ A t u} → Γ ⊢ t ⇒* u ∷ A → Γ ⊢ t ≡ u ∷ A
subset*Term (id t) = refl t
subset*Term (t⇒t′ ⇨ t⇒*u) = trans (subsetTerm t⇒t′) (subset*Term t⇒*u)

subset* : ∀ {Γ A B} → Γ ⊢ A ⇒* B → Γ ⊢ A ≡ B
subset* (id A) = refl A
subset* (A⇒A′ ⇨ A′⇒*B) = trans (subset A⇒A′) (subset* A′⇒*B)

-- Can extract left-part of a reduction

redFirstTerm : ∀ {Γ t u A} → Γ ⊢ t ⇒ u ∷ A → Γ ⊢ t ∷ A
redFirstTerm (conv t⇒u A≡B) = conv (redFirstTerm t⇒u) A≡B
redFirstTerm (app-subst t⇒u a) = (redFirstTerm t⇒u) ∘ⱼ a
redFirstTerm (β-red A t a) = (lamⱼ A t) ∘ⱼ a
redFirstTerm (natrec-subst F z s n⇒n′) = natrecⱼ F z s (redFirstTerm n⇒n′)
redFirstTerm (natrec-zero F z s) = natrecⱼ F z s (zeroⱼ (wfTerm z))
redFirstTerm (natrec-suc n F z s) = natrecⱼ F z s (sucⱼ n)
redFirstTerm (Emptyrec-subst A n⇒n′) = Emptyrecⱼ A (redFirstTerm n⇒n′)
redFirstTerm (fst-subst F G x) = fstⱼ F G (redFirstTerm x)
redFirstTerm (snd-subst F G x) = sndⱼ F G (redFirstTerm x)
redFirstTerm (Σ-β₁ F G x x₁) = fstⱼ F G (prodⱼ F G x x₁)
redFirstTerm (Σ-β₂ F G x x₁) = sndⱼ F G (prodⱼ F G x x₁)

redFirst : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A
redFirst (univ A⇒B) = univ (redFirstTerm A⇒B)

redFirst*Term : ∀ {Γ t u A} → Γ ⊢ t ⇒* u ∷ A → Γ ⊢ t ∷ A
redFirst*Term (id t) = t
redFirst*Term (t⇒t′ ⇨ t′⇒*u) = redFirstTerm t⇒t′

redFirst* : ∀ {Γ A B} → Γ ⊢ A ⇒* B → Γ ⊢ A
redFirst* (id A) = A
redFirst* (A⇒A′ ⇨ A′⇒*B) = redFirst A⇒A′

-- No neutral terms are well-formed in an empty context

noNe : ∀ {t A} → ε ⊢ t ∷ A → Neutral t → ⊥
noNe (conv ⊢t x) n = noNe ⊢t n
noNe (var x₁ ()) (var x)
noNe (⊢t ∘ⱼ ⊢t₁) (∘ₙ neT) = noNe ⊢t neT
noNe (fstⱼ _ _ ⊢t) (fstₙ neT) = noNe ⊢t neT
noNe (sndⱼ _ _ ⊢t) (sndₙ neT) = noNe ⊢t neT
noNe (natrecⱼ x ⊢t ⊢t₁ ⊢t₂) (natrecₙ neT) = noNe ⊢t₂ neT
noNe (Emptyrecⱼ A ⊢e) (Emptyrecₙ neT) = noNe ⊢e neT

-- Neutrals do not weak head reduce

neRedTerm : ∀ {Γ t u A} (d : Γ ⊢ t ⇒ u ∷ A) (n : Neutral t) → ⊥
neRedTerm (conv d x) n = neRedTerm d n
neRedTerm (app-subst d x) (∘ₙ n) = neRedTerm d n
neRedTerm (β-red x x₁ x₂) (∘ₙ ())
neRedTerm (natrec-subst x x₁ x₂ d) (natrecₙ n₁) = neRedTerm d n₁
neRedTerm (natrec-zero x x₁ x₂) (natrecₙ ())
neRedTerm (natrec-suc x x₁ x₂ x₃) (natrecₙ ())
neRedTerm (Emptyrec-subst x d) (Emptyrecₙ n₁) = neRedTerm d n₁
neRedTerm (fst-subst _ _ d) (fstₙ n) = neRedTerm d n
neRedTerm (snd-subst _ _ d) (sndₙ n) = neRedTerm d n
neRedTerm (Σ-β₁ F G x x₁) (fstₙ ())
neRedTerm (Σ-β₂ F G x x₁) (sndₙ ())

neRed : ∀ {Γ A B} (d : Γ ⊢ A ⇒ B) (N : Neutral A) → ⊥
neRed (univ x) N = neRedTerm x N

-- Whnfs do not weak head reduce

whnfRedTerm : ∀ {Γ t u A} (d : Γ ⊢ t ⇒ u ∷ A) (w : Whnf t) → ⊥
whnfRedTerm (conv d x) w = whnfRedTerm d w
whnfRedTerm (app-subst d x) (ne (∘ₙ x₁)) = neRedTerm d x₁
whnfRedTerm (β-red x x₁ x₂) (ne (∘ₙ ()))
whnfRedTerm (natrec-subst x x₁ x₂ d) (ne (natrecₙ x₃)) = neRedTerm d x₃
whnfRedTerm (natrec-zero x x₁ x₂) (ne (natrecₙ ()))
whnfRedTerm (natrec-suc x x₁ x₂ x₃) (ne (natrecₙ ()))
whnfRedTerm (Emptyrec-subst x d) (ne (Emptyrecₙ x₂)) = neRedTerm d x₂
whnfRedTerm (fst-subst _ _ d) (ne (fstₙ n)) = neRedTerm d n
whnfRedTerm (snd-subst _ _ d) (ne (sndₙ n)) = neRedTerm d n
whnfRedTerm (Σ-β₁ F G x x₁) (ne (fstₙ ()))
whnfRedTerm (Σ-β₂ F G x x₁) (ne (sndₙ ()))

whnfRed : ∀ {Γ A B} (d : Γ ⊢ A ⇒ B) (w : Whnf A) → ⊥
whnfRed (univ x) w = whnfRedTerm x w

whnfRed*Term : ∀ {Γ t u A} (d : Γ ⊢ t ⇒* u ∷ A) (w : Whnf t) → t PE.≡ u
whnfRed*Term (id x) Uₙ = PE.refl
whnfRed*Term (id x) Πₙ = PE.refl
whnfRed*Term (id x) Σₙ = PE.refl
whnfRed*Term (id x) ℕₙ = PE.refl
whnfRed*Term (id x) Emptyₙ = PE.refl
whnfRed*Term (id x) Unitₙ = PE.refl
whnfRed*Term (id x) lamₙ = PE.refl
whnfRed*Term (id x) prodₙ = PE.refl
whnfRed*Term (id x) zeroₙ = PE.refl
whnfRed*Term (id x) sucₙ = PE.refl
whnfRed*Term (id x) starₙ = PE.refl
whnfRed*Term (id x) (ne x₁) = PE.refl
whnfRed*Term (conv x x₁ ⇨ d) w = ⊥-elim (whnfRedTerm x w)
whnfRed*Term (x ⇨ d) (ne x₁) = ⊥-elim (neRedTerm x x₁)

whnfRed* : ∀ {Γ A B} (d : Γ ⊢ A ⇒* B) (w : Whnf A) → A PE.≡ B
whnfRed* (id x) w = PE.refl
whnfRed* (x ⇨ d) w = ⊥-elim (whnfRed x w)

-- Whr is deterministic

whrDetTerm : ∀{Γ t u A u′ A′} (d : Γ ⊢ t ⇒ u ∷ A) (d′ : Γ ⊢ t ⇒ u′ ∷ A′) → u PE.≡ u′
whrDetTerm (conv d x) d′ = whrDetTerm d d′
whrDetTerm d (conv d′ x₁) = whrDetTerm d d′
whrDetTerm (app-subst d x) (app-subst d′ x₁) rewrite whrDetTerm d d′ = PE.refl
whrDetTerm (β-red x x₁ x₂) (β-red x₃ x₄ x₅) = PE.refl
whrDetTerm (fst-subst _ _ x) (fst-subst _ _ y) rewrite whrDetTerm x y = PE.refl
whrDetTerm (snd-subst _ _ x) (snd-subst _ _ y) rewrite whrDetTerm x y = PE.refl
whrDetTerm (Σ-β₁ F G x x₁) (Σ-β₁ F₁ G₁ x₂ x₃) = PE.refl
whrDetTerm (Σ-β₂ F G x x₁) (Σ-β₂ F₁ G₁ x₂ x₃) = PE.refl
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-subst x₃ x₄ x₅ d′) rewrite whrDetTerm d d′ = PE.refl
whrDetTerm (natrec-zero x x₁ x₂) (natrec-zero x₃ x₄ x₅) = PE.refl
whrDetTerm (natrec-suc x x₁ x₂ x₃) (natrec-suc x₄ x₅ x₆ x₇) = PE.refl
whrDetTerm (Emptyrec-subst x d) (Emptyrec-subst x₂ d′) rewrite whrDetTerm d d′ = PE.refl

whrDetTerm (app-subst d x) (β-red x₁ x₂ x₃) = ⊥-elim (whnfRedTerm d lamₙ)
whrDetTerm (β-red x x₁ x₂) (app-subst d x₃) = ⊥-elim (whnfRedTerm d lamₙ)
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-zero x₃ x₄ x₅) = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-suc x₃ x₄ x₅ x₆) = ⊥-elim (whnfRedTerm d sucₙ)
whrDetTerm (natrec-zero x x₁ x₂) (natrec-subst x₃ x₄ x₅ d′) = ⊥-elim (whnfRedTerm d′ zeroₙ)
whrDetTerm (natrec-suc x x₁ x₂ x₃) (natrec-subst x₄ x₅ x₆ d′) = ⊥-elim (whnfRedTerm d′ sucₙ)
whrDetTerm (fst-subst _ _ x) (Σ-β₁ F G x₁ x₂) = ⊥-elim (whnfRedTerm x prodₙ)
whrDetTerm (snd-subst _ _ x) (Σ-β₂ F G x₁ x₂) = ⊥-elim (whnfRedTerm x prodₙ)
whrDetTerm (Σ-β₁ F G x x₁) (fst-subst _ _ y) = ⊥-elim (whnfRedTerm y prodₙ)
whrDetTerm (Σ-β₂ F G x x₁) (snd-subst _ _ y) = ⊥-elim (whnfRedTerm y prodₙ)

whrDet : ∀{Γ A B B′} (d : Γ ⊢ A ⇒ B) (d′ : Γ ⊢ A ⇒ B′) → B PE.≡ B′
whrDet (univ x) (univ x₁) = whrDetTerm x x₁

whrDet↘Term : ∀{Γ t u A u′} (d : Γ ⊢ t ↘ u ∷ A) (d′ : Γ ⊢ t ⇒* u′ ∷ A) → Γ ⊢ u′ ⇒* u ∷ A
whrDet↘Term (proj₁ , proj₂) (id x) = proj₁
whrDet↘Term (id x , proj₂) (x₁ ⇨ d′) = ⊥-elim (whnfRedTerm x₁ proj₂)
whrDet↘Term (x ⇨ proj₁ , proj₂) (x₁ ⇨ d′) =
  whrDet↘Term (PE.subst (λ x₂ → _ ⊢ x₂ ↘ _ ∷ _) (whrDetTerm x x₁) (proj₁ , proj₂)) d′

whrDet*Term : ∀{Γ t u A u′} (d : Γ ⊢ t ↘ u ∷ A) (d′ : Γ ⊢ t ↘ u′ ∷ A) → u PE.≡ u′
whrDet*Term (id x , proj₂) (id x₁ , proj₄) = PE.refl
whrDet*Term (id x , proj₂) (x₁ ⇨ proj₃ , proj₄) = ⊥-elim (whnfRedTerm x₁ proj₂)
whrDet*Term (x ⇨ proj₁ , proj₂) (id x₁ , proj₄) = ⊥-elim (whnfRedTerm x proj₄)
whrDet*Term (x ⇨ proj₁ , proj₂) (x₁ ⇨ proj₃ , proj₄) =
  whrDet*Term (proj₁ , proj₂) (PE.subst (λ x₂ → _ ⊢ x₂ ↘ _ ∷ _)
                                    (whrDetTerm x₁ x) (proj₃ , proj₄))

whrDet* : ∀{Γ A B B′} (d : Γ ⊢ A ↘ B) (d′ : Γ ⊢ A ↘ B′) → B PE.≡ B′
whrDet* (id x , proj₂) (id x₁ , proj₄) = PE.refl
whrDet* (id x , proj₂) (x₁ ⇨ proj₃ , proj₄) = ⊥-elim (whnfRed x₁ proj₂)
whrDet* (x ⇨ proj₁ , proj₂) (id x₁ , proj₄) = ⊥-elim (whnfRed x proj₄)
whrDet* (A⇒A′ ⇨ A′⇒*B , whnfB) (A⇒A″ ⇨ A″⇒*B′ , whnfB′) =
  whrDet* (A′⇒*B , whnfB) (PE.subst (λ x → _ ⊢ x ↘ _)
                                     (whrDet A⇒A″ A⇒A′)
                                     (A″⇒*B′ , whnfB′))

-- Identity of syntactic reduction

idRed:*: : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A :⇒*: A
idRed:*: A = [ A , A , id A ]

idRedTerm:*: : ∀ {Γ A t} → Γ ⊢ t ∷ A → Γ ⊢ t :⇒*: t ∷ A
idRedTerm:*: t = [ t , t , id t ]

-- U cannot be a term

UnotInA : ∀ {A Γ} → Γ ⊢ U ∷ A → ⊥
UnotInA (conv U∷U x) = UnotInA U∷U

UnotInA[t] : ∀ {A B t a Γ}
         → t [ a ] PE.≡ U
         → Γ ⊢ a ∷ A
         → Γ ∙ A ⊢ t ∷ B
         → ⊥
UnotInA[t] () x₁ (ℕⱼ x₂)
UnotInA[t] () x₁ (Emptyⱼ x₂)
UnotInA[t] () x₁ (Πⱼ x₂ ▹ x₃)
UnotInA[t] x₁ x₂ (var x₃ here) rewrite x₁ = UnotInA x₂
UnotInA[t] () x₂ (var x₃ (there x₄))
UnotInA[t] () x₁ (lamⱼ x₂ x₃)
UnotInA[t] () x₁ (x₂ ∘ⱼ x₃)
UnotInA[t] () x₁ (zeroⱼ x₂)
UnotInA[t] () x₁ (sucⱼ x₂)
UnotInA[t] () x₁ (natrecⱼ x₂ x₃ x₄ x₅)
UnotInA[t] () x₁ (Emptyrecⱼ x₂ x₃)
UnotInA[t] x x₁ (conv x₂ x₃) = UnotInA[t] x x₁ x₂

redU*Term′ : ∀ {A B U′ Γ} → U′ PE.≡ U → Γ ⊢ A ⇒ U′ ∷ B → ⊥
redU*Term′ U′≡U (conv A⇒U x) = redU*Term′ U′≡U A⇒U
redU*Term′ () (app-subst A⇒U x)
redU*Term′ U′≡U (β-red x x₁ x₂) = UnotInA[t] U′≡U x₂ x₁
redU*Term′ () (natrec-subst x x₁ x₂ A⇒U)
redU*Term′ PE.refl (natrec-zero x x₁ x₂) = UnotInA x₁
redU*Term′ () (natrec-suc x x₁ x₂ x₃)
redU*Term′ () (Emptyrec-subst x A⇒U)
redU*Term′ PE.refl (Σ-β₁ F G x x₁) = UnotInA x
redU*Term′ PE.refl (Σ-β₂ F G x x₁) = UnotInA x₁

redU*Term : ∀ {A B Γ} → Γ ⊢ A ⇒* U ∷ B → ⊥
redU*Term (id x) = UnotInA x
redU*Term (x ⇨ A⇒*U) = redU*Term A⇒*U

-- Nothing reduces to U

redU : ∀ {A Γ} → Γ ⊢ A ⇒ U → ⊥
redU (univ x) = redU*Term′ PE.refl x

redU* : ∀ {A Γ} → Γ ⊢ A ⇒* U → A PE.≡ U
redU* (id x) = PE.refl
redU* (x ⇨ A⇒*U) rewrite redU* A⇒*U = ⊥-elim (redU x)


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

open import Fragment.Algebra.Signature
open import Relation.Binary using (Setoid)

module Fragment.Algebra.Free.Syntax {a ℓ}
  (Σ : Signature)
  (A : Setoid a ℓ)
  where

open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Free.Base Σ

open import Data.Fin using (Fin)
open import Data.Vec using ([]; _∷_)

module _ {n} where

  ⟨_⟩ : Fin n → ∥ Free (Atoms A n) ∥
  ⟨ n ⟩ = atom (dyn n)

  ⟨_⟩ₛ : Setoid.Carrier A → ∥ Free (Atoms A n) ∥
  ⟨ x ⟩ₛ = atom (sta x)

  ⟨_⟩₀ : ops Σ 0 → ∥ Free (Atoms A n) ∥
  ⟨ f ⟩₀ = term f []

  ⟨_⟩₁_ : ops Σ 1 → ∥ Free (Atoms A n) ∥ → ∥ Free (Atoms A n) ∥
  ⟨ f ⟩₁ t = term f (t ∷ [])

  _⟨_⟩₂_ : ∥ Free (Atoms A n) ∥
           → ops Σ 2
           → ∥ Free (Atoms A n) ∥
           → ∥ Free (Atoms A n) ∥
  s ⟨ f ⟩₂ t = term f (s ∷ t ∷ [])

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
-- Transport properties

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

module Constructive.Axiom.Properties.Transport where

-- agda-stdlib
open import Level renaming (suc to lsuc; zero to lzero)
open import Data.Sum as Sum
open import Data.Product as Prod
open import Relation.Binary.PropositionalEquality
open import Function.Base
import Function.LeftInverse as LInv -- TODO use new packages
import Function.Equality as Eq

-- agda-misc
open import Constructive.Common
open import Constructive.Combinators
open import Constructive.Axiom
open import Constructive.Axiom.Properties.Base

module Transport
  {a b p} {A : Set a} {B : Set b}
  (f : A → B) (g : B → A) (inv : ∀ x → f (g x) ≡ x)
  where
  private
    ∃Pf→∃P : {P : B → Set p} → ∃ (λ x → P (f x)) → ∃ P
    ∃Pf→∃P (x , Pfx) = (f x , Pfx)

    ∃P→∃Pf : {P : B → Set p} → ∃ P → ∃ (λ x → P (f x))
    ∃P→∃Pf {P = P} (x , Px) = g x , subst P (sym (inv x)) Px

    ∃Qg→∃Q : {Q : A → Set p} → ∃ (λ x → Q (g x)) → ∃ Q
    ∃Qg→∃Q (x , Qgx) = g x , Qgx

  lpo-transport : LPO A p → LPO B p
  lpo-transport lpo P? =
    Sum.map ∃Pf→∃P (contraposition ∃P→∃Pf) $ lpo (DecU-map f P?)

  llpo-transport : LLPO A p → LLPO B p
  llpo-transport llpo P? Q? w =
    Sum.map (contraposition ∃P→∃Pf) (contraposition ∃P→∃Pf) $
            llpo (DecU-map f P?) (DecU-map f Q?)
                 (contraposition (Prod.map ∃Pf→∃P ∃Pf→∃P) w)

  wlpo-Alt-transport : WLPO-Alt A p → WLPO-Alt B p
  wlpo-Alt-transport wlpo-Alt P? =
    Sum.map (contraposition ∃P→∃Pf) (DN-map ∃Pf→∃P) $ wlpo-Alt (DecU-map f P?)

  wlpo-transport : WLPO A p → WLPO B p
  wlpo-transport = wlpo-Alt⇒wlpo ∘′ wlpo-Alt-transport ∘′ wlpo⇒wlpo-Alt

  mr-transport : MR A p → MR B p
  mr-transport mr P? ¬¬∃P =
    ∃Pf→∃P $ mr (DecU-map f P?) (DN-map ∃P→∃Pf ¬¬∃P)

  mp-transport : MP A p → MP B p
  mp-transport = mr⇒mp ∘′ mr-transport ∘′ mp⇒mr

  wmp-transport : WMP A p → WMP B p
  wmp-transport wmp {P = P} P? hyp =
    ∃Pf→∃P $ wmp (DecU-map f P?)
    λ Q? → Sum.map (DN-map ∃Qg→∃Q) (DN-map λ {(x , Px , ¬Qgx) →
      g x , (subst P (sym (inv x)) Px) , ¬Qgx }) $ hyp (DecU-map g Q?)

  mp⊎-transport : MP⊎ A p → MP⊎ B p
  mp⊎-transport mp⊎ P? Q? w =
    Sum.map (DN-map ∃Pf→∃P) (DN-map ∃Pf→∃P) $
            mp⊎ (DecU-map f P?) (DecU-map f Q?)
                (contraposition (Prod.map (contraposition ∃P→∃Pf)
                                          (contraposition ∃P→∃Pf)) w)

open Transport public

module TransportByLeftInverse
  {a b p} {A : Set a} {B : Set b} (linv : B LInv.↞ A) =
  Transport {p = p} (LInv.LeftInverse.from linv Eq.⟨$⟩_)
    (LInv.LeftInverse.to linv Eq.⟨$⟩_) (LInv.LeftInverse.left-inverse-of linv)


text:
open import Preliminaries

module Idea where

  {- de Bruijn indices are representd as proofs that
     an element is in a list -}
  data _∈_ {A : Set} : (x : A) (l : List A) → Set where -- type \in
    i0 : {x : A} {xs : List A} → x ∈ x :: xs
    iS : {x y : A} {xs : List A} → x ∈ xs → x ∈ y :: xs

  {- types of the STLC -}
  data Tp : Set where
    b : Tp             -- uninterpreted base type
    _⇒_ : Tp → Tp → Tp -- type \=>

  {- contexts are lists of Tp's -}
  Ctx = List Tp
  _,,_ : Ctx → Tp → Ctx
  Γ ,, τ = τ :: Γ

  infixr 10 _⇒_
  infixr 9 _,,_
  infixr 8 _⊢_ -- type \entails
  infix 9 _⊇_

  data _⊢_ (Γ : Ctx) : Tp → Set
  data _≡_ {Γ : Ctx} : {τ : Tp} → Γ ⊢ τ → Γ ⊢ τ → Set
  _⊢c_ : Ctx → Ctx → Set
  _⊇_ : Ctx → Ctx → Set -- type \sup=
  ids : {Γ : Ctx} → Γ ⊢c Γ
  rename : {Γ Γ' : Ctx} {τ : Tp} → Γ' ⊇ Γ → Γ ⊢ τ → Γ' ⊢ τ
  subst : {Γ Γ' : Ctx}{τ : Tp} → Γ ⊢c Γ' → Γ' ⊢ τ  → Γ ⊢ τ
  _·ss_ : {Γ1 Γ2 Γ3 : Ctx} → Γ1 ⊢c Γ2 → Γ2 ⊢c Γ3 → Γ1 ⊢c Γ3
  subst1 : {Γ : Ctx} {τ τ0 : Tp} → Γ ⊢ τ0 → (Γ ,, τ0) ⊢ τ → Γ ⊢ τ

  {- Γ ⊢ τ represents a term of type τ in context Γ -}
  data _⊢_ (Γ : Ctx) where
    c   : Γ ⊢ b -- some constant of the base type
    v   : {τ : Tp}
        → τ ∈ Γ
        → Γ ⊢ τ
    lam : {τ1 τ2 : Tp}
        → Γ ,, τ1 ⊢ τ2
        → Γ ⊢ τ1 ⇒ τ2
    app : {τ1 τ2 : Tp}
        → Γ ⊢ τ1 ⇒ τ2
        → Γ ⊢ τ1
        → Γ ⊢ τ2
    foo : {A : Tp} (e1 e2 : Γ ⊢ A) → e1 ≡ e2 → Γ ⊢ A

{-foo : (e1 : ™ Gamma A) (e2 : ™ Gamma A) -> e1 \equiv e2 -> ™ Gamma A-}

  Γ' ⊇ [] = Unit
  Γ' ⊇ (τ :: Γ) = (Γ' ⊇ Γ) × (τ ∈ Γ')

  rename-var : {Γ Γ' : Ctx} {τ : Tp} → Γ' ⊇ Γ → τ ∈ Γ → τ ∈ Γ'
  rename-var (ρ , x') i0 = x'
  rename-var (ρ , _) (iS x) = rename-var ρ x

  p· : {Γ : Ctx} {Γ' : Ctx} → Γ ⊇ Γ' → {τ : Tp} → (Γ ,, τ) ⊇ Γ'
  p· {Γ' = []} ren = <>
  p· {Γ' = (τ :: Γ')} (ρ , x) = p· ρ , iS x

  idr : {Γ : Ctx} → Γ ⊇ Γ
  idr {[]} = <>
  idr {τ :: Γ} = p· idr , i0

  -- category with families notation
  p : {Γ : Ctx} {τ : Tp} → (Γ ,, τ ⊇ Γ)
  p = p· idr

  addvar-ren : {Γ Γ' : Ctx} {τ : Tp} → Γ' ⊇ Γ → Γ' ,, τ ⊇ Γ ,, τ
  addvar-ren ρ = (p· ρ , i0)

  data _≡_ {Γ : Ctx} where
    CongApp  : {τ1 τ2 : Tp} {e e' : Γ ⊢ τ1 ⇒ τ2} {e1 e1' : Γ ⊢ τ1}
           → e ≡ e' → e1 ≡ e1'
           → (app e e1) ≡ (app e' e1')
    CongLam : {τ1 τ2 : Tp} {e e' : (τ1 :: Γ) ⊢ τ2}
           → e ≡ e'
           → (lam e) ≡ (lam e')
    SubstId : ∀ {τ} {e : Γ ⊢ τ} → subst ids e ≡ e
    SubstComp : ∀ {Γ1 Γ2} {τ} {θ' : Γ ⊢c Γ2} {θ : Γ2 ⊢c Γ1} {e : Γ1 ⊢ τ} → subst θ' (subst θ e) ≡ subst (θ' ·ss θ) e
    Stepβ : {τ1 τ2 : Tp} {e : Γ ,, τ1 ⊢ τ2} {e1 : Γ ⊢ τ1}
           → (app (lam e) e1) ≡ subst1 e1 e
    Refl : {τ : Tp} {e : Γ ⊢ τ} → e ≡ e
    Trans : {τ : Tp} {e1 e2 e3 : Γ ⊢ τ}
         → e1 ≡ e2  →  e2 ≡ e3
         → e1 ≡ e3
    SubstCong : ∀ {Γ2} {τ} {Θ : Γ ⊢c Γ2} {e1 e2 : Γ2 ⊢ τ} → e1 ≡ e2 → subst Θ e1 ≡ subst Θ e2
    RenCong : ∀ {Γ2} {τ} {ρ : Γ ⊇ Γ2} {e1 e2 : Γ2 ⊢ τ} → e1 ≡ e2 → rename ρ e1 ≡ rename ρ e2

  rename ρ c = c
  rename ρ (v x) = v (rename-var ρ x)
  rename ρ (lam e) = lam (rename (addvar-ren ρ) e)
  rename ρ (app e e') = app (rename ρ e) (rename ρ e')
  rename ρ (foo e1 e2 p) = foo (rename ρ e1) (rename ρ e2) (RenCong p)

  _·rr_ : {Γ1 Γ2 Γ3 : Ctx} → Γ1 ⊇ Γ2 → Γ2 ⊇ Γ3 → Γ1 ⊇ Γ3
  _·rr_ {Γ1} {Γ2} {[]} ρ2 ρ3 = <>
  _·rr_ {Γ1} {Γ2} {x :: Γ3} ρ2 (ρ3 , x3) = (ρ2 ·rr ρ3) , rename-var ρ2 x3

  Γ' ⊢c [] = Unit
  Γ' ⊢c (τ :: Γ) = (Γ' ⊢c Γ) × (Γ' ⊢ τ)

  _·rs_ : {Γ1 Γ2 Γ3 : Ctx} →  Γ1 ⊇ Γ2 → Γ2 ⊢c Γ3 → Γ1 ⊢c Γ3
  _·rs_ {Γ1} {Γ2} {[]} ρ θ = <>
  _·rs_ {Γ1} {Γ2} {τ3 :: Γ3} ρ (θ , e) = ρ ·rs θ , rename ρ e

  addvar : {Γ Γ' : Ctx} {τ : Tp} → Γ ⊢c Γ' → (Γ ,, τ) ⊢c (Γ' ,, τ)
  addvar θ = p ·rs θ , v i0

  ids {[]} = <>
  ids {τ :: Γ} = p ·rs ids , v i0

  subst-var : {Γ Γ' : Ctx}{τ : Tp} → Γ ⊢c Γ' → τ ∈ Γ' → Γ ⊢ τ
  subst-var (θ , e) i0 = e
  subst-var (θ , _) (iS x) = subst-var θ x

  subst1 e0 e = subst (ids , e0) e

  -- composition of renamings and substitutions

  _·sr_ : {Γ1 Γ2 Γ3 : Ctx} →  Γ1 ⊢c Γ2 → Γ2 ⊇ Γ3 → Γ1 ⊢c Γ3
  _·sr_ {Γ1} {Γ2} {[]} θ ρ = <>
  _·sr_ {Γ1} {Γ2} {τ3 :: Γ3} θ (ρ , x) = _·sr_ θ ρ , subst-var θ x

  _·ss_ {Γ3 = []} θ1 θ2 = <>
  _·ss_ {Γ1} {Γ2} {τ :: Γ3} θ1 (θ2 , e2) = θ1 ·ss θ2 , subst θ1 e2

  subst θ c = c
  subst θ (v x) = subst-var θ x
  subst θ (lam e) = lam (subst (addvar θ) e)
  subst θ (app e e') = app (subst θ e) (subst θ e')
  subst {Γ} {Γ'} {τ} Θ (foo e1 e2 p) = foo (subst Θ e1) (subst Θ e2) (SubstCong p)

  postulate
    semfoo : (A : Set) (x y : A) -> x == y -> A

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

    ⟦_⟧t : Tp → Set
    ⟦_⟧c : Ctx → Set
    ⟦_⟧v : {Γ : Ctx} {τ : Tp} → τ ∈ Γ → ⟦ Γ ⟧c → ⟦ τ ⟧t
    ⟦_⟧ : {Γ : Ctx} {τ : Tp} → Γ ⊢ τ → ⟦ Γ ⟧c → ⟦ τ ⟧t
    sound : {Γ : Ctx} {τ : Tp} {e : Γ ⊢ τ} {e' : Γ ⊢ τ} → e ≡ e'
          → (γ : ⟦ Γ ⟧c) → ⟦ e ⟧ γ == ⟦ e' ⟧ γ

    ⟦ b ⟧t = B
    ⟦ τ1 ⇒ τ2 ⟧t = ⟦ τ1 ⟧t → ⟦ τ2 ⟧t

    ⟦ [] ⟧c = Unit
    ⟦ τ :: Γ ⟧c = ⟦ Γ ⟧c × ⟦ τ ⟧t

    ⟦_⟧v i0 γ = snd γ
    ⟦_⟧v (iS x) γ = ⟦ x ⟧v (fst γ)

    ⟦ c ⟧ γ = elB
    ⟦ v x ⟧ γ = ⟦ x ⟧v γ
    ⟦ lam e ⟧ γ = \ x → ⟦ e ⟧ (γ , x)
    ⟦ app e1 e2 ⟧ γ = ⟦ e1 ⟧ γ (⟦ e2 ⟧ γ)
    ⟦ (foo e1 e2 p) ⟧ γ = semfoo {!!} (⟦ e1 ⟧ γ) (⟦ e2 ⟧ γ) (sound {_} {_} {e1} {e2} p γ)

    ⟦_⟧s : {Γ Γ' : Ctx} → Γ ⊢c Γ' → ⟦ Γ ⟧c → ⟦ Γ' ⟧c
    ⟦_⟧s {Γ' = []} θ _ = <>
    ⟦_⟧s {Γ' = τ :: Γ'} (θ , e) γ = ⟦ θ ⟧s γ , ⟦ e ⟧ γ

    ⟦_⟧r : {Γ Γ' : Ctx} → Γ ⊇ Γ' → ⟦ Γ ⟧c → ⟦ Γ' ⟧c
    ⟦_⟧r {Γ' = []} θ _ = <>
    ⟦_⟧r {Γ' = τ :: Γ'} (θ , x) γ = ⟦ θ ⟧r γ , ⟦ x ⟧v γ

    interp-rename-var : {Γ' Γ : Ctx} {τ : Tp} (x : τ ∈ Γ) (θ : Γ' ⊇ Γ)
             → (γ' : ⟦ Γ' ⟧c) → ⟦ rename-var θ x ⟧v γ' == (⟦ x ⟧v (⟦ θ  ⟧r γ'))
    interp-rename-var i0 θ γ' = Refl
    interp-rename-var (iS x) θ γ' = interp-rename-var x (fst θ) γ'

    interp-subst-var : {Γ' Γ : Ctx} {τ : Tp} (x : τ ∈ Γ) (θ : Γ' ⊢c Γ)
             → (γ' : ⟦ Γ' ⟧c) → ⟦ subst-var θ x ⟧ γ' == (⟦ x ⟧v (⟦ θ  ⟧s γ'))
    interp-subst-var i0 θ γ' = Refl
    interp-subst-var (iS x) θ γ' = interp-subst-var x (fst θ) γ'

    interp-p· : {Γ : Ctx} {Γ' : Ctx} → (θ : Γ ⊇ Γ') → {τ : Tp} (γ' : _)
              → ⟦ p· θ {τ = τ} ⟧r γ' == ⟦ θ ⟧r (fst γ')
    interp-p· {Γ' = []} θ γ' = Refl
    interp-p· {Γ' = τ' :: Γ'} θ γ' = ap2 _,_ (interp-p· (fst θ) _) Refl

    interp-idr : {Γ : Ctx} (γ : _) → ⟦ idr {Γ} ⟧r γ == γ
    interp-idr {[]} γ = Refl
    interp-idr {x :: Γ} γ = ap (λ x₁ → x₁ , snd γ) (interp-idr (fst γ) ∘ interp-p· idr γ)

    interp-rename : {Γ' Γ : Ctx} {τ : Tp} (e : Γ ⊢ τ) (θ : Γ' ⊇ Γ)
          → (γ' : ⟦ Γ' ⟧c) → ⟦ rename θ e ⟧ γ' == (⟦ e ⟧ (⟦ θ  ⟧r γ'))
    interp-rename c θ γ' = Refl
    interp-rename (v x) θ γ' = interp-rename-var x θ γ'
    interp-rename (lam e) θ γ' = λ= (λ x → ap ⟦ e ⟧ (ap2 _,_ (interp-p· θ (γ' , x)) Refl) ∘ interp-rename e (addvar-ren θ) (γ' , x))
    interp-rename (app e e₁) θ γ' = ap2 (λ f x → f x) (interp-rename e θ γ') (interp-rename e₁ θ γ')
    interp-rename (foo e1 e2 p) Θ γ' = {!!} --interp-rename e1 Θ γ'

    interp-·rs : {Γ1 Γ2 Γ3 : Ctx} → (θ1 : Γ1 ⊇ Γ2) (θ2 : Γ2 ⊢c Γ3) (γ : _) → ⟦ θ1 ·rs θ2 ⟧s γ == ⟦ θ2 ⟧s (⟦ θ1 ⟧r γ)
    interp-·rs {Γ3 = []} θ1 θ2 γ = Refl
    interp-·rs {Γ3 = τ :: Γ3} θ1 (θ2 , e) γ = ap2 _,_ (interp-·rs θ1 θ2 γ) (interp-rename e θ1 γ)

    interp-subst : {Γ' Γ : Ctx} {τ : Tp} (e : Γ ⊢ τ) (θ : Γ' ⊢c Γ)
          → (γ' : ⟦ Γ' ⟧c) → ⟦ subst θ e ⟧ γ' == (⟦ e ⟧ (⟦ θ  ⟧s γ'))
    interp-subst c θ γ' = Refl
    interp-subst (v x) θ γ' = interp-subst-var x θ γ'
    interp-subst (lam e) θ γ' = λ= (λ x → ap (λ h → ⟦ e ⟧ (h , x)) (ap ⟦ θ ⟧s (interp-idr γ' ∘ interp-p· idr (γ' , x)) ∘ interp-·rs (p· idr) θ _) ∘ interp-subst e (addvar θ) (γ' , x))
    interp-subst (app e e₁) θ γ' = ap2 (λ f x → f x) (interp-subst e θ γ') (interp-subst e₁ θ γ')
    interp-subst (foo e1 e2 p) Θ γ' = {!!} --interp-subst e1 Θ γ'

    interp-·ss : {Γ1 Γ2 Γ3 : Ctx} → (θ1 : Γ1 ⊢c Γ2) (θ2 : Γ2 ⊢c Γ3) (γ : _) → ⟦ θ1 ·ss θ2 ⟧s γ == ⟦ θ2 ⟧s (⟦ θ1 ⟧s γ)
    interp-·ss {Γ3 = []} θ1 θ2 γ = Refl
    interp-·ss {Γ3 = τ :: Γ3} θ1 (θ2 , e) γ = ap2 _,_ (interp-·ss θ1 θ2 γ) (interp-subst e θ1 γ)

    interp-ids : ∀ {Γ} (γ : _) → ⟦ ids {Γ} ⟧s γ == γ
    interp-ids {[]} γ = Refl
    interp-ids {τ :: Γ} γ = ap (λ x → x , snd γ) (((interp-idr (fst γ) ∘ interp-p· idr γ) ∘ interp-ids (⟦ p ⟧r γ)) ∘ interp-·rs p ids γ)

    sound (CongApp D D') γ = ap2 (λ f x → f x) (sound D γ) (sound D' γ)
    sound (CongLam D) γ = λ= (λ x → sound D (γ , x))
    sound {e' = e'} SubstId γ = ap ⟦ e' ⟧ (interp-ids γ) ∘ interp-subst e' ids γ
    sound (SubstComp {θ' = θ'}{θ}{e = e}) γ = ((! (interp-subst e _ γ) ∘ ap ⟦ e ⟧ (! (interp-·ss θ' θ γ))) ∘ interp-subst e θ (⟦ θ' ⟧s γ)) ∘ interp-subst (subst θ e) θ' γ
    sound (Stepβ {e = e} {e1 = e1}) γ = ! (interp-subst e (ids , e1) γ) ∘ ap (λ x → ⟦ e ⟧ (x , ⟦ e1 ⟧ γ)) (! (interp-ids γ))
    sound Refl γ = Refl
    sound (Trans D D₁) γ = sound D₁ γ ∘ sound D γ
    sound {Γ'} (SubstCong {Γ} {τ} {Θ} {e1} {e2} D) γ = {!!} --(! (interp-subst e2 Θ γ) ∘ sound D (⟦ Θ ⟧s γ)) ∘ interp-subst e1 Θ γ
    sound {Γ'} (RenCong {Γ} {τ} {ρ} {e1} {e2} D) γ = {!!} --(! (interp-rename e2 ρ γ) ∘ sound D (⟦ ρ ⟧r γ)) ∘ interp-rename e1 ρ γ

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Reducibility {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Valid types are reducible.
reducibleᵛ : ∀ {A rA Γ l}
             ([Γ] : ⊩ᵛ Γ)
           → Γ ⊩ᵛ⟨ l ⟩ A ^ rA / [Γ]
           → Γ ⊩⟨ l ⟩ A ^ rA
reducibleᵛ [Γ] [A] =
  let ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevance′ (subst-id _) (proj₁ ([A] ⊢Γ [id]))

-- Valid type equality is reducible.
reducibleEqᵛ : ∀ {A B rA Γ l}
               ([Γ] : ⊩ᵛ Γ)
               ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ rA / [Γ])
             → Γ ⊩ᵛ⟨ l ⟩ A ≡ B ^ rA / [Γ] / [A]
             → Γ ⊩⟨ l ⟩ A ≡ B ^ rA / reducibleᵛ [Γ] [A]
reducibleEqᵛ {A = A} [Γ] [A] [A≡B] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceEq″ (subst-id _) (subst-id _) PE.refl PE.refl
                     (proj₁ ([A] ⊢Γ [id])) [σA] ([A≡B] ⊢Γ [id])

-- Valid terms are reducible.
reducibleTermᵛ : ∀ {t A rA Γ l}
                 ([Γ] : ⊩ᵛ Γ)
                 ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ rA / [Γ])
               → Γ ⊩ᵛ⟨ l ⟩ t ∷ A ^ rA / [Γ] / [A]
               → Γ ⊩⟨ l ⟩ t ∷ A ^ rA / reducibleᵛ [Γ] [A]
reducibleTermᵛ {A = A} [Γ] [A] [t] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceTerm″ (subst-id _) PE.refl PE.refl (subst-id _)
                        (proj₁ ([A] ⊢Γ [id])) [σA] (proj₁ ([t] ⊢Γ [id]))

-- Valid term equality is reducible.
reducibleEqTermᵛ : ∀ {t u A rA Γ l}
                   ([Γ] : ⊩ᵛ Γ)
                   ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ rA / [Γ])
                 → Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A ^ rA / [Γ] / [A]
                 → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ rA / reducibleᵛ [Γ] [A]
reducibleEqTermᵛ {A = A} [Γ] [A] [t≡u] =
  let [σA] = reducibleᵛ {A = A} [Γ] [A]
      ⊢Γ = soundContext [Γ]
      [id] = idSubstS [Γ]
  in  irrelevanceEqTerm″ PE.refl PE.refl (subst-id _) (subst-id _) (subst-id _)
                          (proj₁ ([A] ⊢Γ [id])) [σA] ([t≡u] ⊢Γ [id])

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

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

open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Consensus.Types
import      LibraBFT.ImplShared.Util.Crypto     as Crypto
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Types.Ledger2WaypointConverter where

new : LedgerInfo → Ledger2WaypointConverter
new ledgerInfo = mkLedger2WaypointConverter
  (ledgerInfo ^∙ liEpoch)
  (ledgerInfo ^∙ liTransactionAccumulatorHash)
  (ledgerInfo ^∙ liVersion)
--(ledgerInfo ^∙ liTimestamp)
  (ledgerInfo ^∙ liNextEpochState)


text:
module Sessions.Syntax.Expr where

open import Prelude

open import Sessions.Syntax.Types
open import Relation.Ternary.Separation.Construct.List Type

data Exp : Type → LCtx → Set where

  var       : ∀[ Just a ⇒ Exp a ]

  -- value constructors
  unit      : ε[ Exp unit ]
  letunit   : ∀[ Exp unit ✴ Exp a ⇒ Exp a ]

  -- linear function introduction and elimination
  lam       : ∀ a → ∀[ ((a ∷_) ⊢ Exp b) ⇒ Exp (a ⊸ b) ]
  ap        :       ∀[ Exp (a ⊸ b) ✴ Exp a ⇒ Exp b ]

  -- product introduction and elimination
  pairs     : ∀[ Exp a ✴ Exp b ⇒ Exp (prod a b) ]
  letpair   : ∀[ Exp (prod a b) ✴ (λ Γ → a ∷ b ∷ Γ) ⊢ Exp c ⇒ Exp c ]

  -- communication
  mkchan    : ∀ α → ε[ Exp (prod (cref α) (cref (α ⁻¹))) ]
  send      : ∀ {b} → ∀[ Exp a ✴ Exp (cref (a ! b)) ⇒ Exp (cref b) ]
  recv      : ∀ {b} → ∀[ Exp (cref (a ¿ b)) ⇒ Exp (prod (cref b) a) ]

  -- fork ; TODO unit
  fork      : ∀[ Exp (unit ⊸ unit) ⇒ Exp unit ]

  -- termination
  terminate : ∀[ Exp (cref end) ⇒ Exp unit ]


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Setoids.Setoids
open import Setoids.Subset

module Setoids.Intersection.Lemmas {a b : _} {A : Set a} (S : Setoid {a} {b} A) {c d : _} {pred1 : A → Set c} {pred2 : A → Set d} (s1 : subset S pred1) (s2 : subset S pred2) where

open import Setoids.Intersection.Definition S
open import Setoids.Equality S

intersectionCommutative : intersection s1 s2 =S intersection s2 s1
intersectionCommutative i = (λ t → _&&_.snd t ,, _&&_.fst t) ,, λ t → _&&_.snd t ,, _&&_.fst t

intersectionAssociative : {e : _} {pred3 : A → Set e} (s3 : subset S pred3) → intersection (intersection s1 s2) s3 =S intersection s1 (intersection s2 s3)
intersectionAssociative s3 x = (λ pr → _&&_.fst (_&&_.fst pr) ,, (_&&_.snd (_&&_.fst pr) ,, _&&_.snd pr)) ,, λ z → (_&&_.fst z ,, _&&_.fst (_&&_.snd z)) ,, _&&_.snd (_&&_.snd z)


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

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Paths

module lib.types.CommutingSquare where

{- maps between two functions -}

infix 0 _□$_
_□$_ = CommSquare.commutes

CommSquare-∘v : ∀ {i₀ i₁ i₂ j₀ j₁ j₂}
  {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂}
  {B₀ : Type j₀} {B₁ : Type j₁} {B₂ : Type j₂}
  {f₀ : A₀ → B₀} {f₁ : A₁ → B₁} {f₂ : A₂ → B₂}
  {hA : A₀ → A₁} {hB : B₀ → B₁}
  {kA : A₁ → A₂} {kB : B₁ → B₂}
  → CommSquare f₁ f₂ kA kB
  → CommSquare f₀ f₁ hA hB
  → CommSquare f₀ f₂ (kA ∘ hA) (kB ∘ hB)
CommSquare-∘v {hA = hA} {kB = kB} (comm-sqr □₁₂) (comm-sqr □₀₁) =
  comm-sqr λ a₀ → ap kB (□₀₁ a₀) ∙ □₁₂ (hA a₀)

CommSquare-inverse-v : ∀ {i₀ i₁ j₀ j₁}
  {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  {f₀ : A₀ → B₀} {f₁ : A₁ → B₁} {hA : A₀ → A₁} {hB : B₀ → B₁}
  → CommSquare f₀ f₁ hA hB → (hA-ise : is-equiv hA) (hB-ise : is-equiv hB)
  → CommSquare f₁ f₀ (is-equiv.g hA-ise) (is-equiv.g hB-ise)
CommSquare-inverse-v {f₀ = f₀} {f₁} {hA} {hB} (comm-sqr □) hA-ise hB-ise =
  comm-sqr λ a₁ → ap hB.g (! (□ (hA.g a₁) ∙ ap f₁ (hA.f-g a₁))) ∙ hB.g-f (f₀ (hA.g a₁))
  where module hA = is-equiv hA-ise
        module hB = is-equiv hB-ise

abstract
  -- 'r' with respect to '∘v'
  CommSquare-inverse-inv-r : ∀ {i₀ i₁ j₀ j₁}
    {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
    {f₀ : A₀ → B₀} {f₁ : A₁ → B₁} {hA : A₀ → A₁} {hB : B₀ → B₁}
    (cs : CommSquare f₀ f₁ hA hB) (hA-ise : is-equiv hA) (hB-ise : is-equiv hB)
    → ∀ a₁ → (CommSquare-∘v cs (CommSquare-inverse-v cs hA-ise hB-ise) □$ a₁)
          == is-equiv.f-g hB-ise (f₁ a₁) ∙ ! (ap f₁ (is-equiv.f-g hA-ise a₁))
  CommSquare-inverse-inv-r {f₀ = f₀} {f₁} {hA} {hB} (comm-sqr □) hA-ise hB-ise a₁ =
    ap hB ( ap hB.g (! (□ (hA.g a₁) ∙ ap f₁ (hA.f-g a₁)))
            ∙ hB.g-f (f₀ (hA.g a₁)))
    ∙ □ (hA.g a₁)
      =⟨ ap-∙ hB (ap hB.g (! (□ (hA.g a₁) ∙ ap f₁ (hA.f-g a₁)))) (hB.g-f (f₀ (hA.g a₁)))
          |in-ctx _∙ □ (hA.g a₁) ⟩
    ( ap hB (ap hB.g (! (□ (hA.g a₁) ∙ ap f₁ (hA.f-g a₁))))
      ∙ ap hB (hB.g-f (f₀ (hA.g a₁))))
    ∙ □ (hA.g a₁)
      =⟨ ap2 _∙_
          (∘-ap hB hB.g (! (□ (hA.g a₁) ∙ ap f₁ (hA.f-g a₁))))
          (hB.adj (f₀ (hA.g a₁)))
          |in-ctx _∙ □ (hA.g a₁) ⟩
    ( ap (hB ∘ hB.g) (! (□ (hA.g a₁) ∙ ap f₁ (hA.f-g a₁)))
      ∙ hB.f-g (hB (f₀ (hA.g a₁))))
    ∙ □ (hA.g a₁)
      =⟨ ! (↓-app=idf-out $ apd hB.f-g (! (□ (hA.g a₁) ∙ ap f₁ (hA.f-g a₁))))
          |in-ctx _∙ □ (hA.g a₁) ⟩
    ( hB.f-g (f₁ a₁)
      ∙' (! (□ (hA.g a₁) ∙ ap f₁ (hA.f-g a₁))))
    ∙ □ (hA.g a₁)
      =⟨ lemma (hB.f-g (f₁ a₁)) (□ (hA.g a₁)) (ap f₁ (hA.f-g a₁)) ⟩
    hB.f-g (f₁ a₁) ∙ ! (ap f₁ (hA.f-g a₁))
      =∎
    where module hA = is-equiv hA-ise
          module hB = is-equiv hB-ise

          lemma : ∀ {i} {A : Type i} {a₀ a₁ a₂ a₃ : A}
            (p₀ : a₀ == a₁) (p₁ : a₃ == a₂) (p₂ : a₂ == a₁)
            → (p₀ ∙' (! (p₁ ∙ p₂))) ∙ p₁ == p₀ ∙ ! p₂
          lemma idp idp idp = idp

  -- 'l' with respect to '∘v'
  CommSquare-inverse-inv-l : ∀ {i₀ i₁ j₀ j₁}
    {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
    {f₀ : A₀ → B₀} {f₁ : A₁ → B₁} {hA : A₀ → A₁} {hB : B₀ → B₁}
    (cs : CommSquare f₀ f₁ hA hB) (hA-ise : is-equiv hA) (hB-ise : is-equiv hB)
    → ∀ a₀ → (CommSquare-∘v (CommSquare-inverse-v cs hA-ise hB-ise) cs □$ a₀)
          == is-equiv.g-f hB-ise (f₀ a₀) ∙ ! (ap f₀ (is-equiv.g-f hA-ise a₀))
  CommSquare-inverse-inv-l {f₀ = f₀} {f₁} {hA} {hB} (comm-sqr □) hA-ise hB-ise a₀ =
    ap hB.g (□ a₀)
    ∙ ( ap hB.g (! (□ (hA.g (hA a₀)) ∙ ap f₁ (hA.f-g (hA a₀))))
        ∙ hB.g-f (f₀ (hA.g (hA a₀))))
      =⟨ ! (hA.adj a₀) |in-ctx ap f₁
          |in-ctx □ (hA.g (hA a₀)) ∙_
          |in-ctx ! |in-ctx ap hB.g
          |in-ctx _∙ hB.g-f (f₀ (hA.g (hA a₀)))
          |in-ctx ap hB.g (□ a₀) ∙_ ⟩
    ap hB.g (□ a₀)
    ∙ ( ap hB.g (! (□ (hA.g (hA a₀)) ∙ ap f₁ (ap hA (hA.g-f a₀))))
        ∙ hB.g-f (f₀ (hA.g (hA a₀))))
      =⟨ ∘-ap f₁ hA (hA.g-f a₀)
          |in-ctx □ (hA.g (hA a₀)) ∙_
          |in-ctx ! |in-ctx ap hB.g
          |in-ctx _∙ hB.g-f (f₀ (hA.g (hA a₀)))
          |in-ctx ap hB.g (□ a₀) ∙_ ⟩
    ap hB.g (□ a₀)
    ∙ ( ap hB.g (! (□ (hA.g (hA a₀)) ∙ ap (f₁ ∘ hA) (hA.g-f a₀)))
        ∙ hB.g-f (f₀ (hA.g (hA a₀))))
      =⟨ ↓-='-out' (apd □ (hA.g-f a₀))
          |in-ctx ! |in-ctx ap hB.g
          |in-ctx _∙ hB.g-f (f₀ (hA.g (hA a₀)))
          |in-ctx ap hB.g (□ a₀) ∙_ ⟩
    ap hB.g (□ a₀)
    ∙ ( ap hB.g (! (ap (hB ∘ f₀) (hA.g-f a₀) ∙' □ a₀))
        ∙ hB.g-f (f₀ (hA.g (hA a₀))))
      =⟨ lemma hB.g (□ a₀) (ap (hB ∘ f₀) (hA.g-f a₀)) (hB.g-f (f₀ (hA.g (hA a₀)))) ⟩
    ! (ap hB.g (ap (hB ∘ f₀) (hA.g-f a₀)))
    ∙' hB.g-f (f₀ (hA.g (hA a₀)))
      =⟨ ∘-ap hB.g (hB ∘ f₀) (hA.g-f a₀)
          |in-ctx ! |in-ctx _∙' hB.g-f (f₀ (hA.g (hA a₀))) ⟩
    ! (ap (hB.g ∘ hB ∘ f₀) (hA.g-f a₀))
    ∙' hB.g-f (f₀ (hA.g (hA a₀)))
      =⟨ !-ap (hB.g ∘ hB ∘ f₀) (hA.g-f a₀)
          |in-ctx _∙' hB.g-f (f₀ (hA.g (hA a₀))) ⟩
    ap (hB.g ∘ hB ∘ f₀) (! (hA.g-f a₀))
    ∙' hB.g-f (f₀ (hA.g (hA a₀)))
      =⟨ ! (↓-='-out' (apd (hB.g-f ∘ f₀) (! (hA.g-f a₀)))) ⟩
    hB.g-f (f₀ a₀) ∙ ap f₀ (! (hA.g-f a₀))
      =⟨ ap-! f₀ (hA.g-f a₀) |in-ctx hB.g-f (f₀ a₀) ∙_ ⟩
    hB.g-f (f₀ a₀) ∙ ! (ap f₀ (hA.g-f a₀))
      =∎
    where module hA = is-equiv hA-ise
          module hB = is-equiv hB-ise

          lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
            {a₀ a₁ a₂ : A} {b : B}
            (p₀ : a₀ == a₁) (p₁ : a₂ == a₀) (q₀ : f a₂ == b)
            → ap f p₀ ∙ (ap f (! (p₁ ∙' p₀)) ∙ q₀) == ! (ap f p₁) ∙' q₀
          lemma f idp idp idp = idp

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- This is an example emphasizing the important of a linearity check
-- in the positivity check.
--
-- Currently it does not type check since there is no universe subtyping.

module PositivityCheckNeedsLinearityCheck where

data Eq (S : Set2) : Set2 -> Set where
  refl : Eq S S

subst' : {S S' : Set2} -> Eq S S' -> S -> S'
subst' refl s = s

-- what happens if Eq is considered covariant in its first argument?
-- then because of subtyping,

p : Eq Set1 Set
p = refl

S : Set
S = subst' p Set

-- now S, which evaluates to Set, is in Set

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Cubical.HCompU where

open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
                                             primHComp to hcomp; primTransp to transp; primComp to comp;
                                             itIsOne to 1=1)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to outS; inc to inS)

module Helpers where
    -- Homogeneous filling
    hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
              (u : ∀ i → Partial φ A)
              (u0 : A [ φ ↦ u i0 ]) (i : I) → A
    hfill {φ = φ} u u0 i =
      hcomp (λ j → \ { (φ = i1) → u (i ∧ j) 1=1
                     ; (i = i0) → outS u0 })
            (outS u0)

    -- Heterogeneous filling defined using comp
    fill : ∀ {ℓ : I → Level} (A : ∀ i → Set (ℓ i)) {φ : I}
             (u : ∀ i → Partial φ (A i))
             (u0 : A i0 [ φ ↦ u i0 ]) →
             ∀ i →  A i
    fill A {φ = φ} u u0 i =
      comp (λ j → A (i ∧ j))
           (λ j → \ { (φ = i1) → u (i ∧ j) 1=1
                    ; (i = i0) → outS u0 })
           (outS {φ = φ} u0)

    module _ {ℓ} {A : Set ℓ} where
      refl : {x : A} → x ≡ x
      refl {x = x} = λ _ → x

      sym : {x y : A} → x ≡ y → y ≡ x
      sym p = λ i → p (~ i)

      cong : ∀ {ℓ'} {B : A → Set ℓ'} {x y : A}
             (f : (a : A) → B a) (p : x ≡ y)
           → PathP (λ i → B (p i)) (f x) (f y)
      cong f p = λ i → f (p i)

    isContr : ∀ {ℓ} → Set ℓ → Set ℓ
    isContr A = Σ A \ x → (∀ y → x ≡ y)

    fiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ ⊔ ℓ')
    fiber {A = A} f y = Σ A \ x → f x ≡ y

open Helpers

primitive
  prim^glueU : {la : Level} {φ : I} {T : I → Partial φ (Set la)}
                 {A : Set la [ φ ↦ T i0 ]} →
                 PartialP φ (T i1) → outS A → hcomp T (outS A)
  prim^unglueU : {la : Level} {φ : I} {T : I → Partial φ (Set la)}
                   {A : Set la [ φ ↦ T i0 ]} →
                   hcomp T (outS A) → outS A
  -- Needed for transp.
  primFaceForall : (I → I) → I

transpProof : ∀ {l} → (e : I → Set l) → (φ : I) → (a : Partial φ (e i0)) → (b : e i1 [ φ ↦ (\ o → transp (\ i → e i) i0 (a o)) ] ) → fiber (transp (\ i → e i) i0) (outS b)
transpProof e φ a b = f , \ j → comp (\ i → e i) (\ i →
                                               \ { (φ = i1) → transp (\ j → e (j ∧ i)) (~ i) (a 1=1)
                                                 ; (j = i0) → transp (\ j → e (j ∧ i)) (~ i) f
                                                 ; (j = i1) → g (~ i) })
                                        f
    where
      b' = outS {u = (\ o → transp (\ i → e i) i0 (a o))} b
      g : (k : I) → e (~ k)
      g k = fill (\ i → e (~ i)) (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ ~ i)) i (a 1=1)
                                          ; (φ = i0) → transp (\ j → e (~ j ∨ ~ i)) (~ i) b' }) (inS b') k
      f = comp (\ i → e (~ i)) (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ ~ i)) i (a 1=1); (φ = i0) → transp (\ j → e (~ j ∨ ~ i)) (~ i) b' }) b'

{-# BUILTIN TRANSPPROOF transpProof #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Invert where

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

open import Data.Nat.Properties

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x = g (f x)

pred₂ : ℕ → ℕ
pred₂ = pred ∘ pred

lemma : (a b : ℕ) → pred₂ (suc a + suc a) ≡ pred₂ (suc b + suc b)
        → a + a ≡ b + b
lemma a b p =
  begin
  a + a ≡⟨⟩
  pred₂ (suc (suc (a + a))) ≡⟨⟩
  pred₂ (suc (suc a + a)) ≡⟨ cong (pred₂ ∘ suc) (+-comm (suc a) a)  ⟩
  pred₂ (suc (a + suc a)) ≡⟨⟩
  pred₂ (suc a + suc a) ≡⟨ p ⟩
  pred₂ (suc b + suc b) ≡⟨⟩
  pred₂ (suc (b + suc b)) ≡⟨ cong (pred₂ ∘ suc) (+-comm b (suc b)) ⟩
  pred₂ (suc (suc b + b)) ≡⟨⟩
  b + b
  ∎ where open ≡-Reasoning

invert : (a b : ℕ) → a + a ≡ b + b → a ≡ b
invert zero zero p = refl
invert (suc m) (suc n) p = cong suc (invert m n (lemma m n (cong pred₂ p)))

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
module _ where

postulate D : Set

module A where

  infixr 5 _∷_

  postulate
    _∷_ : Set₁ → D → D

module B where

  infix 5 _∷_

  postulate
    _∷_ : Set₁ → Set₁ → D

open A
open B

foo : D
foo = Set ∷ Set

-- Expected error:
--
-- <preciseErrorLocation>
-- Ambiguous name _∷_. It could refer to any one of
--   A._∷_ bound at ...
--   B._∷_ bound at ...


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Tables, basic types and operations
------------------------------------------------------------------------

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

module Data.Table.Base where

open import Data.Nat
open import Data.Fin
open import Data.Product using (_×_ ; _,_)
open import Data.List as List using (List)
open import Data.Vec as Vec using (Vec)
open import Function using (_∘_; flip)

------------------------------------------------------------------------
-- Type

record Table {a} (A : Set a) n : Set a where
  constructor tabulate
  field lookup : Fin n → A
open Table public

------------------------------------------------------------------------
-- Basic operations

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

  head : ∀ {n} → Table A (suc n) → A
  head t = lookup t zero

  tail : ∀ {n} → Table A (suc n) → Table A n
  tail t = tabulate (lookup t ∘ suc)

  uncons : ∀ {n} → Table A (suc n) → A × Table A n
  uncons t = head t , tail t

  remove : ∀ {n} → Fin (suc n) → Table A (suc n) → Table A n
  remove i t = tabulate (lookup t ∘ punchIn i)

------------------------------------------------------------------------
-- Operations for transforming tables

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

  rearrange : ∀ {m n} → (Fin m → Fin n) → Table A n → Table A m
  rearrange f t = tabulate (lookup t ∘ f)

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

  map : ∀ {n} → (A → B) → Table A n → Table B n
  map f t = tabulate (f ∘ lookup t)

  _⊛_ : ∀ {n} → Table (A → B) n → Table A n → Table B n
  fs ⊛ xs = tabulate λ i → lookup fs i (lookup xs i)

------------------------------------------------------------------------
-- Operations for reducing tables

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

  foldr : ∀ {n} → (A → B → B) → B → Table A n → B
  foldr {n = zero}  f z t = z
  foldr {n = suc n} f z t = f (head t) (foldr f z (tail t))

  foldl : ∀ {n} → (B → A → B) → B → Table A n → B
  foldl {n = zero}  f z t = z
  foldl {n = suc n} f z t = foldl f (f z (head t)) (tail t)

------------------------------------------------------------------------
-- Operations for building tables

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

  replicate : ∀ {n} → A → Table A n
  replicate x = tabulate (λ _ → x)

------------------------------------------------------------------------
-- Operations for converting tables

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

  toList : ∀ {n} → Table A n → List A
  toList = List.tabulate ∘ lookup

  fromList : ∀ (xs : List A) → Table A (List.length xs)
  fromList = tabulate ∘ List.lookup

  fromVec : ∀ {n} → Vec A n → Table A n
  fromVec = tabulate ∘ Vec.lookup

  toVec : ∀ {n} → Table A n → Vec A n
  toVec = Vec.tabulate ∘ lookup


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

open import Categories.Category using () renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal

module Categories.Enriched.NaturalTransformation
  {o ℓ e} {V : Setoid-Category o ℓ e} (M : Monoidal V) where

open import Level

open import Categories.Category.Monoidal.Properties M using (module Kelly's)
open import Categories.Category.Monoidal.Reasoning M
open import Categories.Category.Monoidal.Utilities M
open import Categories.Enriched.Category M
open import Categories.Enriched.Functor M renaming (id to idF)
open import Categories.Morphism.Reasoning V
import Categories.Morphism.IsoEquiv V as IsoEquiv
open import Categories.NaturalTransformation using (ntHelper)
  renaming (NaturalTransformation to Setoid-NT)

open Setoid-Category V renaming (Obj to ObjV; id to idV)
open Commutation
open Monoidal M
open Shorthands

module _ {c d} {C : Category c} {D : Category d} where

  private
    module C = Category C
    module D = Category D
    module U = Underlying D

  record NaturalTransformation (F G : Functor C D) : Set (ℓ ⊔ e ⊔ c) where
    eta-equality
    private
      module F = Functor F
      module G = Functor G

    field
      comp    : ∀ X → F.₀ X U.⇒ G.₀ X
      commute : ∀ {X Y} →
        [ C [ X , Y ] ⇒ D [ F.₀ X , G.₀ Y ] ]⟨
          unitorˡ.to      ⇒⟨ unit ⊗₀ C [ X , Y ] ⟩
          comp Y ⊗₁ F.₁   ⇒⟨ D [ F.₀ Y , G.₀ Y ] ⊗₀ D [ F.₀ X , F.₀ Y ] ⟩
          D.⊚
        ≈ unitorʳ.to      ⇒⟨ C [ X , Y ] ⊗₀ unit ⟩
          G.₁ ⊗₁ comp X   ⇒⟨ D [ G.₀ X , G.₀ Y ] ⊗₀ D [ F.₀ X , G.₀ X ] ⟩
          D.⊚
        ⟩

    -- A shorthand for the components of a natural transformation:
    --
    --   α [ X ]
    --
    -- is the X-component of the family { αₓ } of "morphisms" that
    -- forms the natural transformation α.

    infixl 16 _[_]

    _[_] = comp

  open NaturalTransformation
  open D hiding (id)
  open IsoEquiv._≃_

  id : ∀ {F : Functor C D} → NaturalTransformation F F
  id {F} = record
    { comp    = λ _ → D.id
    ; commute = λ {X} {Y} → begin
      ⊚ ∘ D.id ⊗₁ F.₁ ∘ λ⇐                ≈⟨ refl⟩∘⟨ pushˡ serialize₁₂ ⟩
      ⊚ ∘ D.id ⊗₁ idV ∘ idV ⊗₁ F.₁ ∘ λ⇐   ≈⟨ pullˡ unitˡ ⟩
      unitorˡ.from ∘ idV ⊗₁ F.₁ ∘ λ⇐      ≈⟨ pullˡ unitorˡ-commute-from ⟩
      (F.₁ ∘ unitorˡ.from) ∘ λ⇐           ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
      F.₁                                 ≈˘⟨ cancelʳ unitorʳ.isoʳ ⟩
      (F.₁ ∘ unitorʳ.from) ∘ ρ⇐           ≈˘⟨ pullˡ unitorʳ-commute-from ⟩
      unitorʳ.from ∘ F.₁ ⊗₁ idV ∘ ρ⇐      ≈˘⟨ pullˡ unitʳ ⟩
      ⊚ ∘ idV ⊗₁ D.id ∘ F.₁ ⊗₁ idV ∘ ρ⇐   ≈˘⟨ refl⟩∘⟨ pushˡ serialize₂₁ ⟩
      ⊚ ∘ F.₁ ⊗₁ D.id ∘ ρ⇐                ∎
    }
    where module F = Functor F

  infixr 9 _∘ᵥ_

  -- Vertical composition

  _∘ᵥ_ : {F G H : Functor C D} →
         NaturalTransformation G H → NaturalTransformation F G →
         NaturalTransformation F H
  _∘ᵥ_ {F} {G} {H} α β = record
    { comp    = λ X → α [ X ] U.∘ β [ X ]
    ; commute = λ {X} {Y} →
      begin
        ⊚ ∘ (⊚ ∘ α [ Y ] ⊗₁ β [ Y ] ∘ λ⇐) ⊗₁ F.₁ ∘ λ⇐
      ≈⟨ helper (α [ Y ]) (β [ Y ]) F.₁ λ⇐ ⟩
        ⊚ ∘ α [ Y ] ⊗₁ (⊚ ∘ β [ Y ] ⊗₁ F.₁ ∘ λ⇐) ∘ λ⇐
      ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ commute β ⟩∘⟨refl ⟩
        ⊚ ∘ α [ Y ] ⊗₁ (⊚ ∘ G.₁ ⊗₁ β [ X ] ∘ ρ⇐) ∘ λ⇐
      ≈˘⟨ helper (α [ Y ]) G.₁ (β [ X ]) ρ⇐ ⟩
        ⊚ ∘ (⊚ ∘ α [ Y ] ⊗₁ G.₁ ∘ λ⇐) ⊗₁ β [ X ] ∘ ρ⇐
      ≈⟨ refl⟩∘⟨ commute α ⟩⊗⟨refl ⟩∘⟨refl ⟩
        ⊚ ∘ (⊚ ∘ H.₁ ⊗₁ α [ X ] ∘ ρ⇐) ⊗₁ β [ X ] ∘ ρ⇐
      ≈˘⟨ refl⟩∘⟨ assoc ⟩⊗⟨refl ⟩∘⟨refl ⟩
        ⊚ ∘ ((⊚ ∘ H.₁ ⊗₁ α [ X ]) ∘ ρ⇐) ⊗₁ β [ X ] ∘ ρ⇐
      ≈⟨ refl⟩∘⟨ split₁ʳ ⟩∘⟨refl ⟩
        ⊚ ∘ ((⊚ ∘ H.₁ ⊗₁ α [ X ]) ⊗₁ β [ X ] ∘ ρ⇐ ⊗₁ idV) ∘ ρ⇐
      ≈⟨ pullˡ (pullˡ ⊚-assoc-var) ⟩
        ((⊚ ∘ H.₁ ⊗₁ (⊚ ∘ α [ X ] ⊗₁ β [ X ]) ∘ α⇒) ∘ ρ⇐ ⊗₁ idV) ∘ ρ⇐
      ≈˘⟨ pushʳ (pushʳ (switch-tofromˡ associator (to-≈ triangle-iso))) ⟩∘⟨refl ⟩
        (⊚ ∘ H.₁ ⊗₁ (⊚ ∘ α [ X ] ⊗₁ β [ X ]) ∘ idV ⊗₁ λ⇐) ∘ ρ⇐
      ≈˘⟨ pushʳ (split₂ʳ ⟩∘⟨refl) ⟩
        ⊚ ∘ H.₁ ⊗₁ ((⊚ ∘ α [ X ] ⊗₁ β [ X ]) ∘ λ⇐) ∘ ρ⇐
      ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟩
        ⊚ ∘ H.₁ ⊗₁ (⊚ ∘ α [ X ] ⊗₁ β [ X ] ∘ λ⇐) ∘ ρ⇐
      ∎
    }
    where
      module F = Functor F
      module G = Functor G
      module H = Functor H

      helper : ∀ {X₁ X₂ X₃ X₄ Y₁ Y₂ Z} (f : X₃ U.⇒ X₄) (g : Y₁ ⇒ D [ X₂ , X₃ ])
                 (h : Y₂ ⇒ D [ X₁ , X₂ ]) (i : Z ⇒ Y₁ ⊗₀ Y₂) →
               ⊚ ∘ (⊚ ∘ f ⊗₁ g ∘ λ⇐) ⊗₁ h ∘ i  ≈
               ⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h ∘ i) ∘ λ⇐
      helper f g h i = begin
          ⊚ ∘ (⊚ ∘ f ⊗₁ g ∘ λ⇐) ⊗₁ h ∘ i
        ≈˘⟨ refl⟩∘⟨ assoc ⟩⊗⟨refl ⟩∘⟨refl ⟩
          ⊚ ∘ ((⊚ ∘ f ⊗₁ g) ∘ λ⇐) ⊗₁ h ∘ i
        ≈⟨ refl⟩∘⟨ split₁ʳ ⟩∘⟨refl ⟩
          ⊚ ∘ ((⊚ ∘ f ⊗₁ g) ⊗₁ h ∘ λ⇐ ⊗₁ idV) ∘ i
        ≈⟨ pullˡ (pullˡ ⊚-assoc-var) ⟩
          ((⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h) ∘ α⇒) ∘ λ⇐ ⊗₁ idV) ∘ i
        ≈˘⟨ pushʳ (pushʳ (switch-tofromˡ associator (to-≈ Kelly's.coherence-iso₁))) ⟩∘⟨refl ⟩
          (⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h) ∘ λ⇐) ∘ i
        ≈⟨ pullʳ (pullʳ unitorˡ-commute-to) ⟩
          ⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h) ∘ idV ⊗₁ i ∘ λ⇐
        ≈˘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
          ⊚ ∘ f ⊗₁ ((⊚ ∘ g ⊗₁ h) ∘ i) ∘ λ⇐
        ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟩
          ⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h ∘ i) ∘ λ⇐
        ∎

  -- A V-enriched natural transformation induces an ordinary natural
  -- transformation on the underlying functors.

  UnderlyingNT : {F G : Functor C D} → NaturalTransformation F G →
                 Setoid-NT (UnderlyingFunctor F) (UnderlyingFunctor G)
  UnderlyingNT {F} {G} α = ntHelper (record
    { η       = comp α
    ; commute = λ {X Y} f →
      begin
        ⊚ ∘ α [ Y ] ⊗₁ (F.₁ ∘ f) ∘ λ⇐          ≈⟨ refl⟩∘⟨ split₂ʳ ⟩∘⟨refl ⟩
        ⊚ ∘ (α [ Y ] ⊗₁ F.₁ ∘ idV ⊗₁ f) ∘ λ⇐   ≈˘⟨ refl⟩∘⟨ extendˡ unitorˡ-commute-to ⟩
        ⊚ ∘ (α [ Y ] ⊗₁ F.₁ ∘ λ⇐) ∘ f          ≈⟨ extendʳ (commute α) ⟩
        ⊚ ∘ (G.₁ ⊗₁ α [ X ] ∘ ρ⇐) ∘ f          ≈⟨ refl⟩∘⟨ extendˡ unitorʳ-commute-to ⟩
        ⊚ ∘ (G.₁ ⊗₁ α [ X ] ∘ f ⊗₁ idV) ∘ ρ⇐   ≈˘⟨ refl⟩∘⟨ split₁ʳ ⟩∘⟨refl ⟩
        ⊚ ∘ (G.₁ ∘ f) ⊗₁ α [ X ] ∘ ρ⇐          ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ to-≈ Kelly's.coherence-iso₃ ⟩
        ⊚ ∘ (G.₁ ∘ f) ⊗₁ α [ X ] ∘ λ⇐          ∎
    })
    where
      module F = Functor F
      module G = Functor G

  module UnderlyingNT {F} {G} α = Setoid-NT (UnderlyingNT {F} {G} α)

module _ {c d e} {C : Category c} {D : Category d} {E : Category e} where

  private
    module C = Category C
    module D = Category D
    module E = Category E
    module U = Underlying E
  open NaturalTransformation

  infixr 9 _∘ₕ_ _∘ˡ_ _∘ʳ_

  -- Left- and right-hand composition with a functor

  _∘ˡ_ : {G H : Functor C D} (F : Functor D E) →
         NaturalTransformation G H → NaturalTransformation (F ∘F G) (F ∘F H)
  _∘ˡ_ {G} {H} F α = record
    { comp    = λ X → F.₁ ∘ α [ X ]
    ; commute = λ {X Y} →
      begin
        E.⊚ ∘ (F.₁ ∘ α [ Y ]) ⊗₁ (F.₁ ∘ G.₁) ∘ λ⇐    ≈⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟩
        E.⊚ ∘ (F.₁ ⊗₁ F.₁) ∘ (α [ Y ] ⊗₁ G.₁) ∘ λ⇐   ≈˘⟨ extendʳ F.homomorphism ⟩
        F.₁ ∘ D.⊚ ∘ (α [ Y ] ⊗₁ G.₁) ∘ λ⇐            ≈⟨ refl⟩∘⟨ commute α ⟩
        F.₁ ∘ D.⊚ ∘ (H.₁ ⊗₁ α [ X ]) ∘ ρ⇐            ≈⟨ extendʳ F.homomorphism ⟩
        E.⊚ ∘ (F.₁ ⊗₁ F.₁) ∘ (H.₁ ⊗₁ α [ X ]) ∘ ρ⇐   ≈˘⟨ refl⟩∘⟨ pushˡ ⊗-distrib-over-∘ ⟩
        E.⊚ ∘ (F.₁ ∘ H.₁) ⊗₁ (F.₁ ∘ α [ X ]) ∘ ρ⇐    ∎
    }
    where
      module F = Functor F
      module G = Functor G
      module H = Functor H

  _∘ʳ_ : {G H : Functor D E} →
         NaturalTransformation G H → (F : Functor C D) →
         NaturalTransformation (G ∘F F) (H ∘F F)
  _∘ʳ_ {G} {H} α F = record
    { comp    = λ X → α [ F.₀ X ]
    ; commute = λ {X Y} →
      begin
        E.⊚ ∘ α [ F.₀ Y ] ⊗₁ (G.₁ ∘ F.₁) ∘ λ⇐          ≈⟨ refl⟩∘⟨ split₂ʳ ⟩∘⟨refl ⟩
        E.⊚ ∘ (α [ F.₀ Y ] ⊗₁ G.₁ ∘ idV ⊗₁ F.₁) ∘ λ⇐   ≈˘⟨ refl⟩∘⟨ extendˡ unitorˡ-commute-to ⟩
        E.⊚ ∘ (α [ F.₀ Y ] ⊗₁ G.₁ ∘ λ⇐) ∘ F.₁          ≈⟨ extendʳ (commute α) ⟩
        E.⊚ ∘ (H.₁ ⊗₁ α [ F.₀ X ] ∘ ρ⇐) ∘ F.₁          ≈⟨ refl⟩∘⟨ extendˡ unitorʳ-commute-to ⟩
        E.⊚ ∘ (H.₁ ⊗₁ α [ F.₀ X ] ∘ F.₁ ⊗₁ idV) ∘ ρ⇐   ≈˘⟨ refl⟩∘⟨ split₁ʳ ⟩∘⟨refl ⟩
        E.⊚ ∘ (H.₁ ∘ F.₁) ⊗₁ α [ F.₀ X ] ∘ ρ⇐          ∎
    }
    where
      module F = Functor F
      module G = Functor G
      module H = Functor H

  -- Horizontal composition

  _∘ₕ_ : {H I : Functor D E} {F G : Functor C D} →
          NaturalTransformation H I → NaturalTransformation F G →
          NaturalTransformation (H ∘F F) (I ∘F G)
  _∘ₕ_ {_} {I} {F} {_} α β = (I ∘ˡ β) ∘ᵥ (α ∘ʳ F)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- This file tests that implicit record fields are not printed out (by
-- default).

-- Andreas, 2016-07-20 Repaired this long disfunctional test case.

module ImplicitRecordFields where

record R : Set₁ where
  field
    {A}         : Set
    f           : A → A
    {B C} D {E} : Set
    g           : B → C → E

postulate
  A : Set
  r : R

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

foo : r ≡ record
  { A = A
  ; f = λ x → x
  ; B = A
  ; C = A
  ; D = A
  ; g = λ x _ → x
  }
foo = refl

-- EXPECTED ERROR:
-- .R.A r != A of type Set
-- when checking that the expression refl has type
-- r ≡ record { f = λ x → x ; D = A ; g = λ x _ → x }