text:
open import Level hiding ( suc ; zero )
open import Algebra
module sym5 where

open import Symmetric
open import Data.Unit using (⊤ ; tt )
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function hiding (flip)
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Data.Nat.Properties
open import Relation.Nullary
open import Data.Empty
open import Data.Product

open import Gutil
open import Putil
open import Solvable using (solvable)
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open import Data.Fin hiding (_<_ ; _≤_  ; lift )
open import Data.Fin.Permutation  hiding (_∘ₚ_)

infixr  200 _∘ₚ_
_∘ₚ_ = Data.Fin.Permutation._∘ₚ_

open import Data.List  hiding ( [_] )
open import nat
open import fin
open import logic

open _∧_

¬sym5solvable : ¬ ( solvable (Symmetric 5) )
¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where
--
--    dba       1320      d → b → a → d
--    (dba)⁻¹   3021      a → b → d → a
--    aec       21430
--    (aec)⁻¹   41032
--    [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
--      so commutator always contains abc, dba and aec

     open ≡-Reasoning

     open solvable
     open Solvable ( Symmetric 5)
     end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →  x =p= pid
     end5 x der = end sol x der

     0<4 : 0 < 4
     0<4 = s≤s z≤n

     0<3 : 0 < 3
     0<3 = s≤s z≤n

     --- 1 ∷ 2 ∷ 0 ∷ []      abc
     3rot : Permutation 3 3
     3rot = pid {3} ∘ₚ pins (n≤ 2)

     save2 : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) →  Permutation  5 5
     save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4)

     ins2 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 )

     ins2cong : {i j : ℕ }  → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → ins2 x i<3 j<4  =p= ins2 y i<3 j<4
     ins2cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )}
         (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl

     open _=p=_

     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     abc i<3 j<4 = ins2 3rot i<3 j<4
     dba : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
     dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4

     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
     counter-example eq with ←pleq _ _ eq
     ...  | ()

     record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where
       field
         dba0<3 : Fin 4
         dba1<4 : Fin 5
         aec0<3 : Fin 4
         aec1<4 : Fin 5
         abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot)  (fin≤n {3} dba0<3) (fin≤n {4} dba1<4)  , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ]

     open Triple
     triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot
     triple z≤n z≤n =                               record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple z≤n (s≤s z≤n) =                         record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple z≤n (s≤s (s≤s z≤n)) =                   record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     triple z≤n (s≤s (s≤s (s≤s z≤n))) =             record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) =       record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
     triple (s≤s z≤n) z≤n =                         record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl }
     triple (s≤s z≤n) (s≤s z≤n) =                   record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl }
     triple (s≤s z≤n) (s≤s (s≤s z≤n)) =             record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) =       record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s z≤n)) z≤n =                   record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s z≤n)) (s≤s z≤n) =             record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) =       record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s (s≤s z≤n))) z≤n =             record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) =       record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =
                                                    record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }

     _⁻¹ : {n : ℕ } ( x : Permutation n n) → Permutation n n
     _⁻¹ = pinv

     -- tt5 : (i : Fin 4) (j : Fin 5) → (z : Fin 4) → (w : Fin 5) → (x : Fin 5) (y : Fin 4)  → (rot : Permutation 3 3 )  → List (List ℕ) → List (List ℕ)
     -- tt5 i j z w x y rot t with is-=p= (ins2 rot (fin≤n  i) (fin≤n  j))
     --             [ ins2 (rot ∘ₚ rot)   (fin≤n  z) (fin≤n  x)  , ins2 (pinv rot) (fin≤n  y)  (fin≤n  w) ]
     -- ... | yes _ = ( toℕ i ∷ toℕ j ∷ 9 ∷ toℕ z ∷ toℕ x ∷ toℕ y ∷ toℕ w  ∷ [] ) ∷ t
     -- ... | no _ = t

     -- open import  Relation.Binary.Definitions

     -- tt2 : (i : Fin 4) (j : Fin 5) →  (rot : Permutation 3 3 ) → List (List ℕ)
     -- tt2  i j rot = tt3 (# 4) (# 3) (# 3) (# 4) [] where
     --     tt3 : (w : Fin 5) (z : Fin 4) (x : Fin 4) (y : Fin 5) → List (List ℕ) → List (List ℕ)
     --     tt3 zero zero zero zero t =                                       ( tt5 i j zero zero zero zero    rot [] ) ++ t
     --     tt3 (suc w)  zero zero zero t =  tt3 (fin+1 w) (# 3) (# 3) (# 4)       ((tt5 i j zero (suc w) zero zero    rot [] ) ++ t)
     --     tt3 w z zero (suc y) t =       tt3 w z         (# 3) (fin+1 y)   ((tt5 i j z w (suc y) zero    rot [] ) ++ t)
     --     tt3 w z (suc x) y    t =       tt3 w z         (fin+1 x)    y    ((tt5 i j z  w y    (suc x) rot [] ) ++ t)
     --     tt3 w (suc z) zero zero t =    tt3 w (fin+1 z) (# 3) (# 4)       ((tt5 i j (suc z) w zero zero    rot [] ) ++ t)

     -- tt4 :  List (List (List ℕ))
     -- tt4  = tt2 (# 0) (# 0) (pinv 3rot) ∷
     --       tt2 (# 1) (# 0) (pinv 3rot) ∷
     --       tt2 (# 2) (# 0) (pinv 3rot) ∷
     --       tt2 (# 3) (# 0) (pinv 3rot) ∷
     --       tt2 (# 0) (# 1) (pinv 3rot) ∷
     --       tt2 (# 1) (# 1) (pinv 3rot) ∷
     --       tt2 (# 2) (# 1) (pinv 3rot) ∷
     --       tt2 (# 3) (# 1) (pinv 3rot) ∷
     --       tt2 (# 0) (# 2) (pinv 3rot) ∷
     --       tt2 (# 1) (# 2) (pinv 3rot) ∷
     --       tt2 (# 2) (# 2) (pinv 3rot) ∷
     --       tt2 (# 3) (# 2) (pinv 3rot) ∷
     --       tt2 (# 0) (# 3) (pinv 3rot) ∷
     --       tt2 (# 1) (# 3) (pinv 3rot) ∷
     --       tt2 (# 2) (# 3) (pinv 3rot) ∷
     --       tt2 (# 3) (# 3) (pinv 3rot) ∷
     --       tt2 (# 0) (# 4) (pinv 3rot) ∷
     --       tt2 (# 1) (# 4) (pinv 3rot) ∷
     --       tt2 (# 2) (# 4) (pinv 3rot) ∷
     --       tt2 (# 3) (# 4) (pinv 3rot) ∷
     --       []

     open Triple
     dba-triple : {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) → Triple i<3 j<4 (3rot  ∘ₚ 3rot )
     dba-triple z≤n z≤n =                               record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple z≤n (s≤s z≤n) =                         record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple z≤n (s≤s (s≤s z≤n)) =                   record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     dba-triple z≤n (s≤s (s≤s (s≤s z≤n))) =             record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
     dba-triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) =       record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     dba-triple (s≤s z≤n) z≤n =                         record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
     dba-triple (s≤s z≤n) (s≤s z≤n) =                   record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl }
     dba-triple (s≤s z≤n) (s≤s (s≤s z≤n)) =             record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) =       record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s z≤n)) z≤n =                   record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s z≤n)) (s≤s z≤n) =             record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) =       record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s (s≤s z≤n))) z≤n =             record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) =       record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl }
     dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) =
                                                    record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl }

     -3=33 : pinv 3rot =p= (3rot ∘ₚ 3rot )
     -3=33 = pleq _ _ refl

     4=1 : (3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot ) =p= 3rot
     4=1 = pleq _ _ refl

     dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
          → deriving n (abc i<3 j<4 )
     dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ }  → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 )
          → deriving n (dba i<3 j<4 )

     commd : {n : ℕ } → (f g : Permutation 5 5)
           →  deriving n f
           →  deriving n g
           → Commutator (deriving n) [ f , g ]
     commd {n} f g df dg =  comm {deriving n} {f} {g} df dg

     dervie-any-3rot0 0 i<3 j<4 = lift tt
     dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where
        tc = triple i<3 j<4
        dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
        aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))
        ceq : abc i<3 j<4  =p=  [ dba0 , aec0 ]
        ceq = record { peq = peq (abc= tc) }
        df =  dervie-any-3rot1 i  (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc))
        dg =  dervie-any-3rot1 i  (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc))

     dervie-any-3rot1 0 i<3 j<4 = lift tt
     dervie-any-3rot1 (suc n) {i} {j} i<3 j<4 = ccong {deriving n} ( psym ceq )  (commd aec0 abc0 df dg ) where
        tdba = dba-triple i<3 j<4
        aec0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))
        abc0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))
        ceq : dba i<3 j<4 =p=  [ aec0 , abc0 ]
        ceq = record { peq = peq (abc= tdba) }
        df : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)))
        df = deriving-subst (psym (ins2cong {toℕ (dba0<3 (dba-triple i<3 j<4))} {toℕ (dba1<4 (dba-triple i<3 j<4))} 4=1 ))
             (dervie-any-3rot0 n  (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)))
        dg : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)))
        dg = deriving-subst (psym (ins2cong {toℕ (aec0<3 (dba-triple i<3 j<4))} {toℕ (aec1<4 (dba-triple i<3 j<4))} 4=1 ))
             (dervie-any-3rot0 n  (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)))

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
module Sandbox.PrimitiveRecursion where

open import Data.Nat
open import Data.Fin using (Fin)
open import Data.Vec

data PR : ℕ → Set where
    -- Constant function: The 0-ary constant function 0 is primitive recursive.
    K : PR 0

    -- Successor function: The 1-ary successor function S, which returns the
    -- successor of its argument (see Peano postulates), is primitive recursive.
    -- That is, S(k) = k + 1.
    S : PR 1

    -- Projection function: For every n≥1 and each i with 1≤i≤n, the n-ary
    -- projection function Pᵢⁿ, which returns its i-th argument, is primitive
    -- recursive.
    Proj : ∀ {n} → (i : Fin n) → PR n

    -- Composition: Given f, a m-ary primitive recursive function, and m n-ary
    -- primitive recursive functions g1,...,gm, the composition of f with
    -- g1,...,gk, is primitive recursive
    --  f(
    --      g₁(x₁, x₂, ..., xₙ)
    --      g₂(x₁, x₂, ..., xₙ)
    --      ...
    --      gₘ(x₁, x₂, ..., xₙ)
    --  )
    Comp : ∀ {m n} → (f : PR m) → Vec (PR n) m → PR n
    -- Primitive recursion: Given f, a m-ary primitive recursive function,
    -- and g, a (m+2)-ary primitive recursive function, the (m+1)-ary function
    -- h is defined as the primitive recursion of f and g, i.e. the function h
    -- is primitive recursive when
    --  h(0   , x₁, x₂, .. xₘ) = f(x₁, x₂, .. xₘ)
    --  h(S(n), x₁, x₂, .. xₘ) = g(n, h(n, x₁, x₂, .. xₘ), x₁, x₂, .. xₘ)
    Rec : ∀ {n} → (f : PR {!   !}) (g : PR (suc (suc n))) → PR (suc n)

mutual
    ⟦_⟧_ : ∀ {a} → PR a → Vec ℕ a → ℕ
    ⟦ K         ⟧ args           = zero
    ⟦ S         ⟧ args           = suc zero
    ⟦ Proj i    ⟧ args           = lookup i args
    ⟦ Comp f gs ⟧ args           = ⟦ f ⟧ (⟦ gs ⟧* args)
    ⟦ Rec  f g  ⟧ (zero  ∷ args) = ⟦ f ⟧ args
    ⟦ Rec  f g  ⟧ (suc x ∷ args) = ⟦ g ⟧ (x ∷ (⟦ f ⟧ args) ∷ args)

    ⟦_⟧* : {m n : ℕ} (gs : Vec (PR n) m) → Vec ℕ n → Vec ℕ m
    ⟦ []     ⟧* args = []
    ⟦ g ∷ gs ⟧* args = (⟦ g ⟧ args) ∷ ⟦ gs ⟧* args

ext: agda

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
open import Agda.Builtin.Nat

data List (A : Set) : Set where
  lnil : List A
  lcons : A → List A → List A

data Vec (A : Set) : Nat → Set where
  vnil  : Vec A 0
  vcons : ∀ {n} → A → Vec A n → Vec A (suc n)

pattern [] = lnil
pattern [] = vnil

pattern _∷_ x xs = lcons x xs
pattern _∷_ y ys = vcons y ys

lmap : ∀ {A B} → (A → B) → List A → List B
lmap f [] = []
lmap f (x ∷ xs) = f x ∷ lmap f xs

vmap : ∀ {A B n} → (A → B) → Vec A n → Vec B n
vmap f [] = []
vmap f (x ∷ xs) = f x ∷ vmap f xs

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  P : Prop
  p : P
  f : P -> P

  g : {A : Set} -> P -> A -> A
  eq : ∀{A} {x : A} -> g p x ≡ x

{-# REWRITE eq #-}

module _ {A : Set} {x : A} {y : P} where

  foo : g p x ≡ x
  foo = refl

  bar : g (f y) x ≡ x
  bar = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Common

module Action {ℙ : Set} (message : Message ℙ)
  where

open Message message

data Action : Set where
  I O : ℙ -> Action

input-injective : ∀{x y} -> I x ≡ I y -> x ≡ y
input-injective refl = refl

output-injective : ∀{x y} -> O x ≡ O y -> x ≡ y
output-injective refl = refl

co-action : Action -> Action
co-action (I x) = O x
co-action (O x) = I x

co-action-injective : ∀{x y} -> co-action x ≡ co-action y -> x ≡ y
co-action-injective {I x} {I .x} refl = refl
co-action-injective {O x} {O .x} refl = refl

co-action-involution : (α : Action) -> co-action (co-action α) ≡ α
co-action-involution (I _) = refl
co-action-involution (O _) = refl

action-equality-dec : (α β : Action) -> Dec (α ≡ β)
action-equality-dec (I x) (I y) with x ?= y
... | yes eq rewrite eq = yes refl
... | no neq = no λ eq -> neq (input-injective eq)
action-equality-dec (I x) (O y) = no λ ()
action-equality-dec (O x) (I y) = no λ ()
action-equality-dec (O x) (O y) with x ?= y
... | yes eq rewrite eq = yes refl
... | no neq = no λ eq -> neq (output-injective eq)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Numeral.Natural.Relation.Divisibility.Proofs.Modulo where

import Lvl
open import Data
open import Functional
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.DivMod.Proofs
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Modulo.Proofs
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function.Domain
open import Structure.Operator.Properties
open import Structure.Operator.Proofs.Util
open import Syntax.Transitivity
open import Type

divides-mod : ∀{a b d} → (d ∣ 𝐒(b)) → (d ∣ a) ↔ (d ∣ a mod 𝐒(b))
divides-mod {a}{b}{d} db = [↔]-intro (l db) (r db) where
  l : ∀{a b d} → (d ∣ 𝐒(b)) → (d ∣ a) ← (d ∣ (a mod₀ 𝐒(b)))
  l {a}{b}{𝟎}    db dmod with () ← [0]-only-divides-[0] db
  l {a}{b}{𝐒(d)} db dmod
    with [∃]-intro (𝐒(n)) ⦃ dnb ⦄  ← [↔]-to-[←] divides-[⋅]-existence db
    with [∃]-intro m     ⦃ dmmod ⦄ ← [↔]-to-[←] divides-[⋅]-existence dmod
    = [↔]-to-[→] divides-[⋅]-existence ([∃]-intro (((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ 𝐒(n)) + m) ⦃ p ⦄) where
    p : (𝐒(d) ⋅ (((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ 𝐒(n)) + m) ≡ a)
    p =
      𝐒(d) ⋅ (((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ 𝐒(n)) + m)                     🝖[ _≡_ ]-[ distributivityₗ(_⋅_)(_+_) {𝐒(d)}{(a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ 𝐒(n)}{m} ]
      (𝐒(d) ⋅ ((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ 𝐒(n))) + (𝐒(d) ⋅ m)            🝖[ _≡_ ]-[ [≡]-with(_+ (𝐒(d) ⋅ m)) (One.commuteₗ-assocᵣ {a = 𝐒(d)}{a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))}{𝐒(n)}) ]
      ((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ (𝐒(d) ⋅ 𝐒(n))) + (𝐒(d) ⋅ m)            🝖[ _≡_ ]-[ [≡]-with(((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ (𝐒(d) ⋅ 𝐒(n))) +_) dmmod ]
      ((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ (𝐒(d) ⋅ 𝐒(n))) + (a mod 𝐒(b))          🝖[ _≡_ ]-[ [≡]-with(expr ↦ ((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ (𝐒(d) ⋅ 𝐒(n))) + (a mod 𝐒(expr))) (injective(𝐒) dnb) ]-sym
      ((a ⌊/⌋ (𝐒(d) ⋅ 𝐒(n))) ⋅ (𝐒(d) ⋅ 𝐒(n))) + (a mod (𝐒(d) ⋅ 𝐒(n))) 🝖[ _≡_ ]-[ [⌊/⌋][mod]-is-division-with-remainder {a}{d + 𝐒(d) ⋅ n} ]
      a                                                               🝖-end

  r : ∀{a b d} → (d ∣ 𝐒(b)) → (d ∣ a) → (d ∣ (a mod₀ 𝐒(b)))
  r {a}{b}{𝟎}   db da with [≡]-intro ← [0]-only-divides-[0] da = Div𝟎
  r {a}{b}{𝐒 d} db da
    with [∃]-intro n ⦃ dna ⦄ ← [↔]-to-[←] divides-[⋅]-existence da
    with [∃]-intro m ⦃ dmb ⦄ ← [↔]-to-[←] divides-[⋅]-existence db
    = [↔]-to-[→] divides-[⋅]-existence ([∃]-intro (n mod₀ m) ⦃ p ⦄) where
    p : (𝐒(d) ⋅ (n mod₀ m) ≡ a mod₀ 𝐒(b))
    p =
      𝐒(d) ⋅ (n mod₀ m)          🝖[ _≡_ ]-[ [⋅][mod]-distributivityₗ {n}{m}{𝐒(d)} ]
      (𝐒(d) ⋅ n) mod₀ (𝐒(d) ⋅ m) 🝖[ _≡_ ]-[ [≡]-with(\expr → ((𝐒(d) ⋅ n) mod₀ expr)) dmb ]
      (𝐒(d) ⋅ n) mod₀ 𝐒(b)       🝖[ _≡_ ]-[ [≡]-with(_mod₀ 𝐒(b)) dna ]
      a mod₀ 𝐒(b)                🝖[ _≡_ ]-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Inductive where

open import Level using (_⊔_)
open import Data.Nat hiding (_⊔_)
open import Data.Fin
open import Data.List hiding (map)
import Data.List as List
open import Data.Vec hiding (_++_)
open import Data.Product hiding (map)
open import Tuple using (Tuple; []; _∷_; unfoldToFunc; apply; proof₁; proof₂)

Const : Set₁
Const = List Set × List (List Set)

data TupleRec (A : Set) : List (List Set) → Set where
  [] : TupleRec A []
  _∷_ : ∀ {x xs} → ((Tuple x) → A) → TupleRec A xs → TupleRec A (x ∷ xs)

data Inductive {n} (A : Vec Const n) : Set where
  construct : (m : Fin n)
              (x : Tuple (proj₁ (lookup m A)))
              (r : TupleRec (Inductive A) (proj₂ (lookup m A)))
            → Inductive A

unfoldToConFunc : List (List Set) → Set → Set
unfoldToConFunc [] B = B
unfoldToConFunc (As ∷ As₁) B = (unfoldToFunc As B) → unfoldToConFunc As₁ B

unfoldToRecFunc : List (List Set) → Set → Set → Set
unfoldToRecFunc [] B C = C
unfoldToRecFunc (As ∷ As₁) B C = (unfoldToFunc As B) → (unfoldToFunc As C) →
                                 unfoldToRecFunc As₁ B C

proofCon : (As : List (List Set)) {B : Set}
         → (TupleRec B As → B) → unfoldToConFunc As B
proofCon [] B₁ = B₁ []
proofCon (As ∷ As₁) B₁ x = proofCon As₁ (λ x₁ → B₁ (proof₂ As x ∷ x₁))

-- The constrution function of an inductive instance
ConFunc : Set → Const → Set
ConFunc A (proj₁ , proj₂) = unfoldToFunc proj₁ (unfoldToConFunc proj₂ A)

-- The recursion function of an inductive instance
RecFunc : Set → Set → Const → Set
RecFunc A B (proj₁ , proj₂) = unfoldToFunc proj₁ (unfoldToRecFunc proj₂ A B)

recapply : ∀ {n} {A : Vec Const n} {B : Set}
        {L : List Set} {R : List (List Set)}
      → RecFunc (Inductive A) B (L , R)
      → Tuple L → TupleRec (Inductive A) R → TupleRec B R → B
recapply {L = []} {[]} f [] [] [] = f
recapply {L = []} {R ∷ Rs} f [] (x ∷ x₁) (x₂ ∷ x₃) =
  recapply {L = []} {R = Rs} (f (proof₁ R x) (proof₁ R x₂)) [] x₁ x₃
recapply {L = _ ∷ _} f (x₁ ∷ x₂) r c = recapply (f x₁) x₂ r c

rec : ∀ {n} {A : Vec Const n} {B : Set}
    → Tuple (toList (map (RecFunc (Inductive A) B) A))
    → Inductive A → B
rec {n} {A} {B} fs (construct m x r) = rec' A fs m x r
  where mapRec : ∀ {m} → TupleRec (Inductive A) m → TupleRec B m
        mapRec {m = []} [] = []
        mapRec {m = _ ∷ _} (x₁ ∷ r₁) = (λ x₂ → rec fs (x₁ x₂)) ∷ mapRec r₁
        rec' : ∀ {m}
             → (A' : Vec Const m)
             → Tuple (toList (map (RecFunc (Inductive A) B) A'))
             → (m' : Fin m)
             → Tuple (proj₁ (lookup m' A'))
             → TupleRec (Inductive A) (proj₂ (lookup m' A'))
             → B
        rec' [] fs () x r
        rec' (_ ∷ A') (f ∷ fs) zero x r = recapply f x r (mapRec r)
        rec' (_ ∷ A') (f ∷ fs) (suc m) x r = rec' A' fs m x r

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Results concerning function extensionality for propositional equality
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Axiom.Extensionality.Heterogeneous where

import Axiom.Extensionality.Propositional as P
open import Function
open import Level
open import Relation.Binary.HeterogeneousEquality.Core
open import Relation.Binary.PropositionalEquality.Core

------------------------------------------------------------------------
-- Function extensionality states that if two functions are
-- propositionally equal for every input, then the functions themselves
-- must be propositionally equal.

Extensionality : (a b : Level) → Set _
Extensionality a b =
  {A : Set a} {B₁ B₂ : A → Set b}
  {f₁ : (x : A) → B₁ x} {f₂ : (x : A) → B₂ x} →
  (∀ x → B₁ x ≡ B₂ x) → (∀ x → f₁ x ≅ f₂ x) → f₁ ≅ f₂

------------------------------------------------------------------------
-- Properties

-- This form of extensionality follows from extensionality for _≡_.

≡-ext⇒≅-ext : ∀ {ℓ₁ ℓ₂} →
              P.Extensionality ℓ₁ (suc ℓ₂) →
              Extensionality ℓ₁ ℓ₂
≡-ext⇒≅-ext {ℓ₁} {ℓ₂} ext B₁≡B₂ f₁≅f₂ with ext B₁≡B₂
... | refl = ≡-to-≅ $ ext′ (≅-to-≡ ∘ f₁≅f₂)
  where
  ext′ : P.Extensionality ℓ₁ ℓ₂
  ext′ = P.lower-extensionality ℓ₁ (suc ℓ₂) ext


text:
module Tactic.Nat.Less.Lemmas where

open import Prelude

open import Tactic.Nat.Exp
open import Tactic.Nat.NF
open import Tactic.Nat.Subtract.Exp
open import Tactic.Nat.Auto.Lemmas
open import Tactic.Nat.Simpl.Lemmas
open import Tactic.Nat.Subtract.Lemmas

liftNFSubLess : ∀ e₁ e₂ ρ → ⟦ normSub e₁ ⟧sn ρ < ⟦ normSub e₂ ⟧sn ρ → ⟦ e₁ ⟧se ρ < ⟦ e₂ ⟧se ρ
liftNFSubLess e₁ e₂ ρ (diff k eq) = diff k (eraseEquality $
  sound-sub e₂ ρ ⟨≡⟩ eq ⟨≡⟩ʳ (suc k +_) $≡ sound-sub e₁ ρ)

SubExpLess : SubExp → SubExp → Env Var → Set
SubExpLess e₁ e₂ ρ = ⟦ e₁ ⟧se ρ < ⟦ e₂ ⟧se ρ

NFLessS : SubNF × SubNF → Env SubAtom → Set
NFLessS (nf₁ , nf₂) ρ = ⟦ nf₁ ⟧ns ρ < ⟦ nf₂ ⟧ns ρ

CancelSubLess : SubExp → SubExp → Env Var → Set
CancelSubLess e₁ e₂ ρ = NFLessS (cancel (normSub e₁) (normSub e₂)) (atomEnvS ρ)

c⟦_⟧eqn : Eqn → Env Var → Set
c⟦ a :≡ b ⟧eqn = CancelSubEq a b
c⟦ a :< b ⟧eqn = CancelSubLess a b

simplifySubLess : ∀ e₁ e₂ (ρ : Env Var) → CancelSubLess e₁ e₂ ρ → SubExpLess e₁ e₂ ρ
simplifySubLess e₁ e₂ ρ H with cancel (normSub e₁) (normSub e₂)
                             | λ a b → cancel-sound′ a b (normSub e₁) (normSub e₂) (atomEnvS ρ)
simplifySubLess e₁ e₂ ρ (diff k H) | v₁ , v₂ | sound =
  liftNFSubLess e₁ e₂ ρ $ diff k $
    lem-eval-sn-nS (normSub e₂) ρ ⟨≡⟩
    sound (suc k) 0
      ((suc k +_) $≡ ns-sound v₁ (atomEnvS ρ) ʳ⟨≡⟩
       H ʳ⟨≡⟩ ns-sound v₂ (atomEnvS ρ)) ʳ⟨≡⟩ʳ
    (suc k +_) $≡ lem-eval-sn-nS (normSub e₁) ρ

complicateSubLess : ∀ e₁ e₂ ρ → SubExpLess e₁ e₂ ρ → CancelSubLess e₁ e₂ ρ
complicateSubLess e₁ e₂ ρ H with cancel (normSub e₁) (normSub e₂)
                                   | λ a b → cancel-complete′ a b (normSub e₁) (normSub e₂) (atomEnvS ρ)
complicateSubLess e₁ e₂ ρ (diff k H) | v₁ , v₂ | complete = diff k (eraseEquality $
  ns-sound v₂ (atomEnvS ρ) ⟨≡⟩
  complete (suc k) 0
    ((suc k +_) $≡ lem-eval-sn-nS (normSub e₁) ρ ʳ⟨≡⟩
     (suc k +_) $≡ sound-sub e₁ ρ ʳ⟨≡⟩
     H ʳ⟨≡⟩ sound-sub e₂ ρ ⟨≡⟩
     lem-eval-sn-nS (normSub e₂) ρ) ʳ⟨≡⟩ʳ
  (suc k +_) $≡ ns-sound v₁ (atomEnvS ρ))

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


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

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

-- This module defines the types used to define a SystemModel.

module LibraBFT.Yasm.Base
  (ℓ-EC        : Level)
  (EpochConfig : Set ℓ-EC)
  (epochId     : EpochConfig → ℕ)
  (authorsN    : EpochConfig → ℕ)
 where

 EpochId : Set
 EpochId = ℕ

 Member : EpochConfig → Set
 Member = Fin ∘ authorsN

 record EpochConfigFor (eid : EpochId) : Set ℓ-EC where
   field
    epochConfig : EpochConfig
    forEpochId  : epochId epochConfig ≡ eid

 -- Our system is configured through a value of type
 -- SystemParameters where we specify:
 record SystemParameters : Set (ℓ+1 0ℓ ℓ⊔ ℓ-EC) where
  constructor mkSysParms
  field
    PeerId    : Set
    _≟PeerId_ : ∀ (p₁ p₂ : PeerId) → Dec (p₁ ≡ p₂)
    PeerState : Set
    initPS    : PeerState  -- Represents an uninitialised PeerState, about which we know nothing whatsoever
    Msg       : Set
    Part      : Set -- Types of interest that can be represented in Msgs

    -- The messages must be able to carry signatures
    instance Part-sig : WithSig Part

    -- A relation specifying what Parts are included in a Msg.
    _⊂Msg_       : Part → Msg → Set

    -- Finally, messages must carry an epoch id and might have an author
    part-epoch  : Part → EpochId

    -- Initializes a potentially-empty state with an EpochConfig
    init : PeerId → EpochConfig → PeerState → PeerState × List Msg

    -- Handles a message on a previously initialized peer.
    handle : PeerId → Msg → PeerState → PeerState × List Msg

    -- TODO-3?: So far, handlers only produce messages to be sent.
    -- It would be reasonable to generalize this to something like
    --
    --   data Action = Send Msg | Crash CrashMsg | Log LogMsg | ...
    --
    -- on the system level, and have the handlers return List Action,
    -- rather than just ListMsg.  For example, if an assertion fires, this
    -- could "kill the process" and make it not send any messages in the future.
    -- We could also then prove that the handlers do not crash, certain
    -- messages are logged under certain circumstances, etc.
    --
    -- Alternatively, we could keep this outside the system model by
    -- defining an application-specific peerState type, for example:
    --
    -- > libraHandle : Msg → Status × Log × LState → Status × LState × List Action
    -- > libraHandle _ (Crashed , l , s) = Crashed , s , [] -- i.e., crashed peers never send messages
    -- >
    -- > handle = filter isSend ∘ libraHandle

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
open import FRP.JS.Level using ()

module FRP.JS.Primitive where

-- We define the primitive types here, to avoid cyclic module dependencies

data Bool : Set where
  true  : Bool
  false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

{-# COMPILED_JS Bool function(x,v) { if (x) { return v["true"](); } else { return v["false"](); } } #-}
{-# COMPILED_JS true true #-}
{-# COMPILED_JS false false #-}

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

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

{-# COMPILED_JS ℕ function (x,v) {
  if (x < 1) { return v.zero(); } else { return v.suc(x-1); }
} #-}
{-# COMPILED_JS zero 0 #-}
{-# COMPILED_JS suc function (x) { return x+1; } #-}

postulate
  Char String ℝ ℤ : Set

{-# BUILTIN CHAR    Char #-}
{-# BUILTIN STRING  String #-}
{-# BUILTIN FLOAT   ℝ #-}
{-# BUILTIN INTEGER ℤ #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module Data.List.Relation.Pairwise.Proofs where

open import Data.List
import      Data.List.Functions as List
open import Data.List.Relation.Pairwise
open import Logic
import      Lvl
open import Type

private variable ℓ ℓₗ : Lvl.Level
private variable T A B : Type{ℓ}
private variable x : T
private variable f : A → B
private variable _▫_ : T → T → Type{ℓₗ}
private variable _▫₁_ : A → A → Type{ℓₗ}
private variable _▫₂_ : B → B → Type{ℓₗ}

AdjacentlyPairwise-map : (∀{x y} → (x ▫₁ y) → (f(x) ▫₂ f(y))) → ∀{l} → AdjacentlyPairwise(_▫₁_)(l) → AdjacentlyPairwise(_▫₂_)(List.map f(l))
AdjacentlyPairwise-map p {∅} s = AdjacentlyPairwise.empty
AdjacentlyPairwise-map p {x ⊰ ∅} s = AdjacentlyPairwise.single
AdjacentlyPairwise-map p {x ⊰ y ⊰ l} (AdjacentlyPairwise.step ⦃ s₁ ⦄ ⦃ s₂ ⦄) = AdjacentlyPairwise.step ⦃ p s₁ ⦄ ⦃ AdjacentlyPairwise-map p {y ⊰ l} s₂ ⦄

AdjacentlyPairwise-prepend : (∀{y} → (x ▫ y)) → ∀{l} → AdjacentlyPairwise(_▫_)(l) → AdjacentlyPairwise(_▫_)(x ⊰ l)
AdjacentlyPairwise-prepend xy {∅}     p = AdjacentlyPairwise.single
AdjacentlyPairwise-prepend xy {_ ⊰ _} p = AdjacentlyPairwise.step ⦃ xy ⦄ ⦃ p ⦄


text:
{-# OPTIONS --rewriting #-}
module JVM.Transform.Assemble where

open import Agda.Builtin.Equality.Rewrite

open import Data.Nat using (ℕ)
open import Data.List as List
open import Data.List.Properties
open import Data.List.Relation.Unary.All as All
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.Any
open import Data.Product hiding (swap)

open import Relation.Unary hiding (_∈_)
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Core
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Data.Bigstar
open import Relation.Ternary.Data.ReflexiveTransitive as Star
open import Relation.Ternary.Data.IndexedMonoid
open import Relation.Ternary.Construct.Bag.Properties

open import JVM.Types
open import JVM.Syntax.Values
open import JVM.Model StackTy
open import JVM.Model.Properties
open import JVM.Syntax.Labeling StackTy
open import JVM.Syntax.Instructions hiding (⟨_↝_⟩; Instr)

{-# REWRITE ++-assoc #-}

Typing = List StackTy

variable
  J₁ J₂ J : Typing

module _ Γ where

  data Instr (J : Typing) : StackTy → StackTy → Set where
    goto  : ψ₁ ∈ J → Instr J ψ₁ ψ₂
    if    : ∀ {as} → Comparator as → ψ₁ ∈ J → Instr J (as ++ ψ₁) ψ₂

    nop   : Instr J ψ₁ ψ₁
    push  : Const a → Instr J ψ₁ (a ∷ ψ₁)
    pop   : Instr J (a ∷ ψ₁) ψ₁
    dup   : Instr J (a ∷ ψ₁) (a ∷ a ∷ ψ₁)
    swap  : Instr J (a ∷ b ∷ ψ₁) (b ∷ a ∷ ψ₁)
    bop   : NativeBinOp a b c → Instr J (b ∷ a ∷ ψ₁) (c ∷ ψ₁)
    load  : a ∈ Γ → Instr J ψ₁ (a ∷ ψ₁)
    store : a ∈ Γ → Instr J (a ∷ ψ₁) ψ₁
    ret   : Instr J (a ∷ ψ₁) ψ₂

  data Bytecode' (J : Typing) : Typing → StackTy → StackTy → Set where
    nil  : Bytecode' J [] ψ₁ ψ₁
    cons : ∀ {I} → Instr J ψ₁ ψ₂ → Bytecode' J I ψ₂ ψ₃ → Bytecode' J (ψ₁ ∷ I) ψ₁ ψ₃

  Bytecode : Typing → StackTy → StackTy → Set
  Bytecode J = Bytecode' J J

module _ where

  Addressing : Labels → Typing → Set
  Addressing lbs J = All (λ ψ → ψ ∈ J) lbs

  instr-tf : ∀ {Γ ℓs} → Addressing ℓs J → ⟨ Γ ∣ ψ₁ ↝ ψ₂ ⟩ ℓs → Instr Γ J ψ₁ ψ₂
  instr-tf ρ noop              = nop
  instr-tf ρ pop               = pop
  instr-tf ρ (push x)          = push x
  instr-tf ρ dup               = dup
  instr-tf ρ swap              = swap
  instr-tf ρ (bop x)           = bop x
  instr-tf ρ (load x)          = load x
  instr-tf ρ (store x)         = store x
  instr-tf (ℓ ∷ _) (goto refl) = goto ℓ
  instr-tf (ℓ ∷ _) (if x refl) = if x ℓ

  Extractor : ∀ Γ → StackTy → StackTy → Intf → Set
  Extractor Γ ψ₁ ψ₂ Φ = {J₁ : Typing} → Addressing (down Φ) J₁
                       → ∃ λ J₂ → Bytecode' Γ (J₁ ++ J₂) J₂ ψ₁ ψ₂ × Addressing (up Φ) (J₁ ++ J₂)

  exec-extractor : ∀ {Γ} → Extractor Γ ψ₁ ψ₂ ε → ∃ λ J → Bytecode Γ J ψ₁ ψ₂
  exec-extractor c = let _ , code , _ = c {[]} [] in -, code

  label-addresses : ∀ {x} → Labeling ψ₁ x → All (λ z → z ∈ J₁ ++ ψ₁ ∷ []) x
  label-addresses (refl ∙⟨ σ ⟩ qx) = joinAll (λ ()) σ (∈-++⁺ʳ _ (here refl) ∷ []) (addr' qx)
    where
      addr' : ∀ {x} → Bigstar (Own List.[ ψ₁ ]) x → All (λ z → z ∈ J₁ ++ ψ₁ ∷ []) x
      addr' emp = []
      addr' (cons (refl ∙⟨ σ ⟩ qx)) = joinAll (λ ()) σ (∈-++⁺ʳ _ (here refl) ∷ []) (addr' qx)

  -- We can extract bytecode that does absolute addressing from the fancy
  -- intrinsically-typed representation.
  -- We do this in a single recursive pass over the bytecode, collecting a global map of instruction typings,
  -- and also collecting indices into that map for every defined label on the forward pass, and
  -- eliminating labels on the backwards pass.
  --
  -- The interface compositions guide the way. The key lemma is `sinkᵣ`
  -- which says that in order to know what l imports in l ✴ r,
  -- it is sufficient to know what l ✴ r imports, *and* what r exports.
  --
  -- In this setting 'l' is the head of some suffix of bytecode.
  -- The imports of 'l ✴ r' have been collected from the labels defined in the prefix.
  -- We get the exports of the tail 'r' of the suffix from the recursive call.
  extract : ∀ {Γ} → ∀[ ⟪ Γ ∣ ψ₁ ↝ ψ₂ ⟫ ⇒ Extractor Γ ψ₁ ψ₂ ]
  extract {ψ₁ = ψ₁} nil ρ    = [] , nil , []

  extract {ψ₁ = ψ₁} (cons (labeled (↑ ls ∙⟨ σ₁ ⟩ ↓ i) ∙⟨ σ₂ ⟩ is)) ρ = let
      -- addressing from ↑ ls
      ρ₀ = label-addresses ls

      -- Addresses for the labels
      ρ₁ = source σ₁ ρ₀ []

      -- Compute addresses for the tail,
      -- by combining the addresses from the state with the addresses for the labels.
      -- We don't need everything, only what is imported in the head instruction.
      ρ₂ = sinkᵣ  σ₂ ρ₁ (All.map (∈-++⁺ˡ {ys = List.[ ψ₁ ]}) ρ)

      -- Recursively extract first to get addressing for forward jumps.
      -- These addresses are exported by the tail.
      k , code , ρ′ = extract is ρ₂

      -- Compute the addresses imported by i
      ρ₃ = sinkᵣ (∙-comm σ₂) ρ′ (All.map ∈-++⁺ˡ ρ)
      ρ₄ = sinkᵣ σ₁ (All.map ∈-++⁺ˡ ρ₀) ρ₃

      -- Compute the exported addresses
      ρ₅ = source σ₂ (All.map ∈-++⁺ˡ ρ₁) ρ′

    in ψ₁ ∷ k , cons (instr-tf ρ₄ i) code , ρ₅

  -- Same as above, but simpler
  extract {ψ₁ = ψ₁} (cons (instr   (↓ i) ∙⟨ σ ⟩ b)) ρ =  let
      ρ₂ = sinkᵣ σ [] (All.map (∈-++⁺ˡ {ys = List.[ ψ₁ ]}) ρ)
      k , code , ρ′ = extract b ρ₂
      ρ₃ = sinkᵣ (∙-comm σ) ρ′ (All.map ∈-++⁺ˡ ρ)
      ρ₄ = source σ [] ρ′
    in ψ₁ ∷ k , cons (instr-tf ρ₃ i) code , ρ₄

module Show where

  open import Data.String as S hiding (show)
  open import Data.Integer as I
  open import Data.Fin as Fin
  open import Data.Nat.Show as NS
  open import Data.Bool.Show as BS

  showInt : ℤ → String
  showInt (+ n) = NS.show n
  showInt (-[1+ n ]) = "-" S.++ NS.show (ℕ.suc n)

  showFin : ∀ {n} → Fin n → String
  showFin f = NS.show (Fin.toℕ f)

  showComp : Comparator as → String
  showComp eq = "eq"
  showComp ne = "ne"
  showComp lt = "lt"
  showComp ge = "ge"
  showComp gt = "gt"
  showComp le = "le"
  showComp icmpge = "icmpge"
  showComp icmpgt = "icmpgt"
  showComp icmpeq = "icmpeq"
  showComp icmpne = "icmpne"
  showComp icmplt = "icmplt"
  showComp icmple = "icmple"

  showOp : NativeBinOp a b c → String
  showOp add = "add"
  showOp sub = "sub"
  showOp mul = "mul"
  showOp div = "div"
  showOp xor = "xor"

  showConst : Const a → String
  showConst Const.null = "null"
  showConst (num x)    = showInt x
  showConst (bool x)   = BS.show x

  showReg : ∀ {Γ} → a ∈ Γ → String
  showReg e = showFin (index e)

  showLabel : ψ ∈ J → String
  showLabel = λ ℓ → showFin (index ℓ)

  showInstr : ∀ {Γ} → Instr Γ J ψ₁ ψ₂ → String
  showInstr (goto ℓ) = "goto " S.++ showLabel ℓ
  showInstr (if c ℓ) = "if " S.++ (showComp c S.++ " " S.++ showLabel ℓ)
  showInstr nop      = "noop"
  showInstr (push c) = "push " S.++ (showConst c)
  showInstr pop      = "pop"
  showInstr dup      = "dup"
  showInstr swap     = "swap"
  showInstr (bop o)  = "bop " S.++ (showOp o)
  showInstr (load r) = "load " S.++ (showReg r)
  showInstr (store r)= "store " S.++ (showReg r)
  showInstr ret      = "ret"

  showTy : Ty → String
  showTy boolean = "bool"
  showTy byte    = "byte"
  showTy short   = "short"
  showTy int     = "int"
  showTy long    = "long"
  showTy char    = "char"
  showTy (ref x) = "ref"
  showTy (array t) = "array"

  showStackTy : StackTy → String
  showStackTy []      = "[]"
  showStackTy (x ∷ ψ) = showTy x S.++ " : " S.++ showStackTy ψ

  showBytecode : ∀ {Γ J} → Bytecode Γ J ψ₁ ψ₂ → String
  showBytecode b = showBytecode' b 0
    where
      open import Data.Nat

      showBytecode' : ∀ {Γ J J'} → Bytecode' Γ J J' ψ₁ ψ₂ → ℕ → String
      showBytecode' nil n = ""
      showBytecode' (cons {ψ₁ = ψ₁} {ψ₂} i b) n =
        NS.show n S.++ ": "
          S.++ showInstr i
          S.++ "\t⟨ " S.++ showStackTy ψ₁ S.++ " ↝ " S.++ showStackTy ψ₂ S.++ " ⟩"
          S.++ "\n" S.++ showBytecode' b (ℕ.suc n)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Subsets of finite sets
------------------------------------------------------------------------

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

module Data.Fin.Subset where

open import Algebra
open import Algebra.FunctionProperties using (Op₁; Op₂)
import Algebra.Properties.BooleanAlgebra as BoolAlgProp
import Algebra.Properties.BooleanAlgebra.Expression as BAExpr
open import Data.Bool using (not; _∧_; _∨_; _≟_)
open import Data.Fin using (Fin; zero; suc)
open import Data.List.Base using (List; foldr; foldl)
open import Data.Nat using (ℕ)
open import Data.Product using (∃)
open import Data.Vec hiding (foldr; foldl)
import Data.Vec.Relation.Binary.Pointwise.Extensional as Pointwise
open import Relation.Nullary

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

-- Sides.

open import Data.Bool.Base public
  using () renaming (Bool to Side; true to inside; false to outside)

-- Partitions a finite set into two parts, the inside and the outside.

Subset : ℕ → Set
Subset = Vec Side

------------------------------------------------------------------------
-- Special subsets

-- The empty subset
⊥ : ∀ {n} → Subset n
⊥ = replicate outside

-- The full subset
⊤ : ∀ {n} → Subset n
⊤ = replicate inside

-- A singleton subset, containing just the given element.
⁅_⁆ : ∀ {n} → Fin n → Subset n
⁅ zero  ⁆ = inside  ∷ ⊥
⁅ suc i ⁆ = outside ∷ ⁅ i ⁆

------------------------------------------------------------------------
-- Membership and subset predicates

infix 4 _∈_ _∉_ _⊆_ _⊈_

_∈_ : ∀ {n} → Fin n → Subset n → Set
x ∈ p = p [ x ]= inside

_∉_ : ∀ {n} → Fin n → Subset n → Set
x ∉ p = ¬ (x ∈ p)

_⊆_ : ∀ {n} → Subset n → Subset n → Set
p ⊆ q = ∀ {x} → x ∈ p → x ∈ q

_⊈_ : ∀ {n} → Subset n → Subset n → Set
p ⊈ q = ¬ (p ⊆ q)

------------------------------------------------------------------------
-- Set operations

infixr 7 _∩_
infixr 6 _∪_

-- Complement
∁ : ∀ {n} → Op₁ (Subset n)
∁ p = map not p

-- Intersection
_∩_ : ∀ {n} → Op₂ (Subset n)
p ∩ q = zipWith _∧_ p q

-- Union
_∪_ : ∀ {n} → Op₂ (Subset n)
p ∪ q = zipWith _∨_ p q

-- N-ary union
⋃ : ∀ {n} → List (Subset n) → Subset n
⋃ = foldr _∪_ ⊥

-- N-ary intersection
⋂ : ∀ {n} → List (Subset n) → Subset n
⋂ = foldr _∩_ ⊤

-- Size
∣_∣ : ∀ {n} → Subset n → ℕ
∣ p ∣ = count (_≟ inside) p

------------------------------------------------------------------------
-- Properties

Nonempty : ∀ {n} (p : Subset n) → Set
Nonempty p = ∃ λ f → f ∈ p

Empty : ∀ {n} (p : Subset n) → Set
Empty p = ¬ Nonempty p

Lift : ∀ {n ℓ} → (Fin n → Set ℓ) → (Subset n → Set ℓ)
Lift P p = ∀ {x} → x ∈ p → P x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Operations on nullary relations (like negation and decidability)
------------------------------------------------------------------------

-- Some operations on/properties of nullary relations, i.e. sets.

module Relation.Nullary where

import Relation.Nullary.Core as Core

------------------------------------------------------------------------
-- Negation

open Core public using (¬_)

------------------------------------------------------------------------
-- Decidable relations

open Core public using (Dec; yes; no)


text:
module Issue2858-Fresh {A : Set} (_#_ : A → A → Set) where

  interleaved mutual

    data Fresh : Set
    data IsFresh (a : A) : Fresh → Set

    -- nil is a fresh list
    constructor
      []  : Fresh
      #[] : IsFresh a []

    -- cons is fresh as long as the new value is fresh
    constructor
      cons  : (x : A) (xs : Fresh) → IsFresh x xs → Fresh
      #cons : ∀ {x xs p} → a # x → IsFresh a xs → IsFresh a (cons x xs p)


text:
-- Andreas, 2017-11-01, issue #2824
-- Don't allow built-ins defined in parametrized modules

module _ (A : Set) where

  data Nat : Set where
    zero : Nat
    suc : Nat → Nat

  {-# BUILTIN NATURAL Nat #-}  -- Should fail

  test = 5

max_forks_repo_name: Agda-zh/agda


text:
module Issue231 where

postulate
  A : Set

data List : Set where
  _∷_ : A → List → List

data Any : List → Set where
  there : ∀ {x xs} → Any xs → Any (x ∷ xs)

postulate
  id : (A : Set) → A → A

lemma : (xs : List) → Set → (p : Any xs) → Set
lemma (x ∷ xs) A (there p) with id (Any xs) p
lemma (x ∷ xs) A (there p) | p′ = {!p′!}

-- Before case-split:
-- lemma (x ∷ xs) A (there p) | p′ = {!p′!}
-- After case-split:
-- lemma (A ∷ _) _ (there p) | there y = ?


text:
-- Andreas, 2016-11-02, issue #2289
-- Meta should be acceptable as sort of record type.

postulate
  F : Set → Set

mutual
  data ⊥ : _ where  -- works

  FBot = F ⊥

mutual
  record ⊤ : _ where  -- should work

  FTop = F ⊤


text:
{-# OPTIONS --without-K #-}
module Search.Searchable.Fun where

open import Type hiding (★)
open import Data.Product
open import Data.Sum
open import Data.One
open import Data.Bits
open import Function.NP
open import Search.Type
open import Search.Searchable
open import Search.Searchable.Product
open import Search.Searchable.Sum
import Function.Inverse.NP as FI
open FI using (_↔_; inverses; module Inverse) renaming (_$₁_ to to; _$₂_ to from)
open import Function.Related.TypeIsomorphisms.NP
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_; _≗_)

private -- unused
    SΠΣ⁻ : ∀ {m A} {B : A → ★ _} {C : Σ A B → ★ _}
           → Search m ((x : A) (y : B x) → C (x , y))
           → Search m (Π (Σ A B) C)
    SΠΣ⁻ s _∙_ f = s _∙_ (f ∘ uncurry)

    SΠΣ⁻-ind : ∀ {m p A} {B : A → ★ _} {C : Σ A B → ★ _}
               → {s : Search m ((x : A) (y : B x) → C (x , y))}
               → SearchInd p s
               → SearchInd p (SΠΣ⁻ s)
    SΠΣ⁻-ind ind P P∙ Pf = ind (P ∘ SΠΣ⁻) P∙ (Pf ∘ uncurry)

    S×⁻ : ∀ {m A B C} → Search m (A → B → C) → Search m (A × B → C)
    S×⁻ = SΠΣ⁻

    S×⁻-ind : ∀ {m p A B C}
              → {s : Search m (A → B → C)}
              → SearchInd p s
              → SearchInd p (S×⁻ s)
    S×⁻-ind = SΠΣ⁻-ind

    SΠ⊎⁻ : ∀ {m A B} {C : A ⊎ B → ★ _}
           → Search m (Π A (C ∘ inj₁) × Π B (C ∘ inj₂))
           → Search m (Π (A ⊎ B) C)
    SΠ⊎⁻ s _∙_ f = s _∙_ (f ∘ uncurry [_,_])

    SΠ⊎⁻-ind : ∀ {m p A B} {C : A ⊎ B → ★ _}
                 {s : Search m (Π A (C ∘ inj₁) × Π B (C ∘ inj₂))}
                 (i : SearchInd p s)
               → SearchInd p (SΠ⊎⁻ {C = C} s) -- A sB)
    SΠ⊎⁻-ind i P P∙ Pf = i (P ∘ SΠ⊎⁻) P∙ (Pf ∘ uncurry [_,_])

    {- For each A→C function
       and each B→C function
       an A⊎B→C function is yield
     -}
    S⊎⁻ : ∀ {m A B C} → Search m (A → C) → Search m (B → C)
                      → Search m (A ⊎ B → C)
    S⊎⁻ sA sB =  SΠ⊎⁻ (sA ×-search sB)

μΠΣ⁻ : ∀ {A B}{C : Σ A B → ★₀} → Searchable ((x : A)(y : B x) → C (x , y)) → Searchable (Π (Σ A B) C)
μΠΣ⁻ = μ-iso (FI.sym curried)

Σ-Fun : ∀ {A B} → Funable A → Funable B → Funable (A × B)
Σ-Fun (μA , μA→) FB  = μΣ μA (searchable FB) , (λ x → μΠΣ⁻ (μA→ (negative FB x)))
  where open Funable

{-
μΠ⊎⁻ : ∀ {A B : ★₀}{C : A ⊎ B → ★ _} → Searchable (Π A (C ∘ inj₁) × Π B (C ∘ inj₂))
     → Searchable (Π (A ⊎ B) C)
μΠ⊎⁻ = μ-iso ?

_⊎-Fun_ : ∀ {A B : ★₀} → Funable A → Funable B → Funable (A ⊎ B)
_⊎-Fun_ (μA , μA→) (μB , μB→) = (μA ⊎-μ μB) , (λ X → μΠ⊎⁻ (μA→ X ×-μ μB→ X))
-}

S𝟙 : ∀ {m A} → Search m A → Search m (𝟙 → A)
S𝟙 sA _∙_ f = sA _∙_ (f ∘ const)

SΠBit : ∀ {m A} → Search m (A 0b) → Search m (A 1b)
                → Search m (Π Bit A)
SΠBit sA₀ sA₁ _∙_ f = sA₀ _∙_ λ x → sA₁ _∙_ λ y → f λ {true → y; false → x}

×-Dist : ∀ {A B} FA FB → DistFunable {A} FA → DistFunable {B} FB → DistFunable (Σ-Fun FA FB)
×-Dist FA FB FA-dist FB-dist μX c _⊙_ distrib _⊙-cong_ f
  = Πᴬ (λ x → Πᴮ (λ y → Σ' (f (x , y))))
  ≈⟨ ⟦search⟧ (searchable FA){_≡_} ≡.refl _≈_ (λ x y → x ⊙-cong y)
       (λ { {x} {.x} ≡.refl → FB-dist μX c _⊙_ distrib _⊙-cong_ (curry f x)}) ⟩
    Πᴬ (λ x → Σᴮ (λ fb → Πᴮ (λ y → f (x , y) (fb y))))
  ≈⟨ FA-dist (negative FB μX) c _⊙_ distrib _⊙-cong_
       (λ x fb → search (searchable FB) _⊙_ (λ y → f (x , y) (fb y))) ⟩
    Σᴬᴮ (λ fab → Πᴬ (λ x → Πᴮ (λ y → f (x , y) (fab x y))))
  ∎
  where
    open CMon c
    open Funable

    Σ' = search μX _∙_

    Πᴬ = search (searchable FA) _⊙_
    Πᴮ = search (searchable FB) _⊙_

    Σᴬᴮ = search (negative FA (negative FB μX)) _∙_
    Σᴮ  = search (negative FB μX) _∙_

    {-
⊎-Dist : ∀ {A B : ★₀} FA FB → DistFunable {A} FA → DistFunable {B} FB → DistFunable (FA ⊎-Fun FB)
⊎-Dist FA FB FA-dist FB-dist μX c _◎_ distrib _◎-cong_ f
 = Πᴬ (Σ' ∘ f ∘ inj₁) ◎ Πᴮ (Σ' ∘ f ∘ inj₂)
 ≈⟨ {!FA-dist μX c _◎_ distrib _◎-cong_ (f ∘ inj₁) ◎-cong FB-dist μX c _◎_ distrib _◎-cong_ (f ∘ inj₂)!} ⟩
 {-
   Σᴬ (λ fa → Πᴬ (λ i → f (inj₁ i) (fa i))) ◎ Σᴮ (λ fb → Πᴮ (λ i → f (inj₂ i) (fb i)))
 ≈⟨ sym (search-linʳ (negative FA μX) monoid _◎_ _ _ (proj₂ distrib)) ⟩
   Σᴬ (λ fa → Πᴬ (λ i → f (inj₁ i) (fa i)) ◎ Σᴮ (λ fb → Πᴮ (λ i → f (inj₂ i) (fb i))))
 ≈⟨ search-sg-ext (negative FA μX) semigroup (λ fa → sym (search-linˡ (negative FB μX) monoid _◎_ _ _ (proj₁ distrib))) ⟩
 -}
   (Σᴬ λ fa → Σᴮ λ fb → Πᴬ ((f ∘ inj₁) ˢ fa) ◎ Πᴮ ((f ∘ inj₂) ˢ fb))
 ∎
 where
    open CMon c
    open Funable

    Σ' = search μX _∙_

    Πᴬ = search (searchable FA) _◎_
    Πᴮ = search (searchable FB) _◎_

    Σᴬ = search (negative FA μX) _∙_
    Σᴮ = search (negative FB μX) _∙_
-}

-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.DecSetoid directly.
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.Vec.Relation.Equality.DecSetoid
  {a ℓ} (DS : DecSetoid a ℓ) where

open import Data.Vec.Relation.Binary.Equality.DecSetoid public


text:
module Human.JS where

open import Human.Unit
open import Human.String
open import Human.IO

infixl 1 _>>=_

postulate
  return : ∀ {a} {A : Set a} → A → IO A
  _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
  _>>_   : ∀ {a b} {A : Set a} {B : Set b} → IO A → IO B → IO B
  print  : String → IO Unit

{-# COMPILE JS return = a => b => c => c #-}
{-# COMPILE JS _>>=_  = a => b => c => d => f => x => f(x) #-}
{-# COMPILE JS _>>_   = a => b => c => d => f => x => x #-}
{-# COMPILE JS print  = s => console.log(s) #-}

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
----------------------------------------------------------------------------------
-- Types for parse trees
----------------------------------------------------------------------------------

module cedille-types where

open import lib
-- open import parse-tree
open import general-util

{-# FOREIGN GHC import qualified CedilleTypes #-}

mutual
  posinfo = string
  var = string
  num = string
  erased? = 𝔹
  minus? = 𝔹
  imports = 𝕃 imprt
  ex-imports = 𝕃 ex-imprt
  params = 𝕃 param
  ex-params = 𝕃 ex-param
  ex-cmds = 𝕃 ex-cmd
  ex-ctrs = 𝕃 ex-ctr
  ctrs = 𝕃 ctr
  args = 𝕃 arg
  ex-args = 𝕃 ex-arg
  opacity = 𝔹
  cases = 𝕃 case
  ex-cases = 𝕃 ex-case
  left-right = maybe 𝔹
  rho-hnf = 𝔹
  opt-public = 𝔹
  is-mu = maybe term ⊎ var
  iota-num = 𝔹
  case-args = 𝕃 case-arg
  tmtp = term ⊎ type
  tpkd = type ⊎ kind
  arg = term ⊎ tmtp

  pattern Tkt T = inj₁ T
  pattern Tkk k = inj₂ k
  pattern Ttm t = inj₁ t
  pattern Ttp T = inj₂ T
  pattern Arg t = inj₁ t
  pattern ArgE tT = inj₂ tT
  pattern ArgTp T = ArgE (Ttp T)
  pattern ArgEr t = ArgE (Ttm t)
  pattern ι1 = ff
  pattern ι2 = tt
  pattern NotErased = ff
  pattern Erased = tt
  pattern opacity-open = tt
  pattern opacity-closed = ff
  pattern EpsHanf = tt
  pattern EpsHnf = ff
  pattern EpsLeft = just ff
  pattern EpsRight = just tt
  pattern EpsBoth = nothing
  pattern Public = tt
  pattern Private = ff

  ctr = var × type
  pattern Ctr x T = x , T

  data param : Set where
    Param : erased? → var → tpkd → param
  pattern ParamTp x k = Param _  x (Tkk k)
  pattern ParamTm x T = Param ff x (Tkt T)
  pattern ParamEr x T = Param tt x (Tkt T)

  data term : Set where
    App : term → term → term
    AppE : term → tmtp → term
    Beta : term → term → term
    Delta : (do-bohm? : maybe (term × term)) → (Tᵣ : type) → (contra : term) → term
    Hole : posinfo → term
    IotaPair : term → term → var → type → term
    IotaProj : term → iota-num → term
    Lam : erased? → var → maybe tpkd → term → term
    LetTm : erased? → var → maybe type → term → term → term
    LetTp : var → kind → type → term → term
    Phi : term → term → term → term
    Rho : term → var → type → term → term
    Sigma : term → term
    Mu : is-mu → term → maybe type → datatype-info → cases → term
    Var : var → term
  pattern AppTp t T = AppE t (Ttp T)
  pattern AppEr t t' = AppE t (Ttm t')

  data case : Set where
    Case : var → case-args → term → 𝕃 tmtp → case

  data type : Set where
    TpAbs : erased? → var → tpkd → type → type
    TpIota : var → type → type → type
    TpApp : type → tmtp → type
    TpEq : term → term → type
    TpHole : posinfo → type
    TpLam : var → tpkd → type → type
    TpVar : var → type
  pattern TpAppTp T T' = TpApp T (Ttp T')
  pattern TpAppTm T t = TpApp T (Ttm t)

  data kind : Set where
    KdStar : kind
    KdHole : posinfo → kind
    KdAbs : var → tpkd → kind → kind

  data case-arg : Set where
    CaseArg : erased? → var → maybe tpkd → case-arg

  data ex-file : Set where
    ExModule : ex-imports → posinfo → posinfo → var → ex-params → ex-cmds → posinfo → ex-file

  cmds = 𝕃 cmd

  data file : Set where
    Module : var → params → cmds → file

  indx : Set
  indx = var × tpkd
  pattern Index x tk = x , tk
  indices = 𝕃 indx

  record encoding-defs : Set where
    constructor mk-enc-defs
    inductive
    field
      ecs : cmds -- encoding
      gcs : cmds -- generated
      Cast : type
      cast-in : term
      cast-out : term
      cast-is : term
      Functor : type
      functor-in : term
      functor-out : term
      Fix : type
      fix-in : term
      fix-out : term
      lambek1 : term
      lambek2 : term
      fix-ind : term

  record encoded-defs : Set where
    constructor mk-encd-defs
    field
      Is/D : var
      is/D : var
      to/D : var
      TypeF/D : var
      IndF/D : var
      fmap/D :  var

  record datatype-info : Set where
    constructor mk-data-info
    inductive
    field
      name : var
      original : var
      asₚ : args
      asᵢ : 𝕃 tmtp
      ps : params
      kᵢ : kind
      k : kind
      cs : ctrs
      csₚₛ : ctrs
      eds : encoding-defs
      gds : encoded-defs

  data cmd : Set where
    CmdDefTerm : var → term → cmd
    CmdDefType : var → kind → type → cmd
    CmdDefKind : var → params → kind → cmd
    CmdDefData : encoding-defs → var → params → kind → ctrs → cmd
    CmdImport : imprt → cmd

  data imprt : Set where
    Import : opt-public → filepath → var → maybe var → args → imprt

  data ex-cmd : Set where
    ExCmdKind : posinfo → var → ex-params → ex-kd → posinfo → ex-cmd
    ExCmdDef : opacity → ex-def → posinfo → ex-cmd
    ExCmdData : def-datatype → posinfo → ex-cmd
    ExCmdImport : ex-imprt → ex-cmd

  data def-datatype : Set where
    DefDatatype : posinfo → posinfo → var → ex-params → ex-kd → ex-ctrs → def-datatype

  data import-as : Set where
    ImportAs : posinfo → var → import-as

  data ex-imprt : Set where
    ExImport : posinfo → opt-public → posinfo → filepath → maybe import-as → ex-args → posinfo → ex-imprt

  data ex-param : Set where
    ExParam : posinfo → erased? → posinfo → var → ex-tk → posinfo → ex-param

  data ex-ctr : Set where
    ExCtr : posinfo → var → ex-tp → ex-ctr

  data ex-arg : Set where
    ExTmArg : erased? → ex-tm → ex-arg
    ExTpArg : ex-tp → ex-arg

  data lterm : Set where
    Lterm : erased? → ex-tm → lterm

  data theta : Set where
    Abstract : theta
    AbstractEq : theta
    AbstractVars : 𝕃 var → theta

  data ex-def : Set where
    ExDefTerm : posinfo → var → maybe ex-tp → ex-tm → ex-def
    ExDefType : posinfo → var → ex-kd → ex-tp → ex-def

  data ex-guide : Set where
    ExGuide : posinfo → var → ex-tp → ex-guide

  data ex-case : Set where
    ExCase : posinfo → var → ex-case-args → ex-tm → ex-case

  ex-case-args = 𝕃 ex-case-arg

  data ex-case-arg-sym : Set where
    ExCaseArgTm : ex-case-arg-sym
    ExCaseArgEr : ex-case-arg-sym
    ExCaseArgTp : ex-case-arg-sym

  data ex-case-arg : Set where
    ExCaseArg : ex-case-arg-sym → posinfo → var → ex-case-arg

  data ex-tk : Set where
    ExTkt : ex-tp → ex-tk
    ExTkk : ex-kd → ex-tk

  data ex-tp : Set where
    ExTpAbs : posinfo → erased? → posinfo → var → ex-tk → ex-tp → ex-tp
    ExTpIota : posinfo → posinfo → var → ex-tp → ex-tp → ex-tp
    ExTpNoSpans : ex-tp → posinfo → ex-tp
    ExTpLet : posinfo → ex-def → ex-tp → ex-tp
    ExTpApp : ex-tp → ex-tp → ex-tp
    ExTpAppt : ex-tp → ex-tm → ex-tp
    ExTpArrow : ex-tp → erased? → ex-tp → ex-tp
    ExTpEq : posinfo → ex-tm → ex-tm → posinfo → ex-tp
    ExTpHole : posinfo → ex-tp
    ExTpLam : posinfo → posinfo → var → ex-tk → ex-tp → ex-tp
    ExTpParens : posinfo → ex-tp → posinfo → ex-tp
    ExTpVar : posinfo → var → ex-tp

  data pos-tm : Set where
    PosTm : ex-tm → posinfo → pos-tm

  data ex-is-mu : Set where
    ExIsMu : posinfo → var → ex-is-mu
    ExIsMu' : maybe ex-tm → ex-is-mu

  data ex-tm : Set where
    ExApp : ex-tm → erased? → ex-tm → ex-tm
    ExAppTp : ex-tm → ex-tp → ex-tm
    ExBeta : posinfo → maybe pos-tm → maybe pos-tm → ex-tm
    ExChi : posinfo → maybe ex-tp → ex-tm → ex-tm
    ExDelta : posinfo → maybe ex-tp → ex-tm → ex-tm
    ExEpsilon : posinfo → left-right → minus? → ex-tm → ex-tm
    ExHole : posinfo → ex-tm
    ExIotaPair : posinfo → ex-tm → ex-tm → maybe ex-guide → posinfo → ex-tm
    ExIotaProj : ex-tm → num → posinfo → ex-tm
    ExLam : posinfo → erased? → posinfo → var → maybe ex-tk → ex-tm → ex-tm
    ExLet : posinfo → erased? → ex-def → ex-tm → ex-tm
    ExOpen : posinfo → opacity → posinfo → var → ex-tm → ex-tm
    ExParens : posinfo → ex-tm → posinfo → ex-tm
    ExPhi : posinfo → ex-tm → ex-tm → ex-tm → posinfo → ex-tm
    ExRho : posinfo → rho-hnf → maybe (𝕃 num) → ex-tm → maybe ex-guide → ex-tm → ex-tm
    ExSigma : posinfo → ex-tm → ex-tm
    ExTheta : posinfo → theta → ex-tm → 𝕃 lterm → ex-tm
    ExMu : posinfo → ex-is-mu → ex-tm → maybe ex-tp → posinfo → ex-cases → posinfo → ex-tm
    ExVar : posinfo → var → ex-tm

  data ex-kd : Set where
    ExKdAbs : posinfo → posinfo → var → ex-tk → ex-kd → ex-kd
    ExKdArrow : ex-tk → ex-kd → ex-kd
    ExKdHole : posinfo → ex-kd
    ExKdParens : posinfo → ex-kd → posinfo → ex-kd
    ExKdStar : posinfo → ex-kd
    ExKdVar : posinfo → var → ex-args → ex-kd

{-# COMPILE GHC ex-param = data CedilleTypes.Param (CedilleTypes.Param) #-}
{-# COMPILE GHC ex-file = data CedilleTypes.File (CedilleTypes.Module) #-}
{-# COMPILE GHC ex-cmd = data CedilleTypes.Cmd (CedilleTypes.CmdKind | CedilleTypes.CmdDef | CedilleTypes.CmdData | CedilleTypes.CmdImport) #-}
{-# COMPILE GHC ex-ctr = data CedilleTypes.Ctr (CedilleTypes.Ctr) #-}
{-# COMPILE GHC ex-arg = data CedilleTypes.Arg (CedilleTypes.TermArg | CedilleTypes.TypeArg) #-}
{-# COMPILE GHC def-datatype = data CedilleTypes.DefDatatype (CedilleTypes.DefDatatype) #-}
{-# COMPILE GHC import-as = data CedilleTypes.ImportAs (CedilleTypes.ImportAs) #-}
{-# COMPILE GHC ex-imprt = data CedilleTypes.Imprt (CedilleTypes.Import) #-}
{-# COMPILE GHC ex-case-arg-sym = data CedilleTypes.CaseArgSym (CedilleTypes.CaseArgTm | CedilleTypes.CaseArgEr | CedilleTypes.CaseArgTp) #-}
--{-# COMPILE GHC case-arg = data CedilleTypes.CaseArg (CedilleTypes.CaseArg) #-}
{-# COMPILE GHC lterm = data CedilleTypes.Lterm (CedilleTypes.Lterm) #-}
{-# COMPILE GHC theta = data CedilleTypes.Theta (CedilleTypes.Abstract | CedilleTypes.AbstractEq | CedilleTypes.AbstractVars) #-}
{-# COMPILE GHC ex-def = data CedilleTypes.Def (CedilleTypes.DefTerm | CedilleTypes.DefType) #-}
{-# COMPILE GHC ex-guide = data CedilleTypes.Guide (CedilleTypes.Guide) #-}
{-# COMPILE GHC ex-case = data CedilleTypes.Case (CedilleTypes.Case) #-}
{-# COMPILE GHC ex-case-arg = data CedilleTypes.CaseArg (CedilleTypes.CaseArg) #-}
{-# COMPILE GHC ex-tk = data CedilleTypes.TpKd (CedilleTypes.Tkt | CedilleTypes.Tkk) #-}
{-# COMPILE GHC ex-tp = data CedilleTypes.Type (CedilleTypes.TpAbs | CedilleTypes.TpIota | CedilleTypes.TpNoSpans | CedilleTypes.TpLet | CedilleTypes.TpApp | CedilleTypes.TpAppt | CedilleTypes.TpArrow | CedilleTypes.TpEq | CedilleTypes.TpHole | CedilleTypes.TpLam | CedilleTypes.TpParens | CedilleTypes.TpVar) #-}
{-# COMPILE GHC pos-tm = data CedilleTypes.PosTerm (CedilleTypes.PosTerm) #-}
{-# COMPILE GHC ex-is-mu = data CedilleTypes.IsMu (CedilleTypes.IsMu | CedilleTypes.IsMu') #-}
{-# COMPILE GHC ex-tm = data CedilleTypes.Term (CedilleTypes.App | CedilleTypes.AppTp | CedilleTypes.Beta | CedilleTypes.Chi | CedilleTypes.Delta | CedilleTypes.Epsilon | CedilleTypes.Hole | CedilleTypes.IotaPair | CedilleTypes.IotaProj | CedilleTypes.Lam | CedilleTypes.Let | CedilleTypes.Open | CedilleTypes.Parens | CedilleTypes.Phi | CedilleTypes.Rho | CedilleTypes.Sigma | CedilleTypes.Theta | CedilleTypes.Mu | CedilleTypes.Var) #-}
{-# COMPILE GHC ex-kd = data CedilleTypes.Kind (CedilleTypes.KdAbs | CedilleTypes.KdArrow | CedilleTypes.KdHole | CedilleTypes.KdParens | CedilleTypes.KdStar | CedilleTypes.KdVar) #-}

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of relations over Vector
------------------------------------------------------------------------

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

module Data.Vec.Functional.Relation.Binary.Pointwise where

open import Data.Fin.Base
open import Data.Nat.Base
open import Data.Vec.Functional as VF hiding (map)
open import Level using (Level)
open import Relation.Binary

private
  variable
    a b r s ℓ : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Definition

Pointwise : REL A B ℓ → ∀ {n} → Vector A n → Vector B n → Set ℓ
Pointwise R xs ys = ∀ i → R (xs i) (ys i)

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

module _ {R : REL A B r} {S : REL A B s} where

  map : R ⇒ S → ∀ {n} → Pointwise R ⇒ Pointwise S {n = n}
  map f rs i = f (rs i)


text:
module Zipper where

  import Derivative
  import Functor
  import Sets

  open Functor
  open Derivative
  open Semantics
  open Recursive
  open Sets

  Zipper : U -> Set
  Zipper F = List (⟦ ∂ F ⟧ (μ F))

  -- Plugging a zipper
  unzip : {F : U} -> Zipper F -> μ F -> μ F
  unzip	    []	     t = t
  unzip {F} (c :: γ) t = inn (plug-∂ F c (unzip γ t))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Data.Product using ( _×_ ; _,_ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind )
open import Web.Semantic.DL.ABox.Skolemization using ( askolem ; askolem-sound )
open import Web.Semantic.DL.FOL using  ( Formula ;  _∧_ )
open import Web.Semantic.DL.FOL.Model using ( _⊨f_ )
open import Web.Semantic.DL.KB using ( KB ; tbox ; abox )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Skolemization using ( TSkolems ; tskolem ; tskolem-sound )

module Web.Semantic.DL.KB.Skolemization {Σ : Signature} {X : Set} where

Skolems : Set → KB Σ X → Set
Skolems Δ K = TSkolems Δ (tbox K)

skolem : ∀ {Δ} → (X → Δ) → ∀ K → (Skolems Δ K) → Formula Σ Δ
skolem i K Φ = tskolem (tbox K) Φ ∧ askolem i (abox K)

skolem-sound : ∀ I K Φ → (⌊ I ⌋ ⊨f skolem (ind I) K Φ) → (I ⊨ K)
skolem-sound I K Φ (I⊨T , I⊨A) = (tskolem-sound ⌊ I ⌋ (tbox K) Φ I⊨T , askolem-sound I (abox K) I⊨A)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module Issue643 where

module M₁ (A : Set) where

  record R : Set₁ where
    field
      P : A → Set

module M₂ (A : Set) where

  open M₁ A

  postulate
    r : R
    T : R → Set

  open R r

  p : ∀ x → P x
  p x = {!!}     -- The goal was printed as "P" rather than "P x".

  q : T r
  q = {!!}       -- This goal was printed as T P at an intermediate stage of fixing


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.Char renaming (primCharEquality to _==ᶜ_)
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.String renaming (primStringAppend to _++_)
open import Agda.Builtin.IO
open import Agda.Builtin.Unit

variable
  A B C : Set

map : (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

<?> = '\xFFFD'

fromCount : Nat → Nat → List Nat
fromCount 0 _ = []
fromCount (suc n) a = a ∷ fromCount n (suc a)

fromTo : Nat → Nat → List Nat
fromTo a b = fromCount (suc b - a) a

isReplaced : Nat → Bool
isReplaced n = primNatToChar n ==ᶜ <?>

and : List Bool → Bool
and []           = true
and (false ∷ _)  = false
and (true  ∷ xs) = and xs

all : (A → Bool) → List A → Bool
all p xs = and (map p xs)

not : Bool → Bool
not false = true
not true  = false

_∘_ : (B → C) → (A → B) → A → C
f ∘ g = λ x → f (g x)

postulate
  putStrLn : String → IO ⊤
  _>>_ : IO A → IO B → IO B

{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}
{-# COMPILE GHC putStrLn = Text.putStrLn #-}
{-# COMPILE GHC _>>_ = \ _ _ -> (>>) #-}

assert : String → Bool → IO ⊤
assert s true  = putStrLn (s ++ " PASSED")
assert s false = putStrLn (s ++ " FAILED")

main : IO ⊤
main = do
  assert "before surrogates" (all (not ∘ isReplaced) (fromTo 0xD780 0xD7FF))
  assert "surrogate range  " (all isReplaced (fromTo 0xD800 0xDFFF))
  assert "after surrogates " (all (not ∘ isReplaced) (fromTo 0xE000 0xE07F))

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

open import lib.Basics
open import lib.types.Sigma

open import Preliminaries
open import Truncation_Level_Criteria
open import Anonymous_Existence_CollSplit

open wtrunc
open with-weak-trunc

module Anonymous_Existence_Populatedness where

-- Definition 4.2.1
⟪_⟫ : ∀ {i} → Type i → Type i
⟪ X ⟫ = (f : X → X) → const f → fix f

-- Proposition 4.2.2
Trunc→Pop : ∀ {i} {X : Type i} → ∣∣ X ∣∣ → ⟪ X ⟫
Trunc→Pop z f c = tr-rec {P = fix f} (fixed-point f c) (to-fix f c) z

-- Corollary 4.2.3: We show pairwise logical equivalence as it is easy
-- (of course, some directions are redundant)
coll-characterizations : ∀ {i} {X : Type i}
  → (coll X ↔ splitSup X)
   × ((coll X ↔ (⟪ X ⟫ → X))
   × ((⟪ X ⟫ → X) ↔ splitSup X))
coll-characterizations {X = X} = coll↔splitSup ,
                                 (coll→pop→X , reverse₁) ,
                                 (pop→X→splitSup , reverse₂) where

  coll→pop→X : coll X → ⟪ X ⟫ → X
  coll→pop→X (f , c) pop = fst (pop f c)

  pop→X→splitSup : (⟪ X ⟫ → X) → splitSup X
  pop→X→splitSup g = g ∘ Trunc→Pop

  reverse₁ = snd coll↔splitSup ∘ pop→X→splitSup
  reverse₂ = coll→pop→X ∘ snd coll↔splitSup

-- Addendum of Corollary 4.2.3
prop-pop : ∀ {i} {P : Type i} → is-prop P → ⟪ P ⟫ → P
prop-pop {P = P} pp = snd (snd (snd coll-characterizations)) (tr-rec pp (idf _))

-- Lemma 4.2.4
module _ {i : ULevel} {X : Type i} where

  pop→splitSup→X : ⟪ X ⟫ → splitSup X → X
  pop→splitSup→X pop = λ hst → snd (snd (snd (coll-characterizations {X = X}))) hst pop

  use-funct : (splitSup X → X) → ∣∣ splitSup X ∣∣ → ∣∣ X ∣∣
  use-funct f = trunc-functorial f

  tr-hst-X→pop : (∣∣ splitSup X ∣∣ → ∣∣ X ∣∣) → ⟪ X ⟫
  tr-hst-X→pop g f c = tr-rec (fixed-point f c) (to-fix f c) (g ∣ coll→splitSup (f , c) ∣)

  -- we formulate the two logical equivalence that we will need explicitly:
  pop-alt : ⟪ X ⟫ ↔ (∣∣ splitSup X ∣∣ → ∣∣ X ∣∣)
  pop-alt = use-funct ∘ pop→splitSup→X , tr-hst-X→pop

  pop-alt' : ⟪ X ⟫ ↔ (splitSup X → X)
  pop-alt' = pop→splitSup→X , tr-hst-X→pop ∘ use-funct

-- Proposition 4.2.5
pop-alt₂ : ∀ {i} {X : Type i} → ⟪ X ⟫ ↔ ((P : Type i) → (is-prop P) → (X ↔ P) → P)
pop-alt₂ {i} {X} = one , two where

  one : ⟪ X ⟫ → (P : Type i) → is-prop P → (X ↔ P) → P
  one pop P pp (xp , px) = xp (fst (pop f c)) where
    f : X → X
    f = px ∘ xp
    c : const f
    c x₁ x₂ = ap px (prop-has-all-paths pp _ _)

  two : ((P : Type i) → is-prop P → (X ↔ P) → P) → ⟪ X ⟫
  two rest f c = rest (fix f) (fixed-point f c) (to-fix f c , from-fix f)

-- Proposition 4.2.6, part 1
pop-property₁ : ∀ {i} {X : Type i} → X → ⟪ X ⟫
pop-property₁ = Trunc→Pop ∘ ∣_∣

-- Proposition 4.2.6, part 2: this needs function extensionality.
-- We import the library file with the consequence of funext that we need.
open import lib.types.Pi
pop-property₂ : ∀ {i} {X : Type i} → is-prop ⟪ X ⟫
pop-property₂ = Π-is-prop (λ f → Π-is-prop (λ c → fixed-point f c))

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Cowriter type and some operations
------------------------------------------------------------------------

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

-- Disabled to prevent warnings from BoundedVec
{-# OPTIONS --warn=noUserWarning #-}

module Codata.Cowriter where

open import Size
open import Level as L using (Level)
open import Codata.Thunk using (Thunk; force)
open import Codata.Conat
open import Codata.Delay using (Delay; later; now)
open import Codata.Stream as Stream using (Stream; _∷_)
open import Data.Unit
open import Data.List.Base using (List; []; _∷_)
open import Data.List.NonEmpty using (List⁺; _∷_)
open import Data.Nat.Base as Nat using (ℕ; zero; suc)
open import Data.Product as Prod using (_×_; _,_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Data.Vec.Base using (Vec; []; _∷_)
open import Data.Vec.Bounded as Vec≤ using (Vec≤; _,_)
open import Function

private
  variable
    a b w x : Level
    A : Set a
    B : Set b
    W : Set w
    X : Set x

------------------------------------------------------------------------
-- Definition

data Cowriter (W : Set w) (A : Set a) (i : Size) : Set (a L.⊔ w) where
  [_] : A → Cowriter W A i
  _∷_ : W → Thunk (Cowriter W A) i → Cowriter W A i

------------------------------------------------------------------------
-- Relationship to Delay.

fromDelay : ∀ {i} → Delay A i → Cowriter ⊤ A i
fromDelay (now a)    = [ a ]
fromDelay (later da) = _ ∷ λ where .force → fromDelay (da .force)

toDelay : ∀ {i} → Cowriter W A i → Delay A i
toDelay [ a ]    = now a
toDelay (_ ∷ ca) = later λ where .force → toDelay (ca .force)

------------------------------------------------------------------------
-- Basic functions.

fromStream : ∀ {i} → Stream W i → Cowriter W A i
fromStream (w ∷ ws) = w ∷ λ where .force → fromStream (ws .force)

repeat : W → Cowriter W A ∞
repeat = fromStream ∘′ Stream.repeat

length : ∀ {i} → Cowriter W A i → Conat i
length [ _ ]    = zero
length (w ∷ cw) = suc λ where .force → length (cw .force)

splitAt : ∀ (n : ℕ) → Cowriter W A ∞ → (Vec W n × Cowriter W A ∞) ⊎ (Vec≤ W n × A)
splitAt zero    cw       = inj₁ ([] , cw)
splitAt (suc n) [ a ]    = inj₂ (Vec≤.[] , a)
splitAt (suc n) (w ∷ cw) = Sum.map (Prod.map₁ (w ∷_)) (Prod.map₁ (w Vec≤.∷_))
                         $ splitAt n (cw .force)

take : ∀ (n : ℕ) → Cowriter W A ∞ → Vec W n ⊎ (Vec≤ W n × A)
take n = Sum.map₁ Prod.proj₁ ∘′ splitAt n

infixr 5 _++_ _⁺++_
_++_ : ∀ {i} → List W → Cowriter W A i → Cowriter W A i
[]       ++ ca = ca
(w ∷ ws) ++ ca = w ∷ λ where .force → ws ++ ca

_⁺++_ : ∀ {i} → List⁺ W → Thunk (Cowriter W A) i → Cowriter W A i
(w ∷ ws) ⁺++ ca = w ∷ λ where .force → ws ++ ca .force

concat : ∀ {i} → Cowriter (List⁺ W) A i → Cowriter W A i
concat [ a ]    = [ a ]
concat (w ∷ ca) = w ⁺++ λ where .force → concat (ca .force)

------------------------------------------------------------------------
-- Functor, Applicative and Monad

map : ∀ {i} → (W → X) → (A → B) → Cowriter W A i → Cowriter X B i
map f g [ a ]    = [ g a ]
map f g (w ∷ cw) = f w ∷ λ where .force → map f g (cw .force)

map₁ : ∀ {i} → (W → X) → Cowriter W A i → Cowriter X A i
map₁ f = map f id

map₂ : ∀ {i} → (A → X) → Cowriter W A i → Cowriter W X i
map₂ = map id

ap : ∀ {i} → Cowriter W (A → X) i → Cowriter W A i → Cowriter W X i
ap [ f ]    ca = map₂ f ca
ap (w ∷ cf) ca = w ∷ λ where .force → ap (cf .force) ca

_>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W X i) → Cowriter W X i
[ a ]    >>= f = f a
(w ∷ ca) >>= f = w ∷ λ where .force → ca .force >>= f

------------------------------------------------------------------------
-- Construction.

unfold : ∀ {i} → (X → (W × X) ⊎ A) → X → Cowriter W A i
unfold next seed with next seed
... | inj₁ (w , seed') = w ∷ λ where .force → unfold next seed'
... | inj₂ a           = [ a ]

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.3

open import Data.BoundedVec as BVec using (BoundedVec)

splitAt′ : ∀ (n : ℕ) → Cowriter W A ∞ → (Vec W n × Cowriter W A ∞) ⊎ (BoundedVec W n × A)
splitAt′ zero    cw       = inj₁ ([] , cw)
splitAt′ (suc n) [ a ]    = inj₂ (BVec.[] , a)
splitAt′ (suc n) (w ∷ cw) = Sum.map (Prod.map₁ (w ∷_)) (Prod.map₁ (w BVec.∷_))
                         $ splitAt′ n (cw .force)
{-# WARNING_ON_USAGE splitAt′
"Warning: splitAt′ (and Data.BoundedVec) was deprecated in v1.3.
Please use splitAt (and Data.Vec.Bounded) instead."
#-}

take′ : ∀ (n : ℕ) → Cowriter W A ∞ → Vec W n ⊎ (BoundedVec W n × A)
take′ n = Sum.map₁ Prod.proj₁ ∘′ splitAt′ n
{-# WARNING_ON_USAGE take′
"Warning: take′ (and Data.BoundedVec) was deprecated in v1.3.
Please use take (and Data.Vec.Bounded) instead."
#-}


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Change evaluation (Def 3.6 and Fig. 4h).
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Denotation.Value as Value
import Parametric.Denotation.Evaluation as Evaluation
import Parametric.Change.Validity as Validity

module Parametric.Change.Specification
    {Base : Type.Structure}
    (Const : Term.Structure Base)
    (⟦_⟧Base : Value.Structure Base)
    (⟦_⟧Const : Evaluation.Structure Const ⟦_⟧Base)
    {{validity-structure : Validity.Structure ⟦_⟧Base}}
  where

open Type.Structure Base
open Term.Structure Base Const
open Value.Structure Base ⟦_⟧Base
open Evaluation.Structure Const ⟦_⟧Base ⟦_⟧Const
open Validity.Structure ⟦_⟧Base {{validity-structure}}

open import Base.Denotation.Notation
open import Relation.Binary.PropositionalEquality
open import Theorem.CongApp
open import Postulate.Extensionality

module Structure where
  ---------------
  -- Interface --
  ---------------

  -- We provide: Derivatives of terms.
  ⟦_⟧Δ : ∀ {τ Γ} → (t : Term Γ τ) (ρ : ⟦ Γ ⟧) (dρ : Δ₍ Γ ₎ ρ) → Δ₍ τ ₎ (⟦ t ⟧ ρ)

  -- And we provide correctness proofs about the derivatives.
  correctness : ∀ {τ Γ} (t : Term Γ τ) →
    IsDerivative₍ Γ , τ ₎ ⟦ t ⟧ ⟦ t ⟧Δ

  --------------------
  -- Implementation --
  --------------------
  open import Base.Change.Equivalence
  open import Base.Change.Equivalence.Realizers

  module _ {σ τ : Type} {Γ : Context} (t : Term (σ • Γ) τ) where
    instance
      cΓ : ChangeAlgebra ⟦ Γ ⟧Context
      cΓ = change-algebra₍ Γ ₎
      cσ : ChangeAlgebra ⟦ σ ⟧Type
      cσ = change-algebra σ
      cτ : ChangeAlgebra ⟦ τ ⟧Type
      cτ = change-algebra τ

    private
      ⟦⟧Δλ = nil {{changeAlgebraFun {{cΓ}} {{change-algebra₍ σ ⇒ τ ₎}}}} ⟦ abs t ⟧

    ⟦⟧Δλ-realizer : ∀
      (ρ : ⟦ Γ ⟧) (dρ : Δ₍ Γ ₎ ρ)
      (v : ⟦ σ ⟧) (dv : Δ₍ σ ₎ v) →
      Δ₍ τ ₎ (⟦ t ⟧ (v • ρ))
    ⟦⟧Δλ-realizer ρ dρ v dv = ⟦ t ⟧Δ (v • ρ) (dv • dρ)

    ⟦⟧Δλ-realizer-correct :
      equiv-hp-binary {{cΓ}} {{cσ}} {{cτ}} (⟦ abs t ⟧) ⟦⟧Δλ ⟦⟧Δλ-realizer
    ⟦⟧Δλ-realizer-correct ρ dρ v dv =
      begin
        ⟦ t ⟧ (v ⊞₍ σ ₎ dv • ρ ⊞₍ Γ ₎ dρ) ⊟₍ τ ₎ ⟦ t ⟧ (v • ρ)
      ≙⟨ equiv-cancel-2 {{change-algebra τ}}
           (⟦ t ⟧ (v ⊞₍ σ ₎ dv • ρ ⊞₍ Γ ₎ dρ))
           (⟦ t ⟧Δ (v • ρ) (dv • dρ))
           (sym (correctness t (v • ρ) (dv • dρ)))
      ⟩
         ⟦ t ⟧Δ (v • ρ) (dv • dρ)
      ∎ where open ≙-Reasoning

    ⟦_⟧Δλ′-faster = proj₁ (equiv-raw-change-to-change-binary {{cΓ}} {{cσ}} {{cτ}} ⟦ abs t ⟧ ⟦⟧Δλ ⟦⟧Δλ-realizer ⟦⟧Δλ-realizer-correct)
      where
        open import Data.Product

  ⟦_⟧ΔVar : ∀ {τ Γ} → (x : Var Γ τ) → (ρ : ⟦ Γ ⟧) → Δ₍ Γ ₎ ρ → Δ₍ τ ₎ (⟦ x ⟧Var ρ)
  ⟦ this   ⟧ΔVar (v • ρ) (dv • dρ) = dv
  ⟦ that x ⟧ΔVar (v • ρ) (dv • dρ) = ⟦ x ⟧ΔVar ρ dρ

  ⟦_⟧Δ (const {τ} c) ρ dρ = nil₍ τ ₎ (⟦ c ⟧Const)
  ⟦_⟧Δ (var x) ρ dρ = ⟦ x ⟧ΔVar ρ dρ
  ⟦_⟧Δ (app {σ} {τ} s t) ρ dρ =
       call-change {σ} {τ} (⟦ s ⟧Δ ρ dρ) (⟦ t ⟧ ρ) (⟦ t ⟧Δ ρ dρ)
  ⟦_⟧Δ (abs {σ} {τ} t) ρ dρ = apply ⟦ t ⟧Δλ′-faster ρ dρ

  correctVar : ∀ {τ Γ} (x : Var Γ τ) →
    IsDerivative₍ Γ , τ ₎ ⟦ x ⟧ ⟦ x ⟧ΔVar
  correctVar (this) (v • ρ) (dv • dρ) = refl
  correctVar (that y) (v • ρ) (dv • dρ) = correctVar y ρ dρ

  correctness (const {τ} c) ρ dρ = update-nil₍ τ ₎ ⟦ c ⟧Const
  correctness {τ} (var x) ρ dρ = correctVar {τ} x ρ dρ
  correctness (app {σ} {τ} s t) ρ dρ =
    let
      f₁ = ⟦ s ⟧ ρ
      f₂ = ⟦ s ⟧ (after-env dρ)
      Δf = ⟦ s ⟧Δ ρ dρ
      u₁ = ⟦ t ⟧ ρ
      u₂ = ⟦ t ⟧ (after-env dρ)
      Δu = ⟦ t ⟧Δ ρ dρ
    in
      begin
        f₁ u₁ ⊞₍ τ ₎ call-change {σ} {τ} Δf u₁ Δu
      ≡⟨  sym (is-valid {σ} {τ} Δf u₁ Δu) ⟩
        (f₁ ⊞₍ σ ⇒ τ ₎ Δf) (u₁ ⊞₍ σ ₎ Δu)
      ≡⟨ correctness {σ ⇒ τ} s ρ dρ ⟨$⟩ correctness {σ} t ρ dρ ⟩
        f₂ u₂
      ∎ where open ≡-Reasoning
  correctness {σ ⇒ τ} {Γ} (abs t) ρ dρ = equiv-raw-deriv-to-deriv-binary {{change-algebra₍ Γ ₎}} {{change-algebra σ}} ⟦ abs t ⟧Term (⟦⟧Δλ-realizer t) (⟦⟧Δλ-realizer-correct t) ρ dρ

  -- Corollary: (f ⊞ df) (v ⊞ dv) = f v ⊞ df v dv

  corollary : ∀ {σ τ Γ}
    (s : Term Γ (σ ⇒ τ)) (t : Term Γ σ) (ρ : ⟦ Γ ⟧) (dρ : Δ₍ Γ ₎ ρ) →
      (⟦ s ⟧ ρ ⊞₍ σ ⇒ τ ₎ ⟦ s ⟧Δ ρ dρ)
        (⟦ t ⟧ ρ ⊞₍ σ ₎ ⟦ t ⟧Δ ρ dρ)
    ≡ (⟦ s ⟧ ρ) (⟦ t ⟧ ρ)
      ⊞₍ τ ₎
      (call-change {σ} {τ} (⟦ s ⟧Δ ρ dρ)) (⟦ t ⟧ ρ) (⟦ t ⟧Δ ρ dρ)

  corollary {σ} {τ} s t ρ dρ =
    is-valid {σ} {τ} (⟦ s ⟧Δ ρ dρ) (⟦ t ⟧ ρ) (⟦ t ⟧Δ ρ dρ)

  corollary-closed : ∀ {σ τ} (t : Term ∅ (σ ⇒ τ))
    (v : ⟦ σ ⟧) (dv : Δ₍ σ ₎ v)
    → ⟦ t ⟧ ∅ (after₍ σ ₎ dv)
    ≡ ⟦ t ⟧ ∅ v ⊞₍ τ ₎ call-change {σ} {τ} (⟦ t ⟧Δ ∅ ∅) v dv

  corollary-closed {σ} {τ} t v dv =
    let
      f  = ⟦ t ⟧ ∅
      Δf = ⟦ t ⟧Δ ∅ ∅
    in
      begin
        f (after₍ σ ₎ dv)
      ≡⟨ cong (λ hole → hole (after₍ σ ₎ dv))
              (sym (correctness {σ ⇒ τ} t ∅ ∅)) ⟩
         (f ⊞₍ σ ⇒ τ ₎ Δf) (after₍ σ ₎ dv)
      ≡⟨ is-valid {σ} {τ} (⟦ t ⟧Δ ∅ ∅) v dv ⟩
        f (before₍ σ ₎ dv) ⊞₍ τ ₎ call-change {σ} {τ} Δf v dv
      ∎ where open ≡-Reasoning

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- W-types
------------------------------------------------------------------------

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

module Data.W where

open import Level
open import Function
open import Data.Product hiding (map)
open import Data.Container.Core hiding (map)
open import Data.Container.Relation.Unary.All using (□; all)
open import Relation.Nullary
open import Agda.Builtin.Equality

-- The family of W-types.

data W {s p} (C : Container s p) : Set (s ⊔ p) where
  sup : ⟦ C ⟧ (W C) → W C

module _ {s p} {C : Container s p} {s : Shape C} {f : Position C s → W C} where

 sup-injective₁ : ∀ {t g} → sup (s , f) ≡ sup (t , g) → s ≡ t
 sup-injective₁ refl = refl

 -- See also Data.W.WithK.sup-injective₂.

-- Projections.

module _ {s p} {C : Container s p} where

  head : W C → Shape C
  head (sup (x , f)) = x

  tail : (x : W C) → Position C (head x) → W C
  tail (sup (x , f)) = f

-- map

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂}
         (m : C₁ ⇒ C₂) where

  map : W C₁ → W C₂
  map (sup (x , f)) = sup (⟪ m ⟫ (x , λ p → map (f p)))

-- induction

module _ {s p ℓ} {C : Container s p} (P : W C → Set ℓ)
         (alg : ∀ {t} → □ C P t → P (sup t)) where

 induction : (w : W C) → P w
 induction (sup (s , f)) = alg $ all (induction ∘ f)

module _ {s p ℓ} {C : Container s p} (open Container C)
         {P : Set ℓ} (alg : ⟦ C ⟧ P → P) where

 foldr : W C → P
 foldr = induction (const P) (alg ∘ -,_ ∘ □.proof)

-- If Position is always inhabited, then W_C is empty.

module _ {s p} {C : Container s p} where

  inhabited⇒empty : (∀ s → Position C s) → ¬ W C
  inhabited⇒empty b = foldr ((_$ b _) ∘ proj₂)


text:
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.meta:20 #-}

module UnifyWithIrrelevantArgument where

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

data Bool : Set where true false : Bool

-- irrelevant arguments are ignored in unification
-- e.g. non linearity
test : let X : Bool -> .Bool -> Bool
           X = _
       in  (x : Bool) -> X x x ≡ x
test x = refl

-- e.g. non-pattern
tst1 : let X : Bool -> .Bool -> Bool
           X = _
       in  (x : Bool) -> X x true ≡ x
tst1 x = refl


text:
module ArrowIsCCC where

open import Categories.Category.CartesianClosed.Canonical
open import Categories.Category.Cartesian.Bundle
open import Categories.Category.Core
open import Categories.Category.Construction.Arrow
open import Data.Product
open import Function using (const)
open import Level
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

𝕦 : {A : Set} → A → A
𝕦 x = x

SetC : Category (suc zero) zero zero
SetC =
 record
  { Obj = Set
  ; _⇒_ = λ x y → x → y
  ; _≈_ = _≡_
  ; id = λ x → x
  ; _∘_ = λ f g a → f (g a)
  ; assoc = refl
  ; sym-assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; identity² = refl
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = λ {refl refl → refl}
  }

data t : Set where
 ⊤ : t

!-unique-lemma : ∀ (x : t) → ⊤ ≡ x
!-unique-lemma ⊤ = refl

Set² : Category (suc zero) zero zero
Set² = Arrow SetC

arrow-cart : CartesianCategory (suc zero) zero zero
arrow-cart =
 record { U = Set²
        ; cartesian =
          record { terminal = record { ⊤ = record { arr = 𝕦 } ; ⊤-is-terminal = record { ! = mor⇒ {!   !} ; !-unique = {!   !} } }
                 ; products =
                   record { product = λ {A} {B} →
                    record
                     { A×B = record { arr = λ x → {!   !} }
                     ; π₁ = mor⇒ {!   !}
                     ; π₂ = mor⇒ {!   !}
                     ; ⟨_,_⟩ = λ x x₁ → {!   !}
                     ; project₁ = {!   !} , {!   !}
                     ; project₂ = {!   !} , {!   !}
                     ; unique = λ x x₁ → {!   !}
                     } } } }

{-
_⋆_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
g ⋆ f = λ t → g (f t)

postulate
 extensionality : ∀ {A B : Set} {f g : A → B} →
  (∀ (x : A) → f x ≡ g x) →
  f ≡ g

data t : Set where
 ⊤ : t

!-unique-lemma : ∀ (x : t) → ⊤ ≡ x
!-unique-lemma ⊤ = refl

arrow : Category (suc zero) zero zero
arrow = record
  { Obj = Σ (Set × Set) (λ x → proj₁ x → proj₂ x)
  ; _⇒_ = arr
  ; _≈_ = _≡_
  ; id = ((λ x → x) , (λ z → z)) , refl
  ; _∘_ = λ {A} {B} {C} f g → comp {A} {B} {C} f g
  ; assoc = {!   !}
  ; sym-assoc = {!   !}
  ; identityˡ = λ {A} {B} {f} → idl {A} {B} {f}
  ; identityʳ = λ {A} {B} {f} → idr {A} {B} {f}
  ; identity² = refl
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = λ {refl refl → refl}
  }
  where
  comm-sq : {a b c d : Set} → (a → c) × (b → d) → (f : a → b) → (g : c → d) → Set
  comm-sq {a} {b} {c} {d} (up , down) left right = ∀ {t : a} → down (left t) ≡ right (up t)
  arr : Rel (Σ (Set × Set) (λ x → proj₁ x → proj₂ x)) zero
  arr ((a , b) , x1) ((c , d) , y1) = Σ ((a → c) × (b → d)) λ x → comm-sq x x1 y1
  trans-comm-sq :
   {A B C X Y Z : Set} {up : A → B} {down : X → Y} {up' : B → C} {down' : Y → Z} {left : A → X} {right : B → Y} {right' : C → Z} →
   (p : comm-sq (up , down) left right) → (q : comm-sq (up' , down') right right') →
    comm-sq (up' ⋆ up , down' ⋆ down) left right'
  trans-comm-sq
   {A} {B} {C} {X} {Y} {Z} {up} {down} {up'} {down'} {left} {right} {right'}
   p q {t} =
    begin
     down' (down (left t)) ≡⟨ cong down' p ⟩
     down' (right (up t))  ≡⟨ q ⟩
     right' (up' (up t))
    ∎
  {-
    up   up'
  A -> B -> C
  ↓    ↓    ↓
  X -> Y -> Z
  down  down'
  -}
  𝕦 : {A : Set} → A → A
  𝕦 x = x

  comp : {A B C : Σ (Set × Set) (λ x → proj₁ x → proj₂ x)} → arr B C → arr A B → arr A C
  comp {(A0 , A1) , u} {(B0 , B1) , v} {(C0 , C1) , w} ((f0 , f1) , p) ((g0 , g1) , q) =
   ((λ x → f0 (g0 x)) , (λ z → f1 (g1 z))) , trans-comm-sq {A0} {B0} {C0} {A1} {B1} {C1} {g0} {g1} {f0} {f1} {u} {v} {w} q p
  idl : {A B : Σ (Set × Set) (λ x → proj₁ x → proj₂ x)} {f : arr A B} → comp {A} {B} {B} (((λ x → x) , (λ z → z)) , refl) f ≡ f
  idl {(A0 , A1) , u} {(B0 , B1) , v} {(f0 , f1) , p} = {!   !}
  idr : {A B : Σ (Set × Set) (λ x → proj₁ x → proj₂ x)} {f : arr A B} → comp {A} {A} {B} f (((λ x → x) , (λ z → z)) , refl) ≡ f
  idr {(A0 , A1) , u} {(B0 , B1) , v} {(f0 , f1) , p} = {!   !} -- trans-comm-sq {!   !} {!   !}

open Category arrow

-- just to see what happens:

arrow-cart : CartesianCategory (suc zero) zero zero
arrow-cart =
 record { U = arrow
        ; cartesian = record {
           terminal = record
            { ⊤ = (t , t) , (λ _ → ⊤)
            ; ⊤-is-terminal = record { ! = (λ _ → ⊤) , (λ _ → ⊤) ; !-unique = λ {A} → bang-uniq {A} }
            }
            ; products = record
             { product = λ {A} {B} → record
               { A×B = ((proj₁ (proj₁ A) × proj₁ (proj₁ B)) , (proj₂ (proj₁ A) × proj₂ (proj₁ B))) , λ x → (proj₂ A (proj₁ x)) , (proj₂ B) (proj₂ x)
               ; π₁ = proj₁ , proj₁
               ; π₂ = proj₂ , proj₂
               ; ⟨_,_⟩ = λ {C = C} f g → pair {C} {A} {B} f g
               ; project₁ = refl
               ; project₂ = refl
               ; unique = λ {refl refl → refl}
               } } } }
        where
        prod : Obj → Obj → Obj
        prod ((X , Y) , u) ((A , B) , v) = ((X × A) , (Y × B)) , λ x → (u (proj₁ x)) , (v (proj₂ x))
        bang-uniq : {A : Obj} (f : (arrow Category.⇒ A) ((t , t) , (λ _ → ⊤))) → ((λ _ → ⊤) , (λ _ → ⊤)) ≡ f
        bang-uniq (f0 , f1) =
         cong₂ _,_ (extensionality λ x → !-unique-lemma (f0 x)) (extensionality (λ x → !-unique-lemma (f1 x)))
        pair : {C A B : Obj} → (arrow Category.⇒ C) A → (arrow Category.⇒ C) B → (arrow Category.⇒ C) (prod A B)
        pair {(X , Y) , u} {(A , B) , v} {(E , F) , w} (f0 , f1) (g0 , g1) = (λ x → (f0 x) , (g0 x)) , (λ x → (f1 x) , (g1 x))

arrow-ccc : CartesianClosed arrow
arrow-ccc = record
 { ⊤ = (t , t) , (λ _ → ⊤)
 ; _×_ = prod
 ; ! = (λ _ → ⊤) , (λ _ → ⊤)
 ; π₁ = proj₁ , proj₁
 ; π₂ = proj₂ , proj₂
 ; ⟨_,_⟩ = λ {A} {B} {C} f g → pair {A} {B} {C} f g
 ; !-unique = λ {A} → bang-uniq {A}
 ; π₁-comp = refl
 ; π₂-comp = refl
 ; ⟨,⟩-unique = λ {refl refl → refl}
 ; _^_ = to-the
 ; eval = λ {B} {A} → ev {B} {A}
 ; curry = λ {C} {A} {B} g → cur {C} {A} {B} g
 ; eval-comp = refl
 ; curry-resp-≈ = λ {refl → refl}
 ; curry-unique = {!   !}
 }
 where
 prod : Obj → Obj → Obj
 prod ((X , Y) , u) ((A , B) , v) = ((X × A) , (Y × B)) , λ x → (u (proj₁ x)) , (v (proj₂ x))
 pair : {C A B : Obj} → (arrow Category.⇒ C) A → (arrow Category.⇒ C) B → (arrow Category.⇒ C) (prod A B)
 pair {(X , Y) , u} {(A , B) , v} {(E , F) , w} (f0 , f1) (g0 , g1) = (λ x → (f0 x) , (g0 x)) , (λ x → (f1 x) , (g1 x))
 bang-uniq : {A : Obj} (f : (arrow Category.⇒ A) ((t , t) , (λ _ → ⊤))) → ((λ _ → ⊤) , (λ _ → ⊤)) ≡ f
 bang-uniq (f0 , f1) = cong₂ _,_ (extensionality λ x → !-unique-lemma (f0 x)) (extensionality (λ x → !-unique-lemma (f1 x)))
 to-the : Obj → Obj → Obj
 to-the ((B0 , B1) , u) ((A0 , A1) , v) = (p , (A1 → B1)) , λ x a1 → proj₂ (proj₁ x) a1
  where
   p : Set
   p = Σ ((A0 → B0) × (A1 → B1)) λ r → (λ x → u ((proj₁ r) x)) ≡ (λ x → (proj₂ r) (v x))
 -- va implementato il pullback-hom di u e v : [v,u] fitta in
 {-
 [v,u]     → (A0 → B0)
   ↓ <- lei      ↓
 (A1 → B1) → (A0 → B1)
 -}
 ev : {B A : Obj} → (prod (to-the B A) A) ⇒ B
 ev {(B0 , B1) , u} {(A0 , A1)  , v} = dis , (λ z → proj₁ z (proj₂ z))
  where
   dis : proj₁ (proj₁ (prod (to-the ((B0 , B1) , u) ((A0 , A1) , v)) ((A0 , A1) , v))) → B0
   dis (((s , t) , p) , a0) = s a0
 cur : {C A B : Obj} → prod C A ⇒ B → C ⇒ to-the B A
 cur {(C0 , C1) , c} {(A0 , A1) , a} {(B0 , B1) , b} (fst , snd) =
  (λ x → ((λ y → fst (x , y)) , λ y → snd (c x , y)) , extensionality (λ y → {!   !})) , (λ z z₁ → snd (z , z₁))

-}

max_stars_repo_name: tetrapharmakon/agda-categories

max_issues_repo_name: tetrapharmakon/agda-categories

max_forks_repo_name: tetrapharmakon/agda-categories


text:
{-# OPTIONS --sized-types #-} -- --no-coverage-check #-}

module DeBruijnExSubstSized where

open import Data.Function -- using (_∘_)       -- composition, identity
open import Data.Nat
open import Data.Maybe
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Size

open import DeBruijn

-- untyped de Bruijn terms
data LamE (A : Set) : Size -> Set where
    varE  : {ι : _} -> A -> LamE A (↑ ι)
    appE  : {ι : _} -> LamE A ι -> LamE A ι -> LamE A (↑ ι)
    absE  : {ι : _} -> LamE (Maybe A) ι -> LamE A (↑ ι)
    flatE : {ι : _} -> LamE (LamE A ι) ι -> LamE A (↑ ι)

-- functoriality of LamE
lamE : {A B : Set} -> (A -> B) -> {ι : _} -> LamE A ι -> LamE B ι
lamE f (varE a)     = varE  (f a)
lamE f (appE t1 t2) = appE (lamE f t1) (lamE f t2)
lamE f (absE r)     = absE (lamE (fmap f) r)
lamE f (flatE r)    = flatE (lamE (lamE f) r)

eval : {ι : _} -> {A : Set} -> LamE A ι -> Lam A
eval (varE a)     = var a
eval (appE t1 t2) = app (eval t1) (eval t2)
eval (absE r)     = abs (eval r)
eval (flatE r)    = subst (eval) (eval r)

-- Theorem (naturality of eval):  eval ∘ lamE f ≡ lam f ∘ eval
evalNAT : {A B : Set}(f : A -> B) -> {ι : _} -> (t : LamE A ι) ->
  eval (lamE f t) ≡ lam f (eval t)
evalNAT f (varE a)     = ≡-refl
evalNAT f (appE t1 t2) = begin
  eval (lamE f (appE t1 t2))
     ≡⟨ ≡-refl ⟩
  eval (appE (lamE f t1) (lamE f t2))
     ≡⟨ ≡-refl ⟩
  app (eval (lamE f t1)) (eval (lamE f t2))
     ≡⟨ ≡-cong (\ x -> app x (eval (lamE f t2))) (evalNAT f t1) ⟩
  app (lam f (eval t1))  (eval (lamE f t2))
     ≡⟨ ≡-cong (\ x -> app (lam f (eval t1)) x)  (evalNAT f t2) ⟩
  app (lam f (eval t1))  (lam f (eval t2))
     ≡⟨ ≡-refl ⟩
  lam f (app (eval t1) (eval t2))
     ≡⟨ ≡-refl ⟩
  lam f (eval (appE t1 t2))
     ∎
evalNAT f (absE r) = begin
  eval (lamE f (absE r))
     ≡⟨ ≡-refl ⟩
  eval (absE (lamE (fmap f) r))
     ≡⟨ ≡-refl ⟩
  abs (eval (lamE (fmap f) r))
     ≡⟨ ≡-cong abs (evalNAT (fmap f) r) ⟩
  abs (lam (fmap f) (eval r))
     ≡⟨ ≡-refl ⟩
  lam f (abs (eval r))
     ≡⟨ ≡-refl ⟩
  lam f (eval (absE r))
     ∎
-- in the following case, one manual size annotation is needed on the RHS
-- it is for the first application of the I.H.
evalNAT f (flatE {ι} r) = begin
  eval (lamE f (flatE r))
     ≡⟨ ≡-refl ⟩
  eval (flatE (lamE (lamE f) r))
     ≡⟨ ≡-refl ⟩
  subst eval (eval (lamE (lamE f) r))
     ≡⟨ ≡-cong (subst (eval {ι})) (evalNAT (lamE f) r) ⟩
  subst eval (lam (lamE f) (eval r))
     ≡⟨ substLaw1 (lamE f) eval (eval r) ⟩
  subst (eval ∘ lamE f) (eval r)
     ≡⟨ substExt (evalNAT f) (eval r) ⟩
  subst (lam f ∘ eval) (eval r)
     ≡⟨ substLaw2 f eval (eval r) ⟩
  lam f (subst eval (eval r))
     ≡⟨ ≡-refl ⟩
  lam f (eval (flatE r))
     ∎

evalNATcor : {A : Set}{ι : _}(ee : LamE (LamE A ι) ι) ->
  subst id (eval (lamE eval ee)) ≡ eval (flatE ee)
evalNATcor ee = begin
  subst id (eval (lamE eval ee))
     ≡⟨ ≡-cong (subst id) (evalNAT eval ee) ⟩
  subst id (lam eval (eval ee))
     ≡⟨ substLaw1 eval id (eval ee) ⟩
  subst eval (eval ee)
     ≡⟨ ≡-refl ⟩
  eval (flatE ee)
     ∎

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------------
-- The mirror function: A function with higher-order recursion
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Mirror where

open import FOTC.Base
open import FOTC.Data.List
open import FOTC.Program.Mirror.Type

------------------------------------------------------------------------------
-- The mirror function.
postulate
  mirror    : D
  mirror-eq : ∀ d ts → mirror · node d ts ≡ node d (reverse (map mirror ts))
{-# ATP axiom mirror-eq #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Cats.Util.Conv where

open import Level

open import Cats.Category.Base

module _ {x} (X : Set x) where

  record HasObj lo la l≈ : Set (x ⊔ suc (lo ⊔ la ⊔ l≈))
    where
    infix 90 _ᴼ
    field
      Cat : Category lo la l≈

    open Category Cat

    field
      _ᴼ : X → Obj

  open HasObj {{...}} public using (_ᴼ)

  record HasArrow lo la l≈ : Set (x ⊔ suc (lo ⊔ la ⊔ l≈))
    where
    infixr 90 _⃗
    field
      Cat : Category lo la l≈

    open Category Cat using (Obj ; _⇒_)

    field
      {A B} : X → Obj
      _⃗ : (x : X) → A x ⇒ B x

  open HasArrow {{...}} public using (_⃗)

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


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

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

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Crypto.Crypto.Hash    as Hash
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.KVMap                          as Map
open import Util.PKCS
open import Util.Prelude

module LibraBFT.Impl.Consensus.ConsensusTypes.BlockData where

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

newGenesis : {-Instant →-} QuorumCert → BlockData

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

newGenesisFromLedgerInfo : LedgerInfo → Either ErrLog BlockData
newGenesisFromLedgerInfo li =
  if not (li ^∙ liEndsEpoch)
  then Left fakeErr -- ["BlockData", "newGenesisFromLedgerInfo", "liNextEpochState == Nothing"]
  else
    let ancestor          = BlockInfo∙new
                              (li ^∙ liEpoch)
                              {-Round-} 0
                              Hash.valueZero
                              (li ^∙ liTransactionAccumulatorHash)
                              (li ^∙ liVersion)
                            --(li ^∙ liTimestamp)
                              nothing
        genesisQuorumCert = QuorumCert∙new
                              (VoteData∙new ancestor ancestor)
                              (LedgerInfoWithSignatures∙new
                               (LedgerInfo∙new ancestor Hash.valueZero) Map.empty)
     in pure $ newGenesis {-(li ^∙ liTimestamp)-} genesisQuorumCert

newGenesis {-timestamp-} qc = BlockData∙new
  (qc ^∙ qcCertifiedBlock ∙ biEpoch + 1)
  {-Round-} 0
--timestamp
  qc
  Genesis

newNil : Round → QuorumCert → BlockData
newNil r qc = BlockData∙new
  (qc ^∙ qcCertifiedBlock ∙ biEpoch)
  r
--(qc ^∙ qcCertifiedBlock ∙ biTimestamp)
  qc
  NilBlock

newProposal : TX → Author → Round → {-Instant →-} QuorumCert → BlockData
newProposal payload author round {-timestamp-} quorumCert = BlockData∙new
  (quorumCert ^∙ qcCertifiedBlock ∙ biEpoch) round {-timestamp-} quorumCert (Proposal payload author)

isGenesisBlock : BlockData → Bool
isGenesisBlock bd = bd ^∙ bdBlockType == Genesis

isNilBlock : BlockData → Bool
isNilBlock bd = bd ^∙ bdBlockType == NilBlock


text:
module Dave.Logic.Theorems where

    K : {A B : Set} → A → B → A
    K a b = a

    S : {A B C : Set} → (A → B → C) → (A → B) → A → C
    S = λ f → λ g → λ a → f a (g a)