text:
-- Andreas, 2016-01-08 allow --type-in-type with universe polymorphism

{-# OPTIONS --type-in-type #-}

-- {-# OPTIONS --v tc:30 #-}
-- {-# OPTIONS --v tc.conv.level:60 #-}

open import Common.Level
open import Common.Equality

Type : Set
Type = Set

data E α β : Set β where
  e : Set α → E α β

data D {α} (A : Set α) : Set where
  d : A → D A

-- Make sure we do not get unsolved level metas

id : ∀{a}{A : Set a} → A → A
id x = x

test = id Set

data Unit : Set where
  unit : Unit

test1 = id unit

data UnitP {α} : Set α where
  unitP : UnitP

test2 = id unitP

-- All levels are equal
-- (need not be for --type-in-type, but this is how it is implemented):

level0≡1 : lzero ≡ lsuc lzero
level0≡1 = refl

levelTrivial : ∀{a b : Level} → a ≡ b
levelTrivial = refl


text:
-- Andreas, 2014-02-17, reported by pumpkingod

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

data Bool : Set where true false : Bool

-- Equality

infix 4 _≡_

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

{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

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

cong : ∀ {a b}{A : Set a}{B : Set b}(f : A → B){x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

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

trans : ∀ {a}{A : Set a}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

infix  3 _∎
infixr 2 _≡⟨_⟩_
infix  1 begin_

data _IsRelatedTo_ (x y : Bool) : Set where
  relTo : (x≡y : x ≡ y) → x IsRelatedTo y

begin_ : ∀ {x y} → x IsRelatedTo y → x ≡ y
begin relTo x≡y = x≡y

_≡⟨_⟩_ : ∀ x {y z} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
_ ≡⟨ x≡y ⟩ relTo y≡z = relTo (trans x≡y y≡z)

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

-- Test

proof : true ≡ true
proof =
  begin
    {!!}
  ≡⟨ {!!} ⟩
    {!!} -- If you do C-c C-s, it will fill in the first and last boxes, but it will also fill this one in with an underscore!
  ≡⟨ {!!} ⟩
    {!!}
  ∎

-- C-c C-s should only solve for ?0 and ?4, not for ?2.

-- Constraints are

-- ?0 := true
-- ?2 := _y_38
-- ?4 := true

-- Metas are
--
-- ?0 : Bool
-- ?1 : true ≡ _y_38
-- ?2 : Bool
-- ?3 : _y_38 ≡ true
-- ?4 : Bool
-- _y_38 : Bool  [ at /home/abel/tmp/Agda2/test/bugs/Issue1060.agda:23,5-24,12 ]

ext: agda


text:
{-# OPTIONS --no-auto-inline #-}

-- Basic things needed by other primitive modules.

module Haskell.Prim where

open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit       public
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Agda.Builtin.Equality
open import Agda.Builtin.FromNat    public
open import Agda.Builtin.FromNeg    public
open import Agda.Builtin.FromString public

variable
  ℓ : Level
  a b c d e : Set
  f m s t : Set → Set

--------------------------------------------------
-- Functions

id : a → a
id x = x

infixr 9 _∘_
_∘_ : (b → c) → (a → b) → a → c
(f ∘ g) x = f (g x)

flip : (a → b → c) → b → a → c
flip f x y = f y x

const : a → b → a
const x _ = x

infixr 0 _$_
_$_ : (a → b) → a → b
f $ x = f x

--------------------------------------------------
-- Language constructs

infix -1 case_of_
case_of_ : a → (a → b) → b
case x of f = f x

infix -2 if_then_else_
if_then_else_ : {a : Set ℓ} → Bool → a → a → a
if false then x else y = y
if true  then x else y = x

--------------------------------------------------
-- Agda strings

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

--------------------------------------------------
-- Numbers

instance
  iNumberNat : Number Nat
  iNumberNat .Number.Constraint _ = ⊤
  iNumberNat .fromNat n = n

--------------------------------------------------
-- Lists

lengthNat : List a → Nat
lengthNat []       = 0
lengthNat (_ ∷ xs) = 1 + lengthNat xs

--------------------------------------------------
-- Proof things

data ⊥ : Set where

-- Use to bundle up constraints
data All {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
  instance
    allNil  : All B []
    allCons : ∀ {x xs} ⦃ i : B x ⦄ ⦃ is : All B xs ⦄ → All B (x ∷ xs)

data IsTrue : Bool → Set where
  instance itsTrue : IsTrue true

data IsFalse : Bool → Set where
  instance itsFalse : IsFalse false

data NonEmpty {a : Set} : List a → Set where
  instance itsNonEmpty : ∀ {x xs} → NonEmpty (x ∷ xs)

data TypeError (err : String) : Set where

it : ∀ {ℓ} {a : Set ℓ} → ⦃ a ⦄ → a
it ⦃ x ⦄ = x


text:
------------------------------------------------------------------------
-- A labelled transition system for the delay monad
------------------------------------------------------------------------

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

open import Prelude

module Labelled-transition-system.Delay-monad {a} (A : Type a) where

open import Delay-monad hiding (steps)
open import Equality.Propositional
open import Prelude.Size

open import Labelled-transition-system

------------------------------------------------------------------------
-- Transitions

infix 4 _[_]⟶_

data _[_]⟶_ : Delay A ∞ → Maybe A → Delay A ∞ → Type a where
  now   : ∀ {x} → now   x [ just x  ]⟶ now   x
  later : ∀ {x} → later x [ nothing ]⟶ force x

delay-monad : LTS a
delay-monad = record
  { Proc      = Delay A ∞
  ; Label     = Maybe A
  ; _[_]⟶_    = _[_]⟶_
  ; is-silent = if_then true else false
  }

open LTS delay-monad public hiding (_[_]⟶_)

------------------------------------------------------------------------
-- Some simple lemmas

-- If now x can make a sequence of silent transitions to y, then y
-- is equal to now x.

now[nothing]⟶ : ∀ {x y} → now x [ nothing ]⟶ y → y ≡ now x
now[nothing]⟶ ()

now⇒ : ∀ {x y} → now x ⇒ y → y ≡ now x
now⇒ done            = refl
now⇒ (step () now _)

now[nothing]⇒ : ∀ {x y} → now x [ nothing ]⇒ y → y ≡ now x
now[nothing]⇒ (steps nx⇒x′ x′⟶x″ x″⇒y)
  rewrite now⇒ nx⇒x′ | now[nothing]⟶ x′⟶x″ = now⇒ x″⇒y

now[nothing]⇒̂ : ∀ {x y} → now x [ nothing ]⇒̂ y → y ≡ now x
now[nothing]⇒̂ (silent _ tr)     = now⇒ tr
now[nothing]⇒̂ (non-silent ¬s _) = ⊥-elim (¬s _)

now[nothing]⟶̂ : ∀ {x y} → now x [ nothing ]⟶̂ y → y ≡ now x
now[nothing]⟶̂ (done _)  = refl
now[nothing]⟶̂ (step tr) = now[nothing]⟶ tr

-- If now x can make a just y-transition, then x is equal to y.

now[just]⟶ : ∀ {x y z} → now x [ just y ]⟶ z → x ≡ y
now[just]⟶ now = refl

now[just]⇒ : ∀ {x y z} → now x [ just y ]⇒ z → x ≡ y
now[just]⇒ (steps tr₁ tr₂ _) =
  now[just]⟶ (subst (_[ _ ]⟶ _) (now⇒ tr₁) tr₂)

now[just]⇒̂ : ∀ {x y z} → now x [ just y ]⇒̂ z → x ≡ y
now[just]⇒̂ (silent () _)
now[just]⇒̂ (non-silent _ tr) = now[just]⇒ tr

now[just]⟶̂ : ∀ {x y z} → now x [ just y ]⟶̂ z → x ≡ y
now[just]⟶̂ (done ())
now[just]⟶̂ (step tr) = now[just]⟶ tr

-- The computation never can only transition to itself.

never⟶never : ∀ {μ x} → never [ μ ]⟶ x → x ≡ never
never⟶never later = refl

never⇒never : ∀ {x} → never ⇒ x → x ≡ never
never⇒never done               = refl
never⇒never (step _ later ne⇒) = never⇒never ne⇒

never[]⇒never : ∀ {μ x} → never [ μ ]⇒ x → x ≡ never
never[]⇒never (steps ne⇒x x⟶y y⇒z)
  rewrite never⇒never ne⇒x | never⟶never x⟶y = never⇒never y⇒z

never⇒̂never : ∀ {μ x} → never [ μ ]⇒̂ x → x ≡ never
never⇒̂never (silent     _ ne⇒) = never⇒never ne⇒
never⇒̂never (non-silent _ ne⇒) = never[]⇒never ne⇒

never⟶̂never : ∀ {μ x} → never [ μ ]⟶̂ x → x ≡ never
never⟶̂never (done _)   = refl
never⟶̂never (step ne⟶) = never⟶never ne⟶

-- If never can make a μ-transition, then μ is silent.

never⟶→silent : ∀ {μ x} → never [ μ ]⟶ x → Silent μ
never⟶→silent later = _

never[]⇒→silent : ∀ {μ x} → never [ μ ]⇒ x → Silent μ
never[]⇒→silent (steps ne⇒x  x⟶  _) with never⇒never ne⇒x
never[]⇒→silent (steps ne⇒ne ne⟶ _) | refl = never⟶→silent ne⟶

never⇒̂→silent : ∀ {μ x} → never [ μ ]⇒̂ x → Silent μ
never⇒̂→silent (silent s _)       = s
never⇒̂→silent (non-silent _ ne⇒) = never[]⇒→silent ne⇒

never⟶̂→silent : ∀ {μ x} → never [ μ ]⟶̂ x → Silent μ
never⟶̂→silent (done s)   = s
never⟶̂→silent (step ne⟶) = never⟶→silent ne⟶

-- If x can make a non-silent transition, with label just y, to z,
-- then z is equal to now y.

[just]⟶ : ∀ {x y z} → x [ just y ]⟶ z → z ≡ now y
[just]⟶ now = refl

[just]⇒ : ∀ {x y z} → x [ just y ]⇒ z → z ≡ now y
[just]⇒ (steps _ now ny⇒z) = now⇒ ny⇒z

[just]⇒̂ : ∀ {x y z} → x [ just y ]⇒̂ z → z ≡ now y
[just]⇒̂ (silent () _)
[just]⇒̂ (non-silent _ x⇒z) = [just]⇒ x⇒z

[just]⟶̂ : ∀ {x y z} → x [ just y ]⟶̂ z → z ≡ now y
[just]⟶̂ (done ())
[just]⟶̂ (step x⟶z) = [just]⟶ x⟶z

-- In some cases x is also equal to now y.

[just]⟶→≡now : ∀ {x y z} → x [ just y ]⟶ z → x ≡ now y
[just]⟶→≡now now = refl

[just]⟶̂→≡now : ∀ {x y z} → x [ just y ]⟶̂ z → x ≡ now y
[just]⟶̂→≡now (done ())
[just]⟶̂→≡now (step x⟶z) = [just]⟶→≡now x⟶z

-- If force x can make a weak μ-transition (_[_]⇒_ or _[_]⇒̂_) to y,
-- then later x can also make a weak μ-transition (of the same kind)
-- to y.

later[]⇒ : ∀ {μ x y} → force x [ μ ]⇒ y → later x [ μ ]⇒ y
later[]⇒ = ⇒[]⇒-transitive (⟶→⇒ _ later)

later⇒̂ : ∀ {μ x y} → force x [ μ ]⇒̂ y → later x [ μ ]⇒̂ y
later⇒̂ = ⇒⇒̂-transitive (⟶→⇒ _ later)

-- The process x can make a silent transition to drop-later x.

⇒drop-later : ∀ {x} → x ⇒ drop-later x
⇒drop-later {now x}   = done
⇒drop-later {later x} = step _ later done

-- If x can make a transition to y, then drop-later x can in some
-- cases make a transition of the same kind to drop-later y.

drop-later-cong⟶ :
  ∀ {x μ y} →
  ¬ Silent μ → x [ μ ]⟶ y → drop-later x [ μ ]⟶ drop-later y
drop-later-cong⟶ _  now   = now
drop-later-cong⟶ ¬s later = ⊥-elim (¬s _)

drop-later-cong⇒ : ∀ {x y} → x ⇒ y → drop-later x ⇒ drop-later y
drop-later-cong⇒ done                = done
drop-later-cong⇒ (step () now   _)
drop-later-cong⇒ (step _  later x⇒y) =
  ⇒-transitive ⇒drop-later (drop-later-cong⇒ x⇒y)

drop-later-cong[]⇒ :
  ∀ {x μ y} →
  ¬ Silent μ → x [ μ ]⇒ y → drop-later x [ μ ]⇒ drop-later y
drop-later-cong[]⇒ ¬s (steps x⇒y y⟶z z⇒u) =
  steps (drop-later-cong⇒ x⇒y) (drop-later-cong⟶ ¬s y⟶z)
        (drop-later-cong⇒ z⇒u)

drop-later-cong⇒̂ :
  ∀ {x μ y} → x [ μ ]⇒̂ y → drop-later x [ μ ]⇒̂ drop-later y
drop-later-cong⇒̂ (silent s x⇒y)      = silent s (drop-later-cong⇒ x⇒y)
drop-later-cong⇒̂ (non-silent ¬s x⇒y) =
  non-silent ¬s (drop-later-cong[]⇒ ¬s x⇒y)

drop-later-cong⟶̂ :
  ∀ {x μ y} →
  ¬ Silent μ → x [ μ ]⟶̂ y → drop-later x [ μ ]⟶̂ drop-later y
drop-later-cong⟶̂ _  (done s)   = done s
drop-later-cong⟶̂ ¬s (step x⟶y) = step (drop-later-cong⟶ ¬s x⟶y)

-- If later x can make a transition to later y, then force x can
-- make a transition (of the same kind) to force y.

drop-later⟶ :
  ∀ {μ x y} → later x [ μ ]⟶ later y → force x [ μ ]⟶ force y
drop-later⟶ lx⟶ly = helper lx⟶ly refl refl
  where
  helper : ∀ {μ x x′ y y′} →
           later x [ μ ]⟶ y′ →
           y′ ≡ later y →
           x′ ≡ force x →
           x′ [ μ ]⟶ force y
  helper {x = x} {x′} {y} later x≡ly x′≡x =
    subst (_[ _ ]⟶ _) ly≡x′ later
    where
    ly≡x′ =
      later y  ≡⟨ sym x≡ly ⟩
      force x  ≡⟨ sym x′≡x ⟩∎
      x′       ∎

drop-later⇒ : ∀ {x y} → later x ⇒ later y → force x ⇒ force y
drop-later⇒ = drop-later-cong⇒

drop-later[]⇒ :
  ∀ {μ x y} → later x [ μ ]⇒ later y → force x [ μ ]⇒ force y
drop-later[]⇒ (steps lx⇒ly later y⇒lz) =
  ⇒[]⇒-transitive (⇒-transitive (drop-later⇒ lx⇒ly) y⇒lz)
                  (⟶→[]⇒ later)
drop-later[]⇒ (steps _ now ny⇒lz) with now⇒ ny⇒lz
... | ()

drop-later⇒̂ :
  ∀ {μ x y} → later x [ μ ]⇒̂ later y → force x [ μ ]⇒̂ force y
drop-later⇒̂ = drop-later-cong⇒̂

drop-later⟶̂ :
  ∀ {μ x y} → later x [ μ ]⟶̂ later y → force x [ μ ]⟶̂ force y
drop-later⟶̂ (done s)     = done s
drop-later⟶̂ (step lx⟶ly) = step (drop-later⟶ lx⟶ly)

-- If x makes silent transitions to both y and z, then one of y and
-- z makes silent transitions to the other.

⇒×⇒→… : ∀ {x y z} → x ⇒ y → x ⇒ z → y ⇒ z ⊎ z ⇒ y
⇒×⇒→… done               x⇒z                = inj₁ x⇒z
⇒×⇒→… x⇒y                done               = inj₂ x⇒y
⇒×⇒→… (step _ later x⇒y) (step _ later x⇒z) = ⇒×⇒→… x⇒y x⇒z
⇒×⇒→… (step () now _)

-- If x makes silent transitions to y and a non-silent weak
-- μ-transition (of one kind) to z, then y makes a weak μ-transition
-- to z.

⇒×⇒[]→… :
  ∀ {x y z μ} →
  ¬ Silent μ → x ⇒ y → x [ μ ]⇒ z → y [ μ ]⇒ z
⇒×⇒[]→… _ x⇒y (steps x⇒x′ x′⟶x″ x″⇒z) with ⇒×⇒→… x⇒y x⇒x′
⇒×⇒[]→… _ _   (steps _    x′⟶x″ x″⇒z) | inj₁ y⇒x′ = steps y⇒x′ x′⟶x″ x″⇒z
⇒×⇒[]→… _ _   (steps _    now   n⇒z)  | inj₂ done = steps done now   n⇒z

⇒×⇒[]→… _  _  _                 | inj₂ (step () now _)
⇒×⇒[]→… ¬s _  (steps _ later _) | _ = ⊥-elim (¬s _)

-- If x makes silent transitions to y and a weak μ-transition (of
-- one kind) to z, then either y makes a weak μ-transition to z, or
-- μ is silent and z makes silent transitions to y.

⇒×⇒̂→… :
  ∀ {x y z μ} → x ⇒ y → x [ μ ]⇒̂ z → y [ μ ]⇒̂ z ⊎ Silent μ × z ⇒ y
⇒×⇒̂→… x⇒y (silent     s  x⇒z) = ⊎-map (silent s) (s ,_)
                                      (⇒×⇒→… x⇒y x⇒z)
⇒×⇒̂→… x⇒y (non-silent ¬s x⇒z) =
  inj₁ (non-silent ¬s (⇒×⇒[]→… ¬s x⇒y x⇒z))

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
--------------------------------------------------------------------------------
-- This file contains functions to turn the tree of parse results into the agda
-- data structures they represent.
--------------------------------------------------------------------------------

{-# OPTIONS --type-in-type #-}

module Parse.TreeConvert where

import Data.Sum
open import Class.Map
open import Class.Monad.Except
open import Data.SimpleMap
open import Data.String using (fromList; toList; fromChar; uncons)
open import Data.Tree
open import Data.Tree.Instance
open import Data.Word using (fromℕ)

open import Prelude
open import Prelude.Strings

open import CoreTheory
open import Bootstrap.InitEnv
open import Parse.MultiChar
open import Parse.LL1
open import Parse.Generate
open import Parse.Escape

continueIfInit : ∀ {a} {A : Set a} → List Char → List Char → (List Char → A) → Maybe A
continueIfInit {A = A} init s = helper init s
  where
    helper : List Char → List Char → (List Char → A) → Maybe A
    helper [] s f = just $ f s
    helper (x₁ ∷ init) [] f = nothing
    helper (x₁ ∷ init) (x ∷ s) f with x ≟ x₁
    ... | yes p = helper init s f
    ... | no ¬p = nothing

ruleId : List Char → List Char → Maybe (ℕ ⊎ Char)
ruleId nonterm rule = do
  rules ← lookup nonterm parseRuleMap
  i ← findIndexList (_≟ (nonterm + "$" + rule)) rules
  return $ inj₁ i

_≡ᴹ_ : ℕ ⊎ Char → Maybe (ℕ ⊎ Char) → Bool
x ≡ᴹ y = just x ≣ y

toSort : Tree (ℕ ⊎ Char) → Maybe Sort
toSort (Node x x₁) =
  if x ≡ᴹ ruleId "sort" "*"
    then return ⋆
    else if x ≡ᴹ ruleId "sort" "□"
      then return □
      else nothing

toConst : Tree (ℕ ⊎ Char) → Maybe Const
toConst (Node x x₁) =
  if x ≡ᴹ ruleId "const" "Char"
    then return CharT
    else nothing

toChar : Tree (ℕ ⊎ Char) → Maybe Char
toChar (Node (inj₁ x) x₁) = nothing
toChar (Node (inj₂ y) x₁) = just y

toChar' : Tree (ℕ ⊎ Char) → Maybe Char
toChar' (Node x x₁) =
  if x ≡ᴹ ruleId "char" "!!"
    then (case x₁ of λ { (y ∷ []) → toChar y ; _ → nothing })
    else nothing

toName : Tree (ℕ ⊎ Char) → Maybe String
toName (Node x x₁) = case x₁ of λ
  { (y ∷ y' ∷ _) → do
    c ← toChar y
    n ← toName y'
    return (fromChar c + n)
  ; [] → if x ≡ᴹ ruleId "string'" ""
      then return ""
      else nothing
  ; _ → nothing }

toNameList : Tree (ℕ ⊎ Char) → Maybe (List String)
toNameList (Node x []) = just []
toNameList (Node x (x₁ ∷ x₂ ∷ _)) = do
  n ← toName x₁
  rest ← toNameList x₂
  return $ n ∷ rest
{-# CATCHALL #-}
toNameList _ = nothing

toIndex : Tree (ℕ ⊎ Char) → Maybe ℕ
toIndex t = do
  res ← helper t
  foldl {A = Maybe ℕ} (λ x c → (λ x' → 10 * x' + c) <$> x) (just 0) res
  where
    helper' : Tree (ℕ ⊎ Char) → Maybe (List ℕ)
    helper' (Node x []) =
      if x ≡ᴹ ruleId "index'" ""
        then return []
        else nothing
    helper' (Node x (x₁ ∷ _)) = do
      rest ← helper' x₁
      decCase (just x) of
        (ruleId "index'" "0_index'_" , return (0 ∷ rest)) ∷
        (ruleId "index'" "1_index'_" , return (1 ∷ rest)) ∷
        (ruleId "index'" "2_index'_" , return (2 ∷ rest)) ∷
        (ruleId "index'" "3_index'_" , return (3 ∷ rest)) ∷
        (ruleId "index'" "4_index'_" , return (4 ∷ rest)) ∷
        (ruleId "index'" "5_index'_" , return (5 ∷ rest)) ∷
        (ruleId "index'" "6_index'_" , return (6 ∷ rest)) ∷
        (ruleId "index'" "7_index'_" , return (7 ∷ rest)) ∷
        (ruleId "index'" "8_index'_" , return (8 ∷ rest)) ∷
        (ruleId "index'" "9_index'_" , return (9 ∷ rest)) ∷ []
        default nothing

    helper : Tree (ℕ ⊎ Char) → Maybe (List ℕ)
    helper (Node x []) = nothing
    helper (Node x (x₁ ∷ _)) = do
      rest ← helper' x₁
      decCase just x of
        (ruleId "index" "0_index'_" , return (0 ∷ rest)) ∷
        (ruleId "index" "1_index'_" , return (1 ∷ rest)) ∷
        (ruleId "index" "2_index'_" , return (2 ∷ rest)) ∷
        (ruleId "index" "3_index'_" , return (3 ∷ rest)) ∷
        (ruleId "index" "4_index'_" , return (4 ∷ rest)) ∷
        (ruleId "index" "5_index'_" , return (5 ∷ rest)) ∷
        (ruleId "index" "6_index'_" , return (6 ∷ rest)) ∷
        (ruleId "index" "7_index'_" , return (7 ∷ rest)) ∷
        (ruleId "index" "8_index'_" , return (8 ∷ rest)) ∷
        (ruleId "index" "9_index'_" , return (9 ∷ rest)) ∷ []
        default nothing

toTerm : Tree (ℕ ⊎ Char) → Maybe AnnTerm
toTerm = helper []
  where
    helper : List String → Tree (ℕ ⊎ Char) → Maybe AnnTerm
    helper accu (Node x x₁) =
      decCase just x of

        (ruleId "term" "_var_" , (case x₁ of λ
          { ((Node y (n ∷ [])) ∷ []) →
            decCase just y of
              (ruleId "var" "_string_" , do
                n' ← toName n
                return $ case findIndexList (n' ≟_) accu of λ
                  { (just x) → BoundVar $ fromℕ x
                  ; nothing → FreeVar n' }) ∷
              (ruleId "var" "_index_" , do
                n' ← toIndex n
                return $ BoundVar $ fromℕ n') ∷ []
            default nothing
          ; _ → nothing })) ∷

        (ruleId "term" "_sort_" , do
          s ← head x₁ >>= toSort
          return $ Sort-A s) ∷

        (ruleId "term" "π^space^_term_" , (case x₁ of λ
          { (y ∷ []) → do
            y' ← helper accu y
            return $ Pr1-A y'
          ; _ → nothing })) ∷

        (ruleId "term" "ψ^space^_term_" , (case x₁ of λ
          { (y ∷ []) → do
            y' ← helper accu y
            return $ Pr2-A y'
          ; _ → nothing })) ∷

        (ruleId "term" "β^space^_term_^space^_term_" , (case x₁ of λ
          { (y ∷ y' ∷ []) → do
            t ← helper accu y
            t' ← helper accu y'
            return $ Beta-A t t'
          ; _ → nothing })) ∷

        (ruleId "term" "δ^space^_term_^space^_term_" , (case x₁ of λ
          { (y ∷ y' ∷ []) → do
            t ← helper accu y
            t' ← helper accu y'
            return $ Delta-A t t'
          ; _ → nothing })) ∷

        (ruleId "term" "σ^space^_term_" , (case x₁ of λ
          { (y ∷ []) → helper accu y >>= λ y' → return (Sigma-A y') ; _ → nothing })) ∷

        (ruleId "term" "[^space'^_term_^space^_term_^space'^]" , (case x₁ of λ
          { (y ∷ y' ∷ []) → do
            t ← helper accu y
            t' ← helper accu y'
            return $ App-A t t'
          ; _ → nothing })) ∷

        (ruleId "term" "<^space'^_term_^space^_term_^space'^>" , (case x₁ of λ
          { (y ∷ y' ∷ []) → do
            t ← helper accu y
            t' ← helper accu y'
            return $ AppE-A t t'
          ; _ → nothing })) ∷

        (ruleId "term"
          "ρ^space^_term_^space^_string_^space'^.^space'^_term_^space^_term_" , (case x₁ of λ
          { (y ∷ n' ∷ y' ∷ y'' ∷ []) → do
            t ← helper accu y
            n ← toName n'
            t' ← helper (n ∷ accu) y'
            t'' ← helper accu y''
            return $ Rho-A t t' t''
          ; _ → nothing })) ∷

        (ruleId "term"
          "∀^space^_string_^space'^:^space'^_term_^space^_term_" , (case x₁ of λ
          { (n' ∷ y ∷ y' ∷ []) → do
            n ← toName n'
            t ← helper accu y
            t' ← helper (n ∷ accu) y'
            return $ All-A n t t'
          ; _ → nothing })) ∷

        (ruleId "term"
          "Π^space^_string_^space'^:^space'^_term_^space^_term_" , (case x₁ of λ
          { (n' ∷ y ∷ y' ∷ []) → do
            n ← toName n'
            t ← helper accu y
            t' ← helper (n ∷ accu) y'
            return $ Pi-A n t t'
          ; _ → nothing })) ∷

        (ruleId "term"
          "ι^space^_string_^space'^:^space'^_term_^space^_term_" , (case x₁ of λ
          { (n' ∷ y ∷ y' ∷ []) → do
            n ← toName n'
            t ← helper accu y
            t' ← helper (n ∷ accu) y'
            return $ Iota-A n t t'
          ; _ → nothing })) ∷

        (ruleId "term"
          "λ^space^_string_^space'^:^space'^_term_^space^_term_" , (case x₁ of λ
          { (n' ∷ y ∷ y' ∷ []) → do
            n ← toName n'
            t ← helper accu y
            t' ← helper (n ∷ accu) y'
            return $ Lam-A n t t'
          ; _ → nothing })) ∷

        (ruleId "term"
          "Λ^space^_string_^space'^:^space'^_term_^space^_term_" , (case x₁ of λ
          { (n' ∷ y ∷ y' ∷ []) → do
            n ← toName n'
            t ← helper accu y
            t' ← helper (n ∷ accu) y'
            return $ LamE-A n t t'
          ; _ → nothing })) ∷

        (ruleId "term"
          "{^space'^_term_^space'^,^space'^_term_^space^_string_^space'^.^space'^_term_^space'^}" ,
          (case x₁ of λ
          { (y ∷ y' ∷ n' ∷ y'' ∷ []) → do
            t ← helper accu y
            t' ← helper accu y'
            n ← toName n'
            t'' ← helper (n ∷ accu) y''
            return $ Pair-A t t' t''
          ; _ → nothing })) ∷

        (ruleId "term" "φ^space^_term_^space^_term_^space^_term_" , (case x₁ of λ
          { (y ∷ y' ∷ y'' ∷ []) → do
            t ← helper accu y
            t' ← helper accu y'
            t'' ← helper accu y''
            return $ Phi-A t t' t''
          ; _ → nothing })) ∷

        (ruleId "term" "=^space^_term_^space^_term_" , (case x₁ of λ
          { (y ∷ y' ∷ []) → do
            t ← helper accu y
            t' ← helper accu y'
            return $ Eq-A t t'
          ; _ → nothing })) ∷

        (ruleId "term" "ω^space^_term_" , (case x₁ of λ
          { (y ∷ []) → do
            t ← helper accu y
            return $ M-A t
          ; _ → nothing })) ∷

        (ruleId "term" "μ^space^_term_^space^_term_" , (case x₁ of λ
          { (y ∷ y' ∷ []) → do
            t ← helper accu y
            t' ← helper accu y'
            return $ Mu-A t t'
          ; _ → nothing })) ∷

        (ruleId "term" "ε^space^_term_" , (case x₁ of λ
          { (y ∷ []) → do
            t ← helper accu y
            return $ Epsilon-A t
          ; _ → nothing })) ∷

        (ruleId "term" "ζEvalStmt^space^_term_" , (case x₁ of λ
          { (z ∷ []) → do
            t ← helper accu z
            return $ Ev-A EvalStmt t
          ; _ → nothing })) ∷

        (ruleId "term" "ζShellCmd^space^_term_^space^_term_" , (case x₁ of λ
          { (z ∷ z' ∷ []) → do
            t ← helper accu z
            t' ← helper accu z'
            return $ Ev-A ShellCmd (t , t')
          ; _ → nothing })) ∷

        (ruleId "term" "ζCheckTerm^space^_term_^space^_term_" , (case x₁ of λ
          { (z ∷ z' ∷ []) → do
            t ← helper accu z
            t' ← helper accu z'
            return $ Ev-A CheckTerm (t , t')
          ; _ → nothing })) ∷

        (ruleId "term" "ζParse^space^_term_^space^_term_^space^_term_" , (case x₁ of λ
          { (z ∷ z' ∷ z'' ∷ []) → do
            t ← helper accu z
            t' ← helper accu z'
            t'' ← helper accu z''
            return $ Ev-A Parse (t , t' , t'')
          ; _ → nothing })) ∷

        (ruleId "term" "ζCatchErr^space^_term_^space^_term_" , (case x₁ of λ
          { (z ∷ z' ∷ []) → do
            t ← helper accu z
            t' ← helper accu z'
            return $ Gamma-A t t'
          ; _ → nothing })) ∷

        (ruleId "term" "ζNormalize^space^_term_" , (case x₁ of λ
          { (z ∷ []) → do
            t ← helper accu z
            return $ Ev-A Normalize t
          ; _ → nothing })) ∷

        (ruleId "term" "ζHeadNormalize^space^_term_" , (case x₁ of λ
          { (z ∷ []) → do
            t ← helper accu z
            return $ Ev-A HeadNormalize t
          ; _ → nothing })) ∷

        (ruleId "term" "ζInferType^space^_term_" , (case x₁ of λ
          { (z ∷ []) → do
            t ← helper accu z
            return $ Ev-A InferType t
          ; _ → nothing })) ∷

        (ruleId "term" "Κ_const_" , (case x₁ of λ
          { (z ∷ []) → do
            c ← toConst z
            return $ Const-A c
          ; _ → nothing })) ∷

        (ruleId "term" "κ_char_" , (case x₁ of λ
          { (z ∷ []) → do
            c ← toChar z <∣> toChar' z
            return $ Char-A c
          ; _ → nothing })) ∷

        (ruleId "term" "γ^space^_term_^space^_term_" , (case x₁ of λ
          { (z ∷ z' ∷ []) → do
            t ← helper accu z
            t' ← helper accu z'
            return $ CharEq-A t t'
          ; _ → nothing })) ∷

        []
        default nothing

data Stmt : Set where
  Let           : GlobalName → AnnTerm → Maybe AnnTerm → Stmt
  Ass           : GlobalName → AnnTerm → Stmt
  SetEval       : AnnTerm → String → String → Stmt
  Import        : String → Stmt
  Empty         : Stmt

instance
  Stmt-Show : Show Stmt
  Stmt-Show = record { show = helper }
    where
      helper : Stmt → String
      helper (Let x x₁ (just x₂)) = "let " + x + " := " + show x₁ + " : " + show x₂
      helper (Let x x₁ nothing)   = "let " + x + " := " + show x₁
      helper (Ass x x₁)           = "ass " + x + " : " + show x₁
      helper (SetEval x n n')     = "seteval " + show x + " " + n + " " + n'
      helper (Import s)           = "import " + s
      helper Empty                = "Empty"

toStmt : Tree (ℕ ⊎ Char) → Maybe Stmt
toStmt (Node x ((Node x' x₂) ∷ [])) =
  if x ≡ᴹ ruleId "stmt" "^space'^_stmt'_"
    then
      decCase just x' of
        (ruleId "stmt'" "let^space^_string_^space'^:=^space'^_term_^space'^_lettail_" ,
          (case x₂ of λ
            { (y ∷ y' ∷ y'' ∷ []) → do
              n ← toName y
              t ← toTerm y'
              return $ Let n t $ toLetTail y''
            ; _ → nothing })) ∷

        (ruleId "stmt'"
          "ass^space^_string_^space'^:^space'^_term_^space'^." ,
          (case x₂ of λ
            { (y ∷ y₁ ∷ []) → do
              n ← toName y
              t ← toTerm y₁
              return $ Ass n t
            ; _ → nothing })) ∷

        (ruleId "stmt'" "seteval^space^_term_^space^_string_^space^_string_^space'^." ,
          (case x₂ of λ
            { (y ∷ y' ∷ y'' ∷ []) → do
              t ← toTerm y
              n ← toName y'
              n' ← toName y''
              return $ SetEval t n n'
            ; _ → nothing })) ∷

        (ruleId "stmt'" "import^space^_string_^space'^." ,
          (case x₂ of λ
            { (y ∷ []) → do
              n ← toName y
              return $ Import n
            ; _ → nothing })) ∷

        (ruleId "stmt'" "" ,
          return Empty) ∷

        []
      default nothing
    else nothing

  where
    toLetTail : Tree (ℕ ⊎ Char) → Maybe AnnTerm
    toLetTail (Node x x₁) =
      decCase just x of
        (ruleId "lettail" ":^space'^_term_^space'^." ,
          (case x₁ of λ
            { (y ∷ []) → toTerm y
            ; _ → nothing })) ∷
        []
      default nothing

{-# CATCHALL #-}
toStmt _ = nothing

private
  -- Folds a tree of constructors back into a term by properly applying the
  -- constructors and prefixing the namespace
  {-# TERMINATING #-}
  foldConstrTree : String → Tree (String ⊎ Char) → AnnTerm
  foldConstrTree namespace (Node x x₁) =
    foldl (λ t t' → t ⟪$⟫ t') (ruleToTerm x) (foldConstrTree namespace <$> x₁)
      where
        ruleToTerm : String ⊎ Char → AnnTerm
        ruleToTerm (inj₁ x) = FreeVar (namespace + "$" + ruleToConstr x)
        ruleToTerm (inj₂ y) = Char-A y

  convertIfChar : Tree (String ⊎ Char) → Maybe (Tree (ℕ ⊎ Char))
  convertIfChar (Node (inj₁ x) x₁) = do
    rest ← stripPrefix "nameInitChar$" x <∣> stripPrefix "nameTailChar$" x
    (c , s) ← uncons rest
    just $ Node (inj₂ $ unescape c s) []
  convertIfChar (Node (inj₂ x) x₁) = nothing

module _ {M} {{_ : Monad M}} {{_ : MonadExcept M String}} where

  preCoreGrammar : M Grammar
  preCoreGrammar = generateCFGNonEscaped "stmt" (map fromList coreGrammarGenerator)

  private
    parseToConstrTree : (G : Grammar) → NonTerminal G → String → M (Tree (String ⊎ Char) × String)
    parseToConstrTree (_ , G , (showRule , showNT)) S s = do
      (t , rest) ← parseWithInitNT showNT matchMulti show G M S s
      return (_<$>_ {{Tree-Functor}} (Data.Sum.map₁ showRule) t , rest)

    parsePreCoreGrammar : String → M (Tree (String ⊎ Char) × String)
    parsePreCoreGrammar s = do
      G ← preCoreGrammar
      parseToConstrTree G (initNT G) s

    {-# TERMINATING #-} -- cannot just use sequence here because of the char special case
    synTreeToℕTree : Tree (String ⊎ Char) → M (Tree (ℕ ⊎ Char))
    synTreeToℕTree t@(Node (inj₁ x) x₁) with convertIfChar t
    ... | (just t') = return t'
    ... | nothing = do
      id ← fullRuleId x
      ids ← sequence $ map synTreeToℕTree x₁
      return (Node id ids)
      where
        fullRuleId : String → M (ℕ ⊎ Char)
        fullRuleId l with break (_≟ '$') (toList l) -- split at '$'
        ... | (x , []) = throwError "No '$' character found!"
        ... | (x , _ ∷ y) = maybeToError (ruleId x y) ("Rule " + l + "doesn't exist!")

    synTreeToℕTree (Node (inj₂ x) x₁) = return $ Node (inj₂ x) []

  -- Parse the next top-level non-terminal symbol from a string, and return a
  -- term representing the result of the parse, as well as the unparsed rest of
  -- the string
  parse : (G : Grammar) → NonTerminal G → String → String → M (AnnTerm × String)
  parse G S namespace s = do
    (t , rest) ← parseToConstrTree G S s
    return (foldConstrTree namespace t , rest)

  -- Used for bootstrapping
  parseStmt : String → M (Stmt × String)
  parseStmt s = do
    (y' , rest) ← parsePreCoreGrammar s
    y ← synTreeToℕTree y'
    case toStmt y of λ where
      (just x) → return (x , rest)
      nothing → throwError ("Error while converting syntax tree to statement!\nTree:\n" + show y
                             + "\nRemaining: " + s)

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
{-

Basic properties about Σ-types

- Action of Σ on functions ([map-fst], [map-snd])
- Characterization of equality in Σ-types using dependent paths ([ΣPath{Iso,≃,≡}PathΣ], [Σ≡Prop])
- Proof that discrete types are closed under Σ ([discreteΣ])
- Commutativity and associativity ([Σ-swap-*, Σ-assoc-*])
- Distributivity of Π over Σ ([Σ-Π-*])
- Action of Σ on isomorphisms, equivalences, and paths ([Σ-cong-fst], [Σ-cong-snd], ...)
- Characterization of equality in Σ-types using transport ([ΣPathTransport{≃,≡}PathΣ])
- Σ with a contractible base is its fiber ([Σ-contractFst, ΣUnit])

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Sigma.Properties where

open import Cubical.Data.Sigma.Base

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Relation.Nullary
open import Cubical.Data.Unit.Base

open import Cubical.Reflection.StrictEquiv

open Iso

private
  variable
    ℓ ℓ' ℓ'' : Level
    A A' : Type ℓ
    B B' : (a : A) → Type ℓ
    C : (a : A) (b : B a) → Type ℓ

map-fst : {B : Type ℓ} → (f : A → A') → A × B → A' × B
map-fst f (a , b) = (f a , b)

map-snd : (∀ {a} → B a → B' a) → Σ A B → Σ A B'
map-snd f (a , b) = (a , f b)

map-× : {B : Type ℓ} {B' : Type ℓ'} → (A → A') → (B → B') → A × B → A' × B'
map-× f g (a , b) = (f a , g b)

≡-× : {A : Type ℓ} {B : Type ℓ'} {x y : A × B} → fst x ≡ fst y → snd x ≡ snd y → x ≡ y
≡-× p q i = (p i) , (q i)

-- Characterization of paths in Σ using dependent paths

module _ {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'}
  {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)}
  where

  ΣPathP : Σ[ p ∈ PathP A (fst x) (fst y) ] PathP (λ i → B i (p i)) (snd x) (snd y)
         → PathP (λ i → Σ (A i) (B i)) x y
  ΣPathP eq i = fst eq i , snd eq i

  PathPΣ : PathP (λ i → Σ (A i) (B i)) x y
         → Σ[ p ∈ PathP A (fst x) (fst y) ] PathP (λ i → B i (p i)) (snd x) (snd y)
  PathPΣ eq = (λ i → fst (eq i)) , (λ i → snd (eq i))

  -- allows one to write
  -- open PathPΣ somePathInΣAB renaming (fst ... )
  module PathPΣ (p : PathP (λ i → Σ (A i) (B i)) x y) where
    open Σ (PathPΣ p) public

  ΣPathIsoPathΣ : Iso (Σ[ p ∈ PathP A (fst x) (fst y) ] (PathP (λ i → B i (p i)) (snd x) (snd y)))
                      (PathP (λ i → Σ (A i) (B i)) x y)
  fun ΣPathIsoPathΣ        = ΣPathP
  inv ΣPathIsoPathΣ        = PathPΣ
  rightInv ΣPathIsoPathΣ _ = refl
  leftInv ΣPathIsoPathΣ _  = refl

  unquoteDecl ΣPath≃PathΣ = declStrictIsoToEquiv ΣPath≃PathΣ ΣPathIsoPathΣ

  ΣPath≡PathΣ : (Σ[ p ∈ PathP A (fst x) (fst y) ] (PathP (λ i → B i (p i)) (snd x) (snd y)))
              ≡ (PathP (λ i → Σ (A i) (B i)) x y)
  ΣPath≡PathΣ = ua ΣPath≃PathΣ

×≡Prop : isProp A' → {u v : A × A'} → u .fst ≡ v .fst → u ≡ v
×≡Prop pB {u} {v} p i = (p i) , (pB (u .snd) (v .snd) i)

-- Characterization of dependent paths in Σ

module _ {A : I → Type ℓ} {B : (i : I) → (a : A i) → Type ℓ'}
  {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)}
  where

  ΣPathPIsoPathPΣ :
    Iso (Σ[ p ∈ PathP A (x .fst) (y .fst) ] PathP (λ i → B i (p i)) (x .snd) (y .snd))
        (PathP (λ i → Σ (A i) (B i)) x y)
  ΣPathPIsoPathPΣ .fun (p , q) i = p i , q i
  ΣPathPIsoPathPΣ .inv pq .fst i = pq i .fst
  ΣPathPIsoPathPΣ .inv pq .snd i = pq i .snd
  ΣPathPIsoPathPΣ .rightInv _ = refl
  ΣPathPIsoPathPΣ .leftInv _ = refl

  unquoteDecl ΣPathP≃PathPΣ = declStrictIsoToEquiv ΣPathP≃PathPΣ ΣPathPIsoPathPΣ

  ΣPathP≡PathPΣ = ua ΣPathP≃PathPΣ

-- Σ of discrete types

discreteΣ : Discrete A → ((a : A) → Discrete (B a)) → Discrete (Σ A B)
discreteΣ {B = B} Adis Bdis (a0 , b0) (a1 , b1) = discreteΣ' (Adis a0 a1)
  where
    discreteΣ' : Dec (a0 ≡ a1) → Dec ((a0 , b0) ≡ (a1 , b1))
    discreteΣ' (yes p) = J (λ a1 p → ∀ b1 → Dec ((a0 , b0) ≡ (a1 , b1))) (discreteΣ'') p b1
      where
        discreteΣ'' : (b1 : B a0) → Dec ((a0 , b0) ≡ (a0 , b1))
        discreteΣ'' b1 with Bdis a0 b0 b1
        ... | (yes q) = yes (transport ΣPath≡PathΣ (refl , q))
        ... | (no ¬q) = no (λ r → ¬q (subst (λ X → PathP (λ i → B (X i)) b0 b1) (Discrete→isSet Adis a0 a0 (cong fst r) refl) (cong snd r)))
    discreteΣ' (no ¬p) = no (λ r → ¬p (cong fst r))

module _ {A : Type ℓ} {A' : Type ℓ'} where
  Σ-swap-Iso : Iso (A × A') (A' × A)
  fun Σ-swap-Iso (x , y) = (y , x)
  inv Σ-swap-Iso (x , y) = (y , x)
  rightInv Σ-swap-Iso _ = refl
  leftInv Σ-swap-Iso _  = refl

  unquoteDecl Σ-swap-≃ = declStrictIsoToEquiv Σ-swap-≃ Σ-swap-Iso

module _ {A : Type ℓ} {B : A → Type ℓ'} {C : ∀ a → B a → Type ℓ''} where
  Σ-assoc-Iso : Iso (Σ[ (a , b) ∈ Σ A B ] C a b) (Σ[ a ∈ A ] Σ[ b ∈ B a ] C a b)
  fun Σ-assoc-Iso ((x , y) , z) = (x , (y , z))
  inv Σ-assoc-Iso (x , (y , z)) = ((x , y) , z)
  rightInv Σ-assoc-Iso _ = refl
  leftInv Σ-assoc-Iso _  = refl

  unquoteDecl Σ-assoc-≃ = declStrictIsoToEquiv Σ-assoc-≃ Σ-assoc-Iso

  Σ-Π-Iso : Iso ((a : A) → Σ[ b ∈ B a ] C a b) (Σ[ f ∈ ((a : A) → B a) ] ∀ a → C a (f a))
  fun Σ-Π-Iso f         = (fst ∘ f , snd ∘ f)
  inv Σ-Π-Iso (f , g) x = (f x , g x)
  rightInv Σ-Π-Iso _    = refl
  leftInv Σ-Π-Iso _     = refl

  unquoteDecl Σ-Π-≃ = declStrictIsoToEquiv Σ-Π-≃ Σ-Π-Iso

Σ-cong-iso-fst : (isom : Iso A A') → Iso (Σ A (B ∘ fun isom)) (Σ A' B)
fun (Σ-cong-iso-fst isom) x = fun isom (x .fst) , x .snd
inv (Σ-cong-iso-fst {B = B} isom) x = inv isom (x .fst) , subst B (sym (ε (x .fst))) (x .snd)
  where
  ε = isHAEquiv.rinv (snd (iso→HAEquiv isom))
rightInv (Σ-cong-iso-fst {B = B} isom) (x , y) = ΣPathP (ε x , toPathP goal)
  where
  ε = isHAEquiv.rinv (snd (iso→HAEquiv isom))
  goal : subst B (ε x) (subst B (sym (ε x)) y) ≡ y
  goal = sym (substComposite B (sym (ε x)) (ε x) y)
      ∙∙ cong (λ x → subst B x y) (lCancel (ε x))
      ∙∙ substRefl {B = B} y
leftInv (Σ-cong-iso-fst {A = A} {B = B} isom) (x , y) = ΣPathP (leftInv isom x , toPathP goal)
  where
  ε = isHAEquiv.rinv (snd (iso→HAEquiv isom))
  γ = isHAEquiv.com (snd (iso→HAEquiv isom))

  lem : (x : A) → sym (ε (fun isom x)) ∙ cong (fun isom) (leftInv isom x) ≡ refl
  lem x = cong (λ a → sym (ε (fun isom x)) ∙ a) (γ x) ∙ lCancel (ε (fun isom x))

  goal : subst B (cong (fun isom) (leftInv isom x)) (subst B (sym (ε (fun isom x))) y) ≡ y
  goal = sym (substComposite B (sym (ε (fun isom x))) (cong (fun isom) (leftInv isom x)) y)
      ∙∙ cong (λ a → subst B a y) (lem x)
      ∙∙ substRefl {B = B} y

Σ-cong-equiv-fst : (e : A ≃ A') → Σ A (B ∘ equivFun e) ≃ Σ A' B
-- we could just do this:
-- Σ-cong-equiv-fst e = isoToEquiv (Σ-cong-iso-fst (equivToIso e))
-- but the following reduces slightly better
Σ-cong-equiv-fst {A = A} {A' = A'} {B = B} e = intro , isEqIntro
 where
  intro : Σ A (B ∘ equivFun e) → Σ A' B
  intro (a , b) = equivFun e a , b
  isEqIntro : isEquiv intro
  isEqIntro .equiv-proof x = ctr , isCtr where
    PB : ∀ {x y} → x ≡ y → B x → B y → Type _
    PB p = PathP (λ i → B (p i))

    open Σ x renaming (fst to a'; snd to b)
    open Σ (equivCtr e a') renaming (fst to ctrA; snd to α)
    ctrB : B (equivFun e ctrA)
    ctrB = subst B (sym α) b
    ctrP : PB α ctrB b
    ctrP = symP (transport-filler (λ i → B (sym α i)) b)
    ctr : fiber intro x
    ctr = (ctrA , ctrB) , ΣPathP (α , ctrP)

    isCtr : ∀ y → ctr ≡ y
    isCtr ((r , s) , p) = λ i → (a≡r i , b!≡s i) , ΣPathP (α≡ρ i , coh i) where
      open PathPΣ p renaming (fst to ρ; snd to σ)
      open PathPΣ (equivCtrPath e a' (r , ρ)) renaming (fst to a≡r; snd to α≡ρ)

      b!≡s : PB (cong (equivFun e) a≡r) ctrB s
      b!≡s i = comp (λ k → B (α≡ρ i (~ k))) (λ k → (λ
        { (i = i0) → ctrP (~ k)
        ; (i = i1) → σ (~ k)
        })) b

      coh : PathP (λ i → PB (α≡ρ i) (b!≡s i) b) ctrP σ
      coh i j = fill (λ k → B (α≡ρ i (~ k))) (λ k → (λ
        { (i = i0) → ctrP (~ k)
        ; (i = i1) → σ (~ k)
        })) (inS b) (~ j)

Σ-cong-fst : (p : A ≡ A') → Σ A (B ∘ transport p) ≡ Σ A' B
Σ-cong-fst {B = B} p i = Σ (p i) (B ∘ transp (λ j → p (i ∨ j)) i)

Σ-cong-iso-snd : ((x : A) → Iso (B x) (B' x)) → Iso (Σ A B) (Σ A B')
fun (Σ-cong-iso-snd isom) (x , y) = x , fun (isom x) y
inv (Σ-cong-iso-snd isom) (x , y') = x , inv (isom x) y'
rightInv (Σ-cong-iso-snd isom) (x , y) = ΣPathP (refl , rightInv (isom x) y)
leftInv (Σ-cong-iso-snd isom) (x , y') = ΣPathP (refl , leftInv (isom x) y')

Σ-cong-equiv-snd : (∀ a → B a ≃ B' a) → Σ A B ≃ Σ A B'
Σ-cong-equiv-snd h = isoToEquiv (Σ-cong-iso-snd (equivToIso ∘ h))

Σ-cong-snd : ((x : A) → B x ≡ B' x) → Σ A B ≡ Σ A B'
Σ-cong-snd {A = A} p i = Σ[ x ∈ A ] (p x i)

Σ-cong-iso : (isom : Iso A A')
           → ((x : A) → Iso (B x) (B' (fun isom x)))
           → Iso (Σ A B) (Σ A' B')
Σ-cong-iso isom isom' = compIso (Σ-cong-iso-snd isom') (Σ-cong-iso-fst isom)

Σ-cong-equiv : (e : A ≃ A')
             → ((x : A) → B x ≃ B' (equivFun e x))
             → Σ A B ≃ Σ A' B'
Σ-cong-equiv e e' = isoToEquiv (Σ-cong-iso (equivToIso e) (equivToIso ∘ e'))

Σ-cong' : (p : A ≡ A') → PathP (λ i → p i → Type ℓ') B B' → Σ A B ≡ Σ A' B'
Σ-cong' p p' = cong₂ (λ (A : Type _) (B : A → Type _) → Σ A B) p p'

-- Alternative version for path in Σ-types, as in the HoTT book

ΣPathTransport : (a b : Σ A B) → Type _
ΣPathTransport {B = B} a b = Σ[ p ∈ (fst a ≡ fst b) ] transport (λ i → B (p i)) (snd a) ≡ snd b

IsoΣPathTransportPathΣ : (a b : Σ A B) → Iso (ΣPathTransport a b) (a ≡ b)
IsoΣPathTransportPathΣ {B = B} a b = compIso (Σ-cong-iso-snd (λ p → invIso (equivToIso (PathP≃Path (λ i → B (p i)) _ _))))
         ΣPathIsoPathΣ

ΣPathTransport≃PathΣ : (a b : Σ A B) → ΣPathTransport a b ≃ (a ≡ b)
ΣPathTransport≃PathΣ {B = B} a b = isoToEquiv (IsoΣPathTransportPathΣ a b)

ΣPathTransport→PathΣ : (a b : Σ A B) → ΣPathTransport a b → (a ≡ b)
ΣPathTransport→PathΣ a b = Iso.fun (IsoΣPathTransportPathΣ a b)

PathΣ→ΣPathTransport : (a b : Σ A B) → (a ≡ b) → ΣPathTransport a b
PathΣ→ΣPathTransport a b = Iso.inv (IsoΣPathTransportPathΣ a b)

ΣPathTransport≡PathΣ : (a b : Σ A B) → ΣPathTransport a b ≡ (a ≡ b)
ΣPathTransport≡PathΣ a b = ua (ΣPathTransport≃PathΣ a b)

Σ-contractFst : (c : isContr A) → Σ A B ≃ B (c .fst)
Σ-contractFst {B = B} c = isoToEquiv isom
  where
  isom : Iso _ _
  isom .fun (a , b) = subst B (sym (c .snd a)) b
  isom .inv b = (c .fst , b)
  isom .rightInv b =
    cong (λ p → subst B p b) (isProp→isSet (isContr→isProp c) _ _ _ _) ∙ transportRefl _
  isom .leftInv (a , b) =
    ΣPathTransport≃PathΣ _ _ .fst (c .snd a , transportTransport⁻ (cong B (c .snd a)) _)

-- a special case of the above
module _ (A : Unit → Type ℓ) where
  ΣUnit : Σ Unit A ≃ A tt
  unquoteDef ΣUnit = defStrictEquiv ΣUnit snd (λ { x → (tt , x) })

Σ-contractSnd : ((a : A) → isContr (B a)) → Σ A B ≃ A
Σ-contractSnd c = isoToEquiv isom
  where
  isom : Iso _ _
  isom .fun = fst
  isom .inv a = a , c a .fst
  isom .rightInv _ = refl
  isom .leftInv (a , b) = cong (a ,_) (c a .snd b)

isEmbeddingFstΣProp : ((x : A) → isProp (B x))
                    → {u v : Σ A B}
                    → isEquiv (λ (p : u ≡ v) → cong fst p)
isEmbeddingFstΣProp {B = B} pB {u = u} {v = v} .equiv-proof x = ctr , isCtr
  where
  ctrP : u ≡ v
  ctrP = ΣPathP (x , isProp→PathP (λ _ → pB _) _ _)
  ctr  : fiber (λ (p : u ≡ v) → cong fst p) x
  ctr  = ctrP , refl

  isCtr : ∀ z → ctr ≡ z
  isCtr (z , p) = ΣPathP (ctrP≡ , cong (sym ∘ snd) fzsingl) where
    fzsingl : Path (singl x) (x , refl) (cong fst z , sym p)
    fzsingl = isContrSingl x .snd (cong fst z , sym p)
    ctrSnd : SquareP (λ i j → B (fzsingl i .fst j)) (cong snd ctrP) (cong snd z) _ _
    ctrSnd = isProp→SquareP (λ _ _ → pB _) _ _ _ _
    ctrP≡ : ctrP ≡ z
    ctrP≡ i = ΣPathP (fzsingl i .fst , ctrSnd i)

Σ≡PropEquiv : ((x : A) → isProp (B x)) → {u v : Σ A B}
            → (u .fst ≡ v .fst) ≃ (u ≡ v)
Σ≡PropEquiv pB = invEquiv (_ , isEmbeddingFstΣProp pB)

Σ≡Prop : ((x : A) → isProp (B x)) → {u v : Σ A B}
       → (p : u .fst ≡ v .fst) → u ≡ v
Σ≡Prop pB p = equivFun (Σ≡PropEquiv pB) p

≃-× : ∀ {ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''} → A ≃ C → B ≃ D → A × B ≃ C × D
≃-× eq1 eq2 =
    map-× (fst eq1) (fst eq2)
  , record
     { equiv-proof
       = λ {(c , d) → ((eq1⁻ c .fst .fst
                        , eq2⁻ d .fst .fst)
                          , ≡-× (eq1⁻ c .fst .snd)
                                (eq2⁻ d .fst .snd))
                     , λ {((a , b) , p) → ΣPathP (≡-× (cong fst (eq1⁻ c .snd (a , cong fst p)))
                                                       (cong fst (eq2⁻ d .snd (b , cong snd p)))
                                                , λ i → ≡-× (snd ((eq1⁻ c .snd (a , cong fst p)) i))
                                                             (snd ((eq2⁻ d .snd (b , cong snd p)) i)))}}}
  where
  eq1⁻ = equiv-proof (eq1 .snd)
  eq2⁻ = equiv-proof (eq2 .snd)

{- Some simple ismorphisms -}

prodIso : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''}
       → Iso A C
       → Iso B D
       → Iso (A × B) (C × D)
Iso.fun (prodIso iAC iBD) (a , b) = (Iso.fun iAC a) , Iso.fun iBD b
Iso.inv (prodIso iAC iBD) (c , d) = (Iso.inv iAC c) , Iso.inv iBD d
Iso.rightInv (prodIso iAC iBD) (c , d) = ΣPathP ((Iso.rightInv iAC c) , (Iso.rightInv iBD d))
Iso.leftInv (prodIso iAC iBD) (a , b) = ΣPathP ((Iso.leftInv iAC a) , (Iso.leftInv iBD b))

toProdIso : {B C : A → Type ℓ}
          → Iso ((a : A) → B a × C a) (((a : A) → B a) × ((a : A) → C a))
Iso.fun toProdIso = λ f → (λ a → fst (f a)) , (λ a → snd (f a))
Iso.inv toProdIso (f , g) = λ a → (f a) , (g a)
Iso.rightInv toProdIso (f , g) = refl
Iso.leftInv toProdIso b = refl

module _ {A : Type ℓ} {B : A → Type ℓ'} {C : ∀ a → B a → Type ℓ''} where
  curryIso : Iso (((a , b) : Σ A B) → C a b) ((a : A) → (b : B a) → C a b)
  Iso.fun curryIso f a b = f (a , b)
  Iso.inv curryIso f a = f (fst a) (snd a)
  Iso.rightInv curryIso a = refl
  Iso.leftInv curryIso f = refl

  unquoteDecl curryEquiv = declStrictIsoToEquiv curryEquiv curryIso

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --guardedness --safe #-}

module Cubical.Codata.M.AsLimit.Container where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv using (_≃_)
open import Cubical.Foundations.Function using (_∘_)

open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.Data.Nat as ℕ using (ℕ ; suc ; _+_ )

open import Cubical.Foundations.Transport

open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open import Cubical.Data.Sum

open import Cubical.Foundations.Structure

open import Cubical.Codata.M.AsLimit.helper

-------------------------------------
-- Container and Container Functor --
-------------------------------------

-- Σ[ A ∈ (Type ℓ) ] (A → Type ℓ)
Container : ∀ ℓ -> Type (ℓ-suc ℓ)
Container ℓ = TypeWithStr ℓ (λ x → x → Type ℓ)

-- Polynomial functor (P₀ , P₁)  defined over a container
-- https://ncatlab.org/nlab/show/polynomial+functor

-- P₀ object part of functor
P₀ : ∀ {ℓ} (S : Container ℓ) -> Type ℓ -> Type ℓ
P₀ (A , B) X  = Σ[ a ∈ A ] (B a -> X)

-- P₁ morphism part of functor
P₁ : ∀ {ℓ} {S : Container ℓ} {X Y} (f : X -> Y) -> P₀ S X -> P₀ S Y
P₁ {S = S} f = λ { (a , g) ->  a , f ∘ g }

-----------------------
-- Chains and Limits --
-----------------------

record Chain ℓ : Type (ℓ-suc ℓ) where
  constructor _,,_
  field
    X : ℕ -> Type ℓ
    π : {n : ℕ} -> X (suc n) -> X n

open Chain public

limit-of-chain : ∀ {ℓ} -> Chain ℓ → Type ℓ
limit-of-chain (x ,, pi) = Σ[ x ∈ ((n : ℕ) → x n) ] ((n : ℕ) → pi {n = n} (x (suc n)) ≡ x n)

shift-chain : ∀ {ℓ} -> Chain ℓ -> Chain ℓ
shift-chain = λ X,π -> ((λ x → X X,π (suc x)) ,, λ {n} → π X,π {suc n})

------------------------------------------------------
-- Limit type of a Container , and Shift of a Limit --
------------------------------------------------------

Wₙ : ∀ {ℓ} -> Container ℓ -> ℕ -> Type ℓ
Wₙ S 0 = Lift Unit
Wₙ S (suc n) = P₀ S (Wₙ S n)

πₙ : ∀ {ℓ} -> (S : Container ℓ) -> {n : ℕ} -> Wₙ S (suc n) -> Wₙ S n
πₙ {ℓ} S {0} _ = lift tt
πₙ S {suc n} = P₁ (πₙ S {n})

sequence : ∀ {ℓ} -> Container ℓ -> Chain ℓ
X (sequence S) n = Wₙ S n
π (sequence S) {n} = πₙ S {n}

PX,Pπ : ∀ {ℓ} (S : Container ℓ) -> Chain ℓ
PX,Pπ {ℓ} S =
  (λ n → P₀ S (X (sequence S) n)) ,,
  (λ {n : ℕ} x → P₁ (λ z → z) (π (sequence S) {n = suc n} x ))

-----------------------------------
-- M type is limit of a sequence --
-----------------------------------

M : ∀ {ℓ} -> Container ℓ → Type ℓ
M = limit-of-chain ∘ sequence

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Issue1078.A where

open import Common.Level using (Level)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- This module contains various line-ending characters in order
-- to test that they don't affect module source hash calculation.
module C where
-- CR --
--
-- LF --
--
-- CRLF --
--
-- LFCR --

--
-- FF ----
-- NEXT LINE ----
-- LINE SEPARATOR --
--
-- PARAGRAPH SEPARATOR --
--


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Unit

module Oscar.Class.SimilaritySingleton where

module SimilaritySingleton
  {𝔞} {𝔄 : Ø 𝔞}
  {𝔟} {𝔅 : Ø 𝔟}
  {𝔣} {𝔉 : Ø 𝔣}
  {𝔞̇ 𝔟̇}
  (∼₁ : Ø 𝔞̇)
  (_∼₂_ : 𝔅 → 𝔅 → Ø 𝔟̇) (let _∼₂_ = _∼₂_; infix 4 _∼₂_)
  (_◃_ : 𝔉 → 𝔄 → 𝔅) (let _◃_ = _◃_; infix 16 _◃_)
  (x y : 𝔄)
  (f : 𝔉)
  = ℭLASS (_◃_ , _∼₂_ , x , y) (∼₁ → f ◃ x ∼₂ f ◃ y)

module _
  {𝔞} {𝔄 : Ø 𝔞}
  {𝔟} {𝔅 : Ø 𝔟}
  {𝔣} {𝔉 : Ø 𝔣}
  {𝔞̇ 𝔟̇}
  {∼₁ : Ø 𝔞̇}
  {_∼₂_ : 𝔅 → 𝔅 → Ø 𝔟̇} (let _∼₂_ = _∼₂_; infix 4 _∼₂_)
  {_◃_ : 𝔉 → 𝔄 → 𝔅} (let _◃_ = _◃_; infix 16 _◃_)
  {x y : 𝔄}
  {f : 𝔉}
  where
  similaritySingleton = SimilaritySingleton.method ∼₁ _∼₂_ _◃_ x y f
  module _ ⦃ _ : SimilaritySingleton.class ∼₁ _∼₂_ _◃_ x y f ⦄ where
    instance
      toUnit : Unit.class (∼₁ → f ◃ x ∼₂ f ◃ y)
      toUnit .⋆ = similaritySingleton


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

open import HoTT
import homotopy.RelativelyConstantToSetExtendsViaSurjection as SurjExt

module homotopy.VanKampen {i j k l}
  (span : Span {i} {j} {k})
  {D : Type l} (h : D → Span.C span) (h-is-surj : is-surj h) where

  open Span span
  open import homotopy.vankampen.CodeAP span h h-is-surj
  open import homotopy.vankampen.CodeBP span h h-is-surj
  open import homotopy.vankampen.Code span h h-is-surj

  -- favonia: [pPP] means path from [P] to [P].
  encode-idp : ∀ p → code p p
  encode-idp = Pushout-elim {P = λ p → code p p}
    (λ a → q[ ⟧a idp₀ ]) (λ b → q[ ⟧b idp₀ ]) lemma where
    abstract
      lemma : ∀ c → q[ ⟧a idp₀ ] == q[ ⟧b idp₀ ] [ (λ p → code p p) ↓ glue c ]
      lemma = SurjExt.ext
        {{↓-preserves-level ⟨⟩}}
        h h-is-surj
        (λ d → from-transp (λ p → code p p) (glue (h d)) $
          transport (λ p → code p p) (glue (h d)) q[ ⟧a idp₀ ]
            =⟨ ap (λ pPP → coe pPP q[ pc-a idp₀ ]) ((! (ap2-diag code (glue (h d)))) ∙ ap2-out code (glue (h d)) (glue (h d))) ⟩
          coe (ap (λ p₀ → code p₀ (left (f (h d)))) (glue (h d)) ∙ ap (codeBP (g (h d))) (glue (h d))) q[ ⟧a idp₀ ]
            =⟨ coe-∙ (ap (λ p₀ → code p₀ (left (f (h d)))) (glue (h d))) (ap (codeBP (g (h d))) (glue (h d))) q[ pc-a idp₀ ] ⟩
          transport (codeBP (g (h d))) (glue (h d)) (transport (λ p₀ → code p₀ (left (f (h d)))) (glue (h d)) q[ ⟧a idp₀ ])
            =⟨ transp-cPA-glue d (⟧a idp₀) |in-ctx transport (λ p₁ → code (right (g (h d))) p₁) (glue (h d)) ⟩
          transport (codeBP (g (h d))) (glue (h d)) q[ ⟧b idp₀ bb⟦ d ⟧a idp₀ ]
            =⟨ transp-cBP-glue d (⟧b idp₀ bb⟦ d ⟧a idp₀) ⟩
          q[ ⟧b idp₀ bb⟦ d ⟧a idp₀ ba⟦ d ⟧b idp₀ ]
            =⟨ quot-rel (pcBBr-idp₀-idp₀ (pc-b idp₀)) ⟩
          q[ ⟧b idp₀ ]
            =∎)
        (λ _ _ _ → prop-has-all-paths-↓ {{↓-level ⟨⟩}})

  encode : ∀ {p₀ p₁} → p₀ =₀ p₁ → code p₀ p₁
  encode {p₀} {p₁} pPP = transport₀ (code p₀) {{code-is-set {p₀} {p₁}}} pPP (encode-idp p₀)

  abstract
    decode-encode-idp : ∀ p → decode {p} {p} (encode-idp p) == idp₀
    decode-encode-idp = Pushout-elim
      {P = λ p → decode {p} {p} (encode-idp p) == idp₀}
      (λ _ → idp) (λ _ → idp)
      (λ c → prop-has-all-paths-↓)

    decode-encode' : ∀ {p₀ p₁} (pPP : p₀ == p₁) → decode {p₀} {p₁} (encode [ pPP ]) == [ pPP ]
    decode-encode' idp = decode-encode-idp _

    decode-encode : ∀ {p₀ p₁} (pPP : p₀ =₀ p₁) → decode {p₀} {p₁} (encode pPP) == pPP
    decode-encode = Trunc-elim decode-encode'

  abstract
    transp-idcAA-r : ∀ {a₀ a₁} (p : a₀ == a₁) -- [idc] = identity code
      → transport (codeAA a₀) p q[ ⟧a idp₀ ] == q[ ⟧a [ p ] ]
    transp-idcAA-r idp = idp

    encode-decodeAA : ∀ {a₀ a₁} (c : precodeAA a₀ a₁)
      → encode (decodeAA q[ c ]) == q[ c ]
    encode-decodeAB : ∀ {a₀ b₁} (c : precodeAB a₀ b₁)
      → encode (decodeAB q[ c ]) == q[ c ]
    encode-decodeAA {a₀} (pc-a pA) = Trunc-elim
      {P = λ pA → encode (decodeAA q[ ⟧a pA ]) == q[ ⟧a pA ]}
      (λ pA →
        transport (codeAP a₀) (ap left pA) q[ ⟧a idp₀ ]
          =⟨ ap (λ e → coe e q[ ⟧a idp₀ ]) (∘-ap (codeAP a₀) left pA) ⟩
        transport (codeAA a₀) pA q[ ⟧a idp₀ ]
          =⟨ transp-idcAA-r pA ⟩
        q[ ⟧a [ pA ] ]
          =∎)
      pA
    encode-decodeAA {a₀} (pc-aba d pc pA) = Trunc-elim
      {P = λ pA → encode (decodeAA q[ pc ab⟦ d ⟧a pA ]) == q[ pc ab⟦ d ⟧a pA ]}
      (λ pA →
        encode (decodeAB q[ pc ] ∙₀' [ ! (glue (h d)) ∙' ap left pA ])
          =⟨ transp₀-∙₀' {{λ {p₁} → code-is-set {left a₀} {p₁}}} (decodeAB q[ pc ]) [ ! (glue (h d)) ∙' ap left pA ] (encode-idp (left a₀)) ⟩
        transport (codeAP a₀) (! (glue (h d)) ∙' ap left pA) (encode (decodeAB q[ pc ]))
          =⟨ ap (transport (codeAP a₀) (! (glue (h d)) ∙' ap left pA)) (encode-decodeAB pc) ⟩
        transport (codeAP a₀) (! (glue (h d)) ∙' ap left pA) q[ pc ]
          =⟨ transp-∙' {B = codeAP a₀} (! (glue (h d))) (ap left pA) q[ pc ] ⟩
        transport (codeAP a₀) (ap left pA) (transport (codeAP a₀) (! (glue (h d))) q[ pc ])
          =⟨ ap (transport (codeAP a₀) (ap left pA)) (transp-cAP-!glue d pc) ⟩
        transport (codeAP a₀) (ap left pA) q[ pc ab⟦ d ⟧a idp₀ ]
          =⟨ ap (λ e → coe e q[ pc ab⟦ d ⟧a idp₀ ]) (∘-ap (codeAP a₀) left pA) ⟩
        transport (codeAA a₀) pA q[ pc ab⟦ d ⟧a idp₀ ]
          =⟨ transp-cAA-r d pA (pc ab⟦ d ⟧a idp₀) ⟩
        q[ pc ab⟦ d ⟧a idp₀ aa⟦ d ⟧b idp₀ ab⟦ d ⟧a [ pA ] ]
          =⟨ quot-rel (pcAAr-cong (pcABr-idp₀-idp₀ pc) [ pA ]) ⟩
        q[ pc ab⟦ d ⟧a [ pA ] ]
          =∎)
      pA
    encode-decodeAB {a₀} (pc-aab d pc pB) = Trunc-elim
      {P = λ pB → encode (decodeAB q[ pc aa⟦ d ⟧b pB ]) == q[ pc aa⟦ d ⟧b pB ]}
      (λ pB →
        encode (decodeAA q[ pc ] ∙₀' [ glue (h d) ∙' ap right pB ])
          =⟨ transp₀-∙₀' {{λ {p₁} → code-is-set {left a₀} {p₁}}} (decodeAA q[ pc ]) [ glue (h d) ∙' ap right pB ] (encode-idp (left a₀)) ⟩
        transport (codeAP a₀) (glue (h d) ∙' ap right pB) (encode (decodeAA q[ pc ]))
          =⟨ ap (transport (codeAP a₀) (glue (h d) ∙' ap right pB)) (encode-decodeAA pc) ⟩
        transport (codeAP a₀) (glue (h d) ∙' ap right pB) q[ pc ]
          =⟨ transp-∙' {B = codeAP a₀} (glue (h d)) (ap right pB) q[ pc ] ⟩
        transport (codeAP a₀) (ap right pB) (transport (codeAP a₀) (glue (h d)) q[ pc ])
          =⟨ ap (transport (codeAP a₀) (ap right pB)) (transp-cAP-glue d pc) ⟩
        transport (codeAP a₀) (ap right pB) q[ pc aa⟦ d ⟧b idp₀ ]
          =⟨ ap (λ e → coe e q[ pc aa⟦ d ⟧b idp₀ ]) (∘-ap (codeAP a₀) right pB) ⟩
        transport (codeAB a₀) pB q[ pc aa⟦ d ⟧b idp₀ ]
          =⟨ transp-cAB-r d pB (pc aa⟦ d ⟧b idp₀) ⟩
        q[ pc aa⟦ d ⟧b idp₀ ab⟦ d ⟧a idp₀ aa⟦ d ⟧b [ pB ] ]
          =⟨ quot-rel (pcABr-cong (pcAAr-idp₀-idp₀ pc) [ pB ]) ⟩
        q[ pc aa⟦ d ⟧b [ pB ] ]
          =∎)
      pB

  abstract
    transp-idcBB-r : ∀ {b₀ b₁} (p : b₀ == b₁) -- [idc] = identity code
      → transport (codeBB b₀) p q[ ⟧b idp₀ ] == q[ ⟧b [ p ] ]
    transp-idcBB-r idp = idp

    encode-decodeBA : ∀ {b₀ a₁} (c : precodeBA b₀ a₁)
      → encode (decodeBA q[ c ]) == q[ c ]
    encode-decodeBB : ∀ {b₀ b₁} (c : precodeBB b₀ b₁)
      → encode (decodeBB q[ c ]) == q[ c ]
    encode-decodeBA {b₀} (pc-bba d pc pA) = Trunc-elim
      {P = λ pA → encode (decodeBA q[ pc bb⟦ d ⟧a pA ]) == q[ pc bb⟦ d ⟧a pA ]}
      (λ pA →
        encode (decodeBB q[ pc ] ∙₀' [ ! (glue (h d)) ∙' ap left pA ])
          =⟨ transp₀-∙₀' {{λ {p₁} → code-is-set {right b₀} {p₁}}} (decodeBB q[ pc ]) [ ! (glue (h d)) ∙' ap left pA ] (encode-idp (right b₀)) ⟩
        transport (codeBP b₀) (! (glue (h d)) ∙' ap left pA) (encode (decodeBB q[ pc ]))
          =⟨ ap (transport (codeBP b₀) (! (glue (h d)) ∙' ap left pA)) (encode-decodeBB pc) ⟩
        transport (codeBP b₀) (! (glue (h d)) ∙' ap left pA) q[ pc ]
          =⟨ transp-∙' {B = codeBP b₀} (! (glue (h d))) (ap left pA) q[ pc ] ⟩
        transport (codeBP b₀) (ap left pA) (transport (codeBP b₀) (! (glue (h d))) q[ pc ])
          =⟨ ap (transport (codeBP b₀) (ap left pA)) (transp-cBP-!glue d pc) ⟩
        transport (codeBP b₀) (ap left pA) q[ pc bb⟦ d ⟧a idp₀ ]
          =⟨ ap (λ e → coe e q[ pc bb⟦ d ⟧a idp₀ ]) (∘-ap (codeBP b₀) left pA) ⟩
        transport (codeBA b₀) pA q[ pc bb⟦ d ⟧a idp₀ ]
          =⟨ transp-cBA-r d pA (pc bb⟦ d ⟧a idp₀) ⟩
        q[ pc bb⟦ d ⟧a idp₀ ba⟦ d ⟧b idp₀ bb⟦ d ⟧a [ pA ] ]
          =⟨ quot-rel (pcBAr-cong (pcBBr-idp₀-idp₀ pc) [ pA ]) ⟩
        q[ pc bb⟦ d ⟧a [ pA ] ]
          =∎)
      pA
    encode-decodeBB {b₀} (pc-b pB) = Trunc-elim
      {P = λ pB → encode (decodeBB q[ ⟧b pB ]) == q[ ⟧b pB ]}
      (λ pB →
        transport (codeBP b₀) (ap right pB) q[ ⟧b idp₀ ]
          =⟨ ap (λ e → coe e q[ ⟧b idp₀ ]) (∘-ap (codeBP b₀) right pB) ⟩
        transport (codeBB b₀) pB q[ ⟧b idp₀ ]
          =⟨ transp-idcBB-r pB ⟩
        q[ ⟧b [ pB ] ]
          =∎)
      pB
    encode-decodeBB {b₀} (pc-bab d pc pB) = Trunc-elim
      {P = λ pB → encode (decodeBB q[ pc ba⟦ d ⟧b pB ]) == q[ pc ba⟦ d ⟧b pB ]}
      (λ pB →
        encode (decodeBA q[ pc ] ∙₀' [ glue (h d) ∙' ap right pB ])
          =⟨ transp₀-∙₀' {{λ {p₁} → code-is-set {right b₀} {p₁}}} (decodeBA q[ pc ]) [ glue (h d) ∙' ap right pB ] (encode-idp (right b₀)) ⟩
        transport (codeBP b₀) (glue (h d) ∙' ap right pB) (encode (decodeBA q[ pc ]))
          =⟨ ap (transport (codeBP b₀) (glue (h d) ∙' ap right pB)) (encode-decodeBA pc) ⟩
        transport (codeBP b₀) (glue (h d) ∙' ap right pB) q[ pc ]
          =⟨ transp-∙' {B = codeBP b₀} (glue (h d)) (ap right pB) q[ pc ] ⟩
        transport (codeBP b₀) (ap right pB) (transport (codeBP b₀) (glue (h d)) q[ pc ])
          =⟨ ap (transport (codeBP b₀) (ap right pB)) (transp-cBP-glue d pc) ⟩
        transport (codeBP b₀) (ap right pB) q[ pc ba⟦ d ⟧b idp₀ ]
          =⟨ ap (λ e → coe e q[ pc ba⟦ d ⟧b idp₀ ]) (∘-ap (codeBP b₀) right pB) ⟩
        transport (codeBB b₀) pB q[ pc ba⟦ d ⟧b idp₀ ]
          =⟨ transp-cBB-r d pB (pc ba⟦ d ⟧b idp₀) ⟩
        q[ pc ba⟦ d ⟧b idp₀ bb⟦ d ⟧a idp₀ ba⟦ d ⟧b [ pB ] ]
          =⟨ quot-rel (pcBBr-cong (pcBAr-idp₀-idp₀ pc) [ pB ]) ⟩
        q[ pc ba⟦ d ⟧b [ pB ] ]
          =∎)
      pB

  abstract
    encode-decode : ∀ {p₀ p₁} (cPP : code p₀ p₁)
      → encode {p₀} {p₁} (decode {p₀} {p₁} cPP) == cPP
    encode-decode {p₀} {p₁} = Pushout-elim
      {P = λ p₀ → ∀ p₁ → (cPP : code p₀ p₁) → encode (decode {p₀} {p₁} cPP) == cPP}
      (λ a₀ → Pushout-elim
        (λ a₁ → SetQuot-elim
          {P = λ cPP → encode (decodeAA cPP) == cPP}
          (encode-decodeAA {a₀} {a₁})
          (λ _ → prop-has-all-paths-↓))
        (λ b₁ → SetQuot-elim
          {P = λ cPP → encode (decodeAB cPP) == cPP}
          (encode-decodeAB {a₀} {b₁})
          (λ _ → prop-has-all-paths-↓))
        (λ _ → prop-has-all-paths-↓))
      (λ b₀ → Pushout-elim
        (λ a₁ → SetQuot-elim
          {P = λ cPP → encode (decodeBA cPP) == cPP}
          (encode-decodeBA {b₀} {a₁})
          (λ _ → prop-has-all-paths-↓))
        (λ b₁ → SetQuot-elim
          {P = λ cPP → encode (decodeBB cPP) == cPP}
          (encode-decodeBB {b₀} {b₁})
          (λ _ → prop-has-all-paths-↓))
        (λ _ → prop-has-all-paths-↓))
      (λ _ → prop-has-all-paths-↓ {{Π-level (λ p₁ → Π-level (λ cPP → has-level-apply (codeBP-is-set {p₁ = p₁}) _ _))}})
      p₀ p₁

  vankampen : ∀ p₀ p₁ → (p₀ =₀ p₁) ≃ code p₀ p₁
  vankampen p₀ p₁ = equiv (encode {p₀} {p₁}) (decode {p₀} {p₁}) (encode-decode {p₀} {p₁}) (decode-encode {p₀} {p₁})

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module evenodd where

mutual
  data Even : Set where
    Z  : Even
    S  : Odd -> Even

  data Odd : Set where
    S' : Even -> Odd

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Predicate lifting for refinement types
------------------------------------------------------------------------

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

module Data.Refinement.Relation.Unary.All where

open import Level
open import Data.Refinement
open import Function.Base
open import Relation.Unary

private
  variable
    a b p q : Level
    A : Set a
    B : Set b

module _ {P : A → Set p} where

  All : (A → Set q) → Refinement A P → Set q
  All P (a , _) = P a


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

   Copyright (c) 2020, 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 Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle sha256 sha256-cr
open        EpochConfig
open import LibraBFT.Yasm.Base (ℓ+1 0ℓ) EpochConfig epochId authorsN

-- In this module, we instantiate the system model with parameters to
-- model a system using the simple implementation model we have so
-- far, which aims to obey the VotesOnceRule, but not LockedRoundRule
-- yet.  This will evolve as we build out a model of a real
-- implementation.

module LibraBFT.Concrete.System.Parameters where
 ConcSysParms : SystemParameters
 ConcSysParms = mkSysParms
                 NodeId
                 _≟NodeId_
                 EventProcessor
                 fakeEP
                 NetworkMsg
                 Vote
                 sig-Vote
                 _⊂Msg_
                 (_^∙ vEpoch)
                 initialEventProcessorAndMessages
                 peerStepWrapper

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
module Ag11 where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_)
open import Ag09 using (_≃_; extensionality)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contraposition)
open import Ag03 using (_⟨_)

⟨-irreflexive : ∀ (n : ℕ) → ¬ (n ⟨ n)
⟨-irreflexive (suc n) (_⟨_.s⟨s H) = ⟨-irreflexive n H

⊎-dual-× : ∀ {A B : Set} → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
⊎-dual-× =
  record
  { to = λ z → (λ x → z (inj₁ x)) Data.Product., (λ x → z (inj₂ x))
  ; from = λ{ (fst Data.Product., snd) → λ {(inj₁ x) → fst x; (inj₂ y) → snd y} }
  ; from∘to = λ x → extensionality λ { (inj₁ y) → refl ; (inj₂ z) → refl }
  ; to∘from = λ {(fst Data.Product., snd) → refl}
  }

-- ×-dual-⊎ : ∀ {A B : Set} → ¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
-- ×-dual-⊎ =
--  record
--  { to = λ x → inj₁ λ y → {!!}
--  ; from = λ { (inj₁ x) → λ z → x (Data.Product.proj₁ z) ; (inj₂ y) → λ z → y (Data.Product.proj₂ z)}
--  ; from∘to = {!!}
--  ; to∘from = {!!}
--  }

postulate
  em : ∀ {A : Set} → A ⊎ ¬ A

em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
em-irrefutable k = k (inj₂ (λ x → k (inj₁ x)))

postulate
  dne : ∀ {A : Set} → ¬ ¬ A → A

em-dne : ∀ {A : Set} → (A ⊎ ¬ A) → (¬ ¬ A → A)
em-dne (inj₁ x) ¬¬A = x
em-dne (inj₂ y) ¬¬A = ⊥-elim (¬¬A y)

dne-em : (∀ (A : Set) → ¬ ¬ A → A) → (∀ (A : Set) → A ⊎ ¬ A)
dne-em H = λ a → H (a ⊎ ((x : a) → ⊥)) (λ z → z (inj₂ (λ x → z (inj₁ x))))

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
-- Andreas, Jesper, 2015-07-02 Error in copyScope

{-# OPTIONS -v tc.decl:5 #-} -- KEEP, this forced Agda to look at A.Decls and loop

-- To trigger the bug, it is important that
-- the main module is in a subdirectory of the imported module.
module Issue1597.Main2 where

open import Issue1597   -- external import is needed

module B where
  open A public  -- public is needed

module C = B
  -- hanged when trying to print the Syntax.Abstract.Declarations


text:
------------------------------------------------------------------------
-- Aczel's structure identity principle (for 1-categories), more or
-- less as found in "Homotopy Type Theory: Univalent Foundations of
-- Mathematics" (first edition)
------------------------------------------------------------------------

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

open import Equality

module Structure-identity-principle
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq using (_↔_; Σ-≡,≡↔≡)
open import Category eq
open Derived-definitions-and-properties eq
open import Equality.Decidable-UIP eq
open import Equivalence eq hiding (id; _∘_; inverse; lift-equality)
open import Function-universe eq hiding (id) renaming (_∘_ to _⊚_)
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (id)

-- Standard notions of structure.

record Standard-notion-of-structure
         {c₁ c₂} ℓ₁ ℓ₂ (C : Precategory c₁ c₂) :
         Type (c₁ ⊔ c₂ ⊔ lsuc (ℓ₁ ⊔ ℓ₂)) where
  open Precategory C

  field
    P               : Obj → Type ℓ₁
    H               : ∀ {X Y} (p : P X) (q : P Y) → Hom X Y → Type ℓ₂
    H-prop          : ∀ {X Y} {p : P X} {q : P Y}
                      (f : Hom X Y) → Is-proposition (H p q f)
    H-id            : ∀ {X} {p : P X} → H p p id
    H-∘             : ∀ {X Y Z} {p : P X} {q : P Y} {r : P Z} {f g} →
                      H p q f → H q r g → H p r (g ∙ f)
    H-antisymmetric : ∀ {X} (p q : P X) →
                      H p q id → H q p id → p ≡ q

  -- P constructs sets. (The proof was suggested by Michael Shulman in
  -- a mailing list post.)

  P-set : ∀ A → Is-set (P A)
  P-set A = propositional-identity⇒set
    (λ p q → H p q id × H q p id)
    (λ _ _ → ×-closure 1 (H-prop id) (H-prop id))
    (λ _ → H-id , H-id)
    (λ p q → uncurry (H-antisymmetric p q))

  -- Two Str morphisms (see below) of equal type are equal if their
  -- first components are equal.

  lift-equality : {X Y : ∃ P} {f g : ∃ (H (proj₂ X) (proj₂ Y))} →
                  proj₁ f ≡ proj₁ g → f ≡ g
  lift-equality eq = Σ-≡,≡→≡ eq (H-prop _ _ _)

  -- A derived precategory.

  Str : Precategory (c₁ ⊔ ℓ₁) (c₂ ⊔ ℓ₂)
  Str = record { precategory =
    ∃ P ,
    (λ { (X , p) (Y , q) →
         ∃ (H p q) ,
         Σ-closure 2 Hom-is-set (λ f → mono₁ 1 (H-prop f)) }) ,
    (id , H-id) ,
    (λ { (f , hf) (g , hg) → f ∙ g , H-∘ hg hf }) ,
    lift-equality left-identity ,
    lift-equality right-identity ,
    lift-equality assoc }

  module Str = Precategory Str

  -- A rearrangement lemma.

  proj₁-≡→≅-¹ :
    ∀ {X Y} (X≡Y : X ≡ Y) →
    proj₁ (Str.≡→≅ X≡Y Str.¹) ≡
    elim (λ {X Y} _ → Hom X Y) (λ _ → id) (cong proj₁ X≡Y)
  proj₁-≡→≅-¹ {X , p} = elim¹
    (λ X≡Y → proj₁ (Str.≡→≅ X≡Y Str.¹) ≡
             elim (λ {X Y} _ → Hom X Y) (λ _ → id) (cong proj₁ X≡Y))
    (proj₁ (Str.≡→≅ (refl (X , p)) Str.¹)                               ≡⟨ cong (proj₁ ∘ Str._¹) $ elim-refl (λ {X Y} _ → X Str.≅ Y) _ ⟩
     proj₁ (Str.id {X = X , p})                                         ≡⟨⟩
     id {X = X}                                                         ≡⟨ sym $ elim-refl (λ {X Y} _ → Hom X Y) _ ⟩
     elim (λ {X Y} _ → Hom X Y) (λ _ → id) (refl X)                     ≡⟨ cong (elim (λ {X Y} _ → Hom X Y) _) $ sym $ cong-refl proj₁ ⟩∎
     elim (λ {X Y} _ → Hom X Y) (λ _ → id) (cong proj₁ (refl (X , p)))  ∎)

-- The structure identity principle states that the precategory Str is
-- a category (assuming extensionality).
--
-- The proof below is based on (but not quite identical to) the one in
-- "Homotopy Type Theory: Univalent Foundations of Mathematics" (first
-- edition).

abstract

  structure-identity-principle :
    ∀ {c₁ c₂ ℓ₁ ℓ₂} →
    Extensionality (ℓ₁ ⊔ ℓ₂) (ℓ₁ ⊔ ℓ₂) →
    (C : Category c₁ c₂) →
    (S : Standard-notion-of-structure ℓ₁ ℓ₂ (Category.precategory C)) →
    ∀ {X Y} → Is-equivalence
                (Precategory.≡→≅ (Standard-notion-of-structure.Str S)
                                 {X} {Y})
  structure-identity-principle ext C S =
    Str.≡→≅-equivalence-lemma ≡≃≅ ≡≃≅-refl
    where
    open Standard-notion-of-structure S
    module C = Category C

    -- _≡_ is pointwise equivalent to Str._≅_.

    module ≅HH≃≅ where

      to : ∀ {X Y} {p : P X} {q : P Y} →
           (∃ λ (f : X C.≅ Y) → H p q (f C.¹) × H q p (f C.⁻¹)) →
           (X , p) Str.≅ (Y , q)
      to ((f , f⁻¹ , f∙f⁻¹ , f⁻¹∙f) , Hf , Hf⁻¹) =
        (f , Hf) , (f⁻¹ , Hf⁻¹) ,
        lift-equality f∙f⁻¹ ,
        lift-equality f⁻¹∙f

    ≅HH≃≅ : ∀ {X Y} {p : P X} {q : P Y} →
            (∃ λ (f : X C.≅ Y) → H p q (f C.¹) × H q p (f C.⁻¹)) ≃
            ((X , p) Str.≅ (Y , q))
    ≅HH≃≅ {X} {Y} {p} {q} = ↔⇒≃ (record
      { surjection = record
        { logical-equivalence = record
          { to   = ≅HH≃≅.to
          ; from = from
          }
        ; right-inverse-of = to∘from
        }
      ; left-inverse-of = from∘to
      })
      where
      from : (X , p) Str.≅ (Y , q) →
             ∃ λ (f : X C.≅ Y) → H p q (f C.¹) × H q p (f C.⁻¹)
      from ((f , Hf) , (f⁻¹ , Hf⁻¹) , f∙f⁻¹ , f⁻¹∙f) =
        (f , f⁻¹ , cong proj₁ f∙f⁻¹ , cong proj₁ f⁻¹∙f) , Hf , Hf⁻¹

      to∘from : ∀ p → ≅HH≃≅.to (from p) ≡ p
      to∘from ((f , Hf) , (f⁻¹ , Hf⁻¹) , f∙f⁻¹ , f⁻¹∙f) =
        cong₂ (λ f∙f⁻¹ f⁻¹∙f →
                 (f , Hf) , (f⁻¹ , Hf⁻¹) , f∙f⁻¹ , f⁻¹∙f)
              (Str.Hom-is-set _ _)
              (Str.Hom-is-set _ _)

      from∘to : ∀ p → from (≅HH≃≅.to p) ≡ p
      from∘to ((f , f⁻¹ , f∙f⁻¹ , f⁻¹∙f) , Hf , Hf⁻¹) =
        cong₂ (λ f∙f⁻¹ f⁻¹∙f → (f , f⁻¹ , f∙f⁻¹ , f⁻¹∙f) , Hf , Hf⁻¹)
              (C.Hom-is-set _ _)
              (C.Hom-is-set _ _)

    module ≡≡≃≅HH where

      to : ∀ {X Y} {p : P X} {q : P Y} →
           (X≡Y : X ≡ Y) → subst P X≡Y p ≡ q →
           H p q (C.≡→≅ X≡Y C.¹) × H q p (C.≡→≅ X≡Y C.⁻¹)
      to {X} {p = p} X≡Y p≡q = elim¹
        (λ X≡Y → ∀ {q} → subst P X≡Y p ≡ q →
                 H p q (C.≡→≅ X≡Y C.¹) × H q p (C.≡→≅ X≡Y C.⁻¹))
        (elim¹
           (λ {q} _ → H p q (C.≡→≅ (refl X) C.¹) ×
                      H q p (C.≡→≅ (refl X) C.⁻¹))
           ( subst (λ { (q , f) → H p q f })
                   (sym $ cong₂ _,_
                            (subst P (refl X) p  ≡⟨ subst-refl P _ ⟩∎
                             p                   ∎)
                            (C.≡→≅ (refl X) C.¹  ≡⟨ cong C._¹ C.≡→≅-refl ⟩∎
                             C.id                ∎))
                   H-id
           , subst (λ { (q , f) → H q p f })
                   (sym $ cong₂ _,_
                            (subst P (refl X) p  ≡⟨ subst-refl P _ ⟩∎
                             p                   ∎)
                            (C.≡→≅ (refl X) C.⁻¹  ≡⟨ cong C._⁻¹ C.≡→≅-refl ⟩∎
                             C.id                 ∎))
                   H-id
           ))
        X≡Y p≡q

      to-refl : ∀ {X} {p : P X} →
                subst (λ f → H p p (f C.¹) × H p p (f C.⁻¹))
                      C.≡→≅-refl
                      (to (refl X) (subst-refl P p)) ≡
                (H-id , H-id)
      to-refl = cong₂ _,_ (H-prop _ _ _) (H-prop _ _ _)

    ≡≡≃≅HH : ∀ {X Y} {p : P X} {q : P Y} →
             (∃ λ (eq : X ≡ Y) → subst P eq p ≡ q) ≃
             (∃ λ (f : X C.≅ Y) → H p q (f C.¹) × H q p (f C.⁻¹))
    ≡≡≃≅HH {X} {p = p} {q} =
      Σ-preserves C.≡≃≅ λ X≡Y →
        _↔_.to (⇔↔≃ ext (P-set _) (×-closure 1 (H-prop _) (H-prop _)))
               (record { to = ≡≡≃≅HH.to X≡Y ; from = from X≡Y })
      where
      from : ∀ X≡Y → H p q (C.≡→≅ X≡Y C.¹) × H q p (C.≡→≅ X≡Y C.⁻¹) →
             subst P X≡Y p ≡ q
      from X≡Y (H¹ , H⁻¹) = elim¹
        (λ {Y} X≡Y → ∀ {q} →
                     H p q (C.≡→≅ X≡Y C.¹) → H q p (C.≡→≅ X≡Y C.⁻¹) →
                     subst P X≡Y p ≡ q)
        (λ {q} H¹ H⁻¹ →
           subst P (refl X) p  ≡⟨ subst-refl P _ ⟩
           p                   ≡⟨ H-antisymmetric p q
                                    (subst (H p q) (cong C._¹  C.≡→≅-refl) H¹)
                                    (subst (H q p) (cong C._⁻¹ C.≡→≅-refl) H⁻¹) ⟩∎
           q                   ∎)
        X≡Y H¹ H⁻¹

    ≡≃≅ : ∀ {X Y} {p : P X} {q : P Y} →
          _≡_ {A = ∃ P} (X , p) (Y , q) ≃ ((X , p) Str.≅ (Y , q))
    ≡≃≅ = ≅HH≃≅ ⊚ ≡≡≃≅HH ⊚ ↔⇒≃ (inverse Σ-≡,≡↔≡)

    -- …and the proof maps reflexivity to the identity morphism.

    ≡≃≅-refl : ∀ {Xp} → _≃_.to ≡≃≅ (refl Xp) Str.¹ ≡ Str.id
    ≡≃≅-refl {X , p} = cong Str._¹ (
      ≅HH≃≅.to (_≃_.to ≡≡≃≅HH (Σ-≡,≡←≡ (refl (_,_ {B = P} X p))))      ≡⟨ cong (≅HH≃≅.to ∘ _≃_.to ≡≡≃≅HH) $ Σ-≡,≡←≡-refl {B = P} ⟩
      ≅HH≃≅.to (_≃_.to ≡≡≃≅HH (refl X , subst-refl P p))               ≡⟨⟩
      ≅HH≃≅.to (C.≡→≅ (refl X) , ≡≡≃≅HH.to (refl X) (subst-refl P p))  ≡⟨ cong ≅HH≃≅.to $ Σ-≡,≡→≡ C.≡→≅-refl ≡≡≃≅HH.to-refl ⟩
      ≅HH≃≅.to (C.id≅ , H-id , H-id)                                   ≡⟨ refl _ ⟩∎
      Str.id≅                                                          ∎)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module container.m.core where

open import level
open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.isomorphism
open import function.extensionality
open import container.core
open import container.equality
open import container.fixpoint

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

module Definition {li la lb}(c : Container li la lb) where
  open Container c public

  -- definition of indexed M-types using native Agda coinduction
  data M (i : I) : Set (la ⊔ lb) where
    inf : (a : A i) → ((b : B a) → ∞ (M (r b))) → M i

  -- the terminal coalgebra
  out : M →ⁱ F M
  out i (inf a f) = a , ♭ ∘' f

  -- normally, the constructor can be defined in terms of out and unfold, but
  -- Agda provides it natively, together with a definitional β rule
  inM' : F M →ⁱ M
  inM' i (a , f) = inf a (λ x → ♯ (f x))

  inM'-β : {i : I}(x : F M i) → out i (inM' i x) ≡ x
  inM'-β x = refl

  module Elim {lx}{X : I → Set lx}
              (α : X →ⁱ F X) where
    -- anamorphisms
    unfold : X →ⁱ M
    unfold i x = inf a f
      where
        u : F X i
        u = α i x

        a : A i
        a = proj₁ u

        f : (b : B a) → ∞ (M (r b))
        f b = ♯ unfold (r b) (proj₂ u b)

    -- computational rule for anamorphisms
    -- this holds definitionally
    unfold-β : {i : I}(x : X i)
             → out i (unfold i x) ≡ imap unfold i (α i x)
    unfold-β x = refl

    -- the corresponding η rule doesn't hold, so we postulate it
    postulate
      unfold-η : (h : X →ⁱ M)
               → (∀ {i} (x : X i) → out i (h i x) ≡ imap h i (α i x))
               → ∀ {i} (x : X i) → h i x ≡ unfold i x
  open Elim public

  -- using η, we can prove that the unfolding of out is the identity
  unfold-id : ∀ {i} (x : M i) → unfold out i x ≡ x
  unfold-id x = sym (unfold-η out idⁱ (λ _ → refl) x)

  -- the usual definition of the constructor
  inM : F M →ⁱ M
  inM = unfold (imap out)

  -- the constructor is the inverse of the destructor
  inM-η : ∀ {i} (x : M i) → inM i (out i x) ≡ x
  inM-η x = unfold-η out (inM ∘ⁱ out) (λ _ → refl) x · unfold-id x

  inM-β : ∀ {i} (x : F M i) → out i (inM i x) ≡ x
  inM-β {i} x = ap u (funext (λ i → funext inM-η))
    where
      u : (M →ⁱ M) → F M i
      u h = imap h i x

  fixpoint : ∀ i → M i ≅ F M i
  fixpoint i = iso (out i) (inM i) inM-η inM-β

  -- now we can prove that the constructor provided by Agda is equal to the
  -- usual one
  inM-alt : ∀ {i} (x : F M i) → inM' i x ≡ inM i x
  inM-alt {i} x = sym (inM-η (inM' i x))

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


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

open import Level

record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  eta-equality
  infix  4 _≈_ _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : Obj → Obj → Set ℓ
    _≈_ : ∀ {A B} → (A ⇒ B) → (A ⇒ B) → Set e

    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  CommutativeSquare : ∀ {A B C D} → (f : A ⇒ B) (g : A ⇒ C) (h : B ⇒ D) (i : C ⇒ D) → Set _
  CommutativeSquare f g h i = h ∘ f ≈ i ∘ g

infix 10  _[_,_]

_[_,_] : ∀ {o ℓ e} → (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ
_[_,_] = Category._⇒_

module Inner {x₁ x₂ x₃} (CC : Category x₁ x₂ x₃) where

  open import Level
  private
    variable
      o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level

  open import Data.Product using (_×_; Σ; _,_; curry′; proj₁; proj₂; zip; map; <_,_>; swap)

  zipWith : ∀ {a b c p q r s} {A : Set a} {B : Set b} {C : Set c} {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → (_*_ : (x : C) → (y : R x) → S x y) → (x : Σ A P) → (y : Σ B Q) → S (proj₁ x ∙ proj₁ y) (proj₂ x ∘ proj₂ y)
  zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q)
  syntax zipWith f g h = f -< h >- g

  record Functor (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
    eta-equality
    private module C = Category C
    private module D = Category D

    field
      F₀ : C.Obj → D.Obj
      F₁ : ∀ {A B} (f : C [ A , B ]) → D [ F₀ A , F₀ B ]

  Product : (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
  Product C D = record
    { Obj       = C.Obj × D.Obj
    ; _⇒_       = C._⇒_ -< _×_ >- D._⇒_
    ; _≈_       = C._≈_ -< _×_ >- D._≈_
    ; _∘_       = zip C._∘_ D._∘_
    }
    where module C = Category C
          module D = Category D

  Bifunctor : Category o ℓ e → Category o′ ℓ′ e′ → Category o″ ℓ″ e″ → Set _
  Bifunctor C D E = Functor (Product C D) E

  private
    module CC = Category CC

  open CC

  infix 4 _≅_
  record _≅_ (A B : Obj) : Set (x₂) where
    field
      from : A ⇒ B
      to   : B ⇒ A

  private
    variable
      X Y Z W : Obj
      f g h : X ⇒ Y

  record Monoidal : Set (x₁ ⊔ x₂ ⊔ x₃) where
    infixr 10 _⊗₀_ _⊗₁_

    field
      ⊗  : Bifunctor CC CC CC

    module ⊗ = Functor ⊗

    open Functor ⊗

    _⊗₀_ : Obj → Obj → Obj
    _⊗₀_ = curry′ F₀

    -- this is also 'curry', but a very-dependent version
    _⊗₁_ : X ⇒ Y → Z ⇒ W → X ⊗₀ Z ⇒ Y ⊗₀ W
    f ⊗₁ g = F₁ (f , g)

    field
      associator : (X ⊗₀ Y) ⊗₀ Z ≅ X ⊗₀ (Y ⊗₀ Z)

    module associator {X} {Y} {Z} = _≅_ (associator {X} {Y} {Z})

    -- for exporting, it makes sense to use the above long names, but for
    -- internal consumption, the traditional (short!) categorical names are more
    -- convenient. However, they are not symmetric, even though the concepts are, so
    -- we'll use ⇒ and ⇐ arrows to indicate that
    private
      α⇒ = associator.from
      α⇐ = λ {X} {Y} {Z} → associator.to {X} {Y} {Z}

    field
      assoc-commute-from   : CommutativeSquare ((f ⊗₁ g) ⊗₁ h) α⇒ α⇒ (f ⊗₁ (g ⊗₁ h))
      assoc-commute-to     : CommutativeSquare (f ⊗₁ (g ⊗₁ h)) α⇐ α⇐ ((f ⊗₁ g) ⊗₁ h)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Containers, based on the work of Abbott and others
------------------------------------------------------------------------

module Data.Container where

open import Data.M
open import Data.Product as Prod hiding (map)
open import Data.W
open import Function renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (_↔_; module Inverse)
import Function.Related as Related
open import Level
open import Relation.Binary
  using (Setoid; module Setoid; Preorder; module Preorder)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≗_; refl)
open import Relation.Unary using (_⊆_)

------------------------------------------------------------------------
-- Containers

-- A container is a set of shapes, and for every shape a set of
-- positions.

infix 5 _▷_

record Container (ℓ : Level) : Set (suc ℓ) where
  constructor _▷_
  field
    Shape    : Set ℓ
    Position : Shape → Set ℓ

open Container public

-- The semantics ("extension") of a container.

⟦_⟧ : ∀ {ℓ} → Container ℓ → Set ℓ → Set ℓ
⟦ C ⟧ X = Σ[ s ∈ Shape C ] (Position C s → X)

-- The least and greatest fixpoints of a container.

μ : ∀ {ℓ} → Container ℓ → Set ℓ
μ C = W (Shape C) (Position C)

ν : ∀ {ℓ} → Container ℓ → Set ℓ
ν C = M (Shape C) (Position C)

-- Equality, parametrised on an underlying relation.

Eq : ∀ {c ℓ} {C : Container c} {X Y : Set c} →
     (X → Y → Set ℓ) → ⟦ C ⟧ X → ⟦ C ⟧ Y → Set (c ⊔ ℓ)
Eq {C = C} _≈_ (s , f) (s′ , f′) =
  Σ[ eq ∈ s ≡ s′ ] (∀ p → f p ≈ f′ (P.subst (Position C) eq p))

private

  -- Note that, if propositional equality were extensional, then
  -- Eq _≡_ and _≡_ would coincide.

  Eq⇒≡ : ∀ {c} {C : Container c} {X : Set c} {xs ys : ⟦ C ⟧ X} →
         P.Extensionality c c → Eq _≡_ xs ys → xs ≡ ys
  Eq⇒≡ {xs = s , f} {ys = .s , f′} ext (refl , f≈f′) =
    P.cong (_,_ s) (ext f≈f′)

setoid : ∀ {ℓ} → Container ℓ → Setoid ℓ ℓ → Setoid ℓ ℓ
setoid C X = record
  { Carrier       = ⟦ C ⟧ X.Carrier
  ; _≈_           = _≈_
  ; isEquivalence = record
    { refl  = (refl , λ _ → X.refl)
    ; sym   = sym
    ; trans = λ {_ _ zs} → trans zs
    }
  }
  where
  module X = Setoid X

  _≈_ = Eq X._≈_

  sym : {xs ys : ⟦ C ⟧ X.Carrier} → xs ≈ ys → ys ≈ xs
  sym {_ , _} {._ , _} (refl , f) = (refl , X.sym ⟨∘⟩ f)

  trans : ∀ {xs ys : ⟦ C ⟧ X.Carrier} zs → xs ≈ ys → ys ≈ zs → xs ≈ zs
  trans {_ , _} {._ , _} (._ , _) (refl , f₁) (refl , f₂) =
    (refl , λ p → X.trans (f₁ p) (f₂ p))

------------------------------------------------------------------------
-- Functoriality

-- Containers are functors.

map : ∀ {c} {C : Container c} {X Y} → (X → Y) → ⟦ C ⟧ X → ⟦ C ⟧ Y
map f = Prod.map ⟨id⟩ (λ g → f ⟨∘⟩ g)

module Map where

  identity : ∀ {c} {C : Container c} X →
             let module X = Setoid X in
             (xs : ⟦ C ⟧ X.Carrier) → Eq X._≈_ (map ⟨id⟩ xs) xs
  identity {C = C} X xs = Setoid.refl (setoid C X)

  composition : ∀ {c} {C : Container c} {X Y : Set c} Z →
                let module Z = Setoid Z in
                (f : Y → Z.Carrier) (g : X → Y) (xs : ⟦ C ⟧ X) →
                Eq Z._≈_ (map f (map g xs)) (map (f ⟨∘⟩ g) xs)
  composition {C = C} Z f g xs = Setoid.refl (setoid C Z)

------------------------------------------------------------------------
-- Container morphisms

-- Representation of container morphisms.

record _⇒_ {c} (C₁ C₂ : Container c) : Set c where
  field
    shape    : Shape C₁ → Shape C₂
    position : ∀ {s} → Position C₂ (shape s) → Position C₁ s

open _⇒_ public

-- Interpretation of _⇒_.

⟪_⟫ : ∀ {c} {C₁ C₂ : Container c} →
      C₁ ⇒ C₂ → ∀ {X} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X
⟪ m ⟫ xs = (shape m (proj₁ xs) , proj₂ xs ⟨∘⟩ position m)

module Morphism where

  -- Naturality.

  Natural : ∀ {c} {C₁ C₂ : Container c} →
            (∀ {X} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X) → Set (suc c)
  Natural {c} {C₁} m =
    ∀ {X} (Y : Setoid c c) → let module Y = Setoid Y in
    (f : X → Y.Carrier) (xs : ⟦ C₁ ⟧ X) →
    Eq Y._≈_ (m $ map f xs) (map f $ m xs)

  -- Natural transformations.

  NT : ∀ {c} (C₁ C₂ : Container c) → Set (suc c)
  NT C₁ C₂ = ∃ λ (m : ∀ {X} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X) → Natural m

  -- Container morphisms are natural.

  natural : ∀ {c} {C₁ C₂ : Container c}
            (m : C₁ ⇒ C₂) → Natural ⟪ m ⟫
  natural {C₂ = C₂} m Y f xs = Setoid.refl (setoid C₂ Y)

  -- In fact, all natural functions of the right type are container
  -- morphisms.

  complete : ∀ {c} {C₁ C₂ : Container c} →
             (nt : NT C₁ C₂) →
             ∃ λ m → (X : Setoid c c) →
                     let module X = Setoid X in
                     (xs : ⟦ C₁ ⟧ X.Carrier) →
                     Eq X._≈_ (proj₁ nt xs) (⟪ m ⟫ xs)
  complete (nt , nat) =
    (m , λ X xs → nat X (proj₂ xs) (proj₁ xs , ⟨id⟩))
    where
    m = record { shape    = λ  s  → proj₁ (nt (s , ⟨id⟩))
               ; position = λ {s} → proj₂ (nt (s , ⟨id⟩))
               }

  -- Identity.

  id : ∀ {c} (C : Container c) → C ⇒ C
  id _ = record {shape = ⟨id⟩; position = ⟨id⟩}

  -- Composition.

  infixr 9 _∘_

  _∘_ : ∀ {c} {C₁ C₂ C₃ : Container c} → C₂ ⇒ C₃ → C₁ ⇒ C₂ → C₁ ⇒ C₃
  f ∘ g = record
    { shape    = shape    f ⟨∘⟩ shape    g
    ; position = position g ⟨∘⟩ position f
    }

  -- Identity and composition commute with ⟪_⟫.

  id-correct : ∀ {c} {C : Container c} {X : Set c} →
               ⟪ id C ⟫ {X} ≗ ⟨id⟩
  id-correct xs = refl

  ∘-correct : ∀ {c} {C₁ C₂ C₃ : Container c}
              (f : C₂ ⇒ C₃) (g : C₁ ⇒ C₂) {X : Set c} →
              ⟪ f ∘ g ⟫ {X} ≗ (⟪ f ⟫ ⟨∘⟩ ⟪ g ⟫)
  ∘-correct f g xs = refl

------------------------------------------------------------------------
-- Linear container morphisms

record _⊸_ {c} (C₁ C₂ : Container c) : Set c where
  field
    shape⊸    : Shape C₁ → Shape C₂
    position⊸ : ∀ {s} → Position C₂ (shape⊸ s) ↔ Position C₁ s

  morphism : C₁ ⇒ C₂
  morphism = record
    { shape    = shape⊸
    ; position = _⟨$⟩_ (Inverse.to position⊸)
    }

  ⟪_⟫⊸ : ∀ {X} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X
  ⟪_⟫⊸ = ⟪ morphism ⟫

open _⊸_ public using (shape⊸; position⊸; ⟪_⟫⊸)

------------------------------------------------------------------------
-- All and any

-- All.

□ : ∀ {c} {C : Container c} {X : Set c} →
    (X → Set c) → (⟦ C ⟧ X → Set c)
□ P (s , f) = ∀ p → P (f p)

□-map : ∀ {c} {C : Container c} {X : Set c} {P Q : X → Set c} →
        P ⊆ Q → □ {C = C} P ⊆ □ Q
□-map P⊆Q = _⟨∘⟩_ P⊆Q

-- Any.

◇ : ∀ {c} {C : Container c} {X : Set c} →
    (X → Set c) → (⟦ C ⟧ X → Set c)
◇ P (s , f) = ∃ λ p → P (f p)

◇-map : ∀ {c} {C : Container c} {X : Set c} {P Q : X → Set c} →
        P ⊆ Q → ◇ {C = C} P ⊆ ◇ Q
◇-map P⊆Q = Prod.map ⟨id⟩ P⊆Q

-- Membership.

infix 4 _∈_

_∈_ : ∀ {c} {C : Container c} {X : Set c} →
      X → ⟦ C ⟧ X → Set c
x ∈ xs = ◇ (_≡_ x) xs

-- Bag and set equality and related preorders. Two containers xs and
-- ys are equal when viewed as sets if, whenever x ∈ xs, we also have
-- x ∈ ys, and vice versa. They are equal when viewed as bags if,
-- additionally, the sets x ∈ xs and x ∈ ys have the same size.

open Related public
  using (Kind; Symmetric-kind)
  renaming ( implication         to subset
           ; reverse-implication to superset
           ; equivalence         to set
           ; injection           to subbag
           ; reverse-injection   to superbag
           ; bijection           to bag
           )

[_]-Order : ∀ {ℓ} → Kind → Container ℓ → Set ℓ → Preorder ℓ ℓ ℓ
[ k ]-Order C X = Related.InducedPreorder₂ k (_∈_ {C = C} {X = X})

[_]-Equality : ∀ {ℓ} → Symmetric-kind → Container ℓ → Set ℓ → Setoid ℓ ℓ
[ k ]-Equality C X = Related.InducedEquivalence₂ k (_∈_ {C = C} {X = X})

infix 4 _∼[_]_

_∼[_]_ : ∀ {c} {C : Container c} {X : Set c} →
         ⟦ C ⟧ X → Kind → ⟦ C ⟧ X → Set c
_∼[_]_ {C = C} {X} xs k ys = Preorder._∼_ ([ k ]-Order C X) xs ys


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

module index where

-- Calf language implementation:
import Calf

-- Case studies:
import Examples

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


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

module AgdaFeatureNoInstanceFromHidden where

postulate
  A : Set
  R : A → A → Set

Alrighty : A → Set₁
Alrighty l = ∀ {r} → R l r → Set

record Foo (Q : A → Set₁) : Set₁ where field foo : ∀ {x y} → R x y → Q x → Q y

open Foo {{...}}

postulate
  instance theInstance : Foo Alrighty

works1 : ∀ {x y} → R x y → Alrighty x → Alrighty y
works1 r = foo r

works2 : ∀ {x y} → R x y → Alrighty x → Alrighty y
works2 r ax = works1 r ax

works3 : ∀ {x y} → R x y → Alrighty x → Alrighty y
works3 r ax = foo {{theInstance}} r ax

works4 : ∀ {x y} → R x y → Alrighty x → Alrighty y
works4 r ax = foo r (λ {v} → ax {v})

fails : ∀ {x y} → R x y → Alrighty x → Alrighty y
fails r ax = {!foo r ax!}
{-
No instance of type Foo (λ v → R v _r_81 → Set) was found in scope.
when checking that r ax are valid arguments to a function of type
{Q : A → Set₁} {{r = r₁ : Foo Q}} {x y : A} → R x y → Q x → Q y
-}


text:
module Issue157 where

X : Set
X = _

error : Set
error = Set


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Relation.Boolean where

open import Light.Library.Data.Boolean as Boolean using (Boolean)
open import Light.Package using (Package)
open import Light.Level using (_⊔_ ; Lifted)
open import Light.Variable.Levels
open import Light.Variable.Sets
open import Light.Library.Data.Unit as Unit using (Unit ; unit)
open import Light.Library.Data.Empty as Empty using (Empty)
open import Light.Library.Relation using (Style)
open import Light.Implementation.Data.Boolean
open import Light.Implementation.Data.Unit
open import Light.Implementation.Data.Empty

instance relation : Style record { Proposition = λ _ → Boolean ; Index = Unit }
relation = record { Implementation }
      where
      module Implementation where
            open Boolean using (true ; false ; ¬_ ; _∧_ ; _∨_ ; _⇢_) public

            True = Boolean.if_then Unit else Empty
            False = Boolean.if_then Empty else Unit

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
------------------------------------------------------------------------
-- The syntax of, and a type system for, an untyped λ-calculus with
-- booleans and recursive unary function calls
------------------------------------------------------------------------

open import Prelude

module Lambda.Syntax (Name : Type) where

open import Equality.Propositional
open import Prelude.Size

open import Vec.Data equality-with-J

------------------------------------------------------------------------
-- Terms

-- Variables are represented using de Bruijn indices.

infixl 9 _·_

data Tm (n : ℕ) : Type where
  var  : Fin n → Tm n
  lam  : Tm (suc n) → Tm n
  _·_  : Tm n → Tm n → Tm n
  call : Name → Tm n → Tm n
  con  : Bool → Tm n
  if   : Tm n → Tm n → Tm n → Tm n

------------------------------------------------------------------------
-- Closure-based definition of values

-- Environments and values. Defined in a module parametrised by the
-- type of terms.

module Closure (Tm : ℕ → Type) where

  mutual

    -- Environments.

    Env : ℕ → Type
    Env n = Vec Value n

    -- Values. Lambdas are represented using closures, so values do
    -- not contain any free variables.

    data Value : Type where
      lam : ∀ {n} → Tm (suc n) → Env n → Value
      con : Bool → Value

------------------------------------------------------------------------
-- Type system

-- Recursive, simple types, defined coinductively.

infixr 8 _⇾_ _⇾′_

mutual

  data Ty (i : Size) : Type where
    bool : Ty i
    _⇾′_ : (σ τ : Ty′ i) → Ty i

  record Ty′ (i : Size) : Type where
    coinductive
    field
      force : {j : Size< i} → Ty j

open Ty′ public

-- Some type formers.

_⇾_ : ∀ {i} → Ty i → Ty i → Ty i
σ ⇾ τ = (λ { .force → σ }) ⇾′ (λ { .force → τ })

-- Contexts.

Ctxt : ℕ → Type
Ctxt n = Vec (Ty ∞) n

-- Type system.

infix 4 _,_⊢_∈_

data _,_⊢_∈_ (Σ : Name → Ty ∞ × Ty ∞) {n} (Γ : Ctxt n) :
             Tm n → Ty ∞ → Type where
  var  : ∀ {x} → Σ , Γ ⊢ var x ∈ index Γ x
  lam  : ∀ {t σ τ} →
         Σ , force σ ∷ Γ ⊢ t ∈ force τ →
         Σ , Γ ⊢ lam t ∈ σ ⇾′ τ
  _·_  : ∀ {t₁ t₂ σ τ} →
         Σ , Γ ⊢ t₁ ∈ σ ⇾′ τ →
         Σ , Γ ⊢ t₂ ∈ force σ →
         Σ , Γ ⊢ t₁ · t₂ ∈ force τ
  call : ∀ {f t} →
         Σ , Γ ⊢ t ∈ proj₁ (Σ f) →
         Σ , Γ ⊢ call f t ∈ proj₂ (Σ f)
  con  : ∀ {b} → Σ , Γ ⊢ con b ∈ bool
  if   : ∀ {t₁ t₂ t₃ σ} →
         Σ , Γ ⊢ t₁ ∈ bool →
         Σ , Γ ⊢ t₂ ∈ σ →
         Σ , Γ ⊢ t₃ ∈ σ →
         Σ , Γ ⊢ if t₁ t₂ t₃ ∈ σ

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

-- A non-terminating term.

ω-body : Tm 1
ω-body = var fzero · var fzero

ω : Tm 0
ω = lam ω-body

Ω : Tm 0
Ω = ω · ω

-- Ω is well-typed.

Ω-well-typed : ∀ {Σ} (τ : Ty ∞) → Σ , [] ⊢ Ω ∈ τ
Ω-well-typed τ =
  _·_ {σ = σ} {τ = λ { .force → τ }} (lam (var · var)) (lam (var · var))
  where
  σ : ∀ {i} → Ty′ i
  force σ = σ ⇾′ λ { .force → τ }

-- A call-by-value fixpoint combinator.

Z : Tm 0
Z = lam (t · t)
  where
  t = lam (var (fsuc fzero) ·
         lam (var (fsuc fzero) · var (fsuc fzero) · var fzero))

-- This combinator is also well-typed.

Z-well-typed :
  ∀ {Σ} {σ τ : Ty ∞} →
  Σ , [] ⊢ Z ∈ ((σ ⇾ τ) ⇾ (σ ⇾ τ)) ⇾ (σ ⇾ τ)
Z-well-typed {σ = σ} {τ = τ} =
  lam (_·_ {σ = υ} {τ = λ { .force → σ ⇾ τ }}
           (lam (var · lam (var · var · var)))
           (lam (var · lam (var · var · var))))
  where
  υ : ∀ {i} → Ty′ i
  force υ = υ ⇾′ λ { .force → σ ⇾ τ }

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
open import Relation.Binary.Core

module Mergesort.Impl2 {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Bound.Lower A
open import Bound.Lower.Order  _≤_
open import Data.List
open import Data.Sum
open import Function
open import LRTree {A}
open import OList _≤_

mutual
  merge' : {b : Bound} → OList b → OList b → OList b
  merge' onil ys = ys
  merge' xs onil = xs
  merge' (:< {x = x} b≤x xs) (:< {x = y} b≤y ys)
      with tot≤ x y
  ... | inj₁ x≤y  = :< b≤x (merge' xs (:< (lexy x≤y) ys))
  ... | inj₂ y≤x = :< b≤y (merge'xs (lexy y≤x) xs ys)

  merge'xs : {b : Bound}{x : A} → LeB b (val x) → OList (val x) → OList b → OList b
  merge'xs b≤x xs onil = :< b≤x xs
  merge'xs {x = x} b≤x xs (:< {x = y} b≤y ys)
      with tot≤ x y
  ... | inj₁ x≤y = :< b≤x (merge' xs (:< (lexy x≤y) ys))
  ... | inj₂ y≤x = :< b≤y (merge'xs (lexy y≤x) xs ys)

deal : List A → LRTree
deal = foldr insert empty

merge : LRTree → OList bot
merge empty = onil
merge (leaf x) = :< (lebx {val x}) onil
merge (node t l r) = merge' (merge l) (merge r)

mergesort : List A → OList bot
mergesort = merge ∘ deal

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module Hmm where

  -- using the HoTT-Agda library leads to highlighting error (missing metadata)
  -- open import lib.Base
  -- open import lib.types.Nat

  -- using this library does not, yet the code is copied/pasted from HoTT-Agda
  open import Base

  S= : {m n : ℕ} → m == n → S m == S n
  S= idp = idp

max_stars_repo_name: aerskine/hott-ex

max_issues_repo_name: aerskine/hott-ex

max_forks_repo_name: aerskine/hott-ex


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core
open import Categories.Category.Monoidal.Core

-- This module defines the category of monoids internal to a given monoidal
-- category.

module Categories.Category.Construction.Monoids {o ℓ e} {𝒞 : Category o ℓ e} (C : Monoidal 𝒞) where

open import Level

open import Categories.Functor using (Functor)
open import Categories.Morphism.Reasoning 𝒞
open import Categories.Object.Monoid C

open Category 𝒞
open Monoidal C
open HomReasoning
open Monoid using (η; μ)
open Monoid⇒

Monoids : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
Monoids = record
  { Obj = Monoid
  ; _⇒_ = Monoid⇒
  ; _≈_ = λ f g → arr f ≈ arr g
  ; id = record
    { arr = id
    ; preserves-μ = identityˡ ○ introʳ (Functor.identity ⊗)
    ; preserves-η = identityˡ
    }
  ; _∘_ = λ f g → record
    { arr = arr f ∘ arr g
    ; preserves-μ = glue (preserves-μ f) (preserves-μ g) ○ ∘-resp-≈ʳ (⟺ (Functor.homomorphism ⊗))
    ; preserves-η = glueTrianglesˡ (preserves-η f) (preserves-η g)
    }
  ; assoc = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  -- We cannot define equiv = equiv here, because _⇒_ of this category is a
  -- different level to the _⇒_ of 𝒞.
  ; equiv = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  ; ∘-resp-≈ = ∘-resp-≈
  } where open Equiv

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homogeneously-indexed binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Indexed.Homogeneous`.

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

module Relation.Binary.Indexed.Homogeneous.Definitions where

open import Data.Product using (_×_)
open import Level using (Level)
import Relation.Binary as B
open import Relation.Unary.Indexed using (IPred)

open import Relation.Binary.Indexed.Homogeneous.Core

private
  variable
    i a ℓ ℓ₁ ℓ₂ : Level
    I : Set i

------------------------------------------------------------------------
-- Definitions

module _ (A : I → Set a) where

  syntax Implies A _∼₁_ _∼₂_ = _∼₁_ ⇒[ A ] _∼₂_

  Implies : IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Implies _∼₁_ _∼₂_ = ∀ {i} → _∼₁_ B.⇒ (_∼₂_ {i})

  Reflexive : IRel A ℓ → Set _
  Reflexive _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})

  Symmetric : IRel A ℓ → Set _
  Symmetric _∼_ = ∀ {i} → B.Symmetric (_∼_ {i})

  Transitive : IRel A ℓ → Set _
  Transitive _∼_ = ∀ {i} → B.Transitive (_∼_ {i})

  Antisymmetric : IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Antisymmetric _≈_ _∼_ = ∀ {i} → B.Antisymmetric _≈_ (_∼_ {i})

  Decidable : IRel A ℓ → Set _
  Decidable _∼_ = ∀ {i} → B.Decidable (_∼_ {i})

  Respects : IPred A ℓ₁ → IRel A ℓ₂ → Set _
  Respects P _∼_ = ∀ {i} {x y : A i} → x ∼ y → P x → P y

  Respectsˡ : IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Respectsˡ P _∼_  = ∀ {i} {x y z : A i} → x ∼ y → P x z → P y z

  Respectsʳ : IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Respectsʳ P _∼_ = ∀ {i} {x y z : A i} → x ∼ y → P z x → P z y

  Respects₂ : IRel A ℓ₁ → IRel A ℓ₂ → Set _
  Respects₂ P _∼_ = (Respectsʳ P _∼_) × (Respectsˡ P _∼_)