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 LibraBFT.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import LibraBFT.ImplShared.Util.Crypto
open import Optics.All
open import Util.PKCS
open import Util.Prelude

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open        EpochConfig
open import Yasm.Base ℓ-RoundManager

-- 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 PreferredRoundRule
-- yet.  This will evolve as we build out a model of a real
-- implementation.

module LibraBFT.Concrete.System.Parameters where
 ConcSysParms : SystemTypeParameters
 ConcSysParms = mkSysTypeParms
                 NodeId
                 _≟NodeId_
                 BootstrapInfo
                 ∈BootstrapInfo-impl
                 RoundManager
                 NetworkMsg
                 Vote         -- TODO-3: This should be a type that also allows Block, because
                              -- NetworkMsgs can include signed Blocks, raising the possibility of
                              -- the "masquerading" issue mentioned in
                              -- LibraBFT.ImplShared.Util.Crypto, which we will need to address by
                              -- using HashTags, as also discussed in the module.
                 sig-Vote
                 _⊂Msg_

 open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

 module ParamsWithInitAndHandlers (iiah : SystemInitAndHandlers ConcSysParms) where
   open SystemInitAndHandlers iiah
   open WithInitAndHandlers iiah

   -- What EpochConfigs are known in the system?  For now, only the
   -- initial one.  Later, we will add knowledge of subsequent
   -- EpochConfigs known via EpochChangeProofs.  In fact, the
   -- implementation creates and stores and EpochChangeProof even for the
   -- initial epoch, so longer term just the inECP constructor may suffice.
   data EpochConfig∈Sys (st : SystemState) (𝓔 : EpochConfig) : Set ℓ-EC where
     inBootstrapInfo : init-EC bootstrapInfo ≡ 𝓔 → EpochConfig∈Sys st 𝓔
     -- inECP  : ∀ {ecp} → ecp ECP∈Sys st → verify-ECP ecp 𝓔 → EpochConfig∈Sys

   -- This is trivial for now, but will be nontrivial when we support epoch change
   𝓔-∈sys-injective : ∀ {st 𝓔₁ 𝓔₂}
                      → EpochConfig∈Sys st 𝓔₁
                      → EpochConfig∈Sys st 𝓔₂
                      → epoch 𝓔₁ ≡ epoch 𝓔₂
                      → 𝓔₁ ≡ 𝓔₂
   𝓔-∈sys-injective (inBootstrapInfo refl) (inBootstrapInfo refl) refl = refl

   -- A peer pid can sign a new message for a given PK if pid is the owner of a PK in a known
   -- EpochConfig.
   record PeerCanSignForPKinEpoch (st : SystemState) (v : Vote) (pid : NodeId) (pk : PK)
                                  (𝓔 : EpochConfig) (𝓔inSys : EpochConfig∈Sys st 𝓔)
                                  : Set ℓ-VSFP where
     constructor mkPCS4PKin𝓔
     field
       𝓔id≡    : epoch 𝓔 ≡ v ^∙ vEpoch
       mbr      : Member 𝓔
       nid≡     : toNodeId  𝓔 mbr ≡ pid
       pk≡      : getPubKey 𝓔 mbr ≡ pk
   open PeerCanSignForPKinEpoch

   record PeerCanSignForPK (st : SystemState) (v : Vote) (pid : NodeId) (pk : PK) : Set ℓ-VSFP where
     constructor mkPCS4PK
     field
       pcs4𝓔     : EpochConfig
       pcs4𝓔∈Sys : EpochConfig∈Sys st pcs4𝓔
       pcs4in𝓔   : PeerCanSignForPKinEpoch st v pid pk pcs4𝓔 pcs4𝓔∈Sys
   open PeerCanSignForPK

   PCS4PK⇒NodeId-PK-OK : ∀ {st v pid pk 𝓔 𝓔∈Sys} → (pcs : PeerCanSignForPKinEpoch st v pid pk 𝓔 𝓔∈Sys) → NodeId-PK-OK 𝓔 pk pid
   PCS4PK⇒NodeId-PK-OK (mkPCS4PKin𝓔 _ mbr n≡ pk≡) = mbr , n≡ , pk≡

   -- This is super simple for now because the only known EpochConfig is dervied from bootstrapInfo, which is not state-dependent
   PeerCanSignForPK-stable : ValidSenderForPK-stable-type PeerCanSignForPK
   PeerCanSignForPK-stable _ _ (mkPCS4PK 𝓔₁ (inBootstrapInfo refl) (mkPCS4PKin𝓔 𝓔id≡₁ mbr₁ nid≡₁ pk≡₁)) =
                               (mkPCS4PK 𝓔₁ (inBootstrapInfo refl) (mkPCS4PKin𝓔 𝓔id≡₁ mbr₁ nid≡₁ pk≡₁))

   peerCanSignEp≡ : ∀ {pid v v' pk s'}
                  → PeerCanSignForPK s' v pid pk
                  → v ^∙ vEpoch ≡ v' ^∙ vEpoch
                  → PeerCanSignForPK s' v' pid pk
   peerCanSignEp≡ (mkPCS4PK 𝓔₁ 𝓔inSys₁ (mkPCS4PKin𝓔 𝓔id≡₁ mbr₁ nid≡₁ pk≡₁)) refl
     = (mkPCS4PK 𝓔₁ 𝓔inSys₁ (mkPCS4PKin𝓔 𝓔id≡₁ mbr₁ nid≡₁ pk≡₁))


text:
open import and-example public
open import ex-andreas-abel public

ext: agda

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
{-# OPTIONS --show-irrelevant #-}

postulate
  A : Set
  f : .A → A

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

mutual
  X : .A → A
  X = _

  Y : A → A
  Y = {!λ x → x!}

  Z : A → A
  Z = {!λ x → x!}

  test : ∀ x → X (Y x) ≡ f (Z x)
  test x = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Adjoint where

open import Level
open import Data.Product

open import Basic
open import Category
import Functor
import Nat

open Category.Category
open Functor.Functor
open Nat.Nat
open Nat.Export

record Adjoint {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} (F : Functor.Functor C D) (G : Functor.Functor D C) : Set (suc ℓ ⊔ suc C₁ ⊔ C₀ ⊔ suc ℓ′ ⊔ suc D₁ ⊔ D₀) where
  field
    adjunction : {x : Obj C} {a : Obj D} → Setoids [ LiftSetoid {b = C₁ ⊔ D₁} {ℓ′ = ℓ ⊔ ℓ′} (Homsetoid D (fobj F x) a) ≅ LiftSetoid {b = C₁ ⊔ D₁} {ℓ′ = ℓ ⊔ ℓ′} (Homsetoid C x (fobj G a)) ]

  adjunct-→-Map : {x : Obj C} {a : Obj D} → Map.Map (Homsetoid D (fobj F x) a) (Homsetoid C x (fobj G a))
  adjunct-→-Map {x} {a} = lowerMap {d = C₁ ⊔ D₁} {ℓ″ = ℓ ⊔ ℓ′} (_[_≅_].map-→ (adjunction {x} {a}))

  adjunct-←-Map : {x : Obj C} {a : Obj D} → Map.Map (Homsetoid C x (fobj G a)) (Homsetoid D (fobj F x) a)
  adjunct-←-Map {x} {a} = lowerMap {d = C₁ ⊔ D₁} {ℓ″ = ℓ ⊔ ℓ′} (_[_≅_].map-← (adjunction {x} {a}))

  adjunct-→ : {x : Obj C} {a : Obj D} → Hom D (fobj F x) a → Hom C x (fobj G a)
  adjunct-→ f = Map.mapping (lowerMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (_[_≅_].map-→ adjunction)) f

  adjunct-← : {x : Obj C} {a : Obj D} → Hom C x (fobj G a) → Hom D (fobj F x) a
  adjunct-← f = Map.mapping (lowerMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (_[_≅_].map-← adjunction)) f

  adjunct-→←≈id : {x : Obj C} {a : Obj D} {f : Hom C x (fobj G a)} → C [ adjunct-→ (adjunct-← f) ≈ f ]
  adjunct-→←≈id {x} {a} {f} = lower (proj₁ (_[_≅_].proof adjunction) (lift f))

  adjunct-←→≈id : {x : Obj C} {a : Obj D} {f : Hom D (fobj F x) a} → D [ adjunct-← (adjunct-→ f) ≈ f ]
  adjunct-←→≈id {x} {a} {f} = lower (proj₂ (_[_≅_].proof adjunction) (lift f))

  field
    natural-in-→-C : {x y : Obj C} {a : Obj D} {f : Hom C y x} →
      Setoids [ Setoids [ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ C ][ f ,-] (fobj G a)) ∘ _[_≅_].map-→ adjunction ] ≈ Setoids [ _[_≅_].map-→ adjunction ∘ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ D ][ fmap F f ,-] a) ] ]
    natural-in-→-D : {x : Obj C} {a b : Obj D} {f : Hom D a b} →
      Setoids [ Setoids [ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ C ][-, fmap G f ] x) ∘ _[_≅_].map-→ adjunction ] ≈ Setoids [ _[_≅_].map-→ adjunction ∘ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ D ][-, f ] (fobj F x)) ] ]

  natural-in-←-C : {x y : Obj C} {a : Obj D} {f : Hom C y x} →
    Setoids [ Setoids [ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ D ][ fmap F f ,-] a) ∘ _[_≅_].map-← adjunction ] ≈ Setoids [ _[_≅_].map-← adjunction ∘ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ C ][ f ,-] (fobj G a)) ] ]
  natural-in-←-C {x} {y} {a} {f} = begin⟨ Setoids ⟩
    Setoids [ Ffa ∘ _[_≅_].map-← adjunction ] ≈⟨ ≈-composite Setoids {f = Ffa} {g = Setoids [ Setoids [ adj← ∘ fGa ] ∘ _[_≅_].map-→ adjunction ]} {h = adj→₂} {i = adj→₂} lem-1 (refl-hom Setoids {f = _[_≅_].map-← adjunction}) ⟩
    Setoids [ Setoids [ adj← ∘ fGa ] ∘ Setoids [ _[_≅_].map-→ adjunction ∘ _[_≅_].map-← adjunction ] ] ≈⟨ ≈-composite Setoids {f = Setoids [ adj← ∘ fGa ]} {g = Setoids [ adj← ∘ fGa ]} {h = Setoids [ _[_≅_].map-→ adjunction ∘ _[_≅_].map-← adjunction ]} {i = id Setoids} (refl-hom Setoids {f = Setoids [ adj← ∘ fGa ]}) (proj₁ (_[_≅_].proof adjunction)) ⟩
    Setoids [ adj← ∘ fGa ]
    ∎
    where
      Ffa = liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ D ][ fmap F f ,-] a)
      fGa = liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ C ][ f ,-] (fobj G a))
      adj← = _[_≅_].map-← adjunction
      adj→₂ = _[_≅_].map-← adjunction
      adj→ = _[_≅_].map-→ adjunction

      lem-1 : Setoids [ Ffa ≈ Setoids [ Setoids [ adj← ∘ fGa ] ∘ _[_≅_].map-→ adjunction ] ]
      lem-1 = begin⟨ Setoids ⟩
        Ffa ≈⟨ leftId Setoids {f = Ffa} ⟩
        Setoids [ id Setoids ∘ Ffa ] ≈⟨ ≈-composite Setoids {f = id Setoids} {g = Setoids [ adj← ∘ adj→ ]} {h = Ffa} {i = Ffa} (sym-hom Setoids {f = Setoids [ adj← ∘ adj→ ]} {g = id Setoids} (proj₂ (_[_≅_].proof adjunction))) (refl-hom Setoids {f = Ffa}) ⟩
        Setoids [ adj← ∘ Setoids [ adj→ ∘ Ffa ] ] ≈⟨ ≈-composite Setoids {f = adj←} {g = adj←} {h = Setoids [ adj→ ∘ Ffa ]} {i = Setoids [ fGa ∘ _[_≅_].map-→ adjunction ]} (refl-hom Setoids {f = adj←}) (sym-hom Setoids {f = Setoids [ fGa ∘ _[_≅_].map-→ adjunction ]} {g = Setoids [ adj→ ∘ Ffa ]} natural-in-→-C) ⟩
        Setoids [ Setoids [ _[_≅_].map-← adjunction ∘ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ C ][ f ,-] (fobj G a)) ] ∘ _[_≅_].map-→ adjunction ]
        ∎

  natural-in-←-D : {x : Obj C} {a b : Obj D} {f : Hom D a b} →
    Setoids [ Setoids [ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ D ][-, f ] (fobj F x)) ∘ _[_≅_].map-← adjunction ] ≈ Setoids [ _[_≅_].map-← adjunction ∘ liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ C ][-, fmap G f ] x) ] ]
  natural-in-←-D {x} {a} {b} {f} = begin⟨ Setoids ⟩
    Setoids [ fFx ∘ adj←a ] ≈⟨ ≈-composite Setoids {f = fFx} {g = Setoids [ Setoids [ adj←b ∘ Gfx ] ∘ adj→a ]} {h = adj←a} {i = adj←a} lem-1 (refl-hom Setoids {f = adj←a}) ⟩
    Setoids [ Setoids [ adj←b ∘ Gfx ] ∘ Setoids [ adj→a ∘ adj←a ] ] ≈⟨ ≈-composite Setoids {f = Setoids [ adj←b ∘ Gfx ]} {g = Setoids [ adj←b ∘ Gfx ]} {h = Setoids [ adj→a ∘ adj←a ]} {i = id Setoids} (refl-hom Setoids {f = Setoids [ adj←b ∘ Gfx ]}) (proj₁ (_[_≅_].proof adjunction)) ⟩
    Setoids [ adj←b ∘ Gfx ]
    ∎
    where
      fFx = liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ D ][-, f ] (fobj F x))
      Gfx = liftMap {d = C₁ ⊔ D₁} {ℓ″  = ℓ ⊔ ℓ′} (component HomNat[ C ][-, fmap G f ] x)
      adj←a = _[_≅_].map-← adjunction
      adj←b = _[_≅_].map-← adjunction
      adj→a = _[_≅_].map-→ adjunction
      adj→b = _[_≅_].map-→ adjunction

      lem-1 : Setoids [ fFx ≈ Setoids [ Setoids [ adj←b ∘ Gfx ] ∘ adj→a ] ]
      lem-1 = begin⟨ Setoids ⟩
        fFx ≈⟨ ≈-composite Setoids {f = id Setoids} {g = Setoids [ adj←b ∘ adj→b ]} {h = fFx} {i = fFx} (sym-hom Setoids {f = Setoids [ adj←b ∘ adj→b ]} {g = id Setoids} (proj₂ (_[_≅_].proof adjunction))) (refl-hom Setoids {f = fFx}) ⟩
        Setoids [ adj←b ∘ Setoids [ adj→b ∘ fFx ] ] ≈⟨ ≈-composite Setoids {f = adj←b} {g = adj←b} {h = Setoids [ adj→b ∘ fFx ]} {i = Setoids [ Gfx ∘ adj→a ]} (refl-hom Setoids {f = adj←b}) (sym-hom Setoids {f = Setoids [ Gfx ∘ adj→a ]} {g = Setoids [ adj→b ∘ fFx ]} natural-in-→-D) ⟩
        Setoids [ Setoids [ adj←b ∘ Gfx ] ∘ adj→a ]
        ∎

  naturality-point-←-C : {x y : Obj C} {a : Obj D} {f : Hom C y x} {k : Hom C x (fobj G a)} → D [ D [ adjunct-← k ∘ fmap F f ] ≈ adjunct-← (C [ k ∘ f ]) ]
  naturality-point-←-C = λ {x} {y} {a} {f} {k} → lower (natural-in-←-C (lift k))

  naturality-point-→-C : {x y : Obj C} {a : Obj D} {f : Hom C y x} {k : Hom D (fobj F x) a} → C [ C [ adjunct-→ k ∘ f ] ≈ adjunct-→ (D [ k ∘ fmap F f ]) ]
  naturality-point-→-C = λ {x} {y} {a} {f} {k} → lower (natural-in-→-C (lift k))

  naturality-point-←-D : {x : Obj C} {a b : Obj D} {f : Hom D a b} {k : Hom C x (fobj G a)} → D [ D [ f ∘ adjunct-← k ] ≈ adjunct-← (C [ fmap G f ∘ k ]) ]
  naturality-point-←-D = λ {x} {y} {a} {f} {k} → lower (natural-in-←-D (lift k))

  naturality-point-→-D : {x : Obj C} {a b : Obj D} {f : Hom D a b} {k : Hom D (fobj F x) a} → C [ C [ fmap G f ∘ adjunct-→ k ] ≈ adjunct-→ (D [ f ∘ k ]) ]
  naturality-point-→-D = λ {x} {y} {a} {f} {k} → lower (natural-in-→-D (lift k))

open Adjoint

unit : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → Adjoint F G → Nat.Nat (Functor.identity C) (Functor.compose G F)
unit {C₀} {C₁} {ℓ} {D₀} {D₁} {ℓ′} {C} {D} {F} {G} F⊣G = record {
  component = λ X → adjunct-→ F⊣G (id D) ;
  naturality = λ {a} {b} {f} → begin⟨ C ⟩
    C [ adjunct-→ F⊣G (id D) ∘ fmap (Functor.identity C) f ] ≈⟨ naturality-point-→-C F⊣G ⟩
    adjunct-→ F⊣G (D [ id D ∘ fmap F (fmap (Functor.identity C) f) ]) ≈⟨ Map.preserveEq (adjunct-→-Map F⊣G) (leftId D) ⟩
    adjunct-→ F⊣G (fmap F f) ≈⟨ Map.preserveEq (adjunct-→-Map F⊣G) (sym-hom D (rightId D)) ⟩
    adjunct-→ F⊣G (D [ fmap F f ∘ id D ]) ≈⟨ sym-hom C (naturality-point-→-D F⊣G) ⟩
    C [ fmap (Functor.compose G F) f ∘ adjunct-→ F⊣G (id D) ]
    ∎ }

counit : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → Adjoint F G → Nat.Nat (Functor.compose F G) (Functor.identity D)
counit {C₀} {C₁} {ℓ} {D₀} {D₁} {ℓ′} {C} {D} {F} {G} F⊣G = record {
  component = λ X → adjunct-← F⊣G (id C) ;
  naturality = λ {a} {b} {f} → begin⟨ D ⟩
    D [ adjunct-← F⊣G (id C) ∘ fmap (Functor.compose F G) f ] ≈⟨ naturality-point-←-C F⊣G ⟩
    adjunct-← F⊣G (C [ id C ∘ fmap G f ]) ≈⟨ Map.preserveEq (adjunct-←-Map F⊣G) (leftId C) ⟩
    adjunct-← F⊣G (fmap G f) ≈⟨ Map.preserveEq (adjunct-←-Map F⊣G) (sym-hom C (rightId C)) ⟩
    adjunct-← F⊣G (C [ fmap G f ∘ id C ]) ≈⟨ sym-hom D (naturality-point-←-D F⊣G) ⟩
    D [ fmap (Functor.identity D) f ∘ adjunct-← F⊣G (id C) ]
    ∎}

Unit-universal : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → Adjoint F G → Set _
Unit-universal {C = C} {D} {F} {G} adj = ∀ {X : Obj C} {A : Obj D} (f : Hom C X (fobj G A)) → ∃! (λ x y → D [ x ≈ y ]) (λ (h : Hom D (fobj F X) A) → C [ C [ fmap G h ∘ component (unit adj) X ] ≈ f ])

unit-universality : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → (adj : Adjoint F G) → Unit-universal adj
unit-universality {C = C} {D} {F} {G} F⊣G {X} {A} f =
  adjunct-← F⊣G f , lem-1 , lem-2
  where
    lem-1 = begin⟨ C ⟩
      C [ fmap G (adjunct-← F⊣G f) ∘ component (unit F⊣G) X ] ≈⟨ naturality-point-→-D F⊣G ⟩
      adjunct-→ F⊣G (D [ adjunct-← F⊣G f ∘ id D ]) ≈⟨ Map.preserveEq (adjunct-→-Map F⊣G) (≈-composite D (refl-hom D) (sym-hom D (preserveId F))) ⟩
      adjunct-→ F⊣G (D [ adjunct-← F⊣G f ∘ fmap F (id C) ]) ≈⟨ sym-hom C (naturality-point-→-C F⊣G) ⟩
      C [ adjunct-→ F⊣G (adjunct-← F⊣G f) ∘ id C ] ≈⟨ rightId C ⟩
      adjunct-→ F⊣G (adjunct-← F⊣G f) ≈⟨ adjunct-→←≈id F⊣G ⟩
      f
      ∎

    lem-2 = λ {y} eq → begin⟨ D ⟩
      adjunct-← F⊣G f ≈⟨ Map.preserveEq (adjunct-←-Map F⊣G) (sym-hom C eq) ⟩
      adjunct-← F⊣G (C [ fmap G y ∘ component (unit F⊣G) X ]) ≈⟨ sym-hom D (naturality-point-←-D (F⊣G)) ⟩
      D [ y ∘ adjunct-← F⊣G (adjunct-→ F⊣G (id D)) ] ≈⟨ ≈-composite D (refl-hom D) (adjunct-←→≈id F⊣G) ⟩
      D [ y ∘ id D ] ≈⟨ rightId D ⟩
      y
      ∎

Counit-universal : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → Adjoint F G → Set _
Counit-universal {C = C} {D} {F} {G} adj = ∀ {X : Obj C} {A : Obj D} (h : Hom D (fobj F X) A) → ∃! (λ x y → C [ x ≈ y ]) (λ (f : Hom C X (fobj G A)) → D [ D [ component (counit adj) A ∘ fmap F f ] ≈ h ])

counit-universality : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → (adj : Adjoint F G) → Counit-universal adj
counit-universality {C = C} {D} {F} {G} F⊣G = λ {X} {A} h →
  adjunct-→ F⊣G h , lem-1 , lem-2
  where
    lem-1 = λ {A} {h} → begin⟨ D ⟩
      D [ component (counit F⊣G) A ∘ fmap F (adjunct-→ F⊣G h) ] ≈⟨ naturality-point-←-C F⊣G ⟩
      adjunct-← F⊣G (C [ id C ∘ adjunct-→ F⊣G h ]) ≈⟨ Map.preserveEq (adjunct-←-Map F⊣G) (leftId C) ⟩
      adjunct-← F⊣G (adjunct-→ F⊣G h) ≈⟨ adjunct-←→≈id F⊣G ⟩
      h
      ∎

    lem-2 = λ {A} {h} {y} eq → begin⟨ C ⟩
      adjunct-→ F⊣G h ≈⟨ Map.preserveEq (adjunct-→-Map F⊣G) (sym-hom D eq) ⟩
      adjunct-→ F⊣G (D [ component (counit F⊣G) A ∘ fmap F y ]) ≈⟨ sym-hom C (naturality-point-→-C F⊣G) ⟩
      C [ adjunct-→ F⊣G (component (counit F⊣G) A) ∘ y ] ≈⟨ ≈-composite C (adjunct-→←≈id F⊣G) (refl-hom C) ⟩
      C [ id C ∘ y ] ≈⟨ leftId C ⟩
      y
      ∎

TriangularL : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → Nat.Nat (Functor.identity C) (Functor.compose G F) → Nat.Nat (Functor.compose F G) (Functor.identity D) → Set _
TriangularL {C = C} {D} {F} {G} η ε = [ C , D ] [ Nat.compose (Nat.compose Nat.leftIdNat→ (ε N∘F F)) (Nat.compose (Nat.assocNat← {F = F} {G} {F}) (Nat.compose (F F∘N η) Nat.rightIdNat←)) ≈ id [ C , D ] ]

triangularL-point : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → (η : Nat.Nat (Functor.identity C) (Functor.compose G F)) → (ε : Nat.Nat (Functor.compose F G) (Functor.identity D)) → {a : Obj C} → (triL : TriangularL {F = F} {G} η ε) → D [ D [ component (ε N∘F F) a ∘ component (F F∘N η) a ] ≈ id D {fobj F a} ]
triangularL-point {C = C} {D} {F} {G} η ε {a} triL = begin⟨ D ⟩
  D [ component (ε N∘F F) a ∘ component (F F∘N η) a ] ≈⟨ sym-hom D (≈-composite D (leftId D) (trans-hom D (leftId D) (rightId D))) ⟩
  D [ D [ id D ∘ component (ε N∘F F) a ] ∘ D [ id D ∘ D [ component (F F∘N η) a ∘ id D ] ] ] ≈⟨ triL {a} ⟩
  id D
  ∎

triangularL : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → (adj : Adjoint F G) → TriangularL {F = F} {G} (unit adj) (counit adj)
triangularL {C = C} {D} {F} {G} adj = λ {a} →
  begin⟨ D ⟩
    component (Nat.compose εF (Nat.compose (Nat.assocNat← {F = F} {G} {F}) Fη)) a
  ≈⟨ ≈-composite D (leftId D) (trans-hom D (leftId D) (rightId D)) ⟩
    D [ component ε (fobj F a) ∘ fmap F (component η a) ]
  ≈⟨ proj₁ (proj₂ (counit-universality adj (id D))) ⟩
    id D
  ≈⟨ refl-hom D ⟩
    component (id [ C , D ] {F}) a
  ∎
  where
    ε = counit adj
    η = unit adj
    εF = Nat.compose Nat.leftIdNat→ (counit adj N∘F F)
    Fη = Nat.compose {F = F} (F F∘N unit adj) Nat.rightIdNat←

TriangularR : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → Nat.Nat (Functor.identity C) (Functor.compose G F) → Nat.Nat (Functor.compose F G) (Functor.identity D) → Set _
TriangularR {C = C} {D} {F} {G} η ε = [ D , C ] [ Nat.compose (Nat.compose Nat.rightIdNat→ (G F∘N ε)) (Nat.compose (Nat.assocNat→ {F = G} {F} {G}) (Nat.compose (η N∘F G) Nat.leftIdNat←)) ≈ id [ D , C ] ]

triangularR : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → (adj : Adjoint F G) → TriangularR {F = F} (unit adj) (counit adj)
triangularR {C = C} {D} {F} {G} adj = λ {a} → begin⟨ C ⟩
  component (Nat.compose Gε (Nat.compose (Nat.assocNat→ {F = G} {F} {G}) ηG)) a ≈⟨ ≈-composite C (leftId C) (trans-hom C (leftId C) (rightId C)) ⟩
  C [ fmap G (component ε a) ∘ component η (fobj G a) ] ≈⟨ proj₁ (proj₂ (unit-universality adj (id C))) ⟩
  id C ≈⟨ refl-hom C ⟩
  component (id [ D , C ] {G}) a
  ∎
  where
    ε = counit adj
    η = unit adj
    Gε = Nat.compose {H = G} Nat.rightIdNat→ (G F∘N counit adj)
    ηG = Nat.compose (unit adj N∘F G) Nat.leftIdNat←

triangularR-point : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → (η : Nat.Nat (Functor.identity C) (Functor.compose G F)) → (ε : Nat.Nat (Functor.compose F G) (Functor.identity D)) → {a : Obj D} → (triR : TriangularR {F = F} {G} η ε) → C [ C [ component (G F∘N ε) a ∘ component (η N∘F G) a ] ≈ id C {fobj G a} ]
triangularR-point {C = C} {D} {F} {G} η ε {a} triR = begin⟨ C ⟩
  C [ component (G F∘N ε) a ∘ component (η N∘F G) a ] ≈⟨ sym-hom C (≈-composite C (leftId C) (trans-hom C (leftId C) (rightId C))) ⟩
  C [ C [ id C ∘ component (G F∘N ε) a ] ∘ C [ id C ∘ C [ component (η N∘F G) a ∘ id C ] ] ] ≈⟨ triR {a = a} ⟩
  id C
  ∎

unit-triangular-holds-adjoint : ∀ {C₀ C₁ ℓ D₀ D₁ ℓ′} {C : Category C₀ C₁ ℓ} {D : Category D₀ D₁ ℓ′} {F : Functor.Functor C D} {G : Functor.Functor D C} → (η : Nat.Nat (Functor.identity C) (Functor.compose G F)) → (ε : Nat.Nat (Functor.compose F G) (Functor.identity D)) → TriangularL {F = F} η ε → TriangularR {F = F} η ε → Adjoint F G
unit-triangular-holds-adjoint {C = C} {D} {F} {G} η ε triL triR = record {
  adjunction = λ {x} {a} → record {
    map-→ = record {
      mapping = λ Fx→a → lift (C [ fmap G (lower Fx→a) ∘ component η x ]) ;
      preserveEq = λ {x′} {y} x₂ → lift (≈-composite C (Functor.preserveEq G (lower x₂)) (refl-hom C)) } ;
    map-← = record {
      mapping = λ x→Ga → lift (D [ component ε a ∘ fmap F (lower x→Ga) ]) ;
      preserveEq = λ {x′} {y} x₂ → lift (≈-composite D (refl-hom D) (Functor.preserveEq F (lower x₂))) } ;
    proof = p1 , p2 } ;
  natural-in-→-C = λ {x} {y} {a} {f} Fx→a → lift (begin⟨ C ⟩
    C [ C [ fmap G (lower Fx→a) ∘ component η x ] ∘ f ] ≈⟨ assoc C ⟩
    C [ fmap G (lower Fx→a) ∘ C [ component η x ∘ f ] ] ≈⟨ ≈-composite C (refl-hom C) (naturality η) ⟩
    C [ fmap G (lower Fx→a) ∘ C [ fmap G (fmap F f) ∘ component η y ] ] ≈⟨ sym-hom C (assoc C) ⟩
    C [ C [ fmap G (lower Fx→a) ∘ fmap G (fmap F f) ] ∘ component η y ] ≈⟨ ≈-composite C (sym-hom C (preserveComp G)) (refl-hom C) ⟩
    C [ fmap G (D [ lower Fx→a ∘ fmap F f ]) ∘ component η y ]
    ∎) ;
  natural-in-→-D = λ {x} {a} {b} {f} Fx→a → lift (begin⟨ C ⟩
    C [ fmap G f ∘ C [ fmap G (lower Fx→a) ∘ component η x ] ] ≈⟨ sym-hom C (assoc C) ⟩
    C [ C [ fmap G f ∘ fmap G (lower Fx→a) ] ∘ component η x ] ≈⟨ ≈-composite C (sym-hom C (preserveComp G)) (refl-hom C) ⟩
    C [ fmap G (D [ f ∘ lower Fx→a ]) ∘ component η x ]
    ∎) }

  where
    p1 = λ {x} {a} x→Ga → lift (begin⟨ C ⟩
      C [ fmap G (D [ component ε a ∘ fmap F (lower x→Ga) ]) ∘ component η x ] ≈⟨ ≈-composite C (preserveComp G) (refl-hom C) ⟩
      C [ C [ fmap G (component ε a) ∘ fmap G (fmap F (lower x→Ga)) ] ∘ component η x ] ≈⟨ assoc C ⟩
      C [ fmap G (component ε a) ∘ C [ fmap G (fmap F (lower x→Ga)) ∘ component η x ] ] ≈⟨ ≈-composite C (refl-hom C) (sym-hom C (naturality η)) ⟩
      C [ fmap G (component ε a) ∘ C [ component η (fobj G a) ∘ (lower x→Ga) ] ] ≈⟨ sym-hom C (assoc C) ⟩
      C [ C [ fmap G (component ε a) ∘ component η (fobj G a) ] ∘ (lower x→Ga) ] ≈⟨ ≈-composite C (triangularR-point {F = F} η ε {a = a} triR) (refl-hom C) ⟩
      C [ id C ∘ (lower x→Ga) ] ≈⟨ leftId C ⟩
      lower x→Ga
      ∎)

    p2 = λ {x} {a} Fx→a → lift (begin⟨ D ⟩
      D [ component ε a ∘ fmap F (C [ fmap G (lower Fx→a) ∘ component η x ]) ] ≈⟨ ≈-composite D (refl-hom D) (preserveComp F) ⟩
      D [ component ε a ∘ D [ fmap F (fmap G (lower Fx→a)) ∘ fmap F (component η x) ] ] ≈⟨ sym-hom D (assoc D) ⟩
      D [ D [ component ε a ∘ fmap F (fmap G (lower Fx→a)) ] ∘ fmap F (component η x) ] ≈⟨ ≈-composite D (naturality ε) (refl-hom D) ⟩
      D [ D [ lower Fx→a ∘ component ε (fobj F x) ] ∘ fmap F (component η x) ] ≈⟨ assoc D ⟩
      D [ lower Fx→a ∘ D [ component ε (fobj F x) ∘ fmap F (component η x) ] ] ≈⟨ ≈-composite D (refl-hom D) (triangularL-point {F = F} η ε {a = x} triL) ⟩
      D [ lower Fx→a ∘ id D ] ≈⟨ rightId D ⟩
      lower Fx→a
      ∎)

module Export where
  _⊣_ = Adjoint

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


text:
------------------------------------------------------------------------------
-- Properties for the equality on streams
------------------------------------------------------------------------------

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

module FOTC.Data.Stream.Equality.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Stream.Type
open import FOTC.Relation.Binary.Bisimilarity.PropertiesATP
open import FOTC.Relation.Binary.Bisimilarity.Type

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

postulate stream-≡→≈ : ∀ {xs ys} → Stream xs → Stream ys → xs ≡ ys → xs ≈ ys
{-# ATP prove stream-≡→≈ ≈-refl #-}

-- See Issue https://github.com/asr/apia/issues/81 .
≈→Stream₁A : D → Set
≈→Stream₁A ws = ∃[ zs ] ws ≈ zs
{-# ATP definition ≈→Stream₁A #-}

≈→Stream₁ : ∀ {xs ys} → xs ≈ ys → Stream xs
≈→Stream₁ {xs} {ys} h = Stream-coind ≈→Stream₁A h' (ys , h)
  where
  postulate h' : ∀ {xs} → ≈→Stream₁A xs →
                 ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ ≈→Stream₁A xs'
  {-# ATP prove h' #-}

-- See Issue https://github.com/asr/apia/issues/81 .
≈→Stream₂A : D → Set
≈→Stream₂A zs = ∃[ ws ] ws ≈ zs
{-# ATP definition ≈→Stream₂A #-}

≈→Stream₂ : ∀ {xs ys} → xs ≈ ys → Stream ys
≈→Stream₂ {xs} {ys} h = Stream-coind ≈→Stream₂A h' (xs , h)
  where
  postulate h' : ∀ {ys} → ≈→Stream₂A ys →
                 ∃[ y' ] ∃[ ys' ] ys ≡ y' ∷ ys' ∧ ≈→Stream₂A ys'
  {-# ATP prove h' #-}

≈→Stream : ∀ {xs ys} → xs ≈ ys → Stream xs ∧ Stream ys
≈→Stream {xs} {ys} h = ≈→Stream₁ h , ≈→Stream₂ h

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Cubical.Categories.Limits.Terminal where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Foundations.HLevels
open import Cubical.Categories.Category
open import Cubical.Categories.Functor

private
  variable
    ℓ ℓ' : Level

module _ (C : Precategory ℓ ℓ') where
  open Precategory C

  isInitial : (x : ob) → Type (ℓ-max ℓ ℓ')
  isInitial x = ∀ (y : ob) → isContr (C [ x , y ])

  isFinal : (x : ob) → Type (ℓ-max ℓ ℓ')
  isFinal x = ∀ (y : ob) → isContr (C [ y , x ])

  hasInitialOb : Type (ℓ-max ℓ ℓ')
  hasInitialOb = Σ[ x ∈ ob ] isInitial x

  hasFinalOb : Type (ℓ-max ℓ ℓ')
  hasFinalOb = Σ[ x ∈ ob ] isFinal x

  -- Initiality of an object is a proposition.
  isPropIsInitial : (x : ob) → isProp (isInitial x)
  isPropIsInitial x = isPropΠ λ y → isPropIsContr

  -- Objects that are initial are isomorphic.
  isInitialToIso : {x y : ob} (hx : isInitial x) (hy : isInitial y) →
    CatIso {C = C} x y
  isInitialToIso {x = x} {y = y} hx hy =
    let x→y : C [ x , y ]
        x→y = fst (hx y) -- morphism forwards
        y→x : C [ y , x ]
        y→x = fst (hy x) -- morphism backwards
        x→y→x : x→y ⋆⟨ C ⟩ y→x ≡ id x
        x→y→x = isContr→isProp (hx x) _ _ -- compose to id by uniqueness
        y→x→y : y→x ⋆⟨ C ⟩ x→y ≡ id y
        y→x→y = isContr→isProp (hy y) _ _ -- similar.
    in catiso x→y y→x y→x→y x→y→x

  open isUnivalent

  -- The type of initial objects of a univalent precategory is a proposition,
  -- i.e. all initial objects are equal.
  isPropInitial : (hC : isUnivalent C) → isProp (hasInitialOb)
  isPropInitial hC x y =
    -- Being initial is a prop ∴ Suffices equal as objects in C.
    Σ≡Prop (isPropIsInitial)
    -- C is univalent ∴ Suffices isomorphic as objects in C.
    (CatIsoToPath hC (isInitialToIso (snd x) (snd y)))

  -- Now the dual argument for final objects.

  -- Finality of an object is a proposition.
  isPropIsFinal : (x : ob) → isProp (isFinal x)
  isPropIsFinal x = isPropΠ λ y → isPropIsContr

  -- Objects that are initial are isomorphic.
  isFinalToIso : {x y : ob} (hx : isFinal x) (hy : isFinal y) →
    CatIso {C = C} x y
  isFinalToIso {x = x} {y = y} hx hy =
    let x→y : C [ x , y ]
        x→y = fst (hy x) -- morphism forwards
        y→x : C [ y , x ]
        y→x = fst (hx y) -- morphism backwards
        x→y→x : x→y ⋆⟨ C ⟩ y→x ≡ id x
        x→y→x = isContr→isProp (hx x) _ _ -- compose to id by uniqueness
        y→x→y : y→x ⋆⟨ C ⟩ x→y ≡ id y
        y→x→y = isContr→isProp (hy y) _ _ -- similar.
    in catiso x→y y→x y→x→y x→y→x

  -- The type of final objects of a univalent precategory is a proposition,
  -- i.e. all final objects are equal.
  isPropFinal : (hC : isUnivalent C) → isProp (hasFinalOb)
  isPropFinal hC x y =
    -- Being final is a prop ∴ Suffices equal as objects in C.
    Σ≡Prop (isPropIsFinal)
    -- C is univalent ∴ Suffices isomorphic as objects in C.
    (CatIsoToPath hC (isFinalToIso (snd x) (snd y)))


text:
-- Andreas, 2017-01-13, issue #2403

open import Common.Nat

postulate
  P : Nat → Set
  f : ∀{n} → P n → P (pred n)

test : ∀ n → P n → Set
test zero    p = Nat
test (suc n) p = test _ (f p)

-- WAS:
-- The meta-variable is solved to (pred (suc n))
-- Termination checking fails.

-- NOW: If the termination checker normalizes the argument and it passes.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module VecSN where

open import Data.Bool

infixr 20 _◎_

------------------------------------------------------------------------------
-- fix a field F_3 = {0, 1, -1}
-- types B (ZERO,ONE,PLUS,TIMES) determine the DIMENSION of a vector space over F_3
-- values of type B are INDICES for B-dimensional vectors
-- we do not allow superpositions (we have AT MOST one entry in the
-- vector that is non-zero), so we can identify the INDICES with the vectors
--
-- in particular:
--   - ZERO is not the empty type! it is like the 0-dimensional vector space
--     (i.e, the type containing one "annihilating value")
--   - ONE is like a 1-dimensional vector space; it is isomorphic to
--     the scalars (0,+1,-1)
--   - PLUS gives the direct sum of vector spaces (dimension is the sum)
--   - TIMES gives the tensor product of vector spaces (dimension is the product)
--   - DUAL gives the dual space (functionals that map vectors to scalars; i.e.
--     that maps values to scalars)

data B : Set where
  ZERO   : B
  ONE    : B
  PLUS   : B → B → B
  TIMES  : B → B → B
  DUAL   : B → B

-- now we describe the vectors for each B-dimensional vector space
-- the zero vector is everywhere

data BVAL : B → Set where
  zero : {b : B} → BVAL b
  unit : BVAL ONE
  left : {b₁ b₂ : B} → BVAL b₁ → BVAL (PLUS b₁ b₂)
  right : {b₁ b₂ : B} → BVAL b₂ → BVAL (PLUS b₁ b₂)
  pair : {b₁ b₂ : B} → BVAL b₁ → BVAL b₂ → BVAL (TIMES b₁ b₂)
  dual : {b : B} → BVAL b → BVAL (DUAL b)

-- syntactic equality on vectors

b= : { b : B } → BVAL b → BVAL b → Bool
b= zero zero = true
b= unit unit = true
b= (left v₁) (left v₂) = b= v₁ v₂
b= (right v₁) (right v₂) = b= v₁ v₂
b= (pair v₁ v₂) (pair v₁' v₂') = b= v₁ v₁' ∧ b= v₂ v₂'
b= (dual v₁) (dual v₂) = b= v₁ v₂
b= _ _ = false

data Iso : B → B → Set where
  -- (+,0) commutative monoid
  unite₊  : { b : B } → Iso (PLUS ZERO b) b
  uniti₊  : { b : B } → Iso b (PLUS ZERO b)
  swap₊   : { b₁ b₂ : B } → Iso (PLUS b₁ b₂) (PLUS b₂ b₁)
  assocl₊ : { b₁ b₂ b₃ : B } → Iso (PLUS b₁ (PLUS b₂ b₃)) (PLUS (PLUS b₁ b₂) b₃)
  assocr₊ : { b₁ b₂ b₃ : B } → Iso (PLUS (PLUS b₁ b₂) b₃) (PLUS b₁ (PLUS b₂ b₃))
  -- (*,1) commutative monoid
  unite⋆  : { b : B } → Iso (TIMES ONE b) b
  uniti⋆  : { b : B } → Iso b (TIMES ONE b)
  swap⋆   : { b₁ b₂ : B } → Iso (TIMES b₁ b₂) (TIMES b₂ b₁)
  assocl⋆ : { b₁ b₂ b₃ : B } → Iso (TIMES b₁ (TIMES b₂ b₃)) (TIMES (TIMES b₁ b₂) b₃)
  assocr⋆ : { b₁ b₂ b₃ : B } → Iso (TIMES (TIMES b₁ b₂) b₃) (TIMES b₁ (TIMES b₂ b₃))
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : B } →
            Iso (TIMES (PLUS b₁ b₂) b₃) (PLUS (TIMES b₁ b₃) (TIMES b₂ b₃))
  factor  : { b₁ b₂ b₃ : B } →
            Iso (PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)) (TIMES (PLUS b₁ b₂) b₃)
  -- closure
  id⟷   : { b : B } → Iso b b
  sym    : { b₁ b₂ : B } → Iso b₁ b₂ → Iso b₂ b₁
  _◎_    : { b₁ b₂ b₃ : B } → Iso b₁ b₂ → Iso b₂ b₃ → Iso b₁ b₃
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           Iso b₁ b₃ → Iso b₂ b₄ → Iso (PLUS b₁ b₂) (PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           Iso b₁ b₃ → Iso b₂ b₄ → Iso (TIMES b₁ b₂) (TIMES b₃ b₄)
  -- multiplicative duality
  refe⋆   : { b : B } → Iso (DUAL (DUAL b)) b
  refi⋆   : { b : B } → Iso b (DUAL (DUAL b))
  rile⋆   : { b : B } → Iso (TIMES b (TIMES b (DUAL b))) b
  rili⋆   : { b : B } → Iso b (TIMES b (TIMES b (DUAL b)))
  -- negatives: we have a circuit that requires the value to choose
  -- the incoming value : b₁ can go left or right
  choose : { b₁ b₂ : B } → Iso b₁ b₂ → Iso b₁ b₂ → Iso b₁ b₂

mutual

  eval : {b₁ b₂ : B} → Iso b₁ b₂ → BVAL b₁ → BVAL b₂
  eval unite₊ (left _) = zero
  eval unite₊ (right v) = v
  eval uniti₊ v = right v
  eval swap₊ (left v) = right v
  eval swap₊ (right v) = left v
  eval assocl₊ (left v) = left (left v)
  eval assocl₊ (right (left v)) = left (right v)
  eval assocl₊ (right (right v)) = right v
  eval assocr₊ (left (left v)) = left v
  eval assocr₊ (left (right v)) = right (left v)
  eval assocr₊ (right v) = right (right v)
  eval unite⋆ (pair unit v) = v
  eval uniti⋆ v = pair unit v
  eval swap⋆ (pair v1 v2) = pair v2 v1
  eval assocl⋆ (pair v1 (pair v2 v3)) = pair (pair v1 v2) v3
  eval assocr⋆ (pair (pair v1 v2) v3) = pair v1 (pair v2 v3)
  eval dist (pair (left v1) v3) = left (pair v1 v3)
  eval dist (pair (right v2) v3) = right (pair v2 v3)
  eval factor (left (pair v1 v3)) = pair (left v1) v3
  eval factor (right (pair v2 v3)) = pair (right v2) v3
  eval id⟷ v = v
  eval (sym c) v = evalB c v
  eval (c₁ ◎ c₂) v = eval c₂ (eval c₁ v)
  eval (c₁ ⊕ c₂) (left v) = left (eval c₁ v)
  eval (c₁ ⊕ c₂) (right v) = right (eval c₂ v)
  eval (c₁ ⊗ c₂) (pair v₁ v₂) = pair (eval c₁ v₁) (eval c₂ v₂)
  eval refe⋆ (dual (dual v)) = v
  eval refi⋆ v = dual (dual v)
  eval rile⋆ (pair v (pair v₁ (dual v₂))) with b= v₁ v₂
  eval rile⋆ (pair v (pair v₁ (dual v₂))) | true = v
  eval rile⋆ (pair v (pair v₁ (dual v₂))) | false = zero
  eval rili⋆ v = pair v (pair v (dual v))
-- choose : { b₁ b₂ : B } → Iso b₁ b₂ → Iso b₁ b₂ → Iso b₁ b₂
  eval (choose c₁ c₂) v = {!!}
  eval _ _ = zero

  evalB : {b₁ b₂ : B} → Iso b₁ b₂ → BVAL b₂ → BVAL b₁
  evalB unite₊ v = right v
  evalB uniti₊ (left _) = zero
  evalB uniti₊ (right v) = v
  evalB swap₊ (left v) = right v
  evalB swap₊ (right v) = left v
  evalB assocl₊ (left (left v)) = left v
  evalB assocl₊ (left (right v)) = right (left v)
  evalB assocl₊ (right v) = right (right v)
  evalB assocr₊ (left v) = left (left v)
  evalB assocr₊ (right (left v)) = left (right v)
  evalB assocr₊ (right (right v)) = right v
  evalB unite⋆ v = pair unit v
  evalB uniti⋆ (pair unit v) = v
  evalB swap⋆ (pair v1 v2) = pair v2 v1
  evalB assocl⋆ (pair (pair v1 v2) v3) = pair v1 (pair v2 v3)
  evalB assocr⋆ (pair v1 (pair v2 v3)) = pair (pair v1 v2) v3
  evalB dist (left (pair v1 v3)) = pair (left v1) v3
  evalB dist (right (pair v2 v3)) = pair (right v2) v3
  evalB factor (pair (left v1) v3) = left (pair v1 v3)
  evalB factor (pair (right v2) v3) = right (pair v2 v3)
  evalB id⟷ v = v
  evalB (sym c) v = eval c v
  evalB (c₁ ◎ c₂) v = evalB c₁ (evalB c₂ v)
  evalB (c₁ ⊕ c₂) (left v) = left (evalB c₁ v)
  evalB (c₁ ⊕ c₂) (right v) = right (evalB c₂ v)
  evalB (c₁ ⊗ c₂) (pair v₁ v₂) = pair (evalB c₁ v₁) (evalB c₂ v₂)
  evalB refe⋆ v = dual (dual v)
  evalB refi⋆ (dual (dual v)) = v
  evalB rile⋆ v = pair v (pair v (dual v))
  evalB rili⋆ (pair v (pair v₁ (dual v₂))) with b= v₁ v₂
  evalB rili⋆ (pair v (pair v₁ (dual v₂))) | true = v
  evalB rili⋆ (pair v (pair v₁ (dual v₂))) | false = zero
  evalB _ _ = zero

------------------------------------------------------------------------------
-- example with duals

pibool : B
pibool = PLUS ONE ONE

pitrue : BVAL pibool
pitrue = left unit

pifalse : BVAL pibool
pifalse = right unit

-- swap clause 1 = (T => F)
clause1 : BVAL (TIMES (DUAL pibool) pibool)
clause1 = pair (dual pitrue) pifalse

-- swap clause 2 = (F => T)
clause2 : BVAL (TIMES (DUAL pibool) pibool)
clause2 = pair (dual pifalse) pitrue

-- swap clause 1 applied to true
ex1 : BVAL (TIMES pibool (TIMES (DUAL pibool) pibool))
ex1 = pair pitrue clause1

-- swap clause 1 applied to false
ex2 : BVAL (TIMES pibool (TIMES (DUAL pibool) pibool))
ex2 = pair pifalse clause1

-- swap clause 1 applied to true
ex3 : BVAL (TIMES pibool (TIMES (DUAL pibool) pibool))
ex3 = pair pitrue clause2

-- swap clause 1 applied to false
ex4 : BVAL (TIMES pibool (TIMES (DUAL pibool) pibool))
ex4 = pair pifalse clause2

-- applies one of the clauses to a value
c : Iso (TIMES pibool (TIMES (DUAL pibool) pibool)) pibool
c =         -- (v,(1/t,f))
  assocl⋆ ◎ -- ((v,1/t),f)
  swap⋆ ◎   -- (f,(v,1/t))
  rile⋆     -- f or zero

--
v1 = eval c ex1
v2 = eval c ex2
v3 = eval c ex3
v4 = eval c ex4

-- generalize

-- applies one of the clauses of a function : b -> b to a value : b
apply : {b : B} → Iso (TIMES b (TIMES (DUAL b) b)) b
apply = assocl⋆ ◎ swap⋆ ◎ rile⋆

{--
want:

value is True
in parallel apply clause1 to value and apply clause2 to value
one of these will return False and the other will return zero
merge the results to get False

better:

value is True
we create a new logic variable ALPHA which can be unified with either clause1 or clause2
we create a value (ALPHA - ALPHA) which we apply to evaluate

--}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Polynomial.Simple.AlmostCommutativeRing.Instances where

open import Polynomial.Simple.AlmostCommutativeRing
open import Level using (0ℓ)
open import Agda.Builtin.Reflection

module Nat where
  open import Data.Nat using (zero; suc)
  open import Relation.Binary.PropositionalEquality using (refl)
  open import Data.Nat.Properties using (*-+-commutativeSemiring)
  open import Data.Maybe using (just; nothing)

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

  module Reflection where
    open import Polynomial.Simple.Reflection using (solveOver-macro)
    open import Data.Unit using (⊤)

    macro
      ∀⟨_⟩ : Term → Term → TC ⊤
      ∀⟨ n ⟩ = solveOver-macro n (quote ring)

module Int where
  open import Data.Nat using (zero)
  open import Data.Integer using (+_)
  open import Data.Integer.Properties using(+-*-commutativeRing)
  open import Data.Maybe using (just; nothing)
  open import Relation.Binary.PropositionalEquality using (refl)

  ring : AlmostCommutativeRing 0ℓ 0ℓ
  ring =
    fromCommutativeRing
      +-*-commutativeRing
      λ { (+ zero) → just refl; _ → nothing }

  module Reflection where
    open import Polynomial.Simple.Reflection using (solveOver-macro)
    open import Data.Unit using (⊤)

    macro
      ∀⟨_⟩ : Term → Term → TC ⊤
      ∀⟨ n ⟩ = solveOver-macro n (quote ring)

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
{-# OPTIONS --safe #-}
module Issue2487.b where

-- trying to import a cubical, non-safe module
open import Issue2487.c

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Construct.Vector
  {k ℓ} (K : Field k ℓ)
  where

open import Level using (_⊔_)
open import Data.Product using (_×_; _,_)
open import Data.Vec public hiding (sum)
import Data.Vec.Properties as VP
import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
open import Data.Nat hiding (_⊔_) renaming (_+_ to _+ℕ_)
open import Data.Fin using (Fin)

open import Relation.Binary
open import Algebra.Linear.Core
open import Algebra.FunctionProperties

open import Relation.Binary.PropositionalEquality as P
  using (_≡_; subst; subst-subst-sym)
  renaming
  ( refl  to ≡-refl
  ; sym   to ≡-sym
  ; trans to ≡-trans
  )

open import Algebra.Structures.Field.Utils K
import Algebra.Linear.Structures.VectorSpace as VS

open VS.VectorSpaceField K

open import Data.Nat.Properties
  using
    ( ≤-refl
    ; ≤-reflexive
    ; ≤-antisym
    ; n∸n≡0
    ; m+[n∸m]≡n
    ; m≤m+n
    ; suc-injective
    )
  renaming
    ( +-identityˡ to +ℕ-identityˡ
    ; +-identityʳ to +ℕ-identityʳ
    )

private
  V : ℕ -> Set k
  V = Vec K'

splitAt' : ∀ {n} (i : ℕ) (j : ℕ) -> i +ℕ j ≡ n -> V n → V i × V j
splitAt' {0} 0 0 r [] = ([] , [])
splitAt' {suc n} 0 (suc j) r u = ([] , subst V (≡-sym r) u)
splitAt' {suc n} (suc i) j r (x ∷ xs) =
  let (xs₁ , xs₂) = splitAt' {n} i j (suc-injective r) xs
  in (x ∷ xs₁ , xs₂)

open PW public
  using ()
  renaming
    ( _∷_    to ≈-cons
    ; []     to ≈-null
    ; head   to ≈-head
    ; tail   to ≈-tail
    ; uncons to ≈-uncons
    ; lookup to ≈-lookup
    ; map      to ≈-map
    )

_≈ʰ_ : ∀ {m n} (xs : Vec K' m) (ys : Vec K' n) → Set (k ⊔ ℓ)
_≈ʰ_ = PW.Pointwise _≈ᵏ_

_≈_ : ∀ {n} (xs : Vec K' n) (ys : Vec K' n) → Set (k ⊔ ℓ)
_≈_ = _≈ʰ_

≈-isEquiv : ∀ {n} -> IsEquivalence (_≈_ {n})
≈-isEquiv {n} = PW.isEquivalence ≈ᵏ-isEquiv n

setoid : ℕ -> Setoid k (k ⊔ ℓ)
setoid n = record { isEquivalence = ≈-isEquiv {n} }

module _ {n} where
  open IsEquivalence (≈-isEquiv {n}) public
    using ()
    renaming
      ( refl  to ≈-refl
      ; sym   to ≈-sym
      ; trans to ≈-trans
      ; reflexive to ≈-reflexive
      )

0# : ∀ {n} → V n
0# {0}     = []
0# {suc n} = 0ᵏ ∷ 0# {n}

-_ : ∀ {n} → V n → V n
-_ = map (-ᵏ_)

infixr 25 _+_
_+_ : ∀ {n} → Op₂ (V n)
_+_ = zipWith _+ᵏ_

infixr 35 _∙_
_∙_ : ∀ {n} → K' → V n → V n
_∙_ k = map (k *ᵏ_)

{-
module HeterogeneousEquivalence where
  import Relation.Binary.Indexed.Heterogeneous as IH

  data _≈ʰ_ : IH.IRel V (k ⊔ ℓ) where
    ≈ʰ-null : ∀ {n p} {u : V n} {v : V p} -> n ≡ 0 -> p ≡ 0 -> u ≈ʰ v
    ≈ʰ-cons : ∀ {n p} {x y : K'} {u : V n} {v : V p} -> n ≡ p -> x ≈ᵏ y -> u ≈ʰ v -> (x ∷ u) ≈ʰ (y ∷ v)

  pattern ≈ʰ-zero = ≈ʰ-null ≡-refl ≡-refl

  ≈ʰ-refl : IH.Reflexive V _≈ʰ_
  ≈ʰ-refl {0} {[]} = ≈ʰ-zero
  ≈ʰ-refl {suc n} {x ∷ xs} = ≈ʰ-cons (≡-refl) ≈ᵏ-refl (≈ʰ-refl {n} {xs})

  ≈ʰ-sym : IH.Symmetric V _≈ʰ_
  ≈ʰ-sym {0} ≈ʰ-zero = ≈ʰ-zero
  ≈ʰ-sym {suc n} (≈ʰ-cons rn r rs) = ≈ʰ-cons (≡-sym rn) (≈ᵏ-sym r) (≈ʰ-sym rs)

  ≈ʰ-trans : IH.Transitive V _≈ʰ_
  ≈ʰ-trans (≈ʰ-null rn rp) (≈ʰ-null rn' rp') = ≈ʰ-null rn rp'
  ≈ʰ-trans (≈ʰ-cons rn r rs) (≈ʰ-cons rn' r' rs') = ≈ʰ-cons (≡-trans rn rn') (≈ᵏ-trans r r') (≈ʰ-trans rs rs')

  ≈ʰ-isEquiv : IH.IsIndexedEquivalence V _≈ʰ_
  ≈ʰ-isEquiv = record
    { refl  = ≈ʰ-refl
    ; sym   = ≈ʰ-sym
    ; trans = ≈ʰ-trans
    }

  ≈-to-≈ʰ : ∀ {n} {u v : V n} -> u ≈ v -> u ≈ʰ v
  ≈-to-≈ʰ {0} ≈-null = ≈ʰ-zero
  ≈-to-≈ʰ {suc n} (≈-cons r rs) = ≈ʰ-cons ≡-refl r (≈-to-≈ʰ rs)

  ≈ʰ-to-≈ : ∀ {n} {u v : V n} -> u ≈ʰ v -> u ≈ v
  ≈ʰ-to-≈ {0} {[]} {[]} ≈ʰ-zero = ≈-null
  ≈ʰ-to-≈ {suc n} (≈ʰ-cons _ r rs) = ≈-cons r (≈ʰ-to-≈ rs)

  ≈ʰ-tail : ∀ {n p} {x y : K'} {u : V n} {v : V p} -> (x ∷ u) ≈ʰ (x ∷ v) -> u ≈ʰ v
  ≈ʰ-tail (≈ʰ-cons _ _ r) = r

  indexedSetoid : IH.IndexedSetoid ℕ k (ℓ ⊔ k)
  indexedSetoid = record
    { Carrier       = V
    ; _≈_           = _≈ʰ_
    ; isEquivalence = ≈ʰ-isEquiv
    }
setoid : ℕ -> Setoid k (k ⊔ ℓ)
setoid n = record
  { Carrier       = V n
  ; _≈_           = _≈_
  ; isEquivalence = ≈-isEquiv
  }
-}

++-identityˡ : ∀ {n} (u : V n) -> ([] ++ u) ≈ u
++-identityˡ _ = ≈-refl

++-cong : ∀ {n p} {u₁ v₁ : V n} {u₂ v₂ : V p}
        -> u₁ ≈ v₁ -> u₂ ≈ v₂ -> (u₁ ++ u₂) ≈ (v₁ ++ v₂)
++-cong  ≈-null        r₂ = r₂
++-cong (≈-cons r₁ rs₁) r₂ = ≈-cons r₁ (++-cong rs₁ r₂)

++-split : ∀ {n p} {u₁ v₁ : V n} {u₂ v₂ : V p}
        ->  (u₁ ++ u₂) ≈ (v₁ ++ v₂) -> (u₁ ≈ v₁ × u₂ ≈ v₂)
++-split {0} {p} {[]} {[]} r = ≈-null , r
++-split {suc n} {p} {x ∷ xs} {y ∷ ys} (≈-cons r rs) =
  let (r₁ , r₂) = ++-split {n} {p} rs
  in (≈-cons r r₁) , r₂

0++0≈0 : ∀ {n p} -> (0# {n} ++ 0# {p}) ≈ 0# {n +ℕ p}
0++0≈0 {zero} = ++-identityˡ 0#
0++0≈0 {suc n} = ≈-cons ≈ᵏ-refl (0++0≈0 {n})

{-
open HeterogeneousEquivalence

++-identityʳ-≈ʰ : ∀ {n} (u : V n) -> (u ++ []) ≈ʰ u
++-identityʳ-≈ʰ [] = ≈ʰ-refl
++-identityʳ-≈ʰ {suc n} (x ∷ xs) = ≈ʰ-cons (+ℕ-identityʳ n) ≈ᵏ-refl (++-identityʳ-≈ʰ {n} xs)

++-cong-≈ʰ : ∀ {n p} {u₁ v₁ : V n} {u₂ v₂ : V p}
           -> u₁ ≈ʰ v₁ -> u₂ ≈ʰ v₂ -> (u₁ ++ u₂) ≈ʰ (v₁ ++ v₂)
++-cong-≈ʰ r₁ r₂ = ≈-to-≈ʰ (++-cong (≈ʰ-to-≈ r₁) (≈ʰ-to-≈ r₂))

splitAt-identityˡ : ∀ {n} (u : V n) -> let (x₁ , x₂) = splitAt 0 z≤n u in (x₁ ≈ʰ []) × (x₂ ≈ʰ u)
splitAt-identityˡ {0}_ = ≈ʰ-zero , ≈ʰ-zero
splitAt-identityˡ {suc n} _ = ≈ʰ-zero , ≈ʰ-refl

splitAt-identityʳ : ∀ {n} (u : V n) -> let (x₁ , x₂) = splitAt n ≤-refl u in (x₁ ≈ʰ u) × (x₂ ≈ʰ [])
splitAt-identityʳ {0} [] = ≈ʰ-refl , ≈ʰ-refl
splitAt-identityʳ {suc n} (x ∷ xs) = ≈ʰ-cons ≡-refl ≈ᵏ-refl (proj₁ (splitAt-identityʳ xs))
                                   , ≈ʰ-null (n∸n≡0 (suc n)) ≡-refl

++-splitAt : ∀ {n} (k : ℕ) (r : k ≤ n) (u : V n) -> let (x₁ , x₂, _) = splitAt n u in (x₁ ++ x₂) ≡ u
++-splitAt {0} 0 r u = ≈ʰ-null (m+[n∸m]≡n r) ≡-refl
++-splitAt {suc n} 0 r (x ∷ xs) = ≈ʰ-refl
++-splitAt {suc n} (suc k) sk≤sn (x ∷ xs) =
  let k≤n = ≤-pred sk≤sn
  in ≈ʰ-cons (m+[n∸m]≡n k≤n) ≈ᵏ-refl (++-splitAt k k≤n xs)

splitAt-++ : ∀ {n p} (u : Vec n) (v : Vec p) ->
  let (u' , v') = splitAt n (m≤m+n n p) (u ++ v) in (u ≈ʰ u') × (v ≈ʰ v')
splitAt-++ {0} {0} [] [] =  ≈ʰ-zero , ≈ʰ-zero
splitAt-++ {0} {suc p} [] (y ∷ ys) = ≈ʰ-zero , ≈ʰ-refl
splitAt-++ {suc n} {0} (x ∷ xs) [] =
  let (rxs , rv) = splitAt-++ xs []
  in ≈ʰ-cons ≡-refl ≈ᵏ-refl rxs , rv
splitAt-++ {suc n} {suc p} (x ∷ xs) (y ∷ ys) =
  let (u' , v') = splitAt (suc n) (m≤m+n (suc n) (suc p)) (x ∷ xs ++ y ∷ ys)
      (ru , rys) = splitAt-++ {suc n} {p} (x ∷ xs) ys
      (rxs , rv) = splitAt-++ {n} {suc p} xs (y ∷ ys)
  in ≈ʰ-cons ≡-refl ≈ᵏ-refl rxs , rv

++-splitAt' : ∀ {n p} (u : Vec (n +ℕ p)) -> let (x₁ , x₂) = splitAt' n p ≡-refl u in x₁ ++ x₂ ≈ u
++-splitAt' {0} [] = ≈-null
++-splitAt' {0} (x ∷ xs) = ≈-refl
++-splitAt' {suc n} (x ∷ xs) = ≈-cons ≈ᵏ-refl (++-splitAt' {n} xs)

splitAt'-++ : ∀ {n p} (u : Vec n) (v : Vec p) ->
  let (u' , v') = splitAt' n p ≡-refl (u ++ v) in (u ≈ u') × (v ≈ v')
splitAt'-++ {0} {0} [] [] =  ≈-null , ≈-null
splitAt'-++ {0} {suc p} [] (y ∷ ys) = ≈-null , ≈-refl
splitAt'-++ {suc n} {0} (x ∷ xs) [] =
  let (rxs , rv) = splitAt'-++ xs []
  in ≈-cons ≈ᵏ-refl rxs , rv
splitAt'-++ {suc n} {suc p} (x ∷ xs) (y ∷ ys) =
  let (u' , v') = splitAt' (suc n) (suc p) ≡-refl (x ∷ xs ++ y ∷ ys)
      (ru , rys) = splitAt'-++ {suc n} {p} (x ∷ xs) ys
      (rxs , rv) = splitAt'-++ {n} {suc p} xs (y ∷ ys)
  in ≈-cons ≈ᵏ-refl rxs , rv
-}

+-cong : ∀ {n} → Congruent₂ (_≈_ {n}) _+_
+-cong ≈-null ≈-null = ≈-null
+-cong (≈-cons r₁ rs₁) (≈-cons r₂ rs₂) = ≈-cons (+ᵏ-cong r₁ r₂) (+-cong rs₁ rs₂)

+-assoc : ∀ {n} → Associative (_≈_ {n}) _+_
+-assoc [] [] [] = ≈-null
+-assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) = ≈-cons (+ᵏ-assoc x y z) (+-assoc xs ys zs)

+-identityˡ : ∀ {n} → LeftIdentity (_≈_ {n}) 0# _+_
+-identityˡ [] = ≈-null
+-identityˡ (x ∷ xs) = ≈-cons (+ᵏ-identityˡ x) (+-identityˡ xs)

+-identityʳ : ∀ {n} → RightIdentity (_≈_ {n}) 0# _+_
+-identityʳ [] = ≈-null
+-identityʳ (x ∷ xs) = ≈-cons (+ᵏ-identityʳ x) (+-identityʳ xs)

+-identity : ∀ {n} → Identity (_≈_ {n}) 0# _+_
+-identity = +-identityˡ , +-identityʳ

+-comm : ∀ {n} -> Commutative (_≈_ {n}) _+_
+-comm [] [] = ≈-null
+-comm (x ∷ xs) (y ∷ ys) = ≈-cons (+ᵏ-comm x y) (+-comm xs ys)

*ᵏ-∙-compat : ∀ {n} (a b : K') (u : V n) -> ((a *ᵏ b) ∙ u) ≈ (a ∙ (b ∙ u))
*ᵏ-∙-compat a b [] = ≈-null
*ᵏ-∙-compat a b (x ∷ xs) = ≈-cons (*ᵏ-assoc a b x) (*ᵏ-∙-compat a b xs)

∙-+-distrib : ∀ {n} (a : K') (u v : V n) -> (a ∙ (u + v)) ≈ ((a ∙ u) + (a ∙ v))
∙-+-distrib a [] [] = ≈-null
∙-+-distrib a (x ∷ xs) (y ∷ ys) = ≈-cons (*ᵏ-+ᵏ-distribˡ a x y) (∙-+-distrib a xs ys)

∙-+ᵏ-distrib : ∀ {n} (a b : K') (u : V n) -> ((a +ᵏ b) ∙ u) ≈ ((a ∙ u) + (b ∙ u))
∙-+ᵏ-distrib a b [] = ≈-null
∙-+ᵏ-distrib a b (x ∷ u) = ≈-cons (*ᵏ-+ᵏ-distribʳ x a b) (∙-+ᵏ-distrib a b u)

∙-cong : ∀ {n} {a b : K'} {u v : V n} → a ≈ᵏ b -> u ≈ v -> (a ∙ u) ≈ (b ∙ v)
∙-cong rᵏ ≈-null = ≈-null
∙-cong rᵏ (≈-cons r rs) = ≈-cons (*ᵏ-cong rᵏ r) (∙-cong rᵏ rs)

∙-identity : ∀ {n} (x : V n) → (1ᵏ ∙ x) ≈ x
∙-identity [] = ≈-null
∙-identity (x ∷ xs) = ≈-cons (*ᵏ-identityˡ x) (∙-identity xs)

∙-absorbˡ : ∀ {n} (x : V n) → (0ᵏ ∙ x) ≈ 0#
∙-absorbˡ [] = ≈-null
∙-absorbˡ (x ∷ xs) = ≈-cons (*ᵏ-zeroˡ x) (∙-absorbˡ xs)

-‿inverseˡ : ∀ {n} → LeftInverse  (_≈_ {n}) 0# -_ _+_
-‿inverseˡ [] = ≈-null
-‿inverseˡ (x ∷ xs) = ≈-cons (-ᵏ‿inverseˡ x) (-‿inverseˡ xs)

-‿inverseʳ : ∀ {n} → RightInverse (_≈_ {n}) 0# -_ _+_
-‿inverseʳ [] = ≈-null
-‿inverseʳ (x ∷ xs) = ≈-cons (-ᵏ‿inverseʳ x) (-‿inverseʳ xs)

-‿inverse : ∀ {n} → Inverse (_≈_ {n}) 0# -_ _+_
-‿inverse = -‿inverseˡ , -‿inverseʳ

-‿cong : ∀ {n} -> Congruent₁ (_≈_ {n}) -_
-‿cong ≈-null = ≈-null
-‿cong (≈-cons r rs) = ≈-cons (-ᵏ‿cong r) (-‿cong rs)

+-++-distrib : ∀ {n p}
                 (u₁ : V n) (u₂ : V p)
                 (v₁ : V n) (v₂ : V p)
             -> ((u₁ ++ u₂) + (v₁ ++ v₂)) ≈ ((u₁ + v₁) ++ (u₂ + v₂))
+-++-distrib [] [] [] [] = ≈-null
+-++-distrib (x₁ ∷ xs₁) [] (y₁ ∷ ys₁) [] = ++-cong ≈-refl (+-++-distrib xs₁ [] ys₁ [])
+-++-distrib {0} {suc p} [] (x₂ ∷ xs₂) [] (y₂ ∷ ys₂) = ++-identityˡ ((x₂ +ᵏ y₂) ∷ (xs₂ + ys₂))
+-++-distrib (x₁ ∷ xs₁) u₂ (y₁ ∷ ys₁) v₂ =
  ≈-cons ≈ᵏ-refl (++-cong ≈-refl (+-++-distrib xs₁ u₂ ys₁ v₂))

∙-++-distrib : ∀ {n p} (a : K') (u : V n) (v : V p) -> (a ∙ (u ++ v)) ≈ ((a ∙ u) ++ (a ∙ v))
∙-++-distrib a [] v = ≈-refl
∙-++-distrib a (x ∷ xs) v = ≈-cons ≈ᵏ-refl (∙-++-distrib a xs v)

sum : ∀ {n} -> V n -> K'
sum = foldr _ _+ᵏ_ 0ᵏ

sum-tab : ∀ {n} -> (Fin n -> K') -> K'
sum-tab f = sum (tabulate f)

sum-cong : ∀ {n} {u v : V n} -> u ≈ v -> sum u ≈ᵏ sum v
sum-cong {0} PW.[] = ≈ᵏ-refl
sum-cong {suc n} (r PW.∷ rs) = +ᵏ-cong r (sum-cong {n} rs)

tabulate-cong-≡ : ∀ {n} {f g : Fin n -> K'} -> (∀ i -> f i ≡ g i) -> tabulate f ≡ tabulate g
tabulate-cong-≡ = VP.tabulate-cong

tabulate-cong : ∀ {n} {f g : Fin n -> K'} -> (∀ i -> f i ≈ᵏ g i) -> tabulate f ≈ tabulate g
tabulate-cong {0} r = PW.[]
tabulate-cong {suc n} r = r Fin.zero PW.∷ tabulate-cong (λ i → r (Fin.suc i))

sum-tab-cong : ∀ {n} {f g : Fin n -> K'} -> (∀ i -> f i ≈ᵏ g i) -> sum-tab f ≈ᵏ sum-tab g
sum-tab-cong r = sum-cong (tabulate-cong r)

*ᵏ-sum-tab-distribʳ : ∀ {n} (a : K') (f : Fin n -> K')
                    → (sum-tab f *ᵏ a) ≈ᵏ sum-tab (λ k -> f k *ᵏ a)
*ᵏ-sum-tab-distribʳ {0} a f = *ᵏ-zeroˡ a
*ᵏ-sum-tab-distribʳ {suc n} a f =
  begin
    sum-tab f *ᵏ a
  ≈⟨ *ᵏ-+ᵏ-distribʳ a (f Fin.zero) (sum-tab (λ k -> f (Fin.suc k))) ⟩
     (f Fin.zero *ᵏ a) +ᵏ (sum-tab (λ k -> f (Fin.suc k)) *ᵏ a)
  ≈⟨ +ᵏ-cong ≈ᵏ-refl  (*ᵏ-sum-tab-distribʳ a (λ k -> f (Fin.suc k))) ⟩
     sum-tab (λ k -> f k *ᵏ a)
  ∎
  where open import Relation.Binary.EqReasoning (Field.setoid K)

sum-assoc : ∀ {n} (f g : Fin n -> K')
          -> (sum-tab f +ᵏ sum-tab g) ≈ᵏ sum-tab (λ k -> f k +ᵏ g k)
sum-assoc {0} f g = +ᵏ-identityˡ 0ᵏ
sum-assoc {suc n} f g =
  begin
    sum-tab f +ᵏ sum-tab g
  ≡⟨⟩
    (f Fin.zero +ᵏ sum-tab {n} (λ k -> f (Fin.suc k))) +ᵏ (g Fin.zero +ᵏ sum-tab {n} (λ k -> g (Fin.suc k)))
  ≈⟨ +ᵏ-assoc (f Fin.zero) (sum-tab {n} (λ k -> f (Fin.suc k))) (g Fin.zero +ᵏ sum-tab {n} (λ k -> g (Fin.suc k))) ⟩
     f Fin.zero +ᵏ (sum-tab (λ k → f (Fin.suc k)) +ᵏ (g Fin.zero +ᵏ sum-tab (λ k → g (Fin.suc k))))
  ≈⟨ +ᵏ-cong ≈ᵏ-refl (+ᵏ-comm (sum-tab (λ k -> f (Fin.suc k))) ((g Fin.zero +ᵏ sum-tab (λ k → g (Fin.suc k))))) ⟩
     f Fin.zero +ᵏ ((g Fin.zero +ᵏ sum-tab (λ k → g (Fin.suc k))) +ᵏ sum-tab (λ k → f (Fin.suc k)))
  ≈⟨ +ᵏ-cong ≈ᵏ-refl (+ᵏ-assoc (g Fin.zero) (sum-tab (λ k -> g (Fin.suc k))) (sum-tab (λ k -> f (Fin.suc k)))) ⟩
     f Fin.zero +ᵏ (g Fin.zero +ᵏ (sum-tab (λ k → g (Fin.suc k)) +ᵏ sum-tab (λ k → f (Fin.suc k))))
  ≈⟨ ≈ᵏ-sym (+ᵏ-assoc (f Fin.zero) (g Fin.zero) (sum-tab (λ k → g (Fin.suc k)) +ᵏ sum-tab (λ k → f (Fin.suc k)))) ⟩
     (f Fin.zero +ᵏ g Fin.zero) +ᵏ (sum-tab (λ k → g (Fin.suc k)) +ᵏ sum-tab (λ k → f (Fin.suc k)))
  ≈⟨ +ᵏ-cong ≈ᵏ-refl (+ᵏ-comm (sum-tab λ k -> g (Fin.suc k)) (sum-tab λ k -> f (Fin.suc k))) ⟩
     (f Fin.zero +ᵏ g Fin.zero) +ᵏ (sum-tab (λ k → f (Fin.suc k)) +ᵏ sum-tab (λ k → g (Fin.suc k)))
  ≈⟨ +ᵏ-cong ≈ᵏ-refl (sum-assoc {n} (λ k -> f (Fin.suc k)) (λ k -> g (Fin.suc k))) ⟩
     sum-tab (λ k -> f k +ᵏ g k)
  ∎
  where open import Relation.Binary.EqReasoning (Field.setoid K)

sum-tab-0ᵏ : ∀ {n} -> sum-tab {n} (λ k -> 0ᵏ) ≈ᵏ 0ᵏ
sum-tab-0ᵏ {0} = ≈ᵏ-refl
sum-tab-0ᵏ {suc n} = ≈ᵏ-trans (+ᵏ-identityˡ (sum-tab {n} λ k -> 0ᵏ)) (sum-tab-0ᵏ {n})

sum-tab-swap : ∀ {n p} (f : Fin n -> Fin p -> K') (g : Fin n -> K')
             -> sum-tab (λ k′ -> sum-tab λ k -> f k k′ *ᵏ g k)
             ≈ᵏ sum-tab (λ k -> sum-tab λ k′ -> f k k′ *ᵏ g k)
sum-tab-swap {n} {0} f g = ≈ᵏ-sym (sum-tab-0ᵏ {n})
sum-tab-swap {n} {suc p} f g =
  begin
    sum-tab (λ k′ -> sum-tab λ k -> f k k′ *ᵏ g k)
  ≡⟨⟩
    (sum-tab λ k -> f k Fin.zero *ᵏ g k) +ᵏ (sum-tab λ k′ -> sum-tab λ k -> f k (Fin.suc k′) *ᵏ g k)
  ≈⟨ +ᵏ-cong ≈ᵏ-refl (sum-tab-swap {n} {p} (λ k k′ -> f k (Fin.suc k′)) g) ⟩
     sum-tab (λ k → f k Fin.zero *ᵏ g k) +ᵏ sum-tab (λ k → sum-tab (λ k′ → f k (Fin.suc k′) *ᵏ g k))
  ≈⟨ +ᵏ-cong ≈ᵏ-refl (sum-tab-cong λ k -> ≈ᵏ-sym (*ᵏ-sum-tab-distribʳ {p} (g k) λ k′ -> f k (Fin.suc k′))) ⟩
     sum-tab (λ k → f k Fin.zero *ᵏ g k) +ᵏ sum-tab (λ k → sum-tab (λ k′ → f k (Fin.suc k′)) *ᵏ g k)
  ≈⟨ sum-assoc (λ k -> f k Fin.zero *ᵏ g k) (λ k -> sum-tab (λ k′ -> f k (Fin.suc k′)) *ᵏ g k) ⟩
     sum-tab (λ k -> (f k Fin.zero *ᵏ g k) +ᵏ (sum-tab (λ k′ -> f k (Fin.suc k′)) *ᵏ g k))
  ≈⟨ sum-tab-cong (λ k -> ≈ᵏ-sym (*ᵏ-+ᵏ-distribʳ (g k) (f k Fin.zero) (sum-tab λ k′ -> f k (Fin.suc k′)))) ⟩
     sum-tab (λ k -> sum-tab (λ k′ -> f k k′) *ᵏ g k)
  ≈⟨ sum-tab-cong (λ k -> *ᵏ-sum-tab-distribʳ {suc p} (g k) (λ k′ -> f k k′)) ⟩
     sum-tab (λ k -> sum-tab λ k′ -> f k k′ *ᵏ g k)
  ∎
  where open import Relation.Binary.EqReasoning (Field.setoid K)

sum-tab-δ : ∀ {n} (f : Fin n -> K') (i : Fin n) -> sum-tab (λ k -> δ i k *ᵏ f k) ≈ᵏ f i
sum-tab-δ {suc n} f i@Fin.zero =
  begin
    sum-tab (λ k -> δ i k *ᵏ f k)
  ≡⟨⟩
    (δ i i *ᵏ f i) +ᵏ sum-tab (λ k -> δ i (Fin.suc k) *ᵏ f (Fin.suc k))
  ≈⟨ +ᵏ-cong (*ᵏ-identityˡ (f i))
     (sum-tab-cong (λ k -> ≈ᵏ-trans (*ᵏ-cong (δ-cancelˡ {n} k) ≈ᵏ-refl) (*ᵏ-zeroˡ (f (Fin.suc k))))) ⟩
    f i +ᵏ sum-tab {n} (λ k -> 0ᵏ)
  ≈⟨ ≈ᵏ-trans (+ᵏ-cong ≈ᵏ-refl (sum-tab-0ᵏ {n})) (+ᵏ-identityʳ (f i)) ⟩
    f i
  ∎
  where open import Relation.Binary.EqReasoning (Field.setoid K)
sum-tab-δ {suc n} f (Fin.suc i) =
  begin
    sum-tab (λ k -> δ (Fin.suc i) k *ᵏ f k)
  ≡⟨⟩
    (δ (Fin.suc i) (Fin.zero {suc n}) *ᵏ f Fin.zero) +ᵏ sum-tab (λ k -> δ (Fin.suc i) (Fin.suc k) *ᵏ f (Fin.suc k))
  ≈⟨ +ᵏ-cong (≈ᵏ-trans (*ᵏ-cong (δ-cancelʳ {p = suc n} (Fin.suc i)) ≈ᵏ-refl) (*ᵏ-zeroˡ (f Fin.zero))) ≈ᵏ-refl ⟩
    0ᵏ +ᵏ sum-tab (λ k → δ (Fin.suc i) (Fin.suc k) *ᵏ f (Fin.suc k))
  ≈⟨ +ᵏ-identityˡ (sum-tab λ k -> δ (Fin.suc i) (Fin.suc k) *ᵏ f (Fin.suc k)) ⟩
    sum-tab (λ k → δ (Fin.suc i) (Fin.suc k) *ᵏ f (Fin.suc k))
  ≈⟨ sum-tab-δ (λ k -> f (Fin.suc k)) i ⟩
    f (Fin.suc i)
  ∎
  where open import Relation.Binary.EqReasoning (Field.setoid K)

module _ {n} where
  open import Algebra.Structures (_≈_ {n})
  open import Algebra.Linear.Structures.Bundles

  isMagma : IsMagma _+_
  isMagma = record
    { isEquivalence = ≈-isEquiv
    ; ∙-cong        = +-cong
    }

  isSemigroup : IsSemigroup _+_
  isSemigroup = record
    { isMagma = isMagma
    ; assoc   = +-assoc
    }

  isMonoid : IsMonoid _+_ 0#
  isMonoid = record
    { isSemigroup = isSemigroup
    ; identity    = +-identity
    }

  isGroup : IsGroup _+_ 0# -_
  isGroup = record
    { isMonoid = isMonoid
    ; inverse  = -‿inverse
    ; ⁻¹-cong   = -‿cong
    }

  isAbelianGroup : IsAbelianGroup _+_ 0# -_
  isAbelianGroup = record
    { isGroup = isGroup
    ; comm    = +-comm
    }

  open VS K

  isVectorSpace : VS.IsVectorSpace K (_≈_ {n}) _+_ _∙_ -_ 0#
  isVectorSpace = record
    { isAbelianGroup  = isAbelianGroup
    ; *ᵏ-∙-compat     = *ᵏ-∙-compat
    ; ∙-+-distrib     = ∙-+-distrib
    ; ∙-+ᵏ-distrib    = ∙-+ᵏ-distrib
    ; ∙-cong          = ∙-cong
    ; ∙-identity      = ∙-identity
    ; ∙-absorbˡ        = ∙-absorbˡ
    }

  vectorSpace : VectorSpace K k (k ⊔ ℓ)
  vectorSpace = record { isVectorSpace = isVectorSpace }

  open import Algebra.Linear.Morphism.VectorSpace K

  open import Algebra.Linear.Morphism.Bundles K

  open import Function

  embed : LinearIsomorphism vectorSpace vectorSpace
  embed = record
    { ⟦_⟧ = id
    ; isLinearIsomorphism = record
        { isLinearMonomorphism = record
            { isLinearMap = record
                { isAbelianGroupMorphism = record
                    { gp-homo = record
                        { mn-homo = record
                          { sm-homo = record
                              { ⟦⟧-cong = id
                              ; ∙-homo = λ x y → ≈-refl
                              }
                          ; ε-homo = ≈-refl
                          }
                        }
                    }
                ; ∙-homo = λ c u → ≈-refl
                }
            ; injective = id
            }
        ; surjective = λ y → y , ≈-refl
        }
    }

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


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

open import lib.Base

module test.succeed.Test1 where

module _ where

  private
    data #I : Type₀ where
      #zero : #I
      #one : #I

  I : Type₀
  I = #I

  zero : I
  zero = #zero

  one : I
  one = #one

  postulate
    seg : zero == one

absurd : zero ≠ one
absurd ()

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module ForallForParameters
         (F : Set -> Set -> Set) X {Y} (Z : F X Y) where

data List A : Set where
  [] : List A
  _::_ : A -> List A -> List A

module M A {B} (C : F A B) where

  data D : Set -> Set where
    d : A -> D A

  data P A : D A -> Set where

  data Q {A} X : P A X -> Set where

module N I J K = M I {J} K
open module O I J K = N I J K

record R {I J} (K : F I J) : Set where

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of homogeneous binary relations
------------------------------------------------------------------------

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

module Relation.Binary where

------------------------------------------------------------------------
-- Re-export various components of the binary relation hierarchy

open import Relation.Binary.Core public
open import Relation.Binary.Definitions public
open import Relation.Binary.Structures public
open import Relation.Binary.Bundles public


text:
-- 2012-03-08 Andreas
module NoTerminationCheck2 where

{-# NON_TERMINATING #-}
data D : Set where
  lam : (D -> D) -> D

-- error: works only for function definitions


text:
module ModusPonens where

modusPonens : ∀ {P Q : Set} → (P → Q) → P → Q
modusPonens x = x

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
module Data.Var where

open import Data.List using (List; []; _∷_; map)
open import Data.List.Relation.Unary.All using (All; []; _∷_)

open import Function using (const; _∘_)

open import Level using (Level; 0ℓ)

open import Relation.Unary using (IUniversal; _⇒_; _⊢_)

-- ------------------------------------------------------------------------
-- Vars and Contexts

private
  variable
    a b : Level

_-Scoped[_] : Set a → (b : Level) → Set _
I -Scoped[ b ] = I → List I → Set b

private
  variable
    I J : Set a
    i j : I
    Γ : List I

data Var : I -Scoped[ 0ℓ ] where
  zero : ∀[ (i ∷_) ⊢ Var i ]
  suc : ∀[ Var i ⇒ (j ∷_) ⊢ Var i ]

get : {P : I → Set b} → ∀[ Var i ⇒ All P ⇒ const (P i) ]
get zero (p  ∷ _) = p
get (suc v) (_  ∷ ps) = get v ps

_<$>_ : (f : I → J) → ∀[ Var i ⇒ map f ⊢ Var (f i) ]
f <$> zero = zero
f <$> suc v = suc (f <$> v)

tabulate : {P : I → Set b} → (∀ {i} → Var i Γ → P i) → All P Γ
tabulate {Γ = []} f = []
tabulate {Γ = i ∷ Γ} f = f zero ∷ tabulate (f ∘ suc)

max_stars_repo_name: johnyob/agda-desc

max_issues_repo_name: johnyob/agda-desc

max_forks_repo_name: johnyob/agda-desc


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

module Data.Fin where

open import Data.Fin.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- notes-05-friday.agda

open import mylib

-- Π-types = dependent function types
Π : (A : Set)(B : A → Set) → Set
Π A B = (x : A) → B x

syntax Π A (λ x → P)  = Π[ x ∈ A ] P

-- Σ-types = dependent pair type

record Σ(A : Set)(B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ

syntax Σ A (λ x → P)  = Σ[ x ∈ A ] P

List' : Set → Set
List' A = Σ[ n ∈ ℕ ] Vec A n

List'' : Set → Set -- ex: show that this is isomorphic to lists
List'' A = Σ[ n ∈ ℕ ] Fin n → A

{-
  Container representation of lists.
  Set of shapes S = ℕ.
  Family of positions P : ℕ → Set, P = Fin.
  All strictly positive types can be represented as containers ( ~ polynomial
  functors) !
-}

{-
A → B = Π[ _ ∈ A ] B
A × B = Σ[ _ ∈ A ] B
-}

_⊎'_ : Set → Set → Set
A ⊎' B = Σ[ b ∈ Bool ] F b
         where F : Bool → Set
               F true = A
               F false = B

_×'_ : Set → Set → Set -- exercise: show that this equivalent to ⊎
A ×' B = Π[ b ∈ Bool ] F b
         where F : Bool → Set
               F true = A
               F false = B

{-
  "Propositions as types": for predicate logic
  P : A → prop = dependent type
-}

All : (A : Set)(P : A → prop) → prop
All A P = Π[ x ∈ A ] P x

Ex : (A : Set)(P : A → prop) → prop
Ex A P = Σ[ x ∈ A ] P x

syntax All A (λ x → P)  = ∀[ x ∈ A ] P
infix 0 All
syntax Ex A (λ x → P) = ∃[ x ∈ A ] P
infix 0 Ex

variable PP QQ : A → prop

taut : (∀[ x ∈ A ] PP x ⇒ Q) ⇔ (∃[ x ∈ A ] PP x) ⇒ Q
proj₁ taut f (a , pa) = f a pa
proj₂ taut g a pa = g (a , pa)

data _≡_ : A → A → prop where
  refl : {a : A} → a ≡ a

infix 4 _≡_

-- inductive definition of equality: _≡_ is an equivalence relation

sym : (a b : A) → a ≡ b → b ≡ a
sym a .a refl = refl

trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl q = q

cong : {a b : A}(f : A → B) → a ≡ b → f a ≡ f b
cong f refl = refl

{-
  Proving that + is associative

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

assoc : (i j k : ℕ) → (i + j) + k ≡ i + (j + k)
assoc zero j k = refl
assoc (suc i) j k = cong suc (assoc i j k)

-- proof by induction = pattern matching + recursion

ind : (P : ℕ → Set)
    → P 0
    → ((n : ℕ) → P n → P (suc n))
    → (n : ℕ) → P n
ind P z s zero = z
ind P z s (suc n) = s n (ind P z s n)

-- eliminator for ℕ = induction/dependent recursion

{-
data _≡_ : A → A → prop where
  refl : {a : A} → a ≡ a

  What is ind for equality?
-}

ind≡ : (P : (a b : A) → a ≡ b → prop)
       (r : (a : A) → P a a refl)
       → (a b : A)(p : a ≡ b) → P a b p
ind≡ P r a .a refl = r a

-- Ex. derive sym, trans, cong from ind≡ (= J)

uip : (a b : A)(p q : a ≡ b) → p ≡ q
uip = ind≡ (λ a b p → (q : a ≡ b) → p ≡ q) λ a q →
           {!!}
--uip refl refl = refl

{-
  Is uip derivable from J ? Hofmann & Streicher: groupoid model of type theory.
  Restricted version of HoTT (infinity groupoid model of TT); observed: version
  of univalence in this theory. Voevodsky formulated HoTT, which supports full
  univalence.
-}

max_stars_repo_path: Type Theory/notes-05-friday.agda

max_issues_repo_path: Type Theory/notes-05-friday.agda

max_forks_repo_path: Type Theory/notes-05-friday.agda


text:
module PatternSynonymImports2 where

open import PatternSynonyms hiding (test)
open import PatternSynonymImports

myzero' = z
myzero'' = myzero

list2 : List _
list2 = 1 ∷ []

test : ℕ → ℕ
test myzero = 0
test sz     = 1
test (ss x) = x


text:
------------------------------------------------------------------------------
-- Sort a list
------------------------------------------------------------------------------

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

-- This module define the program which sorts a list by converting it
-- into an ordered tree and then back to a list (Burstall 1969,
-- pp. 45-46).

module FOTC.Program.SortList.SortList where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.List
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Tree terms.
postulate
  nil  : D
  tip  : D → D
  node : D → D → D → D

-- The tree type.
data Tree : D → Set where
  tnil  : Tree nil
  ttip  : ∀ {i} → N i → Tree (tip i)
  tnode : ∀ {t₁ i t₂} → Tree t₁ → N i → Tree t₂ → Tree (node t₁ i t₂)
{-# ATP axioms tnil ttip tnode #-}

------------------------------------------------------------------------------
-- Inequalites on lists and trees

-- Note from Burstall (p. 46): "The relation ≤ between lists is only an
-- ordering if nil is excluded, similarly for trees. This is untidy but
-- will not cause trouble."

postulate
  le-ItemList    : D → D → D
  le-ItemList-[] : ∀ item → le-ItemList item [] ≡ true
  le-ItemList-∷  : ∀ item i is →
                   le-ItemList item (i ∷ is) ≡ le item i && le-ItemList item is
{-# ATP axioms le-ItemList-[] le-ItemList-∷ #-}

≤-ItemList : D → D → Set
≤-ItemList item is = le-ItemList item is ≡ true
{-# ATP definition ≤-ItemList #-}

postulate
  le-Lists    : D → D → D
  le-Lists-[] : ∀ is → le-Lists [] is ≡ true
  le-Lists-∷  : ∀ i is js →
                le-Lists (i ∷ is) js ≡ le-ItemList i js && le-Lists is js
{-# ATP axioms le-Lists-[] le-Lists-∷ #-}

≤-Lists : D → D → Set
≤-Lists is js = le-Lists is js ≡ true
{-# ATP definition ≤-Lists #-}

postulate
  le-ItemTree      : D → D → D
  le-ItemTree-nil  : ∀ item → le-ItemTree item nil ≡ true
  le-ItemTree-tip  : ∀ item i → le-ItemTree item (tip i) ≡ le item i
  le-ItemTree-node : ∀ item t₁ i t₂ →
                     le-ItemTree item (node t₁ i t₂) ≡
                     le-ItemTree item t₁ && le-ItemTree item t₂
{-# ATP axioms le-ItemTree-nil le-ItemTree-tip le-ItemTree-node #-}

≤-ItemTree : D → D → Set
≤-ItemTree item t = le-ItemTree item t ≡ true
{-# ATP definition ≤-ItemTree #-}

-- This function is not defined in the paper.
postulate
  le-TreeItem      : D → D → D
  le-TreeItem-nil  : ∀ item → le-TreeItem nil item ≡ true
  le-TreeItem-tip  : ∀ i item → le-TreeItem (tip i) item ≡ le i item
  le-TreeItem-node : ∀ t₁ i t₂ item →
                     le-TreeItem (node t₁ i t₂) item ≡
                     le-TreeItem t₁ item && le-TreeItem t₂ item
{-# ATP axioms le-TreeItem-nil le-TreeItem-tip le-TreeItem-node #-}

≤-TreeItem : D → D → Set
≤-TreeItem t item = le-TreeItem t item ≡ true
{-# ATP definition ≤-TreeItem #-}

------------------------------------------------------------------------------
-- Auxiliary functions

postulate
  -- The foldr function with the last two args flipped.
  lit    : D → D → D → D
  lit-[] : ∀ f n → lit f [] n            ≡ n
  lit-∷  : ∀ f d ds n → lit f (d ∷ ds) n ≡ f · d · (lit f ds n)
{-# ATP axioms lit-[] lit-∷ #-}

------------------------------------------------------------------------------
-- Ordering functions and predicates on lists and trees

postulate
  ordList    : D → D
  ordList-[] : ordList []                ≡ true
  ordList-∷  : ∀ i is → ordList (i ∷ is) ≡ le-ItemList i is && ordList is
{-# ATP axioms ordList-[] ordList-∷ #-}

OrdList : D → Set
OrdList is = ordList is ≡ true
{-# ATP definition OrdList #-}

postulate
  ordTree      : D → D
  ordTree-nil  : ordTree nil ≡ true
  ordTree-tip  : ∀ i → ordTree (tip i) ≡ true
  ordTree-node : ∀ t₁ i t₂ →
                 ordTree (node t₁ i t₂) ≡
                 ordTree t₁ && ordTree t₂ && le-TreeItem t₁ i && le-ItemTree i t₂
{-# ATP axioms ordTree-nil ordTree-tip ordTree-node #-}

OrdTree : D → Set
OrdTree t = ordTree t ≡ true
{-# ATP definition OrdTree #-}

------------------------------------------------------------------------------
-- The program

-- The function toTree adds an item to a tree.

-- The items have an ordering ≤ defined over them. The item held at a
-- node of the tree is chosen so that the left subtree has items not
-- greater than it and the right subtree has items not less than it.

postulate
  toTree      : D
  toTree-nil  : ∀ item → toTree · item · nil ≡ tip item
  toTree-tip  : ∀ item i → toTree · item · (tip i) ≡
                (if (le i item)
                   then (node (tip i) item (tip item))
                   else (node (tip item) i (tip i)))
  toTree-node : ∀ item t₁ i t₂ →
                toTree · item · (node t₁ i t₂) ≡
                (if (le i item)
                   then (node t₁ i (toTree · item · t₂))
                   else (node (toTree · item · t₁) i t₂))
{-# ATP axioms toTree-nil toTree-tip toTree-node #-}

-- The function makeTree converts a list to a tree.
makeTree : D → D
makeTree is = lit toTree is nil
{-# ATP definition makeTree #-}

-- The function flatten converts a tree to a list.
postulate
  flatten      : D → D
  flatten-nil  : flatten nil ≡ []
  flatten-tip  : ∀ i → flatten (tip i) ≡ i ∷ []
  flatten-node : ∀ t₁ i t₂ → flatten (node t₁ i t₂) ≡ flatten t₁ ++ flatten t₂
{-# ATP axioms flatten-nil flatten-tip flatten-node #-}

-- The function which sorts the list
sort : D → D
sort is = flatten (makeTree is)
{-# ATP definition sort #-}

------------------------------------------------------------------------------
-- References
--
-- Burstall, R. M. (1969). Proving properties of programs by
-- structural induction. The Computer Journal 12.1, pp. 41–48.


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

open import Categories.Category
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Closed

module Categories.Category.Monoidal.Closed.IsClosed
  {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (Cl : Closed M) where

open import Data.Product using (Σ; _,_)
open import Function using (_$_) renaming (_∘_ to _∙_)
open import Function.Equality as Π using (Π)

open import Categories.Category.Product
open import Categories.Category.Monoidal.Properties M
open import Categories.Morphism C
open import Categories.Morphism.Properties C
open import Categories.Morphism.Reasoning C
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Bifunctor.Properties
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Dinatural hiding (_∘ʳ_)
open import Categories.NaturalTransformation.NaturalIsomorphism as NI hiding (refl)
import Categories.Category.Closed as Cls

open Closed Cl

private
  module C = Category C
  open Category C
  open Commutation
  module ℱ = Functor

open HomReasoning
open Π.Π
open adjoint renaming (unit to η; counit to ε)

-- and here we use sub-modules in the hopes of making things go faster
open import Categories.Category.Monoidal.Closed.IsClosed.Identity Cl
open import Categories.Category.Monoidal.Closed.IsClosed.L Cl
open import Categories.Category.Monoidal.Closed.IsClosed.Dinatural Cl
open import Categories.Category.Monoidal.Closed.IsClosed.Diagonal Cl
open import Categories.Category.Monoidal.Closed.IsClosed.Pentagon Cl

private
  id² : {S T : Obj} → [ S , T ]₀ ⇒ [ S , T ]₀
  id² = [ id , id ]₁

  L-natural-comm : {X Y′ Z′ Y Z : Obj} {f : Y′ ⇒ Y} {g : Z ⇒ Z′} →
                  L X Y′ Z′ ∘ [ f , g ]₁ ≈ [ [ id , f ]₁ , [ id , g ]₁ ]₁ ∘ L X Y Z
  L-natural-comm {X} {Y′} {Z′} {Y} {Z} {f} {g} =
    let I = [-,-].identity in begin
    L X Y′ Z′ ∘ [ f , g ]₁                                     ≈⟨ refl⟩∘⟨ [ [-,-] ]-decompose₂ ⟩
    L X Y′ Z′ ∘ [ id , g ]₁ ∘ [ f , id ]₁                      ≈⟨ pullˡ L-g-swap ⟩
    ([ id² , [ id , g ]₁ ]₁ ∘ L X Y′ Z) ∘ [ f , id ]₁          ≈⟨ pullʳ L-f-swap ⟩
    [ id² , [ id , g ]₁ ]₁ ∘ [ [ id , f ]₁ , id² ]₁ ∘ L X Y Z  ≈˘⟨ pushˡ ([-,-].F-resp-≈ (introʳ I , introʳ I) ○ [-,-].homomorphism) ⟩
    [ [ id , f ]₁ , [ id , g ]₁ ]₁ ∘ L X Y Z
      ∎

closed : Cls.Closed C
closed = record
  { [-,-]            = [-,-]
  ; unit             = unit
  ; identity         = identity
  ; diagonal         = diagonal
  ; L                = L
  ; L-natural-comm   = L-natural-comm
  ; L-dinatural-comm = L-dinatural-comm
  ; Lj≈j             = Lj≈j
  ; jL≈i             = jL≈i
  ; iL≈i             = iL≈i
  ; pentagon         = pentagon′
  ; γ⁻¹              = λ {X Y} → record
    { _⟨$⟩_ = λ f → Radjunct f ∘ unitorˡ.to
    ; cong  = λ eq → ∘-resp-≈ˡ (∘-resp-≈ʳ (ℱ.F-resp-≈ (-⊗ X) eq))
    }
  ; γ-inverseOf-γ⁻¹  = λ {X Y} → record
    { left-inverse-of  = λ f → begin
      [ id , Radjunct f ∘ unitorˡ.to ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit
        ≈⟨ ℱ.homomorphism [ X ,-] ⟩∘⟨ refl ⟩∘⟨ refl ⟩
      ([ id , Radjunct f ]₁ ∘ [ id , unitorˡ.to ]₁) ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit
        ≈⟨ cancelInner (⟺ (ℱ.homomorphism [ X ,-]) ○ ℱ.F-resp-≈ [ X ,-] unitorˡ.isoˡ ○ [-,-].identity) ⟩
      Ladjunct (Radjunct f) ≈⟨ LRadjunct≈id ⟩
      f
        ∎
    ; right-inverse-of = λ f → begin
      Radjunct ([ id , f ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit) ∘ unitorˡ.to
        ≈˘⟨ ∘-resp-≈ʳ (ℱ.F-resp-≈ (-⊗ X) (pushˡ (ℱ.homomorphism [ X ,-]))) ⟩∘⟨refl ⟩
      Radjunct (Ladjunct (f ∘ unitorˡ.from)) ∘ unitorˡ.to
        ≈⟨ RLadjunct≈id ⟩∘⟨refl ⟩
      (f ∘ unitorˡ.from) ∘ unitorˡ.to
        ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
      f
        ∎
    }
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Numeral.Natural.Relation.Proofs where

open import Data
open import Functional
open import Numeral.Natural
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Logic.Propositional
open import Logic.Propositional.Theorems
import      Lvl
open import Relator.Equals
open import Type

private variable n : ℕ

Positive-non-zero : Positive(n) ↔ (n ≢ 𝟎)
Positive-non-zero {𝟎}   = [↔]-intro (apply [≡]-intro) \()
Positive-non-zero {𝐒 n} = [↔]-intro (const <>) (const \())

Positive-greater-than-zero : Positive(n) ↔ (n > 𝟎)
Positive-greater-than-zero = [↔]-transitivity Positive-non-zero ([↔]-intro [>]-to-[≢] [≢]-to-[<]-of-0ᵣ)

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:
-- Isomorphism of indexed families
module SOAS.Families.Isomorphism {T} where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Families.Core {T}

open import Categories.Morphism 𝔽amilies public using ()
        renaming ( _≅_ to _≅ₘ_ ; module ≅ to ≅ₘ ; ≅-setoid to ≅ₘ-setoid)

-- Isomorphism between two families
record FamIso (X Y : Family) : Set where

  -- Prove isomorphism of the families X and Y in the category 𝔽am from
  -- a proof of isomorphism of the sets X Γ and Y Γ for all contexts Γ.
  field iso : (Γ : Ctx) → X Γ ≅ₛ Y Γ

  -- Two directions of the isomorphism.
  iso⇒ : X ⇾ Y
  iso⇒ {Γ} = _≅ₛ_.from (iso Γ)
  iso⇐ : Y ⇾ X
  iso⇐ {Γ} = _≅ₛ_.to (iso Γ)

  -- Construct the isomorphism of families
  ≅ₘ : X ≅ₘ Y
  ≅ₘ = record
    { from = iso⇒
    ; to = iso⇐
    ; iso = record
      { isoˡ = λ {Γ}{x} → _≅ₛ_.isoˡ (iso Γ)
      ; isoʳ = λ {Γ}{x} → _≅ₛ_.isoʳ (iso Γ)
      }
    }

≅ₘ→FamIso : {X Y : Family} → X ≅ₘ Y → FamIso X Y
≅ₘ→FamIso p = record { iso = λ Γ → record
  { from = _≅ₘ_.from p
  ; to = _≅ₘ_.to p
  ; iso = record { isoˡ = _≅ₘ_.isoˡ p ; isoʳ = _≅ₘ_.isoʳ p }
  } }

-- | Isomorphism of sorted families

open import Categories.Morphism 𝔽amiliesₛ public
  using () renaming ( _≅_ to _≅̣ₘ_ ; module ≅ to ≅̣ₘ)

-- Sorted family isomorphism gives a family isomorphism at each sort
≅̣ₘ→≅ₘ : {τ : T}{𝒳 𝒴 : Familyₛ} → 𝒳 ≅̣ₘ 𝒴 → 𝒳 τ ≅ₘ 𝒴 τ
≅̣ₘ→≅ₘ {τ} p = record { from = _≅̣ₘ_.from p ; to = _≅̣ₘ_.to p
                     ; iso = record { isoˡ = _≅̣ₘ_.isoˡ p ; isoʳ = _≅̣ₘ_.isoʳ p } }

-- Family isomorphism at each sort gives sorted family isomorphism
≅ₘ→≅̣ₘ : {𝒳 𝒴 : Familyₛ} → ({τ : T} → 𝒳 τ ≅ₘ 𝒴 τ) → 𝒳 ≅̣ₘ 𝒴
≅ₘ→≅̣ₘ p = record { from = _≅ₘ_.from p ; to = _≅ₘ_.to p
                 ; iso = record { isoˡ = _≅ₘ_.isoˡ p ; isoʳ = _≅ₘ_.isoʳ p } }

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Numeral.Finite.Oper.Comparisons.Proofs where

import      Lvl
open import Data
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Finite
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Sign
open import Numeral.Sign.Oper0
open import Relator.Equals
open import Relator.Equals.Proofs.Equivalence
import      Structure.Operator.Names as Names
open import Structure.Operator.Properties
open import Syntax.Number

⋚-of-𝟎-not-+ : ∀{an bn}{b : 𝕟(bn)} → ⦃ _ : 𝟎 {an} ⋚? b ≡ ➕ ⦄ → ⊥
⋚-of-𝟎-not-+ {b = 𝟎}    ⦃ ⦄
⋚-of-𝟎-not-+ {b = 𝐒(_)} ⦃ ⦄

⋚-of-𝟎-not-− : ∀{an bn}{a : 𝕟(an)} → ⦃ _ : a ⋚? 𝟎 {bn} ≡ ➖ ⦄ → ⊥
⋚-of-𝟎-not-− {a = 𝟎}    ⦃ ⦄
⋚-of-𝟎-not-− {a = 𝐒(_)} ⦃ ⦄

⋚-of-𝐒𝟎-not-𝟎 : ∀{an bn}{a : 𝕟(an)} → ⦃ _ : 𝐒(a) ⋚? 𝟎 {bn} ≡ 𝟎 ⦄ → ⊥
⋚-of-𝐒𝟎-not-𝟎 {a = 𝟎}    ⦃ ⦄
⋚-of-𝐒𝟎-not-𝟎 {a = 𝐒(_)} ⦃ ⦄

⋚-of-𝟎𝐒-not-𝟎 : ∀{an bn}{b : 𝕟(bn)} → ⦃ _ : 𝟎 {an} ⋚? 𝐒(b) ≡ 𝟎 ⦄ → ⊥
⋚-of-𝟎𝐒-not-𝟎 {b = 𝟎}    ⦃ ⦄
⋚-of-𝟎𝐒-not-𝟎 {b = 𝐒(_)} ⦃ ⦄

⋚-surjective : ∀{an bn}{a : 𝕟(an)}{b : 𝕟(bn)} → ∃{Obj = (−|0|+)} (a ⋚? b ≡_)
⋚-surjective {a = 𝟎}   {𝟎}   = [∃]-intro 𝟎
⋚-surjective {a = 𝟎}   {𝐒 b} = [∃]-intro ➖
⋚-surjective {a = 𝐒 a} {𝟎}   = [∃]-intro ➕
⋚-surjective {a = 𝐒 a} {𝐒 b} = ⋚-surjective {a = a} {b}

⋚-to-< : ∀{an bn}{a : 𝕟(an)}{b : 𝕟(bn)} → ⦃ _ : a ⋚? b ≡ ➕ ⦄ → (a >? b ≡ 𝑇)
⋚-to-< {a = 𝐒 a} {𝟎} = [≡]-intro
⋚-to-< {a = 𝐒 a} {𝐒 b} = ⋚-to-< {a = a} {b}

⋚-to-> : ∀{an bn}{a : 𝕟(an)}{b : 𝕟(bn)} → ⦃ _ : a ⋚? b ≡ ➖ ⦄ → (a <? b ≡ 𝑇)
⋚-to-> {a = 𝟎}   {𝐒 b} = [≡]-intro
⋚-to-> {a = 𝐒 a} {𝐒 b} = ⋚-to-> {a = a} {b}

⋚-to-≡ : ∀{an bn}{a : 𝕟(an)}{b : 𝕟(bn)} → ⦃ _ : a ⋚? b ≡ 𝟎 ⦄ → (a ≡? b ≡ 𝑇)
⋚-to-≡ {a = 𝟎}   {𝟎}   = [≡]-intro
⋚-to-≡ {a = 𝐒 a} {𝐒 b} = ⋚-to-≡ {a = a} {b}

instance
  [≡?]-commutativity : ∀{n} → Commutativity{T₁ = 𝕟(n)} ⦃ [≡]-equiv ⦄ (_≡?_)
  [≡?]-commutativity{n} = intro(\{x y} → p{n}{x}{y}) where
    p : ∀{n} → Names.Commutativity{T₁ = 𝕟(n)} ⦃ [≡]-equiv ⦄ (_≡?_)
    p{_}{𝟎}  {𝟎}   = [≡]-intro
    p{_}{𝟎}  {𝐒 y} = [≡]-intro
    p{_}{𝐒 x}{𝟎}   = [≡]-intro
    p{_}{𝐒 x}{𝐒 y} = p{_}{x}{y}

⋚-anticommutativity : ∀{xn yn}{x : 𝕟(xn)}{y : 𝕟(yn)} → (−(x ⋚? y) ≡ y ⋚? x)
⋚-anticommutativity {x = 𝟎}  {y = 𝟎}   = [≡]-intro
⋚-anticommutativity {x = 𝟎}  {y = 𝐒 y} = [≡]-intro
⋚-anticommutativity {x = 𝐒 x}{y = 𝟎}   = [≡]-intro
⋚-anticommutativity {x = 𝐒 x}{y = 𝐒 y} = ⋚-anticommutativity {x = x}{y = y}

⋚-elim₃-negation-flip : ∀{xn yn}{x : 𝕟(xn)}{y : 𝕟(yn)}{b₁ b₂ b₃} → (elim₃{P = \_ → Bool} b₁ b₂ b₃ (−(x ⋚? y)) ≡ elim₃ b₃ b₂ b₁ (x ⋚? y))
⋚-elim₃-negation-flip {x = 𝟎}  {y = 𝟎}   = [≡]-intro
⋚-elim₃-negation-flip {x = 𝟎}  {y = 𝐒 y} = [≡]-intro
⋚-elim₃-negation-flip {x = 𝐒 x}{y = 𝟎}   = [≡]-intro
⋚-elim₃-negation-flip {x = 𝐒 x}{y = 𝐒 y} = ⋚-elim₃-negation-flip {x = x}{y = y}

⋚-elim₃-negation-distribution : ∀{xn yn}{x : 𝕟(xn)}{y : 𝕟(yn)}{b₁ b₂ b₃ : Bool} → (!(elim₃ b₁ b₂ b₃ (x ⋚? y)) ≡ elim₃ (! b₁) (! b₂) (! b₃) (x ⋚? y))
⋚-elim₃-negation-distribution {x = 𝟎}  {y = 𝟎}   = [≡]-intro
⋚-elim₃-negation-distribution {x = 𝟎}  {y = 𝐒 y} = [≡]-intro
⋚-elim₃-negation-distribution {x = 𝐒 x}{y = 𝟎}   = [≡]-intro
⋚-elim₃-negation-distribution {x = 𝐒 x}{y = 𝐒 y} = ⋚-elim₃-negation-distribution {x = x}{y = y}


text:
module STLC.Term.Reduction where

open import STLC.Term as Term
open Term.Substitution using () renaming (_[/_] to _[/t_])

open import Data.Nat using (ℕ; _+_)

open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star)

infix 4 _—→_

data _—→_ { n : ℕ } : Term n -> Term n -> Set where

  β-·₁ : ∀ { t₁ t₂ l : Term n }
    -> t₁ —→ t₂
    -- ----------------
    -> t₁ · l —→ t₂ · l

  β-·₂ : ∀ { v t₁ t₂ : Term n }
    -> Value v
    -> t₁ —→ t₂
    -- ----------------
    -> v · t₁ —→ v · t₂

  β-ƛ : ∀ { t : Term (1 + n) } {v : Term n }
    -> Value v
    -- --------------------
    -> (ƛ t) · v —→ (t [/t v ])

infix 2 _—↠_

_—↠_ : { n : ℕ } -> Term n -> Term n -> Set
_—↠_ = Star (_—→_)

max_stars_repo_name: johnyob/agda-types

max_issues_repo_name: johnyob/agda-types

max_forks_repo_name: johnyob/agda-types