text:
-----------------------------------------------------------------------
-- This file defines Degenerate Dial₂(Sets) and shows that it is a   --
-- CCC.                                                              --
-----------------------------------------------------------------------
module DeDial2Sets where

open import prelude

data UnitType : Set₁ where
  unit : UnitType
  mod : UnitType
  -- comp : UnitType → UnitType → UnitType

⟦_⟧ : UnitType → Set
⟦ unit ⟧ = ⊤
⟦ mod ⟧ = (⊤ *) × (⊤ *)
-- ⟦ comp t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

Obj⊤ : Set₁
Obj⊤ = Σ[ U ∈ Set ] (Σ[ X ∈ UnitType ](U → ⟦ X ⟧ → Set))

Hom⊤ : Obj⊤ → Obj⊤ → Set
Hom⊤ (U , X , α) (V , Y , β) =
  Σ[ f ∈ (U → V) ]
    (Σ[ F ∈  (⟦ Y ⟧ → ⟦ X ⟧) ] (∀{u : U}{y : ⟦ Y ⟧} → α u (F y) → β (f u) y))

comp⊤ : {A B C : Obj⊤} → Hom⊤ A B → Hom⊤ B C → Hom⊤ A C
comp⊤ {(U , X , α)} {(V , Y , β)} {(W , Z , γ)} (f , F , p₁) (g , G , p₂) =
  (g ∘ f , F ∘ G , (λ {u z} p-α → p₂ (p₁ p-α)))

infixl 5 _○⊤_

_○⊤_ = comp⊤

-- The contravariant hom-functor:
Hom⊤ₐ :  {A' A B B' : Obj⊤} → Hom⊤ A' A → Hom⊤ B B' → Hom⊤ A B → Hom⊤ A' B'
Hom⊤ₐ f h g = comp⊤ f (comp⊤ g h)

-- The identity function:
id⊤ : {A : Obj⊤} → Hom⊤ A A
id⊤ {(U , X , α)} = (id-set , id-set , id-set)

-- In this formalization we will only worry about proving that the
-- data of morphisms are equivalent, and not worry about the morphism
-- conditions.  This will make proofs shorter and faster.
--
-- If we have parallel morphisms (f,F) and (g,G) in which we know that
-- f = g and F = G, then the condition for (f,F) will imply the
-- condition of (g,G) and vice versa.  Thus, we can safly ignore it.
infix 4 _≡h⊤_

_≡h⊤_ : {A B : Obj⊤} → (f g : Hom⊤ A B) → Set
_≡h⊤_ {(U , X , α)}{(V , Y , β)} (f , F , p₁) (g , G , p₂) = f ≡ g × F ≡ G

≡h⊤-refl : {A B : Obj⊤}{f : Hom⊤ A B} → f ≡h⊤ f
≡h⊤-refl {U , X , α}{V , Y , β}{f , F , _} = refl , refl

≡h⊤-trans : ∀{A B}{f g h : Hom⊤ A B} → f ≡h⊤ g → g ≡h⊤ h → f ≡h⊤ h
≡h⊤-trans {U , X , α}{V , Y , β}{f , F , _}{g , G , _}{h , H , _} (p₁ , p₂) (p₃ , p₄) rewrite p₁ | p₂ | p₃ | p₄ = refl , refl

≡h⊤-sym : ∀{A B}{f g : Hom⊤ A B} → f ≡h⊤ g → g ≡h⊤ f
≡h⊤-sym {U , X , α}{V , Y , β}{f , F , _}{g , G , _} (p₁ , p₂) rewrite p₁ | p₂ = refl , refl

≡h⊤-subst-○ : ∀{A B C : Obj⊤}{f₁ f₂ : Hom⊤ A B}{g₁ g₂ : Hom⊤ B C}{j : Hom⊤ A C}
  → f₁ ≡h⊤ f₂
  → g₁ ≡h⊤ g₂
  → f₂ ○⊤ g₂ ≡h⊤ j
  → f₁ ○⊤ g₁ ≡h⊤ j
≡h⊤-subst-○ {U , X , α}
         {V , Y , β}
         {W , Z , γ}
         {f₁ , F₁ , _}
         {f₂ , F₂ , _}
         {g₁ , G₁ , _}
         {g₂ , G₂ , _}
         {j , J , _}
         (p₅ , p₆) (p₇ , p₈) (p₉ , p₁₀) rewrite p₅ | p₆ | p₇ | p₈ | p₉ | p₁₀ = refl , refl

○⊤-assoc : ∀{A B C D}{f : Hom⊤ A B}{g : Hom⊤ B C}{h : Hom⊤ C D}
  → f ○⊤ (g ○⊤ h) ≡h⊤ (f ○⊤ g) ○⊤ h
○⊤-assoc {U , X , α}{V , Y , β}{W , Z , γ}{S , T , ι}
        {f , F , _}{g , G , _}{h , H , _} = refl , refl

○⊤-idl : ∀{A B}{f : Hom⊤ A B} → id⊤ ○⊤ f ≡h⊤ f
○⊤-idl {U , X , _}{V , Y , _}{f , F , _} = refl , refl

○⊤-idr : ∀{A B}{f : Hom⊤ A B} → f ○⊤ id⊤ ≡h⊤ f
○⊤-idr {U , X , _}{V , Y , _}{f , F , _} = refl , refl

_⊗ᵣ_ : ∀{U V : Set}{X Y : UnitType} → (α : U → ⟦ X ⟧ → Set) → (β : V → ⟦ Y ⟧ → Set) → Σ U (λ x → V) → Σ ⟦ X ⟧ (λ x → ⟦ Y ⟧) → Set
(α ⊗ᵣ β) (u , v) (l₁ , l₂) = (α u l₁) × (β v l₂)

_⊗ₒ_ : (A B : Obj⊤) → Obj⊤
(U , unit , α) ⊗ₒ (V , unit , β) = (U × V) , unit , (λ p t → (α (fst p) triv) × (β (snd p) triv))
(U , unit , α) ⊗ₒ (V , mod , β) = (U × V) , (mod , (λ p t → (α (fst p) triv) × (β (snd p) t)))
(U , mod , α) ⊗ₒ (V , unit , β) = (U × V) , (mod , (λ p t → (α (fst p) t) × (β (snd p) triv)))
(U , mod , α) ⊗ₒ (V , mod , β) = (U × V) , (mod , (λ p t → (α (fst p) t) × (β (snd p) t)))

-- F⊗ : ∀{S Z W T V X U Y : Set ℓ}{f : U → W}{F : Z → X}{g : V → S}{G : T → Y} → (S → Z) × (W → T) → (V → X) × (U → Y)
-- F⊗ {f = f}{F}{g}{G} (h₁ , h₂) = (λ v → F(h₁ (g v))) , (λ u → G(h₂ (f u)))

-- _⊗ₐ_ : {A B C D : Obj} → Hom A C → Hom B D → Hom (A ⊗ₒ B) (C ⊗ₒ D)
-- _⊗ₐ_ {(U , X , α)}{(V , Y , β)}{(W , Z , γ)}{(S , T , δ)} (f , F , p₁) (g , G , p₂) = ⟨ f , g ⟩ , F⊗ {f = f}{F}{g}{G} , (λ {u y} → cond {u}{y})
--  where
--   cond : {u : Σ U (λ x → V)} {y : Σ (S → Z) (λ x → W → T)} →
--       ((α ⊗ᵣ β) u (F⊗ {f = f}{F}{g}{G} y)) ≤L ((γ ⊗ᵣ δ) (⟨ f , g ⟩ u) y)
--   cond {u , v}{h , j} = l-mul-funct {p = mproset l-pf} (p₁ {u}{h (g v)}) (p₂ {v}{j (f u)})

-- □ᵣ : {U : Set}{X : UnitType} → (U → ⟦ X ⟧ → Set) → U → 𝕃 ⟦ X ⟧ → Set
-- □ᵣ α u [] = ⊤
-- □ᵣ {U}{X} α u (x :: l) = (α u x) × (□ᵣ {U}{X} α u l)

-- □ₒ : Obj⊤ → Obj⊤
-- □ₒ (U , X , α) = U , seq X , □ᵣ {U}{X} α

-- □ₐ : {A B : Obj⊤} → Hom⊤ A B → Hom⊤ (□ₒ A) (□ₒ B)
-- □ₐ {U , n₁ , α}{V , n₂ , β} (f , F , p) = f , map F , {!!}

π₁ : {A B : Obj⊤} → Hom⊤ (A ⊗ₒ B) A
π₁ {U , unit , α} {V , unit , β} = fst , id-set , (λ {u y} → aux {u}{y})
 where
   aux : {u : Σ U (λ x → V)} {y : ⊤} → Σ (α (fst u) triv) (λ x → β (snd u) triv) → α (fst u) y
   aux {u , v}{triv} = fst

π₁ {U , mod , α} {V , unit , β} = fst , id-set , (λ {u y} → aux {u}{y})
 where
  aux : {u : Σ U (λ x → V)} {y : Σ (𝕃 ⊤) (λ x → 𝕃 ⊤)} → Σ (α (fst u) y) (λ x → β (snd u) triv) → α (fst u) y
  aux {u , v}{l₁ , l₂} = fst

π₁ {U , unit , α} {V , mod , β} = fst , (λ x → [ x ] , [ x ]) , (λ {u y} → aux {u}{y})
 where
   aux : {u : Σ U (λ x → V)} {y : ⊤} → Σ (α (fst u) triv) (λ x → β (snd u) (y :: [] , y :: [])) → α (fst u) y
   aux {u , v}{triv} = fst

π₁ {U , mod , α} {V , mod , β} = fst , id-set , (λ {u y} → aux {u}{y})
 where
   aux : {u : Σ U (λ x → V)} {y : Σ (𝕃 ⊤) (λ x → 𝕃 ⊤)} → Σ (α (fst u) y) (λ x → β (snd u) y) → α (fst u) y
   aux {u , v}{l} = fst

π₂ : {A B : Obj⊤} → Hom⊤ (A ⊗ₒ B) B
π₂ {U , unit , α} {V , unit , β} = snd , {!!} , {!!}
π₂ {U , mod , α} {V , unit , β} = snd , {!!} , {!!}
π₂ {U , unit , α} {V , mod , β} = snd , {!!} , {!!}
π₂ {U , mod , α} {V , mod , β} = snd , {!!} , {!!}

postulate rel-++ : ∀{W : Set}{w : W}{γ  : W → 𝕃 (⊤ {lzero}) → Set}{l₁ l₂ : 𝕃 ⊤} → γ w (l₁ ++ l₂) → ((γ w l₁) × (γ w l₂))

cart-ar : {A B C : Obj⊤}
  → (f : Hom⊤ C A)
  → (g : Hom⊤ C B)
  → Hom⊤ C (A ⊗ₒ B)
cart-ar {U , unit , α} {V , unit , β} {W , unit , γ} (f , F , p₁) (g , G , p₂) = trans-× f g , id-set , (λ {u y} → aux {u}{y})
 where
   aux : {u : W} {y : ⊤} → γ u y → Σ (α (f u) triv) (λ x → β (g u) triv)
   aux {w}{triv} p with p₁ {w}{triv} | p₂ {w}{triv}
   ... | p₃ | p₄ with F triv | G triv
   ... | triv | triv = p₃ p , p₄ p

cart-ar {U , unit , α} {V , unit , β} {W , mod , γ} (f , F , p₁) (g , G , p₂) = trans-× f g , (λ x → (fst (F x)) ++ (snd (F x)) , (fst (G x)) ++ (snd (G x))) , {!!}

cart-ar {U , unit , α} {V , mod , β} {W , unit , γ} (f , F , p₁) (g , G , p₂) = trans-× f g , {!!} , {!!}

cart-ar {U , unit , α} {V , mod , β} {W , mod , γ} (f , F , p₁) (g , G , p₂) = trans-× f g , {!!} , {!!}

cart-ar {U , mod , α} {V , unit , β} {W , unit , γ} (f , F , p₁) (g , G , p₂) = trans-× f g , {!!} , {!!}

cart-ar {U , mod , α} {V , unit , β} {W , mod , γ} (f , F , p₁) (g , G , p₂) = trans-× f g , {!!} , {!!}

cart-ar {U , mod , α} {V , mod , β} {W , unit , γ} (f , F , p₁) (g , G , p₂) = trans-× f g , {!!} , {!!}

cart-ar {U , mod , α} {V , mod , β} {W , mod , γ} (f , F , p₁) (g , G , p₂) = trans-× f g , {!!} , {!!}

cart-diag₁ : ∀{A B C : Obj⊤}
  → {f : Hom⊤ C A}
  → {g : Hom⊤ C B}
  → (cart-ar f g) ○⊤ π₁ ≡h⊤ f
cart-diag₁ {U , unit , α} {V , unit , β} {W , unit , γ} {f , F , p₁} {g , G , p₂} = refl , {!!}
cart-diag₁ {U , unit , α} {V , unit , β} {W , mod , γ} {f , F , p₁} {g , G , p₂} = refl , {!!}
cart-diag₁ {U , unit , α} {V , mod , β} {W , unit , γ} {f , F , p₁} {g , G , p₂} = {!!}
cart-diag₁ {U , unit , α} {V , mod , β} {W , mod , γ} {f , F , p₁} {g , G , p₂} = {!!}
cart-diag₁ {U , mod , α} {V , unit , β} {W , unit , γ} {f , F , p₁} {g , G , p₂} = {!!}
cart-diag₁ {U , mod , α} {V , unit , β} {W , mod , γ} {f , F , p₁} {g , G , p₂} = {!!}
cart-diag₁ {U , mod , α} {V , mod , β} {W , unit , γ} {f , F , p₁} {g , G , p₂} = {!!}
cart-diag₁ {U , mod , α} {V , mod , β} {W , mod , γ} {f , F , p₁} {g , G , p₂} = {!!}

-- cart-diag₂ : ∀{A B C : Obj⊤}
--   → {f : Hom (toObj C) (toObj A)}
--   → {g : Hom (toObj C) (toObj B)}
--   → (cart-ar f g) ○ π₂ ≡h g
-- cart-diag₂ {U , α}{V , β}{W , γ}{f , F , p₁}{g , G , p₂} = refl , ext-set ctr
--  where
--    ctr : {a : ⊤} → triv ≡ G a
--    ctr {triv} with G triv
--    ... | triv = refl

-- □ₒ-cond : ∀{U X : Set}
--   → (U → X → Set)
--   → U
--   → (X *)
--   → Set
-- □ₒ-cond {U} α u l = all-pred (α u) l

-- fromObj : (A : Obj) → Σ[ B ∈ Obj⊤ ]( A ≡ toObj(B)) → Obj⊤
-- fromObj _ ((a , b) , b₁) = a , b

-- □ₒ : Obj → Obj
-- □ₒ (U , X , α) = (U , X * , □ₒ-cond α)

-- □ₐ : {A B : Obj} → Hom A B → Hom (□ₒ A) (□ₒ B)
-- □ₐ {U , X , α}{V , Y , β} (f , F , p) = f , map F , cond
--  where
--   cond : {u : U} {y : 𝕃 Y} → all-pred (α u) (map F y) → all-pred (β (f u)) y
--   cond {y = []} x = triv
--   cond {y = x :: y} (a , b) = p a , cond b

-- □-ε : ∀{A : Obj} → Hom (□ₒ A) A
-- □-ε {U , X , α} = id-set , (λ x → [ x ] ) , aux
--  where
--   aux : {u : U} {y : X} → Σ (α u y) (λ x → ⊤) → α u y
--   aux (a , b) = a

-- □-δ : ∀{A : Obj} → Hom (□ₒ A) (□ₒ (□ₒ A))
-- □-δ {U , X , α} = id-set , (foldr _++_ []) , cond
--  where
--    cond : {u : U} {y : 𝕃 (𝕃 X)} → all-pred (α u) (foldr _++_ [] y) → all-pred (λ l → all-pred (α u) l) y
--    cond {y = []} p = triv
--    cond {u}{y = y :: y₁} p rewrite
--      (all-pred-append {X}{α u}{y}{foldr _++_ [] y₁} ∧-unit ∧-assoc)
--      with p
--    ... | p₁ , p₂ = p₁ , cond p₂

-- comonand-diag₁ : ∀{A : Obj}
--   → (□-δ {A}) ○ (□ₐ (□-δ {A})) ≡h (□-δ {A}) ○ (□-δ { □ₒ (A)})
-- comonand-diag₁ {U , X , α} = refl , ext-set (λ {a} → ctr {a})
--  where
--   ctr : {a : 𝕃 (𝕃 (𝕃 X))} → foldr _++_ [] (map (foldr _++_ []) a) ≡ foldr _++_ [] (foldr _++_ [] a)
--   ctr {[]} = refl
--   ctr {a :: a₁} rewrite sym (foldr-append {l₁ = a}{foldr _++_ [] a₁}) | ctr {a₁} = refl

-- comonand-diag₂ : ∀{A : Obj}
--   → (□-δ {A}) ○ (□-ε { □ₒ A}) ≡h (□-δ {A}) ○ (□ₐ (□-ε {A}))
-- comonand-diag₂ {U , X , α} = refl , ext-set (λ {a} → cond {a})
--  where
--    cond : {a : 𝕃 X} → a ++ [] ≡ foldr _++_ [] (map (λ x → x :: []) a)
--    cond {a} rewrite ++[] a = foldr-map

-- □-ctr : {U V : Set} → 𝕃 (Σ (V → ⊤) (λ x → U → ⊤)) → Σ (V → 𝕃 ⊤) (λ x → U → 𝕃 ⊤)
-- □-ctr [] = (λ x → [ triv ]) , (λ x → [ triv ])
-- □-ctr ((a , b) :: l) = (λ v → a v :: (fst (□-ctr l)) v) , (λ u → b u :: (snd (□-ctr l)) u)

-- □-m : {A B : Obj⊤} → Hom ((□ₒ (toObj A)) ⊗ₒ (□ₒ (toObj B))) (□ₒ ((toObj A) ⊗ₒ (toObj B)))
-- □-m {U , α}{V , β} = id-set , □-ctr , cond
--  where
--   cond : {u : Σ U (λ x → V)} {y : 𝕃 (Σ (V → ⊤) (λ x → U → ⊤))} →
--       ((λ u₁ l → all-pred (α u₁) l) ⊗ᵣ (λ u₁ l → all-pred (β u₁) l)) u
--       (□-ctr y) → all-pred ((α ⊗ᵣ β) u) y
--   cond {a , b} {[]} x = triv
--   cond {a , b} {(a₁ , b₁) :: y} ((a₂ , b₂) , a₃ , b₃) with cond {a , b}{y}
--   ... | IH with □-ctr y
--   ... | c , d = (a₂ , a₃) , IH (b₂ , b₃)

-- □-m-nat : ∀{A A' B B' : Obj⊤}
--   → (f : Hom (toObj A) (toObj A'))
--   → (g : Hom (toObj B) (toObj B'))
--   → ((□ₐ f) ⊗ₐ (□ₐ g)) ○ □-m ≡h □-m ○ (□ₐ (f ⊗ₐ g))
-- □-m-nat {U , α}{U' , α'}{V , β}{V' , β'} (f , F , p₁) (g , G , p₂) = refl , ext-set (λ {a} → aux {a})
--   where
--     aux : {a : 𝕃 (Σ (V' → ⊤) (λ x → U' → ⊤))} → F⊗ {V'}{𝕃 ⊤}{U'}{𝕃 ⊤}{V}{𝕃 ⊤}{U}{𝕃 ⊤}{f}{map F}{g}{map G} (□-ctr a) ≡ □-ctr (map (F⊗ {V'} {⊤} {U'} {⊤} {V} {⊤} {U} {⊤} {f} {F} {g} {G}) a)
--     aux {[]} with G triv | F triv
--     ... | triv | triv = refl
--     aux {(a , b) :: a₁} = eq-× (ext-set aux₁) (ext-set aux₄)
--      where
--        aux₂ : ∀{v}{l : 𝕃 (Σ (V' → ⊤) (λ x → U' → ⊤))} → map F (fst (□-ctr l) (g v)) ≡ fst (□-ctr (map (F⊗ {V'} {⊤} {U'} {⊤} {V} {⊤} {U} {⊤} {f} {F} {g} {G}) l)) v
--        aux₂ {_}{[]} with F triv
--        ... | triv = refl
--        aux₂ {v}{(a₂ , b₁) :: l} rewrite aux₂ {v}{l} = refl

--        aux₁ : {a₂ : V} → F (a (g a₂)) :: map F (fst (□-ctr a₁) (g a₂)) ≡ F (a (g a₂)) :: fst (□-ctr (map (F⊗ {V'} {⊤} {U'} {⊤} {V} {⊤} {U} {⊤} {f} {F} {g} {G}) a₁)) a₂
--        aux₁ {v} with F (a (g v))
--        ... | triv rewrite aux₂ {v}{a₁} = refl

--        aux₃ : ∀{u l} → map G (snd (□-ctr l) (f u)) ≡ snd (□-ctr (map (F⊗ {V'} {⊤} {U'} {⊤} {V} {⊤} {U} {⊤} {f} {F} {g} {G}) l)) u
--        aux₃ {u}{[]} with G triv
--        ... | triv = refl
--        aux₃ {u}{(a₂ , b₁) :: l} rewrite aux₃ {u}{l} = refl

--        aux₄ : {a₂ : U} → G (b (f a₂)) :: map G (snd (□-ctr a₁) (f a₂)) ≡ G (b (f a₂)) :: snd (□-ctr (map (F⊗ {V'} {⊤} {U'} {⊤} {V} {⊤} {U} {⊤} {f} {F} {g} {G}) a₁)) a₂
--        aux₄ {u} rewrite aux₃ {u}{a₁} = refl

-- □-m-I : Hom I (□ₒ I)
-- □-m-I = id-set , (λ _ → triv) , cond
--  where
--   cond : {u : ⊤} {y : 𝕃 ⊤} → ι u triv → all-pred (ι u) y
--   cond {triv} {[]} x = triv
--   cond {triv} {triv :: y} triv = triv , cond triv

-- π-□-ctr : {U V : Set} → 𝕃 ⊤ → Σ (V → 𝕃 ⊤) (λ _ → U → 𝕃 ⊤)
-- π-□-ctr [] = (λ x → [ triv ]) , (λ x → [ triv ])
-- π-□-ctr {U}{V} (triv :: l) = (λ v → triv :: fst (π-□-ctr {U}{V} l) v) , ((λ v → triv :: snd (π-□-ctr {U}{V} l) v))

-- π₁-□ : ∀{U α V β} → Hom ((□ₒ (U , ⊤ , α)) ⊗ₒ (□ₒ (V , ⊤ , β))) (□ₒ (U , ⊤ , α))
-- π₁-□ {U}{α}{V}{β} = fst , π-□-ctr , cond
--  where
--    cond : {u : Σ U (λ x → V)} {y : 𝕃 ⊤} →
--       ((λ u₁ l → all-pred (α u₁) l) ⊗ᵣ (λ u₁ l → all-pred (β u₁) l)) u
--       (π-□-ctr y) →
--       all-pred (α (fst u)) y
--    cond {a , b} {[]} x = triv
--    cond {a , b} {triv :: y} ((a₁ , b₁) , a₂ , b₂) with cond {a , b} {y}
--    ... | IH with π-□-ctr {U}{V} y
--    ... | c , d = a₁ , IH (b₁ , b₂)

-- □-prod₁ : ∀{U α V β} → _≡h_ {((□ₒ (U , ⊤ , α)) ⊗ₒ (□ₒ (V , ⊤ , β)))}
--                             {(□ₒ (U , ⊤ , α))}
--                             (_○_ {(□ₒ (U , ⊤ , α)) ⊗ₒ (□ₒ (V , ⊤ , β))}{□ₒ ((U , ⊤ , α) ⊗ₒ (V , ⊤ , β))}{□ₒ (U , ⊤ , α)} (□-m {U , α}{V , β}) (□ₐ {(U , ⊤ , α) ⊗ₒ (V , ⊤ , β)}{U , ⊤ , α} (π₁ {U , α}{V , β})))
--                             (π₁-□ {U}{α}{V}{β})
-- □-prod₁ {U}{α}{V}{β} = refl , ext-set (λ {a} → aux {a})
--  where
--   aux : {a : 𝕃 ⊤} → □-ctr {U}{V} (map π-ctr a) ≡ π-□-ctr a
--   aux {[]} = refl
--   aux {triv :: a} rewrite aux {a} = refl

-- π₂-□ : ∀{U α V β} → Hom ((□ₒ (U , ⊤ , α)) ⊗ₒ (□ₒ (V , ⊤ , β))) (□ₒ (V , ⊤ , β))
-- π₂-□ {U}{α}{V}{β} = snd , π-□-ctr , cond
--  where
--    cond : {u : Σ U (λ x → V)} {y : 𝕃 ⊤} →
--       ((λ u₁ l → all-pred (α u₁) l) ⊗ᵣ (λ u₁ l → all-pred (β u₁) l)) u
--       (π-□-ctr y) →
--       all-pred (β (snd u)) y
--    cond {a , b} {[]} x = triv
--    cond {a , b} {triv :: y} ((a₁ , b₁) , a₂ , b₂) with cond {a , b}{y}
--    ... | IH with π-□-ctr {U}{V} y
--    ... | c , d = a₂ , (IH (b₁ , b₂))

-- □-prod₂ : ∀{U α V β} → _≡h_ {((□ₒ (U , ⊤ , α)) ⊗ₒ (□ₒ (V , ⊤ , β)))}
--                             {(□ₒ (V , ⊤ , β))}
--                             (_○_ {(□ₒ (U , ⊤ , α)) ⊗ₒ (□ₒ (V , ⊤ , β))}{□ₒ ((U , ⊤ , α) ⊗ₒ (V , ⊤ , β))}{□ₒ (V , ⊤ , β)} (□-m {U , α}{V , β}) (□ₐ {(U , ⊤ , α) ⊗ₒ (V , ⊤ , β)}{V , ⊤ , β} (π₂ {U , α}{V , β})))
--                             (π₂-□ {U}{α}{V}{β})
-- □-prod₂ {U}{α}{V}{β} = refl , (ext-set (λ {a} → aux {a}))
--  where
--   aux : {a : 𝕃 ⊤} → □-ctr {U}{V} (map π-ctr a) ≡ π-□-ctr a
--   aux {[]} = refl
--   aux {triv :: a} rewrite aux {a} = refl

-- cart-ar-□ : {A B C : Obj⊤}
--   → (f : Hom (□ₒ (toObj C)) (□ₒ (toObj A)))
--   → (g : Hom (□ₒ (toObj C)) (□ₒ (toObj B)))
--   → Hom (□ₒ (toObj C)) ((□ₒ (toObj A)) ⊗ₒ (□ₒ (toObj B)))
-- cart-ar-□ {U , α}{V , β}{W , γ} (f , F , p₁) (g , G , p₂) = trans-× f g ,  {!!} , {!!}
--  where

-- -}

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import Categories.Category

module Categories.Functor.Hom.Properties.Contra {o ℓ e} (C : Category o ℓ e) where

private
  module C = Category C

open import Level
open import Function.Equality renaming (id to idFun)

open import Categories.Category.Instance.Setoids
open import Categories.Diagram.Limit
open import Categories.Diagram.Limit.Properties
open import Categories.Diagram.Colimit
open import Categories.Diagram.Duality
open import Categories.Functor
open import Categories.Functor.Hom
open import Categories.Functor.Hom.Properties.Covariant C.op
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.NaturalIsomorphism

private
  variable
    o′ ℓ′ e′ : Level
    J : Category o′ ℓ′ e′

open C
open Hom C

-- contravariant hom functor sends colimit of F to its limit.
module _ (W : Obj) {F : Functor J C} (col : Colimit F) where
  private
    module F = Functor F
    module J = Category J
    open HomReasoning

    HomF : Functor J.op (Setoids ℓ e)
    HomF = Hom[-, W ] ∘F F.op

  hom-colimit⇒limit : Limit HomF
  hom-colimit⇒limit = ≃-resp-lim (Hom≃ ⓘʳ F.op) (hom-resp-limit W (Colimit⇒coLimit _ col))
    where Hom≃ : Hom[ op ][ W ,-] ≃ Hom[-, W ]
          Hom≃ = record
            { F⇒G = ntHelper record
              { η       = λ _ → idFun
              ; commute = λ _ eq → C.∘-resp-≈ˡ (C.∘-resp-≈ʳ eq) ○ C.assoc
              }
            ; F⇐G = ntHelper record
              { η       = λ _ → idFun
              ; commute = λ _ eq → C.sym-assoc ○ C.∘-resp-≈ˡ (C.∘-resp-≈ʳ eq)
              }
            ; iso = λ _ → record
              { isoˡ = λ eq → eq
              ; isoʳ = λ eq → eq
              }
            }

ext: agda

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Type

module Graph.Walk.Functions.Proofs {ℓ₁ ℓ₂} {V : Type{ℓ₁}} where

import      Data.Either as Either
open import Data.Either.Proofs
open import Logic.Propositional
import      Lvl
open import Graph{ℓ₁}{ℓ₂}(V)
open import Graph.Properties
open import Graph.Walk{ℓ₁}{ℓ₂}{V}
open import Graph.Walk.Properties{ℓ₁}{ℓ₂}{V}
open import Graph.Walk.Functions{ℓ₁}{ℓ₂}{V}
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Relator.Properties
open import Syntax.Function
open import Type.Dependent
open import Type.Dependent.Functions

module _ (_⟶_ : Graph) where
  at-path-length : ∀{a} → length{_⟶_}(at{x = a}) ≡ 0
  at-path-length = reflexivity(_≡_)

  edge-path-length : ∀{a b}{e : a ⟶ b} → length{_⟶_}(edge e) ≡ 1
  edge-path-length = reflexivity(_≡_)

  join-path-length : ∀{a b c}{e₁ : a ⟶ b}{e₂ : b ⟶ c} → length{_⟶_}(join e₁ e₂) ≡ 2
  join-path-length = reflexivity(_≡_)

  prepend-path-length : ∀{a b c}{e : a ⟶ b}{w : Walk(_⟶_) b c} → length(prepend e w) ≡ 𝐒(length w)
  prepend-path-length {w = at}          = reflexivity(_≡_)
  prepend-path-length {w = prepend e w} = [≡]-with(𝐒) (prepend-path-length{e = e}{w = w})

  [++]-identityᵣ : ∀{a b}{w : Walk(_⟶_) a b} → (w ++ at ≡ w)
  [++]-identityᵣ {w = at}          = reflexivity(_≡_)
  [++]-identityᵣ {w = prepend x w} = [≡]-with(prepend x) ([++]-identityᵣ {w = w})
  {-# REWRITE [++]-identityᵣ #-}

  [++]-path-length : ∀{a b c}{w₁ : Walk(_⟶_) a b}{w₂ : Walk(_⟶_) b c} → length(w₁ ++ w₂) ≡ length w₁ + length w₂
  [++]-path-length {a} {.a} {.a} {at}            {at}          = reflexivity(_≡_)
  [++]-path-length {a} {.a} {c}  {at}            {prepend e w} = prepend-path-length {e = e}{w = w}
  [++]-path-length {a} {b}  {c}  {prepend e₁ w₁} {w₂}          = [≡]-with(𝐒) ([++]-path-length {w₁ = w₁}{w₂ = w₂})
  {-# REWRITE [++]-path-length #-}

  at-visits : ∀{v} → Visits(_⟶_) v (at{x = v})
  at-visits = current

  edge-visits-left : ∀{a b}{e : a ⟶ b} → Visits(_⟶_) a (edge e)
  edge-visits-left = current

  edge-visits-right : ∀{a b}{e : a ⟶ b} → Visits(_⟶_) b (edge e)
  edge-visits-right = skip current

  join-visits-1 : ∀{a b c}{e₁ : a ⟶ b}{e₂ : b ⟶ c} → Visits(_⟶_) a (join e₁ e₂)
  join-visits-1 = current

  join-visits-2 : ∀{a b c}{e₁ : a ⟶ b}{e₂ : b ⟶ c} → Visits(_⟶_) b (join e₁ e₂)
  join-visits-2 = skip current

  join-visits-3 : ∀{a b c}{e₁ : a ⟶ b}{e₂ : b ⟶ c} → Visits(_⟶_) c (join e₁ e₂)
  join-visits-3 = skip (skip current)

  prepend-visitsᵣ-left : ∀{a b c}{e : a ⟶ b}{w : Walk(_⟶_) b c} → Visits(_⟶_) a (prepend e w)
  prepend-visitsᵣ-left = current

  prepend-visitsᵣ-right : ∀{v b c}{w : Walk(_⟶_) b c} → Visits(_⟶_) v w → ∀{a}{e : a ⟶ b} → Visits(_⟶_) v (prepend e w)
  prepend-visitsᵣ-right p = skip p

  prepend-visitsₗ : ∀{v a b c}{e : a ⟶ b}{w : Walk(_⟶_) b c} → Visits(_⟶_) v (prepend e w) → ((v ≡ a) ∨ Visits(_⟶_) v w)
  prepend-visitsₗ current  = [∨]-introₗ(reflexivity(_≡_))
  prepend-visitsₗ (skip p) = [∨]-introᵣ p

  [++]-visitsᵣ : ∀{v a b c}{w₁ : Walk(_⟶_) a b}{w₂ : Walk(_⟶_) b c} → (Visits(_⟶_) v w₁) ∨ (Visits(_⟶_) v w₂) → Visits(_⟶_) v (w₁ ++ w₂)
  [++]-visitsᵣ ([∨]-introₗ current) = current
  [++]-visitsᵣ {w₂ = w₂} ([∨]-introₗ (skip {rest = rest} p)) = skip ([++]-visitsᵣ {w₁ = rest}{w₂ = w₂} ([∨]-introₗ p))
  [++]-visitsᵣ {w₁ = at} ([∨]-introᵣ p) = p
  [++]-visitsᵣ {w₁ = prepend x w₁} {w₂ = w₂} ([∨]-introᵣ p) = skip ([++]-visitsᵣ {w₁ = w₁}{w₂ = w₂} ([∨]-introᵣ p))

  [++]-visitsₗ : ∀{v a b c}{w₁ : Walk(_⟶_) a b}{w₂ : Walk(_⟶_) b c} → (Visits(_⟶_) v w₁) ∨ (Visits(_⟶_) v w₂) ← Visits(_⟶_) v (w₁ ++ w₂)
  [++]-visitsₗ {v} {a} {.a} {.a} {at}           {at}            p = [∨]-introₗ p
  [++]-visitsₗ {v} {a} {.a} {c}  {at}           {prepend x w₂}  p = [∨]-introᵣ p
  [++]-visitsₗ {v} {a} {b}  {c}  {prepend e w₁} {w₂}            p with prepend-visitsₗ p
  [++]-visitsₗ {v} {a} {b}  {c}  {prepend e w₁} {w₂}            p | [∨]-introₗ eq = [∨]-introₗ ([≡]-substitutionₗ eq (Visits.current {path = prepend e w₁}))
  [++]-visitsₗ {v} {a} {b}  {c}  {prepend e w₁} {w₂}            _ | [∨]-introᵣ p  = Either.mapLeft skip ([++]-visitsₗ {w₁ = w₁} {w₂ = w₂} p)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module BadTermination where

data N : Set where
  zero : N
  suc  : N -> N

postulate inf : N

data D : N -> Set where
  d₁ : D (suc inf)
  d₂ : D inf

f : (n : N) -> D n -> N
f .inf       d₂ = zero
f .(suc inf) d₁ = f inf d₂

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
{-# OPTIONS --cumulativity #-}

postulate
  F : (X : Set) → X → Set
  X : Set₁
  a : X
  shouldfail : F _ a

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import M-types.Base

module M-types.Coalg.Core (A : Ty ℓ) (B : A → Ty ℓ) where
    P : Ty ℓ → Ty ℓ
    P X = ∑[ a ∈ A ] (B a → X)

    P-Fun : {X Y : Ty ℓ} →
        (X → Y) → (P X → P Y)
    P-Fun f = λ (a , d) → (a , f ∘ d)

    P-SpanRel : {X : Ty ℓ} →
        SpanRel X → SpanRel (P X)
    P-SpanRel {X} ∼ = (P (ty ∼) , P-Fun (ρ₀ ∼) , P-Fun (ρ₁ ∼))

    P-SpanRelMor : {X : Ty ℓ} {∼ ≈ : SpanRel X} →
        SpanRelMor ∼ ≈ → SpanRelMor (P-SpanRel ∼) (P-SpanRel ≈)
    P-SpanRelMor {X} {∼} {≈} f =
        (
            P-Fun (fun f) ,
            ap P-Fun (com₀ f) ,
            ap P-Fun (com₁ f)
        )

    P-DepRel : {X : Ty ℓ} →
        DepRel X → DepRel (P X)
    P-DepRel {X} ∼ = λ (a₀ , d₀) → λ (a₁ , d₁) →
        ∑[ p ∈ a₀ ≡ a₁ ] ∏[ b₀ ∈ B a₀ ]
        d₀ b₀ [ ∼ ] d₁ (tra B p b₀)

    P-DepRelMor : {X : Ty ℓ} {∼ ≈ : DepRel X} →
        DepRelMor ∼ ≈ → DepRelMor (P-DepRel ∼) (P-DepRel ≈)
    P-DepRelMor {X} {∼} {≈} f = λ (a₀ , d₀) → λ (a₁ , d₁) → λ (p , e) → (
            p ,
            λ b₀ → f (d₀ b₀) (d₁ (tra B p b₀)) (e b₀)
        )

    Coalg : Ty (ℓ-suc ℓ)
    Coalg = ∑[ ty ∈ Ty ℓ ] (ty → P ty)

    obs = pr₁

    P-Coalg : Coalg → Coalg
    P-Coalg X = (P (ty X) , P-Fun (obs X))

    CoalgMor :  Coalg → Coalg → Ty ℓ
    CoalgMor X Y =
        ∑[ fun ∈ (ty X → ty Y) ]
        obs Y ∘ fun ≡ P-Fun fun ∘ obs X

    com = pr₁

    P-CoalgMor : {X Y : Coalg} →
        CoalgMor X Y → CoalgMor (P-Coalg X) (P-Coalg Y)
    P-CoalgMor {X} {Y} f =
        (
            P-Fun (fun f) ,
            ap P-Fun (com f)
        )

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
module Examples.Main where
import Examples.PingPong as PingPong
import Examples.InfiniteBind as InfiniteBind
import Examples.TestSelectiveReceive as SelectiveReceive
import Examples.TestCall as Call
open import Runtime
open import SimulationEnvironment
open import ActorMonad
import IO
open ∞ActorM

pingpongEntry = singleton-env (PingPong.spawner .force)
infinitebindEntry = singleton-env (InfiniteBind.binder .force)
selectiveReceiveEntry = singleton-env SelectiveReceive.spawner
callEntry = singleton-env (Call.calltestActor .force)

main = IO.run (run-env pingpongEntry)

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax GroupAction | GA

type
  * : 0-ary
  X : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20
  neg  : *  ->  * | ⊖_ r40
  act  : *  X  ->  X | _⊙_ r30

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊖N⊕ᴸ) a |> add (neg (a), a) = unit
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = unit
  (εU⊙)      x : X |> act (unit,      x) = x
  (⊕A⊙) g h  x : X |> act (add(g, h), x) = act (g, act(h, x))
-}

module GroupAction.Signature where

open import SOAS.Context

-- Type declaration
data GAT : Set where
  * : GAT
  X : GAT

open import SOAS.Syntax.Signature GAT public
open import SOAS.Syntax.Build GAT public

-- Operator symbols
data GAₒ : Set where
  unitₒ addₒ negₒ actₒ : GAₒ

-- Term signature
GA:Sig : Signature GAₒ
GA:Sig = sig λ
  {  unitₒ  → ⟼₀ *
  ;  addₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  negₒ   → (⊢₀ *) ⟼₁ *
  ;  actₒ   → (⊢₀ *) , (⊢₀ X) ⟼₂ X
  }

open Signature GA:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Typechecker where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

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

_+_ : Nat -> Nat -> Nat
zero   + m = m
suc n  + m = suc (n + m)

data Fin : Nat -> Set where
  f0 : {n : Nat} -> Fin (suc n)
  fs : {n : Nat} -> Fin n -> Fin (suc n)

infixl 30 _::_ _++_

data Vect (A : Set) : Nat -> Set where
  ε    : Vect A zero
  _::_ : {n : Nat} -> Vect A n -> A -> Vect A (suc n)

fs^ : {n : Nat}(m : Nat) -> Fin n -> Fin (m + n)
fs^ zero    i = i
fs^ (suc m) i = fs (fs^ m i)

_++_ : {A : Set}{n m : Nat} -> Vect A n -> Vect A m -> Vect A (m + n)
xs ++ ε         = xs
xs ++ (ys :: y) = (xs ++ ys) :: y

data Chop {A : Set} : {n : Nat} -> Vect A n -> Fin n -> Set where
  chopGlue : {m n : Nat}(xs : Vect A n)(x : A)(ys : Vect A m) ->
             Chop (xs :: x ++ ys) (fs^ m f0)

chop : {A : Set}{n : Nat}(xs : Vect A n)(i : Fin n) -> Chop xs i
chop ε         ()
chop (xs :: x) f0 = chopGlue xs x ε
chop (xs :: y) (fs i) with chop xs i
chop (.(xs :: x ++ ys) :: y) (fs .(fs^ m f0))
  | chopGlue {m} xs x ys = chopGlue xs x (ys :: y)

infixr 40 _⊃_

data Simp : Set where
  o   : Simp
  _⊃_ : Simp -> Simp -> Simp

infix 20 Simp-_

data Simp-_ : Simp -> Set where
  neqo : Simp -> Simp -> Simp- o
  neq⊃ : {S T : Simp} -> Simp- (S ⊃ T)
  neqT : {S T : Simp}(T' : Simp- T) -> Simp- (S ⊃ T)
  neqS : {S : Simp}{T₁ : Simp}(S' : Simp- S)(T₂ : Simp) -> Simp- (S ⊃ T₁)

infixl 60 _∖_

_∖_ : (S : Simp) -> Simp- S -> Simp
.o       ∖ neqo S T        = S ⊃ T
.(_ ⊃ _) ∖ neq⊃            = o
.(S ⊃ T) ∖ neqT {S}{T}  T' = S ⊃ T ∖ T'
.(S ⊃ _) ∖ neqS {S} S' T₂  = S ∖ S' ⊃ T₂

data SimpEq? (S : Simp) : Simp -> Set where
  simpSame : SimpEq? S S
  simpDiff : (T : Simp- S) -> SimpEq? S (S ∖ T)

simpEq? : (S T : Simp) -> SimpEq? S T
simpEq? o o = simpSame
simpEq? o (S ⊃ T) = simpDiff (neqo S T)
simpEq? (S ⊃ T) o = simpDiff neq⊃
simpEq? (S₁ ⊃ T₁) (S₂ ⊃ T₂) with simpEq? S₁ S₂
simpEq? (S ⊃ T₁)  (.S ⊃ T₂)        | simpSame with simpEq? T₁ T₂
simpEq? (S ⊃ T)   (.S ⊃ .T)        | simpSame | simpSame    = simpSame
simpEq? (S ⊃ T)   (.S ⊃ .(T ∖ T')) | simpSame | simpDiff T' = simpDiff (neqT T')
simpEq? (S ⊃ T₁)  (.(S ∖ S') ⊃ T₂) | simpDiff S' = simpDiff (neqS S' T₂)

data Term : Nat -> Set where
  var : {n : Nat} -> Fin n -> Term n
  app : {n : Nat} -> Term n -> Term n -> Term n
  lam : {n : Nat} -> Simp -> Term (suc n) -> Term n

data Good : {n : Nat} -> Vect Simp n -> Simp -> Set where
  gVar : {n m : Nat}(Γ : Vect Simp n)(T : Simp)(Δ : Vect Simp m) ->
         Good (Γ :: T ++ Δ) T
  gApp : {n : Nat}{Γ : Vect Simp n}{S T : Simp} ->
         Good Γ (S ⊃ T) -> Good Γ S -> Good Γ T
  gLam : {n : Nat}{Γ : Vect Simp n}(S : Simp){T : Simp} ->
         Good (Γ :: S) T -> Good Γ (S ⊃ T)

g : {n : Nat}{Γ : Vect Simp n}(T : Simp) -> Good Γ T -> Term n
g T        (gVar{n}{m} Γ .T Δ) = var (fs^ m f0)
g T        (gApp f s)          = app (g _ f) (g _ s)
g .(S ⊃ _) (gLam S t)          = lam S (g _ t)

data Bad {n : Nat}(Γ : Vect Simp n) : Set where
  bNonFun   : Good Γ o -> Term n -> Bad Γ
  bMismatch : {S T : Simp}(S' : Simp- S) ->
              Good Γ (S ⊃ T) -> Good Γ (S ∖ S') -> Bad Γ
  bArg      : {S T : Simp} -> Good Γ (S ⊃ T) -> Bad Γ -> Bad Γ
  bFun      : Bad Γ -> Term n -> Bad Γ
  bLam      : (S : Simp) -> Bad (Γ :: S) -> Bad Γ

b : {n : Nat}{Γ : Vect Simp n} -> Bad Γ -> Term n
b (bNonFun f s)     = app (g o f) s
b (bMismatch _ f s) = app (g _ f) (g _ s)
b (bArg f s)        = app (g _ f) (b s)
b (bFun f s)        = app (b f) s
b (bLam S t)        = lam S (b t)

data TypeCheck? {n : Nat}(Γ : Vect Simp n) : Term n -> Set where
  good : (T : Simp)(t : Good Γ T) -> TypeCheck? Γ (g T t)
  bad  : (t : Bad Γ) -> TypeCheck? Γ (b t)

typeCheck? : {n : Nat}(Γ : Vect Simp n)(t : Term n) -> TypeCheck? Γ t
typeCheck? Γ (var i)   with chop Γ i
typeCheck? .(Γ :: T ++ Δ) (var ._) | chopGlue Γ T Δ = good T (gVar Γ T Δ)

typeCheck? Γ (app f s) with typeCheck? Γ f
typeCheck? Γ (app .(g (S ⊃ T) f) s) | good (S ⊃ T) f with typeCheck? Γ s
typeCheck? Γ (app .(g (S ⊃ T) f) .(g S' s))
             | good (S ⊃ T) f | good S' s with simpEq? S S'
typeCheck? Γ (app .(g (S ⊃ T) f) .(g S s))
             | good (S ⊃ T) f | good .S s        | simpSame    = good T (gApp f s)
typeCheck? Γ (app .(g (S ⊃ T) f) .(g (S ∖ S') s))
             | good (S ⊃ T) f | good .(S ∖ S') s | simpDiff S' = bad (bMismatch S' f s)
typeCheck? Γ (app .(g (S ⊃ T) f) .(b s))
             | good (S ⊃ T) f | bad s     = bad (bArg f s)
typeCheck? Γ (app .(g o f) s)       | good o f       = bad (bNonFun f s)
typeCheck? Γ (app .(b f) s)         | bad f          = bad (bFun f s)

typeCheck? Γ (lam S t) with typeCheck? (Γ :: S) t
typeCheck? Γ (lam S .(g T t)) | good T t = good (S ⊃ T) (gLam S t)
typeCheck? Γ (lam S .(b t))   | bad t    = bad (bLam S t)

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

open import Base

module Homotopy.VanKampen.Guide where

open import Homotopy.Truncation
open import Homotopy.Connected

record legend i (city : Set i) : Set (suc i) where
  constructor leg_,_,_
  field
    name : Set i
    loc : name → city
    all-listed : ∀ c → [ hfiber loc c ]

id-legend : ∀ {i} (A : Set i) → legend i A
id-legend A = leg A , id A , λ x → proj $ x , refl

private
  module Book {i} {city : Set i} {l : legend i city} where
    open legend l

    private
      data #guide : Set i where
        #point : name → #guide

    guide : Set i
    guide = #guide

    point : name → guide
    point = #point

    postulate  -- HIT
      route : ∀ n₁ n₂ → loc n₁ ≡ loc n₂ → point n₁ ≡ point n₂

    guide-rec : ∀ {l} (P : guide → Set l)
      (point* : (n : name) → P (point n))
      (route* : ∀ n₁ n₂ (p : loc n₁ ≡ loc n₂)
        → transport P (route n₁ n₂ p) (point* n₁) ≡ point* n₂)
      → (x : guide) → P x
    guide-rec P point* route* (#point n) = point* n

    postulate  -- HIT
      guide-β-route : ∀ {l} (P : guide → Set l)
        (point* : (n : name) → P (point n))
        (route* : ∀ n₁ n₂ (p : loc n₁ ≡ loc n₂)
          → transport P (route n₁ n₂ p) (point* n₁) ≡ point* n₂)
        n₁ n₂ (p : loc n₁ ≡ loc n₂)
        → apd (guide-rec {l} P point* route*) (route n₁ n₂ p)
        ≡ route* n₁ n₂ p

    guide-rec-nondep : ∀ {l} (P : Set l) (point* : name → P)
      (route* : ∀ n₁ n₂ → loc n₁ ≡ loc n₂ → point* n₁ ≡ point* n₂)
      → (guide → P)
    guide-rec-nondep P point* route* (#point n) = point* n

    postulate  -- HIT
      guide-β-route-nondep : ∀ {l} (P : Set l) (point* : name → P)
        (route* : ∀ n₁ n₂ → loc n₁ ≡ loc n₂ → point* n₁ ≡ point* n₂)
        n₁ n₂ (p : loc n₁ ≡ loc n₂)
        → ap (guide-rec-nondep P point* route*) (route n₁ n₂ p)
        ≡ route* n₁ n₂ p

open Book public hiding (guide)

module _ {i} {city : Set i} (l : legend i city) where
  open legend l

  guide : Set i
  guide = Book.guide {i} {city} {l}

  visit : guide → city
  visit = guide-rec-nondep city loc (λ _ _ p → p)

  visit-β-route : ∀ n₁ n₂ (p : loc n₁ ≡ loc n₂) → ap visit (route n₁ n₂ p) ≡ p
  visit-β-route = guide-β-route-nondep city loc (λ _ _ p → p)

  private
    drawn-as-one : ∀ c → is-contr (π₀ $ hfiber visit c)
    drawn-as-one c = []-extend-nondep
      ⦃ is-connected-is-prop ⟨0⟩ ⦄
      ( λ {(n₁ , p₁) → proj (point n₁ , p₁) , π₀-extend
        ⦃ λ _ → ≡-is-set $ π₀-is-set $ hfiber visit c ⦄
        ( uncurry $ guide-rec
          (λ x → ∀ p₂ → proj (x , p₂) ≡ proj (point n₁ , p₁))
          (λ n₂ p₂ → ap proj let p₃ = p₂ ∘ ! p₁ in
            Σ-eq (route n₂ n₁ p₃) $
              transport (λ x → visit x ≡ c) (route n₂ n₁ p₃) p₂
                ≡⟨ trans-app≡cst visit c (route n₂ n₁ p₃) p₂ ⟩
              ! (ap visit (route n₂ n₁ p₃)) ∘ p₂
                ≡⟨ ap (λ x → ! x ∘ p₂) $ visit-β-route n₂ n₁ p₃ ⟩
              ! (p₂ ∘ ! p₁) ∘ p₂
                ≡⟨ ap (λ x → x ∘ p₂) $ opposite-concat p₂ (! p₁) ⟩
              (! (! p₁) ∘ ! p₂) ∘ p₂
                ≡⟨ concat-assoc (! (! p₁)) (! p₂) p₂ ⟩
              ! (! p₁) ∘ (! p₂ ∘ p₂)
                ≡⟨ ap (λ x → ! (! p₁) ∘ x) $ opposite-left-inverse p₂ ⟩
              ! (! p₁) ∘ refl
                ≡⟨ refl-right-unit $ ! (! p₁) ⟩
              ! (! p₁)
                ≡⟨ opposite-opposite p₁ ⟩∎
              p₁
                ∎)
          (λ _ _ _ → funext λ _ → prop-has-all-paths (π₀-is-set _ _ _) _ _))})
      (all-listed c)

  private
    visit-fiber-rec′ : ∀ {j} (P : city → Set j)
      (h₀-point : ∀ n → P (loc n))
      (h₁-route : ∀ n₁ n₂ r → transport P r (h₀-point n₁) ≡ h₀-point n₂)
      → (∀ c → hfiber visit c → P c)
    visit-fiber-rec′ P h₀-p h₁-r c (pt , p₁) =
      transport P p₁ $ guide-rec (P ◯ visit) h₀-p
        (λ n₁ n₂ r →
            transport (P ◯ visit) (route n₁ n₂ r) (h₀-p n₁)
              ≡⟨ ! $ trans-ap P visit (route n₁ n₂ r) $ h₀-p n₁ ⟩
            transport P (ap visit $ route n₁ n₂ r) (h₀-p n₁)
              ≡⟨ ap (λ x → transport P x $ h₀-p n₁) $ visit-β-route n₁ n₂ r ⟩
            transport P r (h₀-p n₁)
              ≡⟨ h₁-r n₁ n₂ r ⟩∎
            h₀-p n₂
              ∎) pt

  visit-fiber-rec : ∀ {j} (P : city → Set j)
    ⦃ _ : ∀ (c : city) → is-set $ P c ⦄
    (h₀-point : ∀ n → P (loc n))
    (h₁-route : ∀ n₁ n₂ r → transport P r (h₀-point n₁) ≡ h₀-point n₂)
    → (∀ c → P c)
  visit-fiber-rec P ⦃ P-is-set ⦄ h₀-p h₁-r c =
    π₀-extend-nondep ⦃ P-is-set c ⦄
    (visit-fiber-rec′ P h₀-p h₁-r c)
    (π₁ $ drawn-as-one c)

  visit-fiber-β-loc : ∀ {j} (P : city → Set j)
    ⦃ P-is-set : ∀ (c : city) → is-set $ P c ⦄
    (h₀-p : ∀ n → P (loc n))
    (h₁-r : ∀ n₁ n₂ r → transport P r (h₀-p n₁) ≡ h₀-p n₂)
    → ∀ n → visit-fiber-rec P ⦃ P-is-set ⦄ h₀-p h₁-r (loc n) ≡ h₀-p n
  visit-fiber-β-loc P ⦃ P-is-set ⦄ h₀-p h₁-r n =
    visit-fiber-rec P ⦃ P-is-set ⦄ h₀-p h₁-r (loc n)
      ≡⟨ ap (π₀-extend-nondep ⦃ P-is-set $ loc n ⦄ (visit-fiber-rec′ P h₀-p h₁-r $ loc n))
            $ ! $ π₂ (drawn-as-one $ loc n) (proj $ point n , refl) ⟩∎
    h₀-p n
      ∎

  private
    loc-fiber-rec′ : ∀ {j} (P : city → Set j)
      (h₀-point : ∀ n → P (loc n))
      → (∀ c → hfiber loc c → P c)
    loc-fiber-rec′ P h₀-p c (n , p) = transport P p (h₀-p n)

  loc-fiber-rec : ∀ {j} (P : city → Set j)
    ⦃ _ : ∀ c → is-prop $ P c ⦄
    (h₀-point : ∀ n → P (loc n))
    → (∀ c → P c)
  loc-fiber-rec P ⦃ P-is-prop ⦄ h₀-p c = []-extend-nondep ⦃ P-is-prop c ⦄
    (loc-fiber-rec′ P h₀-p c) (all-listed c)

  loc-fiber-β-loc : ∀ {j} (P : city → Set j)
    ⦃ P-is-prop : ∀ (c : city) → is-prop $ P c ⦄
    (h₀-p : ∀ n → P (loc n))
    → ∀ n → loc-fiber-rec P ⦃ P-is-prop ⦄ h₀-p (loc n) ≡ h₀-p n
  loc-fiber-β-loc P ⦃ P-is-prop ⦄ h₀-p n =
    loc-fiber-rec P ⦃ P-is-prop ⦄ h₀-p (loc n)
      ≡⟨ ap ([]-extend-nondep ⦃ P-is-prop $ loc n ⦄ (loc-fiber-rec′ P h₀-p $ loc n))
            $ prop-has-all-paths []-is-prop (all-listed $ loc n) $ proj $ n , refl ⟩∎
    h₀-p n
      ∎

-- Did I preserve the computational contents for identity legend?
private
  module IdTest {i} {city : Set i} where
    open legend (id-legend city)

    visit-fiber-β-id : ∀ {j} (P : city → Set j)
      ⦃ P-is-set : ∀ (c : city) → is-set $ P c ⦄
      (h₀-p : ∀ n → P n)
      (h₁-r : ∀ n₁ n₂ r → transport P r (h₀-p n₁) ≡ h₀-p n₂)
      → ∀ n → visit-fiber-rec (id-legend city) P ⦃ P-is-set ⦄ h₀-p h₁-r n ≡ h₀-p n
    visit-fiber-β-id P ⦃ P-is-set ⦄ h₀-p h₁-r n = refl

    loc-fiber-β-id : ∀ {j} (P : city → Set j)
      ⦃ P-is-prop : ∀ (c : city) → is-prop $ P c ⦄
      (h₀-p : ∀ n → P n)
      → ∀ n → loc-fiber-rec (id-legend city) P ⦃ P-is-prop ⦄ h₀-p n ≡ h₀-p n
    loc-fiber-β-id P ⦃ P-is-prop ⦄ h₀-p n = refl

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text: {-# OPTIONS --profile=notclose #-}

max_stars_repo_name: sseefried/agda


text:
{-

Descriptor language for easily defining relational structures

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Structures.Relational.Macro where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Data.Sigma

open import Cubical.Structures.Relational.Constant
open import Cubical.Structures.Relational.Function
open import Cubical.Structures.Relational.Maybe
open import Cubical.Structures.Relational.Parameterized
open import Cubical.Structures.Relational.Pointed
open import Cubical.Structures.Relational.Product

open import Cubical.Structures.Macro
open import Cubical.Structures.Maybe

data PosRelDesc (ℓ : Level) : Typeω where
  -- constant structure: X ↦ A
  constant : ∀ {ℓ'} → hSet ℓ' → PosRelDesc ℓ
  -- pointed structure: X ↦ X
  var : PosRelDesc ℓ
  -- product of structures S,T : X ↦ (S X × T X)
  _,_ : PosRelDesc ℓ  → PosRelDesc ℓ  → PosRelDesc ℓ
  -- Maybe on a structure S: X ↦ Maybe (S X)
  maybe : PosRelDesc ℓ → PosRelDesc ℓ

data RelDesc (ℓ : Level) : Typeω where
  -- constant structure: X ↦ A
  constant : ∀ {ℓ'} → hSet ℓ' → RelDesc ℓ
  -- pointed structure: X ↦ X
  var : RelDesc ℓ
  -- product of structures S,T : X ↦ (S X × T X)
  _,_ : RelDesc ℓ  → RelDesc ℓ  → RelDesc ℓ
  -- structure S parameterized by constant A : X ↦ (A → S X)
  param : ∀ {ℓ'} → (A : Type ℓ') → RelDesc ℓ  → RelDesc ℓ
  -- function from positive structure S to T: X ↦ (S X → T X)
  function+ : PosRelDesc ℓ → RelDesc ℓ → RelDesc ℓ
  -- Maybe on a structure S: X ↦ Maybe (S X)
  maybe : RelDesc ℓ → RelDesc ℓ

infixr 4 _,_

posRelDesc→TranspDesc : ∀ {ℓ} → PosRelDesc ℓ → TranspDesc ℓ
posRelDesc→TranspDesc (constant A) = constant (A .fst)
posRelDesc→TranspDesc var = var
posRelDesc→TranspDesc (d₀ , d₁) = posRelDesc→TranspDesc d₀ , posRelDesc→TranspDesc d₁
posRelDesc→TranspDesc (maybe d) = maybe (posRelDesc→TranspDesc d)

posRelDesc→RelDesc : ∀ {ℓ} → PosRelDesc ℓ → RelDesc ℓ
posRelDesc→RelDesc (constant A) = constant A
posRelDesc→RelDesc var = var
posRelDesc→RelDesc (d₀ , d₁) = posRelDesc→RelDesc d₀ , posRelDesc→RelDesc d₁
posRelDesc→RelDesc (maybe d) = maybe (posRelDesc→RelDesc d)

relDesc→Desc : ∀ {ℓ} → RelDesc ℓ → Desc ℓ
relDesc→Desc (constant A) = constant (A .fst)
relDesc→Desc var = var
relDesc→Desc (d₀ , d₁) = relDesc→Desc d₀ , relDesc→Desc d₁
relDesc→Desc (param A d) = function+ (constant A) (relDesc→Desc d)
relDesc→Desc (function+ d₀ d₁) = function+ (posRelDesc→TranspDesc d₀) (relDesc→Desc d₁)
relDesc→Desc (maybe d) = maybe (relDesc→Desc d)

{- Universe level calculations -}

posRelMacroStrLevel : ∀ {ℓ} → PosRelDesc ℓ → Level
posRelMacroStrLevel d = transpMacroLevel (posRelDesc→TranspDesc d)

relMacroStrLevel : ∀ {ℓ} → RelDesc ℓ → Level
relMacroStrLevel d = macroStrLevel (relDesc→Desc d)

posRelMacroRelLevel : ∀ {ℓ} → PosRelDesc ℓ → Level
posRelMacroRelLevel (constant {ℓ'} A) = ℓ'
posRelMacroRelLevel {ℓ} var = ℓ
posRelMacroRelLevel (d₀ , d₁) = ℓ-max (posRelMacroRelLevel d₀) (posRelMacroRelLevel d₁)
posRelMacroRelLevel (maybe d) = posRelMacroRelLevel d

relMacroRelLevel : ∀ {ℓ} → RelDesc ℓ → Level
relMacroRelLevel (constant {ℓ'} A) = ℓ'
relMacroRelLevel {ℓ} var = ℓ
relMacroRelLevel (d₀ , d₁) = ℓ-max (relMacroRelLevel d₀) (relMacroRelLevel d₁)
relMacroRelLevel (param {ℓ'} A d) = ℓ-max ℓ' (relMacroRelLevel d)
relMacroRelLevel (function+ d₀ d₁) =
  ℓ-max (posRelMacroStrLevel d₀) (ℓ-max (posRelMacroRelLevel d₀) (relMacroRelLevel d₁))
relMacroRelLevel (maybe d) = relMacroRelLevel d

{- Definition of structure -}

PosRelMacroStructure : ∀ {ℓ} (d : PosRelDesc ℓ) → Type ℓ → Type (posRelMacroStrLevel d)
PosRelMacroStructure d = TranspMacroStructure (posRelDesc→TranspDesc d)

RelMacroStructure : ∀ {ℓ} (d : RelDesc ℓ) → Type ℓ → Type (relMacroStrLevel d)
RelMacroStructure d = MacroStructure (relDesc→Desc d)

{- Notion of structured relation defined by a descriptor -}

PosRelMacroRelStr : ∀ {ℓ} (d : PosRelDesc ℓ) → StrRel {ℓ} (PosRelMacroStructure d) (posRelMacroRelLevel d)
PosRelMacroRelStr (constant A) = ConstantRelStr A
PosRelMacroRelStr var = PointedRelStr
PosRelMacroRelStr (d₀ , d₁) = ProductRelStr (PosRelMacroRelStr d₀) (PosRelMacroRelStr d₁)
PosRelMacroRelStr (maybe d) = MaybeRelStr (PosRelMacroRelStr d)

RelMacroRelStr : ∀ {ℓ} (d : RelDesc ℓ) → StrRel {ℓ} (RelMacroStructure d) (relMacroRelLevel d)
RelMacroRelStr (constant A) = ConstantRelStr A
RelMacroRelStr var = PointedRelStr
RelMacroRelStr (d₀ , d₁) = ProductRelStr (RelMacroRelStr d₀) (RelMacroRelStr d₁)
RelMacroRelStr (param A d) = ParamRelStr A (λ _ → RelMacroRelStr d)
RelMacroRelStr (function+ d₀ d₁) =
  FunctionRelStr (PosRelMacroRelStr d₀)  (RelMacroRelStr d₁)
RelMacroRelStr (maybe d) = MaybeRelStr (RelMacroRelStr d)

{- Proof that structure induced by descriptor is suitable or positive -}

posRelMacroSuitableRel : ∀ {ℓ} (d : PosRelDesc ℓ) → SuitableStrRel _ (PosRelMacroRelStr d)
posRelMacroSuitableRel (constant A) = constantSuitableRel A
posRelMacroSuitableRel var = pointedSuitableRel
posRelMacroSuitableRel (d₀ , d₁) =
  productSuitableRel (posRelMacroSuitableRel d₀) (posRelMacroSuitableRel d₁)
posRelMacroSuitableRel (maybe d) = maybeSuitableRel (posRelMacroSuitableRel d)

posRelMacroPositiveRel : ∀ {ℓ} (d : PosRelDesc ℓ) → PositiveStrRel (posRelMacroSuitableRel d)
posRelMacroPositiveRel (constant A) = constantPositiveRel A
posRelMacroPositiveRel var = pointedPositiveRel
posRelMacroPositiveRel (d₀ , d₁) =
  productPositiveRel (posRelMacroPositiveRel d₀) (posRelMacroPositiveRel d₁)
posRelMacroPositiveRel (maybe d) = maybePositiveRel (posRelMacroPositiveRel d)

relMacroSuitableRel : ∀ {ℓ} (d : RelDesc ℓ) → SuitableStrRel _ (RelMacroRelStr d)
relMacroSuitableRel (constant A) = constantSuitableRel A
relMacroSuitableRel var = pointedSuitableRel
relMacroSuitableRel (d₀ , d₁) = productSuitableRel (relMacroSuitableRel d₀) (relMacroSuitableRel d₁)
relMacroSuitableRel (param A d) = paramSuitableRel A (λ _ → relMacroSuitableRel d)
relMacroSuitableRel (function+ d₀ d₁) =
  functionSuitableRel (posRelMacroSuitableRel d₀) (posRelMacroPositiveRel d₀) (relMacroSuitableRel d₁)
relMacroSuitableRel (maybe d) = maybeSuitableRel (relMacroSuitableRel d)

{- Proof that structured relations and equivalences agree -}

posRelMacroMatchesEquiv : ∀ {ℓ} (d : PosRelDesc ℓ)
  → StrRelMatchesEquiv (PosRelMacroRelStr d) (EquivAction→StrEquiv (transpMacroAction (posRelDesc→TranspDesc d)))
posRelMacroMatchesEquiv (constant A) _ _ _ = idEquiv _
posRelMacroMatchesEquiv var _ _ _ = idEquiv _
posRelMacroMatchesEquiv (d₀ , d₁) =
  productRelMatchesTransp
    (PosRelMacroRelStr d₀) (transpMacroAction (posRelDesc→TranspDesc d₀))
    (PosRelMacroRelStr d₁) (transpMacroAction (posRelDesc→TranspDesc d₁))
    (posRelMacroMatchesEquiv d₀) (posRelMacroMatchesEquiv d₁)
posRelMacroMatchesEquiv (maybe d) =
  maybeRelMatchesTransp
    (PosRelMacroRelStr d) (transpMacroAction (posRelDesc→TranspDesc d))
    (posRelMacroMatchesEquiv d)

relMacroMatchesEquiv : ∀ {ℓ} (d : RelDesc ℓ)
  → StrRelMatchesEquiv (RelMacroRelStr d) (MacroEquivStr (relDesc→Desc d))
relMacroMatchesEquiv (constant A) = constantRelMatchesEquiv A
relMacroMatchesEquiv var = pointedRelMatchesEquiv
relMacroMatchesEquiv (d₁ , d₂) =
  productRelMatchesEquiv
    (RelMacroRelStr d₁) (RelMacroRelStr d₂)
    (relMacroMatchesEquiv d₁) (relMacroMatchesEquiv d₂)
relMacroMatchesEquiv (param A d) =
  paramRelMatchesEquiv A (λ _ → RelMacroRelStr d) (λ _ → relMacroMatchesEquiv d)
relMacroMatchesEquiv (function+ d₀ d₁) =
  functionRelMatchesEquiv+
    (PosRelMacroRelStr d₀) (transpMacroAction (posRelDesc→TranspDesc d₀))
    (RelMacroRelStr d₁) (MacroEquivStr (relDesc→Desc d₁))
    (posRelMacroMatchesEquiv d₀) (relMacroMatchesEquiv d₁)
relMacroMatchesEquiv (maybe d) =
  maybeRelMatchesEquiv (RelMacroRelStr d) (relMacroMatchesEquiv d)

-- Module for easy importing
module RelMacro ℓ (d : RelDesc ℓ) where
  relation = RelMacroRelStr d
  suitable = relMacroSuitableRel d
  matches = relMacroMatchesEquiv d
  open Macro ℓ (relDesc→Desc d) public

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------------
-- Totality properties respect to OrdList
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.OrdListI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Program.SortList.Properties.Totality.BoolI
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- If (i ∷ is) is ordered then 'is' is ordered.
subList-OrdList : ∀ {i is} → N i → ListN is → OrdList (i ∷ is) → OrdList is
subList-OrdList {i} Ni lnnil LOi∷is = ordList-[]

subList-OrdList {i} Ni (lncons {j} {js} Nj Ljs) LOi∷j∷js =
  &&-list₂-t₂ (le-ItemList-Bool Ni (lncons Nj Ljs))
              (ordList-Bool (lncons Nj Ljs))
              (trans (sym (ordList-∷ i (j ∷ js))) LOi∷j∷js)

++-OrdList-helper : ∀ {item is js} → N item → ListN is → ListN js →
                    ≤-ItemList item is →
                    ≤-ItemList item js →
                    ≤-Lists is js →
                    ≤-ItemList item (is ++ js)
++-OrdList-helper {item} {js = js} _ lnnil _ _ item≤js _ =
  subst (≤-ItemList item) (sym (++-leftIdentity js)) item≤js

++-OrdList-helper {item} {js = js} Nitem
                  (lncons {i} {is} Ni LNis) LNjs item≤i∷is item≤js i∷is≤js =
  le-ItemList item ((i ∷ is) ++ js)
    ≡⟨ subst (λ t → le-ItemList item ((i ∷ is) ++ js) ≡ le-ItemList item t)
             (++-∷ i is js)
             refl
    ⟩
  le-ItemList item (i ∷ (is ++ js))
    ≡⟨ le-ItemList-∷ item i (is ++ js) ⟩
  le item i && le-ItemList item (is ++ js)
    ≡⟨ subst (λ t → le item i && le-ItemList item (is ++ js) ≡
                    t && le-ItemList item (is ++ js))
             (&&-list₂-t₁ (le-Bool Nitem Ni)
                          (le-ItemList-Bool Nitem LNis)
                          (trans (sym (le-ItemList-∷ item i is)) item≤i∷is))
             refl
    ⟩
  true && le-ItemList item (is ++ js)
    ≡⟨ subst (λ t → true && le-ItemList item (is ++ js) ≡ true && t)
             (++-OrdList-helper Nitem LNis LNjs lemma₁ item≤js lemma₂)
             refl
    ⟩
  true && true
    ≡⟨ t&&x≡x true ⟩
  true ∎
    where
    lemma₁ : le-ItemList item is ≡ true
    lemma₁ = &&-list₂-t₂ (le-Bool Nitem Ni)
                         (le-ItemList-Bool Nitem LNis)
                         (trans (sym (le-ItemList-∷ item i is)) item≤i∷is)

    lemma₂ : le-Lists is js ≡ true
    lemma₂ = &&-list₂-t₂ (le-ItemList-Bool Ni LNjs)
                         (le-Lists-Bool LNis LNjs)
                         (trans (sym (le-Lists-∷ i is js)) i∷is≤js)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

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

-- This module contains properties that are only about the behavior of the handlers, nothing to do
-- with system state

open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.Types
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Util

module LibraBFT.Impl.Consensus.RoundManager.Properties where

  open import LibraBFT.Impl.Consensus.RoundManager

  voteForCurrentEpoch : ∀ {ts pm pre vm αs}
                      → (SendVote vm αs) ∈ LBFT-outs (processProposalMsg ts pm) pre
                      → (₋rmEC pre) ^∙ rmEpoch ≡ vm ^∙ vmVote ∙ vEpoch
  voteForCurrentEpoch (here refl) = refl

  -- The quorum certificates sent in SyncInfo with votes are those from the peer state
  procPMCerts≡ : ∀ {ts pm pre vm αs}
               → (SendVote vm αs) ∈ LBFT-outs (processProposalMsg ts pm) pre
               → vm ^∙ vmSyncInfo ≡ SyncInfo∙new (₋rmHighestQC pre) (₋rmHighestCommitQC pre)
  procPMCerts≡ (there x)   = ⊥-elim (¬Any[] x)  -- processProposalMsg sends only one vote
  procPMCerts≡ (here refl) = refl

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Cones where

open import Level

open import Categories.Support.PropositionalEquality

open import Categories.Category
open import Categories.Functor hiding (_∘_; _≡_; equiv; id; assoc; identityˡ; identityʳ; ∘-resp-≡)
open import Categories.Cone

record ConeMorphism {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} {F : Functor J C} (c₁ c₂ : Cone F) : Set (ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
  module c₁ = Cone c₁
  module c₂ = Cone c₂
  module C = Category C
  module J = Category J
  open C
  field
    f : C [ c₁.N , c₂.N ]
    .commute : ∀ {X} → c₁.ψ X ≡ c₂.ψ X ∘ f

Cones : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) → Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) (ℓ ⊔ e ⊔ o′ ⊔ ℓ′) e
Cones {C = C} F = record
  { Obj = Obj′
  ; _⇒_ = Hom′
  ; _≡_ = _≡′_
  ; _∘_ = _∘′_
  ; id = record { f = id; commute = Equiv.sym identityʳ }
  ; assoc = assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv = record
    { refl = Equiv.refl
    ; sym = Equiv.sym
    ; trans = Equiv.trans
    }
  ; ∘-resp-≡ = ∘-resp-≡
  }
  where
  open Category C
  open Cone
  open ConeMorphism
  open Functor F

  infixr 9 _∘′_
  infix  4 _≡′_

  Obj′ = Cone F

  Hom′ : Obj′ → Obj′ → Set _
  Hom′ = ConeMorphism

  _≡′_ : ∀ {A B} → Hom′ A B → Hom′ A B → Set _
  F ≡′ G = f F ≡ f G

  _∘′_ : ∀ {A B C} → Hom′ B C → Hom′ A B → Hom′ A C
  _∘′_ {A} {B} {C} F G = record
    { f = f F ∘ f G
    ; commute = commute′
    }
    where
    .commute′ : ∀ {X} → ψ A X ≡ ψ C X ∘ (f F ∘ f G)
    commute′ {X} =
        begin
          ψ A X
        ↓⟨ ConeMorphism.commute G ⟩
          ψ B X ∘ f G
        ↓⟨ ∘-resp-≡ˡ (ConeMorphism.commute F) ⟩
          (ψ C X ∘ f F) ∘ f G
        ↓⟨ assoc ⟩
          ψ C X ∘ (f F ∘ f G)
        ∎
      where
      open HomReasoning

-- Equality of cone morphisms is equality of the underlying arrows in the
-- base category, but the same is not (directly) true of the heterogeneous
-- equality.  These functions make the equivalence manifest.

module Heteroconic {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where
  open Heterogeneous C
  module ▵ = Heterogeneous (Cones F)
  open ▵ public using () renaming (_∼_ to _▵̃_)
  open ConeMorphism using () renaming (f to ⌞_⌝)

  demote-∼ : ∀ {K L K′ L′} {f : ConeMorphism K L} {g : ConeMorphism K′ L′}
           → f ▵̃ g → ⌞ f ⌝ ∼ ⌞ g ⌝
  demote-∼ (≡⇒∼ y) = Heterogeneous.≡⇒∼ y

  -- XXX probably need another argument or something to nail things down
  -- promote-∼ : ∀ {K L K′ L′} {f : ConeMorphism {C = C} K L} {g : ConeMorphism {C = C} K′ L′}
  --           → ⌞ f ⌝ ∼ ⌞ g ⌝ → f ▵̃ g
  -- promote-∼ h = {!h!}

-- The category of cones comes with an equivalence of objects, which can be
-- used to float morphisms from one to another.  Really it should have a
-- setoid of objects, but we're not equipped for that.

module Float {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

  module H = Heterogeneous C
  open H hiding (float₂; floatˡ; floatʳ; floatˡ-resp-trans; float₂-breakdown-lr; float₂-breakdown-rl)

  private
    lemma₁ : ∀ (A B : Cone F) {f₁ f₂ : C [ Cone.N A , Cone.N B ]} (f₁≣f₂ : f₁ ≣ f₂) .(pf₁ : ∀ {X} → C [ Cone.ψ A X ≡ C [ Cone.ψ B X ∘ f₁ ] ]) .(pf₂ : ∀ {X} → C [ Cone.ψ A X ≡ C [ Cone.ψ B X ∘ f₂ ] ]) → _≣_ {A = ConeMorphism A B} record { f = f₁ ; commute = pf₁ } record { f = f₂ ; commute = pf₂ }
    lemma₁ A B ≣-refl = λ ._ ._ → ≣-refl

  morphism-determines-cone-morphism-≣ : ∀ {A B} {m m′ : Cones F [ A , B ]} → ConeMorphism.f m ≣ ConeMorphism.f m′ → m ≣ m′
  morphism-determines-cone-morphism-≣ {A} {B} {m} {m′} pf = lemma₁ A B pf (ConeMorphism.commute m) (ConeMorphism.commute m′)

  float₂ : ∀ {A A′ B B′} → F [ A ≜ A′ ] → F [ B ≜ B′ ] → Cones F [ A , B ] → Cones F [ A′ , B′ ]
  float₂ A≜A′ B≜B′ κ = record
    { f = H.float₂ (N-≣ A≜A′) (N-≣ B≜B′) f
    ; commute = λ {j} → ∼⇒≡ (trans (sym (ψ-≡ A≜A′ j)) (trans (≡⇒∼ commute) (∘-resp-∼ (ψ-≡ B≜B′ j) (float₂-resp-∼ (N-≣ A≜A′) (N-≣ B≜B′)))))
    }
    where
    open ConeMorphism κ
    open ConeOver._≜_

  floatˡ : ∀ {A B B′} → F [ B ≜ B′ ] → Cones F [ A , B ] → Cones F [ A , B′ ]
  floatˡ {A = A} B≜B′ κ = record
    { f = H.floatˡ N-≣ f
    ; commute = λ {j} → C.Equiv.trans commute (∼⇒≡ (∘-resp-∼ (ψ-≡ j) (floatˡ-resp-∼ N-≣)))
    }
    where
    module A = Cone A
    open ConeMorphism κ
    open ConeOver._≜_ B≜B′

  floatˡ-resp-refl : ∀ {A B} (κ : Cones F [ A , B ]) → floatˡ {A} {B} (ConeOver.≜-refl F) κ ≣ κ
  floatˡ-resp-refl f = ≣-refl

  floatˡ-resp-trans : ∀ {A B B′ B″} (B≜B′ : F [ B ≜ B′ ]) (B′≜B″ : F [ B′ ≜ B″ ]) (κ : Cones F [ A , B ]) → floatˡ {A} {B} {B″} (ConeOver.≜-trans F B≜B′ B′≜B″) κ ≣ floatˡ {A} {B′} {B″} B′≜B″ (floatˡ {A} {B} {B′} B≜B′ κ)
  floatˡ-resp-trans {A} {B} {B′} {B″} B≜B′ B′≜B″ κ = morphism-determines-cone-morphism-≣ {A} {B″} {floatˡ {A} {B} {B″} (ConeOver.≜-trans F B≜B′ B′≜B″) κ} {floatˡ {A} {B′} {B″} B′≜B″ (floatˡ {A} {B} {B′} B≜B′ κ)} (H.floatˡ-resp-trans (N-≣ B≜B′) (N-≣ B′≜B″) f)
    where
    module A = Cone A
    open ConeOver._≜_
    open ConeMorphism κ

  floatʳ : ∀ {A A′ B} → F [ A ≜ A′ ] → Cones F [ A , B ] → Cones F [ A′ , B ]
  floatʳ {B = B} A≜A′ κ = record
    { f = ≣-subst (λ X → C [ X , B.N ]) N-≣ f
    ; commute = λ {j} → ∼⇒≡ (trans (sym (ψ-≡ j)) (trans (≡⇒∼ commute) (∘-resp-∼ʳ (floatʳ-resp-∼ N-≣))))
    }
    where
    module B = Cone B
    open ConeMorphism κ
    open ConeOver._≜_ A≜A′

  float₂-breakdown-lr : ∀ {A A′ B B′ : Cone F} (A≜A′ : F [ A ≜ A′ ]) (B≜B′ : F [ B ≜ B′ ]) (κ : Cones F [ A , B ]) → float₂ A≜A′ B≜B′ κ ≣ floatˡ B≜B′ (floatʳ A≜A′ κ)
  float₂-breakdown-lr {A′ = A′} {B′ = B′} A≜A′ B≜B′ κ = morphism-determines-cone-morphism-≣ {A = A′} {B′} {float₂ A≜A′ B≜B′ κ} {floatˡ B≜B′ (floatʳ A≜A′ κ)} (H.float₂-breakdown-lr (N-≣ A≜A′) (N-≣ B≜B′) (ConeMorphism.f κ))
    where open ConeOver._≜_

  float₂-breakdown-rl : ∀ {A A′ B B′ : Cone F} (A≜A′ : F [ A ≜ A′ ]) (B≜B′ : F [ B ≜ B′ ]) (κ : Cones F [ A , B ]) → float₂ A≜A′ B≜B′ κ ≣ floatʳ A≜A′ (floatˡ B≜B′ κ)
  float₂-breakdown-rl {A′ = A′} {B′ = B′} A≜A′ B≜B′ κ = morphism-determines-cone-morphism-≣ {A = A′} {B′} {float₂ A≜A′ B≜B′ κ} {floatʳ A≜A′ (floatˡ B≜B′ κ)} (H.float₂-breakdown-rl (N-≣ A≜A′) (N-≣ B≜B′) (ConeMorphism.f κ))
    where open ConeOver._≜_

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module L.Base.Core where

-- Reexport all of the Cores
open import L.Base.Sigma.Core public
open import L.Base.Coproduct.Core public
open import L.Base.Empty.Core public
open import L.Base.Unit.Core public
open import L.Base.Nat.Core public
open import L.Base.Id.Core public

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
module Data.DependentWidthTree where

import      Lvl
open import Functional using (id)
open import Functional.Dependent
open import Numeral.Finite
open import Numeral.Natural
open import Type

private variable ℓ ℓᵢ ℓₗ ℓₙ ℓₒ : Lvl.Level
private variable N N₁ N₂ L T A B : Type{ℓ}

module _ {N : Type{ℓₙ}} (Index : N → Type{ℓᵢ}) where
  -- A tree where the number of children depends on the data stored in a node.
  -- Leaves should be represented by having nodes that indicate no children.
  -- Note: A tree that have no leaves will not be constructible.
  data Tree : Type{ℓₙ Lvl.⊔ ℓᵢ} where
    Node : (node : N) → (Index(node) → Tree) → Tree

  -- The data of the root node of a tree.
  root : Tree → N
  root (Node node _) = node

  -- The children of a node of a tree.
  -- They are indexed by `Index`.
  child : (t : Tree) → (Index(root t) → Tree)
  child (Node _ child) = child

  Tree-elim : ∀{P : Tree → Type{ℓ}} → (∀(node)(child) → (∀(i) → P(child(i))) → P(Node node child)) → ((tree : Tree) → P(tree))
  Tree-elim{P = P} f (Node node child) = f node child (Tree-elim{P = P} f ∘ child)

  open import Logic.Propositional
  -- It is impossible for every node to have at least one child while at the same time a tree exists.
  -- Note that constructively, this is not enough to prove the existence of leaves.
  Tree-no-leaves-impossibility : (∀{node} → Index(node)) → Tree → ⊥
  Tree-no-leaves-impossibility p (Node n c) = Tree-no-leaves-impossibility p (c(p{n}))

module _ {N : Type{ℓₙ}} (width : N → ℕ) where
  FiniteTree = Tree(𝕟 ∘ width)

module _ where
  open import Data.Boolean

  -- A tree of finite variating width holding no data other than the structure of the tree (the number of children for each node).
  -- Example:
  --   3:
  --   ├1:
  --   │└0
  --   ├2:
  --   │├0
  --   │└1:
  --   │ └0
  --   └0
  FiniteTreeStructure = FiniteTree id

  -- An empty tree contains no children.
  -- This is also functioning as a leaf to a tree.
  empty : FiniteTreeStructure
  empty = Node 0 \()

  -- A tree containing a single child that contains a leaf.
  singleton : FiniteTreeStructure
  singleton = Node 1 \{𝟎 → empty}

  isLeaf : FiniteTreeStructure → Bool
  isLeaf(Node 𝟎     _) = 𝑇
  isLeaf(Node (𝐒 _) _) = 𝐹

  isNode : FiniteTreeStructure → Bool
  isNode(Node 𝟎     _) = 𝐹
  isNode(Node (𝐒 _) _) = 𝑇

  import      Numeral.CoordinateVector as CoordinateVector
  open import Numeral.Natural.Function
  open import Numeral.Natural.Oper

  -- The height is the length of the longest path from the root node.
  -- Alternative implementation (will not pass the termination checker):
  --   height(Node 𝟎         child) = 𝟎
  --   height(Node (𝐒(node)) child) = 𝐒(CoordinateVector.foldᵣ(max ∘ height) 𝟎 child)
  height : FiniteTreeStructure → ℕ
  height = Tree-elim 𝕟 (\{𝟎 _ _ → 𝟎 ; (𝐒(c)) _ prev → 𝐒(CoordinateVector.foldᵣ max 𝟎 prev)})

  -- The size of a tree is the number of nodes in the tree.
  size : FiniteTreeStructure → ℕ
  size = Tree-elim 𝕟 (\{𝟎 _ _ → 𝟎 ; (𝐒(c)) _ prev → 𝐒(CoordinateVector.foldᵣ (_+_) 𝟎 prev)})


text:
module SafeFlagPrimTrustMe where

-- Cannot make an example with the correct type signature for
-- primTrustMe since it requires postulated universe level builtins,
-- which --safe flag will reject.

private
 primitive
   primTrustMe : Set

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- {-# OPTIONS --no-forcing #-}
{-# OPTIONS --rewriting #-}
{-# OPTIONS --sized-types #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Size

{-# BUILTIN REWRITE _≡_ #-}

variable i j : Size

postulate ANY : ∀{A : Set} → A

data Ty : Set where
  bool : Ty

variable a b c d : Ty

infixl 5 _∘_
infixr 6 _∷_ _++_

mutual

  data Tm (c : Ty) : Set where
    tm : ∀{i a} (E : Stack i a c) → Tm c

  data Stack (i : Size) : (a c : Ty) → Set where
    ε    : ∀{c} → Stack i c c
    _∷_  : ∀{j : Size< i}{b} (u : Tm b) (E : Stack j b c) → Stack i bool c

  variable E E' E′ : Stack i a c

_++_ : ∀{a b c} → Stack ∞ a b → Stack ∞ b c → Stack ∞ a c
ε       ++ E′ = E′
(u ∷ E) ++ E′ = u ∷ (E ++ E′)

postulate
  _∘_ : ∀{a c} → Tm a → Stack ∞ a c → Tm c
  app-app : ∀{i j a b c}{t : Tm a} {E : Stack i a b} {E′ : Stack j b c} → t ∘ E ∘ E′ ≡ t ∘ E ++ E′

{-# REWRITE app-app #-}

infix 4 _↦_  _↦ₛ_

mutual

  data _↦_ {c} : (t t′ : Tm c) → Set where
    ↦E  : (r : E ↦ₛ E′) → tm E ↦ tm E′
    -- ↦E  : ∀{i a} {E E′ : Stack i a c} (r : E ↦ₛ E′) → tm E ↦ tm E′ -- no internal error

  data _↦ₛ_ {c} : ∀ {i a} (E E′ : Stack i a c) → Set where
    π     : ∀{i a u v} {E : Stack i a c} → (u ∷ v ∷ E) ↦ₛ ((u ∘ v ∷ ε) ∷ E)
    there : ∀{i a u} {E E′ : Stack i a c} (r : E ↦ₛ E′) → u ∷ E ↦ₛ u  ∷ E′

data SN {a} (t : Tm a) : Set where
  acc : (h : {t′ : Tm a} (r : t ↦ t′) → SN t′) → SN t

-- {-# TERMINATING #-}  -- removes internal error

test : {i : Size} {a c : Ty} {t : Tm a} {E : Stack i a c}
          (sntE : SN (t ∘ E))
          → SN (tm (t ∷ E))
test {i = i} {t = t} (acc sntE) = acc
  λ { (↦E (there r)) → test (sntE ANY)
    ; (↦E (π {i = j})) → test {i = j} (acc sntE)
    }

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module Sets where

  import Equality
  open Equality public

  infixr 10 _$_
  infixr 40 _[+]_ _<+>_ _>+<_
  infixr 60 _[×]_ _<×>_ _>×<_
  infixr 90 _∘_

  id : {A : Set} -> A -> A
  id x = x

  _∘_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
  f ∘ g = \x -> f (g x)

  _$_ : {A B : Set} -> (A -> B) -> A -> B
  f $ x = f x

  data _[+]_ (A B : Set) : Set where
    inl : A -> A [+] B
    inr : B -> A [+] B

  _<+>_ : {A₁ A₂ B₁ B₂ : Set} -> (A₁ -> A₂) -> (B₁ -> B₂) -> A₁ [+] B₁ -> A₂ [+] B₂
  (f <+> g) (inl x) = inl (f x)
  (f <+> g) (inr y) = inr (g y)

  _>+<_ : {A B C : Set} -> (A -> C) -> (B -> C) -> A [+] B -> C
  (f >+< g) (inl x) = f x
  (f >+< g) (inr y) = g y

  data _[×]_ (A B : Set) : Set where
    <_,_> : A -> B -> A [×] B

  -- sections
  <∙,_> : {A B : Set} -> B -> A -> A [×] B
  <∙, x > = \y -> < y , x >

  <_,∙> : {A B : Set} -> A -> B -> A [×] B
  < x ,∙> = \y -> < x , y >

  _<×>_ : {A₁ A₂ B₁ B₂ : Set} -> (A₁ -> A₂) -> (B₁ -> B₂) -> A₁ [×] B₁ -> A₂ [×] B₂
  (f <×> g) < x , y > = < f x , g y >

  _>×<_ : {A B C : Set} -> (A -> B) -> (A -> C) -> A -> B [×] C
  (f >×< g) x = < f x , g x >

  fst : {A B : Set} -> A [×] B -> A
  fst < a , b > = a

  snd : {A B : Set} -> A [×] B -> B
  snd < a , b > = b

  η-[×] : {A B : Set}(p : A [×] B) -> p == < fst p , snd p >
  η-[×] < a , b > = refl

  data [1] : Set where
    <> : [1]

  data [0] : Set where

  data List (A : Set) : Set where
    []   : List A
    _::_ : A -> List A -> List A


text:
-- 2014-04-24

module _ where

open import Common.Size
open import Common.Prelude using (Bool; true; false; if_then_else_)
open import Common.Product

-- sized lists

data List A {i} : Set where
  []  : List A
  _∷_ : {i' : Size< i} (x : A) (xs : List A {i'}) → List A

_++_ : ∀{A} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

partition : ∀{A i} (p : A → Bool) (l : List A {i}) → List A {i} × List A {i}
partition p []       = [] , []
partition p (x ∷ xs) = let l , r = partition p xs in
  if p x then ((x ∷ l) , r) else (l , (x ∷ r))

module Sort {A : Set} (_≤_ : A → A → Bool) where

  quicksort : ∀{i} → List A {i} → List A
  quicksort []       = []
  quicksort (x ∷ []) = x ∷ []
  quicksort (x ∷ xs) = let x≤ , ≤x = partition (_≤_ x) xs in
    quicksort ≤x ++ (x ∷ quicksort x≤)


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

open import LogicalFormulae
open import Functions.Definition
open import Groups.Definition
open import Groups.Abelian.Definition
open import Setoids.Setoids
open import Rings.Definition
open import Sets.FinSet.Definition
open import Vectors
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Sets.EquivalenceRelations

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Modules.Definition

module Modules.Span {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+R_ _*_} {m n : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} {G : AbelianGroup G'} {_·_ : A → M → M} (mod : Module R G _·_) where

open Group G'
open Setoid T
open Equivalence eq

_=V_ : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) {n1 : ℕ} → Rel {a} {b ⊔ n} (Vec A n1)
_=V_ G [] [] = True'
_=V_ {S = S} G (x ,- xs) (y ,- ys) = (Setoid._∼_ S x y) && (_=V_ G xs ys)

dot : {n : ℕ} → (Vec M n) → (Vec A n) → M
dot [] [] = 0G
dot (v ,- vs) (x ,- xs) = (x · v) + (dot vs xs)

Spans : {c : _} {C : Set c} (f : C → M) → Set (a ⊔ m ⊔ n ⊔ c)
Spans {C = C} f = (m : M) → Sg ℕ (λ n → Sg ((Vec C n) && (Vec A n)) (λ t → (dot (vecMap f (_&&_.fst t)) (_&&_.snd t)) ∼ m))

Independent : {c : _} {C : Set c} (f : C → M) → Set (a ⊔ b ⊔ n ⊔ c)
Independent {C = C} f = {n : ℕ} → (r : Vec C n) → ({a b : ℕ} → (a<n : a <N n) → (b<n : b <N n) → vecIndex r a a<n ≡ vecIndex r b b<n → a ≡ b) → (b : Vec A n) → (dot (vecMap f r) b) ∼ 0G → _=V_ (Ring.additiveGroup R) (vecPure (Group.0G (Ring.additiveGroup R))) b

independentSubset : {c : _} {C : Set c} (f : C → M) → {d : _} {D : Set d} {inj : D → C} (isInj : Injection inj) → Independent f → Independent (f ∘ inj)
independentSubset f {inj = inj} isInj indp {n = n} r coeffInj coeffs dotZero = indp {n = n} (vecMap inj r) inj' coeffs (transitive (identityOfIndiscernablesRight _∼_ reflexive (applyEquality (λ i → dot i coeffs) (vecMapCompose inj f r))) dotZero)
  where
    inj' : {a b : ℕ} (a<n : a <N n) (b<n : b <N n) → vecIndex (vecMap inj r) a a<n ≡ vecIndex (vecMap inj r) b b<n → a ≡ b
    inj' a<n b<n x rewrite vecMapAndIndex r inj a<n | vecMapAndIndex r inj b<n = coeffInj a<n b<n (isInj x)

spanSuperset : {c : _} {C : Set c} (f : C → M) → {d : _} {D : Set d} {surj : D → C} (isSurj : Surjection surj) → Spans f → Spans (f ∘ surj)
spanSuperset f {surj = surj} isSurj spans m with spans m
spanSuperset {C = C} f {surj = surj} isSurj spans m | n , ((coeffs ,, basis) , b) = n , ((vecMap (λ c → underlying (isSurj c)) coeffs ,, basis) , transitive (identityOfIndiscernablesLeft _∼_ reflexive (applyEquality (λ i → dot i basis) (equalityCommutative {x = vecMap (λ i → f (surj i)) (vecMap (λ c → underlying (isSurj c)) coeffs)} {vecMap f coeffs} (transitivity (vecMapCompose (λ i → underlying (isSurj i)) (λ z → f (surj z)) coeffs) (t coeffs))))) b)
  where
    t : {n : ℕ} (coeffs : Vec C n) → vecMap (λ i → f (surj (underlying (isSurj i)))) coeffs ≡ vecMap f coeffs
    t [] = refl
    t (x ,- coeffs) with isSurj x
    ... | img , pr rewrite pr | t coeffs = refl

Basis : {c : _} {C : Set c} (f : C → M) → Set (a ⊔ b ⊔ m ⊔ n ⊔ c)
Basis v = Spans v && Independent v


text:
------------------------------------------------------------------------
-- "Equational" reasoning combinator setup
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Bisimilarity.Weak.Equational-reasoning-instances
         {ℓ} {lts : LTS ℓ} where

open import Prelude

open import Bisimilarity lts
import Bisimilarity.Equational-reasoning-instances
open import Bisimilarity.Weak lts
open import Equational-reasoning
open import Expansion lts
import Expansion.Equational-reasoning-instances

instance

  reflexive≈ : ∀ {i} → Reflexive [ i ]_≈_
  reflexive≈ = is-reflexive reflexive-≈

  reflexive≈′ : ∀ {i} → Reflexive [ i ]_≈′_
  reflexive≈′ = is-reflexive reflexive-≈′

  symmetric≈ : ∀ {i} → Symmetric [ i ]_≈_
  symmetric≈ = is-symmetric symmetric-≈

  symmetric≈′ : ∀ {i} → Symmetric [ i ]_≈′_
  symmetric≈′ = is-symmetric symmetric-≈′

  convert≈≈ : ∀ {i} → Convertible [ i ]_≈_ [ i ]_≈_
  convert≈≈ = is-convertible id

  convert≈′≈ : ∀ {i} → Convertible _≈′_ [ i ]_≈_
  convert≈′≈ = is-convertible (λ p≈′q → force p≈′q)

  convert≈≈′ : ∀ {i} → Convertible [ i ]_≈_ [ i ]_≈′_
  convert≈≈′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ≈ q → [ i ] p ≈′ q
    force (lemma p≈q) = p≈q

  convert≈′≈′ : ∀ {i} → Convertible [ i ]_≈′_ [ i ]_≈′_
  convert≈′≈′ = is-convertible id

  convert∼≈ : ∀ {i} → Convertible [ i ]_∼_ [ i ]_≈_
  convert∼≈ = is-convertible ∼⇒≈

  convert∼′≈ : ∀ {i} → Convertible _∼′_ [ i ]_≈_
  convert∼′≈ = is-convertible (convert ∘ ∼⇒≈′)

  convert∼≈′ : ∀ {i} → Convertible [ i ]_∼_ [ i ]_≈′_
  convert∼≈′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ∼ q → [ i ] p ≈′ q
    force (lemma p∼q) = ∼⇒≈ p∼q

  convert∼′≈′ : ∀ {i} → Convertible [ i ]_∼′_ [ i ]_≈′_
  convert∼′≈′ = is-convertible ∼⇒≈′

  convert≳≈ : ∀ {i} → Convertible [ i ]_≳_ [ i ]_≈_
  convert≳≈ = is-convertible ≳⇒≈

  convert≳′≈ : ∀ {i} → Convertible _≳′_ [ i ]_≈_
  convert≳′≈ = is-convertible (convert ∘ ≳⇒≈′)

  convert≳≈′ : ∀ {i} → Convertible [ i ]_≳_ [ i ]_≈′_
  convert≳≈′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ≳ q → [ i ] p ≈′ q
    force (lemma p≳q) = ≳⇒≈ p≳q

  convert≳′≈′ : ∀ {i} → Convertible [ i ]_≳′_ [ i ]_≈′_
  convert≳′≈′ = is-convertible ≳⇒≈′

  trans≈≈ : Transitive _≈_ _≈_
  trans≈≈ = is-transitive transitive-≈

  trans≈′≈ : Transitive _≈′_ _≈_
  trans≈′≈ = is-transitive λ p≈′q → transitive (force p≈′q)

  trans≈′≈′ : Transitive _≈′_ _≈′_
  trans≈′≈′ = is-transitive λ p≈′q q≈′r →
    transitive-≈′ p≈′q (convert q≈′r)

  trans≈≈′ : Transitive _≈_ _≈′_
  trans≈≈′ = is-transitive λ p≈q q≈′r →
    transitive-≈′ (convert p≈q) (convert q≈′r)

  trans∼≈ : ∀ {i} → Transitive _∼_ [ i ]_≈_
  trans∼≈ = is-transitive (transitive-≳≈ ∘ convert {a = ℓ})

  trans∼′≈ : ∀ {i} → Transitive _∼′_ [ i ]_≈_
  trans∼′≈ = is-transitive (transitive-≳≈ ∘ convert {a = ℓ})

  trans∼′≈′ : ∀ {i} → Transitive _∼′_ [ i ]_≈′_
  trans∼′≈′ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → p ∼′ q → [ i ] q ≈′ r → [ i ] p ≈′ r
    force (lemma p∼′q q≈′r) =
      transitive-≳≈ (convert {a = ℓ} p∼′q) (force q≈′r)

  trans∼≈′ : ∀ {i} → Transitive _∼_ [ i ]_≈′_
  trans∼≈′ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → p ∼ q → [ i ] q ≈′ r → [ i ] p ≈′ r
    force (lemma p∼q q≈′r) =
      transitive-≳≈ (convert {a = ℓ} p∼q) (force q≈′r)

  trans≈∼ : ∀ {i} → Transitive′ [ i ]_≈_ _∼_
  trans≈∼ = is-transitive transitive-≈∼

  trans≈∼′ : ∀ {i} → Transitive′ [ i ]_≈_ _∼′_
  trans≈∼′ = is-transitive (λ p≈q q∼′r →
    transitive-≈∼ p≈q (convert {a = ℓ} q∼′r))

  trans≈′∼ : ∀ {i} → Transitive′ [ i ]_≈′_ _∼_
  trans≈′∼ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → [ i ] p ≈′ q → q ∼ r → [ i ] p ≈′ r
    force (lemma p≈′q q∼r) = transitive-≈∼ (force p≈′q) q∼r

  trans≈′∼′ : ∀ {i} → Transitive′ [ i ]_≈′_ _∼′_
  trans≈′∼′ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → [ i ] p ≈′ q → q ∼′ r → [ i ] p ≈′ r
    force (lemma p≈′q q∼r) =
      transitive-≈∼ (force p≈′q) (convert {a = ℓ} q∼r)

  trans≳≈ : ∀ {i} → Transitive _≳_ [ i ]_≈_
  trans≳≈ = is-transitive transitive-≳≈

  trans≳′≈ : ∀ {i} → Transitive _≳′_ [ i ]_≈_
  trans≳′≈ = is-transitive (transitive-≳≈ ∘ convert {a = ℓ})

  trans≳′≈′ : ∀ {i} → Transitive _≳′_ [ i ]_≈′_
  trans≳′≈′ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → p ≳′ q → [ i ] q ≈′ r → [ i ] p ≈′ r
    force (lemma p≳′q q≈′r) =
      transitive-≳≈ (convert {a = ℓ} p≳′q) (force q≈′r)

  trans≳≈′ : ∀ {i} → Transitive _≳_ [ i ]_≈′_
  trans≳≈′ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → p ≳ q → [ i ] q ≈′ r → [ i ] p ≈′ r
    force (lemma p≳q q≈′r) = transitive-≳≈ p≳q (force q≈′r)

  -- For a proof showing that the following lemma cannot, in general,
  -- be made size-preserving in its first argument, see
  -- Bisimilarity.Weak.Delay-monad.size-preserving-transitivity-≈≳ˡ⇔uninhabited.

  trans≈≳ : Transitive′ _≈_ _≳_
  trans≈≳ = is-transitive (λ p≈q → transitive p≈q ∘ ≳⇒≈)

  trans≈≳′ : Transitive′ _≈_ _≳′_
  trans≈≳′ = is-transitive (λ p≈q → transitive p≈q ∘ ≳⇒≈ ∘ convert)

  trans≈′≳′ : Transitive′ _≈′_ _≳′_
  trans≈′≳′ = is-transitive (λ p≈′q → transitive p≈′q ∘ ≳⇒≈′)

  trans≈′≳ : Transitive′ _≈′_ _≳_
  trans≈′≳ = is-transitive (λ p≈′q → transitive p≈′q ∘ ≳⇒≈′ ∘ convert)

  trans≈≲ : ∀ {i} → Transitive′ [ i ]_≈_ _≲_
  trans≈≲ = is-transitive transitive-≈≲

  trans≈≲′ : ∀ {i} → Transitive′ [ i ]_≈_ _≲′_
  trans≈≲′ = is-transitive (λ p≈q q≲r → transitive-≈≲ p≈q (force q≲r))

  trans≈′≲ : ∀ {i} → Transitive′ [ i ]_≈′_ _≲_
  trans≈′≲ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → [ i ] p ≈′ q → q ≲ r → [ i ] p ≈′ r
    force (lemma p≈′q q≳′r) =
      transitive-≈≲ (force p≈′q) q≳′r

  trans≈′≲′ : ∀ {i} → Transitive′ [ i ]_≈′_ _≲′_
  trans≈′≲′ = is-transitive (λ p≈′q q≲′r →
                transitive′ p≈′q (force q≲′r))

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
open import Data.Product using ( _,_ )
open import Data.Sum using ( _⊎_ )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; _*_ )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ ; _⊨b_ ; *-resp-⟨ABox⟩ )
open import Web.Semantic.DL.Category.Object using ( Object ; _,_ ; IN )
open import Web.Semantic.DL.Category.Morphism using ( _⇒_ ; _,_ ; BN ; impl )
open import Web.Semantic.DL.Category.Tensor using
  ( _⟨⊗⟩_ ; ⊨a-intro-⟨&⟩ ; ⊨b-intro-⟨&⟩ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.Util using ( _⊕_⊕_ ; up ; down )

module Web.Semantic.DL.Category.Properties.Tensor.Lemmas
  {Σ : Signature} {S T : TBox Σ} where

tensor-up : ∀ {A₁ A₂ B₁ B₂ : Object S T} (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) I →
  (I ⊨a impl (F₁ ⟨⊗⟩ F₂)) → (up * I ⊨a impl F₁)
tensor-up {X₁ , X₁∈Fin , A₁} {X₂ , X₂∈Fin , A₂} {Y₁ , Y₁∈Fin , B₁} {Y₂ , Y₂∈Fin , B₂}
  (V₁ , F₁ , F₁✓) (V₂ , F₂ , F₂✓) I (I⊨F₁ , I⊨F₂) = *-resp-⟨ABox⟩ up I F₁ I⊨F₁

tensor-down : ∀ {A₁ A₂ B₁ B₂ : Object S T} (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) I →
  (I ⊨a impl (F₁ ⟨⊗⟩ F₂)) → (down * I ⊨a impl F₂)
tensor-down  {X₁ , X₁∈Fin , A₁} {X₂ , X₂∈Fin , A₂} {Y₁ , Y₁∈Fin , B₁} {Y₂ , Y₂∈Fin , B₂}
  (V₁ , F₁ , F₁✓) (V₂ , F₂ , F₂✓) I (I⊨F₁ , I⊨F₂) = *-resp-⟨ABox⟩ down I F₂ I⊨F₂

tensor-resp-⊨a : ∀ {A₁ A₂ B₁ B₂ : Object S T}
  (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) →
    (I : Interp Σ ((IN A₁ ⊎ IN A₂) ⊕ (BN F₁ ⊎ BN F₂) ⊕ (IN B₁ ⊎ IN B₂))) →
      (up * I ⊨a impl F₁) → (down * I ⊨a impl F₂) → (I ⊨a impl (F₁ ⟨⊗⟩ F₂))
tensor-resp-⊨a  {X₁ , X₁∈Fin , A₁} {X₂ , X₂∈Fin , A₂} {Y₁ , Y₁∈Fin , B₁} {Y₂ , Y₂∈Fin , B₂}
  (V₁ , F₁ , F₁✓) (V₂ , F₂ , F₂✓) I I₁⊨F₁ I₂⊨F₂ =
    ⊨a-intro-⟨&⟩ I F₁ F₂ I₁⊨F₁ I₂⊨F₂

tensor-resp-⊨b : ∀ {A₁ A₂ B₁ B₂ : Object S T} {V₁ V₂ : Set}
  (F₁ : A₁ ⇒ B₁) (F₂ : A₂ ⇒ B₂) →
    (I : Interp Σ ((IN A₁ ⊎ IN A₂) ⊕ (V₁ ⊎ V₂) ⊕ (IN B₁ ⊎ IN B₂))) →
      (up * I ⊨b impl F₁) → (down * I ⊨b impl F₂) → (I ⊨b impl (F₁ ⟨⊗⟩ F₂))
tensor-resp-⊨b  {X₁ , X₁∈Fin , A₁} {X₂ , X₂∈Fin , A₂} {Y₁ , Y₁∈Fin , B₁} {Y₂ , Y₂∈Fin , B₂}
    (V₁ , F₁ , F₁✓) (V₂ , F₂ , F₂✓) I I⊨F₁ I⊨F₂ =
      ⊨b-intro-⟨&⟩ I F₁ F₂ I⊨F₁ I⊨F₂

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


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

module TabsInPragmas where


text:
import      Lvl
open import Structure.Setoid
open import Type

module Automaton.Deterministic.Accessible where

open import Automaton.Deterministic
open import Data.List renaming (∅ to ε ; _⊰_ to _·_)
open import Data.List.Functions using (postpend ; _++_)
open import Logic.Predicate
open import Logic.Predicate.Equiv
open import Sets.ExtensionalPredicateSet using (PredSet ; intro ; _∈_ ; _∋_ ; ⊶ ; [∋]-binaryRelator)
open import Structure.Operator
open import Structure.Relator
open import Structure.Relator.Properties
open import Syntax.Transitivity

private variable ℓₚ ℓₛ ℓₑ₁ ℓₐ ℓₑ₂ : Lvl.Level

module _
  {State : Type{ℓₛ}} ⦃ equiv-state : Equiv{ℓₑ₁}(State) ⦄
  {Alphabet : Type{ℓₐ}} ⦃ equiv-alphabet : Equiv{ℓₑ₂}(Alphabet) ⦄
  where

  module _ (d : Deterministic{ℓₚ = ℓₚ}(State)(Alphabet)) where
    open Deterministic(d)

    -- The subset of State which are the accessible states from the start state by chained transitions.
    Accessible : PredSet(State)
    Accessible = ⊶(wordTransition start)

    instance
      accessible-start : (start ∈ Accessible)
      accessible-start = [∃]-intro ε ⦃ reflexivity(_≡_) {x = start} ⦄

    instance
      accessible-transition : ∀{s}{a} → ⦃ _ : (s ∈ Accessible) ⦄ → (transition s a ∈ Accessible)
      accessible-transition {s} {a = a} ⦃ [∃]-intro w ⦃ p ⦄ ⦄ = [∃]-intro (postpend a w)
        ⦃
          wordTransition start (postpend a w)   🝖-[ wordTransition-postpend {d = d} {start}{w}{a} ]
          transition (wordTransition start w) a 🝖-[ congruence₂ₗ(transition) a p ]
          transition s a                        🝖-end
        ⦄

  module _ where
    open Deterministic

    accessibleAutomaton : (d : Deterministic{ℓₚ = ℓₚ}(State)(Alphabet)) → Deterministic(∃(_∈ Accessible d)) (Alphabet)
    transition (accessibleAutomaton d) ([∃]-intro s) a = [∃]-intro (transition d s a) ⦃ accessible-transition d ⦄
    BinaryOperator.congruence (transition-binaryOperator (accessibleAutomaton d)) = congruence₂(transition d)
    start (accessibleAutomaton d) = [∃]-intro (start d) ⦃ accessible-start d ⦄
    Final (accessibleAutomaton d) PredSet.∋ [∃]-intro s = s ∈ Final d
    UnaryRelator.substitution (PredSet.preserve-equiv (Final (accessibleAutomaton d))) {[∃]-intro x} {[∃]-intro y} = substitute₂ᵣ(_∋_) {intro (_∈ Final d)}

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Data.Char using ( Char )
open import Data.Bool using ( Bool )

module Data.Char.Classifier.Primitive where

postulate
  isAscii  : Char → Bool
  isLatin1 : Char → Bool
  isControl : Char → Bool
  isSpace : Char → Bool
  isLower : Char → Bool
  isUpper : Char → Bool
  isAlpha : Char → Bool
  isAlphaNum : Char → Bool
  isPrint : Char → Bool
  isDigit : Char → Bool
  isOctDigit : Char → Bool
  isHexDigit : Char → Bool

{-# FOREIGN GHC import qualified Data.Char #-}
{-# COMPILE GHC isAscii = type Data.Char.isAscii  #-}
{-# COMPILE GHC isLatin1 = type Data.Char.isLatin1 #-}
{-# COMPILE GHC isControl = type Data.Char.isControl #-}
{-# COMPILE GHC isSpace = type Data.Char.isSpace #-}
{-# COMPILE GHC isLower = type Data.Char.isLower #-}
{-# COMPILE GHC isUpper = type Data.Char.isUpper #-}
{-# COMPILE GHC isAlpha = type Data.Char.isAlpha #-}
{-# COMPILE GHC isAlphaNum = type Data.Char.isAlphaNum #-}
{-# COMPILE GHC isPrint = type Data.Char.isPrint #-}
{-# COMPILE GHC isDigit = type Data.Char.isDigit #-}
{-# COMPILE GHC isOctDigit = type Data.Char.isOctDigit #-}
{-# COMPILE GHC isHexDigit = type Data.Char.isHexDigit #-}

max_stars_repo_name: agda/agda-system-io

max_issues_repo_name: agda/agda-system-io

max_forks_repo_name: agda/agda-system-io


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

open import lib.Basics
open import lib.NType2
open import lib.NConnected
open import lib.types.Truncation
open import lib.types.Group

module lib.types.EilenbergMacLane1.Core {i} where

module _ (G : Group i) where
  private
    module G = Group G

  postulate  -- HIT
    EM₁ : Type i
    embase' : EM₁
    emloop' : G.El → embase' == embase'
    emloop-comp' : ∀ g₁ g₂ → emloop' (G.comp g₁ g₂) == emloop' g₁ ∙ emloop' g₂

  emloop-coh₁' : (g₁ g₂ g₃ : G.El)
    → emloop' (G.comp (G.comp g₁ g₂) g₃) =-= emloop' g₁ ∙ (emloop' g₂ ∙ emloop' g₃)
  emloop-coh₁' g₁ g₂ g₃ =
    emloop' (G.comp (G.comp g₁ g₂) g₃)
      =⟪ emloop-comp' (G.comp g₁ g₂) g₃ ⟫
    emloop' (G.comp g₁ g₂) ∙ emloop' g₃
      =⟪ ap (λ l → l ∙ emloop' g₃) (emloop-comp' g₁ g₂) ⟫
    (emloop' g₁ ∙ emloop' g₂) ∙ emloop' g₃
      =⟪ ∙-assoc (emloop' g₁) (emloop' g₂) (emloop' g₃) ⟫
    emloop' g₁ ∙ (emloop' g₂ ∙ emloop' g₃) ∎∎

  emloop-coh₂' : (g₁ g₂ g₃ : G.El)
    → emloop' (G.comp (G.comp g₁ g₂) g₃) =-= emloop' g₁ ∙ (emloop' g₂ ∙ emloop' g₃)
  emloop-coh₂' g₁ g₂ g₃ =
    emloop' (G.comp (G.comp g₁ g₂) g₃)
      =⟪ ap emloop' (Group.assoc G g₁ g₂ g₃) ⟫
    emloop' (G.comp g₁ (G.comp g₂ g₃))
      =⟪ emloop-comp' g₁ (Group.comp G g₂ g₃) ⟫
    emloop' g₁ ∙ emloop' (G.comp g₂ g₃)
      =⟪ ap (λ l → emloop' g₁ ∙ l) (emloop-comp' g₂ g₃) ⟫
    emloop' g₁ ∙ (emloop' g₂ ∙ emloop' g₃) ∎∎

  postulate
    emloop-coh' : ∀ g₁ g₂ g₃ → emloop-coh₁' g₁ g₂ g₃ =ₛ emloop-coh₂' g₁ g₂ g₃
    EM₁-level' : has-level 2 EM₁

  ⊙EM₁ : Ptd i
  ⊙EM₁ = ⊙[ EM₁ , embase' ]

module _ {G : Group i} where
  private
    module G = Group G

  embase = embase' G
  emloop = emloop' G
  emloop-comp = emloop-comp' G
  emloop-coh₁ = emloop-coh₁' G
  emloop-coh₂ = emloop-coh₂' G
  emloop-coh = emloop-coh' G

  instance
    EM₁-level : {n : ℕ₋₂} → has-level (S (S (S (S n)))) (EM₁ G)
    EM₁-level {⟨-2⟩} = EM₁-level' G
    EM₁-level  {S n} = raise-level _ EM₁-level

  abstract
    -- This was in the original paper, but is actually derivable.
    emloop-ident : emloop G.ident == idp
    emloop-ident = ! $ anti-whisker-right (emloop G.ident) $
      ap emloop (! $ G.unit-r G.ident) ∙ emloop-comp G.ident G.ident

  module EM₁Elim {j} {P : EM₁ G → Type j}
    {{_ : (x : EM₁ G) → has-level 2 (P x)}}
    (embase* : P embase)
    (emloop* : ∀ g → embase* == embase* [ P ↓ emloop g ])
    (emloop-comp* : ∀ g₁ g₂ →
       emloop* (G.comp g₁ g₂) == emloop* g₁ ∙ᵈ emloop* g₂
       [ (λ p → embase* == embase* [ P ↓ p ]) ↓ emloop-comp g₁ g₂ ])
    (emloop-coh* : ∀ g₁ g₂ g₃ →
      emloop-comp* (G.comp g₁ g₂) g₃ ∙ᵈ
      (emloop-comp* g₁ g₂ ∙ᵈᵣ emloop* g₃) ∙ᵈ
      ∙ᵈ-assoc (emloop* g₁) (emloop* g₂) (emloop* g₃)
      ==
      ↓-ap-in (λ p → embase* == embase* [ P ↓ p ]) emloop (apd emloop* (G.assoc g₁ g₂ g₃)) ∙ᵈ
      emloop-comp* g₁ (G.comp g₂ g₃) ∙ᵈ
      (emloop* g₁ ∙ᵈₗ emloop-comp* g₂ g₃)
      [ (λ e → emloop* (G.comp (G.comp g₁ g₂) g₃) == emloop* g₁ ∙ᵈ (emloop* g₂ ∙ᵈ emloop* g₃)
               [ (λ p → embase* == embase* [ P ↓ p ]) ↓ e ])
        ↓ =ₛ-out (emloop-coh g₁ g₂ g₃) ])
    where

    postulate  -- HIT
      f : Π (EM₁ G) P
      embase-β : f embase ↦ embase*
    {-# REWRITE embase-β #-}

    postulate  -- HIT
      emloop-β : (g : G.El) → apd f (emloop g) == emloop* g
      emloop-comp-path : (g₁ g₂ : G.El)
        → apd (apd f) (emloop-comp g₁ g₂) ▹
          apd-∙ f (emloop g₁) (emloop g₂) ∙
          ap2 _∙ᵈ_ (emloop-β g₁) (emloop-β g₂)
          ==
          emloop-β (G.comp g₁ g₂) ◃
          emloop-comp* g₁ g₂

  open EM₁Elim public using () renaming (f to EM₁-elim)

  module EM₁Level₁Elim {j} {P : EM₁ G → Type j}
    {{is-1-type : (x : EM₁ G) → has-level 1 (P x)}}
    (embase* : P embase)
    (emloop* : (g : G.El) → embase* == embase* [ P ↓ emloop g ])
    (emloop-comp* : (g₁ g₂ : G.El) →
      emloop* (G.comp g₁ g₂) == emloop* g₁ ∙ᵈ emloop* g₂
      [ (λ p → embase* == embase* [ P ↓ p ]) ↓ emloop-comp g₁ g₂ ]) where

    private
      module M = EM₁Elim {{λ x → raise-level 1 (is-1-type x)}}
                         embase* emloop* emloop-comp*
                         (λ g₁ g₂ g₃ → prop-has-all-paths-↓ {{↓-level (↓-level (is-1-type embase))}})
    abstract
      f : Π (EM₁ G) P
      f = M.f

      embase-β : f embase ↦ embase*
      embase-β = M.embase-β
      {-# REWRITE embase-β #-}

      emloop-β : (g : G.El) → apd f (emloop g) == emloop* g
      emloop-β = M.emloop-β

  open EM₁Level₁Elim public using () renaming (f to EM₁-level₁-elim)

  module EM₁SetElim {j} {P : EM₁ G → Type j}
    {{is-set : (x : EM₁ G) → is-set (P x)}}
    (embase* : P embase)
    (emloop* : (g : G.El) → embase* == embase* [ P ↓ emloop g ]) where

    private
      module M = EM₁Level₁Elim {P = P} {{λ x → raise-level 0 (is-set x)}}
                               embase* emloop*
                               (λ g₁ g₂ → set-↓-has-all-paths-↓ {{is-set embase}})
    open M public

  open EM₁SetElim public using () renaming (f to EM₁-set-elim)

  module EM₁PropElim {j} {P : EM₁ G → Type j}
    {{is-prop : (x : EM₁ G) → is-prop (P x)}}
    (embase* : P embase) where

    module P = EM₁SetElim {{λ x → raise-level -1 (is-prop x)}}
                          embase*
                          (λ g → prop-has-all-paths-↓ {{is-prop embase}})
    open P public

  open EM₁PropElim public using () renaming (f to EM₁-prop-elim)

-- basic lemmas about [EM₁]

module _ {G : Group i} where
  private
    module G = Group G

  abstract
    emloop-inv : ∀ g → emloop' G (G.inv g) == ! (emloop g)
    emloop-inv g = cancels-inverse _ _ lemma
      where
        cancels-inverse : ∀ {i} {A : Type i} {x y : A}
          (p : x == y) (q : y == x) → p ∙ q == idp → p == ! q
        cancels-inverse p idp r = ! (∙-unit-r p) ∙ r

        lemma : emloop' G (G.inv g) ∙ emloop g  == idp
        lemma = ! (emloop-comp (G.inv g) g) ∙ ap emloop (G.inv-l g) ∙ emloop-ident

    {- EM₁ is 0-connected -}
    instance
      EM₁-conn : is-connected 0 (EM₁ G)
      EM₁-conn = has-level-in ([ embase ] , Trunc-elim
        (EM₁-level₁-elim
          {P = λ x → [ embase ] == [ x ]}
          {{λ _ → raise-level _ (=-preserves-level Trunc-level)}}
          idp
          (λ _ → prop-has-all-paths-↓)
          (λ _ _ → set-↓-has-all-paths-↓)))

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

-- A category where the Homs are not sets, but commutative monoids
-- There are weak kind of Ab-enriched.
-- The reason to do these "by hand" is that the
-- "free commutative monoid monad", i.e. Bag, is very hard to work
-- with in type theory, so it is easier to work axiomatically.

open import Level
open import Algebra.Bundles using (CommutativeMonoid)
open import Function.Base using (flip)
open import Relation.Binary using (Rel; IsEquivalence)

open import Categories.Category.Core using (Category)

record CM-Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  infix  4 _≈_ _⇒_
  infixr 9 _∘_
  infixl 7 _+_

  open CommutativeMonoid using (_∙_; ε) renaming (Carrier to ∣_∣)
  field
    Obj : Set o
    Hom : (A B : Obj) → CommutativeMonoid ℓ e

  _⇒_ : (A B : Obj) → Set ℓ
  A ⇒ B = ∣ Hom A B ∣

  _+_ : {A B : Obj} → A ⇒ B → A ⇒ B → A ⇒ B
  _+_ {A} {B} f g = _∙_ (Hom A B) f g

  0M : {A B : Obj} → A ⇒ B
  0M {A} {B} = ε (Hom A B)

  field
    _≈_ : ∀ {A B : Obj} → Rel (A ⇒ B) e

    id  : ∀ {A} → A ⇒ A
    _∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C

  -- The usual categorical structure
  field
    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    -- We add a symmetric proof of associativity so that the opposite category of the
    -- opposite category is definitionally equal to the original category. See how
    -- `op` is implemented.
    sym-assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    -- We add a proof of "neutral" identity proof, in order to ensure the opposite of
    -- constant functor is definitionally equal to itself.
    identity² : ∀ {A} → id ∘ id {A} ≈ id {A}
    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i

    -- preservation of additive structure
    +-resp-∘ : ∀ {A B C D} {f g : B ⇒ C} {h : A ⇒ B} {k : C ⇒ D} →
      k ∘ (f + g) ∘ h ≈ k ∘ f ∘ h + k ∘ g ∘ h

    0-resp-∘ : ∀ {A C D} {h : A ⇒ C} {k : C ⇒ D} → k ∘ 0M ∘ h ≈ 0M

Underlying : {o ℓ e : Level} → CM-Category o ℓ e → Category o ℓ e
Underlying C = record { CM-Category C }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Nat where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Empty
open import Cubical.Data.Unit

open import Cubical.Relation.Binary

open import Cubical.DStructures.Base

private
  variable
    ℓA ℓ≅A : Level

-- observational equality on ℕ
ℕ-≅ : ℕ → ℕ → Type ℓ-zero
ℕ-≅ 0 0 = Unit
ℕ-≅ 0 (suc _) = ⊥
ℕ-≅ (suc _) 0 = ⊥
ℕ-≅ (suc n) (suc m) = ℕ-≅ n m

-- observational equality is reflexive
ℕ-≅-ρ : isRefl ℕ-≅
ℕ-≅-ρ 0 = tt
ℕ-≅-ρ (suc n) = ℕ-≅-ρ n

-- observational equality implies identity
ℕ-≅→≡ : {n m : ℕ} → ℕ-≅ n m → n ≡ m
ℕ-≅→≡ {0} {0} p = refl
ℕ-≅→≡ {0} {suc _} p = rec p
ℕ-≅→≡ {suc _} {0} p = rec p
ℕ-≅→≡ {suc n} {suc m} p = cong suc (ℕ-≅→≡ {n} {m} p)

-- observational equality is prop-valued
ℕ-≅-prop : (n m : ℕ) → isProp (ℕ-≅ n m)
ℕ-≅-prop 0 0 = isContr→isProp isContrUnit
ℕ-≅-prop 0 (suc _) = isProp⊥
ℕ-≅-prop (suc _) 0 = isProp⊥
ℕ-≅-prop (suc n) (suc m) = ℕ-≅-prop n m

-- This module contains the first half of the proof of
-- theorem 10.2.3 of Egbert Rijkes Intro to Hott
-- TODO: privatize
module _ {A : Type ℓA}
         (_≅_ : A → A → Type ℓ≅A)
         (ρ : (a : A) → a ≅ a)
         (prop : (a a' : A) → isProp (a ≅ a'))
         (f : (a a' : A) → (a ≅ a') → a ≡ a')
 where
    module _ (a : A) where
      φ : (a' : A) (p : a ≡ a') → a ≅ a'
      φ a' p = J (λ b q → a ≅ b) (ρ a) p

      tot-f : Σ[ a' ∈ A ] a ≅ a' → singl a
      tot-f (a' , p) = a' , f a a' p

      tot-φ : singl a → Σ[ a' ∈ A ] a ≅ a'
      tot-φ (a' , p) = a' , (φ a' p)

      ret-f-φ : (a' : A) → retract (f a a') (φ a')
      ret-f-φ a' p = prop a a' (φ a' (f a a' p)) p

      retract-totf-totφ : retract tot-f tot-φ
      retract-totf-totφ (a' , p) = ΣPathP (refl , ret-f-φ a' p)

      contr-singl-≅ : isContr (Σ[ a' ∈ A ] a ≅ a')
      contr-singl-≅ = isContrRetract tot-f tot-φ retract-totf-totφ (isContrSingl a)

ℕ-≅-contrSingl : (n : ℕ) → isContr (Σ[ m ∈ ℕ ] ℕ-≅ n m)
ℕ-≅-contrSingl n = contr-singl-≅ ℕ-≅ ℕ-≅-ρ ℕ-≅-prop (λ m m' → ℕ-≅→≡ {m} {m'}) n

𝒮-Nat : URGStr ℕ ℓ-zero
𝒮-Nat = make-𝒮 {_≅_ = ℕ-≅} ℕ-≅-ρ ℕ-≅-contrSingl


text:
open import SOAS.Common
open import SOAS.Families.Core
open import Categories.Object.Initial
open import SOAS.Coalgebraic.Strength
import SOAS.Metatheory.MetaAlgebra

-- Coalgebraic traversal maps
module SOAS.Metatheory.Coalgebraic {T : Set}
  (⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ) (⅀:Str : Strength ⅀F)
  (𝔛 : Familyₛ) (open SOAS.Metatheory.MetaAlgebra ⅀F 𝔛)
  (𝕋:Init : Initial 𝕄etaAlgebras)
  where

open import SOAS.Context
open import SOAS.Variable
open import SOAS.Abstract.Hom
import SOAS.Abstract.Coalgebra as →□ ; open →□.Sorted
import SOAS.Abstract.Box as □ ; open □.Sorted

open import SOAS.Coalgebraic.Map

open import SOAS.Metatheory.Algebra {T} ⅀F
open import SOAS.Metatheory.Semantics ⅀F ⅀:Str 𝔛 𝕋:Init
open import SOAS.Metatheory.Traversal ⅀F ⅀:Str 𝔛 𝕋:Init
open import SOAS.Metatheory.Renaming ⅀F ⅀:Str 𝔛 𝕋:Init

open Strength ⅀:Str

-- Relationship of traversal and interpretation, assuming 𝒜 has compatible renaming structure
module _ {𝒜 : Familyₛ}(𝒜ᵇ : Coalg 𝒜)(𝒜ᵃ : MetaAlg 𝒜)
         (open Semantics 𝒜ᵃ)(open Coalg 𝒜ᵇ)
         (rᵃ⇒ : MetaAlg⇒ 𝒜ᵃ (□ᵃ 𝒜ᵃ) r) where

  open MetaAlg 𝒜ᵃ
  open MetaAlg⇒ rᵃ⇒

  𝒜ᴮ : Coalgₚ 𝒜
  𝒜ᴮ = record { ᵇ = 𝒜ᵇ ; η = 𝑣𝑎𝑟 ; r∘η = cong (λ - → - _) ⟨𝑣𝑎𝑟⟩ }

  -- Interpretation and renaming commute
  𝕤𝕖𝕞∘ren : MapEq₁ ℐᴮ 𝑎𝑙𝑔 (λ t ρ → 𝕤𝕖𝕞 (𝕣𝕖𝕟 t ρ))
                          (λ t ρ → r (𝕤𝕖𝕞 t) ρ)
  𝕤𝕖𝕞∘ren = record
    { φ = 𝑣𝑎𝑟
    ; χ = 𝑚𝑣𝑎𝑟
    ; f⟨𝑣⟩ = trans (cong 𝕤𝕖𝕞 Renaming.𝕥⟨𝕧⟩) ⟨𝕧⟩
    ; f⟨𝑚⟩ = trans (cong 𝕤𝕖𝕞 Renaming.𝕥⟨𝕞⟩) ⟨𝕞⟩
    ; f⟨𝑎⟩ = λ{ {σ = σ}{t} → begin
          𝕤𝕖𝕞 (𝕣𝕖𝕟 (𝕒𝕝𝕘 t) σ)
      ≡⟨ cong 𝕤𝕖𝕞 Renaming.𝕥⟨𝕒⟩ ⟩
          𝕤𝕖𝕞 (𝕒𝕝𝕘 (str ℐᴮ 𝕋 (⅀₁ 𝕣𝕖𝕟 t) σ))
      ≡⟨ ⟨𝕒⟩ ⟩
          𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 (str ℐᴮ 𝕋 (⅀₁ 𝕣𝕖𝕟 t) σ))
      ≡˘⟨ cong 𝑎𝑙𝑔 (str-nat₂ 𝕤𝕖𝕞 (⅀₁ 𝕣𝕖𝕟 t) σ) ⟩
          𝑎𝑙𝑔 (str ℐᴮ 𝒜 (⅀.F₁ (λ { h′ ς → 𝕤𝕖𝕞 (h′ ς) }) (⅀₁ 𝕣𝕖𝕟 t)) σ)
      ≡˘⟨ congr ⅀.homomorphism (λ - → 𝑎𝑙𝑔 (str ℐᴮ 𝒜 - σ)) ⟩
          𝑎𝑙𝑔 (str ℐᴮ 𝒜 (⅀₁ (λ{ t ρ → 𝕤𝕖𝕞 (𝕣𝕖𝕟 t ρ)}) t) σ)
      ∎ }
    ; g⟨𝑣⟩ = trans (r≈₁ ⟨𝕧⟩) (cong (λ - → - _) ⟨𝑣𝑎𝑟⟩)
    ; g⟨𝑚⟩ = trans (r≈₁ ⟨𝕞⟩) (cong (λ - → - _) ⟨𝑚𝑣𝑎𝑟⟩)
    ; g⟨𝑎⟩ = λ{ {σ = σ}{t} → begin
          r (𝕤𝕖𝕞 (𝕒𝕝𝕘 t)) σ
      ≡⟨ r≈₁ ⟨𝕒⟩ ⟩
          r (𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)) σ
      ≡⟨ cong (λ - → - σ) ⟨𝑎𝑙𝑔⟩ ⟩
          𝑎𝑙𝑔 (str ℐᴮ 𝒜 (⅀₁ r (⅀₁ 𝕤𝕖𝕞 t)) σ)
      ≡˘⟨ congr ⅀.homomorphism (λ - → 𝑎𝑙𝑔 (str ℐᴮ 𝒜 - σ)) ⟩
          𝑎𝑙𝑔 (str ℐᴮ 𝒜 (⅀₁ (λ{ t ρ → r (𝕤𝕖𝕞 t) ρ}) t) σ)
      ∎ }
    } where open ≡-Reasoning

  -- Interpretation is a pointed □-coalgebra homomorphism
  𝕤𝕖𝕞ᵇ⇒ : Coalg⇒ 𝕋ᵇ 𝒜ᵇ 𝕤𝕖𝕞
  𝕤𝕖𝕞ᵇ⇒ = record { ⟨r⟩ = λ{ {t = t} → MapEq₁.≈ 𝕤𝕖𝕞∘ren t } }

  𝕤𝕖𝕞ᴮ⇒ : Coalgₚ⇒ 𝕋ᴮ 𝒜ᴮ 𝕤𝕖𝕞
  𝕤𝕖𝕞ᴮ⇒ = record { ᵇ⇒ = 𝕤𝕖𝕞ᵇ⇒ ; ⟨η⟩ = ⟨𝕧⟩ }

-- Coalgebraic traversal maps
module Travᶜ {𝒫 𝒜 : Familyₛ}(𝒫ᴮ : Coalgₚ 𝒫)(𝑎𝑙𝑔 : ⅀ 𝒜 ⇾̣ 𝒜)
               (φ : 𝒫 ⇾̣ 𝒜)(χ : 𝔛 ⇾̣ 〖 𝒜 , 𝒜 〗) where
  open Coalgₚ 𝒫ᴮ

  open Traversal 𝒫ᴮ 𝑎𝑙𝑔 φ χ

  -- Traversal is derived from 𝕤𝕖𝕞, so it is also a pointed coalgebra homomorphism
  𝕥𝕣𝕒𝕧ᵇ⇒ : Coalg⇒ 𝕋ᵇ Travᵇ 𝕥𝕣𝕒𝕧
  𝕥𝕣𝕒𝕧ᵇ⇒ = 𝕤𝕖𝕞ᵇ⇒ Travᵇ Travᵃ record
    { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → dext² (λ ρ ς → cong 𝑎𝑙𝑔 (str-dist 𝒜 (jᶜ 𝒫ᴮ) t ρ ς)) }
    ; ⟨𝑣𝑎𝑟⟩ = refl ; ⟨𝑚𝑣𝑎𝑟⟩ = refl }

  𝕥𝕣𝕒𝕧ᴮ⇒ : Coalgₚ⇒ 𝕋ᴮ Travᴮ 𝕥𝕣𝕒𝕧
  𝕥𝕣𝕒𝕧ᴮ⇒  = record { ᵇ⇒ = 𝕥𝕣𝕒𝕧ᵇ⇒ ; ⟨η⟩ = ⟨𝕧⟩ }

  -- Assuming 𝒜 is also a pointed □-coalgebra, traversal also commutes with renaming
  module _ (𝒜ᴮ : Coalgₚ 𝒜)(φᴮ : Coalgₚ⇒ 𝒫ᴮ 𝒜ᴮ φ)
           (𝒜rᵃ : MetaAlg⇒ 𝒜ᵃ (□ᵃ 𝒜ᵃ) (Coalgₚ.r 𝒜ᴮ)) where

    private module 𝒜ᴮ = Coalgₚ 𝒜ᴮ
    private module φᴮ = Coalgₚ⇒ φᴮ
    private module 𝒜rᵃ = MetaAlg⇒ 𝒜rᵃ

    -- Renaming and interpretation can commute
    r∘𝕥𝕣𝕒𝕧 : MapEq₂ 𝒫ᴮ ℐᴮ 𝑎𝑙𝑔 (λ t σ ϱ → 𝒜ᴮ.r (𝕥𝕣𝕒𝕧 t σ) ϱ)
                              (λ t σ ϱ → 𝕥𝕣𝕒𝕧 t (λ v → r (σ v) ϱ))
    r∘𝕥𝕣𝕒𝕧 = record
      { φ = 𝒜ᴮ.η
      ; ϕ = λ v → 𝒜ᴮ.r (φ v)
      ; χ = χ
      ; f⟨𝑣⟩ = 𝒜ᴮ.r≈₁ 𝕥⟨𝕧⟩
      ; f⟨𝑚⟩ = trans (𝒜ᴮ.r≈₁ 𝕥⟨𝕞⟩) (cong (λ - → - _) 𝒜rᵃ.⟨𝑚𝑣𝑎𝑟⟩)
      ; f⟨𝑎⟩ = λ{ {σ = σ}{ϱ}{t} → begin
            𝒜ᴮ.r (𝕥𝕣𝕒𝕧 (𝕒𝕝𝕘 t) σ) ϱ
        ≡⟨ 𝒜ᴮ.r≈₁ 𝕥⟨𝕒⟩ ⟩
            𝒜ᴮ.r (𝑎𝑙𝑔 (str 𝒫ᴮ 𝒜 (⅀₁ 𝕥𝕣𝕒𝕧 t) σ)) ϱ
        ≡⟨ cong (λ - → - ϱ) 𝒜rᵃ.⟨𝑎𝑙𝑔⟩ ⟩
            𝑎𝑙𝑔 (str ℐᴮ 𝒜 (⅀.F₁ 𝒜ᴮ.r (str 𝒫ᴮ 𝒜 (⅀.F₁ 𝕥𝕣𝕒𝕧 t) σ)) ϱ)
        ≡˘⟨ congr (str-nat₂ 𝒜ᴮ.r (⅀.F₁ 𝕥𝕣𝕒𝕧 t) σ) (λ - → 𝑎𝑙𝑔 (str ℐᴮ 𝒜 - ϱ)) ⟩
            𝑎𝑙𝑔 (str ℐᴮ 𝒜 (str 𝒫ᴮ (□ 𝒜) (⅀.F₁ (λ { h ς → 𝒜ᴮ.r (h ς) }) (⅀.F₁ 𝕥𝕣𝕒𝕧 t)) σ) ϱ)
        ≡˘⟨ congr ⅀.homomorphism (λ - → 𝑎𝑙𝑔 (str ℐᴮ 𝒜 (str 𝒫ᴮ (□ 𝒜) - σ)  ϱ)) ⟩
            𝑎𝑙𝑔 (str ℐᴮ 𝒜 (str 𝒫ᴮ (□ 𝒜) (⅀₁ (λ{ t σ → 𝒜ᴮ.r (𝕥𝕣𝕒𝕧 t σ)}) t) σ)  ϱ)
        ∎ }
      ; g⟨𝑣⟩ = trans 𝕥⟨𝕧⟩ φᴮ.⟨r⟩
      ; g⟨𝑚⟩ = 𝕥⟨𝕞⟩
      ; g⟨𝑎⟩ = λ{ {σ = σ}{ϱ}{t} → begin
            𝕥𝕣𝕒𝕧 (𝕒𝕝𝕘 t) (λ x → r (σ x) ϱ)
        ≡⟨ 𝕥⟨𝕒⟩ ⟩
            𝑎𝑙𝑔 (str 𝒫ᴮ 𝒜 (⅀₁ 𝕥𝕣𝕒𝕧 t) (λ x → r (σ x) ϱ))
        ≡⟨ cong 𝑎𝑙𝑔 (str-dist 𝒜 (rᶜ 𝒫ᴮ) (⅀₁ 𝕥𝕣𝕒𝕧 t) σ ϱ) ⟩
            𝑎𝑙𝑔 (str ℐᴮ 𝒜 (str 𝒫ᴮ (□ 𝒜) (⅀.F₁ (precomp 𝒜 r) (⅀₁ 𝕥𝕣𝕒𝕧 t)) σ) ϱ)
        ≡˘⟨ congr ⅀.homomorphism (λ - → 𝑎𝑙𝑔 (str ℐᴮ 𝒜 (str 𝒫ᴮ (□ 𝒜) - σ) ϱ)) ⟩
            𝑎𝑙𝑔 (str ℐᴮ 𝒜  (str 𝒫ᴮ (□ 𝒜) (⅀₁ (λ{ t σ ϱ → 𝕥𝕣𝕒𝕧 t (λ v → r (σ v) ϱ)}) t) σ) ϱ)
        ∎ }
      } where open ≡-Reasoning

    -- The traversal map 𝕋 ⇾ 〖𝒫, 𝒜〗 is pointed coalgebraic if 𝒜 has coalgebra structure
    𝕥𝕣𝕒𝕧ᶜ : Coalgebraic 𝕋ᴮ 𝒫ᴮ 𝒜ᴮ 𝕥𝕣𝕒𝕧
    𝕥𝕣𝕒𝕧ᶜ = record { r∘f = λ{ {σ = σ}{ϱ}{t = t} → MapEq₂.≈ r∘𝕥𝕣𝕒𝕧 t }
                  ; f∘r = λ{ {ρ = ρ}{ς}{t = t} → cong (λ - → - ς) (Coalg⇒.⟨r⟩ 𝕥𝕣𝕒𝕧ᵇ⇒ {ρ = ρ}{t = t}) }
                  ; f∘η = trans 𝕥⟨𝕧⟩ φᴮ.⟨η⟩ }


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Bool.SwitchStatement where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Bool.Base
open import Cubical.Data.Nat

{-
  Switch-case:

    _==_ : A → A → Bool

    _ : B
    _ = switch (λ x → x == fixedValue) cases
           case value1 ⇒ result1 break
           case value2 ⇒ result2 break
           ...
           case valueN ⇒ resultN break
           default⇒ defaultResult
-}

private
  variable
    ℓ ℓ′ : Level

infixr 6 default⇒_
infixr 5 case_⇒_break_
infixr 4 switch_cases_

switch_cases_ : {A : Type ℓ} {B : Type ℓ′} → (A → Bool) → ((A → Bool) → B) → B
switch caseIndicator cases caseData = caseData caseIndicator

case_⇒_break_ : {A : Type ℓ} {B : Type ℓ′} → A → B → (otherCases : (A → Bool) → B) → (A → Bool) → B
case forValue ⇒ result break otherCases = λ caseIndicator → if (caseIndicator forValue) then result else (otherCases caseIndicator)

default⇒_ : {A : Type ℓ} {B : Type ℓ′} → B → (A → Bool) → B
default⇒_ value caseIndicator = value

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical