text:
module par-swap.confluent where

open import par-swap
open import par-swap.properties
open import Data.Nat using (_+_ ;  _≤′_ ; _<′_ ; suc ; zero ; ≤′-refl)
open import Esterel.Lang.CanFunction
open import utility
open import Esterel.Lang
open import Esterel.Context
open import Data.Product
open import Data.Sum
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; subst ; cong ; trans ;
         module ≡-Reasoning ; cong₂ ; subst₂ ; inspect)
open import sn-calculus
open import context-properties -- get view, E-views
open import Esterel.Lang.Binding
open import binding-preserve using (sn⟶-maintains-binding ; sn⟶*-maintains-binding)

open import sn-calculus-props

∥R-confluent : CB-CONFLUENT _∥R_
∥R-confluent CBp
  (∥Rstep dchole)
  (∥Rstep dchole) =
  _ , ∥Rstep dchole , ∥Rstep dchole
∥R-confluent CBp
  (∥Rstep dchole)
  (∥Rstep (dcpar₁ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcpar₂ d≐C⟦p∥q⟧c₂) , ∥Rstep dchole
∥R-confluent CBp
  (∥Rstep dchole)
  (∥Rstep (dcpar₂ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcpar₁ d≐C⟦p∥q⟧c₂) , ∥Rstep dchole
∥R-confluent CBp
  (∥Rstep (dcpar₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep dchole) =
  _ , ∥Rstep dchole , ∥Rstep (dcpar₂ d≐C⟦p∥q⟧c₁)
∥R-confluent (CBpar CBs _ _ _ _ _)
  (∥Rstep {c₁ ∷ C₁} (dcpar₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcpar₁ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent CBp
  (∥Rstep (dcpar₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcpar₂ d≐C⟦p∥q⟧c₂)) =
  _ ,  ∥Rstep (dcpar₂ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcpar₁ d≐C⟦p∥q⟧c₁)
∥R-confluent CBp
  (∥Rstep (dcpar₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep dchole) =
  _ , ∥Rstep dchole , ∥Rstep (dcpar₁ d≐C⟦p∥q⟧c₁)
∥R-confluent CBp
  (∥Rstep (dcpar₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcpar₁ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcpar₁ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcpar₂ d≐C⟦p∥q⟧c₁)
∥R-confluent (CBpar _ CBs _ _ _ _)
  (∥Rstep {c₁ ∷ C₁} (dcpar₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcpar₂ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBseq CBs _ _)
  (∥Rstep {c₁ ∷ C₁} (dcseq₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcseq₁ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent CBp
  (∥Rstep (dcseq₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcseq₂ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcseq₂ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcseq₁ d≐C⟦p∥q⟧c₁)
∥R-confluent CBp
  (∥Rstep (dcseq₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcseq₁ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcseq₁ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcseq₂ d≐C⟦p∥q⟧c₁)
∥R-confluent (CBseq _ CBs _)
  (∥Rstep {c₁ ∷ C₁} (dcseq₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcseq₂ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBsusp CBs _)
  (∥Rstep {c₁ ∷ C₁} (dcsuspend d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcsuspend d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBtrap CBs)
  (∥Rstep {c₁ ∷ C₁} (dctrap d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dctrap d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBsig CBs)
  (∥Rstep {c₁ ∷ C₁} (dcsignl d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcsignl d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBpresent CBs _)
  (∥Rstep {c₁ ∷ C₁} (dcpresent₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcpresent₁ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent CBp
  (∥Rstep (dcpresent₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcpresent₂ d≐C⟦p∥q⟧c₂)) =
   _ , ∥Rstep (dcpresent₂ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcpresent₁ d≐C⟦p∥q⟧c₁)
∥R-confluent CBp
  (∥Rstep (dcpresent₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcpresent₁ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcpresent₁ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcpresent₂ d≐C⟦p∥q⟧c₁)
∥R-confluent (CBpresent _ CBs)
  (∥Rstep {c₁ ∷ C₁} (dcpresent₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcpresent₂ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBloop CBs _)
  (∥Rstep {c₁ ∷ C₁} (dcloop d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcloop d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBloopˢ CBs _ _ _)
  (∥Rstep {c₁ ∷ C₁} (dcloopˢ₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcloopˢ₁ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent CBp
  (∥Rstep (dcloopˢ₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcloopˢ₂ d≐C⟦p∥q⟧c₂)) =
   _ , ∥Rstep (dcloopˢ₂ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcloopˢ₁ d≐C⟦p∥q⟧c₁)
∥R-confluent CBp
  (∥Rstep (dcloopˢ₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcloopˢ₁ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcloopˢ₁ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcloopˢ₂ d≐C⟦p∥q⟧c₁)
∥R-confluent (CBloopˢ _ CBs _ _)
  (∥Rstep {c₁ ∷ C₁} (dcloopˢ₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcloopˢ₂ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBshared CBs)
  (∥Rstep {c₁ ∷ C₁} (dcshared d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcshared d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBvar CBs)
  (∥Rstep {c₁ ∷ C₁} (dcvar d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcvar d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBif CBs _)
  (∥Rstep {c₁ ∷ C₁} (dcif₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcif₁ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent _
  (∥Rstep (dcif₁ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcif₂ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcif₂ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcif₁ d≐C⟦p∥q⟧c₁)
∥R-confluent CBp
  (∥Rstep (dcif₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep (dcif₁ d≐C⟦p∥q⟧c₂)) =
  _ , ∥Rstep (dcif₁ d≐C⟦p∥q⟧c₂) , ∥Rstep (dcif₂ d≐C⟦p∥q⟧c₁)
∥R-confluent (CBif _ CBs)
  (∥Rstep {c₁ ∷ C₁} (dcif₂ d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcif₂ d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz
∥R-confluent (CBρ CBs)
  (∥Rstep {c₁ ∷ C₁} (dcenv d≐C⟦p∥q⟧c₁))
  (∥Rstep {c₂ ∷ C₂} (dcenv d≐C⟦p∥q⟧c₂))
  with ∥R-confluent CBs (∥Rstep d≐C⟦p∥q⟧c₁) (∥Rstep d≐C⟦p∥q⟧c₂)
... | z , C₁⟦q₁∥p₁⟧c∥Rz , C₂⟦q₂∥p₂⟧c∥Rz  =
  _ , Context1-∥R c₁ C₁⟦q₁∥p₁⟧c∥Rz , Context1-∥R c₂ C₂⟦q₂∥p₂⟧c∥Rz

∥R-maintains-binding :
  ∀ {p BV FV q} →
  CorrectBinding p BV FV →
  p ∥R q →
  CorrectBinding q (BVars q) (FVars q)
∥R-maintains-binding = thm where

  thm :
    ∀ {p BV FV q} →
     CorrectBinding p BV FV →
     p ∥R q →
     CorrectBinding q (BVars q) (FVars q)
  thm{p}{BVp}{FVp}{q} CBp (∥Rstep{C}{r₁}{r₂}{d} d≐C⟦p∥q⟧c)
    with binding-extractc' CBp d≐C⟦p∥q⟧c
  ... | (BVr₁∥r₂ , FVr₁∥r₂) ,
        CBpar{.r₁}{.r₂}{BVr₁}{FVr₁}{BVr₂}{FVr₂}
             CBr₁ CBr₂ BVr₁≠BVr₂ FVr₁≠BVr₂ BVr₁≠FVr₂ Xr₁≠Xr₂
     with CBpar{r₂}{r₁}{BVr₂}{FVr₂}{BVr₁}{FVr₁}
               CBr₂ CBr₁
               (distinct-sym BVr₁≠BVr₂) (distinct-sym BVr₁≠FVr₂)
               (distinct-sym FVr₁≠BVr₂) (dist'-sym Xr₁≠Xr₂)
  ... | CBr₂∥r₁
    with binding-substc' CBp d≐C⟦p∥q⟧c
            (CBpar CBr₁ CBr₂ BVr₁≠BVr₂ FVr₁≠BVr₂
                   BVr₁≠FVr₂ Xr₁≠Xr₂)
            (∪-comm-⊆-right BVr₁ ⊆-refl)
            (∪-comm-⊆-right FVr₁ ⊆-refl)
            CBr₂∥r₁
  ... | (BVq , FVq) , (_ , CBq)
    with BVFVcorrect _ BVq FVq CBq
  ... | (refl , refl) = CBq

∥R*-maintains-binding :
  ∀ {p BV FV q} →
  CorrectBinding p BV FV →
  p ∥R* q →
  CorrectBinding q (BVars q) (FVars q)
∥R*-maintains-binding = thm where

  thm : ∀ {p BV FV q} →
   CorrectBinding p BV FV →
   p ∥R* q →
   CorrectBinding q (BVars q) (FVars q)
  thm CBp ∥R0 with BVFVcorrect _ _ _ CBp
  ... | refl , refl = CBp
  thm CBp (∥Rn p∥Rq₁ q₁∥R*q)
    with ∥R-maintains-binding CBp p∥Rq₁
  ... | CBq₁ = thm CBq₁ q₁∥R*q

∥R*-semi-confluent :
  ∀ {p q r BV FV} ->
  CorrectBinding p BV FV ->
  p ∥R q ->
  p ∥R* r ->
 ∃ λ {z → (q ∥R* z × r ∥R* z)}
∥R*-semi-confluent CBp p∥Rq ∥R0 = _ , ∥R0 , (∥Rn p∥Rq ∥R0)
∥R*-semi-confluent CBp p∥Rq (∥Rn p∥Rq₁ q₁∥R*r)
  with ∥R-confluent CBp p∥Rq p∥Rq₁
... | z , q∥Rz , q₁∥Rz
  with ∥R*-semi-confluent (∥R-maintains-binding CBp p∥Rq₁) q₁∥Rz q₁∥R*r
... | z₁ , z∥R*z₁ , r∥R*z₁ = z₁ , ∥Rn q∥Rz z∥R*z₁ , r∥R*z₁

∥R*-confluent : CB-CONFLUENT _∥R*_
∥R*-confluent CBp ∥R0 p∥R*r = _ , p∥R*r , ∥R0
∥R*-confluent CBp (∥Rn p∥Rp₁ p₁∥R*q) p∥R*r
  with ∥R*-semi-confluent CBp p∥Rp₁ p∥R*r
... | z₁ , p₁∥R*z₁ , r∥R*z₁
  with ∥R*-confluent (∥R-maintains-binding CBp p∥Rp₁) p₁∥R*q p₁∥R*z₁
... | z  , q∥R*z , z₁∥R*z = z , q∥R*z , ∥R*-concat r∥R*z₁ z₁∥R*z

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- Support for sized types
------------------------------------------------------------------------

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

module Prelude.Size where

open import Prelude

-- Size primitives.

open import Agda.Builtin.Size public
  using (Size; ∞)
  renaming (Size<_ to Size<; SizeUniv to Size-universe; ↑_ to ssuc)

-- If S is a type in the size universe, then S in-type is a type in
-- Type.

record _in-type (S : Size-universe) : Type where
  field
    size : S

open _in-type public

ext: agda

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Instances.Polynomials.UnivariatePolyHIT where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat hiding (_·_) renaming (_+_ to _+n_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Monoid.Instances.Nat
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.GradedRing.DirectSumHIT

private variable
  ℓ : Level

open GradedRing-⊕HIT-index
open GradedRing-⊕HIT-⋆
open ExtensionCommRing

module _
  (ACommRing@(A , Astr) : CommRing ℓ)
  where

  open CommRingStr Astr
  open RingTheory (CommRing→Ring ACommRing)

  UnivariatePolyHIT-CommRing : CommRing ℓ
  UnivariatePolyHIT-CommRing = ⊕HITgradedRing-CommRing
                   NatMonoid
                   (λ _ → A)
                   (λ _ → snd (Ring→AbGroup (CommRing→Ring ACommRing)))
                   1r _·_ 0LeftAnnihilates 0RightAnnihilates
                   (λ a b c → ΣPathP ((+-assoc _ _ _) , (·Assoc _ _ _)))
                   (λ a → ΣPathP ((+-zero _) , (·IdR _)))
                   (λ a → ΣPathP (refl , (·IdL _)))
                   ·DistR+
                   ·DistL+
                   λ x y → ΣPathP ((+-comm _ _) , (·Comm _ _))

nUnivariatePolyHIT : (A' : CommRing ℓ) → (n : ℕ) → CommRing ℓ
nUnivariatePolyHIT A' zero = A'
nUnivariatePolyHIT A' (suc n) = UnivariatePolyHIT-CommRing (nUnivariatePolyHIT A' n)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Data.Num.Sandbox.WF where

open import Data.Nat
-- open import Relation.Binary
--
-- open DecTotalOrder decTotalOrder
--   using (trans)
--
-- data Acc (n : ℕ) : Set where
--     acc : (∀ m → m < n → Acc m) → Acc n
--
-- go0 : (m : ℕ) → m < 0 → Acc m
-- go0 m ()
--
-- <-wf : ∀ n → Acc n
-- <-wf n = acc (go n)
--     where   go : (n m : ℕ) → m < n → Acc m
--             go zero m ()
--             go (suc n₁) zero m<n = acc (λ _ → λ ())
--             go (suc n₁) (suc m) (s≤s m<n₁) = acc (λ m₁ m₁<m+1 → go n₁ m₁ (trans m₁<m+1 m<n₁))

pp : ℕ → ℕ
pp zero = zero
pp (suc zero) = zero
pp (suc (suc n)) = n
--
-- f : ℕ → ℕ
-- f n = go n (<-wf n)
--     where
--         go : ∀ n → Acc n → ℕ
--         go zero    _ = zero
--         go (suc n) (acc a) = go (pp (suc n)) (a (pp (suc n)) {!   !})

open import Induction.Nat

half : ℕ → ℕ
half = <-rec _ go
    where   go : (x : ℕ) → ((y : ℕ) → suc y ≤′ x → ℕ) → ℕ
            go zero acc = zero
            go (suc zero) acc = zero
            go (suc (suc n)) acc = suc (acc n (≤′-step ≤′-refl))

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Boring lemmas used in Data.Nat.GCD and Data.Nat.Coprimality
------------------------------------------------------------------------

module Data.Nat.GCD.Lemmas where

open import Data.Nat
import Data.Nat.Properties as NatProp
open NatProp.SemiringSolver
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function

lem₀ = solve 2 (λ n k → n :+ (con 1 :+ k)  :=  con 1 :+ n :+ k) refl

lem₁ : ∀ i j → 2 + i ≤′ 2 + j + i
lem₁ i j = NatProp.≤⇒≤′ $ s≤s $ s≤s $ NatProp.n≤m+n j i

lem₂ : ∀ d x {k n} →
       d + x * k ≡ x * n → d + x * (n + k) ≡ 2 * x * n
lem₂ d x {k} {n} eq = begin
  d + x * (n + k)    ≡⟨ solve 4 (λ d x n k → d :+ x :* (n :+ k)
                                         :=  d :+ x :* k :+ x :* n)
                                refl d x n k ⟩
  d + x * k + x * n  ≡⟨ cong₂ _+_ eq refl ⟩
  x * n + x * n      ≡⟨ solve 3 (λ x n k → x :* n :+ x :* n
                                       :=  con 2 :* x :* n)
                                 refl x n k ⟩
  2 * x * n          ∎

lem₃ : ∀ d x {i k n} →
       d + (1 + x + i) * k ≡ x * n →
       d + (1 + x + i) * (n + k) ≡ (1 + 2 * x + i) * n
lem₃ d x {i} {k} {n} eq = begin
  d + y * (n + k)      ≡⟨ solve 4 (λ d y n k → d :+ y :* (n :+ k)
                                           :=  (d :+ y :* k) :+ y :* n)
                                  refl d y n k ⟩
  (d + y * k) + y * n  ≡⟨ cong₂ _+_ eq refl ⟩
  x * n + y * n        ≡⟨ solve 3 (λ x n i → x :* n :+ (con 1 :+ x :+ i) :* n
                                         :=  (con 1 :+ con 2 :* x :+ i) :* n)
                                  refl x n i ⟩
  (1 + 2 * x + i) * n  ∎
  where y = 1 + x + i

lem₄ : ∀ d y {k i} n →
       d + y * k ≡ (1 + y + i) * n →
       d + y * (n + k) ≡ (1 + 2 * y + i) * n
lem₄ d y {k} {i} n eq = begin
  d + y * (n + k)          ≡⟨ solve 4 (λ d y n k → d :+ y :* (n :+ k)
                                               :=  d :+ y :* k :+ y :* n)
                                      refl d y n k ⟩
  d + y * k + y * n        ≡⟨ cong₂ _+_ eq refl ⟩
  (1 + y + i) * n + y * n  ≡⟨ solve 3 (λ y i n → (con 1 :+ y :+ i) :* n :+ y :* n
                                             :=  (con 1 :+ con 2 :* y :+ i) :* n)
                                      refl y i n ⟩
  (1 + 2 * y + i) * n      ∎

private
  distrib-comm =
    solve 3 (λ x k n → x :* k :+ x :* n  :=  x :* (n :+ k)) refl

lem₅ : ∀ d x {n k} →
       d + x * n ≡ x * k →
       d + 2 * x * n ≡ x * (n + k)
lem₅ d x {n} {k} eq = begin
  d + 2 * x * n      ≡⟨ solve 3 (λ d x n → d :+ con 2 :* x :* n
                                       :=  d :+ x :* n :+ x :* n)
                                refl d x n ⟩
  d + x * n + x * n  ≡⟨ cong₂ _+_ eq refl ⟩
  x * k + x * n      ≡⟨ distrib-comm x k n ⟩
  x * (n + k)        ∎

lem₆ : ∀ d x {n i k} →
       d + x * n ≡ (1 + x + i) * k →
       d + (1 + 2 * x + i) * n ≡ (1 + x + i) * (n + k)
lem₆ d x {n} {i} {k} eq = begin
  d + (1 + 2 * x + i) * n  ≡⟨ solve 4 (λ d x i n → d :+ (con 1 :+ con 2 :* x :+ i) :* n
                                               :=  d :+ x :* n :+ (con 1 :+ x :+ i) :* n)
                                      refl d x i n ⟩
  d + x * n + y * n        ≡⟨ cong₂ _+_ eq refl ⟩
  y * k + y * n            ≡⟨ distrib-comm y k n ⟩
  y * (n + k)              ∎
  where y = 1 + x + i

lem₇ : ∀ d y {i} n {k} →
       d + (1 + y + i) * n ≡ y * k →
       d + (1 + 2 * y + i) * n ≡ y * (n + k)
lem₇ d y {i} n {k} eq = begin
  d + (1 + 2 * y + i) * n      ≡⟨ solve 4 (λ d y i n → d :+ (con 1 :+ con 2 :* y :+ i) :* n
                                                   :=  d :+ (con 1 :+ y :+ i) :* n :+ y :* n)
                                          refl d y i n ⟩
  d + (1 + y + i) * n + y * n  ≡⟨ cong₂ _+_ eq refl ⟩
  y * k + y * n                ≡⟨ distrib-comm y k n ⟩
  y * (n + k)                  ∎

lem₈ : ∀ {i j k q} x y →
       1 + y * j ≡ x * i → j * k ≡ q * i →
       k ≡ (x * k ∸ y * q) * i
lem₈ {i} {j} {k} {q} x y eq eq′ =
  sym (NatProp.im≡jm+n⇒[i∸j]m≡n (x * k) (y * q) i k lemma)
  where
  lemma = begin
    x * k * i        ≡⟨ solve 3 (λ x k i → x :* k :* i
                                       :=  x :* i :* k)
                                refl x k i ⟩
    x * i * k        ≡⟨ cong (λ n → n * k) (sym eq) ⟩
    (1 + y * j) * k  ≡⟨ solve 3 (λ y j k → (con 1 :+ y :* j) :* k
                                       :=  y :* (j :* k) :+ k)
                                refl y j k ⟩
    y * (j * k) + k  ≡⟨ cong (λ n → y * n + k) eq′ ⟩
    y * (q * i) + k  ≡⟨ solve 4 (λ y q i k → y :* (q :* i) :+ k
                                         :=  y :*  q :* i  :+ k)
                                refl y q i k ⟩
    y *  q * i  + k  ∎

lem₉ : ∀ {i j k q} x y →
       1 + x * i ≡ y * j → j * k ≡ q * i →
       k ≡ (y * q ∸ x * k) * i
lem₉ {i} {j} {k} {q} x y eq eq′ =
  sym (NatProp.im≡jm+n⇒[i∸j]m≡n (y * q) (x * k) i k lemma)
  where
  lem   = solve 3 (λ a b c → a :* b :* c  :=  b :* c :* a) refl
  lemma = begin
    y * q * i        ≡⟨ lem y q i ⟩
    q * i * y        ≡⟨ cong (λ n → n * y) (sym eq′) ⟩
    j * k * y        ≡⟨ sym (lem y j k) ⟩
    y * j * k        ≡⟨ cong (λ n → n * k) (sym eq) ⟩
    (1 + x * i) * k  ≡⟨ solve 3 (λ x i k → (con 1 :+ x :* i) :* k
                                       :=  x :* k :* i :+ k)
                                refl x i k ⟩
    x * k * i + k    ∎

lem₁₀ : ∀ {a′} b c {d} e f → let a = suc a′ in
        a + b * (c * d * a) ≡ e * (f * d * a) →
        d ≡ 1
lem₁₀ {a′} b c {d} e f eq =
  NatProp.i*j≡1⇒j≡1 (e * f ∸ b * c) d
    (NatProp.im≡jm+n⇒[i∸j]m≡n (e * f) (b * c) d 1
       (NatProp.cancel-*-right (e * f * d) (b * c * d + 1) (begin
          e * f * d * a        ≡⟨ solve 4 (λ e f d a → e :* f :* d :* a
                                                   :=  e :* (f :* d :* a))
                                          refl e f d a ⟩
          e * (f * d * a)      ≡⟨ sym eq ⟩
          a + b * (c * d * a)  ≡⟨ solve 4 (λ a b c d → a :+ b :* (c :* d :* a)
                                                   :=  (b :* c :* d :+ con 1) :* a)
                                          refl a b c d ⟩
          (b * c * d + 1) * a  ∎)))
  where a = suc a′

lem₁₁ : ∀ {i j m n k d} x y →
       1 + y * j ≡ x * i → i * k ≡ m * d → j * k ≡ n * d →
       k ≡ (x * m ∸ y * n) * d
lem₁₁ {i} {j} {m} {n} {k} {d} x y eq eq₁ eq₂ =
  sym (NatProp.im≡jm+n⇒[i∸j]m≡n (x * m) (y * n) d k lemma)
  where
  assoc = solve 3 (λ x y z → x :* y :* z  :=  x :* (y :* z)) refl

  lemma = begin
    x * m * d        ≡⟨ assoc x m d ⟩
    x * (m * d)      ≡⟨ cong (_*_ x) (sym eq₁) ⟩
    x * (i * k)      ≡⟨ sym (assoc x i k) ⟩
    x * i * k        ≡⟨ cong₂ _*_ (sym eq) refl ⟩
    (1 + y * j) * k  ≡⟨ solve 3 (λ y j k → (con 1 :+ y :* j) :* k
                                       :=  y :* (j :* k) :+ k)
                                refl y j k ⟩
    y * (j * k) + k  ≡⟨ cong (λ p → y * p + k) eq₂ ⟩
    y * (n * d) + k  ≡⟨ cong₂ _+_ (sym $ assoc y n d) refl ⟩
    y * n * d + k    ∎


text:
{-# OPTIONS --safe #-}
module Cubical.Displayed.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence using (pathToEquiv; univalence; ua-ungluePath-Equiv)

open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.Relation.Binary
open BinaryRelation

open import Cubical.Displayed.Base

private
  variable
    ℓ ℓA ℓA' ℓP ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓ≅B' ℓC ℓ≅C : Level

-- induction principles

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) where
  open UARel 𝒮-A
  𝒮-J : {a : A}
        (P : (a' : A) → (p : a ≡ a') → Type ℓ)
        (d : P a refl)
        {a' : A}
        (p : a ≅ a')
        → P a' (≅→≡ p)
  𝒮-J {a} P d {a'} p
    = J (λ y q → P y q)
        d
        (≅→≡ p)

  𝒮-J-2 : {a : A}
            (P : (a' : A) → (p : a ≅ a') → Type ℓ)
            (d : P a (ρ a))
            {a' : A}
            (p : a ≅ a')
            → P a' p
  𝒮-J-2 {a = a} P d {a'} p
    = subst (λ r → P a' r) (Iso.leftInv (uaIso a a') p) g
    where
      g : P a' (≡→≅ (≅→≡ p))
      g = 𝒮-J (λ y q → P y (≡→≅ q)) d p

-- constructors

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB}
  (_≅ᴰ⟨_⟩_ : {a a' : A} → B a → UARel._≅_ 𝒮-A a a' → B a' → Type ℓ≅B)
  where

    open UARel 𝒮-A

    -- constructor that reduces ua to the case where p = ρ a by induction on p
    private
      𝒮ᴰ-make-aux : (uni : {a : A} (b b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ (b ≡ b'))
                    → ({a a' : A} (b : B a) (p : a ≅ a') (b' : B a') → (b ≅ᴰ⟨ p ⟩ b') ≃ PathP (λ i → B (≅→≡ p i)) b b')
      𝒮ᴰ-make-aux uni {a} {a'} b p
        = 𝒮-J-2 𝒮-A
                    (λ y q → (b' : B y) → (b ≅ᴰ⟨ q ⟩ b') ≃ PathP (λ i → B (≅→≡ q i)) b b')
                    (λ b' → uni' b')
                    p
        where
          g : (b' : B a) → (b ≡ b') ≡ PathP (λ i → B (≅→≡ (ρ a) i)) b b'
          g b' = subst (λ r → (b ≡ b') ≡ PathP (λ i → B (r i)) b b')
                       (sym (Iso.rightInv (uaIso a a) refl))
                       refl
          uni' : (b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ PathP (λ i → B (≅→≡ (ρ a) i)) b b'
          uni' b' = compEquiv (uni b b') (pathToEquiv (g b'))

    𝒮ᴰ-make-1 : (uni : {a : A} (b b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ (b ≡ b'))
                → DUARel 𝒮-A B ℓ≅B
    DUARel._≅ᴰ⟨_⟩_ (𝒮ᴰ-make-1 uni) = _≅ᴰ⟨_⟩_
    DUARel.uaᴰ (𝒮ᴰ-make-1 uni) = 𝒮ᴰ-make-aux uni

    -- constructor that reduces univalence further to contractibility of relational singletons

    𝒮ᴰ-make-2 : (ρᴰ : {a : A} → isRefl _≅ᴰ⟨ ρ a ⟩_)
                (contrTotal : (a : A) → contrRelSingl _≅ᴰ⟨ ρ a ⟩_)
                → DUARel 𝒮-A B ℓ≅B
    𝒮ᴰ-make-2 ρᴰ contrTotal = 𝒮ᴰ-make-1 (contrRelSingl→isUnivalent _ ρᴰ (contrTotal _))

-- relational isomorphisms

𝒮-iso→iso : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
               {B : Type ℓB} (𝒮-B : UARel B ℓ≅B)
               (F : RelIso (UARel._≅_ 𝒮-A) (UARel._≅_ 𝒮-B))
               → Iso A B
𝒮-iso→iso 𝒮-A 𝒮-B F
  = RelIso→Iso (UARel._≅_ 𝒮-A)
               (UARel._≅_ 𝒮-B)
               (UARel.≅→≡ 𝒮-A)
               (UARel.≅→≡ 𝒮-B)
               F

-- fiberwise relational isomorphisms

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {A' : Type ℓA'} {𝒮-A' : UARel A' ℓ≅A'}
  (F : Iso A A')
  {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {B' : A' → Type ℓB'} (𝒮ᴰ-B' : DUARel 𝒮-A' B' ℓ≅B') where

  open UARel 𝒮-A
  open DUARel 𝒮ᴰ-B renaming (_≅ᴰ⟨_⟩_ to _≅B⟨_⟩_
                            ; uaᴰ to uaB
                            ; fiberRel to fiberRelB
                            ; uaᴰρ to uaᴰρB)
  open DUARel 𝒮ᴰ-B' renaming (_≅ᴰ⟨_⟩_ to _≅B'⟨_⟩_
                             ; uaᴰ to uaB'
                             ; fiberRel to fiberRelB'
                             ; uaᴰρ to uaᴰρB')

  private
    f = Iso.fun F

    -- the following can of course be done slightly more generally
    -- for fiberwise binary relations

    F*fiberRelB' : (a : A) → Rel (B' (f a)) (B' (f a)) ℓ≅B'
    F*fiberRelB' a = fiberRelB' (f a)

  module _ (G : (a : A) → RelIso (fiberRelB a) (F*fiberRelB' a)) where
    private
      fiberIsoOver : (a : A) → Iso (B a) (B' (f a))
      fiberIsoOver a
        = RelIso→Iso (fiberRelB a)
                     (F*fiberRelB' a)
                     (equivFun (uaᴰρB _ _))
                     (equivFun (uaᴰρB' _ _))
                     (G a)

    -- DUARelFiberIsoOver→TotalIso produces an isomorphism of total spaces
    -- from a relational isomorphism between B a and (F * B) a
    𝒮ᴰ-fiberIsoOver→totalIso : Iso (Σ A B) (Σ A' B')
    𝒮ᴰ-fiberIsoOver→totalIso = Σ-cong-iso F fiberIsoOver

max_stars_repo_name: FernandoLarrain/cubical


text:
open import Oscar.Prelude

module Oscar.Class.Map where

module _
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {ℓ₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø ℓ₁)
  {ℓ₂} (_∼₂_ : 𝔒₁ → 𝔒₁ → Ø ℓ₂)
  where
  𝓶ap = ∀ {x y} → x ∼₁ y → x ∼₂ y
  record 𝓜ap : Ø 𝔬₁ ∙̂ ℓ₁ ∙̂ ℓ₂ where field map : 𝓶ap
open 𝓜ap ⦃ … ⦄ public


text:
-- Andreas, 2016-05-04, issue 1954

module _ where

module P (A : Set) where
  record R : Set where
    field f : A

open module Q A = P A

module M (A : Set) (r : R A) where
  open R A r public

-- Parameter A should be hidden in R.f
works : ∀{A} → R A → A
works r = R.f r

-- Record value should not be hidden in M.f
test : ∀{A} → R A → A
test r = M.f r

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-12-16, issue #2868.

-- Printing record fields correctly inside the record definition
-- in the presence of --postfix-projections.

{-# OPTIONS --postfix-projections #-}

open import Agda.Builtin.Equality

postulate
  A : Set

record R : Set where
  field
    a : A
    same : a ≡ a
  test : A
  test = same

-- (We are reifying  Var 0 [Proj ProjSystem Issue2868.R.a])

-- WAS:    .a ≡ .a !=< A of type Set    -- Note the extra dots!
-- Expected: a ≡ a !=< A of type Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module _ where

open import Data.Nat using (_+_)
open import Data.Nat.Properties.Simple using ( +-comm ; +-assoc)
open import utility
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Environment as Env
open import Esterel.Context
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import sn-calculus
open import context-properties
open import Esterel.Lang.Binding
open import Data.Maybe using ( just )
open import Function using (_$_)

open import Data.FiniteMap
import Data.OrderedListMap as OMap
open import Data.Nat as Nat using (ℕ)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar

open import sn-calculus-confluence.helper
open import sn-calculus-confluence.rec
open import sn-calculus-confluence.potrec
open import sn-calculus-confluence.potpot

ρ-conf : ∀{p FV BV ql qr θ qi A} → CorrectBinding p FV BV → p sn⟶₁ ql → p sn⟶₁ qr → p ≡ (ρ⟨ θ , A ⟩· qi)
         → ql ≡ qr
         ⊎ (∃ (λ o → ql sn⟶₁ o × qr sn⟶₁ o))
         ⊎ ql sn⟶₁ qr
         ⊎ qr sn⟶₁ ql
ρ-conf {(ρ⟨ θ , .A ⟩· qi)}{ql = ql}{qr = qr}{A = A} cb redl redr refl with ρ-stays-ρ-sn⟶₁ redl | ρ-stays-ρ-sn⟶₁ redr
... | (θl , qlin , Al , refl) | (θr , qrin , Ar , refl) with get-view redl | get-view redr
ρ-conf {(ρ⟨ θ , .A ⟩· qi)}{ql = ql}{qr = qr}{A = A} cb redl redr refl | (θl , qlin , Al , refl) | (θr , qrin , Ar , refl) | inj₁ (_ , _ , _ , _ , _ , viewl) | inj₁ (_ , _ , _ , _ , _ , viewr)
   with E-view-main-bind viewl viewr
... | inj₁ (e= , q= , θ= , A=) rewrite e= | q= | θ= | A= = inj₁ refl
... | inj₂ ~a with ρ-conf-rec cb _ _ ~a redl redr _ _ viewl viewr
... | (θo , Ao , so , _ , _ , _ , _ , _ , _ , redol , redor , _) = inj₂ $ inj₁ ((ρ⟨ θo , Ao ⟩· so) , redol , redor)
ρ-conf {(ρ⟨ θ  , .A ⟩· qi)}{ql = ql}{qr = qr}{A = A} cb redl redr refl | (θl , qlin , Al , refl) | (θr , qrin , Ar , refl) | inj₁ (_ , _ , _ , _ , _ , viewl) | inj₂ (_ , _ , viewr)
  with ρ-pot-conf-rec cb viewr viewl
... | inj₁ redo = inj₂ (inj₂ (inj₂ redo))
... | inj₂ (s , env , Ao , redol , redor) = inj₂ $ inj₁ (ρ⟨ env , Ao ⟩· s , redor , redol)
ρ-conf {(ρ⟨ θ  , .A ⟩· qi)}{ql = ql}{qr = qr}{A = A} cb redl redr refl | (θl , qlin , Al , refl) | (θr , qrin , Ar , refl) | inj₂ (_ , _ , viewl) | inj₁ (_ , _ , _ , _ , _ , viewr)
    with ρ-pot-conf-rec cb viewl viewr
... | inj₁ redo = inj₂ (inj₂ (inj₁ redo))
... | inj₂ (s , env , Ao , redol , redor) = inj₂ $ inj₁ ((ρ⟨ env , Ao ⟩· s) , redol , redor)
ρ-conf {(ρ⟨ θ  , .A ⟩· qi)}{ql = ql}{qr = qr}{A = A} cb redl redr refl | (θl , qlin , Al , refl) | (θr , qrin , Ar , refl) | inj₂ (_ , _ , viewl) | inj₂ (_ , _ , viewr)
    with pot-pot-conf-rec viewl viewr
... | inj₁ eq = inj₁ eq
... | inj₂ (env , redol , redor) = inj₂ $ inj₁ (ρ⟨ env , A ⟩· qi , redol , redor)

R-confluent : ∀{p q r BV FV} → CorrectBinding p BV FV → p sn⟶₁ q → p sn⟶₁ r
                                   → q ≡ r
                                   ⊎ (∃ (λ s → q sn⟶₁ s × r sn⟶₁ s))
                                   ⊎ q sn⟶₁ r
                                   ⊎ r sn⟶₁ q
R-confluent {.(_ ∥ _)} cb (rpar-done-right p'' q'') (rpar-done-right p' q') = inj₁ ( value-max-unique{d1 = (dhalted p'')}{d2 = q''}{d3 = (dhalted p')}{d4 = q'} )
R-confluent {.(_ ∥ _)} cb (rpar-done-right p'' q'') (rpar-done-left p' q') = inj₁ ( value-max-unique{d1 = (dhalted p'')}{d2 = q''}{d3 = p'}{d4 = (dhalted q')} )
R-confluent {.(_ ∥ _)} cb (rpar-done-left p'' q'') (rpar-done-right p' q') = inj₁ (value-max-unique{d1 = (p'')}{d2 =(dhalted q'')}{d3 = (dhalted p')}{d4 = (q')})
R-confluent {.(_ ∥ _)} cb (rpar-done-left p'' q'') (rpar-done-left p' q') = inj₁ (value-max-unique{d1 = p''}{d2 = (dhalted q'')}{d3 = p'}{d4 = (dhalted q')})
R-confluent {.(loop _)} cb rloop-unroll rloop-unroll = inj₁ refl
R-confluent {.(nothin >> _)} cb rseq-done rseq-done = inj₁ refl
R-confluent {.(exit _ >> _)} cb rseq-exit rseq-exit = inj₁ refl
R-confluent {.(loopˢ (exit _) _)} cb rloopˢ-exit rloopˢ-exit = inj₁ refl
R-confluent {.(suspend nothin _)} cb (rsuspend-done hnothin) (rsuspend-done hnothin) = inj₁ refl
R-confluent {.(suspend (exit n) _)} cb (rsuspend-done (hexit n)) (rsuspend-done (hexit .n)) = inj₁ refl
R-confluent {.(trap nothin)} cb (rtrap-done hnothin) (rtrap-done hnothin) = inj₁ refl
R-confluent {.(trap (exit n))} cb (rtrap-done (hexit n)) (rtrap-done (hexit .n)) = inj₁ refl
R-confluent {.(signl _ _)} cb rraise-signal rraise-signal = inj₁ refl
R-confluent {p@(ρ⟨ _ , _ ⟩· _)} cb redl redr = ρ-conf cb redl redr refl


text:
module Categories.Functor.Construction.Exponential where

open import Categories.Category
open import Categories.Category.Product using (Product)
open import Categories.Category.CartesianClosed
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Object.Exponential
open import Categories.Functor.Bifunctor

open import Data.Product using (_,_; proj₁; proj₂)

module _ {o ℓ e} (𝒞 : Category o ℓ e) (cartesianClosed : CartesianClosed 𝒞) where
  open import Categories.Morphism.Reasoning 𝒞

  open CartesianClosed cartesianClosed
  open Cartesian cartesian
  open BinaryProducts products

  open Category 𝒞
  open Equiv

  private
    P : Category _ _ _
    P = Product 𝒞 op

  Exp : Bifunctor 𝒞 (Category.op 𝒞) 𝒞
  Exp = record
              { F₀ = λ (x , y) → x ^ y
              ; F₁ = λ (f , g) → λg (f ∘ eval′ ∘ (id ⁂ g))
              ; identity = λ {A} →
                  begin
                    λg (id ∘ eval′ ∘ (id ⁂ id))
                  ≈⟨ λ-cong identityˡ ⟩
                    λg (eval′ ∘ (id ⁂ id))
                  ≈⟨ λ-cong (elimʳ (Equiv.trans (⟨⟩-cong₂ identityˡ identityˡ) η)) ⟩
                    λg eval′
                  ≈⟨ η-id′ ⟩
                    id
                  ∎
              ; homomorphism = λ {X} {Y} {Z} {f} {g} →
                  begin
                    λg ((proj₁ g ∘ proj₁ f) ∘ eval′ ∘ (id ⁂ (proj₂ f ∘ proj₂ g)))
                  ≈⟨ λ-cong assoc ⟩
                    λg (proj₁ g ∘ proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f ∘ proj₂ g))
                  ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (∘-resp-≈ʳ (trans ⁂∘⁂ (⁂-cong₂ identity² refl))))) ⟩
                    λg (proj₁ g ∘ proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f) ∘ (id ⁂ proj₂ g))
                  ≈˘⟨ λ-cong (∘-resp-≈ʳ assoc²') ⟩
                    λg (proj₁ g ∘ (proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f)) ∘ (id ⁂ proj₂ g))
                  ≈˘⟨ λ-cong (∘-resp-≈ʳ (pullˡ β′)) ⟩
                    λg (proj₁ g ∘ eval′ ∘ (λg (proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f)) ⁂ id) ∘ (id ⁂ proj₂ g))
                  ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ ⁂∘⁂)) ⟩
                    λg (proj₁ g ∘ eval′ ∘ (λg (proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f)) ∘ id ⁂ id ∘ proj₂ g))
                  ≈⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ (⁂-cong₂ (trans identityʳ (sym identityˡ)) (trans identityˡ (sym identityʳ))))) ⟩
                    λg (proj₁ g ∘ eval′ ∘ (id ∘ λg (proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f)) ⁂ proj₂ g ∘ id))
                  ≈˘⟨ λ-cong (∘-resp-≈ʳ (∘-resp-≈ʳ ⁂∘⁂)) ⟩
                    λg (proj₁ g ∘ eval′ ∘ (id ⁂ proj₂ g) ∘ (λg (proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f)) ⁂ id))
                  ≈˘⟨ λ-cong assoc²' ⟩
                    λg ((proj₁ g ∘ eval′ ∘ (id ⁂ proj₂ g)) ∘ (λg (proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f)) ⁂ id))
                  ≈˘⟨ exp.subst product product ⟩
                    λg (proj₁ g ∘ eval′ ∘ (id ⁂ proj₂ g)) ∘ λg (proj₁ f ∘ eval′ ∘ (id ⁂ proj₂ f))
                  ∎
              ; F-resp-≈ = λ (x , y) → λ-cong (∘-resp-≈ x (∘-resp-≈ʳ (⁂-cong₂ Equiv.refl y)))
              }
    where open HomReasoning

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


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

open import Level using (_⊔_; suc)
open import Relation.Unary using (Pred)

open import Categories.Category.Core using (Category)
open import Categories.Functor.Core using (Functor)
open import Categories.Morphism using (Iso)

record HasDagger {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C
  infix 10 _†

  field
    _† : ∀ {A B} → A ⇒ B → B ⇒ A
    †-identity : ∀ {A} → id {A} † ≈ id
    †-homomorphism : ∀ {A B C} {f : A ⇒ B} {g : B ⇒ C} → (g ∘ f) † ≈ f † ∘ g †
    †-resp-≈ : ∀ {A B} {f g : A ⇒ B} → f ≈ g → f † ≈ g †
    †-involutive : ∀ {A B} (f : A ⇒ B) → f † † ≈ f

  †-Functor : Functor op C
  †-Functor = record
    { F₀ = λ A → A
    ; F₁ = _†
    ; identity = †-identity
    ; homomorphism = †-homomorphism
    ; F-resp-≈ = †-resp-≈
    }

  isUnitary : ∀ {A B} → Pred (A ⇒ B) e
  isUnitary f = Iso C f (f †)

  isSelfAdjoint : ∀ {A} → Pred (A ⇒ A) e
  isSelfAdjoint f = f † ≈ f

record DaggerCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    C : Category o ℓ e
    hasDagger : HasDagger C

  open Category C public
  open HasDagger hasDagger public

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Andreas, 2017-01-12, issue #2386

postulate
  A : Set

-- Should be rejected:
data Eq : (B : Set) (x y : B) → Set where
  refl : (x : A) → Eq A x x

{-# BUILTIN EQUALITY Eq #-}

-- Expected error:
-- Wrong type of constructor of BUILTIN EQUALITY
-- when checking the pragma BUILTIN EQUALITY Eq


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Reduction
open import Definition.LogicalRelation.Substitution.Conversion
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.Introductions.Prod
open import Definition.LogicalRelation.Substitution.Introductions.Fst
open import Definition.LogicalRelation.Substitution.Introductions.Snd

open import Tools.Product
import Tools.PropositionalEquality as PE

Σ-β₁ᵛ : ∀ {F G t u Γ l}
        ([Γ] : ⊩ᵛ Γ)
        ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
        ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
        ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
        ([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ G [ t ] / [Γ] / substS {F} {G} [Γ] [F] [G] [t])
      → Γ ⊩ᵛ⟨ l ⟩ fst (prod t u) ≡ t ∷ F / [Γ] / [F]
Σ-β₁ᵛ {F} {G} {t} {u} {Γ} {l} [Γ] [F] [G] [t] [u] =
  let [Gt] = substS {F} {G} {t} [Γ] [F] [G] [t]
      fst⇒t : Γ ⊩ᵛ fst (prod t u) ⇒ t ∷ F / [Γ]
      fst⇒t = (λ {Δ} {σ} ⊢Δ [σ] →
                let ⊩σF = proj₁ ([F] ⊢Δ [σ])
                    ⊢σF = escape ⊩σF

                    [Fσ] = liftSubstS {F = F} {σ = σ} [Γ] ⊢Δ [F] [σ]
                    ⊩σG : Δ ∙ subst σ F ⊩⟨ l ⟩ subst (liftSubst σ) G
                    ⊩σG = proj₁ ([G] (⊢Δ ∙ ⊢σF) [Fσ])
                    ⊢σG = escape ⊩σG

                    ⊩σt = proj₁ ([t] ⊢Δ [σ])
                    ⊢σt = escapeTerm ⊩σF ⊩σt

                    ⊩σGt₁ = proj₁ ([Gt] ⊢Δ [σ])
                    ⊩σGt = irrelevance′ (singleSubstLift G t) ⊩σGt₁

                    ⊩σu₁ = proj₁ ([u] ⊢Δ [σ])
                    ⊩σu = irrelevanceTerm′ (singleSubstLift G t) ⊩σGt₁ ⊩σGt ⊩σu₁
                    ⊢σu = escapeTerm ⊩σGt ⊩σu
                in  Σ-β₁ ⊢σF ⊢σG ⊢σt ⊢σu)
  in  proj₂ (redSubstTermᵛ {F} {fst (prod t u)} {t} [Γ] fst⇒t [F] [t])

Σ-β₂ᵛ : ∀ {F G t u Γ l}
        ([Γ] : ⊩ᵛ Γ)
        ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
        ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
        ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
        ([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ G [ t ] / [Γ] / substS {F} {G} [Γ] [F] [G] [t])
      → Γ ⊩ᵛ⟨ l ⟩ snd (prod t u) ≡ u ∷ G [ fst (prod t u) ] / [Γ]
          / substS {F} {G} [Γ] [F] [G]
                   (fstᵛ {F} {G} {prod t u} [Γ] [F] [G]
                         (prodᵛ {F} {G} {t} {u} [Γ] [F] [G] [t] [u]))
Σ-β₂ᵛ {F} {G} {t} {u} {Γ} {l} [Γ] [F] [G] [t] [u] =
  let [Gt] = substS {F} {G} {t} [Γ] [F] [G] [t]
      [prod] = prodᵛ {F} {G} {t} {u} [Γ] [F] [G] [t] [u]
      [fst] = fstᵛ {F} {G} {prod t u} [Γ] [F] [G] [prod]
      [Gfst] = substS {F} {G} {fst (prod t u)} [Γ] [F] [G] [fst]
      [fst≡t] = Σ-β₁ᵛ {F} {G} {t} {u} [Γ] [F] [G] [t] [u]
      [Gfst≡Gt] = substSEq {F} {F} {G} {G} {fst (prod t u)} {t}
                           [Γ] [F] [F] (reflᵛ {F} [Γ] [F])
                               [G] [G] (reflᵛ {G} {Γ ∙ F} ([Γ] ∙ [F]) [G])
                               [fst] [t] [fst≡t]

      [u]Gfst = conv₂ᵛ {u} {G [ fst (prod t u) ]} {G [ t ]}
                       [Γ] [Gfst] [Gt] [Gfst≡Gt] [u]

      snd⇒t : Γ ⊩ᵛ snd (prod t u) ⇒ u ∷ G [ fst (prod t u) ] / [Γ]
      snd⇒t = (λ {Δ} {σ} ⊢Δ [σ] →
                let ⊩σF = proj₁ ([F] ⊢Δ [σ])
                    ⊢σF = escape ⊩σF

                    [Fσ] = liftSubstS {F = F} {σ = σ} [Γ] ⊢Δ [F] [σ]
                    ⊩σG : Δ ∙ subst σ F ⊩⟨ l ⟩ subst (liftSubst σ) G
                    ⊩σG = proj₁ ([G] (⊢Δ ∙ ⊢σF) [Fσ])
                    ⊢σG = escape ⊩σG

                    ⊩σt = proj₁ ([t] ⊢Δ [σ])
                    ⊢σt = escapeTerm ⊩σF ⊩σt

                    ⊩σGt₁ = proj₁ ([Gt] ⊢Δ [σ])
                    ⊩σGt = irrelevance′ (singleSubstLift G t) ⊩σGt₁

                    ⊩σu₁ = proj₁ ([u] ⊢Δ [σ])
                    ⊩σu = irrelevanceTerm′ (singleSubstLift G t) ⊩σGt₁ ⊩σGt ⊩σu₁
                    ⊢σu = escapeTerm ⊩σGt ⊩σu

                    snd⇒t : Δ ⊢ _ ⇒ _ ∷ _
                    snd⇒t = Σ-β₂ ⊢σF ⊢σG ⊢σt ⊢σu
                    σGfst≡σGfst = PE.subst (λ x → Δ ⊢ x ≡ subst σ (G [ fst (prod t u) ]))
                                           (singleSubstLift G (fst (prod t u)))
                                           (refl (escape (proj₁ ([Gfst] ⊢Δ [σ]))))
              in  conv snd⇒t σGfst≡σGfst)
  in  proj₂ (redSubstTermᵛ {G [ fst (prod t u) ]} {snd (prod t u)} {u} [Γ] snd⇒t [Gfst] [u]Gfst)

Σ-η′ : ∀ {F G p r Γ l l′}
         ([F] : Γ ⊩⟨ l′ ⟩ F)
         ([Gfstp] : Γ ⊩⟨ l′ ⟩ G [ fst p ])
         ([ΣFG]₁ : Γ ⊩⟨ l ⟩B⟨ BΣ ⟩ Σ F ▹ G )
         ([p] : Γ ⊩⟨ l ⟩ p ∷ Σ F ▹ G / B-intr BΣ [ΣFG]₁)
         ([r] : Γ ⊩⟨ l ⟩ r ∷ Σ F ▹ G / B-intr BΣ [ΣFG]₁)
         ([fst≡] : Γ ⊩⟨ l′ ⟩ fst p ≡ fst r ∷ F / [F])
         ([snd≡] : Γ ⊩⟨ l′ ⟩ snd p ≡ snd r ∷ G [ fst p ] / [Gfstp])
       → Γ ⊩⟨ l ⟩ p ≡ r ∷ Σ F ▹ G / B-intr BΣ [ΣFG]₁
Σ-η′ {F} {G} {p} {r} {Γ} {l} {l′}
     [F] [Gfstp]
     [ΣFG]₁@(noemb (Bᵣ F₁ G₁ D ⊢F ⊢G A≡A [F]₁ [G]₁ G-ext))
     [p]@(Σₜ p′ dₚ p′Prod p′≅p′ wk[fstp′] wk[sndp′])
     [r]@(Σₜ r′ dᵣ r′Prod r′≅r′ wk[fstr′] wk[sndr′])
     [fst≡]
     [snd≡]
       with B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
... | PE.refl , PE.refl =
  let [ΣFG] = B-intr BΣ [ΣFG]₁
      ⊢Γ = wf ⊢F
      wk[F] = [F]₁ id ⊢Γ
      wk[Gfstp′] = [G]₁ id ⊢Γ wk[fstp′]

      fstp⇒* : Γ ⊢ fst p ⇒* fst p′ ∷ U.wk id F
      fstp⇒* = PE.subst (λ x → Γ ⊢ _ ⇒* _ ∷ x)
                        (PE.sym (wk-id F))
                        (fst-subst* ⊢F ⊢G (redₜ dₚ))
      fstr⇒* = PE.subst (λ x → Γ ⊢ _ ⇒* _ ∷ x)
                        (PE.sym (wk-id F))
                        (fst-subst* ⊢F ⊢G (redₜ dᵣ))

      --wk[fstp≡] : Γ ⊩⟨ l ⟩ fst p ≡ fst p′ ∷ U.wk id F / wk[F]
      wk[fstp] , wk[fstp≡] = redSubst*Term fstp⇒* wk[F] wk[fstp′]
      wk[fstr] , wk[fstr≡] = redSubst*Term fstr⇒* wk[F] wk[fstr′]

      wk[fst≡] = irrelevanceEqTerm′ (PE.sym (wk-id F))
                                    [F] wk[F]
                                    [fst≡]
      wk[fst′≡] : Γ ⊩⟨ l ⟩ fst p′ ≡ fst r′ ∷ U.wk id F / wk[F]
      wk[fst′≡] = transEqTerm wk[F]
                             (symEqTerm wk[F] wk[fstp≡])
                             (transEqTerm wk[F] wk[fst≡] wk[fstr≡])

      [p′] : Γ ⊩⟨ l ⟩ p′ ∷ Σ F ▹ G / [ΣFG]
      [p′] = Σₜ p′ (idRedTerm:*: (⊢u-redₜ dₚ)) p′Prod p′≅p′ wk[fstp′] wk[sndp′]
      [r′] = Σₜ r′ (idRedTerm:*: (⊢u-redₜ dᵣ)) r′Prod r′≅r′ wk[fstr′] wk[sndr′]

      sndp⇒*₁ : Γ ⊢ snd p ⇒* snd p′ ∷ G [ fst p ]
      sndp⇒*₁ = snd-subst* [F] [ΣFG] [p′] (redₜ dₚ)
      sndr⇒*₁ = snd-subst* [F] [ΣFG] [r′] (redₜ dᵣ)

      wk[Gfstp] = [G]₁ id ⊢Γ wk[fstp]
      wk[Gfstr] = [G]₁ id ⊢Γ wk[fstr]
      [Gfstr] = irrelevance′ (PE.cong (λ x → x [ fst r ]) (wk-lift-id G)) wk[Gfstr]
      wk[Gfstr′] = [G]₁ id ⊢Γ wk[fstr′]

      [Gfstp≡wkGfstp′] : Γ ⊩⟨ l′ ⟩ G [ fst p ] ≡ U.wk (lift id) G [ fst p′ ] / [Gfstp]
      [Gfstp≡wkGfstp′] = irrelevanceEq′ (PE.cong (λ x → x [ fst p ]) (wk-lift-id G))
                                        ([G]₁ id ⊢Γ wk[fstp]) [Gfstp]
                                        (G-ext id ⊢Γ wk[fstp] wk[fstp′] wk[fstp≡])
      [Gfstr≡Gfstp] : Γ ⊩⟨ _ ⟩ G [ fst r ] ≡ G [ fst p ] / [Gfstr]
      [Gfstr≡Gfstp] = irrelevanceEq″ (PE.cong (λ x → x [ fst r ]) (wk-lift-id G))
                                     (PE.cong (λ x → x [ fst p ]) (wk-lift-id G))
                                     wk[Gfstr] [Gfstr]
                                     (symEq wk[Gfstp] wk[Gfstr]
                                            (G-ext id ⊢Γ wk[fstp] wk[fstr] wk[fst≡]))
      [Gfstr≡wkGfstp′] : Γ ⊩⟨ l ⟩ G [ fst r ] ≡ U.wk (lift id) G [ fst p′ ] / [Gfstr]
      [Gfstr≡wkGfstp′] = transEq [Gfstr] [Gfstp] wk[Gfstp′]
                                 [Gfstr≡Gfstp] [Gfstp≡wkGfstp′]
      [wkGfstr′≡wkGfstp′] : Γ ⊩⟨ l ⟩ U.wk (lift id) G [ fst r′ ] ≡ U.wk (lift id) G [ fst p′ ] / wk[Gfstr′]
      [wkGfstr′≡wkGfstp′] = G-ext id ⊢Γ wk[fstr′] wk[fstp′] (symEqTerm wk[F] wk[fst′≡])

      sndp⇒* : Γ ⊢ snd p ⇒* snd p′ ∷ U.wk (lift id) G [ fst p′ ]
      sndp⇒* = conv* sndp⇒*₁ (≅-eq (escapeEq [Gfstp] [Gfstp≡wkGfstp′]))
      sndr⇒* = conv* sndr⇒*₁ (≅-eq (escapeEq [Gfstr] [Gfstr≡wkGfstp′]))

      wk[sndp≡] : Γ ⊩⟨ l ⟩ snd p ≡ snd p′ ∷ U.wk (lift id) G [ fst p′ ] / wk[Gfstp′]
      wk[sndp≡] = proj₂ (redSubst*Term sndp⇒* wk[Gfstp′] wk[sndp′])
      wk[sndr≡] = proj₂ (redSubst*Term sndr⇒* wk[Gfstp′]
                                       (convTerm₁ wk[Gfstr′] wk[Gfstp′]
                                                  [wkGfstr′≡wkGfstp′]
                                                  wk[sndr′]))

      wk[snd≡] : Γ ⊩⟨ l ⟩ snd p ≡ snd r ∷ U.wk (lift id) G [ fst p′ ] / wk[Gfstp′]
      wk[snd≡] = convEqTerm₁ [Gfstp] wk[Gfstp′] [Gfstp≡wkGfstp′] [snd≡]

      wk[snd′≡] : Γ ⊩⟨ l ⟩ snd p′ ≡ snd r′ ∷ U.wk (lift id) G [ fst p′ ] / wk[Gfstp′]
      wk[snd′≡] = transEqTerm wk[Gfstp′]
                              (symEqTerm wk[Gfstp′] wk[sndp≡])
                              (transEqTerm wk[Gfstp′] wk[snd≡] wk[sndr≡])

      p′≅r′ : Γ ⊢ p′ ≅ r′ ∷ Σ F ▹ G
      p′≅r′ = ≅-Σ-η ⊢F ⊢G (⊢u-redₜ dₚ) (⊢u-redₜ dᵣ)
                    p′Prod r′Prod
                    (PE.subst (λ x → Γ ⊢ _ ≅ _ ∷ x)
                              (wk-id F)
                              (escapeTermEq wk[F] wk[fst′≡]))
                    (PE.subst (λ x → Γ ⊢ _ ≅ _ ∷ x [ fst p′ ])
                              (wk-lift-id G)
                              (escapeTermEq wk[Gfstp′] wk[snd′≡]))
  in  Σₜ₌ p′ r′ dₚ dᵣ p′Prod r′Prod
          p′≅r′ [p] [r]
          wk[fstp′]
          wk[fstr′]
          wk[fst′≡]
          wk[snd′≡]
Σ-η′ [F] [Gfst] (emb 0<1 x) = Σ-η′ [F] [Gfst] x

Σ-η″ : ∀ {F G p r Γ l}
        ([F] : Γ ⊩⟨ l ⟩ F)
        ([Gfst] : Γ ⊩⟨ l ⟩ G [ fst p ])
        ([ΣFG] : Γ ⊩⟨ l ⟩ Σ F ▹ G)
        ([p] : Γ ⊩⟨ l ⟩ p ∷ Σ F ▹ G / [ΣFG])
        ([r] : Γ ⊩⟨ l ⟩ r ∷ Σ F ▹ G / [ΣFG])
        ([fst≡] : Γ ⊩⟨ l ⟩ fst p ≡ fst r ∷ F / [F])
        ([snd≡] : Γ ⊩⟨ l ⟩ snd p ≡ snd r ∷ G [ fst p ] / [Gfst])
      → Γ ⊩⟨ l ⟩ p ≡ r ∷ Σ F ▹ G / [ΣFG]
Σ-η″ {F} {G} {t} {Γ} {l} [F] [Gfst] [ΣFG] [p] [r] [fst≡] [snd≡] =
  let [ΣFG]′ = B-intr BΣ (B-elim BΣ [ΣFG])
      [p]′ = irrelevanceTerm [ΣFG] [ΣFG]′ [p]
      [r]′ = irrelevanceTerm [ΣFG] [ΣFG]′ [r]
      [p≡]′ = Σ-η′ [F] [Gfst] (B-elim BΣ [ΣFG]) [p]′ [r]′ [fst≡] [snd≡]
  in  irrelevanceEqTerm [ΣFG]′ [ΣFG] [p≡]′

Σ-ηᵛ : ∀ {F G p r Γ l}
         ([Γ] : ⊩ᵛ Γ)
         ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
         ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
       → let [ΣFG] = Σᵛ {F} {G} [Γ] [F] [G] in
         ([p] : Γ ⊩ᵛ⟨ l ⟩ p ∷ Σ F ▹ G / [Γ] / [ΣFG])
         ([r] : Γ ⊩ᵛ⟨ l ⟩ r ∷ Σ F ▹ G / [Γ] / [ΣFG])
         ([fst≡] : Γ ⊩ᵛ⟨ l ⟩ fst p ≡ fst r ∷ F / [Γ] / [F])
       → let [Gfst] = substS {F} {G} [Γ] [F] [G] (fstᵛ {F} {G} {p} [Γ] [F] [G] [p]) in
         ([snd≡] : Γ ⊩ᵛ⟨ l ⟩ snd p ≡ snd r ∷ G [ fst p ] / [Γ] / [Gfst])
       → Γ ⊩ᵛ⟨ l ⟩ p ≡ r ∷ Σ F ▹ G / [Γ] / [ΣFG]
Σ-ηᵛ {F} {G} {p} {r} {Γ} {l} [Γ] [F] [G] [p] [r] [fst≡] [snd≡] {Δ} {σ} ⊢Δ [σ] =
  let [ΣFG] = Σᵛ {F} {G} [Γ] [F] [G]
      [Gfst] = substS {F} {G} [Γ] [F] [G] (fstᵛ {F} {G} {p} [Γ] [F] [G] [p])
      ⊩σF = proj₁ ([F] ⊢Δ [σ])
      ⊩σGfst₁ = proj₁ ([Gfst] ⊢Δ [σ])
      ⊩σGfst = irrelevance′ (singleSubstLift G (fst p)) ⊩σGfst₁
      ⊩σΣFG = proj₁ ([ΣFG] ⊢Δ [σ])
      ⊩σp = proj₁ ([p] ⊢Δ [σ])
      ⊩σr = proj₁ ([r] ⊢Δ [σ])
      σfst≡ = [fst≡] ⊢Δ [σ]
      σsnd≡₁ = [snd≡] ⊢Δ [σ]
      σsnd≡ = irrelevanceEqTerm′ (singleSubstLift G (fst p)) ⊩σGfst₁ ⊩σGfst σsnd≡₁
  in  Σ-η″ ⊩σF ⊩σGfst ⊩σΣFG ⊩σp ⊩σr σfst≡ σsnd≡


text:
Finite : Domain → Formula
Finite(s) = ∃ₛ(ℕ)(n ↦ s ≼ 𝕟(n)) -- TODO: Now this means that there is an injection (s → 𝕟(n)), which is equivalent to the existance of an surjection (𝕟(n) → s) because stuff that follows from excluded middle (more specifically ((s ≼ 𝕟(n)) ↔ (𝕟(n) ≽ s))). Define ∑ (summation over finite sets) by using the existance of a finite sequence

-- reduce : (_▫_ : Domain → Domain → Domain) → ⦃ _ : Commutativity(_▫_) ⦄ → ⦃ _ : Associativity(_▫_) ⦄ → ⦃ _ : Identity(_▫_) ⦄ → (s : Domain) → ⦃ _ : Finite(s) ⦄ → Domain
-- reduce₀ : (_▫_ : Domain → Domain → Domain) → ⦃ _ : Commutativity(_▫_) ⦄ → ⦃ _ : Associativity(_▫_) ⦄ → (s : Domain) → ⦃ _ : Finite(s) ⦄ → Domain → Domain

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Cubical.Algebra.Base public
open import Cubical.Algebra.Definitions public

open import Cubical.Algebra.Structures public using (IsSemigroup; issemigroup)
open import Cubical.Algebra.Bundles public using (Semigroup; mksemigroup; SemigroupCarrier)
open import Cubical.Structures.Carrier public

open import Cubical.Algebra.Semigroup.Properties public
open import Cubical.Algebra.Semigroup.Morphism public
open import Cubical.Algebra.Semigroup.MorphismProperties public hiding (isPropIsSemigroup)


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Semirings.Definition
open import Orders.Total.Definition
open import Lists.Lists

module Vectors where

data Vec {a : _} (X : Set a) : ℕ -> Set a where
  [] : Vec X zero
  _,-_ : {n : ℕ} -> X -> Vec X n -> Vec X (succ n)

infixr 10 _,-_

vecLen : {a : _} {X : Set a} {n : ℕ} → Vec X n → ℕ
vecLen {a} {X} {n} v = n

vecHead : {a : _} {X : Set a} {n : ℕ} → Vec X (succ n) → X
vecHead (x ,- xs) = x

vecTail : {a : _} {X : Set a} {n : ℕ} → Vec X (succ n) → Vec X n
vecTail (x ,- xs) = xs

vecIsHeadPlusTail : {a : _} {X : Set a} {n : ℕ} → (xs : Vec X (succ n)) → (vecHead xs ,- vecTail xs) ≡ xs
vecIsHeadPlusTail (x ,- xs) = refl

_+V_ : {a : _} {X : Set a} {m n : ℕ} → Vec X m → Vec X n → Vec X (m +N n)
[] +V ys = ys
(x ,- xs) +V ys = (x ,- (xs +V ys))

vecIndex : {a : _} {X : Set a} {m : ℕ} → Vec X m → (i : ℕ) → .(i <N m) → X
vecIndex [] zero ()
vecIndex (x ,- vec) zero i<m = x
vecIndex [] (succ i) ()
vecIndex (x ,- vec) (succ i) i<m = vecIndex vec i (canRemoveSuccFrom<N i<m)

vecLast : {a : _} {X : Set a} {m : ℕ} → Vec X m → (0 <N m) → X
vecLast {a} {X} {zero} v ()
vecLast {a} {X} {succ zero} (x ,- []) _ = x
vecLast {a} {X} {succ (succ m)} (x ,- v) _ = vecLast v (succIsPositive m)

vecLast' : {a : _} {X : Set a} {m : ℕ} → Vec X (succ m) → X
vecLast' {m = m} v = vecLast v (le m (applyEquality succ (Semiring.sumZeroRight ℕSemiring m)))

vecAppend : {a : _} {X : Set a} {m : ℕ} → Vec X m → (x : X) → Vec X (succ m)
vecAppend {a} {X} {zero} [] x = x ,- []
vecAppend {a} {X} {succ m} (y ,- v) x = y ,- vecAppend v x

vecAppendIsNowLast : {a : _} {X : Set a} {m : ℕ} → (x : X) → (v : Vec X m) → (vecLast (vecAppend v x) (succIsPositive m)) ≡ x
vecAppendIsNowLast {a} {X} {zero} x [] = refl
vecAppendIsNowLast {a} {X} {succ m} x (y ,- v) = vecAppendIsNowLast x v

vecRev : {a : _} {X : Set a} {m : ℕ} → Vec X m → Vec X m
vecRev {a} {X} {zero} [] = []
vecRev {a} {X} {succ m} (x ,- v) = vecAppend (vecRev v) x

vecMoveAppend : {a : _} {X : Set a} {m : ℕ} → (x : X) → (v : Vec X m) → vecRev (vecAppend v x) ≡ x ,- vecRev v
vecMoveAppend {a} {X} {.0} x [] = refl
vecMoveAppend {a} {X} {.(succ _)} x (y ,- v) rewrite vecMoveAppend x v = refl

vecRevRevIsId : {a : _} {X : Set a} {m : ℕ} → (v : Vec X m) → (vecRev (vecRev v)) ≡ v
vecRevRevIsId {a} {X} {zero} [] = refl
vecRevRevIsId {a} {X} {succ m} (x ,- v) rewrite vecMoveAppend x (vecRev v) = applyEquality (λ i → x ,- i) (vecRevRevIsId v)

record vecContains {a : _} {X : Set a} {m : ℕ} (vec : Vec X m) (x : X) : Set a where
  field
    index : ℕ
    index<m : index <N m
    isHere : vecIndex vec index index<m ≡ x

vecSolelyContains : {a : _} {X : Set a} → {m : X} → (n : X) → (vecContains (m ,- []) n) → m ≡ n
vecSolelyContains {m} n record { index = zero ; index<m = _ ; isHere = isHere } = isHere
vecSolelyContains {m} n record { index = (succ index) ; index<m = (le x proof) ; isHere = isHere } = exFalso (f {x} {index} proof)
  where
    f : {x index : ℕ} → succ (x +N succ index) ≡ 1 → False
    f {x} {index} pr rewrite Semiring.commutative ℕSemiring x (succ index) = naughtE (equalityCommutative (succInjective pr))

vecChop : {a : _} {X : Set a} (m : ℕ) {n : ℕ} → Vec X (m +N n) → Vec X m && Vec X n
_&&_.fst (vecChop zero xs) = []
_&&_.fst (vecChop (succ m) (x ,- xs)) = (x ,- _&&_.fst (vecChop m xs))
_&&_.snd (vecChop zero xs) = xs
_&&_.snd (vecChop (succ m) (x ,- xs)) = _&&_.snd (vecChop m xs)

{-
vecIsChopThenAppend : {a : _} {X : Set a} {m n : ℕ} (xs : Vec X m) (ys : Vec X n) → vecChop m (xs +V ys) ≡ record { fst = xs ; snd = ys }
vecIsChopThenAppend {a} {X} {m} xs ys with vecChop m (xs +V ys)
vecIsChopThenAppend {a} {X} {zero} [] ys | record { fst = [] ; snd = snd } = {!!}
vecIsChopThenAppend {a} {X} {succ m} xs ys | bl = {!!}
-}

vecMap : {a b : _} {X : Set a} {Y : Set b} → (X → Y) → {n : ℕ} → Vec X n → Vec Y n
vecMap f [] = []
vecMap f (x ,- vec) = f x ,- (vecMap f vec)

vecMapCommutesWithAppend : {a b : _} {X : Set a} {Y : Set b} → (f : X → Y) → {n : ℕ} → (x : X) → (v : Vec X n) → (vecMap f (vecAppend v x) ≡ vecAppend (vecMap f v) (f x))
vecMapCommutesWithAppend f {.0} x [] = refl
vecMapCommutesWithAppend f {.(succ _)} x (y ,- v) = applyEquality (λ i → (f y ,- i)) (vecMapCommutesWithAppend f x v)

vecMapCommutesWithRev : {a b : _} {X : Set a} {Y : Set b} → (f : X → Y) → {n : ℕ} → (v : Vec X n) → (vecMap f (vecRev v) ≡ vecRev (vecMap f v))
vecMapCommutesWithRev {a} {b} {X} {Y} f {.0} [] = refl
vecMapCommutesWithRev {a} {b} {X} {Y} f {.(succ _)} (x ,- v) rewrite vecMapCommutesWithAppend f x (vecRev v) = applyEquality (λ i → vecAppend i (f x)) (vecMapCommutesWithRev f v)

vecIndex0AndAppend : {a : _} {X : Set a} {n : ℕ} → (v : Vec X n) → (0<n : 0 <N n) → (x : X) → vecIndex (vecAppend v x) 0 (succIsPositive n) ≡ vecIndex v 0 0<n
vecIndex0AndAppend [] () x
vecIndex0AndAppend (a ,- v) 0<n x = refl

vecIndexMAndAppend : {a : _} {X : Set a} {n : ℕ} → (v : Vec X n) → (x : X) → (m : ℕ) → (m<n : m <N n) → (pr : m <N succ n) → vecIndex (vecAppend v x) m pr ≡ vecIndex v m m<n
vecIndexMAndAppend {n = .(succ _)} (v ,- vs) x zero m<n pr = refl
vecIndexMAndAppend [] x (succ m) ()
vecIndexMAndAppend {n = n} (y ,- v) x (succ m) m<n pr = vecIndexMAndAppend v x m (canRemoveSuccFrom<N m<n) (canRemoveSuccFrom<N pr)

vecMapCompose : {a b c : _} {X : Set a} {Y : Set b} {Z : Set c} → (f : X → Y) → (g : Y → Z) → {n : ℕ} → (v : Vec X n) → (vecMap g (vecMap f v)) ≡ vecMap (λ i → g (f i)) v
vecMapCompose f g [] = refl
vecMapCompose f g (x ,- v) = applyEquality (λ w → (g (f x) ,- w)) (vecMapCompose f g v)

vecMapIdFact : {a : _} {X : Set a} {f : X → X} (feq : (x : X) → f x ≡ x) {n : ℕ} (xs : Vec X n) → vecMap f xs ≡ xs
vecMapIdFact feq [] = refl
vecMapIdFact feq (x ,- xs) rewrite (feq x) | vecMapIdFact feq xs = refl

vecMapCompositionFact : {a b c : _} {X : Set a} {Y : Set b} {Z : Set c} {f : Y → Z} {g : X → Y} {h : X → Z} (heq : (x : X) → f (g x) ≡ h x) → {n : ℕ} (xs : Vec X n) → vecMap f (vecMap g xs) ≡ vecMap h xs
vecMapCompositionFact heq [] = refl
vecMapCompositionFact {a} {b} {c} {X} {Y} {Z} {f} {g} {h} heq (x ,- xs) rewrite heq x | vecMapCompositionFact {a} {b} {c} {X} {Y} {Z} {f} {g} {h} heq xs = refl

vecMapIsNatural : {a b : _} {X : Set a} {Y : Set b} (f : X → Y) → {m n : ℕ} (xs : Vec X m) (xs' : Vec X n) → vecMap f (xs +V xs') ≡ (vecMap f xs +V vecMap f xs')
vecMapIsNatural f [] xs' = refl
vecMapIsNatural f (x ,- xs) xs' rewrite vecMapIsNatural f xs xs' = refl

vecMapAndIndex : {n : ℕ} {a b : _} {A : Set a} {B : Set b} (v : Vec A n) (f : A → B) → {a : ℕ} → (a<n : a <N n) → vecIndex (vecMap f v) a a<n ≡ f (vecIndex v a a<n)
vecMapAndIndex (x ,- v) f {zero} a<n = refl
vecMapAndIndex (x ,- v) f {succ a} a<n = vecMapAndIndex v f (canRemoveSuccFrom<N a<n)

vecPure : {a : _} {X : Set a} → X → {n : ℕ} → Vec X n
vecPure x {zero} = []
vecPure x {succ n} = x ,- vecPure x {n}

vecAllTrue : {a b : _} {X : Set a} (f : X → Set b) → {n : ℕ} (v : Vec X n) → Set b
vecAllTrue f [] = True'
vecAllTrue f (x ,- v) = f x && vecAllTrue f v

vecFold : {a b : _} {X : Set a} {S : Set b} (f : X → S → S) (s : S) {n : ℕ} (v : Vec X n) → S
vecFold f s [] = s
vecFold f s (x ,- v) = vecFold f (f x s) v

private
  succLess1 : (i : ℕ) → .(succ i <N 1) → False
  succLess1 zero pr with <NProp pr
  ... | le zero ()
  ... | le (succ x) ()
  succLess1 (succ i) pr with <NProp pr
  ... | le zero ()
  ... | le (succ x) ()

vecDelete : {a : _} {X : Set a} {n : ℕ} (index : ℕ) .(pr : index <N succ n) → Vec X (succ n) → Vec X n
vecDelete zero _ (x ,- v) = v
vecDelete (succ i) p (x ,- []) = exFalso (succLess1 i p)
vecDelete (succ i) pr (x ,- (y ,- v)) = x ,- vecDelete i (canRemoveSuccFrom<N pr) (y ,- v)

_$V_ : {a b : _} {X : Set a} {Y : Set b} {n : ℕ} → Vec (X → Y) n → Vec X n → Vec Y n
[] $V [] = []
(f ,- fs) $V (x ,- xs) = f x ,- (fs $V xs)
infixl 3 _$V_

vec : {a b : _} {X : Set a} {Y : Set b} → (X → Y) → {n : ℕ} → Vec X n → Vec Y n
vec f xs = (vecPure f) $V xs

vecZip : {a b : _} {X : Set a} {Y : Set b} {n : ℕ} → Vec X n → Vec Y n → Vec (X && Y) n
vecZip [] [] = []
vecZip (x ,- xs) (x₁ ,- ys) = record { fst = x ; snd = x₁ } ,- vecZip xs ys

vecIdentity : {a : _} {X : Set a} {f : X → X} (feq : (x : X) → f x ≡ x) → {n : ℕ} (xs : Vec X n) → (vecPure f $V xs) ≡ xs
vecIdentity feq [] = refl
vecIdentity feq (x ,- xs) rewrite feq x | vecIdentity feq xs = refl

vecHom : {a b : _} {X : Set a} {Y : Set b} (f : X → Y) (x : X) → {n : ℕ} → (vecPure f $V vecPure x) ≡ vecPure (f x) {n}
vecHom f x {zero} = refl
vecHom f x {succ n} rewrite vecHom f x {n} = refl

vecInterchange : {a b : _} {X : Set a} {Y : Set b} {n : ℕ} (fs : Vec (X → Y) n) (x : X) → (fs $V vecPure x) ≡ (vecPure (λ f → f x) $V fs)
vecInterchange [] x = refl
vecInterchange (f ,- fs) x rewrite vecInterchange fs x = refl

vecComposition : {a b c : _} {X : Set a} {Y : Set b} {Z : Set c} {n : ℕ} (fs : Vec (Y → Z) n) (gs : Vec (X → Y) n) (xs : Vec X n) → (vecPure (λ i j x → i (j x)) $V fs $V gs $V xs) ≡ (fs $V (gs $V xs))
vecComposition [] [] [] = refl
vecComposition (f ,- fs) (g ,- gs) (x ,- xs) rewrite vecComposition fs gs xs = refl

vecToList : {a : _} {A : Set a} {n : ℕ} → (v : Vec A n) → List A
vecToList [] = []
vecToList (x ,- v) = x :: vecToList v

listToVec : {a : _} {A : Set a} (l : List A) → Vec A (length l)
listToVec [] = []
listToVec (x :: l) = x ,- listToVec l

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

data _<=_ : ℕ → ℕ → Set where
  oz : zero <= zero
  os : {n m : ℕ} → n <= m → succ n <= succ m
  o' : {n m : ℕ} → n <= m → n <= succ m

all0<=4 : Vec (0 <= 4) 1
all0<=4 = o' (o' (o' (o' oz))) ,- []

all1<=4 : Vec (1 <= 4) 4
all1<=4 = (o' ((o' (o' (os oz))))) ,- ((o' (o' (os (o' oz)))) ,- ((o' (os (o' (o' oz)))) ,- ((os (o' (o' (o' oz)))) ,- [])))

all2<=4 : Vec (2 <= 4) 6
all2<=4 = os (os (o' (o' oz))) ,- (os (o' (os (o' oz))) ,- (os (o' (o' (os oz))) ,- (o' (o' (os (os oz))) ,- (o' (os (o' (os oz))) ,- (o' (os (os (o' oz))) ,- [])))))

all3<=4 : Vec (3 <= 4) 4
all3<=4 = os (os (os (o' oz))) ,- (os (os (o' (os oz))) ,- (os (o' (os (os oz))) ,- (o' (os (os (os oz))) ,- [])))

all4<=4 : Vec (4 <= 4) 1
all4<=4 = os (os (os (os oz))) ,- []

<=Is≤N : {n m : ℕ} → (n <= m) → n ≤N m
<=Is≤N {n} {m} thm with TotalOrder.totality ℕTotalOrder n m
<=Is≤N {n} {m} thm | inl (inl n<m) = inl n<m
<=Is≤N {n} {.n} thm | inr refl = inr refl
<=Is≤N {zero} {zero} thm | inl (inr m<n) = inl m<n
<=Is≤N {zero} {succ m} thm | inl (inr m<n) = inl (succIsPositive m)
<=Is≤N {succ n} {zero} () | inl (inr m<n)
<=Is≤N {succ n} {succ m} (os thm) | inl (inr m<n) with <=Is≤N thm
<=Is≤N {succ n} {succ m} (os thm) | inl (inr m<n) | inl x = inl (succPreservesInequality x)
<=Is≤N {succ n} {succ m} (os thm) | inl (inr m<n) | inr x rewrite x = inr refl
<=Is≤N {succ n} {succ m} (o' thm) | inl (inr m<n) with <=Is≤N thm
<=Is≤N {succ n} {succ m} (o' thm) | inl (inr m<n) | inl x with a<SuccA m
... | m<sm = inl (lessTransitive x m<sm)
<=Is≤N {succ n} {succ m} (o' thm) | inl (inr m<n) | inr x rewrite x = inl (a<SuccA m)

succIsNotEqual : {n : ℕ} → (succ n ≡ n) → False
succIsNotEqual {zero} pr = naughtE (equalityCommutative pr)
succIsNotEqual {succ n} pr = succIsNotEqual (succInjective pr)

succIsNotLess : {n : ℕ} → (succ n <N n) → False
succIsNotLess {zero} (le x proof) = naughtE (equalityCommutative proof)
succIsNotLess {succ n} pr = succIsNotLess (canRemoveSuccFrom<N pr)

noSN<=N : {n : ℕ} → (succ n) <= n → False
noSN<=N {n} thm with <=Is≤N thm
noSN<=N {n} thm | inl x = succIsNotLess x
noSN<=N {n} thm | inr x = succIsNotEqual x

no5<=4 : 5 <= 4 → False
no5<=4 th = noSN<=N {4} th

_<?=_ : {a : _} {X : Set a} {n m : ℕ} → (n <= m) → Vec X m → Vec X n
oz <?= xs = xs
os th <?= (x ,- xs) = x ,- (th <?= xs)
o' th <?= (x ,- xs) = th <?= xs

vMap<?=Fact : {a b : _} {X : Set a} {Y : Set b} (f : X → Y) {n m : ℕ} (th : n <= m) (xs : Vec X m) → vecMap f (th <?= xs) ≡ (th <?= vecMap f xs)
vMap<?=Fact f oz xs = refl
vMap<?=Fact f (os th) (x ,- xs) rewrite vMap<?=Fact f th xs = refl
vMap<?=Fact f (o' th) (x ,- xs) rewrite vMap<?=Fact f th xs = refl

oi : {n : ℕ} → n <= n
oi {zero} = oz
oi {succ n} = os oi

oe : {n : ℕ} → 0 <= n
oe {zero} = oz
oe {succ n} = o' oe

oeUnique : {n : ℕ} (th : 0 <= n) → th ≡ oe
oeUnique oz = refl
oeUnique (o' i) rewrite oeUnique i = refl

oTooBig : {n m : ℕ} → m ≤N n → succ n <= m → False
oTooBig {n} {m} m<=n th with <=Is≤N th
oTooBig {n} {m} (inl m<n) th | inl x = succIsNotLess (lessTransitive x m<n)
oTooBig {n} {m} (inr m=n) th | inl x rewrite m=n = succIsNotLess x
oTooBig {n} {m} (inl m<n) th | inr x rewrite (equalityCommutative x) = succIsNotLess m<n
oTooBig {n} {m} (inr m=n) th | inr x rewrite m=n = succIsNotEqual x

oiUnique : {n : ℕ} (th : n <= n) → (th ≡ oi)
oiUnique oz = refl
oiUnique (os th) rewrite oiUnique th = refl
oiUnique {succ n} (o' th) with oTooBig {n} {n} (inr refl) th
... | bl = exFalso bl

id-<?= : {a : _} {X : Set a} {n : ℕ} (xs : Vec X n) → (oi <?= xs) ≡ xs
id-<?= [] = refl
id-<?= (x ,- xs) rewrite id-<?= xs = refl

_o>>_ : {p n m : ℕ} → p <= n → n <= m → p <= m
oz o>> th' = th'
os th o>> os th' = os (th o>> th')
os th o>> o' th' = os (o' th o>> th')
o' th o>> os th' = o' (th o>> th')
o' th o>> o' th' = o' (o' th o>> th')

eqHelper : {a : _} {X : Set a} (x : X) {n : ℕ} {r s : Vec X n} (pr : r ≡ s) → (x ,- r) ≡ (x ,- s)
eqHelper x pr rewrite pr = refl


text:
module Printf where
import AlonzoPrelude
import PreludeList
import PreludeShow
import PreludeString
import PreludeNat

open AlonzoPrelude
open PreludeList hiding (_++_)
open PreludeShow
open PreludeString
open PreludeNat

data Unit : Set where
  unit : Unit

data Format : Set where
  stringArg : Format
  natArg    : Format
  intArg    : Format
  floatArg  : Format
  charArg   : Format
  litChar   : Char -> Format
  badFormat : Char -> Format

data BadFormat (c : Char) : Set where

format : String -> List Format
format s = format' (toList s)
  where
    format' : List Char -> List Format
    format' ('%' :: 's' :: fmt) = stringArg   :: format' fmt
    format' ('%' :: 'n' :: fmt) = natArg      :: format' fmt
    format' ('%' :: 'd' :: fmt) = intArg      :: format' fmt
    format' ('%' :: 'f' :: fmt) = floatArg    :: format' fmt
    format' ('%' :: 'c' :: fmt) = charArg     :: format' fmt
    format' ('%' :: '%' :: fmt) = litChar '%' :: format' fmt
    format' ('%' ::  c  :: fmt) = badFormat c :: format' fmt
    format' (c		:: fmt) = litChar c   :: format' fmt
    format'  []		= []

Printf' : List Format -> Set
Printf' (stringArg   :: fmt) = String  × Printf' fmt
Printf' (natArg      :: fmt) = Nat     × Printf' fmt
Printf' (intArg      :: fmt) = Int     × Printf' fmt
Printf' (floatArg    :: fmt) = Float   × Printf' fmt
Printf' (charArg     :: fmt) = Char    × Printf' fmt
Printf' (badFormat c :: fmt) = BadFormat c
Printf' (litChar _   :: fmt) = Printf' fmt
Printf'  []		     = Unit

Printf : String -> Set
Printf fmt = Printf' (format fmt)

{-
printf' : (fmt : List Format) -> Printf' fmt -> String
printf' (stringArg   :: fmt) < s , args > = s			 ++ printf' fmt args
printf' (natArg      :: fmt) < n , args > = showNat n		 ++ printf' fmt args
printf' (intArg      :: fmt) < n , args > = showInt n		 ++ printf' fmt args
printf' (floatArg    :: fmt) < x , args > = showFloat x	 ++ printf' fmt args
printf' (charArg     :: fmt) < c , args > = showChar c	 ++ printf' fmt args
printf' (litChar c   :: fmt) args = fromList (c :: []) ++ printf' fmt args
printf' (badFormat _ :: fmt) ()
printf'  []		 unit = ""
-}
printf : (fmt : String) -> Printf fmt -> String
printf fmt = printf' (format fmt)
  where
    printf' : (fmt : List Format) -> Printf' fmt -> String
    printf' (stringArg   :: fmt) < s , args > = s			 ++ printf' fmt args
    printf' (natArg      :: fmt) < n , args > = showNat n		 ++ printf' fmt args
    printf' (intArg      :: fmt) < n , args > = showInt n		 ++ printf' fmt args
    printf' (floatArg    :: fmt) < x , args > = showFloat x	 ++ printf' fmt args
    printf' (charArg     :: fmt) < c , args > = showChar c	 ++ printf' fmt args
    printf' (litChar c   :: fmt) args	    = fromList (c :: []) ++ printf' fmt args
    printf' (badFormat _ :: fmt) ()
    printf'  []		 unit 	    = ""

mainS : String
-- mainS = printf  "pi = %f"  < 3.14 , unit >
mainS = printf "Answer is %n, pi = %f %% %s"
	< 42 , < 3.14159 , < "Alonzo" , unit > > >

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Unary.Any.Properties directly.
------------------------------------------------------------------------

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

module Data.List.Any.Properties where

open import Data.List.Relation.Unary.Any.Properties public


text:
open import Function using (case_of_; _∘_)
open import Data.List using (List; _++_; map) renaming (_∷_ to _,_; _∷ʳ_ to _,′_; [] to ∅)
open import Data.List.Properties using (map-++-commute)
open import Data.Product using () renaming (_×_ to _x'_)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; sym; cong)

module LinearLogic (U : Set) (R : U) (⟦_⟧ᵁ : U → Set) where

infixr 40 ¬_
infix  30 _⊗_
infixr 20 _⊸_
infix  4  _⊢_

data Type : Set where
  el   : (A : U) → Type
  ⊥    : Type
  _⊗_  : Type → Type → Type
  _⊸_  : Type → Type → Type

data _⊢_ : ∀ (X : List Type) (A : Type) → Set where
  var   : ∀ {A} → A , ∅ ⊢ A
  abs   : ∀ {X A B} → A , X ⊢ B → X ⊢ A ⊸ B
  app   : ∀ {X Y A B} → X ⊢ A ⊸ B → Y ⊢ A → X ++ Y ⊢ B
  pair  : ∀ {X Y A B} → X ⊢ A → Y ⊢ B → X ++ Y ⊢ A ⊗ B
  case  : ∀ {X Y A B C } → X ⊢ A ⊗ B → A , B , Y ⊢ C → X ++ Y ⊢ C
  exch  : ∀ {X Y Z W A} →  (X ++ Z) ++ (Y ++ W) ⊢ A
        →  (X ++ Y) ++ (Z ++ W) ⊢ A

¬_ : Type → Type
¬ A = A ⊸ ⊥

exch₀ : ∀ {A B C X} → A , B , X ⊢ C → B , A , X ⊢ C
exch₀ {A} {B} {X = X} t = exch {∅} {B , ∅} {A , ∅} {X} t

swap : ∀ {A B} → ∅ ⊢ A ⊗ B ⊸ B ⊗ A
swap {A} {B} = abs (case var (exch₀ (pair var var)))

raise : ∀ {A B X} → X ⊢ A → X ⊢ (A ⊸ B) ⊸ B
raise t = abs (app var t)

++-assoc : ∀ {a} {A : Set a} (X Y Z : List A) → X ++ (Y ++ Z) ≡ (X ++ Y) ++ Z
++-assoc ∅ Y Z = refl
++-assoc (x , X) Y Z = cong (_,_ x) (++-assoc X Y Z)

xs++[]=xs : ∀ {a} {A : Set a} (xs : List A) → xs ++ ∅ ≡ xs
xs++[]=xs ∅ = refl
xs++[]=xs (x , xs) = cong (_,_ x) (xs++[]=xs xs)

to-front : ∀ {X A B} → A , X ⊢ B → X ,′ A ⊢ B
to-front {X} {A} {B} t = lem1 lem2
  where
    lem1 : A , (X ++ ∅) ⊢ B → X ,′ A ⊢ B
    lem1 = exch {∅} {X} {A , ∅} {∅}
    lem2 : A , (X ++ ∅) ⊢ B
    lem2 rewrite xs++[]=xs X = t

to-back : ∀ {X A B} → X ,′ A ⊢ B → A , X ⊢ B
to-back {X} {A} {B} t = lem2
  where
    lem1 : A , X ++ ∅ ⊢ B
    lem1 = exch {∅} {A , ∅} {X} {∅} t
    lem2 : A , X ⊢ B
    lem2 rewrite sym (xs++[]=xs (A , X)) = lem1

YX↝XY : ∀ {A} X Y → Y ++ X ⊢ A → X ++ Y ⊢ A
YX↝XY {A} X Y t = lem₃
  where
    lem₁ : Y ++ X ++ ∅ ⊢ A
    lem₁ rewrite xs++[]=xs X = t
    lem₂ : X ++ Y ++ ∅ ⊢ A
    lem₂ = exch {∅} {X} {Y} {∅} lem₁
    lem₃ : X ++ Y ⊢ A
    lem₃ = PropEq.subst (λ Y → X ++ Y ⊢ A) (xs++[]=xs Y) lem₂

Y[XZ]↝X[YZ] : ∀ {A} X Y Z → Y ++ (X ++ Z) ⊢ A → X ++ (Y ++ Z) ⊢ A
Y[XZ]↝X[YZ] {A} X Y Z t = exch {∅} {X} {Y} {Z} t

[YX]Z↝[XY]Z : ∀ {A} X Y Z → (Y ++ X) ++ Z ⊢ A → (X ++ Y) ++ Z ⊢ A
[YX]Z↝[XY]Z {A} X Y Z t = lem₃
  where
    lem₁ : Y ++ (X ++ Z) ⊢ A
    lem₁ rewrite ++-assoc Y X Z = t
    lem₂ : X ++ (Y ++ Z) ⊢ A
    lem₂ = Y[XZ]↝X[YZ] X Y Z lem₁
    lem₃ : (X ++ Y) ++ Z ⊢ A
    lem₃ rewrite sym (++-assoc X Y Z) = lem₂

[XZ]Y↝[XY]Z : ∀ {A} X Y Z → (X ++ Z) ++ Y ⊢ A → (X ++ Y) ++ Z ⊢ A
[XZ]Y↝[XY]Z {A} X Y Z t = lem₃
  where
    lem₁ : (X ++ Z) ++ Y ++ ∅ ⊢ A
    lem₁ rewrite xs++[]=xs Y = t
    lem₂ : (X ++ Y) ++ Z ++ ∅ ⊢ A
    lem₂ = exch {X} {Y} {Z} {∅} lem₁
    lem₃ : (X ++ Y) ++ Z ⊢ A
    lem₃ = PropEq.subst (λ Z → (X ++ Y) ++ Z ⊢ A) (xs++[]=xs Z) lem₂

X[ZY]↝X[YZ] : ∀ {A} X Y Z → X ++ (Z ++ Y) ⊢ A → X ++ (Y ++ Z) ⊢ A
X[ZY]↝X[YZ] {A} X Y Z t = lem₃
  where
    lem₁ : (X ++ Z) ++ Y ⊢ A
    lem₁ rewrite sym (++-assoc X Z Y) = t
    lem₂ : (X ++ Y) ++ Z ⊢ A
    lem₂ = [XZ]Y↝[XY]Z X Y Z lem₁
    lem₃ : X ++ Y ++ Z ⊢ A
    lem₃ rewrite ++-assoc X Y Z = lem₂

XYZW↝XWZY : ∀ {A} X Y Z W → (X ++ Y) ++ (Z ++ W) ⊢ A → (X ++ W) ++ (Z ++ Y) ⊢ A
XYZW↝XWZY {A} X Y Z W t = lem₃
  where
    lem₁ : (X ++ Y) ++ (W ++ Z) ⊢ A
    lem₁ = X[ZY]↝X[YZ] (X ++ Y) W Z t
    lem₂ : (X ++ W) ++ (Y ++ Z) ⊢ A
    lem₂ = exch {X} {W} {Y} {Z} lem₁
    lem₃ : (X ++ W) ++ (Z ++ Y) ⊢ A
    lem₃ = X[ZY]↝X[YZ] (X ++ W) Z Y lem₂

XYZW↝YWXZ : ∀ {A} X Y Z W → (X ++ Y) ++ (Z ++ W) ⊢ A → (Y ++ W) ++ (X ++ Z) ⊢ A
XYZW↝YWXZ {A} X Y Z W t = lem₃
  where
    lem₁ : (Y ++ X) ++ (Z ++ W) ⊢ A
    lem₁ = [YX]Z↝[XY]Z Y X (Z ++ W) t
    lem₂ : (Y ++ X) ++ (W ++ Z) ⊢ A
    lem₂ = X[ZY]↝X[YZ] (Y ++ X) W Z lem₁
    lem₃ : (Y ++ W) ++ (X ++ Z) ⊢ A
    lem₃ = exch {Y} {W} {X} {Z} lem₂

XYZW↝ZXWY : ∀ {A} X Y Z W → (X ++ Y) ++ (Z ++ W) ⊢ A → (Z ++ X) ++ (W ++ Y) ⊢ A
XYZW↝ZXWY {A} X Y Z W t = lem₃
  where
    lem₁ : (X ++ Z) ++ (Y ++ W) ⊢ A
    lem₁ = exch {X} {Z} {Y} {W} t
    lem₂ : (Z ++ X) ++ (Y ++ W) ⊢ A
    lem₂ = [YX]Z↝[XY]Z Z X (Y ++ W) lem₁
    lem₃ : (Z ++ X) ++ (W ++ Y) ⊢ A
    lem₃ = X[ZY]↝X[YZ] (Z ++ X) W Y lem₂

XYZW↝ZYXW : ∀ {A} X Y Z W → (X ++ Y) ++ (Z ++ W) ⊢ A → (Z ++ Y) ++ (X ++ W) ⊢ A
XYZW↝ZYXW {A} X Y Z W t = lem₃
  where
    lem₁ : (Y ++ X) ++ (Z ++ W) ⊢ A
    lem₁ = [YX]Z↝[XY]Z Y X (Z ++ W) t
    lem₂ : (Y ++ Z) ++ (X ++ W) ⊢ A
    lem₂ = exch {Y} {Z} {X} {W} lem₁
    lem₃ : (Z ++ Y) ++ (X ++ W) ⊢ A
    lem₃ = [YX]Z↝[XY]Z Z Y (X ++ W) lem₂

pair-left : ∀ {X A B C} → A , B , X ⊢ C → A ⊗ B , X ⊢ C
pair-left t = case var t

pair-left′ : ∀ {X A B C} → X ++ (A , B , ∅) ⊢ C → X ,′ A ⊗ B ⊢ C
pair-left′ {X} {A} {B} {C} = lem₃
  where
    lem₁ : X ,′ A ,′ B ⊢ C → X ,′ A ⊗ B ⊢ C
    lem₁ t = to-front (pair-left (to-back {B , X} {A} (to-back {X ,′ A} {B} t)))
    lem₂ : ∀ {a} {A : Set a} xs (y z : A) → xs ,′ y ,′ z  ≡ xs ++ (y , z , ∅)
    lem₂ ∅ y z = refl
    lem₂ (x , xs) y z = cong (_,_ x) (lem₂ xs y z)
    lem₃ : X ++ (A , B , ∅) ⊢ C → X ,′ A ⊗ B ⊢ C
    lem₃ rewrite sym (lem₂ X A B) = lem₁

open import IntuitionisticLogic U ⟦_⟧ᵁ as IL renaming (Type to TypeIL; _⊗_ to _×_)
open IL.Explicit
  hiding (swap; swap′)
  renaming (_⊢_ to _⊢IL_; ReifyType to ReifyTypeIL; ReifyCtxt to ReiftCtxtIL; [_] to reifyIL)

instance
  ReifyType : Reify Type TypeIL
  ReifyType = record { ⟦_⟧ = ⟦_⟧ }
    where

      ⟦_⟧ : Type → TypeIL
      ⟦ ⊥      ⟧ = el R
      ⟦ el A   ⟧ = el A
      ⟦ A ⊗ B  ⟧ = ⟦ A ⟧ × ⟦ B ⟧
      ⟦ A ⊸ B  ⟧ = ⟦ A ⟧ ⇒ ⟦ B ⟧

open Reify {{...}} using (⟦_⟧)

instance
  ReifyCtxt : Reify (List Type) (List TypeIL)
  ReifyCtxt = record { ⟦_⟧ = map ⟦_⟧ }

⟦X++Y⟧=⟦X⟧++⟦Y⟧ : (X Y : List Type) → ⟦ X ++ Y ⟧ ≡ ⟦ X ⟧ ++ ⟦ Y ⟧
⟦X++Y⟧=⟦X⟧++⟦Y⟧ X Y = map-++-commute ⟦_⟧ X Y

toIL : ∀ {X A} → X ⊢ A → ⟦ X ⟧ ⊢IL ⟦ A ⟧
toIL var       = var
toIL (abs t)   = abs (toIL t)
toIL (app {X} {Y} s t)   rewrite ⟦X++Y⟧=⟦X⟧++⟦Y⟧ X Y  = app (toIL s) (toIL t)
toIL (pair {X} {Y} s t)  rewrite ⟦X++Y⟧=⟦X⟧++⟦Y⟧ X Y  = pair (toIL s) (toIL t)
toIL (case {X} {Y} s t)  rewrite ⟦X++Y⟧=⟦X⟧++⟦Y⟧ X Y  = case (toIL s) (toIL t)
toIL (exch {X} {Y} {Z} {W} {A} t)  = lem4
  where
    lem1 : ⟦ (X ++ Z) ++ (Y ++ W) ⟧ ⊢IL ⟦ A ⟧
    lem1 = toIL t
    lem2 : (⟦ X ⟧ ++ ⟦ Z ⟧) ++ (⟦ Y ⟧ ++ ⟦ W ⟧) ⊢IL ⟦ A ⟧
    lem2 rewrite  sym (⟦X++Y⟧=⟦X⟧++⟦Y⟧ X Z)
               |  sym (⟦X++Y⟧=⟦X⟧++⟦Y⟧ Y W)
               |  sym (⟦X++Y⟧=⟦X⟧++⟦Y⟧ (X ++ Z) (Y ++ W)) = lem1
    lem3 : (⟦ X ⟧ ++ ⟦ Y ⟧) ++ (⟦ Z ⟧ ++ ⟦ W ⟧) ⊢IL ⟦ A ⟧
    lem3 = exch {⟦ X ⟧} {⟦ Y ⟧} {⟦ Z ⟧} {⟦ W ⟧} lem2
    lem4 : ⟦ (X ++ Y) ++ (Z ++ W) ⟧ ⊢IL ⟦ A ⟧
    lem4 rewrite  ⟦X++Y⟧=⟦X⟧++⟦Y⟧ (X ++ Y) (Z ++ W)
               |  ⟦X++Y⟧=⟦X⟧++⟦Y⟧ X Y
               |  ⟦X++Y⟧=⟦X⟧++⟦Y⟧ Z W = lem3

[_] : {A : Type} {X : List Type} → X ⊢ A → (Ctxt ⟦ ⟦ X ⟧ ⟧ → ⟦ ⟦ A ⟧ ⟧)
[_] = reifyIL ∘ toIL

swap′ : {A B : Type} → ⟦ ⟦ A ⟧ ⟧ x' ⟦ ⟦ B ⟧ ⟧ → ⟦ ⟦ B ⟧ ⟧ x' ⟦ ⟦ A ⟧ ⟧
swap′ {A} {B} = [ swap {A} {B} ] ∅


text:
module Issue564 where

postulate
  Level : Set
  zero  : Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}

postulate
  A : Level → Set

module M ℓ where
  postulate a : A ℓ

postulate
  P : A zero → Set

open M zero

p : P a
p = {!!}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

-- This module primarily deals with expressions for pretty-printing,
-- for the step-by-step output from the solver.

open import Algebra
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.String using (String)
open import EqBool
open import Data.Bool

module Polynomial.Expr.Normalising
  {c ℓ}
  (ring : RawRing c ℓ)
  (show : RawRing.Carrier ring → String)
  ⦃ _ : HasEqBool (RawRing.Carrier ring) ⦄
  where

open RawRing ring

-- An expressions which contains some free variables.
infixl 6 _⊕_
infixl 7 _⊗_
data Open : Set c where
  V : String → Open
  K : Carrier → Open
  _⊕_ : Open → Open → Open
  _⊗_ : Open → Open → Open
  ⊝_ : Open → Open

_==O_ : Open → Open → Bool
_==O_ (V v) (V y) = v == y
_==O_ (K k) (K y) = k == y
_==O_ (x₁ ⊕ y₁) (x₂ ⊕ y₂) = x₁ ==O x₂ ∧ y₁ ==O y₂
_==O_ (x₁ ⊗ y₁) (x₂ ⊗ y₂) = x₁ ==O x₂ ∧ y₁ ==O y₂
_==O_ (⊝ x) (⊝ y) = x ==O y
_==O_ _ _ = false

instance
  eqOpen : HasEqBool Open
  _==_ ⦃ eqOpen ⦄ = _==O_

-- An expression which might not have any free variables
data Expr : Set c where
  C : Carrier → Expr
  O : Open → Expr

instance
  eqExpr : HasEqBool Expr
  _==_ ⦃ eqExpr ⦄ (C x₁) (C x₂) = x₁ == x₂
  _==_ ⦃ eqExpr ⦄ (C x₁) (O x₂) = false
  _==_ ⦃ eqExpr ⦄ (O x₁) (C x₂) = false
  _==_ ⦃ eqExpr ⦄ (O x₁) (O x₂) = x₁ == x₂

normalise : Expr → Expr
normalise (C x) = C x
normalise (O x) = go x
  where
  go : Open → Expr
  go (V v) = O (V v)
  go (K k) = C k
  go (x ⊕ y) with go x | go y
  go (x ⊕ y) | C x₁ | C x₂ = C (x₁ + x₂)
  go (x ⊕ y) | C x₁ | O x₂ = if x₁ == 0# then O x₂ else O (K x₁ ⊕ x₂)
  go (x ⊕ y) | O x₁ | C x₂ = if x₂ == 0# then O x₁ else O (x₁ ⊕ K x₂)
  go (x ⊕ y) | O x₁ | O x₂ = O (x₁ ⊕ x₂)
  go (x ⊗ y) with go x | go y
  go (x ⊗ y) | C x₁ | C x₂ = C (x₁ * x₂)
  go (x ⊗ y) | C x₁ | O x₂ = if x₁ == 0# then C 0# else if x₁ == 1# then O x₂ else O (K x₁ ⊗ x₂)
  go (x ⊗ y) | O x₁ | C x₂ = if x₂ == 0# then C 0# else if x₂ == 1# then O x₁ else O (x₁ ⊗ K x₂)
  go (x ⊗ y) | O x₁ | O x₂ = O (x₁ ⊗ x₂)
  go (⊝ x) with go x
  go (⊝ x) | C x₁ = C (- x₁)
  go (⊝ x) | O x₁ = O (⊝ x₁)

open import Data.List.Kleene
open import Data.Product
open import Data.Nat

data Flat : Set c where
  sum : Flat + → Flat
  prd : (Flat × ℕ) + → Flat
  neg : Flat → Flat
  V′ : String → Flat
  K′ : Carrier → Flat

mutual
  _==F*_ : Flat * → Flat * → Bool
  [] ==F* [] = true
  [] ==F* (∹ x₁) = false
  (∹ x₁) ==F* [] = false
  (∹ x & xs) ==F* (∹ y & ys) = x ==F y ∧ xs ==F* ys

  _==F×*_ : (Flat × ℕ) * → (Flat × ℕ) * → Bool
  [] ==F×* [] = true
  [] ==F×* (∹ x₁) = false
  (∹ x₁) ==F×* [] = false
  (∹ (x , i) & xs) ==F×* (∹ (y , j) & ys) = i == j ∧ x ==F y ∧ xs ==F×* ys

  _==F_ : Flat → Flat → Bool
  _==F_ (sum (x & xs)) (sum (y & ys)) = x ==F y ∧ xs ==F* ys
  _==F_ (prd ((x , i) & xs)) (prd ((y , j) & ys)) = i == j ∧ x ==F y ∧ xs ==F×* ys
  _==F_ (neg xs) (neg ys) = xs ==F ys
  _==F_ (V′ x)   (V′ y)   = x == y
  _==F_ (K′ x)   (K′ y)   = x == y
  _==F_ _ _ = false

instance
  eqFlat : HasEqBool Flat
  _==_ ⦃ eqFlat ⦄ = _==F_

prodCons : Flat → (Flat × ℕ) * → (Flat × ℕ) +
prodCons x [] = (x , 0) & []
prodCons x (∹ (y , n) & xs ) with x == y
prodCons x xs@((∹ (y , n) & ys )) | false = (x , 0) & xs
prodCons x (∹ (y , n) & xs ) | true = (y , suc n) & xs

flatten : Open → Flat
flatten (V x) = V′ x
flatten (K x) = K′ x
flatten (x ⊕ y) = sum (x ⊕* (∹ y ⊕* [] ))
  where
  _⊕*_ : Open → Flat * → Flat +
  (x ⊕ y) ⊕* xs = x ⊕* (∹ y ⊕* xs )
  x ⊕* xs = flatten x & xs
flatten (x ⊗ y) = prd (x ⊗* (∹ y ⊗* [] ))
  where
  _⊗*_ : Open → (Flat × ℕ) * → (Flat × ℕ) +
  (x ⊗ y) ⊗* xs = x ⊗* (∹ y ⊗* xs )
  x ⊗* xs = prodCons (flatten x) xs
flatten (⊝ x) = neg (flatten x)

⟨_⟩ₑ : Expr → String
⟨ C x ⟩ₑ = show x
⟨ O x ⟩ₑ = Data.String.fromList (go add (flatten x) List.[])
  where
  import Data.String
  open import Data.Char using (Char)
  open import Data.List.Kleene
  open import Data.List as List using (List; _∷_)
  import Data.Nat.Show

  data PrecLevel : Set where
    mul add neg′ : PrecLevel

  go : PrecLevel → Flat → List Char → List Char

  gop : (Flat × ℕ) → List Char → List Char
  gop (x , zero) = go mul x
  gop (x , suc i) xs = go neg′ x (' ' ∷ '^' ∷ ' ' ∷ Data.String.toList (Data.Nat.Show.show (suc (suc i))) List.++ (' ' ∷ xs))

  f-+ : List Char → Flat * → List Char
  f-+ xs (∹ x & zs ) = ' ' ∷ '+' ∷ ' ' ∷ go add x (f-+ xs zs)
  f-+ xs [] = xs

  f-× : List Char → (Flat × ℕ) * → List Char
  f-× xs (∹ x & zs ) = ' ' ∷ '*' ∷ ' ' ∷ gop x (f-× xs zs)
  f-× xs [] = xs

  go _ (V′ x) xs = Data.String.toList x List.++ xs
  go _ (K′ x) xs = Data.String.toList (show x) List.++ xs
  go neg′ (neg x) xs = '(' ∷ '-' ∷ ' ' ∷ go neg′ x (')' ∷ xs)
  go _   (neg x) xs = '-' ∷ ' ' ∷ go neg′ x xs
  go add (sum (z & zs)) xs = go add z (f-+ xs zs)
  go _   (sum (z & zs)) xs = '(' ∷ go add z (f-+ (')' ∷ xs) zs)
  go neg′ (prd (z & zs)) xs = '(' ∷ gop z (f-× (')' ∷ xs) zs)
  go _    (prd (z & zs)) xs = gop z (f-× xs zs)

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
module Data.Lens.Lens where

open import Haskell.Prelude

{-# FOREIGN AGDA2HS
{-# LANGUAGE Rank2Types #-}
#-}

---- Functors

-- The const functor, for which fmap does not change its value

data Const (a : Set) (b : Set) : Set where
  CConst : a -> Const a b

getConst : {a : Set} {b : Set} -> Const a b -> a
getConst (CConst a) = a

instance
  constFunctor : {a : Set} -> Functor (Const a)
  constFunctor .fmap f (CConst v) = CConst v

{-# COMPILE AGDA2HS Const #-}
{-# COMPILE AGDA2HS getConst #-}
{-# COMPILE AGDA2HS constFunctor #-}

-- The identity functor, which just wraps the object

data Identity (a : Set) : Set where
  CIdentity : a -> Identity a

runIdentity : {a : Set} -> Identity a -> a
runIdentity (CIdentity a) = a

instance
  identityFunctor : Functor Identity
  identityFunctor .fmap f (CIdentity v) = CIdentity (f v)

{-# COMPILE AGDA2HS Identity #-}
{-# COMPILE AGDA2HS runIdentity #-}
{-# COMPILE AGDA2HS identityFunctor #-}

---- Lens
-- van Laarhoven style implementation

Lens : Set -> Set -> Set₁
Lens s a = {f : Set -> Set} -> {{ff : Functor f}} -> (a -> f a) -> s -> f s
{-# FOREIGN AGDA2HS type Lens s a = forall f. Functor f => (a -> f a) -> s -> f s #-}

view : {a b : Set} -> Lens a b -> a -> b
view lens v = getConst $ lens CConst v
{-# COMPILE AGDA2HS view #-}

set : {a b : Set} -> Lens a b -> b -> a -> a
set lens to v = runIdentity $ lens (λ _ -> CIdentity to) v
{-# COMPILE AGDA2HS set #-}

over : {a b : Set} -> Lens a b -> (b -> b) -> a -> a
over lens f v = runIdentity $ lens (CIdentity ∘ f) v
{-# COMPILE AGDA2HS over #-}

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
module Postulate where

postulate

  f
    : {A : Set}
    → A
    → A

  g
    : {A : Set}
    → A
    → A

h
  : {A : Set}
  → A
  → A
h x
  = f x

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


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

module Light.Variable.Other {ℓ} (𝕒 : Set ℓ) where

variable a b c d e f g h i j k l m : 𝕒
variable n o p q r s t u v w x y z : 𝕒

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
open import slots.imports
open import slots.defs

module slots.packed {cfg : config}(g : game cfg) where

open config cfg
open game g

LineCombinations = Vec ℕ n
ReelCombinations = Vec LineCombinations m

PackedLine = Fruit × ReelNo
PackedReel = Vec ℕ m
PackedReels = Vec PackedReel n

packReel : Reel → PackedReel
packReel = L.foldl (λ r f → V.zipWith _+_ r (z V.[ f ]≔ 1)) z where
  z = V.replicate 0

packReels : Reels → PackedReels
packReels = V.map packReel

packedLength : PackedReel → ℕ
packedLength = V.foldl _ _+_ 0

packedTotal : PackedReels → ℕ
packedTotal = V.foldl _ (λ i r → i * packedLength r) 1

packedLineWin : PackedLine → WinTable → ℕ
packedLineWin (f , r) = V.lookup r ∘ V.lookup f

rproducts : ∀ {n} → Vec ℕ n → Vec ℕ n
rproducts = V.foldr (Vec ℕ) (λ k ks → k ∷ V.map (k N.*_) ks) []
lproducts : ∀ {n} → Vec ℕ n → Vec ℕ n
lproducts = V.foldl (Vec ℕ) (λ ks k → k ∷ V.map (k N.*_) ks) []

fruitLineCombinations : PackedReels → Fruit → LineCombinations
fruitLineCombinations rs f = {!!} where
  g′ : PackedReel → ℕ × ℕ
  g′ r = #f , #f̅ where
    #f : ℕ
    #f = V.lookup f r
    #f̅ : ℕ
    #f̅ = V.sum r N.∸ #f
  fs,f̅s = V.unzip (V.map g′ rs)
  fs : Vec ℕ n
  fs = rproducts (proj₁ fs,f̅s)
  -- ts = lproducts
  f̅s : Vec ℕ n
  f̅s = proj₂ fs,f̅s
  -- f₀ f₁ f₂ f₃
  -- f̅₀ f̅₁ f̅₂ f̅₃
  -- t₀ t₁ t₂ t₃
  -- f₀ f̅₁ t₂ t₃ | 1
  -- f₀ f₁ f̅₂ t₃ | 2
  -- f₀ f₁ f₂ f̅₃ | 3
  -- f₀ f₁ f₂ f₃ | 4

fruitReelCombinations : PackedReels → ReelCombinations
fruitReelCombinations rs = V.tabulate (fruitLineCombinations rs)

sum2 : ∀ {n}{A : Set}{B : Set} → (A → B → ℕ) → Vec A n → Vec B n → ℕ
sum2 f as bs = V.sum (V.zipWith f as bs)

rtp : WinTable → ReelCombinations → ℕ
rtp = sum2 (sum2 _*_)

max_stars_repo_name: semenov-vladyslav/slots-agda

max_issues_repo_name: semenov-vladyslav/slots-agda

max_forks_repo_name: semenov-vladyslav/slots-agda


text:
module plfa.part1.Equality where

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

infix 4 _≡_

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

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

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

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B} → u ≡ x → v ≡ y → f u v ≡ f x y
cong₂ f refl refl = refl

cong-app : ∀ {A B : Set} {f g : A → B} → f ≡ g → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

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

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

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

postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)


text:
module Class.Monad.Writer where

open import Class.Monad
open import Data.Product
open import Data.Unit.Polymorphic
open import Level
open import Function

private
  variable
    a : Level
    A : Set a

record MonadWriter (M : Set a → Set a) {{_ : Monad M}} (W : Set a) : Set (suc a) where
  field
    tell : W → M ⊤
    listen : M A → M (A × W)
    pass : M (A × (W → W)) → M A

  listens : {B : Set a} → (W → B) → M A → M (A × B)
  listens f x = do
    (a , w) ← listen x
    return (a , f w)

  censor : (W → W) → M A → M A
  censor f x = pass $ do
    a ← x
    return (a , f)

open MonadWriter {{...}} public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Sigma
open import Definition.LogicalRelation.Substitution.Introductions.Fst
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.MaybeEmbed
open import Definition.LogicalRelation.Substitution.Introductions.Universe

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Valid snd term construction.
sndᵛ : ∀ {F G l∃ tu Γ}
       ([Γ] : ⊩ᵛ Γ) →
       let l    = ∞
           [UF] = maybeEmbᵛ {A = Univ % _} [Γ] (Uᵛ (proj₂ (levelBounded l∃)) [Γ])
           [U∃] = maybeEmbᵛ {A = Univ % _} [Γ] (Uᵛ (proj₂ (levelBounded l∃)) [Γ])
       in
        ([F] : Γ ⊩ᵛ⟨ l ⟩ F ^ [ % , ι l∃ ] / [Γ])
        ([G] : Γ ∙ F ^ [ % , ι l∃ ] ⊩ᵛ⟨ l ⟩ G ^ [ % , ι l∃ ] / [Γ] ∙ [F])
        ([UG] : Γ ∙ F ^ [ % , ι l∃ ] ⊩ᵛ⟨ l ⟩ Univ % l∃ ^ [ ! , next l∃ ] / [Γ] ∙ [F])
        ([Fₜ] : Γ ⊩ᵛ⟨ l ⟩ F ∷ Univ % l∃ ^ [ ! , next l∃ ] / [Γ] / [UF])
        ([Gₜ] : Γ ∙ F ^ [ % , ι l∃ ] ⊩ᵛ⟨ l ⟩ G ∷ Univ % l∃ ^ [ ! , next l∃ ] / [Γ] ∙ [F] / (λ {Δ} {σ} → [UG] {Δ} {σ}))
        ([tu] : Γ ⊩ᵛ⟨ l ⟩ tu ∷ ∃ F ▹ G ^ [ % , ι l∃ ] / [Γ] / ∃ᵛ {F} {G} [Γ] [F] [G])
        → Γ ⊩ᵛ⟨ l ⟩ snd tu ∷ G [ fst tu ] ^ [ % , ι l∃ ] / [Γ] / substS {F} {G} {fst tu} [Γ] [F] [G] (fstᵛ {F} {G} {l∃} {tu} {Γ} [Γ] [F] [G] (λ {Δ} {σ} → [UG] {Δ} {σ}) [Fₜ] [Gₜ] [tu])
sndᵛ {F} {G} {l∃} {tu} {Γ} [Γ] [F] [G] [UG] [Fₜ] [Gₜ] [tu] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [fst] = fstᵛ {F} {G} {l∃} {tu} {Γ} [Γ] [F] [G] (λ {Δ} {σ} → [UG] {Δ} {σ}) [Fₜ] [Gₜ] [tu]
      [G[fsttu]] = substS {F} {G} {fst tu} [Γ] [F] [G] [fst]
      [UF] = maybeEmbᵛ {A = Univ % _} [Γ] (Uᵛ (proj₂ (levelBounded l∃)) [Γ])
      [σUF] = proj₁ ([UF] ⊢Δ [σ])
      [σF] = proj₁ ([F] ⊢Δ [σ])
      ⊢F = escape [σF]
      [σF]ₜ = proj₁ ([Fₜ] ⊢Δ [σ])
      ⊢Fₜ = escapeTerm [σUF] [σF]ₜ
      [σUG] = proj₁ ([UG] {σ = liftSubst σ} (⊢Δ ∙ ⊢F)
                          (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]))
      [σG]ₜ = proj₁ ([Gₜ] (⊢Δ ∙ ⊢F)
                        (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]))
      ⊢Gₜ = escapeTerm [σUG] [σG]ₜ
      [σtu] = proj₁ ([tu] (⊢Δ) [σ])
      [∃FG] = ∃ᵛ {F} {G} {Γ} [Γ] [F] [G]
      [σ∃FG] = proj₁ ([∃FG] ⊢Δ [σ])
      ⊢tu = escapeTerm [σ∃FG] [σtu]
      ⊢snd = sndⱼ {F = subst σ F} {G = subst (liftSubst σ) G} {t = subst σ tu}
                   ⊢Fₜ ⊢Gₜ ⊢tu
      [σG[fsttu]] = proj₁ ([G[fsttu]] ⊢Δ [σ])
      ⊢sndSubst = PE.subst (λ x → _ ⊢ _ ∷ x  ^ _) (PE.sym (singleSubstLift G (fst tu))) ⊢snd
   in logRelIrr [σG[fsttu]] ⊢sndSubst ,
      (λ {σ′} [σ]′ [σ≡σ′] → logRelIrrEq [σG[fsttu]] ⊢sndSubst
     let [UF]′ = maybeEmbᵛ {A = Univ % _} [Γ] (Uᵛ (proj₂ (levelBounded l∃)) [Γ])
         [σUF]′ = proj₁ ([UF] ⊢Δ [σ]′)
         [σF]′ = proj₁ ([F] ⊢Δ [σ]′)
         ⊢F′ = escape [σF]′
         [σF]ₜ′ = proj₁ ([Fₜ] ⊢Δ [σ]′)
         ⊢Fₜ′ = escapeTerm [σUF]′ [σF]ₜ′
         [σUG]′ = proj₁ ([UG] {σ = liftSubst σ′} (⊢Δ ∙ ⊢F′)
                             (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]′))
         [σG]ₜ′ = proj₁ ([Gₜ] (⊢Δ ∙ ⊢F′)
                             (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]′))
         ⊢Gₜ′ = escapeTerm [σUG]′ [σG]ₜ′
         [σtu]′ = proj₁ ([tu] (⊢Δ) [σ]′)
         [σ∃FG]′ = proj₁ ([∃FG] ⊢Δ [σ]′)
         ⊢tu′ = escapeTerm [σ∃FG]′ [σtu]′
         ⊢snd′ = sndⱼ {F = subst σ′ F} {G = subst (liftSubst σ′) G} {t = subst σ′ tu}
                   ⊢Fₜ′ ⊢Gₜ′ ⊢tu′
         [σG[fsttu]′] = proj₁ ([G[fsttu]] ⊢Δ [σ]′)
         ⊢sndSubst′ = PE.subst (λ x → _ ⊢ _ ∷ x  ^ _) (PE.sym (singleSubstLift G (fst tu))) ⊢snd′
         [σG[fsttu]≡σG[fsttu]′] = proj₂ ([G[fsttu]] ⊢Δ [σ]) [σ]′ [σ≡σ′]
         ⊢σG[fsttu]≡σG[fsttu]′ = escapeEq [σG[fsttu]] [σG[fsttu]≡σG[fsttu]′]
      in conv ⊢sndSubst′ (≅-eq (≅-sym ⊢σG[fsttu]≡σG[fsttu]′)) )

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module plfa.part1.Naturals where

import Relation.Binary.PropositionalEquality as Eq

-- import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

-- 'refl' - the name for evidence that two terms are equal

-- Agda uses underbars to indicate where terms appear in
-- infix or mixfix operators:
--
-- * _≡_ and _≡⟨⟩_ -- infix
-- * begin_        -- prefix
-- * _∎            -- postfix

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

-- The following pragma tells Agda that ℕ corresponds to the
-- natural numbers, and hence one is permitted to type 0 as
-- shorthand for 'zero,' 1 as shorthand for 'suc zero'. It also
-- enables a more efficient internal representation of naturals
-- using the Haskell type for arbitrary-precision integers.

{-# BUILTIN NATURAL ℕ #-}

-- Operations on naturals are recursive functions

-- The empty braces are called a hole,
-- and 0 is a number used for referring to the hole

-------------------------------------------------------------
-- Workflow & hotkeys:
-------------------------------------------------------------
-- C-c C-l   - load the current file
-- C-c C-f   - moves to the next hole
-- C-c C-b   - moves to the previous hole
-- C-c C-,   - displays information on the required
--             type of the hole and available free vars
-- C-c C-c   - case split on a variable
-- C-c C-SPC - give to the hole at point an expression in it
-- C-c C-r   - solve the case trivially (refine)
-- gd        - go to definition (custom key binding)
-------------------------------------------------------------

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

-- It works because addition of larger numbers is defined in
-- terms of addition of smaller numbers. Such a definition is
-- called well founded.

-- 0       + n  ≡  n
-- (1 + m) + n  ≡  1 + (m + n)

-- We write '=' for definitions, while we write '≡' for
-- assertions that two already defined things are the same.

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩
    5
  ∎

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    suc (1 + 3)
  ≡⟨⟩
    suc (suc (0 + 3))
  ≡⟨⟩
    suc (suc 3)
  ≡⟨⟩
    5
  ∎

-- In fact, both proofs are longer than need be, and Agda is
-- satisfied with the following:

_ : 2 + 3 ≡ 5
_ = refl

-- Agda knows how to compute the value of 2 + 3, and so can
-- immediately check it is the same as 5. A binary relation is
-- said to be reflexive if every value relates to itself.
-- Evidence that a value is equal to itself is written 'refl'.

-- ^ 'refl' is defined almost the
-- same way as 'eq_relf' in Coq

-- Excercise:

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc (suc (0 + 4)))
  ≡⟨⟩
    7
  ∎

-- Multiplication

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

_ =
  begin
    2 * 3
  ≡⟨⟩    -- inductive case
    3 + (1 * 3)
  ≡⟨⟩    -- inductive case
    3 + (3 + (0 * 3))
  ≡⟨⟩    -- base case
    3 + (3 + 0)
  ≡⟨⟩    -- simplify
    6
  ∎

-- Exercise:

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

_ : 3 ^ 4 ≡ 81
_ =
  begin
    3 ^ 4
  ≡⟨⟩
   3 * (3 ^ 3)
  ≡⟨⟩
   3 * (3 * (3 ^ 2))
  ≡⟨⟩
   3 * (3 * (3 * (3 ^ 1)))
  ≡⟨⟩
   81
  ∎

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

_ =
  begin
    3 ∸ 2
  ≡⟨⟩
    2 ∸ 1
  ≡⟨⟩
    1 ∸ 0
  ≡⟨⟩
    1
  ∎

_ =
  begin
    2 ∸ 3
  ≡⟨⟩
    1 ∸ 2
  ≡⟨⟩
    0 ∸ 1
  ≡⟨⟩
    0
  ∎

-- Precedence

infixl 6  _+_  _∸_
infixl 7  _*_

-- Application binds more tightly than
-- (or has precedence over) any operator

-- Currying _

-- ℕ → ℕ → ℕ stands for ℕ → (ℕ → ℕ)

-- and

-- _+_ 2 3 stands for (_+_ 2) 3.

-- Writing definitions interactively

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

-- Exercise

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc ⟨⟩    = ⟨⟩ O
inc (x O) = x I
inc (x I) = inc x O

_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
_ = {!!}

to : ℕ → Bin
to zero    = ⟨⟩ O
to (suc m) = (to m) I

_ : to 12 ≡ ⟨⟩ I O I I
_ = {!!}

from : Bin → ℕ
from ⟨⟩    = 0
from (x O) = from x
from (x I) = suc (from x)

_ : from (⟨⟩ I O I I) ≡ 12
_ = {!!}

max_stars_repo_name: vyorkin/plfa

max_issues_repo_name: vyorkin/plfa

max_forks_repo_name: vyorkin/plfa


text:
module FunctionsInIndices where

open import Prelude
open import Eq

data Tree (a : Set) : ℕ -> Set where
  leaf : a -> Tree a 1
  node : forall n₁ n₂ -> Tree a n₁ -> Tree a n₂ -> Tree a (n₁ + n₂)

-- This does not work:

-- leftmost : forall {a} n -> Tree a (suc n) -> a
-- leftmost .0         (leaf x)                     = x
-- leftmost .n₂        (node zero     (suc n₂) l r) = leftmost l
-- leftmost .(n₁ + n₂) (node (suc n₁) n₂       l r) = leftmost l

module Workaround1 where

  private

    T : Set -> ℕ -> Set
    T a zero    = ⊤
    T a (suc n) = a

    leftmost' : forall {a n} -> Tree a n -> T a n
    leftmost' (leaf x)                     = x
    leftmost' (node zero     zero     l r) = tt
    leftmost' (node zero     (suc n₂) l r) = leftmost' r
    leftmost' (node (suc n₁) n₂       l r) = leftmost' l

  leftmost : forall {a n} -> Tree a (suc n) -> a
  leftmost = leftmost'

module Workaround2 where

  private

    leftmost' : forall {a n m} -> Tree a m -> m ≡ suc n -> a
    leftmost' (leaf x)                     _  = x
    leftmost' (node zero     (suc n₂) l r) _  = leftmost' r refl
    leftmost' (node (suc n₁) n₂       l r) _  = leftmost' l refl

  leftmost : forall {a n} -> Tree a (suc n) -> a
  leftmost t = leftmost' t refl


text:
{-# OPTIONS --experimental-irrelevance #-}
-- {-# OPTIONS -v tc.lhs:20 #-}
module ShapeIrrelevantIndex where

data Nat : Set where
  Z : Nat
  S : Nat → Nat

data Good : ..(_ : Nat) → Set where
  goo  : .(n : Nat) → Good (S n)

bad : .(n : Nat) → Good n → Nat
bad .(S n) (goo n) = n


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

-- From: Peter Dybjer. Comparing integrated and external logics of
-- functional programs. Science of Computer Programming, 14:59–79,
-- 1990

module Norm where

postulate Char : Set

data Atom : Set where
  True False : Atom
  Var        : Char → Atom

data Exp : Set where
  at : Atom → Exp
  if : Exp → Exp → Exp → Exp

-- Agda doesn't recognize the termination of the function.
{-# TERMINATING #-}
norm : Exp → Exp
norm (at a)              = at a
norm (if (at a) y z)     = if (at a) (norm y) (norm z)
norm (if (if u v w) y z) = norm (if u (if v y z) (if w y z))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Ferros.Resource.CNode where

open import Ferros.Resource.CNode.Base public

max_stars_repo_name: auxoncorp/ferros-spec

max_issues_repo_name: auxoncorp/ferros-spec

max_forks_repo_name: auxoncorp/ferros-spec


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

module Basics where

open import Base public
open import PropT public
open import hSet public

open import lib.Basics public

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization