text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Properties.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Properties ( n : ℕ ) where

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

open import Data.Bool.Base using ( Bool; false; true; not; T )
open import Data.Fin       using ( Fin ; suc; zero )

open import Data.PropFormula.Syntax n
open import Data.PropFormula.Dec n

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

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

suc-injective : ∀ {o} {m n : Fin o} → Fin.suc m ≡ Fin.suc n → m ≡ n
suc-injective refl = refl

var-injective : ∀ {x x₁} → Var x ≡ Var x₁ → x ≡ x₁
var-injective refl = refl

∧-injective₁ : ∀ {φ φ₁ ψ ψ₁} → (φ ∧ φ₁) ≡ (ψ ∧ ψ₁) → φ ≡ ψ
∧-injective₁ refl = refl

∧-injective₂ : ∀ {φ φ₁ ψ ψ₁} → (φ ∧ φ₁) ≡ (ψ ∧ ψ₁) → φ₁ ≡ ψ₁
∧-injective₂ refl = refl

∨-injective₁ : ∀ {φ φ₁ ψ ψ₁} → (φ ∨ φ₁) ≡ (ψ ∨ ψ₁) → φ ≡ ψ
∨-injective₁ refl = refl

∨-injective₂ : ∀ {φ φ₁ ψ ψ₁} → (φ ∨ φ₁) ≡ (ψ ∨ ψ₁) → φ₁ ≡ ψ₁
∨-injective₂ refl = refl

⊃-injective₁ : ∀ {φ φ₁ ψ ψ₁} → (φ ⊃ φ₁) ≡ (ψ ⊃ ψ₁) → φ ≡ ψ
⊃-injective₁ refl = refl

⊃-injective₂ : ∀ {φ φ₁ ψ ψ₁} → (φ ⊃ φ₁) ≡ (ψ ⊃ ψ₁) → φ₁ ≡ ψ₁
⊃-injective₂ refl = refl

⇔-injective₁ : ∀ {φ φ₁ ψ ψ₁} → (φ ⇔ φ₁) ≡ (ψ ⇔ ψ₁) → φ ≡ ψ
⇔-injective₁ refl = refl

⇔-injective₂ : ∀ {φ φ₁ ψ ψ₁} → (φ ⇔ φ₁) ≡ (ψ ⇔ ψ₁) → φ₁ ≡ ψ₁
⇔-injective₂ refl = refl

¬-injective : ∀ {φ ψ} → ¬ φ ≡ ¬ ψ → φ ≡ ψ
¬-injective refl = refl

-- Def.
_≟_ : {n : ℕ} → Decidable {A = Fin n} _≡_
zero  ≟ zero  = yes refl
zero  ≟ suc y = no λ()
suc x ≟ zero  = no λ()
suc x ≟ suc y with x ≟ y
... | yes x≡y = yes (cong Fin.suc x≡y)
... | no  x≢y = no (λ r → x≢y (suc-injective r))

-- Def.
eq : (φ ψ : PropFormula) → Dec (φ ≡ ψ)

-- Equality with Var.
eq (Var x) ⊤        = no λ()
eq (Var x) ⊥        = no λ()
eq (Var x) (ψ ∧ ψ₁) = no λ()
eq (Var x) (ψ ∨ ψ₁) = no λ()
eq (Var x) (ψ ⊃ ψ₁) = no λ()
eq (Var x) (ψ ⇔ ψ₁) = no λ()
eq (Var x) (¬ ψ)    = no λ()
eq (Var x) (Var x₁) with x ≟ x₁
... | yes refl = yes refl
... | no x≢x₁  = no (λ r → x≢x₁ (var-injective r))

-- Equality with ⊤.
eq ⊤ (Var x)        = no λ()
eq ⊤ ⊥              = no λ()
eq ⊤ (ψ ∧ ψ₁)       = no λ()
eq ⊤ (ψ ∨ ψ₁)       = no λ()
eq ⊤ (ψ ⊃ ψ₁)       = no λ()
eq ⊤ (ψ ⇔ ψ₁)      = no λ()
eq ⊤ (¬ ψ)          = no λ()
eq ⊤ ⊤              = yes refl

-- Equality with ⊥.
eq ⊥ (Var x)        = no λ()
eq ⊥ ⊤              = no λ()
eq ⊥ (ψ ∧ ψ₁)       = no λ()
eq ⊥ (ψ ∨ ψ₁)       = no λ()
eq ⊥ (ψ ⊃ ψ₁)       = no λ()
eq ⊥ (ψ ⇔ ψ₁)       = no λ()
eq ⊥ (¬ ψ)          = no λ()
eq ⊥ ⊥              = yes refl

-- Equality with ∧.
eq (φ ∧ φ₁) (Var x)  = no λ()
eq (φ ∧ φ₁) ⊤        = no λ()
eq (φ ∧ φ₁) ⊥        = no λ()
eq (φ ∧ φ₁) (ψ ∨ ψ₁) = no λ()
eq (φ ∧ φ₁) (ψ ⊃ ψ₁) = no λ()
eq (φ ∧ φ₁) (ψ ⇔ ψ₁) = no λ()
eq (φ ∧ φ₁) (¬ ψ)    = no λ()
eq (φ ∧ φ₁) (ψ ∧ ψ₁) with eq φ ψ | eq φ₁ ψ₁
... | yes refl | yes refl = yes refl
... | yes _    | no φ₁≢ψ₁ = no (λ r → φ₁≢ψ₁ (∧-injective₂ r))
... | no φ≢ψ   | _        = no (λ r → φ≢ψ   (∧-injective₁ r))

-- Equality with ∨.
eq (φ ∨ φ₁) (Var x)  = no λ()
eq (φ ∨ φ₁) ⊤        = no λ()
eq (φ ∨ φ₁) ⊥        = no λ()
eq (φ ∨ φ₁) (ψ ∧ ψ₁) = no λ()
eq (φ ∨ φ₁) (ψ ⊃ ψ₁) = no λ()
eq (φ ∨ φ₁) (ψ ⇔ ψ₁) = no λ()
eq (φ ∨ φ₁) (¬ ψ)    = no λ()
eq (φ ∨ φ₁) (ψ ∨ ψ₁) with eq φ ψ | eq φ₁ ψ₁
... | yes refl | yes refl  = yes refl
... | yes _    | no  φ₁≢ψ₁ = no (λ r → φ₁≢ψ₁ (∨-injective₂ r))
... | no φ≢ψ   | _         = no (λ r → φ≢ψ   (∨-injective₁ r))

-- Equality with ⊃.
eq (φ ⊃ φ₁) (Var x)  = no λ()
eq (φ ⊃ φ₁) ⊤        = no λ()
eq (φ ⊃ φ₁) ⊥        = no λ()
eq (φ ⊃ φ₁) (ψ ∧ ψ₁) = no λ()
eq (φ ⊃ φ₁) (ψ ∨ ψ₁) = no λ()
eq (φ ⊃ φ₁) (ψ ⇔ ψ₁) = no λ()
eq (φ ⊃ φ₁) (¬ ψ)    = no λ()
eq (φ ⊃ φ₁) (ψ ⊃ ψ₁) with eq φ ψ | eq φ₁ ψ₁
... | yes refl | yes refl  = yes refl
... | yes _    | no  φ₁≢ψ₁ = no (λ r → φ₁≢ψ₁ (⊃-injective₂ r))
... | no φ≢ψ   | _         = no (λ r → φ≢ψ   (⊃-injective₁ r))

-- Equality with ⇔.
eq (φ ⇔ φ₁) (Var x)  = no λ()
eq (φ ⇔ φ₁) ⊤        = no λ()
eq (φ ⇔ φ₁) ⊥        = no λ()
eq (φ ⇔ φ₁) (ψ ∧ ψ₁) = no λ()
eq (φ ⇔ φ₁) (ψ ∨ ψ₁) = no λ()
eq (φ ⇔ φ₁) (ψ ⊃ ψ₁) = no λ()
eq (φ ⇔ φ₁) (¬ ψ)    = no λ()
eq (φ ⇔ φ₁) (ψ ⇔ ψ₁) with eq φ ψ | eq φ₁ ψ₁
... | yes refl | yes refl  = yes refl
... | yes _    | no  φ₁≢ψ₁ = no (λ r → φ₁≢ψ₁ (⇔-injective₂ r))
... | no φ≢ψ   | _         = no (λ r → φ≢ψ   (⇔-injective₁ r))

-- Equality with ¬.
eq (¬ φ) (Var x)  = no λ()
eq (¬ φ) ⊤        = no λ()
eq (¬ φ) ⊥        = no λ()
eq (¬ φ) (ψ ∧ ψ₁) = no λ()
eq (¬ φ) (ψ ∨ ψ₁) = no λ()
eq (¬ φ) (ψ ⊃ ψ₁) = no λ()
eq (¬ φ) (ψ ⇔ ψ₁) = no λ()
eq (¬ φ) (¬ ψ) with eq φ ψ
... | yes refl = yes refl
... | no φ≢ψ   = no (λ r → φ≢ψ (¬-injective r))

-- Theorem.
subst
  : ∀ {Γ} {φ ψ}
  → φ ≡ ψ
  → Γ ⊢ φ
  → Γ ⊢ ψ
subst refl o = o

-- Theorem.
substΓ
  : ∀ {Γ₁ Γ₂} {φ}
  → Γ₁ ≡ Γ₂
  → Γ₁ ⊢ φ
  → Γ₂ ⊢ φ
substΓ refl o = o

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use `Algebra` or
-- `Algebra.Definitions` instead.
------------------------------------------------------------------------

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

open import Relation.Binary.Core using (Rel)

module Algebra.FunctionProperties {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

{-# WARNING_ON_IMPORT
"Algebra.FunctionProperties was deprecated in v1.2.
Use Algebra.Definitions instead."
#-}

open import Algebra.Core public
open import Algebra.Definitions _≈_ public

ext: agda


text:
{-# OPTIONS --type-in-type #-}

module Lec6 where

open import Lec1Done

ListF : Set -> Set -> Set
ListF X T = One + (X * T)

data List (X : Set) : Set where
  <_> : (ListF X) (List X) -> (List X)
infixr 4 _,-_

listF : {X T U : Set} -> (T -> U) -> (ListF X) T -> (ListF X) U
listF g (inl <>)      = inl <>
listF g (inr (x , t)) = inr (x , g t)

pattern []        = < inl <> >
pattern _,-_ x xs = < inr (x , xs) >

{-(-}
mkList : {X : Set} -> (ListF X) (List X) -> List X
mkList = <_>
{-
mkList (inl <>) = []
mkList (inr (x , xs)) = x ,- xs
-}
{-)-}

{-(-}
foldr : {X T : Set} -> ((ListF X) T -> T) -> List X -> T
foldr alg []        = alg (inl <>)
foldr alg (x ,- xs) = alg (inr (x , foldr alg xs))

ex1 = foldr mkList (1 ,- 2 ,- 3 ,- [])
{-)-}

{-(-}
length : {X : Set} -> List X -> Nat
length = foldr \ { (inl <>) -> zero ; (inr (x , n)) -> suc n }
{-)-}

record CoList (X : Set) : Set where
  coinductive
  field
    force : (ListF X) (CoList X)
open CoList

{-(-}
[]~ : {X : Set} -> CoList X
force []~ = inl <>

_,~_ : {X : Set} -> X -> CoList X -> CoList X
force (x ,~ xs) = inr (x , xs)
infixr 4 _,~_
{-)-}

{-(-}
unfoldr : {X S : Set} -> (S -> (ListF X) S) -> S -> CoList X
force (unfoldr coalg s) with coalg s
force (unfoldr coalg s) | inl <>       = inl <>
force (unfoldr coalg s) | inr (x , s') = inr (x , unfoldr coalg s')

ex2 = unfoldr force (1 ,~ 2 ,~ 3 ,~ []~)
{-)-}

{-(-}
repeat : {X : Set} -> X -> CoList X
repeat = unfoldr \ x -> inr (x , x)
{-)-}

{-(-}
prefix : {X : Set} -> Nat -> CoList X -> List X
prefix zero xs = []
prefix (suc n) xs with force xs
prefix (suc n) xs | inl <> = []
prefix (suc n) xs | inr (x , xs') = x ,- prefix n xs'

ex2' = prefix 3 ex2
{-)-}

StreamF : Set -> Set -> Set
StreamF X S = X * S

data Funny (X : Set) : Set where
  <_> : (StreamF X) (Funny X) -> Funny X

funny : {X : Set} -> Funny X -> Zero
funny < x , xf > = funny xf

record Stream (X : Set) : Set where
  coinductive
  field
    hdTl : (StreamF X) (Stream X)
open Stream

{-(-}
forever : {X : Set} -> X -> Stream X
fst (hdTl (forever x)) = x
snd (hdTl (forever x)) = forever x
{-)-}

natsFrom : Nat -> Stream Nat
fst (hdTl (natsFrom n)) = n
snd (hdTl (natsFrom n)) = natsFrom (suc n)

sprefix : {X : Set} -> Nat -> Stream X -> List X -- could be Vec X n
sprefix zero xs = []
sprefix (suc n) xs with hdTl xs
sprefix (suc n) xs | x , xs' = x ,- sprefix n xs'

{-(-}
unfold : {X S : Set} -> (S -> X * S) -> S -> Stream X
hdTl (unfold coalg s) with coalg s
hdTl (unfold coalg s) | x , s' = x , unfold coalg s'
{-)-}

natsFrom' : Nat -> Stream Nat
natsFrom' = unfold \ n -> n , suc n

data Two : Set where tt ff : Two

So : Two -> Set
So tt = One
So ff = Zero

isSuc : Nat -> Two
isSuc zero = ff
isSuc (suc n) = tt

{-
div : (x y : Nat) -> So (isSuc y) -> Nat
div x zero ()
div x (suc y) p = {!!}
-}

data Poly (X : Set) : Set where
  var' : X -> Poly X
  konst' : Two -> Poly X
  _+'_ _*'_ : Poly X -> Poly X -> Poly X

Eval : {X : Set} -> (X -> Set) -> Poly X -> Set
Eval var (var' x) = var x
Eval var (konst' b) = So b
Eval var (p +' q) = Eval var p + Eval var q
Eval var (p *' q) = Eval var p * Eval var q

eval : {X : Set}(u v : X -> Set)(p : Poly X) ->
       ((x : X) -> u x -> v x) ->
       Eval u p -> Eval v p
eval u v (var' i) f x = f i x
eval u v (konst' b) f x = x
eval u v (p +' q) f (inl x) = inl (eval u v p f x)
eval u v (p +' q) f (inr x) = inr (eval u v q f x)
eval u v (p *' q) f (x , y) = eval u v p f x , eval u v q f y

data Mu (p : Poly One) : Set where
  <_> : Eval (\ _ -> Mu p) p -> Mu p

NatP : Poly One
NatP = konst' tt +' var' <>

NAT = Mu NatP

ze : NAT
ze = < (inl <>) >

su : NAT -> NAT
su n = < (inr n) >

TreeP : Poly One
TreeP = konst' tt +' (var' <> *' var' <>)

-- What's a one-hole context in a Mu P?

Diff : Poly One -> Poly One
Diff (var' x) = konst' tt
Diff (konst' x) = konst' ff
Diff (p +' q) = Diff p +' Diff q
Diff (p *' q) = (Diff p *' q) +' (p *' Diff q)

plug : {X : Set}(p : Poly One) ->
       X -> Eval (\ _ -> X) (Diff p) ->
       Eval (\ _ -> X) p
plug (var' <>) x <> = x
plug (konst' b) x ()
plug (p +' q) x (inl xp') = inl (plug p x xp')
plug (p +' q) x (inr xq') = inr (plug q x xq')
plug (p *' q) x (inl (xp' , xq)) = plug p x xp' , xq
plug (p *' q) x (inr (xp , xq')) = xp , plug q x xq'

Context : Poly One -> Set
Context p = List (Eval (\ _ -> Mu p) (Diff p))

plugs : (p : Poly One) -> Mu p -> Context p -> Mu p
plugs p t []          = t
plugs p t (t' ,- t's) = plugs p < plug p t t' > t's

TernaryP : Poly One
TernaryP = konst' tt +' (var' <> *' (var' <> *' var' <>))

fold : (p : Poly One){T : Set}
       -> (Eval (\ _ -> T) p -> T)
       -> Mu p -> T
fold p {T} alg < x > = alg (evalFold p x)
  where
    evalFold : (q : Poly One)  -> Eval (\ _ -> Mu p) q -> Eval (\ _ -> T) q
    evalFold (var' <>) x = fold p alg x
    evalFold (konst' b) x = x
    evalFold (q +' r) (inl y) = inl (evalFold q y)
    evalFold (q +' r) (inr y) = inr (evalFold r y)
    evalFold (q *' r) (y , z) = evalFold q y , evalFold r z

record Nu (p : Poly One) : Set where
  coinductive
  field
    out : Eval (\ _ -> Nu p) p

-- What's the connection between polynomials and containers?

_-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> (I -> Set)
(S -:> T) i = S i -> T i

[_] : {I : Set} -> (I -> Set) -> Set
[ P ] = forall i -> P i    -- [_] {I} P = (i : I) -> P i

All : {X : Set} -> (X -> Set) -> (List X -> Set)
All P [] = One
All P (x ,- xs) = P x * All P xs

record _|>_ (I O : Set) : Set where
  field
    Cuts   : O -> Set                      -- given o : O, how may we cut it?
    inners : {o : O} -> Cuts o -> List I   -- given how we cut it, what are
                                           --   the shapes of its pieces?

record Cutting {I O}(C : I |> O)(P : I -> Set)(o : O) : Set where
  constructor _8><_               -- "scissors"
  open _|>_ C
  field
    cut     : Cuts o              -- we decide how to cut o
    pieces  : All P (inners cut)  -- then we give all the pieces.
infixr 3 _8><_

data Interior {I}(C : I |> I)(T : I -> Set)(i : I) : Set where
                                         -- either...
  tile : T i -> Interior C T i           -- we have a tile that fits, or...
  <_>  : Cutting C (Interior C T) i ->   -- ...we cut, then tile the pieces.
         Interior C T i

_+L_ : {X : Set} -> List X -> List X -> List X
[] +L ys = ys
(x ,- xs) +L ys = x ,- (xs +L ys)

polyCon : {I : Set} -> Poly I -> I |> One
_|>_.Cuts (polyCon p) <> = Eval (\ _ -> One) p
_|>_.inners (polyCon (var' i)) <> = i ,- []
_|>_.inners (polyCon (konst' x)) s = []
_|>_.inners (polyCon (p +' q)) (inl xp) = _|>_.inners (polyCon p) xp
_|>_.inners (polyCon (p +' q)) (inr xq) =  _|>_.inners (polyCon q) xq
_|>_.inners (polyCon (p *' q)) (sp , sq) =
  _|>_.inners (polyCon p) sp +L  _|>_.inners (polyCon q) sq

Choose : {I J : Set} -> (I -> Set) -> (J -> Set) -> (I + J) -> Set
Choose X Y (inl i) = X i
Choose X Y (inr j) = Y j

data MU {I           -- what sorts of "elements" do we store?
         J           -- what sorts of "nodes" do we have?
         : Set}
        (F : J -> Poly (I + J))    -- what is the structure of each sort of node?
        (X : I -> Set)             -- what are the elements?
        (j : J)                    -- what sort is the outermost node?
        : Set where
  <_> : Eval (Choose X (MU F X))   -- subnodes in recursive positions
             (F j)
    ->  MU F X j

VecF : Nat -> Poly (One + Nat)
VecF zero = konst' tt
VecF (suc n) = (var' (inl <>)) *' (var' (inr n))

VEC : Nat -> Set -> Set
VEC n X = MU VecF (\ _ -> X) n

vnil : {X : Set} -> VEC zero X
vnil = < <> >

vcons : {X : Set}{n : Nat} -> X -> VEC n X -> VEC (suc n) X
vcons x xs = < (x , xs) >

gmap : {I           -- what sorts of "elements" do we store?
         J           -- what sorts of "nodes" do we have?
         : Set}
        {F : J -> Poly (I + J)}    -- what is the structure of each sort of node?
        {X Y : I -> Set} ->             -- what are the elements?
        ((i : I) -> X i -> Y i) ->
        (j : J) ->
        MU F X j -> MU F Y j
gmapHelp : ∀ {I J} (F : J → Poly (I + J)) {X Y : I → Set}
             (w : Poly (I + J)) →
           ((i : I) → X i → Y i) →
           Eval (Choose X (MU F X)) w →
           Eval (Choose Y (MU F Y)) w
gmap {F = F} f j < xt > = < gmapHelp F (F j) f xt >
gmapHelp F (var' (inl i)) f x = f i x
gmapHelp F (var' (inr j)) f t = gmap f j t
gmapHelp F (konst' x) f v = v
gmapHelp F (p +' q) f (inl xp) = inl (gmapHelp F p f xp)
gmapHelp F (p +' q) f (inr xq) = inr (gmapHelp F q f xq)
gmapHelp F (p *' q) f (xp , xq) = (gmapHelp F p f xp) , (gmapHelp F q f xq)

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --safe #-}
module Cubical.Functions.Surjection where

open import Cubical.Core.Everything
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Functions.Embedding
open import Cubical.HITs.PropositionalTruncation as PropTrunc

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'
    f : A → B

isSurjection : (A → B) → Type _
isSurjection f = ∀ b → ∥ fiber f b ∥

_↠_ : Type ℓ → Type ℓ' → Type (ℓ-max ℓ ℓ')
A ↠ B = Σ[ f ∈ (A → B) ] isSurjection f

section→isSurjection : {g : B → A} → section f g → isSurjection f
section→isSurjection {g = g} s b = ∣ g b , s b ∣

isPropIsSurjection : isProp (isSurjection f)
isPropIsSurjection = isPropΠ λ _ → squash

isEquiv→isSurjection : isEquiv f → isSurjection f
isEquiv→isSurjection e b = ∣ fst (equiv-proof e b) ∣

isEquiv→isEmbedding×isSurjection : isEquiv f → isEmbedding f × isSurjection f
isEquiv→isEmbedding×isSurjection e = isEquiv→isEmbedding e , isEquiv→isSurjection e

isEmbedding×isSurjection→isEquiv : isEmbedding f × isSurjection f → isEquiv f
equiv-proof (isEmbedding×isSurjection→isEquiv {f = f} (emb , sur)) b =
  inhProp→isContr (PropTrunc.rec fib' (λ x → x) fib) fib'
  where
  hpf : hasPropFibers f
  hpf = isEmbedding→hasPropFibers emb

  fib : ∥ fiber f b ∥
  fib = sur b

  fib' : isProp (fiber f b)
  fib' = hpf b

isEquiv≃isEmbedding×isSurjection : isEquiv f ≃ isEmbedding f × isSurjection f
isEquiv≃isEmbedding×isSurjection = isoToEquiv (iso
  isEquiv→isEmbedding×isSurjection
  isEmbedding×isSurjection→isEquiv
  (λ _ → isOfHLevelΣ 1 isPropIsEmbedding (\ _ → isPropIsSurjection) _ _)
  (λ _ → isPropIsEquiv _ _ _))

-- obs: for epi⇒surjective to go through we require a stronger
-- hypothesis that one would expect:
-- f must cancel functions from a higher universe.
rightCancellable : (f : A → B) → Type _
rightCancellable {ℓ} {A} {ℓ'} {B} f = ∀ {C : Type (ℓ-suc (ℓ-max ℓ ℓ'))}
  → ∀ (g g' : B → C) → (∀ x → g (f x) ≡ g' (f x)) → ∀ y → g y ≡ g' y

-- This statement is in Mac Lane & Moerdijk (page 143, corollary 5).
epi⇒surjective : (f : A → B) → rightCancellable f → isSurjection f
epi⇒surjective f rc y = transport (fact₂ y) tt*
    where hasPreimage : (A → B) → B → _
          hasPreimage f y = ∥ fiber f y ∥

          fact₁ : ∀ x → Unit* ≡ hasPreimage f (f x)
          fact₁ x = hPropExt isPropUnit*
                             propTruncIsProp
                             (λ _ → ∣ (x , refl) ∣)
                             (λ _ → tt*)

          fact₂ : ∀ y → Unit* ≡ hasPreimage f y
          fact₂ = rc _ _ fact₁

max_stars_repo_name: LuuBluum/cubical

max_issues_repo_name: LuuBluum/cubical

max_forks_repo_name: LuuBluum/cubical


text:
module Prelude where

-- Simple data
open import Data.Bool public
  using (Bool ; false ; true ; not)
open import Data.Empty public
  using (⊥ ; ⊥-elim)
open import Data.Nat public
  using (
  ℕ ; zero ; suc
  ; _+_ ; _*_
  ; _≤_ ; z≤n ; s≤s
  ; _<_ ; _≟_ ; pred
  )
open import Data.Maybe public
  using (Maybe ; just ; nothing)
open import Data.Unit public
  using (⊤ ; tt)
open import Data.String public
  using (String)
  renaming (_++_ to _||_)

-- List-like modules

open import Data.List public
  using (
    List ; [] ; _∷_
    ; _++_ ; map ; drop
    ; reverse ; _∷ʳ_ ; length
    )
open import Data.List.All public
  using (All ; [] ; _∷_ ; lookup)
  renaming (map to ∀map)
open import Membership public
  using (
  _∈_ ; S ; Z
  ; _⊆_ ; _∷_ ; []
  ; ⊆-refl ; ⊆-suc ; find-∈
  ; lookup-parallel ; lookup-parallel-≡ ; translate-∈
  ; translate-⊆ ; ⊆-trans ; All-⊆
  ; ⊆++-l-refl ; lookup-all
  ; ∈-inc ; ⊆++-refl ; ⊆++comm'
  ; ⊆++comm ; ⊆-move ; ⊆-inc
  ; ⊆-skip
  )
open import Data.List.Any public
  using (Any ; here ; there)

open import Singleton public
  using ([_]ˡ ; [_]ᵃ ; [_]ᵐ)

-- Propositions and properties
open import Relation.Binary.PropositionalEquality public
  using (
    _≡_ ; refl ; sym
    ; cong ; cong₂ ; trans
    ; inspect ; [_]
    )
open import Relation.Nullary public
  using (Dec ; yes ; no ; ¬_)
open import Relation.Nullary.Decidable public
  using (⌊_⌋)

-- Other
open import Level public
  using    (Level; _⊔_ ; Lift ; lift)
  renaming (zero to lzero; suc to lsuc)
open import Size public
  using (Size ; Size<_ ; ↑_ ; ∞)

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
{-# OPTIONS --without-K #-}
module Model.Size where

open import Relation.Binary using (Rel ; Preorder ; IsPreorder)

import Data.Nat as ℕ
import Data.Nat.Induction as ℕ
import Data.Nat.Properties as ℕ
import Relation.Binary.Construct.On as On

open import Model.RGraph as RG using (RGraph)
open import Source.Size as S using (Δ ; Ω)
open import Source.Size.Substitution.Universe using (⟨_⟩ ; Sub⊢ᵤ)
open import Util.HoTT.HLevel
open import Util.Induction.WellFounded as WFInd using (Acc ; acc ; WellFounded)
open import Util.Prelude

import Source.Size.Substitution.Canonical as SC
import Source.Size.Substitution.Universe as S

open S.Ctx
open S.Size
open S.Sub
open S.Sub⊢ᵤ
open S.Var
open S._<_ hiding (<-trans)

infix 4 _<_ _≤_

private
  variable
    i j k : ℕ

{-
This is an encoding of the set of ordinals

  ℕ ∪ { ω + i | i ∈ ℕ }

i.e. of the ordinals below ω*2.
-}
data Size : Set where
  zero+ : (i : ℕ) → Size
  ∞+ : (i : ℕ) → Size

variable
  n m o : Size

nat : ℕ → Size
nat = zero+

abstract
  zero+-inj : zero+ i ≡ zero+ j → i ≡ j
  zero+-inj refl = refl

  zero+-≡-canon : (p : zero+ i ≡ zero+ j) → p ≡ cong zero+ (zero+-inj p)
  zero+-≡-canon refl = refl

  ∞+-inj : ∞+ i ≡ ∞+ j → i ≡ j
  ∞+-inj refl = refl

  ∞+-≡-canon : (p : ∞+ i ≡ ∞+ j) → p ≡ cong ∞+ (∞+-inj p)
  ∞+-≡-canon refl = refl

  Size-IsSet : IsSet Size
  Size-IsSet {zero+ i} {zero+ j} p refl
    = trans (zero+-≡-canon p) (cong (cong zero+) (ℕ.≡-irrelevant _ _))
  Size-IsSet {∞+ i} {∞+ j} p refl
    = trans (∞+-≡-canon p) (cong (cong ∞+) (ℕ.≡-irrelevant _ _))

data _<_ : (n m : Size) → Set where
  zero+ : (i<j : i ℕ.< j) → zero+ i < zero+ j
  ∞+ : (i<j : i ℕ.< j) → ∞+ i < ∞+ j
  zero<∞ : zero+ i < ∞+ j

data _≤_ (n m : Size) : Set where
  reflexive : n ≡ m → n ≤ m
  <→≤ : n < m → n ≤ m

pattern ≤-refl = reflexive refl

abstract
  <-trans : n < m → m < o → n < o
  <-trans (zero+ i<j) (zero+ j<k) = zero+ (ℕ.<-trans i<j j<k)
  <-trans (zero+ i<j) zero<∞ = zero<∞
  <-trans (∞+ i<j) (∞+ j<k) = ∞+ (ℕ.<-trans i<j j<k)
  <-trans zero<∞ (∞+ i<j) = zero<∞

  ≤→<→< : n ≤ m → m < o → n < o
  ≤→<→< ≤-refl m<o = m<o
  ≤→<→< (<→≤ n<m) m<o = <-trans n<m m<o

  <→≤→< : n < m → m ≤ o → n < o
  <→≤→< n<m ≤-refl = n<m
  <→≤→< n<m (<→≤ m<o) = <-trans n<m m<o

  ≤-trans : n ≤ m → m ≤ o → n ≤ o
  ≤-trans n≤m ≤-refl = n≤m
  ≤-trans n≤m (<→≤ m<o) = <→≤ (≤→<→< n≤m m<o)

⟦zero⟧ ⟦∞⟧ : Size
⟦zero⟧ = zero+ 0
⟦∞⟧ = ∞+ 0

⟦suc⟧ : Size → Size
⟦suc⟧ (zero+ i) = zero+ (suc i)
⟦suc⟧ (∞+ i) = ∞+ (suc i)

abstract
  ⟦zero⟧<⟦suc⟧ : ⟦zero⟧ < ⟦suc⟧ n
  ⟦zero⟧<⟦suc⟧ {zero+ i} = zero+ (ℕ.s≤s ℕ.z≤n)
  ⟦zero⟧<⟦suc⟧ {∞+ i} = zero<∞

  ⟦zero⟧<⟦∞⟧ : ⟦zero⟧ < ⟦∞⟧
  ⟦zero⟧<⟦∞⟧ = zero<∞

  ⟦suc⟧<⟦suc⟧ : n < m → ⟦suc⟧ n < ⟦suc⟧ m
  ⟦suc⟧<⟦suc⟧ (zero+ i<j) = zero+ (ℕ.s≤s i<j)
  ⟦suc⟧<⟦suc⟧ (∞+ i<j) = ∞+ (ℕ.s≤s i<j)
  ⟦suc⟧<⟦suc⟧ zero<∞ = zero<∞

  ⟦suc⟧<⟦∞⟧ : n < ⟦∞⟧ → ⟦suc⟧ n < ⟦∞⟧
  ⟦suc⟧<⟦∞⟧ zero<∞ = zero<∞

  <⟦suc⟧ : n < ⟦suc⟧ n
  <⟦suc⟧ {zero+ i} = zero+ (ℕ.s≤s ℕ.≤-refl)
  <⟦suc⟧ {∞+ i} = ∞+ (ℕ.s≤s ℕ.≤-refl)

Size< : Size → Set
Size< n = ∃[ m ] (m < n)

mutual
  ⟦_⟧Δ′ : S.Ctx → Set
  ⟦ [] ⟧Δ′ = ⊤
  ⟦ Δ ∙ n ⟧Δ′ = Σ[ δ ∈ ⟦ Δ ⟧Δ′ ] (Size< (⟦ n ⟧n′ δ))

  ⟦_⟧x′ : S.Var Δ → ⟦ Δ ⟧Δ′ → Size
  ⟦ zero ⟧x′ (δ , n , _) = n
  ⟦ suc x ⟧x′ (δ , _ , _) = ⟦ x ⟧x′ δ

  ⟦_⟧n′ : S.Size Δ → ⟦ Δ ⟧Δ′ → Size
  ⟦ var x ⟧n′ = ⟦ x ⟧x′
  ⟦ ∞ ⟧n′ _ = ⟦∞⟧
  ⟦ zero ⟧n′ _ = ⟦zero⟧
  ⟦ suc n ⟧n′ = ⟦suc⟧ ∘ ⟦ n ⟧n′

abstract
  ⟦wk⟧ : ∀ (n m : S.Size Δ) {δ} → ⟦ S.wk {n = n} m ⟧n′ δ ≡ ⟦ m ⟧n′ (proj₁ δ)
  ⟦wk⟧ n (var x) = refl
  ⟦wk⟧ n ∞ = refl
  ⟦wk⟧ n zero = refl
  ⟦wk⟧ n (suc m) = cong ⟦suc⟧ (⟦wk⟧ n m)

  ⟦<⟧ₓ : ∀ (x : S.Var Δ) {δ}
    → ⟦ x ⟧x′ δ < ⟦ S.bound x ⟧n′ δ
  ⟦<⟧ₓ {Δ ∙ n} zero {δ , m , m<n} = subst (m <_) (sym (⟦wk⟧ n n)) m<n
  ⟦<⟧ₓ {Δ ∙ n} (suc x) {δ , m , m<n}
    = subst (⟦ x ⟧x′ δ <_) (sym (⟦wk⟧ n (S.bound x))) (⟦<⟧ₓ x)

  ⟦<⟧ : ∀ {n m : S.Size Δ} {δ}
    → n S.< m
    → ⟦ n ⟧n′ δ < ⟦ m ⟧n′ δ
  ⟦<⟧ (var {x = x} refl) = ⟦<⟧ₓ x
  ⟦<⟧ zero<suc = ⟦zero⟧<⟦suc⟧
  ⟦<⟧ zero<∞ = ⟦zero⟧<⟦∞⟧
  ⟦<⟧ (suc<suc n<m) = ⟦suc⟧<⟦suc⟧ (⟦<⟧ n<m)
  ⟦<⟧ (suc<∞ n<m) = ⟦suc⟧<⟦∞⟧ (⟦<⟧ n<m)
  ⟦<⟧ (S.<-trans n<m m<o) = <-trans (⟦<⟧ n<m) (⟦<⟧ m<o)
  ⟦<⟧ <suc = <⟦suc⟧

  <-irrefl : ¬ n < n
  <-irrefl {zero+ i} (zero+ i<i) = ℕ.<⇒≢ i<i refl
  <-irrefl {∞+ i} (∞+ i<i) = ℕ.<⇒≢ i<i refl

  ≤-antisym : n ≤ m → m ≤ n → n ≡ m
  ≤-antisym ≤-refl m≤n = refl
  ≤-antisym (<→≤ n<m) m≤n = ⊥-elim (<-irrefl (<→≤→< n<m m≤n))

  <-IsProp : IsProp (n < m)
  <-IsProp (zero+ i<j) (zero+ i<j₁) = cong zero+ (ℕ.<-irrelevant _ _)
  <-IsProp (∞+ i<j) (∞+ i<j₁) = cong ∞+ (ℕ.<-irrelevant _ _)
  <-IsProp zero<∞ zero<∞ = refl

  ≤-IsProp : IsProp (n ≤ m)
  ≤-IsProp (reflexive p) (reflexive q) = cong reflexive (Size-IsSet _ _)
  ≤-IsProp ≤-refl (<→≤ q) = ⊥-elim (<-irrefl q)
  ≤-IsProp (<→≤ p) ≤-refl = ⊥-elim (<-irrefl p)
  ≤-IsProp (<→≤ p) (<→≤ q) = cong <→≤ (<-IsProp p q)

  Size<-≡⁺ : (m k : Size< n) → proj₁ m ≡ proj₁ k → m ≡ k
  Size<-≡⁺ (m , _) (k , _) refl = cong (m ,_) (<-IsProp _ _)

  Size<-IsSet : ∀ {n} → IsSet (Size< n)
  Size<-IsSet = Σ-IsSet Size-IsSet λ _ → IsOfHLevel-suc 1 <-IsProp

  ⟦Δ⟧-IsSet : ∀ Δ → IsSet ⟦ Δ ⟧Δ′
  ⟦Δ⟧-IsSet [] = ⊤-IsSet
  ⟦Δ⟧-IsSet (Δ ∙ n) = Σ-IsSet (⟦Δ⟧-IsSet Δ) λ _ → Size<-IsSet

⟦Δ⟧-HSet : S.Ctx → HSet 0ℓ
⟦Δ⟧-HSet Δ = HLevel⁺ _ (⟦Δ⟧-IsSet Δ)

abstract
  ⟦Δ∙n⟧-≡⁺ : ∀ Δ (n : S.Size Δ) {δ δ′ : ⟦ Δ ⟧Δ′} {m m′ : Size}
    → (m<n : m < ⟦ n ⟧n′ δ)
    → (m′<n : m′ < ⟦ n ⟧n′ δ′)
    → δ ≡ δ′
    → m ≡ m′
    → (δ , m , m<n) ≡ (δ′ , m′ , m′<n)
  ⟦Δ∙n⟧-≡⁺  Δ n {δ} _ _ refl eq₂
    = cong (δ ,_) (Size<-≡⁺ _ _ eq₂)

  zero+-<ℕ-acc→<-acc : Acc ℕ._<_ i → Acc _<_ (zero+ i)
  zero+-<ℕ-acc→<-acc (acc rs) = acc λ where
    (zero+ i) (zero+ i<j) → zero+-<ℕ-acc→<-acc (rs i i<j)

  zero+-acc : Acc _<_ (zero+ i)
  zero+-acc = zero+-<ℕ-acc→<-acc (ℕ.<-wellFounded _)

  ∞+-<ℕ-acc→<-acc : Acc ℕ._<_ i → Acc _<_ (∞+ i)
  ∞+-<ℕ-acc→<-acc (acc rs) = acc λ where
    (∞+ i) (∞+ i<j) → ∞+-<ℕ-acc→<-acc (rs i i<j)
    (zero+ i) zero<∞ → zero+-acc

  ∞+-acc : Acc _<_ (∞+ i)
  ∞+-acc = ∞+-<ℕ-acc→<-acc (ℕ.<-wellFounded _)

  <-wf : WellFounded _<_
  <-wf m = acc λ where
    _ (zero+ i<j) → zero+-acc
    _ (∞+ i<j) → ∞+-acc
    _ zero<∞ → zero+-acc

open WFInd.Build <-wf public using () renaming
  ( wfInd to <-ind
  ; wfRec to <-rec
  ; wfInd-unfold to <-ind-unfold
  ; wfRec-unfold to <-rec-unfold
  ; wfInd-ind to <-ind-ind
  ; wfIndΣ to <-indΣ
  ; wfIndΣ-unfold to <-indΣ-unfold
  ; wfIndΣ′ to <-indΣ′
  )

<-ind-ind₂ = WFInd.wfInd-ind₂ <-wf

mutual
  ⟦_⟧σ′ : ∀ {σ} → σ ∶ Δ ⇒ᵤ Ω → ⟦ Δ ⟧Δ′ → ⟦ Ω ⟧Δ′
  ⟦ Id ⟧σ′ δ = δ
  ⟦ comp σ τ ⟧σ′ δ = ⟦ τ ⟧σ′ (⟦ σ ⟧σ′ δ)
  ⟦ Wk ⟧σ′ (δ , m) = δ
  ⟦ Lift {n = n} σ refl ⟧σ′ (δ , m , m<n)
    = ⟦ σ ⟧σ′ δ , m , subst (m <_) (⟦sub⟧ σ n) m<n
  ⟦ Sing {n = n} n<m ⟧σ′ δ = δ , ⟦ n ⟧n′ δ , ⟦<⟧ n<m
  ⟦ Skip ⟧σ′ ((δ , m , m<n) , k , k<m) = δ , k , <-trans k<m m<n

  abstract
    ⟦subV′⟧ : ∀ {σ} (⊢σ : σ ∶ Δ ⇒ᵤ Ω) (x : S.Var Ω) {δ}
      → ⟦ S.subV′ σ x ⟧n′ δ ≡ ⟦ x ⟧x′ (⟦ ⊢σ ⟧σ′ δ)
    ⟦subV′⟧ Id x = refl
    ⟦subV′⟧ (comp {σ = σ} {τ = τ} ⊢σ ⊢τ) x
      = trans (⟦sub′⟧ ⊢σ (S.subV′ τ x)) (⟦subV′⟧ ⊢τ x)
    ⟦subV′⟧ Wk x = refl
    ⟦subV′⟧ (Lift ⊢σ refl) zero {δ , m} = refl
    ⟦subV′⟧ (Lift {σ = σ} {n = n} ⊢σ refl) (suc x) {δ , m}
      rewrite ⟦wk⟧ (S.sub σ n) (S.subV′ σ x) {δ , m}
      = ⟦subV′⟧ ⊢σ x
    ⟦subV′⟧ (Sing n<m) zero = refl
    ⟦subV′⟧ (Sing n<m) (suc x) = refl
    ⟦subV′⟧ Skip zero = refl
    ⟦subV′⟧ Skip (suc x) = refl

    ⟦sub′⟧ : ∀ {σ} (⊢σ : σ ∶ Δ ⇒ᵤ Ω) (n : S.Size Ω) {δ}
      → ⟦ S.sub′ σ n ⟧n′ δ ≡ ⟦ n ⟧n′ (⟦ ⊢σ ⟧σ′ δ)
    ⟦sub′⟧ σ (var x) = ⟦subV′⟧ σ x
    ⟦sub′⟧ σ ∞ = refl
    ⟦sub′⟧ σ zero = refl
    ⟦sub′⟧ σ (suc n) = cong ⟦suc⟧ (⟦sub′⟧ σ n)

    ⟦sub⟧ :  ∀ {σ} (⊢σ : σ ∶ Δ ⇒ᵤ Ω) (n : S.Size Ω) {δ}
      → ⟦ S.sub σ n ⟧n′ δ ≡ ⟦ n ⟧n′ (⟦ ⊢σ ⟧σ′ δ)
    ⟦sub⟧ {σ = σ} ⊢σ n {δ}
      = trans (cong (λ k → ⟦ k ⟧n′ δ) (sym (S.sub′≡sub σ n))) (⟦sub′⟧ ⊢σ n)

abstract
  ⟦subV⟧ : ∀ {σ} (⊢σ : σ ∶ Δ ⇒ᵤ Ω) (x : S.Var Ω) {δ}
    → ⟦ S.subV σ x ⟧n′ δ ≡ ⟦ x ⟧x′ (⟦ ⊢σ ⟧σ′ δ)
  ⟦subV⟧ {σ = σ} ⊢σ x {δ}
    = trans (cong (λ k → ⟦ k ⟧n′ δ) (sym (S.subV′≡subV σ x))) (⟦subV′⟧ ⊢σ x)

  ⟦⟧σ-param : ∀ {σ} (p q : σ ∶ Δ ⇒ᵤ Ω) {δ}
    → ⟦ p ⟧σ′ δ ≡ ⟦ q ⟧σ′ δ
  ⟦⟧σ-param Id Id = refl
  ⟦⟧σ-param (comp p p′) (comp q q′)
    = trans (⟦⟧σ-param p′ q′) (cong (⟦ q′ ⟧σ′) (⟦⟧σ-param p q))
  ⟦⟧σ-param Wk Wk = refl
  ⟦⟧σ-param {Ω = Ω ∙ m} (Lift p refl) (Lift q m≡n[σ]₁)
    rewrite S.Size-IsSet m≡n[σ]₁ refl
    = ⟦Δ∙n⟧-≡⁺ Ω m _ _ (⟦⟧σ-param p q) refl
  ⟦⟧σ-param {Δ = Δ} {σ = Sing {m = m} n} (Sing n<m) (Sing n<m₁)
    = ⟦Δ∙n⟧-≡⁺ Δ m (⟦<⟧ n<m) (⟦<⟧ n<m₁) refl refl
  ⟦⟧σ-param Skip Skip = refl

⟦_⟧Δ : S.Ctx → RGraph
⟦ Δ ⟧Δ = record
  { ObjHSet = ⟦Δ⟧-HSet Δ
  ; eqHProp = λ _ _ → ⊤-HProp
  }

Sizes : RGraph
Sizes = record
  { ObjHSet = HLevel⁺ Size Size-IsSet
  ; eqHProp = λ _ _ → ⊤-HProp
  }

⟦_⟧n : ∀ {Δ} (n : S.Size Δ) → ⟦ Δ ⟧Δ RG.⇒ Sizes
⟦ n ⟧n = record
  { fobj = ⟦ n ⟧n′
  }

⟦_⟧σ : ∀ {Δ Ω σ} → σ ∶ Δ ⇒ᵤ Ω → ⟦ Δ ⟧Δ RG.⇒ ⟦ Ω ⟧Δ
⟦ σ ⟧σ = record
  { fobj = ⟦ σ ⟧σ′
  }

data _≤′_ : (n m : Size) → Set where
  zero+ : (i≤j : i ℕ.≤ j) → zero+ i ≤′ zero+ j
  ∞+ : (i≤j : i ℕ.≤ j) → ∞+ i ≤′ ∞+ j
  zero<∞ : zero+ i ≤′ ∞+ j

abstract
  ≤→≤′ : n ≤ m → n ≤′ m
  ≤→≤′ {zero+ i} ≤-refl = zero+ ℕ.≤-refl
  ≤→≤′ {∞+ i} ≤-refl = ∞+ ℕ.≤-refl
  ≤→≤′ (<→≤ (zero+ i<j)) = zero+ (ℕ.<⇒≤ i<j)
  ≤→≤′ (<→≤ (∞+ i<j)) = ∞+ (ℕ.<⇒≤ i<j)
  ≤→≤′ (<→≤ zero<∞) = zero<∞

  ≤′→≤ : n ≤′ m → n ≤ m
  ≤′→≤ (zero+ i≤j) with ℕ.≤⇒≤′ i≤j
  ... | ℕ.≤′-refl = ≤-refl
  ... | ℕ.≤′-step i≤′j = <→≤ (zero+ (ℕ.s≤s (ℕ.≤′⇒≤ i≤′j)))
  ≤′→≤ (∞+ i≤j) with ℕ.≤⇒≤′ i≤j
  ... | ℕ.≤′-refl = ≤-refl
  ... | ℕ.≤′-step i≤′j = <→≤ (∞+ (ℕ.s≤s (ℕ.≤′⇒≤ i≤′j)))
  ≤′→≤ zero<∞ = <→≤ zero<∞

  0≤n : ⟦zero⟧ ≤ n
  0≤n {zero+ zero} = ≤-refl
  0≤n {zero+ (suc i)} = <→≤ (zero+ (ℕ.s≤s ℕ.z≤n))
  0≤n {∞+ i} = <→≤ zero<∞

  n<m→Sn≤m : n < m → ⟦suc⟧ n ≤ m
  n<m→Sn≤m (zero+ (ℕ.s≤s i≤j)) = ≤′→≤ (zero+ (ℕ.s≤s i≤j))
  n<m→Sn≤m (∞+ (ℕ.s≤s i≤j)) = ≤′→≤ (∞+ (ℕ.s≤s i≤j))
  n<m→Sn≤m zero<∞ = <→≤ zero<∞

  Sn≤m→n<m : ⟦suc⟧ n ≤ m → n < m
  Sn≤m→n<m ≤-refl = <⟦suc⟧
  Sn≤m→n<m (<→≤ Sn<m) = <-trans <⟦suc⟧ Sn<m

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
open import Nat
open import Prelude
open import contexts
open import core
open import type-assignment-unicity

module canonical-indeterminate-forms where

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at base type
  data cif-base : (Δ : hctx) (d : ihexp) → Set where
    CIFBEHole : ∀ {Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇-⦈⟨ u , σ ⟩) ×
         ((u :: b [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
       → cif-base Δ d
    CIFBNEHole : ∀ {Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ] Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: b [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-base Δ d
    CIFBAp : ∀ {Δ d} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ] Σ[ τ2 ∈ htyp ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2 ==> b) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d1' : ihexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-base Δ d
    CIFBCast : ∀ {Δ d} →
      Σ[ d' ∈ ihexp ]
        ((d == d' ⟨ ⦇-⦈ ⇒ b ⟩) ×
         (Δ , ∅ ⊢ d' :: ⦇-⦈) ×
         (d' indet) ×
         ((d'' : ihexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇-⦈ ⟩))
        )
        → cif-base Δ d
    CIFBFailedCast : ∀ {Δ d} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == d' ⟨ τ' ⇒⦇-⦈⇏ b ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (τ' ≠ b)
        )
       → cif-base Δ d

  canonical-indeterminate-forms-base : ∀{Δ d} →
                                       Δ , ∅ ⊢ d :: b →
                                       d indet →
                                       cif-base Δ d
  canonical-indeterminate-forms-base TAConst ()
  canonical-indeterminate-forms-base (TAVar x₁) ()
  canonical-indeterminate-forms-base (TAAp wt wt₁) (IAp x ind x₁) = CIFBAp (_ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-base (TAEHole x x₁) IEHole = CIFBEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-base (TANEHole x wt x₁) (INEHole x₂) = CIFBNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-base (TACast wt x) (ICastHoleGround x₁ ind x₂) = CIFBCast (_ , refl , wt , ind , x₁)
  canonical-indeterminate-forms-base (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) = CIFBFailedCast (_ , _ , refl , x , x₅ , x₇)

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at arrow type
  data cif-arr : (Δ : hctx) (d : ihexp) (τ1 τ2 : htyp) → Set where
    CIFAEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇-⦈⟨ u , σ ⟩) ×
         ((u :: (τ1 ==> τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-arr Δ d τ1 τ2
    CIFANEHole : ∀{d Δ τ1 τ2} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: (τ1 ==> τ2) [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
        → cif-arr Δ d τ1 τ2
    CIFAAp : ∀{d Δ τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ] Σ[ τ2' ∈ htyp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: τ2' ==> (τ1 ==> τ2)) ×
         (Δ , ∅ ⊢ d2 :: τ2') ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d1' : ihexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFACast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ1 ∈ htyp ] Σ[ τ2 ∈ htyp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
        ((d == d' ⟨ (τ1' ==> τ2') ⇒ (τ1 ==> τ2) ⟩) ×
          (Δ , ∅ ⊢ d' :: τ1' ==> τ2') ×
          (d' indet) ×
          ((τ1' ==> τ2') ≠ (τ1 ==> τ2))
        )
       → cif-arr Δ d τ1 τ2
    CIFACastHole : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ]
        ((d == (d' ⟨ ⦇-⦈ ⇒ ⦇-⦈ ==> ⦇-⦈ ⟩)) ×
         (τ1 == ⦇-⦈) ×
         (τ2 == ⦇-⦈) ×
         (Δ , ∅ ⊢ d' :: ⦇-⦈) ×
         (d' indet) ×
         ((d'' : ihexp) (τ' : htyp) → d' ≠ (d'' ⟨ τ' ⇒ ⦇-⦈ ⟩))
        )
        → cif-arr Δ d τ1 τ2
    CIFAFailedCast : ∀{d Δ τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
          ((d == (d' ⟨ τ' ⇒⦇-⦈⇏ ⦇-⦈ ==> ⦇-⦈ ⟩) ) ×
           (τ1 == ⦇-⦈) ×
           (τ2 == ⦇-⦈) ×
           (Δ , ∅ ⊢ d' :: τ') ×
           (τ' ground) ×
           (τ' ≠ (⦇-⦈ ==> ⦇-⦈))
           )
          → cif-arr Δ d τ1 τ2

  canonical-indeterminate-forms-arr : ∀{Δ d τ1 τ2 } →
                                       Δ , ∅ ⊢ d :: (τ1 ==> τ2) →
                                       d indet →
                                       cif-arr Δ d τ1 τ2
  canonical-indeterminate-forms-arr (TAVar x₁) ()
  canonical-indeterminate-forms-arr (TALam _ wt) ()
  canonical-indeterminate-forms-arr (TAAp wt wt₁) (IAp x ind x₁) = CIFAAp (_ , _ , _ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-arr (TAEHole x x₁) IEHole = CIFAEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-arr (TANEHole x wt x₁) (INEHole x₂) = CIFANEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-arr (TACast wt x) (ICastArr x₁ ind) = CIFACast (_ , _ , _ , _ , _ , refl , wt , ind , x₁)
  canonical-indeterminate-forms-arr (TACast wt TCHole2) (ICastHoleGround x₁ ind GHole) = CIFACastHole (_ , refl , refl , refl , wt , ind , x₁)
  canonical-indeterminate-forms-arr (TAFailedCast x x₁ GHole x₃) (IFailedCast x₄ x₅ GHole x₇) = CIFAFailedCast (_ , _ , refl , refl , refl , x , x₅ , x₇)

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for indeterminates at hole type
  data cif-hole : (Δ : hctx) (d : ihexp) → Set where
    CIFHEHole : ∀ {Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ Γ ∈ tctx ]
        ((d == ⦇-⦈⟨ u , σ ⟩) ×
         ((u :: ⦇-⦈ [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-hole Δ d
    CIFHNEHole : ∀ {Δ d} →
      Σ[ u ∈ Nat ] Σ[ σ ∈ env ] Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ] Σ[ Γ ∈ tctx ]
        ((d == ⦇⌜ d' ⌟⦈⟨ u , σ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (d' final) ×
         ((u :: ⦇-⦈ [ Γ ]) ∈ Δ) ×
         (Δ , ∅ ⊢ σ :s: Γ)
        )
      → cif-hole Δ d
    CIFHAp : ∀ {Δ d} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ] Σ[ τ2 ∈ htyp ]
        ((d == d1 ∘ d2) ×
         (Δ , ∅ ⊢ d1 :: (τ2 ==> ⦇-⦈)) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         (d1 indet) ×
         (d2 final) ×
         ((τ3 τ4 τ3' τ4' : htyp) (d1' : ihexp) → d1 ≠ (d1' ⟨ τ3 ==> τ4 ⇒ τ3' ==> τ4' ⟩))
        )
      → cif-hole Δ d
    CIFHCast : ∀ {Δ d} →
      Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
        ((d == d' ⟨ τ' ⇒ ⦇-⦈ ⟩) ×
         (Δ , ∅ ⊢ d' :: τ') ×
         (τ' ground) ×
         (d' indet)
        )
      → cif-hole Δ d

  canonical-indeterminate-forms-hole : ∀{Δ d} →
                                       Δ , ∅ ⊢ d :: ⦇-⦈ →
                                       d indet →
                                       cif-hole Δ d
  canonical-indeterminate-forms-hole (TAVar x₁) ()
  canonical-indeterminate-forms-hole (TAAp wt wt₁) (IAp x ind x₁) = CIFHAp (_ , _ , _ , refl , wt , wt₁ , ind , x₁ , x)
  canonical-indeterminate-forms-hole (TAEHole x x₁) IEHole = CIFHEHole (_ , _ , _ , refl , x , x₁)
  canonical-indeterminate-forms-hole (TANEHole x wt x₁) (INEHole x₂) = CIFHNEHole (_ , _ , _ , _ , _ , refl , wt , x₂ , x , x₁)
  canonical-indeterminate-forms-hole (TACast wt x) (ICastGroundHole x₁ ind) = CIFHCast (_ , _ , refl , wt , x₁ , ind)
  canonical-indeterminate-forms-hole (TACast wt x) (ICastHoleGround x₁ ind ())
  canonical-indeterminate-forms-hole (TAFailedCast x x₁ () x₃) (IFailedCast x₄ x₅ x₆ x₇)

  canonical-indeterminate-forms-coverage : ∀{Δ d τ} →
                                           Δ , ∅ ⊢ d :: τ →
                                           d indet →
                                           τ ≠ b →
                                           ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
                                           τ ≠ ⦇-⦈ →
                                           ⊥
  canonical-indeterminate-forms-coverage TAConst () nb na nh
  canonical-indeterminate-forms-coverage (TAVar x₁) () nb na nh
  canonical-indeterminate-forms-coverage (TALam _ wt) () nb na nh
  canonical-indeterminate-forms-coverage {τ = b} (TAAp wt wt₁) (IAp x ind x₁) nb na nh = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇-⦈} (TAAp wt wt₁) (IAp x ind x₁) nb na nh = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TAAp wt wt₁) (IAp x ind x₁) nb na nh = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = b} (TAEHole x x₁) IEHole nb na nh = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇-⦈} (TAEHole x x₁) IEHole nb na nh = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TAEHole x x₁) IEHole nb na nh = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = b} (TANEHole x wt x₁) (INEHole x₂) nb na nh = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇-⦈} (TANEHole x wt x₁) (INEHole x₂) nb na nh = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TANEHole x wt x₁) (INEHole x₂) nb na nh = na τ τ₁ refl
  canonical-indeterminate-forms-coverage (TACast wt x) (ICastArr x₁ ind) nb na nh = na _ _ refl
  canonical-indeterminate-forms-coverage (TACast wt x) (ICastGroundHole x₁ ind) nb na nh = nh refl
  canonical-indeterminate-forms-coverage {τ = b} (TACast wt x) (ICastHoleGround x₁ ind x₂) nb na nh = nb refl
  canonical-indeterminate-forms-coverage {τ = ⦇-⦈} (TACast wt x) (ICastHoleGround x₁ ind x₂) nb na nh = nh refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TACast wt x) (ICastHoleGround x₁ ind x₂) nb na nh = na τ τ₁ refl
  canonical-indeterminate-forms-coverage {τ = b} (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) = λ z _ _₁ → z refl
  canonical-indeterminate-forms-coverage {τ = ⦇-⦈} (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) = λ _ _₁ z → z refl
  canonical-indeterminate-forms-coverage {τ = τ ==> τ₁} (TAFailedCast x x₁ x₂ x₃) (IFailedCast x₄ x₅ x₆ x₇) = λ _ z _₁ → z τ τ₁ refl

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
module Cats.Util.SetoidReasoning where

open import Relation.Binary.SetoidReasoning public

open import Relation.Binary using (Setoid)
open import Relation.Binary.EqReasoning as EqR using (_IsRelatedTo_)

infixr 2 _≡⟨⟩_

_≡⟨⟩_ : ∀ {c l} {S : Setoid  c l} → ∀ x {y} → _IsRelatedTo_ S x y → _IsRelatedTo_ S x y
_≡⟨⟩_ {S = S} = EqR._≡⟨⟩_ S

triangle : ∀ {l l′} (S : Setoid l l′) →
  let open Setoid S in
  ∀ m {x y}
  → x ≈ m
  → y ≈ m
  → x ≈ y
triangle S m x≈m y≈m = trans x≈m (sym y≈m)
  where
    open Setoid S

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


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

module Fragment.Extensions.CSemigroup.Base where

open import Fragment.Equational.Theory.Bundles

open import Fragment.Algebra.Signature
open import Fragment.Algebra.Free Σ-magma hiding (_~_)
open import Fragment.Algebra.Homomorphism Σ-magma
open import Fragment.Algebra.Algebra Σ-magma
  using (Algebra; IsAlgebra; Interpretation; Congruence)

open import Fragment.Equational.FreeExtension Θ-csemigroup
  using (FreeExtension; IsFreeExtension)
open import Fragment.Equational.Model Θ-csemigroup
open import Fragment.Extensions.CSemigroup.Monomial

open import Fragment.Setoid.Morphism using (_↝_)

open import Level using (Level; _⊔_)

open import Data.Nat using (ℕ)
open import Data.Fin using (#_)

open import Data.Vec using (Vec; []; _∷_; map)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using ([]; _∷_)

import Relation.Binary.Reasoning.Setoid as Reasoning
open import Relation.Binary using (Setoid; IsEquivalence)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

private
  variable
    a ℓ : Level

module _ (A : Model {a} {ℓ}) (n : ℕ) where

  private

    open module A = Setoid ∥ A ∥/≈

    _·_ : ∥ A ∥ → ∥ A ∥ → ∥ A ∥
    x · y = A ⟦ • ⟧ (x ∷ y ∷ [])

    ·-cong : ∀ {x y z w} → x ≈ y → z ≈ w → x · z ≈ y · w
    ·-cong x≈y z≈w = (A ⟦ • ⟧-cong) (x≈y ∷ z≈w ∷ [])

    ·-comm : ∀ (x y : ∥ A ∥) → x · y ≈ y · x
    ·-comm x y = ∥ A ∥ₐ-models comm (env {A = ∥ A ∥ₐ} (x ∷ y ∷ []))

    ·-assoc : ∀ (x y z : ∥ A ∥) → (x · y) · z ≈ x · (y · z)
    ·-assoc x y z = ∥ A ∥ₐ-models assoc (env {A = ∥ A ∥ₐ} (x ∷ y ∷ z ∷ []))

    data Blob : Set a where
      sta  : ∥ A ∥ → Blob
      dyn  : ∥ J' n ∥ → Blob
      blob : ∥ J' n ∥ → ∥ A ∥ → Blob

    infix 6 _≋_

    data _≋_ : Blob → Blob → Set (a ⊔ ℓ) where
      sta  : ∀ {x y} → x ≈ y → sta x ≋ sta y
      dyn  : ∀ {xs ys} → xs ≡ ys → dyn xs ≋ dyn ys
      blob : ∀ {x y xs ys} → xs ≡ ys → x ≈ y
             → blob xs x ≋ blob ys y

    ≋-refl : ∀ {x} → x ≋ x
    ≋-refl {x = sta x}     = sta A.refl
    ≋-refl {x = dyn xs}    = dyn PE.refl
    ≋-refl {x = blob xs x} = blob PE.refl A.refl

    ≋-sym : ∀ {x y} → x ≋ y → y ≋ x
    ≋-sym (sta p)     = sta (A.sym p)
    ≋-sym (dyn ps)    = dyn (PE.sym ps)
    ≋-sym (blob ps p) = blob (PE.sym ps) (A.sym p)

    ≋-trans : ∀ {x y z} → x ≋ y → y ≋ z → x ≋ z
    ≋-trans (sta p)     (sta q)     = sta (A.trans p q)
    ≋-trans (dyn ps)    (dyn qs)    = dyn (PE.trans ps qs)
    ≋-trans (blob ps p) (blob qs q) = blob (PE.trans ps qs) (A.trans p q)

  ≋-isEquivalence : IsEquivalence _≋_
  ≋-isEquivalence = record { refl  = ≋-refl
                           ; sym   = ≋-sym
                           ; trans = ≋-trans
                           }

  Blob/≋ : Setoid _ _
  Blob/≋ = record { Carrier       = Blob
                  ; _≈_           = _≋_
                  ; isEquivalence = ≋-isEquivalence
                  }

  _++_ : Blob → Blob → Blob
  sta x     ++ sta y     = sta (x · y)
  dyn xs    ++ dyn ys    = dyn (xs ⊗ ys)
  sta x     ++ dyn ys    = blob ys        x
  sta x     ++ blob ys y = blob ys        (x · y)
  dyn xs    ++ sta y     = blob xs        y
  dyn xs    ++ blob ys y = blob (xs ⊗ ys) y
  blob xs x ++ sta y     = blob xs        (x · y)
  blob xs x ++ dyn ys    = blob (xs ⊗ ys) x
  blob xs x ++ blob ys y = blob (xs ⊗ ys) (x · y)

  ++-cong : ∀ {x y z w} → x ≋ y → z ≋ w → x ++ z ≋ y ++ w
  ++-cong (sta p)     (sta q)     = sta (·-cong p q)
  ++-cong (dyn ps)    (dyn qs)    = dyn (⊗-cong ps qs)
  ++-cong (sta p)     (dyn qs)    = blob qs p
  ++-cong (sta p)     (blob qs q) = blob qs (·-cong p q)
  ++-cong (dyn ps)    (sta q)     = blob ps q
  ++-cong (dyn ps)    (blob qs q) = blob (⊗-cong ps qs) q
  ++-cong (blob ps p) (sta q)     = blob ps (·-cong p q)
  ++-cong (blob ps p) (dyn qs)    = blob (⊗-cong ps qs) p
  ++-cong (blob ps p) (blob qs q) = blob (⊗-cong ps qs) (·-cong p q)

  ++-comm : ∀ x y → x ++ y ≋ y ++ x
  ++-comm (sta x)     (sta y)     = sta (·-comm x y)
  ++-comm (dyn xs)    (dyn ys)    = dyn (⊗-comm xs ys)
  ++-comm (sta x)     (dyn ys)    = ≋-refl
  ++-comm (sta x)     (blob ys y) = blob PE.refl (·-comm x y)
  ++-comm (dyn xs)    (sta y)     = ≋-refl
  ++-comm (dyn xs)    (blob ys y) = blob (⊗-comm xs ys) A.refl
  ++-comm (blob xs x) (sta y)     = blob PE.refl (·-comm x y)
  ++-comm (blob xs x) (dyn ys)    = blob (⊗-comm xs ys) A.refl
  ++-comm (blob xs x) (blob ys y) = blob (⊗-comm xs ys) (·-comm x y)

  ++-assoc : ∀ x y z → (x ++ y) ++ z ≋ x ++ (y ++ z)
  ++-assoc (sta x)     (sta y)     (sta z)     = sta (·-assoc x y z)
  ++-assoc (dyn xs)    (dyn ys)    (dyn zs)    = dyn (⊗-assoc xs ys zs)
  ++-assoc (sta x)     (sta y)     (dyn zs)    = ≋-refl
  ++-assoc (sta x)     (sta y)     (blob zs z) = blob PE.refl (·-assoc x y z)
  ++-assoc (sta x)     (dyn ys)    (sta z)     = ≋-refl
  ++-assoc (sta x)     (dyn ys)    (dyn zs)    = ≋-refl
  ++-assoc (sta x)     (dyn ys)    (blob zs z) = ≋-refl
  ++-assoc (sta x)     (blob ys y) (sta z)     = blob PE.refl (·-assoc x y z)
  ++-assoc (sta x)     (blob ys y) (dyn zs)    = ≋-refl
  ++-assoc (sta x)     (blob ys y) (blob zs z) = blob PE.refl (·-assoc x y z)
  ++-assoc (dyn xs)    (sta y)     (sta z)     = ≋-refl
  ++-assoc (dyn xs)    (sta y)     (dyn zs)    = ≋-refl
  ++-assoc (dyn xs)    (sta y)     (blob zs z) = ≋-refl
  ++-assoc (dyn xs)    (dyn ys)    (sta z)     = ≋-refl
  ++-assoc (dyn xs)    (dyn ys)    (blob zs z) = blob (⊗-assoc xs ys zs) A.refl
  ++-assoc (dyn xs)    (blob ys y) (sta z)     = ≋-refl
  ++-assoc (dyn xs)    (blob ys y) (dyn zs)    = blob (⊗-assoc xs ys zs) A.refl
  ++-assoc (dyn xs)    (blob ys y) (blob zs z) = blob (⊗-assoc xs ys zs) A.refl
  ++-assoc (blob xs x) (sta y)     (sta z)     = blob PE.refl (·-assoc x y z)
  ++-assoc (blob xs x) (sta y)     (dyn zs)    = ≋-refl
  ++-assoc (blob xs x) (sta y)     (blob zs z) = blob PE.refl (·-assoc x y z)
  ++-assoc (blob xs x) (dyn ys)    (sta z)     = ≋-refl
  ++-assoc (blob xs x) (dyn ys)    (dyn zs)    = blob (⊗-assoc xs ys zs) A.refl
  ++-assoc (blob xs x) (dyn ys)    (blob zs z) = blob (⊗-assoc xs ys zs) A.refl
  ++-assoc (blob xs x) (blob ys y) (sta z)     = blob PE.refl (·-assoc x y z)
  ++-assoc (blob xs x) (blob ys y) (dyn zs)    = blob (⊗-assoc xs ys zs) A.refl
  ++-assoc (blob xs x) (blob ys y) (blob zs z) = blob (⊗-assoc xs ys zs) (·-assoc x y z)

  Blob⟦_⟧ : Interpretation Blob/≋
  Blob⟦ • ⟧ (x ∷ y ∷ []) = x ++ y

  Blob⟦_⟧-cong : Congruence Blob/≋ Blob⟦_⟧
  Blob⟦ • ⟧-cong (p ∷ q ∷ []) = ++-cong p q

  Blob/≋-isAlgebra : IsAlgebra Blob/≋
  Blob/≋-isAlgebra = record { ⟦_⟧     = Blob⟦_⟧
                            ; ⟦⟧-cong = Blob⟦_⟧-cong
                            }

  Blob/≋-algebra : Algebra
  Blob/≋-algebra =
    record { ∥_∥/≈           = Blob/≋
           ; ∥_∥/≈-isAlgebra = Blob/≋-isAlgebra
           }

  Blob/≋-models : Models Blob/≋-algebra
  Blob/≋-models comm θ  = ++-comm (θ (# 0)) (θ (# 1))
  Blob/≋-models assoc θ = ++-assoc (θ (# 0)) (θ (# 1)) (θ (# 2))

  Blob/≋-isModel : IsModel Blob/≋
  Blob/≋-isModel =
    record { isAlgebra = Blob/≋-isAlgebra
           ; models    = Blob/≋-models
           }

  Frex : Model
  Frex = record { ∥_∥/≈   = Blob/≋
                ; isModel = Blob/≋-isModel
                }

  ∣inl∣ : ∥ A ∥ → ∥ Frex ∥
  ∣inl∣ = sta

  ∣inl∣-cong : Congruent _≈_ _≋_ ∣inl∣
  ∣inl∣-cong = sta

  ∣inl∣⃗ : ∥ A ∥/≈ ↝ ∥ Frex ∥/≈
  ∣inl∣⃗ = record { ∣_∣      = ∣inl∣
                  ; ∣_∣-cong = ∣inl∣-cong
                  }

  ∣inl∣-hom : Homomorphic ∥ A ∥ₐ ∥ Frex ∥ₐ ∣inl∣
  ∣inl∣-hom • (x ∷ y ∷ []) = ≋-refl

  inl : ∥ A ∥ₐ ⟿ ∥ Frex ∥ₐ
  inl = record { ∣_∣⃗    = ∣inl∣⃗
               ; ∣_∣-hom = ∣inl∣-hom
               }

  ∣inr∣ : ∥ J n ∥ → ∥ Frex ∥
  ∣inr∣ x = dyn (∣ norm ∣ x)

  ∣inr∣-cong : Congruent ≈[ J n ] _≋_ ∣inr∣
  ∣inr∣-cong p = dyn (∣ norm ∣-cong p)

  ∣inr∣⃗ : ∥ J n ∥/≈ ↝ ∥ Frex ∥/≈
  ∣inr∣⃗ = record { ∣_∣      = ∣inr∣
                  ; ∣_∣-cong = ∣inr∣-cong
                  }

  ∣inr∣-hom : Homomorphic ∥ J n ∥ₐ ∥ Frex ∥ₐ ∣inr∣
  ∣inr∣-hom • (x ∷ y ∷ []) = dyn (∣ norm ∣-hom • (x ∷ y ∷ []))

  inr : ∥ J n ∥ₐ ⟿ ∥ Frex ∥ₐ
  inr = record { ∣_∣⃗    = ∣inr∣⃗
               ; ∣_∣-hom = ∣inr∣-hom
               }

  module _ {b ℓ} (X : Model {b} {ℓ}) where

    private

      open module X = Setoid ∥ X ∥/≈ renaming (_≈_ to _~_)

      _⊕_ : ∥ X ∥ → ∥ X ∥ → ∥ X ∥
      x ⊕ y = X ⟦ • ⟧ (x ∷ y ∷ [])

      ⊕-cong : ∀ {x y z w} → x ~ y → z ~ w → x ⊕ z ~ y ⊕ w
      ⊕-cong p q = (X ⟦ • ⟧-cong) (p ∷ q ∷ [])

      ⊕-comm : ∀ (x y : ∥ X ∥) → x ⊕ y ~ y ⊕ x
      ⊕-comm x y = ∥ X ∥ₐ-models comm (env {A = ∥ X ∥ₐ} (x ∷ y ∷ []))

      ⊕-assoc : ∀ (x y z : ∥ X ∥) → (x ⊕ y) ⊕ z ~ x ⊕ (y ⊕ z)
      ⊕-assoc x y z = ∥ X ∥ₐ-models assoc (env {A = ∥ X ∥ₐ} (x ∷ y ∷ z ∷ []))

    module _
      (f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ)
      (g : ∥ J n ∥ₐ ⟿ ∥ X ∥ₐ)
      where

      ∣resid∣ : ∥ Frex ∥ → ∥ X ∥
      ∣resid∣ (sta x)     = ∣ f ∣ x
      ∣resid∣ (dyn xs)    = ∣ g ∣ (∣ syn ∣ xs)
      ∣resid∣ (blob xs x) = ∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ f ∣ x

      ∣resid∣-cong : Congruent _≋_ _~_ ∣resid∣
      ∣resid∣-cong (sta p)     = ∣ f ∣-cong p
      ∣resid∣-cong (dyn ps)    = ∣ g ∣-cong (∣ syn ∣-cong ps)
      ∣resid∣-cong (blob ps p) =
        ⊕-cong (∣ g ∣-cong (∣ syn ∣-cong ps)) (∣ f ∣-cong p)

      open Reasoning ∥ X ∥/≈

      ∣resid∣-hom : Homomorphic ∥ Frex ∥ₐ ∥ X ∥ₐ ∣resid∣
      ∣resid∣-hom • (sta x     ∷ sta y     ∷ []) = ∣ f ∣-hom • (x ∷ y ∷ [])
      ∣resid∣-hom • (sta x     ∷ dyn ys    ∷ []) = ⊕-comm (∣ f ∣ x) _
      ∣resid∣-hom • (sta x     ∷ blob ys y ∷ []) = begin
          ∣ f ∣ x ⊕ (∣ g ∣ (∣ syn ∣ ys) ⊕ ∣ f ∣ y)
        ≈⟨ ⊕-cong X.refl (⊕-comm _ (∣ f ∣ y)) ⟩
          ∣ f ∣ x ⊕ (∣ f ∣ y ⊕ ∣ g ∣ (∣ syn ∣ ys))
        ≈⟨ X.sym (⊕-assoc (∣ f ∣ x) (∣ f ∣ y) _) ⟩
          (∣ f ∣ x ⊕ ∣ f ∣ y) ⊕ ∣ g ∣ (∣ syn ∣ ys)
        ≈⟨ ⊕-cong (∣ f ∣-hom • (x ∷ y ∷ [])) X.refl ⟩
          ∣ f ∣ (x · y) ⊕ ∣ g ∣ (∣ syn ∣ ys)
        ≈⟨ ⊕-comm _ _ ⟩
          ∣ g ∣ (∣ syn ∣ ys) ⊕ ∣ f ∣ (x · y)
        ∎
      ∣resid∣-hom • (dyn xs    ∷ sta y     ∷ []) = X.refl
      ∣resid∣-hom • (dyn xs    ∷ dyn ys    ∷ []) = ∣ g ⊙ syn ∣-hom • (xs ∷ ys ∷ [])
      ∣resid∣-hom • (dyn xs    ∷ blob ys y ∷ []) = begin
          ∣ g ∣ (∣ syn ∣ xs) ⊕ (∣ g ∣ (∣ syn ∣ ys) ⊕ ∣ f ∣ y)
        ≈⟨ X.sym (⊕-assoc _ _ (∣ f ∣ y)) ⟩
          (∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ g ∣ (∣ syn ∣ ys)) ⊕ ∣ f ∣ y
        ≈⟨ ⊕-cong (∣ g ⊙ syn ∣-hom • (xs ∷ ys ∷ [])) X.refl ⟩
          ∣ g ∣ (∣ syn ∣ (xs ⊗ ys)) ⊕ ∣ f ∣ y
        ∎
      ∣resid∣-hom • (blob xs x ∷ sta y     ∷ []) = begin
          (∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ f ∣ x) ⊕ ∣ f ∣ y
        ≈⟨ ⊕-assoc _ (∣ f ∣ x) (∣ f ∣ y) ⟩
          ∣ g ∣ (∣ syn ∣ xs) ⊕ (∣ f ∣ x ⊕ ∣ f ∣ y)
        ≈⟨ ⊕-cong X.refl (∣ f ∣-hom • (x ∷ y ∷ [])) ⟩
          ∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ f ∣ (x · y)
        ∎
      ∣resid∣-hom • (blob xs x ∷ dyn ys    ∷ []) = begin
          (∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ f ∣ x) ⊕ ∣ g ∣ (∣ syn ∣ ys)
        ≈⟨ ⊕-assoc _ (∣ f ∣ x) _ ⟩
          ∣ g ∣ (∣ syn ∣ xs) ⊕ (∣ f ∣ x ⊕ ∣ g ∣ (∣ syn ∣ ys))
        ≈⟨ ⊕-cong X.refl (⊕-comm (∣ f ∣ x) _) ⟩
          ∣ g ∣ (∣ syn ∣ xs) ⊕ (∣ g ∣ (∣ syn ∣ ys) ⊕ ∣ f ∣ x)
        ≈⟨ X.sym (⊕-assoc _ _ (∣ f ∣ x)) ⟩
          (∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ g ∣ (∣ syn ∣ ys)) ⊕ ∣ f ∣ x
        ≈⟨ ⊕-cong (∣ g ⊙ syn ∣-hom • (xs ∷ ys ∷ [])) X.refl ⟩
          ∣ g ∣ (∣ syn ∣ (xs ⊗ ys)) ⊕ ∣ f ∣ x
        ∎
      ∣resid∣-hom • (blob xs x ∷ blob ys y ∷ []) = begin
          (∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ f ∣ x) ⊕ (∣ g ∣ (∣ syn ∣ ys) ⊕ ∣ f ∣ y)
        ≈⟨ ⊕-assoc _ (∣ f ∣ x) _ ⟩
          ∣ g ∣ (∣ syn ∣ xs) ⊕ (∣ f ∣ x ⊕ (∣ g ∣ (∣ syn ∣ ys) ⊕ ∣ f ∣ y))
        ≈⟨ ⊕-cong X.refl (X.sym (⊕-assoc (∣ f ∣ x) _ _)) ⟩
          ∣ g ∣ (∣ syn ∣ xs) ⊕ ((∣ f ∣ x ⊕ ∣ g ∣ (∣ syn ∣ ys)) ⊕ ∣ f ∣ y)
        ≈⟨ ⊕-cong X.refl (⊕-cong (⊕-comm (∣ f ∣ x) _) X.refl) ⟩
          ∣ g ∣ (∣ syn ∣ xs) ⊕ ((∣ g ∣ (∣ syn ∣ ys) ⊕ ∣ f ∣ x) ⊕ ∣ f ∣ y)
        ≈⟨ ⊕-cong X.refl (⊕-assoc _ (∣ f ∣ x) _) ⟩
          ∣ g ∣ (∣ syn ∣ xs) ⊕ (∣ g ∣ (∣ syn ∣ ys) ⊕ (∣ f ∣ x ⊕ ∣ f ∣ y))
        ≈⟨ X.sym (⊕-assoc _ _ _) ⟩
          (∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ g ∣ (∣ syn ∣ ys)) ⊕ (∣ f ∣ x ⊕ ∣ f ∣ y)
        ≈⟨ ⊕-cong (∣ g ⊙ syn ∣-hom • (xs ∷ ys ∷ [])) (∣ f ∣-hom • (x ∷ y ∷ [])) ⟩
          ∣ g ∣ (∣ syn ∣ (xs ⊗ ys)) ⊕ ∣ f ∣ (x · y)
        ∎

      ∣resid∣⃗ : ∥ Frex ∥/≈ ↝ ∥ X ∥/≈
      ∣resid∣⃗ = record { ∣_∣      = ∣resid∣
                        ; ∣_∣-cong = ∣resid∣-cong
                        }

      _[_,_] : ∥ Frex ∥ₐ ⟿ ∥ X ∥ₐ
      _[_,_] = record { ∣_∣⃗    = ∣resid∣⃗
                      ; ∣_∣-hom = ∣resid∣-hom
                      }

  module _ {b ℓ} {X : Model {b} {ℓ}} where

    private

      open module X = Setoid ∥ X ∥/≈ renaming (_≈_ to _~_)

      _⊕_ : ∥ X ∥ → ∥ X ∥ → ∥ X ∥
      x ⊕ y = X ⟦ • ⟧ (x ∷ y ∷ [])

      ⊕-cong : ∀ {x y z w} → x ~ y → z ~ w → x ⊕ z ~ y ⊕ w
      ⊕-cong p q = (X ⟦ • ⟧-cong) (p ∷ q ∷ [])

      ⊕-comm : ∀ (x y : ∥ X ∥) → x ⊕ y ~ y ⊕ x
      ⊕-comm x y = ∥ X ∥ₐ-models comm (env {A = ∥ X ∥ₐ} (x ∷ y ∷ []))

      ⊕-assoc : ∀ (x y z : ∥ X ∥) → (x ⊕ y) ⊕ z ~ x ⊕ (y ⊕ z)
      ⊕-assoc x y z = ∥ X ∥ₐ-models assoc (env {A = ∥ X ∥ₐ} (x ∷ y ∷ z ∷ []))

    module _
      {f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ}
      {g : ∥ J n ∥ₐ ⟿ ∥ X ∥ₐ}
      where

      commute₁ : X [ f , g ] ⊙ inl ≗ f
      commute₁ = X.refl

      commute₂ : X [ f , g ] ⊙ inr ≗ g
      commute₂ {x} = ∣ g ∣-cong (syn⊙norm≗id {x = x})

      module _ {h : ∥ Frex ∥ₐ ⟿ ∥ X ∥ₐ}
        (c₁ : h ⊙ inl ≗ f)
        (c₂ : h ⊙ inr ≗ g)
        where

        open Reasoning ∥ X ∥/≈

        universal : X [ f , g ] ≗ h
        universal {sta x}     = X.sym c₁
        universal {dyn xs}    = begin
            ∣ g ∣ (∣ syn ∣ xs)
          ≈⟨ X.sym c₂ ⟩
            ∣ h ∣ (dyn (∣ norm ∣ (∣ syn ∣ xs)))
          ≈⟨ ∣ h ∣-cong (dyn norm⊙syn≗id) ⟩
            ∣ h ∣ (dyn xs)
          ∎
        universal {blob xs x} = begin
            ∣ g ∣ (∣ syn ∣ xs) ⊕ ∣ f ∣ x
          ≈⟨ ⊕-cong universal universal ⟩
            ∣ h ∣ (dyn xs) ⊕ ∣ h ∣ (sta x)
          ≈⟨ ∣ h ∣-hom • (dyn xs ∷ sta x ∷ []) ⟩
            ∣ h ∣ (blob xs x)
          ∎

CSemigroupFrex : FreeExtension
CSemigroupFrex = record { _[_]        = Frex
                        ; _[_]-isFrex = isFrex
                        }
  where isFrex : IsFreeExtension Frex
        isFrex A n =
          record { inl       = inl A n
                 ; inr       = inr A n
                 ; _[_,_]    = _[_,_] A n
                 ; commute₁  = λ {_ _ X f g} → commute₁ A n {X = X} {f} {g}
                 ; commute₂  = λ {_ _ X f g} → commute₂ A n {X = X} {f} {g}
                 ; universal = λ {_ _ X f g h} → universal A n {X = X} {f} {g} {h}
                 }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

open import Light.Library.Data.Natural as ℕ using (ℕ ; predecessor ; zero)
open import Light.Package using (Package)

module Light.Literals.Level ⦃ natural‐package : Package record { ℕ } ⦄ where

open import Light.Literals.Definition.Natural using (FromNatural)
open FromNatural using (convert)
open import Light.Level using (Level ; 0ℓ ; ++_)
open import Light.Library.Relation.Decidable using (if_then_else_)
open import Light.Library.Relation.Binary.Equality using (_≈_)
open import Light.Library.Relation.Binary.Equality.Decidable using (DecidableEquality)

instance from‐natural : FromNatural Level
convert from‐natural n =
      if n ≈ zero
      then 0ℓ
      else ++ convert from‐natural (predecessor n)

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Unit

module lib.types.Circle where

{-
Idea :

data S¹ : Type₀ where
  base : S¹
  loop : base == base

I’m using Dan Licata’s trick to have a higher inductive type with definitional
reduction rule for [base]
-}

module _ where
  private
    data #S¹-aux : Type₀ where
      #base : #S¹-aux

    data #S¹ : Type₀ where
      #s¹ : #S¹-aux → (Unit → Unit) → #S¹

  S¹ : Type₀
  S¹ = #S¹

  base : S¹
  base = #s¹ #base _

  postulate  -- HIT
    loop : base == base

  module S¹Elim {i} {P : S¹ → Type i} (base* : P base)
    (loop* : base* == base* [ P ↓ loop ]) where

    f : Π S¹ P
    f = f-aux phantom where

     f-aux : Phantom loop* → Π S¹ P
     f-aux phantom (#s¹ #base _) = base*

    postulate  -- HIT
      loop-β : apd f loop == loop*

open S¹Elim public using () renaming (f to S¹-elim)

module S¹Rec {i} {A : Type i} (base* : A) (loop* : base* == base*) where

  private
    module M = S¹Elim base* (↓-cst-in loop*)

  f : S¹ → A
  f = M.f

  loop-β : ap f loop == loop*
  loop-β = apd=cst-in {f = f} M.loop-β

module S¹RecType {i} (A : Type i) (e : A ≃ A) where

  open S¹Rec A (ua e) public

  coe-loop-β : (a : A) → coe (ap f loop) a == –> e a
  coe-loop-β a =
    coe (ap f loop) a   =⟨ loop-β |in-ctx (λ u → coe u a) ⟩
    coe (ua e) a        =⟨ coe-β e a ⟩
    –> e a ∎

  coe!-loop-β : (a : A) → coe! (ap f loop) a == <– e a
  coe!-loop-β a =
    coe! (ap f loop) a   =⟨ loop-β |in-ctx (λ u → coe! u a) ⟩
    coe! (ua e) a        =⟨ coe!-β e a ⟩
    <– e a ∎

  ↓-loop-out : {a a' : A} → a == a' [ f ↓ loop ] → –> e a == a'
  ↓-loop-out {a} {a'} p =
    –> e a              =⟨ ! (coe-loop-β a) ⟩
    coe (ap f loop) a   =⟨ to-transp p ⟩
    a' ∎

  import lib.types.Generic1HIT as Generic1HIT
  module S¹G = Generic1HIT Unit Unit (idf _) (idf _)
  module P = S¹G.RecType (cst A) (cst e)

  private
    generic-S¹ : Σ S¹ f == Σ S¹G.T P.f
    generic-S¹ = eqv-tot where

      module To = S¹Rec (S¹G.cc tt) (S¹G.pp tt)
      to = To.f

      module From = S¹G.Rec (cst base) (cst loop)
      from : S¹G.T → S¹
      from = From.f

      abstract
        to-from : (x : S¹G.T) → to (from x) == x
        to-from = S¹G.elim (λ _ → idp) (λ _ → ↓-∘=idf-in to from
          (ap to (ap from (S¹G.pp tt)) =⟨ From.pp-β tt |in-ctx ap to ⟩
           ap to loop                  =⟨ To.loop-β ⟩
           S¹G.pp tt ∎))

        from-to : (x : S¹) → from (to x) == x
        from-to = S¹-elim idp (↓-∘=idf-in from to
          (ap from (ap to loop)   =⟨ To.loop-β |in-ctx ap from ⟩
           ap from (S¹G.pp tt)    =⟨ From.pp-β tt ⟩
           loop ∎))

      eqv : S¹ ≃ S¹G.T
      eqv = equiv to from to-from from-to

      eqv-fib : f == P.f [ (λ X → (X → Type _)) ↓ ua eqv ]
      eqv-fib =
        ↓-app→cst-in (λ {t} p → S¹-elim {P = λ t → f t == P.f (–> eqv t)} idp
          (↓-='-in
            (ap (P.f ∘ (–> eqv)) loop   =⟨ ap-∘ P.f to loop ⟩
             ap P.f (ap to loop)        =⟨ To.loop-β |in-ctx ap P.f ⟩
             ap P.f (S¹G.pp tt)         =⟨ P.pp-β tt ⟩
             ua e                       =⟨ ! loop-β ⟩
             ap f loop ∎))
        t ∙ ap P.f (↓-idf-ua-out eqv p))

      eqv-tot : Σ S¹ f == Σ S¹G.T P.f
      eqv-tot = ap (uncurry Σ) (pair= (ua eqv) eqv-fib)

  import lib.types.Flattening as Flattening
  module FlatteningS¹ = Flattening
    Unit Unit (idf _) (idf _) (cst A) (cst e)
  open FlatteningS¹ public hiding (flattening-equiv; module P)

  flattening-S¹ : Σ S¹ f == Wt
  flattening-S¹ = generic-S¹ ∙ ua FlatteningS¹.flattening-equiv

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Andreas, 2015-06-24

{-# OPTIONS --copatterns #-}

-- {-# OPTIONS -v tc.with.strip:20 #-}

module _ where

open import Common.Equality
open import Common.Product

module SynchronousIO (I O : Set) where

  F : Set → Set
  F S = I → O × S

  record SyncIO : Set₁ where
    field
      St : Set
      tr : St → F St

  module Eq (A₁ A₂ : SyncIO) where

    open SyncIO A₁ renaming (St to S₁; tr to tr₁)
    open SyncIO A₂ renaming (St to S₂; tr to tr₂)

    record BiSim (s₁ : S₁) (s₂ : S₂) : Set where
      coinductive
      field
        force : ∀ (i : I) →
          let (o₁ , t₁) = tr₁ s₁ i
              (o₂ , t₂) = tr₂ s₂ i
          in  o₁ ≡ o₂ × BiSim t₁ t₂

  module Trans (A₁ A₂ A₃ : SyncIO) where

    open SyncIO A₁ renaming (St to S₁; tr to tr₁)
    open SyncIO A₂ renaming (St to S₂; tr to tr₂)
    open SyncIO A₃ renaming (St to S₃; tr to tr₃)

    open Eq A₁ A₂ renaming (BiSim to _₁≅₂_; module BiSim to B₁₂)
    open Eq A₂ A₃ renaming (BiSim to _₂≅₃_; module BiSim to B₂₃)
    open Eq A₁ A₃ renaming (BiSim to _₁≅₃_; module BiSim to B₁₃)

    open B₁₂ renaming (force to force₁₂)
    open B₂₃ renaming (force to force₂₃)
    open B₁₃ renaming (force to force₁₃)

    transitivity : ∀{s₁ s₂ s₃} (p : s₁ ₁≅₂ s₂) (p' : s₂ ₂≅₃ s₃) → s₁ ₁≅₃ s₃
    force₁₃ (transitivity p p') i with force₁₂ p i | force₂₃ p' i
    force₁₃ (transitivity p p') i | (q , r) | (q' , r') = trans q q' , transitivity r r'

-- with-clause stripping failed for projections from module applications
-- should work now

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- MIT License

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

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

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

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

{-# OPTIONS --guardedness --sized-types #-}

open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.List using ([]; _∷_; _∷ʳ_; _++_)
open import Data.List.Properties using (∷-injective)

open import Relation.Nullary
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Unary using (_∈_; _∉_; _⊆_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; subst₂; cong)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_)

open import Function.Base using (case_of_)

open import Common

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

open import Trace message
open import SessionType message
open import HasTrace message
open import TraceSet message
open import Transitions message
open import Subtyping message
open import Divergence message
open import Session message
open import Semantics message

make-diverge-backward :
  ∀{T S α}
  (tα : T HasTrace (α ∷ []))
  (sα : S HasTrace (α ∷ [])) ->
  T ↑ S ->
  after tα ↑ after sα ->
  DivergeBackward tα sα
make-diverge-backward tα sα divε divα none = divε
make-diverge-backward tα sα divε divα (some none) =
  subst₂ (λ u v -> after u ↑ after v) (sym (⊑-has-trace-after tα)) (sym (⊑-has-trace-after sα)) divα

has-trace-after-split :
  ∀{T φ ψ} ->
  (tφ : T HasTrace φ)
  (tφψ : T HasTrace (φ ++ ψ)) ->
  has-trace-after tφ (split-trace tφ tφψ) ≡ tφψ
has-trace-after-split (_ , tdef , refl) tφψ = refl
has-trace-after-split (_ , tdef , step inp tr) (_ , sdef , step inp sr)
  rewrite has-trace-after-split (_ , tdef , tr) (_ , sdef , sr) = refl
has-trace-after-split (T , tdef , step (out fx) tr) (S , sdef , step (out gx) sr)
  rewrite has-trace-after-split (_ , tdef , tr) (_ , sdef , sr) =
  cong (S ,_) (cong (sdef ,_) (cong (λ z -> step z sr) (cong out (Defined-eq (transitions+defined->defined sr sdef) gx))))

disc-set-has-outputs :
  ∀{T S φ x} ->
  T <: S ->
  φ ∈ DiscSet T S ->
  T HasTrace (φ ∷ʳ O x) ->
  S HasTrace φ ->
  φ ∷ʳ O x ∈ DiscSet T S
disc-set-has-outputs {_} {S} {φ} {x} sub (inc tφ sφ div←φ) tφx _ with S HasTrace? (φ ∷ʳ O x)
... | yes sφx =
  let tφ/x = split-trace tφ tφx in
  let sφ/x = split-trace sφ sφx in
  let divφ = subst₂ (λ u v -> after u ↑ after v) (⊑-has-trace-after tφ) (⊑-has-trace-after sφ) (div←φ (⊑-refl φ)) in
  let divx = _↑_.divergence divφ {[]} {x} none tφ/x sφ/x in
  let divφ←x = make-diverge-backward tφ/x sφ/x divφ divx in
  let div←φx = subst₂ DivergeBackward (has-trace-after-split tφ tφx) (has-trace-after-split sφ sφx) (append-diverge-backward tφ sφ tφ/x sφ/x div←φ divφ←x) in
  inc tφx sφx div←φx
... | no nsφx = exc refl tφ sφ tφx nsφx div←φ
disc-set-has-outputs sub (exc eq tψ sψ tφ nsφ div←ψ) tφx sφ = ⊥-elim (nsφ sφ)

defined-becomes-nil :
  ∀{T φ S} ->
  Defined T ->
  ¬ Defined S ->
  Transitions T φ S ->
  ∃[ ψ ] ∃[ x ] (φ ≡ ψ ∷ʳ I x × T HasTrace ψ × ¬ T HasTrace φ)
defined-becomes-nil def ndef refl = ⊥-elim (ndef def)
defined-becomes-nil def ndef (step (inp {_} {x}) refl) =
  [] , x , refl , (_ , inp , refl) , inp-has-no-trace λ { (_ , def , refl) → ⊥-elim (ndef def) }
defined-becomes-nil def ndef (step inp tr@(step t _)) with defined-becomes-nil (transition->defined t) ndef tr
... | ψ , x , eq , tψ , ntφ =
  I _ ∷ ψ , x , cong (I _ ∷_) eq , inp-has-trace tψ , inp-has-no-trace ntφ
defined-becomes-nil def ndef (step (out fx) tr) with defined-becomes-nil fx ndef tr
... | ψ , x , refl , tψ , ntφ =
  O _ ∷ ψ , x , refl , out-has-trace tψ , out-has-no-trace ntφ

sub+diverge->defined : ∀{T S} -> T <: S -> T ↑ S -> Defined T × Defined S
sub+diverge->defined nil<:any div with _↑_.with-trace div
... | _ , def , tr = ⊥-elim (contraposition (transitions+defined->defined tr) (λ ()) def)
sub+diverge->defined (end<:def (inp _) def) _ = inp , def
sub+diverge->defined (end<:def (out _) def) _ = out , def
sub+diverge->defined (inp<:inp _ _) _ = inp , inp
sub+diverge->defined (out<:out _ _ _) _ = out , out

sub+diverge->has-empty-trace : ∀{T S} -> T <: S -> T ↑ S -> DiscSet T S []
sub+diverge->has-empty-trace nil<:any div with _↑_.with-trace div
... | tφ = ⊥-elim (nil-has-no-trace tφ)
sub+diverge->has-empty-trace (end<:def e def) div with _↑_.with-trace div | _↑_.without-trace div
... | tφ | nsφ rewrite end-has-empty-trace e tφ = ⊥-elim (nsφ (defined->has-empty-trace def))
sub+diverge->has-empty-trace (inp<:inp _ _) div = inc (_ , inp , refl) (_ , inp , refl) λ { none → div }
sub+diverge->has-empty-trace (out<:out _ _ _) div = inc (_ , out , refl) (_ , out , refl) λ { none → div }

discriminator : SessionType -> SessionType -> SessionType
discriminator T S = decode (co-semantics (disc-set->semantics T S)) .force

discriminator-disc-set-sub : (T S : SessionType) -> CoSet ⟦ discriminator T S ⟧ ⊆ DiscSet T S
discriminator-disc-set-sub T S rφ =
  co-inversion {DiscSet T S} (decode-sub (co-semantics (disc-set->semantics T S)) rφ)

discriminator-disc-set-sup : (T S : SessionType) -> DiscSet T S ⊆ CoSet ⟦ discriminator T S ⟧
discriminator-disc-set-sup T S dφ =
  decode-sup (co-semantics (disc-set->semantics T S)) (co-definition {DiscSet T S} dφ)

sub+diverge->discriminator-defined : ∀{T S} -> T <: S -> T ↑ S -> Defined (discriminator T S)
sub+diverge->discriminator-defined {T} {S} sub div =
  has-trace->defined (co-set-right->left {DiscSet T S} {⟦ discriminator T S ⟧} (discriminator-disc-set-sup T S) (co-definition {DiscSet T S} {[]} (sub+diverge->has-empty-trace sub div)))

input-does-not-win :
  ∀{T S φ x} (tφ : T HasTrace φ) -> Transitions T (φ ∷ʳ I x) S -> ¬ Win (after tφ)
input-does-not-win (_ , _ , refl) (step inp _) ()
input-does-not-win (_ , def , step inp tr) (step inp sr) w = input-does-not-win (_ , def , tr) sr w
input-does-not-win (_ , def , step (out _) tr) (step (out _) sr) w = input-does-not-win (_ , def , tr) sr w

ends-with-output->has-trace : ∀{T S φ x} -> Transitions T (φ ∷ʳ O x) S -> T HasTrace (φ ∷ʳ O x)
ends-with-output->has-trace tr = _ , output-transitions->defined tr , tr

co-trace-swap : ∀{φ ψ} -> co-trace φ ≡ ψ -> φ ≡ co-trace ψ
co-trace-swap {φ} eq rewrite sym eq rewrite co-trace-involution φ = refl

co-trace-swap-⊑ : ∀{φ ψ} -> co-trace φ ⊑ ψ -> φ ⊑ co-trace ψ
co-trace-swap-⊑ {[]} none = none
co-trace-swap-⊑ {α ∷ _} (some le) rewrite co-action-involution α = some (co-trace-swap-⊑ le)

co-maximal : ∀{X φ} -> φ ∈ Maximal X -> co-trace φ ∈ Maximal (CoSet X)
co-maximal {X} (maximal xφ F) =
  maximal (co-definition {X} xφ) λ le xψ -> let le' = co-trace-swap-⊑ le in
                                             let eq = F le' xψ in
                                             co-trace-swap eq

co-maximal-2 : ∀{X φ} -> co-trace φ ∈ Maximal (CoSet X) -> φ ∈ Maximal X
co-maximal-2 {X} (maximal wit F) =
  maximal (co-inversion {X} wit) λ le xψ -> let le' = ⊑-co-trace le in
                                             let eq = F le' (co-definition {X} xψ) in
                                             co-trace-injective eq

co-trace->co-set : ∀{X φ} -> co-trace φ ∈ Maximal X -> φ ∈ Maximal (CoSet X)
co-trace->co-set {_} {φ} cxφ with co-maximal cxφ
... | res rewrite co-trace-involution φ = res

discriminator-after-sync->defined :
  ∀{R T S T' φ} ->
  T <: S ->
  (rdef : Defined (discriminator T S))
  (rr : Transitions (discriminator T S) (co-trace φ) R)
  (tr : Transitions T φ T') ->
  Defined R
discriminator-after-sync->defined {R} {T} {S} sub rdef rr tr with Defined? R
... | yes rdef' = rdef'
... | no nrdef' with defined-becomes-nil rdef nrdef' rr
... | ψ , x , eq , rψ , nrφ rewrite eq with input-does-not-win rψ rr
... | nwin with contraposition (decode+maximal->win (co-semantics (disc-set->semantics T S)) rψ) nwin
... | ncψ with decode-sub (co-semantics (disc-set->semantics T S)) rψ
... | dsψ with contraposition (disc-set-maximal-1 dsψ) (contraposition co-trace->co-set ncψ)
... | nnsψ with has-trace-double-negation nnsψ
... | sψ with (let tr' = subst (λ z -> Transitions _ z _) (co-trace-swap eq) tr in
              let tr'' = subst (λ z -> Transitions _ z _) (co-trace-++ ψ (I x ∷ [])) tr' in
              ends-with-output->has-trace tr'')
... | tψ with disc-set-has-outputs sub dsψ tψ sψ
... | dsφ with decode-sup (co-semantics (disc-set->semantics T S)) (co-definition {DiscSet T S} dsφ)
... | rφ = let rφ' = subst (_ HasTrace_) (co-trace-++ (co-trace ψ) (O x ∷ [])) rφ in
           let rφ'' = subst (λ z -> _ HasTrace (z ++ _)) (co-trace-involution ψ) rφ' in
           ⊥-elim (nrφ rφ'')

after-trace-defined : ∀{T T' φ} -> T HasTrace φ -> Transitions T φ T' -> Defined T'
after-trace-defined (_ , def , refl) refl = def
after-trace-defined (_ , def , step inp tr) (step inp sr) = after-trace-defined (_ , def , tr) sr
after-trace-defined (_ , def , step (out _) tr) (step (out _) sr) = after-trace-defined (_ , def , tr) sr

after-trace-defined-2 : ∀{T φ} (tφ : T HasTrace φ) -> Defined (after tφ)
after-trace-defined-2 (_ , def , _) = def

⊑-after : ∀{φ ψ} -> φ ⊑ ψ -> Trace
⊑-after {_} {ψ} none = ψ
⊑-after (some le) = ⊑-after le

⊑-after-co-trace : ∀{φ ψ} (le : φ ⊑ ψ) -> ⊑-after (⊑-co-trace le) ≡ co-trace (⊑-after le)
⊑-after-co-trace none = refl
⊑-after-co-trace (some le) = ⊑-after-co-trace le

extend-transitions :
  ∀{T S φ ψ}
  (le : φ ⊑ ψ)
  (tr : Transitions T φ S)
  (tψ : T HasTrace ψ) ->
  Transitions S (⊑-after le) (after tψ)
extend-transitions none refl (_ , _ , sr) = sr
extend-transitions (some le) (step inp tr) (_ , sdef , step inp sr) = extend-transitions le tr (_ , sdef , sr)
extend-transitions (some le) (step (out _) tr) (_ , sdef , step (out _) sr) = extend-transitions le tr (_ , sdef , sr)

discriminator-compliant : ∀{T S} -> T <: S -> T ↑ S -> FairComplianceS (discriminator T S # T)
discriminator-compliant {T} {S} sub div {R' # T'} reds with unzip-red* reds
... | φ , rr , tr with sub+diverge->discriminator-defined sub div | sub+diverge->defined sub div
... | rdef | tdef , sdef with discriminator-after-sync->defined sub rdef rr tr
... | rdef' with decode-sub (co-semantics (disc-set->semantics T S)) (_ , rdef' , rr)
... | dsφ rewrite co-trace-involution φ =
  case completion sub dsφ of
  λ { (inj₁ (ψ , lt , cψ@(maximal dsψ _))) ->
      let rψ = decode-sup (co-semantics (disc-set->semantics T S)) (co-definition {DiscSet T S} dsψ) in
      let tψ = disc-set-subset dsψ in
      let rr' = subst (λ z -> Transitions _ z _) (⊑-after-co-trace (⊏->⊑ lt)) (extend-transitions (⊑-co-trace (⊏->⊑ lt)) rr rψ) in
      let tr' = extend-transitions (⊏->⊑ lt) tr tψ in
      let winr = decode+maximal->win (co-semantics (disc-set->semantics T S)) rψ (co-maximal cψ) in
      let reds' = zip-red* rr' tr' in
      _ , reds' , win#def winr (after-trace-defined-2 tψ)
    ; (inj₂ (cφ , nsφ)) ->
      let winr = decode+maximal->win (co-semantics (disc-set->semantics T S)) (_ , rdef' , rr) (co-maximal cφ) in
      _ , ε , win#def winr (after-trace-defined (disc-set-subset dsφ) tr) }

discriminator-not-compliant : ∀{T S} -> T <: S -> T ↑ S -> ¬ FairComplianceS (discriminator T S # S)
discriminator-not-compliant {T} {S} sub div comp with comp ε
... | _ , reds , win#def w def with unzip-red* reds
... | φ , rr , sr with decode+win->maximal (co-semantics (disc-set->semantics T S)) (_ , win->defined w , rr) w
... | cφ with co-maximal-2 {DiscSet T S} cφ
... | csφ with disc-set-maximal-2 sub csφ
... | nsφ = nsφ (_ , def , sr)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda