text:
module Tools where
import PolyDepPrelude
-- import Sigma
-- import And

open PolyDepPrelude  using(Datoid;  Bool; true; false; _&&_; Nat;  True;  Taut; unit)

liftAnd : (a : Bool)(b : Bool)(ta : True a)(tb : True b) -> True (a && b)
liftAnd (true)  (true)  ta tb = unit
liftAnd (true)  (false) ta () -- empty
liftAnd (false) _       () _  -- empty

{-
sigmaCond (D:Datoid)
          (B:D.Elem -> Set)
          (C:Set)
          (ifTrue:(b:D.Elem) -> B b -> B b -> C)
          (ifFalse:C)
          (x:Sigma D.Elem B)
          (y:Sigma D.Elem B)
  : C
  = case x of {
      (si a pa) ->
        case y of {
          (si b pb) ->
            let caseOn (e:Bool)(cast:True e -> B a -> B b) : C
                  = case e of {
                      (false) -> ifFalse;
                      (true) -> ifTrue b (cast tt@_ pa) pb;}
            in  caseOn (D.eq a b) (D.subst B);};}
-- trueAnd = \a b -> (LogicBool.spec_and a b).snd
trueAnd (a:Bool)(b:Bool)(p:And (True a) (True b)) : True (a && b)
  = case p of {
      (Pair a' b') ->
        case a of {
          (true) ->
            case b of {
              (true) -> tt@_;
              (false) -> b';};
          (false) -> a';};}
splitAnd (a:Bool)(b:Bool)(p:True (_&&_ a b))
  : Times (True a) (True b)
  = case a of {
      (true) ->
        case b of {
          (true) ->
            struct {
              fst = tt@_;
              snd = tt@_;};
          (false) -> case p of { };};
      (false) -> case p of { };}
trueSigma (D:Set)(f:D -> Bool)(s:Sigma D (\(d:D) -> True (f d)))
  : True (f (si1 D (\(d:D) -> True (f d)) s))
  = case s of { (si a b) -> b;}
Maybe (A:Set) : Set
  = data Nothing | Just (a:A)
mapMaybe (|A,|B:Set)(f:A -> B)(x:Maybe A) : Maybe B
  = case x of {
      (Nothing) -> Nothing@_;
      (Just a)  -> Just@_ (f a);}
maybe (|A,|B:Set)(e:B)(f:A -> B) : Maybe A -> B
  = \x -> case x of {
            (Nothing) -> e;
            (Just a) -> f a;}
open SET
 use  List,  Absurd,  Unit,  Either,  mapEither,  Times,  mapTimes,  id,
      uncur,  elimEither
elimList (|A:Set)
         (C:List A -> Type)
         (n:C nil@_)
         (c:(a:A) -> (as:List A) -> C as -> C (con@_ a as))
         (as:List A)
  : C as
  = case as of {
      (nil) -> n;
      (con x xs) -> c x xs (elimList C n c xs);}
-- Common generalization of sum and product of a list of sets
--   (represented as a decoding function f and a list of codes)
O (A:Set)(E:Set)(Op:Set -> Set -> Set)(f:A -> Set)
  : List A -> Set
  = elimList (\as -> Set) E (\a -> \as -> Op (f a))
-- The corresponding map function! (Takes a nullary and a binary
-- functor as arguments.)
mapO (|A,|E:Set)
     (|Op:Set -> Set -> Set)
     (mapE:E -> E)
     (mapOp:(A1,B1,A2,B2:Set) |->
             (f1:A1 -> B1) ->
             (f2:A2 -> B2) ->
             Op A1 A2 -> Op B1 B2)
     (X:A -> Set)
     (Y:A -> Set)
     (f:(a:A) -> X a -> Y a)
  : (as:List A) -> O A E Op X as -> O A E Op Y as
  = elimList (\(as:List A) -> O A E Op X as -> O A E Op Y as) mapE
      (\a -> \as -> mapOp (f a))
mapAbsurd : Absurd -> Absurd = id
eqAbsurd  : Absurd -> Absurd -> Bool = \h -> \h' -> case h of { }
-- the name of OPlus and OTimes indicate the symbols they should be
--   shown as in algebra: a big ring (a big "O") with the operator +
--   or x in
-- Disjoint sum over a list of codes
OPlus (A:Set) : (A -> Set) -> List A -> Set
  = O A Absurd Either
-- corresponding map function
mapOPlus (|A:Set)(X:A -> Set)(Y:A -> Set)(f:(a:A) -> X a -> Y a)
  : (as:List A) -> OPlus A X as -> OPlus A Y as
  = mapO id mapEither X Y f
-- Cartesian product over a list of codes
OTimes (A:Set) : (A -> Set) -> List A -> Set
  = O A Unit Times
-- corresponding map
mapOTimes (|A:Set)(X:A -> Set)(Y:A -> Set)(f:(a:A) -> X a -> Y a)
  : (as:List A) -> OTimes A X as -> OTimes A Y as
  = mapO id mapTimes X Y f
sizeOPlus (|A:Set)
          (f:A -> Set)
          (n:(a:A) -> f a -> Nat)
          (as:List A)
          (t:OPlus A f as)
  : Nat
  = case as of {
      (nil) -> case t of { };
      (con a as) ->
        case t of {
          (inl x) -> n a x;
          (inr y) -> sizeOPlus f n as y;};}
triv (x:Absurd)  : Set  = case x of { }
trivT (x:Absurd) : Type = case x of { }
sizeOTimes (|A:Set)
           (f:A -> Set)
           (z:Nat)
           (n:(a:A) -> f a -> Nat)
           (as:List A)
           (t:OTimes A f as)
  : Nat
  = case as of {
      (nil)      -> case t of { (tt) -> z;};
      (con a as) -> uncur (+) (mapTimes (n a) (sizeOTimes f z n as) t);}
eqUnit (x:Unit)(y:Unit) : Bool
  = true@_
eqTimes (|A1,|A2,|B1,|B2:Set)
        (eq1:A1 -> B1 -> Bool)
        (eq2:A2 -> B2 -> Bool)
  : Times A1 A2 -> Times B1 B2 -> Bool
  = \x -> \y -> _&&_ (eq1 x.fst y.fst) (eq2 x.snd y.snd)
EqFam (A:Set)(f:A -> Set)(g:A -> Set) : Set
  = (a:A) -> f a -> g a -> Bool
eqOTimes (A:Set)(f:A -> Set)(g:A -> Set)(eq:EqFam A f g)
  : EqFam (List A) (OTimes A f) (OTimes A g)
  = elimList
      (\as ->  (OTimes A f as -> OTimes A g as -> Bool))
      eqUnit
      (\a -> \as -> eqTimes (eq a))
eqEither (|A1,|A2,|B1,|B2:Set)
       (eq1:A1 -> B1 -> Bool)
       (eq2:A2 -> B2 -> Bool)
  : Either A1 A2 -> Either B1 B2 -> Bool
  = \x -> \y ->
            case x of {
              (inl x') ->
                case y of {
                  (inl x0) -> eq1 x' x0;
                  (inr y') -> false@_;};
              (inr y') ->
                case y of {
                  (inl x') -> false@_;
                  (inr y0) -> eq2 y' y0;};}
eqOPlus (A:Set)(f:A -> Set)(g:A -> Set)(eq:EqFam A f g)
  : EqFam (List A) (OPlus A f) (OPlus A g)
  = elimList
      (\(as:List A) -> OPlus A f as -> OPlus A g as -> Bool)
      eqAbsurd
      (\a -> \as -> eqEither (eq a))
Fam (I:Set)(X:I -> Set) : Type
  = (i:I) -> X i -> Set
eitherSet (A:Set)(B:Set)(f:A -> Set)(g:B -> Set)(x:Either A B)
  : Set
  = case x of {
      (inl x') -> f x';
      (inr y) -> g y;}
famOPlus (A:Set)(G:A -> Set) : Fam A G -> Fam (List A) (OPlus A G)
  = \(f:Fam A G) ->
    elimList (\(as:List A) -> OPlus A G as -> Set) triv
      (\(a:A) -> \(as:List A) -> eitherSet (G a) (OPlus A G as) (f a))
bothSet (A:Set)(B:Set)(f:A -> Set)(g:B -> Set)(x:Times A B)
  : Set
  = Times (f x.fst) (g x.snd)
famOTimes (A:Set)(G:A -> Set)
  : Fam A G -> Fam (List A) (OTimes A G)
  = \(f:Fam A G) ->
    elimList (\(as:List A) -> OTimes A G as -> Set)
      (\(u:OTimes A G nil@_) -> Unit)
      (\(a:A) -> \(as:List A) -> bothSet (G a) (OTimes A G as) (f a))
FAM (I:Set)(X:I -> Set)(Y:(i:I) -> X i -> Set) : Type
  = (i:I) -> (x:X i) -> Y i x
eitherFAM (A:Set)
          (A2:Set)
          (G:A -> Set)
          (G2:A2 -> Set)
          (H:Fam A G)
          (H2:Fam A2 G2)
          (a:A)
          (a2:A2)
          (f:(x:G a) -> H a x)
          (f2:(x2:G2 a2) -> H2 a2 x2)
          (x:Either (G a) (G2 a2))
  : eitherSet (G a) (G2 a2) (H a) (H2 a2) x
  = case x of {
      (inl y) -> f y;
      (inr y2) -> f2 y2;}
FAMOPlus (A:Set)(G:A -> Set)(H:Fam A G)
  : FAM A G H -> FAM (List A) (OPlus A G) (famOPlus A G H)
  = \(f:FAM A G H) ->
    elimList (\(as:List A) -> (x:OPlus A G as) -> famOPlus A G H as x)
      (\(x:OPlus A G nil@_) -> whenZero (famOPlus A G H nil@_ x) x)
      (\(a:A) ->
       \(as:List A) ->
       eitherFAM A (List A) G (OPlus A G) H (famOPlus A G H) a as (f a))
bothFAM (A:Set)
        (A2:Set)
        (G:A -> Set)
        (G2:A2 -> Set)
        (H:Fam A G)
        (H2:Fam A2 G2)
        (a:A)
        (a2:A2)
        (f:(x:G a) -> H a x)
        (f2:(x2:G2 a2) -> H2 a2 x2)
        (x:Times (G a) (G2 a2))
  : bothSet (G a) (G2 a2) (H a) (H2 a2) x
  = struct {
      fst = f x.fst;
      snd = f2 x.snd;}
FAMOTimes (A:Set)(G:A -> Set)(H:Fam A G)
  : FAM A G H -> FAM (List A) (OTimes A G) (famOTimes A G H)
  = \(f:FAM A G H) ->
    elimList
      (\(as:List A) -> (x:OTimes A G as) -> famOTimes A G H as x)
      (\(x:OTimes A G nil@_) -> x)
      (\(a:A) ->
       \(as:List A) ->
       bothFAM A (List A) G (OTimes A G) H (famOTimes A G H) a as (f a))
-}
{-
  Size (A:Set) : Type
    = A -> Nat

  size_OPlus (A:Set)
             (f:A -> Set)
             (size_f:(a:A) -> f a -> Nat)
             (as:List A)
    : OPlus f as -> Nat
    = \(x:OPlus f as) -> ?

  size_OPlus (A:Set)
             (f:A -> Set)
             (size_f:(a:A) -> Size (f a))
             (as:List A)
    : Size (OPlus f as)
    = \(x:OPlus f as) ->
-}
{- Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
var "mapMaybe" hide 2
var "sigmaCond" hide 3
var "maybe" hide 2
var "O" hide 1
var "OTimes" hide 1
var "OPlus" hide 1
var "mapOPlus" hide 3
var "id" hide 1
var "mapOTimes" hide 3
var "mapO" hide 3
var "mapOp" hide 4
var "uncur" hide 3
var "mapTimes" hide 4
var "sizeOTimes" hide 2
var "sizeOPlus" hide 2
var "eqTimes" hide 4
var "OTimesEq" hide 3
var "elimList" hide 1
var "eqOTimes" hide 3
var "eqEither" hide 4
var "eqOPlus" hide 3
var "eitherSet" hide 2
var "bothSet" hide 2
var "famOPlus" hide 2
var "famOTimes" hide 2
var "helper4" hide 4
var "eitherFAM" hide 4
var "FAMOTimes" hide 3
var "FAMOPlus" hide 3
 #-}


text:
{-# OPTIONS --without-K #-}
module Leftovers.TraverseTerm where

open import Data.List
-- We only need the writer monad, but as far as I can tell
-- it's not in the Agda stdlib
open import Category.Monad.State

open import Reflection using (Term ; Meta ; Name ; Arg)
import Leftovers.Everywhere

open import Relation.Binary.PropositionalEquality

open import Data.Product
open import Data.Nat
open import Data.Maybe
open import Data.String

LCxt : Set
LCxt = List (String × Arg Term)

record LeafInfoMaker (A : Set) : Set where
  field
    onVar : LCxt → ℕ → Maybe A
    onMeta : LCxt → Meta → Maybe A
    onCon : LCxt → Name → Maybe A
    onDef : LCxt → Name → Maybe A

collectFromSubterms : ∀ {A : Set} → LeafInfoMaker A → Term → List A
collectFromSubterms {A} f t = proj₂ (stateResult [])
 where
   open RawMonadState (StateMonadState (List A))
   open import Leftovers.Everywhere (StateMonad (List A))

   toAction : ∀ {X : Set} → (LCxt → X → Maybe A) → Action X
   toAction f cxt x with f (Cxt.context cxt) x
   ... | nothing = return x
   ... | just fx =
     do
       modify (fx ∷_)
       return x

   stateResult : State (List A) Term
   stateResult =
        everywhere (record
          { onVar = toAction (LeafInfoMaker.onVar f)
          ; onMeta = toAction (LeafInfoMaker.onMeta f)
          ; onCon = toAction (LeafInfoMaker.onCon f)
          ; onDef = toAction (LeafInfoMaker.onDef f) }) (λ Γ x → return x) t

ext: agda

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers


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

open import Categories.Category using (Category)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Closed using (Closed)

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

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

open import Categories.Morphism.Reasoning C
  using (pull-last; pull-first; pullˡ; pushˡ; center; center⁻¹; pullʳ)
open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor.Properties

open Closed Cl
open Category C
open HomReasoning

private
  module ℱ = Functor
  α⇒ = associator.from
  α⇐ = associator.to
  module ⊗ = Functor ⊗

open Π.Π
open adjoint renaming (unit to η; counit to ε; Ladjunct to 𝕃; Ladjunct-comm′ to 𝕃-comm′;
 Ladjunct-resp-≈ to 𝕃-resp-≈)

L : (X Y Z : Obj) → [ Y , Z ]₀ ⇒ [ [ X , Y ]₀ , [ X , Z ]₀ ]₀
L X Y Z = 𝕃 (𝕃 (ε.η Z ∘ (id ⊗₁ ε.η Y) ∘ α⇒))

private
  [g]₁         : {W Z Z′ : Obj} {g : Z ⇒ Z′} → [ W , Z ]₀ ⇒ [ W , Z′ ]₀
  [g]₁ {g = g} = [ id , g ]₁

  push-α⇒-right : {X Y Z Z′ : Obj} {g : Z ⇒ Z′} → (ε.η Z′ ∘ (id ⊗₁ ε.η {X} Y) ∘ α⇒) ∘ ([g]₁ ⊗₁ id) ⊗₁ id ≈ (g ∘ ε.η Z) ∘ (id ⊗₁ ε.η Y) ∘ α⇒
  push-α⇒-right {X} {Y} {Z} {Z′} {g} = begin
   (ε.η Z′ ∘ (id ⊗₁ ε.η {X} Y) ∘ α⇒) ∘ ([g]₁ ⊗₁ id) ⊗₁ id   ≈⟨ pull-last assoc-commute-from ⟩
   ε.η Z′ ∘ (id ⊗₁ ε.η {X} Y) ∘ ([g]₁ ⊗₁ (id ⊗₁ id)) ∘ α⇒   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ℱ.F-resp-≈ ⊗ (refl , ⊗.identity) ⟩∘⟨refl ⟩
   ε.η Z′ ∘ (id ⊗₁ ε.η Y) ∘ [g]₁ ⊗₁ id ∘ α⇒                 ≈⟨ refl⟩∘⟨ pullˡ [ ⊗ ]-commute ⟩
   ε.η Z′ ∘ ([g]₁ ⊗₁ id ∘ (id ⊗₁ ε.η Y)) ∘ α⇒               ≈⟨ pull-first (ε.commute g) ⟩
   (g ∘ ε.η Z) ∘ (id ⊗₁ ε.η Y) ∘ α⇒                          ∎

L-g-swap : {X Y Z Z′ : Obj} {g : Z ⇒ Z′} → L X Y Z′ ∘  [ id , g ]₁ ≈ [ [ id , id ]₁ , [ id , g ]₁ ]₁ ∘ L X Y Z
L-g-swap {X} {Y} {Z} {Z′} {g} = begin
  L X Y Z′ ∘  [g]₁                                              ≈˘⟨ 𝕃-comm′ ⟩
  𝕃 (𝕃 (ε.η Z′ ∘ (id ⊗₁ ε.η Y) ∘ α⇒) ∘ [g]₁ ⊗₁ id)             ≈˘⟨ 𝕃-resp-≈ 𝕃-comm′ ⟩
  𝕃 (𝕃 $ (ε.η Z′ ∘ (id ⊗₁ ε.η Y) ∘ α⇒) ∘ ([g]₁ ⊗₁ id) ⊗₁ id)  ≈⟨ 𝕃-resp-≈ $ 𝕃-resp-≈ push-α⇒-right ⟩
  𝕃 (𝕃 $ (g ∘ ε.η Z) ∘ (id ⊗₁ ε.η Y) ∘ α⇒)                     ≈⟨ 𝕃-resp-≈ $ pushˡ $ X-resp-≈ assoc ○ ℱ.homomorphism [ X ,-] ⟩
  𝕃 ([ id , g ]₁ ∘ 𝕃 (ε.η Z ∘ (id ⊗₁ ε.η Y) ∘ α⇒))             ≈⟨ pushˡ (ℱ.homomorphism [ XY ,-]) ⟩
  [ id , [g]₁ ]₁ ∘ L X Y Z                                      ≈˘⟨ [-,-].F-resp-≈ ([-,-].identity , refl) ⟩∘⟨refl ⟩
  [ [ id , id ]₁ , [g]₁ ]₁ ∘ L X Y Z                            ∎
  where
  XY        = [ X , Y ]₀
  X-resp-≈  = ℱ.F-resp-≈ [ X ,-]

L-f-swap : {X Y Y′ Z : Obj} {f : Y′ ⇒ Y} → L X Y′ Z ∘ [ f , id ]₁ ≈ [ [ id , f ]₁ , [ id , id ]₁ ]₁ ∘ L X Y Z
L-f-swap {X} {Y} {Y′} {Z} {f} = begin
  L X Y′ Z ∘ [fˡ]₁                                        ≈˘⟨ 𝕃-comm′ ⟩
  𝕃 (𝕃 inner-L ∘ [fˡ]₁ ⊗₁ id)                             ≈˘⟨ 𝕃-resp-≈ 𝕃-comm′ ⟩
  𝕃 (𝕃 (inner-L ∘ ([fˡ]₁ ⊗₁ id) ⊗₁ id))                  ≈⟨ 𝕃-resp-≈ $ 𝕃-resp-≈ fˡ⇒fʳ ⟩
  𝕃 (𝕃 $ inner-L ∘ (id ⊗₁ [fʳ]₁) ⊗₁ id)                  ≈⟨ 𝕃-resp-≈ $ ∘-resp-≈ˡ $ ℱ.homomorphism [ X ,-] ⟩
  𝕃 (([ id , inner-L ]₁ ∘ [ id , (id ⊗₁ [fʳ]₁) ⊗₁ id ]₁)
           ∘ η.η (YZ ⊗₀ XY′))                             ≈⟨ 𝕃-resp-≈ $ pullʳ (⟺ (η.commute _)) ○ (⟺ assoc) ⟩
  𝕃 (𝕃 inner-L ∘ id ⊗₁ [fʳ]₁)                             ≈⟨ ℱ.homomorphism [ XY′ ,-] ⟩∘⟨refl ⟩
  ([ id , 𝕃 inner-L ]₁ ∘ [ id , id ⊗₁ [fʳ]₁ ]₁) ∘ η.η YZ  ≈⟨ pullʳ (mate.commute₁ [fʳ]₁) ⟩
  [ id , 𝕃 inner-L ]₁ ∘ [ [fʳ]₁ , id ]₁ ∘ η.η YZ          ≈⟨ pullˡ [ [-,-] ]-commute ○ assoc ○ ∘-resp-≈ˡ ([-,-].F-resp-≈ (refl , ⟺ [-,-].identity)) ⟩
  [ [fʳ]₁ , [ id , id ]₁ ]₁ ∘ L X Y Z                           ∎
  where
  XY′        = [ X , Y′ ]₀
  YZ         = [ Y , Z ]₀
  [fʳ]₁      : ∀ {W} → [ W , Y′ ]₀ ⇒ [ W , Y ]₀
  [fʳ]₁      = [ id , f ]₁
  [fˡ]₁      : ∀ {W} → [ Y , W ]₀ ⇒ [ Y′ , W ]₀
  [fˡ]₁      = [ f , id ]₁
  inner-L     : ∀ {W} → ([ W , Z ]₀ ⊗₀ [ X , W ]₀) ⊗₀ X ⇒ Z
  inner-L {W} = ε.η Z ∘ id ⊗₁ ε.η {X} W ∘ α⇒

  fˡ⇒fʳ : inner-L {Y′} ∘ ([fˡ]₁ ⊗₁ id) ⊗₁ id ≈ inner-L {Y} ∘ (id ⊗₁ [fʳ]₁) ⊗₁ id
  fˡ⇒fʳ = begin
    inner-L ∘ ([fˡ]₁ ⊗₁ id) ⊗₁ id                      ≈⟨ pull-last assoc-commute-from ⟩
    ε.η Z ∘ (id ⊗₁ ε.η Y′) ∘ [fˡ]₁ ⊗₁ id ⊗₁ id ∘ α⇒   ≈⟨ ∘-resp-≈ʳ $ pullˡ
                                                          (∘-resp-≈ʳ (ℱ.F-resp-≈ ⊗ (refl , ⊗.identity)) ○ [ ⊗ ]-commute) ⟩
    ε.η Z ∘ ([fˡ]₁ ⊗₁ id ∘ id ⊗₁ ε.η Y′) ∘ α⇒          ≈⟨ pull-first (mate.commute₂ f) ⟩
    (ε.η Z ∘ id ⊗₁ f) ∘ id ⊗₁ ε.η Y′ ∘ α⇒              ≈⟨ center $ ⟺ (ℱ.homomorphism (YZ ⊗-)) ⟩
    ε.η Z ∘ id ⊗₁ (f ∘ ε.η Y′) ∘ α⇒                    ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ ℱ.F-resp-≈ (YZ ⊗-) $ ⟺ (ε.commute f) ⟩
    ε.η Z ∘ id ⊗₁ (ε.η Y ∘ [fʳ]₁ ⊗₁ id) ∘ α⇒           ≈⟨ ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ ℱ.homomorphism (YZ ⊗-) ⟩
    ε.η Z ∘ (id ⊗₁ ε.η Y ∘ id ⊗₁ [fʳ]₁ ⊗₁ id) ∘ α⇒     ≈⟨ (center⁻¹ refl (⟺ assoc-commute-from)) ○ pullˡ assoc ⟩
    inner-L ∘ (id ⊗₁ [fʳ]₁) ⊗₁ id ∎

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
-- Andreas, 2011-10-02
module IrrelevantLambdasDoNotNeedDotsAlways where

bla : ((.Set → Set1) → Set1) -> Set1
bla f = f (λ x → Set)

-- here, the lambda does not need a dot, like in (λ .x → Set)
-- because the dot from the function space can be taken over

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Data.Empty using ( ⊥ )
open import Data.Nat using ( ℕ ; zero ; suc ; _+_ ; _≤_ ; z≤n ; s≤s )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong )
open import Relation.Binary.PropositionalEquality.TrustMe using ( trustMe )
open import Relation.Nullary using ( ¬_ )

module FRP.LTL.Util where

infixr 5 _trans_ _∋_

-- Irrelevant projections

postulate
  .irrelevant : ∀ {A : Set} → .A → A

-- Irrelevant ≡ can be promoted to relevant ≡

≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
≡-relevant a≡b = trustMe

-- A version of ⊥-elim which takes an irrelevant argument

⊥-elim : {A : Set} → .⊥ → A
⊥-elim ()

-- An infix variant of trans

_trans_ : ∀ {X : Set} {x y z : X} → (x ≡ y) → (y ≡ z) → (x ≡ z)
refl trans refl = refl

-- Help the type inference engine out by being explicit about X.

_∋_ : (X : Set) → X → X
X ∋ x = x

-- Lemmas about addition on ℕ
-- These are from Data.Nat.Properties,
-- included here to avoid having to load all of Data.Nat.Properties' dependencies.

m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
m+1+n≡1+m+n zero    n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)

+-comm : ∀ m n → (m + n ≡ n + m)
+-comm zero    zero    = refl
+-comm zero    (suc n) = cong suc (+-comm zero n)
+-comm (suc m) n       = (cong suc (+-comm m n)) trans (sym (m+1+n≡1+m+n n m))

+-assoc : ∀ l m n → ((l + m) + n ≡ l + (m + n))
+-assoc zero    m n = refl
+-assoc (suc l) m n = cong suc (+-assoc l m n)

m+n≡0-impl-m≡0 : ∀ m n → (m + n ≡ 0) → (m ≡ 0)
m+n≡0-impl-m≡0 zero    n m+n≡0 = refl
m+n≡0-impl-m≡0 (suc m) n ()

1+n≰n : ∀ n → ¬(suc n ≤ n)
1+n≰n zero    ()
1+n≰n (suc n) (s≤s m≤n) = 1+n≰n n m≤n

≤0-impl-≡0 : ∀ {n} → (n ≤ 0) → (n ≡ 0)
≤0-impl-≡0 z≤n = refl

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
open import Coinduction using ( ♭ )
open import Data.Empty using ( ⊥-elim )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import System.IO.Transducers.Lazy
  using ( _⇒_ ; inp ; out ; done ; ⟦_⟧ ; _≃_ ; out' ; out* ;
     _⟫_ ;_[&]_ ; unit₁ ; unit₂ ; assoc ; assoc⁻¹ ; swap'' ; swap' ; swap )
open import System.IO.Transducers.Reflective using ( Reflective )
open import System.IO.Transducers.Strict using ( Strict )
open import System.IO.Transducers.Session using ( I ; Σ ; IsΣ ; _&_ )
open import System.IO.Transducers.Trace
  using ( Trace ; _✓ ; _≤_ ; [] ; _∷_ ; revApp )
open import System.IO.Transducers.Properties.Lemmas
  using ( ✓? ; I-✓ ; I-η ; ⟦⟧-resp-✓ ; ⟦⟧-refl-✓ ; ⟦⟧-resp-[] )
open import System.IO.Transducers.Properties.Category
  using ( ⟦done⟧ ; _⟦⟫⟧_ ; ⟫-≃-⟦⟫⟧ ; done-semantics )
open import System.IO.Transducers.Properties.Monoidal
  using ( _++_ ; front ; back ; _⟦[&]⟧_ ; ⟦unit₁⟧ ; ⟦unit₂⟧ ; ⟦assoc⟧ ; ⟦assoc⁻¹⟧ ;
    ++-cong ; ++-β₁ ; ++-β₂ ; ++-β₂-[] ; ++-η ; back≡[] ; back-resp-[] ; ++-resp-[] ;
    ++-refl-✓₁ ; ++-refl-✓₂ ; front-refl-✓ ; back-refl-✓ ; ++-resp-✓ ; front-resp-✓ ;
    ⟦[&]⟧-++ ; ⟦assoc⟧-++ ; ⟦assoc⁻¹⟧-++ ;
    [&]-≃-⟦[&]⟧ ; [&]-semantics ;
    assoc-semantics ; assoc⁻¹-semantics ;
    unit₁-semantics ; unit₂-semantics ; unit₂⁻¹-semantics )
open import Relation.Binary.PropositionalEquality
  using ( _≡_ ; sym ; refl ; trans ; cong ; cong₂ )
open import Relation.Nullary using ( Dec ; yes ; no )

module System.IO.Transducers.Properties.LaxBraided where

open Relation.Binary.PropositionalEquality.≡-Reasoning

-- Semantics of out*

⟦out*⟧ : ∀ {S T U} → (T ≤ U) → (Trace S → Trace T) → (Trace S → Trace U)
⟦out*⟧ cs f as = revApp cs (f as)

out*-semantics : ∀ {S T U} (cs : T ≤ U) (P : S ⇒ T) →
  ⟦ out* cs P ⟧ ≃ ⟦out*⟧ cs ⟦ P ⟧
out*-semantics []                 P as = refl
out*-semantics (_∷_ {Σ V F} c cs) P as = out*-semantics cs (out c P) as
out*-semantics (_∷_ {I}    () cs) P as

-- Semantics of swap

⟦swap''⟧ : ∀ {T U} → (I ≤ U) → (Trace T) → (Trace (T & U))
⟦swap''⟧ cs as = as ++ revApp cs []

⟦swap'⟧ : ∀ {S T U} → (S ≤ U) → (Trace (S & T)) → (Trace (T & U))
⟦swap'⟧ {S} cs as = back {S} as ++ revApp cs (front {S} as)

⟦swap⟧ : ∀ {S T} → (Trace (S & T) → Trace (T & S))
⟦swap⟧ {S} as = back {S} as ++ front {S} as

swap''-semantics : ∀ {T U} cs → ⟦ swap'' {T} {U} cs ⟧ ≃ ⟦swap''⟧ cs
swap''-semantics {I}     cs []       = out*-semantics cs done []
swap''-semantics {Σ W G} cs []       = refl
swap''-semantics {Σ W G} cs (a ∷ as) = cong (_∷_ a) (swap''-semantics cs as)
swap''-semantics {I}     cs (() ∷ as)

swap'-semantics : ∀ {S T isΣ U} cs → ⟦ swap' {S} {T} {isΣ} {U} cs ⟧ ≃ ⟦swap'⟧ cs
swap'-semantics {I}             cs as       = swap''-semantics cs as
swap'-semantics {Σ V F} {Σ W G} cs []       = refl
swap'-semantics {Σ V F} {Σ W G} cs (a ∷ as) = swap'-semantics (a ∷ cs) as
swap'-semantics {Σ V F} {I}  {} cs as

swap-semantics : ∀ {S T} → ⟦ swap {S} {T} ⟧ ≃ ⟦swap⟧ {S} {T}
swap-semantics {I}             as = unit₂⁻¹-semantics as
swap-semantics {Σ V F} {I}     as = cong₂ _++_ (sym (I-η (back {Σ V F} as))) (unit₂-semantics as)
swap-semantics {Σ V F} {Σ W G} as = swap'-semantics {Σ V F} [] as

-- Swap reflects completion

⟦swap⟧-refl-✓ : ∀ {S T} as → (⟦swap⟧ {S} {T} as ✓) → (as ✓)
⟦swap⟧-refl-✓ {S} {I}     as ✓bs = front-refl-✓ {S} as (++-refl-✓₂ {I} {S} {back {S} as} ✓bs)
⟦swap⟧-refl-✓ {S} {Σ W G} as ✓bs = back-refl-✓ {S} as (++-refl-✓₁ {Σ W G} ✓bs)

-- Swap plays nicely with concatenation

⟦swap⟧-++ : ∀ {S T} (as : Trace S) (bs : Trace T) → (as ✓ ⊎ bs ≡ []) →
  ⟦swap⟧ {S} {T} (as ++ bs) ≡ bs ++ as
⟦swap⟧-++ as bs ✓as/bs≡[] with ✓? as
⟦swap⟧-++ as bs ✓as/bs≡[]    | yes ✓as = cong₂ _++_ (++-β₂ ✓as bs) (++-β₁ as bs)
⟦swap⟧-++ as bs (inj₁ ✓as)   | no ¬✓as = cong₂ _++_ (++-β₂ ✓as bs) (++-β₁ as bs)
⟦swap⟧-++ as bs (inj₂ bs≡[]) | no ¬✓as = cong₂ _++_ (trans (++-β₂-[] ¬✓as bs) (sym bs≡[])) (++-β₁ as bs)

-- Swap is natural when f respects completion, and g reflects completion and is strict

⟦swap⟧-natural : ∀ {S T U V} → (f : Trace S → Trace T) → (g : Trace U → Trace V) →
  (∀ as → (as ✓) → (f as ✓)) →
    (∀ as → ((g as ✓)) → (as ✓)) → (g [] ≡ []) →
      (f ⟦[&]⟧ g ⟦⟫⟧ ⟦swap⟧ {T} {V}) ≃ (⟦swap⟧ {S} {U} ⟦⟫⟧ g ⟦[&]⟧ f)
⟦swap⟧-natural {S} {T} {U} {V} f g f-resp-✓ g-refl-✓ g-resp-[] as =
  begin
    ⟦swap⟧ {T} {V} (f as₁ ++ g as₂)
  ≡⟨ ⟦swap⟧-++ (f as₁) (g as₂) ✓fas₁/gas₂≡[] ⟩
    g as₂ ++ f as₁
  ≡⟨ sym (⟦[&]⟧-++ g f g-refl-✓ as₂ as₁) ⟩
    (g ⟦[&]⟧ f) (as₂ ++ as₁)
  ∎ where
  as₁ = front {S} as
  as₂ = back {S} as
  ✓fas₁/gas₂≡[] : f as₁ ✓ ⊎ g as₂ ≡ []
  ✓fas₁/gas₂≡[] with ✓? as₁
  ✓fas₁/gas₂≡[] | yes ✓as₁ = inj₁ (f-resp-✓ as₁ ✓as₁)
  ✓fas₁/gas₂≡[] | no ¬✓as₁ = inj₂ (trans (cong g (back≡[] ¬✓as₁)) g-resp-[])

swap-natural : ∀ {S T U V} (P : S ⇒ T) {Q : U ⇒ V} →
  (Reflective Q) → (Strict Q) →
    ⟦ P [&] Q ⟫ swap {T} {V} ⟧ ≃ ⟦ swap {S} {U} ⟫ Q [&] P ⟧
swap-natural {S} {T} {U} {V} P {Q} ⟳Q #Q as =
  begin
    ⟦ P [&] Q ⟫ swap {T} {V} ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ ([&]-semantics P Q) (swap-semantics {T} {V}) as ⟩
    (⟦ P ⟧ ⟦[&]⟧ ⟦ Q ⟧ ⟦⟫⟧ ⟦swap⟧ {T} {V}) as
  ≡⟨ ⟦swap⟧-natural ⟦ P ⟧ ⟦ Q ⟧ (⟦⟧-resp-✓ P) (⟦⟧-refl-✓ ⟳Q) (⟦⟧-resp-[] #Q) as ⟩
    (⟦swap⟧ {S} {U} ⟦⟫⟧ ⟦ Q ⟧ ⟦[&]⟧ ⟦ P ⟧) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ (swap-semantics {S} {U}) ([&]-semantics Q P) as) ⟩
    ⟦ swap {S} {U} ⟫ Q [&] P ⟧ as
  ∎

-- Coherence of swap with units

⟦swap⟧-⟦unit₁⟧ : ∀ {S} →
  ⟦swap⟧ {S} {I} ⟦⟫⟧ ⟦unit₁⟧ ≃ ⟦unit₂⟧
⟦swap⟧-⟦unit₁⟧ {S} as = cong₂ _++_ (I-η (back {S} as)) refl

swap-unit₁ : ∀ {S} →
  ⟦ swap {S} {I} ⟫ unit₁ ⟧ ≃ ⟦ unit₂ ⟧
swap-unit₁ {S} as =
  begin
    ⟦ swap {S} {I} ⟫ unit₁ ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ (swap-semantics {S}) unit₁-semantics as ⟩
    (⟦swap⟧ {S} {I} ⟦⟫⟧ ⟦unit₁⟧) as
  ≡⟨ ⟦swap⟧-⟦unit₁⟧ as ⟩
    ⟦unit₂⟧ as
  ≡⟨ sym (unit₂-semantics as) ⟩
    ⟦ unit₂ ⟧ as
  ∎

⟦swap⟧-⟦unit₂⟧ : ∀ {S} →
  ⟦swap⟧ {I} {S} ⟦⟫⟧ ⟦unit₂⟧ ≃ ⟦unit₁⟧
⟦swap⟧-⟦unit₂⟧ as = ++-β₁ as []

swap-unit₂ : ∀ {S} →
  ⟦ swap {I} {S} ⟫ unit₂ ⟧ ≃ ⟦ unit₁ ⟧
swap-unit₂ {S} as =
  begin
    ⟦ swap {I} {S} ⟫ unit₂ ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ (swap-semantics {I}) (unit₂-semantics {S}) as ⟩
    (⟦swap⟧ {I} {S} ⟦⟫⟧ ⟦unit₂⟧) as
  ≡⟨ ⟦swap⟧-⟦unit₂⟧ as ⟩
    ⟦unit₁⟧ as
  ≡⟨ sym (unit₁-semantics as) ⟩
    ⟦ unit₁ ⟧ as
  ∎

-- Coherence of swap with associators

⟦swap⟧-⟦assoc⟧ : ∀ {S T U} →
  ⟦assoc⟧ {S} {T} {U} ⟦⟫⟧ ⟦swap⟧ {S & T} {U} ⟦⟫⟧ ⟦assoc⟧ {U} {S} {T}
    ≃ ⟦done⟧ {S} ⟦[&]⟧ ⟦swap⟧ {T} {U} ⟦⟫⟧
        ⟦assoc⟧ {S} {U} {T} ⟦⟫⟧ ⟦swap⟧ {S} {U} ⟦[&]⟧ ⟦done⟧ {T}
⟦swap⟧-⟦assoc⟧ {S} {T} {U} as =
  begin
    ⟦assoc⟧ {U} {S} {T} (⟦swap⟧ {S & T} {U} ((as₁ ++ as₂) ++ as₃))
  ≡⟨ cong (⟦assoc⟧ {U} {S} {T}) (⟦swap⟧-++ (as₁ ++ as₂) as₃ ✓as₁₂/as₃≡[]) ⟩
    ⟦assoc⟧ {U} {S} {T} (as₃ ++ as₁ ++ as₂)
  ≡⟨ ⟦assoc⟧-++ as₃ as₁ as₂ ⟩
    (as₃ ++ as₁) ++ as₂
  ≡⟨ cong₂ _++_ (sym (⟦swap⟧-++ as₁ as₃ ✓as₁/as₃≡[])) refl ⟩
    ⟦swap⟧ {S} {U} (as₁ ++ as₃) ++ as₂
  ≡⟨ (sym (⟦[&]⟧-++ (⟦swap⟧ {S} {U}) ⟦done⟧ (⟦swap⟧-refl-✓ {S} {U}) (as₁ ++ as₃) as₂)) ⟩
    (⟦swap⟧ {S} {U} ⟦[&]⟧ ⟦done⟧ {T}) ((as₁ ++ as₃) ++ as₂)
  ≡⟨ cong (⟦swap⟧ {S} {U} ⟦[&]⟧ ⟦done⟧ {T}) (sym (⟦assoc⟧-++ as₁ as₃ as₂)) ⟩
    (⟦swap⟧ {S} {U} ⟦[&]⟧ ⟦done⟧ {T}) (⟦assoc⟧ {S} {U} {T} (as₁ ++ as₃ ++ as₂))
  ∎ where
  as₁ = front {S} as
  as₂ = front {T} (back {S} as)
  as₃ = back {T} (back {S} as)
  ✓as₁₂/as₃≡[] : as₁ ++ as₂ ✓ ⊎ as₃ ≡ []
  ✓as₁₂/as₃≡[] with ✓? as₁ | ✓? as₂
  ✓as₁₂/as₃≡[] | yes ✓as₁ | yes ✓as₂ = inj₁ (++-resp-✓ ✓as₁ ✓as₂)
  ✓as₁₂/as₃≡[] | _        | no ¬✓as₂ = inj₂ (back≡[] ¬✓as₂)
  ✓as₁₂/as₃≡[] | no ¬✓as₁ | _        = inj₂ (back-resp-[] {T} (back≡[] ¬✓as₁))
  ✓as₁/as₃≡[] : as₁ ✓ ⊎ as₃ ≡ []
  ✓as₁/as₃≡[] with ✓? as₁
  ✓as₁/as₃≡[] | yes ✓as₁ = inj₁ ✓as₁
  ✓as₁/as₃≡[] | no ¬✓as₁ = inj₂ (back-resp-[] {T} (back≡[] ¬✓as₁))

swap-assoc : ∀ {S T U} →
  ⟦ assoc {S} {T} {U} ⟫ swap {S & T} {U} ⟫ assoc {U} {S} {T} ⟧
    ≃ ⟦ done {S} [&] swap {T} {U} ⟫ assoc {S} {U} {T} ⟫ swap {S} {U} [&] done {T} ⟧
swap-assoc {S} {T} {U} as =
  begin
    ⟦ assoc {S} {T} {U} ⟫ swap {S & T} {U} ⟫ assoc {U} {S} {T} ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ (assoc-semantics {S} {T} {U})
       (⟫-≃-⟦⟫⟧ (swap-semantics {S & T} {U}) (assoc-semantics {U} {S} {T})) as ⟩
    (⟦assoc⟧ {S} {T} {U} ⟦⟫⟧ ⟦swap⟧ {S & T} {U} ⟦⟫⟧ ⟦assoc⟧ {U} {S} {T}) as
  ≡⟨ ⟦swap⟧-⟦assoc⟧ {S} {T} {U} as ⟩
    (⟦done⟧ {S} ⟦[&]⟧ ⟦swap⟧ {T} {U} ⟦⟫⟧
       ⟦assoc⟧ {S} {U} {T} ⟦⟫⟧ ⟦swap⟧ {S} {U} ⟦[&]⟧ ⟦done⟧ {T}) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ ([&]-≃-⟦[&]⟧ {P = done} (done-semantics {S}) (swap-semantics {T} {U}))
       (⟫-≃-⟦⟫⟧ (assoc-semantics {S} {U} {T})
         ([&]-≃-⟦[&]⟧ {Q = done} (swap-semantics {S} {U}) (done-semantics {T}))) as) ⟩
    ⟦ done {S} [&] swap {T} {U} ⟫ assoc {S} {U} {T} ⟫ swap {S} {U} [&] done {T} ⟧ as
  ∎

⟦swap⟧-⟦assoc⁻¹⟧ : ∀ {S T U} →
  ⟦assoc⁻¹⟧ {S} {T} {U} ⟦⟫⟧ ⟦swap⟧ {S} {T & U} ⟦⟫⟧ ⟦assoc⁻¹⟧ {T} {U} {S}
    ≃ ⟦swap⟧ {S} {T} ⟦[&]⟧ ⟦done⟧ {U} ⟦⟫⟧
        ⟦assoc⁻¹⟧ {T} {S} {U} ⟦⟫⟧ ⟦done⟧ {T} ⟦[&]⟧ ⟦swap⟧ {S} {U}
⟦swap⟧-⟦assoc⁻¹⟧ {S} {T} {U} as =
  begin
    ⟦assoc⁻¹⟧ {T} {U} {S} (⟦swap⟧ {S} {T & U} (as₁ ++ as₂ ++ as₃))
  ≡⟨ cong (⟦assoc⁻¹⟧ {T} {U} {S}) (⟦swap⟧-++ as₁ (as₂ ++ as₃) ✓as₁/as₂₃≡[]) ⟩
    ⟦assoc⁻¹⟧ {T} {U} {S} ((as₂ ++ as₃) ++ as₁)
  ≡⟨ ⟦assoc⁻¹⟧-++ as₂ as₃ as₁ ⟩
    as₂ ++ as₃ ++ as₁
  ≡⟨ cong (_++_ as₂) (sym (⟦swap⟧-++ as₁ as₃ ✓as₁/as₃≡[])) ⟩
    as₂ ++ ⟦swap⟧ {S} {U} (as₁ ++ as₃)
  ≡⟨ sym (⟦[&]⟧-++ (⟦done⟧ {T}) (⟦swap⟧ {S} {U}) (λ cs → λ ✓cs → ✓cs) as₂ (as₁ ++ as₃)) ⟩
    (⟦done⟧ {T} ⟦[&]⟧ ⟦swap⟧ {S} {U}) (as₂ ++ as₁ ++ as₃)
  ≡⟨ cong (⟦done⟧ {T} ⟦[&]⟧ ⟦swap⟧ {S} {U}) (sym (⟦assoc⁻¹⟧-++ as₂ as₁ as₃)) ⟩
    (⟦done⟧ {T} ⟦[&]⟧ ⟦swap⟧ {S} {U}) (⟦assoc⁻¹⟧ {T} {S} {U} ((as₂ ++ as₁) ++ as₃))
  ∎ where
  as₁ = front {S} (front {S & T} as)
  as₂ = back {S} (front {S & T} as)
  as₃ = back {S & T} as
  ✓as₁/as₂₃≡[] : as₁ ✓ ⊎ as₂ ++ as₃ ≡ []
  ✓as₁/as₂₃≡[] with ✓? as₁
  ✓as₁/as₂₃≡[] | yes ✓as₁ = inj₁ ✓as₁
  ✓as₁/as₂₃≡[] | no ¬✓as₁ = inj₂ (++-resp-[] (back≡[] ¬✓as₁) (back≡[] (λ ✓as₁₂ → ¬✓as₁ (front-resp-✓ ✓as₁₂))))
  ✓as₁/as₃≡[] : as₁ ✓ ⊎ as₃ ≡ []
  ✓as₁/as₃≡[] with ✓? as₁
  ✓as₁/as₃≡[] | yes ✓as₁ = inj₁ ✓as₁
  ✓as₁/as₃≡[] | no ¬✓as₁ = inj₂ (back≡[] (λ ✓as₁₂ → ¬✓as₁ (front-resp-✓ ✓as₁₂)))

swap-assoc⁻¹ : ∀ {S T U} →
  ⟦ assoc⁻¹ {S} {T} {U} ⟫ swap {S} {T & U} ⟫ assoc⁻¹ {T} {U} {S} ⟧
    ≃ ⟦ swap {S} {T} [&] done {U} ⟫ assoc⁻¹ {T} {S} {U} ⟫ done {T} [&] swap {S} {U} ⟧
swap-assoc⁻¹ {S} {T} {U} as =
  begin
    ⟦ assoc⁻¹ {S} {T} {U} ⟫ swap {S} {T & U} ⟫ assoc⁻¹ {T} {U} {S} ⟧ as
  ≡⟨ ⟫-≃-⟦⟫⟧ (assoc⁻¹-semantics {S} {T} {U})
       (⟫-≃-⟦⟫⟧ (swap-semantics {S} {T & U}) (assoc⁻¹-semantics {T} {U} {S})) as ⟩
    (⟦assoc⁻¹⟧ {S} {T} {U} ⟦⟫⟧ ⟦swap⟧ {S} {T & U} ⟦⟫⟧ ⟦assoc⁻¹⟧ {T} {U} {S}) as
  ≡⟨ ⟦swap⟧-⟦assoc⁻¹⟧ {S} {T} {U} as ⟩
    (⟦swap⟧ {S} {T} ⟦[&]⟧ ⟦done⟧ {U} ⟦⟫⟧
      ⟦assoc⁻¹⟧ {T} {S} {U} ⟦⟫⟧ ⟦done⟧ {T} ⟦[&]⟧ ⟦swap⟧ {S} {U}) as
  ≡⟨ sym (⟫-≃-⟦⟫⟧ ([&]-≃-⟦[&]⟧ {Q = done} (swap-semantics {S} {T}) (done-semantics {U}))
       (⟫-≃-⟦⟫⟧ (assoc⁻¹-semantics {T} {S} {U})
         ([&]-≃-⟦[&]⟧ {P = done} (done-semantics {T}) (swap-semantics {S} {U}))) as) ⟩
    ⟦ swap {S} {T} [&] done {U} ⟫ assoc⁻¹ {T} {S} {U} ⟫ done {T} [&] swap {S} {U} ⟧ as
  ∎

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
{-# OPTIONS --cubical --no-import-sorts #-}

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

module Number.Inclusions where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base -- Rel

-- open import Data.Nat.Base using (ℕ) renaming (_≤_ to _≤ₙ_)
open import Cubical.Data.Nat using (ℕ; zero; suc) renaming (_+_ to _+ₙ_)
open import Cubical.Data.Nat.Order renaming (zero-≤ to z≤n; suc-≤-suc to s≤s; _≤_ to _≤ₙ_; _<_ to _<ₙ_)

open import Cubical.Data.Unit.Base -- Unit
open import Cubical.Data.Empty -- ⊥
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
open import Cubical.Data.Maybe.Base

-- open import Number.Structures ℝℓ ℝℓ'
open import Number.Bundles

-- Finₖ ℕ ℤ ℚ ℚ₀⁺ ℚ⁺ ℝ ℝ₀⁺ ℝ⁺
record IsRLatticeInclusion
  {ℓ ℓ' ℓₚ ℓₚ'}
  (F : RLattice {ℓ} {ℓₚ}) (G : RLattice {ℓ'} {ℓₚ'})
  (f : (RLattice.Carrier F) → (RLattice.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  private
    module F = RLattice F
    module G = RLattice G
  field
    -- injectivity? might follow from preserves-#?
    reflects-≡    : ∀ x y → f x   ≡ f y →   x ≡     y
    -- lattice
    preserves-<   : ∀ x y →   x F.<   y → f x G.< f y
    preserves-≤   : ∀ x y →   x F.≤   y → f x G.≤ f y
    preserves-#   : ∀ x y →   x F.#   y → f x G.# f y
    reflects-<    : ∀ x y → f x G.< f y →   x F.<   y
    reflects-≤    : ∀ x y → f x G.≤ f y →   x F.≤   y
    reflects-#    : ∀ x y → f x G.# f y →   x F.#   y
    preserves-min : ∀ x y → f (F.min x y) ≡ G.min (f x) (f y)
    preserves-max : ∀ x y → f (F.max x y) ≡ G.max (f x) (f y)

-- ℕ ℤ ℚ ℚ₀⁺ ℚ⁺ ℝ ℝ₀⁺ ℝ⁺
-- ring without additive inverse
record IsROrderedCommSemiringInclusion
  {ℓ ℓ' ℓₚ ℓₚ'}
  (F : ROrderedCommSemiring {ℓ} {ℓₚ}) (G : ROrderedCommSemiring {ℓ'} {ℓₚ'})
  (f : (ROrderedCommSemiring.Carrier F) → (ROrderedCommSemiring.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  private
    module F = ROrderedCommSemiring F
    module G = ROrderedCommSemiring G
  field
    isRLatticeInclusion : IsRLatticeInclusion (record {F}) (record {G}) f
    preserves-0   :         f  F.0f       ≡ G.0f
    preserves-1   :         f  F.1f       ≡ G.1f
    preserves-+   : ∀ x y → f (x F.+ y)   ≡ f x G.+  f y
    preserves-·   : ∀ x y → f (x F.· y)   ≡ f x G.·  f y
  open IsRLatticeInclusion isRLatticeInclusion public

  preserves-#0 : ∀ x →   x  F.# F.0f → f x  G.# G.0f
  preserves-0≤ : ∀ x → F.0f F.≤   x  → G.0f G.≤ f x
  preserves-0< : ∀ x → F.0f F.<   x  → G.0f G.< f x
  preserves-<0 : ∀ x →   x  F.< F.0f → f x  G.< G.0f
  preserves-≤0 : ∀ x →   x  F.≤ F.0f → f x  G.≤ G.0f

  preserves-#0 x q = transport (λ i → f x G.# preserves-0 i) (preserves-# _ _ q)
  preserves-0≤ x q = transport (λ i → preserves-0 i G.≤ f x) (preserves-≤ _ _ q)
  preserves-0< x q = transport (λ i → preserves-0 i G.< f x) (preserves-< _ _ q)
  preserves-<0 x q = transport (λ i → f x G.< preserves-0 i) (preserves-< _ _ q)
  preserves-≤0 x q = transport (λ i → f x G.≤ preserves-0 i) (preserves-≤ _ _ q)

-- ℤ ℚ ℝ
record IsROrderedCommRingInclusion
  {ℓ ℓ' ℓₚ ℓₚ'}
  (F : ROrderedCommRing {ℓ} {ℓₚ}) (G : ROrderedCommRing {ℓ'} {ℓₚ'})
  (f : (ROrderedCommRing.Carrier F) → (ROrderedCommRing.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  private
    module F = ROrderedCommRing F
    module G = ROrderedCommRing G
  field
    isROrderedCommSemiringInclusion : IsROrderedCommSemiringInclusion (record {F}) (record {G}) f
    preserves-    : ∀ x   → f (  F.- x)   ≡     G.- (f x)
  open IsROrderedCommSemiringInclusion isROrderedCommSemiringInclusion public

-- ℚ ℝ
record IsROrderedFieldInclusion
  {ℓ ℓ' ℓₚ ℓₚ'}
  (F : ROrderedField {ℓ} {ℓₚ}) (G : ROrderedField {ℓ'} {ℓₚ'})
  (f : (ROrderedField.Carrier F) → (ROrderedField.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  private
    module F = ROrderedField F
    module G = ROrderedField G
  field
    isROrderedCommRingInclusion : IsROrderedCommRingInclusion (record {F}) (record {G}) f
    preserves-⁻¹  : ∀ x → (p : x F.# F.0f) → (q : f x G.# G.0f) → f (F._⁻¹ x {{p}}) ≡ G._⁻¹ (f x) {{q}}
  open IsROrderedCommRingInclusion isROrderedCommRingInclusion public

-- ℚ ℝ ℂ
record IsRFieldInclusion
  {ℓ ℓ' ℓₚ ℓₚ'}
  (F : RField {ℓ} {ℓₚ}) (G : RField {ℓ'} {ℓₚ'})
  (f : (RField.Carrier F) → (RField.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  private
    module F = RField F
    module G = RField G
  field
    -- CommSemiringInclusion
    preserves-0   :         f  F.0f       ≡ G.0f
    preserves-1   :         f  F.1f       ≡ G.1f
    preserves-+   : ∀ x y → f (x F.+ y)   ≡ f x G.+  f y
    preserves-·   : ∀ x y → f (x F.· y)   ≡ f x G.·  f y
    -- other
    reflects-≡    : ∀ x y → f x   ≡ f y →   x ≡     y
    preserves-#   : ∀ x y →   x F.#   y → f x G.# f y
    reflects-#    : ∀ x y → f x G.# f y →   x F.#   y
    -- TODO: properties

  preserves-#0 : ∀ x →   x  F.# F.0f → f x  G.# G.0f
  preserves-#0 x q = transport (λ i → f x G.# preserves-0 i) (preserves-# _ _ q)

-- ℕ ℤ ℚ ℝ ℂ
record IsRCommSemiringInclusion
  {ℓ ℓ' ℓₚ ℓₚ'}
  (F : RCommSemiring {ℓ} {ℓₚ}) (G : RCommSemiring {ℓ'} {ℓₚ'})
  (f : (RCommSemiring.Carrier F) → (RCommSemiring.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  private
    module F = RCommSemiring F
    module G = RCommSemiring G
  field
    -- CommSemiringInclusion
    preserves-0   :         f  F.0f       ≡ G.0f
    preserves-1   :         f  F.1f       ≡ G.1f
    preserves-+   : ∀ x y → f (x F.+ y)   ≡ f x G.+  f y
    preserves-·   : ∀ x y → f (x F.· y)   ≡ f x G.·  f y
    -- other
    reflects-≡    : ∀ x y → f x   ≡ f y →   x ≡     y
    preserves-#   : ∀ x y →   x F.#   y → f x G.# f y
    reflects-#    : ∀ x y → f x G.# f y →   x F.#   y
    -- TODO: properties

-- ℤ ℚ ℝ ℂ
record IsRCommRingInclusion
  {ℓ ℓ' ℓₚ ℓₚ'}
  (F : RCommRing {ℓ} {ℓₚ}) (G : RCommRing {ℓ'} {ℓₚ'})
  (f : (RCommRing.Carrier F) → (RCommRing.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  private
    module F = RCommRing F
    module G = RCommRing G
  field
    -- CommSemiringInclusion
    preserves-0   :         f  F.0f       ≡ G.0f
    preserves-1   :         f  F.1f       ≡ G.1f
    preserves-+   : ∀ x y → f (x F.+ y)   ≡ f x G.+  f y
    preserves-·   : ∀ x y → f (x F.· y)   ≡ f x G.·  f y
    -- other
    reflects-≡    : ∀ x y → f x   ≡ f y →   x ≡     y
    preserves-#   : ∀ x y →   x F.#   y → f x G.# f y
    reflects-#    : ∀ x y → f x G.# f y →   x F.#   y
    -- TODO: properties

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.Kernel where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Algebra.CommRing.Base
open import Cubical.Algebra.CommRing.Ideal using (Ideal→CommIdeal)
open import Cubical.Algebra.Ring.Kernel using () renaming (kernelIdeal to ringKernel)
open import Cubical.Algebra.CommAlgebra.Base
open import Cubical.Algebra.CommAlgebra.Properties
open import Cubical.Algebra.CommAlgebra.Ideal

private
  variable
    ℓ : Level

module _ {R : CommRing ℓ} (A B : CommAlgebra R ℓ) (ϕ : CommAlgebraHom A B) where

  kernel : IdealsIn A
  kernel = Ideal→CommIdeal (ringKernel (CommAlgebraHom→RingHom {A = A} {B = B} ϕ))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Prelude.Ord.Reasoning where

open import Prelude.Equality
open import Prelude.Ord
open import Prelude.Function

module _ {a} {A : Set a} {{OrdA : Ord/Laws A}} where

  private
    lt/leq-trans : ∀ {x y z : A} → x < y → y ≤ z → x < z
    lt/leq-trans x<y y≤z =
      case leq-to-lteq {A = A} y≤z of λ where
        (less  y<z)  → less-trans {A = A} x<y y<z
        (equal refl) → x<y

    leq/lt-trans : ∀ {x y z : A} → x ≤ y → y < z → x < z
    leq/lt-trans x≤y y<z =
      case leq-to-lteq {A = A} x≤y of λ where
        (less  x<y)  → less-trans {A = A} x<y y<z
        (equal refl) → y<z

  data _≲_ (x y : A) : Set a where
    strict    : x < y → x ≲ y
    nonstrict : x ≤ y → x ≲ y

  module _ {x y : A} where
    OrdProof : x ≲ y → Set a
    OrdProof (strict    _) = x < y
    OrdProof (nonstrict _) = x ≤ y

    infix -1 ordProof_
    ordProof_ : (p : x ≲ y) → OrdProof p
    ordProof strict    p = p
    ordProof nonstrict p = p

  infixr 0 eqOrdStep ltOrdStep leqOrdStep
  infix  1 _∎Ord

  syntax eqOrdStep x q p = x ≡[ p ] q
  eqOrdStep : ∀ (x : A) {y z} → y ≲ z → x ≡ y → x ≲ z
  x ≡[ x=y ] strict    y<z = strict    (case x=y of λ where refl → y<z)
  x ≡[ x=y ] nonstrict y≤z = nonstrict (case x=y of λ where refl → y≤z)
    -- ^ Note: don't match on the proof here, we need to decide strict vs nonstrict for neutral proofs

  syntax eqOrdStepʳ x q p = x ≡[ p ]ʳ q
  eqOrdStepʳ : ∀ (x : A) {y z} → y ≲ z → y ≡ x → x ≲ z
  x ≡[ y=x ]ʳ strict    y<z = strict    (case y=x of λ where refl → y<z)
  x ≡[ y=x ]ʳ nonstrict y≤z = nonstrict (case y=x of λ where refl → y≤z)

  syntax ltOrdStep x q p = x <[ p ] q
  ltOrdStep : ∀ (x : A) {y z} → y ≲ z → x < y → x ≲ z
  x <[ x<y ] strict    y<z = strict (less-trans {A = A} x<y y<z)
  x <[ x<y ] nonstrict y≤z = strict (lt/leq-trans x<y y≤z)

  syntax leqOrdStep x q p = x ≤[ p ] q
  leqOrdStep : ∀ (x : A) {y z} → y ≲ z → x ≤ y → x ≲ z
  x ≤[ x≤y ] strict    y<z = strict    (leq/lt-trans x≤y y<z)
  x ≤[ x≤y ] nonstrict y≤z = nonstrict (leq-trans {A = A} x≤y y≤z)

  _∎Ord : ∀ (x : A) → x ≲ x
  x ∎Ord = nonstrict (eq-to-leq {A = A} refl)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module ModuleInfix where

open import Data.List using (List; _∷_; [])
open import Data.Bool using (Bool; true; false)

module Sort(A : Set)(_≤_ : A → A → Bool)(_⊝_ : A → A → A)(zero : A) where

  infix 1 _≤_
  infix 2 _⊝_

  insert : A → List A → List A
  insert x [] = x ∷ []
  insert x (y ∷ ys) with zero ≤ (y ⊝ x)
  insert x (y ∷ ys)    | true  = x ∷ y ∷ ys
  insert x (y ∷ ys)    | false = y ∷ insert x ys

  sort : List A → List A
  sort []       = []
  sort (x ∷ xs) = insert x (sort xs)


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

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
module Optics.All where
  open import Optics.Functorial public
  open import Optics.Reflection public

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; cong)

open import Syntax
import Renaming

-- Substitutions
module Substitution where

  module _ {𝕊 : Signature} where

    open Expression 𝕊
    open Renaming
    open Equality

    infix 5 _∥_→ˢ_

    -- the set of substitutions
    _∥_→ˢ_ : MShape → VShape → VShape → Set
    𝕄 ∥ γ →ˢ δ = var γ → ExprTm 𝕄 δ

    -- equality of substitutions

    infix 4 _≈ˢ_

    _≈ˢ_ : ∀ {𝕄} {γ δ} (σ : 𝕄 ∥ γ →ˢ δ) (σ : 𝕄 ∥ γ →ˢ δ) → Set
    σ ≈ˢ τ = ∀ x → σ x ≈ τ x

    -- equality is an equivalence relation

    ≈ˢ-refl : ∀ {𝕄} {γ δ} {σ : 𝕄 ∥ γ →ˢ δ} → σ ≈ˢ σ
    ≈ˢ-refl x = ≈-refl

    ≈ˢ-sym : ∀ {𝕄} {γ δ} {σ τ : 𝕄 ∥ γ →ˢ δ} → σ ≈ˢ τ → τ ≈ˢ σ
    ≈ˢ-sym ξ x = ≈-sym (ξ x)

    ≈ˢ-trans : ∀ {𝕄} {γ δ} {σ τ χ : 𝕄 ∥ γ →ˢ δ} → σ ≈ˢ τ → τ ≈ˢ χ → σ ≈ˢ χ
    ≈ˢ-trans ζ ξ x = ≈-trans (ζ x) (ξ x)

    -- identity substitution
    𝟙ˢ : ∀ {𝕄} {γ} → 𝕄 ∥ γ →ˢ γ
    𝟙ˢ = expr-var

    -- inclusions

    inlˢ : ∀ {𝕄} {γ δ} → 𝕄 ∥ γ →ˢ γ ⊕ δ
    inlˢ x = expr-var (var-left x)

    inrˢ : ∀ {𝕄} {γ δ} → 𝕄 ∥ δ →ˢ γ ⊕ δ
    inrˢ x = expr-var (var-right x)

    -- join of substitutions

    [_,_]ˢ : ∀ {𝕄} {γ δ η} → (𝕄 ∥ γ →ˢ η) → (𝕄 ∥ δ →ˢ η) → (𝕄 ∥ γ ⊕ δ →ˢ η)
    [ ξ , σ ]ˢ (var-left x) = ξ x
    [ ξ , σ ]ˢ (var-right y) = σ y

    -- join respect equality

    [,]ˢ-resp-≈ˢ : ∀ {𝕄} {γ δ η} {ρ₁ ρ₂ : 𝕄 ∥ γ →ˢ η} {τ₁ τ₂ : 𝕄 ∥ δ →ˢ η} →
                 ρ₁ ≈ˢ ρ₂ → τ₁ ≈ˢ τ₂ → [ ρ₁ , τ₁ ]ˢ ≈ˢ [ ρ₂ , τ₂ ]ˢ
    [,]ˢ-resp-≈ˢ ζ ξ (var-left x) = ζ x
    [,]ˢ-resp-≈ˢ ζ ξ (var-right y) = ξ y

    -- substutution extension

    ⇑ˢ : ∀ {𝕄} {γ δ η} → (𝕄 ∥ γ →ˢ δ) → (𝕄 ∥ γ ⊕ η →ˢ δ ⊕ η)
    ⇑ˢ σ (var-left x) = [ var-left ]ʳ σ x
    ⇑ˢ σ (var-right y) = expr-var (var-right y)

    -- extension preserves equality

    ⇑ˢ-resp-≈ˢ : ∀ {𝕄} {γ δ η} {σ τ : 𝕄 ∥ γ →ˢ δ} → σ ≈ˢ τ → ⇑ˢ {η = η} σ ≈ˢ ⇑ˢ τ
    ⇑ˢ-resp-≈ˢ ξ (var-left x) = []ʳ-resp-≈ var-left (ξ x)
    ⇑ˢ-resp-≈ˢ ξ (var-right y) = ≈-refl

    -- extension preserves identity

    ⇑ˢ-𝟙ˢ : ∀ {𝕄} {γ δ} → ⇑ˢ 𝟙ˢ ≈ˢ 𝟙ˢ {𝕄 = 𝕄} {γ = γ ⊕ δ}
    ⇑ˢ-𝟙ˢ (var-left x) = ≈-refl
    ⇑ˢ-𝟙ˢ (var-right x) = ≈-refl

    -- action of a substitution

    infix 5 [_]ˢ_

    [_]ˢ_ : ∀ {cl 𝕄} {γ δ} → (𝕄 ∥ γ →ˢ δ) → Expr cl 𝕄 γ → Expr cl 𝕄 δ
    [ σ ]ˢ (expr-var x) =  σ x
    [ σ ]ˢ (expr-symb S es) = expr-symb S (λ i → [ ⇑ˢ σ ]ˢ es i)
    [ σ ]ˢ (expr-meta M ts) = expr-meta M (λ i → [ σ ]ˢ ts i )
    [ σ ]ˢ expr-eqty = expr-eqty
    [ σ ]ˢ expr-eqtm = expr-eqtm

    -- the action respects equality

    []ˢ-resp-≈ : ∀ {cl 𝕄} {γ δ} (σ : 𝕄 ∥ γ →ˢ δ) {t u : Expr cl 𝕄 γ} → t ≈ u → [ σ ]ˢ t ≈ [ σ ]ˢ u
    []ˢ-resp-≈ σ (≈-≡ ξ) = ≈-≡ (cong ([ σ ]ˢ_) ξ)
    []ˢ-resp-≈ σ (≈-symb ξ) = ≈-symb (λ i → []ˢ-resp-≈ (⇑ˢ σ) (ξ i))
    []ˢ-resp-≈ σ (≈-meta ξ) = ≈-meta (λ i → []ˢ-resp-≈ σ (ξ i))

    []ˢ-resp-≈ˢ : ∀ {cl 𝕄} {γ δ} {σ τ : 𝕄 ∥ γ →ˢ δ} → σ ≈ˢ τ → ∀ (t : Expr cl 𝕄 γ) → [ σ ]ˢ t ≈ [ τ ]ˢ t
    []ˢ-resp-≈ˢ ξ (expr-var x) = ξ x
    []ˢ-resp-≈ˢ ξ (expr-symb S es) = ≈-symb (λ i → []ˢ-resp-≈ˢ (⇑ˢ-resp-≈ˢ ξ) (es i))
    []ˢ-resp-≈ˢ ξ (expr-meta M ts) = ≈-meta (λ i → []ˢ-resp-≈ˢ ξ (ts i))
    []ˢ-resp-≈ˢ ξ expr-eqty = ≈-eqty
    []ˢ-resp-≈ˢ ξ expr-eqtm = ≈-eqtm

    []ˢ-resp-≈ˢ-≈ : ∀ {cl 𝕄} {γ δ} {σ τ : 𝕄 ∥ γ →ˢ δ} {t u : Expr cl 𝕄 γ} → σ ≈ˢ τ → t ≈ u → [ σ ]ˢ t ≈ [ τ ]ˢ u
    []ˢ-resp-≈ˢ-≈ {τ = τ} {t = t} ζ ξ = ≈-trans ([]ˢ-resp-≈ˢ ζ t) ([]ˢ-resp-≈ τ ξ)

    -- composition of substitutions

    infixl 7 _∘ˢ_

    _∘ˢ_ : ∀ {𝕄} {γ δ η} → (𝕄 ∥ δ →ˢ η) → (𝕄 ∥ γ →ˢ δ) → (𝕄 ∥ γ →ˢ η)
    (ξ ∘ˢ σ) x = [ ξ ]ˢ (σ x)

    -- sum of substitutions

    infixl 8 _⊕ˢ_

    _⊕ˢ_ : ∀ {𝕄} {γ δ η χ} → (𝕄 ∥ γ →ˢ δ) → (𝕄 ∥ η →ˢ χ) → (𝕄 ∥ γ ⊕ η →ˢ δ ⊕ χ)
    σ ⊕ˢ τ = [ inlˢ ∘ˢ σ , inrˢ ∘ˢ τ  ]ˢ

    -- composition of renaming and substitition

    infixr 7 _ʳ∘ˢ_

    _ʳ∘ˢ_ : ∀ {𝕄} {γ δ η} → (δ →ʳ η) → (𝕄 ∥ γ →ˢ δ) → (𝕄 ∥ γ →ˢ η)
    (ρ ʳ∘ˢ σ) x = [ ρ ]ʳ σ x

    infixl 7 _ˢ∘ʳ_

    _ˢ∘ʳ_ : ∀ {𝕄} {γ δ η} → (𝕄 ∥ δ →ˢ η) → (γ →ʳ δ) → (𝕄 ∥ γ →ˢ η)
    (σ ˢ∘ʳ ρ) x =  σ (ρ x)

    -- extension commutes with the composition of renaming and substitution

    ⇑ˢ-resp-ʳ∘ˢ : ∀ {𝕄} {γ δ η θ} {ρ : δ →ʳ η} → {σ : 𝕄 ∥ γ →ˢ δ} →
                  ⇑ˢ {η = θ} (ρ ʳ∘ˢ σ) ≈ˢ ⇑ʳ ρ ʳ∘ˢ ⇑ˢ σ
    ⇑ˢ-resp-ʳ∘ˢ {σ = σ} (var-left x) =
      ≈-trans
        (≈-sym ([∘ʳ] (σ x)))
        (≈-trans
           ([]ʳ-resp-≡ʳ (σ x) ≡ʳ-refl)
           ([∘ʳ] (σ x)))
    ⇑ˢ-resp-ʳ∘ˢ (var-right y) = ≈-refl

    ⇑ˢ-resp-ˢ∘ʳ : ∀ {𝕄} {β γ δ η} {ρ : β →ʳ γ} {σ : 𝕄 ∥ γ →ˢ δ} → ⇑ˢ {η = η} (σ ˢ∘ʳ ρ) ≈ˢ ⇑ˢ σ ˢ∘ʳ ⇑ʳ ρ
    ⇑ˢ-resp-ˢ∘ʳ (var-left x) = ≈-refl
    ⇑ˢ-resp-ˢ∘ʳ (var-right y) = ≈-refl

    ⇑ˢ-ʳ∘ˢ : ∀ {𝕄} {β γ δ η} {σ : 𝕄 ∥ β →ˢ γ} {ρ : γ →ʳ δ} → ⇑ˢ {η = η} (ρ ʳ∘ˢ σ) ≈ˢ ⇑ʳ ρ ʳ∘ˢ ⇑ˢ σ
    ⇑ˢ-ʳ∘ˢ (var-left x) = ≈-trans (≈-trans (≈-sym ([∘ʳ] _)) ([]ʳ-resp-≡ʳ _ λ x → refl)) ([∘ʳ] _)
    ⇑ˢ-ʳ∘ˢ (var-right x) = ≈-refl

    -- action of a composition of a renaming and a substitition

    [ˢ∘ʳ] : ∀ {𝕄 cl} {γ δ η} → {σ : 𝕄 ∥ δ →ˢ η} → {ρ : γ →ʳ δ} (t : Expr cl 𝕄 γ) → [ σ ˢ∘ʳ ρ ]ˢ t  ≈ [ σ ]ˢ [ ρ ]ʳ t
    [ˢ∘ʳ] (expr-var x) = ≈-refl
    [ˢ∘ʳ] (expr-symb S es) = ≈-symb (λ i → ≈-trans ([]ˢ-resp-≈ˢ ⇑ˢ-resp-ˢ∘ʳ (es i)) ([ˢ∘ʳ] (es i)))
    [ˢ∘ʳ] (expr-meta M ts) = ≈-meta (λ i → [ˢ∘ʳ] (ts i))
    [ˢ∘ʳ] expr-eqty = ≈-eqty
    [ˢ∘ʳ] expr-eqtm = ≈-eqtm

    [ʳ∘ˢ] : ∀ {𝕄 cl} {γ δ η} → {σ : 𝕄 ∥ γ →ˢ δ} → {ρ : δ →ʳ η} (t : Expr cl 𝕄 γ) → [ ρ ʳ∘ˢ σ ]ˢ t ≈ [ ρ ]ʳ ([ σ ]ˢ  t)
    [ʳ∘ˢ] (expr-var x) = ≈-refl
    [ʳ∘ˢ] (expr-symb S es) = ≈-symb (λ i → ≈-trans ([]ˢ-resp-≈ˢ ⇑ˢ-ʳ∘ˢ (es i)) ([ʳ∘ˢ] (es i)))
    [ʳ∘ˢ] (expr-meta M ts) = ≈-meta (λ i → [ʳ∘ˢ] (ts i))
    [ʳ∘ˢ] expr-eqty = ≈-eqty
    [ʳ∘ˢ] expr-eqtm = ≈-eqtm

    -- composition commutes with extensions

    ⇑ˢ-resp-∘ˢ : ∀ {𝕄} {β γ δ η} {σ : 𝕄 ∥ β →ˢ γ} {τ : 𝕄 ∥ γ →ˢ δ} → ⇑ˢ {η = η} (τ ∘ˢ σ) ≈ˢ ⇑ˢ τ ∘ˢ ⇑ˢ σ
    ⇑ˢ-resp-∘ˢ {σ = σ} (var-left x) = ≈-trans (≈-trans (≈-sym ([ʳ∘ˢ] (σ x))) ([]ˢ-resp-≈ˢ (λ x₁ → ≈-refl) (σ x))) ([ˢ∘ʳ] (σ x))
    ⇑ˢ-resp-∘ˢ (var-right y) = ≈-refl

    -- action of substitutions is functorial

    [𝟙ˢ] : ∀ {cl 𝕄 γ} (t : Expr cl 𝕄 γ) → [ 𝟙ˢ ]ˢ t ≈ t
    [𝟙ˢ] (expr-var x) = ≈-refl
    [𝟙ˢ] (expr-symb S es) = ≈-symb (λ i → ≈-trans ([]ˢ-resp-≈ˢ ⇑ˢ-𝟙ˢ (es i)) ([𝟙ˢ] (es i)))
    [𝟙ˢ] (expr-meta M ts) = ≈-meta (λ i → [𝟙ˢ] (ts i))
    [𝟙ˢ] expr-eqty = ≈-eqty
    [𝟙ˢ] expr-eqtm = ≈-eqtm

    [∘ˢ] : ∀ {cl 𝕄} {γ δ η} {σ : 𝕄 ∥ γ →ˢ δ} {τ : 𝕄 ∥ δ →ˢ η} (t : Expr cl 𝕄 γ) → [ τ ∘ˢ σ ]ˢ t ≈ [ τ ]ˢ [ σ ]ˢ t
    [∘ˢ] (expr-var x) = ≈-refl
    [∘ˢ] (expr-symb S es) = ≈-symb (λ i → ≈-trans ([]ˢ-resp-≈ˢ ⇑ˢ-resp-∘ˢ (es i)) ([∘ˢ] (es i)))
    [∘ˢ] (expr-meta M ts) = ≈-meta (λ i → [∘ˢ] (ts i))
    [∘ˢ] expr-eqty = ≈-eqty
    [∘ˢ] expr-eqtm = ≈-eqtm

    []ˢ-id : ∀ {cl 𝕄 γ} {σ : 𝕄 ∥ γ →ˢ γ} {t : Expr cl 𝕄 γ} → σ ≈ˢ 𝟙ˢ → [ σ ]ˢ t ≈ t
    []ˢ-id {t = t} ξ = ≈-trans ([]ˢ-resp-≈ˢ ξ t) ([𝟙ˢ] t)

    []ˢ-𝟘-initial : ∀ {cl 𝕄 γ} {σ : 𝕄 ∥ γ →ˢ 𝟘} (t : Expr cl 𝕄 𝟘) → [ σ ]ˢ [ 𝟘-initial ]ʳ t ≈ t
    []ˢ-𝟘-initial (expr-symb S es) =
      ≈-symb (λ i → ≈-trans (≈-sym ([ˢ∘ʳ] (es i))) ([]ˢ-id (λ {(var-right x) → ≈-refl})))
    []ˢ-𝟘-initial (expr-meta M ts) = ≈-meta (λ i → []ˢ-𝟘-initial (ts i))
    []ˢ-𝟘-initial expr-eqty = ≈-eqty
    []ˢ-𝟘-initial expr-eqtm = ≈-eqtm

  infix 5 _%_∥_→ˢ_
  _%_∥_→ˢ_ : ∀ (𝕊 : Signature) → MShape → VShape → VShape → Set
  _%_∥_→ˢ_ 𝕊 = _∥_→ˢ_ {𝕊 = 𝕊}


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

--
-- This module defines/proves some basic functions/theorem using only
-- the induction principle of the equality types the way they are done
-- in the HoTT book.  The functions defined/theorems proved in this
-- module is often exposed in a better way from the main equality
-- module, the word better means simpler definitions/proofs.  This
-- module is thus not meant for use in "production" hott.
--

module hott.core.equality.induction-proofs where

open import hott.core

-- The symmetry of ≡ defined in terms of the induction principle
sym : ∀{ℓ} {A : Type ℓ} {x y : A}
    → x ≡ y → y ≡ x
sym {ℓ} {A}  = induction≡ D d
  where
    D : {u v : A} → u ≡ v → Type ℓ
    D {u} {v} _ = v ≡ u
    d : {u : A} → D {u} refl
    d  = refl

-- The transitivity of ≡.
trans : ∀{ℓ} {A : Type ℓ} {x y z : A}
      → x ≡ y → y ≡ z → x ≡ z
trans {ℓ} {A} xEy = induction≡ D d xEy
  where
    D : {u v : A} → u ≡ v → Type ℓ
    D {u} {v} _ = {w : A} → v ≡ w → u ≡ w

    d : {u : A} → D {u} refl
    d uEw = uEw

symIsInv : ∀{ℓ} {A : Type ℓ} {x y : A}
         → (p : x ≡ y) → sym p ≡ p ⁻¹
symIsInv refl = refl

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


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

module rational-numbers where

import integers
open integers public

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

{- We introduce the type of non-zero integers. -}

ℤ\0 : UU lzero
ℤ\0 = Σ ℤ (λ k → ¬ (Id zero-ℤ k))

int-ℤ\0 : ℤ\0 → ℤ
int-ℤ\0 = pr1

{- We first show that multiplication by a non-zero integer is an injective
   function. -}

mul-ℤ-ℤ\0 : ℤ → ℤ\0 → ℤ
mul-ℤ-ℤ\0 x y = mul-ℤ x (int-ℤ\0 y)

mul-ℤ\0 : ℤ\0 → ℤ\0 → ℤ\0
mul-ℤ\0 (pair x Hx) (pair y Hy) = pair (mul-ℤ x y) (neq-zero-mul-ℤ x y Hx Hy)

postulate is-emb-mul-ℤ-ℤ\0 : (y : ℤ\0) → is-emb (λ x → mul-ℤ-ℤ\0 x y)

is-injective-mul-ℤ-ℤ\0 :
  (y : ℤ\0) (x1 x2 : ℤ) → Id (mul-ℤ-ℤ\0 x1 y) (mul-ℤ-ℤ\0 x2 y) → Id x1 x2
is-injective-mul-ℤ-ℤ\0 y x1 x2 = inv-is-equiv (is-emb-mul-ℤ-ℤ\0 y x1 x2)

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

{- We introduce the prerational numbers. -}

ℚ' : UU lzero
ℚ' = ℤ × ℤ\0

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

{- We introduce the equivalence relation on the prerational numbers that will
   define the rational numbers. -}

equiv-ℚ' : ℚ' → ℚ' → UU lzero
equiv-ℚ' (pair x1 x2) (pair y1 y2) =
  Id (mul-ℤ-ℤ\0 x1 y2) (mul-ℤ-ℤ\0 y1 x2)

refl-equiv-ℚ' :
  (x : ℚ') → equiv-ℚ' x x
refl-equiv-ℚ' (pair x1 x2) = refl

symmetric-equiv-ℚ' :
  (x y : ℚ') → equiv-ℚ' x y → equiv-ℚ' y x
symmetric-equiv-ℚ' (pair x1 x2) (pair y1 y2) = inv

transitive-equiv-ℚ' :
  (x y z : ℚ') →
  equiv-ℚ' x y → equiv-ℚ' y z → equiv-ℚ' x z
transitive-equiv-ℚ' (pair x1 x2) (pair y1 y2) (pair z1 z2) p q =
  is-injective-mul-ℤ-ℤ\0 y2
    ( mul-ℤ-ℤ\0 x1 z2)
    ( mul-ℤ-ℤ\0 z1 x2)
    ( ( associative-mul-ℤ x1 (int-ℤ\0 z2) (int-ℤ\0 y2)) ∙
      ( ( ap ( mul-ℤ x1)
             ( commutative-mul-ℤ (int-ℤ\0 z2) (int-ℤ\0 y2))) ∙
        ( ( inv (associative-mul-ℤ x1 (int-ℤ\0 y2) (int-ℤ\0 z2))) ∙
          ( ( ap ( λ t → mul-ℤ t (int-ℤ\0 z2))
                 ( p ∙ (commutative-mul-ℤ y1 (int-ℤ\0 x2)))) ∙
            ( ( associative-mul-ℤ (int-ℤ\0 x2) y1 (int-ℤ\0 z2)) ∙
              ( ( ap (mul-ℤ (int-ℤ\0 x2)) q) ∙
                ( ( inv (associative-mul-ℤ (int-ℤ\0 x2) z1 (int-ℤ\0 y2))) ∙
                  ( ap ( λ t → mul-ℤ-ℤ\0 t y2)
                       ( commutative-mul-ℤ (int-ℤ\0 x2) z1)))))))))

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

{- We define addition on the prerational numbers. -}

add-ℚ' : ℚ' → ℚ' → ℚ'
add-ℚ' (pair x1 x2) (pair y1 y2) =
  pair (add-ℤ (mul-ℤ-ℤ\0 x1 y2) (mul-ℤ-ℤ\0 y1 x2)) (mul-ℤ\0 x2 y2)

equiv-add-ℚ' :
  (x y x' y' : ℚ') → equiv-ℚ' x x' → equiv-ℚ' y y' →
  equiv-ℚ' (add-ℚ' x y) (add-ℚ' x' y')
equiv-add-ℚ'
  ( pair x1 (pair x2 Hx))
  ( pair y1 (pair y2 Hy))
  ( pair x1' (pair x2' Hx'))
  ( pair y1' (pair y2' Hy')) e f =
  ( right-distributive-mul-add-ℤ
    ( mul-ℤ x1 y2)
    ( mul-ℤ y1 x2)
    ( mul-ℤ x2' y2')) ∙
  ( ( ap-add-ℤ
      ( ( interchange-2-3-mul-ℤ {x1}) ∙
        ( ( ap (λ t → mul-ℤ t (mul-ℤ y2 y2')) e) ∙
          ( move-four-mul-ℤ {x1'})))
      ( ( move-five-mul-ℤ {y1}) ∙
        ( ( ap (mul-ℤ (mul-ℤ x2 x2')) f) ∙
          ( interchange-1-3-mul-ℤ {x2} {x2'} {y1'})))) ∙
    ( inv
      ( right-distributive-mul-add-ℤ
        ( mul-ℤ x1' y2')
        ( mul-ℤ y1' x2')
        ( mul-ℤ x2 y2))))

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

{- We define multiplication on the prerational numbers. -}

mul-ℚ' : ℚ' → ℚ' → ℚ'
mul-ℚ' (pair x1 x2) (pair y1 y2) = pair (mul-ℤ x1 y1) (mul-ℤ\0 x2 y2)

ap-mul-ℤ :
  {a b a' b' : ℤ} →
  Id a a' → Id b b' → Id (mul-ℤ a b) (mul-ℤ a' b')
ap-mul-ℤ refl refl = refl

equiv-mul-ℚ' :
  (x y x' y' : ℚ') → equiv-ℚ' x x' → equiv-ℚ' y y' →
  equiv-ℚ' (mul-ℚ' x y) (mul-ℚ' x' y')
equiv-mul-ℚ'
  ( pair x1 (pair x2 Hx))
  ( pair y1 (pair y2 Hy))
  ( pair x1' (pair x2' Hx'))
  ( pair y1' (pair y2' Hy')) e f =
  ( interchange-2-3-mul-ℤ {x1} {y1} {x2'}) ∙
  ( ( ap-mul-ℤ e f) ∙
    ( interchange-2-3-mul-ℤ {x1'}))

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
-- Christian Sattler, 2013-12-31
-- Testing eta-expansion of bound record metavars, as implemented by Andreas.
module Issue376-2 where

{- A simple example. -}
module example-0 {A B : Set} where
  record Prod : Set where
    constructor _,_
    field
      fst : A
      snd : B

  module _ (F : (Prod → Set) → Set) where
    q : (∀ f → F f) → (∀ f → F f)
    q h _ = h (λ {(a , b) → _})

{- A more complex, real-life-based example: the dependent
   generalization of (A × B) × (C × D) ≃ (A × C) × (B × D). -}
module example-1 where
  record Σ (A : Set) (B : A → Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B fst

  postulate
    _≃_ : (A B : Set) → Set

  Σ-interchange-Type =
    (A : Set) (B C : A → Set) (D : (a : A) → B a → C a → Set)
      → Σ (Σ A B) (λ {(a , b) → Σ (C a) (λ c → D a b c)})
      ≃ Σ (Σ A C) (λ {(a , c) → Σ (B a) (λ b → D a b c)})

  postulate
    Σ-interchange : Σ-interchange-Type

  {- Can the implicit arguments to Σ-interchange
     be inferred from the global type? -}
  Σ-interchange' : Σ-interchange-Type
  Σ-interchange' A B C D = Σ-interchange _ _ _ _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module _ where

module M where

  data D : Set where
    c : D

  private

    pattern c′ = c

open M

x : D
x = c′

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Nat
open import Prelude
open import dynamics-core

module lemmas-progress-checks where
  -- boxed values don't have an instruction transition
  boxedval-not-trans : ∀{d d'} → d boxedval → d →> d' → ⊥
  boxedval-not-trans (BVVal VNum) ()
  boxedval-not-trans (BVVal VLam) ()
  boxedval-not-trans (BVArrCast x bv) (ITCastID) = x refl
  boxedval-not-trans (BVHoleCast () bv) (ITCastID)
  boxedval-not-trans (BVHoleCast () bv) (ITCastSucceed x₁)
  boxedval-not-trans (BVHoleCast GArrHole bv) (ITGround (MGArr x)) = x refl
  boxedval-not-trans (BVHoleCast x a) (ITExpand ())
  boxedval-not-trans (BVHoleCast x x₁) (ITCastFail x₂ () x₄)
  boxedval-not-trans (BVVal (VInl x)) ()
  boxedval-not-trans (BVVal (VInr x)) ()
  boxedval-not-trans (BVSumCast x x₁) ITCastID = x refl
  boxedval-not-trans (BVHoleCast GSumHole x₁) (ITGround (MGSum x₂)) = x₂ refl
  boxedval-not-trans (BVInl bv) ()
  boxedval-not-trans (BVInr bv) ()
  boxedval-not-trans (BVPair bv bv₁) ()
  boxedval-not-trans (BVProdCast x bv) ITCastID = x refl
  boxedval-not-trans (BVHoleCast GProdHole bv) (ITGround (MGProd x)) = x refl

  -- indets don't have an instruction transition
  indet-not-trans : ∀{d d'} → d indet → d →> d' → ⊥
  indet-not-trans IEHole ()
  indet-not-trans (INEHole x) ()
  indet-not-trans (IAp x₁ () x₂) (ITLam)
  indet-not-trans (IAp x (ICastArr x₁ ind) x₂) ITApCast = x _ _ _ _ _ refl
  indet-not-trans (ICastArr x ind) (ITCastID) = x refl
  indet-not-trans (ICastGroundHole () ind) (ITCastID)
  indet-not-trans (ICastGroundHole x ind) (ITCastSucceed ())
  indet-not-trans (ICastGroundHole GArrHole ind) (ITGround (MGArr x)) = x refl
  indet-not-trans (ICastHoleGround x ind ()) (ITCastID)
  indet-not-trans (ICastHoleGround x ind x₁) (ITCastSucceed x₂) = x _ _ refl
  indet-not-trans (ICastHoleGround x ind GArrHole) (ITExpand (MGArr x₂)) = x₂ refl
  indet-not-trans (ICastGroundHole x a) (ITExpand ())
  indet-not-trans (ICastHoleGround x a x₁) (ITGround ())
  indet-not-trans (ICastGroundHole x x₁) (ITCastFail x₂ () x₄)
  indet-not-trans (ICastHoleGround x x₁ x₂) (ITCastFail x₃ x₄ x₅) = x _ _ refl
  indet-not-trans (IFailedCast x x₁ x₂ x₃) ()
  indet-not-trans (IPlus1 () x₁) (ITPlus x₂)
  indet-not-trans (IPlus2 x ()) (ITPlus x₂)
  indet-not-trans (ICase x x₂ x₃ (IInl x₄)) ITCaseInl = x _ _ refl
  indet-not-trans (ICase x x₂ x₃ (IInr x₄)) ITCaseInr = x₂ _ _ refl
  indet-not-trans (ICase x x₂ x₃ (ICastSum x₁ x₄)) ITCaseCast = x₃ _ _ _ _ _ refl
  indet-not-trans (ICastSum x x₂) ITCastID = x refl
  indet-not-trans (ICastGroundHole GSumHole x₂) (ITGround (MGSum x₁)) = x₁ refl
  indet-not-trans (ICastGroundHole GProdHole ind) (ITGround (MGProd x)) = x refl
  indet-not-trans (ICastHoleGround x x₂ GSumHole) (ITExpand (MGSum x₁)) = x₁ refl
  indet-not-trans (ICastHoleGround x ind GProdHole) (ITExpand (MGProd x₁)) = x₁ refl
  indet-not-trans (IInl ind) ()
  indet-not-trans (IInr ind) ()
  indet-not-trans (IPair1 ind x) ()
  indet-not-trans (IPair2 x ind) ()
  indet-not-trans (IFst x x₁ ind) ITFstPair = x _ _ refl
  indet-not-trans (IFst x x₁ ind) ITFstCast = x₁ _ _ _ _ _ refl
  indet-not-trans (ISnd x x₁ ind) ITSndPair = x _ _ refl
  indet-not-trans (ISnd x x₁ ind) ITSndCast = x₁ _ _ _ _ _ refl
  indet-not-trans (ICastProd x ind) ITCastID = x refl
  indet-not-trans (ICastGroundHole GNum ind) (ITGround ())
  indet-not-trans (ICastHoleGround x ind GNum) (ITExpand ())
  -- finals don't have an instruction transition
  final-not-trans : ∀{d d'} → d final → d →> d' → ⊥
  final-not-trans (FBoxedVal x) = boxedval-not-trans x
  final-not-trans (FIndet x) = indet-not-trans x

  -- finals cast from a ground are still final
  final-gnd-cast : ∀{ d τ } → d final → τ ground → (d ⟨ τ ⇒ ⦇-⦈ ⟩) final
  final-gnd-cast (FBoxedVal x) gnd = FBoxedVal (BVHoleCast gnd x)
  final-gnd-cast (FIndet x) gnd = FIndet (ICastGroundHole gnd x)

  -- if an expression results from filling a hole in an evaluation context,
  -- the hole-filler must have been final
  final-sub-final : ∀{d ε x} → d final → d == ε ⟦ x ⟧ → x final
  final-sub-final x FHOuter = x
  final-sub-final (FBoxedVal (BVVal ())) (FHPlus1 eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHPlus2 eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHAp1 eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHAp2 eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHNEHole eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHCast eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHFailedCast y)
  final-sub-final (FBoxedVal (BVArrCast x₁ x₂)) (FHCast eps) = final-sub-final (FBoxedVal x₂) eps
  final-sub-final (FBoxedVal (BVHoleCast x₁ x₂)) (FHCast eps) = final-sub-final (FBoxedVal x₂) eps
  final-sub-final (FIndet (IPlus1 x x₁)) (FHPlus1 eps) = final-sub-final (FIndet x) eps
  final-sub-final (FIndet (IPlus2 x x₁)) (FHPlus1 eps) = final-sub-final x eps
  final-sub-final (FIndet (IPlus1 x x₁)) (FHPlus2 eps) = final-sub-final x₁ eps
  final-sub-final (FIndet (IPlus2 x x₁)) (FHPlus2 eps) = final-sub-final (FIndet x₁) eps
  final-sub-final (FIndet (IAp x₁ x₂ x₃)) (FHAp1 eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (IAp x₁ x₂ x₃)) (FHAp2 eps) = final-sub-final x₃ eps
  final-sub-final (FIndet (INEHole x₁)) (FHNEHole eps) = final-sub-final x₁ eps
  final-sub-final (FIndet (ICastArr x₁ x₂)) (FHCast eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (ICastGroundHole x₁ x₂)) (FHCast eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (ICastHoleGround x₁ x₂ x₃)) (FHCast eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (IFailedCast x₁ x₂ x₃ x₄)) (FHFailedCast y) = final-sub-final x₁ y
  final-sub-final (FBoxedVal (BVVal ())) (FHCase eps)
  final-sub-final (FBoxedVal (BVSumCast x x₁)) (FHCast eps) = final-sub-final (FBoxedVal x₁) eps
  final-sub-final (FIndet (ICase x x₁ x₂ x₃)) (FHCase eps) = final-sub-final (FIndet x₃) eps
  final-sub-final (FIndet (ICastSum x x₁)) (FHCast eps) = final-sub-final (FIndet x₁) eps
  final-sub-final (FBoxedVal (BVVal (VInl x))) (FHInl eps) = final-sub-final (FBoxedVal (BVVal x)) eps
  final-sub-final (FBoxedVal (BVInl x)) (FHInl eps) = final-sub-final (FBoxedVal x) eps
  final-sub-final (FIndet (IInl x)) (FHInl eps) = final-sub-final (FIndet x) eps
  final-sub-final (FBoxedVal (BVVal (VInr x))) (FHInr eps) = final-sub-final (FBoxedVal (BVVal x)) eps
  final-sub-final (FBoxedVal (BVInr x)) (FHInr eps) = final-sub-final (FBoxedVal x) eps
  final-sub-final (FBoxedVal (BVProdCast x x₁)) (FHCast eps) = final-sub-final (FBoxedVal x₁) eps
  final-sub-final (FIndet (IInr x)) (FHInr eps) = final-sub-final (FIndet x) eps
  final-sub-final (FBoxedVal (BVVal ())) (FHFst eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHSnd eps)
  final-sub-final (FBoxedVal (BVVal (VPair x x₁))) (FHPair1 eps) = final-sub-final (FBoxedVal (BVVal x)) eps
  final-sub-final (FBoxedVal (BVPair x x₁)) (FHPair1 eps) = final-sub-final (FBoxedVal x) eps
  final-sub-final (FBoxedVal (BVVal (VPair x x₁))) (FHPair2 eps) = final-sub-final (FBoxedVal (BVVal x₁)) eps
  final-sub-final (FBoxedVal (BVPair x x₁)) (FHPair2 eps) = final-sub-final (FBoxedVal x₁) eps
  final-sub-final (FIndet (IFst x x₁ x₂)) (FHFst eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (ISnd x x₁ x₂)) (FHSnd eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (IPair1 x x₁)) (FHPair1 eps) = final-sub-final (FIndet x) eps
  final-sub-final (FIndet (IPair2 x x₁)) (FHPair1 eps) = final-sub-final x eps
  final-sub-final (FIndet (IPair1 x x₁)) (FHPair2 eps) = final-sub-final x₁ eps
  final-sub-final (FIndet (IPair2 x x₁)) (FHPair2 eps) = final-sub-final (FIndet x₁) eps
  final-sub-final (FIndet (ICastProd x x₁)) (FHCast eps) = final-sub-final (FIndet x₁) eps

  final-sub-not-trans : ∀{d d' d'' ε} →  d final → d == ε ⟦ d' ⟧ → d' →> d'' → ⊥
  final-sub-not-trans f sub step = final-not-trans (final-sub-final f sub) step

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Structure.Category.Functor where

open import Functional using (_on₂_)
open import Lang.Instance
import      Lvl
open import Logic.Predicate
open import Structure.Category
open import Structure.Function
open import Structure.Function.Multi
import      Structure.Relator.Names as Names
open import Structure.Setoid
open import Syntax.Function
open import Type

private variable ℓ ℓₒ ℓₘ ℓₗₒ ℓₗₘ ℓᵣₒ ℓᵣₘ ℓₑ ℓₗₑ ℓᵣₑ : Lvl.Level
private variable Obj Objₗ Objᵣ : Type{ℓ}
private variable Morphism Morphismₗ Morphismᵣ : Objₗ → Objᵣ → Type{ℓ}

module _
  ⦃ morphism-equivₗ : ∀{x y : Objₗ} → Equiv{ℓₗₑ}(Morphismₗ x y) ⦄
  ⦃ morphism-equivᵣ : ∀{x y : Objᵣ} → Equiv{ℓᵣₑ}(Morphismᵣ x y) ⦄
  (Categoryₗ : Category(Morphismₗ))
  (Categoryᵣ : Category(Morphismᵣ))
  where

  -- A covariant functor.
  -- A mapping which transforms objects and morphisms from one category to another while "preserving" the categorical structure.
  -- A homomorphism between categories.
  -- In the context of equivalence relations instead of categories, this is the "function"/"congruence" property of the function `F`.
  record Functor (F : Objₗ → Objᵣ) : Type{Lvl.of(Type.of(Categoryₗ)) Lvl.⊔ Lvl.of(Type.of(Categoryᵣ))} where
    constructor intro
    open Category ⦃ … ⦄
    open Category.ArrowNotation ⦃ … ⦄
    private instance _ = Categoryₗ
    private instance _ = Categoryᵣ

    field
      -- Morphs/Transforms morphisms from the left category to the right category.
      -- ∀{x y : Objₗ} → (x ⟶ y) → (F(x) ⟶ F(y))
      map : Names.Subrelation(_⟶_) ((_⟶_) on₂ F)

    field
      ⦃ map-function ⦄     : ∀{x y} → Function(map{x}{y})
      ⦃ op-preserving ⦄    : ∀{x y z : Objₗ}{f : y ⟶ z}{g : x ⟶ y} → (map(f ∘ g) ≡ map(f) ∘ map(g))
      ⦃ id-preserving ⦄    : ∀{x : Objₗ} → Names.Preserving₀(map{x})(id)(id) --(map(id {x = x}) ≡ id)

    open import Structure.Categorical.Properties
    open import Structure.Function.Domain

    Faithful      = ∀{x y} → Injective (map{x}{y}) -- TODO: F also? Not sure
    Full          = ∀{x y} → Surjective(map{x}{y})
    FullyFaithful = ∀{x y} → Bijective (map{x}{y})
    -- TODO: Conservative  = ∀{x y : Objₗ}{f : x ⟶ y} → Morphism.Isomorphism(\{x} → _∘_ {x = x})(\{x} → id{x = x})(map f) → Morphism.Isomorphism(\{x} → _∘_ {x = x})(id)(f)

module _
  ⦃ morphism-equiv : ∀{x y : Obj} → Equiv{ℓₑ}(Morphism x y) ⦄
  (Category : Category(Morphism))
  where

  Endofunctor = Functor(Category)(Category)
  module Endofunctor = Functor{Categoryₗ = Category}{Categoryᵣ = Category}

_→ᶠᵘⁿᶜᵗᵒʳ_ : CategoryObject{ℓₗₒ}{ℓₗₘ}{ℓₗₑ} → CategoryObject{ℓᵣₒ}{ℓᵣₘ}{ℓᵣₑ} → Type
catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ = ∃(Functor (CategoryObject.category(catₗ)) ((CategoryObject.category(catᵣ))))

⟲ᶠᵘⁿᶜᵗᵒʳ_ : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ} → Type
⟲ᶠᵘⁿᶜᵗᵒʳ cat = cat →ᶠᵘⁿᶜᵗᵒʳ cat

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:
-- exercises-03-wednesday.agda

open import mylib

{-
  Part 1 : Recursion via patterns
  Define the following functions using pattern matching and structural
  recursion on the natural numbers.
-}

-- Define a function even that determines wether its input is even.
even :  ℕ → Bool
{-
  even zero = true
  even (suc n) = ! even n
-}
even zero = true
even (suc zero) = false
even (suc (suc n)) = even n

-- Define a function sum that sums the numbers from 0 until n-1
sum : ℕ → ℕ
sum 0 = 0
sum (suc n) =  n + sum n

-- Define a function max that calculates the maximum of 2 numbers
max : ℕ → ℕ → ℕ
max zero n = n
max (suc m) zero = suc m
max (suc m) (suc n) = suc (max m n)

-- Define a function fib which calculates the nth item of the
-- Fibonacci sequence: 1,1,2,3,5,8,13
-- (each number is the sum of the two previous ones).
fib : ℕ → ℕ
fib zero = 1
fib (suc zero) = 1
fib (suc (suc n)) = fib n + fib (suc n)

-- Define a function eq that determines wether two numbers are equal.
eq : ℕ → ℕ → Bool
eq zero zero = true
eq zero (suc m) = false
eq (suc n) zero = false
eq (suc n) (suc m) = eq n m

-- Define a function rem such that rem m n returns the remainder
-- when dividing m by suc n (this way we avoid division by 0).
rem : ℕ → ℕ → ℕ
rem zero n = zero
rem (suc m) n = if eq (rem m n) n then 0 else suc (rem m n)

-- Define a function div such that div m n returns the result
-- of dividing m by suc n (ignoring the remainder)
div : ℕ → ℕ → ℕ
div zero n = zero
div (suc m) n = if eq (rem m n) n then suc (div m n) else div m n

{-
  Part 2 : Iterator and recursor
  Define all the functions of part 1 but this time only use the
  iterator Itℕ. That is NO PATTERNMATCHING (not even in lambdas) and
  NO RECURSION.

  Naming convention if the function in part 1 is called f then call it
  f-i if you only use the iterator.

  Test the functions with at least the same test cases.

  Hint: you may want to derive the recursor first (from the iterator):
  Rℕ : M → (ℕ → M → M) → ℕ → M
  where the method can access the current number. Using pattern matching
  the recursor can be defined as follows:
  Rℕ z s zero = z
  Rℕ z s (suc n) = s n (Rℕ z s n)
-}

Itℕ : M → (M → M) → ℕ → M
Itℕ z s zero = z
Itℕ z s (suc n) = s (Itℕ z s n)

even-i :  ℕ → Bool
even-i = Itℕ true (λ even-n → ! even-n)

{-
sum : ℕ → ℕ
sum 0 = 0
sum (suc n) =  n + sum n
-}
sum-i-aux : ℕ → ℕ × ℕ -- sum-i-aux n = (n , sum n)
sum-i-aux = Itℕ (0 , 0)
  λ n-sum-n → (suc (proj₁ n-sum-n)) , ((proj₁ n-sum-n) + (proj₂ n-sum-n))

sum-i : ℕ → ℕ
sum-i n = proj₂ (sum-i-aux n)

{-
fib : ℕ → ℕ
fib zero = 1
fib (suc zero) = 1
fib (suc (suc n)) = fib n + fib (suc n)

fib-i-aux : ℕ → ℕ × ℕ  = fib-i-aux n = fib n , fib (suc n)
-}

max_stars_repo_path: Type Theory/exercises-03-wednesday.agda

max_issues_repo_path: Type Theory/exercises-03-wednesday.agda

max_forks_repo_path: Type Theory/exercises-03-wednesday.agda


text:
{-
      Agda file from the exercise session(s).
-}

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

open import Agda.Primitive

{-
  Two inductive implementations of the
    Martin-Löf identity type
  aka
    equality type
  aka
    identification type
  aka
    path type.
-}

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

infixr 10 _≡_

-- explcit
data _≡'_ {A : Set} : A → A → Set where
  refl : (a : A) → a ≡' a

-- variables can be used later and are understood as Pi-quantified.
variable
  A B C : Set

-- sym' for ≡'
sym' : {a b : A} → a ≡' b → b ≡' a
sym' {a = x} {.x} (refl .x) = refl x

-- sym for ≡
sym : {a b : A} → a ≡ b → b ≡ a
sym refl = refl

_⁻¹ = sym

symsym : {a b : A} → (p : a ≡ b) → sym (sym p) ≡ p
symsym refl = refl

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

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

infixl 26 _∘_

ap-g∘f : (f : A → B) (g : B → C) {a b : A} (p : a ≡ b)
         → ap (g ∘ f) p ≡ (ap g ∘ ap f) p
ap-g∘f f g refl = refl

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

_∙_ = trans
infixr 30 _∙_

sym-refl : {a b : A} → (p : a ≡ b) → (p ⁻¹) ∙ p ≡ refl
sym-refl refl = refl

trans2 : {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
trans2 p refl = p

trans-trans2 : {a b c : A} -> (p : a ≡ b) -> (q : b ≡ c)
               -> trans p q ≡ trans2 p q
trans-trans2 {a = x} {b = .x} {c = .x} refl refl = refl

trans3 : {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
trans3 refl refl = refl

trans-trans3 : {a b c : A} -> (p : a ≡ b) -> (q : b ≡ c)
               -> trans p q ≡ trans3 p q
trans-trans3 {a = x} {b = .x} {c = .x} refl refl = refl

test : {a c : A} → (q : a ≡ c) → trans refl q ≡ q
test q = refl

test2 : {a c : A} → (q : a ≡ c) → trans2 q refl ≡ q
test2 q = refl

test3 : {a c : A} → (q : a ≡ c) → trans3 refl q ≡ q
test3 refl = refl

{-
  In test3 above, we have to pattern match (path induct) on q!
  What if we cannot, as in
    test4 : {a : A} → (q : a ≡ a) → trans3 refl q ≡ q
  ?
-}

-- solution:
test4 : {a : A} → (q : a ≡ a) → trans3 refl q ≡ q
test4 q = test3 q

-- We can only pattern match on q if we remove the --without-K option:
uip : {a b : A} → (p q : a ≡ b) → p ≡ q
uip {a = x} {b = .x} refl q = {!q!}

-- implementation of the J eliminator (aka path induction)
module _ (C : (a b : A) → a ≡ b → Set) where

   J-elim : (d : (a : A) → C a a refl) → (a b : A) → (p : a ≡ b) → C a b p
   J-elim d a .a refl = d a

-- implementation of the Paulin-Mohring version of J (based bath induction)
module _ (a₀ : A) (C : (b : A) → a₀ ≡ b → Set) where

   J-elim-PM : (d : C a₀ refl) → (b : A) → (p : a₀ ≡ b) → C b p
   J-elim-PM d b refl = d

-- this is "Axiom K" (which is disabled in the options)
module _ (a₀ : A) (C : a₀ ≡ a₀ → Set) where

  K : (d : C refl) → (p : a₀ ≡ a₀) → C p
  K d p = {!p!}

-- Caveat:
-- judgmental equality in Agda: = but on paper: ≡
-- path type in Agda: ≡ but on paper: =

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public
infixr 4 _,_

_×_ : (A B : Set) → Set
A × B = Σ A (λ _ → B)

{-
  Exercise 5
  For a given function f : A -> B, a *pointwise left inverse* is a
  function g : B -> A such that (a : A) -> g (f a) = a.

  Show: If f has a pointwise left inverse then, for all a,b : A, the
  function ap_f {a} {b} has a pointwise left inverse. (Does the other
  direction hold as well?)

  Solution of the easy part:
-}

has-ptw-left-inv : {A B : Set} → (f : A → B) → Set
has-ptw-left-inv {A} {B} f = Σ (B → A) λ g → (a : A) → g (f a) ≡ a

ptw-left-inv-ap : {A B : Set} → (f : A → B) →
                  has-ptw-left-inv f →
                  {a₁ a₂ : A} → has-ptw-left-inv (ap f {a₁} {a₂})
ptw-left-inv-ap f (g , g∘f) {a₁} {a₂} =
                (λ q → (g∘f a₁ ⁻¹) ∙ ap g {f a₁} {f a₂} q ∙ g∘f a₂) ,
                λ {refl →  sym-refl (g∘f a₁) }

{-
  Exercise 6: a1 a2 : A, b1 b2 : B
  (a1 , b1) ≡ (a2 , b2) is equivalent to (a1 = a2) × (b1 = b2).

  Exercise 7:
  eqv2iso :   isEqv(f) -> isIso(f)   [easy]
  iso2eqv :  isIso(f) -> isEqv(f)   [hard]
-}

module _ (A B : Set) (g : B → A) (a b : B) where

  lemma : (pair1 pair2 : Σ A λ x → x ≡ g a) → pair1 ≡ pair2
  lemma (.(g a) , refl) (.(g a) , refl) = refl

  wrong : (pair1 pair2 : Σ A λ x → g a ≡ g b) → pair1 ≡ pair2
  wrong (x1 , p1) (x2 , p2) = {!p1!}

split-equality : {x y : A × B} → x ≡ y → (fst x ≡ fst y) × (snd x ≡ snd y)
split-equality = {!!}

combine-equalities : {x y : A × B} → (fst x ≡ fst y) × (snd x ≡ snd y) → x ≡ y
combine-equalities = {!!}

max_stars_repo_path: Homotopy Type Theory/exercises.agda

max_issues_repo_path: Homotopy Type Theory/exercises.agda

max_forks_repo_path: Homotopy Type Theory/exercises.agda


text:
module par-swap.dpg-pot where

open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym)
open import Data.Maybe using ()
open import Data.List.Any using (here ; there)
open import Data.List.Any.Properties using ( ++-comm ; ++⁻ ; ++⁺ˡ ; ++⁺ʳ )
open import Data.Nat as Nat using (ℕ)

open import par-swap
open import par-swap.properties

open import Esterel.Lang.CanFunction
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction.Plug
open import Esterel.Environment as Env
open import Esterel.Context

open import utility

open import sn-calculus
open import context-properties -- get view, E-views
open import sn-calculus-props

open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)

canₛ-par :
  ∀ r₁ r₂ -> ∀ (θ : Env) (S : ℕ) →
   S ∈ Canₛ (r₂ ∥ r₁) θ →
   S ∈ Canₛ (r₁ ∥ r₂) θ
canₛ-par r₁ r₂ θ S S∈r₂∥r₁
 = ++-comm (proj₁ (Can r₂ θ)) (proj₁ (Can r₁ θ)) S∈r₂∥r₁

canₖ-par :
  ∀ r₁ r₂ -> ∀ (θ : Env) (k : Code) →
    k ∈ Canₖ (r₂ ∥ r₁) θ →
    k ∈ Canₖ (r₁ ∥ r₂) θ
canₖ-par
 = \ {r₁ r₂ θ S S∈r₂∥r₁ ->
      thing S
      (proj₁ (proj₂ (Can r₁ θ)))
      (proj₁ (proj₂ (Can r₂ θ)))
      S∈r₂∥r₁}  where

 simplify-foldr++-[] : ∀ (l2 : List Code) ->
   (Data.List.foldr{A = (List Code)}
     _++_
     []
     (Data.List.map (λ (k : Code) → []) l2)) ≡ []
 simplify-foldr++-[] [] = refl
 simplify-foldr++-[] (x ∷ l2) = simplify-foldr++-[] l2

 whatevs-left : ∀ S (whatevs : Code -> Code) l1 l2 ->
   Data.List.Any.Any (_≡_ S)
     (Data.List.foldr _++_ []
      (Data.List.map (λ k → Data.List.map (Code._⊔_ k) l2) l1))
   ->
   Data.List.Any.Any (_≡_ S)
     (Data.List.foldr _++_ []
      (Data.List.map (λ k → (whatevs k) ∷ Data.List.map (Code._⊔_ k) l2) l1))
 whatevs-left S whatevs [] l2 ()
 whatevs-left S whatevs (x ∷ l1) l2 blob
  with ++⁻ (Data.List.map (Code._⊔_ x) l2) blob
 ... | inj₁ y = there (++⁺ˡ y)
 ... | inj₂ y
  with whatevs-left S whatevs l1 l2 y
 ... | R = there (++⁺ʳ (Data.List.map (Code._⊔_ x) l2)  R)

 whatevs-right :
   ∀ S (whatevs : Code -> List Code) x l1 ->
   Data.List.Any.Any (_≡_ S) (Data.List.map (Code._⊔_ x) l1)
   ->
   Data.List.Any.Any (_≡_ S)
      (Data.List.foldr _++_ []
       (Data.List.map (λ k → (k Code.⊔ x) ∷ whatevs k)
        l1))
 whatevs-right S whatevs x [] blob = blob
 whatevs-right S whatevs x (x₁ ∷ l1) (here px)
  rewrite px = here (Code.⊔-comm x x₁)
 whatevs-right S whatevs x (x₁ ∷ l1) (there blob)
  = there (++⁺ʳ (whatevs x₁) (whatevs-right S whatevs x l1 blob))

 thing : ∀ S l1 l2 ->
    Data.List.Any.Any (_≡_ S)
     (Data.List.foldr _++_ []
      (Data.List.map
       (λ k → Data.List.map (Code._⊔_ k) l1)
       l2))
    ->
    Data.List.Any.Any (_≡_ S)
     (Data.List.foldr _++_ []
      (Data.List.map
       (λ k → Data.List.map (Code._⊔_ k) l2)
       l1))

 thing S l1 [] blob
   rewrite simplify-foldr++-[] l1
   = blob

 thing S l1 (x ∷ l2) blob
  with ++⁻ (Data.List.map (Code._⊔_ x) l1) blob
 thing S l1 (x ∷ l2) _ | inj₁ y =
   whatevs-right S (λ { k → Data.List.map (Code._⊔_ k) l2 }) x l1 y
 thing S l1 (x ∷ l2) _ | inj₂ y =
   whatevs-left S (\ { k ->  (k Code.⊔ x)}) l1 l2 (thing S l1 l2 y)

canₛₕ-par :
  ∀ r₁ r₂ -> ∀ (θ : Env) →
   Canₛₕ (r₂ ∥ r₁) θ ⊆¹ Canₛₕ (r₁ ∥ r₂) θ
canₛₕ-par r₁ r₂ θ S S∈r₂∥r₁
 = ++-comm (proj₂ (proj₂ (Can r₂ θ))) (proj₂ (proj₂ (Can r₁ θ))) S∈r₂∥r₁

canθₛ-C-par : ∀ sigs S'' -> ∀ {C p r₁ r₂} ->
    p ≐ C ⟦ r₁ ∥ r₂ ⟧c ->
    ∀ {θ} S' ->
     S' ∉ Canθₛ sigs S'' p θ ->
     S' ∉ Canθₛ sigs S'' (C ⟦ r₂ ∥ r₁ ⟧c) θ
canθₛ-C-par sigs S'' {C} {p} {r₁} {r₂} pC {θ} S' S'∉Canθₛ[p] S'∈Canθₛ[C⟦r₂∥r₁⟧c]
  with canθₛ-plug S'' sigs C (r₁ ∥ r₂) (r₂ ∥ r₁)
                 (canₛ-par r₁ r₂) (canₖ-par r₁ r₂) θ S'
... |  r₂r₁->r₁r₂ rewrite sym (unplugc pC) = S'∉Canθₛ[p] (r₂r₁->r₁r₂ S'∈Canθₛ[C⟦r₂∥r₁⟧c])

canθₛₕ-C-par : ∀ sigs S' -> ∀ {C p r₁ r₂} ->
    p ≐ C ⟦ r₁ ∥ r₂ ⟧c ->
    ∀ {θ} s' ->
     s' ∉ Canθₛₕ sigs S' p θ ->
     s' ∉ Canθₛₕ sigs S' (C ⟦ r₂ ∥ r₁ ⟧c) θ
canθₛₕ-C-par sigs S' {C} {p} {r₁} {r₂} pC {θ} s' s'∉Canθₛₕ[p] s'∈Canθₛₕ[C⟦r₂∥r₁⟧c]
  with canθₛₕ-plug S' sigs C (r₁ ∥ r₂) (r₂ ∥ r₁)
                  (canₛₕ-par r₁ r₂) (canₖ-par r₁ r₂) (canₛ-par r₁ r₂) θ s'
... | r₂r₁->r₁r₂ rewrite sym (unplugc pC) = s'∉Canθₛₕ[p] (r₂r₁->r₁r₂ s'∈Canθₛₕ[C⟦r₂∥r₁⟧c])

DPG-pot-view :
 ∀ {C r₁ r₂ p q θ θ' A A'} ->
  p ≐ C ⟦ r₁ ∥ r₂ ⟧c ->
  (psn⟶₁q : ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θ' , A' ⟩· q) ->
  (p≡q : p ≡ q) ->
  (A≡A' : A ≡ A') ->
  ->pot-view psn⟶₁q p≡q A≡A' ->
  Σ[ dd′ ∈ Term × Term ]
  (ρ⟨ θ , A ⟩· C ⟦ r₂ ∥ r₁ ⟧c sn⟶ (proj₂ dd′))
  ×
  ((proj₂ dd′) sn⟶* (proj₁ dd′))
  ×
  ((ρ⟨ θ' , A' ⟩· q) ∥R* (proj₁ dd′))
DPG-pot-view pC (ris-present S∈ x x₁) p≡q A≡A' ()
DPG-pot-view pC (ris-absent S∈ x x₁) p≡q A≡A' ()
DPG-pot-view pC (remit S∈ ¬S≡a x) p≡q A≡A' ()
DPG-pot-view pC (rraise-shared e' x) p≡q A≡A' ()
DPG-pot-view pC (rset-shared-value-old e' s∈ x x₁) p≡q A≡A' ()
DPG-pot-view pC (rset-shared-value-new e' s∈ x x₁) p≡q A≡A' ()
DPG-pot-view pC (rraise-var e' x₁) p≡q A≡A' ()
DPG-pot-view pC (rset-var x∈ e' x₁) p≡q A≡A' ()
DPG-pot-view pC (rif-false x∈ x₁ x₂) p≡q A≡A' ()
DPG-pot-view pC (rif-true x∈ x₁ x₂) p≡q A≡A' ()
DPG-pot-view pC (rabsence{θ}{_}{S} S∈ x x₁) .refl .refl (vabsence .S .S∈ .x .x₁)
  = _ , rcontext [] dchole
         (rabsence{θ}{_}{S} S∈ x (canθₛ-C-par (sig θ) 0 pC (Signal.unwrap S) x₁)) ,
    rrefl ,
    Context1-∥R* (cenv _ _) (∥Rn (∥Rstep pC) ∥R0)
DPG-pot-view pC (rreadyness{θ}{_}{s} s∈ x x₁) .refl .refl (vreadyness .s .s∈ .x .x₁)
  = _ , rcontext [] dchole
         (rreadyness{s = s} s∈ x (canθₛₕ-C-par (sig θ) 0 pC (SharedVar.unwrap s) x₁)) ,
    rrefl ,
    Context1-∥R* (cenv _ _) (∥Rn (∥Rstep pC) ∥R0)
DPG-pot-view pC (rmerge x) p≡q A≡A' ()

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module Pi.NoRepeat where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Pi.Syntax
open import Pi.Opsem
open import Pi.AuxLemmas
import RevNoRepeat

-- Forward deterministic
deterministic : ∀ {st st₁ st₂} → st ↦ st₁ → st ↦ st₂ → st₁ ≡ st₂
deterministic (↦₁ {b = b₁}) (↦₁ {b = b₂}) with base-is-prop _ b₁ b₂
... | refl = refl
deterministic ↦₂ ↦₂ = refl
deterministic ↦₃ ↦₃ = refl
deterministic ↦₄ ↦₄ = refl
deterministic ↦₅ ↦₅ = refl
deterministic ↦₆ ↦₆ = refl
deterministic ↦₇ ↦₇ = refl
deterministic ↦₈ ↦₈ = refl
deterministic ↦₉ ↦₉ = refl
deterministic ↦₁₀ ↦₁₀ = refl
deterministic ↦₁₁ ↦₁₁ = refl
deterministic ↦₁₂ ↦₁₂ = refl

-- Backward deterministic
deterministicᵣₑᵥ : ∀ {st st₁ st₂} → st₁ ↦ st → st₂ ↦ st → st₁ ≡ st₂
deterministicᵣₑᵥ {［ c ∣ _ ∣ κ ］} {⟨ c ∣ v ∣ κ ⟩} {⟨ c' ∣ v' ∣ κ' ⟩} ↦₁ r with Lemma₁ r
... | refl , refl with Lemma₂ r
deterministicᵣₑᵥ {［ unite₊l  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ y        ∣ κ ⟩} {⟨ _ ∣ inj₂ y        ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ uniti₊l  ∣ _ ∣ κ ］} {⟨ _ ∣ v             ∣ κ ⟩} {⟨ _ ∣ v             ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ y        ∣ κ ⟩} {⟨ _ ∣ inj₂ y        ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩} ↦₁ () | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ x        ∣ κ ⟩} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩} ↦₁ () | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩} {⟨ _ ∣ inj₂ (inj₁ y) ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩} {⟨ _ ∣ inj₂ (inj₂ z) ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ z        ∣ κ ⟩} {⟨ _ ∣ inj₁ (inj₁ x) ∣ κ ⟩} ↦₁ () | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ z        ∣ κ ⟩} {⟨ _ ∣ inj₁ (inj₂ y) ∣ κ ⟩} ↦₁ () | refl , refl | refl , refl
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ z        ∣ κ ⟩} {⟨ _ ∣ inj₂ z        ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ unite⋆l  ∣ _ ∣ κ ］} {⟨ _ ∣ (tt , v)      ∣ κ ⟩} {⟨ _ ∣ (tt , v)      ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ uniti⋆l  ∣ _ ∣ κ ］} {⟨ _ ∣ v             ∣ κ ⟩} {⟨ _ ∣ v             ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ swap⋆    ∣ _ ∣ κ ］} {⟨ _ ∣ (x , y)       ∣ κ ⟩} {⟨ _ ∣ (x , y)       ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocl⋆  ∣ _ ∣ κ ］} {⟨ _ ∣ (x , (y , z)) ∣ κ ⟩} {⟨ _ ∣ (x , (y , z)) ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ assocr⋆  ∣ _ ∣ κ ］} {⟨ _ ∣ ((x , y) , z) ∣ κ ⟩} {⟨ _ ∣ ((x , y) , z) ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］} {⟨ _ ∣ (inj₁ x , z)  ∣ κ ⟩} {⟨ _ ∣ (inj₁ x , z)  ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］} {⟨ _ ∣ (inj₂ y , z)  ∣ κ ⟩} {⟨ _ ∣ (inj₂ y , z)  ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］} {⟨ _ ∣ inj₁ (x , z)  ∣ κ ⟩} {⟨ _ ∣ inj₁ (x , z)  ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］} {⟨ _ ∣ inj₂ (y , z)  ∣ κ ⟩} {⟨ _ ∣ inj₂ (y , z)  ∣ κ ⟩} ↦₁ ↦₁ | refl , refl | refl , refl = refl
deterministicᵣₑᵥ {［ unite₊l  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ uniti₊l  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ swap₊    ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ assocl₊  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ assocr₊  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ unite⋆l  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ uniti⋆l  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ swap⋆    ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ assocl⋆  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ assocr⋆  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ dist     ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ factor   ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} ↦₁ ()
deterministicᵣₑᵥ {［ id↔      ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} (↦₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⨾ c₂  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} (↦₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⊕ c₂  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} (↦₁ {b = ()})
deterministicᵣₑᵥ {［ c₁ ⊗ c₂  ∣ _ ∣ κ ］} {⟨ _ ∣ v  ∣ κ ⟩} {［ c' ∣ v' ∣ κ' ］} (↦₁ {b = ()})
deterministicᵣₑᵥ ↦₂ ↦₂ = refl
deterministicᵣₑᵥ ↦₃ ↦₃ = refl
deterministicᵣₑᵥ ↦₄ ↦₄ = refl
deterministicᵣₑᵥ ↦₅ ↦₅ = refl
deterministicᵣₑᵥ ↦₆ ↦₆ = refl
deterministicᵣₑᵥ ↦₇ ↦₇ = refl
deterministicᵣₑᵥ ↦₈ ↦₈ = refl
deterministicᵣₑᵥ ↦₉ ↦₉ = refl
deterministicᵣₑᵥ ↦₁₀ ↦₁₀ = refl
deterministicᵣₑᵥ {［ c₁ ⊕ c₂ ∣ inj₁ v ∣ κ ］} {_} {⟨ c₁' ⊕ c₂' ∣ v' ∣ κ' ⟩} ↦₁₁ r with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with Lemma₃ r
... | inj₂ refl with Lemma₄ r
... | inj₁ ()
... | inj₂ ()
deterministicᵣₑᵥ {［ c₁ ⊕ c₂ ∣ inj₁ v ∣ κ ］} {［ c₁ ∣ v ∣ ☐⊕ c₂ • κ ］} {［ c₁ ∣ v ∣ ☐⊕ c₂ • κ ］} ↦₁₁ ↦₁₁ = refl
deterministicᵣₑᵥ {［ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ］} {［ c₂ ∣ y ∣ c₁ ⊕☐• κ ］} {⟨ c ∣ x ∣ x₁ ⟩} ↦₁₂ r with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with Lemma₃ r
... | inj₂ refl with Lemma₄ r
... | inj₂ ()
deterministicᵣₑᵥ {［ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ］} {［ c₂ ∣ y ∣ c₁ ⊕☐• κ ］} {［ c₂ ∣ y ∣ (c₁ ⊕☐• κ) ］} ↦₁₂ ↦₁₂ = refl

-- Non-repeating Lemma
open RevNoRepeat (record { State = State
                         ; _↦_ = _↦_
                         ; deterministic = deterministic
                         ; deterministicᵣₑᵥ = deterministicᵣₑᵥ }) public


text:
module examplesPaperJFP.BasicIO where

open import Data.Maybe hiding ( _>>=_ )
open import Data.Sum renaming (inj₁ to left; inj₂ to right; [_,_]′ to either)
open import Function

open import examplesPaperJFP.NativeIOSafe
open import examplesPaperJFP.triangleRightOperator

module _ where  -- for indentation
  record IOInterface : Set₁ where
    field  Command   :  Set
           Response  :  (c : Command) → Set

open IOInterface public

module _ {C : Set} {R : C → Set} (let
  I = record { Command = C; Response = R }
    ) where
module Postulated {I : IOInterface} (let C = Command I) (let R = Response I) where

  postulate
    IO                :  (I : IOInterface) (A : Set) → Set
    exec               :  ∀{A}    (c  :  C)       (f  :  R c → IO I A)  → IO I A
    return            :  ∀{A}    (a  :  A)                             → IO I A
    _>>=_             :  ∀{A B}  (m  :  IO I A)  (k  :  A → IO I B)    → IO I B

mutual
  record IO I A : Set where
    coinductive
    constructor delay
    field force : IO′ I A

  data IO′ I A : Set where
    exec′      :  (c : Command I) (f : Response I c → IO I A)  → IO′ I A
    return′  :  (a : A)                                      → IO′ I A

open IO public

delay′ : ∀{I A} → IO′ I A → IO I A
force (delay′ x) = x

module _ {I : IOInterface} (let C = Command I) (let R = Response I) where
-- module _ {I : IOInterface} (let record { Command = C; Response = R } = I) where
-- module _ {I : IOInterface} (let ioInterface C R = I) where
  exec                :  ∀{A} (c : C) (f : R c → IO I A) → IO I A
  force (exec c f)    =  exec′ c f

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

  infixl 2 _>>=_
  _>>=_             :  ∀{A B} (m : IO I A) (k : A → IO I B) → IO I B
  force (m >>= k) with force m
  ... | exec′ c f     =  exec′ c λ x → f x >>= k
  ... | return′ a   =  force (k a)

module _ {I : IOInterface} (let C = Command I) (let R = Response I)
      where

  {-# NON_TERMINATING #-}
  translateIO : ∀ {A} (tr : (c : C) → NativeIO (R c)) → IO I A → NativeIO A
  translateIO tr m = force m ▹ λ
     {  (exec′ c f)    →  (tr c) native>>= λ r → translateIO tr (f r)
     ;  (return′ a)  →  nativeReturn a
     }

-- Recursion

-- trampoline provides a generic form of loop (generalizing while/repeat).
-- Starting at state s : S, step function f is iterated until it returns
-- a result in A.

module _ (I : IOInterface)(let C = Command I) (let R = Response I)
      where
  data IO+ (A : Set) : Set where
      exec′ : (c : C) (f : R c → IO I A) → IO+ A

module _ {I : IOInterface}(let C = Command I) (let R = Response I)
      where
  fromIO+′ : ∀{A} → IO+ I A → IO′ I A
  fromIO+′ (exec′ c f) = exec′ c f

  fromIO+ : ∀{A} → IO+ I A → IO I A
  force (fromIO+ (exec′ c f)) = exec′ c f

  _>>=+′_ : ∀{A B} (m : IO+ I A) (k : A → IO I B) → IO′ I B
  exec′ c f >>=+′ k = exec′ c λ x → f x >>= k

  _>>=+_ : ∀{A B} (m : IO+ I A) (k : A → IO I B) → IO I B
  force (m >>=+ k) = m >>=+′ k

  mutual

    _>>+_ : ∀{A B} (m : IO I (A ⊎ B)) (k : A → IO I B) → IO I B
    force (m >>+ k) = force m >>+′ k

    _>>+′_ : ∀{A B} (m : IO′ I (A ⊎ B)) (k : A → IO I B) → IO′ I B
    exec′ c f            >>+′ k = exec′ c λ x → f x >>+ k
    return′ (left  a)  >>+′ k = force (k a)
    return′ (right b)  >>+′ k = return′ b

   -- loop

  {-# TERMINATING #-}

  trampoline : ∀{A S} (f : S → IO+ I (S ⊎ A)) (s : S) → IO I A
  force (trampoline f s) = case (f s) of
    \ { (exec′ c k) → exec′ c λ r → k r >>+ trampoline f }

  -- simple infinite loop

  {-# TERMINATING #-}
  forever : ∀{A B} → IO+ I A → IO I B
  force (forever (exec′ c f)) = exec′ c λ r → f r >>= λ _ → forever (exec′ c f)

  whenJust : {A : Set} → Maybe A → (A → IO I Unit) → IO I Unit
  whenJust nothing  k = return _
  whenJust (just a) k = k a

main : NativeIO Unit
main = nativePutStrLn "Hello, world!"

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module _ where

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

data L : Nat → Set where
  nil  : L zero
  cons : ∀ n → L n → L (suc n)

pattern one = cons .zero nil


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Integer division
------------------------------------------------------------------------

module Data.Nat.DM where

open import Data.Fin as Fin using (Fin; toℕ)
import Data.Fin.Properties as FinP
open import Data.Nat as Nat
open import Data.Nat.Properties as NatP
open import Data.Nat.Properties.Simple
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Relation.Binary.PropositionalEquality.TrustMe as TrustMe
  using (erase)

open NatP.SemiringSolver
open P.≡-Reasoning
open Nat.≤-Reasoning
  renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≡⟨_⟩′_)

infixl 7 _div_ _mod_ _divMod_

-- Integer division.

private

  div-helper : ℕ → ℕ → ℕ → ℕ → ℕ
  div-helper acc s zero    n       = acc
  div-helper acc s (suc d) zero    = div-helper (suc acc) s d s
  div-helper acc s (suc d) (suc n) = div-helper acc       s d n

  -- {-# BUILTIN NATDIVSUCAUX div-helper #-}

_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
(d div 0) {}
(d div suc s) = div-helper 0 s d s

-- The remainder after integer division.

private

  mod-helper : ℕ → ℕ → ℕ → ℕ → ℕ
  mod-helper acc s zero    n       = acc
  mod-helper acc s (suc d) zero    = mod-helper zero      s d s
  mod-helper acc s (suc d) (suc n) = mod-helper (suc acc) s d n

  -- {-# BUILTIN NATMODSUCAUX mod-helper #-}

  -- The remainder is not too large.

  mod-lemma : (acc d n : ℕ) →
              let s = acc + n in
              mod-helper acc s d n ≤ s

  mod-lemma acc zero n = start
    acc      ≤⟨ m≤m+n acc n ⟩
    acc + n  □

  mod-lemma acc (suc d) zero = start
    mod-helper zero (acc + 0) d (acc + 0)  ≤⟨ mod-lemma zero d (acc + 0) ⟩
    acc + 0                                □

  mod-lemma acc (suc d) (suc n) =
    P.subst (λ x → mod-helper (suc acc) x d n ≤ x)
            (P.sym (+-suc acc n))
            (mod-lemma (suc acc) d n)

_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
(d mod 0) {}
(d mod suc s) =
  Fin.fromℕ≤″ (mod-helper 0 s d s)
              (Nat.erase (≤⇒≤″ (s≤s (mod-lemma 0 d s))))

-- Integer division with remainder.

private

  -- The quotient and remainder are related to the dividend and
  -- divisor in the right way.

  division-lemma :
    (mod-acc div-acc d n : ℕ) →
    let s = mod-acc + n in
    mod-acc + div-acc * suc s + d
      ≡
    mod-helper mod-acc s d n + div-helper div-acc s d n * suc s

  division-lemma mod-acc div-acc zero n = begin

    mod-acc + div-acc * suc s + zero  ≡⟨ +-right-identity _ ⟩

    mod-acc + div-acc * suc s         ∎

    where s = mod-acc + n

  division-lemma mod-acc div-acc (suc d) zero = begin

    mod-acc + div-acc * suc s + suc d                ≡⟨ solve 3
                                                              (λ mod-acc div-acc d →
                                                                   let s = mod-acc :+ con 0 in
                                                                   mod-acc :+ div-acc :* (con 1 :+ s) :+ (con 1 :+ d)
                                                                     :=
                                                                   (con 1 :+ div-acc) :* (con 1 :+ s) :+ d)
                                                              P.refl mod-acc div-acc d ⟩
    suc div-acc * suc s + d                          ≡⟨ division-lemma zero (suc div-acc) d s ⟩

    mod-helper zero          s      d  s    +
    div-helper (suc div-acc) s      d  s    * suc s  ≡⟨⟩

    mod-helper      mod-acc  s (suc d) zero +
    div-helper      div-acc  s (suc d) zero * suc s  ∎

    where s = mod-acc + 0

  division-lemma mod-acc div-acc (suc d) (suc n) = begin

    mod-acc + div-acc * suc s + suc d                   ≡⟨ solve 4
                                                                 (λ mod-acc div-acc n d →
                                                                      mod-acc :+ div-acc :* (con 1 :+ (mod-acc :+ (con 1 :+ n))) :+ (con 1 :+ d)
                                                                        :=
                                                                      con 1 :+ mod-acc :+ div-acc :* (con 2 :+ mod-acc :+ n) :+ d)
                                                                 P.refl mod-acc div-acc n d ⟩
    suc mod-acc + div-acc * suc s′ + d                  ≡⟨ division-lemma (suc mod-acc) div-acc d n ⟩

    mod-helper (suc mod-acc) s′ d n +
    div-helper      div-acc  s′ d n * suc s′            ≡⟨ P.cong (λ s → mod-helper (suc mod-acc) s d n +
                                                                         div-helper div-acc s d n * suc s)
                                                                  (P.sym (+-suc mod-acc n)) ⟩

    mod-helper (suc mod-acc) s d n +
    div-helper      div-acc  s d n * suc s              ≡⟨⟩

    mod-helper      mod-acc  s (suc d) (suc n) +
    div-helper      div-acc  s (suc d) (suc n) * suc s  ∎

    where
    s  = mod-acc + suc n
    s′ = suc mod-acc + n

-- A specification of integer division.

record DivMod (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} : Set where
  constructor result
  field
    quotient  : ℕ
    remainder : Fin divisor
    property  : dividend ≡ toℕ remainder + quotient * divisor
    div-eq : _div_ dividend divisor {≢0} ≡ quotient
    mod-eq : _mod_ dividend divisor {≢0} ≡ remainder

_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
           DivMod dividend divisor {≢0}
(d divMod 0) {}
(d divMod suc s) =
  result
    (d div suc s)
    (d mod suc s)
    (TrustMe.erase (begin
            d
        ≡⟨ division-lemma 0 0 d s ⟩
            mod-helper 0 s d s         + div-helper 0 s d s * suc s
        ≡⟨ P.cong₂ _+_ (P.sym (FinP.toℕ-fromℕ≤ lemma)) P.refl ⟩
            toℕ (Fin.fromℕ≤    lemma)  + div-helper 0 s d s * suc s
        ≡⟨ P.cong (λ n → toℕ n + div-helper 0 s d s * suc s) (FinP.fromℕ≤≡fromℕ≤″ lemma _) ⟩
            toℕ (Fin.fromℕ≤″ _ lemma′) + div-helper 0 s d s * suc s
        ∎))
    _≡_.refl
    _≡_.refl
  where
  lemma  = s≤s (mod-lemma 0 d s)
  lemma′ = Nat.erase (≤⇒≤″ lemma)

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral