text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties about subsets
------------------------------------------------------------------------

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

module Data.Fin.Subset.Properties where

import Algebra.Definitions as AlgebraicDefinitions
import Algebra.Structures as AlgebraicStructures
open import Algebra.Bundles
import Algebra.Properties.Lattice as L
import Algebra.Properties.DistributiveLattice as DL
import Algebra.Properties.BooleanAlgebra as BA
open import Data.Bool.Base using (not)
open import Data.Bool.Properties
open import Data.Fin.Base using (Fin; suc; zero)
open import Data.Fin.Subset
open import Data.Fin.Properties using (any?; decFinSubset)
open import Data.Nat.Base
import Data.Nat.Properties as ℕₚ
open import Data.Product as Product using (∃; ∄; _×_; _,_; proj₁)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Vec.Base
open import Data.Vec.Properties
open import Function.Base using (_∘_; const; id; case_of_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Binary as B hiding (Decidable)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (Dec; yes; no)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Unary using (Pred; Decidable; Satisfiable)

------------------------------------------------------------------------
-- Constructor mangling

drop-there : ∀ {s n x} {p : Subset n} → suc x ∈ s ∷ p → x ∈ p
drop-there (there x∈p) = x∈p

drop-not-there : ∀ {s n x} {p : Subset n} → suc x ∉ s ∷ p → x ∉ p
drop-not-there x∉sp x∈p = contradiction (there x∈p) x∉sp

drop-∷-⊆ : ∀ {n s₁ s₂} {p₁ p₂ : Subset n} → s₁ ∷ p₁ ⊆ s₂ ∷ p₂ → p₁ ⊆ p₂
drop-∷-⊆ p₁s₁⊆p₂s₂ x∈p₁ = drop-there (p₁s₁⊆p₂s₂ (there x∈p₁))

drop-∷-⊂ : ∀ {n s} {p₁ p₂ : Subset n} → s ∷ p₁ ⊂ s ∷ p₂ → p₁ ⊂ p₂
drop-∷-⊂ {s = inside} (_       , zero  ,      x∈sp₂ , x∉sp₁) = contradiction here x∉sp₁
drop-∷-⊂ {s}          (sp₁⊆sp₂ , suc x , there x∈p₂ , x∉sp₁) = drop-∷-⊆ sp₁⊆sp₂ , x , x∈p₂ , drop-not-there x∉sp₁

module _ {n} {p q : Subset n} where

  out⊆ : ∀ {y} → p ⊆ q → outside ∷ p ⊆ y ∷ q
  out⊆ p⊆q (there ∈p) = there (p⊆q ∈p)

  out⊆-⇔ : ∀ {y} → p ⊆ q ⇔ outside ∷ p ⊆ y ∷ q
  out⊆-⇔ = equivalence out⊆ drop-∷-⊆

  in⊆in : p ⊆ q → inside ∷ p ⊆ inside ∷ q
  in⊆in p⊆q here = here
  in⊆in p⊆q (there ∈p) = there (p⊆q ∈p)

  in⊆in-⇔ : p ⊆ q ⇔ inside ∷ p ⊆ inside ∷ q
  in⊆in-⇔ = equivalence in⊆in drop-∷-⊆

  s⊆s : ∀ {s} →  p ⊆ q → s ∷ p ⊆ s ∷ q
  s⊆s p⊆q here = here
  s⊆s p⊆q (there ∈p) = there (p⊆q ∈p)

  out⊂ : ∀ {y} → p ⊂ q → outside ∷ p ⊂ y ∷ q
  out⊂ (p⊆q , x , x∈q , x∉p) = out⊆ p⊆q , suc x , there x∈q , x∉p ∘ drop-there

  out⊂in : p ⊆ q → outside ∷ p ⊂ inside ∷ q
  out⊂in p⊆q = out⊆ p⊆q , zero , here , λ ()

  out⊂in-⇔ : p ⊆ q ⇔ outside ∷ p ⊂ inside ∷ q
  out⊂in-⇔ = equivalence out⊂in (drop-∷-⊆ ∘ proj₁)

  out⊂out-⇔ : p ⊂ q ⇔ outside ∷ p ⊂ outside ∷ q
  out⊂out-⇔ = equivalence out⊂ drop-∷-⊂

  in⊂in : p ⊂ q → inside ∷ p ⊂ inside ∷ q
  in⊂in (p⊆q , x , x∈q , x∉p) = in⊆in p⊆q , suc x , there x∈q , x∉p ∘ drop-there

  in⊂in-⇔ : p ⊂ q ⇔ inside ∷ p ⊂ inside ∷ q
  in⊂in-⇔ = equivalence in⊂in drop-∷-⊂

------------------------------------------------------------------------
-- _∈_

infix 4 _∈?_
_∈?_ : ∀ {n} x (p : Subset n) → Dec (x ∈ p)
zero  ∈? inside  ∷ p = yes here
zero  ∈? outside ∷ p = no  λ()
suc n ∈? s       ∷ p = Dec.map′ there drop-there (n ∈? p)

------------------------------------------------------------------------
-- Empty

drop-∷-Empty : ∀ {n s} {p : Subset n} → Empty (s ∷ p) → Empty p
drop-∷-Empty ¬∃∈ (x , x∈p) = ¬∃∈ (suc x , there x∈p)

Empty-unique : ∀ {n} {p : Subset n} → Empty p → p ≡ ⊥
Empty-unique {_} {[]}          ¬∃∈ = refl
Empty-unique {_} {inside  ∷ p} ¬∃∈ = contradiction (zero , here) ¬∃∈
Empty-unique {_} {outside ∷ p} ¬∃∈ =
  cong (outside ∷_) (Empty-unique (drop-∷-Empty ¬∃∈))

nonempty? : ∀ {n} → Decidable (Nonempty {n})
nonempty? p = any? (_∈? p)

------------------------------------------------------------------------
-- ∣_∣

∣p∣≤n : ∀ {n} (p : Subset n) → ∣ p ∣ ≤ n
∣p∣≤n = count≤n (_≟ inside)

------------------------------------------------------------------------
-- ⊥

∉⊥ : ∀ {n} {x : Fin n} → x ∉ ⊥
∉⊥ (there p) = ∉⊥ p

⊥⊆ : ∀ {n} {p : Subset n} → ⊥ ⊆ p
⊥⊆ x∈⊥ = contradiction x∈⊥ ∉⊥

∣⊥∣≡0 : ∀ n → ∣ ⊥ {n = n} ∣ ≡ 0
∣⊥∣≡0 zero    = refl
∣⊥∣≡0 (suc n) = ∣⊥∣≡0 n

------------------------------------------------------------------------
-- ⊤

∈⊤ : ∀ {n} {x : Fin n} → x ∈ ⊤
∈⊤ {x = zero}  = here
∈⊤ {x = suc x} = there ∈⊤

⊆⊤ : ∀ {n} {p : Subset n} → p ⊆ ⊤
⊆⊤ = const ∈⊤

∣⊤∣≡n : ∀ n → ∣ ⊤ {n = n} ∣ ≡ n
∣⊤∣≡n zero    = refl
∣⊤∣≡n (suc n) = cong suc (∣⊤∣≡n n)

∣p∣≡n⇒p≡⊤ : ∀ {n} {p : Subset n} → ∣ p ∣ ≡ n → p ≡ ⊤
∣p∣≡n⇒p≡⊤ {p = []}          _     = refl
∣p∣≡n⇒p≡⊤ {p = outside ∷ p} |p|≡n = contradiction |p|≡n (ℕₚ.<⇒≢ (s≤s (∣p∣≤n p)))
∣p∣≡n⇒p≡⊤ {p = inside  ∷ p} |p|≡n = cong (inside ∷_) (∣p∣≡n⇒p≡⊤ (ℕₚ.suc-injective |p|≡n))

------------------------------------------------------------------------
-- ⁅_⁆

x∈⁅x⁆ : ∀ {n} (x : Fin n) → x ∈ ⁅ x ⁆
x∈⁅x⁆ zero    = here
x∈⁅x⁆ (suc x) = there (x∈⁅x⁆ x)

x∈⁅y⁆⇒x≡y : ∀ {n x} (y : Fin n) → x ∈ ⁅ y ⁆ → x ≡ y
x∈⁅y⁆⇒x≡y zero    here      = refl
x∈⁅y⁆⇒x≡y zero    (there p) = contradiction p ∉⊥
x∈⁅y⁆⇒x≡y (suc y) (there p) = cong suc (x∈⁅y⁆⇒x≡y y p)

x∈⁅y⁆⇔x≡y : ∀ {n} {x y : Fin n} → x ∈ ⁅ y ⁆ ⇔ x ≡ y
x∈⁅y⁆⇔x≡y {_} {x} {y} = equivalence
  (x∈⁅y⁆⇒x≡y y)
  (λ x≡y → subst (λ y → x ∈ ⁅ y ⁆) x≡y (x∈⁅x⁆ x))

x≢y⇒x∉⁅y⁆ : ∀ {n} {x y : Fin n} → x ≢ y → x ∉ ⁅ y ⁆
x≢y⇒x∉⁅y⁆ x≢y = x≢y ∘ x∈⁅y⁆⇒x≡y _

x∉⁅y⁆⇒x≢y : ∀ {n} {x y : Fin n} → x ∉ ⁅ y ⁆ → x ≢ y
x∉⁅y⁆⇒x≢y x∉⁅x⁆ refl = x∉⁅x⁆ (x∈⁅x⁆ _)

∣⁅x⁆∣≡1 : ∀ {n} (i : Fin n) → ∣ ⁅ i ⁆ ∣ ≡ 1
∣⁅x⁆∣≡1 {suc n} zero    = cong suc (∣⊥∣≡0 n)
∣⁅x⁆∣≡1 {_}     (suc i) = ∣⁅x⁆∣≡1 i

------------------------------------------------------------------------
-- _⊆_

⊆-refl : ∀ {n} → Reflexive (_⊆_ {n})
⊆-refl = id

⊆-reflexive : ∀ {n} → _≡_ ⇒ (_⊆_ {n})
⊆-reflexive refl = ⊆-refl

⊆-trans : ∀ {n} → Transitive (_⊆_ {n})
⊆-trans p⊆q q⊆r x∈p = q⊆r (p⊆q x∈p)

⊆-antisym : ∀ {n} → Antisymmetric _≡_ (_⊆_ {n})
⊆-antisym {i = []}     {[]}     p⊆q q⊆p = refl
⊆-antisym {i = x ∷ xs} {y ∷ ys} p⊆q q⊆p with x | y
... | inside  | inside  = cong₂ _∷_ refl (⊆-antisym (drop-∷-⊆ p⊆q) (drop-∷-⊆ q⊆p))
... | inside  | outside = contradiction (p⊆q here) λ()
... | outside | inside  = contradiction (q⊆p here) λ()
... | outside | outside = cong₂ _∷_ refl (⊆-antisym (drop-∷-⊆ p⊆q) (drop-∷-⊆ q⊆p))

⊆-min : ∀ {n} → Minimum (_⊆_ {n}) ⊥
⊆-min (x ∷ xs) (there v∈⊥) = there (⊆-min xs v∈⊥)

⊆-max : ∀ {n} → Maximum (_⊆_ {n}) ⊤
⊆-max (inside ∷ xs) here         = here
⊆-max (x      ∷ xs) (there v∈xs) = there (⊆-max xs v∈xs)

infix 4 _⊆?_
_⊆?_ : ∀ {n} → B.Decidable (_⊆_ {n = n})
[]          ⊆? []          = yes id
outside ∷ p ⊆?       y ∷ q = Dec.map out⊆-⇔ (p ⊆? q)
inside  ∷ p ⊆? outside ∷ q = no (λ p⊆q → case (p⊆q here) of λ())
inside  ∷ p ⊆? inside  ∷ q = Dec.map in⊆in-⇔ (p ⊆? q)

module _ (n : ℕ) where

  ⊆-isPreorder : IsPreorder _≡_ (_⊆_ {n})
  ⊆-isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive     = ⊆-reflexive
    ; trans         = ⊆-trans
    }

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = record
    { isPreorder = ⊆-isPreorder
    }

  ⊆-isPartialOrder : IsPartialOrder _≡_ (_⊆_ {n})
  ⊆-isPartialOrder = record
    { isPreorder = ⊆-isPreorder
    ; antisym    = ⊆-antisym
    }

  ⊆-poset : Poset _ _ _
  ⊆-poset = record
    { isPartialOrder = ⊆-isPartialOrder
    }

p⊆q⇒∣p∣≤∣q∣ : ∀ {n} {p q : Subset n} → p ⊆ q → ∣ p ∣ ≤ ∣ q ∣
p⊆q⇒∣p∣≤∣q∣ {p = []}          {[]}          p⊆q = z≤n
p⊆q⇒∣p∣≤∣q∣ {p = outside ∷ p} {outside ∷ q} p⊆q = p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q)
p⊆q⇒∣p∣≤∣q∣ {p = outside ∷ p} {inside  ∷ q} p⊆q = ℕₚ.≤-step (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q))
p⊆q⇒∣p∣≤∣q∣ {p = inside  ∷ p} {outside ∷ q} p⊆q = contradiction (p⊆q here) λ()
p⊆q⇒∣p∣≤∣q∣ {p = inside  ∷ p} {inside  ∷ q} p⊆q = s≤s (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ p⊆q))

------------------------------------------------------------------------
-- _⊂_

p⊂q⇒p⊆q : ∀ {n} → {p q : Subset n} → p ⊂ q → p ⊆ q
p⊂q⇒p⊆q = proj₁

⊂-trans : ∀ {n} → Transitive (_⊂_ {n})
⊂-trans (p⊆q , x , x∈q , x∉p) (q⊆r , _ , _ , _) = ⊆-trans p⊆q q⊆r , x , q⊆r x∈q , x∉p

⊂-⊆-trans : ∀ {n} → Trans {A = Subset n} _⊂_ _⊆_ _⊂_
⊂-⊆-trans (p⊆q , x , x∈q , x∉p) q⊆r = ⊆-trans p⊆q q⊆r , x , q⊆r x∈q , x∉p

⊆-⊂-trans : ∀ {n} → Trans {A = Subset n} _⊆_ _⊂_ _⊂_
⊆-⊂-trans p⊆q (q⊆r , x , x∈r , x∉q) = ⊆-trans p⊆q q⊆r , x , x∈r , x∉q ∘ p⊆q

⊂-irref : ∀ {n} → Irreflexive _≡_ (_⊂_ {n})
⊂-irref refl (_ , x , x∈p , x∉q) = contradiction x∈p x∉q

⊂-antisym : ∀ {n} → Antisymmetric _≡_ (_⊂_ {n})
⊂-antisym (p⊆q , _) (q⊆p , _) = ⊆-antisym p⊆q q⊆p

⊂-asymmetric : ∀ {n} → Asymmetric (_⊂_ {n})
⊂-asymmetric (p⊆q , _) (_ , x , x∈p , x∉q) = contradiction (p⊆q x∈p) x∉q

infix 4 _⊂?_

_⊂?_ : ∀ {n} → B.Decidable (_⊂_ {n = n})
[]          ⊂? []          = no λ ()
outside ∷ p ⊂? outside ∷ q = Dec.map out⊂out-⇔ (p ⊂? q)
outside ∷ p ⊂? inside  ∷ q = Dec.map out⊂in-⇔ (p ⊆? q)
inside  ∷ p ⊂? outside ∷ q = no (λ {(p⊆q , _) → case (p⊆q here) of λ ()})
inside  ∷ p ⊂? inside  ∷ q = Dec.map in⊂in-⇔ (p ⊂? q)

module _ (n : ℕ) where

  ⊂-isStrictPartialOrder : IsStrictPartialOrder _≡_ (_⊂_ {n})
  ⊂-isStrictPartialOrder = record
    { isEquivalence = isEquivalence
    ; irrefl = ⊂-irref
    ; trans = ⊂-trans
    ; <-resp-≈ = (λ {refl → id}) , (λ {refl → id})
    }

  ⊂-strictPartialOrder : StrictPartialOrder _ _ _
  ⊂-strictPartialOrder = record
    { isStrictPartialOrder = ⊂-isStrictPartialOrder
    }

  ⊂-isDecStrictPartialOrder : IsDecStrictPartialOrder _≡_ (_⊂_ {n})
  ⊂-isDecStrictPartialOrder = record
    { isStrictPartialOrder = ⊂-isStrictPartialOrder
    ; _≟_ = ≡-dec _≟_
    ; _<?_ = _⊂?_
    }

  ⊂-decStrictPartialOrder : DecStrictPartialOrder _ _ _
  ⊂-decStrictPartialOrder = record
    { isDecStrictPartialOrder = ⊂-isDecStrictPartialOrder
    }

p⊂q⇒∣p∣<∣q∣ : ∀ {n} → {p q : Subset n} → p ⊂ q → ∣ p ∣ < ∣ q ∣
p⊂q⇒∣p∣<∣q∣ {p = outside ∷ p} {outside ∷ q} op⊂oq@(_     , _     , _ , _)    = p⊂q⇒∣p∣<∣q∣ (drop-∷-⊂ op⊂oq)
p⊂q⇒∣p∣<∣q∣ {p = outside ∷ p} {inside  ∷ q}       (op⊆iq , _     , _ , _)    = s≤s (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ op⊆iq))
p⊂q⇒∣p∣<∣q∣ {p = inside  ∷ p} {outside ∷ q}       (ip⊆oq , _     , _ , _)    = contradiction (ip⊆oq here) (λ ())
p⊂q⇒∣p∣<∣q∣ {p = inside  ∷ p} {inside  ∷ q}       (_     , zero  , _ , x∉ip) = contradiction here x∉ip
p⊂q⇒∣p∣<∣q∣ {p = inside  ∷ p} {inside  ∷ q} ip⊂iq@(_     , suc x , _ , _)    = s≤s (p⊂q⇒∣p∣<∣q∣ (drop-∷-⊂ ip⊂iq))

------------------------------------------------------------------------
-- ∁

x∈p⇒x∉∁p : ∀ {n x} {p : Subset n} → x ∈ p → x ∉ ∁ p
x∈p⇒x∉∁p (there x∈p) (there x∈∁p) = x∈p⇒x∉∁p x∈p x∈∁p

x∈∁p⇒x∉p : ∀ {n x} {p : Subset n} → x ∈ ∁ p → x ∉ p
x∈∁p⇒x∉p (there x∈∁p) (there x∈p) = x∈∁p⇒x∉p x∈∁p x∈p

x∉∁p⇒x∈p : ∀ {n x} {p : Subset n} → x ∉ ∁ p → x ∈ p
x∉∁p⇒x∈p {x = zero}  {outside ∷ p} x∉∁p = contradiction here x∉∁p
x∉∁p⇒x∈p {x = zero}  {inside  ∷ p} x∉∁p = here
x∉∁p⇒x∈p {x = suc x} {_       ∷ p} x∉∁p = there (x∉∁p⇒x∈p (x∉∁p ∘ there))

x∉p⇒x∈∁p : ∀ {n x} {p : Subset n} → x ∉ p → x ∈ ∁ p
x∉p⇒x∈∁p {x = zero}  {outside ∷ p} x∉p = here
x∉p⇒x∈∁p {x = zero}  {inside  ∷ p} x∉p = contradiction here x∉p
x∉p⇒x∈∁p {x = suc x} {_       ∷ p} x∉p = there (x∉p⇒x∈∁p (x∉p ∘ there))

p∪∁p≡⊤ : ∀ {n} (p : Subset n) → p ∪ ∁ p ≡ ⊤
p∪∁p≡⊤ []            = refl
p∪∁p≡⊤ (outside ∷ p) = cong (inside ∷_) (p∪∁p≡⊤ p)
p∪∁p≡⊤ (inside  ∷ p) = cong (inside ∷_) (p∪∁p≡⊤ p)

∣∁p∣≡n∸∣p∣ : ∀ {n} (p : Subset n) → ∣ ∁ p ∣ ≡ n ∸ ∣ p ∣
∣∁p∣≡n∸∣p∣ []            = refl
∣∁p∣≡n∸∣p∣ (inside  ∷ p) = ∣∁p∣≡n∸∣p∣ p
∣∁p∣≡n∸∣p∣ (outside ∷ p) = begin
  suc ∣ ∁ p ∣     ≡⟨ cong suc (∣∁p∣≡n∸∣p∣ p) ⟩
  suc (_ ∸ ∣ p ∣) ≡⟨ sym (ℕₚ.+-∸-assoc 1 (∣p∣≤n p)) ⟩
  suc  _ ∸ ∣ p ∣  ∎
  where open ≡-Reasoning

------------------------------------------------------------------------
-- _∩_

module _ {n : ℕ} where

  open AlgebraicDefinitions {A = Subset n} _≡_

  ∩-assoc : Associative _∩_
  ∩-assoc = zipWith-assoc ∧-assoc

  ∩-comm : Commutative _∩_
  ∩-comm = zipWith-comm ∧-comm

  ∩-idem : Idempotent _∩_
  ∩-idem = zipWith-idem ∧-idem

  ∩-identityˡ : LeftIdentity ⊤ _∩_
  ∩-identityˡ = zipWith-identityˡ ∧-identityˡ

  ∩-identityʳ : RightIdentity ⊤ _∩_
  ∩-identityʳ = zipWith-identityʳ ∧-identityʳ

  ∩-identity : Identity ⊤ _∩_
  ∩-identity = ∩-identityˡ , ∩-identityʳ

  ∩-zeroˡ : LeftZero ⊥ _∩_
  ∩-zeroˡ = zipWith-zeroˡ ∧-zeroˡ

  ∩-zeroʳ : RightZero ⊥ _∩_
  ∩-zeroʳ = zipWith-zeroʳ ∧-zeroʳ

  ∩-zero : Zero ⊥ _∩_
  ∩-zero = ∩-zeroˡ , ∩-zeroʳ

  ∩-inverseˡ : LeftInverse ⊥ ∁ _∩_
  ∩-inverseˡ = zipWith-inverseˡ ∧-inverseˡ

  ∩-inverseʳ : RightInverse ⊥ ∁ _∩_
  ∩-inverseʳ = zipWith-inverseʳ ∧-inverseʳ

  ∩-inverse : Inverse ⊥ ∁ _∩_
  ∩-inverse = ∩-inverseˡ , ∩-inverseʳ

module _ (n : ℕ) where

  open AlgebraicStructures {A = Subset n} _≡_

  ∩-isMagma : IsMagma _∩_
  ∩-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = cong₂ _∩_
    }

  ∩-magma : Magma _ _
  ∩-magma = record
    { isMagma = ∩-isMagma
    }

  ∩-isSemigroup : IsSemigroup _∩_
  ∩-isSemigroup = record
    { isMagma = ∩-isMagma
    ; assoc   = ∩-assoc
    }

  ∩-semigroup : Semigroup _ _
  ∩-semigroup = record
    { isSemigroup = ∩-isSemigroup
    }

  ∩-isBand : IsBand _∩_
  ∩-isBand = record
    { isSemigroup = ∩-isSemigroup
    ; idem        = ∩-idem
    }

  ∩-band : Band _ _
  ∩-band = record
    { isBand = ∩-isBand
    }

  ∩-isSemilattice : IsSemilattice _∩_
  ∩-isSemilattice = record
    { isBand = ∩-isBand
    ; comm   = ∩-comm
    }

  ∩-semilattice : Semilattice _ _
  ∩-semilattice = record
    { isSemilattice = ∩-isSemilattice
    }

  ∩-isMonoid : IsMonoid _∩_ ⊤
  ∩-isMonoid = record
    { isSemigroup = ∩-isSemigroup
    ; identity    = ∩-identity
    }

  ∩-monoid : Monoid _ _
  ∩-monoid = record
    { isMonoid = ∩-isMonoid
    }

  ∩-isCommutativeMonoid : IsCommutativeMonoid _∩_ ⊤
  ∩-isCommutativeMonoid = record
    { isMonoid = ∩-isMonoid
    ; comm     = ∩-comm
    }

  ∩-commutativeMonoid : CommutativeMonoid _ _
  ∩-commutativeMonoid = record
    { isCommutativeMonoid = ∩-isCommutativeMonoid
    }

  ∩-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∩_ ⊤
  ∩-isIdempotentCommutativeMonoid = record
    { isCommutativeMonoid = ∩-isCommutativeMonoid
    ; idem                = ∩-idem
    }

  ∩-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
  ∩-idempotentCommutativeMonoid = record
    { isIdempotentCommutativeMonoid = ∩-isIdempotentCommutativeMonoid
    }

p∩q⊆p : ∀ {n} (p q : Subset n) → p ∩ q ⊆ p
p∩q⊆p []            []           x∈p∩q        = x∈p∩q
p∩q⊆p (inside  ∷ p) (inside ∷ q) here         = here
p∩q⊆p (inside  ∷ p) (_      ∷ q) (there ∈p∩q) = there (p∩q⊆p p q ∈p∩q)
p∩q⊆p (outside ∷ p) (_      ∷ q) (there ∈p∩q) = there (p∩q⊆p p q ∈p∩q)

p∩q⊆q : ∀ {n} (p q : Subset n) → p ∩ q ⊆ q
p∩q⊆q p q rewrite ∩-comm p q = p∩q⊆p q p

x∈p∩q⁺ : ∀ {n} {p q : Subset n} {x} → x ∈ p × x ∈ q → x ∈ p ∩ q
x∈p∩q⁺ (here      , here)      = here
x∈p∩q⁺ (there x∈p , there x∈q) = there (x∈p∩q⁺ (x∈p , x∈q))

x∈p∩q⁻ : ∀ {n} (p q : Subset n) {x} → x ∈ p ∩ q → x ∈ p × x ∈ q
x∈p∩q⁻ (inside ∷ p) (inside ∷ q) here          = here , here
x∈p∩q⁻ (s      ∷ p) (t      ∷ q) (there x∈p∩q) =
  Product.map there there (x∈p∩q⁻ p q x∈p∩q)

∩⇔× : ∀ {n} {p q : Subset n} {x} → x ∈ p ∩ q ⇔ (x ∈ p × x ∈ q)
∩⇔× = equivalence (x∈p∩q⁻ _ _) x∈p∩q⁺

module _ {n} (p q : Subset n) where

  ∣p∩q∣≤∣p∣ : ∣ p ∩ q ∣ ≤ ∣ p ∣
  ∣p∩q∣≤∣p∣ = p⊆q⇒∣p∣≤∣q∣ (p∩q⊆p p q)

  ∣p∩q∣≤∣q∣ : ∣ p ∩ q ∣ ≤ ∣ q ∣
  ∣p∩q∣≤∣q∣ = p⊆q⇒∣p∣≤∣q∣ (p∩q⊆q p q)

  ∣p∩q∣≤∣p∣⊓∣q∣ : ∣ p ∩ q ∣ ≤ ∣ p ∣ ⊓ ∣ q ∣
  ∣p∩q∣≤∣p∣⊓∣q∣ = ℕₚ.⊓-pres-m≤ ∣p∩q∣≤∣p∣ ∣p∩q∣≤∣q∣

------------------------------------------------------------------------
-- _∪_

module _ {n : ℕ} where

  open AlgebraicDefinitions {A = Subset n} _≡_

  ∪-assoc : Associative _∪_
  ∪-assoc = zipWith-assoc ∨-assoc

  ∪-comm : Commutative _∪_
  ∪-comm = zipWith-comm ∨-comm

  ∪-idem : Idempotent _∪_
  ∪-idem = zipWith-idem ∨-idem

  ∪-identityˡ : LeftIdentity ⊥ _∪_
  ∪-identityˡ = zipWith-identityˡ ∨-identityˡ

  ∪-identityʳ : RightIdentity ⊥ _∪_
  ∪-identityʳ = zipWith-identityʳ ∨-identityʳ

  ∪-identity : Identity ⊥ _∪_
  ∪-identity = ∪-identityˡ , ∪-identityʳ

  ∪-zeroˡ : LeftZero ⊤ _∪_
  ∪-zeroˡ = zipWith-zeroˡ ∨-zeroˡ

  ∪-zeroʳ : RightZero ⊤ _∪_
  ∪-zeroʳ = zipWith-zeroʳ ∨-zeroʳ

  ∪-zero : Zero ⊤ _∪_
  ∪-zero = ∪-zeroˡ , ∪-zeroʳ

  ∪-inverseˡ : LeftInverse ⊤ ∁ _∪_
  ∪-inverseˡ = zipWith-inverseˡ ∨-inverseˡ

  ∪-inverseʳ : RightInverse ⊤ ∁ _∪_
  ∪-inverseʳ = zipWith-inverseʳ ∨-inverseʳ

  ∪-inverse : Inverse ⊤ ∁ _∪_
  ∪-inverse = ∪-inverseˡ , ∪-inverseʳ

  ∪-distribˡ-∩ : _∪_ DistributesOverˡ _∩_
  ∪-distribˡ-∩ = zipWith-distribˡ ∨-distribˡ-∧

  ∪-distribʳ-∩ : _∪_ DistributesOverʳ _∩_
  ∪-distribʳ-∩ = zipWith-distribʳ ∨-distribʳ-∧

  ∪-distrib-∩ : _∪_ DistributesOver _∩_
  ∪-distrib-∩ = ∪-distribˡ-∩ , ∪-distribʳ-∩

  ∩-distribˡ-∪ : _∩_ DistributesOverˡ _∪_
  ∩-distribˡ-∪ = zipWith-distribˡ ∧-distribˡ-∨

  ∩-distribʳ-∪ : _∩_ DistributesOverʳ _∪_
  ∩-distribʳ-∪ = zipWith-distribʳ ∧-distribʳ-∨

  ∩-distrib-∪ : _∩_ DistributesOver _∪_
  ∩-distrib-∪ = ∩-distribˡ-∪ , ∩-distribʳ-∪

  ∪-abs-∩ : _∪_ Absorbs _∩_
  ∪-abs-∩ = zipWith-absorbs ∨-abs-∧

  ∩-abs-∪ : _∩_ Absorbs _∪_
  ∩-abs-∪ = zipWith-absorbs ∧-abs-∨

module _ (n : ℕ) where

  open AlgebraicStructures {A = Subset n} _≡_

  ∪-isMagma : IsMagma _∪_
  ∪-isMagma = record
    { isEquivalence = isEquivalence
    ; ∙-cong        = cong₂ _∪_
    }

  ∪-magma : Magma _ _
  ∪-magma = record
    { isMagma = ∪-isMagma
    }

  ∪-isSemigroup : IsSemigroup _∪_
  ∪-isSemigroup = record
    { isMagma = ∪-isMagma
    ; assoc   = ∪-assoc
    }

  ∪-semigroup : Semigroup _ _
  ∪-semigroup = record
    { isSemigroup = ∪-isSemigroup
    }

  ∪-isBand : IsBand _∪_
  ∪-isBand = record
    { isSemigroup = ∪-isSemigroup
    ; idem        = ∪-idem
    }

  ∪-band : Band _ _
  ∪-band = record
    { isBand = ∪-isBand
    }

  ∪-isSemilattice : IsSemilattice _∪_
  ∪-isSemilattice = record
    { isBand = ∪-isBand
    ; comm   = ∪-comm
    }

  ∪-semilattice : Semilattice _ _
  ∪-semilattice = record
    { isSemilattice = ∪-isSemilattice
    }

  ∪-isMonoid : IsMonoid _∪_ ⊥
  ∪-isMonoid = record
    { isSemigroup = ∪-isSemigroup
    ; identity    = ∪-identity
    }

  ∪-monoid : Monoid _ _
  ∪-monoid = record
    { isMonoid = ∪-isMonoid
    }

  ∪-isCommutativeMonoid : IsCommutativeMonoid _∪_ ⊥
  ∪-isCommutativeMonoid = record
    { isMonoid = ∪-isMonoid
    ; comm     = ∪-comm
    }

  ∪-commutativeMonoid : CommutativeMonoid _ _
  ∪-commutativeMonoid = record
    { isCommutativeMonoid = ∪-isCommutativeMonoid
    }

  ∪-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _∪_ ⊥
  ∪-isIdempotentCommutativeMonoid = record
    { isCommutativeMonoid = ∪-isCommutativeMonoid
    ; idem                = ∪-idem
    }

  ∪-idempotentCommutativeMonoid : IdempotentCommutativeMonoid _ _
  ∪-idempotentCommutativeMonoid = record
    { isIdempotentCommutativeMonoid = ∪-isIdempotentCommutativeMonoid
    }

  ∪-∩-isLattice : IsLattice _∪_ _∩_
  ∪-∩-isLattice = record
    { isEquivalence = isEquivalence
    ; ∨-comm        = ∪-comm
    ; ∨-assoc       = ∪-assoc
    ; ∨-cong        = cong₂ _∪_
    ; ∧-comm        = ∩-comm
    ; ∧-assoc       = ∩-assoc
    ; ∧-cong        = cong₂ _∩_
    ; absorptive    = ∪-abs-∩ , ∩-abs-∪
    }

  ∪-∩-lattice : Lattice _ _
  ∪-∩-lattice = record
    { isLattice = ∪-∩-isLattice
    }

  ∪-∩-isDistributiveLattice : IsDistributiveLattice _∪_ _∩_
  ∪-∩-isDistributiveLattice = record
    { isLattice    = ∪-∩-isLattice
    ; ∨-distribʳ-∧ = ∪-distribʳ-∩
    }

  ∪-∩-distributiveLattice : DistributiveLattice _ _
  ∪-∩-distributiveLattice = record
    { isDistributiveLattice = ∪-∩-isDistributiveLattice
    }

  ∪-∩-isBooleanAlgebra : IsBooleanAlgebra _∪_ _∩_ ∁ ⊤ ⊥
  ∪-∩-isBooleanAlgebra = record
    { isDistributiveLattice = ∪-∩-isDistributiveLattice
    ; ∨-complementʳ         = ∪-inverseʳ
    ; ∧-complementʳ         = ∩-inverseʳ
    ; ¬-cong                = cong ∁
    }

  ∪-∩-booleanAlgebra : BooleanAlgebra _ _
  ∪-∩-booleanAlgebra = record
    { isBooleanAlgebra = ∪-∩-isBooleanAlgebra
    }

  ∩-∪-isLattice : IsLattice _∩_ _∪_
  ∩-∪-isLattice = L.∧-∨-isLattice ∪-∩-lattice

  ∩-∪-lattice : Lattice _ _
  ∩-∪-lattice = L.∧-∨-lattice ∪-∩-lattice

  ∩-∪-isDistributiveLattice : IsDistributiveLattice _∩_ _∪_
  ∩-∪-isDistributiveLattice = DL.∧-∨-isDistributiveLattice ∪-∩-distributiveLattice

  ∩-∪-distributiveLattice : DistributiveLattice _ _
  ∩-∪-distributiveLattice = DL.∧-∨-distributiveLattice ∪-∩-distributiveLattice

  ∩-∪-isBooleanAlgebra : IsBooleanAlgebra _∩_ _∪_ ∁ ⊥ ⊤
  ∩-∪-isBooleanAlgebra = BA.∧-∨-isBooleanAlgebra ∪-∩-booleanAlgebra

  ∩-∪-booleanAlgebra : BooleanAlgebra _ _
  ∩-∪-booleanAlgebra = BA.∧-∨-booleanAlgebra ∪-∩-booleanAlgebra

p⊆p∪q : ∀ {n p} (q : Subset n) → p ⊆ p ∪ q
p⊆p∪q (s ∷ q) here        = here
p⊆p∪q (s ∷ q) (there x∈p) = there (p⊆p∪q q x∈p)

q⊆p∪q : ∀ {n} (p q : Subset n) → q ⊆ p ∪ q
q⊆p∪q p q rewrite ∪-comm p q = p⊆p∪q p

x∈p∪q⁻ :  ∀ {n} (p q : Subset n) {x} → x ∈ p ∪ q → x ∈ p ⊎ x ∈ q
x∈p∪q⁻ (inside  ∷ p) (t       ∷ q) here          = inj₁ here
x∈p∪q⁻ (outside ∷ p) (inside  ∷ q) here          = inj₂ here
x∈p∪q⁻ (s       ∷ p) (t       ∷ q) (there x∈p∪q) =
  Sum.map there there (x∈p∪q⁻ p q x∈p∪q)

x∈p∪q⁺ : ∀ {n} {p q : Subset n} {x} → x ∈ p ⊎ x ∈ q → x ∈ p ∪ q
x∈p∪q⁺ (inj₁ x∈p) = p⊆p∪q _   x∈p
x∈p∪q⁺ (inj₂ x∈q) = q⊆p∪q _ _ x∈q

∪⇔⊎ : ∀ {n} {p q : Subset n} {x} → x ∈ p ∪ q ⇔ (x ∈ p ⊎ x ∈ q)
∪⇔⊎ = equivalence (x∈p∪q⁻ _ _) x∈p∪q⁺

module _ {n} (p q : Subset n) where

  ∣p∣≤∣p∪q∣ : ∣ p ∣ ≤ ∣ p ∪ q ∣
  ∣p∣≤∣p∪q∣ = p⊆q⇒∣p∣≤∣q∣ (p⊆p∪q {p = p} q)

  ∣q∣≤∣p∪q∣ : ∣ q ∣ ≤ ∣ p ∪ q ∣
  ∣q∣≤∣p∪q∣ = p⊆q⇒∣p∣≤∣q∣ (q⊆p∪q p q)

  ∣p∣⊔∣q∣≤∣p∪q∣ : ∣ p ∣ ⊔ ∣ q ∣ ≤ ∣ p ∪ q ∣
  ∣p∣⊔∣q∣≤∣p∪q∣ = ℕₚ.⊔-pres-≤m ∣p∣≤∣p∪q∣ ∣q∣≤∣p∪q∣

------------------------------------------------------------------------
-- Lift

Lift? : ∀ {n p} {P : Pred (Fin n) p} → Decidable P → Decidable (Lift P)
Lift? P? p = decFinSubset (_∈? p) (λ {x} _ → P? x)

------------------------------------------------------------------------
-- Other

module _ {p} {P : Pred (Subset zero) p} where

  ∃-Subset-zero : ∃⟨ P ⟩ → P []
  ∃-Subset-zero ([] , P[]) = P[]

  ∃-Subset-[]-⇔ : P [] ⇔ ∃⟨ P ⟩
  ∃-Subset-[]-⇔ = equivalence ([] ,_) ∃-Subset-zero

module _ {p n} {P : Pred (Subset (suc n)) p} where

  ∃-Subset-suc : ∃⟨ P ⟩ → ∃⟨ P ∘ (inside ∷_) ⟩ ⊎ ∃⟨ P ∘ (outside ∷_) ⟩
  ∃-Subset-suc (outside ∷ p , Pop) = inj₂ (p , Pop)
  ∃-Subset-suc ( inside ∷ p , Pip) = inj₁ (p , Pip)

  ∃-Subset-∷-⇔ : (∃⟨ P ∘ (inside ∷_) ⟩ ⊎ ∃⟨ P ∘ (outside ∷_) ⟩) ⇔ ∃⟨ P ⟩
  ∃-Subset-∷-⇔ = equivalence
    [ Product.map _ id , Product.map _ id ]′
    ∃-Subset-suc

anySubset? : ∀ {p n} {P : Pred (Subset n) p} → Decidable P → Dec ∃⟨ P ⟩
anySubset? {n = zero}  P? = Dec.map ∃-Subset-[]-⇔ (P? [])
anySubset? {n = suc n} P? =
  Dec.map ∃-Subset-∷-⇔ (anySubset? (P? ∘ ( inside ∷_)) ⊎-dec
                        anySubset? (P? ∘ (outside ∷_)))

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.3

p⊆q⇒∣p∣<∣q∣ = p⊆q⇒∣p∣≤∣q∣
{-# WARNING_ON_USAGE p⊆q⇒∣p∣<∣q∣
"Warning: p⊆q⇒∣p∣<∣q∣ was deprecated in v1.3.
Please use p⊆q⇒∣p∣≤∣q∣ instead."
#-}


text:
{-# OPTIONS --universe-polymorphism #-}
module tests.Literals where

open import Prelude.Nat
open import Prelude.Float
open import Prelude.Char
open import Prelude.String
open import Prelude.Unit
open import Prelude.IO

afloat : Float
afloat = 1.23

astring : String
astring = "abc"

achar : Char
achar = 'd'

anat : Nat
anat = 123

main : IO Unit
main =
  printFloat  afloat  ,,
  putStr      astring ,,
  printChar   achar   ,,
  printNat    anat    ,,
  putStrLn ""

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
import      Lvl

module Structure.Category {ℓₒ ℓₘ ℓₑ : Lvl.Level} where

open import Functional using (swap)
open import Logic
open import Logic.Propositional
import      Structure.Categorical.Names as Names
open import Structure.Categorical.Properties
open import Structure.Semicategory{ℓₒ}{ℓₘ}{ℓₑ}
open import Structure.Operator
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

-- Obj is the collection of objects.
-- _⟶_ is the collection of morphisms.
module _
  {Obj : Type{ℓₒ}}
  (_⟶_ : Obj → Obj → Type{ℓₘ})
  ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(x ⟶ y) ⦄
  where

  -- A category is a structure on a relation called a morphism.
  --
  -- It can be seen as a generalization of the structure in functions between a collection of types/sets.
  -- More specifically, the algebraic properties of functions regarding composition and the identity function.
  -- In this case, sets are objects and functions are morphisms.
  -- See `Type.Category`.
  --
  -- It can also be seen as a generalized algebraic structure, or more specifically a generalization of monoids.
  -- The type of a monoid's operator is usually restricted to a single type, but a category allows it to vary (depending on the rules of morphism instead).
  -- (One can loosely call a category to be a monoid without the "closed" property of algebraic structures).
  -- In this case, the binary operation is (_∘_) and the laws are the usual identity and associative laws.
  -- See `Structure.Category.Monoid`.
  --
  -- A category can also be constructed by letting objects be the models of algebraic structures, and morphisms the homomorphisms of the respective algebraic structure.
  --
  -- In the case of categories being the objects in a category, functors are homomorphisms, and therefore also the morphisms.
  -- See `Structure.Category.Category`.
  --
  -- An alternative interpretation of the definition:
  -- A type (Obj) and a binary relation (Morphism) on this type is a category when:
  -- • The relator is transitive.
  -- • The relator is reflexive.
  -- • The reflexivity proof inside the transitivity proof does not result in a new proof.
  -- • Chains of the transitivity proofs can be applied in any order and the resulting proof will be the same.
  -- See `Relator.Equals.Category` for an example of this kind of binary relation.
  --
  -- A more concrete interpretation of the binary relation one is that a category describes a graph.
  -- Vertices are objects and morphisms are paths between the vertices.
  -- The operator joins two paths into one, and the identity is a loop (the empty path).
  -- See `Graph.Category`.
  --
  -- A category is the common pattern seen in all the examples above.
  record Category : Stmt{ℓₒ Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ} where
    field
      -- Existence of morphisms constructed by connecting two morphisms (The composition of two morphisms).
      -- Existence of a binary operator on morphisms connecting the ends of two morphisms.
      -- Also a proof of transitivity for the binary relator (_⟶_).
      -- Note that this is the operator like the operators in other algebraic structures with binary operators
      -- ∀{x y z : Obj} → (y ⟶ z) → (x ⟶ y) → (x ⟶ z)
      _∘_ : Names.SwappedTransitivity(_⟶_)

      -- Existence of a morphism connected to itself (The identity morphism).
      -- Also a proof of reflexivity for the binary relator (_⟶_).
      -- ∀{x : Obj} → (x ⟶ x)
      id  : Names.Reflexivity(_⟶_)
    infixr 20 _∘_

    field
      -- The binary operator respects the equivalence relation.
      ⦃ binaryOperator ⦄ : ∀{x y z} → BinaryOperator(_∘_ {x}{y}{z})

      -- The binary operator on mophisms is associative.
      -- Or, the order of applying two transitivies on three proofs does not matter. It is the same proof.
      -- ∀{x y z w : Obj}{f : y ⟶ x}{g : z ⟶ y}{h : w ⟶ z} → ((f ∘ g) ∘ h ≡ f ∘ (g ∘ h))
      ⦃ associativity ⦄ : Morphism.Associativity(\{x} → _∘_ {x})

      -- The morphism `id` behaves like aa identity element with respect to the binary operator.
      -- Or, applying the proof of reflexivity on transitivity is an identity function for proofs.
      ⦃ identity ⦄ : Morphism.Identity(_∘_)(\{x} → id{x})

    instance
      identityₗ : Morphism.Identityₗ(_∘_)(\{x} → id{x})
      identityₗ = [∧]-elimₗ identity

    instance
      identityᵣ : Morphism.Identityᵣ(_∘_)(\{x} → id{x})
      identityᵣ = [∧]-elimᵣ identity

    -- As stated in `id`, this can be interpreted as proof of reflexivity when `Morphism` is interpreted as a binary relation.
    morphism-reflexivity : Reflexivity(_⟶_)
    morphism-reflexivity = intro id

    semicategory : Semicategory(_⟶_)
    Semicategory._∘_ semicategory = _∘_
    Semicategory.binaryOperator semicategory = binaryOperator
    Semicategory.associativity semicategory = associativity

    open Semicategory(semicategory) hiding (_∘_ ; binaryOperator ; associativity) public

-- A category object can be used when one refers to a category as an object.
-- Examples of usage are in functors (morphism between categories) or in equivalences of categories.
record CategoryObject : Stmt{Lvl.𝐒(ℓₒ Lvl.⊔ ℓₘ Lvl.⊔ ℓₑ)} where
  constructor intro
  field
    {Object}           : Type{ℓₒ}
    {Morphism}         : Object → Object → Type{ℓₘ}
    ⦃ morphism-equiv ⦄ : ∀{x y} → Equiv{ℓₑ}(Morphism x y)
    category           : Category(Morphism)

  instance
    category-instance = category

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:
{-# OPTIONS --without-K --rewriting #-}

module PropT where

  open import Base

  open import lib.Basics
  open import lib.types.Sigma
  open import lib.NType2
  open import lib.types.Truncation
  open import lib.types.Lift

  _is-contractible : {i : ULevel} (A : Type i) → Type i
  _is-contractible = is-contr

  ⊤-is-contr : ⊤ is-contractible
  ⊤-is-contr = has-level-in (unit , (λ {unit → refl}))

  contr-≃-⊤ : {i : ULevel} {A : Type i} (c : A is-contractible)
              → A ≃ ⊤
  contr-≃-⊤ {A = A} c =
    equiv (λ _ → unit) (λ { unit → contr-center c })
          (λ {unit → refl})
          (λ a → contr-path c a)

  _is-a-prop : ∀ {i} → (A : Type i)  → Type i
  A is-a-prop = is-prop A

  PropT : (i : ULevel) → Type _
  PropT = hProp

  PropT₀ = hProp₀

  _holds : ∀ {i} (P : PropT i) → Type i
  _holds = fst

  _holds-is-a-prop : {i : ULevel} (P : PropT i) → (P holds) is-a-prop
  _holds-is-a-prop = snd

  ∥_∥ : ∀ {i} (A :  Type i) → Type i
  ∥_∥ = Trunc -1

  True : PropT₀
  True = ⊤ , contr-is-prop ⊤-is-contr

  False : PropT₀
  False = ⊥ , has-level-in (λ x → quodlibet x)

  _And_ : ∀ {i j} → (A : Type i) (B : Type j) → Type (lmax i j)
  A And B = Σ A (λ _ → B)

  _And→_ : ∀ {i j k l} {A : Type i} {B : Type j} {C : Type k} {D : Type l}
           (f : A → C) (g : B → D)
           → (A And B) → (C And D)
  f And→ g = λ { (a , b) → f a , g b }

  infixl 30 _∧_
  _∧_ : ∀ {i j} (P : PropT i) (Q : PropT j) → PropT (lmax i j)
  P ∧ Q = ((P holds) And (Q  holds)) , Σ-level (P holds-is-a-prop) (λ _ → Q holds-is-a-prop)

  infixl 35 _∨_
  _∨_ : ∀ {i j} (P : PropT i) (Q : PropT j) → PropT (lmax i j)
  P ∨ Q = ∥ (P holds) ⊔ (Q holds) ∥ , ⟨⟩

  mapping-into-prop-is-a-prop : {i j : ULevel} {A : Type i} {P : A → Type j}
                                (f : (a : A) → ((P a) is-a-prop))
                                → ((a : A) → P a) is-a-prop
  mapping-into-prop-is-a-prop f = all-paths-is-prop (λ x y →
                                    λ= (λ a → prop-path (f a) (x a) (y a)))

  _⇒_ : ∀ {i j} (P : PropT i) (Q : PropT j) → PropT (lmax i j)
  P ⇒ Q = (P holds → Q holds) , mapping-into-prop-is-a-prop (λ _ → Q holds-is-a-prop)

  not : ∀ {i} (P : PropT i) → PropT i
  not P = P ⇒ False

  {-
    To say ``There exists an a : A such that B a", write
      ∃ (λ (a : A) → B a)
  -}
  ∃ : {i j : ULevel} {A : Type i} (B : A → Type j) → PropT (lmax i j)
  ∃ {_} {_} {A} B = ∥ (Σ A B) ∥ , ⟨⟩

  ∃ₚ : ∀ {i j} {A : Type i} (B : A → PropT j) → PropT (lmax i j)
  ∃ₚ {A = A} B = ∃ λ (a : A) → (B a) holds

  ∀ₚ : ∀ {i j} {A : Type i} (P : A → PropT j) → PropT (lmax i j)
  ∀ₚ P = (∀ a → (P a) holds) , mapping-into-prop-is-a-prop (λ a → (P a) holds-is-a-prop)

  _holds-implies-dec-eq : {i : ULevel} (P : PropT i)
                          → P holds → (P holds) ≃ (Dec (P holds))
  (P holds-implies-dec-eq) p  = equiv (λ _ → inl p)
                                      ((λ { (inl q) → q ; (inr nq) → quodlibet (nq p) }))
                                      (λ { (inl q) → ap inl (prop-path (P holds-is-a-prop) p q)
                                         ; (inr nq) → quodlibet (nq p) })
                                      (λ q → prop-path (P holds-is-a-prop) p q)

  _holds-by_implies-=-True : (P : PropT₀) (p : P holds)
                             → P == True
  (P , q) holds-by p implies-=-True = pair= left-id right-id
    where
      left-id : P == ⊤
      left-id = (ua {A = P} {B = True holds} (contr-≃-⊤ {A = P} (inhab-prop-is-contr p {{q}})))

      right-id : q == (snd True) [ _is-a-prop ↓ left-id ]
      right-id = from-transp _is-a-prop left-id
                      (prop-path (has-level-is-prop) (transport _is-a-prop left-id q) (snd True) )

  ¬-_holds-by_implies-=-False : (P : PropT₀) (p : ¬ (P holds))
                                → P == False
  ¬- (P , q) holds-by np implies-=-False = pair= left-id right-id
    where
      left-id : P == ⊥
      left-id = ua {A = P} {B = False holds} e
        where e : P ≃ ⊥
              e = equiv np (λ ()) (λ ()) (λ p → quodlibet (np p))

      right-id : q == (snd False) [ _is-a-prop ↓ left-id ]
      right-id =
        from-transp _is-a-prop left-id
          (prop-path (has-level-is-prop) (transport _is-a-prop left-id q) (snd False))

  iff-to-≃ : ∀ {i j} {P : PropT i} {Q : PropT j}
             → (P holds → Q holds)
             → (Q holds → P holds)
             → (P holds) ≃ (Q holds)
  iff-to-≃ {P = P} {Q = Q} f g =
    equiv f g
      (λ b → prop-path (snd Q) (f (g b)) b)
      (λ a → prop-path (snd P) (g (f a)) a)

  -- Propositional Resizing

  lift-prop : {i j : ULevel} → PropT i → PropT (lmax i j)
  lift-prop {i} {j} (P , q) = (Lift {i} {j} P) , Lift-level q

  postulate prop-resize : {i j : ULevel} → (lift-prop {i} {j}) is-an-equiv

  resize-eq : {i j : ULevel} → PropT i ≃ PropT (lmax i j)
  resize-eq {i} {j} = (lift-prop {i} {j}) , prop-resize

  resize₀ : {i : ULevel} → PropT i → PropT₀
  resize₀ {i} = <– (resize-eq {lzero} {i})

  unresize₀ : {i : ULevel} → PropT₀ → PropT i
  unresize₀ {i} = –> (resize-eq {lzero} {i})

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


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

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

open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Sets.EquivalenceRelations
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Fields
open import Groups.Definition
open import Sequences
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Semirings.Definition
open import Functions.Definition
open import Fields.Orders.Total.Definition
open import Numbers.Primes.PrimeNumbers

module Fields.Orders.Limits.Lemmas {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {_} {c} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} {F : Field R} {pRing : PartiallyOrderedRing R pOrder} (oF : TotallyOrderedField F pRing) where

open Ring R
open TotallyOrderedField oF
open TotallyOrderedRing oRing
open PartiallyOrderedRing pRing
open import Rings.Orders.Total.Lemmas oRing
open import Rings.Orders.Total.AbsoluteValue oRing
open import Rings.Orders.Partial.Lemmas pRing
open SetoidTotalOrder total
open SetoidPartialOrder pOrder
open Group additiveGroup
open import Groups.Lemmas additiveGroup
open Setoid S
open Equivalence eq
open Field F
open import Fields.CauchyCompletion.Definition (TotallyOrderedField.oRing oF) F
open import Fields.Orders.Limits.Definition oF
open import Fields.Lemmas F
open import Fields.Orders.Total.Lemmas oF
open import Rings.Characteristic R
open import Rings.InitialRing R
open import Rings.Orders.Total.Cauchy oRing

private
  2!=3 : 2 ≡ 3 → False
  2!=3 ()

convergentSequenceCauchy : (nontrivial : 0R ∼ 1R → False) → {a : Sequence A} → {r : A} → a ~> r → cauchy a
convergentSequenceCauchy _ {a} {r} a->r e 0<e with halve (λ i → charNotN 1 (transitive (transitive +Associative identRight) i)) e
... | e/2 , prE/2 with a->r e/2 (halvePositive' prE/2 0<e)
... | N , pr = N , λ {m} {n} → ans m n
  where
    ans : (m n : ℕ) → N <N m → N <N n → abs (index a m + inverse (index a n)) < e
    ans m n N<m N<n = <WellDefined reflexive prE/2 (bothNearImpliesNear {r} e/2 (halvePositive' prE/2 0<e) (pr m N<m) (pr n N<n))


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.RingStructure.CohomologyRingFun where

{-
   There is two definitionof the Cohomology Ring.
   We recommend to use the HIT definition (the other one)
   as the ring product is eaiser to handle.
   Nevertheless the equality is harder to handle so
   this definition can interessting too.
-}

open import Cubical.Foundations.Prelude

open import Cubical.Relation.Nullary

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.DirectSumFun

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.GradedCommutativity

private variable
  ℓ ℓ' : Level

open PlusBis

module _ (A : Type ℓ) where

  H*FunR : Ring ℓ
  H*FunR = ⊕FunGradedRing-Ring
           _+'_ (makeIsMonoid isSetℕ +'-assoc +'-rid +'-lid)
           +'≡+
           (λ k → coHom k A)
           (λ k → snd (coHomGroup k A))
           1⌣
           _⌣_
           (λ {k} {l} → 0ₕ-⌣ k l)
           (λ {k} {l} → ⌣-0ₕ k l)
           (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ ((sym (+'-assoc _ _ _)) , (sym (assoc-⌣ _ _ _ _ _ _)))))
           (λ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-rid _) , sym (lUnit⌣ _ _))))
           (λ _ → ΣPathTransport→PathΣ _ _ (refl , transportRefl _ ∙ rUnit⌣ _ _))
           (λ _ _ _ → leftDistr-⌣ _ _ _ _ _)
           λ _ _ _ → rightDistr-⌣ _ _ _ _ _

  H*Fun : Type ℓ
  H*Fun = fst H*FunR

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Agda.Primitive using (Prop)

postulate
  Set₁ : Prop

open import Agda.Primitive using (Set)

postulate
  A : Set₁

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2014-10-09
-- Reported by ohmanjoakim

infixr 8 _⇒_

data Ty : Set where
  _⇒_ : Ty → Ty → Ty

⟦_⟧ : Ty → Set
⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

data Term : Ty → Set where
  K : (A B : Ty) → Term (A ⇒ B ⇒ A)

test : (A : Ty) (a : Term A) → ⟦ A ⟧
test A a = {!a!}

-- When doing a case split on a in foo, the following is written:
-- test .(x ⇒ x₁ ⇒ x) (K A B) x x₁ = ?

-- Correct is
-- test .(A ⇒ B ⇒ A) (K A B) x x₁ = ?


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

open import Categories.Category using (module Commutation)
  renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)

module Categories.Enriched.Category.Opposite
  {o ℓ e} {V : Setoid-Category o ℓ e} {M : Monoidal V} (S : Symmetric M) where

-- The dual of a V-enriched category.
--
-- Note that, for this construction to work, V needs to be a
-- *symmetric* monoidal category.

open import Data.Product using (_,_)

import Categories.Category.Monoidal.Braided.Properties as BraidedProperties
open import Categories.Category.Monoidal.Reasoning M
open import Categories.Category.Monoidal.Utilities M using (module Shorthands)
open import Categories.Enriched.Category M using (Category)
open import Categories.Morphism.Reasoning V

open Setoid-Category V renaming (id to idV) using (_⇒_; _∘_; assoc)
open Commutation V
open Shorthands
open Symmetric S
open BraidedProperties (Symmetric.braided S) using (braiding-coherence)

private σ = λ {A B} → braiding.⇒.η (A , B)

-- The opposite of a V-enriched category.

op : ∀ {v} → Category v → Category v
op C = record
  { Obj = Obj
  ; hom = λ A B → hom B A
  ; id  = id
  ; ⊚   = ⊚ ∘ σ
  ; ⊚-assoc = begin
      (⊚ ∘ σ) ∘ (⊚ ∘ σ) ⊗₁ idV               ≈⟨ refl⟩∘⟨ split₁ʳ ⟩
      (⊚ ∘ σ) ∘ ⊚ ⊗₁ idV ∘ σ ⊗₁ idV          ≈⟨ extend² (braiding.⇒.commute _) ⟩
      (⊚ ∘ idV ⊗₁ ⊚) ∘ σ ∘ σ ⊗₁ idV          ≈⟨ ⊚-assoc′ ⟩∘⟨refl ⟩
      (⊚ ∘ ⊚ ⊗₁ idV ∘ α⇐) ∘ σ ∘ σ ⊗₁ idV     ≈˘⟨ assoc ⟩∘⟨refl ⟩
      ((⊚ ∘ ⊚ ⊗₁ idV) ∘ α⇐) ∘ σ ∘ σ ⊗₁ idV   ≈⟨ pullʳ invert-braidings ⟩
      (⊚ ∘ ⊚ ⊗₁ idV) ∘ σ ∘ idV ⊗₁ σ ∘ α⇒     ≈˘⟨ refl⟩∘⟨ assoc ⟩
      (⊚ ∘ ⊚ ⊗₁ idV) ∘ (σ ∘ idV ⊗₁ σ) ∘ α⇒
                                    ≈˘⟨ pushˡ (extend² (braiding.⇒.commute _)) ⟩
      ((⊚ ∘ σ) ∘ idV ⊗₁ ⊚ ∘ idV ⊗₁ σ) ∘ α⇒   ≈˘⟨ pullˡ (refl⟩∘⟨ split₂ʳ) ⟩
      (⊚ ∘ σ) ∘ idV ⊗₁ (⊚ ∘ σ) ∘ α⇒   ∎
  ; unitˡ = λ {A B} → begin
      (⊚ ∘ σ) ∘ id ⊗₁ idV   ≈⟨ pullʳ (braiding.⇒.commute _) ⟩
      ⊚ ∘ idV ⊗₁ id ∘ σ     ≈⟨ pullˡ unitʳ ⟩
      ρ⇒ ∘ σ                ≈˘⟨ switch-fromtoʳ braided-iso braiding-coherence ⟩
      λ⇒                    ∎
  ; unitʳ = begin
      (⊚ ∘ σ) ∘ idV ⊗₁ id   ≈⟨ pullʳ (braiding.⇒.commute _) ⟩
      ⊚ ∘ id ⊗₁ idV ∘ σ     ≈⟨ pullˡ unitˡ ⟩
      λ⇒ ∘ σ                ≈⟨ braiding-coherence ⟩
      ρ⇒                    ∎
  }
  where
    open Category C

    ⊚-assoc′ : ∀ {A B C D} →
               [ hom C D ⊗₀ (hom B C ⊗₀ hom A B) ⇒ hom A D ]⟨
                 idV ⊗₁ ⊚    ⇒⟨ hom C D ⊗₀ hom A C ⟩
                 ⊚
               ≈ α⇐          ⇒⟨ (hom C D ⊗₀ hom B C) ⊗₀ hom A B ⟩
                 ⊚ ⊗₁ idV    ⇒⟨ hom B D ⊗₀ hom A B ⟩
                 ⊚
               ⟩
    ⊚-assoc′ = switch-fromtoʳ associator (assoc ○ ⟺ ⊚-assoc) ○ assoc

    -- implements the following equation of string diagrams
    --
    --     |   |   |               |   |   |
    --      \ /    |               |    \ /
    --       \     |               |     \
    --      / \   /                 \   / \
    --     |   \ /        ===        \ /   |
    --      \   \                     /   /
    --       \ / \                   / \ /
    --        \   \                 /   /
    --       / \   \               /   / \
    --      |   |   |             |   |   |
    --
    invert-braidings : ∀ {A B C} →
                       [ (A ⊗₀ B) ⊗₀ C ⇒ (C ⊗₀ B) ⊗₀ A ]⟨
                         σ ⊗₁ idV      ⇒⟨ (B ⊗₀ A) ⊗₀ C ⟩
                         σ             ⇒⟨ C ⊗₀ (B ⊗₀ A) ⟩
                         α⇐
                       ≈ α⇒            ⇒⟨ A ⊗₀ (B ⊗₀ C) ⟩
                         idV ⊗₁ σ      ⇒⟨ A ⊗₀ (C ⊗₀ B) ⟩
                         σ
                       ⟩
    invert-braidings = begin
        α⇐ ∘ σ ∘ σ ⊗₁ idV
      ≈⟨ extendʳ (switch-tofromʳ associator (⟺ hexagon₂)) ⟩
        ((σ ⊗₁ idV ∘ α⇐) ∘ idV ⊗₁ σ) ∘ α⇒ ∘ σ ⊗₁ idV
      ≈⟨ assoc ⟩
        (σ ⊗₁ idV ∘ α⇐) ∘ idV ⊗₁ σ ∘ α⇒ ∘ σ ⊗₁ idV
      ≈˘⟨ pushʳ (switch-fromtoˡ associator (⟺ hexagon₁)) ⟩
        σ ⊗₁ idV ∘ σ ∘ α⇒
      ≈˘⟨ extendʳ (braiding.⇒.commute _) ⟩
        σ ∘ idV ⊗₁ σ ∘ α⇒
      ∎

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Product.Relation.Binary.Pointwise.NonDependent directly.
------------------------------------------------------------------------

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

module Data.Product.Relation.Pointwise.NonDependent where

open import Data.Product.Relation.Binary.Pointwise.NonDependent public


text:
{-# OPTIONS --without-K  #-}
module sets.nat.ordering.lt.core where

open import sum
open import equality.core
open import function.isomorphism.core
open import sets.core
open import sets.nat.core
open import sets.nat.ordering.leq.core

_<_ : ℕ → ℕ → Set
m < n = suc m ≤ n
infixr 4 _<_

z<n : ∀ {n} → 0 < suc n
z<n = s≤s z≤n

<⇒≤ : ∀ {n m} → n < m → n ≤ m
<⇒≤ p = trans≤ suc≤ p

trans< : ∀ {n m p} → n < m → m < p → n < p
trans< p q = <⇒≤ (trans≤ (s≤s p) q)

ap<-suc : ∀ {n m} → n < m → suc n < suc m
ap<-suc = s≤s

compare : (n m : ℕ) → Ordering _<_ n m
compare zero zero = eq refl
compare zero (suc m) = lt z<n
compare (suc n) zero = gt z<n
compare (suc n) (suc m) with compare n m
... | lt p = lt (ap<-suc p)
... | eq p = eq (ap suc p)
... | gt p = gt (ap<-suc p)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{- NEW TRANSLATION: notation change to avoid exponential increase in term size during translation -}

open import Preliminaries
open import Source
open import Complexity

module Translation-WithLet where

  mutual
    ⟨⟨_⟩⟩ : Tp → Complexity.CTp
    ⟨⟨ unit ⟩⟩ = unit
    ⟨⟨ nat ⟩⟩ = nat
    ⟨⟨ susp A ⟩⟩ = || A ||
    ⟨⟨ A ->s B ⟩⟩ = ⟨⟨ A ⟩⟩ ->c || B ||
    ⟨⟨ A ×s B ⟩⟩ = ⟨⟨ A ⟩⟩ ×c ⟨⟨ B ⟩⟩
    ⟨⟨ list A ⟩⟩ = list ⟨⟨ A ⟩⟩
    ⟨⟨ bool ⟩⟩ = bool

    ||_|| : Tp → Complexity.CTp
    || τ || = C ×c ⟨⟨ τ ⟩⟩

  ⟨⟨_⟩⟩c : Source.Ctx → Complexity.Ctx
  ⟨⟨ [] ⟩⟩c = []
  ⟨⟨ x :: Γ ⟩⟩c = ⟨⟨ x ⟩⟩ :: ⟨⟨ Γ ⟩⟩c

  interp-Cost : ∀{Γ} → Cost → Γ Complexity.|- C
  interp-Cost 0c = 0C
  interp-Cost 1c = 1C
  interp-Cost (m +c n) = plusC (interp-Cost m) (interp-Cost n)

  lookup : ∀{Γ τ} → τ Source.∈ Γ → ⟨⟨ τ ⟩⟩ Complexity.∈ ⟨⟨ Γ ⟩⟩c
  lookup i0 = i0
  lookup (iS x) = iS (lookup x)

  throw-s : ∀ {Γ Γ' τ} → Complexity.sctx Γ (τ :: Γ') → Complexity.sctx Γ Γ'
  throw-s Θ x = Θ (iS x)

  _+C_ : ∀ {Γ τ} → Γ Complexity.|- C  → Γ Complexity.|- (C ×c τ)→ Γ Complexity.|- (C ×c τ)
  c +C e = letc (prod (l-proj (var i0)) (r-proj (var i0))) e

  -- translation from source expressions to complexity expressions
  ||_||e : ∀{Γ τ} → Γ Source.|- τ → ⟨⟨ Γ ⟩⟩c Complexity.|- || τ ||
  || unit ||e = prod 0C unit
  || var x ||e = prod 0C (var (lookup x))
  || z ||e = prod 0C z
  || suc e ||e = (letc (prod (l-proj (var i0)) (s (r-proj (var i0)))) || e ||e)
  || rec e e0 e1 ||e =
      letc (l-proj (var i0) +C rec (r-proj (var i0))
           (Complexity.wkn (1C +C || e0 ||e)) (Complexity.subst (1C +C || e1 ||e) (Complexity.s-extend (Complexity.s-extend (throw-s Complexity.ids))))) || e ||e
  || lam e ||e = prod 0C (lam || e ||e)
  || app e1 e2 ||e = letc (letc (prod (plusC (plusC (l-proj (var (iS i0))) (l-proj (var i0))) (l-proj (app (r-proj (var (iS i0))) (r-proj (var i0)))))
                            (r-proj (app (r-proj (var (iS i0))) (r-proj (var i0))))) (Complexity.wkn || e2 ||e)) || e1 ||e
  || prod e1 e2 ||e = letc (letc (prod (plusC (l-proj (var (iS i0))) (l-proj (var i0))) (prod (r-proj (var (iS i0))) (r-proj (var i0)))) (Complexity.wkn || e2 ||e)) || e1 ||e
  || delay e ||e = prod 0C || e ||e
  || force e ||e = letc (prod (plusC (l-proj (var i0)) (l-proj (r-proj (var i0)))) (r-proj (r-proj (var i0)))) || e ||e
  || split e0 e1 ||e = letc (prod (plusC (Complexity.wkn (l-proj || e0 ||e)) (l-proj (var i0))) (r-proj (var i0))) E1
       where E1 = letc (Complexity.subst || e1 ||e (Complexity.lem4 (l-proj (r-proj (var i0))) (r-proj (r-proj (var i0))) Complexity.ss Complexity.s-extend (Complexity.s-extend (throw-s Complexity.ids)))) || e0 ||e
  || nil ||e = prod 0C nil
  || e ::s e₁ ||e = letc (letc (prod (plusC (l-proj (var (iS i0))) (l-proj (var i0))) (r-proj (var (iS i0)) ::c r-proj (var i0))) (Complexity.wkn || e₁ ||e)) || e ||e
  || listrec e e₁ e₂ ||e =
      letc (l-proj (var i0) +C listrec (r-proj (var i0))
        (Complexity.wkn (1C +C || e₁ ||e)) (Complexity.subst (1C +C || e₂ ||e) (Complexity.s-extend (Complexity.s-extend (Complexity.s-extend (throw-s Complexity.ids)))))) || e ||e
  || true ||e = prod 0C true
  || false ||e = prod 0C false

{-
  module Proofs where
    open NewTranslation renaming (||_||e to ||_||new)
    open import Translation renaming (||_||e to ||_||old)

    convert-type : Complexity-WithLet.CTp → Complexity.CTp
    convert-type unit = unit
    convert-type nat = nat
    convert-type (τ ->c τ₁) = convert-type τ ->c convert-type τ₁
    convert-type (τ ×c τ₁) = convert-type τ ×c convert-type τ₁
    convert-type (list τ) = list (convert-type τ)
    convert-type bool = bool
    convert-type C = C
    convert-type rnat = rnat

    convert-ctx : Complexity-WithLet.Ctx → Complexity.Ctx
    convert-ctx [] = []
    convert-ctx (x :: Γ) = convert-type x :: convert-ctx Γ

    convert-var : ∀ {Γ τ} → τ Complexity-WithLet.∈ Γ → convert-type τ Complexity.∈ convert-ctx Γ
    convert-var i0 = i0
    convert-var (iS x) = iS (convert-var x)

    convert-exp : ∀{Γ τ} → (e : Γ Complexity-WithLet.|- τ) → convert-ctx Γ Complexity.|- convert-type τ
    convert-exp unit = unit
    convert-exp 0C = 0C
    convert-exp 1C = 1C
    convert-exp (plusC e e₁) = plusC (convert-exp e) (convert-exp e₁)
    convert-exp (var x) = var (convert-var x)
    convert-exp z = z
    convert-exp (s e) = s (convert-exp e)
    convert-exp (rec e e₁ e₂) = rec (convert-exp e) (convert-exp e₁) (convert-exp e₂)
    convert-exp (lam e) = lam (convert-exp e)
    convert-exp (app e e₁) = app (convert-exp e) (convert-exp e₁)
    convert-exp (prod e e₁) = {!!}
    convert-exp (l-proj e) = {!!}
    convert-exp (r-proj e) = {!!}
    convert-exp nil = {!!}
    convert-exp (e ::c e₁) = {!!}
    convert-exp (listrec e e₁ e₂) = {!!}
    convert-exp true = true
    convert-exp false = false
    convert-exp (max x e e₁) = max {!!} {!!} {!!}
    convert-exp (letc e e₁) = app (lam (convert-exp e)) (convert-exp e₁)

    trans-eq : ∀{Γ τ} → (e : Γ Source.|- τ)
                      → (t1 : convert-exp ?) --((NewTranslation.⟨⟨ Γ ⟩⟩c) Complexity-WithLet.|- NewTranslation.|| τ ||))
                      → (t2 : Translation.⟨⟨ Γ ⟩⟩c Complexity.|- Translation.|| τ ||)
                      → {!convert-exp t1!} == t2
    trans-eq e = {!!}
-}

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
module _ where

record LinearOrderStr (D : Set) : Set₁ where
  no-eta-equality
  field
    _<_ : D -> D -> Set

open LinearOrderStr {{...}}

postulate
  D : Set

module _ {{O : LinearOrderStr D}} where
  abstract
    broken : {b c : D} -> (b < c) -> b < c
    broken {b} {c} b<c = b<c
      where
      b<c2 : b < c
      b<c2 = b<c

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
------------------------------------------------------------------------
-- A simple backend
------------------------------------------------------------------------

module RecursiveDescent.Hybrid.Simple where

open import Data.Bool renaming (true to ⊤; false to ⊥)
open import Data.Product.Record
import Data.Product as Prod
open import Data.Maybe
open import Data.BoundedVec.Inefficient
import Data.List as L
open import Data.Nat
open import Data.Function using (id; _∘_)
open import Category.Applicative.Indexed
open import Category.Monad.Indexed
open import Category.Monad.State

open import RecursiveDescent.Hybrid.Type
open import Utilities

------------------------------------------------------------------------
-- Parser monad

private

  P : Set -> IFun ℕ
  P tok = IStateT (BoundedVec tok) L.List

  open module M₁ {tok} =
    RawIMonadPlus (StateTIMonadPlus (BoundedVec tok) L.monadPlus)
    renaming (return to ret)

  open module M₂ {tok} =
    RawIMonadState (StateTIMonadState (BoundedVec tok) L.monad)
    using (get; put; modify)

------------------------------------------------------------------------
-- Run function for the parsers

-- For every successful parse the run function returns the remaining
-- string. (Since there can be several successful parses a list of
-- strings is returned.)

-- This function is structurally recursive with respect to the
-- following lexicographic measure:
--
-- 1) The upper bound of the length of the input string.
-- 2) The parser's proper left corner tree.

private

 module Dummy {tok nt} (g : Grammar tok nt) where

  mutual
    parse : forall n {e c r} ->
            Parser tok nt (e , c) r ->
            P tok n (if e then n else pred n) r
    parse n       (! x)           = parse n (g x)
    parse zero    symbol          = ∅
    parse (suc n) symbol          = eat =<< get
    parse n       (return x)      = ret x
    parse n       fail            = ∅
    parse n       (p₁ ?>>= p₂)    = parse  n      p₁ >>= parse  n ∘′ p₂
    parse zero    (p₁ !>>= p₂)    = ∅
    parse (suc n) (p₁ !>>= p₂)    = parse (suc n) p₁ >>= parse↑ n ∘′ p₂
    parse n       (alt ⊤ _ p₁ p₂) = parse  n      p₁ ∣   parse↑ n    p₂
    parse n       (alt ⊥ ⊤ p₁ p₂) = parse↑ n      p₁ ∣   parse  n    p₂
    parse n       (alt ⊥ ⊥ p₁ p₂) = parse  n      p₁ ∣   parse  n    p₂

    parse↑ : forall n {e c r} -> Parser tok nt (e , c) r -> P tok n n r
    parse↑ n       {⊤} p = parse n p
    parse↑ zero    {⊥} p = ∅
    parse↑ (suc n) {⊥} p = parse (suc n) p >>= \r ->
                           modify ↑ >>
                           ret r

    eat : forall {n} -> BoundedVec tok (suc n) -> P tok (suc n) n tok
    eat []      = ∅
    eat (c ∷ s) = put s >> ret c

-- Exported run function.

parse :  forall {tok nt i r}
      -> Parser tok nt i r -> Grammar tok nt
      -> L.List tok -> L.List (Prod._×_ r (L.List tok))
parse p g s = L.map (Prod.map id toList)
                    (Dummy.parse g _ p (fromList s))

-- A variant which only returns parses which leave no remaining input.

parse-complete :  forall {tok nt i r}
               -> Parser tok nt i r -> Grammar tok nt
               -> L.List tok -> L.List r
parse-complete p g s =
  L.map Prod.proj₁ (L.filter (L.null ∘ Prod.proj₂) (parse p g s))

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

module Cardinality.Finite.SplitEnumerable.Isomorphism where

open import Prelude
open import Container
open import Container.List
open import Data.Fin
open import Container.Membership (ℕ , Fin)
open import Path.Reasoning
open import Data.Sigma.Properties
open import Function.Surjective.Properties
open import Data.Fin.Properties
import Data.List.Membership as 𝕃
open import Container.List.Isomorphism
open import Data.Nat.Properties
open import Data.List using (_∷_; []; List)
import Cardinality.Finite.SplitEnumerable.Container as ℒ
import Cardinality.Finite.SplitEnumerable.Inductive as 𝕃

∈ℒ⇒∈𝕃 : ∀ (x : A) (xs : ⟦ ℕ , Fin ⟧ A) → x ∈ xs → x 𝕃.∈ ℒ→𝕃 xs
∈ℒ⇒∈𝕃 x (suc l , xs) (f0   , p) = f0 , p
∈ℒ⇒∈𝕃 x (suc l , xs) (fs n , p) = 𝕃.push (∈ℒ⇒∈𝕃 x (l , xs ∘ fs) (n , p))

𝕃⇔ℒ⟨ℰ!⟩ : 𝕃.ℰ! A ⇔ ℒ.ℰ! A
𝕃⇔ℒ⟨ℰ!⟩ .fun (sup , cov) = 𝕃→ℒ sup , cov
𝕃⇔ℒ⟨ℰ!⟩ .inv (sup , cov) = ℒ→𝕃 sup , λ x → ∈ℒ⇒∈𝕃 x sup (cov x)
𝕃⇔ℒ⟨ℰ!⟩ .rightInv (sup , cov) i .fst = 𝕃⇔ℒ .rightInv sup i
𝕃⇔ℒ⟨ℰ!⟩ .rightInv (sup , cov) i .snd x = ∈ℒ⇒∈𝕃-rightInv sup (cov x) i
  where
  ∈ℒ⇒∈𝕃-rightInv : ∀ xs x∈xs →
    PathP (λ i → x ∈ 𝕃⇔ℒ .rightInv xs i)
      (∈ℒ⇒∈𝕃 x xs x∈xs) x∈xs
  ∈ℒ⇒∈𝕃-rightInv (suc l , xs) (f0   , x∈xs) i = f0 , x∈xs
  ∈ℒ⇒∈𝕃-rightInv (suc l , xs) (fs n , x∈xs) i =
    let m , q = ∈ℒ⇒∈𝕃-rightInv (l , xs ∘ fs) (n , x∈xs) i
    in fs m , q
𝕃⇔ℒ⟨ℰ!⟩ .leftInv (sup , cov) i .fst = 𝕃⇔ℒ .leftInv sup i
𝕃⇔ℒ⟨ℰ!⟩ .leftInv (sup , cov) i .snd x = ∈ℒ⇒∈𝕃-leftInv sup (cov x) i
  where
  ∈ℒ⇒∈𝕃-leftInv : ∀ xs x∈xs →
    PathP (λ i → x 𝕃.∈ 𝕃→ℒ→𝕃 xs i)
      (∈ℒ⇒∈𝕃 x (𝕃→ℒ xs) x∈xs) x∈xs
  ∈ℒ⇒∈𝕃-leftInv (_ ∷ xs) (f0   , x∈xs) i = f0 , x∈xs
  ∈ℒ⇒∈𝕃-leftInv (_ ∷ xs) (fs n , x∈xs) i =
    let m , p = ∈ℒ⇒∈𝕃-leftInv xs (n , x∈xs) i
    in fs m , p

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Σ where

A : Set₁
A = Set

max_stars_repo_name: L-TChen/agda

max_issues_repo_name: L-TChen/agda

max_forks_repo_name: L-TChen/agda


text:
module STLCRef.SemanticsLB where

-- This file contains a definitional interpreter for STLC+Ref as
-- described in Section 3 of the paper.  The interpreter operates with
-- the notion of monadic bind described in Section 3.3 of the paper;
-- see `Semantics.agda` for the version of the interpreter of STLC+Ref
-- using monadic strength as described in Section 3.4 of the paper.

open import Agda.Primitive
open import Data.Unit
open import Data.Nat hiding (_⊔_ ; _^_)
open import Data.Integer hiding (_⊔_)
open import Data.List
open import Data.Product
open import Data.Maybe hiding (_>>=_)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.Any
open import Data.List.Prefix
open import Data.List.Properties.Extra
open import Data.List.All.Properties.Extra
open import Function
open import Common.Weakening

------------
-- SYNTAX --
------------

-- These definitions correspond to Section 3.1, except we have
-- included integers, integer operations, and a simple conditional
-- expression (if-zero) in the language.

data Ty : Set

Ctx = List Ty

data Ty where
  _⇒_  : (a b : Ty) → Ty
  unit : Ty
  int  : Ty
  ref  : Ty -> Ty

data Expr (Γ : List Ty) : Ty → Set where
  unit  : Expr Γ unit
  var   : ∀ {t} → t ∈ Γ → Expr Γ t
  ƛ     : ∀ {a b} → Expr (a ∷ Γ) b → Expr Γ (a ⇒ b)
  _·_   : ∀ {a b} → Expr Γ (a ⇒ b) → Expr Γ a → Expr Γ b
  num   : ℤ → Expr Γ int
  iop   : (ℤ → ℤ → ℤ) → (l r : Expr Γ int) → Expr Γ int
  ifz   : ∀ {t} → Expr Γ int → Expr Γ t → Expr Γ t → Expr Γ t
  ref   : ∀ {t} → Expr Γ t → Expr Γ (ref t)
  !_    : ∀ {t} → Expr Γ (ref t) → Expr Γ t
  _≔_   : ∀ {t} → Expr Γ (ref t) → Expr Γ t → Expr Γ unit

-----------------------
-- STORES AND VALUES --
-----------------------

StoreTy = List Ty

-- `Val` uses `_∈_` from `Relation.Binary` in the Agda Standard
-- Library to represent typed locations which witness the existence of
-- a store location in the store type.

mutual
  data Val : Ty → (Σ : StoreTy) → Set where
    loc    : ∀ {Σ t} → t ∈ Σ → Val (ref t) Σ
    unit   : ∀ {Σ} → Val unit Σ
    ⟨_,_⟩  : ∀ {Σ Γ a b} → Expr (a ∷ Γ) b → Env Γ Σ → Val (a ⇒ b) Σ
    num   : ∀ {Σ} → ℤ → Val int Σ

  Env : (Γ : Ctx)(Σ : StoreTy) → Set
  Env Γ Σ = All (λ t → Val t Σ) Γ

Store : (Σ : StoreTy) → Set
Store Σ = All (λ t → Val t Σ) Σ

-- The `lookup-store` function is defined in terms of the `lookup`
-- function from `Data.List.All` in the Agda Standard Library.
lookup-store : ∀ {Σ t} → t ∈ Σ → Store Σ → Val t Σ
lookup-store x μ = All.lookup μ x

-- The `update-store` function is defined in terms of the update
-- function for the `All` type: `_All[_]≔'_` from the Standard Library
-- extension (contained in the `lib/*` folder of this artifact).
update-store : ∀ {Σ t} → t ∈ Σ → Val t Σ → Store Σ → Store Σ
update-store ptr v μ = μ All.[ ptr ]≔ v

-----------
-- MONAD --
-----------

-- These definitions correspond to Section 3.3.

M : ∀ {i}(Γ : Ctx) → (p : StoreTy → Set i) → (Σ : StoreTy) → Set i
M Γ p Σ = Env Γ Σ → Store Σ → Maybe (∃ λ Σ' → Store Σ' × p Σ' × Σ ⊑ Σ')

mutual
  weaken-val  : ∀ {a}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Val a Σ → Val a Σ'
  weaken-val ext unit      = unit
  weaken-val ext (loc l)   = loc (∈-⊒ l ext)
  weaken-val ext ⟨ e , E ⟩ = ⟨ e , weaken-env ext E ⟩
  weaken-val ext (num z)   = num z

  weaken-env  : ∀ {Γ}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Env Γ Σ → Env Γ Σ'
  weaken-env ext (v ∷ vs)  = weaken-val ext v ∷ weaken-env ext vs
  weaken-env ext []        = []

return   :    ∀ {Σ Γ}{p : List Ty → Set} → p Σ → M Γ p Σ
return x E μ = just (_ , μ , x , ⊑-refl)

_>>=_ : ∀ {Σ Γ}{p q : StoreTy → Set} →
        (f : M Γ p Σ) → (g : ∀ {Σ'} → Σ ⊑ Σ' → p Σ' → M Γ q Σ') → M Γ q Σ
(f >>= c) E μ = case (f E μ) of λ{
  nothing → nothing ;
  (just (_ , μ' , x , ext)) → case (c ext x (weaken-env ext E) μ') of λ{
    nothing → nothing ;
    (just (_ , μ'' , y , ext')) → just (_ , μ'' , y , ext ⊚ ext')
  }}

getEnv  : ∀ {Σ Γ} → M Γ (Env Γ) Σ
getEnv E = return E E

usingEnv : ∀ {Σ Γ Γ'}{p : List Ty → Set} → Env Γ Σ → M Γ p Σ → M Γ' p Σ
usingEnv E f  _ = f E

timeout : ∀ {Σ Γ}{p : List Ty → Set} → M Γ p Σ
timeout _ _ = nothing

store : ∀ {Σ t Γ} → Val t Σ → M Γ (Val (ref t)) Σ
store {Σ} {t} v _ μ
  = let ext = ∷ʳ-⊒ t Σ
        v'  = loc (∈-∷ʳ Σ t)
        μ'  = (All.map (weaken-val ext) μ) all-∷ʳ (weaken-val ext v)
    in just (_ , μ' , v' , ext)

deref : ∀ {Σ Γ t} → t ∈ Σ → M Γ (Val t) Σ
deref x E μ = return (All.lookup μ x) E μ

update : ∀ {Σ Γ t} → t ∈ Σ → Val t Σ → M Γ (λ _ → ⊤) Σ
update x v E μ = return tt E (update-store x v μ)

eval : ℕ → ∀ {Σ Γ t} → Expr Γ t → M Γ (Val t) Σ
eval zero    _           =
  timeout
eval (suc k) unit        =
  return unit
eval (suc k) (var x)     =
  getEnv >>= λ _ E →
  return (All.lookup E x)
eval (suc k) (ƛ e)       =
  getEnv >>= λ _ E →
  return ⟨ e , E ⟩
eval (suc k) (l · r)     =
  eval k l >>= λ{ ext ⟨ e , E ⟩ →
  eval k r >>= λ ext' v →
  usingEnv (v ∷ weaken-env ext' E) (eval k e) }  -- explicit weakening
eval (suc k) (num x)     =
  return (num x)
eval (suc k) (iop f l r) =
  eval k l >>= λ{ _ (num v) →
  eval k r >>= λ{ _ (num vᵣ) →
  return (num (f v vᵣ)) }}
eval (suc k) (ifz c t e) =
  eval k c >>= λ{ _ (num z) →
  case z of λ{ (+ zero) →
    eval k t
  ; _ →
    eval k e }}
eval (suc k) (ref e)     =
  eval k e >>= λ _ v →
  store v
eval (suc k) (! e)       =
  eval k e >>= λ{ _ (loc l) →
  deref l }
eval (suc k) (r ≔ e)     =
  eval k r >>= λ{ _ (loc l) →
  eval k e >>= λ ext v →
  update (∈-⊒ l ext) v >>= λ _ _ →             -- explicit weakening
  return unit }


text:
module Library where

open import Function using (id; _∘_; _$_) public
open import Relation.Binary.HeterogeneousEquality public
open ≅-Reasoning renaming (begin_ to proof_) public
open import Data.Product renaming (proj₁ to fst; proj₂ to snd) public
open import Data.Empty public using (⊥; ⊥-elim)
open import Data.Unit public using (⊤)
open import Data.Nat public using (ℕ; zero; suc; _+_; module ℕ)
open import Data.Nat.Properties.Simple public
open import Data.Fin public using (Fin; zero; suc; raise)
                            renaming (_+_ to _F+_; fromℕ to fromNat)
open import Level public renaming (suc to lsuc; zero to lzero) hiding (lift)

-- needed for setoids
congid : ∀{a}{A : Set a}{a a' : A}(p : a ≅ a') → cong id p ≅ p
congid refl = refl

congcomp : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
           {a a' : A}(f : B → C)(g : A → B)(p : a ≅ a') →
            cong (f ∘ g) p ≅ cong f (cong g p)
congcomp f g refl = refl

-- should be replaced by dcong
cong' : ∀{a b}{A A' : Set a} → A ≅ A' →
        {B : A → Set b}{B' : A' → Set b} → B ≅ B' →
        {f : ∀ a → B a}{f' : ∀ a → B' a} → f ≅ f' →
        {a : A}{a' : A'} → a ≅ a' → f a ≅ f' a'
cong' refl refl refl refl = refl

-- should be replaced by dicong
icong' : ∀{a b}{A A' : Set a} → A ≅ A' →
         {B : A → Set b}{B' : A' → Set b} → B ≅ B' →
         {f : ∀ {a} → B a}{f' : ∀ {a} → B' a} →
         (λ {a} → f {a}) ≅ (λ {a} → f' {a}) →
         {a : A}{a' : A'} → a ≅ a' → f {a} ≅ f' {a'}
icong' refl refl refl refl = refl

fcong : ∀{a b}{A : Set a}{B : A → Set b}{f f' : (x : A) → B x}
        (a : A) → f ≅ f' → f a ≅ f' a
fcong a refl = refl

dcong : ∀{a b}{A A' : Set a}{B : A → Set b}{B' : A' → Set b}
        {f : (a : A) → B a}{f' : (a : A') → B' a}{a : A}{a' : A'} →
        a ≅ a' → B ≅ B' → f ≅ f' → f a ≅ f' a'
dcong refl refl refl = refl

dicong : ∀{a b}{A A' : Set a}{B : A → Set b}{B' : A' → Set b}
         {f : ∀ {a} → B a}{f' : ∀ {a} → B' a} → {a : A}{a' : A'} →
         a ≅ a' →  B ≅ B' →
         (λ {a} → f {a}) ≅ (λ {a} → f' {a}) →
         f {a} ≅ f' {a'}
dicong refl refl refl = refl

ifcong : ∀{a b}{A : Set a}{B : A → Set b}{f f' : {x : A} → B x}(a : A) →
         _≅_ {_}{ {x : A} → B x} f { {x : A} → B x} f' → f {a} ≅ f' {a}
ifcong a refl = refl

cong₃ : ∀{a b c d}{A : Set a}{B : A → Set b}
        {C : ∀ x → B x → Set c }{D : ∀ x y → C x y → Set d}
        (f : ∀ x y z → D x y z)
        {a a' : A} → a ≅ a' →
        {b : B a}{b' : B a'} → b ≅ b' →
        {c : C a b}{c' : C a' b'} → c ≅ c' →
        f a b c ≅ f a' b' c'
cong₃ f refl refl refl = refl

ir : ∀{a}{A B : Set a}{x : A}{y : B}(p q : x ≅ y) → p ≅ q
ir refl refl = refl

stripsubst : ∀{a c}{A : Set a}(C : A → Set c) →
             {a : A} → (c : C a) →
             {b : A} → (p : a ≅ b) →
             subst C p c ≅ c
stripsubst C c refl = refl

postulate ext : ∀{a b}{A : Set a}{B B' : A → Set b}
                {f : ∀ a → B a}{g : ∀ a → B' a} →
                (∀ a → f a ≅ g a) → f ≅ g

postulate dext : ∀{a b}{A A' : Set a}{B : A → Set b}{B' : A' → Set b}
                 {f : ∀ a → B a}{g : ∀ a → B' a} →
                (∀ {a a'} → a ≅ a' → f a ≅ g a') → f ≅ g

-- this could just be derived from ext

postulate iext : ∀{a b}{A : Set a}{B B' : A → Set b}
                 {f : ∀ {a} → B a}{g : ∀{a} → B' a} →
                 (∀ a → f {a} ≅ g {a}) →
                 _≅_ {_}{ {a : A} → B a} f { {a : A} → B' a} g

postulate diext : ∀{a b}{A A' : Set a}{B : A → Set b}{B' : A' → Set b}
                  {f : ∀ {a} → B a}{f' : ∀{a'} → B' a'} →
                  (∀{a a'} → a ≅ a' → f {a} ≅ f' {a'}) →
                  _≅_ {_}{ {a : A} → B a} f { {a' : A'} → B' a'} f'

hir : ∀{a}{A A' A'' A''' : Set a}{a : A}{a' : A'}{a'' : A''}{a''' : A'''}
           {p : a ≅ a'}{q : a'' ≅ a'''} → a ≅ a'' → p ≅ q
hir {p = refl} {q = refl} refl = refl

hir' : ∀{a}{A A' A'' A''' : Set a}{a : A}{a' : A'}{a'' : A''}{a''' : A'''}
           {p : a ≅ a'}{q : a'' ≅ a'''} → a' ≅ a''' → p ≅ q
hir' {p = refl} {q = refl} refl = refl

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


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

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma

open import Sec2preliminaries
open import Sec3hedberg
open import Sec4hasConstToSplit

-- In this section, we require function extensionality again.

module Sec6populatedness where

-- Definition 6.1
Pop : Type → Type
Pop X = (f : X → X) → const f → fix f

-- Theorem 6.2
Trunc→Pop : {X : Type} → Trunc X → Pop X
Trunc→Pop z f c = rec {P = fix f} (fixed-point f c) (to-fix f c) z

-- Lemma 6.3
module _ {X : Type} where

  pop→splitSup→X : Pop X → splitSup X → X
  pop→splitSup→X pop sps = fst (pop (fst fc) (snd fc)) where
                             fc = (snd hasConst↔splitSup sps)

  use-funct : (splitSup X → X) → Trunc (splitSup X) → Trunc X
  use-funct f = trunc-functorial f

  tr-hst-X→pop : (Trunc (splitSup X) → Trunc X) → Pop X
  tr-hst-X→pop g f c = rec (fixed-point f c) (to-fix f c) (g ∣ hasConst→splitSup (f , c) ∣)

  -- we formulate the two logical equivalence that we will need explicitly:
  pop-alt : Pop X ↔ (Trunc (splitSup X) → Trunc X)
  pop-alt = use-funct ∘ pop→splitSup→X , tr-hst-X→pop

  pop-alt' : Pop X ↔ (splitSup X → X)
  pop-alt' = pop→splitSup→X , tr-hst-X→pop ∘ use-funct

-- Theorem 6.4
pop-alt₂ : {X : Type} → Pop X ↔₀₁ ((P : Type) → (is-prop P) → (X ↔ P) → P)
pop-alt₂ {X} = one , two where

  one : Pop X → (P : Type) → is-prop P → (X ↔ P) → P
  one pop P pp (xp , px) = xp (fst (pop f c)) where
    f : X → X
    f = px ∘ xp
    c : const f
    c x₁ x₂ = ap px (prop-has-all-paths pp _ _)

  two : ((P : Type) → is-prop P → (X ↔ P) → P) → Pop X
  two rest f c = rest (fix f) (fixed-point f c) (to-fix f c , from-fix f)

-- Theorem 6.5
pop-property₁ : {X : Type} → X → Pop X
pop-property₁ = Trunc→Pop ∘ ∣_∣

-- this (and the following results of this section) needs function extensionality
open import library.types.Pi

pop-property₂ : {X : Type} → is-prop (Pop X)
pop-property₂ = Π-is-prop (λ f → Π-is-prop (λ c → fixed-point f c))

-- Theorem 6.6
hasConst↔PopX→X : {X : Type} → (hasConst X) ↔ (Pop X → X)
hasConst↔PopX→X {X} = hasConst→PopX→X , rev where

  hasConst→PopX→X : hasConst X → Pop X → X
  hasConst→PopX→X (f , c) pop = fst (pop f c)

  rev : (Pop X → X) → hasConst X
  rev pp = (pp ∘ pop-property₁) ,
           (λ x₁ x₂ → ap pp (prop-has-all-paths pop-property₂ _ _))

-- Theorem 6.6, second part
prop→hasConst×PopX→X : {X : Type} → (is-prop X) → (hasConst X) × (Pop X → X)
prop→hasConst×PopX→X p = fc , fst hasConst↔PopX→X fc where

  fc = idf _ , prop-has-all-paths p

-- Theorem 6.7
pop-idem : {X : Type} → (Pop (Pop X)) ≃ (Pop X)
pop-idem {X} = equiv f g auto₁ auto₂ where

  f = snd (prop→hasConst×PopX→X pop-property₂)
  g = pop-property₁

  auto₁ = λ _ → prop-has-all-paths pop-property₂ _ _
  auto₂ = λ _ → prop-has-all-paths pop-property₂ _ _

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

U = Set

id  : {A : Set} → A → A
id = λ x → x

id2 : ∀ {A} → A → A
id2 = id id

id3 : ∀ {A} → A → A
id3 = λ x → id x

id4 : {A : Set} -> A -> A
id4 = \x -> x

the : (A : Set) → A → A
the = λ _ x → x

constTy = {A B : Set} → A → B → A

const : constTy
const = λ x y → x

constU = const {Set}

namedArgTest  = const {B = U} U
namedArgTest2 = the constTy (λ x y → x) {B = U} U

-- Church bools
--------------------------------------------------------------------------------
Bool = (B : U) → B → B → B

true  : Bool
true = λ _ t f → t

false : Bool
false = λ _ t f  → f

and : Bool → Bool → Bool
and = λ b1 b2 → b1 Bool true b2

-- Church natural numbers
--------------------------------------------------------------------------------

Nat : U
Nat = (n : U) → (n → n) → n → n

zero : Nat
zero = λ n s z → z

suc : Nat → Nat
suc = λ a n s z → s (a n s z)

n2 : Nat
n2 = λ n s z → s (s z)

n5 : Nat
n5 = λ n s z → s (s (s (s (s z))))

mul : Nat → Nat → Nat
mul = λ a b n s z → a n (b n s) z

add : Nat → Nat → Nat
add = λ a b n s z → a n s (b n s z)

n10    = mul n2    n5
n10b   = mul n5    n2
n100   = mul n10   n10
n100b  = mul n10b  n10b
n10k   = mul n100  n100
n10kb  = mul n100b n100b
n100k  = mul n10k  n10
n100kb = mul n10kb n10b
n1M    = mul n10k  n100
n1Mb   = mul n10kb n100b
n10M   = mul n1M   n10
n10Mb  = mul n1Mb  n10b
n100M  = mul n10M  n10
n200M  = mul n2    n100M

-- Church lists
--------------------------------------------------------------------------------

List : U → U
List = λ a → (l : U) → (a → l → l) → l → l

lnil  : ∀{a} → List a
lnil = λ l c n → n

lcons : ∀{a} → a → List a → List a
lcons = λ a as l c n → c a (as l c n)

list1 = lcons true (lcons false (lcons false lnil))

map : ∀{a b} → (a → b) → List a → List b
map = λ f as l c → as l (λ a → c (f a))

-- Church vectors
--------------------------------------------------------------------------------

Vec : U → Nat → U
Vec = λ a n → (V : Nat → U) → V zero → (∀{n} → a → V n → V (suc n)) → V n

vnil : ∀{a} → Vec a zero
vnil = λ V n c → n

vcons : ∀{a n} → a → Vec a n → Vec a (suc n)
vcons = λ a as V n c → c a (as V n c)

vec1 = vcons true (vcons false (vcons true vnil))

vecStress =
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true (vcons true (vcons true (vcons true (vcons true
   (vcons true (vcons true
   vnil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
       ))))))))))))))))))))))))))))))))))))

-- Leibniz (Church) propositional equality, useful for testing conversion.
--------------------------------------------------------------------------------

Eq : ∀{A : U} → A → A → U
Eq {A} = λ x y → (P : A → U) → P x → P y

refl : ∀{A}{x : A} → Eq x x
refl = λ P px → px

trans : ∀{A}{x y z : A} → Eq x y → Eq y z → Eq x z
trans = λ p q → q _ p

sym : ∀{A}{x y : A} → Eq x y → Eq y x
sym {_}{x}{y} = λ p → p (λ y → Eq y x) refl

ap : ∀{A B}(f : A → B){x y : A} → Eq x y → Eq (f x) (f y)
ap = λ f {x}{y} p → p (λ y → Eq (f x) (f y)) refl

-- Pairs, Top, Bot
--------------------------------------------------------------------------------

Pair : U → U → U
Pair = λ A B → (Pair : U)(pair : A → B → Pair) → Pair

pair : ∀{A B} → A → B → Pair A B
pair = λ a b Pair pair → pair a b

proj1 : ∀{A B} → Pair A B → A
proj1 = λ p → p _ (λ x y → x)

proj2 : ∀{A B} → Pair A B → B
proj2 = λ p → p _ (λ x y → y)

Top : U
Top = (Top : U)(tt : Top) → Top

tt : Top
tt = λ Top tt → tt

Bot : U
Bot = (Bot : U) → Bot

-- Dependent function composition
--------------------------------------------------------------------------------

comp :
  ∀ {A : U}
  {B : A → U}
  {C : ∀{a} → B a → U}
  (f : ∀{a}(b : B a) → C b)
  (g : (a : A) → B a)
  (x : A)
  → C (g x)
comp = λ f g a → f (g a)

compTest1 : Nat → Nat
compTest1 = comp suc suc

compTest2 : ∀{m A} → A → Vec A m → Vec A (suc (suc m))
compTest2 = λ a → comp (vcons a) (vcons a)

-- Some stress tests
--------------------------------------------------------------------------------

nfun : Nat → U
nfun n = n U (λ A → U → A) U

-- OK
synEqTest1 : Eq n1M n1M
synEqTest1 = refl

-- fail
-- synEqTest2 : nfun n10k → nfun n10k
-- synEqTest2 = λ x → x

-- OK
idStress : ∀{A} → A → A
idStress =
   id id id id id id id id id id id id id id id id id id id id
   id id id id id id id id id id id id id id id id id id id id

-- fail
-- pairStress : Top
-- pairStress =
--    let x0  = pair tt tt
--        x1  = pair x0  x0
--        x2  = pair x1  x1
--        x3  = pair x2  x2
--        x4  = pair x3  x3
--        x5  = pair x4  x4
--        x6  = pair x5  x5
--        x7  = pair x6  x6
--        x8  = pair x7  x7
--        x9  = pair x8  x8
--        x10 = pair x9  x9
--        x11 = pair x10 x10
--        x12 = pair x11 x11
--        x13 = pair x12 x12
--        x14 = pair x13 x13
--        x15 = pair x14 x14
--        x16 = pair x15 x15
--        x17 = pair x16 x16
--        x18 = pair x17 x17
--        x19 = pair x18 x18
--        x20 = pair x19 x19
--    in tt

forceNat : Nat → Bool
forceNat n = n _ (λ b → b) true

computeTest = forceNat n10M

-- Conversion checking tests
--------------------------------------------------------------------------------

-- conv100k : Eq n100k n100kb
-- conv100k = refl

-- conv1M : Eq n1M n1Mb
-- conv1M = refl

-- OOM
-- conv10M : Eq n10M n1M0b
-- conv10M = refl

-- convNfun1M : Eq (nfun n1M) (nfun n1Mb)
-- convNfun1M = refl

-- conv10kmeta : Eq n10k (add n10kb _)
-- conv10kmeta = refl

-- OOM
-- conv1Mmeta : Eq n1M (add n1Mb _)
-- conv1Mmeta = refl

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

-- normalized instantly
lazyU = const U (forceNat n10M)

localCBN : Nat → Bool
localCBN
  = λ n → let m = forceNat (mul n n100k)
          in n _ (λ b → and m b) true

cbnReference = forceNat (mul n10 n100k)
localCBNtest = localCBN n10

-- Church-coded simply typed lambda calculus
--------------------------------------------------------------------------------

Ty : U
Ty
 = (Ty  : U)
   (ι   : Ty)
   (fun : Ty → Ty → Ty)
 → Ty

ι : Ty
ι
 = λ _ ι _ → ι

fun : Ty → Ty → Ty
fun
 = λ A B Ty ι fun → fun (A Ty ι fun) (B Ty ι fun)

Con : U
Con
 = (Con : U)
   (nil  : Con)
   (cons : Con → Ty → Con)
 → Con

nil : Con
nil
 = λ Con nil cons → nil

cons : Con → Ty → Con
cons
 = λ Γ A Con nil cons → cons (Γ Con nil cons) A

Var : Con → Ty → U
Var
 = λ Γ A →
   (Var : Con → Ty → U)
   (vz  : ∀{Γ A} → Var (cons Γ A) A)
   (vs  : ∀{Γ B A} → Var Γ A → Var (cons Γ B) A)
 → Var Γ A

vz : ∀{Γ A} → Var (cons Γ A) A
vz
 = λ Var vz vs → vz

vs : ∀{Γ B A} → Var Γ A → Var (cons Γ B) A
vs
 = λ x Var vz vs → vs (x Var vz vs)

Tm : Con → Ty → U
Tm
 = λ Γ A →
   (Tm  : Con → Ty → U)
   (var : ∀{Γ A} → Var Γ A → Tm Γ A)
   (lam : ∀{Γ A B} → Tm (cons Γ A) B → Tm Γ (fun A B))
   (app : ∀{Γ A B} → Tm Γ (fun A B) → Tm Γ A → Tm Γ B)
 → Tm Γ A

var : ∀{Γ A} → Var Γ A → Tm Γ A
var
 = λ x Tm var lam app → var x

lam : ∀{Γ A B} → Tm (cons Γ A) B → Tm Γ (fun A B)
lam
 = λ t Tm var lam app → lam (t Tm var lam app)

app : ∀{Γ A B} → Tm Γ (fun A B) → Tm Γ A → Tm Γ B
app
 = λ t u Tm var lam app → app (t Tm var lam app) (u Tm var lam app)

-- Well-typed interpreter for Church-coded STLC
--------------------------------------------------------------------------------

EvalTy : Ty → U
EvalTy
 = λ A → A _ Bot (λ A B → A → B)

EvalCon : Con → U
EvalCon
 = λ Γ → Γ _ Top (λ Δ A → Pair Δ (EvalTy A))

EvalVar : ∀{Γ A} → Var Γ A → EvalCon Γ → EvalTy A
EvalVar
 = λ x → x (λ Γ A → EvalCon Γ → EvalTy A)
           (λ env → proj2 env)
           (λ rec env → rec (proj1 env))

EvalTm : ∀{Γ A} → Tm Γ A → EvalCon Γ → EvalTy A
EvalTm
 = λ t → t (λ Γ A → EvalCon Γ → EvalTy A)
          EvalVar
          (λ t env α → t (pair env α))
          (λ t u env → t env (u env))

-- Large embedded STLC term
--------------------------------------------------------------------------------

t1 : Tm nil (fun (fun ι ι) (fun ι ι))
t1
 = lam (lam (
      app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz)) (app (var (vs vz))
     (var vz))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     ))))))))))))))))))))))))))))))))))))))
     ))

-- test evaluation
evalTest = EvalTm t1 tt

max_stars_repo_name: zarybnicky/smalltt

max_issues_repo_name: zarybnicky/smalltt

max_forks_repo_name: zarybnicky/smalltt


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

open import Categories.Category

-- Biproducts, a-la Karvonen.
--
-- This definition has advantages over more traditional ones,
-- namely that that we don't require either enrichment in CMon/Ab, or Zero Objects.
--
-- See https://arxiv.org/abs/1801.06488
module Categories.Object.Biproduct {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Object.Coproduct 𝒞
open import Categories.Object.Product 𝒞

open import Categories.Morphism 𝒞

open Category 𝒞
open HomReasoning

private
  variable
    A B C D : Obj
    f g h : A ⇒ B

record IsBiproduct {A B A⊕B : Obj} (π₁ : A⊕B ⇒ A) (π₂ : A⊕B ⇒ B) (i₁ : A ⇒ A⊕B) (i₂ : B ⇒ A⊕B) : Set (o ⊔ ℓ ⊔ e) where
  field
    isCoproduct : IsCoproduct i₁ i₂
    isProduct : IsProduct π₁ π₂

    π₁∘i₁≈id : π₁ ∘ i₁ ≈ id
    π₂∘i₂≈id : π₂ ∘ i₂ ≈ id
    permute  : i₁ ∘ π₁ ∘ i₂ ∘ π₂ ≈ i₂ ∘ π₂ ∘ i₁ ∘ π₁

  open IsCoproduct isCoproduct public renaming (unique to []-unique)
  open IsProduct isProduct public renaming (unique to ⟨⟩-unique)

record Biproduct (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    A⊕B : Obj

    π₁    : A⊕B ⇒ A
    π₂    : A⊕B ⇒ B

    i₁    : A ⇒ A⊕B
    i₂    : B ⇒ A⊕B

    isBiproduct : IsBiproduct π₁ π₂ i₁ i₂

  open IsBiproduct isBiproduct public

IsBiproduct⇒Biproduct : {π₁ : C ⇒ A} {π₂ : C ⇒ B} {i₁ : A ⇒ C} {i₂ : B ⇒ C}  → IsBiproduct π₁ π₂ i₁ i₂ → Biproduct A B
IsBiproduct⇒Biproduct isBiproduct = record
  { isBiproduct = isBiproduct
  }

Biproduct⇒IsBiproduct : (b : Biproduct A B) → IsBiproduct (Biproduct.π₁ b) (Biproduct.π₂ b) (Biproduct.i₁ b) (Biproduct.i₂ b)
Biproduct⇒IsBiproduct biproduct = Biproduct.isBiproduct biproduct

Biproduct⇒Product : Biproduct A B → Product A B
Biproduct⇒Product b = record
  { ⟨_,_⟩ = ⟨_,_⟩
  ; project₁ = project₁
  ; project₂ = project₂
  ; unique = ⟨⟩-unique
  }
  where
    open Biproduct b

Biproduct⇒Coproduct : Biproduct A B → Coproduct A B
Biproduct⇒Coproduct b = record
  { [_,_] = [_,_]
  ; inject₁ = inject₁
  ; inject₂ = inject₂
  ; unique = []-unique
  }
  where
    open Biproduct b


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

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

module Categories.Category.Monoidal.Rigid {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Level

open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation.NaturalIsomorphism

open Category C
open Commutation C

private
  variable
    X : Obj

-- left rigid monoidal category
record LeftRigid : Set (levelOfTerm M) where
  open Monoidal M public

  field
    _⁻¹ : Obj → Obj
    η   : ∀ {X} → unit ⇒ X ⊗₀ X ⁻¹
    ε   : ∀ {X} → X ⁻¹ ⊗₀ X  ⇒ unit

    snake₁ : [ X ⇒ X ]⟨
               unitorˡ.to  ⇒⟨ (unit ⊗₀ X) ⟩
               (η ⊗₁ id)  ⇒⟨ (X ⊗₀ X ⁻¹) ⊗₀ X ⟩
               associator.from  ⇒⟨ X ⊗₀ (X ⁻¹ ⊗₀ X) ⟩
               (id ⊗₁ ε) ⇒⟨ X ⊗₀ unit ⟩
               unitorʳ.from
             ≈ id
             ⟩
    snake₂ : [ X ⁻¹ ⇒ X ⁻¹ ]⟨
               unitorʳ.to  ⇒⟨ X ⁻¹ ⊗₀ unit ⟩
               (id ⊗₁ η)  ⇒⟨ X ⁻¹ ⊗₀ (X ⊗₀ X ⁻¹) ⟩
               associator.to  ⇒⟨ (X ⁻¹ ⊗₀ X) ⊗₀ X ⁻¹ ⟩
               (ε ⊗₁ id) ⇒⟨ unit ⊗₀ X ⁻¹ ⟩
               unitorˡ.from
             ≈ id
             ⟩

-- right rigid monoidal category
record RightRigid : Set (levelOfTerm M) where
  open Monoidal M public

  field
    _⁻¹ : Obj → Obj
    η   : ∀ {X} → unit ⇒ X ⁻¹ ⊗₀ X
    ε   : ∀ {X} → X ⊗₀ X ⁻¹  ⇒ unit

    snake₁ : [ X ⇒ X ]⟨
               unitorʳ.to  ⇒⟨ (X ⊗₀ unit) ⟩
               (id ⊗₁ η)  ⇒⟨ X ⊗₀ (X ⁻¹ ⊗₀ X) ⟩
               associator.to ⇒⟨ (X ⊗₀ X ⁻¹) ⊗₀ X ⟩
               (ε ⊗₁ id) ⇒⟨ unit ⊗₀ X ⟩
               unitorˡ.from
             ≈ id
             ⟩
    snake₂ : [ X ⁻¹ ⇒ X ⁻¹ ]⟨
               unitorˡ.to  ⇒⟨ unit ⊗₀ X ⁻¹ ⟩
               (η ⊗₁ id)  ⇒⟨ (X ⁻¹ ⊗₀ X) ⊗₀ X ⁻¹ ⟩
               associator.from  ⇒⟨ X ⁻¹ ⊗₀ (X ⊗₀ X ⁻¹) ⟩
               (id ⊗₁ ε) ⇒⟨ X ⁻¹ ⊗₀ unit ⟩
               unitorʳ.from
             ≈ id
             ⟩


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

-- The 'strict' category of groupoids.
-- The difference here is that _≈_ is not |NaturalIsomorphism| but |_≡F_|

open import Level
open import Relation.Binary.PropositionalEquality using (refl)

open import Categories.Category using (Category)
open import Categories.Category.Groupoid using (Groupoid)
open import Categories.Category.Instance.Groupoids using (F-resp-⁻¹)
open import Categories.Functor using (Functor; id; _∘F_)
open import Categories.Functor.Equivalence

private
  variable
    o ℓ e : Level

open Groupoid using (category)

Groupoids : ∀ o ℓ e → Category (suc (o ⊔ ℓ ⊔  e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
Groupoids o ℓ e = record
  { Obj       = Groupoid o ℓ e
  ; _⇒_       = λ G H → Functor (category G) (category H)
  ; _≈_       = _≡F_
  ; id        = id
  ; _∘_       = _∘F_
  ; assoc     = λ {_ _ _ _ F G H} → ≡F-assoc     {F = F} {G} {H}
  ; sym-assoc = λ {_ _ _ _ F G H} → ≡F-sym-assoc {F = F} {G} {H}
  ; identityˡ = ≡F-identityˡ
  ; identityʳ = ≡F-identityʳ
  ; identity² = ≡F-identity²
  ; equiv     = ≡F-equiv
  ; ∘-resp-≈  = ∘F-resp-≡F
  }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
open import Data.PropFormula 2

⋀comm : ∀ {Γ}{φ ψ : PropFormula} → Γ ⊢ φ ∧ ψ ⊃ ψ ∧ φ
⋀comm {Γ} {φ = φ}{ψ} =
  ⊃-intro $
    ∧-intro
      (∧-proj₂ $ assume {Γ = Γ} $ φ ∧ ψ)
      (∧-proj₁ {ψ = ψ} $ assume {Γ = Γ} $ φ ∧ ψ)

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


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

module BitVec where

open import Data.Bool       using (Bool; false; true; _∨_; _∧_)
open import Data.Fin        using (Fin; toℕ)
open import Data.List       using (List; []; _∷_; foldr)
open import Data.Nat        using (ℕ; zero; suc; _≡ᵇ_)
open import Data.Product    using (_×_; _,_; proj₂)
open import Data.String     using (String; fromList)
open import Data.Vec        using (Vec; []; _∷_; map; lookup; replicate; _[_]%=_; toList; zip; zipWith)

open import Function        using (_∘_)

-- Bit vector representation of finite sets

BitVec : ℕ → Set
BitVec = Vec Bool

show : {n : ℕ} → BitVec n → String
show = fromList ∘ toList ∘ map (λ {true → '1' ; false → '0'})

empty : {n : ℕ} → BitVec n
empty = replicate false

insert : {n : ℕ} → Fin n → BitVec n → BitVec n
insert k s = s [ k ]%= (λ _ → true)

infixr 5 _∪_
_∪_ : {n : ℕ} → BitVec n → BitVec n → BitVec n
_∪_ = zipWith _∨_

infixr 6 _∩_
_∩_ : {n : ℕ} → BitVec n → BitVec n → BitVec n
_∩_ = zipWith _∧_

infix 4 _∈_
_∈_ : {n : ℕ} → Fin n → BitVec n → Bool
b ∈ bv = lookup bv b

indices : {n : ℕ} → Vec (Fin n) n
indices {ℕ.zero} = []
indices {suc n} = Fin.zero ∷ map Fin.suc (indices {n})

elements : {n : ℕ} → BitVec n → List (Fin n)
elements {n} bv = foldr f [] (toList (zip bv indices))
  where f : Bool × Fin n → List (Fin n) → List (Fin n)
        f (false , _) xs = xs
        f (true  , x) xs = x ∷ xs

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
{-# OPTIONS --without-K #-}
module NTypes.Negation where

open import FunExt
open import NTypes
open import Types

¬-isProp : ∀ {a} {A : Set a} → isProp (¬ A)
¬-isProp ¬a _ = funext λ a → 0-elim (¬a a)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures