text:
module Grove where

open import Axiom.Extensionality.Propositional
open import Data.Bool hiding (_<_; _≟_)
open import Function.Equivalence hiding (_∘_)
open import Function hiding (_⇔_)
open import Function.Equality using (_⟨$⟩_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open import Relation.Nullary

postulate
  extensionality : {ℓ₁ ℓ₂ : Level} → Extensionality ℓ₁ ℓ₂

----------------
-- Constructors
----------------

postulate
  Ctor : Set
  _≟ℂ_ : (c₁ c₂ : Ctor) → Dec (c₁ ≡ c₂)

----------------
-- Positions
----------------

postulate
  Pos : Set
  _≟ℙ_ : (p₁ p₂ : Pos) → Dec (p₁ ≡ p₂)
  _∈ℙ_ : Pos → Ctor → Set

----------------
-- Identifiers
----------------

postulate
  Ident : Set
  _≟𝕀_ : (i₁ i₂ : Ident) → Dec (i₁ ≡ i₂)

----------------
-- The Root Vertex
----------------

-- Note actually used in the proofs, but here it is anyway
postulate
  ctorRoot : Ctor
  posRoot : Pos
  posRoot∈ctorRoot : posRoot ∈ℙ ctorRoot
  identRoot : Ident

----------------
-- Vertex
----------------

record Vertex : Set where
  constructor V
  field
    ctor : Ctor
    ident : Ident

_≟Vertex_ : (v₁ v₂ : Vertex) → Dec (v₁ ≡ v₂)
V c₁ i₁ ≟Vertex V c₂ i₂ with c₁ ≟ℂ c₂ | i₁ ≟𝕀 i₂
... | yes refl | yes refl = yes refl
... | _        | no p     = no (λ { refl → p refl })
... | no p     | _        = no (λ { refl → p refl })

----------------
-- Edge
----------------

record Edge : Set where
  constructor E
  field
    parent : Vertex
    child : Vertex
    position : Pos
    ident : Ident
    .isValid : position ∈ℙ Vertex.ctor parent

_≟Edge_ : (e₁ e₂ : Edge) → Dec (e₁ ≡ e₂)
E parent₁ child₁ position₁ ident₁ _ ≟Edge E parent₂ child₂ position₂ ident₂ _
  with parent₁ ≟Vertex parent₂
     | child₁ ≟Vertex child₂
     | position₁ ≟ℙ position₂
     | ident₁ ≟𝕀 ident₂
... | yes refl | yes refl | yes refl | yes refl = yes refl
... | no p     | _        | _        | _        = no (λ { refl → p refl })
... | _        | no p     | _        | _        = no (λ { refl → p refl })
... | _        | _        | no p     | _        = no (λ { refl → p refl })
... | _        | _        | _        | no p     = no (λ { refl → p refl })

----------------
-- EdgeState
----------------

data EdgeState : Set where
  ⊥ : EdgeState -- smallest
  + : EdgeState -- middle
  - : EdgeState -- largest

_⊔_ : EdgeState → EdgeState → EdgeState
- ⊔ _ = -
_ ⊔ - = -
+ ⊔ _ = +
_ ⊔ + = +
_ ⊔ _ = ⊥

⊔-assoc : (s₁ s₂ s₃ : EdgeState) → (s₁ ⊔ (s₂ ⊔ s₃)) ≡ ((s₁ ⊔ s₂) ⊔ s₃)
⊔-assoc ⊥ ⊥ ⊥ = refl
⊔-assoc ⊥ ⊥ + = refl
⊔-assoc ⊥ ⊥ - = refl
⊔-assoc ⊥ + ⊥ = refl
⊔-assoc ⊥ + + = refl
⊔-assoc ⊥ + - = refl
⊔-assoc ⊥ - ⊥ = refl
⊔-assoc ⊥ - + = refl
⊔-assoc ⊥ - - = refl
⊔-assoc + ⊥ ⊥ = refl
⊔-assoc + ⊥ + = refl
⊔-assoc + ⊥ - = refl
⊔-assoc + + ⊥ = refl
⊔-assoc + + + = refl
⊔-assoc + + - = refl
⊔-assoc + - ⊥ = refl
⊔-assoc + - + = refl
⊔-assoc + - - = refl
⊔-assoc - ⊥ ⊥ = refl
⊔-assoc - ⊥ + = refl
⊔-assoc - ⊥ - = refl
⊔-assoc - + ⊥ = refl
⊔-assoc - + + = refl
⊔-assoc - + - = refl
⊔-assoc - - ⊥ = refl
⊔-assoc - - + = refl
⊔-assoc - - - = refl

⊔-comm : (s₁ s₂ : EdgeState) → s₁ ⊔ s₂ ≡ s₂ ⊔ s₁
⊔-comm ⊥ ⊥ = refl
⊔-comm ⊥ + = refl
⊔-comm ⊥ - = refl
⊔-comm + ⊥ = refl
⊔-comm + + = refl
⊔-comm + - = refl
⊔-comm - ⊥ = refl
⊔-comm - + = refl
⊔-comm - - = refl

⊔-idem : (s : EdgeState) → s ⊔ s ≡ s
⊔-idem ⊥ = refl
⊔-idem + = refl
⊔-idem - = refl

----------------
-- Graph
----------------

Graph : Set
Graph = Edge → EdgeState

_[_↦_] :  Graph → Edge → EdgeState → Graph
_[_↦_] f k v = λ { x → if does (x ≟Edge k) then v ⊔ f x else f x }

[↦]-comm : (s₁ s₂ : EdgeState) (e₁ e₂ : Edge) (g : Graph)
  → (g [ e₁ ↦ s₁ ]) [ e₂ ↦ s₂ ]
  ≡ (g [ e₂ ↦ s₂ ]) [ e₁ ↦ s₁ ]
[↦]-comm s₁ s₂ e₁ e₂ g = extensionality go where
  go : (e : Edge) → ((g [ e₁ ↦ s₁ ]) [ e₂ ↦ s₂ ]) e ≡ ((g [ e₂ ↦ s₂ ]) [ e₁ ↦ s₁ ]) e
  go e with e ≟Edge e₁ | e ≟Edge e₂
  ... | yes refl | yes refl rewrite ⊔-assoc s₁ s₂ (g e) | ⊔-assoc s₂ s₁ (g e) | ⊔-comm s₁ s₂ = refl
  ... | no _ | yes refl = refl
  ... | yes refl | no _ = refl
  ... | no _ | no _ = refl

[↦]-join : (s₁ s₂ : EdgeState) (e : Edge) (g : Graph)
  → (g [ e ↦ s₁ ]) [ e ↦ s₂ ]
  ≡ g [ e ↦ s₁ ⊔ s₂ ]
[↦]-join s₁ s₂ e g = extensionality go where
  go : (e' : Edge) → ((g [ e ↦ s₁ ]) [ e ↦ s₂ ]) e' ≡ (g [ e ↦ s₁ ⊔ s₂ ]) e'
  go e' with e' ≟Edge e
  ... | yes refl rewrite ⊔-assoc s₂ s₁ (g e) | ⊔-comm s₁ s₂ = refl
  ... | no _ = refl

----------------
-- Action
----------------

data Action : Set where
  A : Edge → EdgeState → Action

⟦_⟧ : Action → Graph → Graph
⟦ (A e s) ⟧ g = g [ e ↦ s ]

⟦⟧-comm' : (a₁ a₂ : Action) (g : Graph)
  → ⟦ a₁ ⟧ (⟦ a₂ ⟧ g)
  ≡ ⟦ a₂ ⟧ (⟦ a₁ ⟧ g)
⟦⟧-comm' (A e₁ s₁) (A e₂ s₂) g = [↦]-comm s₂ s₁ e₂ e₁ g

⟦⟧-comm : (a₁ a₂ : Action)
  → ⟦ a₁ ⟧ ∘′ ⟦ a₂ ⟧
  ≡ ⟦ a₂ ⟧ ∘′ ⟦ a₁ ⟧
⟦⟧-comm a₁ a₂ = extensionality (⟦⟧-comm' a₁ a₂)

⟦⟧-idem' : (a : Action) (g : Graph)
  → ⟦ a ⟧ (⟦ a ⟧ g)
  ≡ ⟦ a ⟧ g
⟦⟧-idem' (A e s) g rewrite [↦]-join s s e g with s
... | ⊥ = refl
... | + = refl
... | - = refl

⟦⟧-idem : (a : Action)
  → ⟦ a ⟧ ∘′ ⟦ a ⟧
  ≡ ⟦ a ⟧
⟦⟧-idem a = extensionality (⟦⟧-idem' a)

----------------
-- Action Relation Between Graphs
----------------

data ActionRel : Graph → Action → Graph → Set where
  AR : (a : Action) → (g : Graph) → ActionRel g a (⟦ a ⟧ g)

ActionRel-eqv : {g g' : Graph} {a : Action}
  → ActionRel g a g' ⇔ g' ≡ ⟦ a ⟧ g
ActionRel-eqv {g} {g'} {a} = equivalence to from where
  to : ActionRel g a g' → g' ≡ ⟦ a ⟧ g
  to (AR .a .g) = refl
  from : g' ≡ ⟦ a ⟧ g → ActionRel g a g'
  from refl = AR a g

ActionRel-comm : {a₁ a₂ : Action} {g₁ g₂₁ g₃₁ g₂₂ g₃₂ : Graph}
  → ActionRel g₁ a₁ g₂₁ → ActionRel g₂₁ a₂ g₃₁
  → ActionRel g₁ a₂ g₂₂ → ActionRel g₂₂ a₁ g₃₂
  → g₃₁ ≡ g₃₂
ActionRel-comm {a₁} {a₂} {g₁} {g₂₁} {g₃₁} {g₂₂} {g₃₂} ar₁ ar₂ ar₂₂ ar₁' = eqgg where
  eqg₂ : g₂₁ ≡ ⟦ a₁ ⟧ g₁
  eqg₂ = Equivalence.to ActionRel-eqv ⟨$⟩ ar₁
  eqg₃ : g₃₁ ≡ ⟦ a₂ ⟧ (⟦ a₁ ⟧ g₁)
  eqg₃ with eqg₂
  ... | refl = Equivalence.to ActionRel-eqv ⟨$⟩ ar₂
  eqg₂₂ : g₂₂ ≡ ⟦ a₂ ⟧ g₁
  eqg₂₂ = Equivalence.to ActionRel-eqv ⟨$⟩ ar₂₂
  eqg₃₂ : g₃₂ ≡ ⟦ a₁ ⟧ (⟦ a₂ ⟧ g₁)
  eqg₃₂ with eqg₂₂
  ... | refl = Equivalence.to ActionRel-eqv ⟨$⟩ ar₁'
  eqgg : g₃₁ ≡ g₃₂
  eqgg with eqg₃ | eqg₃₂
  ... | refl | refl = ⟦⟧-comm' a₂ a₁ g₁

max_stars_repo_name: fplab/grove-agda

max_issues_repo_name: fplab/grove-agda

max_forks_repo_name: fplab/grove-agda


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

data Unit : Set where
  unit : Unit

record _∼_ (From To : Set) : Set where
  field
    to      : From → To
    from    : To → From
    to-from : ∀ {x} → to (from x) ≡ x

postulate
  P : {A : Set} → A → Set
  f : {A B : Set} (A∼B : A ∼ B) (x : A) → P (_∼_.to A∼B x) ∼ P x

record R : Set where
  field
    p   : {x y : Unit} → P x → P y
    u v : Unit

g : (r : R) → _ ∼ P r
g = f lemma
  where
  lemma : R ∼ Σ _ λ _ → Σ _ λ (_ : ∀ {x y} → _ → _) → _
  lemma = record
    { to      = λ x → R.u x , R.p x , R.v x
    ; from    = λ { (u , p , v) → record
                    { u  = u
                    ; p  = λ {x y} → p {x = x} {y = y}
                    ; v  = v
                    } }
    ; to-from = refl
    }

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module CompilingCoinduction where

open import Common.Coinduction
open import Common.Char
open import Common.String

data Unit : Set where
  unit : Unit

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

postulate
  IO : Set → Set

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

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

postulate
  putStrLn : ∞ String → IO Unit

{-# COMPILE GHC putStrLn = Data.Text.IO.putStrLn . MAlonzo.RTE.flat #-}
{-# COMPILE JS  putStrLn = function(x) { return function(cb) { process.stdout.write(x.flat() + "\n"); cb(0); }; } #-}

main = putStrLn (♯ "a")

max_forks_repo_name: shlevy/agda


text:
module Fail.BadBuiltinImport where

import Agda.Builtin.Nat

{-# FOREIGN AGDA2HS
import RandomModule (Natural)
import AlsoNotRight (foo, Natural(..))
import AsConstructor (D(Natural))
#-}


text:
module Functional.Dependent where

import      Lvl
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level

-- Function type as a function
_→ᶠ_ : (X : Type{ℓ₁}) → (Type{ℓ₁} → Type{ℓ₂}) → Type{ℓ₁ Lvl.⊔ ℓ₂}
X →ᶠ Y = X → Y(X)
infixl 30 _→ᶠ_

module _ where
  private variable X : Type{ℓ}
  private variable Y : X → Type{ℓ}
  private variable Z : ∀{x : X} → Y(x) → Type{ℓ}

  apply : (x : X) → ((x : X) → Y(x)) → Y(x)
  apply(x)(f) = f(x)
  {-# INLINE apply #-}

  const : (∀{x : X} → Y(x)) → ((x : X) → Y(x))
  const y _ = y
  {-# INLINE const #-}

  _$_ : ((x : X) → Y(x)) → (x : X) → Y(x)
  f $ x = f(x)
  {-# INLINE _$_ #-}
  infixr 0 _$_

  _⩺_ : (x : X) → ((x : X) → Y(x)) → Y(x)
  x ⩺ f = f(x)
  {-# INLINE _⩺_ #-}
  infixl 10000 _⩺_

  _⩹_ : ((x : X) → Y(x)) → (x : X) → Y(x)
  f ⩹ x = f(x)
  {-# INLINE _⩹_ #-}
  infixl 10000 _⩹_

  _∘ᵢₘₚₗ_ : (∀{x : X}{y : Y(x)} → Z{x}(y)) → (g : ∀{x : X} → Y(x)) → (∀{x : X} → Z(g{x}))
  (f ∘ᵢₘₚₗ g){x} = f{x}{g{x}}
  infixl 10000 _∘ᵢₘₚₗ_

  _∘ᵢₙₛₜ_ : (⦃ x : X ⦄ ⦃ y : Y(x) ⦄ → Z{x}(y)) → (g : ⦃ x : X ⦄ → Y(x)) → (⦃ x : X ⦄ → Z(g ⦃ x ⦄))
  (f ∘ᵢₙₛₜ g) ⦃ x ⦄ = f ⦃ x ⦄ ⦃ g ⦃ x ⦄ ⦄
  infixl 10000 _∘ᵢₙₛₜ_

  _∘ₛ_ : ((x : X) → (y : Y(x)) → Z{x}(y)) → (g : (x : X) → Y(x)) → ((x : X) → Z(g(x)))
  (f ∘ₛ g)(x) = f(x)(g(x))
  {-# INLINE _∘ₛ_ #-}
  infixl 10000 _∘ₛ_

  _∘_ : (∀{x : X} → (y : Y(x)) → Z{x}(y)) → (g : (x : X) → Y(x)) → ((x : X) → Z(g(x)))
  _∘_ f = (const f) ∘ₛ_
  {-# INLINE _∘_ #-}
  infixl 10000 _∘_

module _ where
  private variable X : Type{ℓ}
  private variable Y : X → Type{ℓ}
  private variable Z : ∀{x₁ x₂ : X} → Y(x₁) → Y(x₂) → Type{ℓ}

  _on₂_ : (f : ∀{x₁ x₂ : X} → (y₁ : Y(x₁)) → (y₂ : Y(x₂)) → Z{x₁}{x₂}(y₁)(y₂)) → (g : (x : X) → Y(x)) → ((x₁ : X) → (x₂ : X) → Z(g(x₁))(g(x₂)))
  ((_▫_) on₂ f)(y₁)(y₂) = f(y₁) ▫ f(y₂)

module _ where
  private variable X Y : Type{ℓ}
  private variable Z : X → Y → Type{ℓ}

  swap : ((x : X) → (y : Y) → Z(x)(y)) → ((y : Y) → (x : X) → Z(x)(y))
  swap f(y)(x) = f(x)(y)
  {-# INLINE swap #-}

{- TODO: Agda errors
module _ where
  private variable X₁ : Type{ℓ}
  private variable X₂ : X₁ → Type{ℓ}
  private variable Y₁ : ∀{x₁ : X₁} → X₂(x₁) → Type{ℓ}
  private variable Y₂ : ∀{x₁ : X₁}{x₂ : X₂(x₁)} → Y₁{x₁}(x₂) → Type{ℓ}
  private variable Z : ∀{x₁ : X₁}{x₂ : X₂(x₁)}{y₁ : Y₁{x₁}(x₂)} → (Y₂{x₁}{x₂}(y₁)) → Type{ℓ}

  pointwise₂,₁' : (∀{x₁ : X₁} → (x₂ : X₂(x₁)) → {y₁ : Y₁(x₂)} → (y₂ : Y₂(y₁)) → Z{x₁}{x₂}{y₁}(y₂)) → (f : (x₁ : X₁) → X₂(x₁)) → (g : ∀{x₁}{x₂} → (y₁ : Y₁{x₁}(x₂)) → Y₂{x₁}{x₂}(y₁)) → ((x₁ : X₁) → (y₁ : Y₁{x₁}(f(x₁))) → Z{x₁}{f(x₁)}{y₁}(g(y₁)))
-}
{-
module _ where
  private variable X₁ : Type{ℓ}
  private variable X₂ : X₁ → Type{ℓ}
  private variable Y₁ : ∀{x₁ : X₁} → X₂(x₁) → Type{ℓ}
  private variable Y₂ : ∀{x₁ : X₁}{x₂ : X₂(x₁)} → Y₁{x₁}(x₂) → Type{ℓ}
  private variable Z : ∀{x₁ : X₁}{x₂ : X₂(x₁)}{y₁ : Y₁{x₁}(x₂)} → Type{ℓ}

  pointwise₂,₁' : ∀{x₁ : X₁} → (x₂ : X₂(x₁)) → {y₁ : Y₁(x₂)} → (y₂ : Y₂(y₁)) → Z{x₁}{x₂}{y₁}
-}

module _ where
  private variable A : Type{ℓ}
  private variable B : A → Type{ℓ}
  private variable C : ∀{a : A} → B(a) → Type{ℓ}
  private variable D : ∀{a : A}{b : B(a)} → (C{a}(b)) → Type{ℓ}
  private variable E : ∀{a : A}{b : B(a)}{c : C{a}(b)} → D{a}{b}(c) → Type{ℓ}
  private variable F : ∀{a : A}{b : B(a)}{c : C{a}(b)}{d : D{a}{b}(c)} → E{a}{b}{c}(d) → Type{ℓ}

  -- Alternative definition: (f ∘₂ g) a b = f(g a b)
  _∘₂_ : (∀{a : A}{b : B(a)} → (c : C{a}(b)) → D{a}{b}(c)) → (g : ∀(a)(b) → C{a}(b)) → (∀(a)(b) → D(g a b))
  _∘₂_ f = (f ∘_) ∘_
  {-# INLINE _∘₂_ #-}

  -- Alternative definition: (f ∘₂ₛ g) x y = f a b (g a b)
  _∘₂ₛ_ : ((a : A) → (b : B(a)) → (c : C{a}(b)) → D{a}{b}(c)) → (g : ∀(a)(b) → C{a}(b)) → (∀(a)(b) → D(g a b))
  _∘₂ₛ_ f = ((_∘ₛ_) ∘ f) ∘ₛ_
  {-# INLINE _∘₂ₛ_ #-}

  -- Alternative definition: (f ∘₂ g) a b c = f(g a b c)
  _∘₃_ : (∀{a : A}{b : B(a)}{c : C{a}(b)} → (d : D{a}{b}(c)) → E{a}{b}{c}(d)) → (g : ∀(a)(b)(c) → D{a}{b}(c)) → (∀(a)(b)(c) → E(g a b c))
  _∘₃_ f = (f ∘₂_) ∘_
  {-# INLINE _∘₃_ #-}

  -- Alternative definition: (f ∘₃ₛ g) a b c = f a b c (g a b c)
  _∘₃ₛ_ : (∀(a : A)(b : B(a))(c : C{a}(b)) → (d : D{a}{b}(c)) → E{a}{b}{c}(d)) → (g : ∀(a)(b)(c) → D{a}{b}(c)) → (∀(a)(b)(c) → E(g a b c))
  _∘₃ₛ_ f = ((_∘₂ₛ_) ∘ f) ∘ₛ_
  {-# INLINE _∘₃ₛ_ #-}

  -- Alternative definition: (f ∘₄ g) a b c d = f(g a b c d)
  _∘₄_ : (∀{a : A}{b : B(a)}{c : C{a}(b)}{d : D{a}{b}(c)} → (e : E{a}{b}{c}(d)) → F{a}{b}{c}{d}(e)) → (g : ∀(a)(b)(c)(d) → E{a}{b}{c}(d)) → (∀(a)(b)(c)(d) → F(g a b c d))
  _∘₄_ f = (f ∘₃_) ∘_
  {-# INLINE _∘₄_ #-}

  -- Alternative definition: (f ∘₄ₛ g) a b c d = f a b c d (g a b c d)
  _∘₄ₛ_ : (∀(a : A)(b : B(a))(c : C{a}(b))(d : D{a}{b}(c)) → (e : E{a}{b}{c}(d)) → F{a}{b}{c}{d}(e)) → (g : ∀(a)(b)(c)(d) → E{a}{b}{c}(d)) → (∀(a)(b)(c)(d) → F(g a b c d))
  _∘₄ₛ_ f = ((_∘₃ₛ_) ∘ f) ∘ₛ_
  {-# INLINE _∘₄ₛ_ #-}

  -- Alternative definition: pointwise₂,₁(_▫_) f g a = f(a) ▫ g(a)
  pointwise₂,₁ : (∀{a : A} → (b : B(a)) → (c : C{a}(b)) → D{a}{b}(c)) → (f : (a : A) → B(a)) → (g : (a : A) → C{a}(f(a))) → (a : A) → D{a}{f(a)}(g(a))
  pointwise₂,₁(_▫_) = ((_∘ₛ_) ∘ ((_▫_) ∘_))
  {-# INLINE pointwise₂,₁ #-}

  -- Alternative definition: pointwise₂,₂(_▫_) f g a b = (f a b) ▫ (g a b)
  pointwise₂,₂ : (∀{a : A}{b : B(a)} → (c : C{a}(b)) → (d : D{a}{b}(c)) → E{a}{b}{c}(d)) → (f : (a : A) → (b : B(a)) → C{a}(b)) → (g : (a : A) → (b : B(a)) → D{a}{b}(f a b)) → (a : A) → (b : B(a)) → E{a}{b}{f a b}(g a b)
  pointwise₂,₂(_▫_) = pointwise₂,₁(pointwise₂,₁(_▫_))
  {-# INLINE pointwise₂,₂ #-}

  -- Alternative definition: pointwise₂,₃(_▫_) f g a b c = (f a b c) ▫ (g a b c)
  pointwise₂,₃ : (∀{a : A}{b : B(a)}{c : C{a}(b)} → (d : D{a}{b}(c)) → (e : E{a}{b}{c}(d)) → F{a}{b}{c}{d}(e)) → (f : (a : A) → (b : B(a)) → (c : C{a}(b)) → D{a}{b}(c)) → (g : (a : A) → (b : B(a)) → (c : C{a}(b)) → E{a}{b}(f a b c)) → (a : A) → (b : B(a)) → (c : C{a}(b)) → F{a}{b}{c}{f a b c}(g a b c)
  pointwise₂,₃(_▫_) = pointwise₂,₁(pointwise₂,₂(_▫_))
  {-# INLINE pointwise₂,₃ #-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --omega-in-omega #-}

open import Agda.Primitive

test : Setω
test = Setω

record R : Setω where
  field
     A : ∀ {ℓ} → Set ℓ

data Type : Setω where
  el : ∀ {ℓ} → Set ℓ → Type

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

-- Properties relating Initial and Terminal Objects,
-- and Product / Coproduct via op

module Categories.Object.Duality {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

open import Categories.Morphism C
open import Categories.Object.Terminal op
open import Categories.Object.Initial C
open import Categories.Object.Product op
open import Categories.Object.Coproduct C

IsInitial⇒coIsTerminal : ∀ {X} → IsInitial X → IsTerminal X
IsInitial⇒coIsTerminal is⊥ = record
  { !        = !
  ; !-unique = !-unique
  }
  where open IsInitial is⊥

⊥⇒op⊤ : Initial → Terminal
⊥⇒op⊤ i = record
  { ⊤             = ⊥
  ; ⊤-is-terminal = IsInitial⇒coIsTerminal ⊥-is-initial
  }
  where open Initial i

coIsTerminal⇒IsInitial : ∀ {X} → IsTerminal X → IsInitial X
coIsTerminal⇒IsInitial is⊤ = record
  { !        = !
  ; !-unique = !-unique
  }
  where open IsTerminal is⊤

op⊤⇒⊥ : Terminal → Initial
op⊤⇒⊥ t = record
  { ⊥            = ⊤
  ; ⊥-is-initial = coIsTerminal⇒IsInitial ⊤-is-terminal
  }
  where open Terminal t

Coproduct⇒coProduct : ∀ {A B} → Coproduct A B → Product A B
Coproduct⇒coProduct A+B = record
  { A×B      = A+B.A+B
  ; π₁       = A+B.i₁
  ; π₂       = A+B.i₂
  ; ⟨_,_⟩    = A+B.[_,_]
  ; project₁ = A+B.inject₁
  ; project₂ = A+B.inject₂
  ; unique   = A+B.unique
  }
  where
  module A+B = Coproduct A+B

coProduct⇒Coproduct : ∀ {A B} → Product A B → Coproduct A B
coProduct⇒Coproduct A×B = record
  { A+B     = A×B.A×B
  ; i₁      = A×B.π₁
  ; i₂      = A×B.π₂
  ; [_,_]   = A×B.⟨_,_⟩
  ; inject₁ = A×B.project₁
  ; inject₂ = A×B.project₂
  ; unique  = A×B.unique
  }
  where
  module A×B = Product A×B

private
  coIsTerminal⟺IsInitial : ∀ {X} (⊥ : IsInitial X) →
    coIsTerminal⇒IsInitial (IsInitial⇒coIsTerminal ⊥) ≡ ⊥
  coIsTerminal⟺IsInitial _ = ≡.refl

  IsInitial⟺coIsTerminal : ∀ {X} (⊤ : IsTerminal X) →
    IsInitial⇒coIsTerminal (coIsTerminal⇒IsInitial ⊤) ≡ ⊤
  IsInitial⟺coIsTerminal _ = ≡.refl

  ⊥⟺op⊤ : (⊤ : Terminal) → ⊥⇒op⊤ (op⊤⇒⊥ ⊤) ≡ ⊤
  ⊥⟺op⊤ _ = ≡.refl

  op⊤⟺⊥ : (⊥ : Initial) → op⊤⇒⊥ (⊥⇒op⊤ ⊥) ≡ ⊥
  op⊤⟺⊥ _ = ≡.refl

  Coproduct⟺coProduct : ∀ {A B} (p : Product A B) → Coproduct⇒coProduct (coProduct⇒Coproduct p) ≡ p
  Coproduct⟺coProduct _ = ≡.refl

  coProduct⟺Coproduct : ∀ {A B} (p : Coproduct A B) → coProduct⇒Coproduct (Coproduct⇒coProduct p) ≡ p
  coProduct⟺Coproduct _ = ≡.refl

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module Impure.LFRef.Eval where

open import Prelude
open import Data.Fin using (fromℕ≤)
open import Data.List hiding ([_])
open import Data.List.All
open import Data.List.Any
open import Data.Vec hiding (map; _∷ʳ_)
open import Data.Maybe hiding (All; Any)
open import Extensions.List as L

open import Impure.LFRef.Syntax hiding (subst)
open import Impure.LFRef.Welltyped

-- machine configuration: expression to reduce and a store
Config : Set
Config = Exp 0 × Store

!load : ∀ {i} → (μ : Store) → i < length μ → Term 0
!load {i = i} [] ()
!load {i = zero} (x ∷ μ) (s≤s p) = proj₁ x
!load {i = suc i} (x ∷ μ) (s≤s p) = !load μ p

!store : ∀ {i e} → (μ : Store) → i < length μ → Val e → Store
!store [] () v
!store {i = zero} (x ∷ μ) (s≤s p) v = (, v) ∷ μ
!store {i = suc i} (x ∷ μ) (s≤s p) v = (, v) ∷ (!store μ p v)

!call : ∀ {n m} → Exp m → (l : List (Term n)) → length l ≡ m → Exp n
!call e ts p = e exp/ subst (Vec _) p (fromList ts)

-- small steps for expressions
infix 1 _⊢_≻_
data _⊢_≻_ (𝕊 : Sig) : (t t' : Config) → Set where

  funapp-β : ∀ {fn ts μ φ} →
             (Sig.funs 𝕊) L.[ fn ]= φ →
             (p : length ts ≡ Fun.m φ) →
             -------------------------
             𝕊 ⊢ fn ·★ ts , μ ≻ (!call (Fun.body φ) ts p) , μ

  ref-val : ∀ {t μ} →
            (v : Val t) →
            ----------------------------------------------------
            𝕊 ⊢ ref (tm t) , μ ≻ (tm (loc (length μ))) , (μ ∷ʳ (, v))

  ≔-val : ∀ {i e μ} →
          (p : i < length μ) →
          (v : Val e) →
          --------------------------------------------
          𝕊 ⊢ (tm (loc i)) ≔ (tm e) , μ ≻ (tm unit) , (μ L.[ fromℕ≤ p ]≔ (, v))

  !-val : ∀ {i μ} →
          (p : i < length μ) →
          -----------------------------------------
          𝕊 ⊢ ! (tm (loc i)) , μ ≻ tm (!load μ p) , μ

  ref-clos : ∀ {e e' μ μ'} →
             𝕊 ⊢ e , μ ≻ e' , μ' →
             ---------------------------
             𝕊 ⊢ ref e , μ ≻ ref e' , μ'

  !-clos   : ∀ {e e' μ μ'} →
             𝕊 ⊢ e , μ ≻ e' , μ' →
             -----------------------
             𝕊 ⊢ ! e , μ ≻ ! e' , μ'

  ≔-clos₁  : ∀ {x x' e μ μ'} →
             𝕊 ⊢ x , μ ≻ x' , μ' →
             --------------------------
             𝕊 ⊢ x ≔ e , μ ≻ x' ≔ e , μ'

  ≔-clos₂  : ∀ {x e e' μ μ'} →
             ExpVal x →
             𝕊 ⊢ e , μ ≻ e' , μ' →
             --------------------------
             𝕊 ⊢ x ≔ e , μ ≻ x ≔ e' , μ'

infix 1 _⊢_≻ₛ_
data _⊢_≻ₛ_ (𝕊 : Sig) : (t t' : SeqExp 0 × Store) → Set where

  -- reductions
  lett-β  : ∀ {t e μ} →
            ----------------------------------------------
            𝕊 ⊢ (lett (tm t) e) , μ ≻ₛ (e seq/ (sub t)) , μ

  -- contextual closure
  ret-clos  : ∀ {e μ e' μ'} →
              𝕊 ⊢ e , μ ≻ e' , μ' →
              -------------------------------------
              𝕊 ⊢ (ret e) , μ ≻ₛ (ret e') , μ'

  lett-clos : ∀ {x e x' μ μ'} →
              𝕊 ⊢ x , μ ≻ x' , μ' →
              -------------------------------------
              𝕊 ⊢ (lett x e) , μ ≻ₛ (lett x' e) , μ'

-- reflexive-transitive closure of ≻
open import Data.Star
infix 1 _⊢_≻⋆_
_⊢_≻⋆_ : (Sig) → (c c' : SeqExp 0 × Store) → Set
𝕊 ⊢ c ≻⋆ c' = Star (_⊢_≻ₛ_ 𝕊) c c'


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

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.ReflectionSolving

private
  variable
    ℓ : Level

module Test (R : CommRing {ℓ}) where
  open CommRingStr (snd R)

  _ :   1r · (1r + 0r)
      ≡ (1r · 0r) + 1r
  _ = solve R

  _ :   1r · 0r + (1r - 1r)
      ≡ 0r - 0r
  _ = solve R

  _ : (x : fst R) → x ≡ x
  _ = solve R

  _ : (x y : fst R) → x ≡ x
  _ = solve R

  _ : (x y : fst R) → x + y ≡ y + x
  _ = solve R

  _ : (x y : fst R) → (x + y) · (x - y) ≡ x · x - y · y
  _ = solve R

  {-
    A bigger example, copied from the other example files:
  -}
  _ : (x y z : (fst R)) → (x + y) · (x + y) · (x + y) · (x + y)
                ≡ x · x · x · x + (fromℤ R 4) · x · x · x · y + (fromℤ R 6) · x · x · y · y
                  + (fromℤ R 4) · x · y · y · y + y · y · y · y
  _ = solve R

  {-
    Keep in mind, that the solver can lead to wrong error locations.
    For example, the commented code below tries to solve an equation that does not hold,
    with the result of an error at the wrong location.

  _ : (x y : (fst R)) → x ≡ y
  _ = solve R
  -}

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 Luau.RuntimeType.ToString where

open import FFI.Data.String using (String)
open import Luau.RuntimeType using (RuntimeType; function; number; nil)

runtimeTypeToString : RuntimeType → String
runtimeTypeToString function = "function"
runtimeTypeToString number = "number"
runtimeTypeToString nil = "nil"


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Inverse where

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

open import Categories.Category
import Categories.Morphism

record Inverse {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C public
  open Definitions C public
  open Categories.Morphism C

  infix 10 _⁻¹

  field
    _⁻¹ : ∀ {A B} → A ⇒ B → B ⇒ A
    pseudo-iso₁ : ∀ {A B} {f : A ⇒ B} →  f ∘ f ⁻¹ ∘ f ≈ f
    pseudo-iso₂ : ∀ {A B} {f : A ⇒ B} →  f ⁻¹ ∘ f ∘ f ⁻¹ ≈ f ⁻¹


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

module Categories.Functor.Power.NaturalTransformation {o ℓ e : Level} (C : Category o ℓ e) where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin; inject+; raise)
open import Data.Sum using (_⊎_; [_,_]′; inj₁; inj₂)
open import Function using () renaming (_∘_ to _∙_)
open import Function using () renaming (_∘_ to _∙_)
open import Data.Product using (_,_)

import Categories.Functor.Power as Power
module Pow = Power C
open Pow
open import Categories.Functor.Bifunctor using (Bifunctor)

-- open import Categories.Functor.Bifunctor.NaturalTransformation renaming (id to idⁿ; _≡_ to _≡ⁿ_)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper; _∘ˡ_)
open import Categories.Category.Product using (_※ⁿ_)
open import Categories.Functor using (Functor; module Functor)

flattenPⁿ : {D : Category o ℓ e} {m n : ℕ} {F G : Powerfunctor′ D (Fin m ⊎ Fin n)} (η : NaturalTransformation F G) →
            NaturalTransformation (flattenP F) (flattenP G)
flattenPⁿ {m = m} {n} η = record
  { η           = λ Xs → η.η (Xs ∙ pack)
  ; commute     = λ fs → η.commute (fs ∙ pack)
  ; sym-commute = λ fs → η.sym-commute (fs ∙ pack)
  }
  where
  private module η = NaturalTransformation η
  pack = [ inject+ n , raise m ]′

reduceN′ : ∀ {i j : Level} {I : Set i} {J : Set j}  {F F′ : Powerendo′ I} {G G′ : Powerendo′ J}
  (H : Bifunctor C C C)
  (φ : NaturalTransformation F F′)  (γ : NaturalTransformation G G′) → NaturalTransformation (reduce′ H F G) (reduce′ H F′ G′)
reduceN′ {I = I} {J} {F} {F′} {G} {G′} H φ γ = ntHelper record
  { η = my-η
  ; commute = λ {Xs Ys} → my-commute Xs Ys
  }
  where
  module C = Category C
  module F = Functor F
  module F′ = Functor F′
  module G = Functor G
  module G′ = Functor G′
  module φ = NaturalTransformation φ
  module γ = NaturalTransformation γ
  module H = Functor H
  module L = Functor (reduce′ H F G)
  module R = Functor (reduce′ H F′ G′)
  my-η : ∀ Xs → C [ L.F₀ Xs , R.F₀ Xs ]
  my-η Xs = H.F₁ ((φ.η (Xs ∙ inj₁)) , (γ.η (Xs ∙ inj₂)))
  my-commute : ∀ Xs Ys fs → C.CommutativeSquare (L.F₁ fs) (my-η Xs) (my-η Ys) (R.F₁ fs)
  my-commute Xs Ys fs = begin
      my-η Ys ∘ L.F₁ fs                             ≈˘⟨ H.homomorphism ⟩
      H.F₁ ((φ.η _ ∘ F.F₁ _) , (γ.η _ ∘ G.F₁ _))    ≈⟨ H.F-resp-≈ ((φ.commute _) , (γ.commute _)) ⟩
      H.F₁ ((F′.F₁ _ ∘ φ.η _) , (G′.F₁ _ ∘ γ.η _))  ≈⟨ H.homomorphism ⟩
      R.F₁ fs ∘ my-η Xs
    ∎
    where
    open C using (_∘_)
    open C.HomReasoning

-- Giving the implicits below is not necessary, but makes typechecking faster
reduceN : {m n : ℕ} {F F′ : Powerendo m} {G G′ : Powerendo n}
  (H : Bifunctor C C C)  (φ : NaturalTransformation F F′) (γ : NaturalTransformation G G′) →
  NaturalTransformation (reduce H F G) (reduce H F′ G′)
reduceN  {F = f} {f′} {g} {g′} H φ γ = flattenPⁿ  {F = reduce′ H f g} {G = reduce′ H f′ g′} (reduceN′ H φ γ)

overlapN : {n : ℕ} {F F′ : Powerendo n} {G G′ : Powerendo n}
           (H : Bifunctor C C C) (φ : NaturalTransformation F F′) (γ : NaturalTransformation G G′) →
           NaturalTransformation (overlaps H F G) (overlaps H F′ G′)
overlapN H φ γ = H ∘ˡ (φ ※ⁿ γ)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Record declarations can now contain arbitrary declarations.
-- These are included in the projection module.
module FancyRecordModule where

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

record Exist {A : Set}(P : A -> Set) : Set where
  field witness : A
  x = witness
  field proof   : P x
  silly : Nat -> Nat
  silly zero = zero
  silly (suc n) = silly n

postulate
  P : Nat -> Set
  e : Exist P

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

test : Exist.silly e (suc zero) == zero
test = refl


text:
module ExtendedLambdaCase where

data Bool : Set where
  true false : Bool

data Void : Set where

foo : Bool -> Bool -> Bool -> Bool
foo = λ { x → λ { y z → {!!} } }

module parameterised {A : Set}(B : A -> Set) where

  data Bar : (Bool -> Bool) -> Set where
    baz : (t : Void) -> Bar λ { x → {!!} }

  -- with hidden argument
  data Bar' : (Bool -> Bool) -> Set where
    baz' : {t : Void} -> (t' : Void) -> Bar' λ { x' → {!!} }

baz : Bool -> {w : Bool} -> Bool
baz = λ { z {w} → {!!} }

another-short-name : {A : Set} -> (A -> {x : A} -> A -> A)
another-short-name = {! λ { a {x} b → a } !}

f : Set
f =  (y : Bool) -> parameterised.Bar {Bool}(λ _ → Void) (λ { true → true ; false → false })


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of < to ≤, along with a number of properties
------------------------------------------------------------------------

-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
-- relation equivalent to the original one (and similarly for
-- < → ≤ → <).

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

open import Relation.Binary

module Relation.Binary.Construct.StrictToNonStrict
  {a ℓ₁ ℓ₂} {A : Set a}
  (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂)
  where

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

------------------------------------------------------------------------
-- Conversion

-- _<_ can be turned into _≤_ as follows:

_≤_ : Rel A _
x ≤ y = (x < y) ⊎ (x ≈ y)

------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = inj₁

reflexive : _≈_ ⇒ _≤_
reflexive = inj₂

antisym : IsEquivalence _≈_ → Transitive _<_ → Irreflexive _≈_ _<_ →
          Antisymmetric _≈_ _≤_
antisym eq trans irrefl = as
  where
  module Eq = IsEquivalence eq

  as : Antisymmetric _≈_ _≤_
  as (inj₂ x≈y) _          = x≈y
  as (inj₁ _)   (inj₂ y≈x) = Eq.sym y≈x
  as (inj₁ x<y) (inj₁ y<x) =
    ⊥-elim (trans∧irr⟶asym {_≈_ = _≈_} Eq.refl trans irrefl x<y y<x)

trans : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → Transitive _<_ →
        Transitive _≤_
trans eq (respʳ , respˡ) <-trans = tr
  where
  module Eq = IsEquivalence eq

  tr : Transitive _≤_
  tr (inj₁ x<y) (inj₁ y<z) = inj₁ $ <-trans x<y y<z
  tr (inj₁ x<y) (inj₂ y≈z) = inj₁ $ respʳ y≈z x<y
  tr (inj₂ x≈y) (inj₁ y<z) = inj₁ $ respˡ (Eq.sym x≈y) y<z
  tr (inj₂ x≈y) (inj₂ y≈z) = inj₂ $ Eq.trans x≈y y≈z

<-≤-trans : Transitive _<_ → _<_ Respectsʳ _≈_ → Trans _<_ _≤_ _<_
<-≤-trans trans respʳ x<y (inj₁ y<z) = trans x<y y<z
<-≤-trans trans respʳ x<y (inj₂ y≈z) = respʳ y≈z x<y

≤-<-trans : Symmetric _≈_ → Transitive _<_ → _<_ Respectsˡ _≈_ → Trans _≤_ _<_ _<_
≤-<-trans sym trans respˡ (inj₁ x<y) y<z = trans x<y y<z
≤-<-trans sym trans respˡ (inj₂ x≈y) y<z = respˡ (sym x≈y) y<z

≤-respʳ-≈ : Transitive _≈_ → _<_ Respectsʳ _≈_ → _≤_ Respectsʳ _≈_
≤-respʳ-≈ trans respʳ y'≈y (inj₁ x<y') = inj₁ (respʳ y'≈y x<y')
≤-respʳ-≈ trans respʳ y'≈y (inj₂ x≈y') = inj₂ (trans x≈y' y'≈y)

≤-respˡ-≈ : Symmetric _≈_ → Transitive _≈_ → _<_ Respectsˡ _≈_ → _≤_ Respectsˡ _≈_
≤-respˡ-≈ sym trans respˡ x'≈x (inj₁ x'<y) = inj₁ (respˡ x'≈x x'<y)
≤-respˡ-≈ sym trans respˡ x'≈x (inj₂ x'≈y) = inj₂ (trans (sym x'≈x) x'≈y)

≤-resp-≈ : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → _≤_ Respects₂ _≈_
≤-resp-≈ eq (respʳ , respˡ) = ≤-respʳ-≈ Eq.trans respʳ , ≤-respˡ-≈ Eq.sym Eq.trans respˡ
  where module Eq = IsEquivalence eq

total : Trichotomous _≈_ _<_ → Total _≤_
total <-tri x y with <-tri x y
... | tri< x<y x≉y x≯y = inj₁ (inj₁ x<y)
... | tri≈ x≮y x≈y x≯y = inj₁ (inj₂ x≈y)
... | tri> x≮y x≉y x>y = inj₂ (inj₁ x>y)

decidable : Decidable _≈_ → Decidable _<_ → Decidable _≤_
decidable ≈-dec <-dec x y with ≈-dec x y | <-dec x y
... | yes x≈y | _       = yes (inj₂ x≈y)
... | no  x≉y | yes x<y = yes (inj₁ x<y)
... | no  x≉y | no  x≮y = no [ x≮y , x≉y ]′

decidable' : Trichotomous _≈_ _<_ → Decidable _≤_
decidable' compare x y with compare x y
... | tri< x<y _   _ = yes (inj₁ x<y)
... | tri≈ _   x≈y _ = yes (inj₂ x≈y)
... | tri> x≮y x≉y _ = no [ x≮y , x≉y ]′

------------------------------------------------------------------------
-- Converting structures

isPreorder₁ : IsPreorder _≈_ _<_ → IsPreorder _≈_ _≤_
isPreorder₁ PO = record
  { isEquivalence = S.isEquivalence
  ; reflexive     = reflexive
  ; trans         = trans S.isEquivalence S.∼-resp-≈ S.trans
  }
  where module S = IsPreorder PO

isPreorder₂ : IsStrictPartialOrder _≈_ _<_ → IsPreorder _≈_ _≤_
isPreorder₂ SPO = record
  { isEquivalence = S.isEquivalence
  ; reflexive     = reflexive
  ; trans         = trans S.isEquivalence S.<-resp-≈ S.trans
  }
  where module S = IsStrictPartialOrder SPO

isPartialOrder : IsStrictPartialOrder _≈_ _<_ → IsPartialOrder _≈_ _≤_
isPartialOrder SPO = record
  { isPreorder = isPreorder₂ SPO
  ; antisym    = antisym S.isEquivalence S.trans S.irrefl
  }
  where module S = IsStrictPartialOrder SPO

isTotalOrder : IsStrictTotalOrder _≈_ _<_ → IsTotalOrder _≈_ _≤_
isTotalOrder STO = record
  { isPartialOrder = isPartialOrder S.isStrictPartialOrder
  ; total          = total S.compare
  }
  where module S = IsStrictTotalOrder STO

isDecTotalOrder : IsStrictTotalOrder _≈_ _<_ → IsDecTotalOrder _≈_ _≤_
isDecTotalOrder STO = record
  { isTotalOrder = isTotalOrder STO
  ; _≟_          = S._≟_
  ; _≤?_         = decidable' S.compare
  }
  where module S = IsStrictTotalOrder STO


text:
record R : Set₂ where
  field
    f : Set₁

f : Set → R
f .R.f = Set


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An explanation about how to use the solver in Tactic.MonoidSolver.
------------------------------------------------------------------------

open import Algebra

module README.Tactic.MonoidSolver {a ℓ} (M : Monoid a ℓ) where

open Monoid M

open import Data.Nat as Nat using (ℕ; suc; zero; _+_)
open import Data.Nat.Properties as Properties using (+-0-monoid; +-comm)
open import Relation.Binary.Reasoning.Setoid setoid

open import Tactic.MonoidSolver using (solve; solve-macro)

-- The monoid solver is capable to of solving equations without having
-- to specify the equation itself in the proof.

example₁ : ∀ x y z → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z) ∙ ε
example₁ x y z = solve M

-- The solver can also be used in equational reasoning.

example₂ : ∀ w x y z → w ≈ x → (w ∙ y) ∙ z ≈ x ∙ (y ∙ z) ∙ ε
example₂ w x y z w≈x = begin
  (w ∙ y) ∙ z      ≈⟨ ∙-congʳ (∙-congʳ w≈x) ⟩
  (x ∙ y) ∙ z      ≈⟨ solve M ⟩
  x ∙ (y ∙ z) ∙ ε  ∎


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.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Impl.Base.Types

open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle
open import LibraBFT.Impl.Handle.Properties
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Concrete.System
open        EpochConfig
open import LibraBFT.Yasm.Types
open import LibraBFT.Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms PeerCanSignForPK (λ {st} {part} {pk} → PeerCanSignForPK-stable {st} {part} {pk})

-- In this module, we define two "implementation obligations"
-- (ImplObligationᵢ for i ∈ {1 , 2}), which are predicates over
-- reachable states of a system defined by
-- 'LibraBFT.Concrete.System.Parameters'.  These two properties relate
-- votes sent by the same sender, ensuring that if they are for the
-- same epoch and round, then they vote for the same blockID; the
-- first relates a vote output by the handler to a vote sent
-- previously, and the second relates two votes both sent by the
-- handler.
--
-- We then prove that, if an implementation satisfies these two
-- semantic obligations, along with a structural one about messages
-- sent by honest peers in the implementation, then the implemenation
-- satisfies the LibraBFT.Abstract.Properties.VotesOnce invariant.

module LibraBFT.Concrete.Properties.VotesOnce where
 -- TODO-3: This may not be the best way to state the implementation obligation.  Why not reduce
 -- this as much as possible before giving the obligation to the implementation?  For example, this
 -- will still require the implementation to deal with hash collisons (v and v' could be different,
 -- but yield the same bytestring and therefore same signature).  Also, avoid the need for the
 -- implementation to reason about messages sent by step-cheat, or give it something to make this
 -- case easy to eliminate.

 ImplObligation₁ : Set (ℓ+1 ℓ-RoundManager)
 ImplObligation₁ =
   ∀{pid pid' s' outs pk}{pre : SystemState}
   → ReachableSystemState pre
   -- For any honest call to /handle/ or /init/,
   → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
   → ∀{v m v' m'} → Meta-Honest-PK pk
   -- For signed every vote v of every outputted message
   → v  ⊂Msg m  → send m ∈ outs
   → (sig : WithVerSig pk v) → ¬ (∈GenInfo (ver-signature sig))
   -- If v is really new and valid
   → ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool pre)) → PeerCanSignForPK (StepPeer-post {pre = pre} (step-honest sps)) v pid pk
   -- And if there exists another v' that has been sent before
   → v' ⊂Msg m' → (pid' , m') ∈ (msgPool pre)
   → (sig' : WithVerSig pk v') → ¬ (∈GenInfo (ver-signature sig'))
   -- If v and v' share the same epoch and round
   → v ^∙ vEpoch ≡ v' ^∙ vEpoch
   → v ^∙ vRound ≡ v' ^∙ vRound
   ----------------------------------------------------------
   -- Then an honest implemenation promises v and v' vote for the same blockId.
   → v ^∙ vProposedId ≡ v' ^∙ vProposedId

 ImplObligation₂ : Set (ℓ+1 ℓ-RoundManager)
 ImplObligation₂ =
   ∀{pid s' outs pk}{pre : SystemState}
   → ReachableSystemState pre
   -- For any honest call to /handle/ or /init/,
   → (sps : StepPeerState pid (msgPool pre) (initialised pre) (peerStates pre pid) (s' , outs))
   → ∀{v m v' m'}
   → Meta-Honest-PK pk
   -- For every vote v represented in a message output by the call
   → v  ⊂Msg m  → send m ∈ outs
   → (sig : WithVerSig pk v) → ¬ (∈GenInfo (ver-signature sig))
   -- If v is really new and valid
   → ¬ (MsgWithSig∈ pk (ver-signature sig) (msgPool pre)) → PeerCanSignForPK (StepPeer-post {pre = pre} (step-honest sps)) v pid pk

   -- And if there exists another v' that is also new and valid
   → v' ⊂Msg m'  → send m' ∈ outs
   → (sig' : WithVerSig pk v') → ¬ (∈GenInfo (ver-signature sig'))
   → ¬ (MsgWithSig∈ pk (ver-signature sig') (msgPool pre)) → PeerCanSignForPK (StepPeer-post {pre = pre} (step-honest sps)) v' pid pk

   -- If v and v' share the same epoch and round
   → v ^∙ vEpoch ≡ v' ^∙ vEpoch
   → v ^∙ vRound ≡ v' ^∙ vRound
   ----------------------------------------------------------
   -- Then, an honest implemenation promises v and v' vote for the same blockId.
   → v ^∙ vProposedId ≡ v' ^∙ vProposedId

 -- Next, we prove that, given the necessary obligations,
 module Proof
   (sps-corr : StepPeerState-AllValidParts)
   (Impl-VO1 : ImplObligation₁)
   (Impl-VO2 : ImplObligation₂)
   where

  -- Any reachable state satisfies the VO rule for any epoch in the system.
  module _ (st : SystemState)(r : ReachableSystemState st)(𝓔 : EpochConfig) where

   open Structural sps-corr
   -- Bring in IntSystemState
   open WithSPS sps-corr
   open PerState st r
   open PerEpoch 𝓔

   open import LibraBFT.Concrete.Obligations.VotesOnce 𝓔 (ConcreteVoteEvidence 𝓔) as VO

   -- The VO proof is done by induction on the execution trace leading to 'st'. In
   -- Agda, this is 'r : RechableSystemState st' above.

   private

    -- From this point onwards, it might be easier to read this proof starting at 'voo'
    -- at the end of the file. Next, we provide an overview the proof.
    --
    -- We wish to prove that, for any two votes v and v' cast by an honest α in the message
    -- pool of a state st, if v and v' have equal rounds and epochs, then they vote for the
    -- same block.
    --
    -- The base case and the case for a new epoch in the system are trivial. For the base case
    -- we get to a contradiction because it's not possible to have any message in the msgpool.
    --
    -- Regarding the PeerStep case. The induction hypothesis tells us that the property holds
    -- in the pre-state.  Next, we reason about the post-state.  We start by analyzing whether
    -- v and v' have been sent as outputs of the PeerStep under scrutiny or were already in
    -- the pool before.
    --
    -- There are four possibilities:
    --
    --   i) v and v' were aleady present in the msgPool before: use induction hypothesis.
    --  ii) v and v' are both in the output produced by the PeerStep under scrutiny.
    -- iii) v was present before, but v' is new.
    --  iv) v' was present before, but v is new.
    --
    -- In order to obtain this four possiblities we invoke newMsg⊎msgSent4 lemma, which
    -- receives proof that some vote is in a message that is in the msgPool of the post state
    -- and returns evidence that either the vote is new or that some message with the same
    -- signature was sent before.
    --
    -- Case (i) is trivial; cases (iii) and (iv) are symmetric and reduce to an implementation
    -- obligation (Impl-VO1) and case (ii) reduces to a different implementation obligation
    -- (Impl-VO2).

    VotesOnceProof :
       ∀ {v v' pk} {st : SystemState}
       → ReachableSystemState st
       → Meta-Honest-PK pk
       → (vv  : WithVerSig pk v)  → MsgWithSig∈ pk (ver-signature vv)  (msgPool st)
       → (vv' : WithVerSig pk v') → MsgWithSig∈ pk (ver-signature vv') (msgPool st)
       → v ^∙ vEpoch ≡ v' ^∙ vEpoch
       → v ^∙ vRound ≡ v' ^∙ vRound
       → v ^∙ vProposedId ≡ v' ^∙ vProposedId
    VotesOnceProof step-0 _ _ msv _ _ _ _ = ⊥-elim (¬Any[] (msg∈pool msv))
    VotesOnceProof {v} {v'} (step-s r theStep) pkH vv msv vv' msv' eid≡ r≡
       with msgSameSig msv | msgSameSig msv'
    ...| refl | refl
      with sameSig⇒sameVoteDataNoCol (msgSigned msv)  vv  (msgSameSig msv )
         | sameSig⇒sameVoteDataNoCol (msgSigned msv') vv' (msgSameSig msv')
    ...| refl | refl
       with ∈GenInfo? (₋vSignature (msgPart msv)) | ∈GenInfo? (₋vSignature (msgPart msv'))
    ...| yes init  | yes init' =  genVotesConsistent (msgPart msv) (msgPart msv') init init'
       -- A signature in GenInfo is for a vote with round 0, and a signature for which we have a
       -- MsgWithSig∈ that is not in GenInfo and is for an honest PK is for a round ≢ 0, so we can
       -- derive a contradiction using r≡.
    ...| yes init  | no  ¬init = ⊥-elim (¬genVotesRound≢0 (step-s r theStep) pkH msv' ¬init ((trans (sym r≡) (genVotesRound≡0 vv  init))))
    ...| no  ¬init | yes init  = ⊥-elim (¬genVotesRound≢0 (step-s r theStep) pkH msv  ¬init ((trans r≡       (genVotesRound≡0 vv' init))))
    ...| no  ¬init | no ¬init'
       with theStep
    ...| step-peer cheat@(step-cheat c)
       with ¬cheatForgeNew cheat refl unit pkH msv  ¬init
          | ¬cheatForgeNew cheat refl unit pkH msv' ¬init'
    ...| msb4 | m'sb4
       with  msgSameSig msb4 | msgSameSig m'sb4
    ...| refl | refl = VotesOnceProof r pkH vv msb4 vv' m'sb4 eid≡ r≡

    VotesOnceProof (step-s r theStep) pkH vv msv vv' msv' eid≡ r≡
       | refl | refl
       | refl | refl
       | no  ¬init | no ¬init'
       | step-peer (step-honest stPeer)
       with newMsg⊎msgSentB4 r stPeer pkH (msgSigned msv)  ¬init  (msg⊆ msv)  (msg∈pool msv)
          | newMsg⊎msgSentB4 r stPeer pkH (msgSigned msv') ¬init' (msg⊆ msv') (msg∈pool msv')
    ...| inj₂ msb4                   | inj₂ m'sb4
         = VotesOnceProof r pkH vv msb4 vv' m'sb4 eid≡ r≡
    ...| inj₁ (m∈outs , vspk , newV) | inj₁ (m'∈outs , v'spk , newV')
      = Impl-VO2 r stPeer pkH (msg⊆ msv) m∈outs (msgSigned msv) ¬init newV vspk
                 (msg⊆ msv') m'∈outs (msgSigned msv') ¬init' newV' v'spk eid≡ r≡
    ...| inj₁ (m∈outs , vspk , newV) | inj₂ m'sb4
       with sameSig⇒sameVoteData (msgSigned m'sb4) vv' (msgSameSig m'sb4)
    ...| inj₁ hb   = ⊥-elim (meta-sha256-cr hb)
    ...| inj₂ refl rewrite sym (msgSameSig msv')
      = Impl-VO1 r stPeer pkH (msg⊆ msv) m∈outs (msgSigned msv) ¬init newV vspk
                 (msg⊆ m'sb4) (msg∈pool m'sb4) (msgSigned m'sb4) (¬subst ¬init' (msgSameSig m'sb4)) eid≡ r≡

    VotesOnceProof (step-s r theStep) pkH vv msv vv' msv' eid≡ r≡
       | refl | refl
       | refl | refl
       | no  ¬init | no ¬init'
       | step-peer (step-honest stPeer)
       | inj₂ msb4                   | inj₁ (m'∈outs , v'spk , newV')
       with sameSig⇒sameVoteData (msgSigned msb4) vv (msgSameSig msb4)
    ...| inj₁ hb = ⊥-elim (meta-sha256-cr hb)
    ...| inj₂ refl
      = sym (Impl-VO1 r stPeer pkH (msg⊆ msv') m'∈outs (msgSigned msv') ¬init' newV' v'spk
                      (msg⊆ msb4) (msg∈pool msb4) (msgSigned msb4) (¬subst ¬init (msgSameSig msb4)) (sym eid≡) (sym r≡))

   voo : VO.Type IntSystemState
   voo hpk refl sv refl sv' round≡
      with vmsg≈v (vmFor sv) | vmsg≈v (vmFor sv')
   ...| refl | refl
       = let ver = vmsgSigned (vmFor sv)
             mswsv = mkMsgWithSig∈ (nm (vmFor sv)) (cv (vmFor sv)) (cv∈nm (vmFor sv))
                                    _ (nmSentByAuth sv) (vmsgSigned (vmFor sv)) refl
             ver' = vmsgSigned (vmFor sv')
             mswsv' = mkMsgWithSig∈ (nm (vmFor sv')) (cv (vmFor sv')) (cv∈nm (vmFor sv'))
                                     _ (nmSentByAuth sv') (vmsgSigned (vmFor sv')) refl
             epoch≡ = trans (vmsgEpoch (vmFor sv)) (sym (vmsgEpoch (vmFor sv')))
         in VotesOnceProof r hpk ver mswsv ver' mswsv' epoch≡ round≡

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
-- exercises-04-thursday.agda

open import mylib

-- 1. Coinduction

{-
  Now your task is to define multiplication _*∞_ for conatural numbers.

  This is harder then it sounds. Why? Because to check termination of
  corecursive programs agda needs to make sure that if you want to find out a
  finite amout of information about the result of the function it only needs a
  finite amount of information about its inputs. Such a function is called
  productive. And agda isn't very clever in figuring this out, it has to be
  obvious from the program (similar as structural recursion has to be
  obviously structural).
  You should *not* use the TERMINATING pragma in your solution.
  But it may be useful for experiments.

  _*_ : ℕ → ℕ → ℕ
  zero * n = zero
  suc m * n = n + m * n
-}

{-
_*∞_ :  ℕ∞ → ℕ∞ → ℕ∞
m *∞ n = {!!}
-}

aux : ℕ∞ → ℕ∞ → ℕ∞ → ℕ∞  -- aux l m n = l +∞ (m *∞ n)
pred∞ (aux l m n) with pred∞ l
pred∞ (aux l m n) | nothing with  pred∞ m
pred∞ (aux l m n) | nothing | nothing = nothing
pred∞ (aux l m n) | nothing | just m' with pred∞ n
pred∞ (aux l m n) | nothing | just m' | nothing = nothing
pred∞ (aux l m n) | nothing | just m' | just n' = just (aux n' m' n)
pred∞ (aux l m n) | just l' = just (aux l' m n)

{-# TERMINATING #-}
_*∞_ :  ℕ∞ → ℕ∞ → ℕ∞
m *∞ n = aux zero∞ m n
{-
pred∞ (m *∞ n) with pred∞ m
... | nothing = nothing
... | just m' with pred∞ n
...           | nothing = nothing
...           | just n' = just (n' +∞ (m' *∞ n))
-}

{-
with pred∞ m
...| nothing = zero∞
...| just m' with pred∞ n
...|              nothing = zero∞
...|              just n' = n' +∞ (m' *∞ n)
-}

-- pred∞ (∞ *∞ zero∞) = nothing
-- here are some testing tools
ℕ→ℕ∞ : ℕ → ℕ∞
ℕ→ℕ∞ zero = zero∞
ℕ→ℕ∞ (suc n) = suc∞ (ℕ→ℕ∞ n)

{-# TERMINATING #-} -- a lie
-- this function is a cheat - it doesn't terminate for ∞
ℕ∞→ℕ : ℕ∞ → ℕ
ℕ∞→ℕ n with pred∞ n
ℕ∞→ℕ n | nothing = 0
ℕ∞→ℕ n | just n' = suc (ℕ∞→ℕ n')

-- My unit-test
x3*5 = ℕ∞→ℕ (ℕ→ℕ∞ 3 *∞ ℕ→ℕ∞ 5)

-- 2. Dependent types  Fin

{-
  Define the following operations on Fin
  - max returns the largest element in Fin (suc n)
  - emb embeds Fin n into Fin (suc n) without changing its values
  - inv inverts the order of elements in Fin n
-}

max : (n : ℕ) → Fin (suc n)
max zero = zero
max (suc n) = suc (max n)

emb : {n : ℕ} → Fin n → Fin (suc n)
emb zero = zero
emb (suc m) = suc (emb m)

inv : {n : ℕ} → Fin n → Fin n
inv zero = max _
inv (suc i) = emb (inv i)

-- 2. Dependent types : Vec

Vector : ℕ → Set {- Vec n is an n-dimensional vector -}
Vector m = Vec ℕ m

Matrix : ℕ → ℕ → Set {- Matrix m n is an m x n Matrix -}
Matrix m n = Vec (Vector n) m

m3 : Matrix 3 3
m3 = (1 ∷ 2 ∷ 3 ∷ [])
    ∷ (4 ∷ 5 ∷ 6 ∷ [])
    ∷ (7 ∷ 8 ∷ 9 ∷ [])
    ∷ []

m4 : Matrix 3 2
m4 = (1 ∷ 2 ∷ [])
    ∷ (4 ∷ 5 ∷ [])
    ∷ (7 ∷ 8 ∷ [])
    ∷ []

-- Define the operation transpose which switches columns and rows.
-- Applicative functor, Vec _ n is an applicative functor
-- mapVec : (A → B) → Vec A n → Vec B n
-- return : A → Vec A n
-- app : Vec (A → B) n → Vec A n → Vec B n
-- mapVec f as = app (return f) as

return : {A : Set}{n : ℕ} → A → Vec A n
return {n = zero} a = []
return {n = suc m} a = a ∷ return {n = m} a

app : {A B : Set}{n : ℕ} → Vec (A → B) n → Vec A n → Vec B n
app [] [] = []
app (a2b ∷ a2bs) (a ∷ as) = a2b a ∷ app a2bs as

transpose : {m n : ℕ} → Matrix m n → Matrix n m
transpose [] = return []
transpose (ns ∷ mns) = app (app (return _∷_) ns) (transpose mns)

{-
transpose : {m n : ℕ} → Matrix m n → Matrix n m
transpose [] = {!!} -- [ [] , [] , [] ] m empty rows
transpose (ns ∷ mns) = {!transpose mns!}
-}
-- if ns = [1 , 2 , 3]
-- transpose mns = [ns1 , ns2 , ns3] => [1 ∷ ns1 , 2 ∷ ns2 , 3 ∷ ns3]

test8 : Matrix 2 3
test8 = transpose m4

test9 : Matrix 3 3
test9 = transpose m3

max_stars_repo_path: Type Theory/exercises-04-thursday.agda

max_issues_repo_path: Type Theory/exercises-04-thursday.agda

max_forks_repo_path: Type Theory/exercises-04-thursday.agda


text:
module Async where

open import Data.Fin
open import Data.List hiding (drop)
open import Data.List.All

open import Typing renaming (send to ssend ; recv to srecv)
open import Syntax
open import Values

-- an asynchronous channel is a promise for a channel
ASession DSession : STypeF SType → STypeF SType
ASession s = srecv (TChan s) (delay send!)
DSession s = dualF (ASession s)

AChan DChan : STypeF SType → Type
AChan s = TChan (ASession s)
DChan s = TChan (DSession s)

Promise : (s : SType) → Type
Promise s = TPair (AChan (SType.force s)) (DChan (SType.force s))

new-promise : ∀ {Φ} → All Unr Φ → (s : SType) → Expr Φ (Promise s)
new-promise unr-Φ s = new unr-Φ (delay (ASession (SType.force s)))

-- create an async channel
anew : ∀ {Φ}
  → (unr-Φ : All Unr Φ)
  → (s : SType)
  → Expr Φ (TPair (AChan (SType.force s)) (AChan (SType.force (dual s))))
anew unr-Φ s =
  letbind (split-all-unr unr-Φ) (new unr-Φ s)
  (letpair (left (split-all-unr unr-Φ)) (here unr-Φ)
  (letbind (rght (rght (split-all-unr unr-Φ))) (new-promise unr-Φ s)
  (letpair (left (rght (rght (split-all-unr unr-Φ)))) (here unr-Φ)
  (letbind (rght (rght (rght (rght (split-all-unr unr-Φ))))) (new-promise unr-Φ (dual s))
  (letpair (left (rght (rght (rght (rght (split-all-unr unr-Φ)))))) (here unr-Φ)
  (letbind (rght (rght (rght (left (left (rght (split-all-unr unr-Φ)))))))
           (fork (letbind (left (left (split-all-unr unr-Φ))) (send (left (rght (split-all-unr unr-Φ))) (here unr-Φ) (here unr-Φ))
                 (wait (here unr-Φ))))
  (letbind (drop UUnit (rght (left (rght (left (split-all-unr unr-Φ))))))
           (fork (letbind (left (left (split-all-unr unr-Φ))) (send (left (rght (split-all-unr unr-Φ))) (here unr-Φ) (here unr-Φ))
                 (wait (here unr-Φ))))
  (pair (drop UUnit (rght (left (split-all-unr unr-Φ))))
        (here unr-Φ) (here unr-Φ)))))))))

asend : ∀ {Φ Φ₁ Φ₂ s t}
  → (sp : Split Φ Φ₁ Φ₂)
  → (ch : (AChan (ssend t s)) ∈ Φ₁)
  → (vt : t ∈ Φ₂)
  → Expr Φ (AChan (SType.force s))
asend {Φ} {s = s} sp ch vt =
  letbind (split-all-right Φ) (new-promise [] s)
  (letpair (left (split-all-right Φ)) (here [])
  (letbind (rght (left (split-all-left Φ)))
           -- read actual channel & actual send & send depleted channel & close
           (fork (letbind (rght sp) (recv ch)
                 (letpair (left (split-all-right _)) (here [])
                 (letbind (left (split-all-right _)) (close (here []))
                 (letbind (drop UUnit (left (rght (split-all-left _)))) (send (left (split-all-right _)) (here []) vt)
                 (letbind (left (left [])) (send (rght (left [])) (here []) (here []))
                 (letbind (left []) (wait (here []))
                 (var (here [])))))))))
  (var (there UUnit (here [])))))

-- receive is a blocking operation!
arecv : ∀ {Φ s t}
      → (ch : (AChan (srecv t s)) ∈ Φ)
      → Expr Φ (TPair (AChan (SType.force s)) t)
arecv {s = s} ch =
  letbind (split-all-right _) (new-promise [] s)
  (letpair (left (split-all-right _)) (here [])
  (letbind (rght (rght (split-all-left _))) (recv ch)
  (letpair (left (rght (rght (split-all-right _)))) (here [])
  (letbind (left (rght (rght (rght [])))) (close (here []))
  (letbind (drop UUnit (left (rght (rght [])))) (recv (here []))
  (letpair (left (rght (rght []))) (here [])
  (letbind (left (rght (rght (left []))))
           (fork (letbind (left (left []))
                          (send (rght (left [])) (here []) (here []))
                          (wait (here []))))
  (pair (drop UUnit (rght (left []))) (here []) (here [])))))))))

aclose : ∀ {Φ}
      → (ch : AChan send! ∈ Φ)
      → Expr Φ TUnit
aclose ch =
  fork (letbind (split-all-left _) (recv ch)
       (letpair (left []) (here [])
       (letbind (left (rght [])) (close (here []))
       (close (there UUnit (here []))))))

await : ∀ {Φ}
      → (ch : AChan send? ∈ Φ)
      → Expr Φ TUnit
await ch =
  fork (letbind (split-all-left _) (recv ch)
       (letpair (left []) (here [])
       (letbind (left (rght [])) (close (here []))
       (wait (there UUnit (here []))))))

anselect : ∀ {Φ m alt}
      → (lab : Fin m)
      → (ch : AChan (sintN m alt) ∈ Φ)
      → Expr Φ (AChan (SType.force (alt lab)))
anselect {alt = alt} lab ch =
  letbind (split-all-right _)
          (new-promise [] (alt lab))
  (letpair (left (split-all-right _)) (here [])
  (letbind (rght (left (split-all-left _)))
           (fork (letbind (rght (split-all-left _)) (recv ch)
                 (letpair (left (rght [])) (here [])
                 (letbind (left (rght (rght []))) (close (here []))
                 (letbind (drop UUnit (left (rght []))) (nselect lab (here []))
                 (letbind (left (left [])) (send (rght (left [])) (here []) (here []))
                 (wait (here []))))))))
  (var (there UUnit (here [])))))

-- branching is a blocking operation!
anbranch : ∀ {Φ m alt Φ₁ Φ₂ t}
      → (sp : Split Φ Φ₁ Φ₂)
      → (ch : AChan (sextN m alt) ∈ Φ₁)
      → (ealts : (i : Fin m) → Expr (AChan (SType.force (alt i)) ∷ Φ₂) t)
      → Expr Φ t
anbranch{alt = alt} sp ch ealts =
  letbind sp (recv ch)
  (letpair (left (split-all-right _)) (here [])
  (letbind (left (split-all-right _)) (close (here []))
  (nbranch (drop UUnit (left (split-all-right _))) (here [])
  (λ i → letbind (split-all-right _) (new-promise [] (alt i))
         (letpair (left (split-all-right _)) (here [])
         (letbind (rght (left (left (split-all-right _))))
                  (fork (letbind (left (left [])) (send (left (rght [])) (here []) (here []))
                        (wait (here []))))
         (letbind (drop UUnit (left (split-all-right _))) (var (here []))
                  (ealts i))))))))

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text: module Sessions.Semantics where


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

module Categories.Functor.Monoidal.Properties where

open import Level
open import Data.Product using (_,_)

open import Categories.Category
open import Categories.Category.Monoidal
open import Categories.Category.Cartesian.Structure
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.Functor.Cartesian
open import Categories.Functor.Monoidal
open import Categories.Functor.Monoidal.Braided as Braided
open import Categories.Functor.Monoidal.Symmetric as Symmetric
open import Categories.NaturalTransformation

import Categories.Object.Terminal as ⊤
import Categories.Object.Product as P
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR

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

-- The identity functor is monoidal

module _ (C : MonoidalCategory o ℓ e) where
  private
    module C = MonoidalCategory C
    open C.HomReasoning
    open M C.U
    open MR C.U

  idF-IsStrongMonoidal : IsStrongMonoidalFunctor C C idF
  idF-IsStrongMonoidal = record
    { ε             = ≅.refl
    ; ⊗-homo        = record
      { F⇒G = record
        { η           = λ _ → C.id
        ; commute     = λ _ → id-comm-sym
        ; sym-commute = λ _ → id-comm
        }
      ; F⇐G = record
        { η           = λ _ → C.id
        ; commute     = λ _ → id-comm-sym
        ; sym-commute = λ _ → id-comm
        }
      ; iso = λ _ → record
        { isoˡ = C.identity²
        ; isoʳ = C.identity²
        }
      }
    ; associativity = begin
      C.associator.from C.∘ C.id C.∘ Functor.F₁ C.⊗ (C.id , C.id) ≈⟨ refl⟩∘⟨ elimʳ C.⊗.identity ⟩
      C.associator.from C.∘ C.id                                  ≈⟨ id-comm ⟩
      C.id C.∘ C.associator.from                                  ≈⟨ refl⟩∘⟨ introˡ C.⊗.identity ⟩
      C.id C.∘ Functor.F₁ C.⊗ (C.id , C.id) C.∘ C.associator.from ∎
    ; unitaryˡ      = elimʳ (elimʳ C.⊗.identity)
    ; unitaryʳ      = elimʳ (elimʳ C.⊗.identity)
    }

  idF-IsMonoidal : IsMonoidalFunctor C C idF
  idF-IsMonoidal = IsStrongMonoidalFunctor.isMonoidal idF-IsStrongMonoidal

  idF-StrongMonoidal : StrongMonoidalFunctor C C
  idF-StrongMonoidal = record { isStrongMonoidal = idF-IsStrongMonoidal }

  idF-Monoidal : MonoidalFunctor C C
  idF-Monoidal = record { isMonoidal = idF-IsMonoidal }

-- The identity functor is braided monoidal

module _ (C : BraidedMonoidalCategory o ℓ e) where
  open Braided

  idF-IsStrongBraidedMonoidal : Strong.IsBraidedMonoidalFunctor C C idF
  idF-IsStrongBraidedMonoidal = record
    { isStrongMonoidal = idF-IsStrongMonoidal monoidalCategory
    ; braiding-compat  = MR.id-comm U
    }
    where open BraidedMonoidalCategory C

  idF-IsBraidedMonoidal : Lax.IsBraidedMonoidalFunctor C C idF
  idF-IsBraidedMonoidal =
    Strong.IsBraidedMonoidalFunctor.isLaxBraidedMonoidal idF-IsStrongBraidedMonoidal

  idF-StrongBraidedMonoidal : Strong.BraidedMonoidalFunctor C C
  idF-StrongBraidedMonoidal = record { isBraidedMonoidal = idF-IsStrongBraidedMonoidal }

  idF-BraidedMonoidal : Lax.BraidedMonoidalFunctor C C
  idF-BraidedMonoidal = record { isBraidedMonoidal = idF-IsBraidedMonoidal }

-- The identity functor is symmetric monoidal

module _ (C : SymmetricMonoidalCategory o ℓ e) where
  open Symmetric
  open SymmetricMonoidalCategory C using (braidedMonoidalCategory)

  idF-StrongSymmetricMonoidal : Strong.SymmetricMonoidalFunctor C C
  idF-StrongSymmetricMonoidal = record
    { isBraidedMonoidal = idF-IsStrongBraidedMonoidal braidedMonoidalCategory }

  idF-SymmetricMonoidal : Lax.SymmetricMonoidalFunctor C C
  idF-SymmetricMonoidal = record
    { isBraidedMonoidal = idF-IsBraidedMonoidal braidedMonoidalCategory }

-- Functor composition preserves monoidality

module _ (A : MonoidalCategory o ℓ e) (B : MonoidalCategory o′ ℓ′ e′) (C : MonoidalCategory o″ ℓ″ e″) where
  private
    module A = MonoidalCategory A
    module B = MonoidalCategory B
    module C = MonoidalCategory C
    open P C.U
    open M C.U
    open C.HomReasoning
    open MR C.U

  ∘-IsMonoidal : ∀ {F : Functor A.U B.U} {G : Functor B.U C.U} →
                    IsMonoidalFunctor B C G → IsMonoidalFunctor A B F →
                    IsMonoidalFunctor A C (G ∘F F)
  ∘-IsMonoidal {F} {G} CG CF = record
    { ε             = G.₁ CF.ε C.∘ CG.ε
    ; ⊗-homo        = ntHelper record
      { η       = λ { (X , Y) → G.₁ (CF.⊗-homo.η (X , Y)) C.∘ CG.⊗-homo.η (F.F₀ X , F.F₀ Y) }
      ; commute = λ { (f , g) → begin
        (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ (G.₁ (F.₁ f) C.⊗₁ G.₁ (F.₁ g)) ≈⟨ C.assoc ⟩
        G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _ C.∘ (G.₁ (F.₁ f) C.⊗₁ G.₁ (F.₁ g))   ≈⟨ pushʳ (CG.⊗-homo.commute _) ⟩
        (G.₁ (CF.⊗-homo.η _) C.∘ G.₁ (F.₁ f B.⊗₁ F.₁ g)) C.∘ CG.⊗-homo.η _         ≈⟨ pushˡ ([ G ]-resp-square (CF.⊗-homo.commute _)) ⟩
        G.₁ (F.₁ (f A.⊗₁ g)) C.∘ G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _             ∎ }
      }
    ; associativity = begin
      G.₁ (F.₁ A.associator.from) C.∘ (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ ((G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.⊗₁ C.id)
        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (Functor.homomorphism (C.-⊗ _) ○ C.∘-resp-≈ˡ (C.⊗.F-resp-≈ (C.Equiv.refl , ⟺ G.identity))) ⟩
      G.₁ (F.₁ A.associator.from) C.∘ (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ (G.₁ (CF.⊗-homo.η _) C.⊗₁ G.₁ B.id) C.∘ (CG.⊗-homo.η _ C.⊗₁ C.id)
        ≈⟨ refl⟩∘⟨ center (CG.⊗-homo.commute _) ⟩
      G.₁ (F.₁ A.associator.from) C.∘ G.₁ (CF.⊗-homo.η _) C.∘ (G.₁ (CF.⊗-homo.η _ B.⊗₁ B.id) C.∘ CG.⊗-homo.η _) C.∘ (CG.⊗-homo.η _ C.⊗₁ C.id)
        ≈⟨ C.∘-resp-≈ʳ (center⁻¹ C.Equiv.refl C.Equiv.refl) ○ C.sym-assoc ⟩
      (G.₁ (F.₁ A.associator.from) C.∘ G.₁ (CF.⊗-homo.η _) C.∘ G.₁ (CF.⊗-homo.η _ B.⊗₁ B.id)) C.∘ CG.⊗-homo.η _ C.∘ (CG.⊗-homo.η _ C.⊗₁ C.id)
        ≈⟨ C.∘-resp-≈ʳ (⟺ G.homomorphism) ⟩∘⟨refl ⟩
      (G.₁ (F.₁ A.associator.from) C.∘ G.₁ (CF.⊗-homo.η _ B.∘ CF.⊗-homo.η _ B.⊗₁ B.id)) C.∘ CG.⊗-homo.η _ C.∘ (CG.⊗-homo.η _ C.⊗₁ C.id)
        ≈⟨ [ G ]-resp-square CF.associativity ⟩∘⟨refl ⟩
      (G.₁ (CF.⊗-homo.η _) C.∘ G.₁ ((B.id B.⊗₁ CF.⊗-homo.η _) B.∘ B.associator.from)) C.∘ CG.⊗-homo.η _ C.∘ (CG.⊗-homo.η _ C.⊗₁ C.id)
        ≈⟨ C.∘-resp-≈ʳ G.homomorphism ⟩∘⟨refl ⟩
      (G.₁ (CF.⊗-homo.η _) C.∘ G.₁ (B.id B.⊗₁ CF.⊗-homo.η _) C.∘ G.₁ B.associator.from) C.∘ CG.⊗-homo.η _ C.∘ (CG.⊗-homo.η _ C.⊗₁ C.id)
        ≈⟨ C.∘-resp-≈ˡ C.sym-assoc ○ C.assoc ⟩
      (G.₁ (CF.⊗-homo.η _) C.∘ G.₁ (B.id B.⊗₁ CF.⊗-homo.η _)) C.∘ G.₁ B.associator.from C.∘ CG.⊗-homo.η _ C.∘ (CG.⊗-homo.η _ C.⊗₁ C.id)
        ≈⟨ refl⟩∘⟨ CG.associativity ⟩
      (G.₁ (CF.⊗-homo.η _) C.∘ G.₁ (B.id B.⊗₁ CF.⊗-homo.η _)) C.∘ CG.⊗-homo.η _ C.∘ (C.id C.⊗₁ CG.⊗-homo.η _) C.∘ C.associator.from
        ≈⟨ center (CG.⊗-homo.sym-commute _) ⟩
      G.₁ (CF.⊗-homo.η _) C.∘ (CG.⊗-homo.η _ C.∘ (G.₁ B.id C.⊗₁ G.₁ (CF.⊗-homo.η _))) C.∘ (C.id C.⊗₁ CG.⊗-homo.η _) C.∘ C.associator.from
        ≈⟨ pull-first C.Equiv.refl ○ C.∘-resp-≈ʳ (C.∘-resp-≈ˡ (C.⊗.F-resp-≈ (G.identity , C.Equiv.refl))) ⟩
      (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ (C.id C.⊗₁ G.₁ (CF.⊗-homo.η _)) C.∘ (C.id C.⊗₁ CG.⊗-homo.η _) C.∘ C.associator.from
        ≈˘⟨ refl⟩∘⟨ pushˡ (Functor.homomorphism (_ C.⊗-)) ⟩
      (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ (C.id C.⊗₁ (G.F₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _)) C.∘ C.associator.from
        ∎
    ; unitaryˡ      = begin
      G.₁ (F.₁ A.unitorˡ.from) C.∘ (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ ((G.₁ CF.ε C.∘ CG.ε) C.⊗₁ C.id)
        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (Functor.homomorphism (C.-⊗ _) ○ C.∘-resp-≈ˡ (C.⊗.F-resp-≈ (C.Equiv.refl , ⟺ G.identity))) ⟩
      G.₁ (F.₁ A.unitorˡ.from) C.∘ (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ (G.₁ CF.ε C.⊗₁ G.₁ B.id) C.∘ (CG.ε C.⊗₁ C.id)
        ≈⟨ refl⟩∘⟨ center (CG.⊗-homo.commute _) ⟩
      G.₁ (F.₁ A.unitorˡ.from) C.∘ G.₁ (CF.⊗-homo.η _) C.∘ (G.₁ (CF.ε B.⊗₁ B.id) C.∘ CG.⊗-homo.η _) C.∘ (CG.ε C.⊗₁ C.id)
        ≈⟨ C.∘-resp-≈ʳ (center⁻¹ C.Equiv.refl C.Equiv.refl) ○ C.sym-assoc ⟩
      (G.₁ (F.₁ A.unitorˡ.from) C.∘ G.₁ (CF.⊗-homo.η _) C.∘ G.₁ (CF.ε B.⊗₁ B.id)) C.∘ CG.⊗-homo.η _ C.∘ (CG.ε C.⊗₁ C.id)
        ≈⟨ C.∘-resp-≈ʳ (⟺ G.homomorphism) ⟩∘⟨refl ⟩
      (G.₁ (F.₁ A.unitorˡ.from) C.∘ G.₁ (CF.⊗-homo.η _ B.∘ CF.ε B.⊗₁ B.id)) C.∘ CG.⊗-homo.η _ C.∘ (CG.ε C.⊗₁ C.id)
        ≈⟨ [ G ]-resp-∘ CF.unitaryˡ ⟩∘⟨refl ⟩
      G.₁ B.unitorˡ.from C.∘ CG.⊗-homo.η _ C.∘ (CG.ε C.⊗₁ C.id)
        ≈⟨ CG.unitaryˡ ⟩
      C.unitorˡ.from
        ∎
    ; unitaryʳ      = begin
      G.₁ (F.₁ A.unitorʳ.from) C.∘ (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ (C.id C.⊗₁ (G.₁ CF.ε C.∘ CG.ε))
        ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ (Functor.homomorphism (_ C.⊗-) ○ C.∘-resp-≈ˡ (C.⊗.F-resp-≈ (⟺ G.identity , C.Equiv.refl)))) ⟩
      G.₁ (F.₁ A.unitorʳ.from) C.∘ (G.₁ (CF.⊗-homo.η _) C.∘ CG.⊗-homo.η _) C.∘ (G.₁ B.id C.⊗₁ G.₁ CF.ε) C.∘ (C.id C.⊗₁ CG.ε)
        ≈⟨ refl⟩∘⟨ center (CG.⊗-homo.commute _) ⟩
      G.₁ (F.₁ A.unitorʳ.from) C.∘ G.₁ (CF.⊗-homo.η _) C.∘ (G.₁ (B.id B.⊗₁ CF.ε) C.∘ CG.⊗-homo.η _) C.∘ (C.id C.⊗₁ CG.ε)
        ≈⟨ C.∘-resp-≈ʳ (center⁻¹ C.Equiv.refl C.Equiv.refl) ○ C.sym-assoc ⟩
      (G.₁ (F.₁ A.unitorʳ.from) C.∘ G.₁ (CF.⊗-homo.η _) C.∘ G.₁ (B.id B.⊗₁ CF.ε)) C.∘ CG.⊗-homo.η _ C.∘ (C.id C.⊗₁ CG.ε)
        ≈⟨ C.∘-resp-≈ʳ (⟺ G.homomorphism) ⟩∘⟨refl ⟩
      (G.₁ (F.₁ A.unitorʳ.from) C.∘ G.F₁ (CF.⊗-homo.η _ B.∘ (B.id B.⊗₁ CF.ε))) C.∘ CG.⊗-homo.η _ C.∘ (C.id C.⊗₁ CG.ε)
        ≈⟨ [ G ]-resp-∘ CF.unitaryʳ ⟩∘⟨refl ⟩
      G.F₁ B.unitorʳ.from C.∘ CG.⊗-homo.η _ C.∘ C.id C.⊗₁ CG.ε
        ≈⟨ CG.unitaryʳ ⟩
      C.unitorʳ.from
        ∎
    }
    where module F  = Functor F
          module G  = Functor G
          module CF = IsMonoidalFunctor CF
          module CG = IsMonoidalFunctor CG

  ∘-IsStrongMonoidal : ∀ {F : Functor A.U B.U} {G : Functor B.U C.U} →
                    IsStrongMonoidalFunctor B C G → IsStrongMonoidalFunctor A B F →
                    IsStrongMonoidalFunctor A C (G ∘F F)
  ∘-IsStrongMonoidal {F} {G} CG CF = record
    { ε             = ≅.trans CG.ε ([ G ]-resp-≅ CF.ε)
    ; ⊗-homo        = record
      { F⇒G = ∘.⊗-homo
      ; F⇐G = ntHelper record
        { η       = λ { (X , Y) → CG.⊗-homo.⇐.η (F.F₀ X , F.F₀ Y) C.∘ G.₁ (CF.⊗-homo.⇐.η (X , Y)) }
        ; commute = λ _ → pullʳ ([ G ]-resp-square (CF.⊗-homo.⇐.commute _)) ○ pullˡ (CG.⊗-homo.⇐.commute _) ○ C.assoc
        }
      ; iso = λ _ → record
        { isoˡ = cancelInner ([ G ]-resp-∘ (CF.⊗-homo.iso.isoˡ _) ○ G.identity) ○ CG.⊗-homo.iso.isoˡ _
        ; isoʳ = cancelInner (CG.⊗-homo.iso.isoʳ _) ○ [ G ]-resp-∘ (CF.⊗-homo.iso.isoʳ _) ○ G.identity
        }
      }
    ; associativity = ∘.associativity
    ; unitaryˡ      = ∘.unitaryˡ
    ; unitaryʳ      = ∘.unitaryʳ
    }
    where module F  = Functor F
          module G  = Functor G
          module CF = IsStrongMonoidalFunctor CF
          module CG = IsStrongMonoidalFunctor CG
          module ∘  = IsMonoidalFunctor (∘-IsMonoidal CG.isMonoidal CF.isMonoidal)

module _ {A : MonoidalCategory o ℓ e} {B : MonoidalCategory o′ ℓ′ e′} {C : MonoidalCategory o″ ℓ″ e″} where

    ∘-StrongMonoidal : StrongMonoidalFunctor B C → StrongMonoidalFunctor A B → StrongMonoidalFunctor A C
    ∘-StrongMonoidal G F = record { isStrongMonoidal = ∘-IsStrongMonoidal _ _ _ (StrongMonoidalFunctor.isStrongMonoidal G) (StrongMonoidalFunctor.isStrongMonoidal F) }

    ∘-Monoidal : MonoidalFunctor B C → MonoidalFunctor A B → MonoidalFunctor A C
    ∘-Monoidal G F = record { isMonoidal = ∘-IsMonoidal _ _ _ (MonoidalFunctor.isMonoidal G) (MonoidalFunctor.isMonoidal F) }

-- Functor composition preserves braided monoidality

module _ {A : BraidedMonoidalCategory o ℓ e}
         {B : BraidedMonoidalCategory o′ ℓ′ e′}
         {C : BraidedMonoidalCategory o″ ℓ″ e″} where

  private
    module A = BraidedMonoidalCategory A
    module B = BraidedMonoidalCategory B
    module C = BraidedMonoidalCategory C
  open Braided

  ∘-IsBraidedMonoidal : ∀ {G : Functor B.U C.U} {F : Functor A.U B.U} →
                        Lax.IsBraidedMonoidalFunctor B C G →
                        Lax.IsBraidedMonoidalFunctor A B F →
                        Lax.IsBraidedMonoidalFunctor A C (G ∘F F)
  ∘-IsBraidedMonoidal {G} {F} GB FB = record
    { isMonoidal      = ∘-IsMonoidal _ _ _ (isMonoidal GB) (isMonoidal FB)
    ; braiding-compat = begin
        G₁ (F₁ AB) ∘ G₁ FH ∘ GH   ≈˘⟨ pushˡ (homomorphism G) ⟩
        G₁ (F₁ AB B.∘ FH) ∘ GH    ≈⟨ F-resp-≈ G (braiding-compat FB) ⟩∘⟨refl ⟩
        G₁ (FH B.∘ BB) ∘ GH       ≈⟨ pushˡ (homomorphism G) ⟩
        G₁ FH ∘ G₁ BB ∘ GH        ≈⟨ pushʳ (braiding-compat GB) ⟩
        (G₁ FH ∘ GH) ∘ CB         ∎
    }
    where
      open C
      open HomReasoning
      open MR C.U
      open Functor hiding (F₁)
      open Functor F using (F₁)
      open Functor G using () renaming (F₁ to G₁)
      open Lax.IsBraidedMonoidalFunctor

      FH  = λ {X Y} → ⊗-homo.η FB (X , Y)
      GH  = λ {X Y} → ⊗-homo.η GB (X , Y)
      AB = λ {X Y} → A.braiding.⇒.η (X , Y)
      BB = λ {X Y} → B.braiding.⇒.η (X , Y)
      CB = λ {X Y} → C.braiding.⇒.η (X , Y)

  ∘-IsStrongBraidedMonoidal : ∀ {G : Functor B.U C.U} {F : Functor A.U B.U} →
                              Strong.IsBraidedMonoidalFunctor B C G →
                              Strong.IsBraidedMonoidalFunctor A B F →
                              Strong.IsBraidedMonoidalFunctor A C (G ∘F F)
  ∘-IsStrongBraidedMonoidal {G} {F} GB FB = record
    { isStrongMonoidal =
      ∘-IsStrongMonoidal _ _ _ (isStrongMonoidal GB) (isStrongMonoidal FB)
    ; braiding-compat =
      Lax.IsBraidedMonoidalFunctor.braiding-compat
        (∘-IsBraidedMonoidal (isLaxBraidedMonoidal GB) (isLaxBraidedMonoidal FB))
    }
    where open Strong.IsBraidedMonoidalFunctor

  ∘-BraidedMonoidal : Lax.BraidedMonoidalFunctor B C →
                      Lax.BraidedMonoidalFunctor A B →
                      Lax.BraidedMonoidalFunctor A C
  ∘-BraidedMonoidal G F = record
    { isBraidedMonoidal =
      ∘-IsBraidedMonoidal (isBraidedMonoidal G) (isBraidedMonoidal F)
    }
    where open Lax.BraidedMonoidalFunctor hiding (F)

  ∘-StrongBraidedMonoidal : Strong.BraidedMonoidalFunctor B C →
                            Strong.BraidedMonoidalFunctor A B →
                            Strong.BraidedMonoidalFunctor A C
  ∘-StrongBraidedMonoidal G F = record
    { isBraidedMonoidal =
      ∘-IsStrongBraidedMonoidal (isBraidedMonoidal G) (isBraidedMonoidal F)
    }
    where open Strong.BraidedMonoidalFunctor hiding (F)

-- Functor composition preserves symmetric monoidality

module _ {A : SymmetricMonoidalCategory o ℓ e}
         {B : SymmetricMonoidalCategory o′ ℓ′ e′}
         {C : SymmetricMonoidalCategory o″ ℓ″ e″} where
  open Symmetric

  ∘-SymmetricMonoidal : Lax.SymmetricMonoidalFunctor B C →
                        Lax.SymmetricMonoidalFunctor A B →
                        Lax.SymmetricMonoidalFunctor A C
  ∘-SymmetricMonoidal G F = record
    { isBraidedMonoidal =
      ∘-IsBraidedMonoidal (isBraidedMonoidal G) (isBraidedMonoidal F)
    }
    where open Lax.SymmetricMonoidalFunctor hiding (F)

  ∘-StrongSymmetricMonoidal : Strong.SymmetricMonoidalFunctor B C →
                              Strong.SymmetricMonoidalFunctor A B →
                              Strong.SymmetricMonoidalFunctor A C
  ∘-StrongSymmetricMonoidal G F = record
    { isBraidedMonoidal =
      ∘-IsStrongBraidedMonoidal (isBraidedMonoidal G) (isBraidedMonoidal F)
    }
    where open Strong.SymmetricMonoidalFunctor hiding (F)

module _ (C : CartesianCategory o ℓ e) (D : CartesianCategory o′ ℓ′ e′) where
  private
    module C = CartesianCategory C
    module D = CartesianCategory D
    open D.HomReasoning
    open MR D.U

  module _ (F : StrongMonoidalFunctor C.monoidalCategory D.monoidalCategory) where
    private
      module F = StrongMonoidalFunctor F

      F-resp-⊤ : ⊤.IsTerminal D.U (F.F₀ C.⊤)
      F-resp-⊤ = ⊤.Terminal.⊤-is-terminal (⊤.transport-by-iso D.U D.terminal F.ε)
      module F-resp-⊤ = ⊤.IsTerminal F-resp-⊤

      lemma₁ : ∀ {X} → F.ε.from D.∘ D.! {F.₀ X} D.≈ F.₁ (C.! {X})
      lemma₁ = F-resp-⊤.!-unique _

      π₁-comm : ∀ {X Y} → F.F₁ C.π₁ D.∘ F.⊗-homo.⇒.η (X , Y) D.≈ D.π₁
      π₁-comm {X} {Y} = begin
        F.F₁ C.π₁ D.∘ F.⊗-homo.⇒.η (X , Y)                                                ≈˘⟨ [ F.F ]-resp-∘ (C.Equiv.trans C.project₁ C.identityˡ) ⟩∘⟨refl ⟩
        (F.F₁ C.π₁ D.∘ F.F₁ (C.id C.⁂ C.!)) D.∘ F.⊗-homo.⇒.η (X , Y)                      ≈⟨ pullʳ (F.⊗-homo.⇒.sym-commute _) ⟩
        F.F₁ C.π₁ D.∘ F.⊗-homo.⇒.η (X , C.⊤) D.∘ (F.F₁ C.id D.⁂ F.F₁ C.!)                 ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ([ F.₀ X D.×- ]-resp-∘ lemma₁ ○ Functor.F-resp-≈ D.-×- (⟺ F.identity , D.Equiv.refl)) ⟩
        F.F₁ C.π₁ D.∘ F.⊗-homo.⇒.η (X , C.⊤) D.∘ (D.id D.⁂ F.ε.from) D.∘ (D.id D.⁂ D.!)   ≈⟨ D.∘-resp-≈ʳ D.sym-assoc ○ D.sym-assoc ⟩
        (F.F₁ C.π₁ D.∘ F.⊗-homo.⇒.η (X , C.⊤) D.∘ (D.id D.⁂ F.ε.from)) D.∘ (D.id D.⁂ D.!) ≈⟨ F.unitaryʳ ⟩∘⟨refl ⟩
        D.π₁ D.∘ (D.id D.⁂ D.!)                                                           ≈⟨ D.project₁ ○ D.identityˡ ⟩
        D.π₁                                                                              ∎

      π₂-comm : ∀ {X Y} → F.F₁ C.π₂ D.∘ F.⊗-homo.⇒.η (X , Y) D.≈ D.π₂
      π₂-comm {X} {Y} = begin
        F.F₁ C.π₂ D.∘ F.⊗-homo.⇒.η (X , Y)                                                ≈˘⟨ [ F.F ]-resp-∘ (C.Equiv.trans C.project₂ C.identityˡ) ⟩∘⟨refl ⟩
        (F.F₁ C.π₂ D.∘ F.F₁ (C.! C.⁂ C.id)) D.∘ F.⊗-homo.⇒.η (X , Y)                      ≈⟨ pullʳ (F.⊗-homo.⇒.sym-commute _) ⟩
        F.F₁ C.π₂ D.∘ F.⊗-homo.⇒.η (C.⊤ , Y) D.∘ (F.F₁ C.! D.⁂ F.F₁ C.id)                 ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ([ D.-× F.₀ Y ]-resp-∘ lemma₁ ○ Functor.F-resp-≈ D.-×- (D.Equiv.refl , ⟺ F.identity)) ⟩
        F.F₁ C.π₂ D.∘ F.⊗-homo.⇒.η (C.⊤ , Y) D.∘ (F.ε.from D.⁂ D.id) D.∘ (D.! D.⁂ D.id)   ≈⟨ D.∘-resp-≈ʳ D.sym-assoc ○ D.sym-assoc ⟩
        (F.F₁ C.π₂ D.∘ F.⊗-homo.⇒.η (C.⊤ , Y) D.∘ (F.ε.from D.⁂ D.id)) D.∘ (D.! D.⁂ D.id) ≈⟨ F.unitaryˡ ⟩∘⟨refl ⟩
        D.π₂ D.∘ (D.! D.⁂ D.id)                                                           ≈⟨ D.project₂ ○ D.identityˡ ⟩
        D.π₂                                                                              ∎

      unique : ∀ {X A B} {h : X D.⇒ F.₀ (A C.× B)} {i : X D.⇒ F.₀ A} {j : X D.⇒ F.₀ B} →
                 F.₁ C.π₁ D.∘ h D.≈ i →
                 F.₁ C.π₂ D.∘ h D.≈ j →
                 F.⊗-homo.⇒.η (A , B) D.∘ D.product.⟨ i , j ⟩ D.≈ h
      unique  eq₁ eq₂ = ⟺ (switch-tofromˡ F.⊗-homo.FX≅GX (⟺ (D.unique (pullˡ (⟺ (switch-fromtoʳ F.⊗-homo.FX≅GX π₁-comm)) ○ eq₁)
                                                                      (pullˡ (⟺ (switch-fromtoʳ F.⊗-homo.FX≅GX π₂-comm)) ○ eq₂))))

    StrongMonoidal⇒Cartesian : CartesianF C D
    StrongMonoidal⇒Cartesian = record
      { F           = F.F
      ; isCartesian = record
        { F-resp-⊤ = F-resp-⊤
        ; F-resp-× = λ {A B} → record
          { ⟨_,_⟩    = λ f g → F.⊗-homo.⇒.η _ D.∘ D.⟨ f , g ⟩
          ; project₁ = λ {_ h i} → begin
            F.₁ C.π₁ D.∘ F.⊗-homo.⇒.η _ D.∘ D.⟨ h , i ⟩ ≈⟨ pullˡ π₁-comm ⟩
            D.π₁ D.∘ D.product.⟨ h , i ⟩                ≈⟨ D.project₁ ⟩
            h                                           ∎
          ; project₂ = λ {_ h i} → begin
            F.₁ C.π₂ D.∘ F.⊗-homo.⇒.η _ D.∘ D.⟨ h , i ⟩ ≈⟨ pullˡ π₂-comm ⟩
            D.π₂ D.∘ D.⟨ h , i ⟩                        ≈⟨ D.project₂ ⟩
            i                                           ∎
          ; unique   = unique
          }
        }
      }

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: TOTBWF/agda-categories

max_forks_repo_name: TOTBWF/agda-categories


text:
------------------------------------------------------------------------------
-- Mirror example
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Example where

open import FOTC.Base
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Program.Mirror.Mirror
open import FOTC.Program.Mirror.Type
open import FOTC.Program.Mirror.PropertiesI

------------------------------------------------------------------------------
-- Example
--       1
--    / / \ \
--   2 3   4 5
--  / \
-- 6   7

t : D
t = node 1' (node 2' (node 6' [] ∷ node 7' [] ∷ []) ∷
             node 3' [] ∷
             node 4' [] ∷
             node 5' [] ∷
             []
            )

tTree : Tree t
tTree = tree 1' (fcons (tree 2' (fcons (tree 6' fnil)
                                (fcons (tree 7' fnil)
                                fnil)))
                (fcons (tree 3' fnil)
                (fcons (tree 4' fnil)
                (fcons (tree 5' fnil)
                fnil))))

test : t ≡ mirror · (mirror · t)
test = sym (mirror-involutive tTree)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Generics.Telescope.Equality where

-- freely inspired by jespercockx/telescopic
-- note that our telescopes extend to the right
-- while in telescopic they extend to the left
-- a byproduct is that the following defs are overly mutual

open import Generics.Prelude
open import Generics.Telescope

private
  variable
    l     : Level
    A     : Set l
    a x y : A

-----------
-- Helpers

private
  J⁻¹ : ∀ {a b} {A : Set a} {x : A} (B : (y : A) → x ≡ y → Set b)
      → {y : A} (p : x ≡ y) → B y p → B x refl
  J⁻¹ B p = J (λ y e → B y e → B _ refl) p id

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

  Jω⁻¹ : ∀ {a} {A : Set a} {x : A} (B : (y : A) → x ≡ y → Setω)
      → {y : A} (p : x ≡ y) → B y p → B x refl
  Jω⁻¹ B p = Jω (λ y e → B y e → B _ refl) p λ x → x

  JJ⁻¹ : ∀ {a b} {A : Set a} {x : A} (B : (y : A) → x ≡ y → Set b)
      → {y : A} {p : x ≡ y}
      → (z : B y p)
      → J B p (J⁻¹ B p z) ≡ z
  JJ⁻¹ B {p = refl} z = refl

  JJω⁻¹ : ∀ {a} {A : Set a} {x : A} (B : (y : A) → x ≡ y → Setω)
      → {y : A} {p : x ≡ y}
      → (z : B y p)
      → Jω B p (Jω⁻¹ B p z) ≡ω z
  JJω⁻¹ B {p = refl} z = refl

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

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

----------------------
-- Telescope Equality

_≡ⁿ_ : {T : Telescope A} → ⟦ T ⟧tel a → ⟦ T ⟧tel a → Telescope ⊤

substⁿ : {T : Telescope A} (f : ∀ {x} → ⟦ T ⟧tel x → Set l)
         {xs ys : ⟦ T ⟧tel a}
       → ⟦ xs ≡ⁿ ys ⟧tel tt
       → f xs → f ys

reflⁿ : {T : Telescope A} {xs : ⟦ T ⟧tel a}
      → ⟦ xs ≡ⁿ xs ⟧tel tt

substⁿ-refl : {T : Telescope A} (f : ∀ {x} → ⟦ T ⟧tel x → Set l)
              {xs : ⟦ T ⟧tel a} {x : f xs}
            → substⁿ f reflⁿ x ≡ x

Jⁿ : {T : Telescope A} {xs : ⟦ T ⟧tel a}
     (ϕ : ∀ ss → ⟦ xs ≡ⁿ ss ⟧tel tt → Set l)
   → ∀ {ss} (es : ⟦ xs ≡ⁿ ss ⟧tel tt)
   → ϕ xs reflⁿ
   → ϕ ss es

Jⁿ-refl : {T : Telescope A} {xs : ⟦ T ⟧tel a}
          (ϕ : ∀ ss → ⟦ xs ≡ⁿ ss ⟧tel tt → Set l)
          (φ : ϕ xs reflⁿ)
        → Jⁿ ϕ reflⁿ φ ≡ φ

-- TODO: discard equality between irrelevant values
_≡ⁿ_ {T = ε} tt tt = ε
_≡ⁿ_ {T = T ⊢< n , ai > f} (xs , x) (ys , y) =
  e ∶ xs ≡ⁿ ys , substⁿ (< relevance ai >_ ∘ f ∘ (_ ,_)) e x ≡ y

reflⁿ {T = ε} = tt
reflⁿ {T = T ⊢< n , ai > f} {xs , x} =
  reflⁿ , substⁿ-refl (< relevance ai >_ ∘ f ∘ (_ ,_))

Jⁿ {T = ε} ϕ _ φ = φ
Jⁿ {T = T ⊢< n , ai > f} {xs , x} ϕ {ss , s} (es , e) φ =
  J (λ y ey → ϕ (ss , y) (es , ey)) e $
     Jⁿ (λ ss′ es′ → ϕ (ss′ , substⁿ (< relevance ai >_ ∘ f ∘ (_ ,_)) es′ x)
                       (es′ , refl)) es d
  where
    d : ϕ (xs , substⁿ (< relevance ai >_ ∘ f ∘ (_ ,_)) reflⁿ x)
          (reflⁿ , refl)
    d = J⁻¹ (λ y ey → ϕ (xs , y) (reflⁿ , ey)) (substⁿ-refl _) φ

substⁿ {T = ε} f tt z = z
substⁿ {T = T ⊢< n , ai > g} f {xs , x} {ys , y} (es , e) z =
  subst (f ∘ (ys ,_)) e $
   Jⁿ (λ rs er → f (rs , substⁿ (< relevance ai >_ ∘ g ∘ (_ ,_)) er x))
      es
      (subst (f ∘ (xs ,_)) (sym (substⁿ-refl (< relevance ai >_ ∘ g ∘ (_ ,_)))) z)

substⁿ-refl {T = ε} f = refl
substⁿ-refl {T = T ⊢< n , ai > g} f {xs , x} {z}
  rewrite Jⁿ-refl (λ rs er → f (rs , substⁿ (< relevance ai >_ ∘ g ∘ (_ ,_)) er x))
                  (subst (f ∘ (xs ,_)) (sym (substⁿ-refl (< relevance ai >_ ∘ g ∘ (_ ,_)))) z)
        = subst-subst-sym (substⁿ-refl (< relevance ai >_ ∘ g ∘ (_ ,_)))

Jⁿ-refl {T = ε} ϕ φ = refl
Jⁿ-refl {T = T ⊢< n , ai > f} {xs , x} ϕ φ
  rewrite Jⁿ-refl (λ ss′ es′ → ϕ (ss′ , substⁿ (< relevance ai >_ ∘ f ∘ (_ ,_)) es′ x) (es′ , refl))
                  (J⁻¹ (λ y ey → ϕ (xs , y) (reflⁿ , ey)) _ φ)
        = JJ⁻¹ (λ y ey → ϕ (xs , y) (reflⁿ , ey)) φ

------------------------------
-- Telescope Equality in Setω

substωⁿ : {T : Telescope A} (f : ∀ {x} → ⟦ T ⟧tel x → Setω)
          {xs ys : ⟦ T ⟧tel a}
        → ⟦ xs ≡ⁿ ys ⟧tel tt
        → f xs → f ys

substωⁿ-refl : {T : Telescope A} (f : ∀ {x} → ⟦ T ⟧tel x → Setω)
               {xs : ⟦ T ⟧tel a} {x : f xs}
             → substωⁿ f reflⁿ x ≡ω x

Jωⁿ : {T : Telescope A} {xs : ⟦ T ⟧tel a}
      (ϕ : ∀ ss → ⟦ xs ≡ⁿ ss ⟧tel tt → Setω)
    → ∀ {ss} (es : ⟦ xs ≡ⁿ ss ⟧tel tt)
    → ϕ xs reflⁿ
    → ϕ ss es

Jωⁿ-refl : {T : Telescope A} {xs : ⟦ T ⟧tel a}
           (ϕ : ∀ ss → ⟦ xs ≡ⁿ ss ⟧tel tt → Setω)
           (φ : ϕ xs reflⁿ)
         → Jωⁿ ϕ reflⁿ φ ≡ω φ

Jωⁿ {T = ε} ϕ _ φ = φ
Jωⁿ {T = T ⊢< n , ai > f} {xs , x} ϕ {ss , s} (es , e) φ =
  Jω (λ y ey → ϕ (ss , y) (es , ey)) e
     (Jωⁿ (λ ss′ es′ → ϕ (ss′ , substⁿ (< relevance ai >_ ∘ f ∘ (_ ,_)) es′ x)
                        (es′ , refl)) es d)
  where
    d : ϕ (xs , substⁿ (< relevance ai >_ ∘ f ∘ (_ ,_)) reflⁿ x)
          (reflⁿ , refl)
    d = Jω⁻¹ (λ y ey → ϕ (xs , y) (reflⁿ , ey)) (substⁿ-refl (< relevance ai >_ ∘ f ∘ (_ ,_))) φ

substωⁿ {T = ε} f tt z = z
substωⁿ {T = T ⊢< n , ai > g} f {xs , x} {ys , y} (es , e) z =
  substω (λ x → f (ys , x)) e
   (Jωⁿ (λ rs er → f (rs , substⁿ (< relevance ai >_ ∘ g ∘ (_ ,_)) er x))
       es
       (substω (λ x → f (xs , x)) (sym (substⁿ-refl (< relevance ai >_ ∘ g ∘ (_ ,_)))) z))

substωⁿ-refl {T = ε} f = refl
substωⁿ-refl {T = T ⊢< n , ai > g} f {xs , x} {z} =
  transω (cong≡ωω (λ x → substω (λ x → f (_ , x)) ((substⁿ-refl (< relevance ai >_ ∘ g ∘ (_ ,_)))) x)
                  p)
         (substω-substω-sym (substⁿ-refl (< relevance ai >_ ∘ g ∘ (_ ,_))))
  where
    p = Jωⁿ-refl (λ rs er → f (rs , substⁿ (< relevance ai >_ ∘ g ∘ (_ ,_)) er x))
                 (substω (λ x → f (xs , x)) (sym (substⁿ-refl (< relevance ai >_ ∘ g ∘ (_ ,_)))) z)

Jωⁿ-refl {T = ε} ϕ φ = refl
Jωⁿ-refl {T = T ⊢< n , ai > f} {xs , x} ϕ φ =
  transω (cong≡ωω (λ x → Jω (λ y ey → ϕ (xs , y) (reflⁿ , ey))
                       (substⁿ-refl (< relevance ai >_ ∘ f ∘ (_ ,_))) x) p)
         (JJω⁻¹ (λ y ey → ϕ (xs , y) (reflⁿ , ey)) φ)
  where
    p = Jωⁿ-refl (λ ss′ es′ → ϕ (ss′ , substⁿ (< relevance ai >_ ∘ f ∘ (_ ,_)) es′ x) (es′ , refl))
                 (Jω⁻¹ (λ y ey → ϕ (xs , y) (reflⁿ , ey)) _ φ)

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
module ShouldBePi where

postulate X : Set


text:
{-# OPTIONS --no-flat-split #-}
module _ where

postulate
  A : Set

data Id (A : Set) : Set where
  id : A → Id A

-- --no-flat-split disables matching on the @♭ x agument.
test2 : (@♭ x : Id A) → A
test2 (id x) = x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of Stream
------------------------------------------------------------------------

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

module Codata.Stream.Categorical where

open import Data.Product using (<_,_>)
open import Codata.Stream
open import Function
open import Category.Functor
open import Category.Applicative
open import Category.Comonad

functor : ∀ {ℓ i} → RawFunctor {ℓ} (λ A → Stream A i)
functor = record { _<$>_ = λ f → map f }

applicative : ∀ {ℓ i} → RawApplicative {ℓ} (λ A → Stream A i)
applicative = record
  { pure = repeat
  ; _⊛_  = ap
  }

comonad : ∀ {ℓ} → RawComonad {ℓ} (λ A → Stream A _)
comonad = record
  { extract = head
  ; extend  = unfold ∘′ < tail ,_>
  }


text:
module Issue470 where

data Bool : Set where
  true false : Bool

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

infixr 5 _∷_

data Foo : Bool → Set where
  []  : Foo true
  _∷_ : ∀ {b} (x : Bool) → Foo b → Foo (x and b)

Baz : Bool → Set
Baz true = Bool
Baz false = Foo false

data Bar : ∀ {b} → Foo b → Set where
  []  : Bar []
  _∷_ : ∀ {b} {foo : Foo b} {x} (g : Baz x) → (bar : Bar foo) → Bar (x ∷ foo)

foo : Foo false
foo = false ∷ true ∷ []

bar : Bar foo
bar = (false ∷ []) ∷ false ∷ [] -- ← is yellow

{-
_59 := _55 ∷ false ∷ [] [blocked by problem 75]
[75] ["apply" (_53 ∷ true ∷ [])] == ["apply" (false ∷ true ∷ [])] : Foo
(_53 and (true and true)) → Set [blocked by problem 76]
[76] (_53 and (true and true)) = false : Bool
_54 := false ∷ [] :? Baz _53
-}


text:
module Data.Permutation where

open import Prelude
open import Data.Fin as Fin hiding (_==_; _<_)
open import Data.Nat
open import Data.Vec
open import Logic.Identity
open import Logic.Base
import Logic.ChainReasoning

-- What is a permutation?
-- Answer 1: A bijection between Fin n and itself

data Permutation (n : Nat) : Set where
  permutation :
    (π π⁻¹ : Fin n -> Fin n) ->
    (forall {i} -> π (π⁻¹ i) ≡ i) ->
    Permutation n

module Permutation {n : Nat}(P : Permutation n) where

  private
    π' : Permutation n -> Fin n -> Fin n
    π' (permutation x _ _) = x

    π⁻¹' : Permutation n -> Fin n -> Fin n
    π⁻¹' (permutation _ x _) = x

    proof : (P : Permutation n) -> forall {i} -> π' P (π⁻¹' P i) ≡ i
    proof (permutation _ _ x) = x

  π : Fin n -> Fin n
  π	  = π' P

  π⁻¹ : Fin n -> Fin n
  π⁻¹	  = π⁻¹' P

  module Proofs where

    ππ⁻¹-id : {i : Fin n} -> π (π⁻¹ i) ≡ i
    ππ⁻¹-id = proof P

    open module Chain = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans)

    π⁻¹-inj : (i j : Fin n) -> π⁻¹ i ≡ π⁻¹ j -> i ≡ j
    π⁻¹-inj i j h =
      chain> i
	 === π (π⁻¹ i)	by sym ππ⁻¹-id
	 === π (π⁻¹ j)	by cong π h
	 === j		by ππ⁻¹-id

    -- Generalise
    lem : {n : Nat}(f g : Fin n -> Fin n)
	  -> (forall i -> f (g i) ≡ i)
	  -> (forall i -> g (f i) ≡ i)
    lem {zero}  f g inv ()
    lem {suc n} f g inv i  = ?
      where
	gz≠gs : {i : Fin n} -> g fzero ≢ g (fsuc i)
	gz≠gs {i} gz=gs = fzero≠fsuc $
	  chain> fzero
	     === f (g fzero)	 by sym (inv fzero)
	     === f (g (fsuc i))  by cong f gz=gs
	     === fsuc i		 by inv (fsuc i)

	z≠f-thin-gz : {i : Fin n} -> fzero ≢ f (thin (g fzero) i)
	z≠f-thin-gz {i} z=f-thin-gz = ?
-- 	  f (g fzero)
-- 	  = fzero
-- 	  = f (thin (g fzero) i)

	g' : Fin n -> Fin n
	g' j = thick (g fzero) (g (fsuc j)) gz≠gs

	f' : Fin n -> Fin n
	f' j = thick fzero (f (thin (g fzero) j)) ?

	g'f' : forall j -> g' (f' j) ≡ j
	g'f' = lem {n} f' g' ?

    π⁻¹π-id : forall {i} -> π⁻¹ (π i) ≡ i
    π⁻¹π-id = ?

-- Answer 2: A Vec (Fin n) n with no duplicates

{-
infixr 40 _◅_ _↦_,_
infixr 20 _○_

data Permutation : Nat -> Set where
  ε   : Permutation zero
  _◅_ : {n : Nat} -> Fin (suc n) -> Permutation n -> Permutation (suc n)

_↦_,_ : {n : Nat}(i j : Fin (suc n)) -> Permutation n -> Permutation (suc n)
fzero  ↦ j , π	    = j ◅ π
fsuc i ↦ j , j' ◅ π = thin j j' ◅ i ↦ ? , π

indices : {n : Nat} -> Permutation n -> Vec (Fin n) n
indices  ε	= []
indices (i ◅ π) = i :: map (thin i) (indices π)

-- permute (i ◅ π) xs with xs [!] i where
--   permute₁ (i ◅ π) .(insert i x xs) (ixV x xs) = x :: permute π xs

permute : {n : Nat}{A : Set} -> Permutation n -> Vec A n -> Vec A n
permute (i ◅ π) xs = permute' π i xs (xs [!] i)
  where
    permute' : {n : Nat}{A : Set} -> Permutation n -> (i : Fin (suc n))(xs : Vec A (suc n)) ->
	       IndexView i xs -> Vec A (suc n)
    permute' π i .(insert i x xs') (ixV x xs') = x :: permute π xs'

delete : {n : Nat} -> Fin (suc n) -> Permutation (suc n) -> Permutation n
delete		fzero    (j ◅ π) = π
delete {zero}  (fsuc ())  _
delete {suc _} (fsuc i)  (j ◅ π) = ? ◅ delete i π

identity : {n : Nat} -> Permutation n
identity {zero } = ε
identity {suc n} = fzero ◅ identity

_⁻¹ : {n : Nat} -> Permutation n -> Permutation n
ε	⁻¹ = ε
(i ◅ π) ⁻¹ = ?

_○_ : {n : Nat} -> Permutation n -> Permutation n -> Permutation n
ε      ○ π₂ = ε
i ◅ π₁ ○ π₂ = (indices π₂ ! i) ◅ (π₁ ○ delete i π₂)
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import HoTT
open import cohomology.Theory

module cw.cohomology.TopGrid {i} (OT : OrdinaryTheory i)
  (n : ℤ) {X Y Z : Ptd i} (f : X ⊙→ Y) (g : Y ⊙→ Z) where

{-
  X --> Y ---> Z
  |     | this |
  v     v  one v
  1 -> Y/X -> Z/X
-}

  open OrdinaryTheory OT
  open import cohomology.PtdMapSequence cohomology-theory
  open import cw.cohomology.GridPtdMap f g using (Y/X-to-Z/X)

  top-grid-comm-sqr : CommSquare (fst g) (fst Y/X-to-Z/X) cfcod cfcod
  top-grid-comm-sqr = comm-sqr λ _ → idp

  C-top-grid-commutes : CommSquareᴳ
    (C-fmap n Y/X-to-Z/X) (C-fmap n g) (C-fmap n (⊙cfcod' (g ⊙∘ f))) (C-fmap n (⊙cfcod' f))
  C-top-grid-commutes = C-comm-square n top-grid-comm-sqr

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module my-nat where

open import product
open import bool
open import eq

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

infixl 10 _*_
infixl 9 _+_
--infixl 8 _<_ _=ℕ_ _≤_ _>_ _≥_

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

0+ : ∀ (x : ℕ) → 0 + x ≡ x
0+ x = refl

+0 : ∀ (x : ℕ) → x + 0 ≡ x
+0 zero = refl
+0 (suc x) rewrite +0 x = refl

+assoc : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
+assoc zero y z = refl
+assoc (suc x) y z rewrite +assoc x y z = refl

+suc : ∀ (x y : ℕ) → x + (suc y) ≡ suc(x + y)
+suc zero y = refl
+suc (suc x) y rewrite +suc x y = refl

+comm : ∀ (x y : ℕ) → x + y ≡ y + x
+comm zero y rewrite +0 y = refl
+comm (suc x) y rewrite +suc y x | +comm x y = refl

_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)

*distribr : ∀ (x y z : ℕ) → (x + y) * z ≡ x * z + y * z
--*distribr : ∀ (x y z : ℕ) → (x + y) * z ≡ x * z + y * z
*distribr zero y z = refl
*distribr (suc x) y z rewrite *distribr x y z = +assoc z (x * z) (y * z)

*0 : ∀ (x : ℕ) → x * 0 ≡ 0
*0 zero = refl
*0 (suc x) = *0 x

*suc : ∀ (x y : ℕ) → x * (suc y) ≡ x + x * y
*suc zero y = refl
*suc (suc x) y rewrite *suc x y
                       | +assoc y x (x * y)
                       | +assoc x y (x * y)
                       | +comm x y = refl

*comm : ∀ (x y : ℕ) → x * y ≡ y * x
*comm zero y rewrite *0 y = refl
*comm (suc x) y rewrite *suc y x | *comm x y = refl

*assoc : ∀ (x y z : ℕ) → x * (y * z) ≡ (x * y) * z
*assoc zero y z = refl
*assoc (suc x) y z rewrite *distribr y (x * y) z
                           | *assoc x y z = refl

_<_ : ℕ → ℕ → 𝔹
0 < 0 = ff
0 < (suc y) = tt
(suc x) < (suc y) = x < y
(suc x) < 0 = ff

_=ℕ_ : ℕ → ℕ → 𝔹
0 =ℕ 0 = tt
suc x =ℕ suc y = x =ℕ y
_ =ℕ _ = ff

=ℕ-refl : ∀ (x : ℕ) → (x =ℕ x) ≡ tt
=ℕ-refl zero = refl
=ℕ-refl (suc x) = =ℕ-refl x

=ℕ-to-≡ : ∀ {x y : ℕ} → x =ℕ y ≡ tt → x ≡ y
=ℕ-to-≡ {zero} {zero} u = refl
=ℕ-to-≡ {zero} {suc y} ()
=ℕ-to-≡ {suc x} {zero} ()
=ℕ-to-≡ {suc x} {suc y} u rewrite =ℕ-to-≡ {x} {y} u = refl

=ℕ-from-≡ : ∀ {x y : ℕ} → x ≡ y → x =ℕ y ≡ tt
=ℕ-from-≡ {x} {.x} refl = =ℕ-refl x

is-even : ℕ → 𝔹
is-odd : ℕ → 𝔹
is-even 0 = tt
is-even (suc x) = is-odd x
is-odd 0 = ff
is-odd (suc x) = is-even x

even~odd : ∀ (x : ℕ) → is-even x ≡ ~ is-odd x
odd~even : ∀ (x : ℕ) → is-odd x ≡ ~ is-even x
even~odd zero = refl
even~odd (suc x) = odd~even x
odd~even zero = refl
odd~even (suc x) = even~odd x

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


text:
module Common where
  ∗ : Set₁
  ∗ = Set

  _∘_ : {A B C : ∗} → (B → C) → (A → B) → (A → C)
  f ∘ g = λ a → f (g a)

  infixr 2 _×_
  infixr 1 _⊎_

  data _×_ (A B : ∗) : ∗ where
    _,_ : A → B → A × B

  proj₁ : ∀ {A B} → A × B → A
  proj₁ (a , b) = a

  proj₂ : ∀ {A B} → A × B → B
  proj₂ (a , b) = b

  uncurry : {A B C : ∗} → (A → B → C) → (A × B → C)
  uncurry f (a , b) = f a b

  data _⊎_ (A B : ∗) : ∗ where
    inj₁ : (x : A) → A ⊎ B
    inj₂ : (y : B) → A ⊎ B

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.Size

postulate
  P : (A : Set₁) → A → Set₁
  p : (i : Size) (f : {_ : Size< i} → Set) (x : _) →
      P ({_ : Size< i} → Set) f