text:
module chap0 where

open import Data.List
open import Data.Nat hiding (_⊔_)
-- open import Data.Integer hiding (_⊔_ ;  _≟_ ; _+_ )
open import Data.Product

A : List ℕ
A = 1 ∷ 2 ∷ []

data Literal : Set where
    x : Literal
    y : Literal
    z : Literal

B : List Literal
B = x ∷ y ∷ z ∷ []

ListProduct : {A B : Set } → List A → List B → List ( A × B )
ListProduct  = {!!}

ex05 : List ( ℕ × Literal )
ex05 = ListProduct A B   -- (1 , x) ∷ (1 , y) ∷ (1 , z) ∷ (2 , x) ∷ (2 , y) ∷ (2 , z) ∷ []

ex06 : List ( ℕ × Literal × ℕ )
ex06 = ListProduct A (ListProduct B A)

ex07 : Set
ex07 =  ℕ × ℕ

data ex08-f : ℕ → ℕ → Set where
    ex08f0 : ex08-f 0 1
    ex08f1 : ex08-f 1 2
    ex08f2 : ex08-f 2 3
    ex08f3 : ex08-f 3 4
    ex08f4 : ex08-f 4 0

data ex09-g : ℕ → ℕ → ℕ → ℕ → Set where
    ex09g0 : ex09-g 0 1 2 3
    ex09g1 : ex09-g 1 2 3 0
    ex09g2 : ex09-g 2 3 0 1
    ex09g3 : ex09-g 3 0 1 2

open import Data.Nat.DivMod
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Data.Nat.Properties

-- _%_ : ℕ → ℕ → ℕ
-- _%_ a b with <-cmp a b
-- _%_ a b | tri< a₁ ¬b ¬c = a
-- _%_ a b | tri≈ ¬a b₁ ¬c = 0
-- _%_ a b | tri> ¬a ¬b c = _%_ (a - b) b

_≡7_ : ℕ → ℕ → Set
n ≡7 m = (n % 7) ≡ (m % 7 )

refl7 :  { n : ℕ} → n ≡7 n
refl7 = {!!}

sym7  : { n m : ℕ} → n ≡7 m → m ≡7 n
sym7  = {!!}

trans7 : { n m o : ℕ} → n ≡7 m → m ≡7 o → n ≡7 o
trans7 = {!!}

open import Level renaming ( zero to Zero ; suc to Suc )

record Graph  { v v' : Level } : Set (Suc v ⊔ Suc v' ) where
  field
    vertex : Set v
    edge : vertex  → vertex → Set v'

open Graph

-- open import Data.Fin hiding ( _≟_ )
open import Data.Empty
open import Relation.Nullary
open import Data.Unit  hiding ( _≟_ )

-- data Dec (P : Set) : Set where
--    yes :   P → Dec P
--    no  : ¬ P → Dec P
--
--  _≟_ :  (s t : ℕ ) → Dec ( s ≡ t )

-- ¬ A = A → ⊥

_n≟_ :  (s t : ℕ ) → Dec ( s ≡ t )
zero n≟ zero = yes refl
zero n≟ suc t = no (λ ())
suc s n≟ zero = no (λ ())
suc s n≟ suc t with s n≟ t
... | yes refl = yes refl
... | no n = no (λ k → n (tt1 k) )  where
   tt1 : suc s ≡ suc t → s ≡ t
   tt1 refl = refl

open import Data.Bool  hiding ( _≟_ )

conn : List ( ℕ × ℕ ) → ℕ → ℕ → Bool
conn [] _ _ = false
conn ((n1 , m1 ) ∷ t ) n m  with n ≟ n1 | m ≟ m1
conn ((n1 , m1) ∷ t) n m | yes refl | yes refl  = true
conn ((n1 , m1) ∷ t) n m | _ | _ = conn t n m

list012a : List ( ℕ × ℕ )
list012a = (1 , 2) ∷ (2 , 3) ∷ (3 , 4) ∷ (4 , 5) ∷ (5 , 1) ∷ []

graph012a : Graph {Zero} {Zero}
graph012a = record { vertex = ℕ ; edge = λ s t → (conn list012a s t) ≡ true }

data edge012b :  ℕ → ℕ →  Set where
    e012b-1 : edge012b 1 2
    e012b-2 : edge012b 1 3
    e012b-3 : edge012b 1 4
    e012b-4 : edge012b 2 3
    e012b-5 : edge012b 2 4
    e012b-6 : edge012b 3 4

edge? : (E : ℕ → ℕ →  Set) → ( a b : ℕ ) → Set
edge? E a b = Dec ( E a b )

lemma3 : ( a b : ℕ ) → edge? edge012b a b
lemma3 1 2  = yes e012b-1
lemma3 1 3  = yes e012b-2
lemma3 1 4  = yes e012b-3
lemma3 2 3  = yes e012b-4
lemma3 2 4  = yes e012b-5
lemma3 3 4  = yes e012b-6
lemma3 1 1  = no ( λ () )
lemma3 2 1  = no ( λ () )
lemma3 2 2  = no ( λ () )
lemma3 3 1  = no ( λ () )
lemma3 3 2  = no ( λ () )
lemma3 3 3  = no ( λ () )
lemma3 0 _  = no ( λ () )
lemma3 _ 0  = no ( λ () )
lemma3 _ (suc (suc (suc (suc (suc _)))))  = no ( λ () )
lemma3 (suc (suc (suc (suc _)))) _  = no ( λ () )

graph012b : Graph {Zero} {Zero}
graph012b = record { vertex = ℕ  ; edge = edge012b }

data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
    direct :   E x y → connected E x y
    indirect :  ( z : V  ) -> E x z  →  connected {V} E z y → connected E x y

lemma1 : connected ( edge graph012a ) 1 2
lemma1 = direct refl  where

lemma1-2 : connected ( edge graph012a ) 1 3
lemma1-2 = indirect 2 refl (direct refl )

lemma2 : connected ( edge graph012b ) 1 2
lemma2 = direct e012b-1

reachable :  { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
reachable {V} E X Y = Dec ( connected {V} E X Y )

dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )

open import Function

lemma4 : ¬ ( dag ( edge graph012a)  )
lemma4 neg = neg 1 $ indirect 2 refl $ indirect 3 refl $ indirect 4 refl $ indirect 5 refl $ direct refl

dgree : List ( ℕ × ℕ ) → ℕ → ℕ
dgree [] _ = 0
dgree ((e , e1) ∷ t) e0 with e0 ≟ e | e0 ≟ e1
dgree ((e , e1) ∷ t) e0 | yes _ | _ = 1 + (dgree t e0)
dgree ((e , e1) ∷ t) e0 | _ | yes p = 1 + (dgree t e0)
dgree ((e , e1) ∷ t) e0 | no _ | no _ = dgree t e0

dgree-c : {t : Set} → List ( ℕ × ℕ ) → ℕ → (ℕ → t)  → t
dgree-c {t} [] e0 next = next 0
dgree-c {t} ((e , e1) ∷ tail ) e0 next with e0 ≟ e | e0 ≟ e1
... | yes _ | _ = dgree-c tail e0 ( λ n → next (n + 1 ))
... | _ | yes _ = dgree-c tail e0 ( λ n → next (n + 1 ))
... | no _ | no _ = dgree-c tail e0 next

lemma6 = dgree list012a 2
lemma7 = dgree-c list012a 2 ( λ n → n )

even2 : (n : ℕ ) → n % 2 ≡ 0 → (n + 2) % 2 ≡ 0
even2 0 refl = refl
even2 1 ()
even2 (suc (suc n)) eq = trans ([a+n]%n≡a%n n _) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n

sum-of-dgree : ( g : List ( ℕ × ℕ )) → ℕ
sum-of-dgree [] = 0
sum-of-dgree ((e , e1) ∷ t) = 2 + sum-of-dgree t

dgree-even : ( g : List ( ℕ × ℕ )) → sum-of-dgree g % 2 ≡ 0
dgree-even [] = refl
dgree-even ((e , e1) ∷ t) = begin
       sum-of-dgree ((e , e1) ∷ t) % 2
    ≡⟨⟩
       (2 + sum-of-dgree t ) % 2
    ≡⟨ cong ( λ k → k % 2 ) ( +-comm 2 (sum-of-dgree t) )  ⟩
       (sum-of-dgree t + 2) % 2
    ≡⟨ [a+n]%n≡a%n (sum-of-dgree t) _ ⟩
       sum-of-dgree t % 2
    ≡⟨ dgree-even t ⟩
       0
    ∎ where open ≡-Reasoning

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


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

------------------------------------------------------------------------------
-- The translation from pattern matching equations to equational
-- axioms requires some care because the pattern matching equations
-- are processed from top to bottom and from left to right.

-- From: Herbert P. Sander. A logic of functional programs with an
-- application to concurrency. PhD thesis, Chalmers University of
-- Technology and University of Gothenburg, Department of Computer
-- Sciences, 1992. pp. 12-13.

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

module Berry.Berry where

infix 7 _≡_

postulate
  D         : Set
  zero loop : D
  succ      : D → D

data _≡_ (x : D) : D → Set where
  refl : x ≡ x

-- For example, the translation of the Haskell function

-- f ∷ Nat → Nat → Nat → Nat
-- f Zero        (Succ Zero) x           = Succ Zero
-- f (Succ Zero) x           Zero        = Succ (Succ Zero)
-- f x           Zero        (Succ Zero) = Succ (Succ (Succ Zero))

-- to the equational axioms

postulate
  f     : D → D → D → D
  f-eq₁ : ∀ x → f zero        (succ zero) x           ≡ succ zero
  f-eq₂ : ∀ x → f (succ zero) x           zero        ≡ succ (succ zero)
  f-eq₃ : ∀ x → f x           zero        (succ zero) ≡ succ (succ (succ zero))
{-# ATP axioms f-eq₁ f-eq₂ f-eq₃ #-}

-- is not correct, because using the Haskell equations we have
--
-- f loop zero (succ zero) = *** Non-terminating ***
--
-- but using the equational axioms we can proof that
postulate
  bad : f loop zero (succ zero) ≡ succ (succ (succ zero))
{-# ATP prove bad #-}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Experiments.ZCohomologyOld.KcompPrelims where

open import Cubical.ZCohomology.Base
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Hopf
-- open import Cubical.Homotopy.Freudenthal hiding (encode)
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Truncation renaming (elim to trElim ; rec to trRec ; map to trMap)

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv.HalfAdjoint

open import Cubical.Data.Int renaming (_+_ to +Int) hiding (_·_)
open import Cubical.Data.Nat hiding (_·_)
open import Cubical.Data.Unit

open import Cubical.HITs.Susp
open import Cubical.HITs.Nullification
open import Cubical.Data.Prod.Base
open import Cubical.Homotopy.Loopspace
open import Cubical.Data.Bool
open import Cubical.Data.Sum.Base
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.HITs.S3

private
  variable
    ℓ : Level
    A : Type ℓ

{- We want to prove that Kn≃ΩKn+1. For this we use the map ϕ-}

-- Proof of Kₙ ≃ ∥ ΩSⁿ⁺¹ ∥ₙ for $n ≥ 2$
-- Entirely based on Cavallos proof of Freudenthal in Cubical.Homotopy.Freudenthal
module miniFreudenthal (n : HLevel) where
  σ : S₊ (2 + n) → typ (Ω (S₊∙ (3 + n)))
  σ a = merid a ∙ merid north ⁻¹

  S2+n = S₊ (2 + n)
  4n+2 = (2 + n) + (2 + n)

  module WC-S (p : north ≡ north) where
    P : (a b : S₊ (2 + n)) → Type₀
    P a b = σ b ≡ p → hLevelTrunc 4n+2 (fiber (λ x → merid x ∙ merid a ⁻¹) p)

    hLevelP : (a b : S₊ (2 + n)) → isOfHLevel 4n+2 (P a b)
    hLevelP _ _ = isOfHLevelΠ 4n+2 λ _ → isOfHLevelTrunc 4n+2

    leftFun : (a : S₊ (2 + n)) → P a north
    leftFun a r = ∣ a , (rCancel' (merid a) ∙ rCancel' (merid north) ⁻¹) ∙ r ∣

    rightFun : (b : S₊ (2 + n)) → P north b
    rightFun b r = ∣ b , r ∣

    funsAgree : leftFun north ≡ rightFun north
    funsAgree =
      funExt λ r → (λ i → ∣ north , rCancel' (rCancel' (merid north)) i ∙ r ∣)
                   ∙ λ i → ∣ north , lUnit r (~ i) ∣

    totalFun : (a b : S2+n) → P a b
    totalFun =  wedgeConSn (suc n) (suc n) hLevelP rightFun leftFun funsAgree .fst

    leftId : (λ x → totalFun x north) ≡ leftFun
    leftId x i = wedgeConSn (suc n) (suc n) hLevelP rightFun leftFun funsAgree .snd .snd i x

  fwd : (p : north ≡ north) (a : S2+n)
    → hLevelTrunc 4n+2 (fiber σ p)
    → hLevelTrunc 4n+2 (fiber (λ x → merid x ∙ merid a ⁻¹) p)
  fwd p a = trRec (isOfHLevelTrunc 4n+2) (uncurry (WC-S.totalFun p a))

  fwdnorth : (p : north ≡ north) → fwd p north ≡ idfun _
  fwdnorth p = funExt (trElim (λ _ → isOfHLevelPath 4n+2 (isOfHLevelTrunc 4n+2) _ _)
                      λ p → refl)

  isEquivFwd : (p : north ≡ north) (a : S2+n) → isEquiv (fwd p a)
  isEquivFwd p =
    suspToPropElim (ptSn (suc n))
                   (λ _ → isPropIsEquiv _)
                   helper
    where
    helper : isEquiv (fwd p north)
    helper = subst isEquiv (sym (fwdnorth p)) (idIsEquiv _)

  interpolate : (a : S2+n)
          → PathP (λ i → S2+n → north ≡ merid a i) (λ x → merid x ∙ merid a ⁻¹) merid
  interpolate a i x j = compPath-filler (merid x) (merid a ⁻¹) (~ i) j

  Code : (y : Susp S2+n) → north ≡ y → Type₀
  Code north p = hLevelTrunc 4n+2 (fiber σ p)
  Code south q = hLevelTrunc 4n+2 (fiber merid q)
  Code (merid a i) p =
    Glue
      (hLevelTrunc 4n+2 (fiber (interpolate a i) p))
      (λ
        { (i = i0) → _ , (fwd p a , isEquivFwd p a)
        ; (i = i1) → _ , idEquiv _
        })

  encodeS : (y : S₊ (3 + n)) (p : north ≡ y) → Code y p
  encodeS y = J Code ∣ north , rCancel' (merid north) ∣

  encodeMerid : (a : S2+n) → encodeS south (merid a) ≡ ∣ a , refl ∣
  encodeMerid a =
    cong (transport (λ i → gluePath i))
      (funExt⁻ (funExt⁻ (WC-S.leftId refl) a) _ ∙ λ i → ∣ a , lem (rCancel' (merid a)) (rCancel' (merid north)) i ∣)
    ∙ transport (PathP≡Path gluePath _ _)
      (λ i → ∣ a , (λ j k → rCancel-filler' (merid a) i j k) ∣)
    where
    gluePath : I → Type _
    gluePath i = hLevelTrunc 4n+2 (fiber (interpolate a i) (λ j → merid a (i ∧ j)))

    lem : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : z ≡ y) → (p ∙ q ⁻¹) ∙ q ≡ p
    lem p q = assoc p (q ⁻¹) q ⁻¹ ∙ cong (p ∙_) (lCancel q) ∙ rUnit p ⁻¹

  contractCodeSouth : (p : north ≡ south) (c : Code south p) → encodeS south p ≡ c
  contractCodeSouth p =
    trElim
      (λ _ → isOfHLevelPath 4n+2 (isOfHLevelTrunc 4n+2) _ _)
      (uncurry λ a →
        J (λ p r → encodeS south p ≡ ∣ a , r ∣) (encodeMerid a))

  isConnectedMerid : isConnectedFun 4n+2 (merid {A = S2+n})
  isConnectedMerid p = encodeS south p , contractCodeSouth p

  isConnectedσ : isConnectedFun 4n+2 σ
  isConnectedσ =
    transport (λ i → isConnectedFun 4n+2 (interpolate north (~ i))) isConnectedMerid

isConnectedσ-Sn : (n : ℕ) → isConnectedFun (4 + n) (miniFreudenthal.σ n)
isConnectedσ-Sn n =
  isConnectedFunSubtr _ n _
    (subst (λ x → isConnectedFun x (miniFreudenthal.σ n))
           helper
           (miniFreudenthal.isConnectedσ n))
  where
  helper : 2 + (n + (2 + n)) ≡ n + (4 + n)
  helper = cong suc (sym (+-suc n _)) ∙ sym (+-suc n _)

stabSpheres-n≥2 : (n : ℕ) → Iso (hLevelTrunc (4 + n) (S₊ (2 + n)))
                                  (hLevelTrunc (4 + n) (typ (Ω (S₊∙ (3 + n)))))
stabSpheres-n≥2 n = connectedTruncIso (4 + n) (miniFreudenthal.σ n) (isConnectedσ-Sn n)

--

ϕ : (pt a : A) → typ (Ω (Susp A , north))
ϕ pt a = (merid a) ∙ sym (merid pt)

private
  Kn→ΩKn+1 : (n : ℕ) → coHomK n → typ (Ω (coHomK-ptd (suc n)))
  Kn→ΩKn+1 zero x i = ∣ intLoop x i ∣
  Kn→ΩKn+1 (suc zero) = trRec (isOfHLevelTrunc 4 ∣ north ∣ ∣ north ∣)
                               λ a i → ∣ ϕ base a i ∣
  Kn→ΩKn+1 (suc (suc n)) = trRec (isOfHLevelTrunc (2 + (3 + n)) ∣ north ∣ ∣ north ∣)
                                  λ a i → ∣ ϕ north a i ∣

  d-map : typ (Ω ((Susp S¹) , north)) → S¹
  d-map p = subst HopfSuspS¹ p base

  d-mapId : (r : S¹) → d-map (ϕ base r) ≡ r
  d-mapId r = substComposite HopfSuspS¹ (merid r) (sym (merid base)) base ∙
              rotLemma r
    where
    rotLemma : (r : S¹) → r · base ≡ r
    rotLemma base = refl
    rotLemma (loop i) = refl

sphereConnectedSpecCase : isConnected 4 (Susp (Susp S¹))
sphereConnectedSpecCase = sphereConnected 3

d-mapComp : Iso (fiber d-map base) (Path (S₊ 3) north north)
d-mapComp = compIso (IsoΣPathTransportPathΣ {B = HopfSuspS¹} _ _)
                     (congIso (invIso IsoS³TotalHopf))

is1Connected-dmap : isConnectedFun 3 d-map
is1Connected-dmap = toPropElim (λ _ → isPropIsOfHLevel 0)
                               (isConnectedRetractFromIso 3 d-mapComp
                                 (isOfHLevelRetractFromIso 0 (invIso (PathIdTruncIso 3))
                                              contrHelper))
  where
  contrHelper : isContr (Path (∥ Susp (Susp S¹) ∥ 4) ∣ north ∣ ∣ north ∣)
  fst contrHelper = refl
  snd contrHelper = isOfHLevelPlus {n = 0} 2 (sphereConnected 3) ∣ north ∣ ∣ north ∣ refl

d-Iso : Iso (∥ Path (S₊ 2) north north ∥ 3) (coHomK 1)
d-Iso = connectedTruncIso _ d-map is1Connected-dmap

d-mapId2 : Iso.fun d-Iso ∘ trMap (ϕ base) ≡ idfun (coHomK 1)
d-mapId2 = funExt (trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) λ a i → ∣ d-mapId a i ∣)

Iso∥ϕ₁∥ : Iso (coHomK 1) (∥ Path (S₊ 2) north north ∥ 3)
Iso∥ϕ₁∥ = composesToId→Iso d-Iso (trMap (ϕ base)) d-mapId2

Iso-Kn-ΩKn+1 : (n : HLevel) → Iso (coHomK n) (typ (Ω (coHomK-ptd (suc n))))
Iso-Kn-ΩKn+1 zero = invIso (compIso (congIso (truncIdempotentIso _ isGroupoidS¹)) ΩS¹IsoInt)
Iso-Kn-ΩKn+1 (suc zero) = compIso Iso∥ϕ₁∥ (invIso (PathIdTruncIso 3))
Iso-Kn-ΩKn+1 (suc (suc n)) = compIso (stabSpheres-n≥2 n)
                                     (invIso (PathIdTruncIso (4 + n)))
 where
  helper : n + (4 + n) ≡ 2 + (n + (2 + n))
  helper = +-suc n (3 + n) ∙ (λ i → suc (+-suc n (2 + n) i))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- Unary relations
------------------------------------------------------------------------

module Relation.Unary where

open import Data.Empty
open import Data.Function
open import Data.Unit
open import Data.Product
open import Data.Sum
open import Relation.Nullary

------------------------------------------------------------------------
-- Unary relations

Pred : Set → Set₁
Pred a = a → Set

------------------------------------------------------------------------
-- Unary relations can be seen as sets

-- I.e., they can be seen as subsets of the universe of discourse.

private
 module Dummy {a : Set} -- The universe of discourse.
          where

  -- Set membership.

  infix 4 _∈_ _∉_

  _∈_ : a → Pred a → Set
  x ∈ P = P x

  _∉_ : a → Pred a → Set
  x ∉ P = ¬ x ∈ P

  -- The empty set.

  ∅ : Pred a
  ∅ = λ _ → ⊥

  -- The property of being empty.

  Empty : Pred a → Set
  Empty P = ∀ x → x ∉ P

  ∅-Empty : Empty ∅
  ∅-Empty x ()

  -- The universe, i.e. the subset containing all elements in a.

  U : Pred a
  U = λ _ → ⊤

  -- The property of being universal.

  Universal : Pred a → Set
  Universal P = ∀ x → x ∈ P

  U-Universal : Universal U
  U-Universal = λ _ → _

  -- Set complement.

  ∁ : Pred a → Pred a
  ∁ P = λ x → x ∉ P

  ∁∅-Universal : Universal (∁ ∅)
  ∁∅-Universal = λ x x∈∅ → x∈∅

  ∁U-Empty : Empty (∁ U)
  ∁U-Empty = λ x x∈∁U → x∈∁U _

  -- P ⊆ Q means that P is a subset of Q. _⊆′_ is a variant of _⊆_.

  infix 4 _⊆_ _⊇_ _⊆′_ _⊇′_

  _⊆_ : Pred a → Pred a → Set
  P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

  _⊆′_ : Pred a → Pred a → Set
  P ⊆′ Q = ∀ x → x ∈ P → x ∈ Q

  _⊇_ : Pred a → Pred a → Set
  Q ⊇ P = P ⊆ Q

  _⊇′_ : Pred a → Pred a → Set
  Q ⊇′ P = P ⊆′ Q

  ∅-⊆ : (P : Pred a) → ∅ ⊆ P
  ∅-⊆ P ()

  ⊆-U : (P : Pred a) → P ⊆ U
  ⊆-U P _ = _

  -- Set union.

  infixl 6 _∪_

  _∪_ : Pred a → Pred a → Pred a
  P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q

  -- Set intersection.

  infixl 7 _∩_

  _∩_ : Pred a → Pred a → Pred a
  P ∩ Q = λ x → x ∈ P × x ∈ Q

open Dummy public

------------------------------------------------------------------------
-- Unary relation combinators

infixr 2 _⟨×⟩_
infixr 1 _⟨⊎⟩_
infixr 0 _⟨→⟩_

_⟨×⟩_ : ∀ {A B} → Pred A → Pred B → Pred (A × B)
(P ⟨×⟩ Q) p = P (proj₁ p) × Q (proj₂ p)

_⟨⊎⟩_ : ∀ {A B} → Pred A → Pred B → Pred (A ⊎ B)
(P ⟨⊎⟩ Q) (inj₁ p) = P p
(P ⟨⊎⟩ Q) (inj₂ q) = Q q

_⟨→⟩_ : ∀ {A B} → Pred A → Pred B → Pred (A → B)
(P ⟨→⟩ Q) f = P ⊆ Q ∘₀ f

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module main where

open import prelude
open import defns
open import lemmas

BackTheorem : ∀ {D} {H H′ H″ : NavigationHistory(D)} {δ δ′} →
  (WellFormed(H)) →
  (H traverses-by (-ve δ) to H′) →
  (H′ traverses-by δ′ to H″) →
  (H traverses-by (-ve δ + δ′) to H″)

BackTheorem {δ = zero} H∈WF (back nil ds∈CGB ds∈BT) H′-to-H″ = H′-to-H″
BackTheorem {D} {H} {._} {H″} {δ = succ δ} {δ′} H∈WF (back (d ∷ ds) (d∈CGB , ds∈CGB) d∷ds∈BT) H′-to-H″ = H-to-H″ where

  H₁ = (H traverse-from d ∵ d∈CGB)
  H′ = (H₁ traverses-from ds ∵ ds∈CGB)

  d∈BT : (d ∈ BackTarget(H))
  d∈BT = BT-hd {H = H} d ds d∷ds∈BT

  ds∈BT₁ : (ds ∈ BackTarget*(H₁))
  ds∈BT₁ = BT-tl {H = H} d d∈CGB ds d∷ds∈BT

  H₁∈WF : WellFormed(H₁)
  H₁∈WF = back-WF H d d∈CGB H∈WF d∈BT

  H₁-to-H″ : H₁ traverses-by (-ve δ + δ′) to H″
  H₁-to-H″ = BackTheorem H₁∈WF (back ds ds∈CGB ds∈BT₁) H′-to-H″

  Lemma : ∀ {H″} n →
    (H₁ traverses-by n to H″) →
    (H traverses-by pred n to H″)
  Lemma (succ zero) (fwd (e ∷ nil) e∷es∈FT₁) = H-to-H₀ where

    H₀ = (H₁ traverse-to e)

    e∈FT₁ : (e ∈ FwdTarget(H₁))
    e∈FT₁ = FT-hd {H = H₁} e nil e∷es∈FT₁

    H=H₀ : H ≣ H₀
    H=H₀ = from-to d e d∈CGB H∈WF d∈BT e∈FT₁

    H₀-to-H₀ : (H₀ traverses-by (-ve zero) to H₀)
    H₀-to-H₀ = back nil tt (BT-nil {H = H₀})

    H-to-H₀ : H traverses-by (-ve zero) to H₀
    H-to-H₀ = SUBST (λ ∙ → ∙ traverses-by (-ve zero) to H₀) H=H₀ H₀-to-H₀

  Lemma (succ (succ n)) (fwd (e ∷ es) e∷es∈FT₁) = H-to-Hₙ where

    H₀ = (H₁ traverse-to e)
    Hₙ = (H₁ traverses-to (e ∷ es))

    e∈FT₁ : (e ∈ FwdTarget(H₁))
    e∈FT₁ = FT-hd {H = H₁} e es e∷es∈FT₁

    es∈FT₀ : (es ∈ FwdTarget*(H₀))
    es∈FT₀ = FT-tl {H = H₁} e es e∷es∈FT₁

    H=H₀ : H ≣ H₀
    H=H₀ = from-to d e d∈CGB H∈WF d∈BT e∈FT₁

    H₀-to-Hₙ : H₀ traverses-by (succ n) to Hₙ
    H₀-to-Hₙ = fwd es es∈FT₀

    H-to-Hₙ : H traverses-by (succ n) to Hₙ
    H-to-Hₙ = SUBST (λ ∙ → ∙ traverses-by succ n to Hₙ) H=H₀ H₀-to-Hₙ

  Lemma (-ve n) (back es es∈CGB es∈BT₁) = back (d ∷ es) (d∈CGB , es∈CGB) (BT-cons {H = H} d d∈CGB es d∈BT es∈BT₁)

  H-to-H″ : H traverses-by (-ve (succ δ) + δ′) to H″
  H-to-H″ = Lemma (-ve δ + δ′) H₁-to-H″

FwdTheorem : ∀ {D} {H H′ H″ : NavigationHistory(D)} {δ δ′} →
  (WellFormed(H)) →
  (H traverses-by (succ δ) to H′) →
  (H′ traverses-by δ′ to H″) →
  (H traverses-by (succ δ + δ′) to H″)

FwdTheorem {D} {H} {._} {H″} {δ = δ} {δ′} H∈WF (fwd (d ∷ ds) d∷ds∈FT) H′-to-H″ with Lemma where

  H₁ = (H traverse-to d)
  H′ = (H₁ traverses-to ds)

  d∈FT : (d ∈ FwdTarget(H))
  d∈FT = FT-hd {H = H} d ds d∷ds∈FT

  Lemma : ∀ {H″} n →
    (H₁ traverses-by n to H″) →
    (H traverses-by sucz n to H″)
  Lemma (succ n) (fwd es es∈FT₁) = fwd (d ∷ es) (FT-cons {H = H} d es d∈FT es∈FT₁)

  Lemma (-ve zero) (back nil _ _) = fwd (d ∷ nil) (FT-cons {H = H} d nil d∈FT (FT-nil {H = H₁}))

  Lemma (-ve (succ n)) (back (e ∷ es) (e∈CGB , es∈CGB) e∷es∈BT₁) = H-to-Hₙ where

    H₀ = (H₁ traverse-from e ∵ e∈CGB)
    Hₙ = (H₁ traverses-from (e ∷ es) ∵ (e∈CGB , es∈CGB))

    e∈BT₁ : (e ∈ BackTarget(H₁))
    e∈BT₁ = BT-hd {H = H₁} e es e∷es∈BT₁

    es∈BT₀ : (es ∈ BackTarget*(H₀))
    es∈BT₀ = BT-tl {H = H₁} e e∈CGB es e∷es∈BT₁

    H=H₀ : H ≣ H₀
    H=H₀ = to-from d e e∈CGB H∈WF d∈FT e∈BT₁

    H₀-to-Hₙ : H₀ traverses-by (-ve n) to Hₙ
    H₀-to-Hₙ = back es es∈CGB es∈BT₀

    H-to-Hₙ : H traverses-by (-ve n) to Hₙ
    H-to-Hₙ = SUBST (λ ∙ → ∙ traverses-by (-ve n) to Hₙ) H=H₀ H₀-to-Hₙ

FwdTheorem {D} {H} {._} {H″} {δ = zero} {δ′} H∈WF (fwd (d ∷ nil) d∷nil∈FT) H′-to-H″ | Lemma = Lemma δ′ H′-to-H″

FwdTheorem {D} {H} {._} {H″} {δ = succ δ} {δ′} H∈WF (fwd (d ∷ ds) d∷ds∈FT) H′-to-H″ | Lemma = H-to-H″ where

  H₁ = (H traverse-to d)

  d∈FT : (d ∈ FwdTarget(H))
  d∈FT = FT-hd {H = H} d ds d∷ds∈FT

  ds∈FT₁ : (ds ∈ FwdTarget*(H₁))
  ds∈FT₁ = FT-tl {H = H} d ds d∷ds∈FT

  H₁∈WF : WellFormed(H₁)
  H₁∈WF = fwd-WF H d H∈WF d∈FT

  H₁-to-H″ : H₁ traverses-by (succ δ + δ′) to H″
  H₁-to-H″ = FwdTheorem H₁∈WF (fwd ds ds∈FT₁) H′-to-H″

  H-to-H″ : H traverses-by sucz (succ δ + δ′) to H″
  H-to-H″ = subst (λ ∙ → H traverses-by ∙ to H″) (succ-dist-+ (succ δ) δ′) (Lemma (succ δ + δ′) H₁-to-H″)

Theorem : ∀ {D} {H H′ H″ : NavigationHistory(D)} {δ δ′} →
  (WellFormed(H)) →
  (H traverses-by δ to H′) →
  (H′ traverses-by δ′ to H″) →
  (H traverses-by (δ + δ′) to H″)

Theorem {δ = succ δ} = FwdTheorem
Theorem {δ = -ve δ} = BackTheorem

max_stars_repo_name: cbrewster/ServoNavigation

max_issues_repo_name: cbrewster/ServoNavigation

max_forks_repo_name: cbrewster/ServoNavigation


text:
{-

This file contains:

- Properties of 2-groupoid truncations

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.2GroupoidTruncation.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.2GroupoidTruncation.Base

rec : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (gB : is2Groupoid B) → (A → B) → (∥ A ∥₂ → B)
rec gB f ∣ x ∣₂ = f x
rec gB f (squash₂ _ _ _ _ _ _ t u i j k l) =
  gB _ _ _ _ _ _
    (λ m n o → rec gB f (t m n o))
    (λ m n o → rec gB f (u m n o))
    i j k l

elim : ∀ {ℓ ℓ'} {A : Type ℓ} {B : ∥ A ∥₂ → Type ℓ'}
  (bG : (x : ∥ A ∥₂) → is2Groupoid (B x))
  (f : (x : A) → B ∣ x ∣₂) (x : ∥ A ∥₂) → B x
elim bG f ∣ x ∣₂ = f x
elim bG f (squash₂ x y p q r s u v i j k l) =
  isOfHLevel→isOfHLevelDep 4 bG _ _ _ _ _ _
    (λ j k l → elim bG f (u j k l)) (λ j k l → elim bG f (v j k l))
    (squash₂ x y p q r s u v)
    i j k l

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
------------------------------------------------------------------------
-- The structure identity principle can be used to establish that
-- isomorphism coincides with equality (assuming univalence)
------------------------------------------------------------------------

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

open import Equality

module
  Univalence-axiom.Isomorphism-is-equality.Structure-identity-principle
    {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Bijection eq using (_↔_)
open import Category eq
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq renaming (_∘_ to _⊚_)
open import H-level eq
open import H-level.Closure eq
open import Logical-equivalence using (_⇔_)
open import Prelude as P
open import Structure-identity-principle eq
open import Univalence-axiom eq
open import Univalence-axiom.Isomorphism-is-equality.Simple eq
  using (Assumptions; module Assumptions;
         Universe; module Universe;
         module Class)

-- The structure identity principle can be used to prove a slightly
-- restricted variant of isomorphism-is-equality (which is defined in
-- Univalence-axiom.Isomorphism-is-equality.Simple.Class).

isomorphism-is-equality′ :
  (Univ : Universe) → let open Universe Univ in
  Assumptions →
  ∀ c X Y →
  (∀ {B} → Is-set B → Is-set (El (proj₁ c) B)) →  -- Extra assumption.
  Is-set (proj₁ X) → Is-set (proj₁ Y) →           -- Extra assumptions.
  Class.Isomorphic Univ c X Y ↔ (X ≡ Y)
isomorphism-is-equality′ Univ ass
  (a , P) (C , x , p) (D , y , q) El-set C-set D-set = isomorphic

  module Isomorphism-is-equality′ where

  open Assumptions ass
  open Universe Univ
  open Class Univ using (Carrier; Instance; Isomorphic)

  -- The category of sets and functions.

  Fun : Category (# 2) (# 1)
  Fun = category-Set (# 1) ext (λ _ _ → univ₁)

  module Fun = Category Fun

  -- The category of sets and bijections.

  Bij : Category (# 2) (# 1)
  Bij = category-Set-≅ (# 1) ext (λ _ _ → univ₁)

  module Bij = Category Bij

  -- If two sets are isomorphic, then the underlying types are
  -- equivalent.

  ≅⇒≃ : (C D : Fun.Obj) → C Fun.≅ D → ⌞ C ⌟ ≃ ⌞ D ⌟
  ≅⇒≃ C D = _≃_.from (≃≃≅-Set (# 1) ext C D)

  -- The "standard notion of structure" that the structure identity
  -- principle is instantiated with.

  S : Standard-notion-of-structure (# 1) (# 1) Bij.precategory
  S = record
    { P               = El a ∘ ⌞_⌟
    ; H               = λ {C D} x y C≅D →
                          Is-isomorphism a (≅⇒≃ C D C≅D) x y
    ; H-prop          = λ {C D} → H-prop′ C D
    ; H-id            = λ {C} → H-id′ C
    ; H-∘             = λ {B C D} → H-∘′ B C D
    ; H-antisymmetric = λ {C} → H-antisymmetric′ C
    }
    where

    module Separate-abstract-block where

      abstract

        H-prop′ :
          (C D : Set (# 1))
          {x : El a ⌞ C ⌟} {y : El a ⌞ D ⌟}
          (f : Bij.Hom C D) →
          Is-proposition (Is-isomorphism a (≅⇒≃ C D f) x y)
        H-prop′ _ D _ = El-set (proj₂ D)

        H-id′ :
          (C : Set (# 1)) {x : El a ⌞ C ⌟} →
          Is-isomorphism a (≅⇒≃ C C (Bij.id {X = C})) x x
        H-id′ C {x} =
          resp a (≅⇒≃ C C (Bij.id {X = C})) x  ≡⟨ cong (λ eq → resp a eq x) $ Eq.lift-equality ext (refl _) ⟩
          resp a Eq.id x                       ≡⟨ resp-id ass a x ⟩∎
          x                                    ∎

        H-∘′ :
          (B C D : Set (# 1))
          {x : El a ⌞ B ⌟} {y : El a ⌞ C ⌟} {z : El a ⌞ D ⌟}
          {B≅C : Bij.Hom B C} {C≅D : Bij.Hom C D} →
          Is-isomorphism a (≅⇒≃ B C B≅C) x y →
          Is-isomorphism a (≅⇒≃ C D C≅D) y z →
          Is-isomorphism a
            (≅⇒≃ B D (Bij._∙_ {X = B} {Y = C} {Z = D} C≅D B≅C)) x z
        H-∘′ B C D {x} {y} {z} {B≅C} {C≅D} x≅y y≅z =
          resp a (≅⇒≃ B D (C≅D Bij.∙ B≅C)) x             ≡⟨ cong (λ eq → resp a eq x) $ Eq.lift-equality ext (refl _) ⟩
          resp a (≅⇒≃ C D C≅D ⊚ ≅⇒≃ B C B≅C) x           ≡⟨ resp-preserves-compositions (El a) (resp a) (resp-id ass a)
                                                                                univ₁ ext (≅⇒≃ B C B≅C) (≅⇒≃ C D C≅D) x ⟩
          resp a (≅⇒≃ C D C≅D) (resp a (≅⇒≃ B C B≅C) x)  ≡⟨ cong (resp a (≅⇒≃ C D C≅D)) x≅y ⟩
          resp a (≅⇒≃ C D C≅D) y                         ≡⟨ y≅z ⟩∎
          z                                              ∎

        H-antisymmetric′ :
          (C : Set (# 1))
          (x y : El a ⌞ C ⌟) →
          Is-isomorphism a (≅⇒≃ C C (Bij.id {X = C})) x y →
          Is-isomorphism a (≅⇒≃ C C (Bij.id {X = C})) y x →
          x ≡ y
        H-antisymmetric′ C x y x≡y _ =
          x                                    ≡⟨ sym $ resp-id ass a x ⟩
          resp a Eq.id x                       ≡⟨ cong (λ eq → resp a eq x) $ Eq.lift-equality ext (refl _) ⟩
          resp a (≅⇒≃ C C (Bij.id {X = C})) x  ≡⟨ x≡y ⟩∎
          y                                    ∎

    open Separate-abstract-block

  open module S = Standard-notion-of-structure S
    using (H; Str; module Str)

  abstract

    -- Every Str morphism is an isomorphism.

    Str-homs-are-isos :
      ∀ {C D x y} (f : ∃ (H {X = C} {Y = D} x y)) →
      Str.Is-isomorphism {X = C , x} {Y = D , y} f
    Str-homs-are-isos {C} {D} {x} {y} (C≅D , x≅y) =

      (D≅C ,
       (resp a (≅⇒≃ D C D≅C) y            ≡⟨ cong (λ eq → resp a eq y) $ Eq.lift-equality ext (refl _) ⟩
        resp a (inverse $ ≅⇒≃ C D C≅D) y  ≡⟨ resp-preserves-inverses (El a) (resp a) (resp-id ass a) univ₁ ext (≅⇒≃ C D C≅D) _ _ x≅y ⟩∎
        x                                 ∎)) ,

      S.lift-equality {X = D , y} {Y = D , y} (
        C≅D Fun.∙≅ D≅C   ≡⟨ _≃_.from (Fun.≡≃≡¹ {X = D} {Y = D}) (Fun._¹⁻¹ {X = C} {Y = D} C≅D) ⟩∎
        Fun.id≅ {X = D}  ∎) ,

      S.lift-equality {X = C , x} {Y = C , x} (
        D≅C Fun.∙≅ C≅D   ≡⟨ _≃_.from (Fun.≡≃≡¹ {X = C} {Y = C}) (Fun._⁻¹¹ {X = C} {Y = D} C≅D) ⟩∎
        Fun.id≅ {X = C}  ∎)

      where

      D≅C : D Fun.≅ C
      D≅C = Fun._⁻¹≅ {X = C} {Y = D} C≅D

    -- The isomorphism that should be constructed.

    isomorphic : Isomorphic (a , P) (C , x , p) (D , y , q) ↔
                 _≡_ {A = Instance (a , P)} (C , x , p) (D , y , q)
    isomorphic =
      Σ (C ≃ D) (λ eq → Is-isomorphism a eq x y)                   ↝⟨ (let ≃≃≅-CD = ≃≃≅-Set (# 1) ext (C , C-set) (D , D-set) in
                                                                       Σ-cong ≃≃≅-CD (λ eq →
                                                                         let eq′ = _≃_.from ≃≃≅-CD (_≃_.to ≃≃≅-CD eq) in
                                                                         Is-isomorphism a eq  x y  ↝⟨ ≡⇒↝ _ $
                                                                                cong (λ eq → Is-isomorphism a eq x y) $ sym $
                                                                                _≃_.left-inverse-of ≃≃≅-CD eq ⟩
                                                                         Is-isomorphism a eq′ x y  □)) ⟩
      ∃ (H {X = C , C-set} {Y = D , D-set} x y)                    ↝⟨ inverse ×-right-identity ⟩
      ∃ (H {X = C , C-set} {Y = D , D-set} x y) × ⊤                ↝⟨ ∃-cong (λ X≅Y → inverse $ _⇔_.to contractible⇔↔⊤ $
                                                                                propositional⇒inhabited⇒contractible
                                                                                (Str.Is-isomorphism-propositional X≅Y)
                                                                                (Str-homs-are-isos X≅Y)) ⟩
      (((C , C-set) , x) Str.≅ ((D , D-set) , y))                  ↔⟨ inverse Eq.⟨ _ , structure-identity-principle ext Bij S
                                                                                {X = (C , C-set) , x} {Y = (D , D-set) , y} ⟩ ⟩
      (((C , λ {_ _} → C-set) , x) ≡ ((D , λ {_ _} → D-set) , y))  ↔⟨ Eq.≃-≡ $ Eq.↔⇒≃ (Σ-assoc ⊚ ∃-cong (λ _ → ×-comm) ⊚ inverse Σ-assoc) ⟩
      (((C , x) , λ {_ _} → C-set) ≡ ((D , y) , λ {_ _} → D-set))  ↝⟨ inverse $ ignore-propositional-component (H-level-propositional ext 2) ⟩
      ((C , x) ≡ (D , y))                                          ↝⟨ ignore-propositional-component (proj₂ (P D y) ass) ⟩
      (((C , x) , p) ≡ ((D , y) , q))                              ↔⟨ Eq.≃-≡ $ Eq.↔⇒≃ Σ-assoc ⟩□
      ((C , x , p) ≡ (D , y , q))                                  □

    -- A simplification lemma.

    proj₁-from-isomorphic :
      ∀ X≡Y →
      proj₁ (_↔_.from isomorphic X≡Y) ≡
      elim (λ {X Y} _ → proj₁ X ≃ proj₁ Y) (λ _ → Eq.id) X≡Y
    proj₁-from-isomorphic X≡Y = Eq.lift-equality ext (

      _≃_.to (proj₁ (_↔_.from isomorphic X≡Y))                         ≡⟨⟩

      cast C-set D-set X≡Y                                             ≡⟨ lemma ⟩∎

      _≃_.to (elim (λ {X Y} _ → proj₁ X ≃ proj₁ Y) (λ _ → Eq.id) X≡Y)  ∎)

      where

      cast : ∀ {X Y} →
             Is-set (Carrier (a , P) X) → Is-set (Carrier (a , P) Y) →
             X ≡ Y → Carrier (a , P) X → Carrier (a , P) Y
      cast {C , x , p} {D , y , q} C-set D-set X≡Y =
        proj₁ $ proj₁ $ proj₁ $
        Str.≡→≅ {X = (C , C-set) , x} {Y = (D , D-set) , y} $
        cong (λ { ((C , x) , C-set) → (C , C-set) , x }) $
        Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡
                   (cong (λ { (C , (x , p)) → (C , x) , p }) X≡Y)))
                (proj₁ (+⇒≡ $ H-level-propositional ext 2))

      lemma :
        cast C-set D-set X≡Y ≡
        _≃_.to (elim (λ {X Y} _ → proj₁ X ≃ proj₁ Y) (λ _ → Eq.id) X≡Y)
      lemma = elim¹
        (λ X≡Y → (D-set : Is-set _) →
                 cast C-set D-set X≡Y ≡
                 _≃_.to (elim (λ {X Y} _ → proj₁ X ≃ proj₁ Y)
                              (λ _ → Eq.id) X≡Y))
        (λ C-set′ →

           cast C-set C-set′ (refl (C , x , p))                           ≡⟨ cong (λ eq →
                                                                                proj₁ $ proj₁ $ proj₁ $
                                                                                Str.≡→≅ {X = (C , C-set) , x} {Y = (C , C-set′) , x} $
                                                                                cong (λ { ((C , x) , C-set) → (C , C-set) , x }) $
                                                                                Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ {B = proj₁ ∘ uncurry P} eq))
                                                                                (proj₁ (+⇒≡ $ H-level-propositional ext 2)))
                                                                                (cong-refl (λ { (C , (x , p)) → (C , x) , p })) ⟩
           (proj₁ $ proj₁ $ proj₁ $
            Str.≡→≅ {X = (C , C-set) , x} {Y = (C , C-set′) , x} $
            cong (λ { ((C , x) , C-set) → (C , C-set) , x }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (+⇒≡ $ H-level-propositional ext 2)))          ≡⟨ cong proj₁ (S.proj₁-≡→≅-¹ _) ⟩

           (proj₁ $
            Fun.≡→≅ $
            cong proj₁ $
            cong (λ { ((C , x) , C-set) → (C , C-set) , x }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (+⇒≡ $ H-level-propositional ext 2)))          ≡⟨ cong (proj₁ ∘ Fun.≡→≅) $
                                                                               cong-∘ proj₁ (λ { ((C , x) , C-set) → (C , C-set) , x }) _ ⟩
           (proj₁ $
            Fun.≡→≅ $
            cong (λ { ((C , _) , C-set) → C , C-set }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (+⇒≡ $ H-level-propositional ext 2)))          ≡⟨ Fun.≡→≅-¹ _ ⟩

           (elim (λ {X Y} _ → Fun.Hom X Y) (λ _ → P.id) $
            cong (λ { ((C , _) , C-set) → C , C-set }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (+⇒≡ $ H-level-propositional ext 2)))          ≡⟨ elim¹ (λ eq → elim (λ {X Y} _ → Fun.Hom X Y) (λ _ → P.id) eq ≡
                                                                                ≡⇒↝ implication (cong proj₁ eq)) (
               elim (λ {X Y} _ → Fun.Hom X Y) (λ _ → P.id)
                    (refl (C , λ {_ _} → C-set))                                        ≡⟨ elim-refl (λ {X Y} _ → Fun.Hom X Y) _ ⟩
               P.id                                                                     ≡⟨ sym $ elim-refl (λ {A B} _ → A → B) _ ⟩
               ≡⇒↝ implication (refl C)                                                 ≡⟨ cong (≡⇒↝ implication) (sym $ cong-refl proj₁) ⟩∎
               ≡⇒↝ implication (cong proj₁ (refl (C , λ {_ _} → C-set)))                ∎) _ ⟩

           (≡⇒↝ implication $
            cong proj₁ $
            cong (λ { ((C , _) , C-set) → C , C-set }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (+⇒≡ $ H-level-propositional ext 2)))          ≡⟨ cong (≡⇒↝ implication)
                                                                                (cong-∘ proj₁ (λ { ((C , _) , C-set) → C , C-set }) _) ⟩
           (≡⇒↝ implication $
            cong (λ { ((C , _) , _) → C }) $
            Σ-≡,≡→≡ (proj₁ (Σ-≡,≡←≡ (refl ((C , x) , p))))
                    (proj₁ (+⇒≡ $ H-level-propositional ext 2)))          ≡⟨ cong (λ (eq : ∃ λ q → subst (proj₁ ∘ uncurry P) q p ≡ p) →
                                                                                ≡⇒↝ implication $
                                                                                cong (λ { ((C , _) , _) → C }) $
                                                                                Σ-≡,≡→≡ (proj₁ eq)
                                                                                (proj₁ (+⇒≡ $ H-level-propositional ext 2)))
                                                                                (Σ-≡,≡←≡-refl {B = λ { (C , x) → proj₁ (P C x)}}) ⟩
           (≡⇒↝ implication $
            cong (λ { ((C , _) , _) → C }) $
            Σ-≡,≡→≡ (refl (C , x))
                    (proj₁ (+⇒≡ $ H-level-propositional ext 2)))          ≡⟨ cong (≡⇒↝ implication ∘ cong (λ { ((C , _) , _) → C }))
                                                                                (Σ-≡,≡→≡-reflˡ (proj₁ (+⇒≡ $ H-level-propositional ext 2))) ⟩
           (≡⇒↝ implication $
            cong (λ { ((C , _) , _) → C }) $
            cong (_,_ (C , x))
                 (trans (sym $ subst-refl (Is-set ∘ proj₁) C-set)
                        (proj₁ (+⇒≡ $ H-level-propositional ext 2))))     ≡⟨ cong (≡⇒↝ implication)
                                                                                (cong-∘ (λ { ((C , _) , _) → C }) (_,_ (C , x)) _) ⟩
           (≡⇒↝ implication $
            cong (const C)
                 (trans (sym $ subst-refl (Is-set ∘ proj₁) C-set)
                        (proj₁ (+⇒≡ $ H-level-propositional ext 2))))     ≡⟨ cong (≡⇒↝ implication) (cong-const _) ⟩

           ≡⇒↝ implication (refl C)                                       ≡⟨ ≡⇒↝-refl ⟩

           P.id                                                           ≡⟨ sym $ cong _≃_.to $ elim-refl (λ {X Y} _ → proj₁ X ≃ proj₁ Y) _ ⟩∎

           _≃_.to (elim (λ {X Y} _ → proj₁ X ≃ proj₁ Y)
                        (λ _ → Eq.id)
                        (refl (C , x , p)))                               ∎)

        X≡Y D-set

abstract

  -- The from component of isomorphism-is-equality′ is equal
  -- to a simple function.

  from-isomorphism-is-equality′ :
    ∀ Univ ass c X Y → let open Universe Univ; open Class Univ in
    (El-set : ∀ {B} → Is-set B → Is-set (El (proj₁ c) B)) →
    (X-set : Is-set (proj₁ X)) (Y-set : Is-set (proj₁ Y)) →
    _↔_.from (isomorphism-is-equality′
                Univ ass c X Y El-set X-set Y-set) ≡
    elim (λ {X Y} _ → Isomorphic c X Y)
         (λ { (_ , x , _) → Eq.id , resp-id ass (proj₁ c) x })
  from-isomorphism-is-equality′ Univ ass c X Y El-set X-set Y-set =
    apply-ext ext λ eq →
      Σ-≡,≡→≡ (lemma eq) (El-set Y-set _ _)
    where
    open Assumptions ass
    open Universe Univ
    open Class Univ

    lemma :
      ∀ eq →
      proj₁ (_↔_.from (isomorphism-is-equality′
                         Univ ass c X Y El-set X-set Y-set) eq) ≡
      proj₁ (elim (λ {X Y} _ → Isomorphic c X Y)
                  (λ { (_ , x , _) → Eq.id , resp-id ass (proj₁ c) x })
                  eq)
    lemma eq =
      proj₁ (_↔_.from (isomorphism-is-equality′
                         Univ ass c X Y El-set X-set Y-set) eq)          ≡⟨ Isomorphism-is-equality′.proj₁-from-isomorphic
                                                                              Univ ass _ _ _ _ _ _ _ _ El-set X-set Y-set eq ⟩
      elim (λ {X Y} _ → proj₁ X ≃ proj₁ Y) (λ _ → Eq.id) eq              ≡⟨ sym $ elim-∘ (λ {X Y} _ → Isomorphic c X Y) _ proj₁ _ ⟩∎
      proj₁ (elim (λ {X Y} _ → Isomorphic c X Y)
                  (λ { (_ , x , _) → Eq.id , resp-id ass (proj₁ c) x })
                  eq)                                                    ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Thesis.Contexts where

open import Thesis.Types

-- Instantiate generic Context support
open import Base.Syntax.Context Type public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
-- {-# OPTIONS -v tc.meta:30 #-}
{-# OPTIONS --sized-types #-}
module GiveSize where

postulate Size : Set
postulate ∞ : Size
{-# BUILTIN SIZE Size #-}
-- {-# BUILTIN SIZEINF ∞ #-}

id : Size → Size
id i = {!i!}

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module par-swap.union-properties where

open import par-swap
open import par-swap.union-confluent
open import par-swap.confluent
open import sn-calculus
open import sn-calculus-props
open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Context
open import Esterel.Context.Properties
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; sig ; []env ; VarList ;
         module SigMap ; module ShrMap ; module VarMap)
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Data.Product
open import Data.Empty
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; sym)

open import binding-preserve

∥R∪sn≡ₑ-preserve-cb : ∀ {p BVp FVp q} ->
  CorrectBinding p BVp FVp ->
  p ∥R∪sn≡ₑ q ->
  Σ (VarList × VarList) λ { (BVq , FVq) -> CorrectBinding q BVq FVq }
∥R∪sn≡ₑ-preserve-cb CBp (∪stpsn psn⟶q)
  with sn⟶-maintains-binding CBp psn⟶q
... | _ , CBq , _ = _ , CBq
∥R∪sn≡ₑ-preserve-cb CBp (∪stp∥ p∥Rq)
  with ∥R-maintains-binding CBp p∥Rq
... | CBq = _ , CBq
∥R∪sn≡ₑ-preserve-cb CBp (∪sym p∪≡ₑq CBq) = _ , CBq
∥R∪sn≡ₑ-preserve-cb CBp ∪ref = _ , CBp
∥R∪sn≡ₑ-preserve-cb CBp (∪trn p∪≡ₑr r∪≡ₑq)
  with ∥R∪sn≡ₑ-preserve-cb CBp p∪≡ₑr
... | _ , CBr = ∥R∪sn≡ₑ-preserve-cb CBr r∪≡ₑq

∥R∪sn≡ₑ-consistent : ∀{p q BV FV} →
  CorrectBinding p BV FV →
  p ∥R∪sn≡ₑ q →
  Σ[ r ∈ Term ] (p ∥R*∪sn⟶* r) × (q ∥R*∪sn⟶* r)
∥R∪sn≡ₑ-consistent CBp (∪stpsn psn⟶q)
  = _ ,  ∪sn⟶* (rstep psn⟶q rrefl) ∪refl  , ∪refl
∥R∪sn≡ₑ-consistent CBp (∪stp∥ ps∥Rq)
  = _ , ∪∥R* (∥Rn ps∥Rq ∥R0) ∪refl , ∪refl
∥R∪sn≡ₑ-consistent CBp (∪sym psn∪∥R≡ₑq CBq)
  with ∥R∪sn≡ₑ-consistent CBq psn∪∥R≡ₑq
... | _ , a , b
  = _ , b , a
∥R∪sn≡ₑ-consistent CBp ∪ref = _ , ∪refl , ∪refl
∥R∪sn≡ₑ-consistent{p}{q} CBp (∪trn{.p}{r}{.q} p≡r r≡q)
  with ∥R∪sn≡ₑ-preserve-cb CBp p≡r
... | ((BVr , FVr) , CBr)
  with ∥R∪sn≡ₑ-preserve-cb CBr r≡q
... | ((BVq , FVq) , CBq)
  with ∥R∪sn≡ₑ-consistent CBp p≡r
... | (y , p⟶y , r⟶y)
  with ∥R∪sn≡ₑ-consistent CBr r≡q
... | (z , r⟶z , q⟶z)
  with ∥R*∪sn⟶*-confluent CBr r⟶y r⟶z
... | (x , y⟶x , z⟶x)
  = x , ∥R*∪sn⟶*-concat p⟶y y⟶x , ∥R*∪sn⟶*-concat q⟶z z⟶x

inescapability-of-complete-∥R : ∀ {p q} ->
  complete p ->
  p ∥R q ->
  complete q
inescapability-of-complete-∥R
 = \ { completep (∥Rstep dc) -> thm completep dc } where

  thm-p : ∀ {p C p₁ p₂} ->
    paused p ->
    p ≐ C ⟦ p₁ ∥ p₂ ⟧c ->
    paused (C ⟦ p₂ ∥ p₁ ⟧c)
  thm-p ppause ()
  thm-p (pseq paused₁) (dcseq₁ pC) = pseq (thm-p paused₁ pC)
  thm-p (pseq paused₁) (dcseq₂ pC) = pseq paused₁
  thm-p (ploopˢ paused₁) (dcloopˢ₁ pC) = ploopˢ (thm-p paused₁ pC)
  thm-p (ploopˢ paused₁) (dcloopˢ₂ pC) = ploopˢ paused₁
  thm-p (ppar paused₁ paused₂) dchole = ppar paused₂ paused₁
  thm-p (ppar paused₁ paused₂) (dcpar₁ pC) = ppar (thm-p paused₁ pC) paused₂
  thm-p (ppar paused₁ paused₂) (dcpar₂ pC) = ppar paused₁ (thm-p paused₂ pC)
  thm-p (psuspend paused₁) (dcsuspend pC) = psuspend (thm-p paused₁ pC)
  thm-p (ptrap paused₁) (dctrap pC) = ptrap (thm-p paused₁ pC)

  thm-d : ∀ {p C p₁ p₂} ->
    done p ->
    p ≐ C ⟦ p₁ ∥ p₂ ⟧c ->
    done (C ⟦ p₂ ∥ p₁ ⟧c)
  thm-d (dhalted hnothin) ()
  thm-d (dhalted (hexit n)) ()
  thm-d (dpaused p/paused) pC
    = dpaused (thm-p p/paused pC)

  thm : ∀ {p C p₁ p₂} ->
    complete p ->
    p ≐ C ⟦ p₁ ∥ p₂ ⟧c ->
    complete (C ⟦ p₂ ∥ p₁ ⟧c)
  thm (codone x) pC = codone (thm-d x pC)
  thm (coenv x x₁) (dcenv pC) = coenv x (thm-d x₁ pC)

inescapability-of-complete-∥R* : ∀ {p q} ->
  complete p ->
  p ∥R* q ->
  complete q
inescapability-of-complete-∥R* = thm where
  thm : ∀ {p q} ->
    complete p ->
    p ∥R* q ->
    complete q
  thm completep ∥R0 = completep
  thm completep (∥Rn p∥Rr r⟶q)
    = thm (inescapability-of-complete-∥R completep p∥Rr) r⟶q

inescapability-of-complete-∪ : ∀ {p q} ->
  complete p ->
  p ∥R*∪sn⟶* q ->
  complete q
inescapability-of-complete-∪ = thm where
  thm : ∀ {p q} ->
   complete p ->
   p ∥R*∪sn⟶* q ->
   complete q
  thm completep (∪∥R* p∥R*r r⟶q)
   = thm (inescapability-of-complete-∥R* completep p∥R*r) r⟶q
  thm completep (∪sn⟶* psn⟶*r r⟶q)
   = thm (inescapability-of-complete-sn completep psn⟶*r) r⟶q
  thm completep ∪refl = completep

ρ-stays-ρ-∪ : ∀{θ p q A} →
  (ρ⟨ θ , A ⟩· p) ∥R*∪sn⟶* q →
  Σ[ θ' ∈ Env.Env ] Σ[ A' ∈ Ctrl ] Σ[ qin ∈ Term ] q ≡ (ρ⟨ θ' , A' ⟩· qin)
ρ-stays-ρ-∪ = thm where

  thm∥R : ∀{θ p q A} →
   (ρ⟨ θ , A ⟩· p) ∥R q →
   Σ[ θ' ∈ Env.Env ] Σ[ A ∈ Ctrl ] Σ[ qin ∈ Term ] q ≡ (ρ⟨ θ' , A ⟩· qin)
  thm∥R (∥Rstep (dcenv d≐C⟦p∥q⟧c))
   rewrite sym (unplugc d≐C⟦p∥q⟧c)
   = _ , _ , _ , refl

  thm∥R* : ∀{θ p q A} →
   (ρ⟨ θ , A ⟩· p) ∥R* q →
   Σ[ θ' ∈ Env.Env ] Σ[ A' ∈ Ctrl ] Σ[ qin ∈ Term ] q ≡ (ρ⟨ θ' , A' ⟩· qin)
  thm∥R* ∥R0 = _ , _ , _ , refl
  thm∥R* (∥Rn p∥Rq p⟶q)
    with thm∥R p∥Rq
  ... | (θ' , qin , A' , refl) = thm∥R* p⟶q

  thm : ∀{θ p q A} →
   (ρ⟨ θ , A ⟩· p) ∥R*∪sn⟶* q →
   Σ[ θ' ∈ Env.Env ] Σ[ A' ∈ Ctrl ] Σ[ qin ∈ Term ] q ≡ (ρ⟨ θ' , A' ⟩· qin)
  thm (∪∥R* p∥R*q p⟶q)
    with thm∥R* p∥R*q
  ... | (θ' , qin , A' , refl) = thm p⟶q
  thm (∪sn⟶* psn⟶*q p⟶q)
    with ρ-stays-ρ-sn⟶* psn⟶*q
  ... | (θ' , qin , A' , refl) = thm p⟶q
  thm ∪refl = _ , _ , _ , refl

irreducibility-of-halted-∥R : ∀ {p q} ->
  halted p ->
  p ∥R q ->
  ⊥
irreducibility-of-halted-∥R hnothin (∥Rstep ())
irreducibility-of-halted-∥R (hexit n) (∥Rstep ())

inescapability-of-paused-∥R : ∀ {p q} ->
  paused p ->
  p ∥R q ->
  paused q
inescapability-of-paused-∥R ppause (∥Rstep ())
inescapability-of-paused-∥R (pseq pausedp) (∥Rstep (dcseq₁ dc))
 = pseq (inescapability-of-paused-∥R pausedp (∥Rstep dc))
inescapability-of-paused-∥R (pseq pausedp) (∥Rstep (dcseq₂ dc))
 = pseq pausedp
inescapability-of-paused-∥R (ploopˢ pausedp) (∥Rstep (dcloopˢ₁ dc))
  = ploopˢ (inescapability-of-paused-∥R pausedp (∥Rstep dc))
inescapability-of-paused-∥R (ploopˢ pausedp) (∥Rstep (dcloopˢ₂ dc))
  = ploopˢ pausedp
inescapability-of-paused-∥R (ppar pausedp pausedq) (∥Rstep dchole)
  = ppar pausedq pausedp
inescapability-of-paused-∥R (ppar pausedp pausedq) (∥Rstep (dcpar₁ dc))
  = ppar (inescapability-of-paused-∥R pausedp (∥Rstep dc)) pausedq
inescapability-of-paused-∥R (ppar pausedp pausedq) (∥Rstep (dcpar₂ dc))
  = ppar pausedp (inescapability-of-paused-∥R pausedq (∥Rstep dc))
inescapability-of-paused-∥R (psuspend pausedp) (∥Rstep (dcsuspend dc))
  = psuspend (inescapability-of-paused-∥R pausedp (∥Rstep dc))
inescapability-of-paused-∥R (ptrap pausedp) (∥Rstep (dctrap dc))
  = ptrap (inescapability-of-paused-∥R pausedp (∥Rstep dc))

inescapability-of-paused-∥R* : ∀ {p q} ->
  paused p ->
  p ∥R* q ->
  paused q
inescapability-of-paused-∥R* pausedp ∥R0 = pausedp
inescapability-of-paused-∥R* pausedp (∥Rn p∥Rq p⟶q)
 = inescapability-of-paused-∥R* (inescapability-of-paused-∥R pausedp p∥Rq) p⟶q

equality-of-complete-∪ : ∀{θ θ' p q A A'} →
  complete (ρ⟨ θ , A ⟩·  p) →
  (ρ⟨ θ , A ⟩· p) ∥R*∪sn⟶* (ρ⟨ θ' , A' ⟩· q) →
  θ ≡ θ' × A ≡ A'
equality-of-complete-∪ = thm where

 done-not-to-ρ-∪ : ∀ {p θ q A} ->
    done p ->
    p ∥R*∪sn⟶* (ρ⟨ θ , A ⟩· q) ->
    ⊥
 done-not-to-ρ-∪ (dhalted p/halted) (∪∥R* ∥R0 p⟶q)
   = done-not-to-ρ-∪ (dhalted p/halted) p⟶q
 done-not-to-ρ-∪ (dhalted p/halted) (∪∥R* (∥Rn p∥Rq p∥R*q) p⟶q)
   = irreducibility-of-halted-∥R p/halted p∥Rq
 done-not-to-ρ-∪ (dpaused p/paused) (∪∥R* p∥R*q p⟶q)
   = done-not-to-ρ-∪ (dpaused (inescapability-of-paused-∥R* p/paused p∥R*q)) p⟶q
 done-not-to-ρ-∪ (dhalted p/halted) (∪sn⟶* rrefl r⟶q)
  = done-not-to-ρ-∪ (dhalted p/halted) r⟶q
 done-not-to-ρ-∪ (dhalted p/halted) (∪sn⟶* (rstep psn⟶q p⟶r) r⟶q)
  = irreducibility-of-halted-sn⟶ p/halted psn⟶q
 done-not-to-ρ-∪ (dpaused p/paused) (∪sn⟶* p⟶r r⟶q)
  = done-not-to-ρ-∪ (dpaused (inescapability-of-paused-sn⟶* p/paused p⟶r)) r⟶q
 done-not-to-ρ-∪ (dhalted ()) ∪refl
 done-not-to-ρ-∪ (dpaused ()) ∪refl

 ∥R*-lemma : ∀ {θ p q A} ->
   done p ->
   (ρ⟨ θ , A ⟩·  p) ∥R* q ->
   Σ[ q' ∈ Term ] q ≡ (ρ⟨ θ , A ⟩·  q') × done q'
 ∥R*-lemma done₁ ∥R0 = _ , refl , done₁
 ∥R*-lemma (dhalted hnothin) (∥Rn (∥Rstep (dcenv ())) p⟶q)
 ∥R*-lemma (dhalted (hexit n)) (∥Rn (∥Rstep (dcenv ())) p⟶q)
 ∥R*-lemma (dpaused p/paused) (∥Rn (∥Rstep (dcenv d≐C⟦p∥q⟧c)) p⟶q)
   with inescapability-of-paused-∥R p/paused (∥Rstep d≐C⟦p∥q⟧c)
 ... | q/paused = ∥R*-lemma (dpaused q/paused) p⟶q

 thm : ∀{θ θ' p q A A'} →
  complete (ρ⟨ θ , A ⟩·  p) →
  (ρ⟨ θ , A ⟩· p) ∥R*∪sn⟶* (ρ⟨ θ' , A' ⟩· q) →
  θ ≡ θ' × A ≡ A'
 thm (codone x) p⟶q =  ⊥-elim (done-not-to-ρ-∪ x p⟶q)
 thm (coenv complete-θθ donep) (∪∥R* p∥R*q p⟶q)
   with ∥R*-lemma donep p∥R*q
 ... | _ , refl , doneq' = thm (coenv complete-θθ doneq') p⟶q
 thm (coenv complete-θθ donep) (∪sn⟶* psn⟶*r r⟶q)
   with inescapability-of-complete-sn (coenv complete-θθ donep) psn⟶*r
 thm (coenv complete-θθ donep) (∪sn⟶* psn⟶*r r⟶q) | codone x
   = ⊥-elim (done-not-to-ρ-∪ x r⟶q)
 thm (coenv complete-θθ donep) (∪sn⟶* psn⟶*r r⟶q) | coenv x x₁
   with equality-of-complete-sn⟶* (coenv complete-θθ donep) psn⟶*r
 ... | refl , refl = thm (coenv x x₁) r⟶q
 thm (coenv complete-θθ donep) ∪refl = refl , refl

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-# OPTIONS --injective-type-constructors #-}
module InjectiveTypeConstructors where

data D (A : Set) : Set where

data _==_ (A : Set) : Set → Set where
  refl : A == A

injD : ∀ {A B} → D A == D B → A == B
injD refl = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Data.Fin.Subset where

open import Algebra
import Algebra.Properties.BooleanAlgebra as BoolAlgProp
import Algebra.Properties.BooleanAlgebra.Expression as BAExpr
import Data.Bool.Properties as BoolProp
open import Data.Fin
open import Data.List as List using (List)
open import Data.Nat
open import Data.Product
open import Data.Vec using (Vec; _∷_; _[_]=_)
import Relation.Binary.Vec.Pointwise as Pointwise
open import Relation.Nullary

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

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

-- Sides.

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

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

Subset : ℕ → Set
Subset = Vec Side

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

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

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

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

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

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

-- Pointwise lifting of the usual boolean algebra for booleans gives
-- us a boolean algebra for subsets.
--
-- The underlying equality of the returned boolean algebra is
-- propositional equality.

booleanAlgebra : ℕ → BooleanAlgebra _ _
booleanAlgebra n =
  BoolAlgProp.replace-equality
    (BAExpr.lift BoolProp.booleanAlgebra n)
    Pointwise.Pointwise-≡

private
  open module BA {n} = BooleanAlgebra (booleanAlgebra n) public
    using
      ( ⊥  -- The empty subset.
      ; ⊤  -- The subset containing all elements.
      )
    renaming
      ( _∨_ to _∪_  -- Binary union.
      ; _∧_ to _∩_  -- Binary intersection.
      ; ¬_  to ∁    -- Complement.
      )

-- A singleton subset, containing just the given element.

⁅_⁆ : ∀ {n} → Fin n → Subset n
⁅ zero  ⁆ = inside  ∷ ⊥
⁅ suc i ⁆ = outside ∷ ⁅ i ⁆

-- N-ary union.

⋃ : ∀ {n} → List (Subset n) → Subset n
⋃ = List.foldr _∪_ ⊥

-- N-ary intersection.

⋂ : ∀ {n} → List (Subset n) → Subset n
⋂ = List.foldr _∩_ ⊤

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

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

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

-- Point-wise lifting of properties.

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


text:
module Subst where

import Level

postulate Ty : Set

data Cxt : Set where
  ε   : Cxt
  _,_ : (Γ : Cxt) (A : Ty) → Cxt

_++_ : Cxt → Cxt → Cxt
Γ ++ ε       = Γ
Γ ++ (Δ , A) = (Γ ++ Δ) , A

data Tm : Cxt → Ty → Set where
  vz : ∀ {Γ A} → Tm (Γ , A) A
  other : ∀ {Γ A} → Tm Γ A

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

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

data Sub : Cxt → Cxt → Set where
  _∷_  : ∀ {Γ Δ A} → Tm Γ A → Sub Γ Δ → Sub Γ (Δ , A)
  lift : ∀ {Γ Δ} Ψ → Sub Γ Δ → Sub (Γ ++ Ψ) (Δ ++ Ψ)
  wk   : ∀ {Γ Δ} Ψ → Sub Γ Δ → Sub (Γ ++ Ψ) Δ
  id   : ∀ {Γ} → Sub Γ Γ
  ∅    : ∀ {Γ} → Sub Γ ε

assoc : ∀ {Γ Δ} Ψ → (Γ ++ (Δ ++ Ψ)) ≡ ((Γ ++ Δ) ++ Ψ)
assoc ε = refl
assoc {Γ}{Δ} (Ψ , A) rewrite assoc {Γ} {Δ} Ψ = refl

ε++ : ∀ Γ → (ε ++ Γ) ≡ Γ
ε++ ε = refl
ε++ (Γ , A) rewrite ε++ Γ = refl

postulate

  apply : ∀ {Γ Δ A} → Sub Γ Δ → Tm Δ A → Tm Γ A

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

cast : ∀ {Γ₁ Γ₂ Δ₁ Δ₂} → Γ₁ ≡ Γ₂ → Δ₁ ≡ Δ₂ → Sub Γ₁ Δ₁ → Sub Γ₂ Δ₂
cast refl refl ρ = ρ

inj : ∀ {Γ Δ A B} → (Γ , A) ≡ (Δ , B) → Γ ≡ Δ
inj refl = refl

injT : ∀ {Γ Δ A B} → (Γ , A) ≡ (Δ , B) → A ≡ B
injT refl = refl

drop : ∀ {Γ Δ ΔΨ} Ψ → Sub Γ ΔΨ → ΔΨ ≡ (Δ ++ Ψ) → Sub Γ Δ
drop Ψ id refl = wk Ψ id
drop Ψ (wk Δ ρ) refl = wk Δ (drop Ψ ρ refl)
drop Ψ (lift ε ρ) refl = drop Ψ ρ refl
drop ε ρ refl = ρ
drop (Ψ , A) (x ∷ ρ) refl = drop Ψ ρ refl
drop {Δ = Δ} (Ψ , A) (lift {Γ = Γ}{Δ = Σ} (Θ , A′) ρ) eq =
     wk (ε , A′) (drop Ψ (lift Θ ρ) (inj eq))
drop (Ψ , A) ∅ ()

wkS : ∀ {Γ Δ} Ψ → Sub Γ Δ → Sub (Γ ++ Ψ) Δ
wkS ε ρ = ρ
wkS Ψ (x ∷ ρ) = (apply (wk Ψ id) x) ∷ wkS Ψ ρ
wkS Ψ (lift Ψ₁ ρ) = wk Ψ (lift Ψ₁ ρ)
wkS Ψ (wk Ψ₁ ρ) = cast (assoc Ψ) refl (wkS (Ψ₁ ++ Ψ) ρ)
wkS Ψ id = wk Ψ id
wkS Ψ ∅ = ∅

liftS : ∀ {Γ Δ} Ψ → Sub Γ Δ → Sub (Γ ++ Ψ) (Δ ++ Ψ)
liftS Ψ (x ∷ ρ) = lift Ψ (x ∷ ρ)
liftS Ψ (lift Ψ₁ ρ) = cast (assoc Ψ) (assoc Ψ) (liftS (Ψ₁ ++ Ψ) ρ)
liftS Ψ (wk Ψ₁ ρ) = lift Ψ (wk Ψ₁ ρ)
liftS Ψ id = id
liftS Ψ ∅ = lift Ψ ∅

data _×_ A B : Set where
  _,_ : A → B → A × B

split : ∀ {Γ Δ ΔΨ} Ψ → Sub Γ ΔΨ → ΔΨ ≡ (Δ ++ Ψ) → Sub Γ Δ × Sub Γ Ψ
split {Γ} ε ρ refl = ρ , ∅
split (Ψ , A) (x ∷ ρ) refl with split Ψ ρ refl
... | σ , δ = σ , (x ∷ δ)
split Ψ (lift ε ρ) eq = split Ψ ρ eq
split (Ψ , A) (lift (Ψ₁ , A₁) ρ) eq with split Ψ (lift Ψ₁ ρ) (inj eq) | injT eq
split (Ψ , A) (lift (Ψ₁ , .A) ρ) eq | σ , δ | refl =
  wk (ε , A) σ , lift (ε , A) δ
split Ψ (wk Ψ₁ ρ) eq with split Ψ ρ eq
... | σ , δ = wk Ψ₁ σ , wk Ψ₁ δ
split {Δ = Δ} Ψ id refl = wk Ψ id , cast refl (ε++ Ψ) (lift {Γ = Δ} Ψ ∅)
split (Ψ , A) ∅ ()

_<>_ : ∀ {Γ Δ Ψ} → Sub Γ Ψ → Sub Γ Δ → Sub Γ (Δ ++ Ψ)
(x ∷ ρ) <> σ = x ∷ (ρ <> σ)
lift Ψ ρ <> σ = {!!}
wk Ψ₁ ρ <> σ = {!!}
-- _<>_ {Ψ = Ψ} id (_∷_ {Δ = Δ}{A = A} x σ) = cast refl (assoc {_}{ε , A} Ψ)
--   (_<>_ {Ψ = (ε , A) ++ Ψ} {!!} σ)
id <> lift Ψ σ = {!!}
id <> wk Ψ σ = {!!}
id <> id = {!!}
_<>_ {Ψ = Ψ} id ∅ = cast (ε++ Ψ) refl id
_<>_ {Ψ = ε} id σ = {!!}
_<>_ {Ψ = Ψ , A} id σ = vz ∷ (_<>_ {Ψ = Ψ} (wk (ε , A) id) σ)
∅ <> σ = σ

comp : ∀ {Γ Δ Δ′ Ψ} → Sub Γ Δ → Sub Δ′ Ψ → Δ ≡ Δ′ → Sub Γ Ψ
comp ρ id refl = ρ
comp ρ (wk Δ σ) refl = comp (drop Δ ρ refl) σ refl
comp ρ (x ∷ σ) refl = apply ρ x ∷ comp ρ σ refl
comp ρ (lift ε σ) refl = comp ρ σ refl
comp ρ (lift Ψ σ) refl with split Ψ ρ refl
... | ρ₁ , ρ₂ = ρ₂ <> comp ρ₁ σ refl
comp {Γ} ∅ σ refl = cast (ε++ Γ) refl (wk Γ σ)
-- comp (u ∷ ρ) (lift (Ψ , A) σ) eq
--   with injT eq
-- ... | refl = u ∷ comp ρ (lift Ψ σ) (inj eq)
-- comp ρ (lift (Ψ , A) σ) eq =
--   apply (cast refl eq ρ) vz ∷
--   comp ρ (wk (ε , A) (lift Ψ σ)) eq
comp ρ ∅ refl = ∅

_∘_ : ∀ {Γ Δ Ψ} → Sub Γ Δ → Sub Δ Ψ → Sub Γ Ψ
ρ ∘ σ = comp ρ σ refl

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda