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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Functions.Embedding
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Empty
open import Cubical.Data.Nat

open import Cubical.Data.Sum.Base

open Iso

private
  variable
    ℓa ℓb ℓc ℓd : Level
    A : Type ℓa
    B : Type ℓb
    C : Type ℓc
    D : Type ℓd

-- Path space of sum type
module ⊎Path {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where

  Cover : A ⊎ B → A ⊎ B → Type (ℓ-max ℓ ℓ')
  Cover (inl a) (inl a') = Lift {j = ℓ-max ℓ ℓ'} (a ≡ a')
  Cover (inl _) (inr _) = Lift ⊥
  Cover (inr _) (inl _) = Lift ⊥
  Cover (inr b) (inr b') = Lift {j = ℓ-max ℓ ℓ'} (b ≡ b')

  reflCode : (c : A ⊎ B) → Cover c c
  reflCode (inl a) = lift refl
  reflCode (inr b) = lift refl

  encode : ∀ c c' → c ≡ c' → Cover c c'
  encode c _ = J (λ c' _ → Cover c c') (reflCode c)

  encodeRefl : ∀ c → encode c c refl ≡ reflCode c
  encodeRefl c = JRefl (λ c' _ → Cover c c') (reflCode c)

  decode : ∀ c c' → Cover c c' → c ≡ c'
  decode (inl a) (inl a') (lift p) = cong inl p
  decode (inl a) (inr b') ()
  decode (inr b) (inl a') ()
  decode (inr b) (inr b') (lift q) = cong inr q

  decodeRefl : ∀ c → decode c c (reflCode c) ≡ refl
  decodeRefl (inl a) = refl
  decodeRefl (inr b) = refl

  decodeEncode : ∀ c c' → (p : c ≡ c') → decode c c' (encode c c' p) ≡ p
  decodeEncode c _ =
    J (λ c' p → decode c c' (encode c c' p) ≡ p)
      (cong (decode c c) (encodeRefl c) ∙ decodeRefl c)

  encodeDecode : ∀ c c' → (d : Cover c c') → encode c c' (decode c c' d) ≡ d
  encodeDecode (inl a) (inl _) (lift d) =
    J (λ a' p → encode (inl a) (inl a') (cong inl p) ≡ lift p) (encodeRefl (inl a)) d
  encodeDecode (inr a) (inr _) (lift d) =
    J (λ a' p → encode (inr a) (inr a') (cong inr p) ≡ lift p) (encodeRefl (inr a)) d

  Cover≃Path : ∀ c c' → Cover c c' ≃ (c ≡ c')
  Cover≃Path c c' =
    isoToEquiv (iso (decode c c') (encode c c') (decodeEncode c c') (encodeDecode c c'))

  isOfHLevelCover : (n : HLevel)
    → isOfHLevel (suc (suc n)) A
    → isOfHLevel (suc (suc n)) B
    → ∀ c c' → isOfHLevel (suc n) (Cover c c')
  isOfHLevelCover n p q (inl a) (inl a') = isOfHLevelLift (suc n) (p a a')
  isOfHLevelCover n p q (inl a) (inr b') =
    isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥)
  isOfHLevelCover n p q (inr b) (inl a') =
    isOfHLevelLift (suc n) (isProp→isOfHLevelSuc n isProp⊥)
  isOfHLevelCover n p q (inr b) (inr b') = isOfHLevelLift (suc n) (q b b')

isEmbedding-inl : isEmbedding (inl {A = A} {B = B})
isEmbedding-inl w z = snd (compEquiv LiftEquiv (⊎Path.Cover≃Path (inl w) (inl z)))

isEmbedding-inr : isEmbedding (inr {A = A} {B = B})
isEmbedding-inr w z = snd (compEquiv LiftEquiv (⊎Path.Cover≃Path (inr w) (inr z)))

isOfHLevel⊎ : (n : HLevel)
  → isOfHLevel (suc (suc n)) A
  → isOfHLevel (suc (suc n)) B
  → isOfHLevel (suc (suc n)) (A ⊎ B)
isOfHLevel⊎ n lA lB c c' =
  isOfHLevelRetract (suc n)
    (⊎Path.encode c c')
    (⊎Path.decode c c')
    (⊎Path.decodeEncode c c')
    (⊎Path.isOfHLevelCover n lA lB c c')

isSet⊎ : isSet A → isSet B → isSet (A ⊎ B)
isSet⊎ = isOfHLevel⊎ 0

isGroupoid⊎ : isGroupoid A → isGroupoid B → isGroupoid (A ⊎ B)
isGroupoid⊎ = isOfHLevel⊎ 1

is2Groupoid⊎ : is2Groupoid A → is2Groupoid B → is2Groupoid (A ⊎ B)
is2Groupoid⊎ = isOfHLevel⊎ 2

⊎Iso : Iso A C → Iso B D → Iso (A ⊎ B) (C ⊎ D)
fun (⊎Iso iac ibd) (inl x) = inl (iac .fun x)
fun (⊎Iso iac ibd) (inr x) = inr (ibd .fun x)
inv (⊎Iso iac ibd) (inl x) = inl (iac .inv x)
inv (⊎Iso iac ibd) (inr x) = inr (ibd .inv x)
rightInv (⊎Iso iac ibd) (inl x) = cong inl (iac .rightInv x)
rightInv (⊎Iso iac ibd) (inr x) = cong inr (ibd .rightInv x)
leftInv (⊎Iso iac ibd) (inl x)  = cong inl (iac .leftInv x)
leftInv (⊎Iso iac ibd) (inr x)  = cong inr (ibd .leftInv x)

⊎-swap-Iso : Iso (A ⊎ B) (B ⊎ A)
fun ⊎-swap-Iso (inl x) = inr x
fun ⊎-swap-Iso (inr x) = inl x
inv ⊎-swap-Iso (inl x) = inr x
inv ⊎-swap-Iso (inr x) = inl x
rightInv ⊎-swap-Iso (inl _) = refl
rightInv ⊎-swap-Iso (inr _) = refl
leftInv ⊎-swap-Iso (inl _)  = refl
leftInv ⊎-swap-Iso (inr _)  = refl

⊎-swap-≃ : A ⊎ B ≃ B ⊎ A
⊎-swap-≃ = isoToEquiv ⊎-swap-Iso

⊎-assoc-Iso : Iso ((A ⊎ B) ⊎ C) (A ⊎ (B ⊎ C))
fun ⊎-assoc-Iso (inl (inl x)) = inl x
fun ⊎-assoc-Iso (inl (inr x)) = inr (inl x)
fun ⊎-assoc-Iso (inr x)       = inr (inr x)
inv ⊎-assoc-Iso (inl x)       = inl (inl x)
inv ⊎-assoc-Iso (inr (inl x)) = inl (inr x)
inv ⊎-assoc-Iso (inr (inr x)) = inr x
rightInv ⊎-assoc-Iso (inl _)       = refl
rightInv ⊎-assoc-Iso (inr (inl _)) = refl
rightInv ⊎-assoc-Iso (inr (inr _)) = refl
leftInv ⊎-assoc-Iso (inl (inl _))  = refl
leftInv ⊎-assoc-Iso (inl (inr _))  = refl
leftInv ⊎-assoc-Iso (inr _)        = refl

⊎-assoc-≃ : (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc-≃ = isoToEquiv ⊎-assoc-Iso

⊎-⊥-Iso : Iso (A ⊎ ⊥) A
fun ⊎-⊥-Iso (inl x) = x
inv ⊎-⊥-Iso x       = inl x
rightInv ⊎-⊥-Iso x      = refl
leftInv ⊎-⊥-Iso (inl x) = refl

⊎-⊥-≃ : A ⊎ ⊥ ≃ A
⊎-⊥-≃ = isoToEquiv ⊎-⊥-Iso

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module Data.Word32 where

open import Data.Bool
open import Data.Char

{-#
  FOREIGN GHC

  import Data.Bits
  import Data.Word

  data Byte = Byte Bool Bool Bool Bool Bool Bool Bool Bool
  data Bytes = Bytes Byte Byte Byte Byte

  byteToWord8 :: Byte -> Word8
  byteToWord8 (Byte b0 b1 b2 b3 b4 b5 b6 b7) =
    boolToBit b0 0 + boolToBit b1 1 + boolToBit b2 2 + boolToBit b3 3 +
    boolToBit b4 4 + boolToBit b5 5 + boolToBit b6 6 + boolToBit b7 7
    where
      boolToBit b i = if b then bit i else 0

  word8ToByte :: Word8 -> Byte
  word8ToByte w =
    Byte
      (testBit w 0) (testBit w 1) (testBit w 2) (testBit w 3)
      (testBit w 4) (testBit w 5) (testBit w 6) (testBit w 7)

  bytesToWord32 :: Bytes -> Word32
  bytesToWord32 (Bytes b0 b1 b2 b3) =
    byteToWordShifted b0 0 + byteToWordShifted b1 1 + byteToWordShifted b2 2 + byteToWordShifted b3 3
    where
      byteToWordShifted :: Byte -> Int -> Word32
      byteToWordShifted b i = shift (fromIntegral $ byteToWord8 b) (i * 8)

  word32ToBytes :: Word32 -> Bytes
  word32ToBytes w = Bytes (getByte w 0) (getByte w 1) (getByte w 2) (getByte w 3)
    where
      getByte :: Word32 -> Int -> Byte
      getByte w i = word8ToByte $ fromIntegral (shift w (-i * 8))

  bytesToChar :: Bytes -> Char
  bytesToChar = toEnum . fromIntegral . bytesToWord32

  charToBytes :: Char -> Bytes
  charToBytes = word32ToBytes . fromIntegral . fromEnum
#-}

data Byte : Set where
  mkByte : Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Byte

data Word32 : Set where
  mkWord32 : Byte -> Byte -> Byte -> Byte -> Word32

{-# COMPILE GHC Byte = data Byte (Byte) #-}
{-# COMPILE GHC Word32 = data Bytes (Bytes) #-}

postulate
  bytesToChar : Word32 -> Char
  charToBytes : Char -> Word32

{-# COMPILE GHC bytesToChar = bytesToChar #-}
{-# COMPILE GHC charToBytes = charToBytes #-}

word32ToChar : Word32 -> Char
word32ToChar = bytesToChar

charToWord32 : Char -> Word32
charToWord32 = charToBytes

ext: agda

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers defined in terms of Data.Star
------------------------------------------------------------------------

module Data.Star.Nat where

open import Data.Star
open import Data.Unit
open import Function
open import Relation.Binary
open import Relation.Binary.Simple

-- Natural numbers.

ℕ : Set
ℕ = Star Always tt tt

-- Zero and successor.

zero : ℕ
zero = ε

suc : ℕ → ℕ
suc = _◅_ _

-- The length of a star-list.

length : ∀ {i t} {I : Set i} {T : Rel I t} {i j} → Star T i j → ℕ
length = gmap (const _) (const _)

-- Arithmetic.

infixl 7 _*_
infixl 6 _+_ _∸_

_+_ : ℕ → ℕ → ℕ
_+_ = _◅◅_

_*_ : ℕ → ℕ → ℕ
_*_ m = const m ⋆

_∸_ : ℕ → ℕ → ℕ
m       ∸ ε       = m
ε       ∸ (_ ◅ n) = zero
(_ ◅ m) ∸ (_ ◅ n) = m ∸ n

-- Some constants.

0# = zero
1# = suc 0#
2# = suc 1#
3# = suc 2#
4# = suc 3#
5# = suc 4#


text:
module Issue1496 where

open import Common.Unit
open import Common.String
open import Common.Char
open import Common.List
open import Common.IO

-- Agda infers that the "a" level argument to return has to be
-- Agda.Primitive.lzero.
main : IO Unit
main = return unit

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
--
-- In this module we conclude our proof: we have shown that t, derive-dterm t
-- and produce related values (in the sense of the fundamental property,
-- rfundamental3), and for related values v1, dv and v2 we have v1 ⊕ dv ≡
-- v2 (because ⊕ agrees with validity, rrelV3→⊕).
--
-- We now put these facts together via derive-correct-si and derive-correct.
-- This is immediate, even though I spend so much code on it:
-- Indeed, all theorems are immediate corollaries of what we established (as
-- explained above); only the statements are longer, especially because I bother
-- expanding them.

module Thesis.SIRelBigStep.DeriveCorrect where

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

open import Thesis.SIRelBigStep.IlcSILR
open import Thesis.SIRelBigStep.FundamentalProperty

-- Theorem statement. This theorem still mentions step-indexes explicitly.
derive-correct-si-type =
  ∀ {τ Γ k} (t : Term Γ τ) ρ1 dρ ρ2 → (ρρ : rrelρ3 Γ ρ1 dρ ρ2 k) →
  rrelT3-skeleton (λ v1 dv v2 _ → v1 ⊕ dv ≡ v2) t (derive-dterm t) t ρ1 dρ ρ2 k

-- A verified expansion of the theorem statement.
derive-correct-si-type-means :
  derive-correct-si-type ≡
  ∀ {τ Γ k} (t : Term Γ τ)
  ρ1 dρ ρ2 (ρρ : rrelρ3 Γ ρ1 dρ ρ2 k) →
  (v1 v2 : Val τ) →
  ∀ j (j<k : j < k) →
  (ρ1⊢t1↓[j]v1 : ρ1 ⊢ t ↓[ i' j ] v1) →
  (ρ2⊢t2↓[n2]v2 : ρ2 ⊢ t ↓[ no ] v2) →
  Σ[ dv ∈ DVal τ ]
  ρ1 D dρ ⊢ derive-dterm t ↓ dv ×
  v1 ⊕ dv ≡ v2
derive-correct-si-type-means = refl

derive-correct-si : derive-correct-si-type
derive-correct-si t ρ1 dρ ρ2 ρρ = rrelT3→⊕ t (derive-dterm t) t ρ1 dρ ρ2 (rfundamental3 _ t ρ1 dρ ρ2 ρρ)

-- Infinitely related environments:
rrelρ3-inf : ∀ Γ (ρ1 : ⟦ Γ ⟧Context) (dρ : ChΔ Γ) (ρ2 : ⟦ Γ ⟧Context) → Set
rrelρ3-inf Γ ρ1 dρ ρ2 = ∀ k → rrelρ3 Γ ρ1 dρ ρ2 k

-- A theorem statement for infinitely-related environments. On paper, if we informally
-- omit the arbitrary derivation step-index as usual, we get a statement without
-- step-indexes.
derive-correct :
  ∀ {τ Γ} (t : Term Γ τ)
  ρ1 dρ ρ2 (ρρ : rrelρ3-inf Γ ρ1 dρ ρ2) →
  (v1 v2 : Val τ) →
  ∀ j →
  (ρ1⊢t1↓[j]v1 : ρ1 ⊢ t ↓[ i' j ] v1) →
  (ρ2⊢t2↓[n2]v2 : ρ2 ⊢ t ↓[ no ] v2) →
  Σ[ dv ∈ DVal τ ]
  ρ1 D dρ ⊢ derive-dterm t ↓ dv ×
  v1 ⊕ dv ≡ v2
derive-correct t ρ1 dρ ρ2 ρρ v1 v2 j = derive-correct-si t ρ1 dρ ρ2 (ρρ (suc j)) v1 v2 j ≤-refl

open import Data.Unit

nilρ : ∀ {Γ n} (ρ : ⟦ Γ ⟧Context) → Σ[ dρ ∈ ChΔ Γ ] rrelρ3 Γ ρ dρ ρ n
nilV : ∀ {τ n} (v : Val τ) → Σ[ dv ∈ DVal τ ] rrelV3 τ v dv v n
nilV (closure t ρ) = let dρ , ρρ = nilρ ρ in dclosure (derive-dterm t) ρ dρ , rfundamental3svv _ (abs t) ρ dρ ρ ρρ
nilV (natV n₁) = dnatV zero , refl
nilV (pairV a b) = let 0a , aa = nilV a; 0b , bb = nilV b in dpairV 0a 0b , aa , bb

nilρ ∅ = ∅ , tt
nilρ (v • ρ) = let dv , vv = nilV v ; dρ , ρρ = nilρ ρ in dv • dρ , vv , ρρ

-- -- Try to prove to define validity-preserving change composition.
-- -- If we don't store proofs that environment changes in closures are valid, we
-- -- can't finish the proof for the closure case using the Fundamental property.
-- -- But it seems that's not the approach we need to use: we might need
-- -- environment validity elsewhere.
-- -- Moreover, the proof is annoying to do unless we build a datatype to invert
-- -- validity proofs (as suggested by Ezyang in
-- -- http://blog.ezyang.com/2013/09/induction-and-logical-relations/).

-- ocomposeρ : ∀ {Γ} n ρ1 dρ1 ρ2 dρ2 ρ3 → rrelρ3 Γ ρ1 dρ1 ρ2 n → rrelρ3 Γ ρ2 dρ2 ρ3 n → Σ[ dρ ∈ ChΔ Γ ] rrelρ3 Γ ρ1 dρ ρ3 n

-- ocomposev : ∀ {τ} n v1 dv1 v2 dv2 v3 → rrelV3 τ v1 dv1 v2 n → rrelV3 τ v2 dv2 v3 n → Σ[ dv ∈ DVal τ ] rrelV3 τ v1 dv v3 n
-- ocomposev n v1 dv1 v2 (bang v3) .v3 vv1 refl = bang v3 , refl
-- ocomposev n v1 (bang x) v2 (dclosure dt ρ dρ) v3 vv1 vv2 = {!!}
-- ocomposev n (closure t ρ) (dclosure .(derive-dterm t) .ρ dρ1) (closure .t .(ρ ⊕ρ dρ1)) (dclosure .(derive-dterm t) .(ρ ⊕ρ dρ1) dρ2) (closure .t .((ρ ⊕ρ dρ1) ⊕ρ dρ2)) ((refl , refl) , refl , refl , refl , refl , vv1) ((refl , refl) , refl , refl , refl , refl , vv2) =
--   let dρ , ρρ = ocomposeρ n ρ dρ1 (ρ ⊕ρ dρ1) dρ2 ((ρ ⊕ρ dρ1) ⊕ρ dρ2) {!!} {!!}
--   in dclosure (derive-dterm t) ρ dρ , (refl , refl) , refl , {!!} , refl , refl ,
--     λ { k (s≤s k≤n) v1 dv v2 vv →
--       let nilv2 , nilv2v = nilV v2
--       -- vv1 k ? v1 dv v2 vv
--       -- vv2 k ? v2 nilv2 v2 nilv2v
--       in {!!}
--       }
--       -- rfundamental3 k t (v1 • ρ) (dv • dρ) (v2 • ((ρ ⊕ρ dρ1) ⊕ρ dρ2)) (vv , rrelρ3-mono k n (≤-step k<n) _ ρ dρ ((ρ ⊕ρ dρ1) ⊕ρ dρ2) ρρ)}
-- -- p1 , p2 , p3 , p4 , p5
-- ocomposev n v1 dv1 v2 (dnatV n₁) v3 vv1 vv2 = {!!}
-- ocomposev n v1 dv1 v2 (dpairV dv2 dv3) v3 vv1 vv2 = {!!}
-- -- ocomposev n v1 (bang v2) .v2 dv2 v3 refl vv2 = bang (v2 ⊕ dv2) , rrelV3→⊕ v2 dv2 v3 vv2
-- -- ocomposev n v1 (dclosure dt ρ dρ) v2 dv2 v3 vv1 vv2 = {!!}
-- -- ocomposev n v1 (dnatV n₁) v2 dv2 v3 vv1 vv2 = {!!}
-- -- ocomposev n v1 (dpairV dv1 dv2) v2 dv3 v3 vv1 vv2 = {!!}
-- -- ocomposeV : ∀ {τ n} (v : Val τ) → Σ[ dv ∈ DVal τ ] rrelV3 τ v dv v n

-- ocomposeρ {∅} n ∅ dρ1 ρ2 dρ2 ∅ ρρ1 ρρ2 = ∅ , tt
-- ocomposeρ {τ • Γ} n (v1 • ρ1) (dv1 • dρ1) (v2 • ρ2) (dv2 • dρ2) (v3 • ρ3) (vv1 , ρρ1) (vv2 , ρρ2) =
--   let dv , vv = ocomposev n v1 dv1 v2 dv2 v3 vv1 vv2
--       dρ , ρρ = ocomposeρ n ρ1 dρ1 ρ2 dρ2 ρ3 ρρ1 ρρ2
--   in  dv • dρ , vv , ρρ

-- -- But we sort of know how to store environments validity proofs in closures, you just need to use well-founded inductions, even if you're using types. Sad, yes, that's insanely tedious. Let's leave that to Coq.
-- -- What is also interesting: if that were fixed, could we prove correct
-- -- composition for change *terms* and rrelT3? And for *open expressions*? The
-- -- last is the main problem Ahmed run into.

-- 1: the proof of transitivity of rrelT by Ahmed is for the case where the second rrelT holds at arbitrary step counts :-)
-- 2: that proof doesn't go through for us. If de1 : e1 -> e2 and de2 : e2 ->
-- e3, we must show that if e1 and e3 evaluate something happens, but to use our
-- hypothesis we need that e2 also terminates, which in our case does not
-- follow. For Ahmed 2006, instead, e1 terminates and e1 ≤ e2 implies that e2
-- terminates.
--
-- Indeed, it seems that we can have a change from e1 to looping e2 and a change
-- from looping e2 to e3, and I don't expect the composition of such changes to
-- satisfy anything.
--
-- Indeed, "Imperative self-adjusting computation" does not mention any
-- transitivity result (even in the technical report).

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --safe  #-}
module Cubical.HITs.SetCoequalizer where

open import Cubical.HITs.SetCoequalizer.Base public
open import Cubical.HITs.SetCoequalizer.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module datatype-util where
open import constants
open import ctxt
open import syntax-util
open import general-util
open import type-util
open import cedille-types
open import subst
open import rename
open import free-vars

{-# TERMINATING #-}
decompose-arrows : ctxt → type → params × type
decompose-arrows Γ (TpAbs me x atk T) =
  let x' = fresh-var-new Γ x in
  case decompose-arrows (ctxt-var-decl x' Γ) (rename-var Γ x x' T) of λ where
    (ps , T') → Param me x' atk :: ps , T'
decompose-arrows Γ T = [] , T

decompose-ctr-type : ctxt → type → type × params × 𝕃 tmtp
decompose-ctr-type Γ T with decompose-arrows Γ T
...| ps , Tᵣ with decompose-tpapps Tᵣ
...| Tₕ , as = Tₕ , ps , as

{-# TERMINATING #-}
kind-to-indices : ctxt → kind → indices
kind-to-indices Γ (KdAbs x atk k) =
  let x' = fresh-var-new Γ x in
  Index x' atk :: kind-to-indices (ctxt-var-decl x' Γ) (rename-var Γ x x' k)
kind-to-indices Γ _ = []

rename-indices-h : ctxt → renamectxt → indices → 𝕃 tmtp → indices
rename-indices-h Γ ρ (Index x atk :: is) (ty :: tys) =
  Index x' atk' ::
    rename-indices-h (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') is tys
  where
  x' = fresh-var-renamectxt Γ ρ (maybe-else x id (is-var-unqual ty))
  atk' = subst-renamectxt Γ ρ -tk atk
rename-indices-h Γ ρ (Index x atk :: is) [] =
  let x' = fresh-var-renamectxt Γ ρ x in
  Index x' (subst-renamectxt Γ ρ -tk atk) ::
    rename-indices-h (ctxt-var-decl x' Γ) (renamectxt-insert ρ x x') is []
rename-indices-h _ _ [] _ = []

rename-indices : ctxt → indices → 𝕃 tmtp → indices
rename-indices Γ = rename-indices-h Γ empty-renamectxt

positivity : Set
positivity = 𝔹 × 𝔹 -- occurs positively × occurs negatively

pattern occurs-nil = ff , ff
pattern occurs-pos = tt , ff
pattern occurs-neg = ff , tt
pattern occurs-all = tt , tt

--positivity-inc : positivity → positivity
--positivity-dec : positivity → positivity
positivity-neg : positivity → positivity
positivity-add : positivity → positivity → positivity

--positivity-inc = map-fst λ _ → tt
--positivity-dec = map-snd λ _ → tt
positivity-neg = uncurry $ flip _,_
positivity-add (+ₘ , -ₘ) (+ₙ , -ₙ) = (+ₘ || +ₙ) , (-ₘ || -ₙ)

-- just tt = negative occurrence; just ff = not in the return type; nothing = okay
module positivity (x : var) where

  open import conversion

  not-free : ∀ {ed} → ⟦ ed ⟧ → maybe 𝔹
  not-free = maybe-map (λ _ → tt) ∘' maybe-if ∘' is-free-in x

  if-free : ∀ {ed} → ⟦ ed ⟧ → positivity
  if-free t with is-free-in x t
  ...| f = f , f

  if-free-args : args → positivity
  if-free-args as with stringset-contains (free-vars-args as) x
  ...| f = f , f

  hnf' : ∀ {ed} → ctxt → ⟦ ed ⟧ → ⟦ ed ⟧
  hnf' Γ T = hnf Γ unfold-no-defs T

  mtt = maybe-else tt id
  mff = maybe-else ff id

  posₒ = fst
  negₒ = snd

  occurs : positivity → maybe 𝔹
  occurs p = maybe-if (negₒ p) >> just tt

  {-# TERMINATING #-}
  arrs+ : ctxt → type → maybe 𝔹
  type+ : ctxt → type → positivity
  kind+ : ctxt → kind → positivity
  tpkd+ : ctxt → tpkd → positivity
  tpapp+ : ctxt → type → positivity

  arrs+ Γ (TpAbs me x' atk T) =
    let Γ' = ctxt-var-decl x' Γ in
    occurs (tpkd+ Γ $ hnf' Γ -tk atk) maybe-or arrs+ Γ' (hnf' Γ' T)
  arrs+ Γ (TpApp T tT) = occurs (tpapp+ Γ $ hnf' Γ (TpApp T tT))
                       --arrs+ Γ T maybe-or (not-free -tT' tT)
  arrs+ Γ (TpLam x' atk T) =
    let Γ' = ctxt-var-decl x' Γ in
    occurs (tpkd+ Γ $ hnf' Γ -tk atk) maybe-or arrs+ Γ' (hnf' Γ' T)
  arrs+ Γ (TpVar x') = maybe-if (~ x =string x') >> just ff
  arrs+ Γ T = just ff

  type+ Γ (TpAbs me x' atk T) =
    let Γ' = ctxt-var-decl x' Γ in
    positivity-add (positivity-neg $ tpkd+ Γ $ hnf' Γ -tk atk) (type+ Γ' $ hnf' Γ' T)
  type+ Γ (TpIota x' T T') =
    let Γ' = ctxt-var-decl x' Γ in
    positivity-add (type+ Γ $ hnf' Γ T) (type+ Γ' $ hnf' Γ' T')
  type+ Γ (TpApp T tT) = tpapp+ Γ $ hnf' Γ $ TpApp T tT
  type+ Γ (TpEq tₗ tᵣ) = occurs-nil
  type+ Γ (TpHole _) = occurs-nil
  type+ Γ (TpLam x' atk T)=
    let Γ' = ctxt-var-decl x' Γ in
    positivity-add (positivity-neg $ tpkd+ Γ $ hnf' Γ -tk atk) (type+ Γ' (hnf' Γ' T))
  type+ Γ (TpVar x') = x =string x' , ff

  tpapp+ Γ T with decompose-tpapps T
  ...| TpVar x' , as =
    let f = if-free-args (tmtps-to-args NotErased as) in
    if x =string x'
      then positivity-add occurs-pos f
      else maybe-else' (data-lookup Γ x' as) f
        λ {(mk-data-info x'' xₒ'' asₚ asᵢ ps kᵢ k cs csₚₛ eds gds) →
          type+ Γ (hnf' Γ $ TpAbs tt x'' (Tkk k) $ foldr (uncurry λ cₓ cₜ → TpAbs ff ignored-var (Tkt cₜ)) (TpVar x'') (inst-ctrs Γ ps asₚ cs))}
  ...| _ , _ = if-free T

  kind+ Γ (KdAbs x' atk k) =
    let Γ' = ctxt-var-decl x' Γ in
    positivity-add (positivity-neg $ tpkd+ Γ $ hnf' Γ -tk atk) (kind+ Γ' k)
  kind+ Γ _ = occurs-nil

  tpkd+ Γ (Tkt T) = type+ Γ (hnf' Γ T)
  tpkd+ Γ (Tkk k) = kind+ Γ k

  ctr-positive : ctxt → type → maybe 𝔹
  ctr-positive Γ = arrs+ Γ ∘ hnf' Γ

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


text:
module DSyntax where

open import Data.List
open import Data.List.All
open import Data.Nat

open import Typing

data DExpr φ : Type → Set where
  var : ∀ {t}
      → (x : t ∈ φ)
      → DExpr φ t

  nat : (unr-φ : All Unr φ)
      → (i : ℕ)
      → DExpr φ TInt

  unit : (unr-φ : All Unr φ)
      → DExpr φ TUnit

  pair : ∀ {φ₁ φ₂ t₁ t₂}
    → (sp : Split φ φ₁ φ₂)
    → (e₁ : DExpr φ₁ t₁)
    → (e₂ : DExpr φ₂ t₂)
    → DExpr φ (TPair t₁ t₂)

  letpair : ∀ {φ₁ φ₂ t₁ t₂ t}
    → (sp : Split φ φ₁ φ₂)
    → (epair : DExpr φ₁ (TPair t₁ t₂))
    → (ebody : DExpr (t₁ ∷ t₂ ∷ φ₂) t)
    → DExpr φ t

  fork : (e : DExpr φ TUnit)
    → DExpr φ TUnit

  new : (unr-φ : All Unr φ)
      → (s : SType)
      → DExpr φ (TPair (TChan (SType.force s)) (TChan (SType.force (dual s))))

  send : ∀ {φ₁ φ₂ s t}
      → (sp : Split φ φ₁ φ₂)
      → (ech : DExpr φ₁ (TChan (send t s)))
      → (earg : DExpr φ₂ t)
      → DExpr φ (TChan (SType.force s))

  recv : ∀ {s t}
      → (ech : DExpr φ (TChan (recv t s)))
      → DExpr φ (TPair (TChan (SType.force s)) t)

  close : (ech : DExpr φ (TChan send!))
      → DExpr φ TUnit

  wait : (ech : DExpr φ (TChan send?))
      → DExpr φ TUnit

  select : ∀ {s₁ s₂}
      → (lab : Selector)
      → (ech : DExpr φ (TChan (sintern s₁ s₂)))
      → DExpr φ (TChan (selection lab (SType.force s₁) (SType.force s₂)))

  branch : ∀ {s₁ s₂ φ₁ φ₂ t}
      → (sp : Split φ φ₁ φ₂)
      → (ech : DExpr φ₁ (TChan (sextern s₁ s₂)))
      → (eleft : DExpr (TChan (SType.force s₁) ∷ φ₂) t)
      → (erght : DExpr (TChan (SType.force s₂) ∷ φ₂) t)
      → DExpr φ t

  ulambda : ∀ {t₁ t₂}
      → (unr-φ : All Unr φ)
      → (ebody : DExpr (t₁ ∷ φ) t₂)
      → DExpr φ (TFun UU t₁ t₂)

  llambda : ∀ {t₁ t₂}
      → (ebody : DExpr (t₁ ∷ φ) t₂)
      → DExpr φ (TFun LL t₁ t₂)

  app : ∀ {φ₁ φ₂ lu t₁ t₂}
      → (sp : Split φ φ₁ φ₂)
      → (efun : DExpr φ₁ (TFun lu t₁ t₂))
      → (earg : DExpr φ₂ t₁)
      → DExpr φ t₂

  subsume : ∀ {t₁ t₂}
      → (e : DExpr φ t₁)
      → (t≤t' : SubT t₁ t₂)
      → DExpr φ t₂

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
module Max where

open import Data.Empty using (⊥-elim)
open import Data.Fin
open import Data.Nat hiding (_≤_)
open import Function using (_∘_)

open import Relation.Nullary

variable
  n : ℕ

-- from https://github.com/zmthy/recursive-types/tree/ftfjp16
-- RecursiveTypes.Inductive.Type
-- adapted to use "variable"

-- A proposition that the indexed number is the largest it can be, i.e. one less
-- than its exclusive upper bound.
data Max : Fin n → Set where
  max : Max {suc n} (fromℕ n)

-- A lemma on Max: if a number is max, then one less than that number with a
-- simultaneously lowered upper bound is also max.
max-pre : {x : Fin (suc n)} → Max (suc x) → Max x
max-pre max = max

-- A lemma on Max: if a number is max, then one more than that number with a
-- simultaneously increased upper bound is also max.
max-suc : {x : Fin n} → Max x → Max (suc x)
max-suc max = max

-- Given a proof that a number is not max, reduce its lower bound by one,
-- keeping the value of the number the same.
reduce : {x : Fin (suc n)} → ¬ Max x → Fin n
reduce {zero}  {zero}   ¬p = ⊥-elim (¬p max)
reduce {zero}  {suc ()} ¬p
reduce {suc n} {zero}   ¬p = zero
reduce {suc n} {suc x}  ¬p = suc (reduce {x = x} (¬p ∘ max-suc))

-- Max is a decidable proposition: just compare the number value to the value of
-- the upper bound.
max? : (x : Fin n) → Dec (Max x)
max? {zero}        ()
max? {suc zero}    zero     = yes max
max? {suc zero}    (suc ())
max? {suc (suc n)} zero     = no (λ ())
max? {suc (suc n)} (suc x)  with max? x
max? {suc (suc n)} (suc .(fromℕ n)) | yes max = yes max
max? {suc (suc n)} (suc x)          | no ¬p = no (¬p ∘ max-pre)

-- The reduce function preserves ≤.
reduce₁ : ∀ {m} {x : Fin n} (¬p : ¬ Max (suc x))
          → m ≤ x → suc m ≤ inject₁ (reduce ¬p)
reduce₁ {m = zero} ¬p₁ z≤n = s≤s z≤n
reduce₁ {m = suc m} {zero} ¬p ()
reduce₁ {m = suc m₁} {suc x₁} ¬p₁ (s≤s q₁) =
  s≤s (reduce₁ (λ z → ¬p₁ (max-suc z)) q₁)

-- Injection is compatible with ordering.
inject-≤ : {i j : Fin n} → inject₁ i ≤ inject₁ j → i ≤ j
inject-≤ {i = 0F} {0F} z≤n = z≤n
inject-≤ {i = 0F} {suc j} z≤n = z≤n
inject-≤ {i = suc i} {0F} ()
inject-≤ {i = suc i} {suc j} (s≤s ii≤ij) = s≤s (inject-≤ ii≤ij)

-- Technical lemma about reduce.
lemma-reduce : {i j : Fin (suc n)} →
  (i≤j : inject₁ i ≤ inject₁ j) → (¬p  : ¬ Max j) → i ≤ inject₁ (reduce ¬p)
lemma-reduce {i = 0F} i≤j ¬p = z≤n
lemma-reduce {i = suc i} {suc j} (s≤s i≤j) ¬p = reduce₁ ¬p (inject-≤ i≤j)

-- A lemma on ≤: if x ≤ y, then x ≤ suc y.
suc-≤ : {x y : Fin n} → x ≤ y → inject₁ x ≤ suc y
suc-≤ {x = zero} z≤n = z≤n
suc-≤ {x = suc x} {zero} ()
suc-≤ {x = suc x} {suc y} (s≤s p) = s≤s (suc-≤ p)

-- A lemma on ≤: if suc x ≤ y, then x ≤ y.
pred-≤ : {x y : Fin n} → suc x ≤ inject₁ y → inject₁ x ≤ inject₁ y
pred-≤ {y = zero} ()
pred-≤ {y = suc x} (s≤s p) = suc-≤ p

-- A lemma on ≤: if x ≤ y, then for any z < x, z ≤ y.
trans-< : {x y : Fin n} {z : Fin′ x} → x ≤ y → inject z ≤ y
trans-< {x = zero} {z = ()} p
trans-< {x = suc x} {zero} ()
trans-< {x = suc x} {suc y} {zero} (s≤s p) = z≤n
trans-< {x = suc x} {suc y} {suc z} (s≤s p) = s≤s (trans-< p)

max_stars_repo_name: kcaliban/dual-session

max_issues_repo_name: kcaliban/dual-session

max_forks_repo_name: kcaliban/dual-session


text:
{-

This file contains a summary of the proof that π₄(S³) ≡ ℤ/2ℤ

The --experimental-lossy-unification flag is used to speed up type checking.
The file still type checks without it, but it's a lot slower (about 10 times).

-}
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Group.Pi4S3.Summary where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed

open import Cubical.Data.Nat.Base
open import Cubical.Data.Sigma.Base

open import Cubical.HITs.Sn
open import Cubical.HITs.SetTruncation

open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.HopfInvariant.Homomorphism
open import Cubical.Homotopy.HopfInvariant.HopfMap
open import Cubical.Homotopy.HopfInvariant.Brunerie
open import Cubical.Homotopy.Whitehead
open import Cubical.Homotopy.Group.Base hiding (π)
open import Cubical.Homotopy.Group.Pi3S2
open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Instances.Bool
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.GroupPath
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.Instances.IntMod
open import Cubical.Algebra.Group.ZAction

-- Homotopy groups (shifted version of π'Gr to get nicer numbering)
π : ℕ → Pointed₀ → Group₀
π n X = π'Gr (predℕ n) X

-- Nicer notation for the spheres (as pointed types)
𝕊² 𝕊³ : Pointed₀
𝕊² = S₊∙ 2
𝕊³ = S₊∙ 3

-- The Brunerie number; defined in Cubical.Homotopy.Group.Pi4S3.BrunerieNumber
-- as "abs (HopfInvariant-π' 0 ([ (∣ idfun∙ _ ∣₂ , ∣ idfun∙ _ ∣₂) ]×))"
β : ℕ
β = Brunerie

-- The connection to π₄(S³) is then also proved in the BrunerieNumber
-- file following Corollary 3.4.5 in Guillaume Brunerie's PhD thesis.
βSpec : GroupEquiv (π 4 𝕊³) (ℤGroup/ β)
βSpec = BrunerieIso

-- Ideally one could prove that β is 2 by normalization, but this does
-- not seem to terminate before we run out of memory. To try normalize
-- this use "C-u C-c C-n β≡2" (which normalizes the term, ignoring
-- abstract's). So instead we prove this by hand as in the second half
-- of Guillaume's thesis.
β≡2 : β ≡ 2
β≡2 = Brunerie≡2

-- This involves a lot of theory, for example that π₃(S²) ≃ ℤGroup where
-- the underlying map is induced by the Hopf invariant (which involves
-- the cup product on cohomology).
_ : GroupEquiv (π 3 𝕊²) ℤGroup
_ = hopfInvariantEquiv

-- Which is a consequence of the fact that π₃(S²) is generated by the
-- Hopf map.
_ : gen₁-by (π 3 𝕊²) ∣ HopfMap ∣₂
_ = π₂S³-gen-by-HopfMap

-- etc. For more details see the proof of "Brunerie≡2".

-- Combining all of this gives us the desired equivalence of groups:
π₄S³≃ℤ/2ℤ : GroupEquiv (π 4 𝕊³) (ℤGroup/ 2)
π₄S³≃ℤ/2ℤ = subst (GroupEquiv (π 4 𝕊³)) (cong ℤGroup/_ β≡2) βSpec

-- By the SIP this induces an equality of groups:
π₄S³≡ℤ/2ℤ : π 4 𝕊³ ≡ ℤGroup/ 2
π₄S³≡ℤ/2ℤ = GroupPath _ _ .fst π₄S³≃ℤ/2ℤ

-- As a sanity check we also establish the equality with Bool:
π₄S³≡Bool : π 4 𝕊³ ≡ BoolGroup
π₄S³≡Bool = π₄S³≡ℤ/2ℤ ∙ GroupPath _ _ .fst (GroupIso→GroupEquiv ℤGroup/2≅Bool)

max_stars_repo_name: xekoukou/cubical

max_issues_repo_name: xekoukou/cubical

max_forks_repo_name: xekoukou/cubical


text:
module BasicIS4.Metatheory.Hilbert-TarskiClosedOvergluedImplicit where

open import BasicIS4.Syntax.Hilbert public
open import BasicIS4.Semantics.TarskiClosedOvergluedImplicit public

open ImplicitSyntax (∅ ⊢_) public

-- Completeness with respect to a particular model, for closed terms only.

module _ {{_ : Model}} where
  reify : ∀ {A} → ⊩ A → ∅ ⊢ A
  reify {α P}   s = syn s
  reify {A ▻ B} s = syn s
  reify {□ A}   s = syn s
  reify {A ∧ B} s = pair (reify (π₁ s)) (reify (π₂ s))
  reify {⊤}    s = unit

-- Additional useful equipment.

module _ {{_ : Model}} where
  ⟪K⟫ : ∀ {A B} → ⊩ A → ⊩ B ▻ A
  ⟪K⟫ a = app ck (reify a) ⅋ K a

  ⟪S⟫′ : ∀ {A B C} → ⊩ A ▻ B ▻ C → ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ s₁ = app cs (reify s₁) ⅋ λ s₂ →
              app (app cs (reify s₁)) (reify s₂) ⅋ ⟪S⟫ s₁ s₂

  _⟪D⟫_ : ∀ {A B} → ⊩ □ (A ▻ B) → ⊩ □ A → ⊩ □ B
  (t ⅋ s) ⟪D⟫ (u ⅋ a) = app (app cdist t) u ⅋ s ⟪$⟫ a

  _⟪D⟫′_ : ∀ {A B} → ⊩ □ (A ▻ B) → ⊩ □ A ▻ □ B
  _⟪D⟫′_ s = app cdist (reify s) ⅋ _⟪D⟫_ s

  ⟪↑⟫ : ∀ {A} → ⊩ □ A → ⊩ □ □ A
  ⟪↑⟫ s = box (syn s) ⅋ s

  _⟪,⟫′_ : ∀ {A B} → ⊩ A → ⊩ B ▻ A ∧ B
  _⟪,⟫′_ a = app cpair (reify a) ⅋ _,_ a

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  _⟦D⟧_ : ∀ {A B Γ} → ⊩ Γ ⇒ □ (A ▻ B) → ⊩ Γ ⇒ □ A → ⊩ Γ ⇒ □ B
  (s₁ ⟦D⟧ s₂) γ = (s₁ γ) ⟪D⟫ (s₂ γ)

  ⟦↑⟧ : ∀ {A Γ} → ⊩ Γ ⇒ □ A → ⊩ Γ ⇒ □ □ A
  ⟦↑⟧ s γ = ⟪↑⟫ (s γ)

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)   γ = lookup i γ
eval (app t u) γ = eval t γ ⟪$⟫ eval u γ
eval ci        γ = ci ⅋ I
eval ck        γ = ck ⅋ ⟪K⟫
eval cs        γ = cs ⅋ ⟪S⟫′
eval (box t)   γ = box t ⅋ eval t ∙
eval cdist     γ = cdist ⅋ _⟪D⟫′_
eval cup       γ = cup ⅋ ⟪↑⟫
eval cdown     γ = cdown ⅋ ⟪↓⟫
eval cpair     γ = cpair ⅋ _⟪,⟫′_
eval cfst      γ = cfst ⅋ π₁
eval csnd      γ = csnd ⅋ π₂
eval unit      γ = ∙

-- Correctness of evaluation with respect to conversion.

eval✓ : ∀ {{_ : Model}} {A Γ} {t t′ : Γ ⊢ A} → t ⋙ t′ → eval t ≡ eval t′
eval✓ refl⋙                   = refl
eval✓ (trans⋙ p q)            = trans (eval✓ p) (eval✓ q)
eval✓ (sym⋙ p)                = sym (eval✓ p)
eval✓ (congapp⋙ p q)          = cong² _⟦$⟧_ (eval✓ p) (eval✓ q)
eval✓ (congi⋙ p)              = cong I (eval✓ p)
eval✓ (congk⋙ p q)            = cong² K (eval✓ p) (eval✓ q)
eval✓ (congs⋙ p q r)          = cong³ ⟦S⟧ (eval✓ p) (eval✓ q) (eval✓ r)
eval✓ (congdist⋙ p q)         = cong² _⟦D⟧_ (eval✓ p) (eval✓ q)
eval✓ (congup⋙ p)             = cong ⟦↑⟧ (eval✓ p)
eval✓ (congdown⋙ p)           = cong ⟦↓⟧ (eval✓ p)
eval✓ (congpair⋙ {A} {B} p q) = cong² (_⟦,⟧_ {A} {B}) (eval✓ p) (eval✓ q)
eval✓ (congfst⋙ {A} {B} p)    = cong (⟦π₁⟧ {A} {B}) (eval✓ p)
eval✓ (congsnd⋙ {A} {B} p)    = cong (⟦π₂⟧ {A} {B}) (eval✓ p)
eval✓ beta▻ₖ⋙                 = refl
eval✓ beta▻ₛ⋙                 = refl
eval✓ beta∧₁⋙                 = refl
eval✓ beta∧₂⋙                 = refl
eval✓ eta∧⋙                   = refl
eval✓ eta⊤⋙                  = refl

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { ⊩ᵅ_ = λ P → ∅ ⊢ α P
      }

-- Completeness with respect to all models, or quotation, for closed terms only.

quot₀ : ∀ {A} → ∅ ⊨ A → ∅ ⊢ A
quot₀ t = reify (t ∙)

-- Normalisation by evaluation, for closed terms only.

norm₀ : ∀ {A} → ∅ ⊢ A → ∅ ⊢ A
norm₀ = quot₀ ∘ eval

-- TODO: Correctness of normalisation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence
open import HoTT.Identity

module HoTT.Identity.NaturalNumber where

private variable m n : ℕ

_=ℕ_ : ℕ → ℕ → 𝒰₀
zero =ℕ zero = 𝟏
zero =ℕ (succ _) = 𝟎
succ _ =ℕ zero = 𝟎
succ m =ℕ succ n = m =ℕ n

private
  r : (n : ℕ) → n =ℕ n
  r zero = ★
  r (succ n) = r n

=ℕ-elim : m == n → m =ℕ n
=ℕ-elim {m} p = transport (m =ℕ_) p (r m)

=ℕ-intro : m =ℕ n → m == n
=ℕ-intro {zero} {zero} _ = refl
=ℕ-intro {zero} {succ n} ()
=ℕ-intro {succ m} {zero} ()
=ℕ-intro {succ m} {succ n} = ap succ ∘ =ℕ-intro

=ℕ-equiv : {m n : ℕ} → m == n ≃ m =ℕ n
=ℕ-equiv {x} = f , qinv→isequiv (g , η , ε {x})
  where
  f = =ℕ-elim
  g = =ℕ-intro

  η : g ∘ f {m} {n} ~ id
  η {zero} refl = refl
  η {succ n} refl = ap (ap succ) (η refl)

  ε : f ∘ g {m} {n} ~ id
  ε {zero} {zero} ★ = refl
  ε {zero} {succ n} ()
  ε {succ m} {zero} ()
  ε {succ m} {succ n} p = transport-ap (succ m =ℕ_) succ (g p) (r m) ∙ ε {m} p

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module Common.Reflect where

open import Common.Level
open import Common.Prelude renaming (Nat to ℕ)

postulate QName : Set
{-# BUILTIN QNAME QName #-}
primitive primQNameEquality : QName → QName → Bool

data Hiding : Set where
  hidden visible instance : Hiding

{-# BUILTIN HIDING   Hiding   #-}
{-# BUILTIN HIDDEN   hidden   #-}
{-# BUILTIN VISIBLE  visible  #-}
{-# BUILTIN INSTANCE instance #-}

-- relevant    the argument is (possibly) relevant at compile-time
-- irrelevant  the argument is irrelevant at compile- and runtime
data Relevance : Set where
  relevant irrelevant : Relevance

{-# BUILTIN RELEVANCE  Relevance  #-}
{-# BUILTIN RELEVANT   relevant   #-}
{-# BUILTIN IRRELEVANT irrelevant #-}

data ArgInfo : Set where
  arginfo : Hiding → Relevance → ArgInfo

data Arg A : Set where
  arg : ArgInfo → A → Arg A

{-# BUILTIN ARGINFO    ArgInfo #-}
{-# BUILTIN ARG        Arg     #-}
{-# BUILTIN ARGARG     arg     #-}
{-# BUILTIN ARGARGINFO arginfo #-}

mutual

  Args : Set

  data Type : Set
  data Sort : Set

  data Term : Set where
    var     : ℕ → Args → Term
    con     : QName → Args → Term
    def     : QName → Args → Term
    lam     : Hiding → Term → Term
    pi      : Arg Type → Type → Term
    sort    : Sort → Term
    unknown : Term

  Args = List (Arg Term)

  data Type where
    el : Sort → Term → Type

  data Sort where
    set     : Term → Sort
    lit     : ℕ → Sort
    unknown : Sort

{-# BUILTIN AGDASORT            Sort    #-}
{-# BUILTIN AGDATERM            Term    #-}
{-# BUILTIN AGDATYPE            Type    #-}
{-# BUILTIN AGDATERMVAR         var     #-}
{-# BUILTIN AGDATERMCON         con     #-}
{-# BUILTIN AGDATERMDEF         def     #-}
{-# BUILTIN AGDATERMLAM         lam     #-}
{-# BUILTIN AGDATERMPI          pi      #-}
{-# BUILTIN AGDATERMSORT        sort    #-}
{-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
{-# BUILTIN AGDATYPEEL          el      #-}
{-# BUILTIN AGDASORTSET         set     #-}
{-# BUILTIN AGDASORTLIT         lit     #-}
{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}

postulate
  FunDef    : Set
  DataDef   : Set
  RecordDef : Set

{-# BUILTIN AGDAFUNDEF          FunDef  #-}
{-# BUILTIN AGDADATADEF         DataDef #-}
{-# BUILTIN AGDARECORDDEF       RecordDef #-}

data Definition : Set where
  funDef          : FunDef    → Definition
  dataDef         : DataDef   → Definition
  recordDef       : RecordDef → Definition
  dataConstructor : Definition
  axiom           : Definition
  prim            : Definition

{-# BUILTIN AGDADEFINITION                Definition      #-}
{-# BUILTIN AGDADEFINITIONFUNDEF          funDef          #-}
{-# BUILTIN AGDADEFINITIONDATADEF         dataDef         #-}
{-# BUILTIN AGDADEFINITIONRECORDDEF       recordDef       #-}
{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR dataConstructor #-}
{-# BUILTIN AGDADEFINITIONPOSTULATE       axiom           #-}
{-# BUILTIN AGDADEFINITIONPRIMITIVE       prim            #-}

primitive
  primQNameType         : QName → Type
  primQNameDefinition   : QName → Definition
--primFunClauses        : FunDef → List Clause
  primDataConstructors  : DataDef   → List QName
--primRecordConstructor : RecordDef → QName
--primRecordFields      : RecordDef → List QName

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module FreeReader where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Function.Base using (id; _$_)

open import Class
open Functor

variable
  A B C : Set

-- The Reader monad, as a free monad
data FreeReader (R : Set) : Set → Set₁ where
  Pure : A → FreeReader R A
  Bind : FreeReader R A → (A → FreeReader R B) → FreeReader R B
  Ask : FreeReader R R

  -- Monad laws
  LeftId : ∀ {A B}
    → (a : A)
    → (f : A → FreeReader R B)
    → Bind (Pure a) f ≡ f a
  RightId : ∀ {A}
    → (m : FreeReader R A)
    → Bind m Pure ≡ m
  Assoc : ∀ {A B C}
    → (m : FreeReader R A)
    → (f : A → FreeReader R B)
    → (g : B → FreeReader R C)
    → Bind (Bind m f) g ≡ Bind m (λ x → Bind (f x) g)

freereader-functor : ∀ {R} → Functor (FreeReader R)
freereader-functor .fmap f m = Bind m (Pure ∘ f)
freereader-functor .fmap-id-legit m i = RightId m i
freereader-functor .fmap-compose-legit m f g i
  = hcomp (λ j → λ { (i = i0) → Bind m (Pure ∘ f ∘ g)
                   ; (i = i1) → Assoc m (Pure ∘ g) (Pure ∘ f) (~ j)
                   })
          (Bind m (λ x → LeftId (g x) (Pure ∘ f) (~ i)))

freereader-ap : ∀ {R} → Applicative (FreeReader R)
freereader-ap .Applicative.functor = freereader-functor
freereader-ap .Applicative.pure = Pure
freereader-ap .Applicative._<*>_ mf m = Bind mf (λ f → Bind m (Pure ∘ f))
freereader-ap .Applicative.app-identity v i
  = hcomp (λ j → λ { (i = i0) → LeftId id (λ f → Bind v (Pure ∘ f)) (~ j)
                   ; (i = i1) → v
                   })
          (RightId v i)
freereader-ap .Applicative.app-compose u v w
  -- For some reason, Agda doesn't like wildcards in cubical proofs. Oh well.
        = Pure _∘_ <*> u <*> v <*> w
  ≡[ i ]⟨ LeftId _∘_ (λ f → Bind u (Pure ∘ f)) i <*> v <*> w ⟩
          Bind u (λ u' → Pure (u' ∘_)) <*> v <*> w
  ≡[ i ]⟨ Assoc u (λ u' → Pure (u' ∘_)) (λ f → Bind v (Pure ∘ f)) i <*> w ⟩
          Bind u (λ u' → Bind (Pure (u' ∘_)) (λ c → Bind v (Pure ∘ c))) <*> w
  ≡[ i ]⟨ Bind u (λ u' → LeftId (u' ∘_) (λ c → Bind v (Pure ∘ c)) i) <*> w ⟩
          Bind u (λ u' → Bind v (λ v' → Pure (u' ∘ v'))) <*> w
  ≡[ i ]⟨ Assoc u (λ u' → Bind v (λ v' → Pure (u' ∘ v'))) (λ f → Bind w (Pure ∘ f)) i ⟩
          Bind u (λ u' → Bind (Bind v (λ v' → Pure (u' ∘ v'))) (λ f → Bind w (Pure ∘ f)))
  ≡[ i ]⟨ Bind u (λ u' → Assoc v (λ v' → Pure (u' ∘ v')) (λ f → Bind w (Pure ∘ f)) i) ⟩
          Bind u (λ u' → Bind v (λ v' → Bind (Pure (u' ∘ v')) (λ f → Bind w (Pure ∘ f))))
  ≡[ i ]⟨ Bind u (λ u' → Bind v (λ v' → LeftId (u' ∘ v') (λ f → Bind w (Pure ∘ f)) i)) ⟩
          Bind u (λ u' → Bind v (λ v' → Bind w (Pure ∘ u' ∘ v')))
  ≡[ i ]⟨ Bind u (λ u' → Bind v (λ v' → Bind w (λ w' → LeftId (v' w') (Pure ∘ u') (~ i)))) ⟩
          Bind u (λ u' → Bind v (λ v' → Bind w (λ w' → Bind (Pure (v' w')) (Pure ∘ u'))))
  ≡[ i ]⟨ Bind u (λ u' → Bind v (λ v' → Assoc w (Pure ∘ v') (Pure ∘ u') (~ i))) ⟩
          Bind u (λ u' → Bind v (λ v' → Bind (Bind w (Pure ∘ v')) (Pure ∘ u')))
  ≡[ i ]⟨ Bind u (λ u' → Assoc v (λ f → Bind w (Pure ∘ f)) (Pure ∘ u') (~ i)) ⟩
          Bind u (λ u' → Bind (Bind v (λ v' → Bind w (Pure ∘ v'))) (Pure ∘ u'))
          ∎
  where open Applicative freereader-ap
freereader-ap .Applicative.app-homo f x
  = LeftId f (λ f' → Bind (Pure x) (λ x' → Pure (f' x')))
  ∙ LeftId x (λ x' → Pure (f x'))
freereader-ap .Applicative.app-intchg u y
          -- u <*> pure y
        = Bind u (λ u' → Bind (Pure y) (Pure ∘ u'))
  ≡[ i ]⟨ Bind u (λ u' → LeftId y (Pure ∘ u') i) ⟩
          Bind u (λ u' → Pure (u' y))
  ≡[ i ]⟨ LeftId (_$ y) (λ f → Bind u (Pure ∘ f)) (~ i) ⟩
          Bind (Pure (_$ y)) (λ _y' → Bind u (λ u' → Pure (u' y')))
          -- pure (_$ y) <*> u
          ∎

freereader-monad : ∀ {R} → Monad (FreeReader R)
freereader-monad .Monad.applicative    = freereader-ap
freereader-monad .Monad._>>=_          = Bind
freereader-monad .Monad.monad-left-id  = LeftId
freereader-monad .Monad.monad-right-id = RightId
freereader-monad .Monad.monad-assoc    = Assoc


text:
module Ids where

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

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

-- The example above is based on one in "Implementing Typed
-- Intermediate Languages" by Shao, League and Monnier.


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

open import 17-number-theory
open import Cubical.Core.Everything

data circle-C : UU lzero where
  base : circle-C
  loop : Path circle-C base base

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


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

module Cubical.HITs.Modulo.FinEquiv where

open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude

open import Cubical.Data.Fin
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order

open import Cubical.HITs.Modulo.Base

-- For positive `k`, every `Modulo k` can be reduced to its
-- residue modulo `k`, given by a value of type `Fin k`. This
-- forms an equivalence between `Fin k` and `Modulo k`.
module Reduction {k₀ : ℕ} where
  private
    k = suc k₀

  fembed : Fin k → Modulo k
  fembed = embed ∘ toℕ

  ResiduePath : ℕ → Type₀
  ResiduePath n =  Σ[ f ∈ Fin k ] fembed f ≡ embed n

  rbase : ∀ n (n<k : n < k) → ResiduePath n
  rbase n n<k = (n , n<k) , refl

  rstep : ∀ n → ResiduePath n → ResiduePath (k + n)
  rstep n (f , p) = f , p ∙ step n

  rstep≡
    : ∀ n (R : ResiduePath n)
    → PathP (λ i → fembed (fst R) ≡ step n i) (snd R) (snd (rstep n R))
  rstep≡ n (f , p) = λ i j → compPath-filler p (step n) i j

  residuePath : ∀ n → ResiduePath n
  residuePath = +induction k₀ ResiduePath rbase rstep

  lemma₁ : ∀ n → rstep n (residuePath n) ≡ residuePath (k + n)
  lemma₁ = sym ∘ +inductionStep k₀ ResiduePath rbase rstep

  residueStep₁
    : ∀ n →  fst (residuePath n) ≡ fst (residuePath (k + n))
  residueStep₁ = cong fst ∘ lemma₁

  residueStep₂
    : ∀ n → PathP (λ i → fembed (residueStep₁ n i) ≡ step n i)
              ((snd ∘ residuePath) n)
              ((snd ∘ residuePath) (k + n))
  residueStep₂ n i j
    = hfill (λ ii → λ
            { (i = i0) → snd (residuePath n) j
            ; (j = i0) → fembed (residueStep₁ n (i ∧ ii))
            ; (i = i1) → snd (lemma₁ n ii) j
            ; (j = i1) → step n i
            })
        (inS (rstep≡ n (residuePath n) i j))
        i1

  residue : Modulo k → Fin k
  residue (embed n) = fst (residuePath n)
  residue (step n i) = residueStep₁ n i

  sect : section residue fembed
  sect (r , r<k) = cong fst (+inductionBase k₀ ResiduePath rbase rstep r r<k)

  retr : retract residue fembed
  retr (embed n) = snd (residuePath n)
  retr (step n i) = residueStep₂ n i

  Modulo≡Fin : Modulo k ≡ Fin k
  Modulo≡Fin = isoToPath (iso residue fembed sect retr)

open Reduction using (fembed; residue; Modulo≡Fin) public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Identity
open import HoTT.Equivalence
open import HoTT.Homotopy

module HoTT.Identity.Identity where

ap⁻¹ : ∀ {i j} {A : 𝒰 i} {B : 𝒰 j} ((f , _) : A ≃ B) {a a' : A} →
       f a == f a' → a == a'
ap⁻¹ e {a} {a'} p = η a ⁻¹ ∙ ap g p ∙ η a'
  where open Iso (eqv→iso e)

-- Theorem 2.11.1
ap≃ : ∀ {i j} {A : 𝒰 i} {B : 𝒰 j} →
      ((f , _) : A ≃ B) → (a a' : A) → (a == a') ≃ (f a == f a')
ap≃ e a a' = iso→eqv iso
  where
  open Iso (eqv→iso e)
  iso : Iso _ _
  Iso.f iso = ap f
  Iso.g iso = ap⁻¹ e
  Iso.η iso p =
    η a ⁻¹ ∙ ap g (ap f p) ∙ η a'   =⟨ _ ∙ₗ ap-∘ g f p ⁻¹ ∙ᵣ _ ⟩
    η a ⁻¹ ∙ ap (g ∘ f) p ∙ η a'    =⟨ assoc ⁻¹ ⟩
    η a ⁻¹ ∙ (ap (g ∘ f) p ∙ η a')  =⟨ pivotₗ (~-natural-id η p) ⁻¹ ⟩
    p                               ∎
    where open =-Reasoning
  Iso.ε iso q =
    ap f (η a ⁻¹ ∙ ap g q ∙ η a')                 =⟨ pivotₗ (~-natural (ε ∘ f) _) ⟩
    ε (f a) ⁻¹ ∙ (ap (f ∘ g ∘ f) _ ∙ ε (f a'))    =⟨ _ ∙ₗ (ap-∘ f (g ∘ f) _ ∙ᵣ _) ⟩
    ε (f a) ⁻¹ ∙ (ap f (ap (g ∘ f) _) ∙ ε (f a')) =⟨ ap (λ p → _ ∙ (ap f p ∙ _)) inner ⟩
    ε (f a) ⁻¹ ∙ (ap f (ap g q) ∙ ε (f a'))       =⟨ _ ∙ₗ (ap-∘ f g q ⁻¹ ∙ᵣ _) ⟩
    ε (f a) ⁻¹ ∙ (ap (f ∘ g) q ∙ ε (f a'))        =⟨ pivotₗ (~-natural-id ε q) ⁻¹ ⟩
    q                                             ∎
    where
    open =-Reasoning
    inner : ap (g ∘ f) (η a ⁻¹ ∙ ap g q ∙ η a') == ap g q
    inner =
      ap (g ∘ f) (η a ⁻¹ ∙ ap g q ∙ η a')      =⟨ pivotᵣ (~-natural-id η _ ⁻¹) ⟩
      η a ∙ (η a ⁻¹ ∙ ap g q ∙ η a') ∙ η a' ⁻¹ =⟨ assoc ∙ᵣ η a' ⁻¹ ⟩
      η a ∙ (η a ⁻¹ ∙ ap g q) ∙ η a' ∙ η a' ⁻¹ =⟨ assoc ∙ᵣ _ ∙ᵣ _ ⟩
      η a ∙ η a ⁻¹ ∙ ap g q ∙ η a' ∙ η a' ⁻¹   =⟨ invᵣ ∙ᵣ _ ∙ᵣ _ ∙ᵣ _ ⟩
      refl ∙ ap g q ∙ η a' ∙ η a' ⁻¹           =⟨ unitₗ ⁻¹ ∙ᵣ _ ∙ᵣ _ ⟩
      ap g q ∙ η a' ∙ η a' ⁻¹                  =⟨ assoc ⁻¹ ⟩
      ap g q ∙ (η a' ∙ η a' ⁻¹)                =⟨ _ ∙ₗ invᵣ ⟩
      ap g q ∙ refl                            =⟨ unitᵣ ⁻¹ ⟩
      ap g q                                   ∎

-- Theorem 2.11.3
=-transport : ∀ {i j} {A : 𝒰 i} {B : 𝒰 j} {a a' : A}
                (f g : A → B) (p : a == a') (q : f a == g a) →
                transport (λ x → f x == g x) p q == ap f p ⁻¹ ∙ q ∙ ap g p
=-transport _ _ refl q rewrite q = refl

module _ {i} {A : 𝒰 i} {x₁ x₂ : A} (a : A) (p : x₁ == x₂)
  where
  =-transportₗ : (q : a == x₁) → transport (a ==_) p q == q ∙ p
  =-transportₗ q rewrite p = unitᵣ

  =-transportᵣ : (q : x₁ == a) → transport (_== a) p q == p ⁻¹ ∙ q
  =-transportᵣ q rewrite p = unitₗ


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the membership predicate for fresh lists
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Setoid)

module Data.List.Fresh.Membership.Setoid.Properties {c ℓ} (S : Setoid c ℓ) where

open import Level using (Level; _⊔_)
open import Data.Empty
open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Product using (∃; _×_; _,_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂)

open import Function using (id; _∘′_; _$_)
open import Relation.Nullary
open import Relation.Unary as U using (Pred)
import Relation.Binary as B
import Relation.Binary.PropositionalEquality as P
open import Relation.Nary

open import Data.List.Fresh
open import Data.List.Fresh.Properties
open import Data.List.Fresh.Membership.Setoid S
open import Data.List.Fresh.Relation.Unary.Any using (Any; here; there; _─_)
import Data.List.Fresh.Relation.Unary.Any.Properties as Anyₚ
import Data.List.Fresh.Relation.Unary.All.Properties as Allₚ

open Setoid S renaming (Carrier to A)

private
  variable
    p r : Level

------------------------------------------------------------------------
-- transport

module _ {R : Rel A r} where

  ≈-subst-∈ : ∀ {x y} {xs : List# A R} → x ≈ y → x ∈ xs → y ∈ xs
  ≈-subst-∈ x≈y (here x≈x′)  = here (trans (sym x≈y) x≈x′)
  ≈-subst-∈ x≈y (there x∈xs) = there (≈-subst-∈ x≈y x∈xs)

------------------------------------------------------------------------
-- relationship to fresh

module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) where

  fresh⇒∉ : ∀ {x} {xs : List# A R} → x # xs → x ∉ xs
  fresh⇒∉ (r , _)    (here x≈y)   = R⇒≉ r x≈y
  fresh⇒∉ (_ , x#xs) (there x∈xs) = fresh⇒∉ x#xs x∈xs

------------------------------------------------------------------------
-- disjointness

module _ {R : Rel A r} where

  distinct : ∀ {x y} {xs : List# A R} → x ∈ xs → y ∉ xs → x ≉ y
  distinct x∈xs y∉xs x≈y = y∉xs (≈-subst-∈ x≈y x∈xs)

------------------------------------------------------------------------
-- remove

module _ {R : Rel A r} where

  remove-inv : ∀ {x y} {xs : List# A R} (x∈xs : x ∈ xs) →
               y ∈ xs → x ≈ y ⊎ y ∈ (xs ─ x∈xs)
  remove-inv (here x≈z)   (here y≈z)   = inj₁ (trans x≈z (sym y≈z))
  remove-inv (here _)     (there y∈xs) = inj₂ y∈xs
  remove-inv (there _)    (here y≈z)   = inj₂ (here y≈z)
  remove-inv (there x∈xs) (there y∈xs) = Sum.map₂ there (remove-inv x∈xs y∈xs)

  ∈-remove : ∀ {x y} {xs : List# A R} (x∈xs : x ∈ xs) → y ∈ xs → x ≉ y → y ∈ (xs ─ x∈xs)
  ∈-remove x∈xs y∈xs x≉y = fromInj₂ (⊥-elim ∘′ x≉y) (remove-inv x∈xs y∈xs)

module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≉⇒R : ∀[ _≉_ ⇒ R ]) where

  private
    R≈ : R B.Respectsˡ _≈_
    R≈ x≈y Rxz = ≉⇒R (R⇒≉ Rxz ∘′ trans x≈y)

  fresh-remove : ∀ {x} {xs : List# A R} (x∈xs : x ∈ xs) → x # (xs ─ x∈xs)
  fresh-remove {xs = cons x xs pr} (here x≈y)   = fresh-respectsˡ R≈ (sym x≈y) pr
  fresh-remove {xs = cons x xs pr} (there x∈xs) =
    ≉⇒R (distinct x∈xs (fresh⇒∉ R⇒≉ pr)) , fresh-remove x∈xs

  ∉-remove : ∀ {x} {xs : List# A R} (x∈xs : x ∈ xs) → x ∉ (xs ─ x∈xs)
  ∉-remove x∈xs = fresh⇒∉ R⇒≉ (fresh-remove x∈xs)

------------------------------------------------------------------------
-- injection

module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) where

  injection : ∀ {xs ys : List# A R} (inj : ∀ {x} → x ∈ xs → x ∈ ys) →
              length xs ≤ length ys
  injection {[]}                 {ys} inj = z≤n
  injection {xxs@(cons x xs pr)} {ys} inj = begin
    length xxs               ≤⟨ s≤s (injection step) ⟩
    suc (length (ys ─ x∈ys)) ≡⟨ P.sym (Anyₚ.length-remove x∈ys) ⟩
    length ys                ∎

    where

    open ≤-Reasoning

    x∉xs : x ∉ xs
    x∉xs = fresh⇒∉ R⇒≉ pr

    x∈ys : x ∈ ys
    x∈ys = inj (here refl)

    step : ∀ {y} → y ∈ xs → y ∈ (ys ─ x∈ys)
    step {y} y∈xs = ∈-remove x∈ys (inj (there y∈xs)) (distinct y∈xs x∉xs ∘′ sym)

  strict-injection : ∀ {xs ys : List# A R} (inj : ∀ {x} → x ∈ xs → x ∈ ys) →
   (∃ λ x → x ∈ ys × x ∉ xs) → length xs < length ys
  strict-injection {xs} {ys} inj (x , x∈ys , x∉xs) = begin
    suc (length xs)          ≤⟨ s≤s (injection step) ⟩
    suc (length (ys ─ x∈ys)) ≡⟨ P.sym (Anyₚ.length-remove x∈ys) ⟩
    length ys                ∎

    where

    open ≤-Reasoning

    step : ∀ {y} → y ∈ xs → y ∈ (ys ─ x∈ys)
    step {y} y∈xs = fromInj₂ (λ x≈y → ⊥-elim (x∉xs (≈-subst-∈ (sym x≈y) y∈xs)))
                  $ remove-inv x∈ys (inj y∈xs)

------------------------------------------------------------------------
-- proof irrelevance

module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≈-irrelevant : B.Irrelevant _≈_) where

  ∈-irrelevant : ∀ {x} {xs : List# A R} → Irrelevant (x ∈ xs)
  -- positive cases
  ∈-irrelevant (here x≈y₁)   (here x≈y₂)   = P.cong here (≈-irrelevant x≈y₁ x≈y₂)
  ∈-irrelevant (there x∈xs₁) (there x∈xs₂) = P.cong there (∈-irrelevant x∈xs₁ x∈xs₂)
  -- absurd cases
  ∈-irrelevant {xs = cons x xs pr} (here x≈y)    (there x∈xs₂) =
    ⊥-elim (distinct x∈xs₂ (fresh⇒∉ R⇒≉ pr) x≈y)
  ∈-irrelevant {xs = cons x xs pr} (there x∈xs₁) (here x≈y)    =
    ⊥-elim (distinct x∈xs₁ (fresh⇒∉ R⇒≉ pr) x≈y)


text:
module Interpreter where

open import Data.Char
open import Data.Bool
open import Data.Nat
import Data.Unit as U
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality as PropEq
open import Relation.Nullary.Core
import Data.String as Str
open import Data.Nat.Show
import Data.List as List
open import Data.Empty

infix 3 _:::_,_
infix 2 _∈_
infix 1 _⊢_

data `Set : Set where
  `Nat  : `Set
  `Bool : `Set
  `_⇨_  : `Set → `Set → `Set
  `Unit : `Set
  `_×_  : `Set → `Set → `Set
  `_+_  : `Set → `Set → `Set

#_ : `Set → Set
# `Nat = ℕ
# `Bool = Bool
# (` t ⇨ s) = # t → # s
# `Unit = U.Unit
# (` t × s) = # t × # s
# (` t + s) = # t ⊎ # s

data Γ : Set where
  ·         : Γ
  _:::_,_   : Char → `Set → Γ → Γ

data _∈_ :  Char → Γ → Set where
  H  : ∀ {x Δ t } → x ∈ x ::: t , Δ
  TH : ∀ {x y Δ t } → {{prf : x ∈ Δ}} → x ∈ y ::: t , Δ

!Γ_[_] : ∀ {x} → (Δ : Γ) → x ∈ Δ → `Set
!Γ_[_] · ()
!Γ _ ::: t , Δ [ H ]     = t
!Γ _ ::: _ , Δ [ TH {{prf = i}} ]  = !Γ Δ [ i ]

data _⊢_ : Γ → `Set → Set where
  `false           : ∀ {Δ} → Δ ⊢ `Bool
  `true            : ∀ {Δ} → Δ ⊢ `Bool
  `n_              : ∀ {Δ} → ℕ → Δ ⊢ `Nat
  `v_              : ∀ {Δ} → (x : Char) → {{i : x ∈ Δ}} → Δ ⊢ !Γ Δ [ i ]
  `_₋_              : ∀ {Δ t s} → Δ ⊢ ` t ⇨ s → Δ ⊢ t → Δ ⊢ s
  `λ_`:_⇨_         : ∀ {Δ tr} → (x : Char) → (tx : `Set)
                        → x ::: tx , Δ ⊢ tr → Δ ⊢ ` tx ⇨ tr
  `_+_             : ∀ {Δ} → Δ ⊢ `Nat → Δ ⊢ `Nat → Δ ⊢ `Nat
  `_*_             : ∀ {Δ} → Δ ⊢ `Nat →  Δ ⊢ `Nat → Δ ⊢ `Nat
  `_∧_             : ∀ {Δ} → Δ ⊢ `Bool → Δ ⊢ `Bool → Δ ⊢ `Bool
  `_∨_             : ∀ {Δ} → Δ ⊢ `Bool →  Δ ⊢ `Bool → Δ ⊢ `Bool
  `_≤_             : ∀ {Δ} → Δ ⊢ `Nat → Δ ⊢ `Nat →  Δ ⊢ `Bool
  `¬_              : ∀ {Δ} → Δ ⊢ `Bool →  Δ ⊢ `Bool
  `_,_             : ∀ {Δ t s} → Δ ⊢ t →  Δ ⊢ s →  Δ ⊢ ` t × s
  `fst             : ∀ {Δ t s} → Δ ⊢ ` t × s → Δ ⊢ t
  `snd             : ∀ {Δ t s} → Δ ⊢ ` t × s → Δ ⊢ s
  `left            : ∀ {Δ t s} → Δ ⊢ t → Δ ⊢ ` t + s
  `right           : ∀ {Δ t s} → Δ ⊢ s → Δ ⊢ ` t + s
  `case_`of_||_    : ∀ {Δ t s u} → Δ ⊢ ` t + s
                        → Δ ⊢ ` t ⇨ u → Δ ⊢ ` s ⇨ u → Δ ⊢ u
  `tt              : ∀ {Δ} → Δ ⊢ `Unit
  `let_`=_`in_     : ∀ {Δ th tb} → (x : Char)
                       → Δ ⊢ th → x ::: th , Δ ⊢ tb → Δ ⊢ tb
  `if_`then_`else_ : ∀ {Δ t} → Δ ⊢ `Bool → Δ ⊢ t → Δ ⊢ t → Δ ⊢ t

data ⟨_⟩ : Γ → Set₁ where
  []   : ⟨ · ⟩
  _∷_  : ∀ {x t Δ} → # t → ⟨ Δ ⟩ → ⟨ x ::: t , Δ ⟩

!_[_] : ∀ {x Δ} → ⟨ Δ ⟩ → (i : x ∈ Δ) → # !Γ Δ [ i ]
!_[_] [] ()
!_[_] (val ∷ env) H      = val
!_[_] (val ∷ env) (TH {{prf = i}}) = ! env [ i ]

interpret : ∀ {t} → · ⊢ t → # t
interpret = interpret' []
  where interpret' : ∀ {Δ t} → ⟨ Δ ⟩ → Δ ⊢ t → # t
        interpret' env `true = true
        interpret' env `false = false
        interpret' env `tt = U.unit
        interpret' env (`n n) = n
        interpret' env ((`v x) {{i = idx}}) = ! env [ idx ]
        interpret' env (` f ₋ x) = (interpret' env f) (interpret' env x)
        interpret' env (`λ _ `: tx ⇨ body) = λ (x : # tx) → interpret' (x ∷ env) body
        interpret' env (` l + r) = interpret' env l + interpret' env r
        interpret' env (` l * r) = interpret' env l * interpret' env r
        interpret' env (` l ∧ r) = interpret' env l ∧ interpret' env r
        interpret' env (` l ∨ r) = interpret' env l ∨ interpret' env r
        interpret' env (` l ≤ r) with interpret' env l ≤? interpret' env r
        interpret' env (` l ≤ r) | yes p = true
        interpret' env (` l ≤ r) | no ¬p = false
        interpret' env (`¬ x) = not (interpret' env x)
        interpret' env (` f , s) = interpret' env f ,′ interpret' env s
        interpret' env (`fst p) with interpret' env p
        interpret' env (`fst p) | f , s = f
        interpret' env (`snd p) with interpret' env p
        interpret' env (`snd p) | f , s = s
        interpret' env (`left v) = inj₁ (interpret' env v)
        interpret' env (`right v) = inj₂ (interpret' env v)
        interpret' env (`case s `of le || re) with interpret' env s
        interpret' env (`case s `of le || re) | inj₁ l = (interpret' env le) l
        interpret' env (`case s `of le || re) | inj₂ r = (interpret' env re) r
        interpret' env (`let _ `= h `in b) = let hval = interpret' env h in interpret' (hval ∷ env) b
        interpret' env (`if b `then et `else ef) with interpret' env b
        interpret' env (`if b `then et `else ef) | true = interpret' env et
        interpret' env (`if b `then et `else ef) | false = interpret' env ef

testSimpleLambda : · ⊢ `Nat
testSimpleLambda = ` (`λ 'x' `: `Nat ⇨ ` `v 'x' + `v 'x') ₋ `n 10

testNestedLambda : · ⊢ `Nat
testNestedLambda = ` ` (`λ 'x' `: `Nat ⇨ (`λ 'y' `: `Nat ⇨ ` `v 'x' * `v 'y')) ₋ `n 10 ₋ `n 15

-- Should not work because the inner x is not bound to a boolean, and it should not be possible to refer to the outside x using Elem
-- TODO Fix this to not work with instance search
--testNamingNotWorking : · ⊢ `Bool
--testNamingNotWorking = ` ` `λ 'x' `: `Bool ⇨ (`λ 'x' `: `Unit ⇨ `v 'x') ₋ `true ₋ `tt

testNamingWorking : · ⊢ `Unit
testNamingWorking = ` ` `λ 'x' `: `Bool ⇨ (`λ 'x' `: `Unit ⇨ `v 'x') ₋ `true ₋ `tt

testSum1 : · ⊢ `Nat
testSum1 = `let 'n' `= `case `left (`n 10) `of
                              `λ 'n' `: `Nat ⇨ `v 'n'
                           || `λ 'b' `: `Bool ⇨ `if `v 'b' `then `n 1 `else `n 0
           `in `v 'n'

testSum2 : · ⊢ `Nat
testSum2 = `let 'n' `= `case `right `true `of
                              `λ 'n' `: `Nat ⇨ `v 'n'
                           || `λ 'b' `: `Bool ⇨ `if `v 'b' `then `n 1 `else `n 0
           `in `v 'n'

testProduct1 : · ⊢ `Bool
testProduct1 = `fst (` `true , (` `n 10 , `tt ))

testProduct2 : · ⊢ ` `Nat × `Unit
testProduct2 = `snd (` `true , (` `n 10 , `tt ))

testDeMorganFullOr : · ⊢ `Bool
testDeMorganFullOr = `let 's' `= `λ 'x' `: `Bool ⇨ `λ 'y' `: `Bool ⇨ `¬ (` `v 'x' ∨ `v 'y')
                     `in ` ` `v 's'₋ `true ₋ `true
testDeMorganBrokenAnd : · ⊢ `Bool
testDeMorganBrokenAnd = `let 's' `= `λ 'x' `: `Bool ⇨ `λ 'y' `: `Bool ⇨ ` `¬ `v 'x' ∧ `¬ `v 'y'
                        `in ` ` `v 's' ₋ `true ₋ `true

max_stars_repo_name: ahmadsalim/well-typed-agda-interpreter

max_issues_repo_name: ahmadsalim/well-typed-agda-interpreter

max_forks_repo_name: ahmadsalim/well-typed-agda-interpreter


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

module Relation.Binary.PropositionalEquality.Subst.Properties where

-- Properties of 'subst' onto binary relations.

open import Level
open import Function using (_$_; flip) renaming (id to idFun; _∘_ to _⊚_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

private
  variable
    ℓ ℓ₁ ℓ₂ t t₁ t₂ o : Level

-- Two shorthands:  transport the domain or codomain of a relation along an equality.
module Shorthands {O : Set o} (R : Rel O ℓ) where
  infixr 9 _◂_
  infixl 9 _▸_

  _◂_ : ∀ {A B C} → A ≡ B → R B C → R A C
  p ◂ f = subst (flip R _) (sym p) f

  _▸_ : ∀ {A B C} → R A B → B ≡ C → R A C
  f ▸ p = subst (R _) p f

  -- Some simple properties of transports
module Transport {O : Set o} (R : Rel O ℓ) where
  open Shorthands R public

  ◂-▸-id : ∀ {A} (f : R A A) → refl ◂ f ≡ f ▸ refl
  ◂-▸-id f = refl

  ◂-▸-comm : ∀ {A B C D} (p : A ≡ B) (f : R B C) (q : C ≡ D) →
             (p ◂ (f ▸ q)) ≡ ((p ◂ f) ▸ q)
  ◂-▸-comm refl f refl = refl

  ◂-assocˡ : ∀ {A B C D} (p : A ≡ B) {q : B ≡ C} (f : R C D) →
            p ◂ q ◂ f ≡ (trans p q) ◂ f
  ◂-assocˡ refl {refl} f = refl

  ▸-assocʳ : ∀ {A B C D} (f : R A B) {p : B ≡ C} (q : C ≡ D) →
            f ▸ p ▸ q ≡ f ▸ trans p q
  ▸-assocʳ f {refl} refl = refl

-- If we have a relation Q over a relation R, we can transport over that too
module TransportOverQ {O : Set o} (R : Rel O ℓ) (Q : {X Y : O} → Rel (R X Y) t)  where
  open Transport R

  ◂-resp-≈ : ∀ {A B C} (p : A ≡ B) {f g : R B C} → Q f g → Q (p ◂ f) (p ◂ g)
  ◂-resp-≈ refl f≈g = f≈g

  ▸-resp-≈ : ∀ {A B C} {f g : R A B} → Q f g → (p : B ≡ C) → Q (f ▸ p) (g ▸ p)
  ▸-resp-≈ f≈g refl = f≈g

-- Given two relations and a homomorphism between them,
-- congruence properties over subst
module TransportMor {O₁ O₂ : Set o}
  (R₁ : Rel O₁ ℓ) (R₂ : Rel O₂ t)
  (M₀       : O₁ → O₂)
  (M₁       : ∀ {A B} → R₁ A B → R₂ (M₀ A) (M₀ B)) where

  open Shorthands R₁
  open Shorthands R₂ renaming (_◂_ to _◃_; _▸_ to _▹_)

  M-resp-▸ : ∀ {A B C} (f : R₁ A B) (p : B ≡ C) →
             M₁ (f ▸ p) ≡ M₁ f ▹ cong M₀ p
  M-resp-▸ f refl = refl

  M-resp-◂ : ∀ {A B C} (p : A ≡ B) (f : R₁ B C) →
             M₁ (p ◂ f) ≡ cong M₀ p ◃ M₁ f
  M-resp-◂ refl f = refl

-- Transports on paths
module TransportStar {O : Set o} (R : Rel O ℓ) where
  open Shorthands (Star R) public renaming
    ( _◂_ to _◂*_
    ; _▸_ to _▸*_
    )
  open Shorthands R

  -- Lemmas relating transports to path operations.

  ◂*-▸*-ε : {A B : O} (p : A ≡ B) → ε ▸* p ≡ p ◂* ε
  ◂*-▸*-ε refl = refl

  ◂*-◅ : {A B C D : O} (p : A ≡ B) (f : R B C) (fs : Star R C D) →
         p ◂* (f ◅ fs) ≡ (p ◂ f) ◅ fs
  ◂*-◅ refl f fs = refl

  ◅-▸* : {A B C D : O} (f : R A B) (fs : Star R B C) (p : C ≡ D) →
         (f ◅ fs) ▸* p ≡ f ◅ (fs ▸* p)
  ◅-▸* f fs refl = refl

  ◅-◂*-▸ : {A B C D : O} (f : R A B) (p : B ≡ C) (fs : Star R C D) →
           _≡_ {_} {Star R A D} (f ◅ (p ◂* fs)) ((f ▸ p) ◅ fs)
  ◅-◂*-▸ f refl fs = refl

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Computability.Enumeration.Univalence where

open import Cubical.Core.Everything
open import Computability.Prelude
open import Computability.Enumeration.Base

max_stars_repo_name: jesyspa/computability-in-agda

max_issues_repo_name: jesyspa/computability-in-agda

max_forks_repo_name: jesyspa/computability-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the sublist relation over setoid equality.
------------------------------------------------------------------------

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

open import Relation.Binary hiding (Decidable)

module Data.List.Relation.Binary.Subset.Propositional.Properties
  where

open import Category.Monad
open import Data.Bool.Base using (Bool; true; false; T)
open import Data.List
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Categorical
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
import Data.List.Relation.Binary.Subset.Setoid.Properties as Setoidₚ
open import Data.List.Relation.Binary.Subset.Propositional
import Data.Product as Prod
import Data.Sum as Sum
open import Function using (_∘_; _∘′_; id; _$_)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Equivalence using (module Equivalence)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Unary using (Decidable)
open import Relation.Binary using (_⇒_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; _≗_; isEquivalence; refl; setoid; module ≡-Reasoning)
import Relation.Binary.PreorderReasoning as PreorderReasoning

private
  open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})

------------------------------------------------------------------------
-- Relational properties

module _ {a} {A : Set a} where

  ⊆-reflexive : _≡_ ⇒ (_⊆_ {A = A})
  ⊆-reflexive refl = id

  ⊆-refl : Reflexive {A = List A} _⊆_
  ⊆-refl x∈xs = x∈xs

  ⊆-trans : Transitive {A = List A} (_⊆_ {A = A})
  ⊆-trans xs⊆ys ys⊆zs x∈xs = ys⊆zs (xs⊆ys x∈xs)

module _ {a} (A : Set a) where

  ⊆-isPreorder : IsPreorder {A = List A} _≡_ _⊆_
  ⊆-isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive     = ⊆-reflexive
    ; trans         = ⊆-trans
    }

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

------------------------------------------------------------------------
-- Reasoning over subsets

module ⊆-Reasoning {a} (A : Set a) where
  open Setoidₚ.⊆-Reasoning (setoid A) public
    hiding (_≋⟨_⟩_; _≋˘⟨_⟩_; _≋⟨⟩_)

------------------------------------------------------------------------
-- Properties relating _⊆_ to various list functions
------------------------------------------------------------------------
-- Any

module _ {a p} {A : Set a} {P : A → Set p} {xs ys : List A} where

  mono : xs ⊆ ys → Any P xs → Any P ys
  mono xs⊆ys =
    _⟨$⟩_ (Inverse.to Any↔) ∘′
    Prod.map id (Prod.map xs⊆ys id) ∘
    _⟨$⟩_ (Inverse.from Any↔)

------------------------------------------------------------------------
-- map

module _ {a b} {A : Set a} {B : Set b} (f : A → B) {xs ys} where

  map-mono : xs ⊆ ys → map f xs ⊆ map f ys
  map-mono xs⊆ys =
    _⟨$⟩_ (Inverse.to (map-∈↔ f)) ∘
    Prod.map id (Prod.map xs⊆ys id) ∘
    _⟨$⟩_ (Inverse.from (map-∈↔ f))

------------------------------------------------------------------------
-- _++_

module _ {a} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} where

  _++-mono_ : xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → xs₁ ++ xs₂ ⊆ ys₁ ++ ys₂
  _++-mono_ xs₁⊆ys₁ xs₂⊆ys₂ =
    _⟨$⟩_ (Inverse.to ++↔) ∘
    Sum.map xs₁⊆ys₁ xs₂⊆ys₂ ∘
    _⟨$⟩_ (Inverse.from ++↔)

------------------------------------------------------------------------
-- concat

module _ {a} {A : Set a} {xss yss : List (List A)} where

  concat-mono : xss ⊆ yss → concat xss ⊆ concat yss
  concat-mono xss⊆yss =
    _⟨$⟩_ (Inverse.to $ concat-∈↔ {a = a}) ∘
    Prod.map id (Prod.map id xss⊆yss) ∘
    _⟨$⟩_ (Inverse.from $ concat-∈↔ {a = a})

------------------------------------------------------------------------
-- _>>=_

module _ {ℓ} {A B : Set ℓ} (f g : A → List B) {xs ys} where

  >>=-mono : xs ⊆ ys → (∀ {x} → f x ⊆ g x) → (xs >>= f) ⊆ (ys >>= g)
  >>=-mono xs⊆ys f⊆g =
    _⟨$⟩_ (Inverse.to $ >>=-∈↔ {ℓ = ℓ}) ∘
    Prod.map id (Prod.map xs⊆ys f⊆g) ∘
    _⟨$⟩_ (Inverse.from $ >>=-∈↔ {ℓ = ℓ})

------------------------------------------------------------------------
-- _⊛_

module _ {ℓ} {A B : Set ℓ} {fs gs : List (A → B)} {xs ys : List A} where

  _⊛-mono_ : fs ⊆ gs → xs ⊆ ys → (fs ⊛ xs) ⊆ (gs ⊛ ys)
  _⊛-mono_ fs⊆gs xs⊆ys =
    _⟨$⟩_ (Inverse.to $ ⊛-∈↔ gs) ∘
    Prod.map id (Prod.map id (Prod.map fs⊆gs (Prod.map xs⊆ys id))) ∘
    _⟨$⟩_ (Inverse.from $ ⊛-∈↔ fs)

------------------------------------------------------------------------
-- _⊗_

module _ {ℓ} {A B : Set ℓ} {xs₁ ys₁ : List A} {xs₂ ys₂ : List B} where

  _⊗-mono_ : xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → (xs₁ ⊗ xs₂) ⊆ (ys₁ ⊗ ys₂)
  xs₁⊆ys₁ ⊗-mono xs₂⊆ys₂ =
    _⟨$⟩_ (Inverse.to $ ⊗-∈↔ {ℓ = ℓ}) ∘
    Prod.map xs₁⊆ys₁ xs₂⊆ys₂ ∘
    _⟨$⟩_ (Inverse.from $ ⊗-∈↔ {ℓ = ℓ})

------------------------------------------------------------------------
-- any

module _ {a} {A : Set a} (p : A → Bool) {xs ys} where

  any-mono : xs ⊆ ys → T (any p xs) → T (any p ys)
  any-mono xs⊆ys =
    _⟨$⟩_ (Equivalence.to any⇔) ∘
    mono xs⊆ys ∘
    _⟨$⟩_ (Equivalence.from any⇔)

------------------------------------------------------------------------
-- map-with-∈

module _ {a b} {A : Set a} {B : Set b}
         {xs : List A} {f : ∀ {x} → x ∈ xs → B}
         {ys : List A} {g : ∀ {x} → x ∈ ys → B} where

  map-with-∈-mono : (xs⊆ys : xs ⊆ ys) → (∀ {x} → f {x} ≗ g ∘ xs⊆ys) →
                    map-with-∈ xs f ⊆ map-with-∈ ys g
  map-with-∈-mono xs⊆ys f≈g {x} =
    _⟨$⟩_ (Inverse.to map-with-∈↔) ∘
    Prod.map id (Prod.map xs⊆ys (λ {x∈xs} x≡fx∈xs → begin
      x               ≡⟨ x≡fx∈xs ⟩
      f x∈xs          ≡⟨ f≈g x∈xs ⟩
      g (xs⊆ys x∈xs)  ∎)) ∘
    _⟨$⟩_ (Inverse.from map-with-∈↔)
    where open ≡-Reasoning

------------------------------------------------------------------------
-- filter

module _ {a p} {A : Set a} {P : A → Set p} (P? : Decidable P) where

  filter⁺ : ∀ xs → filter P? xs ⊆ xs
  filter⁺ = Setoidₚ.filter⁺ (setoid A) P?

------------------------------------------------------------------------
-- DEPRECATED
------------------------------------------------------------------------

-- Version 0.16

boolFilter-⊆ : ∀ {a} {A : Set a} (p : A → Bool) →
               (xs : List A) → boolFilter p xs ⊆ xs
boolFilter-⊆ _ []       = λ ()
boolFilter-⊆ p (x ∷ xs) with p x | boolFilter-⊆ p xs
... | false | hyp = there ∘ hyp
... | true  | hyp =
  λ { (here  eq)          → here eq
    ; (there ∈boolFilter) → there (hyp ∈boolFilter)
    }
{-# WARNING_ON_USAGE boolFilter-⊆
"Warning: boolFilter was deprecated in v0.15.
Please use filter instead."
#-}


text:
{-# OPTIONS --cubical --prop #-}
module Issue2487.Infective where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An equality postulate which evaluates
------------------------------------------------------------------------

{-# OPTIONS --with-K #-}

module Relation.Binary.PropositionalEquality.TrustMe where

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

open import Agda.Builtin.TrustMe

-- trustMe {x = x} {y = y} evaluates to refl if x and y are
-- definitionally equal.

trustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
trustMe = primTrustMe

-- "Erases" a proof. The original proof is not inspected. The
-- resulting proof reduces to refl if the two sides are definitionally
-- equal. Note that checking for definitional equality can be slow.

erase : ∀ {a} {A : Set a} {x y : A} → x ≡ y → x ≡ y
erase _ = trustMe

-- A "postulate with a reduction": postulate[ a ↦ b ] a evaluates to b,
-- while postulate[ a ↦ b ] a' gets stuck if a' is not definitionally
-- equal to a. This can be used to define a postulate of type (x : A) → B x
-- by only specifying the behaviour at B t for some t : A. Introduced in
--
--   Alan Jeffrey, Univalence via Agda's primTrustMe again
--   23 January 2015
--   https://lists.chalmers.se/pipermail/agda/2015/007418.html

postulate[_↦_] : ∀ {a b} {A : Set a}{B : A → Set b} →
                  (t : A) → B t → (x : A) → B x
postulate[ a ↦ b ] a' with trustMe {x = a} {a'}
postulate[ a ↦ b ] .a | refl = b

------------------------------------------------------------------------
-- DEPRECATION
------------------------------------------------------------------------

-- Version 0.18

{-# WARNING_ON_USAGE erase
"Warning: erase was deprecated in v0.18.
Please use the safe function ≡-erase defined in Relation.Binary.PropositionalEquality.WithK instead."
#-}


text:
module Issue237 where

open import Common.Equality

data Unit : Set where
  unit : Unit

f : Unit → Unit
f u with u
... | unit = unit

postulate
  eq : ∀ u → f u ≡ unit

foo : Unit → Set₁
foo u rewrite eq u = Set

-- Bug.agda:20,1-25
-- Not implemented: type checking of with application
-- when checking that the expression f u | u has type _35 u


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

open import Cubical.Algebra.Monoid.Base public


text:
-- {-# OPTIONS -v reify:100 -v syntax.reify:100  #-}
module Issue857b where

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

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

_∋_ : (A : Set) → A → A
_ ∋ x = x

foo : {A B : Set} {x : ⊥} {y : B} →
      ((⊥ → A) ∋ λ()) x ≡ ((⊥ → B → A) ∋ λ()) x y
foo = refl

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

bar : {A B C : Set} {x : ⊥} {y : B} {z : C} →
      ((⊥ → B → A) ∋ λ()) x y ≡ ((⊥ → C → A) ∋ λ()) x z
bar = refl

-- WAS:
-- .y != .z of type .B
-- when checking that the expression refl has type
-- ((⊥ → .B → .A) ∋ .Test.absurdLambda) .x .y ≡
-- ((⊥ → .C → .A) ∋ .Test.absurdLambda) .x .z

-- Note that z has type C, not B.

baz : {A : Set} → _≡_ {A = ⊥ → A} ⊥-elim (λ())
baz = refl

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

-- ERROR: ⊥-elim x != (λ ()) x of type .A
-- when checking that the expression refl has type ⊥-elim ≡ (λ ())


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Monoid.Instances.NatPlusBis where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat

open import Cubical.Algebra.Monoid

open PlusBis

NatPlusBis-Monoid : Monoid ℓ-zero
fst NatPlusBis-Monoid = ℕ
MonoidStr.ε (snd NatPlusBis-Monoid) = 0
MonoidStr._·_ (snd NatPlusBis-Monoid) = _+'_
MonoidStr.isMonoid (snd NatPlusBis-Monoid) = makeIsMonoid isSetℕ +'-assoc +'-rid +'-lid


text:
module Ints.Properties where

open import Ints
open import Equality

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

private
  ≡→≡ : ∀ {a b} → (+ a ≡ + b) → a ≡ b
  ≡→≡ refl = refl

  ≡→≡′ : ∀ {a b} → (-[1+ a ] ≡ -[1+ b ]) → a ≡ b
  ≡→≡′ refl = refl

  ≡←≡ : ∀ {a b} → a ≡ b → (+ a ≡ + b)
  ≡←≡ refl = refl

  ≡←≡′ : ∀ {a b} → a ≡ b → (-[1+ a ] ≡ -[1+ b ])
  ≡←≡′ refl = refl

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

eq-int-to-nat : ∀ {a b} → (+ a ≡ + b) → a ≡ b
eq-int-to-nat = ≡→≡

eq-neg-int-to-nat : ∀ {a b} → (-[1+ a ] ≡ -[1+ b ]) → a ≡ b
eq-neg-int-to-nat = ≡→≡′

eq-nat-to-int : ∀ {a b} → a ≡ b → (+ a ≡ + b)
eq-nat-to-int = ≡←≡

eq-neg-nat-to-int : ∀ {a b} → a ≡ b → (-[1+ a ] ≡ -[1+ b ])
eq-neg-nat-to-int = ≡←≡′


text:
{-# OPTIONS --no-universe-polymorphism #-}

module Issue202 where

open import Common.Level
open import Imports.Test

module Test2 {ℓ : Level} (F : Foo ℓ) where

-- Test2.agda:4,31-36
-- The metavariable _1 cannot depend on ℓ because it does not depend
-- on any variables
-- when checking that the expression Foo ℓ has type _1

-- The code is accepted if universe polymorphism is turned on in
-- Test2.agda.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

open import HoTT
open import homotopy.CircleHSpace
open import homotopy.LoopSpaceCircle
open import homotopy.Pi2HSusp
open import homotopy.IterSuspensionStable

-- This summerizes all [πₙ Sⁿ]
module homotopy.PinSn where

  private
    π1S¹-iso-ℤ : πS 0 ⊙S¹ ≃ᴳ ℤ-group
    π1S¹-iso-ℤ = ΩS¹-iso-ℤ ∘eᴳ unTrunc-iso ΩS¹-group-structure ΩS¹-is-set

  private
    πS-SphereS'-iso-ℤ : ∀ n → πS n (⊙Susp^ n ⊙S¹) ≃ᴳ ℤ-group
    πS-SphereS'-iso-ℤ 0 = π1S¹-iso-ℤ
    πS-SphereS'-iso-ℤ 1 =
      πS 1 ⊙S²
        ≃ᴳ⟨ Pi2HSusp.π₂-Susp S¹-level S¹-conn ⊙S¹-hSpace ⟩
      πS 0 ⊙S¹
        ≃ᴳ⟨ πS-SphereS'-iso-ℤ O ⟩
      ℤ-group
        ≃ᴳ∎
    πS-SphereS'-iso-ℤ (S (S n)) =
      πS (S (S n)) (⊙Susp^ (S (S n)) ⊙S¹)
        ≃ᴳ⟨ Susp^StableSucc.stable ⊙S¹ S¹-conn
             (S n) (S n) (≤-ap-S $ ≤-ap-S $ *2-increasing n) ⟩
      πS (S n) (⊙Susp^ (S n) ⊙S¹)
        ≃ᴳ⟨ πS-SphereS'-iso-ℤ (S n) ⟩
      ℤ-group
        ≃ᴳ∎

  πS-SphereS-iso-ℤ : ∀ n → πS n (⊙Sphere (S n)) ≃ᴳ ℤ-group
  πS-SphereS-iso-ℤ n = πS-SphereS'-iso-ℤ n
                   ∘eᴳ πS-emap n (⊙Susp^-Susp-split-iso n ⊙S⁰)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module InstanceArgumentsBraceSpaces where

postulate
  A B : Set
  test : {{a : A} } → B


text:
module Tactic.Nat.Subtract.Auto where

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.Quote
open import Tactic.Reflection.Meta

open import Tactic.Nat.Reflect
open import Tactic.Nat.NF
open import Tactic.Nat.Auto
open import Tactic.Nat.Simpl.Lemmas
open import Tactic.Nat.Subtract.Exp
open import Tactic.Nat.Subtract.Reflect
open import Tactic.Nat.Subtract.Lemmas
open import Tactic.Nat.Less.Lemmas

autosub-proof : ∀ eqn ρ → Maybe (⟦ eqn ⟧eqn ρ)
autosub-proof (e₁ :≡ e₂) ρ with normSub e₁ == normSub e₂
autosub-proof (e₁ :≡ e₂) ρ | no _   = nothing
autosub-proof (e₁ :≡ e₂) ρ | yes eq = just (liftNFSubEq e₁ e₂ ρ (cong (λ n → ⟦ n ⟧sn ρ) eq))
autosub-proof (e₁ :< e₂) ρ with cancel (normSub e₁) (normSub e₂) | simplifySubLess e₁ e₂ ρ
autosub-proof (e₁ :< e₂) ρ | [] , (suc n , []) ∷ nf | simp =
  let sk : SubNF
      sk = (suc n , []) ∷ nf
      k  = (    n , []) ∷ nf in
  just $ simp $ LessNat.diff (⟦ k ⟧sns ρ) $
    ns-sound sk (atomEnvS ρ) ⟨≡⟩
    auto ⟨≡⟩ʳ (λ z → suc (z + 0)) $≡ lem-eval-sns-nS k ρ
autosub-proof (e₁ :< e₂) ρ | _  , _ | simp = nothing

autosub-tactic : Type → TC Term
autosub-tactic t = do
  ensureNoMetas t
  just (eqn , Γ) ← termToSubEqn t
    where nothing → typeError $ strErr "Invalid goal:" ∷ termErr t ∷ []
  pure $
    getProof (quote cantProve) t $
      def (quote autosub-proof)
          ( vArg (` eqn)
          ∷ vArg (quotedEnv Γ)
          ∷ [] )

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-# FOREIGN GHC import qualified Issue223 #-}

data A : Set
data B : Set

data A where
  BA : B → A

data B where
  AB : A → B
  BB : B

{-# COMPILE GHC A = data Issue223.A (Issue223.BA) #-}
{-# COMPILE GHC B = data Issue223.B (Issue223.AB | Issue223.BB) #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- de Bruijn-aware generic traversal of reflected terms.
------------------------------------------------------------------------

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

open import Category.Applicative using (RawApplicative)
open import Category.Monad using (RawMonad)

module Leftovers.Everywhere {F : Set → Set} (MF : RawMonad F) where

open import Data.Nat     using (ℕ; zero; suc; _+_)
open import Data.List    using (List; []; _∷_; _++_; reverse; length)
open import Data.Product using (_×_; _,_)
open import Data.String  using (String)
open import Function     using (_∘_)
open import Reflection

open RawMonad MF

------------------------------------------------------------------------
-- Context representation

-- Track both number of variables and actual context, to avoid having to
-- compute the length of the context everytime it's needed.
record Cxt : Set where
  constructor _,,_
  pattern
  field
    len     : ℕ
    context : List (String × Arg Term)

private
  _∷cxt_ : String × Arg Term → Cxt → Cxt
  e ∷cxt (n ,, Γ) = (suc n ,, (e ∷ Γ))

  _++cxt_ : List (String × Arg Term) → Cxt → Cxt
  es ++cxt (n ,, Γ) = ((length es + n) ,, (es ++ Γ))

------------------------------------------------------------------------
-- Actions

Action : Set → Set
Action A = Cxt → A → F A
-- A traversal gets to operate on variables, metas, and names.
record Actions : Set where
  field
    onVar  : Action ℕ
    onMeta : Action Meta
    onCon  : Action Name
    onDef  : Action Name

-- Default action: do nothing.
defaultActions : Actions
defaultActions .Actions.onVar  _ = pure
defaultActions .Actions.onMeta _ = pure
defaultActions .Actions.onCon  _ = pure
defaultActions .Actions.onDef  _ = pure

------------------------------------------------------------------------
-- Traversal functions
private
 module Params (actions : Actions) (everyAction : Action Term) where

  open Actions actions

  everywhereTerm    : Action Term
  everywhereTerm'    : Action Term
  everywhereSort    : Action Sort
  everywherePattern : Action Pattern
  everywhereArgs    : Action (List (Arg Term))
  everywhereArg     : Action (Arg Term)
  everywherePats    : Action (List (Arg Pattern))
  everywhereAbs     : Arg Term → Action (Abs Term)
  everywhereClauses : Action Clauses
  everywhereClause  : Action Clause
  everywhereTel     : Action (List (String × Arg Term))

  everywhereTerm Γ t = everyAction Γ =<< everywhereTerm' Γ t

  everywhereTerm' Γ (var x args)      = var       <$> onVar Γ x ⊛ everywhereArgs Γ args
  everywhereTerm' Γ (con c args)      = con       <$> onCon Γ c ⊛ everywhereArgs Γ args
  everywhereTerm' Γ (def f args)      = def       <$> onDef Γ f ⊛ everywhereArgs Γ args
  everywhereTerm' Γ (pat-lam cs args) = pat-lam   <$> everywhereClauses Γ cs ⊛ everywhereArgs Γ args
  everywhereTerm' Γ (pi a b)          = pi        <$> everywhereArg Γ a ⊛ everywhereAbs a Γ b
  everywhereTerm' Γ (agda-sort s)     = agda-sort <$> everywhereSort Γ s
  everywhereTerm' Γ (meta x args)     = meta      <$> onMeta Γ x ⊛ everywhereArgs Γ args
  everywhereTerm' Γ t@(lit _)         = pure t
  everywhereTerm' Γ t@unknown         = pure t
  everywhereTerm' Γ (lam v t)         = lam v     <$> everywhereAbs (arg (arg-info v m) unknown) Γ t
    where
    m = defaultModality

  everywhereArg Γ (arg i t) = arg i <$> everywhereTerm Γ t
  everywhereArgs Γ []       = pure []
  everywhereArgs Γ (a ∷ as) = _∷_ <$> everywhereArg Γ a ⊛ everywhereArgs Γ as

  everywhereAbs ty Γ (abs x t) = abs x <$> everywhereTerm ((x , ty) ∷cxt Γ) t

  everywhereClauses Γ []       = pure []
  everywhereClauses Γ (c ∷ cs) = _∷_ <$> everywhereClause Γ c ⊛ everywhereClauses Γ cs

  everywhereClause Γ (Clause.clause tel ps t) =
      Clause.clause <$> everywhereTel Γ tel
                     ⊛  everywherePats Γ′ ps
                     ⊛ everywhereTerm Γ′ t
    where Γ′ = reverse tel ++cxt Γ
  everywhereClause Γ (Clause.absurd-clause tel ps) =
      Clause.absurd-clause <$> everywhereTel Γ tel
                            ⊛  everywherePats Γ′ ps
    where Γ′ = reverse tel ++cxt Γ

  everywhereTel Γ [] = pure []
  everywhereTel Γ ((x , ty) ∷ tel) =
    _∷_ ∘ (x ,_) <$> everywhereArg Γ ty ⊛ everywhereTel ((x , ty) ∷cxt Γ) tel

  everywhereSort Γ (Sort.set t)       = Sort.set <$> everywhereTerm Γ t
  everywhereSort Γ t@(Sort.lit _)     = pure t
  everywhereSort Γ (Sort.prop t)      = Sort.prop <$> everywhereTerm Γ t
  everywhereSort Γ t@(Sort.propLit _) = pure t
  everywhereSort Γ t@(Sort.inf _)     = pure t
  everywhereSort Γ t@Sort.unknown     = pure t

  everywherePattern Γ (Pattern.con c ps) = Pattern.con <$> onCon Γ c ⊛ everywherePats Γ ps
  everywherePattern Γ (Pattern.dot t)    = Pattern.dot <$> everywhereTerm Γ t
  everywherePattern Γ (Pattern.var x)    = Pattern.var <$> onVar Γ x
  everywherePattern Γ p@(Pattern.lit _)  = pure p
  everywherePattern Γ p@(Pattern.proj _) = pure p
  everywherePattern Γ (Pattern.absurd x) = Pattern.absurd <$> onVar Γ x

  everywherePats Γ [] = pure []
  everywherePats Γ (arg i p ∷ ps) = _∷_ ∘ arg i <$> everywherePattern Γ p ⊛ everywherePats Γ ps

everywhere : (actions : Actions) → (everyAction : Action Term) → Term → F Term
everywhere actions every = Params.everywhereTerm actions every (0 ,, [])

max_stars_repo_name: JoeyEremondi/AgdaLeftovers

max_issues_repo_name: JoeyEremondi/AgdaLeftovers

max_forks_repo_name: JoeyEremondi/AgdaLeftovers


text:
{-# OPTIONS --universe-polymorphism #-}
module Reflection where

open import Common.Prelude hiding (Unit; module Unit) renaming (Nat to ℕ; module Nat to ℕ)
open import Common.Reflection
open import Common.Equality
open import Agda.Builtin.TrustMe

data Id {A : Set}(x : A) : (B : Set) → B → Set where
  course : Id x A x

open import Common.Level

set₀ : Type
set₀ = sort (lit 0)

unCheck : Term → Term
unCheck (def x (_ ∷ _ ∷ arg _ t ∷ [])) = t
unCheck t = unknown

infix 1 _is_of_
data Check {a}{A : Set a}(x : A) : Set where
  _is_of_ : (t t′ : Term) →
            Id (primTrustMe {x = unCheck t} {t′})
               (t′ ≡ t′) refl → Check x

`Check : QName
`Check = quote Check

test₁ : Check ({A : Set} → A → A)
test₁ = quoteGoal t in
        t is pi (hArg set₀) (abs "A" (pi (vArg (var 0 [])) (abs "_" (var 1 []))))
        of course

test₂ : (X : Set) → Check (λ (x : X) → x)
test₂ X = quoteGoal t in
          t is lam visible (abs "x" (var 0 [])) of course

infixr 5 _`∷_

pattern _`∷_ x xs = con (quote _∷_) (hArg unknown ∷ hArg unknown ∷ vArg x ∷ vArg xs ∷ [])
pattern `[]    = con (quote []) (hArg unknown ∷ hArg unknown ∷ [])
pattern `true  = con (quote true) []
pattern `false = con (quote false) []

test₃ : Check (true ∷ false ∷ [])
test₃ = quoteGoal t in
        t is (`true `∷ `false `∷ `[]) of course

`List : Term → Term
`List A = def (quote List) (hArg (def (quote lzero) []) ∷ vArg A ∷ [])
`ℕ      = def (quote ℕ) []

`Term : Term
`Term = def (quote Term) []
`Type : Term
`Type = def (quote Type) []
`Sort : Term
`Sort = def (quote Sort) []

test₄ : Check (List ℕ)
test₄ = quoteGoal t in
        t is `List `ℕ of course

postulate
  a : ℕ

test₁₄ : Check 1
test₁₄ = quoteGoal t in t is lit (nat 1) of course

record R : Set₁ where
  field
    A : Set

macro

  RA : Term → TC _
  RA goal = bindTC (getDefinition (quote R)) λ where
    (recordDef _ (vArg A ∷ [])) → unify goal (def A [])
    _                           → typeError (strErr "Impossible" ∷ [])

test₁₅ : RA ≡ R.A
test₁₅ = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module Data.Real where

open import Data.Real.Base public

open import Data.Real.Order public

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
module MJ.Examples.While where

open import MJ.Examples.Integer

open import Prelude
open import MJ.Types
open import MJ.Classtable.Code Σ
open import MJ.Syntax Σ
open import MJ.Syntax.Program Σ
open import MJ.Semantics Σ Lib
open import MJ.Semantics.Values Σ
open import Data.List.Any
open import Data.List.Membership.Propositional
open import Data.Star
open import Data.Bool as Bools hiding (_≤?_)
open import Relation.Nullary.Decidable

-- a simple program that computes 10 using a while loop
p₁ : Prog int
p₁ = Lib ,
  let
    x = (here refl)
  in body
    (
        loc int
      ◅ asgn x (num 1)
      ◅ while iop (λ x y → Bools.if ⌊ suc x ≤? y ⌋ then 0 else 1) (var x) (num 10) run (
        asgn x (iop (λ x y → x + y) (var x) (num 1))
      )
      -- test simplest if-then-else and early return from statement
      ◅ if (num 0) then (ret (var x)) else (ret (num 0))
      ◅ ε
    )
    (num 0)

test1 : p₁ ⇓⟨ 100 ⟩ (λ {W} (v : Val W int) → v ≡ num 10)
test1 = refl


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

module Function.Biconditional where

open import Level
open import Relation.Binary
open import Path as ≡ using (_;_; cong)
open import Function

infix 4 _↔_
record _↔_ {a b} (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  constructor _iff_
  field
    fun : A → B
    inv : B → A
open _↔_ public

sym-↔ : (A ↔ B) → (B ↔ A)
fun (sym-↔ A↔B) = inv A↔B
inv (sym-↔ A↔B) = fun A↔B

refl-↔ : A ↔ A
fun refl-↔ = id
inv refl-↔ = id

trans-↔ : A ↔ B → B ↔ C → A ↔ C
fun (trans-↔ A↔B B↔C) = fun B↔C ∘ fun A↔B
inv (trans-↔ A↔B B↔C) = inv A↔B ∘ inv B↔C

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Reflexivity where
import PolyDepPrelude
open PolyDepPrelude using(Bool; True)

-- Local reflexivity

lref : {X : Set} -> (X -> X -> Bool) -> X -> Set
lref _R_ = \x -> True (x R x)

-- Reflexive = locally reflexive everywhere

data Refl {X : Set} (r : X -> X -> Bool) : Set where
  refl : ((x : X) -> lref r x) -> Refl r

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda