text:
module MLib.Algebra.PropertyCode.Structures where

open import MLib.Prelude
open import MLib.Finite

open import MLib.Algebra.PropertyCode.RawStruct public
open import MLib.Algebra.PropertyCode.Core public
open import MLib.Algebra.PropertyCode public

open import Relation.Binary as B using (Setoid)

open import Data.List.Any using (Any; here; there)
open import Data.Bool using (_∨_)

open import Category.Applicative

--------------------------------------------------------------------------------
--  Combinators for constructing property sets from smaller sets
--------------------------------------------------------------------------------

subΠ : ∀ {k k′} {code : Code k} {code′ : Code k′} →
  let open Code code using (K)
      open Code code′ using () renaming (K to K′)
  in (∀ {n} → K′ n → Maybe (K n)) →
     Properties code → Properties code′ → Properties code′
hasProperty (subΠ f Π₀ Π₁) (π , κs) = hasProperty Π₁ (π , κs) ∨ satUnder
  where
    satUnder : Bool
    satUnder with List.All.traverse f κs
    satUnder | just κs′ = hasProperty Π₀ (π , κs′)
    satUnder | nothing = false

subΠ′ : ∀ {k k′} {code : Code k} {code′ : Code k′} →
  let open Code code using (K)
      open Code code′ using () renaming (K to K′)
  in (∀ {n} → K′ n → Maybe (K n)) →
     Properties code → List (Property K′) → Properties code′
subΠ′ f Π πs = subΠ f Π (fromList πs)

--------------------------------------------------------------------------------
--  Code Types
--------------------------------------------------------------------------------

data MagmaK : ℕ → Set where
  ∙ : MagmaK 2

data MonoidK : ℕ → Set where
  ε : MonoidK 0
  ∙ : MonoidK 2

data BimonoidK : ℕ → Set where
  0# 1# : BimonoidK 0
  + * : BimonoidK 2

--------------------------------------------------------------------------------
--  Code Proofs
--------------------------------------------------------------------------------

module _ where
  open Code

  -- TODO: automate proofs like these.

  magmaCode : Code _
  K magmaCode = MagmaK
  boundAt magmaCode 2 = 1
  boundAt magmaCode _ = 0
  isFiniteAt magmaCode 0 = enumerable-isFiniteSet [] λ ()
  isFiniteAt magmaCode 1 = enumerable-isFiniteSet [] λ ()
  isFiniteAt magmaCode (suc (suc (suc _))) = enumerable-isFiniteSet [] λ ()
  isFiniteAt magmaCode 2 = enumerable-isFiniteSet (∙ ∷ []) λ {∙ → here ≡.refl}

  monoidCode : Code _
  K monoidCode = MonoidK
  boundAt monoidCode 0 = 1
  boundAt monoidCode 2 = 1
  boundAt monoidCode _ = 0
  isFiniteAt monoidCode 0 = enumerable-isFiniteSet (ε ∷ []) λ {ε → here ≡.refl}
  isFiniteAt monoidCode 1 = enumerable-isFiniteSet [] λ ()
  isFiniteAt monoidCode 2 = enumerable-isFiniteSet (∙ ∷ []) λ {∙ → here ≡.refl}
  isFiniteAt monoidCode (suc (suc (suc _))) = enumerable-isFiniteSet [] λ ()

  bimonoidCode : Code _
  K bimonoidCode = BimonoidK
  boundAt bimonoidCode 0 = 2
  boundAt bimonoidCode 2 = 2
  boundAt bimonoidCode _ = 0
  isFiniteAt bimonoidCode 0 = enumerable-isFiniteSet (0# ∷ 1# ∷ []) λ {0# → here ≡.refl; 1# → there (here ≡.refl)}
  isFiniteAt bimonoidCode 1 = enumerable-isFiniteSet [] λ ()
  isFiniteAt bimonoidCode 2 = enumerable-isFiniteSet (+ ∷ * ∷ []) λ {+ → here ≡.refl; * → there (here ≡.refl)}
  isFiniteAt bimonoidCode (suc (suc (suc _))) = enumerable-isFiniteSet [] λ ()

--------------------------------------------------------------------------------
--  Subparts of bimonoids
--------------------------------------------------------------------------------

+-part : ∀ {n} → BimonoidK n → Maybe (MonoidK n)
+-part 0# = just ε
+-part + = just ∙
+-part _ = nothing

*-part : ∀ {n} → BimonoidK n → Maybe (MonoidK n)
*-part 1# = just ε
*-part * = just ∙
*-part _ = nothing

--------------------------------------------------------------------------------
--  Some named property combinations
--------------------------------------------------------------------------------

isSemigroup : Properties magmaCode
isSemigroup = fromList (associative on ∙ ∷ [])

isMonoid : Properties monoidCode
isMonoid = subΠ′ (λ {∙ → just ∙; _ → nothing}) isSemigroup
  ( ε is leftIdentity for ∙
  ∷ ε is rightIdentity for ∙
  ∷ [])

isCommutativeMonoid : Properties monoidCode
isCommutativeMonoid = subΠ just isMonoid (fromList (commutative on ∙ ∷ []))

isSemiring : Properties bimonoidCode
isSemiring =
  subΠ +-part isCommutativeMonoid (
  subΠ′ *-part isMonoid
  ( 0# is leftZero for *
  ∷ 0# is rightZero for *
  ∷ * ⟨ distributesOverˡ ⟩ₚ +
  ∷ * ⟨ distributesOverʳ ⟩ₚ +
  ∷ []
  ))

--------------------------------------------------------------------------------
--  Subcode Proofs
--------------------------------------------------------------------------------

magma⊂monoid : IsSubcode magmaCode monoidCode
magma⊂monoid .subK→supK ∙ = ∙
magma⊂monoid .supK→subK ∙ = just ∙
magma⊂monoid .supK→subK ε = nothing
magma⊂monoid .acrossSub ∙ = ≡.refl

+-monoid⊂bimonoid : IsSubcode monoidCode bimonoidCode
+-monoid⊂bimonoid .subK→supK ∙ = +
+-monoid⊂bimonoid .subK→supK ε = 0#
+-monoid⊂bimonoid .supK→subK + = just ∙
+-monoid⊂bimonoid .supK→subK 0# = just ε
+-monoid⊂bimonoid .supK→subK _ = nothing
+-monoid⊂bimonoid .acrossSub ∙ = ≡.refl
+-monoid⊂bimonoid .acrossSub ε = ≡.refl

*-monoid⊂bimonoid : IsSubcode monoidCode bimonoidCode
*-monoid⊂bimonoid .subK→supK ∙ = *
*-monoid⊂bimonoid .subK→supK ε = 1#
*-monoid⊂bimonoid .supK→subK * = just ∙
*-monoid⊂bimonoid .supK→subK 1# = just ε
*-monoid⊂bimonoid .supK→subK _ = nothing
*-monoid⊂bimonoid .acrossSub ∙ = ≡.refl
*-monoid⊂bimonoid .acrossSub ε = ≡.refl

--------------------------------------------------------------------------------
--  Conversion to structures from the agda standard library
--------------------------------------------------------------------------------

module Into {c ℓ} where
  open Algebra using (Semigroup; Monoid; CommutativeMonoid; Semiring)

  module _ (struct : Struct magmaCode c ℓ) where
    open Struct struct

    semigroup : ∀ ⦃ hasSemigroup : Hasₚ isSemigroup ⦄ → Semigroup _ _
    semigroup ⦃ hasSemigroup ⦄ = record
      { _∙_ = ⟦ ∙ ⟧
      ; isSemigroup = record
        { isEquivalence = isEquivalence
        ; assoc = from hasSemigroup (associative on ∙)
        ; ∙-cong = cong ∙
        }
      }

  module _ (struct : Struct monoidCode c ℓ) where
    open Struct struct

    monoid : ⦃ hasMonoid : Hasₚ isMonoid ⦄ → Monoid c ℓ
    monoid ⦃ hasMonoid ⦄ = record
      { isMonoid = record
        { isSemigroup = S.isSemigroup
        ; identity = from hasMonoid (ε is leftIdentity for ∙) , from hasMonoid (ε is rightIdentity for ∙)
        }
      }
      where
      magmaPart : Struct magmaCode c ℓ
      magmaPart = substruct magma⊂monoid

      module S = Semigroup (semigroup magmaPart ⦃ toSubstruct magma⊂monoid (weaken hasMonoid) ⦄)

    commutativeMonoid : ⦃ hasCommutativeMonoid : Hasₚ isCommutativeMonoid ⦄ → CommutativeMonoid c ℓ
    commutativeMonoid ⦃ hasCommutativeMonoid ⦄ = record
      { isCommutativeMonoid = record
        { isSemigroup = S.isSemigroup
        ; identityˡ = from hasCommutativeMonoid (ε is leftIdentity for ∙)
        ; comm = from hasCommutativeMonoid (commutative on ∙)
        }
      }
      where
      magmaPart : Struct magmaCode c ℓ
      magmaPart = substruct magma⊂monoid

      module S = Semigroup (semigroup magmaPart ⦃ toSubstruct magma⊂monoid (weaken hasCommutativeMonoid) ⦄)

  module _ (struct : Struct bimonoidCode c ℓ) where
    open Struct struct

    semiring : ⦃ hasSemiring : Hasₚ isSemiring ⦄ → Semiring c ℓ
    semiring ⦃ hasSemiring ⦄ = record
      { isSemiring = record
        { isSemiringWithoutAnnihilatingZero = record
          { +-isCommutativeMonoid = +-CM.isCommutativeMonoid
          ; *-isMonoid = *-M.isMonoid
          ; distrib = from hasSemiring (* ⟨ distributesOverˡ ⟩ₚ +),
                      from hasSemiring (* ⟨ distributesOverʳ ⟩ₚ +)
          }
        ; zero = from hasSemiring (0# is leftZero for *) ,
                 from hasSemiring (0# is rightZero for *)
        }
      }
      where
      +-monoidPart : Struct monoidCode c ℓ
      +-monoidPart = substruct +-monoid⊂bimonoid

      *-monoidPart : Struct monoidCode c ℓ
      *-monoidPart = substruct *-monoid⊂bimonoid

      module +-CM = CommutativeMonoid (commutativeMonoid +-monoidPart ⦃ toSubstruct +-monoid⊂bimonoid (weaken hasSemiring) ⦄)
      module *-M = Monoid (monoid *-monoidPart ⦃ toSubstruct *-monoid⊂bimonoid (weaken hasSemiring) ⦄)


text:
-- MIT License

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

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

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

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

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

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

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

open import Function.Base using (case_of_)

open import Common

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

open import Trace message
open import SessionType message
open import Transitions message
open import HasTrace message
open import Session message
open import TraceInclusion message
open import Divergence message
open import FairCompliance message

PreConvergence : (SessionType -> SessionType -> Set) -> SessionType -> SessionType -> Set
PreConvergence rel T S =
  ∀{φ} (tφ : T HasTrace φ) (sφ : ¬ S HasTrace φ) ->
  ∃[ ψ ] ∃[ x ] (ψ ⊑ φ × ∃ λ (tψ : T HasTrace (ψ ∷ʳ O x)) ->
                         ∃ λ (sψ : S HasTrace (ψ ∷ʳ O x)) ->
                         rel (after tψ) (after sψ))

data _↓_ : SessionType -> SessionType -> Set where
  converge : ∀{T S} -> PreConvergence _↓_ T S -> T ↓ S

Convergence : SessionType -> SessionType -> Set
Convergence = PreConvergence _↓_

con-sound : ∀{T S} -> T ↓ S -> ConvergenceS T S
con-sound {T} {S} (converge C) {R} comp with fair-compliance->may-succeed comp
... | (R' # T') , reds , win#def w tdef with unzip-red* reds
... | φ , rr , tr with S HasTrace? φ
... | yes (S' , sdef , sr) = _ , zip-red* rr sr , win#def w sdef
... | no nsφ with C (_ , tdef , tr) nsφ
... | (ψ , x , prefix , tψx , sψx , con)
  with ⊑-has-co-trace prefix (_ , win->defined w , rr) | has-trace-snoc sψx
... | rψ | sψ@(_ , sdef , _) , _ with client-wins-or-accepts-prefix comp rψ tψx
... | inj₁ wψ = _ , zip-traces rψ sψ , win#def wψ sdef
... | inj₂ rψx with zip-traces rψx tψx
... | reds' with con-sound con (fair-compliance-red* comp reds')
... | (_ , reds'' , success) = _ , zip-traces rψx sψx ◅◅ reds'' , success

inclusion->convergence : ∀{T S} -> TraceInclusionS T S -> T ↓ S
inclusion->convergence sub = converge λ tφ nsφ -> ⊥-elim (nsφ (sub tφ))

not-convergence->exclusion : ∀{T S} -> ¬ T ↓ S -> ¬ TraceInclusionS T S
not-convergence->exclusion not sub = not (inclusion->convergence sub)

not-convergence+divergence : ∀{T S} -> T ↓ S -> T ↑ S -> ⊥
not-convergence+divergence (converge F) div =
  let φ = _↑_.trace div in
  let tφ = _↑_.with-trace div in
  let nsφ = _↑_.without-trace div in
  let _ , _ , pre , tψx , sψx , con' = F tφ nsφ in
  let div' = _↑_.divergence div pre tψx sψx in
  not-convergence+divergence con' div'

↓->preconv : ∀{S T} → S ↓ T → PreConvergence _↓_ S T
↓->preconv (converge x) = x

conv->defined : ∀{S T} → Defined S → S ↓ T → Defined T
conv->defined {_} {nil} inp (converge f) with f {[]} (inp _ , inp , refl) (λ x → not-nil-has-trace x)
... | _ , _ , none , _ , ht , _ = ⊥-elim (not-nil-has-trace ht)
conv->defined {_} {inp _} inp (converge _) = inp
conv->defined {_} {out _} inp (converge _) = out
conv->defined {_} {nil} out (converge f) with f {[]} (out _ , out , refl) (λ x → not-nil-has-trace x)
... | _ , _ , none , _ , ht , _ = ⊥-elim (not-nil-has-trace ht)
conv->defined {_} {inp _} out (converge _) = inp
conv->defined {_} {out _} out (converge _) = out

nil-converges : ∀{S} → nil ↓ S
nil-converges {S} = converge λ tφ _ → ⊥-elim (not-nil-has-trace tφ)

end-converges : ∀{T S} → End T → Defined S → T ↓ S
end-converges (inp e) def = converge λ tφ sφ →
  let eq = empty-inp-has-empty-trace e tφ in
  ⊥-elim (sφ (subst (λ ψ → _ HasTrace ψ) (sym eq) (_ , def , refl)))
end-converges (out e) def = converge λ tφ sφ →
  let eq = empty-out-has-empty-trace e tφ in
  ⊥-elim (sφ (subst (λ ψ → _ HasTrace ψ) (sym eq) (_ , def , refl)))

pre-conv-inp-back : ∀{f g}
  → (∀{x} → x ∈ dom f → PreConvergence _↓_ (f x .force) (g x .force))
  → PreConvergence _↓_ (inp f) (inp g)
pre-conv-inp-back _ {[]} _ no-tr = ⊥-elim (no-tr (_ , inp , refl))
pre-conv-inp-back {f} conv {I x ∷ tr} ok-tr no-tr with x ∈? f
pre-conv-inp-back {f} conv {I x ∷ tr} (_ , def , step inp red) no-tr | yes ok-x =
  let ϕ , α , (pref , (_ , d , r) , (_ , d' , r') , pr) = conv ok-x (_ , def , red) λ (_ , d , r) → no-tr (_ , d , step inp r) in
  I x ∷ ϕ , α , some pref , (_ , d , step inp r) , (_ , d' , step inp r') , pr
pre-conv-inp-back {f} conv {I x ∷ tr} ok-tr no-tr | no no-x = ⊥-elim (no-x (inp-hastrace->defined ok-tr))
pre-conv-inp-back _ {O _ ∷ _} (_ , _ , step () _) _

ext: agda

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module TestsTransport where

open import Function
open import Data.Product
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning

open import Isomorphisms
open import Tests

Foo : (A : Set) → (T : Testable A) →
      (x y : A) → (φ : Test T) → Set
Foo A T x y ⊤ =
  _⊨_ {A} {T} x ⊤ ≡ _⊨_ {A} {T} y ⊤
Foo A T x y ⊥ =
  _⊨_ {A} {T} x ⊥ ≡ _⊨_ {A} {T} y ⊥
Foo A T x y (nonTriv nt) = sat≡ (kind T) (subT nt) (obs T)
  where
    sat≡ : (k : Kind) → SubTests T k → (A → ObsTy (index T) (parts T) k) → Set
    sat≡ ind φs o =
      cotuple (λ i y → y ⊨ app φs i) (o x)
      ≡ cotuple (λ i y → y ⊨ app φs i) (o y)
    sat≡ coind (i , φ) o =
      app (o x) i ⊨ φ ≡ app (o y) i ⊨ φ

-- Note: Maybe Reveal_is_ can help to match on (kind T)??

{-
≃-transport : {A B : Set} → {T : Testable A} → (I : Iso A B) →
              (x y : A) → x ≃〈 T 〉 y →
              (Iso.iso I x) ≃〈 iso-testable T I 〉 (Iso.iso I y)
≃-transport {A} {B} {T₁} I x y p = record { eqProof = q }
    where
    T₂ =  iso-testable T₁ I
    f : A → B
    f = Iso.iso I
    g : B → A
    g = IsIso.inv (Iso.indeedIso I)
    o₁ = obs T₁
    o₂ = obs T₂
    lem : (a : A) → (o₂ ∘ f) a ≡ o₁ a
    lem a =
      begin
        (o₂ ∘ f) a
      ≡⟨ refl ⟩
        (o₁ ∘ g ∘ f) a
      ≡⟨ cong (λ x₁ → o₁ x₁) (IsIso.isLeftInv (Iso.indeedIso I) a) ⟩
        o₁ a
      ∎
    q : (φ : Test T₂) → f x ⊨ φ ≡ f y ⊨ φ
    q ⊤ = refl
    q ⊥ = refl
    q (nonTriv (nonTrivTest t)) =
      begin
        sat (kind T₂) t (o₂ (f x))
      ≡⟨ cong (λ u → sat (kind T₂) t u) (lem x) ⟩
        sat (kind T₂) t (o₁ x)
      ≡⟨ sat≡ (index T₁) (parts T₁) (kind T₁)
              o₂ (obsIso T₂) (partsTestable T₁) o₁ (obsIso T₁) lem p t ⟩
        sat (kind T₂) t (o₁ y)
      ≡⟨ cong (λ u → sat (kind T₂) t u) (sym $ lem y) ⟩
        sat (kind T₂) t (o₂ (f y))
      ∎
      where
        -- Agda complains at this point that
        -- T₁ != record { index = index T₁ ; parts = parts T₁ ; kind = kind T₁
        --              ; obs = obs T₁ ; obsIso = obsIso T₁
        --              ; partsTestable = partsTestable T₁}
        -- ...
        -- Is it possible to circumvent this issue?

        sat≡ : (Idx : Set) → (P : Idx → Set) → (k : Kind) →
               (o₂ : B → ObsTy Idx P k) → (isoT₂ : IsIso o₂) →
               (pTestable : (i : Idx) → Testable (P i)) →
               (o₁ : A → ObsTy Idx P k) → (isoT₁ : IsIso o₁) →
               ((a : A) → (o₂ ∘ f) a ≡ o₁ a) →
               x ≃〈 record
                  { index = Idx
                  ; parts = P
                  ; kind = k
                  ; obs = o₁
                  ; obsIso = isoT₁
                  ; partsTestable = pTestable
                  } 〉 y →
               (t' : SubTests
                     ( record
                      { index = Idx ; parts = P ; kind = k ; obs = o₂
                      ; obsIso = isoT₂ ; partsTestable = pTestable }) k ) →
               sat k t' (o₁ x) ≡ sat k t' (o₁ y)
        sat≡ = {!!}
-}

{-
≃-transport {A} {B} {T₁} I x y p =
  q (index T₁) (parts T₁) (kind T₁) (obs T₂) (obsIso T₂) (partsTestable T₁)
    (obs T₁) (obsIso T₁) lem {!!}
    -- Agda complains at this point that
    -- T₁ != record { index = index T₁ ; parts = parts T₁ ; kind = kind T₁
    --              ; obs = obs T₁ ; obsIso = obsIso T₁
    --              ; partsTestable = partsTestable T₁}
    -- ...
    -- Is it possible to circumvent this issue?
  where
    T₂ =  iso-testable T₁ I
    f : A → B
    f = Iso.iso I
    g : B → A
    g = IsIso.inv (Iso.indeedIso I)
    o₁ = obs T₁
    o₂ = obs T₂
    lem : (a : A) → (o₂ ∘ f) a ≡ o₁ a
    lem a =
      begin
        (o₂ ∘ f) a
      ≡⟨ refl ⟩
        (o₁ ∘ g ∘ f) a
      ≡⟨ cong (λ x₁ → o₁ x₁) (IsIso.isLeftInv (Iso.indeedIso I) a) ⟩
        o₁ a
      ∎

    q : (Idx : Set) → (P : Idx → Set) → (k : Kind) →
        (o₂ : B → ObsTy Idx P k) → (isoT₂ : IsIso o₂) →
        (pTestable : (i : Idx) → Testable (P i)) →
        (o₁ : A → ObsTy Idx P k) → (isoT₁ : IsIso o₁) →
        ((a : A) → (o₂ ∘ f) a ≡ o₁ a) →
        x ≃〈 record
                  { index = Idx
                  ; parts = P
                  ; kind = k
                  ; obs = o₁
                  ; obsIso = isoT₁
                  ; partsTestable = pTestable
                  } 〉 y →
        f x ≃〈 record
                  { index = Idx
                  ; parts = P
                  ; kind = k
                  ; obs = o₂
                  ; obsIso = isoT₂
                  ; partsTestable = pTestable
                  } 〉
        f y
    q Idx P ind o₂ isoT₂ pTestable o₁ isoT₁ lem p = record { eqProof = qi }
      where
        T₁' = record
          { index = Idx ; parts = P ; kind = ind
          ; obs = o₁ ; obsIso = isoT₁ ; partsTestable = pTestable }
        T₂' = record
          { index = Idx ; parts = P ; kind = ind
          ; obs = o₂ ; obsIso = isoT₂ ; partsTestable = pTestable }
        qi : (φ : Test T₂') → f x ⊨ φ ≡ f y ⊨ φ
        qi ⊤ = refl
        qi ⊥ = refl
        qi (nonTriv (nonTrivTest φs)) =
          begin
            cotuple (λ i z → z ⊨ app φs i) (o₂ (f x))
          ≡⟨ cong (λ u → cotuple (λ i z → z ⊨ app φs i) u) (lem x) ⟩
            cotuple (λ i z → z ⊨ app φs i) (o₁ x)
          ≡⟨ refl ⟩
            _⊨_ {A} {T₁'} x (nonTriv (nonTrivTest φs))
          ≡⟨ eqProof p (nonTriv (nonTrivTest φs)) ⟩
            _⊨_ {A} {T₁'} y (nonTriv (nonTrivTest φs))
          ≡⟨ refl ⟩
            cotuple (λ i z → z ⊨ app φs i) (o₁ y)
          ≡⟨ cong (λ u → cotuple (λ i z → z ⊨ app φs i) u) (sym $ lem y) ⟩
            cotuple (λ i z → z ⊨ app φs i) (o₂ (f y))
          ∎
    q Idx P coind o₂ isoT₂ pTestable o₁ isoT₁ lem p = record { eqProof = qc }
      where
        T₁' = record
          { index = Idx ; parts = P ; kind = coind
          ; obs = o₁ ; obsIso = isoT₁ ; partsTestable = pTestable }
        T₂' = record
          { index = Idx ; parts = P ; kind = coind
          ; obs = o₂ ; obsIso = isoT₂ ; partsTestable = pTestable }
        qc : (φ : Test T₂') → f x ⊨ φ ≡ f y ⊨ φ
        qc ⊤ = refl
        qc ⊥ = refl
        qc (nonTriv (nonTrivTest (i , φ))) =
          begin
            app (o₂ (f x)) i ⊨ φ
          ≡⟨ cong (λ u → app u i ⊨ φ) (lem x) ⟩
            app (o₁ x) i ⊨ φ
          ≡⟨ {!!} ⟩
            app (o₁ y) i ⊨ φ
          ≡⟨ cong (λ u → app u i ⊨ φ) (sym $ lem y) ⟩
            app (o₂ (f y)) i ⊨ φ
          ∎
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------------
-- Exclusive disjunction theorems
------------------------------------------------------------------------------

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

module FOL.ExclusiveDisjunction.TheoremsI where

-- The theorems below are valid on intuitionistic logic and with an
-- empty domain.
open import FOL.Base hiding ( D≢∅ ; pem )
open import FOL.ExclusiveDisjunction.Base

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

p⊻q→p→¬q : {P Q : Set} → P ⊻ Q → P → ¬ Q
p⊻q→p→¬q (inj₁ _ , h) p q = h (p , q)
p⊻q→p→¬q (inj₂ _ , h) p q = h (p , q)

p⊻q→q→¬p : {P Q : Set} → P ⊻ Q → Q → ¬ P
p⊻q→q→¬p (inj₁ _ , h) q p = h (p , q)
p⊻q→q→¬p (inj₂ _ , h) q p = h (p , q)

p⊻q→¬p→q : {P Q : Set} → P ⊻ Q → ¬ P → Q
p⊻q→¬p→q (inj₁ p , _) ¬p = ⊥-elim (¬p p)
p⊻q→¬p→q (inj₂ q , _) _  = q

p⊻q→¬q→p : {P Q : Set} → P ⊻ Q → ¬ Q → P
p⊻q→¬q→p (inj₁ p , _) ¬q = p
p⊻q→¬q→p (inj₂ q , _) ¬q = ⊥-elim (¬q q)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Structures.VectorSpace
  {k ℓᵏ} (K : Field k ℓᵏ)
  where

open import Algebra.FunctionProperties
open import Relation.Binary using (Rel)
open import Level using (_⊔_)
open import Data.Nat using (ℕ)

module VectorSpaceField where
    open Field K public
      using ()
      renaming
      ( Carrier       to K'
      ; _≈_           to _≈ᵏ_
      ; refl          to ≈ᵏ-refl
      ; sym           to ≈ᵏ-sym
      ; trans         to ≈ᵏ-trans
      ; reflexive     to ≈ᵏ-reflexive
      ; isEquivalence to ≈ᵏ-isEquiv
      ; setoid        to K-setoid
      ; _+_           to _+ᵏ_
      ; _*_           to _*ᵏ_
      ; _-_           to _-ᵏ_
      ; 0#            to 0ᵏ
      ; 1#            to 1ᵏ
      ; -_            to -ᵏ_
      ; _⁻¹            to _⁻¹ᵏ
      ; +-cong        to +ᵏ-cong
      ; +-identity    to +ᵏ-identity
      ; +-identityˡ    to +ᵏ-identityˡ
      ; +-identityʳ    to +ᵏ-identityʳ
      ; +-assoc       to +ᵏ-assoc
      ; +-comm        to +ᵏ-comm
      ; *-cong        to *ᵏ-cong
      ; *-identity    to *ᵏ-identity
      ; *-identityˡ    to *ᵏ-identityˡ
      ; *-identityʳ    to *ᵏ-identityʳ
      ; *-assoc       to *ᵏ-assoc
      ; *-comm        to *ᵏ-comm
      ; zero          to *ᵏ-zero
      ; zeroˡ          to *ᵏ-zeroˡ
      ; zeroʳ          to *ᵏ-zeroʳ
      ; distrib       to *ᵏ-+ᵏ-distrib
      ; distribˡ      to *ᵏ-+ᵏ-distribˡ
      ; distribʳ      to *ᵏ-+ᵏ-distribʳ
      ; -‿distribˡ-*  to -ᵏ‿distribˡ-*ᵏ
      ; -‿distribʳ-*  to -ᵏ‿distribʳ-*ᵏ
      ; -‿cong       to -ᵏ‿cong
      ; -‿inverse    to -ᵏ‿inverse
      ; -‿inverseˡ    to -ᵏ‿inverseˡ
      ; -‿inverseʳ    to -ᵏ‿inverseʳ
      ; uniqueˡ-⁻¹     to uniqueˡ-⁻¹ᵏ
      ; uniqueʳ-⁻¹     to uniqueʳ-⁻¹ᵏ
      ; _⁻¹-inverse    to _⁻¹ᵏ-inverse
      ; _⁻¹-involutive to _⁻¹ᵏ-involutive
      ; 0#-not-1#     to 0ᵏ-not-1ᵏ
      )

module _
  {v ℓ} {V : Set v}
  (_≈_ : Rel V ℓ)
  where

  open VectorSpaceField

  open import Algebra.Structures _≈_

  record IsVectorSpace (_+_ : Op₂ V) (_∙_ : K' → V → V) (-_ : Op₁ V) (0# : V) : Set (v ⊔ k ⊔ ℓ ⊔ ℓᵏ) where
    field
      isAbelianGroup : IsAbelianGroup _+_ 0# -_
      *ᵏ-∙-compat    : ∀ (a b : K') (u : V) -> ((a *ᵏ b) ∙ u) ≈ (a ∙ (b ∙ u))
      ∙-+-distrib    : ∀ (a : K') (u v : V) -> (a ∙ (u + v)) ≈ ((a ∙ u) + (a ∙ v))
      ∙-+ᵏ-distrib   : ∀ (a b : K') (u : V) -> ((a +ᵏ b) ∙ u) ≈ ((a ∙ u) + (b ∙ u))
      ∙-cong         : ∀ {a b : K'} {u v : V} -> a ≈ᵏ b -> u ≈ v -> (a ∙ u) ≈ (b ∙ v)
      ∙-identity     : ∀ (x : V) → (1ᵏ ∙ x) ≈ x
      ∙-absorbˡ       : ∀ (x : V) → (0ᵏ ∙ x) ≈ 0#

    open IsAbelianGroup isAbelianGroup public
      renaming
      ( assoc     to +-assoc
      ; ∙-cong    to +-cong
      ; identity  to +-identity
      ; identityˡ  to +-identityˡ
      ; identityʳ  to +-identityʳ
      ; comm      to +-comm
      ; inverse   to -‿inverse
      ; inverseˡ   to -‿inverseˡ
      ; inverseʳ   to -‿inverseʳ
      ; ⁻¹-cong    to -‿cong
      )

    open import Algebra.Properties.AbelianGroup (record { isAbelianGroup = isAbelianGroup }) public
      renaming
      ( ε⁻¹≈ε            to -0≈0
      ; ∙-cancelˡ        to +-cancelˡ
      ; ∙-cancelʳ        to +-cancelʳ
      ; ∙-cancel        to +-cancel
      ; identityˡ-unique to +-identityˡ-unique
      ; identityʳ-unique to +-identityʳ-unique
      ; identity-unique to +-identity-unique
      ; inverseˡ-unique  to +-inverseˡ-unique
      ; inverseʳ-unique  to +-inverseʳ-unique
      ; xyx⁻¹≈y          to x+y-x≈y
      ; ⁻¹-∙-comm        to -‿+-comm
      )

    open import Relation.Binary.EqReasoning setoid

    ∙-absorbʳ : ∀ (a : K') -> (a ∙ 0#) ≈ 0#
    ∙-absorbʳ a =
      begin
        a ∙ 0#
      ≈⟨ trans (∙-cong ≈ᵏ-refl (sym (∙-absorbˡ 0#))) (sym (*ᵏ-∙-compat a 0ᵏ 0#))  ⟩
        (a *ᵏ 0ᵏ) ∙ 0#
      ≈⟨ ∙-cong (*ᵏ-zeroʳ a) refl ⟩
        0ᵏ ∙ 0#
      ≈⟨ ∙-absorbˡ 0# ⟩
        0#
      ∎

    ∙-∙-comm : ∀ (a b : K') (u : V) -> (a ∙ (b ∙ u)) ≈ (b ∙ (a ∙ u))
    ∙-∙-comm a b u =
      begin
        a ∙ (b ∙ u)
      ≈⟨ sym (*ᵏ-∙-compat a b u) ⟩
        (a *ᵏ b) ∙ u
      ≈⟨ ∙-cong (*ᵏ-comm a b) refl ⟩
        (b *ᵏ a) ∙ u
      ≈⟨ *ᵏ-∙-compat b a u ⟩
        b ∙ (a ∙ u)
      ∎

    private
      lemma-inverseʳ : ∀ (u : V) -> (u + ((-ᵏ 1ᵏ) ∙ u)) ≈ 0#
      lemma-inverseʳ u =
        begin
          u + ((-ᵏ 1ᵏ) ∙ u)
        ≈⟨ +-cong (sym (∙-identity u)) refl ⟩
          (1ᵏ ∙ u) + ((-ᵏ 1ᵏ) ∙ u)
        ≈⟨ sym (∙-+ᵏ-distrib 1ᵏ (-ᵏ 1ᵏ) u) ⟩
          (1ᵏ +ᵏ (-ᵏ 1ᵏ)) ∙ u
        ≈⟨ ∙-cong (-ᵏ‿inverseʳ 1ᵏ) refl ⟩
          0ᵏ ∙ u
        ≈⟨ ∙-absorbˡ u ⟩
          0#
        ∎

    -1∙u≈-u : ∀ (u : V) -> ((-ᵏ 1ᵏ) ∙ u) ≈ (- u)
    -1∙u≈-u u =
      begin
        ((-ᵏ 1ᵏ) ∙ u)
      ≈⟨ +-inverseʳ-unique u ((-ᵏ 1ᵏ) ∙ u) (lemma-inverseʳ u) ⟩
        - u
      ∎

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
-- Andreas, 2016-06-21 fixed context for a debug message

{-# OPTIONS -v tc.section:10 #-} -- KEEP! to print debug message

module _ {A : Set} where

postulate B : Set

module M {A : Set} where

-- Intentional crash:

fail : Set
fail = Set

-- Expected debug printout:

-- checking section Issue2018debug {A = A₁ : Set}
--     actual tele: {A : Set}
-- checking section M {A = A₁ : Set}
--     actual tele: {A : Set} {A₁ : Set}
--
-- The last "actual tele" hints to a problem: Agda has renamed the second parameter!

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module hello-agda where

open import IO using (run; putStrLn)
import Agda.Builtin.IO as Builtin using (IO)
open import Data.Unit.Polymorphic.Base using (⊤)
open import Agda.Primitive using (lzero)

main : Builtin.IO {lzero} ⊤
main = run (putStrLn "Hello, Agda!")

max_stars_repo_name: neosimsim/myenv

max_issues_repo_name: neosimsim/myenv

max_forks_repo_name: neosimsim/myenv


text:
module lambda.hw7 where

open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Data.Nat
open import Data.Fin hiding (lift)

open import lambda.untyped
open import lambda.vec
open import lambda.system-f renaming (⊢_∶_ to ⊢F_∶_; type to typeF)
                            hiding (subst; ↑; lift; subst₁)
open import lambda.system-d renaming (⊢_∶_ to ⊢D_∶_; type to typeD;
  _⊢_∶_ to _⊢D_∶_; context to contextD)

-- Peio BORTHELLE -- Homework 7

-- Maybe it's a bit unusual to present things like this, we didn't do any Agda
-- but it would really have been more hassle formalizing the homework in Coq.
-- So here it is, there are some utilities in the other files and also some
-- bonus simply-typed lambda calculus. It was a bit more fun for me than to
-- write again some long derivation tree with no guarantee at all that there
-- isn't a stupid mistake kicking in. I tried to get the notations close to
-- what we had in the lesson, hope this doesn't look too alien.

-- Utilities
A B C : typeD
A = base 0
B = base 1
C = base 1

V₀ : ∀ {n} → typeF (suc n)
V₀ = var zero

V₁ : ∀ {n} → typeF (suc (suc n))
V₁ = var (suc zero)

module Q₁ where
  -- Source terms
  t₁ t₂ t₃ t₄ : term 0
  t₁ = lam (app (var zero) (var zero))
  t₂ = app t₁ (lam (var zero))
  t₃ = app t₁ t₁
  t₄ = lam (lam (app (var (suc zero)) (app (var zero) (var (suc zero)))))

  -- a) system F
  F₁ F₂ F₄ : typeF 0
  F₁ = (∀' V₀ ⇒ V₀) ⇒ (∀' V₀ ⇒ V₀)
  F₂ = ∀' V₀ ⇒ V₀
  F₄ = ∀' ∀' (V₀ ⇒ V₁) ⇒ ((V₀ ⇒ V₁) ⇒ V₀) ⇒ V₁

  F₁-p : ⊢F t₁ ∶ F₁
  F₁-p = lam (∀' V₀ ⇒ V₀) (app (sub (∀' V₀ ⇒ V₀) ax) ax)

  F₂-p : ⊢F t₂ ∶ F₂
  F₂-p = app (lam (∀' V₀ ⇒ V₀) (app (sub (∀' V₀ ⇒ V₀) ax) ax)) (gen (lam V₀ ax))

  -- t₃ is not normalizing: it has a non-trivial beta-reduction to itself.
  -- Because system F is strongly normalizing this prooves that it has no valid
  -- typing judgment.
  t₃-no-norm : t₃ β* t₃
  t₃-no-norm = β-beta ← ε

  F₄-p : ⊢F t₄ ∶ F₄
  F₄-p = gen (gen (lam (V₀ ⇒ V₁) (lam ((V₀ ⇒ V₁) ⇒ V₀) (app ax (app ax ax)))))

  -- b) system D
  σ₁ σ₂ σ₄ : typeD
  σ₁ = (A ∧ A ⇒ B) ⇒ B
  σ₂ = A ⇒ A
  σ₄ = (A ⇒ B) ⇒ ((A ⇒ B) ⇒ A) ⇒ B

  σ₁-p : ⊢D t₁ ∶ σ₁
  σ₁-p = lam (app (∧ᵉʳ ax) (∧ᵉˡ ax))

  σ₂-p : ⊢D t₂ ∶ σ₂
  σ₂-p = app (lam (app (∧ᵉʳ ax) (∧ᵉˡ ax))) (∧ⁱ (lam ax) (lam ax))

  -- Same as system F for t₃ because of the strongly normalizing property.

  σ₄-p : ⊢D t₄ ∶ σ₄
  σ₄-p = lam (lam (app ax (app ax ax)))

module Q₂ where
  --
  σ₁ σ₂ σ₃ σ₄ : typeD
  σ₁ = ((A ∧ B) ⇒ C) ⇒ A ⇒ B ⇒ C
  σ₂ = (A ⇒ B ⇒ C) ⇒ (A ∧ B) ⇒ C
  σ₃ = (C ⇒ A ∧ C ⇒ B) ⇒ C ⇒ (A ∧ B)
  σ₄ = C ⇒ (A ∧ B) ⇒ (C ⇒ A ∧ C ⇒ B)

  σ₁-p : ∀ {t} → ¬ ⊢D t ∶ σ₁
  σ₁-p p = {!!}

  σ₂-p : ⊢D lam (lam (app (app (var (suc zero)) (var zero)) (var zero))) ∶ σ₂
  σ₂-p = lam (lam (app (app ax (∧ᵉˡ ax)) (∧ᵉʳ ax)))

  σ₃-p : ⊢D lam (lam (app (var (suc zero)) (var zero))) ∶ σ₃
  σ₃-p = lam (lam (∧ⁱ (app (∧ᵉˡ ax) ax) (app (∧ᵉʳ ax) ax)))

  σ₄-p : ⊢D lam (lam (lam (var (suc zero)))) ∶ σ₄
  σ₄-p = lam (lam (∧ⁱ (lam (∧ᵉˡ ax)) (lam (∧ᵉʳ ax))))

module Q₃ where
  -- I got stuck on applying the substitution lemma on function type that are
  -- not lambda abstractions but ∧ eliminations. I don't manage to get from
  -- a proof of that type to a proof with the argument type on the top of the
  -- context. Maybe the substitution lemma is not well choosen.
  subj-red : ∀ {n T} → {x y : term n} → {Γ : contextD n} → Γ ⊢D x ∶ T → x →β y → Γ ⊢D y ∶ T
  subj-red ax ()
  subj-red (∧ⁱ x₁ x₂) p = ∧ⁱ (subj-red x₁ p) (subj-red x₂ p)
  subj-red (∧ᵉˡ x) p = ∧ᵉˡ (subj-red x p)
  subj-red (∧ᵉʳ x) p = ∧ᵉʳ (subj-red x p)
  subj-red (app (lam x) y) β-beta = subst-p x (λ { zero → y; (suc i) → ax })
  subj-red (app (∧ᵉˡ x) y) β-beta = {!   !}
  subj-red (app (∧ᵉʳ x) y) β-beta = {!   !}
  subj-red (app x y) (β-app₁ p) = app (subj-red x p) y
  subj-red (app x y) (β-app₂ p) = app x (subj-red y p)
  subj-red (lam x) (β-lam p) = lam (subj-red x p)

module Q₄ where
  -- The BNF grammar i use is:
  --
  --  <NF> ::= "λ" <VAR> "." <NF> | <NE>
  --  <NE> ::= <NE> <NF> | <VAR>
  --
  -- I implemented this grammar as a judgment on untyped lambda terms
  -- with the datatypes `lambda.untyped.norm` and `lambda.untyped.neut`.

  -- Proof that NF and NE don't allow further derivation
  -- This proof as well as the reciprocical were quite mechanized but still
  -- a bit cumbersome.
  nf-last : ∀ {n} → {x : term n} → norm x → ¬ ∃[ y ] (x →β y)
  ne-last : ∀ {n} → {x : term n} → neut x → ¬ ∃[ y ] (x →β y)

  nf-last (lam x) (lam y , β-lam p) = nf-last x (y , p)
  nf-last (gnd x) (lam y , p) = ne-last x (lam y , p)
  nf-last (gnd x) (var i , p) = ne-last x (var i , p)
  nf-last (gnd x) (app a b , p) = ne-last x (app a b , p)

  ne-last var (y , ())
  ne-last (app () y) (_ , β-beta)
  ne-last (app x y) (app a b , β-app₁ p) = ne-last x (a , p)
  ne-last (app x y) (app a b , β-app₂ p) = nf-last y (b , p)

  -- Proof that terms with no further derivation are in NF
  last-nf : ∀ {n} → (x : term n) → ¬ ∃[ y ] (x →β y) → norm x
  last-ne : ∀ {n y} → (x : term n) → ¬ ∃[ z ] (app x y →β z) → neut x

  last-nf (lam x) p = lam (last-nf x λ { (y , p₂) → p (lam y , β-lam p₂) })
  last-nf (var x) p = gnd var
  last-nf (app x y) p = gnd (app
    (last-ne x λ { (z , p₁) → p (z , p₁) })
    (last-nf y λ { (a , b) → p (app x a , β-app₂ b) }))

  last-ne {y = y} (lam x) p with p (subst₁ x y , β-beta)
  ...               | ()
  last-ne (var x) p = var
  last-ne {y = y} (app x z) p = app
    (last-ne x λ { (a , b) → p (app a y , β-app₁ b) })
    (last-nf z λ { (a , b) → p (app (app x a) y , (β-app₁ (β-app₂ b))) })

  const : ∀ {n} → contextD n
  const {zero} = ε
  const {suc n} = const ▸ base 0

  -- Again because i messed up the renaming/substitution on ⊢D terms, i
  -- did not get to formalize the typing properly here.
  type-n : ∀ {n} → {x : term n} → norm x → ∃ (λ Γ → ∃ (λ T → Γ ⊢D x ∶ T))
  type-e : ∀ {n} → {x : term n} → neut x → ∃ (λ Γ → ∃ (λ T → Γ ⊢D x ∶ T))

  -- Here we compute inductively on the subterm, then "unload" the top of
  -- the context A and the result type B into the type A ⇒ B.
  type-n (lam x) = {!   !}
  type-n (gnd x) = type-e x

  -- Here we create a context with fresh base types, assigning the matching
  -- one to the term.
  type-e (var {i}) = {!   !}

  -- Here we compute inductively on both subterms:
  --   Γx ⊢D x ∶ Tx    Γy ⊢D y ∶ Ty
  -- x is a neutral term so it has a type looking like
  --   T ⇒ A₁ ∧ T ⇒ A₁ ⇒ A₂ ∧ …
  -- We then simply extend it with An = Ty. This requires some proof
  -- rewriting with ∧ᵉ*.
  type-e (app x y) = {!   !}

-- Question 5
-- a) The definition of the conjunction in system F is:
--     conjⁱ : Γ ⊢F x ∶ A → Γ ⊢F y ∶ B → Γ ⊢F (x , y) ∶ A ∧F B
--     conjᵉʳ : Γ ⊢F x ∶ A ∧F B → Γ ⊢F π₀ x ∶ A
--     conjᵉˡ : Γ ⊢F x : A ∧F B → Γ ⊢F π₁ x ∶ B
--    The difference is that in system D, the conjunction is more of
--    an intersection: if a single term has 2 type judgements, then
--    it has a judgment for the intersection, whereas for system F
--    it is a couple of 2 different terms.


text:
-- {-# OPTIONS --show-implicit --show-irrelevant #-}
module Data.QuadTree.FunctorProofs.FunctorLaws where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Logic
open import Data.QuadTree.InternalAgda
open import Agda.Primitive
open import Data.QuadTree.Implementation.Functors

-- First, define the Functor laws

IdentityLaw : (f : (t : Set) -> {{ eqT : Eq t }} -> Set) -> {{ff : FunctorEq f}} -> Set₁
IdentityLaw f {{ff}} = {t : Set} -> {{ eqT : Eq t }}
  -> (v : f t) -> fmapₑ ff id v ≡ id v

CompositionLaw : (f : (t : Set) -> {{ eqT : Eq t }} -> Set) -> {{ff : FunctorEq f}} -> Set₁
CompositionLaw f {{ff}} = {a b c : Set} -> {{ eqA : Eq a }} {{ eqB : Eq b }} {{ eqC : Eq c }}
  -> (v : f a) -> (fun1 : a -> b) -> (fun2 : b -> c) -> fmapₑ ff (fun2 ∘ fun1) v ≡ fmapₑ ff fun2 (fmapₑ ff fun1 v)

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


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

module FOT.FOTC.Program.Mirror.StructurallySmaller.StructurallySmallerSL where

open import Data.List

data Tree (D : Set) : Set where
  tree : D → List (Tree D) → Tree D

foo : {D : Set} → Tree D → D
foo (tree a [])       = a
foo (tree a (t ∷ ts)) = foo (tree a ts)

bar : {D : Set} → Tree D → D
bar     (tree a [])       = a
bar {D} (tree a (t ∷ ts)) = helper (bar t) (bar (tree a ts))
  where
  postulate helper : D → D → D


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

open import lib.Basics
open import lib.NType2
open import lib.Equivalence2
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Paths
open import lib.types.TLevel
open import lib.types.Truncation

module lib.NConnected where

is-connected : ∀ {i} → ℕ₋₂ → Type i → Type i
is-connected n A = is-contr (Trunc n A)

has-conn-fibers : ∀ {i j} {A : Type i} {B : Type j} → ℕ₋₂ → (A → B) → Type (lmax i j)
has-conn-fibers {A = A} {B = B} n f =
  Π B (λ b → is-connected n (hfiber f b))

{- all types are -2-connected -}
-2-conn : ∀ {i} (A : Type i) → is-connected -2 A
-2-conn A = Trunc-level

{- all inhabited types are -1-connected -}
inhab-conn : ∀ {i} {A : Type i} (a : A) → is-connected -1 A
inhab-conn a = has-level-in ([ a ] , prop-has-all-paths [ a ])

{- connectedness is a prop -}
is-connected-is-prop : ∀ {i} {n : ℕ₋₂} {A : Type i}
  → is-prop (is-connected n A)
is-connected-is-prop = is-contr-is-prop

{- "induction principle" for n-connected maps (where codomain is n-type) -}
abstract
  pre∘-conn-is-equiv : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂}
    → {h : A → B} → has-conn-fibers n h
    → (∀ {k} (P : B → n -Type k) → is-equiv (λ (s : Π B (fst ∘ P)) → s ∘ h))
  pre∘-conn-is-equiv {A = A} {B = B} {n = n} {h = h} c P = is-eq f g f-g g-f
    where f : Π B (fst ∘ P) → Π A (fst ∘ P ∘ h)
          f k a = k (h a)

          helper : Π A (fst ∘ P ∘ h)
            → (b : B) → Trunc n (Σ A (λ a → h a == b)) → (fst (P b))
          helper t b r =
            Trunc-rec {{snd (P b)}}
              (λ x → transport (λ y → fst (P y)) (snd x) (t (fst x)))
              r

          g : Π A (fst ∘ P ∘ h) → Π B (fst ∘ P)
          g t b = helper t b (contr-center (c b))

          f-g : ∀ t → f (g t) == t
          f-g t = λ= $ λ a → transport
            (λ r →  Trunc-rec {{snd (P (h a))}} _ r == t a)
            (! (contr-path(c (h a)) [ (a , idp) ]))
            idp

          g-f : ∀ k → g (f k) == k
          g-f k = λ= $ λ (b : B) →
            Trunc-elim {{λ r → =-preserves-level {x = helper (k ∘ h) b r} (snd (P b))}}
                       (λ x → lemma (fst x) b (snd x)) (contr-center (c b))
            where
            lemma : ∀ xl → ∀ b → (p : h xl == b) →
              helper (k ∘ h) b [ (xl , p) ] == k b
            lemma xl ._ idp = idp

conn-extend : ∀ {i j k} {A : Type i} {B : Type j} {n : ℕ₋₂}
  → {h : A → B} → has-conn-fibers n h
  → (P : B → n -Type k)
  → Π A (fst ∘ P ∘ h) → Π B (fst ∘ P)
conn-extend c P f = is-equiv.g (pre∘-conn-is-equiv c P) f

conn-out = conn-extend

conn-extend-β : ∀ {i j k} {A : Type i} {B : Type j} {n : ℕ₋₂}
  {h : A → B} (c : has-conn-fibers n h)
  (P : B → n -Type k) (f : Π A (fst ∘ P ∘ h))
  → ∀ a → (conn-extend c P f (h a)) == f a
conn-extend-β c P f = app= (is-equiv.f-g (pre∘-conn-is-equiv c P) f)

{- generalized "almost induction principle" for maps into ≥n-types
   TODO: rearrange this to use ≤T?                                 -}
conn-extend-general : ∀ {i j} {A : Type i} {B : Type j} {n k : ℕ₋₂}
  → {f : A → B} → has-conn-fibers n f
  → ∀ {l} (P : B → (k +2+ n) -Type l)
  → ∀ t → has-level k (Σ (Π B (fst ∘ P)) (λ s → (s ∘ f) == t))
conn-extend-general {k = ⟨-2⟩} c P t =
  equiv-is-contr-map (pre∘-conn-is-equiv c P) t
conn-extend-general {B = B} {n = n} {k = S k'} {f = f} c P t = has-level-in
  λ {(g , p) (h , q) →
    equiv-preserves-level (e g h p q)
      {{conn-extend-general {k = k'} c (Q g h) (app= (p ∙ ! q))}} }
  where
    Q : (g h : Π B (fst ∘ P)) → B → (k' +2+ n) -Type _
    Q g h b = ((g b == h b) , has-level-apply (snd (P b)) _ _)

    app=-ap : ∀ {i j k} {A : Type i} {B : Type j} {C : B → Type k}
      (f : A → B) {g h : Π B C} (p : g == h)
      → app= (ap (λ k → k ∘ f) p) == (app= p ∘ f)
    app=-ap f idp = idp

    move-right-on-right-econv : ∀ {i} {A : Type i} {x y z : A}
      (p : x == y) (q : x == z) (r : y == z)
      → (p == q ∙ ! r) ≃ (p ∙ r == q)
    move-right-on-right-econv {x = x} p idp idp =
      (_ , pre∙-is-equiv (∙-unit-r p))

    lemma : ∀ g h p q → (H : g ∼ h)
      → ((H ∘ f) == app= (p ∙ ! q))
         ≃ (ap (λ v → v ∘ f) (λ= H) ∙ q == p)
    lemma g h p q H =
      move-right-on-right-econv (ap (λ v → v ∘ f) (λ= H)) p q
      ∘e transport (λ w → (w == app= (p ∙ ! q))
                      ≃ (ap (λ v → v ∘ f) (λ= H) == p ∙ ! q))
                   (app=-ap f (λ= H) ∙ ap (λ k → k ∘ f) (λ= $ app=-β H))
                   (ap-equiv app=-equiv _ _ ⁻¹)

    e : ∀ g h p q  →
      (Σ (g ∼ h) (λ r → (r ∘ f) == app= (p ∙ ! q)))
      ≃ ((g , p) == (h , q))
    e g h p q =
      ((=Σ-econv _ _ ∘e Σ-emap-r (λ u → ↓-app=cst-econv ∘e !-equiv))
      ∘e (Σ-emap-l _ λ=-equiv)) ∘e Σ-emap-r (lemma g h p q)

conn-in : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} {h : A → B}
  → (∀ (P : B → n -Type (lmax i j))
     → Σ (Π A (fst ∘ P ∘ h) → Π B (fst ∘ P))
         (λ u → ∀ (t : Π A (fst ∘ P ∘ h)) → u t ∘ h ∼ t))
  → has-conn-fibers n h
conn-in {A = A} {B = B} {h = h} sec b =
  let s = sec (λ b → (Trunc _ (hfiber h b) , Trunc-level))
  in has-level-in (fst s (λ a → [ a , idp ]) b ,
      Trunc-elim (λ k → transport
                   (λ v → fst s (λ a → [ a , idp ]) (fst v) == [ fst k , snd v ])
                   (contr-path (pathfrom-is-contr (h (fst k))) (b , snd k))
                   (snd s (λ a → [ a , idp ]) (fst k))))

abstract
  pointed-conn-in : ∀ {i} {n : ℕ₋₂} (A : Type i) (a₀ : A)
    → has-conn-fibers {A = ⊤} n (cst a₀) → is-connected (S n) A
  pointed-conn-in {n = n} A a₀ c = has-level-in
    ([ a₀ ] ,
     Trunc-elim
       (λ a → Trunc-rec
             (λ x → ap [_] (snd x)) (contr-center $ c a)))

abstract
  pointed-conn-out : ∀ {i} {n : ℕ₋₂} (A : Type i) (a₀ : A)
    {{_ : is-connected (S n) A}} → has-conn-fibers {A = ⊤} n (cst a₀)
  pointed-conn-out {n = n} A a₀ {{c}} a = has-level-in
    (point ,
     λ y → ! (cancel point)
           ∙ (ap out $ contr-has-all-paths (into point) (into y))
           ∙ cancel y)
    where
      into-aux : Trunc n (Σ ⊤ (λ _ → a₀ == a)) → Trunc n (a₀ == a)
      into-aux = Trunc-fmap snd

      into : Trunc n (Σ ⊤ (λ _ → a₀ == a))
        → [_] {n = S n} a₀ == [ a ]
      into = <– (Trunc=-equiv [ a₀ ] [ a ]) ∘ into-aux

      out-aux : Trunc n (a₀ == a) → Trunc n (Σ ⊤ (λ _ → a₀ == a))
      out-aux = Trunc-fmap (λ p → (tt , p))

      out : [_] {n = S n} a₀ == [ a ] → Trunc n (Σ ⊤ (λ _ → a₀ == a))
      out = out-aux ∘ –> (Trunc=-equiv [ a₀ ] [ a ])

      cancel : (x : Trunc n (Σ ⊤ (λ _ → a₀ == a))) → out (into x) == x
      cancel x =
        out (into x)
          =⟨ ap out-aux (<–-inv-r (Trunc=-equiv [ a₀ ] [ a ]) (into-aux x)) ⟩
        out-aux (into-aux x)
          =⟨ Trunc-fmap-∘ _ _ x ⟩
        Trunc-fmap (λ q → (tt , (snd q))) x
          =⟨ Trunc-elim {P = λ x → Trunc-fmap (λ q → (tt , snd q)) x == x}
               (λ _ → idp) x ⟩
        x =∎

      point : Trunc n (Σ ⊤ (λ _ → a₀ == a))
      point = out $ contr-has-all-paths [ a₀ ] [ a ]

prop-over-connected :  ∀ {i j} {A : Type i} {a : A} {{p : is-connected 0 A}}
  → (P : A → hProp j)
  → fst (P a) → Π A (fst ∘ P)
prop-over-connected P x = conn-extend (pointed-conn-out _ _) P (λ _ → x)

{- Connectedness of a truncated type -}
instance
  Trunc-preserves-conn : ∀ {i} {A : Type i} {n : ℕ₋₂} {m : ℕ₋₂}
    → is-connected n A → is-connected n (Trunc m A)
  Trunc-preserves-conn {n = ⟨-2⟩} _ = Trunc-level
  Trunc-preserves-conn {A = A} {n = S n} {m} c = lemma (contr-center c) (contr-path c)
    where
    lemma : (x₀ : Trunc (S n) A) → (∀ x → x₀ == x) → is-connected (S n) (Trunc m A)
    lemma = Trunc-elim
      (λ a → λ p → has-level-in ([ [ a ] ] ,
        Trunc-elim
          (Trunc-elim
            {{λ _ → =-preserves-level
                      (Trunc-preserves-level (S n) Trunc-level)}}
            (λ x → <– (Trunc=-equiv [ [ a ] ] [ [ x ] ])
               (Trunc-fmap (ap [_])
                 (–> (Trunc=-equiv [ a ] [ x ]) (p [ x ])))))))

{- Connectedness of a Σ-type -}
abstract
 instance
  Σ-conn : ∀ {i} {j} {A : Type i} {B : A → Type j} {n : ℕ₋₂}
    → is-connected n A → (∀ a → is-connected n (B a))
    → is-connected n (Σ A B)
  Σ-conn {A = A} {B = B} {n = ⟨-2⟩} cA cB = -2-conn (Σ A B)
  Σ-conn {A = A} {B = B} {n = S m} cA cB =
    Trunc-elim
      {P = λ ta → (∀ tx → ta == tx) → is-connected (S m) (Σ A B)}
      (λ a₀ pA →
        Trunc-elim
          {P = λ tb → (∀ ty → tb == ty) → is-connected (S m) (Σ A B)}
          (λ b₀ pB → has-level-in
            ([ a₀ , b₀ ] ,
              Trunc-elim
                {P = λ tp → [ a₀ , b₀ ] == tp}
                (λ {(r , s) →
                  Trunc-rec
                    (λ pa → Trunc-rec
                      (λ pb → ap [_] (pair= pa (from-transp! B pa pb)))
                      (–> (Trunc=-equiv [ b₀ ] [ transport! B pa s ])
                          (pB [ transport! B pa s ])))
                    (–> (Trunc=-equiv [ a₀ ] [ r ]) (pA [ r ]))})))
          (contr-center (cB a₀)) (contr-path (cB a₀)))
      (contr-center cA) (contr-path cA)

  ×-conn : ∀ {i} {j} {A : Type i} {B : Type j} {n : ℕ₋₂}
    → is-connected n A → is-connected n B
    → is-connected n (A × B)
  ×-conn cA cB = Σ-conn cA (λ _ → cB)

{- connectedness of a path space -}
abstract
 instance
  path-conn : ∀ {i} {A : Type i} {x y : A} {n : ℕ₋₂}
    → is-connected (S n) A → is-connected n (x == y)
  path-conn {x = x} {y = y} cA =
    equiv-preserves-level (Trunc=-equiv [ x ] [ y ])
      {{has-level-apply (contr-is-prop cA) [ x ] [ y ]}}

{- an n-Type which is n-connected is contractible -}
connected-at-level-is-contr : ∀ {i} {A : Type i} {n : ℕ₋₂}
  {{pA : has-level n A}} {{cA : is-connected n A}} → is-contr A
connected-at-level-is-contr {{pA}} {{cA}} =
  equiv-preserves-level (unTrunc-equiv _) {{cA}}

{- if A is n-connected and m ≤ n, then A is m-connected -}
connected-≤T : ∀ {i} {m n : ℕ₋₂} {A : Type i}
  → m ≤T n → {{_ : is-connected n A}} → is-connected m A
connected-≤T {m = m} {n = n} {A = A} leq =
  transport (λ B → is-contr B)
            (ua (Trunc-fuse A m n) ∙ ap (λ k → Trunc k A) (minT-out-l leq))
            (Trunc-preserves-level m ⟨⟩)

{- Equivalent types have the same connectedness -}
equiv-preserves-conn : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂} (e : A ≃ B)
  {{_ : is-connected n A}} → is-connected n B
equiv-preserves-conn {n = n} e = equiv-preserves-level (Trunc-emap e)

{- Composite of two connected functions is connected -}
∘-conn : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  → {n : ℕ₋₂} → (f : A → B) → (g : B → C)
  → has-conn-fibers n f
  → has-conn-fibers n g
  → has-conn-fibers n (g ∘ f)
∘-conn {n = n} f g cf cg =
  conn-in (λ P → conn-extend cg P ∘ conn-extend cf (P ∘ g) , lemma P)
    where
      lemma : ∀ P h x → conn-extend cg P (conn-extend cf (P ∘ g) h) (g (f x)) == h x
      lemma P h x =
        conn-extend cg P (conn-extend cf (P ∘ g) h) (g (f x))
          =⟨ conn-extend-β cg P (conn-extend cf (P ∘ g) h) (f x) ⟩
        conn-extend cf (P ∘ g) h (f x)
          =⟨ conn-extend-β cf (P ∘ g) h x ⟩
        h x
          =∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- {-# OPTIONS -v tc.term.exlam:100 -v extendedlambda:100 -v int2abs.reifyterm:100 #-}
-- Andreas, 2013-02-26
module Issue778 (Param : Set) where

data ⊥ : Set where

interactive : ⊥ → ⊥
interactive = λ {x → {!x!}}
  where aux : ⊥ → ⊥
        aux x = x

-- splitting did not work for extended lambda in the presence of
-- module parameters and where block

data ⊤ : Set where
  tt : ⊤

test : ⊤ → ⊤
test = λ { x → {!x!} }
  where aux : ⊤ → ⊤
        aux x = x


text:
module Shift (Gnd : Set)(U : Set)(El : U -> Set) where

open import Basics
open import Pr
open import Nom
import Kind
open Kind Gnd U El
import Cxt
open Cxt Kind
import Loc
open Loc Kind
import Term
open Term Gnd U El

popH : {D : Cxt}{M : Loc}{S T : Kind} ->
       D [ M / Head ]- T -> D [ M * S / Head ]- T
popH ( ` x -! xg )  = ` x -! xg
popH ( # v -! _ )   = # (pop v) -! _

weak : {G D : Cxt}{L M : Loc}{S : Kind} ->
       ({T : Kind} -> G [ L / Head ]- T -> D [ M / Head ]- T) ->
       {T : Kind} -> G [ L * S / Head ]- T -> D [ M * S / Head ]- T
weak rho (` x -! p )        = popH (rho (` x -! p))
weak rho (# top -! _ )      = # top -! _
weak rho (# (pop v) -! _ )  = popH (rho (# v -! _))

shift : {G D : Cxt}{L M : Loc} ->
  ({T : Kind} -> G [ L / Head ]- T -> D [ M / Head ]- T) ->
  {j : Jud}{T : Kind} -> G [ L / j ]- T  ->  D [ M / j ]- T
shift {G} {D} rho (t -! tg) = chug rho t tg where
  chug : {j : Jud}{L M : Loc} ->
    ({T : Kind} -> G [ L / Head ]- T -> D [ M / Head ]- T) ->
    {T : Kind}(t : L [ j ]- T) -> [| Good G t |] ->  D [ M / j ]- T
  chug {Head} rho h hg = rho ( h -! hg )
  chug rho [ s ] sg = G[ chug rho s sg ]
  chug rho (fn A f) fg = Gfn A (\ a -> chug rho (f a) (fg a))
  chug rho (\\ b) bg = G\\ (chug (weak rho) b bg)
  chug rho (a ^ s) sg = a G^ chug rho s sg
  chug rho (r & s) rsg = chug rho r (fst rsg) G& chug rho s (snd rsg)
  chug rho nil _ = Gnil
  chug rho (h $ s) hsg = chug rho h (fst hsg) G$ chug rho s (snd hsg)

bind : {G : Cxt}(x : Nom){Gx : [| G Hasn't x |]}{S : Kind}{j : Jud}{T : Kind} ->
       (G [ x - S ]) {Gx} [ EL / j ]- T -> G [ EL * S / j ]- T
bind {G} x {Gx}{S} = shift topx where
  topx : {T : Kind} -> (G [ x - S ]) {Gx} [ EL / Head ]- T ->
         G [ EL * S / Head ]- T
  topx (` y -! yg) with nomEq x y
  topx (` .x -! refl) | yes refl = # top -! _
  topx (` y -! yg)    | no _     = ` y -! yg
  topx (# () -! _)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2015-03-16

open import Common.Size
open import Common.Prelude

-- Note: the assumption of pred is absurd,
-- but still should not make Agda loop.

module _ (pred : ∀ i → Size< i) where

data D (i : Size) : Set where
  wrap : (j : Size< i) → D i

loop : ∀ i → D i → ⊥
loop i (wrap j) = loop j (wrap (pred j))
-- Loops during injectivity check

d : ∀ i → D i
d i = wrap (pred i)

absurd : ⊥
absurd = FIXME loop ∞ (d ∞)

-- Testcase temporarily mutilated, original error:
-- -Issue1428a.agda:9,20-31
-- -Functions may not return sizes, thus, function type
-- -(i : Size) → Size< i is illegal
-- -when checking that the expression ∀ i → Size< i is a type
-- +Issue1428a.agda:22,10-15
-- +Not in scope:
-- +  FIXME at Issue1428a.agda:22,10-15
-- +when scope checking FIXME

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

-- | Exclusive option for predicates
module Dodo.Unary.XOpt where

-- Stdlib imports
open import Level using (Level)
open import Relation.Unary using (Pred)
-- Local imports
open import Dodo.Nullary.XOpt

-- # XOpt₂

XOptPred₂ : {a ℓ₁ ℓ₂ : Level} {A : Set a} → Pred A ℓ₁ → Pred A ℓ₂ → Set _
XOptPred₂ {A = A} P Q = ∀ (x : A) → XOpt₂ (P x) (Q x)

-- # XOpt₃

XOptPred₃ : {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} → Pred A ℓ₁ → Pred A ℓ₂ → Pred A ℓ₃ → Set _
XOptPred₃ {A = A} P Q R = ∀ (x : A) → XOpt₃ (P x) (Q x) (R x)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

module Math.NumberTheory.Product.Nat.Properties where

open import Data.Nat.Properties
open import Math.NumberTheory.Product.Generic.Properties

-- TODO rename _≈_ to _≡_
open CommutativeMonoidProductProperties *-1-commutativeMonoid public


text:
open import Prelude hiding (id; Bool)

module Examples.Unification where

data TC : Set where
  tc-int : TC
  tc-bool : TC

_tc≟_ : (a b : TC) → Dec (a ≡ b)
tc-int tc≟ tc-int = yes refl
tc-int tc≟ tc-bool = no (λ ())
tc-bool tc≟ tc-int = no (λ ())
tc-bool tc≟ tc-bool = yes refl

open import Implicits.Oliveira.Types TC _tc≟_
open import Implicits.Oliveira.Terms TC _tc≟_
open import Implicits.Oliveira.Contexts TC _tc≟_
open import Implicits.Oliveira.WellTyped TC _tc≟_
open import Implicits.Oliveira.Substitutions TC _tc≟_
open import Implicits.Oliveira.Types.Unification TC _tc≟_
open import Implicits.Oliveira.Types.Unification.McBride TC _tc≟_ as McBride using ()
open import Data.Star as S
open import Data.Maybe

open import Level using () renaming (zero to level₀)
open import Data.Maybe using (monad; functor)
open import Category.Functor
open RawFunctor {level₀} functor

module M = MetaTypeMetaSubst
module T = MetaTypeTypeSubst

Bool : ∀ {n} → Type n
Bool = simpl (tc tc-bool)

Int : ∀ {n} → Type n
Int = simpl (tc tc-int)

module ex₂ where
  -- mgu test for simple 2 variable substitution

  a : MetaType (suc (suc zero)) (suc zero)
  a = open-meta $ open-meta $ to-meta $ (simpl ((simpl (tvar zero)) →' (simpl (simpl (tvar (suc zero)) →' simpl (tvar (suc (suc zero)))))))

  b : SimpleType (suc zero)
  b = Int →' (simpl (Int →' simpl (tvar zero)))

  s = mgu a b

  u = asub (proj₁ $ from-just s)

  unifies : a M./ u ≡ (simpl (to-smeta b))
  unifies = refl

module ex₃ where
  -- mgu test for simple 1 variable substitution
  -- (limited α)

  a : MetaType (suc zero) (suc zero)
  a = open-meta (to-meta (∀' (simpl ((simpl (tvar zero)) →' simpl (tvar (suc zero))))))

  b : SimpleType (suc zero)
  b = Int →' Int

  s : mgu a b ≡ nothing
  s = refl

module ex₄ where
  -- with ∀' in there somewhere

  a : MetaType (suc zero) (suc zero)
  a = simpl ((∀' (s-mvar zero)) →' (s-tc tc-int))

  -- won't unify with a because we'd need to instantiate s-mvar zero with
  -- a s-tvar that's not yet introduced
  b : SimpleType (suc zero)
  b = (∀' (simpl (tvar zero))) →' Int

  s : mgu a b ≡ nothing
  s = refl

module ex₅ where
  -- renaming example

  a : MetaType (suc (suc zero)) (suc zero)
  a = (s-mvar zero) ⇒ (s-mvar (suc zero))

  b : Type (suc zero)
  b = (simpl (tvar (zero))) ⇒ (simpl (tvar zero))

  s : is-just (McBride.mgu a b) ≡ true
  s = refl

open ex₅


text:
{-# OPTIONS --cubical-compatible #-}
-- {-# OPTIONS -v tc.data:100 #-}
module Issue865Big where

data _≡_ (A : Set) : Set → Set₁ where
  refl : A ≡ A

K : {A : Set} (P : A ≡ A → Set) → P refl → (p : A ≡ A) → P p
K P h refl = h


text:
------------------------------------------------------------------------
-- agda-combinatorics
-- All modules
------------------------------------------------------------------------

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

module AgdaCombinatoricsEverything where

import Math.BinomialTheorem.Generic

-- Proof of the binomial theorem
import Math.BinomialTheorem.Nat

-- Definitions of combinatorial functions
import Math.Combinatorics.Function

-- Properties of combinatorial functions
import Math.Combinatorics.Function.Properties

-- Definitions of combinatorial functions on integer
import Math.Combinatorics.IntegerFunction

-- Properties of combinatorial functions on integer
import Math.Combinatorics.IntegerFunction.Properties

import Math.Combinatorics.ListFunction

import Math.Combinatorics.ListFunction.Properties

import Math.Combinatorics.VecFunction


text:
module Cats.Category.Constructions.Equalizer where

open import Level

open import Cats.Category.Base
open import Cats.Util.Conv

import Cats.Category.Constructions.Mono as Mono
import Cats.Category.Constructions.Unique as Unique

module Build {lo la l≈} (Cat : Category lo la l≈) where

  private open module Cat = Category Cat
  open Cat.≈-Reasoning
  open Mono.Build Cat
  open Unique.Build Cat

  record IsEqualizer {A B} (f g : A ⇒ B) {E} (e : E ⇒ A)
    : Set (lo ⊔ la ⊔ l≈)
    where
    field
      equalizes : f ∘ e ≈ g ∘ e
      universal : ∀ {Z} (z : Z ⇒ A)
        → f ∘ z ≈ g ∘ z
        → ∃![ u ] (e ∘ u ≈ z)

  record Equalizer {A B} (f g : A ⇒ B) : Set (lo ⊔ la ⊔ l≈) where
    field
      {E} : Obj
      e : E ⇒ A
      isEqualizer : IsEqualizer f g e

    open IsEqualizer isEqualizer public

  instance
    HasObj-Equalizer : ∀ {A B} {f g : A ⇒ B}
      → HasObj (Equalizer f g) lo la l≈
    HasObj-Equalizer = record { Cat = Cat ; _ᴼ = Equalizer.E }

    HasArrow-Equalizer : ∀ {A B} {f g : A ⇒ B}
      → HasArrow (Equalizer f g) lo la l≈
    HasArrow-Equalizer = record { Cat = Cat ; _⃗ = Equalizer.e }

  equalizer→mono : ∀ {A B} {f g : A ⇒ B} {E} {e : E ⇒ A}
    → IsEqualizer f g e
    → IsMono e
  equalizer→mono {f = f} {g} {E} {e} eql {Z} {i} {j} e∘i≈e∘j
      = ∃!→≈ (universal (e ∘ j) lemma) e∘i≈e∘j ≈.refl
    where
      open IsEqualizer eql

      lemma : f ∘ e ∘ j ≈ g ∘ e ∘ j
      lemma
          = begin
              f ∘ e ∘ j
            ≈⟨ unassoc ⟩
              (f ∘ e) ∘ j
            ≈⟨ ∘-resp-l equalizes ⟩
              (g ∘ e) ∘ j
            ≈⟨ assoc ⟩
              g ∘ e ∘ j
            ∎

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module DenotCommutes where

open import Prelude
open import T

---- Proof that dynamic semantics commute with denotational semantics

module DenotCommutes where

  -- Proving that the dynamic semantics and the denotational semantics
  -- commute (at least if we are using regular equality as our
  -- equality for interpreted terms) basically requires
  -- extensionality, since we need to show that things at function
  -- type are equal.
  postulate iext : {A : Set}{B : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B a} →
                   (∀ a → f {a} ≡ g {a}) →
                   _≡_ { A = {a : A} → B a} f g

  postulate ext : {A : Set}{B : A → Set}{f : ∀ a → B a}{g : ∀ a → B a} →
                  (∀ a → f a ≡ g a) → f ≡ g

  -- Show that renaming and substitution commute with denotational semantics
  -- in the appropriate sense. This mirrors a bunch of the machinery in SubstTheory.

  -- Some equality related stuff

  Meaning≡ : ∀ {Γ}(f g : meaningη Γ) → Set
  Meaning≡ f g = ∀ {A} x → f {A} x ≡ g {A} x

  -- These are extensionality like lemmas. I feel like they are usually nicer
  -- to use than actually using extensionality.
  -- They could be proven legitimately but we have ext and I am feeling lazy.
  meaningeq : ∀{Γ A} {f g : meaningη Γ} → Meaning≡ f g → (e : TExp Γ A) →
               meaning e f ≡ meaning e g
  meaningeq eq e = resp (meaning e) (iext (λ B → ext (λ x → eq x)))

  foldeq : ∀{A} {a0 a0' : A} {an an' : Nat} {as as' : Nat → A → A} →
           a0 ≡ a0' →
           ((n : Nat) (x : A) → as n x ≡ as' n x) →
           an ≡ an' →
           NAT.fold a0 as an ≡ NAT.fold a0' as' an'
  foldeq eq0 eqs eqn = resp3 NAT.fold eq0 (ext (λ n → ext (λ a → eqs n a))) eqn

  -- First stuff for renaming, lifting
  meaning-ren-wk : ∀{A B Γ Γ'} → (γ : TRen Γ Γ') →
                   (η : meaningη Γ') →
                   (a : interp A) →
                   (x : B ∈ A :: Γ) →
                   extendη η a (wk γ x) ≡ extendη (λ y → η (γ y)) a x
  meaning-ren-wk γ η a Z = Refl
  meaning-ren-wk γ η a (S x) = Refl

  meaning-ren : ∀{A Γ Γ'} → (γ : TRen Γ Γ') →
                (e : TExp Γ A) →
                (η : meaningη Γ') →
                meaning (ren γ e) η ≡ meaning e (η o γ)
  meaning-ren γ (var x) η = Refl
  meaning-ren γ (Λ e) η =
    ext (λ M →
     meaning-ren (wk γ) e (extendη η M) ≡≡ meaningeq (meaning-ren-wk γ η M) e)
  meaning-ren γ (e $ e') η = resp2 (λ x y → x y) (meaning-ren γ e η) (meaning-ren γ e' η)
  meaning-ren γ zero η = Refl
  meaning-ren γ (suc e) η = resp S (meaning-ren γ e η)
  meaning-ren γ (rec en e0 es) η =
    foldeq
     (meaning-ren γ e0 η)
     (λ _ M → meaning-ren (wk γ) es (extendη η M) ≡≡ meaningeq (meaning-ren-wk γ η M) es)
     (meaning-ren γ en η)

  meaning-sub-lift : ∀{A B Γ Γ'} → (γ : TSubst Γ Γ') →
                     (η : meaningη Γ') →
                     (a : interp A) →
                     (x : B ∈ A :: Γ) →
                     meaning (liftγ γ x) (extendη η a) ≡
                     extendη (λ y → meaning (γ y) η) a x
  meaning-sub-lift γ η a Z = Refl
  meaning-sub-lift γ η a (S x) =
    (meaning-ren S (γ x) (extendη η a)) ≡≡
    resp (meaning (γ x)) (iext (λ C → ext (λ x → Refl)))

  -- Define a notion of how to commute a substitution with a
  -- denotational interpretation
  substMeaning : ∀{A Γ Γ'} → (γ : TSubst Γ Γ') →
                 (f : meaningη Γ → interp A) →
                 (meaningη Γ' → interp A)
  substMeaning γ f η = f (λ x → meaning (γ x) η)

  -- And show that that notion actually does commute with it.
  meaning-sub : ∀{A Γ Γ'} → (γ : TSubst Γ Γ') →
                (e : TExp Γ A) →
                (η : meaningη Γ') →
                meaning (ssubst γ e) η ≡ substMeaning γ (meaning e) η
  meaning-sub γ (var x) η = Refl
  meaning-sub γ (Λ e) η =
    ext (λ M →
      meaning-sub (liftγ γ) e (extendη η M) ≡≡ meaningeq (meaning-sub-lift γ η M) e)
  meaning-sub γ (e $ e') η = resp2 (λ x y → x y) (meaning-sub γ e η) (meaning-sub γ e' η)
  meaning-sub γ zero η = Refl
  meaning-sub γ (suc e) η = resp S (meaning-sub γ e η)
  meaning-sub γ (rec en e0 es) η =
   foldeq
   (meaning-sub γ e0 η)
   (λ _ M → meaning-sub (liftγ γ) es (extendη η M) ≡≡ meaningeq (meaning-sub-lift γ η M) es)
   (meaning-sub γ en η)

  -- Easy lemma about singleton contexts
  meaning-sing : ∀{A B}(e' : TCExp B) →
                 (x : A ∈ [ B ]) →
                 meaning (singγ e' x) emptyη ≡ extendη emptyη (meaning e' emptyη) x
  meaning-sing e Z = Refl
  meaning-sing e (S x) = Refl

  -- The basic fact we need about substitution.
  meaning-subst : ∀{A B}(e' : TCExp B)(e : TExp [ B ] A) →
                  meaning e (extendη emptyη (cmeaning e')) ≡
                  cmeaning (subst e' e)
  meaning-subst e' e =
    symm (meaning-sub (singγ e') e emptyη ≡≡
          resp (meaning e) (iext (λ A → ext (λ x → meaning-sing e' x))))

  -- The main theorem about the dynamic semantics
  meaning-steps : ∀{A}{e e' : TCExp A} → (e ~> e') → cmeaning e ≡ cmeaning e'
  meaning-steps {e = e₁ $ e₂} (step-app-l St) =
         resp (λ f → f (meaning e₂ emptyη)) (meaning-steps St)
  meaning-steps {e = (Λ e₁) $ e₂} step-beta = meaning-subst e₂ e₁
  meaning-steps (step-suc St) = resp S (meaning-steps St)
  meaning-steps {e = rec e e₀ es} (step-rec St) =
         resp (λ e' → NAT.fold (meaning e₀ emptyη)
                        (λ n x → meaning es (extendη emptyη x)) e')
              (meaning-steps St)
  meaning-steps step-rec-z = Refl
  meaning-steps {e = rec (suc e) e₀ es} (step-rec-s _) = meaning-subst (rec e e₀ es) es

  meaning-eval : ∀{A}{e e' : TCExp A} → (e ~>* e') → cmeaning e ≡ cmeaning e'
  meaning-eval eval-refl = Refl
  meaning-eval (eval-cons S1 E) = meaning-steps S1 ≡≡ meaning-eval E

open DenotCommutes public

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
module Introduction.All where

import Introduction.Basics
import Introduction.Universes
import Introduction.Unicode
import Introduction.Built-in
import Introduction.Modules
import Introduction.Implicit
import Introduction.Data.Vec
import Introduction.Data.Empty
import Introduction.Data.Parameterised
import Introduction.Data.ByRecursion
import Introduction.Operators
import Introduction.Modules.Parameterised

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2011-09-11
module Issue392 where

import Common.Irrelevance

-- Create an irrelevant record R1 (all fields irrelevant).
record R1 : Set1 where
  field
    .f1 : Set

{- module R1 .(r : R1) where
     .f1 : Set -- = R1.f1 r
-}

-- Create an irrelevant instance f2 of R1.
record R2 : Set2 where
  field
    .f2 : R1
    f3  : Set

-- This succeeds even though f2 is irrelevant.
  open R1 f2 public

{- A more realistic use would be s.th. like

  record IsEquivalence {a ℓ} {A : Set a}
                       (_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
    field
      .refl  : Reflexive _≈_
      .sym   : Symmetric _≈_
      .trans : Transitive _≈_

  record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
    infix 4 _≈_
    field
      Carrier       : Set c
      _≈_           : Rel Carrier ℓ
      .isEquivalence : IsEquivalence _≈_

    open IsEquivalence isEquivalence public
-}


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

{-
  Ribbon is an explicit covering space construction.

  This construction is given by Daniel Grayson, Favonia
  and Guillaume Brunerie together.
-}

open import HoTT

-- A is the pointed base space.
-- El is intended to be a (group-)set,
module homotopy.RibbonCover {i : ULevel} where

  -- The HIT ribbon---reconstructed covering space

  module _ (X : Ptd i) {j} (gs : GroupSet (πS 0 X) j) (a₂ : de⊙ X) where
    private
      A = de⊙ X
      a₁ = pt X
      El = GroupSet.El gs
      El-level = GroupSet.El-level gs
      infix 80 _⊙_
      _⊙_ = GroupSet.act gs

    RibbonSet : Type (lmax i j)
    RibbonSet = El × (a₁ =₀ a₂)

    data RibbonRel : RibbonSet → RibbonSet → Type (lmax i j) where
      ribbon-rel : ∀ el loop (p : a₁ =₀ a₂)
        → RibbonRel (el ⊙ loop , p) (el , loop ∙₀ p)

    Ribbon : Type (lmax i j)
    Ribbon = SetQuot RibbonRel

  module _ {X : Ptd i} {j} {gs : GroupSet (πS 0 X) j} {a₂ : de⊙ X} where
    private
      A = de⊙ X
      a = pt X
      El = GroupSet.El gs
      El-level = GroupSet.El-level gs
      infix 80 _⊙_
      _⊙_ = GroupSet.act gs

    -- A point in the fiber [a₂].
    {-
      [e] is a point in the [fiber a], and
      [p] is a path to transport [y] to fiber [a₂].
    -}
    trace : El → a =₀ a₂ → Ribbon X gs a₂
    trace el p = q[ el , p ]

    {-
      A loop based at [a] can used as a group action
      or for concatination.  Both should be equivalent.
    -}
    paste : ∀ el loop (p : a =₀ a₂) → trace (el ⊙ loop) p == trace el (loop ∙₀ p)
    paste el loop p = quot-rel (ribbon-rel el loop p)

    {-
      Make each fiber a set and cancel all higher structures
      due to [paste].
    -}
    Ribbon-level : is-set (Ribbon X gs a₂)
    Ribbon-level = SetQuot-level

    Ribbon-is-set = Ribbon-level

    -- Elimination rules.
    module RibbonElim {j} {P : Ribbon X gs a₂ → Type j}
      (P-level : ∀ r → is-set (P r))
      (trace* : ∀ el p → P (trace el p))
      (paste* : ∀ el loop p
                → trace* (el ⊙ loop) p == trace* el (loop ∙₀ p)
                  [ P ↓ paste el loop p ]) where

      private
        q[_]* : (α : RibbonSet X gs a₂) → P q[ α ]
        q[ el , p ]* = trace* el p

        rel* : ∀ {α₁ α₂} (r : RibbonRel X gs a₂ α₁ α₂) → q[ α₁ ]* == q[ α₂ ]* [ P ↓ quot-rel r ]
        rel* (ribbon-rel el loop p) = paste* el loop p

        module M = SetQuotElim P-level q[_]* rel*

      f : Π (Ribbon X gs a₂) P
      f = M.f

    open RibbonElim public using () renaming (f to Ribbon-elim)

    module RibbonRec {j} {P : Type j}
      (P-level : is-set P)
      (trace* : ∀ el p → P)
      (paste* : ∀ el loop p
                → trace* (el ⊙ loop) p == trace* el (loop ∙₀ p)) where

      private
        module M = RibbonElim (λ _ → P-level) trace*
          (λ el loop p → ↓-cst-in (paste* el loop p))

      f : Ribbon X gs a₂ → P
      f = M.f

    open RibbonRec public using () renaming (f to Ribbon-rec)

  -- This data structure gives a cover.
  Ribbon-cover : ∀ (X : Ptd i) {j} (gs : GroupSet (πS 0 X) j)
    → Cover (de⊙ X) (lmax i j)
  Ribbon-cover X gs = record
    { Fiber = Ribbon X gs
    ; Fiber-level = λ a → Ribbon-level
    }

  transp-trace : ∀ {A : Type i} {a₁} {j}
    {gs : GroupSet (πS 0 ⊙[ A , a₁ ]) j}
    {a₂} (q : a₁ == a₂) y p
    → transport (Ribbon ⊙[ A , a₁ ] gs) q (trace y p) == trace y (p ∙₀ [ q ])
  transp-trace idp y p = ap (trace y) $ ! $ ∙₀-unit-r p

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

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

import Data.Empty as Empty
import Data.Product as Product
import Data.Product.Properties as Productₚ
import Data.Unit as Unit
import Data.Nat as Nat
import Data.Vec as Vec
import Data.Vec.Properties as Vecₚ
import Data.Bool as Bool
import Data.Fin as Fin
import Data.Vec.Relation.Unary.All as All

open Empty using (⊥-elim)
open Nat using (ℕ; zero; suc)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)
open Fin using (Fin ; zero ; suc)
open Product using (_,_; proj₁; proj₂)

import PiCalculus.Syntax
open PiCalculus.Syntax.Scoped
open import PiCalculus.Semantics
open import PiCalculus.LinearTypeSystem.Algebras

module PiCalculus.LinearTypeSystem.Strengthening (Ω : Algebras) where
open Algebras Ω
open import PiCalculus.LinearTypeSystem Ω
open import PiCalculus.LinearTypeSystem.ContextLemmas Ω

private
  variable
    n : ℕ
    idxs : Idxs n
    idx idx' : Idx
    t t' : Type
    i j : Fin n
    P Q : Scoped n

∋-strengthen : {γ : PreCtx (suc n)} {idxs : Idxs (suc n)} {Γ Θ : Ctx idxs} {m' : Usage idx' ²}
             → (i : Fin (suc n))
             → (i≢j : i ≢ j)
             → γ              ； Γ              ∋[ j ] t' ； m' ▹ Θ
             → Vec.remove γ i ； ctx-remove Γ i ∋[ Fin.punchOut i≢j ] t' ； m' ▹ ctx-remove Θ i
∋-strengthen zero i≢x (zero , zero _) = ⊥-elim (i≢x refl)
∋-strengthen zero i≢x (suc t , suc x) = t , x
∋-strengthen {γ = _ -, _ -, _} {_ -, _ -, _} {_ -, _ -, _} (suc i) i≢x (zero , zero xyz) = zero , zero xyz
∋-strengthen {γ = _ -, _ -, _} {_ -, _ -, _} {_ -, _ -, _} {_ -, _ -, _} (suc i) i≢x (suc t , suc x) = there (∋-strengthen i (i≢x ∘ cong suc) (t , x))

⊢-strengthen : {P : Scoped (suc n)} {γ : PreCtx (suc n)} {idxs : Idxs (suc n)} {Γ Θ : Ctx idxs}
             → (i : Fin (suc n))
             → (uP : Unused i P)
             → γ ； Γ ⊢ P ▹ Θ
             → Vec.remove γ i ； ctx-remove Γ i ⊢ lower i P uP ▹ ctx-remove Θ i
⊢-strengthen i uP 𝟘 = 𝟘
⊢-strengthen {γ = _ -, _} {Γ = _ -, _} {Θ = _ -, _} i uP (ν t m μ ⊢P)
  = ν t m μ (⊢-strengthen (suc i) uP ⊢P)
⊢-strengthen {γ = _ -, _} {Γ = _ -, _} {Θ = _ -, _} i (i≢x , uP) (_⦅⦆_ {Ξ = _ -, _} x ⊢P)
  = ∋-strengthen i i≢x x ⦅⦆ ⊢-strengthen (suc i) uP ⊢P
⊢-strengthen {γ = _ -, _} i (i≢x , i≢y , uP) (x ⟨ y ⟩ ⊢P)
  = ∋-strengthen i i≢x x ⟨ ∋-strengthen i i≢y y ⟩ ⊢-strengthen i uP ⊢P
⊢-strengthen {γ = _ -, _} i (uP , uQ) (⊢P ∥ ⊢Q)
  = ⊢-strengthen i uP ⊢P ∥ ⊢-strengthen i uQ ⊢Q

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
open import Functional hiding (Domain)
import      Structure.Logic.Classical.NaturalDeduction

module Structure.Logic.Classical.SetTheory.ZFC {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ (_∈_ : Domain → Domain → Formula) where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)

open import Lang.Instance
import      Lvl
open import Structure.Logic.Classical.NaturalDeduction.Proofs            ⦃ classicLogic ⦄
open import Structure.Logic.Classical.SetTheory.SetBoundedQuantification ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Classical.SetTheory.Relation                 ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Constructive.Functions.Properties            ⦃ constructiveLogicSignature ⦄

private
  module Meta where
    open import Numeral.Finite           public
    open import Numeral.Finite.Bound{ℓₗ} public
    open import Numeral.Natural                public

-- The symbols/signature of ZFC set theory.
record Signature : Set((ℓₗ Lvl.⊔ ℓₒ) Lvl.⊔ ℓₘₗ) where
  infixl 3000 _∪_
  infixl 3001 _∩_
  infixl 3002 _⨯_ _∖_

  field
    -- Empty set
    -- The set consisting of no elements.
    ∅ : Domain

    -- Pair set.
    -- The set consisting of only two elements.
    pair : Domain → Domain → Domain

    -- Subset filtering.
    -- The subset of the specified set where all elements satisfy the specified formula.
    filter : Domain → (Domain → Formula) → Domain

    -- Power set.
    -- The set of all subsets of the specified set.
    ℘ : Domain → Domain

    -- Union over arbitrary sets.
    -- Constructs a set which consists of elements which are in any of the specified sets.
    ⋃ : Domain → Domain

    -- An inductive set.
    -- A set which has the `Inductive`-property. Also infinite.
    inductiveSet : Domain

    -- The map of a set.
    -- The set of values when a function is applied to every element of a set.
    -- Or: The image of the function on the set.
    -- Or: The image of the function.
    map : (Domain → Domain) → Domain → Domain

    -- An inverse function of a function from its domain to its image.
    inv : (Domain → Domain) → Domain → Domain

  -- Singleton set.
  -- A set consisting of only a single element.
  singleton : Domain → Domain
  singleton(s) = pair(s)(s)

  -- Union operator.
  -- Constructs a set which consists of both elements from LHS and RHS.
  _∪_ : Domain → Domain → Domain
  a ∪ b = ⋃(pair a b)

  -- Intersection operator.
  -- Constructs a set which consists of elements which are in both LHS and RHS.
  _∩_ : Domain → Domain → Domain
  a ∩ b = filter(a)(_∈ b)

  -- "Without"-operator.
  -- Constructs a set which consists of elements which are in LHS, but not RHS.
  _∖_ : Domain → Domain → Domain
  a ∖ b = filter(a)(_∉ b)

  -- Intersection over arbitrary sets.
  -- Constructs a set which consists of elements which are in all of the specified sets.
  ⋂ : Domain → Domain
  ⋂(a) = filter(⋃(a)) (a₁ ↦ ∀ₗ(a₂ ↦ (a₂ ∈ a) ⟶ (a₁ ∈ a₂)))

  -- Tuple value.
  -- An ordered pair of values.
  _,_ : Domain → Domain → Domain
  a , b = pair(singleton(a)) (pair(a)(b))

  -- Set product (Set of tuples) (Cartesian product).
  _⨯_ : Domain → Domain → Domain
  a ⨯ b = filter(℘(℘(a ∪ b))) (t ↦ ∃ₗ(x ↦ (x ∈ a) ∧ ∃ₗ(y ↦ (y ∈ b) ∧ (t ≡ (x , y)))))

  identityPairing : Domain → Domain
  identityPairing(D) = filter(D ⨯ D) (xy ↦ ∃ₗ(a ↦ xy ≡ (a , a)))

  -- swappedPairing : Domain → Domain
  -- swappedPairing() =

  -- Set product over a finite indexed family (Cartesian product).
  -- TODO: Not really like this. See definition of (_⨯_) and (_,_), and try to express the same here
  -- TODO: Also, make it possible to take the set product of infinite indexed families
  -- TODO: Maybe just use functions like (𝕟(n) →ₛₑₜ _) for finite and (ℕ → _) for infinite
  -- ∏_ : ∀{n} → FiniteIndexedFamily(n) → Domain
  -- ∏_ {Meta.𝟎}            _ = singleton(∅)
  -- ∏_ {Meta.𝐒(Meta.𝟎)}    I = I(Meta.𝟎)
  -- ∏_ {Meta.𝐒(Meta.𝐒(n))} I = I(Meta.maximum) ⨯ (∏_ {Meta.𝐒(n)} (I ∘ Meta.bound-𝐒))

  -- Quotient set.
  -- The set of equivalence classes.
  _/_ : Domain → BinaryRelator → Domain
  a / (_▫_) = filter(℘(a))(aₛ ↦ ∀ₛ(aₛ)(x ↦ ∀ₛ(aₛ)(y ↦ x ▫ y)))

  -- Equivalence class
  -- The set of elements which are equivalent to the specified one.
  [_of_,_] : Domain → Domain → BinaryRelator → Domain
  [ x of a , (_▫_) ] = filter(a)(y ↦ x ▫ y)

  -- TODO: Implement a choice function (the "axiom of choice" one) by inv
  -- choice : Domain → Domain → Domain

  -- The unmap of a set.
  -- The set of elements in the domain X when applied to a function gives an element in Y.
  -- Or: The inverse image of the function on the set.
  -- Or: The pre-image of the function on the set.
  -- Note:
  --   The domain is neccessary because a class function's domain is not neccesarily a set.
  --   For example: `const(x): Domain → Domain` for any (x: Domain) is a class function for which its domain is not a set.
  --   This is because const is defined for all objects in `Domain`, so if a set would have to have all objects in `Domain`, it has to be the universal set, but there is no universal set.
  unmap : Domain → (Domain → Domain) → Domain → Domain
  unmap(X) f(Y) = filter(X) (x ↦ f(x) ∈ Y)

{-
module Function ⦃ signature : Signature ⦄ where
  open Signature ⦃ ... ⦄

  record SetRepresentable (f : Function) : Set((ℓₗ Lvl.⊔ ℓₒ) Lvl.⊔ ℓₘₗ) where
    constructor intro

    field
      set : Domain

    field
      proof : Proof(∀ₗ(x ↦ ∀ₗ(y ↦ (f(x) ≡ y) ⟷ ((x , y) ∈ set))))

  -- An instance of Type(f) means that the function f has a default domain and codomain, and a proof that the function actually are closed inside this domain/codomain pair.
  record Type (f : Function) : Set((ℓₗ Lvl.⊔ ℓₒ) Lvl.⊔ ℓₘₗ) where
    constructor intro
    field
      domain   : Domain
      codomain : Domain

    field
      closure : Proof(∀ₛ(domain)(x ↦ f(x) ∈ codomain))
  open Type ⦃ ... ⦄ public
-}

module Tuple ⦃ signature : Signature ⦄ where -- TODO: Move
  open Signature ⦃ ... ⦄

  left : Domain → Domain
  left(s) = ⋃(⋂ s)

  right : Domain → Domain
  right(s) = (⋃ s) ∖ left(s)

-- A model of natural numbers expressed in set theory (using only sets).
module NumeralNatural ⦃ signature : Signature ⦄ where -- TODO: Move
  open Signature ⦃ ... ⦄

  -- The zero constant from the standard inductive set definition of ℕ in ZFC set theory.
  𝟎 : Domain
  𝟎 = ∅

  -- The successor function from the standard inductive set definition of ℕ in ZFC set theory.
  -- This means that all lesser numbers are contained in every number.
  -- Examples:
  -- • 0: {}
  -- • 1: 0∪{0} = {0} = {{},{{}}}
  -- • 2: 1∪{1} = {0}∪{1} = {0,1} = {{},{{},{{}}}}
  -- • 3: 2∪{2} = {0,1}∪{2} = {0,1,2} = {{{},{{},{{}}}},{{{},{{},{{}}}}}}
  -- • 4: 3∪{3} = {0,1,2}∪{3} = {0,1,2,3} = {{{{},{{},{{}}}},{{{},{{},{{}}}}}},{{{{},{{},{{}}}},{{{},{{},{{}}}}}}}}
  𝐒 : Domain → Domain
  𝐒(n) = n ∪ singleton(n)

  -- A set is ℕ-inductive when has zero and all its successors.
  -- In loose terms: Inductive(I) means (I ⊆ ℕ)
  Inductive : Domain → Formula
  Inductive(I) = (𝟎 ∈ I) ∧ (∀ₗ(x ↦ (x ∈ I) ⟶ (𝐒(x) ∈ I)))

  -- The "smallest" inductive set is the set of natural numbers.
  -- All elements which can be expressed using only 𝟎 and 𝐒.
  ℕ : Domain
  ℕ = ⋂(filter(℘(inductiveSet)) Inductive) -- TODO: This pattern seems useful

  -- The relation "lesser than" in this model of ℕ.
  -- This works for all elements in ℕ by the definition of 𝟎 and 𝐒.
  _<_ : BinaryRelator
  a < b = a ∈ b

  _≤_ : BinaryRelator
  a ≤ b = (a < b) ∨ (a ≡ b)

  _>_ : BinaryRelator
  a > b = b < a

  _≥_ : BinaryRelator
  a ≥ b = b ≤ a

  infixl 2000 _<_ _≤_ _>_ _≥_

  𝕟 : Domain → Domain
  𝕟(n) = filter(ℕ) (_< n)

module Axioms ⦃ signature : Signature ⦄ where
  open NumeralNatural using () renaming (Inductive to [ℕ]-Inductive)
  open Signature ⦃ ... ⦄

  -- `∅` is a set which is empty.
  -- • Allows a construction of an empty set.
  EmptySetMembership : Formula
  EmptySetMembership = Empty(∅)

  -- `pair` is the construction of a set with two elements.
  -- • Allows a construction of a set with two elements.
  PairingMembership : Formula
  PairingMembership = ∀ₗ(x₁ ↦ ∀ₗ(x₂ ↦ (∀ₗ(x ↦ (x ∈ pair(x₁)(x₂)) ⟷ (x ≡ x₁)∨(x ≡ x₂)))))

  -- `filter` is the set which is the subset of a set where all elements satisfies a predicate.
  RestrictedComprehension : (Domain → Formula) → Formula
  RestrictedComprehension(φ) = ∀ₗ(s ↦ ∀ₗ(x ↦ ((x ∈ filter(s)(φ)) ⟷ ((x ∈ s) ∧ φ(x)))))

  -- `℘` is the construction of a set which contains all the subsets of a set.
  -- • Allows a construction of a set that is the powerset of a set.
  PowerSetMembership : Formula
  PowerSetMembership = ∀ₗ(s ↦ ∀ₗ(x ↦ (x ∈ ℘(s)) ⟷ (x ⊆ s)))

  -- `⋃` is the construction of a set which contains all the elements of a collection of sets.
  -- • Allows a construction of a set that is the union of some sets.
  UnionMembership : Formula
  UnionMembership = ∀ₗ(ss ↦ ∀ₗ(x ↦ (x ∈ ⋃(ss)) ⟷ ∃ₗ(s ↦ (s ∈ ss)∧(x ∈ s))))

  -- `inductiveSet` is ℕ-inductive.
  -- • An inductive set is infinite, so this implies that an infinite set exists.
  -- • Makes it possible to construct the set of natural numbers (ℕ).
  Infinity : Formula
  Infinity = [ℕ]-Inductive(inductiveSet)

  -- Set identity is extensionally determined. More specifically by its contents.
  -- • Guarantees the definition of equality for sets.
  Extensionality : Formula
  Extensionality = ∀ₗ(s₁ ↦ ∀ₗ(s₂ ↦ ∀ₗ(x ↦ (x ∈ s₁)⟷(x ∈ s₂)) ⟷ (s₁ ≡ s₂)))

  -- A non-empty set contain sets that are disjoint to it.
  -- • Prevents sets containing themselves.
  -- • Makes every set have an ordinal rank.
  Regularity : Formula
  Regularity = ∀ₗ(s₁ ↦ (NonEmpty(s₁) ⟶ ∃ₗ(s₂ ↦ (s₂ ∈ s₁) ∧ Disjoint(s₁)(s₂))))

  -- `map` is the construction of the image of a function restricted to a set.
  -- • The `map`-function on a function is a function from sets to sets.
  Replacement : (Domain → Domain) → Formula
  Replacement(f) = ∀ₗ(A ↦ ∀ₗ(y ↦ (y ∈ map f(A)) ⟷ ∃ₛ(A)(x ↦ y ≡ f(x))))
  -- ReplacementTraditional = ∀{φ : Domain → Domain → Formula} → Proof(∀ₗ(A ↦ TotalFunction(φ)(A) ⟶ ∃ₗ(B ↦ ∀ₗ(y ↦ (y ∈ B) ⟷ ∃ₗ(x ↦ (x ∈ A) ∧ φ(x)(y))))))

  -- The set product of non-empty finite indexed family of sets where all the sets are non-empty is non-empty.
  -- TODO: Should the indexed family really be finite? https://en.wikipedia.org/wiki/Cartesian_product#Infinite_Cartesian_products
  -- Choice = ∀{n : Meta.ℕ}{F : FiniteIndexedFamily(Meta.𝐒(n))} → (∀{i : Meta.𝕟(Meta.𝐒(n))} → Proof(NonEmpty(F(i)))) → Proof(NonEmpty(∏ F))

  -- `inv` constructs the right inverse for function composition.
  -- • All surjective class functions have a right inverse.
  -- • An element applied to the inverse function of a function yields/returns one of the arguments that yield/return this element as a value when it exists.
  -- TODO: MAybe this is too strong of a statement? Because the image is not neccessarily a set if the class function is defined for all objects (in the domain) in the theory? Is this really equivalent to `ChoiceTraditional`?
  Choice : (Domain → Domain) → Formula
  Choice(f) = ∀ₗ(y ↦ (Value f(y)) ⟶ ((f ∘ (inv f))(y) ≡ y))

  -- ChoiceTraditional = Proof(∀ₗ(s ↦ (∅ ∉ s) ⟶ ∃ₛ(s →ₛₑₜ (⋃ s))(f ↦ ∀ₛ(s)(x ↦ ∀ₛ(⋃ s)(y ↦ ((x , y) ∈ f) ⟶ (y ∈ x))))))
  -- ChoiceTraditional : (Domain → Domain → Domain) → Formula
  -- ChoiceTraditional(choice) = ∀ₗ(s ↦ ∀ₛ(s)(x ↦ NonEmpty(x) ⟶ (choice(s)(x) ∈ x)))

record Z ⦃ signature : Signature ⦄ : Set((ℓₗ Lvl.⊔ ℓₒ) Lvl.⊔ ℓₘₗ) where
  open Axioms
  open Signature ⦃ ... ⦄

  field
    extensional   : Proof(Extensionality)
    empty         : Proof(EmptySetMembership)
    pairing       : Proof(PairingMembership)
    comprehension : ∀{φ} → Proof(RestrictedComprehension(φ))
    union         : Proof(UnionMembership)
    power         : Proof(PowerSetMembership)
    infinity      : Proof(Infinity)

record ZF ⦃ signature : Signature ⦄ : Set((ℓₗ Lvl.⊔ ℓₒ) Lvl.⊔ ℓₘₗ) where
  open Axioms
  open Signature ⦃ ... ⦄

  field
    extensional   : Proof(Extensionality)
    empty         : Proof(EmptySetMembership)
    pairing       : Proof(PairingMembership)
    comprehension : ∀{φ} → Proof(RestrictedComprehension(φ))
    union         : Proof(UnionMembership)
    power         : Proof(PowerSetMembership)
    infinity      : Proof(Infinity)
    regular       : Proof(Regularity)
    replacement   : ∀{f} → Proof(Replacement(f))

record ZFC ⦃ signature : Signature ⦄ : Set((ℓₗ Lvl.⊔ ℓₒ) Lvl.⊔ ℓₘₗ) where
  open Axioms
  open Signature ⦃ ... ⦄

  field
    extensional   : Proof(Extensionality)
    empty         : Proof(EmptySetMembership)
    pairing       : Proof(PairingMembership)
    comprehension : ∀{φ} → Proof(RestrictedComprehension(φ))
    union         : Proof(UnionMembership)
    power         : Proof(PowerSetMembership)
    infinity      : Proof(Infinity)
    regular       : Proof(Regularity)
    replacement   : ∀{f} → Proof(Replacement(f))
    choice        : ∀{f} → Proof(Choice(f))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Luau.RuntimeError where

open import Agda.Builtin.Equality using (_≡_)
open import Luau.Heap using (Heap; _[_])
open import FFI.Data.Maybe using (just; nothing)
open import FFI.Data.String using (String)
open import Luau.Syntax using (Block; Expr; nil; var; addr; block_is_end; _$_; local_←_; return; done; _∙_; number; binexp)
open import Luau.RuntimeType using (RuntimeType; valueType)
open import Luau.Value using (val)
open import Properties.Equality using (_≢_)

data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set

data RuntimeErrorᴱ H where
  TypeMismatch : ∀ t v → (t ≢ valueType v) → RuntimeErrorᴱ H (val v)
  UnboundVariable : ∀ x → RuntimeErrorᴱ H (var x)
  SEGV : ∀ a → (H [ a ] ≡ nothing) → RuntimeErrorᴱ H (addr a)
  app₁ : ∀ {M N} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (M $ N)
  app₂ : ∀ {M N} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (M $ N)
  block : ∀ b {B} → RuntimeErrorᴮ H B → RuntimeErrorᴱ H (block b is B end)
  bin₁ : ∀ {M N op} → RuntimeErrorᴱ H M → RuntimeErrorᴱ H (binexp M op N)
  bin₂ : ∀ {M N op} → RuntimeErrorᴱ H N → RuntimeErrorᴱ H (binexp M op N)

data RuntimeErrorᴮ H where
  local : ∀ x {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (local x ← M ∙ B)
  return : ∀ {M B} → RuntimeErrorᴱ H M → RuntimeErrorᴮ H (return M ∙ B)


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Sets.Facts.Terminal where

open import Data.Unit using (⊤)
open import Level using (Lift ; lift ; lower)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

open import Cats.Category
open import Cats.Category.Sets using (Sets)

instance
  hasTerminal : ∀ {l} → HasTerminal (Sets l)
  hasTerminal = record
    { ⊤ = Lift _ ⊤
    ; isTerminal = λ X → record { unique = λ _ _ → refl }
    }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
{-# OPTIONS -WUnknownFixityInMixfixDecl #-}

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

_+_ : Nat → Nat → Nat
zero + n = n
(suc m) + n = suc (m + n)

private
  _*_ : Nat → Nat → Nat
  zero    * n = zero
  (suc m) * n = n + (m * n)

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr _<>_ n []       = n
foldr _<>_ n (x ∷ xs) = x <> (foldr _<>_ n xs)

sumOfPowers : Nat → List Nat → Nat
sumOfPowers x = foldr (λ p → (x ^ p) +_) zero where

  _^_ : Nat → Nat → Nat
  m ^ zero  = suc zero
  m ^ suc n = m * (m ^ n)


text:
------------------------------------------------------------------------
-- An implementation of tree sort, formally proved to return a
-- permutation of the input
------------------------------------------------------------------------

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

open import Equality
open import Prelude hiding (id)

module Tree-sort.Partial
  {c⁺}
  (eq : ∀ {a p} → Equality-with-J a p c⁺)
  {A : Type}
  (_≤_ : A → A → Bool) -- A comparison function.
  where

open Derived-definitions-and-properties eq

open import Bag-equivalence eq
open import Bijection eq using (_↔_)
open import Function-universe eq hiding (_∘_)
open import List eq
open import Tree eq

------------------------------------------------------------------------
-- Insertion into trees

-- Inserts an element into the tree.

insert : A → Tree A → Tree A
insert x leaf         = singleton x
insert x (node l y r) =
  if x ≤ y then node (insert x l) y r
           else node l y (insert x r)

-- The insert function inserts.

Any-insert : ∀ (P : A → Type) x t →
             AnyT P (insert x t) ↔ P x ⊎ AnyT P t
Any-insert P x leaf =
  AnyT P (singleton x)  ↔⟨ Any-singleton P ⟩
  P x                   ↔⟨ inverse ⊎-right-identity ⟩
  P x ⊎ ⊥               ↔⟨⟩
  P x ⊎ AnyT P leaf     □
Any-insert P x (node l y r) with x ≤ y
... | true  =
  AnyT P (insert x l) ⊎ P y ⊎ AnyT P r  ↔⟨ Any-insert P x l ⊎-cong id ⟩
  (P x ⊎ AnyT P l)    ⊎ P y ⊎ AnyT P r  ↔⟨ inverse ⊎-assoc ⟩
  P x ⊎ AnyT P l      ⊎ P y ⊎ AnyT P r  □
... | false =
  AnyT P l ⊎ P y ⊎ AnyT P (insert x r)  ↔⟨ id ⊎-cong id ⊎-cong Any-insert P x r ⟩
  AnyT P l ⊎ P y ⊎ P x ⊎ AnyT P r       ↔⟨ lemma (AnyT P l) (P y) (P x) (AnyT P r) ⟩
  P x ⊎ AnyT P l ⊎ P y ⊎ AnyT P r       □
  where
  -- The following lemma is easy to prove automatically (for instance
  -- by using a ring solver).

  lemma : (A B C D : Type) → A ⊎ B ⊎ C ⊎ D ↔ C ⊎ A ⊎ B ⊎ D
  lemma A B C D =
    A ⊎ B ⊎ C ⊎ D      ↔⟨ id ⊎-cong ⊎-assoc ⟩
    A ⊎ (B ⊎ C) ⊎ D    ↔⟨ id ⊎-cong ⊎-comm ⊎-cong id ⟩
    A ⊎ (C ⊎ B) ⊎ D    ↔⟨ ⊎-assoc ⟩
    (A ⊎ C ⊎ B) ⊎ D    ↔⟨ ⊎-assoc ⊎-cong id ⟩
    ((A ⊎ C) ⊎ B) ⊎ D  ↔⟨ (⊎-comm ⊎-cong id) ⊎-cong id ⟩
    ((C ⊎ A) ⊎ B) ⊎ D  ↔⟨ inverse ⊎-assoc ⊎-cong id ⟩
    (C ⊎ A ⊎ B) ⊎ D    ↔⟨ inverse ⊎-assoc ⟩
    C ⊎ (A ⊎ B) ⊎ D    ↔⟨ id ⊎-cong inverse ⊎-assoc ⟩
    C ⊎ A ⊎ B ⊎ D      □

------------------------------------------------------------------------
-- Turning a list into a search tree

-- Converts the list to a search tree.

to-search-tree : List A → Tree A
to-search-tree = foldr insert leaf

-- No elements are added or removed.

to-search-tree-lemma : ∀ xs z → z ∈T to-search-tree xs ↔ z ∈ xs
to-search-tree-lemma [] = λ z →
  z ∈T leaf  ↔⟨⟩
  z ∈  []    □
to-search-tree-lemma (x ∷ xs) = λ z →
  z ∈T insert x (to-search-tree xs)  ↔⟨ Any-insert (λ x → z ≡ x) _ _ ⟩
  z ≡ x ⊎ z ∈T to-search-tree xs     ↔⟨ id ⊎-cong to-search-tree-lemma xs z ⟩
  z ∈ x ∷ xs                         □

------------------------------------------------------------------------
-- Sorting

-- Sorts a list.

tree-sort : List A → List A
tree-sort = flatten ∘ to-search-tree

-- The result is a permutation of the input.

tree-sort-permutes : ∀ xs → tree-sort xs ≈-bag xs
tree-sort-permutes xs = λ z →
  z ∈  flatten (to-search-tree xs)  ↔⟨ flatten-lemma (to-search-tree xs) z ⟩
  z ∈T to-search-tree xs            ↔⟨ to-search-tree-lemma xs z ⟩
  z ∈  xs                           □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import Categories.Category
open import Categories.Monoidal

-- moar

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories