text:
module Data.Fin.Subset.Properties.Cardinality where

open import Data.Nat as ℕ using (ℕ)
open import Data.Nat.Properties as NP
open import Data.Empty using (⊥-elim)
open import Data.Fin
open import Data.Fin.Subset
open import Data.Fin.Subset.Properties
open import Data.Vec using (_∷_; [])
open import Data.Vec.Any  using (here ; there)
open import Data.Vec.Properties as VP
open import Data.Product
open import Data.Sum
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq
open import Relation.Nullary.Negation

open import Function
-- some trivial lemma

∣p∣≡0→≡⊥  : ∀ {n}(p : Subset n) → ∣ p ∣ ≡ 0 → p ≡ ⊥
∣p∣≡0→≡⊥ {ℕ.zero} [] refl = refl
∣p∣≡0→≡⊥ {ℕ.suc n} (outside ∷ p) eq = cong (outside ∷_) (∣p∣≡0→≡⊥ p eq)
∣p∣≡0→≡⊥ {ℕ.suc n} (inside ∷ p) ()

∣p∣≡n→≡⊤  : ∀ {n}(p : Subset n) → ∣ p ∣ ≡ n → p ≡ ⊤
∣p∣≡n→≡⊤ {ℕ.zero} [] refl = refl
∣p∣≡n→≡⊤ {ℕ.suc n} (outside ∷ p) eq = ⊥-elim (1+n≰n (≤-respˡ-≈ eq (∣p∣≤n p)))
  where
    open IsPartialOrder NP.≤-isPartialOrder using (≤-respˡ-≈)
∣p∣≡n→≡⊤ {ℕ.suc n} (inside ∷ p) eq = cong (inside ∷_) (∣p∣≡n→≡⊤ p (NP.suc-injective eq))

∣p∣≡1→≡⁅x⁆ : ∀ {n}(p : Subset n) → ∣ p ∣ ≡ 1 → ∃ λ x → p ≡ ⁅ x ⁆
∣p∣≡1→≡⁅x⁆ {ℕ.zero} [] ()
∣p∣≡1→≡⁅x⁆ {ℕ.suc n} (outside ∷ p) eq with ∣p∣≡1→≡⁅x⁆ p eq
... | x , q = suc x , cong (outside ∷_) q
∣p∣≡1→≡⁅x⁆ {ℕ.suc n} (inside ∷ p) eq rewrite ∣p∣≡0→≡⊥ p (NP.suc-injective eq) = zero , refl

-- union

≤∪ˡ : ∀ {n} {p} (q : Subset n) → ∣ p ∣ ℕ.≤  ∣ p ∪ q ∣
≤∪ˡ {n}{p} q = p⊆q⇒∣p∣<∣q∣ (p⊆p∪q {p = p} q)
≤∪ʳ : ∀ {n} (p q : Subset n) → ∣ q ∣ ℕ.≤  ∣ p ∪ q ∣
≤∪ʳ p q =  p⊆q⇒∣p∣<∣q∣ (q⊆p∪q p q)

∪≤ : ∀ {n} (p q : Subset n) → ∣ p ∪ q ∣ ℕ.≤ ∣ p ∣ ℕ.+ ∣ q ∣
∪≤ {ℕ.zero} [] [] = ℕ.z≤n
∪≤ {ℕ.suc n} (outside ∷ p) (outside ∷ q) = ∪≤ p q
∪≤ {ℕ.suc n} (outside ∷ p) (inside ∷ q) rewrite +-suc ∣ p ∣ ∣ q ∣ = ℕ.s≤s (∪≤ p q)
∪≤ {ℕ.suc n} (inside ∷ p) (outside ∷ q) = ℕ.s≤s (∪≤ p q)
∪≤ {ℕ.suc n} (inside ∷ p) (inside ∷ q) = ℕ.s≤s (NP.≤-trans (∪≤ p q) (NP.+-mono-≤ (≤-refl {∣ p ∣}) (n≤1+n _)))

disjoint-∪≡+ : ∀ {n} (p q : Subset n) → p ∩ q ≡ ⊥ → ∣ p ∪ q ∣ ≡ ∣ p ∣ ℕ.+ ∣ q ∣
disjoint-∪≡+ {ℕ.zero} [] [] refl = refl
disjoint-∪≡+ {ℕ.suc n} (outside ∷ p) (outside ∷ q) dis = disjoint-∪≡+ p q (VP.∷-injectiveʳ dis)
disjoint-∪≡+ {ℕ.suc n} (outside ∷ p) (inside ∷ q) dis =
  Eq.trans (Eq.cong ℕ.suc (disjoint-∪≡+ p q (VP.∷-injectiveʳ dis))) (Eq.sym (NP.+-suc _ _))
disjoint-∪≡+ {ℕ.suc n} (inside ∷ p) (outside ∷ q) dis = Eq.cong ℕ.suc (disjoint-∪≡+ p q (VP.∷-injectiveʳ dis))
disjoint-∪≡+ {ℕ.suc n} (inside ∷ p) (inside ∷ q) ()

x∈p⇒⁅x⁆∪p≡p : ∀ {n} (x : Fin n)(p : Subset n) → x ∈ p → ⁅ x ⁆ ∪ p ≡ p
x∈p⇒⁅x⁆∪p≡p x p x∈p = ⊆-antisym from to
  where
    from : ∀ {y} → y ∈ ⁅ x ⁆ ∪ p → y ∈ p
    from h with x∈p∪q⁻ ⁅ x ⁆ p h
    from h | inj₁ y∈⁅x⁆ rewrite x∈⁅y⁆⇒x≡y _ y∈⁅x⁆ = x∈p
    from h | inj₂ y∈p = y∈p

    to : ∀ {y}  → y ∈ p → y ∈ ⁅ x ⁆ ∪ p
    to h = x∈p∪q⁺ (inj₂ h)

∣⁅x⁆∪p∣≡1+∣p∣⇒x∉p : ∀ {n}(x : Fin n)(p : Subset n) → ∣ ⁅ x ⁆ ∪ p  ∣ ≡ 1 ℕ.+ ∣ p ∣ →  x ∉ p
∣⁅x⁆∪p∣≡1+∣p∣⇒x∉p x p h x∈p rewrite x∈p⇒⁅x⁆∪p≡p x p x∈p = contradiction h lemma
  where
    lemma : ∀ {n} → n ≢ ℕ.suc n
    lemma ()

∣⁅x⁆∪⁅y⁆∣≡2⇒x≢y : ∀ {n}(x y : Fin n) → ∣ ⁅ x ⁆ ∪ ⁅ y ⁆  ∣ ≡ 2 →  x ≢ y
∣⁅x⁆∪⁅y⁆∣≡2⇒x≢y x .x h refl with ∣⁅x⁆∪p∣≡1+∣p∣⇒x∉p x ⁅ x ⁆ (trans h (cong ℕ.suc (sym (∣⁅x⁆∣≡1 x))))
... | x∉⁅y⁆ = contradiction (x∈⁅x⁆ _) x∉⁅y⁆

module _ {n : ℕ} where
  open import Algebra.Structures {A = Subset n} _≡_
  open IsBooleanAlgebra (∪-∩-isBooleanAlgebra n) renaming (∧-complementʳ to ∩-complementʳ; ∨-complementʳ to ∪-complementʳ)
  ∣p∣+∣∁p∣≡n : ∀ (p : Subset n) → ∣ p ∣  ℕ.+ ∣ ∁ p ∣ ≡ n
  ∣p∣+∣∁p∣≡n p = ∣ p ∣  ℕ.+ ∣ ∁ p ∣
                     ≡⟨ Eq.sym (disjoint-∪≡+ _ _ (∩-complementʳ p)) ⟩ _
                     ≡⟨ Eq.cong ∣_∣ (∪-complementʳ p) ⟩ _
                     ≡⟨ ∣⊤∣≡n _ ⟩ n ∎
    where
      open Eq.≡-Reasoning

∩≤ˡ : ∀ {n} (a b : Subset n) → ∣ a ∩ b ∣  ℕ.≤  ∣ a ∣
∩≤ˡ {n} a b = p⊆q⇒∣p∣<∣q∣ (p∩q⊆p a b)

∩≤ʳ : ∀ {n} (a b : Subset n) → ∣ a ∩ b ∣  ℕ.≤  ∣ b ∣
∩≤ʳ {n} a b = p⊆q⇒∣p∣<∣q∣ (p∩q⊆q a b)

∣p∣<∣q∣⇒∣∁q∣<∣∁p∣ : ∀ {n} (p q : Subset n) → ∣ p ∣ ℕ.< ∣ q ∣ → ∣ ∁ q ∣ ℕ.< ∣ ∁ p ∣
∣p∣<∣q∣⇒∣∁q∣<∣∁p∣ p q p<q = NP.+-cancelˡ-< ∣ q ∣
  (begin-strict ∣ q ∣ ℕ.+ ∣ ∁ q ∣ ≡⟨ ∣p∣+∣∁p∣≡n q ⟩ _ ≡⟨ sym (∣p∣+∣∁p∣≡n p) ⟩ ∣ p ∣ ℕ.+ ∣ ∁ p ∣ <⟨ NP.+-monoˡ-< _ p<q ⟩  ∣ q ∣ ℕ.+ ∣ ∁ p ∣ ∎)
  where
    open NP.≤-Reasoning
-- intersection
{-

private
  open import Relation.Nullary.Negation using (contraposition)
  p∩∁q≡⊥→p⊆q :  ∀ {n} {p q : Subset n} → p ∩ ∁ q ≡ ⊥ → p ⊆ q
  p∩∁q≡⊥→p⊆q {zero} {[]} {[]} refl ()
  p∩∁q≡⊥→p⊆q {suc n} {true ∷ p} {outside ∷ q} () here
  p∩∁q≡⊥→p⊆q {suc n} {inside ∷ p} {inside ∷ q} eq here = here
  p∩∁q≡⊥→p⊆q {suc n} {true ∷ p} {_ ∷ q} eq (there x∈p) with ∷-injective eq
  ... | _ , teq = there (p∩∁q≡⊥→p⊆q teq x∈p)
  p∩∁q≡⊥→p⊆q {suc n} {outside ∷ p} {_ ∷ q} eq (there x∈p) with ∷-injective eq
  ... | _ , teq = there (p∩∁q≡⊥→p⊆q teq x∈p)

  p∩q≡p→p⊆q : ∀ {n} {p q : Subset n} → p ∩ q ≡ p → p ⊆ q
  p∩q≡p→p⊆q {zero} {[]} {[]} refl ()
  p∩q≡p→p⊆q {suc n} {inside ∷ p} {x ∷ q} eq here with ∷-injective eq
  p∩q≡p→p⊆q {suc n} {inside ∷ p} {.inside ∷ q} eq here | refl , _ = here
  p∩q≡p→p⊆q {suc n} {inside ∷ p} {_ ∷ q} eq (there x∈p) with ∷-injective eq
  ... | _ , teq = there (p∩q≡p→p⊆q teq x∈p)
  p∩q≡p→p⊆q {suc n} {outside ∷ p} {_ ∷ q} eq (there x∈p) with ∷-injective eq
  ... | _ , teq = there (p∩q≡p→p⊆q teq x∈p)
  p⊈q→p∩q≢p : ∀ {n} {p q : Subset n} → p ⊈ q → p ∩ q ≢ p
  p⊈q→p∩q≢p = contraposition p∩q≡p→p⊆q

  split-size : ∀ {n} {a} (b : Subset n) → ∣ a ∣ ≡ ∣ a ∩ b ∣ ℕ.+ ∣ a ∩ ∁ b ∣
  split-size {n}{a} b = ∣a∣≡∣a∩b∣+∣a∩∁b∣
    where
      open P.≡-Reasoning
      a∩b∩a∩∁b≡⊥ : (a ∩ b) ∩ (a ∩ ∁ b) ≡ ⊥
      a∩b∩a∩∁b≡⊥ = begin
                   (a ∩ b) ∩ (a ∩ ∁ b) ≡⟨ ∩-assoc _ _ _ ⟩ _
                                       ≡⟨ cong (a ∩_ ) (sym (∩-assoc _ _ _)) ⟩ _
                                       ≡⟨ cong (a ∩_ ) (cong (_∩ _) (∩-comm _ _)) ⟩ _
                                       ≡⟨ cong (a ∩_ ) (∩-assoc _ _ _) ⟩ _
                                       ≡⟨ cong (a ∩_ ) (cong (a ∩_) (∩-complementʳ _)) ⟩ _
                                       ≡⟨ cong (a ∩_ ) (∩-zeroʳ _) ⟩ _
                                       ≡⟨ ∩-zeroʳ _ ⟩ ⊥
                   ∎
      a≡a∩b∪a∩∁b : a ≡ (a ∩ b) ∪ (a ∩ ∁ b)
      a≡a∩b∪a∩∁b = begin
                     a ≡⟨ sym (∩-identityʳ _) ⟩ a ∩ ⊤
                       ≡⟨ cong (_ ∩_) (sym (∪-complementʳ _)) ⟩ a ∩ (b ∪ ∁ b)
                       ≡⟨ (proj₁ ∪-∩-distrib) _ _ _  ⟩ (a ∩ b) ∪ (a ∩ ∁ b)
                   ∎
      ∣a∣≡∣a∩b∣+∣a∩∁b∣ : ∣ a ∣ ≡ ∣ a ∩ b ∣ ℕ.+ ∣ a ∩ ∁ b ∣
      ∣a∣≡∣a∩b∣+∣a∩∁b∣ = begin
                         ∣ a ∣ ≡⟨ cong size a≡a∩b∪a∩∁b ⟩ ∣ (a ∩ b) ∪ (a ∩ ∁ b) ∣
                              ≡⟨ disjoint-∪≡ a∩b∩a∩∁b≡⊥ ⟩  ∣ a ∩ b ∣ ℕ.+ ∣ a ∩ ∁ b ∣
                      ∎

  ⊈→∩<ˡ : ∀ {n} {a b : Subset n} → a ⊈ b → ∣ a ∩ b ∣ ℕ.< ∣ a ∣
  ⊈→∩<ˡ {n}{a}{b} a⊈b = ≤+≢⇒< (∩≤ˡ a b) lemma
    where
      open P.≡-Reasoning

      n+m≡n→m≡0 : ∀ {n m} → n ℕ.+ m ≡ n → m ≡ 0
      n+m≡n→m≡0 {n}{m} eq = +-cancelˡ-≡ n (P.trans eq (sym (+-identityʳ n)))

      lemma : ∣ a ∩ b ∣ ≢ ∣ a ∣
      lemma eq = (contraposition p∩∁q≡⊥→p⊆q a⊈b) (size0 (n+m≡n→m≡0 (sym (P.trans eq (split-size b)))))
-}

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


text:
module _ where

open import Agda.Builtin.Nat
open import Imports.ImportedDisplayForms

postulate
  T : Nat → Set

foo : (a : Nat) → T (a + a)
foo a = {!!}

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Oscar.Prelude
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Smap
open import Oscar.Class.Surjextensionality
open import Oscar.Class.Symmetry
open import Oscar.Class.Symmetrical
open import Oscar.Class.Transitivity
open import Oscar.Data.ProductIndexEquivalence
open import Oscar.Data.Surjextenscollation
import Oscar.Class.HasEquivalence.ExtensionṖroperty
import Oscar.Class.Surjection.⋆
import Oscar.Data.ExtensionṖroperty
import Oscar.Data.Proposequality

module Oscar.Class.Symmetrical.ExtensionalUnifies where

module _
    {𝔵} {𝔛 : Ø 𝔵}
    {𝔞} {𝔄 : 𝔛 → Ø 𝔞}
    {𝔟} {𝔅 : 𝔛 → Ø 𝔟}
    (let _↦_ = Arrow 𝔄 𝔅)
    {𝔠} {ℭ : 𝔛 → Ø 𝔠}
    {ℓ₁} {_↦̇_ : ∀ {x y} → x ↦ y → x ↦ y → Ø ℓ₁}
    {ℓ₂} {_∼₂_ : ∀ {y} → ℭ y → ℭ y → Ø ℓ₂}
    ⦃ _ : ∀ {y} → Symmetry.class (_∼₂_ {y}) ⦄
    ⦃ _ : ∀ {y} → Transitivity.class (_∼₂_ {y}) ⦄
    ⦃ _ : Smap!.class _↦_ (Extension ℭ) ⦄
    ⦃ _ : Surjextensionality!.class _↦_ _↦̇_ (Extension ℭ) (Pointwise _∼₂_) ⦄
  where

  instance

    𝓢ymmetricalExtensionalUnifies : ∀ {m} → Symmetrical {𝔄 = (ℭ m)} {𝔅 = (LeftExtensionṖroperty ℓ₂ _↦_ _↦̇_ m)} surjextenscollation⟦ _↦̇_ ⟧ _≈_
    𝓢ymmetricalExtensionalUnifies .𝓢ymmetrical.symmetrical x y .π₀ = ∁ (symmetry , symmetry)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.AbGroup.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Reflection.StrictEquiv
open import Cubical.Structures.Axioms
open import Cubical.Structures.Macro
open import Cubical.Structures.Pointed
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Group

open Iso

private
  variable
    ℓ ℓ' : Level

record IsAbGroup {G : Type ℓ}
                 (0g : G) (_+_ : G → G → G) (-_ : G → G) : Type ℓ where

  constructor isabgroup

  field
    isGroup : IsGroup 0g _+_ -_
    comm    : (x y : G) → x + y ≡ y + x

  open IsGroup isGroup public

record AbGroupStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor abgroupstr

  field
    0g        : A
    _+_       : A → A → A
    -_        : A → A
    isAbGroup : IsAbGroup 0g _+_ -_

  infix  8 -_
  infixr 7 _+_

  open IsAbGroup isAbGroup public

AbGroup : Type (ℓ-suc ℓ)
AbGroup = TypeWithStr _ AbGroupStr

makeIsAbGroup : {G : Type ℓ} {0g : G} {_+_ : G → G → G} { -_ : G → G}
              (is-setG : isSet G)
              (assoc   : (x y z : G) → x + (y + z) ≡ (x + y) + z)
              (rid     : (x : G) → x + 0g ≡ x)
              (rinv    : (x : G) → x + (- x) ≡ 0g)
              (comm    : (x y : G) → x + y ≡ y + x)
            → IsAbGroup 0g _+_ -_
makeIsAbGroup is-setG assoc rid rinv comm =
  isabgroup (makeIsGroup is-setG assoc rid (λ x → comm _ _ ∙ rid x) rinv (λ x → comm _ _ ∙ rinv x)) comm

makeAbGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
            (is-setG : isSet G)
            (assoc : (x y z : G) → x + (y + z) ≡ (x + y) + z)
            (rid : (x : G) → x + 0g ≡ x)
            (rinv : (x : G) → x + (- x) ≡ 0g)
            (comm    : (x y : G) → x + y ≡ y + x)
          → AbGroup
makeAbGroup 0g _+_ -_ is-setG assoc rid rinv comm =
  _ , abgroupstr 0g _+_ -_ (makeIsAbGroup is-setG assoc rid rinv comm)

open GroupStr
AbGroup→Group : AbGroup {ℓ} → Group
fst (AbGroup→Group A) = fst A
0g (snd (AbGroup→Group A)) = AbGroupStr.0g (snd A)
_+_ (snd (AbGroup→Group A)) = AbGroupStr._+_ (snd A)
- snd (AbGroup→Group A) = AbGroupStr.- (snd A)
isGroup (snd (AbGroup→Group A)) = IsAbGroup.isGroup (AbGroupStr.isAbGroup (snd A))

Group→AbGroup : (G : Group {ℓ}) → ((x y : fst G) → _+_ (snd G) x y ≡ _+_ (snd G) y x) → AbGroup
fst (Group→AbGroup G comm) = fst G
AbGroupStr.0g (snd (Group→AbGroup G comm)) = 0g (snd G)
AbGroupStr._+_ (snd (Group→AbGroup G comm)) = _+_ (snd G)
AbGroupStr.- snd (Group→AbGroup G comm) = - (snd G)
IsAbGroup.isGroup (AbGroupStr.isAbGroup (snd (Group→AbGroup G comm))) = isGroup (snd G)
IsAbGroup.comm (AbGroupStr.isAbGroup (snd (Group→AbGroup G comm))) = comm

isSetAbGroup : (A : AbGroup {ℓ}) → isSet ⟨ A ⟩
isSetAbGroup A = isSetGroup (AbGroup→Group A)

AbGroupHom : (G : AbGroup {ℓ}) (H : AbGroup {ℓ'}) → Type (ℓ-max ℓ ℓ')
AbGroupHom G H = GroupHom (AbGroup→Group G) (AbGroup→Group H)

AbGroupEquiv : (G : AbGroup {ℓ}) (H : AbGroup {ℓ'}) → Type (ℓ-max ℓ ℓ')
AbGroupEquiv G H = GroupEquiv (AbGroup→Group G) (AbGroup→Group H)

module AbGroupΣTheory {ℓ} where

  open GroupΣTheory

  AbGroupAxioms : (G : Type ℓ) → RawGroupStructure G → Type ℓ
  AbGroupAxioms G _+_ = GroupAxioms G _+_ × ((x y : G) → x + y ≡ y + x)

  AbGroupStructure : Type ℓ → Type ℓ
  AbGroupStructure = AxiomsStructure RawGroupStructure AbGroupAxioms

  AbGroupΣ : Type (ℓ-suc ℓ)
  AbGroupΣ = TypeWithStr ℓ AbGroupStructure

  isSetAbGroupΣ : (A : AbGroupΣ) → isSet _
  isSetAbGroupΣ (A , _+_ , (isGroup-A , _)) = isSetGroupΣ (A , _+_ , isGroup-A)

  AbGroupEquivStr : StrEquiv AbGroupStructure ℓ
  AbGroupEquivStr = AxiomsEquivStr RawGroupEquivStr AbGroupAxioms

  isPropAbGroupAxioms : (G : Type ℓ) (s : RawGroupStructure G)
                      → isProp (AbGroupAxioms G s)
  isPropAbGroupAxioms G _+_ =
    isPropΣ (isPropGroupAxioms G _+_)
            λ { (H , _) → isPropΠ2 λ _ _ → IsSemigroup.is-set H _ _}

  AbGroup→AbGroupΣ : AbGroup → AbGroupΣ
  AbGroup→AbGroupΣ (_ , abgroupstr _ _ _ (isabgroup G C)) =
    _ , _ , Group→GroupΣ (group _ _ _ _ G) .snd .snd , C

  AbGroupΣ→AbGroup : AbGroupΣ → AbGroup
  AbGroupΣ→AbGroup (_ , _ , G , C) =
    _ , abgroupstr _ _ _ (isabgroup (GroupΣ→Group (_ , _ , G) .snd .GroupStr.isGroup) C)

  open AbGroupStr

  AbGroupIsoAbGroupΣ : Iso AbGroup AbGroupΣ
  AbGroupIsoAbGroupΣ = iso AbGroup→AbGroupΣ AbGroupΣ→AbGroup (λ _ → refl) (λ _ → refl)

  abGroupUnivalentStr : UnivalentStr AbGroupStructure AbGroupEquivStr
  abGroupUnivalentStr = axiomsUnivalentStr _ isPropAbGroupAxioms rawGroupUnivalentStr

  AbGroupΣPath : (G H : AbGroupΣ) → (G ≃[ AbGroupEquivStr ] H) ≃ (G ≡ H)
  AbGroupΣPath = SIP abGroupUnivalentStr

  AbGroupEquivΣ : (G H : AbGroup) → Type ℓ
  AbGroupEquivΣ G H = AbGroup→AbGroupΣ G ≃[ AbGroupEquivStr ] AbGroup→AbGroupΣ H

  AbGroupPath : (G H : AbGroup) → (AbGroupEquiv G H) ≃ (G ≡ H)
  AbGroupPath G H =
    AbGroupEquiv G H                        ≃⟨ strictIsoToEquiv GroupIsoΣPath ⟩
    AbGroupEquivΣ G H                       ≃⟨ AbGroupΣPath _ _ ⟩
    AbGroup→AbGroupΣ G ≡ AbGroup→AbGroupΣ H ≃⟨ isoToEquiv (invIso (congIso AbGroupIsoAbGroupΣ)) ⟩
    G ≡ H ■

  AbGroup→RawGroupΣ : AbGroup {ℓ} → RawGroupΣ
  AbGroup→RawGroupΣ (G , abgroupstr _ _+_ _ _) = G , _+_

  InducedAbGroup : (G : AbGroup) (H : RawGroupΣ) (e : ⟨ G ⟩ ≃ H .fst)
                 → RawGroupEquivStr (AbGroup→RawGroupΣ G) H e → AbGroup
  InducedAbGroup G H e r =
    AbGroupΣ→AbGroup (inducedStructure rawGroupUnivalentStr (AbGroup→AbGroupΣ G) H (e , r))

  InducedAbGroupPath : (G : AbGroup {ℓ}) (H : RawGroupΣ) (e : ⟨ G ⟩ ≃ H .fst)
                       (E : RawGroupEquivStr (AbGroup→RawGroupΣ G) H e)
                     → G ≡ InducedAbGroup G H e E
  InducedAbGroupPath G H e E =
    AbGroupPath G (InducedAbGroup G H e E) .fst (groupequiv e E)

-- Extract the characterization of equality of groups
AbGroupPath : (G H : AbGroup {ℓ}) → (AbGroupEquiv G H) ≃ (G ≡ H)
AbGroupPath = AbGroupΣTheory.AbGroupPath

isPropIsAbGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (- : G → G)
                → isProp (IsAbGroup 0g _+_ -)
isPropIsAbGroup 0g _+_ -_ (isabgroup GG GC) (isabgroup HG HC) =
  λ i → isabgroup (isPropIsGroup _ _ _ GG HG i) (isPropComm GC HC i)
  where
  isSetG : isSet _
  isSetG = GG .IsGroup.isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropComm : isProp ((x y : _) → x + y ≡ y + x)
  isPropComm = isPropΠ2 λ _ _ → isSetG _ _

InducedAbGroup : (G : AbGroup {ℓ}) (H : GroupΣTheory.RawGroupΣ) (e : ⟨ G ⟩ ≃ H .fst)
               → GroupΣTheory.RawGroupEquivStr (AbGroupΣTheory.AbGroup→RawGroupΣ G) H e
               → AbGroup
InducedAbGroup = AbGroupΣTheory.InducedAbGroup

InducedAbGroupPath : (G : AbGroup {ℓ}) (H : GroupΣTheory.RawGroupΣ) (e : ⟨ G ⟩ ≃ H .fst)
                     (E : GroupΣTheory.RawGroupEquivStr (AbGroupΣTheory.AbGroup→RawGroupΣ G) H e)
                   → G ≡ InducedAbGroup G H e E
InducedAbGroupPath = AbGroupΣTheory.InducedAbGroupPath

open IsMonoid
open IsSemigroup
open IsGroup
open AbGroupStr
open IsAbGroup

dirProdAb : AbGroup {ℓ} → AbGroup {ℓ'} → AbGroup
dirProdAb A B =
  Group→AbGroup (dirProd (AbGroup→Group A) (AbGroup→Group B))
                 λ p q → ΣPathP (comm (isAbGroup (snd A)) _ _
                                , comm (isAbGroup (snd B)) _ _)

trivialAbGroup : ∀ {ℓ} → AbGroup {ℓ}
fst trivialAbGroup = Unit*
0g (snd trivialAbGroup) = tt*
_+_ (snd trivialAbGroup) _ _ = tt*
(- snd trivialAbGroup) _ = tt*
is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd trivialAbGroup))))) =
  isProp→isSet isPropUnit*
assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd trivialAbGroup))))) _ _ _ = refl
identity (isMonoid (isGroup (isAbGroup (snd trivialAbGroup)))) _ = refl , refl
inverse (isGroup (isAbGroup (snd trivialAbGroup))) _ = refl , refl
comm (isAbGroup (snd trivialAbGroup)) _ _ = refl

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-# OPTIONS --cubical #-}

module Type.Cubical.Path.Category{ℓ} where

open import Data.Tuple as Tuple using (_,_)
open import Data
open import Functional
open import Function.Axioms
open import Logic.Propositional
open import Structure.Category
open import Structure.Categorical.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Type
open import Type.Cubical.Path
open import Type.Cubical.Path.Equality
open import Type.Properties.Singleton

-- The type category is a category containing all types of a single universe level in the language.
-- The objects are all sets/types.
-- The morphisms are all functions where the domain/codomain-pair are from these objects.
typeFunctionPathCategory : Category{Obj = Type{ℓ}}(_→ᶠ_)
Category._∘_ typeFunctionPathCategory = _∘_
Category.id  typeFunctionPathCategory = id
Morphism.Associativity.proof (Category.associativity typeFunctionPathCategory)      = reflexivity(Path)
Morphism.Identityₗ.proof (Tuple.left (Category.identity typeFunctionPathCategory))  = reflexivity(Path)
Morphism.Identityᵣ.proof (Tuple.right (Category.identity typeFunctionPathCategory)) = reflexivity(Path)

typeFunctionPathCategoryObject : CategoryObject
typeFunctionPathCategoryObject = intro typeFunctionPathCategory

Empty-initialObject : Object.Initial{Obj = Type{ℓ}}(_→ᶠ_) (Empty)
IsUnit.unit       Empty-initialObject       = empty
IsUnit.uniqueness (Empty-initialObject {T}) = functionExtensionality(Empty)(T) \{}

Unit-terminalObject : Object.Terminal{Obj = Type{ℓ}}(_→ᶠ_) (Unit)
IsUnit.unit       Unit-terminalObject = const <>
IsUnit.uniqueness Unit-terminalObject = reflexivity(Path)

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:
open import Agda.Builtin.Bool

f : Bool → Bool
f x = let y = x in {!!}


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Ints.QuoInt where

open import Cubical.HITs.Ints.QuoInt.Base public

-- open import Cubical.HITs.Ints.QuoInt.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

module dn-sheaves where

import rings
open rings public

{- We postulate a propositional resizing axiom -}

raise-UU-Prop :
  (l : Level) → UU-Prop lzero → UU-Prop l
raise-UU-Prop l (pair P is-prop-P) =
  pair ( raise l P)
       ( is-prop-is-equiv' P
         ( map-raise l P)
         ( is-equiv-map-raise l P)
         ( is-prop-P))

postulate propositional-resizing : {l : Level} → is-equiv (raise-UU-Prop l)

lower-UU-Prop :
  {l : Level} → UU-Prop l → UU-Prop lzero
lower-UU-Prop = inv-is-equiv propositional-resizing

issec-lower-UU-Prop :
  {l : Level} (P : UU-Prop l) → Id (raise-UU-Prop l (lower-UU-Prop P)) P
issec-lower-UU-Prop = issec-inv-is-equiv propositional-resizing

isretr-lower-UU-Prop :
  {l : Level} (P : UU-Prop lzero) → Id (lower-UU-Prop (raise-UU-Prop l P)) P
isretr-lower-UU-Prop = isretr-inv-is-equiv propositional-resizing

{- We define what it means for a type to be a double-negation-sheaf -}

is-dn-sheaf :
  {l : Level} (X : UU l) → UU (l ⊔ (lsuc lzero))
is-dn-sheaf X =
  (P : UU-Prop lzero) → is-equiv (λ (f : ¬¬ (type-Prop P) → X) → f ∘ intro-dn)

universal-property-dn-sheafification :
  (l : Level) {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X → Y) →
  is-dn-sheaf Y → UU ((lsuc l) ⊔ l1 ⊔ l2)
universal-property-dn-sheafification l {Y = Y} f is-dn-sheaf-Y =
  (Z : UU l) (H : is-dn-sheaf Z) → is-equiv (λ (h : Y → Z) → h ∘ f)

postulate dn-sheafification : {l : Level} → UU l → UU l

postulate unit-dn-sheafification : {l : Level} (X : UU l) → X → dn-sheafification X

postulate is-dn-sheaf-dn-sheafification : {l : Level} (X : UU l) → is-dn-sheaf (dn-sheafification X)

postulate is-dn-sheafification : {l1 l2 : Level} (X : UU l1) → universal-property-dn-sheafification l2 (unit-dn-sheafification X) (is-dn-sheaf-dn-sheafification X)

{- We show that on propositions, dn-sheafification agrees with double negation. -}

is-dn-sheaf-dn : {l : Level} (P : UU l) → is-dn-sheaf (¬¬ P)
is-dn-sheaf-dn P Q =
  is-equiv-is-prop
    ( is-prop-function-type (¬¬ (type-Prop Q)) (¬¬ P) is-prop-neg)
    ( is-prop-function-type (type-Prop Q) (¬¬ P) is-prop-neg)
    ( dn-extend)

is-dn-sheafification-intro-dn :
  (k : Level) {l : Level} (P : UU l) →
  universal-property-dn-sheafification k (intro-dn {P = P}) (is-dn-sheaf-dn P)
is-dn-sheafification-intro-dn k {l} P X is-dn-sheaf-X =
  is-equiv-top-is-equiv-bottom-square
    ( λ f → f ∘ ( functor-dn {!map-raise l ?!}))
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
-- MIT License

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

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

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

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

{-# OPTIONS --guardedness #-}

open import Data.Empty using (⊥-elim)
open import Data.Unit using (⊤)
open import Data.Product
open import Data.Sum
open import Data.Vec using ([]; _∷_)
open import Data.List as List
import Data.Fin as Fin
open import Data.Nat

open import Relation.Nullary using (¬_; yes; no)
open import Relation.Binary.Definitions
open import Relation.Unary using (_∈_; _∉_; _⊆_; Satisfiable)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; inspect)
open import Common

open import is-lib.InfSys

module FairTermination-IS {𝕋 : Set} (message : Message 𝕋) where

  open import SessionType message
  open import Trace message
  open import Transitions message
  open import HasTrace message
  open import TraceSet message

  U : Set
  U = SessionType

  data RuleNames : Set where
    nil inp out : RuleNames

  data CoRuleNames : Set where
    inp out : CoRuleNames

  nil-r : FinMetaRule U
  nil-r .Ctx = ⊤
  nil-r .comp _ =
    [] ,
    ----
    nil

  inp-r : MetaRule U
  inp-r .Ctx = Continuation
  inp-r .Pos _ = 𝕋
  inp-r .prems f p = f p .force
  inp-r .conclu f = inp f

  out-r : MetaRule U
  out-r .Ctx = Continuation
  out-r .Pos _ = 𝕋
  out-r .prems f p = f p .force
  out-r .conclu f = out f

  inp-co-r : FinMetaRule U
  inp-co-r .Ctx = Σ[ (f , x) ∈ Continuation × 𝕋 ] x ∈ dom f
  inp-co-r .comp ((f , x) , _) =
    f x .force ∷ [] ,
    --------------------
    inp f

  out-co-r : FinMetaRule U
  out-co-r .Ctx = Σ[ (f , x) ∈ Continuation × 𝕋 ] x ∈ dom f
  out-co-r .comp ((f , x) , _) =
    f x .force ∷ [] ,
    --------------------
    out f

  WeakTerminationS : SessionType → Set
  WeakTerminationS T = ∀{φ} → φ ∈ ⟦ T ⟧ → ∃[ ψ ] (φ ++ ψ ∈ Maximal ⟦ T ⟧)

  WeakTerminationIS : IS U
  Names WeakTerminationIS = RuleNames
  rules WeakTerminationIS nil    = from nil-r
  rules WeakTerminationIS inp    = inp-r
  rules WeakTerminationIS out    = out-r

  WeakTerminationCOIS : IS U
  WeakTerminationCOIS .Names = CoRuleNames
  WeakTerminationCOIS .rules inp = from inp-co-r
  WeakTerminationCOIS .rules out = from out-co-r

  WeakTermination : SessionType → Set
  WeakTermination = FCoInd⟦ WeakTerminationIS , WeakTerminationCOIS ⟧

  WeakTerminationI : SessionType → Set
  WeakTerminationI = Ind⟦ WeakTerminationIS ∪ WeakTerminationCOIS ⟧

  {- Soundness -}

  lemma-inp : ∀{f φ x} → φ ∈ Maximal ⟦ f x .force ⟧ → I x ∷ φ ∈ Maximal ⟦ inp f ⟧
  lemma-inp (maximal wit F) =
    maximal (inp-has-trace wit) λ { (some le) (_ , def , step inp tr) → cong (_ ∷_) (F le (_ , def , tr))}

  lemma-out : ∀{f φ x} → φ ∈ Maximal ⟦ f x .force ⟧ → O x ∷ φ ∈ Maximal ⟦ out f ⟧
  lemma-out (maximal wit F) =
    maximal (out-has-trace wit) λ { (some le) (_ , def , step (out _) tr) → cong (_ ∷_) (F le (_ , def , tr))}

  lemma-end : ∀{f} → (∀{x} → x ∉ dom f) → [] ∈ Maximal ⟦ inp f ⟧
  lemma-end no-x = maximal (_ , inp , refl)
    λ { {[]} none _ → refl
      ; {O _ ∷ _} none (_ , _ , step () _)
      ; {I _ ∷ _} none (_ , def , step inp tr) → ⊥-elim (no-x (transitions+defined->defined tr def))}

  lemma-win : ∀{f} → (∀{x} → x ∉ dom f) → [] ∈ Maximal ⟦ out f ⟧
  lemma-win no-x = maximal (_ , out , refl)
    λ { {[]} none _ → refl
      ; {I _ ∷ _} none (_ , _ , step () _)
      ; {O _ ∷ _} none (_ , def , step (out ok) _) → ⊥-elim (no-x ok)}

  may-terminate : ∀{T} → Defined T → WeakTerminationI T → Satisfiable (Maximal ⟦ T ⟧)
  may-terminate _ (fold (inj₁ inp , f , refl , pr)) with Empty? f
  ... | inj₁ e = _ , lemma-end λ x → e _ x
  ... | inj₂ (p , def) =
    let tr , max = may-terminate def (pr p) in
    I p ∷ tr , lemma-inp max
  may-terminate _ (fold (inj₁ out , f , refl , pr)) with Empty? f
  ... | inj₁ e = _ , lemma-win λ x → e _ x
  ... | inj₂ (p , def) =
    let tr , max = may-terminate def (pr p) in
    O p ∷ tr , lemma-out max
  may-terminate _ (fold (inj₂ inp , ((_ , x) , def) , refl , pr)) =
    let tr , max = may-terminate def (pr Fin.zero) in
    I x ∷ tr , lemma-inp max
  may-terminate _ (fold (inj₂ out , ((_ , x) , def) , refl , pr)) =
    let tr , max = may-terminate def (pr Fin.zero) in
    O x ∷ tr , lemma-out max

  wt-sound : WeakTermination ⊆ WeakTerminationS
  wt-sound wt (_ , def , refl) = may-terminate def (fcoind-to-ind wt)
  wt-sound wt (_ , def , step t tr) with wt .CoInd⟦_⟧.unfold
  wt-sound wt (_ , def , step (inp {_} {p}) tr) | inp , _ , refl , pr =
    let tr' , max = wt-sound (pr p) (_ , def , tr) in
    tr' , lemma-inp max
  wt-sound wt (_ , def , step (out {_} {p} fx) tr) | out , _ , refl , pr =
    let tr' , max = wt-sound (pr p) (_ , def , tr) in
    tr' , lemma-out max

  {- Boundedness -}

  undefined→terminates : ∀{T} → ¬ Defined T → WeakTerminationI T
  undefined→terminates {nil}   _   = apply-ind (inj₁ nil) _ λ ()
  undefined→terminates {inp f} und = ⊥-elim (und inp)
  undefined→terminates {out f} und = ⊥-elim (und out)

  input-maximal→terminates : ∀{f x} → [] ∈ Maximal ⟦ inp f ⟧ → WeakTerminationI (f x .force)
  input-maximal→terminates {f} {x} (maximal (_ , inp , refl) F) with x ∈? f
  ... | no nfx = undefined→terminates nfx
  ... | yes fx with F none (_ , fx , step inp refl)
  ... | ()

  output-maximal→terminates : ∀{f x} → [] ∈ Maximal ⟦ out f ⟧ → WeakTerminationI (f x .force)
  output-maximal→terminates {f} {x} (maximal (_ , out , refl) F) with x ∈? f
  ... | no nfx = undefined→terminates nfx
  ... | yes fx with F none (_ , fx , step (out fx) refl)
  ... | ()

  bounded-lemma : ∀{T ϕ} → ϕ ∈ Maximal ⟦ T ⟧ → WeakTerminationI T
  bounded-lemma {nil} (maximal _ _) = apply-ind (inj₁ nil) _ λ ()
  bounded-lemma {inp f} c[]@(maximal (_ , def , refl) F) =
    apply-ind (inj₁ inp) _ λ p → input-maximal→terminates {f} {p} c[]
  bounded-lemma {inp f} cϕ@(maximal (_ , def , step inp tr) F) =
    apply-ind (inj₂ inp) (_ , (transitions+defined->defined tr def)) λ{Fin.zero → bounded-lemma (input-maximal cϕ)}
  bounded-lemma {out f} c[]@(maximal (_ , def , refl) F) =
    apply-ind (inj₁ out) _ λ p → output-maximal→terminates {f} {p} c[]
  bounded-lemma {out f} cϕ@(maximal (_ , def , step (out x) tr) F) =
    apply-ind (inj₂ out) (_ , x) λ{Fin.zero → bounded-lemma (output-maximal cϕ)}

  wtS-bounded : WeakTerminationS ⊆ WeakTerminationI
  wtS-bounded {nil} _ = apply-ind (inj₁ nil) _ λ ()
  wtS-bounded {inp f} s with s (_ , inp , refl)
  ... | _ , max = bounded-lemma max
  wtS-bounded {out f} s with s (_ , out , refl)
  ... | _ , max = bounded-lemma max

  {- Consistency -}

  lemma-input-maximal : ∀{f x} → WeakTerminationS (inp f) → WeakTerminationS (f x .force)
  lemma-input-maximal {f} {x} spec tφ with x ∈? f
  ... | no nfx = ⊥-elim (nfx (has-trace->defined tφ))
  ... | yes fx with spec (inp-has-trace tφ)
  ... | _ , cψ = _ , input-maximal cψ

  lemma-output-maximal : ∀{f x} → WeakTerminationS (out f) → WeakTerminationS (f x .force)
  lemma-output-maximal {f} {x} spec tφ with x ∈? f
  ... | no nfx = ⊥-elim (nfx (has-trace->defined tφ))
  ... | yes fx with spec (out-has-trace tφ)
  ... | _ , cψ = _ , output-maximal cψ

  wtS-cons : WeakTerminationS ⊆ ISF[ WeakTerminationIS ] WeakTerminationS
  wtS-cons {nil} spec = nil , _ , refl , λ ()
  wtS-cons {inp f} spec =
    inp , f , refl , λ p → lemma-input-maximal {f} {p} spec
  wtS-cons {out f} spec =
    out , f , refl , λ p → lemma-output-maximal {f} {p} spec

  {- Completeness -}

  wt-complete : WeakTerminationS ⊆ WeakTermination
  wt-complete =
    bounded-coind[ WeakTerminationIS , WeakTerminationCOIS ] WeakTerminationS wtS-bounded wtS-cons

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Algebra.Dioid.Bool where

open import Algebra.Dioid

data Bool : Set where
  true  : Bool
  false : Bool

data _≡_ : (x y : Bool) -> Set where
  reflexivity  : ∀ {x     : Bool} ->                   x ≡ x
  symmetry     : ∀ {x y   : Bool} -> x ≡ y ->          y ≡ x
  transitivity : ∀ {x y z : Bool} -> x ≡ y -> y ≡ z -> x ≡ z

_or_ : Bool -> Bool -> Bool
false or false = false
_ or _ = true

_and_ : Bool -> Bool -> Bool
true and true = true
_ and _ = false

max_stars_repo_name: snowleopard/alga-proofs

max_issues_repo_name: snowleopard/alga-proofs

max_forks_repo_name: snowleopard/alga-proofs


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

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

-- For each desired property (VotesOnce and PreferredRoundRule), we have a
-- module containing a Type that defines a property that an implementation
-- should prove, and a proof that it implies the corresponding rule used by
-- the abstract proofs.  Then, we use those proofs to instantiate thmS5,
-- and the use thmS5 to prove a number of correctness conditions.
--
-- TODO-1: refactor this file to separate the definitions and proofs of
-- VotesOnce and PreferredRoundRule from their use in proving the correctness
-- properties.

module LibraBFT.Abstract.Properties
  (UID    : Set)
  (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
  (NodeId : Set)
  (𝓔  : EpochConfig UID NodeId)
  (𝓥  : VoteEvidence UID NodeId 𝓔)
  where

 open import LibraBFT.Abstract.Records                 UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.Records.Extends         UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.RecordChain             UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.RecordChain.Assumptions UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.System                  UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.RecordChain.Properties  UID _≟UID_ NodeId 𝓔 𝓥
 open        EpochConfig 𝓔

 module WithAssumptions {ℓ}
   (InSys                 : Record → Set ℓ)
   (votes-only-once       : VotesOnlyOnceRule InSys)
   (preferred-round-rule  : PreferredRoundRule InSys)
  where

   open All-InSys-props InSys

   CommitsDoNotConflict : ∀{q q'}
        → {rc  : RecordChain (Q q)}  → All-InSys rc
        → {rc' : RecordChain (Q q')} → All-InSys rc'
        → {b b' : Block}
        → CommitRule rc  b
        → CommitRule rc' b'
        → NonInjective-≡ bId ⊎ ((B b) ∈RC rc' ⊎ (B b') ∈RC rc)
   CommitsDoNotConflict = WithInvariants.thmS5 InSys votes-only-once preferred-round-rule

   -- When we are dealing with a /Complete/ InSys predicate, we can go a few steps
   -- further and prove that commits do not conflict even if we have only partial
   -- knowledge about Records represented in the system.
   module _ (∈QC⇒AllSent : Complete InSys) where

    -- For a /complete/ system we can go even further; if we have evidence that
    -- only the tip of the record chains is in the system, we can infer
    -- the rest of it is also in the system (or blockIDs are not injective).
    CommitsDoNotConflict'
      : ∀{q q'}{rc  : RecordChain (Q q)}{rc' : RecordChain (Q q')}{b b' : Block}
      → InSys (Q q) → InSys (Q q')
      → CommitRule rc  b
      → CommitRule rc' b'
      → NonInjective-≡ bId ⊎ ((B b) ∈RC rc' ⊎ (B b') ∈RC rc)
    CommitsDoNotConflict' {q} {q'} {step {r = B bb} rc b←q} {step {r = B bb'} rc' b←q'} {b} {b'} q∈sys q'∈sys cr cr'
       with bft-assumption (qVotes-C1 q) (qVotes-C1 q')
    ...| α , α∈qmem , α∈q'mem , hα
       with Any-sym (Any-map⁻ α∈qmem) | Any-sym (Any-map⁻ α∈q'mem)
    ...| α∈q | α∈q'
       with ∈QC⇒AllSent {q = q} hα α∈q q∈sys | ∈QC⇒AllSent {q = q'} hα α∈q' q'∈sys
    ...| ab , (arc , ais) , ab←q | ab' , (arc' , ais') , ab←q'
       with RecordChain-irrelevant (step arc  ab←q)  (step rc  b←q) |
            RecordChain-irrelevant (step arc' ab←q') (step rc' b←q')
    ...| inj₁ hb     | _       = inj₁ hb
    ...| inj₂ _      | inj₁ hb = inj₁ hb
    ...| inj₂ arc≈rc | inj₂ arc'≈rc'
       with CommitsDoNotConflict
                 (All-InSys-step ais  ab←q  q∈sys )
                 (All-InSys-step ais' ab←q' q'∈sys)
                 (transp-CR (≈RC-sym arc≈rc  ) cr )
                 (transp-CR (≈RC-sym arc'≈rc') cr')
    ...| inj₁ hb = inj₁ hb
    ...| inj₂ (inj₁ b∈arc') = inj₂ (inj₁ (transp-B∈RC arc'≈rc' b∈arc'))
    ...| inj₂ (inj₂ b'∈arc) = inj₂ (inj₂ (transp-B∈RC arc≈rc   b'∈arc))

    -- The final property is even stronger; it states that even if an observer
    -- has access only to suffixes of record chains that match the commit rule,
    -- we can still guarantee that b and b' are non-conflicting blocks.  This
    -- will be important for showing that observers can have confidence in commit
    -- messages without participating in the protocol and without having access to
    -- all previously sent records.
    CommitsDoNotConflict''
      : ∀{o o' q q'}
      → {rcf  : RecordChainFrom o  (Q q)}
      → {rcf' : RecordChainFrom o' (Q q')}
      → {b b' : Block}
      → InSys (Q q)
      → InSys (Q q')
      → CommitRuleFrom rcf  b
      → CommitRuleFrom rcf' b'
      → NonInjective-≡ bId ⊎ Σ (RecordChain (Q q')) ((B b)  ∈RC_)
                           ⊎ Σ (RecordChain (Q q))  ((B b') ∈RC_)
    CommitsDoNotConflict'' {cb} {q = q} {q'} {rcf} {rcf'} q∈sys q'∈sys crf crf'
       with bft-assumption (qVotes-C1 q) (qVotes-C1 q')
    ...| α , α∈qmem , α∈q'mem , hα
       with Any-sym (Any-map⁻ α∈qmem) | Any-sym (Any-map⁻ α∈q'mem)
    ...| α∈q | α∈q'
       with ∈QC⇒AllSent {q = q} hα α∈q q∈sys | ∈QC⇒AllSent {q = q'} hα α∈q' q'∈sys
    ...| ab , (arc , ais) , ab←q | ab' , (arc' , ais') , ab←q'
       with step arc  ab←q | step arc' ab←q'
    ...| rcq | rcq'
       with crf⇒cr rcf  rcq  crf | crf⇒cr rcf' rcq' crf'
    ...| inj₁ hb | _       = inj₁ hb
    ...| inj₂ _  | inj₁ hb = inj₁ hb
    ...| inj₂ cr | inj₂ cr'
       with CommitsDoNotConflict' q∈sys q'∈sys cr cr'
    ...| inj₁ hb = inj₁ hb
    ...| inj₂ (inj₁ b∈arc') = inj₂ (inj₁ (rcq' , b∈arc'))
    ...| inj₂ (inj₂ b'∈arc) = inj₂ (inj₂ (rcq  , b'∈arc))

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:
module Identity where

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

elim== : {A : Set}(x : A)(C : (y : A) -> x == y -> Set) ->
         C x refl -> (y : A) -> (p : x == y) -> C y p
elim== x C Cx .x refl = Cx

elim==₁ : {A : Set}(x : A)(C : (y : A) -> x == y -> Set1) ->
	  C x refl -> (y : A) -> (p : x == y) -> C y p
elim==₁ x C Cx .x refl = Cx

sym : {A : Set}{x y : A} -> x == y -> y == x
sym {A}{x}{y} eq = elim== x (\z _ -> z == x) refl y eq

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong {A} f {x}{y} eq = elim== x (\z _ -> f x == f z) refl y eq

subst : {A : Set}{x y : A}(P : A -> Set) -> x == y -> P x -> P y
subst P xy px = elim== _ (\z _ -> P z) px _ xy

subst₁ : {A : Set}{x y : A}(P : A -> Set1) -> x == y -> P x -> P y
subst₁ P xy px = elim==₁ _ (\z _ -> P z) px _ xy

symRef : (A : Set)(x : A) -> sym (refl{A}{x}) == refl
symRef A x = refl

symSym : {A : Set}{x y : A}(p : x == y) -> sym (sym p) == p
symSym {A}{x}{y} p = elim== x (\y q -> sym (sym q) == q) refl y p

-- Proving the symmetric elimination rule is not trivial.
elimS : {A : Set}(x : A)(C : (y : A) -> y == x -> Set) ->
        C x refl -> (y : A) -> (p : y == x) -> C y p
elimS x C r y p = subst (C y) (symSym p) h
  where
    h : C y (sym (sym p))
    h = elim== x (\y p -> C y (sym p)) r y (sym p)

data _==¹_ {A : Set1}(x : A) : {B : Set1} -> B -> Set where
  refl¹ : x ==¹ x

subst¹ : {A : Set1}{x y : A}(P : A -> Set) -> x ==¹ y -> P x -> P y
subst¹ {A} P refl¹ px = px

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --no-auto-inline #-}

module Haskell.Prim.Num where

open import Agda.Builtin.Nat as Nat hiding (_+_; _-_; _*_; _<_; _==_)
open import Agda.Builtin.Int using (pos; negsuc)
open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
open import Agda.Builtin.Unit

open import Haskell.Prim
open import Haskell.Prim.Word
open import Haskell.Prim.Int
open import Haskell.Prim.Integer
open import Haskell.Prim.Double
open import Haskell.Prim.Eq
open import Haskell.Prim.Ord
open import Haskell.Prim.Monoid

--------------------------------------------------
-- Num

record Num (a : Set) : Set₁ where
  infixl 6 _+_ _-_
  infixl 7 _*_
  field
    MinusOK       : a → a → Set
    NegateOK      : a → Set
    FromIntegerOK : Integer → Set
    _+_           : a → a → a
    _-_           : (x y : a) → ⦃ MinusOK x y ⦄ → a
    _*_           : a → a → a
    negate        : (x : a) → ⦃ NegateOK x ⦄ → a
    abs           : a → a
    signum        : a → a
    fromInteger   : (n : Integer) → ⦃ FromIntegerOK n ⦄ → a
    overlap ⦃ number ⦄  : Number a
    overlap ⦃ numZero ⦄ : number .Number.Constraint 0
    overlap ⦃ numOne ⦄  : number .Number.Constraint 1

open Num ⦃ ... ⦄ public hiding (FromIntegerOK; number)

instance
  iNumNat : Num Nat
  iNumNat .MinusOK n m      = IsFalse (n Nat.< m)
  iNumNat .NegateOK 0       = ⊤
  iNumNat .NegateOK (suc _) = ⊥
  iNumNat .Num.FromIntegerOK (negsuc _) = ⊥
  iNumNat .Num.FromIntegerOK (pos _) = ⊤
  iNumNat ._+_ n m = n Nat.+ m
  iNumNat ._-_ n m = n Nat.- m
  iNumNat ._*_ n m = n Nat.* m
  iNumNat .negate n = n
  iNumNat .abs    n = n
  iNumNat .signum 0       = 0
  iNumNat .signum (suc n) = 1
  iNumNat .fromInteger (pos n) = n
  iNumNat .fromInteger (negsuc _) ⦃ () ⦄

  iNumInt : Num Int
  iNumInt .MinusOK _ _         = ⊤
  iNumInt .NegateOK _          = ⊤
  iNumInt .Num.FromIntegerOK _ = ⊤
  iNumInt ._+_ x y             = addInt x y
  iNumInt ._-_ x y             = subInt x y
  iNumInt ._*_ x y             = mulInt x y
  iNumInt .negate x            = negateInt x
  iNumInt .abs x               = absInt x
  iNumInt .signum x            = signInt x
  iNumInt .fromInteger n       = integerToInt n

  iNumInteger : Num Integer
  iNumInteger .MinusOK _ _ = ⊤
  iNumInteger .NegateOK _          = ⊤
  iNumInteger .Num.FromIntegerOK _ = ⊤
  iNumInteger ._+_ x y             = addInteger x y
  iNumInteger ._-_ x y             = subInteger x y
  iNumInteger ._*_ x y             = mulInteger x y
  iNumInteger .negate x            = negateInteger x
  iNumInteger .abs x               = absInteger x
  iNumInteger .signum x            = signInteger x
  iNumInteger .fromInteger n       = n

  iNumWord : Num Word
  iNumWord .MinusOK _ _         = ⊤
  iNumWord .NegateOK _          = ⊤
  iNumWord .Num.FromIntegerOK _ = ⊤
  iNumWord ._+_ x y             = addWord x y
  iNumWord ._-_ x y             = subWord x y
  iNumWord ._*_ x y             = mulWord x y
  iNumWord .negate x            = negateWord x
  iNumWord .abs x               = x
  iNumWord .signum x            = if x == 0 then 0 else 1
  iNumWord .fromInteger n       = integerToWord n

  iNumDouble : Num Double
  iNumDouble .MinusOK _ _         = ⊤
  iNumDouble .NegateOK _          = ⊤
  iNumDouble .Num.FromIntegerOK _ = ⊤
  iNumDouble ._+_ x y             = primFloatPlus x y
  iNumDouble ._-_ x y             = primFloatMinus x y
  iNumDouble ._*_ x y             = primFloatTimes x y
  iNumDouble .negate x            = primFloatMinus 0.0 x
  iNumDouble .abs x               = if x < 0.0 then primFloatMinus 0.0 x else x
  iNumDouble .signum x            = case compare x 0.0 of λ where
                                      LT → -1.0
                                      EQ → x
                                      GT → 1.0
  iNumDouble .fromInteger (pos    n) = fromNat n
  iNumDouble .fromInteger (negsuc n) = fromNeg (suc n)

MonoidSum : ⦃ iNum : Num a ⦄ → Monoid a
MonoidSum .mempty      = 0
MonoidSum .super ._<>_ = _+_

MonoidProduct : ⦃ iNum : Num a ⦄ → Monoid a
MonoidProduct .mempty      = 1
MonoidProduct .super ._<>_ = _*_


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Properties.Lattice {l₁ l₂} (L : Lattice l₁ l₂) where

open Lattice L
open import Algebra.Structures
import Algebra.FunctionProperties as P; open P _≈_
open import Relation.Binary
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Data.Product

∧-idempotent : Idempotent _∧_
∧-idempotent x = begin
  x ∧ x            ≈⟨ refl ⟨ ∧-cong ⟩ sym (proj₁ absorptive _ _) ⟩
  x ∧ (x ∨ x ∧ x)  ≈⟨ proj₂ absorptive _ _ ⟩
  x                ∎

∨-idempotent : Idempotent _∨_
∨-idempotent x = begin
  x ∨ x      ≈⟨ refl ⟨ ∨-cong ⟩ sym (∧-idempotent _) ⟩
  x ∨ x ∧ x  ≈⟨ proj₁ absorptive _ _ ⟩
  x          ∎

-- The dual construction is also a lattice.

∧-∨-isLattice : IsLattice _≈_ _∧_ _∨_
∧-∨-isLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = ∧-comm
  ; ∨-assoc       = ∧-assoc
  ; ∨-cong        = ∧-cong
  ; ∧-comm        = ∨-comm
  ; ∧-assoc       = ∨-assoc
  ; ∧-cong        = ∨-cong
  ; absorptive    = swap absorptive
  }

∧-∨-lattice : Lattice _ _
∧-∨-lattice = record
  { _∧_       = _∨_
  ; _∨_       = _∧_
  ; isLattice = ∧-∨-isLattice
  }

-- Every lattice can be turned into a poset.

poset : Poset _ _ _
poset = record
  { Carrier        = Carrier
  ; _≈_            = _≈_
  ; _≤_            = λ x y → x ≈ x ∧ y
  ; isPartialOrder = record
    { isPreorder = record
      { isEquivalence = isEquivalence
      ; reflexive     = λ {i} {j} i≈j → begin
                          i      ≈⟨ sym $ ∧-idempotent _ ⟩
                          i ∧ i  ≈⟨ ∧-cong refl i≈j ⟩
                          i ∧ j  ∎
      ; trans         = λ {i} {j} {k} i≈i∧j j≈j∧k → begin
                          i            ≈⟨ i≈i∧j ⟩
                          i ∧ j        ≈⟨ ∧-cong refl j≈j∧k ⟩
                          i ∧ (j ∧ k)  ≈⟨ sym (∧-assoc _ _ _) ⟩
                          (i ∧ j) ∧ k  ≈⟨ ∧-cong (sym i≈i∧j) refl ⟩
                          i ∧ k        ∎
      }
    ; antisym = λ {x} {y} x≈x∧y y≈y∧x → begin
                  x      ≈⟨ x≈x∧y ⟩
                  x ∧ y  ≈⟨ ∧-comm _ _ ⟩
                  y ∧ x  ≈⟨ sym y≈y∧x ⟩
                  y      ∎
    }
  }

-- One can replace the underlying equality with an equivalent one.

replace-equality : {_≈′_ : Rel Carrier l₂} →
                   (∀ {x y} → x ≈ y ⇔ x ≈′ y) → Lattice _ _
replace-equality {_≈′_} ≈⇔≈′ = record
  { _≈_       = _≈′_
  ; _∧_       = _∧_
  ; _∨_       = _∨_
  ; isLattice = record
    { isEquivalence = record
      { refl  = to ⟨$⟩ refl
      ; sym   = λ x≈y → to ⟨$⟩ sym (from ⟨$⟩ x≈y)
      ; trans = λ x≈y y≈z → to ⟨$⟩ trans (from ⟨$⟩ x≈y) (from ⟨$⟩ y≈z)
      }
    ; ∨-comm     = λ x y → to ⟨$⟩ ∨-comm x y
    ; ∨-assoc    = λ x y z → to ⟨$⟩ ∨-assoc x y z
    ; ∨-cong     = λ x≈y u≈v → to ⟨$⟩ ∨-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
    ; ∧-comm     = λ x y → to ⟨$⟩ ∧-comm x y
    ; ∧-assoc    = λ x y z → to ⟨$⟩ ∧-assoc x y z
    ; ∧-cong     = λ x≈y u≈v → to ⟨$⟩ ∧-cong (from ⟨$⟩ x≈y) (from ⟨$⟩ u≈v)
    ; absorptive = (λ x y → to ⟨$⟩ proj₁ absorptive x y)
                 , (λ x y → to ⟨$⟩ proj₂ absorptive x y)
    }
  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})


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

-- Some of the obvious properties of cartesian functors
module Categories.Functor.Cartesian.Properties where

open import Level
open import Data.Product using (Σ ; _,_)

open import Categories.Category
open import Categories.Category.Cartesian.Structure
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.Functor.Cartesian
open import Categories.Functor.Monoidal
open import Categories.NaturalTransformation

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Object.Terminal as ⊤
import Categories.Object.Product as P

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level

module _ (C : CartesianCategory o ℓ e) where
  open CartesianCategory C
  open P U

  idF-IsCartesianF : IsCartesianF C C idF
  idF-IsCartesianF = record
    { F-resp-⊤ = terminal.⊤-is-terminal
    ; F-resp-× = Product⇒IsProduct product
    }

  idF-CartesianF : CartesianF C C
  idF-CartesianF = record
    { isCartesian = idF-IsCartesianF
    }

module _ (A : CartesianCategory o ℓ e) (B : CartesianCategory o′ ℓ′ e′) (C : CartesianCategory o″ ℓ″ e″) where
  private
    module A = CartesianCategory A
    module B = CartesianCategory B
    module C = CartesianCategory C
    open P C.U

  ∘-IsCartesianF : ∀ {F : Functor A.U B.U} {G : Functor B.U C.U} →
                    IsCartesianF B C G → IsCartesianF A B F →
                    IsCartesianF A C (G ∘F F)
  ∘-IsCartesianF {F} {G} CG CF = record
    { F-resp-⊤ = ⊤.Terminal.⊤-is-terminal (⊤.transport-by-iso C.U C.terminal
                                          (M.≅.trans C.U (M.≅.sym C.U CG.⊤-iso) ([ G ]-resp-≅ (M.≅.sym B.U CF.⊤-iso))))
    ; F-resp-× = record
      { ⟨_,_⟩    = λ f g → G.₁ (CF.×-iso.to _ _) C.∘ CG.×-iso.to _ _ C.∘ C.⟨ f , g ⟩
      ; project₁ = λ {_ f g} → begin
        G.₁ (F.₁ A.π₁) C.∘ G.₁ (CF.×-iso.to _ _) C.∘ CG.×-iso.to _ _ C.∘ C.⟨ f , g ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ([ CG.F-prod _ _ ]⟨⟩∘ ○ CG.F-prod.⟨⟩-cong₂ _ _ C.project₁ C.project₂) ⟩
        G.₁ (F.₁ A.π₁) C.∘ G.₁ (CF.×-iso.to _ _) C.∘ CG.F-resp-×.⟨ f , g ⟩           ≈⟨ pullˡ ([ G ]-resp-∘ CF.F-resp-×.project₁) ⟩
        G.₁ B.π₁ C.∘ CG.F-resp-×.⟨ f , g ⟩                                           ≈⟨ CG.F-resp-×.project₁ ⟩
        f ∎
      ; project₂ = λ {_ f g} → begin
        G.₁ (F.₁ A.π₂) C.∘ G.₁ (CF.×-iso.to _ _) C.∘ CG.×-iso.to _ _ C.∘ C.⟨ f , g ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ([ CG.F-prod _ _ ]⟨⟩∘ ○ CG.F-prod.⟨⟩-cong₂ _ _ C.project₁ C.project₂) ⟩
        G.₁ (F.₁ A.π₂) C.∘ G.₁ (CF.×-iso.to _ _) C.∘ CG.F-resp-×.⟨ f , g ⟩           ≈⟨ pullˡ ([ G ]-resp-∘ CF.F-resp-×.project₂) ⟩
        G.₁ B.π₂ C.∘ CG.F-resp-×.⟨ f , g ⟩                                           ≈⟨ CG.F-resp-×.project₂ ⟩
        g ∎
      ; unique   = λ {_ h f g} eq₁ eq₂ → begin
        G.₁ (CF.×-iso.to _ _) C.∘ CG.×-iso.to _ _ C.∘ C.⟨ f , g ⟩
          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ C.unique′ (C.project₁ ○ ⟺ eq₁ ○ pushˡ (⟺ ([ G ]-resp-∘ B.project₁)) ○ pushˡ (⟺ C.project₁))
                                       (C.project₂ ○ ⟺ eq₂ ○ pushˡ (⟺ ([ G ]-resp-∘ B.project₂)) ○ pushˡ (⟺ C.project₂)) ⟩
        G.₁ (CF.×-iso.to _ _) C.∘ CG.×-iso.to _ _ C.∘ CG.×-iso.from _ _ C.∘ G.₁ (CF.×-iso.from _ _) C.∘ h
          ≈⟨ refl⟩∘⟨ cancelˡ (CG.×-iso.isoˡ _ _) ⟩
        G.₁ (CF.×-iso.to _ _) C.∘ G.₁ (CF.×-iso.from _ _) C.∘ h
          ≈⟨ cancelˡ (M._≅_.isoˡ ([ G ]-resp-≅ (CF.×-iso _ _))) ⟩
        h
          ∎
      }
    }
    where module F  = Functor F
          module G  = Functor G
          module CG = IsCartesianF CG
          module CF = IsCartesianF CF
          open C.HomReasoning
          open MR C.U

∘-CartesianF : {A : CartesianCategory o ℓ e} {B : CartesianCategory o′ ℓ′ e′} {C : CartesianCategory o″ ℓ″ e″} →
               CartesianF B C → CartesianF A B → CartesianF A C
∘-CartesianF G F = record { isCartesian = ∘-IsCartesianF _ _ _ (CartesianF.isCartesian G) (CartesianF.isCartesian F) }

module _ {C : CartesianCategory o ℓ e} {D : CartesianCategory o′ ℓ′ e′} where
  private
    module C = CartesianCategory C
    module D = CartesianCategory D
    open D.HomReasoning
    open MR D.U
    open M D.U

  isMonoidalFunctor : CartesianF C D → MonoidalFunctor C.monoidalCategory D.monoidalCategory
  isMonoidalFunctor F = record
    { F          = F.F
    ; isMonoidal = record
      { ε             = F.⊤-iso.to
      ; ⊗-homo        = ntHelper record
        { η       = λ { (X , Y) → F.×-iso.to X Y }
        ; commute = λ { {X , Y} {Z , W} (f , g) →
          F.F-prod.unique′ _ _
            (begin
              F.₁ C.π₁ D.∘ F.×-iso.to Z W D.∘ (F.₁ f D.⁂ F.₁ g) ≈⟨ pullˡ F.F-resp-×.project₁ ⟩
              D.π₁ D.∘ (F.₁ f D.⁂ F.₁ g)                        ≈⟨ D.project₁ ⟩
              F.₁ f D.∘ D.π₁                                    ≈˘⟨ pullʳ F.F-resp-×.project₁ ⟩
              (F.₁ f D.∘ F.₁ C.π₁) D.∘ F.×-iso.to X Y           ≈˘⟨ pullˡ ([ F.F ]-resp-square C.project₁) ⟩
              F.₁ C.π₁ D.∘ F.₁ (f C.⁂ g) D.∘ F.×-iso.to X Y     ∎)
            (begin
              F.₁ C.π₂ D.∘ F.×-iso.to Z W D.∘ (F.₁ f D.⁂ F.₁ g) ≈⟨ pullˡ F.F-resp-×.project₂ ⟩
              D.π₂ D.∘ (F.₁ f D.⁂ F.₁ g)                        ≈⟨ D.project₂ ⟩
              F.₁ g D.∘ D.π₂                                    ≈˘⟨ pullʳ F.F-resp-×.project₂ ⟩
              (F.₁ g D.∘ F.₁ C.π₂) D.∘ F.×-iso.to X Y           ≈˘⟨ pullˡ ([ F.F ]-resp-square C.project₂) ⟩
              F.₁ C.π₂ D.∘ F.₁ (f C.⁂ g) D.∘ F.×-iso.to X Y     ∎)
          }
        }
      ; associativity = λ {X Y Z} → let open P D.U in begin
        F.₁ C.associator.from D.∘ F.×-iso.to (X C.× Y) Z D.∘ (F.×-iso.to X Y D.⁂ D.id)
          ≈⟨ F.F-resp-⟨⟩′ _ _ ⟩∘⟨ [ D.product ⇒ D.product ⇒ F.F-prod _ _ ]repack∘× ⟩
        F.F-resp-×.⟨ F.₁ (C.π₁ C.∘ C.π₁) , F.₁ C.⟨ C.π₂ C.∘ C.π₁ , C.π₂ ⟩ ⟩ D.∘ F.F-resp-×.⟨ F.×-iso.to X Y D.∘ D.π₁ , D.id D.∘ D.π₂ ⟩
          ≈⟨ F.F-prod.⟨⟩-cong₂ _ _ F.homomorphism (F.F-resp-⟨⟩′ _ _ ○ F.F-prod.⟨⟩-cong₂ _ _ F.homomorphism D.Equiv.refl) ⟩∘⟨refl ⟩
        F.F-resp-×.⟨ F.₁ C.π₁ D.∘ F.₁ C.π₁ , F.F-resp-×.⟨ F.₁ C.π₂ D.∘ F.₁ C.π₁ , F.₁ C.π₂ ⟩ ⟩ D.∘ F.F-resp-×.⟨ F.×-iso.to X Y D.∘ D.π₁ , D.id D.∘ D.π₂ ⟩
          ≈⟨ [ F.F-prod _ _ ]⟨⟩∘ ⟩
        F.F-resp-×.⟨ (F.₁ C.π₁ D.∘ F.₁ C.π₁) D.∘ _ , F.F-resp-×.⟨ F.₁ C.π₂ D.∘ F.₁ C.π₁ , F.₁ C.π₂ ⟩ D.∘ _ ⟩
          ≈⟨ F.F-prod.⟨⟩-cong₂ _ _ (pullʳ F.F-resp-×.project₁ ○ pullˡ F.F-resp-×.project₁)
                                   [ F.F-prod _ _ ]⟨⟩∘ ⟩
        F.F-resp-×.⟨ D.π₁ D.∘ D.π₁ , F.F-resp-×.⟨ (F.₁ C.π₂ D.∘ F.₁ C.π₁) D.∘ _ , F.₁ C.π₂ D.∘ _ ⟩ ⟩
          ≈⟨ F.F-prod.⟨⟩-cong₂ _ _ D.Equiv.refl
            (F.F-prod.⟨⟩-cong₂ _ _ (pullʳ F.F-resp-×.project₁ ○ pullˡ F.F-resp-×.project₂)
                                   (F.F-resp-×.project₂ ○ D.identityˡ)) ⟩
        F.F-resp-×.⟨ D.π₁ D.∘ D.π₁ , F.F-resp-×.⟨ D.π₂ D.∘ D.π₁ , D.π₂ ⟩ ⟩
          ≈˘⟨ F.F-prod.⟨⟩-cong₂ _ _ D.identityˡ ([ F.F-prod _ _ ]⟨⟩∘ ○ (F.F-prod.⟨⟩-cong₂ _ _ D.project₁ D.project₂)) ⟩
        F.F-resp-×.⟨ D.id D.∘ D.π₁ D.∘ D.π₁ , F.×-iso.to Y Z D.∘ D.⟨ D.π₂ D.∘ D.π₁ , D.π₂ ⟩ ⟩
          ≈˘⟨ [ D.product ⇒ (F.F-prod _ _) ]×∘⟨⟩ ⟩
        F.F-resp-×.⟨ D.id D.∘ D.π₁ , F.×-iso.to Y Z D.∘ D.π₂ ⟩ D.∘ D.associator.from
          ≈˘⟨ pullˡ [ D.product ⇒ D.product ⇒ F.F-prod _ _ ]repack∘× ⟩
        F.×-iso.to X (Y C.× Z) D.∘ (D.id D.⁂ F.×-iso.to Y Z) D.∘ D.associator.from
          ∎
      ; unitaryˡ      = begin
        F.₁ C.π₂ D.∘ F.F-resp-×.⟨ D.π₁ , D.π₂ ⟩ D.∘ (F.F-resp-⊤.! D.⁂ D.id) ≈⟨ pullˡ F.F-resp-×.project₂ ⟩
        D.π₂ D.∘ (F.F-resp-⊤.! D.⁂ D.id)                                    ≈⟨ D.project₂ ⟩
        D.id D.∘ D.π₂                                                       ≈⟨ D.identityˡ ⟩
        D.π₂                                                                ∎
      ; unitaryʳ      = begin
        F.₁ C.π₁ D.∘ F.F-resp-×.⟨ D.π₁ , D.π₂ ⟩ D.∘ (D.id D.⁂ F.F-resp-⊤.!) ≈⟨ pullˡ F.F-resp-×.project₁ ⟩
        D.π₁ D.∘ (D.id D.⁂ F.F-resp-⊤.!)                                    ≈⟨ D.project₁ ⟩
        D.id D.∘ D.π₁                                                       ≈⟨ D.identityˡ ⟩
        D.π₁                                                                ∎
      }
    }
    where module F = CartesianF F

  isStrongMonoidalFunctor : CartesianF C D → StrongMonoidalFunctor C.monoidalCategory D.monoidalCategory
  isStrongMonoidalFunctor F = record
    { F                = F.F
    ; isStrongMonoidal = record
      { ε             = ≅.sym F.⊤-iso
      ; ⊗-homo        = record
        { F⇒G = MF.⊗-homo
        ; F⇐G = ntHelper record
          { η       = λ { (X , Y) → F.×-iso.from X Y }
          ; commute = λ { {X , Y} {Z , W} (f , g) →
            begin
              D.⟨ F.₁ C.π₁ , F.₁ C.π₂ ⟩ D.∘ F.₁ (f C.⁂ g)                   ≈⟨ D.⟨⟩∘ ⟩
              D.⟨ F.₁ C.π₁ D.∘ F.₁ (f C.⁂ g) , F.₁ C.π₂ D.∘ F.₁ (f C.⁂ g) ⟩ ≈⟨ D.⟨⟩-cong₂ ([ F.F ]-resp-square C.project₁) ([ F.F ]-resp-square C.project₂) ⟩
              D.⟨ F.₁ f D.∘ F.F₁ C.π₁ , F.₁ g D.∘ F.F₁ C.π₂ ⟩               ≈˘⟨ D.⁂∘⟨⟩ ⟩
              (F.₁ f D.⁂ F.₁ g) D.∘ D.⟨ F.F₁ C.π₁ , F.F₁ C.π₂ ⟩             ∎ }
          }
        ; iso = λ { (X , Y) → record
          { isoˡ = F.×-iso.isoʳ X Y
          ; isoʳ = F.×-iso.isoˡ X Y
          } }
        }
      ; associativity = MF.associativity
      ; unitaryˡ      = MF.unitaryˡ
      ; unitaryʳ      = MF.unitaryʳ
      }
    }
    where module F  = CartesianF F
          module MF = MonoidalFunctor (isMonoidalFunctor F)

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
-- Andreas, 2012-05-24, issue reported by Nisse
{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS -v tc.meta:50 #-}
module Issue658 where

import Common.Level

postulate
  A : Set
  P : A → Set
  Q : (x : A) → P x → Set
  p : (x : A) → P x

record R : Set where
  field
    a : A

r : R
r = {!!}

postulate
  q : Q (R.a r) (p (R.a r))

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/MetaVars.hs:101

-- The internal error was cause by eta-expanding the frozen meta.
-- Eta-expansion of frozen metas is now allowed.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

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

open import LibraBFT.Abstract.Types

open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Consensus.Types

open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Concrete.Obligations
import LibraBFT.Concrete.Properties.VotesOnce   as VO
import LibraBFT.Concrete.Properties.LockedRound as LR

open import LibraBFT.Yasm.System     ConcSysParms
open import LibraBFT.Yasm.Properties ConcSysParms

-- In this module, we assume that the implementation meets its
-- obligations, and use this assumption to prove that the
-- implementatioon enjoys one of the per-epoch correctness conditions
-- proved in Abstract.Properties.  It can be extended to other
-- properties later.

module LibraBFT.Concrete.Properties (impl-correct : ImplObligations) where
  open ImplObligations impl-correct

  -- For any reachable state,
  module _ {e}(st : SystemState e)(r : ReachableSystemState st)(eid : Fin e) where
   open import LibraBFT.Concrete.System sps-cor
   open PerState st r
   open PerEpoch eid

   import LibraBFT.Abstract.Records 𝓔 Hash _≟Hash_ (ConcreteVoteEvidence 𝓔) as Abs
   open import LibraBFT.Abstract.RecordChain 𝓔 Hash _≟Hash_ (ConcreteVoteEvidence 𝓔)
   open import LibraBFT.Abstract.System 𝓔 Hash _≟Hash_ (ConcreteVoteEvidence 𝓔)
   open import LibraBFT.Abstract.Properties 𝓔 Hash _≟Hash_ (ConcreteVoteEvidence 𝓔)

   open import LibraBFT.Abstract.Obligations.VotesOnce 𝓔 Hash _≟Hash_ (ConcreteVoteEvidence 𝓔)
   open import LibraBFT.Abstract.Obligations.LockedRound 𝓔 Hash _≟Hash_ (ConcreteVoteEvidence 𝓔)

   validState : ValidSysState ConcSystemState
   validState = record
     { vss-votes-once   = VO.Proof.voo sps-cor vo₁ vo₂ st r eid
     ; vss-locked-round = LR.Proof.lrr sps-cor lr₁ st r eid
     }

   open All-InSys-props (AbsSystemState.InSys ConcSystemState)

   -- commited blocks do not conflict.
   S5 : ∀{q q'}
      → {rc  : RecordChain (Abs.Q q)}  → All-InSys rc
      → {rc' : RecordChain (Abs.Q q')} → All-InSys rc'
      → {b b' : Abs.Block}
      → CommitRule rc  b
      → CommitRule rc' b'
      → NonInjective-≡ Abs.bId ⊎ ((Abs.B b) ∈RC rc' ⊎ (Abs.B b') ∈RC rc)
   S5 = CommitsDoNotConflict ConcSystemState validState


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

-- Pi combinators inspired by duals and traced monoidal categories

module PiPointedFracTrace where

open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import PiPointedFrac

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

dual : {A B : ∙𝕌} → (f : A ∙⟶ B) →  (Recipᵤ B ∙⟶ Recipᵤ A)
dual {A} {B} f = ∙uniti⋆l ∙⊚ (η A ∙⊗ ∙id⟷) ∙⊚ ((∙Singᵤ f ∙⊗ ∙id⟷) ∙⊗ ∙id⟷) ∙⊚
                 ∙assocr⋆ ∙⊚ (∙id⟷ ∙⊗ ∙swap⋆) ∙⊚ ∙assocl⋆ ∙⊚ (ε B ∙⊗ ∙id⟷) ∙⊚ ∙unite⋆l

-- name, coname
name : {A B : ∙𝕌} → (f : A ∙⟶ B) → ∙𝟙 ∙⟶ Singᵤ B ∙×ᵤ Recipᵤ A
name {A} {B} f = η A ∙⊚ (∙Singᵤ f ∙⊗ ∙id⟷)

coname : {A B : ∙𝕌} → (f : A ∙⟶ B) → Singᵤ A ∙×ᵤ Recipᵤ B ∙⟶ ∙𝟙
coname {A} {B} f = (∙Singᵤ f ∙⊗ ∙id⟷) ∙⊚ ε B

-- and 'trace' reveals something neat: we can't choose just any random 'a' and 'c'
-- to start with, but we need that make a coherence choice of a and c !!
trace : {A B C : ∙𝕌} → (f : A ∙×ᵤ C ∙⟶ B ∙×ᵤ C) → A ∙⟶ B
trace {A} {B} {C} f =
  ∙uniti⋆r ∙⊚                -- A ×ᵤ 1
  (return _ ∙⊗ η C) ∙⊚       -- A ×ᵤ (C ×ᵤ 1/C)
  ∙assocl⋆ ∙⊚                -- (A ×ᵤ C) ×ᵤ 1/C
  (tensor ∙⊗ ∙id⟷) ∙⊚    -- bring in the ●
  (∙Singᵤ f ∙⊗ ∙id⟷) ∙⊚  -- (B ×ᵤ C) ×ᵤ 1/C
  (untensor ∙⊗ ∙id⟷) ∙⊚  -- bring out the ●
  ∙assocr⋆ ∙⊚                -- B ×ᵤ (C ×ᵤ 1/C)
  (extract _ ∙⊗ ε C) ∙⊚
  ∙unite⋆r

-- Trace terminates!  The type C is pointed with point c; trace uses c
-- as the initial value for C. So f gets two values (a,c). It can do
-- whatever to produce (b',c'). But f is reversible so it is limited
-- to essentially either id or swap. Makes sense???

𝔹 : 𝕌
𝔹 = 𝟙 +ᵤ 𝟙

𝔽 𝕋 : ⟦ 𝔹 ⟧
𝔽 = inj₁ tt
𝕋 = inj₂ tt

zz1 : (A : 𝕌) (v : ⟦ A ⟧) → Σ (⟦ A ⟧ → ⟦ A ⟧) (λ f → f v ≡ v)
zz1 A v = ∙eval (trace {A # v} ∙swap⋆)

zz3 : (A : 𝕌) (v : ⟦ A ⟧) (T : ∙𝕌) → Σ (⟦ A ⟧ → ⟦ A ⟧) (λ f → f v ≡ v)
zz3 A v T = ∙eval (trace {A # v} {_} {T} ∙id⟷)

-- There are more thing you can put in trace as long as c is the fixpoint
NOT : 𝔹 ⟷ 𝔹
NOT = swap₊

CONTROLLED : {A : 𝕌} → (A ⟷ A) → 𝔹 ×ᵤ A ⟷ 𝔹 ×ᵤ A
CONTROLLED c = dist ⊚ (id⟷ ⊕ (id⟷ ⊗ c)) ⊚ factor

CNOT : 𝔹 ×ᵤ 𝔹 ⟷ 𝔹 ×ᵤ 𝔹
CNOT = CONTROLLED NOT

ex1 : ∀ {b} → 𝔹 # b ∙⟶ 𝔹 # b
ex1 = trace {C = 𝔹 # 𝔽} (∙swap⋆ ∙⊚ ∙#times ∙⊚ ∙c CNOT ∙⊚ ∙times# ∙⊚ ∙swap⋆)

-- Example in Sec. 4.3 from Abramsky's paper
-- http://www.cs.ox.ac.uk/files/341/calco05.pdf
∙q : {A1 A2 A3 A4 B1 B2 B3 B4 : ∙𝕌}
   → (f1 : A1 ∙⟶ B2)
   → (f2 : A2 ∙⟶ B4)
   → (f3 : A3 ∙⟶ B3)
   → (f4 : A4 ∙⟶ B1)
   → A1 ∙×ᵤ (A2 ∙×ᵤ (A3 ∙×ᵤ A4)) ∙⟶ B1 ∙×ᵤ (B2 ∙×ᵤ (B3 ∙×ᵤ B4))
∙q {A1} {A2} {A3} {A4} {B1} {B2} {B3} {B4} f1 f2 f3 f4 =
   (f1 ∙⊗ (f2 ∙⊗ (f3 ∙⊗ f4))) ∙⊚
   ∙assocl⋆ ∙⊚
   ∙swap⋆ ∙⊚
   ∙swap⋆ ∙⊗ ∙id⟷ ∙⊚
   ∙assocr⋆ ∙⊚ (∙id⟷ ∙⊗ ∙assocl⋆) ∙⊚
   ∙id⟷ ∙⊗ (∙swap⋆ ∙⊗ ∙id⟷ ∙⊚ ∙assocr⋆)

∙q' : {A1 U2 U3 U4 B1 : ∙𝕌}
    → (f1 : A1 ∙⟶ U2)
    → (f2 : U2 ∙⟶ U4)
    → (f3 : U3 ∙⟶ U3)
    → (f4 : U4 ∙⟶ B1)
    → A1 ∙⟶ B1
∙q' f1 f2 f3 f4 = trace (∙q f1 f2 f3 f4)

_⊸_ : (A B : ∙𝕌) → ∙𝕌
A ⊸ B = Recipᵤ A ∙×ᵤ Singᵤ B

id⊸ : {A : ∙𝕌} → (A ⊸ A) ∙⟶ ∙𝟙
id⊸ {A} = ∙swap⋆ ∙⊚ ε A

comp⊸ : (A B C : ∙𝕌) → (A ⊸ B) ∙×ᵤ (B ⊸ C) ∙⟶ (A ⊸ C)
comp⊸ A B C = ∙assocr⋆ ∙⊚
              ∙id⟷ ∙⊗ ∙assocl⋆ ∙⊚
              ∙id⟷ ∙⊗ (ε B ∙⊗ ∙id⟷) ∙⊚
              ∙id⟷ ∙⊗ ∙unite⋆l

app : (A B : ∙𝕌) → (A ⊸ B) ∙×ᵤ Singᵤ A ∙⟶ Singᵤ B
app A B = ∙swap⋆ ∙⊗ ∙id⟷ ∙⊚
          ∙assocr⋆ ∙⊚ (∙id⟷ ∙⊗ (∙swap⋆ ∙⊚ ε A)) ∙⊚
          ∙unite⋆r

-- B/A × D/C ⟷ B × D / A × C
dist×/ : {A B C D : ∙𝕌} → (A ⊸ B) ∙×ᵤ (C ⊸ D) ∙⟶ ((A ∙×ᵤ C) ⊸ (B ∙×ᵤ D))
dist×/ {A} {B} {C} {D} = ∙assocr⋆ ∙⊚
                         (∙id⟷ ∙⊗ ∙assocl⋆) ∙⊚
                         ∙id⟷ ∙⊗ (∙swap⋆ ∙⊗ ∙id⟷) ∙⊚
                         (∙id⟷ ∙⊗ ∙assocr⋆) ∙⊚ ∙assocl⋆ ∙⊚
                         c ∙⊗ tensor
  where
  c : (Recipᵤ A ∙×ᵤ Recipᵤ C) ∙⟶ Recipᵤ (A ∙×ᵤ C)
  c = ∙uniti⋆l ∙⊚
      (η (A ∙×ᵤ C) ∙⊗ ∙id⟷) ∙⊚
      (∙swap⋆ ∙⊗ ∙id⟷) ∙⊚
      ∙assocr⋆ ∙⊚
      (∙id⟷ ∙⊗ (untensor ∙⊗ ∙id⟷)) ∙⊚
      (∙id⟷ ∙⊗ (∙swap⋆ ∙⊗ ∙id⟷)) ∙⊚
      (∙id⟷ ∙⊗ ∙assocr⋆) ∙⊚
      (∙id⟷ ∙⊗ (∙id⟷ ∙⊗ ∙assocl⋆)) ∙⊚
      (∙id⟷ ∙⊗ (∙id⟷ ∙⊗ ((ε A ∙⊗ ∙id⟷) ∙⊚ ∙unite⋆l))) ∙⊚
      (∙id⟷ ∙⊗ ε C) ∙⊚
      ∙unite⋆r

-- 1/A x 1/B <-> 1 / (A x B)
rev× : {A B : ∙𝕌} → (A ⊸ ∙𝟙) ∙×ᵤ (B ⊸ ∙𝟙) ∙⟶ (A ∙×ᵤ B ⊸ ∙𝟙)
rev× {A} {B} = dist×/ ∙⊚ (∙id⟷ ∙⊗ ∙Singᵤ ∙unite⋆l)

-- (A <-> B) -> (1/A <-> 1/B)
rev : {A B : ∙𝕌} → (f : A ∙⟶ B) → Recipᵤ B ∙⟶ Recipᵤ A
rev {A} {B} f = dual f

-- A <-> 1 / (1/A)
revrev : {A : ∙𝕌} → Singᵤ A ∙⟶ Recipᵤ (Recipᵤ A)
revrev {A} = ∙uniti⋆r ∙⊚
             ∙id⟷ ∙⊗ η (Recipᵤ A) ∙⊚
             ∙assocl⋆ ∙⊚
             ((∙id⟷ ∙⊗ extract (Recipᵤ A)) ∙⊗ ∙id⟷) ∙⊚
             (ε A ∙⊗ ∙id⟷) ∙⊚
             ∙unite⋆l

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module McK-B where

open import CS410-Prelude
open import CS410-Nat
open import CS410-Vec

data Bit : Set where O I : Bit

exp2 : Nat -> Nat
exp2 zero    = 1
exp2 (suc n) = exp2 n +N exp2 n

WordNZ : Nat -> Set
data Word (n : Nat) : Set where
  O : Word n
  [_]  : WordNZ n -> Word n
WordNZ zero    = One
WordNZ (suc n) = (WordNZ n * Word n) + WordNZ n

_!_ : {n : Nat} -> Word n -> Word n -> Word (suc n)
O  ! O   = O
O  ! [ x ]  = [ inr x ]
[ x ] ! y      = [ inl (x , y) ]

_!+_ : {n : Nat} -> Word n -> WordNZ n -> WordNZ (suc n)
O  !+ y  = inr y
[ x ] !+ y  = inl (x , [ y ])

iNZ : (n : Nat) -> WordNZ n
iNZ zero = <>
iNZ (suc n) = inr (iNZ n)
i : {n : Nat} -> Word n
i {n} = [ iNZ n ] where

data WViewable : {n : Nat} -> Word n -> Set where
  O0 : WViewable {zero} O
  I0  : WViewable {zero} i
  _!!_  : {n : Nat}(x y : Word n) -> WViewable (x ! y)

wView : {n : Nat}(x : Word n) -> WViewable x
wView {zero} O    = O0
wView {zero} [ <> ]  = I0
wView {suc n} O   = O !! O
wView {suc n} [ inl (x , y) ] = [ x ] !! y
wView {suc n} [ inr      y  ] = O !! [ y ]

expand : {n : Nat} -> Word n -> Vec Bit (exp2 n)
expand x with wView x
expand .O      | O0   = O :: []
expand .([ <> ])  | I0    = I :: []
expand .(x ! y)   | x !! y  = expand x +V expand y

inc : {n : Nat}(x : Word n) -> One + WordNZ n
inc x with wView x
inc .O     | O0   = inr (iNZ zero)
inc .([ <> ]) | I0    = inl <>
inc .(x ! y)  | x !! y  with inc y
inc .(x ! y)  | x !! y  | inr y' = inr (x !+ y')
inc .(x ! y)  | x !! y  | inl <> with inc x
inc .(x ! y)  | x !! y  | inl <> | inr x'  = inr (inl (x' , O))
inc .(x ! y)  | x !! y  | inl <> | inl <>  = inl <>

incm : {n : Nat}(x : Word n) -> Word n
incm x with inc x
incm x | inl <> = O
incm x | inr x' = [ x' ]

fiveW2 : Word 2
fiveW2 = incm (incm (incm (incm (incm O))))

adc : {n : Nat} -> Word n -> Word n -> Bit -> Bit * Word n
adc x y c with wView x | wView y
adc .O .O O | O0 | O0 = O , O
adc .O .O I | O0 | O0 = O , i
adc .O .i O | O0 | I0 = O , i
adc .O .i I | O0 | I0 = I , O
adc .i .O O | I0 | O0 = O , i
adc .i .O I | I0 | O0 = I , O
adc .i .i O | I0 | I0 = I , O
adc .i .i I | I0 | I0 = I , i
adc .(xh ! xl) .(yh ! yl) c | xh !! xl | yh !! yl with adc xl yl c
... | cl , zl with adc xh yh cl
... | ch , zh = ch , zh ! zl

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module IdentP where

data Bool
  : Set
  where

  false
    : Bool

  true
    : Bool

f
  : {A : Set}
  → A
  → A
  → A
f x y
  = x

g
  : Bool
  → Bool
g false
  = true
g true
  = true

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
-- Andreas, 2018-09-03, issue #3207
--
-- Error message for disabled Prop.

{-# OPTIONS --no-prop #-}

test = Prop


text:
module Fin where

open import Prelude
open import Star
open import Modal
open import Nat

Fin : Nat -> Set
Fin = Any (\_ -> True)

fzero : {n : Nat} -> Fin (suc n)
fzero = done _ • ε

fsuc : {n : Nat} -> Fin n -> Fin (suc n)
fsuc i = step • i


text:
module HasDecidableSalvation where

open import OscarPrelude
open import HasSalvation

record HasDecidableSalvation (A : Set) : Set₁
 where
  field
    ⦃ hasSalvation ⦄ : HasSalvation A
    ▷?_ : (x : A) → Dec $ ▷ x

open HasDecidableSalvation ⦃ … ⦄ public

{-# DISPLAY HasDecidableSalvation.▷?_ _ = ▷?_ #-}


text:
{-

A couple of general facts about equivalences:

- if f is an equivalence then (cong f) is an equivalence ([equivCong])
- if f is an equivalence then pre- and postcomposition with f are equivalences ([preCompEquiv], [postCompEquiv])
- if f is an equivalence then (Σ[ g ] section f g) and (Σ[ g ] retract f g) are contractible ([isContr-section], [isContr-retract])

- isHAEquiv is a proposition [isPropIsHAEquiv]
(these are not in 'Equiv.agda' because they need Univalence.agda (which imports Equiv.agda))
-}
{-# OPTIONS --safe #-}
module Cubical.Foundations.Equiv.Properties where

open import Cubical.Core.Everything

open import Cubical.Data.Sigma

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

open import Cubical.Functions.FunExtEquiv

private
  variable
    ℓ ℓ′ ℓ′′ : Level
    A B C : Type ℓ

isEquivInvEquiv : isEquiv (λ (e : A ≃ B) → invEquiv e)
isEquivInvEquiv = isoToIsEquiv goal where
  open Iso
  goal : Iso (A ≃ B) (B ≃ A)
  goal .fun = invEquiv
  goal .inv = invEquiv
  goal .rightInv g = equivEq refl
  goal .leftInv f = equivEq refl

invEquivEquiv : (A ≃ B) ≃ (B ≃ A)
invEquivEquiv = _ , isEquivInvEquiv

isEquivCong : {x y : A} (e : A ≃ B) → isEquiv (λ (p : x ≡ y) → cong (equivFun e) p)
isEquivCong e = isoToIsEquiv (congIso (equivToIso e))

congEquiv : {x y : A} (e : A ≃ B) → (x ≡ y) ≃ (equivFun e x ≡ equivFun e y)
congEquiv e = isoToEquiv (congIso (equivToIso e))

equivAdjointEquiv : (e : A ≃ B) → ∀ {a b} → (a ≡ invEq e b) ≃ (equivFun e a ≡ b)
equivAdjointEquiv e = compEquiv (congEquiv e) (compPathrEquiv (secEq e _))

invEq≡→equivFun≡ : (e : A ≃ B) → ∀ {a b} → invEq e b ≡ a → equivFun e a ≡ b
invEq≡→equivFun≡ e = equivFun (equivAdjointEquiv e) ∘ sym

isEquivPreComp : (e : A ≃ B) → isEquiv (λ (φ : B → C) → φ ∘ equivFun e)
isEquivPreComp e = snd (equiv→ (invEquiv e) (idEquiv _))

preCompEquiv : (e : A ≃ B) → (B → C) ≃ (A → C)
preCompEquiv e = (λ φ → φ ∘ fst e) , isEquivPreComp e

isEquivPostComp : (e : A ≃ B) → isEquiv (λ (φ : C → A) → e .fst ∘ φ)
isEquivPostComp e = snd (equivΠCod (λ _ → e))

postCompEquiv : (e : A ≃ B) → (C → A) ≃ (C → B)
postCompEquiv e = _ , isEquivPostComp e

-- see also: equivΠCod for a dependent version of postCompEquiv

hasSection : (A → B) → Type _
hasSection {A = A} {B = B} f = Σ[ g ∈ (B → A) ] section f g

hasRetract : (A → B) → Type _
hasRetract {A = A} {B = B} f = Σ[ g ∈ (B → A) ] retract f g

isEquiv→isContrHasSection : {f : A → B} → isEquiv f → isContr (hasSection f)
fst (isEquiv→isContrHasSection isEq) = invIsEq isEq , secIsEq isEq
snd (isEquiv→isContrHasSection isEq) (f , ε) i = (λ b → fst (p b i)) , (λ b → snd (p b i))
  where p : ∀ b → (invIsEq isEq b , secIsEq isEq b) ≡ (f b , ε b)
        p b = isEq .equiv-proof b .snd (f b , ε b)

isEquiv→hasSection : {f : A → B} → isEquiv f → hasSection f
isEquiv→hasSection = fst ∘ isEquiv→isContrHasSection

isContr-hasSection : (e : A ≃ B) → isContr (hasSection (fst e))
isContr-hasSection e = isEquiv→isContrHasSection (snd e)

isEquiv→isContrHasRetract : {f : A → B} → isEquiv f → isContr (hasRetract f)
fst (isEquiv→isContrHasRetract isEq) = invIsEq isEq , retIsEq isEq
snd (isEquiv→isContrHasRetract {f = f} isEq) (g , η) =
    λ i → (λ b → p b i) , (λ a →  q a i)
  where p : ∀ b → invIsEq isEq b ≡ g b
        p b = sym (η (invIsEq isEq b)) ∙' cong g (secIsEq isEq b)
        -- one square from the definition of invIsEq
        ieSq : ∀ a → Square (cong g (secIsEq isEq (f a)))
                            refl
                            (cong (g ∘ f) (retIsEq isEq a))
                            refl
        ieSq a k j = g (commSqIsEq isEq a k j)
        -- one square from η
        ηSq : ∀ a → Square (η (invIsEq isEq (f a)))
                           (η a)
                           (cong (g ∘ f) (retIsEq isEq a))
                           (retIsEq isEq a)
        ηSq a i j = η (retIsEq isEq a i) j
        -- and one last square from the definition of p
        pSq : ∀ b → Square (η (invIsEq isEq b))
                           refl
                           (cong g (secIsEq isEq b))
                           (p b)
        pSq b i j = compPath'-filler (sym (η (invIsEq isEq b))) (cong g (secIsEq isEq b)) j i
        q : ∀ a → Square (retIsEq isEq a) (η a) (p (f a)) refl
        q a i j = hcomp (λ k → λ { (i = i0) → ηSq a j k
                                 ; (i = i1) → η a (j ∧ k)
                                 ; (j = i0) → pSq (f a) i k
                                 ; (j = i1) → η a k
                                 })
                        (ieSq a j i)

isEquiv→hasRetract : {f : A → B} → isEquiv f → hasRetract f
isEquiv→hasRetract = fst ∘ isEquiv→isContrHasRetract

isContr-hasRetract : (e : A ≃ B) → isContr (hasRetract (fst e))
isContr-hasRetract e = isEquiv→isContrHasRetract (snd e)

cong≃ : (F : Type ℓ → Type ℓ′) → (A ≃ B) → F A ≃ F B
cong≃ F e = pathToEquiv (cong F (ua e))

cong≃-char : (F : Type ℓ → Type ℓ′) {A B : Type ℓ} (e : A ≃ B) → ua (cong≃ F e) ≡ cong F (ua e)
cong≃-char F e = ua-pathToEquiv (cong F (ua e))

cong≃-idEquiv : (F : Type ℓ → Type ℓ′) (A : Type ℓ) → cong≃ F (idEquiv A) ≡ idEquiv (F A)
cong≃-idEquiv F A = cong≃ F (idEquiv A) ≡⟨ cong (λ p → pathToEquiv (cong F p)) uaIdEquiv  ⟩
                    pathToEquiv refl    ≡⟨ pathToEquivRefl ⟩
                    idEquiv (F A)       ∎

isPropIsHAEquiv : {f : A → B} → isProp (isHAEquiv f)
isPropIsHAEquiv {f = f} ishaef = goal ishaef where
  equivF : isEquiv f
  equivF = isHAEquiv→isEquiv ishaef

  rCoh1 : (sec : hasSection f) → Type _
  rCoh1 (g , ε) = Σ[ η ∈ retract f g ] ∀ x → cong f (η x) ≡ ε (f x)

  rCoh2 : (sec : hasSection f) → Type _
  rCoh2 (g , ε) = Σ[ η ∈ retract f g ] ∀ x → Square (ε (f x)) refl (cong f (η x)) refl

  rCoh3 : (sec : hasSection f) → Type _
  rCoh3 (g , ε) = ∀ x → Σ[ ηx ∈ g (f x) ≡ x ] Square (ε (f x)) refl (cong f ηx) refl

  rCoh4 : (sec : hasSection f) → Type _
  rCoh4 (g , ε) = ∀ x → Path (fiber f (f x)) (g (f x) , ε (f x)) (x , refl)

  characterization : isHAEquiv f ≃ Σ _ rCoh4
  characterization =
    isHAEquiv f
      -- first convert between Σ and record
      ≃⟨ isoToEquiv (iso (λ e → (e .g , e .rinv) , (e .linv , e .com))
                         (λ e → record { g = e .fst .fst ; rinv = e .fst .snd
                                       ; linv = e .snd .fst ; com = e .snd .snd })
                         (λ _ → refl) λ _ → refl) ⟩
    Σ _ rCoh1
      -- secondly, convert the path into a dependent path for later convenience
      ≃⟨  Σ-cong-equiv-snd (λ s → Σ-cong-equiv-snd
                             λ η → equivΠCod
                               λ x → compEquiv (flipSquareEquiv {a₀₀ = f x}) (invEquiv slideSquareEquiv)) ⟩
    Σ _ rCoh2
      ≃⟨ Σ-cong-equiv-snd (λ s → invEquiv Σ-Π-≃) ⟩
    Σ _ rCoh3
      ≃⟨ Σ-cong-equiv-snd (λ s → equivΠCod λ x → ΣPath≃PathΣ) ⟩
    Σ _ rCoh4
      ■
    where open isHAEquiv

  goal : isProp (isHAEquiv f)
  goal = subst isProp (sym (ua characterization))
    (isPropΣ (isContr→isProp (isEquiv→isContrHasSection equivF))
             λ s → isPropΠ λ x → isProp→isSet (isContr→isProp (equivF .equiv-proof (f x))) _ _)

-- loop spaces connected by a path are equivalent
conjugatePathEquiv : {A : Type ℓ} {a b : A} (p : a ≡ b) → (a ≡ a) ≃ (b ≡ b)
conjugatePathEquiv p = compEquiv (compPathrEquiv p) (compPathlEquiv (sym p))

-- composition on the right induces an equivalence of path types
compr≡Equiv : {A : Type ℓ} {a b c : A} (p q : a ≡ b) (r : b ≡ c) → (p ≡ q) ≃ (p ∙ r ≡ q ∙ r)
compr≡Equiv p q r = congEquiv ((λ s → s ∙ r) , compPathr-isEquiv r)

-- composition on the left induces an equivalence of path types
compl≡Equiv : {A : Type ℓ} {a b c : A} (p : a ≡ b) (q r : b ≡ c) → (q ≡ r) ≃ (p ∙ q ≡ p ∙ r)
compl≡Equiv p q r = congEquiv ((λ s → p ∙ s) , (compPathl-isEquiv p))

isEquivFromIsContr : {A : Type ℓ} {B : Type ℓ′}
                   → (f : A → B) → isContr A → isContr B
                   → isEquiv f
isEquivFromIsContr f isContrA isContrB =
  subst isEquiv (λ i x → isContr→isProp isContrB (fst B≃A x) (f x) i) (snd B≃A)
  where B≃A = isContr→Equiv isContrA isContrB

isEquiv[f∘equivFunA≃B]→isEquiv[f] : {A : Type ℓ} {B : Type ℓ′} {C : Type ℓ′′}
                 → (f : B → C) (A≃B : A ≃ B)
                 → isEquiv (f ∘ equivFun A≃B)
                 → isEquiv f
isEquiv[f∘equivFunA≃B]→isEquiv[f] f (g , gIsEquiv) f∘gIsEquiv  =
  precomposesToId→Equiv f _ w w'
    where
      w : f ∘ g ∘ equivFun (invEquiv (_ , f∘gIsEquiv)) ≡ idfun _
      w = (cong fst (invEquiv-is-linv (_ , f∘gIsEquiv)))

      w' : isEquiv (g ∘ equivFun (invEquiv (_ , f∘gIsEquiv)))
      w' = (snd (compEquiv (invEquiv (_ , f∘gIsEquiv) ) (_ , gIsEquiv)))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module List where

  import Prelude
  import Equiv
  import Datoid
  import Nat

  open Prelude
  open Equiv
  open Datoid
  open Nat

  data List (a : Set) : Set where
    nil  : List a
    _::_ : a -> List a -> List a

  map : {a b : Set} -> (a -> b) -> List a -> List b
  map f nil       = nil
  map f (x :: xs) = f x :: map f xs

  member : (a : Datoid) -> El a -> List (El a) -> Set
  member _ x nil       = Absurd
  member a x (y :: ys) = Either (rel' (datoidEq a) x y) (member a x ys)

  memberPreservesEq
    :  {a : Datoid}
    -> {x y : El a}
    -> datoidRel a x y
    -> (zs : List (El a))
    -> member a x zs
    -> member a y zs
  memberPreservesEq     xy nil       abs         = abs
  memberPreservesEq {a} xy (z :: zs) (left xz)   =
    left  (dTrans a (dSym a xy) xz)
  memberPreservesEq {a} xy (z :: zs) (right xzs) =
    right (memberPreservesEq {a} xy zs xzs)

  private
    noCopies' : (a : Datoid) -> (x y : El a) -> Dec (datoidRel a x y)
              -> Nat -> Nat
    noCopies' _ _ _ (left _)  n = suc n
    noCopies' _ _ _ (right _) n = n

  noCopies : (a : Datoid) -> El a -> List (El a) -> Nat
  noCopies a x nil       = zero
  noCopies a x (y :: ys) =
    noCopies' a x y (datoidDecRel a x y) (noCopies a x ys)

  NoDuplicates : (a : Datoid) -> List (El a) -> Set
  NoDuplicates _ nil      = Unit
  NoDuplicates a (x :: b) = Pair (Not (member a x b)) (NoDuplicates a b)

  private
    delete'
      : (a : Datoid)
      -> (x y : El a)
      -> Dec (datoidRel a x y)
      -> (ys delXYs : List (El a))
      -> List (El a)
    delete' _ _ _ (left _)  ys _      = ys
    delete' _ _ _ (right _) _  delXYs = delXYs

  -- Removes first occurrence if any.
  delete : (a : Datoid) -> El a -> List (El a) -> List (El a)
  delete a x nil       = nil
  delete a x (y :: ys) = delete' a x y (datoidDecRel a x y) ys (delete a x ys)

  private
    Perm : (a : Datoid) -> (xs ys : List (El a)) -> Set
    Perm a xs ys = forall z -> datoidRel natDatoid (noCopies a z xs)
                                                   (noCopies a z ys)

    refl' : {a : Datoid} -> (xs : List (El a)) -> Perm a xs xs
    refl' {a} xs = \z -> dRefl natDatoid {noCopies a z xs}

    sym' :  {a : Datoid} -> (xs ys : List (El a))
         -> Perm a xs ys -> Perm a ys xs
    sym' {a} xs ys xy =
      \z -> dSym natDatoid {noCopies a z xs} {noCopies a z ys} (xy z)

    trans' : {a : Datoid} -> (xs ys zs : List (El a))
           -> Perm a xs ys -> Perm a ys zs -> Perm a xs zs
    trans' {a} xs ys zs xy yz =
      \z -> dTrans natDatoid
                   {noCopies a z xs} {noCopies a z ys} {noCopies a z zs}
                   (xy z) (yz z)

    postulate
      dec' : {a : Datoid} -> (xs ys : List (El a))
             -> Either (Perm a xs ys) (Not (Perm a xs ys))

  Permutation : (a : Datoid) -> DecidableEquiv (List (El a))
  Permutation a = decEquiv (equiv (Perm a) (refl' {a}) (sym' {a}) (trans' {a})) (dec (dec' {a}))


text:
interleaved mutual

  data CoNat : Set
  record ∞CoNat : Set

  constructor
    zero : CoNat

  record ∞CoNat where
    coinductive
    field force : CoNat

  constructor
    suc : ∞CoNat → ?

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------------
-- Inductive PA properties using the induction principle
------------------------------------------------------------------------------

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

module PA.Inductive.PropertiesByInductionI where

open import PA.Inductive.Base

open import PA.Inductive.PropertiesByInduction
open import PA.Inductive.Relation.Binary.EqReasoning

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

+-comm : ∀ m n → m + n ≡ n + m
+-comm m n = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + n ≡ n + i

  A0 : A zero
  A0 = sym (+-rightIdentity n)

  is : ∀ i → A i → A (succ i)
  is i ih = succ (i + n) ≡⟨ succCong ih ⟩
            succ (n + i) ≡⟨ sym (x+Sy≡S[x+y] n i) ⟩
            n + succ i   ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2014-03-27 fixed issue

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

open import Common.Size

record R (i : Size) : Set where
  inductive
  constructor c
  field
    j : Size< i
    r : R j

data ⊥ : Set where

elim : (i : Size) → R i → ⊥
elim i (c j r) = elim j r

-- elim should be rejected by termination checker.

-- Being accepted, its is translated into
--
--   elim i x = elim (R.j x) (R.r x)
--
-- which is making reduceHead in the injectivity checker
-- produce larger and larger applications of elim.
-- Leading to a stack overflow.

inh : R ∞
R.j inh = ∞
R.r inh = inh

-- inh should also be rejected

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module Rationals.Properties where

open import Nats renaming (_*_ to _:*:_)
open import Rationals
open import Data.Empty
open import Data.Product
open import Equality

------------------------------------------------------------------------
-- internal stuffs

private

  a*b÷b=a : ∀ a b → a :*: b ÷ b →ℕ ≡ (a , refl)
  a*b÷b=a _ _ = refl

------------------------------------------------------------------------
-- public aliases

times-div-id : ∀ a b → a :*: b ÷ b →ℕ ≡ (a , refl)
times-div-id = a*b÷b=a


text:
module RandomAccessList.Standard.Core where

open import BuildingBlock.BinaryLeafTree using (BinaryLeafTree; Node; Leaf)

open import Data.Nat
open import Data.Nat.Etc

--  parameterized by the level of the least significant digit
data 0-1-RAL (A : Set) : ℕ → Set where
    []   : ∀ {n} →                                          0-1-RAL A n
    0∷_  : ∀ {n} →                      0-1-RAL A (suc n) → 0-1-RAL A n
    _1∷_ : ∀ {n} → BinaryLeafTree A n → 0-1-RAL A (suc n) → 0-1-RAL A n

--------------------------------------------------------------------------------
-- to ℕ

⟦_⟧ₙ : ∀ {A n} → 0-1-RAL A n → ℕ
⟦      [] ⟧ₙ = 0
⟦   0∷ xs ⟧ₙ =     2 * ⟦ xs ⟧ₙ
⟦ x 1∷ xs ⟧ₙ = 1 + 2 * ⟦ xs ⟧ₙ

⟦_⟧ : ∀ {n A} → 0-1-RAL A n → ℕ
⟦_⟧ {n} xs = (2 ^ n) * ⟦ xs ⟧ₙ

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
------------------------------------------------------------------------------
-- Test the consistency of PA.Axiomatic.Standard.Base
------------------------------------------------------------------------------

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

-- In the module PA.Axiomatic.Standard.Base we declare Agda postulates
-- as first-order logic axioms. We test if it is possible to prove an
-- unprovable theorem from these axioms.

module PA.Axiomatic.Standard.Base.Consistency.Axioms where

open import PA.Axiomatic.Standard.Base

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

postulate impossible : (m n : ℕ) → m ≡ n
{-# ATP prove impossible #-}


text:
-- Box modality: cofree presheaf on a family
module SOAS.Abstract.Box {T : Set} where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Sorting
open import SOAS.Variable
open import SOAS.Families.Core {T}
open import SOAS.Families.Isomorphism
open import SOAS.Families.BCCC using (_×ₘ_; _+ₘ_; _⇨_; _⇨̣_)

open import SOAS.Abstract.Hom

open import Categories.Functor.Bifunctor

module Unsorted where
  -- Box modality: the skew-closed action of variables on a family
  □ : Family → Family
  □ X = ⟨ ℐ , X ⟩

  -- □ is an endofunctor on families
  □F : Functor 𝔽amilies 𝔽amilies
  □F = appˡ ⟨-,-⟩F ℐ

  -- | Properties of □

  private
    variable
      X Y : Family

  -- | □ preserves products of families
  □[X×Y]≅□X×□Y : □ (X ×ₘ Y) ≅ₘ (□ X ×ₘ □ Y)
  □[X×Y]≅□X×□Y = ⟨𝒳,Y×Z⟩≅⟨𝒳,Y⟩×⟨𝒳,Z⟩

  -- □ can be factored out from a sum
  □X+□Y⇾□[X+Y] : (□ X +ₘ □ Y) ⇾ □ (X +ₘ Y)
  □X+□Y⇾□[X+Y] = ⟨𝒳,Y⟩+⟨𝒳,Z⟩⇾⟨𝒳,Y+Z⟩

module Sorted where

  -- Sorted box modality: the skew-closed hom of variables and a family
  □ : Familyₛ → Familyₛ
  □ X = 〖 ℐ , X 〗

  -- □ is an endofunctor on families
  □F : Functor 𝔽amiliesₛ 𝔽amiliesₛ
  □F = appˡ 〖-,-〗F ℐ

  □₁ : {X Y : Familyₛ} → (X ⇾̣ Y) → □ X ⇾̣ □ Y
  □₁ f x ρ = f (x ρ)

  ζ : (X : Familyₛ) → □ X ⇾̣ □ (□ X)
  ζ X b ρ ϱ = b (ϱ ∘ ρ)

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- 2011-10-04 Andreas
{-# OPTIONS --experimental-irrelevance #-}
module TerminationOnIrrelevant where

data ⊥ : Set where

data Empty : Set where
  c : Empty → Empty

d : Empty → Empty
d (c x) = x

f : .Empty → ⊥
f (c x) = f x

g : .Empty → ⊥
g (c x) = g x

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

-- the following would loop if we evaluated f x to f (d x)
mayloop : .(x y : Empty) → f x ≡ g y
mayloop x y = refl

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
module RepeatedVariableInPattern where

K : Set -> Set
K A A = A


text:
module Categories.Functor.CartesianClosed where

open import Categories.Category using (Category; _[_∘_]; _[_,_])
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.CartesianClosed using (CartesianClosed)
open import Categories.Category.CartesianClosed.Bundle using (CartesianClosedCategory)
open import Categories.Functor using (Functor)
open import Categories.Functor.Cartesian using (IsCartesianF)
import Categories.Morphism as Morphism

open import Level

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

record IsCartesianClosedF
  (C : CartesianClosedCategory o ℓ e)
  (D : CartesianClosedCategory o′ ℓ′ e′)
  (F : Functor (CartesianClosedCategory.U C) (CartesianClosedCategory.U D))
  : Set (levelOfTerm C ⊔ levelOfTerm D) where
  open Morphism (CartesianClosedCategory.U D) using (IsIso; Iso)
  open Functor F

  private
    CU = CartesianClosedCategory.U C
    DU = CartesianClosedCategory.U D
    CC₁ = CartesianClosedCategory.cartesianClosed C
    CC₂ = CartesianClosedCategory.cartesianClosed D
    C₁ = CartesianClosed.cartesian CC₁
    C₂ = CartesianClosed.cartesian CC₂
    C′ = record { U = CU ; cartesian = C₁ }
    D′ = record { U = DU ; cartesian = C₂ }
    _^C_ = CartesianClosed._^_ CC₁
    _^D_ = CartesianClosed._^_ CC₂

  field
    isCartesianF : IsCartesianF C′ D′ F

  module isCartesianF = IsCartesianF isCartesianF

  conv : forall {A B : Category.Obj CU} -> DU [ F₀ (B ^C A) , F₀ B ^D F₀ A ]
  conv {A} {B} =
    CartesianClosed.λg CC₂
      (DU [ F₁ (CartesianClosed.eval′ CC₁) ∘ IsCartesianF.×-iso.to isCartesianF (B ^C A) A ])

  field
    F-preserve-^ : forall {A B : Category.Obj CU} -> IsIso (conv {A} {B})

  module F-preserve-^ {A B : Category.Obj CU} = IsIso (F-preserve-^ {A} {B})

  -- Note that F is called strict if `conv` ≈ id.

record CartesianClosedF
  (C : CartesianClosedCategory o ℓ e)
  (D : CartesianClosedCategory o′ ℓ′ e′)
  : Set (levelOfTerm C ⊔ levelOfTerm D) where
  field
    F : Functor (CartesianClosedCategory.U C) (CartesianClosedCategory.U D)
    isCartesianClosed : IsCartesianClosedF C D F

  open Functor F public
  open IsCartesianClosedF isCartesianClosed public

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
module Issue2937.WithUnicode where

foo : _ → _ → Set
foo bar x =  λ x → foo (bar x {!!}) x