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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.OBM.ConfigHardCoded                 as ConfigHardCoded
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Storage.DiemDB.DiemDB               as DiemDB
import      LibraBFT.Impl.Types.OnChainConfig.ValidatorSet    as ValidatorSet
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.ByteString                                   as BS
import      Util.Encode                                       as S
open import Util.Hash
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                       using (String)

module LibraBFT.Impl.Consensus.StateComputerByteString where

-- LBFT-OBM-DIFF: In Rust, the following might throw BlockNotFound
-- in execution_correctness_client.execute_block (not needed/implemented).
-- In OBM we call this error ErrECCBlockNotFound so it is easy to see it is
-- defined, caught, but never thrown.
compute : StateComputerComputeType
compute _self block _parentBlockId =
  StateComputeResult∙new
    (Version∙new (block ^∙ bEpoch {-∙ eEpoch-}) (block ^∙ bRound {-∙ rRound-}))
    <$> maybeEC
 where
  getES : ByteString → Either (List String) EpochState

  maybeEC : Either (List String) (Maybe EpochState)
  maybeEC = case block ^∙ bBlockData ∙ bdBlockType of λ where
    (Proposal {-Payload [-}a{-])-} _author) →
      if BS∙isPrefixOf ConfigHardCoded.ePOCHCHANGE a then just <$> getES a else pure nothing
    NilBlock → pure nothing
    Genesis  → pure nothing

  getES bs = do
    let bs' = BS∙drop (BS∙length ConfigHardCoded.ePOCHCHANGE) bs
    case S.decode bs' of λ where
      (Left   e) → Left ("StateComputerByteString" ∷ "compute" ∷ "decode" ∷ {-T.pack-} e ∷ [])
      (Right vv) → Right (EpochState∙new (block ^∙ bEpoch + 1) vv)

-- LBFT-OBM-DIFF : gets block instead of vector of hashes
-- TODO-2: consider converting to EitherD before proving anything about this
commit : StateComputerCommitType
commit self db (ExecutedBlock∙new _b (StateComputeResult∙new version _)) liws =
  case (DiemDB.saveTransactions.E db (just liws)) of λ where
    (Left   e)  → Left (errText e)
    (Right db') → pure
       ( (self & scObmVersion ∙~ version)
       , db'
       , (maybeS (liws ^∙ liwsLedgerInfo ∙ liNextEpochState) nothing $ λ (EpochState∙new e vv) →
           just (ReconfigEventEpochChange∙new
                 (OnChainConfigPayload∙new e (ValidatorSet.obmFromVV vv))))
       )

-- LBFT-OBM-DIFF : completely different
syncTo : StateComputerSyncToType
syncTo liws =
  maybeS (liws ^∙ liwsNextEpochState) (Left ("StateComputerByteString" ∷ "syncTo" ∷ "Nothing" ∷ [])) $
         λ (EpochState∙new e vv) →
            Right  (ReconfigEventEpochChange∙new
                    (OnChainConfigPayload∙new e (ValidatorSet.obmFromVV vv)))


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Data.Vec.OperationsNat where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Vec.Base
open import Cubical.Data.Vec.Properties
open import Cubical.Data.Sigma
open import Cubical.Data.Sum

open import Cubical.Relation.Nullary

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Generating Vector

genδℕ-Vec : {A : Type ℓ} → (m k : ℕ) → (a b : A) → Vec A m
genδℕ-Vec zero k a b = []
genδℕ-Vec (suc m) k a b  with (discreteℕ k m)
... | yes p = a ∷ replicate b
... | no ¬p = b ∷ (genδℕ-Vec m k a b)

-- some results are easier / false without general a and b
δℕ-Vec : (m : ℕ) → (k : ℕ) → Vec ℕ m
δℕ-Vec m k = genδℕ-Vec m k 1 0

δℕ-Vec-n≤k→≡ : (m k : ℕ) → (m ≤ k) → δℕ-Vec m k ≡ replicate 0
δℕ-Vec-n≤k→≡ zero k r = refl
δℕ-Vec-n≤k→≡ (suc m) k r with (discreteℕ k m)
... | yes p = ⊥.rec (<→≢ r (sym p))
... | no ¬p = cong (λ X → 0 ∷ X) (δℕ-Vec-n≤k→≡ m k (≤-trans ≤-sucℕ r))

δℕ-Vec-k<n→≢ : (m k : ℕ) → (k < m) → (δℕ-Vec m k ≡ replicate 0 → ⊥)
δℕ-Vec-k<n→≢ zero k r = ⊥.rec (¬-<-zero r)
δℕ-Vec-k<n→≢ (suc m) k r q with (discreteℕ k m) | (≤-split r)
... | yes p | z = compute-eqℕ 1 0 (fst (VecPath.encode _ _ q))
... | no ¬p | inl x = δℕ-Vec-k<n→≢ m k (pred-≤-pred x) (snd (VecPath.encode _ _ q))
... | no ¬p | inr x = ¬p (injSuc x)

-----------------------------------------------------------------------------
-- Point wise add
_+n-vec_ : {m : ℕ} → Vec ℕ m → Vec ℕ m → Vec ℕ m
_+n-vec_ {.zero} [] [] = []
_+n-vec_ {.(suc _)} (k ∷ v) (l ∷ v') = (k +n l) ∷ (v +n-vec v')

+n-vec-lid : {m : ℕ} → (v : Vec ℕ m) → replicate 0 +n-vec v ≡ v
+n-vec-lid {.zero} [] = refl
+n-vec-lid {.(suc _)} (k ∷ v) = cong (_∷_ k) (+n-vec-lid v)

+n-vec-rid : {m : ℕ} → (v : Vec ℕ m) → v +n-vec replicate 0 ≡ v
+n-vec-rid {.zero} [] = refl
+n-vec-rid {.(suc _)} (k ∷ v) = cong₂ _∷_ (+-zero k) (+n-vec-rid v)

+n-vec-assoc : {m : ℕ} → (v v' v'' : Vec ℕ m) → v +n-vec (v' +n-vec v'') ≡ (v +n-vec v') +n-vec v''
+n-vec-assoc [] [] [] = refl
+n-vec-assoc (k ∷ v) (l ∷ v') (p ∷ v'') = cong₂ _∷_ (+-assoc k l p) (+n-vec-assoc v v' v'')

+n-vec-comm : {m : ℕ} → (v v' : Vec ℕ m) → v +n-vec v' ≡ v' +n-vec v
+n-vec-comm {.zero} [] [] = refl
+n-vec-comm {.(suc _)} (k ∷ v) (l ∷ v') = cong₂ _∷_ (+-comm k l) (+n-vec-comm v v')

-----------------------------------------------------------------------------
-- Equlity on Vec ℕ
+n-vecSplitReplicate0 : {m : ℕ} → (v v' : Vec ℕ m) → (v +n-vec v') ≡ replicate 0
                        → (v ≡ replicate 0) × (v' ≡ replicate 0)
+n-vecSplitReplicate0 [] [] p = refl , refl
+n-vecSplitReplicate0 (k ∷ v) (l ∷ v') p with VecPath.encode ((k +n l) ∷ (v +n-vec v')) (replicate 0) p
... | pkl , pvv' = (cong₂ _∷_ (fst (m+n≡0→m≡0×n≡0 pkl)) (fst (+n-vecSplitReplicate0 v v' pvv'))) ,
                   (cong₂ _∷_ (snd (m+n≡0→m≡0×n≡0 pkl)) (snd (+n-vecSplitReplicate0 v v' pvv')))

pred-vec-≢0 : {m : ℕ} → (v : Vec ℕ m) → (v ≡ replicate 0 → ⊥)
              → Σ[ k ∈ ℕ ] (Σ[ v' ∈ Vec ℕ m ] ( Σ[ r ∈ (k < m) ] v ≡ v' +n-vec (δℕ-Vec m k)))
pred-vec-≢0 {zero} [] ¬q = ⊥.rec (¬q refl)
pred-vec-≢0 {(suc m)} (l ∷ v) ¬q with (discreteℕ l 0)
-- case l ≡ 0
pred-vec-≢0 {(suc m)} (l ∷ v) ¬q | yes p with pred-vec-≢0 v (λ r → ¬q (cong₂ _∷_ p r))
... | k , v' , infkm , eqvv' = k , ((0 ∷ v') , ((≤-trans infkm ≤-sucℕ) , helper))
  where
  helper : _
  helper with (discreteℕ k m)
  ... | yes pp = ⊥.rec (<→≢ (fst infkm , +-suc _ _ ∙ cong suc (snd infkm)) (cong suc pp))
  ... | no ¬pp = cong₂ _∷_ p eqvv'
-- case l ≢ 0
pred-vec-≢0 {(suc m)} (l ∷ v) ¬q | no ¬p = m , ((predℕ l ∷ v) , (≤-refl , helper))
  where
  helper : _
  helper with (discreteℕ m m)
  ... | yes pp = cong₂ _∷_ (sym (+-suc _ _ ∙ +-zero _ ∙ sym (suc-predℕ l ¬p)))
                      (sym (+n-vec-rid v))
  ... | no ¬pp = ⊥.rec (¬pp refl)

-- split + concat vec results
sep-vec : (k l : ℕ) → Vec ℕ (k +n l) → (Vec ℕ k) ×  (Vec ℕ l )
sep-vec zero l v = [] , v
sep-vec (suc k) l (x ∷ v) = (x ∷ fst (sep-vec k l v)) , (snd (sep-vec k l v))

sep-vec-fst : (k l : ℕ) → (v : Vec ℕ k) → (v' : Vec ℕ l) → fst (sep-vec k l (v ++ v')) ≡ v
sep-vec-fst zero l [] v' = refl
sep-vec-fst (suc k) l (x ∷ v) v' = cong (λ X → x ∷ X) (sep-vec-fst k l v v')

sep-vec-snd : (k l : ℕ) → (v : Vec ℕ k) → (v' : Vec ℕ l) → snd (sep-vec k l (v ++ v')) ≡ v'
sep-vec-snd zero l [] v' = refl
sep-vec-snd (suc k) l (x ∷ v) v' = sep-vec-snd k l v v'

sep-vec-id : (k l : ℕ) → (v : Vec ℕ (k +n l)) → fst (sep-vec k l v) ++ snd (sep-vec k l v) ≡ v
sep-vec-id zero l v = refl
sep-vec-id (suc k) l (x ∷ v) = cong (λ X → x ∷ X) (sep-vec-id k l v)

rep-concat : (k l : ℕ) → {B : Type ℓ} → (b : B) →
             replicate {_} {k} {B} b ++ replicate {_} {l} {B} b ≡ replicate {_} {k +n l} {B} b
rep-concat zero l b = refl
rep-concat (suc k) l b = cong (λ X → b ∷ X) (rep-concat k l b)

+n-vec-concat : (k l : ℕ) → (v w : Vec ℕ k) → (v' w' : Vec ℕ l)
                → (v +n-vec w) ++ (v' +n-vec w') ≡ (v ++ v') +n-vec (w ++ w')
+n-vec-concat zero l [] [] v' w' = refl
+n-vec-concat (suc k) l (x ∷ v) (y ∷ w) v' w' = cong (λ X → x +n y ∷ X) (+n-vec-concat k l v w v' w')

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import HoTT
open import cohomology.Theory

module cohomology.Coproduct {i} (CT : CohomologyTheory i)
  (n : ℤ) (X Y : Ptd i) where

open CohomologyTheory CT
open import cohomology.Sigma CT

private
  P : Bool → Ptd i
  P true = X
  P false = Y

C-⊔ : C n (X ⊙⊔ Y) ≃ᴳ C n (X ⊙∨ Y) ×ᴳ C2 n
C-⊔ = (×ᴳ-emap
        (C-emap n (≃-to-⊙≃ ( BigWedge-Bool-equiv-Wedge P
                          ∘e BigWedge-emap-l P lower-equiv) idp))
        (idiso _)) ⁻¹ᴳ
  ∘eᴳ C-Σ n (⊙Lift {j = i} ⊙Bool) (P ∘ lower)
  ∘eᴳ C-emap n (≃-to-⊙≃ ( ΣBool-equiv-⊔ (de⊙ ∘ P)
                       ∘e Σ-emap-l (de⊙ ∘ P) lower-equiv) idp)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Sigma

data ⊥ : Set where

type : Bool → Set
type true = ⊤
type false = ⊥

record Bad : Set where
  constructor b
  field
    .f : Σ Bool type

test : Bad → Bool
test (b (x , y)) = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Negative3 where

data Mu (F : Set -> Set) : Set where
    inn : F (Mu F) -> Mu F

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Ethambda.Position

import Eth.Prelude -- using (bool)
import Prelude.Bool -- using (bool)
import Data.List -- using (intercalate)
import Prelude.Monad -- using ((>=>))
import Control.Monad.Identity
import Control.Monad.Writer -- using
--  (MonadWriter, WriterT, Writer, execWriterT, execWriter, tell)
import Control.Monad.Reader -- using
--  (MonadReader, ReaderT, Reader, runReaderT, runReader, ask, local)

import Ethambda.Common -- using ((<.>), (<.))
import Ethambda.System -- using (Type(Var, Fun))

-- * The 'PosNeg' type.

record PosNeg a where
  constructor PN
  negatives : List a
  positives : List a

stuff : Show a => String -> List a -> String
stuff ttl l = case l of
  [] => neutral
  _  => ttl <> ": " <> unwords (intercalate (pure ",") (map (pure . show) l))

Show a => Show (PosNeg a) where
  show (PN neg pos)
    =   "PN"
    <.> "neg"
    <.> "pos"

Semigroup (PosNeg a) where
  (PN p n) <+> (PN p' n') = PN (p <> p') (n <> n')

Monoid (PosNeg a) where
  neutral = PN neutral neutral

pos : a -> PosNeg a
pos a = PN neutral (pure a)

neg : a -> PosNeg a
neg a = PN (pure a) neutral

-- * Core algorithm.
AppM : Type -> (Type -> Type) -> Type
AppM a m =
  ( MonadWriter (PosNeg a) m
  , MonadReader Bool m
  )

App : Type -> Type -> Type
App a x = WriterT (PosNeg a) (Reader Bool) x

-- implementation Functor (ReaderT ?a ?m) where

-- execApp : App a x -> PosNeg a
execApp : WriterT (PosNeg a) (ReaderT Bool Identity) x -> PosNeg a
execApp = (`runReader` True) . execWriterT

-- tellPos : AppM a m => a -> m ()
tellPos : MonadWriter (PosNeg a) m => a -> m ()
-- tellPos = tell . pos
tellPos = tell . pos

-- tellNeg : AppM a m => a -> m ()
-- tellNeg = tell . neg
tellNeg : MonadWriter (PosNeg a) m => a -> m ()
tellNeg = tell . neg

-- tellIt : AppM a m => a -> m ()
-- tellIt a = ask >>= bool (tellNeg a) (tellPos a)
tellIt
  : MonadWriter (PosNeg a) m
  => MonadReader Bool m
  => a -> m ()
tellIt a = ask >>= bool (tellNeg a) (tellPos a)

-- positionM : AppM a m => Type a -> m ()
positionM
  : MonadWriter (PosNeg a) n
  => MonadReader Bool m
  => Tp a -> m ()
positionM tp = case tp of
  Var a => tellIt a
  Fun t u => do
    positionM u
    local not $ positionM t

-- export
-- position : Type a -> PosNeg a
-- position = execApp . positionM

max_stars_repo_name: fredefox/ethambda-agda

max_issues_repo_name: fredefox/ethambda-agda

max_forks_repo_name: fredefox/ethambda-agda


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

module Pitch where

open import Cubical.Core.Everything using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)

open import Cubical.Foundations.Prelude     using (refl; sym; _∙_; cong; transport; subst; funExt; transp)
--open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Univalence  using (ua)
open import Cubical.Foundations.Isomorphism using (iso; Iso; isoToPath; section; retract; isoToEquiv)

open import Data.Bool       using (Bool; false; true)
open import Data.Integer    using (ℤ; +_; -[1+_])
open import Data.Fin        using (Fin; toℕ; #_; _≟_; fromℕ<) renaming (zero to fz; suc to fs)
open import Data.List       using (List; []; _∷_; foldr; map)
open import Data.Maybe      using (Maybe; just; nothing) renaming (map to mmap)
open import Data.Nat        using (ℕ; zero; suc; _+_; _*_; _∸_; _≡ᵇ_; _>_)
open import Data.Nat.DivMod using (_mod_; _div_)
open import Data.Product    using (_×_; _,_; proj₁)
open import Data.String     using (String; intersperse) renaming (_++_ to _++s_)
open import Data.Vec        using (Vec; []; _∷_; lookup; replicate; _[_]%=_; toList) renaming (map to vmap)

open import Relation.Nullary using (yes; no)

open import BitVec          using (BitVec; insert; empty; show)
open import Util            using (n∸k<n; _+N_; opposite; _∘_)

-- Position of a pitch on an absolute scale
-- 0 is C(-1) on the international scale (where C4 is middle C)
-- or C0 on the Midi scale (where C5 is middle C)
-- Pitch is intentially set to match Midi pitch.
-- However it is fine to let 0 represent some other note and
-- translate appropriately at the end.
Pitch : Type
Pitch = ℕ

-- Number of notes in the chromatic scale.
s12 : ℕ
s12 = 12

-- Number of notes in the diatonic scale.
s7 : ℕ
s7 = 7

-- Pitch Class: position of a pitch within an octave, in the range [0..s12-1].
-- Pitch class 0 corresponds to C (assuming pitch 0 is Midi C0), which is standard.
PC : Type
PC = Fin s12

showPC : PC → String
showPC fz = "0"
showPC (fs fz) = "1"
showPC (fs (fs fz)) = "2"
showPC (fs (fs (fs fz))) = "3"
showPC (fs (fs (fs (fs fz)))) = "4"
showPC (fs (fs (fs (fs (fs fz))))) = "5"
showPC (fs (fs (fs (fs (fs (fs fz)))))) = "6"
showPC (fs (fs (fs (fs (fs (fs (fs fz))))))) = "7"
showPC (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))) = "8"
showPC (fs (fs (fs (fs (fs (fs (fs (fs (fs fz))))))))) = "9"
showPC (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz)))))))))) = "a"
showPC (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs (fs fz))))))))))) = "b"

showPCs : List PC → String
showPCs pcs = intersperse " " (map showPC pcs)

toPC : Pitch → PC
toPC = _mod s12

Scale : ℕ → Type
Scale = Vec PC

-- Which octave one is in.
Octave : Type
Octave = ℕ

PitchOctave : Type
PitchOctave = PC × Octave

relativeToAbsolute : PitchOctave → Pitch
relativeToAbsolute (n , o) = (o * s12 + (toℕ n))

absoluteToRelative : Pitch → PitchOctave
absoluteToRelative n = (toPC n , n div s12)

pitchToClass : Pitch → PC
pitchToClass = proj₁ ∘ absoluteToRelative

majorScale harmonicMinorScale : Scale s7
majorScale         = # 0 ∷ # 2 ∷ # 4 ∷ # 5 ∷ # 7 ∷ # 9 ∷ # 11 ∷ []
harmonicMinorScale = # 0 ∷ # 2 ∷ # 3 ∷ # 5 ∷ # 7 ∷ # 8 ∷ # 11 ∷ []

wholeTone0Scale wholeTone1Scale : Scale 6
wholeTone0Scale    = # 0 ∷ # 2 ∷ # 4 ∷ # 6 ∷ # 8 ∷ # 10 ∷ []
wholeTone1Scale    = # 1 ∷ # 3 ∷ # 5 ∷ # 7 ∷ # 9 ∷ # 11 ∷ []

octatonic01Scale octatonic02Scale octatonic12Scale : Scale 8
octatonic01Scale   = # 0 ∷ # 1 ∷ # 3 ∷ # 4 ∷ # 6 ∷ # 7 ∷ # 9 ∷ # 10 ∷ []
octatonic02Scale   = # 0 ∷ # 2 ∷ # 3 ∷ # 5 ∷ # 6 ∷ # 8 ∷ # 9 ∷ # 11 ∷ []
octatonic12Scale   = # 1 ∷ # 2 ∷ # 4 ∷ # 5 ∷ # 7 ∷ # 8 ∷ # 10 ∷ # 11 ∷ []

majorPentatonicScale minorPentatonicScale ryukyuScale : Scale 5
majorPentatonicScale = # 0 ∷ # 2 ∷ # 4 ∷ # 7 ∷ # 9 ∷ []
minorPentatonicScale = # 0 ∷ # 2 ∷ # 4 ∷ # 7 ∷ # 9 ∷ []
ryukyuScale          = # 0 ∷ # 4 ∷ # 5 ∷ # 7 ∷ # 11 ∷ []

indexInScale : {n : ℕ} → Vec PC n → Fin s12 → Maybe (Fin n)
indexInScale []         p = nothing
indexInScale (pc ∷ pcs) p with pc ≟ p
... | yes _ = just fz
... | no  _ = mmap fs (indexInScale pcs p)

scaleSize : {n : ℕ} → Scale n → ℕ
scaleSize {n} _ = n

transposePitch : ℤ → Pitch → Pitch
transposePitch (+_     k) n = n + k
transposePitch (-[1+_] k) n = n ∸ suc k

-- transpose pitch class
Tp : ℕ  → PC → PC
Tp n pc = pc +N n

-- invert pitch class
Ip : PC → PC
Ip = opposite

-- Set of pitch classes represented as a bit vector.
PCSet : Type
PCSet = BitVec s12

toPCSet : List PC → PCSet
toPCSet = foldr insert empty

fromPCSet : PCSet → List PC
fromPCSet pcs = fromPCS s12 pcs
  where fromPCS : (n : ℕ) → BitVec n → List PC
        fromPCS zero []              = []
        fromPCS (suc n) (false ∷ xs) = fromPCS n xs
        fromPCS (suc n) (true  ∷ xs) = fromℕ< (n∸k<n 11 n) ∷ fromPCS n xs

-- transpose pitch class set
T : ℕ → PCSet → PCSet
T n = toPCSet ∘ map (Tp n) ∘ fromPCSet

-- invert pitch class set
I : PCSet → PCSet
I = toPCSet ∘ map Ip ∘ fromPCSet

-- Standard Midi pitches

-- first argument is relative pitch within octave
-- second argument is octave (C5 = middle C for Midi)
standardMidiPitch : Fin s12 → ℕ → Pitch
standardMidiPitch p o = relativeToAbsolute (p , o)

c c♯ d d♯ e f f♯ g g♯ a b♭ b : ℕ → Pitch
c  = standardMidiPitch (# 0)
c♯ = standardMidiPitch (# 1)
d  = standardMidiPitch (# 2)
d♯ = standardMidiPitch (# 3)
e  = standardMidiPitch (# 4)
f  = standardMidiPitch (# 5)
f♯ = standardMidiPitch (# 6)
g  = standardMidiPitch (# 7)
g♯ = standardMidiPitch (# 8)
a  = standardMidiPitch (# 9)
b♭ = standardMidiPitch (# 10)
b  = standardMidiPitch (# 11)

-- Equivalences

rel→abs : PitchOctave → Pitch
rel→abs = relativeToAbsolute

abs→rel : Pitch → PitchOctave
abs→rel = absoluteToRelative

{-
rel→abs→rel : (p : PitchOctave) → (abs→rel ∘ rel→abs) p ≡ p
rel→abs→rel (pitchClass p , octave o) i =
  let a = cong pitchClass (modUnique s12 o p)
      b = cong octave     (divUnique s12 o p)
  in a i , b i

abs→rel→abs : (p : Pitch) → (rel→abs ∘ abs→rel) p ≡ p
abs→rel→abs (pitch p) = cong pitch (sym (n≡divmod p s12))

abs≃rel : Iso Pitch PitchOctave
abs≃rel = iso abs→rel rel→abs rel→abs→rel abs→rel→abs

abs≡rel : Pitch ≡ PitchOctave
abs≡rel = isoToPath abs≃rel
-}

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Strings
------------------------------------------------------------------------

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

module Data.String where

open import Data.Vec as Vec using (Vec)
open import Data.Char as Char using (Char)

------------------------------------------------------------------------
-- Re-export contents of base, and decidability of equality

open import Data.String.Base public
open import Data.String.Properties using (_≟_; _==_) public

------------------------------------------------------------------------
-- Operations

toVec : (s : String) → Vec Char (length s)
toVec s = Vec.fromList (toList s)


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Groups.Torus where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.Prelims

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv

open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +Comm to +ℤ-comm ; +Assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Algebra.Group renaming (ℤ to ℤGroup ; Bool to BoolGroup ; Unit to UnitGroup)

open import Cubical.HITs.Pushout
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2) hiding (map)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim2 to pElim2 ; ∣_∣ to ∣_∣₁) hiding (map)
open import Cubical.HITs.Nullification
open import Cubical.HITs.Truncation renaming (elim to trElim ; elim2 to trElim2 ; map to trMap ; rec to trRec)
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Loopspace

open IsGroupHom
open Iso

-- The following section contains stengthened induction principles for cohomology groups of T². They are particularly useful for showing that
-- that some Isos are morphisms. They make things type-check faster, but should probably not be used for computations.

-- We first need some functions
elimFunT² : (n : ℕ) (p q : typ (Ω (coHomK-ptd (suc n))))
                  → Square q q p p
                  → S¹ × S¹ → coHomK (suc n)
elimFunT² n p q P (base , base) = ∣ ptSn (suc n) ∣
elimFunT² n p q P (base , loop i) = q i
elimFunT² n p q P (loop i , base) = p i
elimFunT² n p q P (loop i , loop j) = P i j

elimFunT²' : (n : ℕ) → Square (refl {ℓ-zero} {coHomK (suc n)} {∣ ptSn (suc n) ∣}) refl refl refl
           → S¹ × S¹ → coHomK (suc n)
elimFunT²' n P (x , base) = ∣ ptSn (suc n) ∣
elimFunT²' n P (base , loop j) = ∣ ptSn (suc n) ∣
elimFunT²' n P (loop i , loop j) = P i j

elimFunT²'≡elimFunT² : (n : ℕ) → (P : _) → elimFunT²' n P ≡ elimFunT² n refl refl P
elimFunT²'≡elimFunT² n P i (base , base) = ∣ ptSn (suc n) ∣
elimFunT²'≡elimFunT² n P i (base , loop k) = ∣ ptSn (suc n) ∣
elimFunT²'≡elimFunT² n P i (loop j , base) = ∣ ptSn (suc n) ∣
elimFunT²'≡elimFunT² n P i (loop j , loop k) = P j k

{-
The first induction principle says that when proving a proposition for some x : Hⁿ(T²), n ≥ 1, it suffices to show that it holds for
(elimFunT² p q P) for any paths p q : ΩKₙ, and square P : Square q q p p. This is useful because elimFunT² p q P (base , base) recudes to 0
-}

coHomPointedElimT² : ∀ {ℓ} (n : ℕ) {B : coHom (suc n) (S¹ × S¹) → Type ℓ}
                 → ((x : coHom (suc n) (S¹ × S¹)) → isProp (B x))
                 → ((p q : _) (P : _) → B ∣ elimFunT² n p q P ∣₂)
                 → (x : coHom (suc n) (S¹ × S¹)) → B x
coHomPointedElimT² n {B = B} isprop indp =
  coHomPointedElim _ (base , base) isprop
    λ f fId → subst B (cong ∣_∣₂ (funExt (λ { (base , base) → sym fId
                                           ; (base , loop i) j → helper f fId i1 i (~ j)
                                           ; (loop i , base) j → helper f fId i i1 (~ j)
                                           ; (loop i , loop j) k → helper f fId i j (~ k)})))
                       (indp (λ i → helper f fId i i1 i1)
                             (λ i → helper f fId i1 i i1)
                              λ i j → helper f fId i j i1)
    where
    helper : (f : S¹ × S¹ → coHomK (suc n)) → f (base , base) ≡ ∣ ptSn (suc n) ∣
           → I → I → I → coHomK (suc n)
    helper f fId i j k =
      hfill (λ k → λ {(i = i0) → doubleCompPath-filler (sym fId) (cong f (λ i → (base , loop i))) fId k j
                     ; (i = i1) → doubleCompPath-filler (sym fId) (cong f (λ i → (base , loop i))) fId k j
                     ; (j = i0) → doubleCompPath-filler (sym fId) (cong f (λ i → (loop i , base))) fId k i
                     ; (j = i1) → doubleCompPath-filler (sym fId) (cong f (λ i → (loop i , base))) fId k i})
            (inS (f ((loop i) , (loop j))))
            k

private
  lem : ∀ {ℓ} (n : ℕ) {B : coHom (2 + n) (S¹ × S¹) → Type ℓ}
                   → ((P : _) → B ∣ elimFunT² (suc n) refl refl P ∣₂)
                   → (p : _) → (refl ≡ p)
                   → (q : _) → (refl ≡ q)
                   → (P : _)
                   → B ∣ elimFunT² (suc n) p q P ∣₂
  lem n {B = B} elimP p =
    J (λ p _ → (q : _) → (refl ≡ q)
             → (P : _)
             → B ∣ elimFunT² (suc n) p q P ∣₂)
      λ q →
        J (λ q _ → (P : _) → B ∣ elimFunT² (suc n) refl q P ∣₂)
           elimP

{- When working with Hⁿ(T²) , n ≥ 2, we are, in the case described above, allowed to assume that any f : Hⁿ(T²) is
   elimFunT² n refl refl P -}
coHomPointedElimT²' : ∀ {ℓ} (n : ℕ) {B : coHom (2 + n) (S¹ × S¹) → Type ℓ}
                 → ((x : coHom (2 + n) (S¹ × S¹)) → isProp (B x))
                 → ((P : _) → B ∣ elimFunT² (suc n) refl refl P ∣₂)
                 → (x : coHom (2 + n) (S¹ × S¹)) → B x
coHomPointedElimT²' n {B = B} prop ind =
  coHomPointedElimT² (suc n) prop
    λ p q P → trRec (isProp→isOfHLevelSuc n (prop _))
      (λ p-refl → trRec (isProp→isOfHLevelSuc n (prop _))
                         (λ q-refl → lem n {B = B} ind p (sym p-refl) q (sym q-refl) P)
      (isConnectedPath _ (isConnectedPathKn (suc n) _ _) q refl .fst))
      (isConnectedPath _ (isConnectedPathKn (suc n) _ _) p refl .fst)

{- A slight variation of the above which gives definitional equalities for all points (x , base) -}
private
  coHomPointedElimT²'' : ∀ {ℓ} (n : ℕ) {B : coHom (2 + n) (S¹ × S¹) → Type ℓ}
                   → ((x : coHom (2 + n) (S¹ × S¹)) → isProp (B x))
                   → ((P : _) → B ∣ elimFunT²' (suc n) P ∣₂)
                   → (x : coHom (2 + n) (S¹ × S¹)) → B x
  coHomPointedElimT²'' n {B = B} prop ind =
    coHomPointedElimT²' n prop λ P → subst (λ x → B ∣ x ∣₂)
                        (elimFunT²'≡elimFunT² (suc n) P) (ind P)

--------- H⁰(T²) ------------
H⁰-T²≅ℤ : GroupIso (coHomGr 0 (S₊ 1 × S₊ 1)) ℤGroup
H⁰-T²≅ℤ =
  H⁰-connected (base , base)
    λ (a , b) → pRec isPropPropTrunc
                     (λ id1 → pRec isPropPropTrunc
                                   (λ id2 → ∣ ΣPathP (id1 , id2) ∣₁)
                                   (Sn-connected 0 b) )
                     (Sn-connected 0 a)

--------- H¹(T²) -------------------------------

H¹-T²≅ℤ×ℤ : GroupIso (coHomGr 1 ((S₊ 1) × (S₊ 1))) (DirProd ℤGroup ℤGroup)
H¹-T²≅ℤ×ℤ = theIso □ GroupIsoDirProd (Hⁿ-Sⁿ≅ℤ 0) (H⁰-Sⁿ≅ℤ 0)
  where
  typIso : Iso _ _
  typIso = setTruncIso (curryIso ⋄ codomainIso S1→K₁≡S1×ℤ ⋄ toProdIso)
                      ⋄ setTruncOfProdIso

  theIso : GroupIso _ _
  fst theIso = typIso
  snd theIso =
    makeIsGroupHom
      (coHomPointedElimT² _ (λ _ → isPropΠ λ _ → isSet× isSetSetTrunc isSetSetTrunc _ _)
        λ pf qf Pf →
        coHomPointedElimT² _ (λ _ → isSet× isSetSetTrunc isSetSetTrunc _ _)
          λ pg qg Pg i → ∣ funExt (helperFst pf qf pg qg Pg Pf) i  ∣₂
                        , ∣ funExt (helperSnd pf qf pg qg Pg Pf) i ∣₂)
     where
       module _ (pf qf pg qg : 0ₖ 1 ≡ 0ₖ 1) (Pg : Square qg qg pg pg) (Pf : Square qf qf pf pf) where
         helperFst : (x : S¹)
                → fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pf qf Pf (x , y) +ₖ elimFunT² 0 pg qg  Pg (x , y)) .fst
                 ≡ fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pf qf Pf (x , y)) .fst
                +ₖ fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pg qg  Pg (x , y)) .fst
         helperFst base = refl
         helperFst (loop i) j = loopLem j i
           where
           loopLem : cong (λ x → fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pf qf Pf (x , y) +ₖ elimFunT² 0 pg qg  Pg (x , y)) .fst) loop
                   ≡ cong (λ x → fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pf qf Pf (x , y)) .fst
                               +ₖ fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pg qg  Pg (x , y)) .fst) loop
           loopLem = (λ i j → S¹map-id (pf j +ₖ pg j) i)
                   ∙ (λ i j → S¹map-id (pf j) (~ i) +ₖ S¹map-id (pg j) (~ i))

         helperSnd : (x : S¹)
                → fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pf qf Pf (x , y) +ₖ elimFunT² 0 pg qg  Pg (x , y)) .snd
                ≡ fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pf qf Pf (x , y)) .snd +ℤ fun S1→K₁≡S1×ℤ (λ y → elimFunT² 0 pg qg  Pg (x , y)) .snd
         helperSnd =
           toPropElim (λ _ → isSetℤ _ _)
                      ((λ i → winding (basechange2⁻ base λ j → S¹map (∙≡+₁ qf qg (~ i) j)))
                    ∙∙ cong (winding ∘ basechange2⁻ base) (congFunct S¹map qf qg)
                    ∙∙ (cong winding (basechange2⁻-morph base (cong S¹map qf) (cong S¹map qg))
                      ∙ winding-hom (basechange2⁻ base (cong S¹map qf)) (basechange2⁻ base (cong S¹map qg))))

----------------------- H²(T²) ------------------------------

H²-T²≅ℤ : GroupIso (coHomGr 2 (S₊ 1 × S₊ 1)) ℤGroup
H²-T²≅ℤ = compGroupIso helper2 (Hⁿ-Sⁿ≅ℤ 0)
  where
  helper : Iso (∥ ((a : S¹) → coHomK 2) ∥₂ × ∥ ((a : S¹) → coHomK 1) ∥₂) (coHom 1 S¹)
  inv helper s = 0ₕ _ , s
  fun helper = snd
  leftInv helper _ =
    ΣPathP (isOfHLevelSuc 0 (isOfHLevelRetractFromIso 0 (fst (Hⁿ-S¹≅0 0)) (isContrUnit)) _ _
          , refl)
  rightInv helper _ = refl
  theIso : Iso (coHom 2 (S¹ × S¹)) (coHom 1 S¹)
  theIso = setTruncIso (curryIso ⋄ codomainIso S1→K2≡K2×K1 ⋄ toProdIso)
         ⋄ setTruncOfProdIso
         ⋄ helper

  helper2 : GroupIso (coHomGr 2 (S¹ × S¹)) (coHomGr 1 S¹)
  helper2 .fst = theIso
  helper2 .snd = makeIsGroupHom (
    coHomPointedElimT²'' 0 (λ _ → isPropΠ λ _ → isSetSetTrunc _ _)
      λ P → coHomPointedElimT²'' 0 (λ _ → isSetSetTrunc _ _)
      λ Q → ((λ i → ∣ (λ a → ΩKn+1→Kn 1 (sym (rCancel≡refl 0 i)
                                        ∙∙ cong (λ x → (elimFunT²' 1 P (a , x) +ₖ elimFunT²' 1 Q (a , x)) -ₖ ∣ north ∣) loop
                                        ∙∙ rCancel≡refl 0 i)) ∣₂))
          ∙∙ (λ i → ∣ (λ a → ΩKn+1→Kn 1 (rUnit (cong (λ x → rUnitₖ 2 (elimFunT²' 1 P (a , x) +ₖ elimFunT²' 1 Q (a , x)) i) loop) (~ i))) ∣₂)
          ∙∙ (λ i → ∣ (λ a → ΩKn+1→Kn 1 (∙≡+₂ 0 (cong (λ x → elimFunT²' 1 P (a , x)) loop) (cong (λ x → elimFunT²' 1 Q (a , x)) loop) (~ i))) ∣₂)
          ∙∙ (λ i → ∣ (λ a → ΩKn+1→Kn-hom 1 (cong (λ x → elimFunT²' 1 P (a , x)) loop) (cong (λ x → elimFunT²' 1 Q (a , x)) loop) i) ∣₂)
          ∙∙ (λ i → ∣ ((λ a → ΩKn+1→Kn 1 (rUnit (cong (λ x → rUnitₖ 2 (elimFunT²' 1 P (a , x)) (~ i)) loop) i)
                                           +ₖ ΩKn+1→Kn 1 (rUnit (cong (λ x → rUnitₖ 2 (elimFunT²' 1 Q (a , x)) (~ i)) loop) i))) ∣₂)
           ∙ (λ i → ∣ ((λ a → ΩKn+1→Kn 1 (sym (rCancel≡refl 0 (~ i))
                                                         ∙∙ cong (λ x → elimFunT²' 1 P (a , x) +ₖ ∣ north ∣) loop
                                                         ∙∙ rCancel≡refl 0 (~ i))
                                           +ₖ ΩKn+1→Kn 1 (sym (rCancel≡refl 0 (~ i))
                                                         ∙∙ cong (λ x → elimFunT²' 1 Q (a , x) +ₖ ∣ north ∣) loop
                                                         ∙∙ rCancel≡refl 0 (~ i)))) ∣₂))
-- >>>>>>> master

private
  to₂ : coHom 2 (S₊ 1 × S₊ 1) → ℤ
  to₂ = fun (fst H²-T²≅ℤ)

  from₂ : ℤ → coHom 2 (S₊ 1 × S₊ 1)
  from₂ = inv (fst H²-T²≅ℤ)

  to₁ : coHom 1 (S₊ 1 × S₊ 1) → ℤ × ℤ
  to₁ = fun (fst H¹-T²≅ℤ×ℤ)

  from₁ : ℤ × ℤ → coHom 1 (S₊ 1 × S₊ 1)
  from₁ = inv (fst H¹-T²≅ℤ×ℤ)

  to₀ : coHom 0 (S₊ 1 × S₊ 1) → ℤ
  to₀ = fun (fst H⁰-T²≅ℤ)

  from₀ : ℤ → coHom 0 (S₊ 1 × S₊ 1)
  from₀ = inv (fst H⁰-T²≅ℤ)

{-
-- Compute fast:
test : to₁ (from₁ (0 , 1) +ₕ from₁ (1 , 0)) ≡ (1 , 1)
test = refl

test2 : to₁ (from₁ (5 , 1) +ₕ from₁ (-2 , 3)) ≡ (3 , 4)
test2 = refl

-- Compute pretty fast

test3 : to₂ (from₂ 1) ≡ 1
test3 = refl

test4 : to₂ (from₂ 2) ≡ 2
test4 = refl

test5 : to₂ (from₂ 3) ≡ 3
test5 = refl

-- Compute, but slower

test6 : to₂ (from₂ 0 +ₕ from₂ 0) ≡ 0
test6 = refl

test6 : to₂ (from₂ 0 +ₕ from₂ 1) ≡ 1
test6 = refl

-- Does not compute
test7 : to₂ (from₂ 1 +ₕ from₂ 0) ≡ 1
test7 = refl
-}


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

-- In this module, we define the subtyping relation of D<: according to Lemma 2.
module Dsub where

open import Data.List as List
open import Data.List.All as All
open import Data.Nat as ℕ
open import Data.Maybe as Maybe
open import Data.Product as Σ
open import Data.Sum
open import Data.Empty renaming (⊥ to False)
open import Data.Vec as Vec renaming (_∷_ to _‼_ ; [] to nil) hiding (_++_)
open import Function

open import Data.Maybe.Properties as Maybeₚ
open import Data.Nat.Properties as ℕₚ
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import DsubDef
open import Utils

module Dsub where

  infix 4 _⊢_<:_

  data _⊢_<:_ : Env → Typ → Typ → Set where
    dtop   : ∀ {Γ T} →
      Γ ⊢ T <: ⊤
    dbot   : ∀ {Γ T} →
      Γ ⊢ ⊥ <: T
    drefl  : ∀ {Γ T} →
      Γ ⊢ T <: T
    dtrans : ∀ {Γ S U} T →
      (S<:T : Γ ⊢ S <: T) →
      (T<:U : Γ ⊢ T <: U) →
      Γ ⊢ S <: U
    dbnd   : ∀ {Γ S U S′ U′} →
      (S′<:S : Γ ⊢ S′ <: S) →
      (U<:U′ : Γ ⊢ U <: U′) →
      Γ ⊢ ⟨A: S ⋯ U ⟩ <: ⟨A: S′ ⋯ U′ ⟩
    dall   : ∀ {Γ S U S′ U′} →
      (S′<:S : Γ ⊢ S′ <: S) →
      (U<:U′ : (S′ ∷ Γ) ⊢ U <: U′) →
      Γ ⊢ Π S ∙ U <: Π S′ ∙ U′
    dsel₁  : ∀ {Γ n T S} →
      (T∈Γ : env-lookup Γ n ≡ just T) →
      (D : Γ ⊢ T <: ⟨A: S ⋯ ⊤ ⟩) →
      Γ ⊢ S <: n ∙A
    dsel₂  : ∀ {Γ n T U} →
      (T∈Γ : env-lookup Γ n ≡ just T) →
      (D : Γ ⊢ T <: ⟨A: ⊥ ⋯ U ⟩) →
      Γ ⊢ n ∙A <: U

  D-measure : ∀ {Γ S U} (D : Γ ⊢ S <: U) → ℕ
  D-measure dtop                 = 1
  D-measure dbot                 = 1
  D-measure drefl                = 1
  D-measure (dtrans _ S<:T T<:U) = 1 + D-measure S<:T + D-measure T<:U
  D-measure (dbnd D₁ D₂)         = 1 + D-measure D₁ + D-measure D₂
  D-measure (dall Dp Db)         = 1 + D-measure Dp + D-measure Db
  D-measure (dsel₁ T∈Γ D)        = 1 + D-measure D
  D-measure (dsel₂ T∈Γ D)        = 1 + D-measure D

  D-measure≥1 : ∀ {Γ S U} (D : Γ ⊢ S <: U) → D-measure D ≥ 1
  D-measure≥1 dtop           = s≤s z≤n
  D-measure≥1 dbot           = s≤s z≤n
  D-measure≥1 drefl          = s≤s z≤n
  D-measure≥1 (dtrans _ _ _) = s≤s z≤n
  D-measure≥1 (dbnd _ _)     = s≤s z≤n
  D-measure≥1 (dall _ _)     = s≤s z≤n
  D-measure≥1 (dsel₁ _ _)    = s≤s z≤n
  D-measure≥1 (dsel₂ _ _)    = s≤s z≤n

  D-deriv : Set
  D-deriv = Σ (Env × Typ × Typ) λ { (Γ , S , U) → Γ ⊢ S <: U }

  env : D-deriv → Env
  env ((Γ , _) , _) = Γ

  typ₁ : D-deriv → Typ
  typ₁ ((_ , S , U) , _) = S

  typ₂ : D-deriv → Typ
  typ₂ ((_ , S , U) , _) = U

  drefl-dec : ∀ (D : D-deriv) → Dec (D ≡ ((env D , typ₁ D , _) , drefl))
  drefl-dec (_ , dtop)         = no (λ ())
  drefl-dec (_ , dbot)         = no (λ ())
  drefl-dec (_ , drefl)        = yes refl
  drefl-dec (_ , dtrans _ _ _) = no (λ ())
  drefl-dec (_ , dbnd _ _)     = no (λ ())
  drefl-dec (_ , dall _ _)     = no (λ ())
  drefl-dec (_ , dsel₁ _ _)    = no (λ ())
  drefl-dec (_ , dsel₂ _ _)    = no (λ ())

  -- weakening
  infixl 7 _⇑
  _⇑ : Env → Env
  [] ⇑      = []
  (T ∷ Γ) ⇑ = T ↑ length Γ ∷ Γ ⇑

  ↦∈-weaken-≤ : ∀ {n T Γ} →
                  n ↦ T ∈ Γ →
                ∀ Γ₁ Γ₂ T′ →
                  Γ ≡ Γ₁ ‣ Γ₂ →
                  length Γ₂ ≤ n →
                  suc n ↦ T ↑ length Γ₂ ∈ Γ₁ ‣ T′ ! ‣ Γ₂ ⇑
  ↦∈-weaken-≤ hd .(_ ∷ _) [] T′ refl z≤n       = tl hd
  ↦∈-weaken-≤ hd Γ₁ (_ ∷ Γ₂) T′ eqΓ ()
  ↦∈-weaken-≤ (tl T∈Γ) .(_ ∷ _) [] T′ refl z≤n = tl (tl T∈Γ)
  ↦∈-weaken-≤ (tl {_} {T} T∈Γ) Γ₁ (_ ∷ Γ₂) T′ refl (s≤s l≤n)
    rewrite ↑-↑-comm T 0 (length Γ₂) z≤n       = tl (↦∈-weaken-≤ T∈Γ Γ₁ Γ₂ T′ refl l≤n)

  ↦∈-weaken-> : ∀ {n T Γ} →
                  n ↦ T ∈ Γ →
                ∀ Γ₁ Γ₂ T′ →
                  Γ ≡ Γ₁ ‣ Γ₂ →
                  length Γ₂ > n →
                  n ↦ T ↑ length Γ₂ ∈ Γ₁ ‣ T′ ! ‣ Γ₂ ⇑
  ↦∈-weaken-> T∈Γ Γ₁ [] T′ eqΓ ()
  ↦∈-weaken-> (hd {T}) Γ₁ (_ ∷ Γ₂) T′ refl (s≤s l>n)
    rewrite ↑-↑-comm T 0 (length Γ₂) l>n = hd
  ↦∈-weaken-> (tl {_} {T} T∈Γ) Γ₁ (_ ∷ Γ₂) T′ refl (s≤s l>n)
    rewrite ↑-↑-comm T 0 (length Γ₂) z≤n = tl (↦∈-weaken-> T∈Γ Γ₁ Γ₂ T′ refl l>n)

  ↦∈-weaken : ∀ {n T Γ} →
                n ↦ T ∈ Γ →
              ∀ Γ₁ Γ₂ T′ →
                Γ ≡ Γ₁ ‣ Γ₂ →
                ↑-idx n (length Γ₂) ↦ T ↑ length Γ₂ ∈ Γ₁ ‣ T′ ! ‣ Γ₂ ⇑
  ↦∈-weaken {n} T∈Γ _ Γ₂ _ eqΓ with length Γ₂ ≤? n
  ... | yes l≤n = ↦∈-weaken-≤ T∈Γ _ Γ₂ _ eqΓ l≤n
  ... | no l>n  = ↦∈-weaken-> T∈Γ _ Γ₂ _ eqΓ (≰⇒> l>n)

  ↦∈-weaken′ : ∀ {n T Γ} →
                 env-lookup Γ n ≡ just T →
               ∀ Γ₁ Γ₂ T′ →
                 Γ ≡ Γ₁ ‣ Γ₂ →
                 env-lookup (Γ₁ ‣ T′ ! ‣ Γ₂ ⇑) (↑-idx n (length Γ₂)) ≡ just (T ↑ length Γ₂)
  ↦∈-weaken′ T∈Γ Γ₁ Γ₂ T′ eqΓ = ↦∈⇒lookup (↦∈-weaken (lookup⇒↦∈ T∈Γ) Γ₁ Γ₂ T′ eqΓ)

  <:-weakening-gen : ∀ {Γ S U} →
                        Γ ⊢ S <: U →
                      ∀ Γ₁ Γ₂ T →
                        Γ ≡ Γ₁ ‣ Γ₂ →
                        Γ₁ ‣ T ! ‣ Γ₂ ⇑ ⊢ S ↑ length Γ₂ <: U ↑ length Γ₂
  <:-weakening-gen dtop Γ₁ Γ₂ T eqΓ                    = dtop
  <:-weakening-gen dbot Γ₁ Γ₂ T eqΓ                    = dbot
  <:-weakening-gen drefl Γ₁ Γ₂ T eqΓ                   = drefl
  <:-weakening-gen (dtrans T′ S<:T′ T′<:U) Γ₁ Γ₂ T eqΓ = dtrans _
                                                                (<:-weakening-gen S<:T′ Γ₁ Γ₂ T eqΓ)
                                                                (<:-weakening-gen T′<:U Γ₁ Γ₂ T eqΓ)
  <:-weakening-gen (dbnd S′<:S U<:U′) Γ₁ Γ₂ T eqΓ      = dbnd (<:-weakening-gen S′<:S Γ₁ Γ₂ T eqΓ)
                                                              (<:-weakening-gen U<:U′ Γ₁ Γ₂ T eqΓ)
  <:-weakening-gen (dall S′<:S U<:U′) Γ₁ Γ₂ T eqΓ      = dall (<:-weakening-gen S′<:S Γ₁ Γ₂ T eqΓ)
                                                              (<:-weakening-gen U<:U′ Γ₁ (_ ∷ Γ₂) T (cong (_ ∷_) eqΓ))
  <:-weakening-gen (dsel₁ {_} {n} T∈Γ T<:B) Γ₁ Γ₂ T eqΓ
    rewrite ↑-var n (length Γ₂)                        = dsel₁ (↦∈-weaken′ T∈Γ Γ₁ Γ₂ T eqΓ)
                                                               (<:-weakening-gen T<:B Γ₁ Γ₂ T eqΓ)
  <:-weakening-gen (dsel₂ {_} {n} T∈Γ T<:B) Γ₁ Γ₂ T eqΓ
    rewrite ↑-var n (length Γ₂)                        = dsel₂ (↦∈-weaken′ T∈Γ Γ₁ Γ₂ T eqΓ)
                                                               (<:-weakening-gen T<:B Γ₁ Γ₂ T eqΓ)

  <:-weakening : ∀ {Γ₁ Γ₂ S U} T →
                    Γ₁ ‣ Γ₂ ⊢ S <: U →
                    Γ₁ ‣ T ! ‣ Γ₂ ⇑ ⊢ S ↑ length Γ₂ <: U ↑ length Γ₂
  <:-weakening T S<:U = <:-weakening-gen S<:U _ _ T refl

  <:-weakening-hd : ∀ {Γ S U} T →
                       Γ ⊢ S <: U →
                       Γ ‣ T ! ⊢ S ↑ 0 <: U ↑ 0
  <:-weakening-hd T = <:-weakening {Γ₂ = []} T

  -- narrowing
  infix 4 _≺:[_]_
  data _≺:[_]_ : Env → ℕ → Env → Set where
    ≺[_,_] : ∀ {Γ U} S → Γ ⊢ S <: U → Γ ‣ S ! ≺:[ 0 ] Γ ‣ U !
    _∷_    : ∀ {Γ₁ n Γ₂} T → Γ₁ ≺:[ n ] Γ₂ → Γ₁ ‣ T ! ≺:[ suc n ] Γ₂ ‣ T !

  <:∈-find : ∀ {x T Γ Γ′ n} →
               x ↦ T ∈ Γ →
               Γ′ ≺:[ n ] Γ →
               x ≡ n × (∃ λ T′ → n ↦ T′ ∈ Γ′ × Γ′ ⊢ T′ <: T) ⊎ x ≢ n × x ↦ T ∈ Γ′
  <:∈-find hd ≺[ T′ , T′<:T ]           = inj₁ (refl , T′ ↑ 0 , hd , <:-weakening-hd T′ T′<:T)
  <:∈-find hd (T ∷ Γ′≺:Γ)               = inj₂ ((λ ()) , hd)
  <:∈-find (tl T∈Γ) ≺[ T′ , T′<:T ]     = inj₂ ((λ ()) , tl T∈Γ)
  <:∈-find (tl T∈Γ) (S ∷ Γ′≺:Γ) with <:∈-find T∈Γ Γ′≺:Γ
  ... | inj₁ (x≡n , T′ , T′∈Γ′ , T′<:T) = inj₁ (cong suc x≡n , T′ ↑ 0 , tl T′∈Γ′ , <:-weakening-hd S T′<:T)
  ... | inj₂ (x≢n , T∈Γ′)               = inj₂ (x≢n ∘ suc-injective , tl T∈Γ′)

  <:∈-find′ : ∀ {x T Γ Γ′ n} →
                env-lookup Γ x ≡ just T →
                Γ′ ≺:[ n ] Γ →
                x ≡ n × (∃ λ T′ → env-lookup Γ′ n ≡ just T′ × Γ′ ⊢ T′ <: T) ⊎ x ≢ n × env-lookup Γ′ x ≡ just T
  <:∈-find′ T∈Γ Γ′≺Γ with <:∈-find (lookup⇒↦∈ T∈Γ) Γ′≺Γ
  ... | inj₁ (x≡n , T′ , T′∈Γ′ , T′<:T) = inj₁ (x≡n , T′ , ↦∈⇒lookup T′∈Γ′ , T′<:T)
  ... | inj₂ (x≢n , T∈Γ′)               = inj₂ (x≢n , ↦∈⇒lookup T∈Γ′)

  <:-narrow : ∀ {Γ Γ′ n S U T} →
                Γ ⊢ S <: U →
                Γ′ ≺:[ n ] Γ →
                env-lookup Γ n ≡ just T →
                Γ′ ⊢ S <: U
  <:-narrow dtop Γ′≺Γ T∈Γ                         = dtop
  <:-narrow dbot Γ′≺Γ T∈Γ                         = dbot
  <:-narrow drefl Γ′≺Γ T∈Γ                        = drefl
  <:-narrow (dtrans T S<:T T<:U) Γ′≺Γ T∈Γ         = dtrans T (<:-narrow S<:T Γ′≺Γ T∈Γ) (<:-narrow T<:U Γ′≺Γ T∈Γ)
  <:-narrow (dbnd S′<:S U<:U′) Γ′≺Γ T∈Γ           = dbnd (<:-narrow S′<:S Γ′≺Γ T∈Γ) (<:-narrow U<:U′ Γ′≺Γ T∈Γ)
  <:-narrow  {Γ} {Γ′} {n} (dall {S′ = S′} S′<:S U<:U′) Γ′≺Γ T∈Γ
    = dall (<:-narrow S′<:S Γ′≺Γ T∈Γ)
           (<:-narrow U<:U′ (_ ∷ Γ′≺Γ) (↦∈⇒lookup (tl {n} {T′ = S′} {Γ} (lookup⇒↦∈ T∈Γ))))
  <:-narrow (dsel₁ T′∈Γ T′<:B) Γ′≺Γ T∈Γ
    with <:∈-find′ T′∈Γ Γ′≺Γ
  ...  | inj₁ (refl , T″ , T″∈Γ′ , T″<:T)
    rewrite just-injective (trans (sym T′∈Γ) T∈Γ) = dsel₁ T″∈Γ′ (dtrans _ T″<:T (<:-narrow T′<:B Γ′≺Γ T∈Γ))
  ... | inj₂ (x≢n , T′∈Γ′)                        = dsel₁ T′∈Γ′ (<:-narrow T′<:B Γ′≺Γ T∈Γ)
  <:-narrow (dsel₂ T′∈Γ T′<:B) Γ′≺Γ T∈Γ
    with <:∈-find′ T′∈Γ Γ′≺Γ
  ...  | inj₁ (refl , T″ , T″∈Γ′ , T″<:T)
    rewrite just-injective (trans (sym T′∈Γ) T∈Γ) = dsel₂ T″∈Γ′ (dtrans _ T″<:T (<:-narrow T′<:B Γ′≺Γ T∈Γ))
  ... | inj₂ (x≢n , T′∈Γ′)                        = dsel₂ T′∈Γ′ (<:-narrow T′<:B Γ′≺Γ T∈Γ)

open Dsub hiding (<:-weakening-gen; <:-weakening; <:-weakening-hd
                 ; _≺:[_]_; ≺[_,_]; _∷_; <:∈-find; <:∈-find′; <:-narrow) public

-- materialization of inversion properties in invertible contexts
module DsubInvProperties {P : Env → Set}
                         (invertible : InvertibleEnv P) where

  module ContraEnvProperties = InvertibleProperties invertible _⊢_<:_
  open ContraEnvProperties public

  mutual
    <:⇒<:ᵢ : ∀ {Γ S U} → Γ ⊢ S <: U → P Γ → Γ ⊢ᵢ S <: U
    <:⇒<:ᵢ dtop pΓ                 = ditop
    <:⇒<:ᵢ dbot pΓ                 = dibot
    <:⇒<:ᵢ drefl pΓ                = direfl
    <:⇒<:ᵢ (dtrans T S<:T T<:U) pΓ = ditrans T (<:⇒<:ᵢ S<:T pΓ) (<:⇒<:ᵢ T<:U pΓ)
    <:⇒<:ᵢ (dbnd S′<:S U<:U′) pΓ   = dibnd (<:⇒<:ᵢ S′<:S pΓ) (<:⇒<:ᵢ U<:U′ pΓ)
    <:⇒<:ᵢ (dall S′<:S U<:U′) pΓ   = diall (<:⇒<:ᵢ S′<:S pΓ) U<:U′
    <:⇒<:ᵢ (dsel₁ T∈Γ T<:B) pΓ with sel-case T∈Γ T<:B pΓ
    ... | refl , _                 = dibot
    <:⇒<:ᵢ (dsel₂ T∈Γ T<:B) pΓ with sel-case T∈Γ T<:B pΓ
    ... | refl , U′ , refl
        with ⟨A:⟩<:⟨A:⟩ (<:⇒<:ᵢ T<:B pΓ) pΓ
    ...    | _ , U′<:U             = ditrans U′ (disel T∈Γ) U′<:U

    sel-case : ∀ {T Γ n S U} →
                 env-lookup Γ n ≡ just T →
                 Γ ⊢ T <: ⟨A: S ⋯ U ⟩ →
                 P Γ →
                 S ≡ ⊥ × ∃ λ U′ → T ≡ ⟨A: ⊥ ⋯ U′ ⟩
    sel-case {⊤} T∈Γ T<:B pΓ = case ⊤<: (<:⇒<:ᵢ T<:B pΓ) of λ ()
    sel-case {⊥} T∈Γ T<:B pΓ = ⊥-elim (no-⊥ pΓ T∈Γ)
    sel-case {n ∙A} T∈Γ T<:B pΓ
      with <:⟨A:⟩ (<:⇒<:ᵢ T<:B pΓ) pΓ
    ...  | inj₁ ()
    ...  | inj₂ (_ , _ , ())
    sel-case {Π S ∙ U} T∈Γ T<:B pΓ
      with <:⟨A:⟩ (<:⇒<:ᵢ T<:B pΓ) pΓ
    ...  | inj₁ ()
    ...  | inj₂ (_ , _ , ())
    sel-case {⟨A: S ⋯ U ⟩} T∈Γ T<:B pΓ
      rewrite ⊥-lb pΓ T∈Γ with ⟨A:⟩<:⟨A:⟩ (<:⇒<:ᵢ T<:B pΓ) pΓ
    ... | S<:⊥ , _ with <:⊥ S<:⊥ pΓ
    ...               | refl = refl , U , refl

  <:ᵢ⇒<: : ∀ {Γ S U} → Γ ⊢ᵢ S <: U → Γ ⊢ S <: U
  <:ᵢ⇒<: ditop                 = dtop
  <:ᵢ⇒<: dibot                 = dbot
  <:ᵢ⇒<: direfl                = drefl
  <:ᵢ⇒<: (ditrans T S<:T T<:U) = dtrans T (<:ᵢ⇒<: S<:T) (<:ᵢ⇒<: T<:U)
  <:ᵢ⇒<: (dibnd S′<:S U<:U′)   = dbnd (<:ᵢ⇒<: S′<:S) (<:ᵢ⇒<: U<:U′)
  <:ᵢ⇒<: (diall S′<:S U<:U′)   = dall (<:ᵢ⇒<: S′<:S) U<:U′
  <:ᵢ⇒<: (disel T∈Γ)           = dsel₂ T∈Γ drefl

  ⊤<:′ : ∀ {Γ T} → Γ ⊢ ⊤ <: T → P Γ → T ≡ ⊤
  ⊤<:′ ⊤<:T = ⊤<: ∘ <:⇒<:ᵢ ⊤<:T

  <:⊥′ : ∀ {Γ T} → Γ ⊢ T <: ⊥ → P Γ → T ≡ ⊥
  <:⊥′ T<:⊥ pΓ = <:⊥ (<:⇒<:ᵢ T<:⊥ pΓ) pΓ

  ⟨A:⟩<:⟨A:⟩′ : ∀ {Γ S′ U U′} → Γ ⊢ ⟨A: ⊥ ⋯ U ⟩ <: ⟨A: S′ ⋯ U′ ⟩ → P Γ →
                        S′ ≡ ⊥
  ⟨A:⟩<:⟨A:⟩′ B<:B′ pΓ with ⟨A:⟩<:⟨A:⟩ (<:⇒<:ᵢ B<:B′ pΓ) pΓ
  ... | S<:⊥ , _ = <:⊥ S<:⊥ pΓ

  Π<:⟨A:⟩⇒⊥ : ∀ {Γ S U S′ U′} → Γ ⊢ᵢ Π S ∙ U <: ⟨A: S′ ⋯ U′ ⟩ → P Γ → False
  Π<:⟨A:⟩⇒⊥ Π<:⟨A:⟩ eΓ with <:⟨A:⟩ Π<:⟨A:⟩ eΓ
  ... | inj₁ ()
  ... | inj₂ (_ , _ , ())

  ∙A<:⟨A:⟩⇒⊥ : ∀ {Γ x S U} → Γ ⊢ᵢ x ∙A <: ⟨A: S ⋯ U ⟩ → P Γ → False
  ∙A<:⟨A:⟩⇒⊥ x∙A<:⟨A:⟩ eΓ with <:⟨A:⟩ x∙A<:⟨A:⟩ eΓ
  ... | inj₁ ()
  ... | inj₂ (_ , _ , ())

  Π<:Π : ∀ {Γ S U S′ U′} →
            Γ ⊢ Π S ∙ U <: Π S′ ∙ U′ →
            P Γ →
            Γ ⊢ S′ <: S × (S′ ∷ Γ) ⊢ U <: U′
  Π<:Π <: pΓ = Σ.map₁ <:ᵢ⇒<: $ helper (<:⇒<:ᵢ <: pΓ) pΓ
    where helper : ∀ {Γ S U S′ U′} →
                     Γ ⊢ᵢ Π S ∙ U <: Π S′ ∙ U′ →
                     P Γ →
                     Γ ⊢ᵢ S′ <: S × (S′ ∷ Γ) ⊢ U <: U′
          helper direfl pΓ                           = direfl , drefl
          helper (ditrans T <: <:′) pΓ with Π<: <:
          ... | inj₁ refl                            = case ⊤<: <:′ of λ ()
          ... | inj₂ (_ , _ , refl)
              with helper <: pΓ    | helper <:′ pΓ
          ...    | S″<:S′ , U′<:U″ | S‴<:S″ , U″<:U‴ = ditrans _ S‴<:S″ S″<:S′
                                                     , dtrans _ (Dsub.<:-narrow U′<:U″ Dsub.≺[ _ , <:ᵢ⇒<: S‴<:S″ ] refl) U″<:U‴
          helper (diall <: U<:U′) pΓ                 = <: , U<:U′


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

syntax Sum | S

type
  _⊕_ : 2-ary | l30

term
  inl  : α  ->  α ⊕ β
  inr  : β  ->  α ⊕ β
  case : α ⊕ β  α.γ  β.γ  ->  γ

theory
  (lβ) a : α   f : α.γ  g : β.γ |> case (inl(a), x.f[x], y.g[y])      = f[a]
  (rβ) b : β   f : α.γ  g : β.γ |> case (inr(b), x.f[x], y.g[y])      = g[b]
  (cη) s : α ⊕ β  c : (α ⊕ β).γ |> case (s, x.c[inl(x)], y.c[inr(y)]) = c[s]
-}

module Sum.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Sum.Signature
open import Sum.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution S:Syn
open import SOAS.Metatheory.SecondOrder.Equality S:Syn

private
  variable
    α β γ τ : ST
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ S) α Γ → (𝔐 ▷ S) α Γ → Set where
  lβ : ⁅ α ⁆ ⁅ α ⊩ γ ⁆ ⁅ β ⊩ γ ⁆̣ ▹ ∅ ⊢   case (inl 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩) ≋ₐ 𝔟⟨ 𝔞 ⟩
  rβ : ⁅ β ⁆ ⁅ α ⊩ γ ⁆ ⁅ β ⊩ γ ⁆̣ ▹ ∅ ⊢   case (inr 𝔞) (𝔟⟨ x₀ ⟩) (𝔠⟨ x₀ ⟩) ≋ₐ 𝔠⟨ 𝔞 ⟩
  cη : ⁅ α ⊕ β ⁆ ⁅ (α ⊕ β) ⊩ γ ⁆̣ ▹ ∅ ⊢ case 𝔞 (𝔟⟨ inl x₀ ⟩) (𝔟⟨ inr x₀ ⟩) ≋ₐ 𝔟⟨ 𝔞 ⟩

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
open import Relation.Binary.Core

module BBHeap.Subtyping {A : Set}
                  (_≤_ : A → A → Set)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Bound.Lower.Order.Properties _≤_ trans≤

subtyping : {b b' : Bound} → LeB b' b → BBHeap b → BBHeap b'
subtyping _ leaf = leaf
subtyping b'≤b (left b≤x l⋘r) = left (transLeB b'≤b b≤x) l⋘r
subtyping b'≤b (right b≤x l⋙r) = right (transLeB b'≤b b≤x) l⋙r

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Andreas, 2016-12-22, issue #2354
-- Interaction between size solver, constraint solver, and instance search.

-- The instance search fails initially because of a non rigid meta.
-- Before freezing, there is another attempt.
-- The instance search succeeds and instantiates the meta for M.
-- Then, a size constraint is solved which had blocked a term.
-- Finally the blocking constraint can be resolved.

-- Thus, we need to
-- * wake constraints
-- * solve size constraints
-- * wake constraints again.
-- In principle, there could be many alternations needed!?

-- {-# OPTIONS -v tc.meta:30 -v tc.instance:30 -v tc.constr:50 -v tc.size:30 -v tc.decl:10 #-}
-- {-# OPTIONS -v tc.instance:30 -v tc.decl:20 #-}
-- {-# OPTIONS -v tc.instance.rigid:100 -v tc.instance:70 -v tc.size:30 #-}
-- {-# OPTIONS -v tc.term.con:50 #-}

{-# BUILTIN SIZEUNIV SizeU #-}
{-# BUILTIN SIZE     Size   #-}
{-# BUILTIN SIZELT   Size<_ #-}
{-# BUILTIN SIZESUC  ↑_     #-}
{-# BUILTIN SIZEINF  ω      #-}

record ⊤ : Set where
  constructor tt

record RawMonad (M : Set → Set) : Set₁ where
  field return : ∀{A} → A → M A

mutual
  data Delay (i : Size) (A : Set) : Set where
    now : A → Delay i A
    later : Delay∞ i A → Delay i A

  record Delay∞ (i : Size) (A : Set) : Set where
    coinductive
    field force : ∀ {j : Size< i} → Delay j A

instance
  RawMonad-Delay : ∀ {i} → RawMonad (Delay i)
  RawMonad-Delay = record
    { return = Delay.now
    }

open RawMonad {{...}}

test : ∀ {i} → Delay i ⊤
test {i} = return tt  -- Solution: return {{RawMonad-Delay {i}}} tt

-- Should find solution!

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}
module TermByFunctionNames where

open import OscarPrelude
open import VariableName
open import FunctionName

data TermByFunctionNames : Nat → Set
 where
  variable : VariableName → TermByFunctionNames zero
  function : FunctionName → {arity : Nat} → (τs : Vec (Σ Nat TermByFunctionNames) arity) → {n : Nat} → n ≡ sum (vecToList $ (fst <$> τs)) → TermByFunctionNames (suc n)

mutual
  eqTermByFunctionNames : ∀ {n} → (x y : TermByFunctionNames n) → Dec (x ≡ y)
  eqTermByFunctionNames = {!!}
{-
  eqTermByFunctionNames : ∀ {n} → (x y : TermByFunctionNames n) → Dec (x ≡ y)
  eqTermByFunctionNames {.0} (variable x) (variable x₁) = {!!}
  eqTermByFunctionNames {.(suc n)} (function x {arity = arity₁} τs {n = n} x₁) (function x₂ {arity = arity₂} τs₁ {n = .n} x₃) with x ≟ x₂ | arity₁ ≟ arity₂
  eqTermByFunctionNames {.(suc n)} (function x {arity₁} τs {n} x₄) (function .x {.arity₁} τs₁ {.n} x₅) | yes refl | (yes refl) with eqTermByFunctionNamess τs τs₁
  eqTermByFunctionNames {.(suc n)} (function x₁ {arity₁} τs {n} x₄) (function .x₁ {.arity₁} .τs {.n} x₅) | yes refl | (yes refl) | (yes refl) rewrite x₄ | x₅ = yes refl
  eqTermByFunctionNames {.(suc n)} (function x₁ {arity₁} τs {n} x₄) (function .x₁ {.arity₁} τs₁ {.n} x₅) | yes refl | (yes refl) | (no x) = {!!}
  eqTermByFunctionNames {.(suc n)} (function x {arity₁} τs {n} x₄) (function x₂ {arity₂} τs₁ {.n} x₅) | yes x₁ | (no x₃) = {!!}
  eqTermByFunctionNames {.(suc n)} (function x {arity₁} τs {n} x₄) (function x₂ {arity₂} τs₁ {.n} x₅) | no x₁ | (yes x₃) = {!!}
  eqTermByFunctionNames {.(suc n)} (function x {arity₁} τs {n} x₄) (function x₂ {arity₂} τs₁ {.n} x₅) | no x₁ | (no x₃) = {!!}
-}
  eqTermByFunctionNamess : ∀ {n} → (x y : Vec (Σ Nat TermByFunctionNames) n) → Dec (x ≡ y)
  eqTermByFunctionNamess {.0} [] [] = {!!}
  eqTermByFunctionNamess (_∷_ {n = n} (fst₁ , snd₁) x₁) (_∷_ {n = .n} (fst₂ , snd₂) y) with fst₁ ≟ fst₂
  eqTermByFunctionNamess (_∷_ {n = n} (fst₁ , snd₁) x₁) (_∷_ {n = .n} (fst₂ , snd₂) y) | yes refl with eqTermByFunctionNames snd₁ snd₂
  eqTermByFunctionNamess (_∷_ {n = n} (fst₁ , snd₁) x₁) (_∷_ {n = .n} (fst₂ , snd₂) y) | yes refl | yes refl with eqTermByFunctionNamess x₁ y
  eqTermByFunctionNamess (_∷_ {n = n} (fst₁ , snd₁) x₁) (_∷_ {n = .n} (fst₂ , snd₂) y) | yes refl | yes refl | yes refl = yes refl
  eqTermByFunctionNamess (_∷_ {n = n} (fst₁ , snd₁) x₁) (_∷_ {n = .n} (fst₂ , snd₂) y) | yes refl | yes refl | no ref = {!!}
  eqTermByFunctionNamess (_∷_ {n = n} (fst₁ , snd₁) x₁) (_∷_ {n = .n} (fst₂ , snd₂) y) | yes refl | no ref = {!!}
  eqTermByFunctionNamess (_∷_ {n = n} (fst₁ , snd₁) x₁) (_∷_ {n = .n} (fst₂ , snd₂) y) | no ref = {!!}

instance EqTermByFunctionNames : ∀ {n} → Eq (TermByFunctionNames n)
Eq._==_ EqTermByFunctionNames = eqTermByFunctionNames

{-
instance EqTermByFunctionNames : ∀ {n} → Eq (TermByFunctionNames n)
Eq._==_ EqTermByFunctionNames (variable x) (variable x₁) = {!!}
Eq._==_ EqTermByFunctionNames (function x {arity = arity₁} τs {n = n} x₁) (function x₂ {arity = arity₂} τs₁ {n = .n} x₃) with x ≟ x₂ | arity₁ ≟ arity₂
Eq._==_ EqTermByFunctionNames (function x {arity₁} τs {n} x₄) (function .x {.arity₁} τs₁ {.n} x₅) | yes refl | (yes refl) with τs ≟ τs₁
Eq._==_ EqTermByFunctionNames (function x {arity₁} τs {n} x₄) (function .x {.arity₁} τs₁ {.n} x₅) | yes refl | (yes refl) | τs≡τs₁ = {!!}
Eq._==_ EqTermByFunctionNames (function x {arity₁} τs {n} x₄) (function x₂ {arity₂} τs₁ {.n} x₅) | yes x₁ | (no x₃) = {!!}
Eq._==_ EqTermByFunctionNames (function x {arity₁} τs {n} x₄) (function x₂ {arity₂} τs₁ {.n} x₅) | no x₁ | (yes x₃) = {!!}
Eq._==_ EqTermByFunctionNames (function x {arity₁} τs {n} x₄) (function x₂ {arity₂} τs₁ {.n} x₅) | no x₁ | (no x₃) = {!!}
-}


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.RingStructure.CohomologyRing where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport

open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_)
open import Cubical.Data.Sum

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring

open import Cubical.Algebra.DirectSum.Base
open import Cubical.Algebra.AbGroup.Instances.DirectSum

open import Cubical.HITs.SetTruncation as ST

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.GradedCommutativity

private variable
  ℓ ℓ' : Level

open Iso

-----------------------------------------------------------------------------
-- Definition Cohomology Ring

module intermediate-def where
  H*AbGr : (A : Type ℓ) → AbGroup ℓ
  H*AbGr A = ⊕-AbGr ℕ (λ n → coHom n A) (λ n → snd (coHomGroup n A))

  H* : (A : Type ℓ) → Type ℓ
  H* A = fst (H*AbGr A)

module CupRingProperties (A : Type ℓ) where
  open intermediate-def
  open AbGroupStr (snd (H*AbGr A))
  open AbGroupTheory (H*AbGr A)

  _cup_ : H* A → H* A → H* A
  _cup_ = DS-Rec-Set.f ℕ (λ n → coHom n A) (λ n → snd (coHomGroup n A))
          (H* A → H* A)
          (λ f g p q i j x → is-set (f x) (g x) (λ X → p X x) (λ X → q X x) i j)
          -- elements
          (λ x → 0g)
          (λ n a → DS-Rec-Set.f ℕ _ _ (H* A) is-set
                    -- elements
                    0g
                    (λ m b → base (n +' m) (a ⌣ b))
                    _+_
                    -- equations
                    assoc
                    rid
                    comm
                    (λ m → (cong (base (n +' m)) (⌣-0ₕ n m a)) ∙ (base-neutral (n +' m)))
                    λ m b c → base-add (n +' m) (a ⌣ b) (a ⌣ c) ∙ cong (base (n +' m)) (sym (leftDistr-⌣ n m a b c)))
          (λ U V y → (U y) + (V y))
          -- equations
          (λ xs ys zs i y → assoc (xs y) (ys y) (zs y) i)
          (λ xs i y       → rid (xs y) i)
          (λ xs ys i y    → comm (xs y) (ys y) i)
          (λ n → funExt(
                  DS-Ind-Prop.f ℕ _ _ _ (λ _ → is-set _ _)
                  refl
                  (λ m b → cong (base (n +' m)) (0ₕ-⌣ n m b) ∙ base-neutral (n +' m))
                  λ {U V} ind-U ind-V → (cong₂ _+_ ind-U ind-V) ∙ (rid 0g)))
          λ n a b → funExt (
                     DS-Ind-Prop.f ℕ _ _ _ (λ _ → is-set _ _)
                     (rid 0g)
                     (λ m c → (base-add (n +' m) (a ⌣ c) (b ⌣ c)) ∙ (cong (base (n +' m)) (sym (rightDistr-⌣ n m a b c))))
                     λ {U V} ind-U ind-V → comm-4 _ _ _ _ ∙ cong₂ _+_ ind-U ind-V)

  1H* : H* A
  1H* = base 0 1⌣

  cupAssoc : (x y z : H* A) → x cup (y cup z) ≡ (x cup y) cup z
  cupAssoc = DS-Ind-Prop.f ℕ _ _ _
              (λ x p q i y z j → is-set _ _ (p y z) (q y z) i j)
              (λ y z → refl)
              (λ n a → DS-Ind-Prop.f ℕ _ _ _
                        (λ y p q i z j → is-set _ _ (p z) (q z) i j)
                        (λ z → refl)
                        (λ m b → DS-Ind-Prop.f ℕ _ _ _ (λ _ → is-set _ _)
                                  refl
                                  (λ k c → (cong (base (n +' (m +' k))) (assoc-⌣ n m k a b c))
                                             ∙ sym (constSubstCommSlice (λ n → coHom n A) (H* A) base (sym (+'-assoc n m k)) ((a ⌣ b) ⌣ c)))
                                  λ {U V} ind-U ind-V → cong₂ _+_ ind-U ind-V)
                        λ {U V} ind-U ind-V z → cong₂ _+_ (ind-U z) (ind-V z))
              λ {U V} ind-U ind-V y z → cong₂ _+_ (ind-U y z) (ind-V y z)

  cupIdR : (x : H* A) → x cup 1H* ≡ x
  cupIdR = DS-Ind-Prop.f ℕ _ _ _ (λ _ → is-set _ _)
            refl
            (λ n a → (cong (base (n +' 0)) (lUnit⌣ n a)) ∙ sym (constSubstCommSlice (λ n → coHom n A) (H* A) base (sym (n+'0 n)) a))
            λ {U V} ind-U ind-V → (cong₂ _+_ ind-U ind-V)

  cupIdL : (x : H* A) → 1H* cup x ≡ x
  cupIdL = DS-Ind-Prop.f ℕ _ _ _ (λ _ → is-set _ _)
            refl
            (λ n a → cong (base n) (rUnit⌣ n a))
            (λ {U V} ind-U ind-V → cong₂ _+_ ind-U ind-V)

  cupDistR : (x y z : H* A) → x cup (y + z) ≡ (x cup y) + (x cup z)
  cupDistR = DS-Ind-Prop.f ℕ _ _ _
               (λ x p q i y z j → is-set _ _ (p y z) (q y z) i j)
               (λ y z → sym (rid 0g))
               (λ n a y z → refl)
               λ {U V} ind-U ind-V y z → cong₂ _+_ (ind-U y z) (ind-V y z) ∙ comm-4 (U cup y) (U cup z) (V cup y) (V cup z)

  cupDistL : (x y z : H* A) → (x + y) cup z ≡ (x cup z) + (y cup z)
  cupDistL = λ x y z → refl

-----------------------------------------------------------------------------
-- Graded Comutative Ring

  -- def + commutation with base
  -^-gen : (n m : ℕ) → (p : isEvenT n ⊎ isOddT n) → (q : isEvenT m ⊎ isOddT m)
          → H* A → H* A
  -^-gen n m (inl p)      q  x = x
  -^-gen n m (inr p) (inl q) x = x
  -^-gen n m (inr p) (inr q) x = - x

  -^_·_ : (n m : ℕ) → H* A → H* A
  -^_·_ n m x = -^-gen n m (evenOrOdd n) (evenOrOdd m) x

  -^-gen-base : {k : ℕ} → (n m : ℕ) → (p : isEvenT n ⊎ isOddT n) → (q : isEvenT m ⊎ isOddT m)
              (a : coHom k A) → -^-gen n m p q (base k a) ≡ base k (-ₕ^-gen n m p q a)
  -^-gen-base n m (inl p) q a = refl
  -^-gen-base n m (inr p) (inl q) a = refl
  -^-gen-base n m (inr p) (inr q) a = refl

  -^-base : {k : ℕ} → (n m : ℕ) → (a : coHom k A) → (-^ n · m) (base k a) ≡ base k ((-ₕ^ n · m) a)
  -^-base n m a = -^-gen-base n m (evenOrOdd n) (evenOrOdd m) a

module _ (A : Type ℓ) where
  open intermediate-def renaming (H* to H*')
  open CupRingProperties A
  open AbGroupStr (snd (H*AbGr A))
  open AbGroupTheory (H*AbGr A)

  H*R : Ring ℓ
  fst H*R = H*' A
  RingStr.0r (snd H*R) = 0g
  RingStr.1r (snd H*R) = 1H*
  RingStr._+_ (snd H*R) = _+_
  RingStr._·_ (snd H*R) = _cup_
  RingStr.- snd H*R = -_
  RingStr.isRing (snd H*R) = makeIsRing is-set
                                        assoc rid (λ x → fst (inverse x)) comm
                                        cupAssoc cupIdR cupIdL cupDistR cupDistL

  H* : Type ℓ
  H* = fst H*R

  gradCommRing : (n m : ℕ) → (a : coHom n A) → (b : coHom m A) →
                 (base n a) cup (base m b) ≡ (-^ n · m) ((base m b) cup (base n a))
  gradCommRing n m a b = base (n +' m) (a ⌣ b)
                                 ≡⟨ cong (base (n +' m)) (gradedComm-⌣ n m a b) ⟩
                        base (n +' m) ((-ₕ^ n · m) (subst (λ n₁ → coHom n₁ A) (+'-comm m n) (b ⌣ a)))
                                 ≡⟨ sym (-^-base n m (subst (λ k → coHom k A) (+'-comm m n) (b ⌣ a))) ⟩
                        (-^ n · m)  (base (n +' m) (subst (λ k → coHom k A) (+'-comm m n) (b ⌣ a)))
                                 ≡⟨ cong (-^ n · m) (sym (constSubstCommSlice (λ k → coHom k A) H* base (+'-comm m n) (b ⌣ a))) ⟩
                         (-^ n · m) (base (m +' n) (b ⌣ a)) ∎

-----------------------------------------------------------------------------
-- Equivalence of Type implies equivalence of Cohomology Ring

module CohomologyRing-Equiv
  {X : Type ℓ}
  {Y : Type ℓ'}
  (e : Iso X Y)
  where

  open IsGroupHom

  open RingStr (snd (H*R X)) using ()
    renaming
    ( 0r        to 0H*X
    ; 1r        to 1H*X
    ; _+_       to _+H*X_
    ; -_        to -H*X_
    ; _·_       to _cupX_
    ; +Assoc    to +H*XAssoc
    ; +Identity to +H*XIdentity
    ; +Lid      to +H*XLid
    ; +Rid      to +H*XRid
    ; +Inv      to +H*XInv
    ; +Linv     to +H*XLinv
    ; +Rinv     to +H*XRinv
    ; +Comm     to +H*XComm
    ; ·Assoc    to ·H*XAssoc
    ; ·Identity to ·H*XIdentity
    ; ·Lid      to ·H*XLid
    ; ·Rid      to ·H*XRid
    ; ·Rdist+   to ·H*XRdist+
    ; ·Ldist+   to ·H*XLdist+
    ; is-set    to isSetH*X     )

  open RingStr (snd (H*R Y)) using ()
    renaming
    ( 0r        to 0H*Y
    ; 1r        to 1H*Y
    ; _+_       to _+H*Y_
    ; -_        to -H*Y_
    ; _·_       to _cupY_
    ; +Assoc    to +H*YAssoc
    ; +Identity to +H*YIdentity
    ; +Lid      to +H*YLid
    ; +Rid      to +H*YRid
    ; +Inv      to +H*YInv
    ; +Linv     to +H*YLinv
    ; +Rinv     to +H*YRinv
    ; +Comm     to +H*YComm
    ; ·Assoc    to ·H*YAssoc
    ; ·Identity to ·H*YIdentity
    ; ·Lid      to ·H*YLid
    ; ·Rid      to ·H*YRid
    ; ·Rdist+   to ·H*YRdist+
    ; ·Ldist+   to ·H*YLdist+
    ; is-set    to isSetH*Y     )

  coHomGr-Iso : {n : ℕ} → GroupIso (coHomGr n X) (coHomGr n Y)
  fst (coHomGr-Iso {n}) = is
    where
    is : Iso (coHom n X) (coHom n Y)
    fun is = ST.rec squash₂ (λ f → ∣ (λ y → f (inv e y)) ∣₂)
    inv is = ST.rec squash₂ (λ g → ∣ (λ x → g (fun e x)) ∣₂)
    rightInv is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ f → cong ∣_∣₂ (funExt (λ y → cong f (rightInv e y))))
    leftInv is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ g → cong ∣_∣₂ (funExt (λ x → cong g (leftInv e x))))
  snd (coHomGr-Iso {n}) = makeIsGroupHom
                                        (ST.elim (λ _ → isProp→isSet λ u v i y → squash₂ _ _ (u y) (v y) i)
                                        (λ f → ST.elim (λ _ → isProp→isSet (squash₂ _ _))
                                        (λ f' → refl)))

  H*-X→H*-Y : H* X → H* Y
  H*-X→H*-Y = DS-Rec-Set.f _ _ _ _ isSetH*Y
               0H*Y
               (λ n a → base n (fun (fst coHomGr-Iso) a))
               _+H*Y_
               +H*YAssoc
               +H*YRid
               +H*YComm
               (λ n → cong (base n) (pres1 (snd coHomGr-Iso)) ∙ base-neutral n)
               λ n a b → base-add _ _ _ ∙ cong (base n) (sym (pres· (snd coHomGr-Iso) a b))

  H*-Y→H*-X : H* Y → H* X
  H*-Y→H*-X = DS-Rec-Set.f _ _ _ _ isSetH*X
               0H*X
               (λ m a → base m (inv (fst coHomGr-Iso) a))
               _+H*X_
               +H*XAssoc
               +H*XRid
               +H*XComm
               (λ m → cong (base m) (pres1 (snd (invGroupIso coHomGr-Iso))) ∙ base-neutral m)
               λ m a b → base-add _ _ _ ∙ cong (base m) (sym (pres· (snd (invGroupIso coHomGr-Iso)) a b))

  e-sect : (y : H* Y) → H*-X→H*-Y (H*-Y→H*-X y) ≡ y
  e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*Y _ _)
           refl
           (λ m a → cong (base m) (rightInv (fst coHomGr-Iso) a))
           (λ {U V} ind-U ind-V → cong₂ _+H*Y_ ind-U ind-V)

  e-retr : (x : H* X) → H*-Y→H*-X (H*-X→H*-Y x) ≡ x
  e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*X _ _)
           refl
           (λ n a → cong (base n) (leftInv (fst coHomGr-Iso) a))
           (λ {U V} ind-U ind-V → cong₂ _+H*X_ ind-U ind-V)

  H*-X→H*-Y-pres1 : H*-X→H*-Y 1H*X ≡ 1H*Y
  H*-X→H*-Y-pres1 = refl

  H*-X→H*-Y-pres+ : (x x' : H* X) → H*-X→H*-Y (x +H*X x') ≡ H*-X→H*-Y x +H*Y H*-X→H*-Y x'
  H*-X→H*-Y-pres+ x x' = refl

  H*-X→H*-Y-pres· : (x x' : H* X) → H*-X→H*-Y (x cupX x') ≡ H*-X→H*-Y x cupY H*-X→H*-Y x'
  H*-X→H*-Y-pres· = DS-Ind-Prop.f _ _ _ _ (λ x u v i y → isSetH*Y _ _ (u y) (v y) i)
         (λ _ → refl)
         (λ n → ST.elim (λ x → isProp→isSet λ u v i y → isSetH*Y _ _ (u y) (v y) i)
                (λ f → DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*Y _ _)
                        refl
                        (λ m → ST.elim (λ _ → isProp→isSet (isSetH*Y _ _))
                                (λ g → refl))
                        λ {U V} ind-U ind-V → cong₂ _+H*Y_ ind-U ind-V) )
         (λ {U V} ind-U ind-V y → cong₂ _+H*Y_ (ind-U y) (ind-V y))

module _
  {X : Type ℓ}
  {Y : Type ℓ'}
  (e : Iso X Y)
  where

  open CohomologyRing-Equiv e

  CohomologyRing-Equiv : RingEquiv (H*R X) (H*R Y)
  fst CohomologyRing-Equiv = isoToEquiv is
    where
    is : Iso (H* X) (H* Y)
    fun is = H*-X→H*-Y
    inv is = H*-Y→H*-X
    rightInv is = e-sect
    leftInv is = e-retr
  snd CohomologyRing-Equiv = makeIsRingHom H*-X→H*-Y-pres1 H*-X→H*-Y-pres+ H*-X→H*-Y-pres·

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
module Setoid where

module Logic where

  infix 4 _/\_
  -- infix 2 _\/_

  data True : Set where
    tt : True

  data False : Set where

  data _/\_ (P Q : Set) : Set where
    andI : P -> Q -> P /\ Q

--   Not allowed if we have proof irrelevance
--   data _\/_ (P Q : Set) : Set where
--     orIL : P -> P \/ Q
--     orIR : Q -> P \/ Q

module Setoid where

  data Setoid : Set1 where
    setoid : (A     : Set)
          -> (_==_  : A -> A -> Set)
          -> (refl  : (x : A) -> x == x)
          -> (sym   : (x y : A) -> x == y -> y == x)
          -> (trans : (x y z : A) -> x == y -> y == z -> x == z)
          -> Setoid

  El : Setoid -> Set
  El (setoid A _ _ _ _) = A

  module Projections where

    eq : (A : Setoid) -> El A -> El A -> Set
    eq (setoid _ e _ _ _) = e

    refl : (A : Setoid) -> {x : El A} -> eq A x x
    refl (setoid _ _ r _ _) = r _

    sym : (A : Setoid) -> {x y : El A} -> (h : eq A x y) -> eq A y x
    sym (setoid _ _ _ s _) = s _ _

    trans : (A : Setoid) -> {x y z : El A} -> eq A x y -> eq A y z -> eq A x z
    trans (setoid _ _ _ _ t) = t _ _ _

  module Equality (A : Setoid) where

    infix 6 _==_

    _==_ : El A -> El A -> Set
    _==_ = Projections.eq A

    refl : {x : El A} -> x == x
    refl = Projections.refl A

    sym : {x y : El A} -> x == y -> y == x
    sym = Projections.sym A

    trans : {x y z : El A} -> x == y -> y == z -> x == z
    trans = Projections.trans A

module EqChain (A : Setoid.Setoid) where

  infixl 5 _===_ _=-=_
  infix  8 _since_

  open Setoid
  private open module EqA = Equality A

  eqProof>_ : (x : El A) -> x == x
  eqProof> x = refl

  _=-=_ : (x : El A) -> {y : El A} -> x == y -> x == y
  x =-= eq = eq

  _===_ : {x y z : El A} -> x == y -> y == z -> x == z
  _===_ = trans

  _since_ : {x : El A} -> (y : El A) -> x == y -> x == y
  _ since eq = eq

module Fun where

  open Logic
  open Setoid

  infixr 10 _=>_ _==>_

  open Setoid.Projections using (eq)

  data _=>_ (A B : Setoid) : Set where
    lam : (f : El A -> El B)
       -> ({x y : El A} -> eq A x y
                         -> eq B (f x) (f y)
          )
       -> A => B

  app : {A B : Setoid} -> (A => B) -> El A -> El B
  app (lam f _) = f

  cong : {A B : Setoid} -> (f : A => B) -> {x y : El A} ->
         eq A x y -> eq B (app f x) (app f y)
  cong (lam _ resp) = resp

  data EqFun {A B : Setoid}(f g : A => B) : Set where
    eqFunI : ({x y : El A} -> eq A x y -> eq B (app f x) (app g y)) ->
             EqFun f g

  eqFunE : {A B : Setoid} -> {f g : A => B} -> {x y : El A} ->
           EqFun f g -> eq A x y -> eq B (app f x) (app g y)
  eqFunE (eqFunI h) = h

  _==>_ : Setoid -> Setoid -> Setoid
  A ==> B = setoid (A => B) EqFun r s t
    where
      module Proof where
        open module EqChainB = EqChain B
        module EqA = Equality A
        open module EqB = Equality B

        -- either abstract or --proof-irrelevance needed
        -- (we don't want to compare the proofs for equality)
        -- abstract
        r : (f : A => B) -> EqFun f f
        r f = eqFunI (\xy -> cong f xy)

        s : (f g : A => B) -> EqFun f g -> EqFun g f
        s f g fg =
          eqFunI (\{x}{y} xy ->
            app g x =-= app g y  since  cong g xy
                    === app f x  since  sym (eqFunE fg xy)
                    === app f y  since  cong f xy
          )

        t : (f g h : A => B) -> EqFun f g -> EqFun g h -> EqFun f h
        t f g h fg gh =
          eqFunI (\{x}{y} xy ->
            app f x =-= app g y  since  eqFunE fg xy
                    === app g x  since  cong g (EqA.sym xy)
                    === app h y  since  eqFunE gh xy
          )
      open Proof

  infixl 100 _$_
  _$_ : {A B : Setoid} -> El (A ==> B) -> El A -> El B
  _$_ = app

  lam2 : {A B C : Setoid} ->
         (f : El A -> El B -> El C) ->
         ({x x' : El A} -> eq A x x' ->
          {y y' : El B} -> eq B y y' -> eq C (f x y) (f x' y')
         ) -> El (A ==> B ==> C)
  lam2 {A} f h = lam (\x -> lam (\y -> f x y)
                                (\y -> h EqA.refl y))
                     (\x -> eqFunI (\y -> h x y))
    where
      module EqA = Equality A

  lam3 : {A B C D : Setoid} ->
         (f : El A -> El B -> El C -> El D) ->
         ({x x' : El A} -> eq A x x' ->
          {y y' : El B} -> eq B y y' ->
          {z z' : El C} -> eq C z z' -> eq D (f x y z) (f x' y' z')
         ) -> El (A ==> B ==> C ==> D)
  lam3 {A} f h =
    lam (\x -> lam2 (\y z -> f x y z)
                    (\y z -> h EqA.refl y z))
        (\x -> eqFunI (\y -> eqFunI (\z -> h x y z)))
    where
      module EqA = Equality A

  eta : {A B : Setoid} -> (f : El (A ==> B)) ->
        eq (A ==> B) f (lam (\x -> f $ x) (\xy -> cong f xy))
  eta f = eqFunI (\xy -> cong f xy)

  id : {A : Setoid} -> El (A ==> A)
  id = lam (\x -> x) (\x -> x)

  {- Now it looks okay. But it's incredibly slow!  Proof irrelevance makes it
     go fast again...  The problem is equality checking of (function type)
     setoids which without proof irrelevance checks equality of the proof that
     EqFun is an equivalence relation.  It's not clear why using lam3 involves
     so many more equality checks than using lam. Making the proofs abstract
     makes the problem go away.
  -}
  compose : {A B C : Setoid} -> El ((B ==> C) ==> (A ==> B) ==> (A ==> C))
  compose =
    lam3 (\f g x -> f $ (g $ x))
         (\f g x -> eqFunE f (eqFunE g x))

  _∘_ : {A B C : Setoid} -> El (B ==> C) -> El (A ==> B) -> El (A ==> C)
  f ∘ g = compose $ f $ g

  const : {A B : Setoid} -> El (A ==> B ==> A)
  const = lam2 (\x y -> x) (\x y -> x)

module Nat where

  open Logic
  open Setoid
  open Fun

  infixl 10 _+_

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

  module NatSetoid where

    eqNat : Nat -> Nat -> Set
    eqNat zero     zero   = True
    eqNat zero    (suc _) = False
    eqNat (suc _)  zero   = False
    eqNat (suc n) (suc m) = eqNat n m

    data EqNat (n m : Nat) : Set where
      eqnat : eqNat n m -> EqNat n m

    uneqnat : {n m : Nat} -> EqNat n m -> eqNat n m
    uneqnat (eqnat x) = x

    r : (x : Nat) -> eqNat x x
    r zero    = tt
    r (suc n) = r n

    -- reflexivity of EqNat
    rf : (n : Nat) -> EqNat n n
    rf = \ x -> eqnat (r x)

    s : (x y : Nat) -> eqNat x y -> eqNat y x
    s  zero    zero   _ = tt
    s (suc n) (suc m) h = s n m h
    s zero    (suc _) ()
    s (suc _) zero    ()

    -- symmetry of EqNat
    sy : (x y : Nat) -> EqNat x y -> EqNat y x
    sy = \x y h -> eqnat (s x y (uneqnat h))

    t : (x y z : Nat) -> eqNat x y -> eqNat y z -> eqNat x z
    t  zero    zero    z      xy yz = yz
    t (suc x) (suc y) (suc z) xy yz = t x y z xy yz
    t  zero   (suc _)  _      () _
    t (suc _)  zero    _      () _
    t (suc _) (suc _)  zero   _  ()

    -- transitivity of EqNat
    tr : (x y z : Nat) -> EqNat x y -> EqNat y z -> EqNat x z
    tr = \x y z xy yz -> eqnat (t x y z (uneqnat xy) (uneqnat yz))

  NAT : Setoid
  NAT = setoid Nat NatSetoid.EqNat NatSetoid.rf NatSetoid.sy NatSetoid.tr

  _+_ : Nat -> Nat -> Nat
  zero  + m = m
  suc n + m = suc (n + m)

  plus : El (NAT ==> NAT ==> NAT)
  plus = lam2 (\n m -> n + m) eqPlus
    where
      module EqNat = Equality NAT
      open EqNat
      open NatSetoid

      eqPlus : {n n' : Nat} -> n == n' -> {m m' : Nat} -> m == m' -> n + m == n' + m'
      eqPlus {zero}  {zero}    _  mm = mm
      eqPlus {suc n} {suc n'}  (eqnat nn) {m}{m'} (eqnat mm) =
        eqnat (uneqnat (eqPlus{n}{n'} (eqnat nn)
                              {m}{m'} (eqnat mm)
              )        )
      eqPlus {zero}  {suc _}  (eqnat ())  _
      eqPlus {suc _} {zero}   (eqnat ())  _

module List where

  open Logic
  open Setoid

  data List (A : Set) : Set where
    nil  : List A
    _::_ : A -> List A -> List A

  LIST : Setoid -> Setoid
  LIST A = setoid (List (El A)) eqList r s t
    where
      module EqA = Equality A
      open EqA

      eqList : List (El A) -> List (El A) -> Set
      eqList nil        nil      = True
      eqList nil       (_ :: _)  = False
      eqList (_ :: _)   nil      = False
      eqList (x :: xs) (y :: ys) = x == y /\ eqList xs ys

      r : (x : List (El A)) -> eqList x x
      r  nil      = tt
      r (x :: xs) = andI refl (r xs)

      s : (x y : List (El A)) -> eqList x y -> eqList y x
      s  nil       nil       h            = h
      s (x :: xs) (y :: ys) (andI xy xys) = andI (sym xy) (s xs ys xys)
      s  nil      (_ :: _)  ()
      s (_ :: _)   nil      ()

      t : (x y z : List (El A)) -> eqList x y -> eqList y z -> eqList x z
      t  nil       nil       zs        _             h            = h
      t (x :: xs) (y :: ys) (z :: zs) (andI xy xys) (andI yz yzs) =
        andI (trans xy yz) (t xs ys zs xys yzs)
      t  nil      (_ :: _)  _          () _
      t (_ :: _)   nil      _          () _
      t (_ :: _)  (_ :: _)  nil        _  ()

open Fun


text:
{-# OPTIONS --rewriting --confluence-check -v rewriting:80 #-}

open import Agda.Builtin.Equality

postulate
  decorate      : ∀{a} (A : Set a) → Set a
  rewriteMe     : ∀{a b} {A : Set a} {B : A → Set b}
                → decorate ((x : A) → B x) ≡ (decorate A → ∀ x → decorate (B x))

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE rewriteMe #-}

postulate A : Set

test : decorate (A → A) ≡ (decorate A → ∀ (x : A) → decorate A)
test = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module interactiveProgramsAgda where

open import NativeIO
open import Function
open import Size
open import Data.Maybe.Base

record IOInterface : Set₁ where
  field  Command  : Set
         Response : (c : Command) → Set

open IOInterface public

mutual
  record IO (I : IOInterface) (i : Size) (A : Set) : Set where
     coinductive
     constructor delay
     field force : {j : Size< i} → IO' I j A

  data IO' (I : IOInterface) (i : Size) (A : Set) : Set where
    do'     : (c : Command I) (f : Response I c → IO I i A) → IO' I i A
    return' : (a : A)                                        → IO' I i A

open IO public

module _ {I : IOInterface} (let C = Command I) (let R = Response I) where
  do  : ∀{i A} (c : C) (f : R c → IO I i A) → IO I i A
  force (do c f) = do' c f

  return : ∀{i A} (a : A) → IO I i A
  force (return a) = return' a

  infixl 2 _>>=_

  _>>=_ :  ∀{i A B} (m : IO I i A) (k : A → IO I i B) → IO I i B
  force (m >>= k) with force m
  ... | do' c f   = do' c λ x → f x >>= k
  ... | return' a = force (k a)

  {-# NON_TERMINATING #-}
  translateIO : ∀ {A} (tr : (c : C) → NativeIO (R c)) → IO I ∞ A → NativeIO A
  translateIO tr m = case (force m) of λ
     {  (do' c f)    →  (tr c) native>>= λ r → translateIO tr (f r)
     ;  (return' a)  →  nativeReturn a
     }

{- Specific case of Console IO -}

data ConsoleCommand : Set where
  getLine   :  ConsoleCommand
  putStrLn  :  String → ConsoleCommand

ConsoleResponse : ConsoleCommand → Set
ConsoleResponse  getLine      =  String
ConsoleResponse (putStrLn s)  =  Unit

ConsoleInterface : IOInterface
Command ConsoleInterface  = ConsoleCommand
Response ConsoleInterface = ConsoleResponse

IOConsole : (i : Size) → Set → Set
IOConsole i = IO ConsoleInterface i

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

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

cat   :  ∀ {i} → IOConsole i Unit
force cat =  do' getLine λ line →
             do (putStrLn line)   λ _ →
             cat

main : NativeIO Unit
main = translateIOConsole cat

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality

open import Imports.StaleMetaLiteral

macro
  unquoteMeta : Meta → Tactic
  unquoteMeta m = give (meta m [])

thm : unquoteMeta staleMeta ≡ 42
thm = refl


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

module Data.Option.Equiv.Path where

import      Lvl
open import Data
open import Data.Option
open import Data.Option.Functions
open import Data.Option.Equiv
open import Functional
open import Structure.Function.Domain
open import Structure.Operator
open import Structure.Relator
open import Type.Cubical.Path.Equality
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

instance
  Some-injectivity : Injective {B = Option(T)} (Some)
  Injective.proof Some-injectivity {x}{y} = congruence₂ₗ(_or_)(x)

instance
  Path-Option-extensionality : Extensionality{A = T} (Path-equiv)
  Extensionality.cases-inequality (Path-Option-extensionality {T = T}) {x} p with () ← substitute₁(elim{A = T}{B = λ _ → Type}(Option(T)) (const Empty)) p (Some x)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Cats.Category.Cat.Facts.Terminal where

open import Cats.Category
open import Cats.Category.Cat using (Cat)
open import Cats.Category.One using (One)

instance
  hasTerminal : ∀ lo la l≈ → HasTerminal (Cat lo la l≈)
  hasTerminal lo la l≈ = record
      { One = One lo la l≈
      ; isTerminal = _
      }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --safe #-}
module Cubical.Homotopy.WedgeConnectivity where

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.HITs.Susp
open import Cubical.HITs.Truncation as Trunc
open import Cubical.Homotopy.Connected

module WedgeConnectivity {ℓ ℓ' ℓ''} (n m : ℕ)
  (A : Pointed ℓ) (connA : isConnected (suc n) (typ A))
  (B : Pointed ℓ') (connB : isConnected (suc m) (typ B))
  (P : typ A → typ B → TypeOfHLevel ℓ'' (n + m))
  (f : (a : typ A) → P a (pt B) .fst)
  (g : (b : typ B) → P (pt A) b .fst)
  (p : f (pt A) ≡ g (pt B))
  where

  private
    Q : typ A → TypeOfHLevel _ n
    Q a =
      ( (Σ[ k ∈ ((b : typ B) → P a b .fst) ] k (pt B) ≡ f a)
      , isOfHLevelRetract n
          (λ {(h , q) → h , funExt λ _ → q})
          (λ {(h , q) → h , funExt⁻ q _})
          (λ _ → refl)
          (isOfHLevelPrecomposeConnected n m (P a) (λ _ → pt B)
            (isConnectedPoint m connB (pt B)) (λ _ → f a))
      )

    main : isContr (fiber (λ s _ → s (pt A)) (λ _ → g , p ⁻¹))
    main =
      elim.isEquivPrecompose (λ _ → pt A) n Q
        (isConnectedPoint n connA (pt A))
        .equiv-proof (λ _ → g , p ⁻¹)

  extension : ∀ a b → P a b .fst
  extension a b = main .fst .fst a .fst b

  left : ∀ a → extension a (pt B) ≡ f a
  left a = main .fst .fst a .snd

  right : ∀ b → extension (pt A) b ≡ g b
  right = funExt⁻ (cong fst (funExt⁻ (main .fst .snd) _))

  hom : left (pt A) ⁻¹ ∙ right (pt B) ≡ p
  hom i j = hcomp (λ k → λ { (i = i1) → p j
                           ; (j = i0) → (cong snd (funExt⁻ (main .fst .snd) tt)) i (~ j)
                           ; (j = i1) → right (pt B) (i ∨ k)})
                  (cong snd (funExt⁻ (main .fst .snd) tt) i (~ j))

  hom' : left (pt A) ≡ right (pt B) ∙ sym p
  hom' = (lUnit (left _) ∙ cong (_∙ left (pt A)) (sym (rCancel (right (pt B)))))
       ∙∙ sym (assoc _ _ _)
       ∙∙ cong (right (pt B) ∙_) (sym (symDistr (left (pt A) ⁻¹) (right (pt B))) ∙ (cong sym hom))

  homSquare : PathP (λ i → extension (pt A) (pt B) ≡ p i) (left (pt A)) (right (pt B))
  homSquare i j = hcomp (λ k → λ { (i = i0) → left (pt A) j
                                 ; (i = i1) → compPath-filler (right (pt B)) (sym p) (~ k) j
                                 ; (j = i0) → extension (pt A) (pt B)
                                 ; (j = i1) → p (i ∧ k) })
                        (hom' i j)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module #13 where

{-
  Using propositions-as-types, derive the double negation of the principle of excluded
  middle, i.e. prove not (not (P or not P)).
-}

open import Data.Sum
open import Relation.Nullary

excluded-middle : (P : Set) → ¬ (¬ (P ⊎ (¬ P)))
excluded-middle P z = z (inj₂ (λ x → z (inj₁ x)))

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
-- Andreas, 2015-06-24 Parsing of forall should be like lambda

open import Common.Prelude
open import Common.Product

test : ⊤ × ∀ (B : Set) → B → B  -- should parse
test = _ , λ B b → b

test1 : ⊤ × forall (B : Set) → B → B  -- should parse
test1 = _ , λ B b → b


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

open import HoTT
open import cohomology.Theory

open import cw.CW

module cw.cohomology.ZerothCohomologyGroupOnDiag {i} (OT : OrdinaryTheory i)
  (⊙skel : ⊙Skeleton {i} 0) (ac : ⊙has-cells-with-choice 0 ⊙skel i) where

open OrdinaryTheory OT
open import cw.cohomology.TipAndAugment OT ⊙skel

open import groups.KernelSndImageInl (C2 0) {H = CX₀ 0}
  {K = Lift-group {j = i} Unit-group}
  cst-hom cst-hom (λ _ → idp)
  (C2×CX₀-is-abelian 0)

open import groups.KernelImage
  (cst-hom {G = C2×CX₀ 0} {H = Lift-group {j = i} Unit-group})
  cw-coε (C2×CX₀-is-abelian 0)

C-cw-iso-ker/im : C 0 ⊙⟦ ⊙skel ⟧ ≃ᴳ Ker/Im
C-cw-iso-ker/im =
      Ker-φ-snd-quot-Im-inl
  ∘eᴳ full-subgroup (ker-cst-hom-is-full (CX₀ 0) (Lift-group {j = i} Unit-group)) ⁻¹ᴳ

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Data.Nat.Properties.Extra where

open import Data.Nat.Base
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Data.Empty

≤′-unique : ∀ {i u} (p q : i ≤′ u) → p ≡ q
≤′-unique ≤′-refl ≤′-refl = refl
≤′-unique ≤′-refl (≤′-step q) = ⊥-elim (1+n≰n (≤′⇒≤ q))
≤′-unique (≤′-step p) ≤′-refl = ⊥-elim (1+n≰n (≤′⇒≤ p))
≤′-unique (≤′-step p) (≤′-step q) = cong ≤′-step (≤′-unique p q)

m+n+o≡n+m+o : ∀ m n o → m + (n + o) ≡ n + (m + o)
m+n+o≡n+m+o m n o = begin
  m + (n + o) ≡⟨ sym (+-assoc m n o) ⟩
  (m + n) + o ≡⟨ cong (λ x → x + o) (+-comm m n) ⟩
  (n + m) + o ≡⟨ +-assoc n m o ⟩
  n + (m + o) ∎


text:
module Data.List.First {ℓ}{A : Set ℓ} where

open import Data.Product
open import Data.List
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Level
open import Function
open import Data.Empty

-- proof that an element is the first in a vector to satisfy the predicate B
data First {b}(B : A → Set b) : (x : A) → List A → Set (ℓ ⊔ b) where

  here  : ∀ {x : A} → (p : B x) → {v : List A} → First B x (x ∷ v)
  there : ∀ {x} {v : List A} (x' : A) → ¬ (B x') → First B x v → First B x (x' ∷ v)

-- get the witness of B x from the element ∈ First
first⟶witness : ∀ {B : A → Set} {x l} → First B x l → B x
first⟶witness (here p) = p
first⟶witness (there x ¬px f) = first⟶witness f

-- more likable syntax for the above structure
first_∈_⇒_ : ∀ {p} → A → List A → (B : A → Set p) → Set (p ⊔ ℓ)
first_∈_⇒_ x v p = First p x v

-- a decision procedure to find the first element in a vector that satisfies a predicate
find : ∀ (P : A → Set) → ((a : A) → Dec (P a)) → (v : List A) →
       Dec (∃ λ e → first e ∈ v ⇒ P)
find P dec [] = no (λ{ (e , ()) })
find P dec (x ∷ v) with dec x
find P dec (x ∷ v) | yes px = yes (x , here px)
find P dec (x ∷ v) | no ¬px with find P dec v
find P dec (x ∷ v) | no ¬px | yes firstv = yes (-, there x ¬px (proj₂ firstv))
find P dec (x ∷ v) | no ¬px | no ¬firstv = no $ helper ¬px ¬firstv
  where
    helper : ¬ (P x) → ¬ (∃ λ e → First P e v) → ¬ (∃ λ e → First P e (x ∷ v))
    helper ¬px ¬firstv (.x , here p) = ¬px p
    helper ¬px ¬firstv (u  , there ._ _ firstv) = ¬firstv (u , firstv)


text:
------------------------------------------------------------------------
-- Example: Left recursive expression grammar
------------------------------------------------------------------------

module TotalRecognisers.LeftRecursion.Expression where

open import Codata.Musical.Notation
open import Data.Bool hiding (_∧_; _≤_; _≤?_)
open import Data.Char as Char using (Char)
open import Data.Nat using (ℕ; _≤?_)
open import Data.String as String using (String)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable

import TotalRecognisers.LeftRecursion as P
import TotalRecognisers.LeftRecursion.Lib as Lib

open P Char
open Lib Char
open KleeneStar₁
open Tok Char._≟_

------------------------------------------------------------------------
-- Recognisers for digits and numbers

-- Digits.

digit : P _
digit = sat in-range
  where
  in-range : Char → Bool
  in-range t = ⌊ Char.toℕ '0' ≤? Char.toℕ  t  ⌋ ∧
               ⌊ Char.toℕ  t  ≤? Char.toℕ '9' ⌋

-- Numbers.

number : P _
number = digit +

------------------------------------------------------------------------
-- An expression grammar

-- t ∷= t '+' f ∣ f
-- f ∷= f '*' a ∣ a
-- a ∷= '(' t ')' ∣ n

mutual

  term   = ♯ (♯ term · ♯ tok '+') · ♯ factor
         ∣ factor

  factor = ♯ (♯ factor · ♯ tok '*') · ♯ atom
         ∣ atom

  atom   = ♯ (♯ tok '(' · ♯ term) · ♯ tok ')'
         ∣ number

------------------------------------------------------------------------
-- Unit tests

module Tests where

  test : ∀ {n} → P n → String → Bool
  test p s = ⌊ String.toList s ∈? p ⌋

  ex₁ : test term "1*(2+3)" ≡ true
  ex₁ = refl

  ex₂ : test term "1*(2+3" ≡ false
  ex₂ = refl

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

module Math.NumberTheory.Summation.Generic.Properties.Lemma where

-- agda-stdlib
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Relation.Binary.PropositionalEquality
open import Function.Base

lemma₁ : ∀ m n → 2 + m + n ≡ suc m + suc n
lemma₁ = solve 2 (λ m n → con 2 :+ m :+ n := con 1 :+ m :+ (con 1 :+ n)) refl
  where open +-*-Solver


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

module Cubical.Foundations.Logic where

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Prod as × using (_×_; _,_; proj₁; proj₂)
open import Cubical.Data.Sum as ⊎ using (_⊎_)
open import Cubical.Data.Unit

open import Cubical.Foundations.Prelude

open import Cubical.HITs.PropositionalTruncation as PropTrunc

open import Cubical.Foundations.HLevels using (hProp; ΣProp≡; isPropPi) public
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open import Cubical.Relation.Nullary hiding (¬_)

infix 10 ¬_
infixr 8 _⊔_
infixr 8 _⊔′_
infixr 8 _⊓_
infixr 8 _⊓′_
infixr 6 _⇒_
infixr 4 _⇔_
infix 30 _≡ₚ_
infix 30 _≢ₚ_

infix 2 ∃[]-syntax
infix 2 ∃[∶]-syntax

infix 2 ∀[∶]-syntax
infix 2 ∀[]-syntax

infix 2 ⇒∶_⇐∶_
infix 2 ⇐∶_⇒∶_

--------------------------------------------------------------------------------
-- The type hProp of mere propositions
-- the definition hProp is given in Foundations.HLevels
-- hProp ℓ = Σ (Type ℓ) isProp

private
  variable
    ℓ ℓ' ℓ'' : Level
    P Q R : hProp ℓ
    A B C : Type ℓ

[_] : hProp ℓ → Type ℓ
[_] = fst

∥_∥ₚ : Type ℓ → hProp ℓ
∥ A ∥ₚ = ∥ A ∥ , propTruncIsProp

_≡ₚ_ : (x y : A) → hProp _
x ≡ₚ y = ∥ x ≡ y ∥ₚ

hProp≡ : [ P ] ≡ [ Q ] → P ≡ Q
hProp≡ p = ΣProp≡ (\ _ → isPropIsProp) p

--------------------------------------------------------------------------------
-- Logical implication of mere propositions

_⇒_ : (A : hProp ℓ) → (B : hProp ℓ') → hProp _
A ⇒ B = ([ A ] → [ B ]) , isPropPi λ _ → B .snd

⇔toPath : [ P ⇒ Q ] → [ Q ⇒ P ] → P ≡ Q
⇔toPath {P = P} {Q = Q} P⇒Q Q⇒P = hProp≡ (isoToPath
  (iso P⇒Q Q⇒P (λ b → Q .snd (P⇒Q (Q⇒P b)) b) λ a → P .snd (Q⇒P (P⇒Q a)) a))

pathTo⇒ : P ≡ Q → [ P ⇒ Q ]
pathTo⇒ p x = subst fst  p x

pathTo⇐ : P ≡ Q → [ Q ⇒ P ]
pathTo⇐ p x = subst fst (sym p) x

substₚ : {x y : A} (B : A → hProp ℓ) → [ x ≡ₚ y ⇒ B x ⇒ B y ]
substₚ {x = x} {y = y} B = PropTrunc.elim (λ _ → isPropPi λ _ → B y .snd) (subst (fst ∘ B))

--------------------------------------------------------------------------------
-- Mixfix notations for ⇔-toPath
-- see ⊔-identityˡ and ⊔-identityʳ for the difference

⇒∶_⇐∶_ : [ P ⇒ Q ] → [ Q ⇒ P ] → P ≡ Q
⇒∶_⇐∶_ = ⇔toPath

⇐∶_⇒∶_ : [ Q ⇒ P ] → [ P ⇒ Q ] → P ≡ Q
⇐∶ g ⇒∶ f  = ⇔toPath f g
--------------------------------------------------------------------------------
-- False and True

⊥ : hProp _
⊥ = ⊥.⊥ , λ ()

⊤ : hProp _
⊤ = Unit , (λ _ _ _ → tt)

--------------------------------------------------------------------------------
-- Pseudo-complement of mere propositions

¬_ : hProp ℓ → hProp _
¬ A = ([ A ] → ⊥.⊥) , isPropPi λ _ → ⊥.isProp⊥

_≢ₚ_ : (x y : A) → hProp _
x ≢ₚ y = ¬ x ≡ₚ y

--------------------------------------------------------------------------------
-- Disjunction of mere propositions

_⊔′_ : Type ℓ → Type ℓ' → Type _
A ⊔′ B = ∥ A ⊎ B ∥

_⊔_ : hProp ℓ → hProp ℓ' → hProp _
P ⊔ Q = ∥ [ P ] ⊎ [ Q ] ∥ₚ

inl : A → A ⊔′ B
inl x = ∣ ⊎.inl x ∣

inr : B → A ⊔′ B
inr x = ∣ ⊎.inr x ∣

⊔-elim : (P : hProp ℓ) (Q : hProp ℓ') (R : [ P ⊔ Q ] → hProp ℓ'')
  → (∀ x → [ R (inl x) ]) → (∀ y → [ R (inr y) ]) → (∀ z → [ R z ])
⊔-elim _ _ R P⇒R Q⇒R = PropTrunc.elim (snd ∘ R) (⊎.elim P⇒R Q⇒R)

--------------------------------------------------------------------------------
-- Conjunction of mere propositions
_⊓′_ : Type ℓ → Type ℓ' → Type _
A ⊓′ B = A × B

_⊓_ : hProp ℓ → hProp ℓ' → hProp _
A ⊓ B = [ A ] ⊓′ [ B ] , ×.isOfHLevelProd 1 (A .snd) (B .snd)

⊓-intro : (P : hProp ℓ) (Q : [ P ] → hProp ℓ') (R : [ P ] → hProp ℓ'')
       → (∀ a → [ Q a ]) → (∀ a → [ R a ]) → (∀ (a : [ P ]) → [ Q a ⊓ R a ] )
⊓-intro _ _ _ = ×.intro

--------------------------------------------------------------------------------
-- Logical bi-implication of mere propositions

_⇔_ : hProp ℓ → hProp ℓ' → hProp _
A ⇔ B = (A ⇒ B) ⊓ (B ⇒ A)

--------------------------------------------------------------------------------
-- Universal Quantifier

∀[∶]-syntax : (A → hProp ℓ) → hProp _
∀[∶]-syntax {A = A} P = (∀ x → [ P x ]) , isPropPi (snd ∘ P)

∀[]-syntax : (A → hProp ℓ) → hProp _
∀[]-syntax {A = A} P = (∀ x → [ P x ]) , isPropPi (snd ∘ P)

syntax ∀[∶]-syntax {A = A} (λ a → P) = ∀[ a ∶ A ] P
syntax ∀[]-syntax (λ a → P)          = ∀[ a ] P
--------------------------------------------------------------------------------
-- Existential Quantifier

∃[]-syntax : (A → hProp ℓ) → hProp _
∃[]-syntax {A = A} P = ∥ Σ A (fst ∘ P) ∥ₚ

∃[∶]-syntax : (A → hProp ℓ) → hProp _
∃[∶]-syntax {A = A} P = ∥ Σ A (fst ∘ P) ∥ₚ

syntax ∃[]-syntax {A = A} (λ x → P) = ∃[ x ∶ A ] P
syntax ∃[∶]-syntax (λ x → P) = ∃[ x ] P
--------------------------------------------------------------------------------
-- Decidable mere proposition

Decₚ : (P : hProp ℓ) → hProp ℓ
Decₚ P = Dec [ P ] , isPropDec (snd P)

--------------------------------------------------------------------------------
-- Negation commutes with truncation

∥¬A∥≡¬∥A∥ : (A : Type ℓ) → ∥ (A → ⊥.⊥) ∥ₚ ≡ (¬ ∥ A ∥ₚ)
∥¬A∥≡¬∥A∥ _ =
  ⇒∶ (λ ¬A A → PropTrunc.elim (λ _ → ⊥.isProp⊥)
    (PropTrunc.elim (λ _ → isPropPi λ _ → ⊥.isProp⊥) (λ ¬p p → ¬p p) ¬A) A)
  ⇐∶ λ ¬p → ∣ (λ p → ¬p ∣ p ∣) ∣

--------------------------------------------------------------------------------
-- (hProp, ⊔, ⊥) is a bounded ⊔-semilattice

⊔-assoc : (P : hProp ℓ) (Q : hProp ℓ') (R : hProp ℓ'')
  → P ⊔ (Q ⊔ R) ≡ (P ⊔ Q) ⊔ R
⊔-assoc P Q R =
  ⇒∶ ⊔-elim P (Q ⊔ R) (λ _ → (P ⊔ Q) ⊔ R)
    (inl ∘ inl)
    (⊔-elim Q R (λ _ → (P ⊔ Q) ⊔ R) (inl ∘ inr) inr)

  ⇐∶ assoc2
  where
    assoc2 : (A ⊔′ B) ⊔′ C → A ⊔′ (B ⊔′ C)
    assoc2 ∣ ⊎.inr a ∣              = ∣ ⊎.inr ∣ ⊎.inr a ∣ ∣
    assoc2 ∣ ⊎.inl ∣ ⊎.inr b ∣ ∣  = ∣ ⊎.inr ∣ ⊎.inl b ∣ ∣
    assoc2 ∣ ⊎.inl ∣ ⊎.inl c ∣ ∣  = ∣ ⊎.inl c ∣
    assoc2 ∣ ⊎.inl (squash x y i) ∣ = propTruncIsProp (assoc2 ∣ ⊎.inl x ∣) (assoc2 ∣ ⊎.inl y ∣) i
    assoc2 (squash x y i)             = propTruncIsProp (assoc2 x) (assoc2 y) i

⊔-idem : (P : hProp ℓ) → P ⊔ P ≡ P
⊔-idem P =
  ⇒∶ (⊔-elim P P (\ _ → P) (\ x → x) (\ x → x))
  ⇐∶ inl

⊔-comm : (P : hProp ℓ) (Q : hProp ℓ') → P ⊔ Q ≡ Q ⊔ P
⊔-comm P Q =
  ⇒∶ (⊔-elim P Q (\ _ → (Q ⊔ P)) inr inl)
  ⇐∶ (⊔-elim Q P (\ _ → (P ⊔ Q)) inr inl)

⊔-identityˡ : (P : hProp ℓ) → ⊥ ⊔ P ≡ P
⊔-identityˡ P =
  ⇒∶ (⊔-elim ⊥ P (λ _ → P) (λ ()) (λ x → x))
  ⇐∶ inr

⊔-identityʳ : (P : hProp ℓ) → P ⊔ ⊥ ≡ P
⊔-identityʳ P = ⇔toPath (⊔-elim P ⊥ (λ _ → P) (λ x → x) λ ()) inl

--------------------------------------------------------------------------------
-- (hProp, ⊓, ⊤) is a bounded ⊓-lattice

⊓-assoc : (P : hProp ℓ) (Q : hProp ℓ') (R : hProp ℓ'')
  → P ⊓ Q ⊓ R ≡ (P ⊓ Q) ⊓ R
⊓-assoc _ _ _ =
  ⇒∶ (λ {(x , (y , z)) →  (x , y) , z})
  ⇐∶ (λ {((x , y) , z) → x , (y , z) })

⊓-comm : (P : hProp ℓ) (Q : hProp ℓ') → P ⊓ Q ≡ Q ⊓ P
⊓-comm _ _ = ⇔toPath ×.swap ×.swap

⊓-idem : (P : hProp ℓ) → P ⊓ P ≡ P
⊓-idem _ = ⇔toPath proj₁ (λ x → x , x)

⊓-identityˡ : (P : hProp ℓ) → ⊤ ⊓ P ≡ P
⊓-identityˡ _ = ⇔toPath proj₂ λ x → tt , x

⊓-identityʳ : (P : hProp ℓ) → P ⊓ ⊤ ≡ P
⊓-identityʳ _ = ⇔toPath proj₁ λ x → x , tt

--------------------------------------------------------------------------------
-- Distributive laws

⇒-⊓-distrib : (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'')
  → P ⇒ (Q ⊓ R) ≡ (P ⇒ Q) ⊓ (P ⇒ R)
⇒-⊓-distrib _ _ _ =
  ⇒∶ (λ f → (proj₁ ∘ f) , (proj₂ ∘ f))
  ⇐∶ (λ { (f , g) x → f x , g x})

⊓-⊔-distribˡ : (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'')
  → P ⊓ (Q ⊔ R) ≡ (P ⊓ Q) ⊔ (P ⊓ R)
⊓-⊔-distribˡ P Q R =
  ⇒∶ (λ { (x , a) → ⊔-elim Q R (λ _ → (P ⊓ Q) ⊔ (P ⊓ R))
        (λ y → ∣ ⊎.inl (x , y) ∣ )
        (λ z → ∣ ⊎.inr (x , z) ∣ ) a })

  ⇐∶ ⊔-elim (P ⊓ Q) (P ⊓ R) (λ _ → P ⊓ Q ⊔ R)
       (λ y → proj₁ y , inl (proj₂ y))
       (λ z → proj₁ z , inr (proj₂ z))

⊔-⊓-distribˡ : (P : hProp ℓ) (Q : hProp ℓ')(R : hProp ℓ'')
  → P ⊔ (Q ⊓ R) ≡ (P ⊔ Q) ⊓ (P ⊔ R)
⊔-⊓-distribˡ P Q R =
  ⇒∶ ⊔-elim P (Q ⊓ R) (λ _ → (P ⊔ Q) ⊓ (P ⊔ R) )
    (×.intro inl inl) (×.map inr inr)

  ⇐∶ (λ { (x , y) → ⊔-elim P R (λ _ → P ⊔ Q ⊓ R) inl
      (λ z → ⊔-elim P Q (λ _ → P ⊔ Q ⊓ R) inl (λ y → inr (y , z)) x) y })

⊓-∀-distrib :  (P : A → hProp ℓ) (Q : A → hProp ℓ')
  → (∀[ a ∶ A ] P a) ⊓ (∀[ a ∶ A ] Q a) ≡ (∀[ a ∶ A ] (P a ⊓ Q a))
⊓-∀-distrib P Q =
  ⇒∶ (λ {(p , q) a → p a , q a})
  ⇐∶ λ pq → (proj₁ ∘ pq ) , (proj₂ ∘ pq)

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
module Monads.WriterT where

open import Class.Monad
open import Class.MonadTrans
open import Class.Monad.Except
open import Class.Monad.State
open import Class.Monad.Writer
open import Class.Monoid
open import Data.Product
open import Data.Unit.Polymorphic
open import Function
open import Level

private
  variable
    a : Level
    A B W : Set a

WriterT : (Set a → Set a) → Set a → Set a → Set a
WriterT M W A = M (A × W)

module _ {M : Set a → Set a} {{_ : Monad M}} {W} {{_ : Monoid W}} where

  WriterT-Monad : Monad (WriterT M W)
  WriterT-Monad = record { _>>=_ = helper ; return = λ a → return (a , mzero) }
    where
      helper : WriterT M W A → (A → WriterT M W B) → WriterT M W B
      helper a f = do
        (a' , w) ← a
        (b , w') ← f a'
        return (b , w + w')

  private
    tell' : W → WriterT M W ⊤
    tell' w = return (tt , w)

    listen' : WriterT M W A → WriterT M W (A × W)
    listen' x = do
      (a , w) ← x
      return ((a , w) , w)

    pass' : WriterT M W (A × (W → W)) → WriterT M W A
    pass' x = do
      ((a , f) , w) ← x
      return (a , f w)

  WriterT-MonadWriter : MonadWriter (WriterT M W) {{WriterT-Monad}} W
  WriterT-MonadWriter = record { tell = tell' ; listen = listen' ; pass = pass' }

WriterT-MonadTrans : {W : Set a} {{_ : Monoid W}} → MonadTrans (λ (M : Set a → Set a) → WriterT M W)
WriterT-MonadTrans = record { embed = λ x → x >>= λ a → return (a , mzero) }

module _ {M : Set a → Set a} {{_ : Monad M}} {W} {{_ : Monoid W}} where

  WriterT-MonadState : ∀ {S : Set a} {{_ : MonadState M S}} → MonadState (WriterT M W) {{WriterT-Monad}} S
  WriterT-MonadState = record
    { get = embed {{WriterT-MonadTrans}} get
    ; put = embed {{WriterT-MonadTrans}} ∘ put }

  WriterT-MonadExcept : ∀ {E : Set a} {{_ : MonadExcept M E}} → MonadExcept (WriterT M W) {{WriterT-Monad}} E
  WriterT-MonadExcept = record
    { throwError = embed {{WriterT-MonadTrans}} ∘ throwError
    ; catchError = catchError }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille