text:
{-# OPTIONS --without-K #-}
open import Data.Bits.Search
open import Data.Nat.NP

open import Function.NP

import Relation.Binary.PropositionalEquality.NP as ≡
open ≡

module Data.Bits.Sum where
    open SimpleSearch _+_ using (module Comm; module SearchInterchange; module SearchUnit; module Bij)
    open SimpleSearch _+_ public using () renaming (search to sum; search-≗ to sum-≗; searchBit to sumBit;
                                                    search-≗₂ to sum-≗₂;
                                                    search-+ to sum-+)
    open Comm ℕ°.+-comm public renaming (search-comm to sum-comm)
    open SearchUnit 0 refl public renaming
       (search-constε≡ε to sum-const0≡0)
    open SearchInterchange +-interchange public renaming (
        search-dist to sum-dist;
        search-searchBit to sum-sumBit;
        search-search to sum-sum;
        search-swap to sum-swap)
    open Bij ℕ°.+-comm +-interchange public renaming (search-bij to sum-bij)

    sum-const : ∀ n x → sum {n} (const x) ≡ ⟨2^ n * x ⟩
    sum-const zero    _ = refl
    sum-const (suc n) x = cong₂ _+_ (sum-const n x) (sum-const n x)

ext: agda

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module x05isomorphism where

{-
------------------------------------------------------------------------------
Isomorphism: Isomorphism and Embedding

isomorphism
- way of asserting two types are equal

embedding
- way of asserting that one type is smaller than another

apply isomorphisms in next chapter to show 'product' and 'sum' satisfy properties
similar to associativity, commutativity, and distributivity
-}

import Relation.Binary.PropositionalEquality as Eq
open        Eq                  using (_≡_; refl; cong; cong-app)
open        Eq.≡-Reasoning
open import Data.Nat            using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

{-
------------------------------------------------------------------------------
LAMBDA EXPRESSIONS : ANONYMOUS FUNS

λ{ P₁ → N₁; ⋯ ; Ppₙ → Np }

equivalent def by equations

f P₁ = N₁
⋯
f Pp = Npₙ

where
- P are patterns    (left-hand sides of an equation)
- N are expressions (right-hand side of an equation)

for case of one equation and pattern is a variable:

λ x → N

or

λ (x : A) → N

equivalent to

λ{x → N}

------------------------------------------------------------------------------
Function composition
-}

-- first apply f, then apply g to result
_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) x  = g (f x)

-- equivalent
_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘′ f  =  λ x → g (f x)

{-
------------------------------------------------------------------------------
EXTENSIONALITY : only way to distinguish functions is by applying them

If two functions applied to same arg always give same result, then they are same.

converse of cong-app

Agda does not presume extensionality, so
-}

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    →              f   ≡ g

{-
Postulating extensionality does not lead to difficulties.
It is known to be consistent with the theory that underlies Agda.

example
-}

-- version that matches on right
_+′_ : ℕ → ℕ → ℕ
m +′ zero  = m
m +′ suc n = suc (m +′ n)

-- using commutativity, show + and +′ always return same result for same arg
same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m n                --     (m +′ n) ≡      m + n
  rewrite +-comm m n        --     (m +′ n) ≡      n + m
  = helper m n
 where
  helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
  helper m   zero  = refl
  helper m (suc n)          -- suc (m +′ n) ≡ suc (n + m)
    = cong suc (helper m n)

-- now assert + and +′ to be indistinguishable (via two applications of extensionality)
same : _+′_ ≡ _+_
same = extensionality (λ m → extensionality (λ n → same-app m n))

{-
to postulate extensionality in what follows
(and to postulate extensionality for dependent functions):
-}

-- type of f and g has changed from A → B to ∀ (x : A) → B x
postulate
  ∀-extensionality : ∀ {A : Set} {B : A → Set} {f g : ∀(x : A) → B x}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    →              f   ≡ g

{-
------------------------------------------------------------------------------
ISOMORPHISM : sets are isomorphic if they are in one-to-one correspondence

formal definition:
-}

infix 0 _≃_

-- RECORD
-- isomorphism between sets A and B consists of four things
record _≃_ (A B : Set) : Set where
  field
    to      : A → B                       -- function from A to B
    from    : B → A                       -- function from B to A
    from∘to : ∀ (x : A) → from (to x) ≡ x -- evidence asserting 'from' is a  left-inverse for 'to'
    to∘from : ∀ (y : B) → to (from y) ≡ y -- evidence asserting 'from' is a right-inverse for 'to'
open _≃_ -- makes field names 'to', etc., available without needing to write '_≃_.to'

{-
from ∘ to AND to ∘ from are identities

record declaration behaves similar to single-constructor data declaration
(there are minor differences - see Connectives):
-}
data _≃′_ (A B : Set): Set where
  mk-≃′ : ∀ (to      : A → B)
        → ∀ (from    : B → A)
        → ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x))
        → ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y))
        → A ≃′ B

to′      : ∀ {A B : Set} → (A ≃′ B) → (A → B)
to′      (mk-≃′ f g g∘f f∘g) = f

from′    : ∀ {A B : Set} → (A ≃′ B) → (B → A)
from′    (mk-≃′ f g g∘f f∘g) = g

from∘to′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (x : A) → from′ A≃B (to′ A≃B x) ≡ x)
from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

to∘from′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (y : B) → to′ A≃B (from′ A≃B y) ≡ y)
to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g

{-
construct record values via

record
  { to      = f
  ; from    = g
  ; from∘to = g∘f
  ; to∘from = f∘g
  }

corresponds to using the constructor of the corresponding inductive type

mk-≃′ f g g∘f f∘g

------------------------------------------------------------------------------
ISOMORPHISM is an EQUIVALENCE : REFLEXIVE, SYMMETRIC, and TRANSITIVE
-}

-- REFLEXIVE
≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}    -- bind to identity function
    ; from    = λ{y → y}    -- ditto
    -- refl next is proof since for left inverse, from (to x) simplifies to x, and vice versa
    ; from∘to = λ{x → refl} -- bound to fun that discards arg; returns refl
    ; to∘from = λ{y → refl} -- ditto
    }

-- SYMMETRIC : swap roles of to/from and from∘to/to∘from
≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A
≃-sym A≃B =
  record
    { to      = from    A≃B
    ; from    = to      A≃B
    ; from∘to = to∘from A≃B
    ; to∘from = from∘to A≃B
    }

-- TRANSITIVE : compose to/from and use equational reasoning to combine inverses
≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C
≃-trans A≃B B≃C =
  record
    { to       = to   B≃C ∘ to   A≃B
    ; from     = from A≃B ∘ from B≃C
    ; from∘to  = λ{x →
      begin
        (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)   ≡⟨⟩
         from A≃B  (from B≃C   (to B≃C  (to A≃B  x))) ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
         from A≃B                       (to A≃B  x)   ≡⟨ from∘to A≃B x ⟩
                                                 x
      ∎}
    ; to∘from = λ{y →
      begin
        (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)   ≡⟨⟩
         to B≃C  (to A≃B   (from A≃B  (from B≃C  y))) ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
         to B≃C                       (from B≃C  y)   ≡⟨ to∘from B≃C y ⟩
                                                 y
      ∎}
     }
{-
------------------------------------------------------------------------------
EQUATIONAL REASONING FOR ISOMORPHISM

Essentially copy previous definition of equality for isomorphism.
Omit the form that corresponds to _≡⟨⟩_,
since simple isomorphisms arise less often than simple equalities
-}

module ≃-Reasoning where

  infix  1 ≃-begin_
  infixr 2 _≃⟨_⟩_
  infix  3 _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

{-
------------------------------------------------------------------------------
EMBEDDING : WEAKENING of ISOMORPHISM : EMBEDDING SHOWS 1ST TYPE INCLUDED IN SECOND
i.e., there is many-to-one correspondence between second type and first
-}

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

{-
same as isomorphism, except it omits 'to∘from' field
- says 'from' is left-inverse for 'to', but not a right-inverse

EMBEDDING IS NOT SYMMETRIC

proofs of REFLEXIVE and TRANSITIVE same as ISOMORPHISM except omitting one unneeded case
-}

-- REFLEXIVE
≲-refl : ∀ {A : Set} → A ≲ A
≲-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    }

-- TRANSITIVE
≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
≲-trans A≲B B≲C =
  record
    { to      = λ{x → to   B≲C (to   A≲B x)}
    ; from    = λ{y → from A≲B (from B≲C y)}
    ; from∘to = λ{x →
      begin
        from A≲B (from B≲C (to B≲C (to A≲B x))) ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B x)) ⟩
        from A≲B                   (to A≲B x)   ≡⟨ from∘to A≲B x ⟩
                                           x
      ∎}
     }
{-
weak form of ANTI-SYMMETRY
if two types embed in each other, and embedding functions correspond, they are isomorphic
-}

≲-antisym : ∀ {A B : Set}
  → (A≲B : A ≲ B)
  → (B≲A : B ≲ A)
  → (to   A≲B ≡ from B≲A)
  → (from A≲B ≡ to   B≲A)
    -------------------
  → A ≃ B
≲-antisym A≲B B≲A to≡from from≡to =
  record
    { to      = to      A≲B
    ; from    = from    A≲B
    ; from∘to = from∘to A≲B
    ; to∘from = λ{y →
      begin
        to   A≲B (from A≲B y)   ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
        to   A≲B (to   B≲A y)   ≡⟨ cong-app to≡from (to B≲A y) ⟩
        from B≲A (to   B≲A y)   ≡⟨ from∘to B≲A y ⟩
                           y
      ∎}
    }

{-
First three components are copied from the embedding.
The last combines left inverse of B ≲ A with the equivalences of the 'to' and 'from' components
from the two embeddings to obtain the right inverse of the isomorphism.

------------------------------------------------------------------------------
Equational reasoning for embedding
-}

module ≲-Reasoning where

  infix  1 ≲-begin_
  infixr 2 _≲⟨_⟩_
  infix  3 _≲-∎

  ≲-begin_ : ∀ {A B : Set}
    → A ≲ B
      -----
    → A ≲ B
  ≲-begin A≲B = A≲B

  _≲⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≲ B
    →     B ≲ C
      -----
    → A ≲     C
  A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

  _≲-∎ : ∀ (A : Set)
      -----
    → A ≲ A
  A ≲-∎ = ≲-refl

open ≲-Reasoning

{-
------------------------------------------------------------------------------
Exercise ≃-implies-≲ (practice) Show that every isomorphism implies an embedding. TODO

postulate
  ≃-implies-≲ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≲ B
-- Your code goes here

------------------------------------------------------------------------------
Exercise _⇔_ (practice) Define equivalence of propositions TODO
(also known as “if and only if”) as follows:

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
Show that equivalence is reflexive, symmetric, and transitive.

-- Your code goes here

------------------------------------------------------------------------------
Exercise Bin-embedding (stretch) TODO

Bin and Bin-laws define a datatype Bin of bitstrings representing natural numbers
with functions

to : ℕ → Bin
from : Bin → ℕ

that satisfy

from (to n) ≡ n

Using the above, establish that there is an embedding of ℕ into Bin.

-- Your code goes here

Why do to and from not form an isomorphism?

------------------------------------------------------------------------------
Standard library

import Function             using (_∘_)
import Function.Inverse     using (_↔_)
import Function.LeftInverse using (_↞_)

The standard library _↔_ and _↞_ correspond to our _≃_ and _≲_, respectively,
but those in the standard library are less convenient,
since they depend on a nested record structure
and are parameterised with regard to an arbitrary notion of equivalence.

------------------------------------------------------------------------------
Unicode
This chapter uses the following unicode:

∘  U+2218  RING OPERATOR              (\o, \circ, \comp)
λ  U+03BB  GREEK SMALL LETTER LAMBDA  (\lambda, \Gl)
≃  U+2243  ASYMPTOTICALLY EQUAL TO    (\~-)
≲  U+2272  LESS-THAN OR EQUIVALENT TO (\<~)
⇔ U+21D4  LEFT RIGHT DOUBLE ARROW    (\<=>)
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
open import Common.Prelude
open import Common.Reflection

module TermSplicingOutOfScope where

f : Set → Set → Set → Set
f x y z = unquote (give (var 3 []))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Hash
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Util.Util
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId

-- This is a minimal/fake example handler that obeys the VotesOnce rule, enabling us to start
-- exploring how we express the algorithm and prove properties about it.  It simply sends a vote for
-- 1 + its LatestVotedRound, and increments its LatestVotedRound.  It is called RoundManager for
-- historical reasons, because this what a previous version of LibraBFT called its main handler;
-- this will be updated when we move towards modeling a more recent implementation.

module LibraBFT.Impl.Consensus.RoundManager where

  open RWST-do

  processCommitM : LedgerInfoWithSignatures → LBFT (List ExecutedBlock)
  processCommitM finalityProof = pure []

  fakeAuthor : Author
  fakeAuthor = 0

  fakeBlockInfo : Epoch → Round → ProposalMsg → BlockInfo
  fakeBlockInfo eid rnd pm = BlockInfo∙new eid rnd (pm ^∙ pmProposal ∙ bId)

  fakeLedgerInfo : BlockInfo → ProposalMsg → LedgerInfo
  fakeLedgerInfo bi pm = LedgerInfo∙new bi (pm ^∙ pmProposal ∙ bId)

  postulate -- TODO-1: these are temporary scaffolding for the fake implementation
    fakeSK  : SK
    fakeSig : Signature

  processProposalMsg : Instant → ProposalMsg → LBFT Unit
  processProposalMsg inst pm = do
    st ← get
    xx ← use rmHighestQC   -- Not used; just a demonstration that our RoundManager-specific "use" works
    modify' rmHighestQC xx -- Similarly for modify'
    let RoundManager∙new rm rmc rmw = st
        𝓔  = α-EC (rm , rmc)
        e  = rm ^∙ rmEpoch
        nr = suc (rm ^∙ rmLastVotedRound)
        uv = Vote∙new
                    (VoteData∙new (fakeBlockInfo e nr pm) (fakeBlockInfo e 0 pm))
                    fakeAuthor
                    (fakeLedgerInfo (fakeBlockInfo e nr pm) pm)
                    fakeSig
                    nothing
        sv = record uv { ₋vSignature = sign ⦃ sig-Vote ⦄ uv fakeSK}
        bt = rmw ^∙ (lBlockTree 𝓔)
        si = SyncInfo∙new (₋btHighestQuorumCert bt) (₋btHighestCommitCert bt)
        rm' = rm [ rmLastVotedRound := nr ]
        st' = RoundManager∙new rm' (RoundManagerEC-correct-≡ (₋rmEC st) rm' refl rmc)
                                   (subst RoundManagerWithEC (α-EC-≡ rm rm' refl refl rmc) rmw)
    put st'
    tell1 (SendVote (VoteMsg∙new sv si) (fakeAuthor ∷ []))
    pure unit

  processVote : Instant → VoteMsg → LBFT Unit
  processVote now msg = pure unit

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
open import Agda.Builtin.Nat

record _×_ (A B : Set) : Set where
  constructor _,_
  field fst : A
        snd : B

open _×_

Δ : ∀ {A} → A → A × A
Δ x = x , x

foo : Nat → Nat
foo n = let x , y = Δ n in x + y

bar : Nat → Nat
bar n = let _!_ : Nat → Nat → Nat
            x ! y = 2 * x + y
        in n ! n

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Data.Empty
open import Data.Maybe
open import Data.Product
open import Data.Sum

open import AEff
open import EffectAnnotations
open import Types

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Negation

module AwaitingComputations where

-- COMPUTATIONS THAT ARE TEMPORARILY STUCK DUE TO AWAITING FOR A PARTICULAR PROMISE

data _⧗_ {Γ : Ctx} {X : VType} (x : ⟨ X ⟩ ∈ Γ) : {C : CType} → Γ ⊢M⦂ C → Set where

  await     : {C : CType}
              {M : Γ ∷ X ⊢M⦂ C} →
              -------------------------
              x ⧗ (await (` x) until M)

  let-in    : {X Y : VType}
              {o : O}
              {i : I}
              {M : Γ ⊢M⦂ X ! (o , i)}
              {N : Γ ∷ X ⊢M⦂ Y ! (o , i)} →
              x ⧗ M →
              -----------------------------
              x ⧗ (let= M `in N)

  interrupt : {X : VType}
              {o : O}
              {i : I}
              {op : Σₛ}
              {V : Γ ⊢V⦂ ``(payload op)}
              {M : Γ ⊢M⦂ X ! (o , i)} →
              x ⧗ M →
              -------------------------
              x ⧗ (↓ op V M)

  coerce    : {X : VType}
              {o o' : O}
              {i i' : I}
              {p : o ⊑ₒ o'}
              {q : i ⊑ᵢ i'}
              {M : Γ ⊢M⦂ X ! (o , i)} →
              x ⧗ M →
              -------------------------
              x ⧗ (coerce p q M)

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


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

module Dodo.Binary.Immediate where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; subst) renaming (sym to ≡-sym)
open import Level using (Level; _⊔_)
open import Function using (_∘_; flip)
open import Data.Empty using (⊥-elim)
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel; REL)
open import Relation.Binary using (IsStrictTotalOrder; Irreflexive; Trichotomous)
open import Relation.Binary using (Transitive)
open import Relation.Binary using (Tri; tri<; tri≈; tri>)
open import Relation.Binary.Construct.Closure.Transitive using (TransClosure; [_]; _∷_; _∷ʳ_; _++_)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Unary.Unique
open import Dodo.Binary.Equality
open import Dodo.Binary.Transitive
open import Dodo.Binary.Functional
open import Dodo.Binary.Filter
open import Dodo.Binary.Domain

-- # Definitions #

-- | The immediate relation over the given (order) relation
immediate : ∀ {a ℓ : Level} {A : Set a}
  → Rel A ℓ
    -------------
  → Rel A (a ⊔ ℓ)
immediate r x y = r x y × ¬ (∃[ z ] r x z × TransClosure r z y)
-- A more conventional definitions is:
-- immediate r x y = r x y × (¬ ∃ λ{z → r x z × r z y})
-- which is identical to this one when r is Transitive

Immediate : ∀ {a ℓ : Level} {A : Set a}
  → Rel A ℓ
  → Set (a ⊔ ℓ)
-- For some reason, x and y have to be /explicit/. Otherwise, Agda complains about some
-- of Immediate's uses. Unsure why.
Immediate {A = A} r = ∀ (x y : A) → r x y → ¬ (∃[ z ] r x z × TransClosure r z y)

-- # Operations #

imm-flip : ∀ {a ℓ : Level} {A : Set a}
  → {R : Rel A ℓ} {x y : A}
  → immediate R x y
  → immediate (flip R) y x
imm-flip {R = R} {x} {y} (Rxy , ¬∃z) = (Rxy , lemma)
  where
  ⁺-invert : {a ℓ : Level} {A : Set a} {R : Rel A ℓ} {x y : A}
    → {z : A} → R x z → TransClosure R z y
    → ∃[ q ] (TransClosure R x q × R q y)
  ⁺-invert {z = z} Rxz [ Rzy ] = (z , [ Rxz ] , Rzy)
  ⁺-invert {z = z} Rxz ( Rzq ∷ R⁺qy ) with ⁺-invert Rzq R⁺qy
  ... | v , R⁺zv , Rvy = (v , Rxz ∷ R⁺zv , Rvy)

  lemma : ¬ (∃[ z ] (flip R y z × TransClosure (flip R) z x))
  lemma (z , flipRyz , flipR⁺zx) =
    let (q , R⁺yq , Rqx) = ⁺-invert flipRyz flipR⁺zx
    in ¬∃z (q , Rqx , ⁺-flip R⁺yq)

-- # Properties #

module _ {a ℓ : Level} {A : Set a} {R : Rel A ℓ} where

  imm-imm : Immediate (immediate R)
  imm-imm _ _ (Rxy , ¬∃z) (z , (Rxz , ¬∃w) , [immR]⁺xy) = ¬∃z (z , Rxz , ⁺-map _ proj₁ [immR]⁺xy)

  imm-⊆₂ : immediate R ⊆₂ R
  imm-⊆₂ = ⊆: λ{_ _ → proj₁}

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where

  imm-uniqueˡ : Trichotomous _≈_ _<_ → {z : A} → Unique₁ _≈_ λ{τ → immediate _<_ τ z}
  imm-uniqueˡ triR {z} {x} {y} (Rxz , ¬∃y) (Ryz , ¬∃x) with triR x y
  ... | tri<  Rxy x≉y ¬Ryx = ⊥-elim (¬∃y (y , Rxy , [ Ryz ]))
  ... | tri≈ ¬Rxy x≈y ¬Ryx = x≈y
  ... | tri> ¬Rxy x≉y  Ryx = ⊥-elim (¬∃x (x , Ryx , [ Rxz ]))

  imm-uniqueʳ : Trichotomous _≈_ _<_ → {x : A} → Unique₁ _≈_ (immediate _<_ x)
  imm-uniqueʳ triR {x} {y} {z} (Rxy , ¬∃z) (Rxz , ¬∃y) with triR y z
  ... | tri<  Ryz y≈z ¬Rzy = ⊥-elim (¬∃y (y , Rxy , [ Ryz ]))
  ... | tri≈ ¬Ryz y≈z ¬Rzy = y≈z
  ... | tri> ¬Ryz y≈z  Rzy = ⊥-elim (¬∃z (z , Rxz , [ Rzy ]))

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {≈ : Rel A ℓ₁} {< : Rel A ℓ₂} where

  -- immediate < x y → immediate < x z → y ≈ z
  imm-func : IsStrictTotalOrder ≈ < → Functional ≈ (immediate <)
  imm-func sto x y₁ y₂ (x<y₁ , ¬∃z[x<z×z<y₁]) (x<y₂ , ¬∃z[x<z×z<y₂])
      with IsStrictTotalOrder.compare sto y₁ y₂
  ... | tri< y₁<y₂ _     _     = ⊥-elim (¬∃z[x<z×z<y₂] (y₁ , x<y₁ , [ y₁<y₂ ]))
  ... | tri≈ _     y₁≈y₂ _     = y₁≈y₂
  ... | tri> _     _     y₂<y₁ = ⊥-elim (¬∃z[x<z×z<y₁] (y₂ , x<y₂ , [ y₂<y₁ ]))

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Rel A ℓ₂} where

  imm-filter-⊆₂ : filter-rel P (immediate R) ⊆₂ immediate (filter-rel P R)
  imm-filter-⊆₂ = ⊆: lemma
    where
    lemma : filter-rel P (immediate R) ⊆₂' immediate (filter-rel P R)
    lemma (with-pred x Px) (with-pred y Py) (Rxy , ¬∃z) = Rxy , ¬∃z'
      where
      ¬∃z' : ¬ (∃[ z ] (filter-rel P R (with-pred x Px) z × TransClosure (filter-rel P R) z (with-pred y Py)))
      ¬∃z' (with-pred z Pz , Rxz , fR⁺zy) = ¬∃z (z , Rxz , ⁺-strip-filter fR⁺zy)

module _ {a ℓ : Level} {A : Set a} {R : Rel A ℓ} where

  immediate⁺ : Immediate R → R ⇔₂ immediate (TransClosure R)
  immediate⁺ immR = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : R ⊆₂' immediate (TransClosure R)
    ⊆-proof x y xRy = ([ xRy ] , lemma x y xRy)
      where
      lemma : (x y : A) → R x y → ¬ (∃[ z ] TransClosure R x z × TransClosure (TransClosure R) z y)
      lemma x y xRy (z , [ xRz ] , zR⁺y) =
        immR x y xRy (z , xRz , ⇔₂-apply-⊇₂ ⁺-idem zR⁺y)
      lemma x y xRy (z , _∷_ {_} {w} xRw wR⁺z , zR⁺y) =
        immR x y xRy (w , xRw , ⇔₂-apply-⊇₂ ⁺-idem (wR⁺z ∷ zR⁺y))

    ⊇-proof : immediate (TransClosure R) ⊆₂' R
    ⊇-proof x y ([ x∼y ] , ¬∃z) = x∼y
    ⊇-proof x y (_∷_ {_} {w} x∼w wR⁺y , ¬∃z) = ⊥-elim (¬∃z (w , [ x∼w ] , [ wR⁺y ]))

  trans-imm⁺-⊆ : Transitive R → TransClosure (immediate R) ⊆₂ R
  trans-imm⁺-⊆ transR = ⊆: lemma
    where
    lemma : TransClosure (immediate R) ⊆₂' R
    lemma x y [ R[xy] ] = proj₁ R[xy]
    lemma x y (_∷_ {_} {z} R[xz] R⁺[zy]) = transR (proj₁ R[xz]) (lemma z y R⁺[zy])

  imm-udr-⊆₁ : udr (immediate R) ⊆₁ udr R
  imm-udr-⊆₁ = ⊆: lemma
    where
    lemma : udr (immediate R) ⊆₁' udr R
    lemma _ (inj₁ (y , Rxy , ¬∃z)) = inj₁ (y , Rxy)
    lemma _ (inj₂ (x , Rxy , ¬∃z)) = inj₂ (x , Rxy)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
module Signature where

open import Data.Product renaming (Σ to ⨿)
open import Function
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
open import Function
open import Data.Empty
open import Data.Unit hiding (_≤_)
open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Nat as Nat
open import Data.Sum as Sum

record Sig : Set₁ where
  field
    ∥_∥ : Set
    ar : ∥_∥ → Set
open Sig public

-- | Extension of signature Σ, on objects
⟪_⟫ : Sig → Set → Set
⟪ Σ ⟫ X = ⨿ ∥ Σ ∥ λ f → (ar Σ f → X)

-- | Extension of signature Σ, on morphisms
⟪_⟫₁ : (Σ : Sig) {A B : Set} → (A → B) → ⟪ Σ ⟫ A → ⟪ Σ ⟫ B
⟪_⟫₁ Σ f (s , α) = (s , f ∘ α)

-- | Lift ⟪ Σ ⟫ to relations
sig-lift : {Σ : Sig} {X : Set} (R : X → X → Set) (x y : ⟪ Σ ⟫ X) → Set
sig-lift {Σ} R (f , α) (g , β) =
  ⨿ (f ≡ g) λ p → ∀ {i} → R (α i) (β (subst (Sig.ar Σ) p i))

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module Lattice where

open import Prelude
open import PartialOrder as PO
open import SemiLattice  as SL
import Chain
open POrder using (Dual)

record Lattice (A : Set) : Set1 where
  field
    sl : SemiLattice A
    _⊔_ : A -> A -> A
    prf : IsSemiLattice (Dual (SemiLat.po sl)) _⊔_

module Lat {A : Set}(L : Lattice A) where

  private
    module LL    = Lattice L
    module SLL   = SemiLat LL.sl

  private
    sl' : SemiLattice A
    sl' = record { po = Dual SLL.po; _⊓_ = LL._⊔_; prf = LL.prf }

    module SLL'  = SemiLat sl'
      hiding   ( Monotone
               ; Antitone
               ; _==_; ==-refl; ==-sym; ==-trans
               ; po
               )
      renaming ( _≤_          to _≥_
               ; ≤-refl       to ≥-refl
               ; ≤-trans      to ≥-trans
               ; ≤-antisym    to ≥-antisym
               ; ==≤-L        to ==≥-R
               ; ==≤-R        to ==≥-L
               ; _⊓_          to _⊔_
               ; ⊓-lbL        to ⊔-ubL
               ; ⊓-lbR        to ⊔-ubR
               ; ⊓-glb        to ⊔-lub
               ; ⊓-commute    to ⊔-commute
               ; ⊓-assoc      to ⊔-assoc
               ; ⊓-idem       to ⊔-idem
               ; ≤⊓-L         to ≥⊔-L
               ; ≤⊓-R         to ≥⊔-R
               ; ⊓-monotone-R to ⊔-monotone-R
               ; ⊓-monotone-L to ⊔-monotone-L
               ; ≤⊓-compat    to ≥⊔-compat
               ; ⊓-cong       to ⊔-cong
               ; ⊓-cong-L     to ⊔-cong-L
               ; ⊓-cong-R     to ⊔-cong-R
               )

  open SLL  public
  open SLL' public

  DualLattice : Lattice A
  DualLattice = record { sl = sl'; _⊔_ = _⊓_; prf = SemiLattice.prf LL.sl }

module MeetJoin {A : Set}(L : Lattice A) where

  private module L = Lat L
  open L

  open module C== = Chain _==_ (\x -> ==-refl) (\x y z -> ==-trans)

  -- Experiment with very explicit proof
  ⊓⊔-absorb-LL = \{x y} ->
    (x ⊓ (x ⊔ y)) == x  from
      ≤-antisym
        ((x ⊓ (x ⊔ y)) ≤ x from ⊓-lbL)
        (x ≤ (x ⊓ (x ⊔ y)) from
          ⊓-glb (x ≤ x       from ≤-refl)
                (x ≤ (x ⊔ y) from ⊔-ubL)
        )

  ⊓⊔-eq : forall {x y} -> (x ⊓ y) == (x ⊔ y) -> x == y
  ⊓⊔-eq {x}{y} p =
    chain> x
       === x ⊓ (x ⊔ y) by ==-sym ⊓⊔-absorb-LL
       === x ⊓ (x ⊓ y) by ==-sym (⊓-cong-R p)
       === (x ⊓ x) ⊓ y by {!!} -- ⊓-assoc
       === x ⊓ y       by ⊓-cong-L ⊓-idem
       === y ⊓ x       by ⊓-commute
       === (y ⊓ y) ⊓ x by ⊓-cong-L (==-sym ⊓-idem)
       === y ⊓ (y ⊓ x) by ==-sym ⊓-assoc
       === y ⊓ (x ⊓ y) by ⊓-cong-R ⊓-commute
       === y ⊓ (x ⊔ y) by {! !} -- ⊓-cong-R p
       === y ⊓ (y ⊔ x) by ⊓-cong-R ⊔-commute
       === y           by ⊓⊔-absorb-LL

module JoinMeet {A : Set}(L : Lattice A) =
  MeetJoin (Lat.DualLattice L)
  hiding (⊓⊔-eq)
  renaming (⊓⊔-absorb-LL to ⊔⊓-absorb-LL)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Agda.Builtin.Nat

record R : Set₁ where
  field f : Nat

open R ⦃ ... ⦄

foo : Nat → R
foo n .f = {!n!} -- C-c C-c makes clause disappear

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Path
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Bool
open import Cubical.Data.Sigma

open import Cubical.HITs.Join
open import Cubical.HITs.Susp.Base
open import Cubical.Homotopy.Loopspace

private
  variable
    ℓ : Level

open Iso

Susp-iso-joinBool : ∀ {ℓ} {A : Type ℓ} → Iso (Susp A) (join A Bool)
fun Susp-iso-joinBool north = inr true
fun Susp-iso-joinBool south = inr false
fun Susp-iso-joinBool (merid a i) = (sym (push a true) ∙ push a false) i
inv Susp-iso-joinBool (inr true ) = north
inv Susp-iso-joinBool (inr false) = south
inv Susp-iso-joinBool (inl _) = north
inv Susp-iso-joinBool (push a true  i) = north
inv Susp-iso-joinBool (push a false i) = merid a i
rightInv Susp-iso-joinBool (inr true ) = refl
rightInv Susp-iso-joinBool (inr false) = refl
rightInv Susp-iso-joinBool (inl a) = sym (push a true)
rightInv Susp-iso-joinBool (push a true  i) j = push a true (i ∨ ~ j)
rightInv Susp-iso-joinBool (push a false i) j
  = hcomp (λ k → λ { (i = i0) → push a true (~ j)
                   ; (i = i1) → push a false k
                   ; (j = i1) → push a false (i ∧ k) })
          (push a true (~ i ∧ ~ j))
leftInv Susp-iso-joinBool north = refl
leftInv Susp-iso-joinBool south = refl
leftInv (Susp-iso-joinBool {A = A}) (merid a i) j
  = hcomp (λ k → λ { (i = i0) → transp (λ _ → Susp A) (k ∨ j) north
                   ; (i = i1) → transp (λ _ → Susp A) (k ∨ j) (merid a k)
                   ; (j = i1) → merid a (i ∧ k) })
          (transp (λ _ → Susp A) j north)

Susp≃joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≃ join A Bool
Susp≃joinBool = isoToEquiv Susp-iso-joinBool

Susp≡joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≡ join A Bool
Susp≡joinBool = isoToPath Susp-iso-joinBool

congSuspIso : ∀ {ℓ} {A B : Type ℓ} → Iso A B → Iso (Susp A) (Susp B)
fun (congSuspIso is) = suspFun (fun is)
inv (congSuspIso is) = suspFun (inv is)
rightInv (congSuspIso is) north = refl
rightInv (congSuspIso is) south = refl
rightInv (congSuspIso is) (merid a i) j = merid (rightInv is a j) i
leftInv (congSuspIso is) north = refl
leftInv (congSuspIso is) south = refl
leftInv (congSuspIso is) (merid a i) j = merid (leftInv is a j) i

congSuspEquiv : ∀ {ℓ} {A B : Type ℓ} → A ≃ B → Susp A ≃ Susp B
congSuspEquiv {ℓ} {A} {B} h = isoToEquiv (congSuspIso (equivToIso h))

suspToPropElim : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Susp A → Type ℓ'} (a : A)
                 → ((x : Susp A) → isProp (B x))
                 → B north
                 → (x : Susp A) → B x
suspToPropElim a isProp Bnorth north = Bnorth
suspToPropElim {B = B} a isProp Bnorth south = subst B (merid a) Bnorth
suspToPropElim {B = B} a isProp Bnorth (merid a₁ i) =
  isOfHLevel→isOfHLevelDep 1 isProp Bnorth (subst B (merid a) Bnorth) (merid a₁) i

suspToPropElim2 : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Susp A → Susp A → Type ℓ'} (a : A)
                 → ((x y : Susp A) → isProp (B x y))
                 → B north north
                 → (x y : Susp A) → B x y
suspToPropElim2 _ _ Bnorth north north = Bnorth
suspToPropElim2 {B = B} a _ Bnorth north south = subst (B north) (merid a) Bnorth
suspToPropElim2 {B = B} a isprop Bnorth north (merid x i) =
  isProp→PathP (λ i → isprop north (merid x i))
               Bnorth (subst (B north) (merid a) Bnorth) i
suspToPropElim2 {B = B} a _ Bnorth south north = subst (λ x → B x north) (merid a) Bnorth
suspToPropElim2 {B = B} a _ Bnorth south south = subst (λ x → B x x) (merid a) Bnorth
suspToPropElim2 {B = B} a isprop Bnorth south (merid x i) =
  isProp→PathP (λ i → isprop south (merid x i))
               (subst (λ x → B x north) (merid a) Bnorth)
               (subst (λ x → B x x) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) north =
  isProp→PathP (λ i → isprop (merid x i) north)
               Bnorth (subst (λ x → B x north) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) south =
  isProp→PathP (λ i → isprop (merid x i) south)
               (subst (B north) (merid a) Bnorth)
               (subst (λ x → B x x) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) (merid y j) =
  isSet→SquareP (λ i j → isOfHLevelSuc 1 (isprop _ _))
     (isProp→PathP (λ i₁ → isprop north (merid y i₁)) Bnorth
                   (subst (B north) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop south (merid y i₁))
                   (subst (λ x₁ → B x₁ north) (merid a) Bnorth)
                   (subst (λ x₁ → B x₁ x₁) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop (merid x i₁) north) Bnorth
                   (subst (λ x₁ → B x₁ north) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop (merid x i₁) south)
                   (subst (B north) (merid a) Bnorth)
                   (subst (λ x₁ → B x₁ x₁) (merid a) Bnorth)) i j
{- Clever proof:
suspToPropElim2 a isProp Bnorth =
  suspToPropElim a (λ x → isOfHLevelΠ 1 λ y → isProp x y)
                   (suspToPropElim a (λ x → isProp north x) Bnorth)
-}

funSpaceSuspIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
                   → Iso (Σ[ x ∈ B ] Σ[ y ∈ B ] (A → x ≡ y)) (Susp A → B)
Iso.fun funSpaceSuspIso (x , y , f) north = x
Iso.fun funSpaceSuspIso (x , y , f) south = y
Iso.fun funSpaceSuspIso (x , y , f) (merid a i) = f a i
Iso.inv funSpaceSuspIso f = (f north) , (f south , (λ x → cong f (merid x)))
Iso.rightInv funSpaceSuspIso f = funExt λ {north → refl
                                             ; south → refl
                                             ; (merid a i) → refl}
Iso.leftInv funSpaceSuspIso _ = refl

toSusp : (A : Pointed ℓ) → typ A → typ (Ω (Susp∙ (typ A)))
toSusp A x = merid x ∙ merid (pt A) ⁻¹

toSuspPointed : (A : Pointed ℓ) → A →∙ Ω (Susp∙ (typ A))
fst (toSuspPointed A) = toSusp A
snd (toSuspPointed A) = rCancel (merid (pt A))

module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} where
  fromSusp→toΩ : Susp∙ (typ A) →∙ B → (A →∙ Ω B)
  fst (fromSusp→toΩ f) x = sym (snd f) ∙∙ cong (fst f) (toSusp A x) ∙∙ snd f
  snd (fromSusp→toΩ f) =
    cong (sym (snd f) ∙∙_∙∙ (snd f))
          (cong (cong (fst f))
           (rCancel (merid (pt A))))
       ∙ ∙∙lCancel (snd f)

  toΩ→fromSusp : A →∙ Ω B → Susp∙ (typ A) →∙ B
  fst (toΩ→fromSusp f) north = pt B
  fst (toΩ→fromSusp f) south = pt B
  fst (toΩ→fromSusp f) (merid a i) = fst f a i
  snd (toΩ→fromSusp f) = refl

  ΩSuspAdjointIso : Iso (A →∙ Ω B) (Susp∙ (typ A) →∙ B)
  fun ΩSuspAdjointIso = toΩ→fromSusp
  inv ΩSuspAdjointIso = fromSusp→toΩ
  rightInv ΩSuspAdjointIso f =
    ΣPathP (funExt
      (λ { north → sym (snd f)
         ; south → sym (snd f) ∙ cong (fst f) (merid (pt A))
         ; (merid a i) j →
           hcomp (λ k → λ { (i = i0) → snd f (~ j ∧ k)
                           ; (i = i1) → compPath-filler'
                                          (sym (snd f))
                                          (cong (fst f) (merid (pt A))) k j
                           ; (j = i1) → fst f (merid a i)})
                 (fst f (compPath-filler (merid a) (sym (merid (pt A))) (~ j) i))})
         , λ i j → snd f (~ i ∨ j))
  leftInv ΩSuspAdjointIso f =
    →∙Homogeneous≡ (isHomogeneousPath _ _)
      (funExt λ x → sym (rUnit _)
             ∙ cong-∙ (fst (toΩ→fromSusp f)) (merid x) (sym (merid (pt A)))
             ∙ cong (fst f x ∙_) (cong sym (snd f))
             ∙ sym (rUnit _))

  IsoΩFunSuspFun : Iso (typ (Ω (A →∙ B ∙))) (Susp∙ (typ A) →∙ B)
  IsoΩFunSuspFun = compIso (ΩfunExtIso A B) ΩSuspAdjointIso

max_stars_repo_name: ecavallo/cubical

max_issues_repo_name: ecavallo/cubical

max_forks_repo_name: ecavallo/cubical


text:
------------------------------------------------------------------------------
-- Testing a non-admissible property from the HALO paper
------------------------------------------------------------------------------

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

module FOT.FOTC.UnguardedCorecursion.HALO where

-- open import Common.FOL.Relation.Binary.EqReasoning

-- open import FOTC.Base
-- open import FOTC.Base.List
-- open import FOTC.Base.List.PropertiesI
-- open import FOTC.Data.Conat
-- open import FOTC.Data.Conat.PropertiesI
-- open import FOTC.Data.Nat
-- open import FOTC.Data.Stream.Type
-- open import FOTC.Data.Stream.Equality.PropertiesI
-- open import FOTC.Relation.Binary.Bisimilarity.PropertiesI
-- open import FOTC.Relation.Binary.Bisimilarity.Type

-- ------------------------------------------------------------------------------
-- -- The HALO paper states the property
-- --
-- -- ∀ x . f x ≠ ones (1)
-- --
-- -- cannot be proved because it is a non-admissible one.

-- postulate
--   ones    : D
--   ones-eq : ones ≡ succ₁ zero ∷ ones

-- postulate
--   f     : D → D
--   f-eq₁ : ∀ n → f (succ₁ n) ≡ succ₁ zero ∷ f n
--   f-eq₂ : f zero ≡ zero ∷ []

-- ------------------------------------------------------------------------------
-- -- Auxiliary properties

-- fCong : ∀ {m n} → m ≡ n → f m ≡ f n
-- fCong refl = refl

-- succ-∞-Conat : Conat (succ₁ ∞)
-- succ-∞-Conat = subst Conat ∞-eq ∞-Conat

-- ones-Stream : Stream ones
-- ones-Stream = Stream-coind A h refl
--   where
--   A : D → Set
--   A xs = xs ≡ xs

--   h : A ones → ∃[ x' ] ∃[ xs' ] ones ≡ x' ∷ xs' ∧ A xs'
--   h _ = succ₁ zero , ones , ones-eq , refl

-- f-∞-Stream : Stream (f ∞)
-- f-∞-Stream = Stream-coind A h refl
--   where
--   A : D → Set
--   A xs = f xs ≡ f xs

--   h : A (f ∞) → ∃[ x' ] ∃[ xs' ] f ∞ ≡ x' ∷ xs' ∧ A xs'
--   h Af∞ = succ₁ zero , f ∞ , trans (fCong ∞-eq) (f-eq₁ ∞) , Af∞

-- ------------------------------------------------------------------------------
-- -- A proof of (1) adding the N totality hypothesis.

-- thm₁ : ∀ {n} → N n → f n ≢ ones
-- thm₁ nzero h = 0≢S (∧-proj₁ (∷-injective helper))
--   where
--   helper : zero ∷ [] ≡ succ₁ zero ∷ ones
--   helper = trans₂ (sym f-eq₂) h ones-eq

-- thm₁ (nsucc {n} Nn) h = thm₁ Nn (∧-proj₂ (∷-injective helper))
--   where
--   helper : succ₁ zero ∷ f n ≡ succ₁ zero ∷ ones
--   helper = trans₂ (sym (f-eq₁ n)) h ones-eq

-- ------------------------------------------------------------------------------
-- -- A proof of (1) adding the N totality hypothesis and replacing the
-- -- propositional equality by the bisimilarity relation.

-- thm₂ : ∀ {n} → N n → f n ≉ ones
-- thm₂ nzero h with ≈-out h
-- ... | x' , xs' , ys' , prf₁ , prf₂ , prf₃ = 0≢S (trans (sym x'≡0) x'≡1)
--   where
--   x'≡0 : x' ≡ zero
--   x'≡0 = ∧-proj₁ (∷-injective (trans (sym prf₁) f-eq₂))

--   x'≡1 : x' ≡ succ₁ zero
--   x'≡1 = ∧-proj₁ (∷-injective (trans (sym prf₂) ones-eq))

-- thm₂ (nsucc {n} Nn) h with ≈-out h
-- ... | x' , xs' , ys' , prf₁ , prf₂ , prf₃ = thm₂ Nn (∷-injective≈ helper)
--   where
--   xs'≡fn : xs' ≡ f n
--   xs'≡fn = ∧-proj₂ (∷-injective (trans (sym prf₁) (f-eq₁ n)))

--   ys'≡ones : ys' ≡ ones
--   ys'≡ones = ∧-proj₂ (∷-injective (trans (sym prf₂) ones-eq))

--   helper : x' ∷ f n ≈ x' ∷ ones
--   helper = ≈-in ( x'
--                 , xs'
--                 , ys'
--                 , ∷-rightCong (sym xs'≡fn)
--                 , ∷-rightCong (sym ys'≡ones)
--                 , prf₃
--                 )

-- ------------------------------------------------------------------------------
-- -- A proof of the negation of (1) adding the Conat totality hypothesis
-- -- and replacing the propositional equality by the bisimilarity
-- -- relation.

-- thm₃ : ∃[ n ] (Conat n ∧ f n ≈ ones)
-- thm₃ =  ∞ , ∞-Conat , ≈-coind B h (refl , refl)
--   where
--   B : D → D → Set
--   B xs ys = xs ≡ xs ∧ ys ≡ ys

--   h : B (f ∞) ones →
--       ∃[ x' ] ∃[ xs' ] ∃[ ys' ] f ∞ ≡ x' ∷ xs' ∧ ones ≡ x' ∷ ys' ∧ B xs' ys'
--   h Bh' = succ₁ zero , f ∞ , ones , trans (fCong ∞-eq) (f-eq₁ ∞) , ones-eq , Bh'

------------------------------------------------------------------------------
-- References
--
-- Vytiniotis, D., Peyton Jones, S., Rosén, D. and Claessen,
-- K. (2013). HALO: Haskell to Logic thorugh Denotational
-- Semantics. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT
-- symposium on Principles of programming languages (POPL’13),
-- pp. 431–442.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2011-09-13, shrunk from Data.Colist
-- {-# OPTIONS -v tc.lhs.unify:15 #-}

{-# OPTIONS --universe-polymorphism #-}

module TransColist where

open import Common.Level
open import Common.Coinduction

-- From Relation.Binary.Core:
------------------------------------------------------------------------
-- Binary relations

-- Heterogeneous binary relations

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ lsuc ℓ)
REL A B ℓ = A → B → Set ℓ

-- Homogeneous binary relations

Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Rel A ℓ = REL A A ℓ

-- Generalised transitivity.

Trans : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c} →
        REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

Transitive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
Transitive _∼_ = Trans _∼_ _∼_ _∼_

infixr 5 _∷_

data Colist {a} (A : Set a) : Set a where
  []  : Colist A
  _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A

infix 4 _≈_

data _≈_ {a} {A : Set a} : (xs ys : Colist A) → Set a where
  []  :                                       []     ≈ []
  _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys

postulate
  a : Level
  A : Set a
{- succeeds:
trans : -- forall {a}{A : Set a}
        forall {xs ys zs : Colist A} →
  xs ≈ ys → ys ≈ zs →  xs ≈ zs
-}

-- succeeds:
-- trans : forall {a}{A : Set a}{xs ys zs : Colist A} → xs ≈ ys → ys ≈ zs →  xs ≈ zs

trans : Transitive (_≈_ {A = A})
trans []        []         = []
trans (x ∷ xs≈) (.x ∷ ys≈) = x ∷ ♯ trans (♭ xs≈) (♭ ys≈)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
import Parametric.Syntax.Type as Type

module Parametric.Syntax.MType where

module Structure (Base : Type.Structure) where
  open Type.Structure Base

  mutual
    --  Derived from CBPV
    data ValType : Set where
      U : (c : CompType) → ValType
      B : (ι : Base) → ValType
      vUnit : ValType
      _v×_ : (τ₁ : ValType) → (τ₂ : ValType) → ValType
      _v+_ : (τ₁ : ValType) → (τ₂ : ValType) → ValType

    -- Same associativity as the standard _×_
    infixr 2 _v×_

    data CompType : Set where
      F : ValType → CompType
      _⇛_ : ValType → CompType → CompType
      -- We did not use this in CBPV, so dropped.
      -- _Π_ : CompType → CompType → CompType

  cbnToCompType : Type → CompType
  cbnToCompType (base ι) = F (B ι)
  cbnToCompType (σ ⇒ τ) = U (cbnToCompType σ) ⇛ cbnToCompType τ

  cbvToValType : Type → ValType
  cbvToValType (base ι) = B ι
  cbvToValType (σ ⇒ τ) = U (cbvToValType σ ⇛ F (cbvToValType τ))

  open import Base.Syntax.Context ValType public
    using ()
    renaming
      ( ∅ to ∅∅
      ; _•_ to _••_
      ; mapContext to mapValCtx
      ; Var to ValVar
      ; Context to ValContext
      ; this to vThis; that to vThat
      ; _≼_ to _≼≼_
      ; weaken-var to weaken-val-var
      ; keep_•_ to keep_••_
      ; drop_•_ to drop_••_
      ; ≼-refl to ≼≼-refl
      ; ≼-trans to ≼≼-trans)

  cbnToValType : Type → ValType
  cbnToValType τ = U (cbnToCompType τ)

  cbvToCompType : Type → CompType
  cbvToCompType τ = F (cbvToValType τ)

  fromCBNCtx : Context → ValContext
  fromCBNCtx Γ = mapValCtx cbnToValType Γ

  fromCBVCtx : Context → ValContext
  fromCBVCtx Γ = mapValCtx cbvToValType Γ

  open import Data.List
  open Data.List using (List) public
  fromCBVToCompList : Context → List CompType
  fromCBVToCompList Γ = mapValCtx cbvToCompType Γ

  fromVar : ∀ {Γ τ} → (f : Type → ValType) → Var Γ τ → ValVar (mapValCtx f Γ) (f τ)
  fromVar {x • Γ} f this = vThis
  fromVar {x • Γ} f (that v) = vThat (fromVar f v)

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

open import OscarPrelude

mutual

  data Delay (i : Size) (A : Set) : Set where
    now    :  A           → Delay i A
    later  :  ∞Delay i A  → Delay i A

  record ∞Delay (i : Size) (A : Set) : Set where
    coinductive
    field
      force : {j : Size< i} → Delay j A

open ∞Delay public

private
  module BindDelay
   where

    mutual

      bindDelay          :  ∀ {i A B} → Delay i A → (A → Delay i B) → Delay i B
      bindDelay (now    a) f   =  f a
      bindDelay (later ∞a) f   =  later (bind∞Delay ∞a f)

      bind∞Delay             :  ∀ {i A B} → ∞Delay i A → (A → Delay i B) → ∞Delay i B
      force (bind∞Delay ∞a f)  =  bindDelay (force ∞a) f

module _
 where

  open BindDelay

  open BindDelay public using () renaming (bind∞Delay to _∞>>=_)

  instance FunctorDelay : {i : Size} → Functor (Delay i)
  Functor.fmap FunctorDelay f x = bindDelay x $ now ∘ f

  instance ApplicativeDelay : {i : Size} → Applicative (Delay i)
  Applicative.pure ApplicativeDelay x = now x
  Applicative._<*>_ ApplicativeDelay (now f) x = f <$> x
  Applicative._<*>_ ApplicativeDelay (later ∞f) x = later ∘ bind∞Delay ∞f $ flip fmap x
  Applicative.super ApplicativeDelay = FunctorDelay

  instance MonadDelay : {i : Size} → Monad (Delay i)
  Monad._>>=_ MonadDelay = bindDelay
  Monad.super MonadDelay = ApplicativeDelay

  {-# DISPLAY BindDelay.bindDelay x f = x >>= f #-}

mutual

  data _∼_ {i : Size} {A : Set} : (a? b? : Delay ∞ A) → Set where
    ∼now    :  ∀ a                              →  now a     ∼ now a
    ∼later  :  ∀ {a∞ b∞} (eq : a∞ ∞∼⟨ i ⟩∼ b∞)  →  later a∞  ∼ later b∞

  _∼⟨_⟩∼_ = λ {A} a? i b? → _∼_ {i}{A} a? b?

  record _∞∼⟨_⟩∼_ {A} (a∞ : ∞Delay ∞ A) i (b∞ : ∞Delay ∞ A) : Set where
    coinductive
    field
      ∼force : {j : Size< i} → force a∞ ∼⟨ j ⟩∼ force b∞

open _∞∼⟨_⟩∼_ public

_∞∼_ = λ {i} {A} a∞ b∞ → _∞∼⟨_⟩∼_ {A} a∞ i b∞

mutual

  ∼refl    :  ∀{i A} (a?  : Delay ∞ A)   →  a? ∼⟨ i ⟩∼ a?
  ∼refl (now a)    = ∼now a
  ∼refl (later a∞) = ∼later (∞∼refl a∞)

  ∞∼refl   :  ∀{i A} (a∞  : ∞Delay ∞ A)  →  a∞ ∞∼⟨ i ⟩∼ a∞
  ∼force (∞∼refl a∞) = ∼refl (force a∞)

mutual

  ∼sym     :  ∀{i A}{a?  b?  : Delay ∞ A }  →  a? ∼⟨ i ⟩∼ b?   →  b? ∼⟨ i ⟩∼ a?
  ∼sym (∼now a)    = ∼now a
  ∼sym (∼later eq) = ∼later (∞∼sym eq)

  ∞∼sym    :  ∀{i A}{a∞  b∞  : ∞Delay ∞ A}  →  a∞ ∞∼⟨ i ⟩∼ b∞  →  b∞ ∞∼⟨ i ⟩∼ a∞
  ∼force (∞∼sym eq) = ∼sym (∼force eq)

mutual

  ∼trans   :  ∀{i A}{a? b? c? : Delay ∞ A} →
              a? ∼⟨ i ⟩∼ b? →  b? ∼⟨ i ⟩∼ c? → a? ∼⟨ i ⟩∼ c?
  ∼trans (∼now a)    (∼now .a)    = ∼now a
  ∼trans (∼later eq) (∼later eq′) = ∼later (∞∼trans eq eq′)

  ∞∼trans  :  ∀{i A}{a∞ b∞ c∞ : ∞Delay ∞ A} →
              a∞ ∞∼⟨ i ⟩∼ b∞ →  b∞ ∞∼⟨ i ⟩∼ c∞ → a∞ ∞∼⟨ i ⟩∼ c∞
  ∼force (∞∼trans eq eq′) = ∼trans (∼force eq) (∼force eq′)

--∼setoid : (i : Size) (A : Set) → Setoid lzero lzero
--∞∼setoid : (i : Size) (A : Set) → Setoid lzero lzero

mutual

  bind-assoc               :  ∀{i A B C} (m : Delay ∞ A)
                              {k : A → Delay ∞ B} {l : B → Delay ∞ C} →
                              ((m >>= k) >>= l) ∼⟨ i ⟩∼ (m >>= λ a → (k a >>= l))
  bind-assoc (now a)       =  ∼refl _
  bind-assoc (later a∞)    =  ∼later (∞bind-assoc a∞)

  ∞bind-assoc              :  ∀{i A B C} (a∞ : ∞Delay ∞ A)
                              {k : A → Delay ∞ B} {l : B → Delay ∞ C} →
                              ((a∞ ∞>>= k) ∞>>= l) ∞∼⟨ i ⟩∼ (a∞ ∞>>= λ a → (k a >>= l))
  ∼force (∞bind-assoc a∞)  =  bind-assoc (force a∞)

mutual

  bind-cong-l   :  ∀{i A B}{a? b? : Delay ∞ A} →  a? ∼⟨ i ⟩∼ b? →
                   (k : A → Delay ∞ B) → (a? >>= k) ∼⟨ i ⟩∼ (b? >>= k)
  bind-cong-l (∼now a)    k = ∼refl _
  bind-cong-l (∼later eq) k = ∼later (∞bind-cong-l eq k)

  ∞bind-cong-l  :  ∀{i A B}{a∞ b∞ : ∞Delay ∞ A} → a∞ ∞∼⟨ i ⟩∼ b∞ →
                   (k : A → Delay ∞ B) → (a∞ ∞>>= k) ∞∼⟨ i ⟩∼ (b∞ ∞>>= k)
  ∼force (∞bind-cong-l eq k) = bind-cong-l (∼force eq) k

mutual
  bind-cong-r   :  ∀{i A B}(a? : Delay ∞ A){k l : A → Delay ∞ B} →
                   (∀ a → (k a) ∼⟨ i ⟩∼ (l a)) → (a? >>= k) ∼⟨ i ⟩∼ (a? >>= l)
  bind-cong-r (now a)    h = h a
  bind-cong-r (later a∞) h = ∼later (∞bind-cong-r a∞ h)

  ∞bind-cong-r  :  ∀{i A B}(a∞ : ∞Delay ∞ A){k l : A → Delay ∞ B} →
                   (∀ a → (k a) ∼⟨ i ⟩∼ (l a)) → (a∞ ∞>>= k) ∞∼⟨ i ⟩∼ (a∞ ∞>>= l)
  ∼force (∞bind-cong-r a∞ h) = bind-cong-r (force a∞) h

map-compose     :  ∀{i A B C} (a? : Delay ∞ A) {f : A → B} {g : B → C} →
                   (g <$> (f <$> a?)) ∼⟨ i ⟩∼ ((g ∘ f) <$> a?)
map-compose a?  =  bind-assoc a?

map-cong        :  ∀{i A B}{a? b? : Delay ∞ A} (f : A → B) →
                   a? ∼⟨ i ⟩∼ b? → (f <$> a?) ∼⟨ i ⟩∼ (f <$> b?)
map-cong f eq   =  bind-cong-l eq (now ∘ f)

data _⇓_ {A : Set} : (a? : Delay ∞ A) (a : A) → Set where
  now⇓    :  ∀{a}                                   → now a ⇓ a
  later⇓  :  ∀{a} {a∞ : ∞Delay ∞ A} → force a∞ ⇓ a  → later a∞ ⇓ a

_⇓   :  {A : Set} (x : Delay ∞ A) → Set
x ⇓  =  ∃ λ a → x ⇓ a

map⇓     :  ∀{A B}{a : A}{a? : Delay ∞ A}(f : A → B) → a? ⇓ a → (f <$> a?) ⇓ f a
map⇓ f now⇓        = now⇓
map⇓ f (later⇓ a⇓) = later⇓ (map⇓ f a⇓)

bind⇓    :  ∀{A B}(f : A → Delay ∞ B){?a : Delay ∞ A}{a : A}{b : B} →
            ?a ⇓ a → f a ⇓ b → (?a >>= f) ⇓ b
bind⇓ f now⇓ q = q
bind⇓ f (later⇓ p) q = later⇓ (bind⇓ f p q)

infixl 4 _>>=⇓_
_>>=⇓_    :  ∀{A B}{f : A → Delay ∞ B}{?a : Delay ∞ A}{a : A}{b : B} →
             ?a ⇓ a → f a ⇓ b → (?a >>= f) ⇓ b
_>>=⇓_ = bind⇓ _

infixl 4 _⇓>>=⇓_
_⇓>>=⇓_    :  ∀{A B}{f : A → Delay ∞ B}{?a : Delay ∞ A}{b : B} →
              (?a⇓ : ?a ⇓) → f (fst ?a⇓) ⇓ b → (?a >>= f) ⇓ b
_⇓>>=⇓_ (_ , a⇓) = bind⇓ _ a⇓

_⇓Dec>>=⇓_else⇓_ : ∀{A B}{f-yes : A → Delay ∞ B}{f-no : ¬ A → Delay ∞ B}{?a : Delay ∞ (Dec A)}{b : B} →
            (?a⇓ : ?a ⇓) →
            ((a : A) → f-yes a ⇓ b) →
            ((¬a : ¬ A) → f-no ¬a ⇓ b) →
            ((?a >>= (λ { (yes y) → f-yes y ; (no n) → f-no n }))) ⇓ b
(yes y , y⇓) ⇓Dec>>=⇓ fy⇓ else⇓ fn⇓ = y⇓ >>=⇓ fy⇓ y
(no n , n⇓) ⇓Dec>>=⇓ fy⇓ else⇓ fn⇓ = n⇓ >>=⇓ fn⇓ n

_⇓DecEq>>=⇓_else⇓_ : ∀{A : Set} {A₁ A₂ : A} {B}{f-yes : A₁ ≡ A₂ → Delay ∞ B}{f-no : A₁ ≢ A₂ → Delay ∞ B}{?a : Delay ∞ (Dec (A₁ ≡ A₂))}{b : B} →
            (?a⇓ : ?a ⇓) →
            ((eq : A₁ ≡ A₂) → f-yes eq ⇓ b) →
            ((¬eq : A₁ ≢ A₂) → f-no ¬eq ⇓ b) →
            ((?a >>= (λ { (yes refl) → f-yes refl ; (no n) → f-no n }))) ⇓ b
(yes refl , y⇓) ⇓DecEq>>=⇓ fy⇓ else⇓ fn⇓ = y⇓ >>=⇓ fy⇓ refl
(no n , n⇓) ⇓DecEq>>=⇓ fy⇓ else⇓ fn⇓ = n⇓ >>=⇓ fn⇓ n

app⇓ : ∀{A}{B}{f? : Delay ∞ (A → B)}{f : A → B}{x? : Delay ∞ A}{x : A} → f? ⇓ f → x? ⇓ x → (f? <*> x?) ⇓ f x
app⇓ now⇓ now⇓ = now⇓
app⇓ now⇓ (later⇓ x?) = later⇓ $ map⇓ _ x?
app⇓ (later⇓ f?) now⇓ = later⇓ $ bind⇓ _ f? now⇓
app⇓ (later⇓ ⇓f) (later⇓ ⇓x) = later⇓ $ bind⇓ _ ⇓f $ later⇓ $ bind⇓ _ ⇓x now⇓

subst∼⇓  :  ∀{A}{a? a?′ : Delay ∞ A}{a : A} → a? ⇓ a → a? ∼ a?′ → a?′ ⇓ a
subst∼⇓ now⇓ (∼now a) = now⇓
subst∼⇓ (later⇓ p) (∼later eq) = later⇓ (subst∼⇓ p (∼force eq))

traverse-list⇓ : ∀{A}{B} (f? : A → Delay ∞ B) → (∀ x → f? x ⇓) → (xs : List A) → traverse f? xs ⇓
traverse-list⇓ f? f?⇓ [] = [] , now⇓
traverse-list⇓ f? f?⇓ (x ∷ xs)
 with f?⇓ x | traverse-list⇓ f? f?⇓ xs
… | y , y⇓ | ys , ys⇓ = y ∷ ys , app⇓ (map⇓ _ y⇓) ys⇓


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

{- This module serves to develop some basic theory about pointed types.
   After defining the usual notions of pointed types, pointed equivalences,
   and loop spaces, we derive a version of univalence for pointed equivalences
   and observe that univalence between identical types is a pointed equivalence.

   We define pointed versions of dependent sums and products using the usual
   notion of pointed families and observe that they commute in a certain sense
   with taking loop spaces.

   We finish by deriving a generalization to n-truncation and n-th loop spaces
   of the fact allowing us to 'forget' contractible components in a dependent
   sum type that will be needed in the Hierarchy module. -}
module Universe.Utility.Pointed where

open import lib.Basics
open import lib.NType2
open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.TLevel

open import Universe.Utility.General
open import Universe.Utility.TruncUniverse

{- Pointed types.
   A pointed type is a type (base) together with a chosen element (pt).
   The loop space construction Ω takes a pointed type and returns the type
   of all loops at the given basepoint. The trivial loop is taken as
   canonical element, thus forming a new pointed type. -}
Type• : (i : ULevel) → Type (lsucc i)
Type• i = Σ (Type i) (idf _)

module _ {i} (X : Type• i) where
  base = fst X
  pt   = snd X

-- Alternate definition: Σ (n -Type i) ⟦_⟧
_-Type•_ : (n : ℕ₋₂) (i : ULevel) → Type (lsucc i)
n -Type• i = Σ (Type• i) (has-level n ∘ base)

-- For alternate definition: Σ-≤ (n -Type-≤ i) raise
_-Type•-≤_ : (n : ℕ₋₂) (i : ULevel) → S n -Type lsucc i
n -Type•-≤ i = (n -Type• i
              , equiv-preserves-level Σ-comm-snd
                                      (snd (Σ-≤ (n -Type-≤ i) raise)))

{- Pointed equivalences.
   An equivalence of pointed types is an equivalences of the bases
   that preserves the points -}
_≃•_ : ∀ {i j} → Type• i → Type• j → Set (i ⊔ j)
A ≃• B = Σ (base A ≃ base B) (λ f → –> f (pt A) == pt B)

ide• : ∀ {i} (X : Type• i) → X ≃• X
ide• _ = ide _ , idp

_∘e•_ : ∀ {i j k} {X : Type• i} {Y : Type• j} {Z : Type• k}
       → Y ≃• Z → X ≃• Y → X ≃• Z
(u , p) ∘e• (v , q) = (u ∘e v , ap (–> u) q ∙ p)

_⁻¹• : ∀ {i j} {X : Type• i} {Y : Type• j} → X ≃• Y → Y ≃• X
(u , p) ⁻¹• = (u ⁻¹ , ap (<– u) (! p) ∙ <–-inv-l u _)

-- Equational reasoning for pointed equivalences.
infix  2 _≃•∎
infixr 2 _≃•⟨_⟩_

_≃•⟨_⟩_ : ∀ {i j k} (X : Type• i) {Y : Type• j} {Z : Type• k}
          → X ≃• Y → Y ≃• Z → X ≃• Z
_ ≃•⟨ u ⟩ v = v ∘e• u

_≃•∎ : ∀ {i} (X : Type• i) → X ≃• X
_≃•∎ = ide•

-- The loop space construction.
Ω : ∀ {i} → Type• i → Type• i
Ω (A , a) = (a == a , idp)

Ω-≤ : ∀ {i} {n : ℕ₋₂} → (S n) -Type• i → n -Type• i
Ω-≤ ((A , a) , t) = (Ω (A , a) , t a a)

-- Loop spaces are preserved by pointed equivalences.
equiv-Ω : ∀ {i j} {X : Type• i} {Y : Type• j} → X ≃• Y → Ω X ≃• Ω Y
equiv-Ω (u , p) = split u p where
  split : ∀ u {a} {b} → –> u a == b → Ω (_ , a) ≃• Ω (_ , b)
  split u idp = (equiv-ap u _ _ , idp)

equiv-Ω^ : ∀ {i j} {X : Type• i} {Y : Type• j} (n : ℕ)
           → X ≃• Y → (Ω ^ n) X ≃• (Ω ^ n) Y
equiv-Ω^ 0     e = e
equiv-Ω^ (S n) e = equiv-Ω^ n (equiv-Ω e)

{- We call a pointed type n-truncated if its base is.
   Constructing the loop space decrements the truncation level. -}
has-level• : ∀ {i} → ℕ₋₂ → Type• i → Type i
has-level• n = has-level n ∘ base

trunc-many : ∀ {i} {X : Type• i} {k : ℕ} (n : ℕ)
             → has-level• (k + n -2)          X
             → has-level• (k     -2) ((Ω ^ n) X)
trunc-many 0     t = t
trunc-many (S n) t = trunc-many n (t _ _)

--Ω^-≤ : ∀ {i} {k : ℕ} (n : ℕ) → (k + n -2) -Type• i → (k -2) -Type• i
--Ω^-≤ O     X = X
--Ω^-≤ (S n) X = Ω^-≤ n (Ω-≤ X)

Ω^-≤ : ∀ {i} {k : ℕ} (n : ℕ) → (k + n -2) -Type• i → (k -2) -Type• i
Ω^-≤ n (X , t) = ((Ω ^ n) X , trunc-many n t)

Ω^-≤' : ∀ {i} {k : ℕ} (n : ℕ) → (n + k -2) -Type• i → (k -2) -Type• i
Ω^-≤' n (X , t) =
  ((Ω ^ n) X , trunc-many n (transport (λ z → has-level• (z -2) X)
                                       (+-comm _ n) t))

{- Pointedness allows for a more direct notion of contractibility.
   Beware that is-contr• will be equivalent --- not definitionally equal ---
   to has-level∙ ⟨-2⟩. -}
module _ {i} (X : Type• i) where
  is-contr• : Type i
  is-contr• = ∀ a → pt X == a

{- Since pointed types are always inhabited,
   being contractible and propositional is equivalent. -}
module _ {i} {X : Type• i} where
  contr•-equiv-contr : is-contr• X ≃ is-contr (base X)
  contr•-equiv-contr = prop-equiv'
                         (λ c → Π-level (λ a → raise-level-<T (ltSR ltS) c _ _))
                         (cst is-contr-is-prop)
                         (λ x → (pt X , x))
                         (λ y _ → prop-has-all-paths (contr-is-prop y) _ _)

  is-contr•-is-prop : is-prop (is-contr• X)
  is-contr•-is-prop = equiv-preserves-level (contr•-equiv-contr ⁻¹)
                                            is-contr-is-prop

  prop-equiv-contr : is-prop (base X) ≃ is-contr (base X)
  prop-equiv-contr = prop-equiv is-prop-is-prop
                                is-contr-is-prop
                                (inhab-prop-is-contr (pt X))
                                contr-is-prop

  contr•-equiv-prop : is-contr• X ≃ is-prop (base X)
  contr•-equiv-prop = prop-equiv-contr ⁻¹ ∘e contr•-equiv-contr

-- ** Lemma 5.4 ***
{- The induction step for Lemma 7.2.9 in the HoTT Book is much
   more complicated than neccesarry. Associating iterated loop spaces in
   the reverse order, we can do away with the prerequisites 7.2.7 and 7.2.8
   as well as further auxiliary steps. -}
has-level-equiv-contr-loops : ∀ {i} {n : ℕ} {A : Type i}
                              →   has-level (n -1) A
                                ≃ ((a : A) → is-contr• ((Ω ^ n) (A , a)))
has-level-equiv-contr-loops {n = O} {A} =
    is-prop A                      ≃⟨ prop-equiv-inhab-to-contr ⟩
    (A → is-contr A)               ≃⟨ equiv-Π-r (λ _ → contr•-equiv-contr ⁻¹) ⟩
    ((a : A) → is-contr• (A , a))  ≃∎
has-level-equiv-contr-loops {n = S n} {A} = equiv-Π-r lem where
  lem = λ a →
      (((b : A) → has-level ( n -1) (a == b)))
    ≃⟨ equiv-Π-r (λ _ → has-level-equiv-contr-loops) ⟩
      (((b : A) (p : a == b) → is-contr• ((Ω ^ n) (a == b , p))))
    ≃⟨ Π₁-contr (pathfrom-is-contr _) ∘e curry-equiv ⁻¹ ⟩
      is-contr• ((Ω ^ n) (a == a , idp))
    ≃∎

-- Pointed equivalences preserve (pointed) contractibility.
equiv-is-contr• : ∀ {i j} {X : Type• i} {Y : Type• j}
                → X ≃• Y → is-contr• X ≃ is-contr• Y
equiv-is-contr• (u , p) = contr•-equiv-contr ⁻¹
                       ∘e equiv-level u
                       ∘e contr•-equiv-contr

-- Univalence for pointed equivalences.
module _ {i} {A B : Type• i} where
  ua•-equiv : (A ≃• B) ≃ (A == B)
  ua•-equiv =
      A ≃• B
    ≃⟨ ide _ ⟩
      Σ (base A ≃ base B) (λ f → –> f (pt A) == pt B)
    ≃⟨ equiv-Σ-fst _ (snd (ua-equiv ⁻¹)) ⁻¹ ⟩
      Σ (base A == base B) (λ q → coe q (pt A) == pt B)
    ≃⟨ equiv-Σ-snd (λ q → coe-equiv (ap (λ f → coe f (pt A) == pt B)
                                        (! (ap-idf q)))) ⟩
      Σ (base A == base B) (λ q → coe (ap (idf _) q) (pt A) == pt B)
    ≃⟨ equiv-Σ-snd (λ q → to-transp-equiv _ q ⁻¹) ⟩
      Σ (base A == base B) (λ q → pt A == pt B [ idf _ ↓ q ])
    ≃⟨ =Σ-eqv _ _ ⟩
      A == B
    ≃∎

  ua• : A ≃• B → A == B
  ua• = –> ua•-equiv

  coe•-equiv : A == B → A ≃• B
  coe•-equiv = <– ua•-equiv

-- Normal univalence can be made pointed in the endo-setting.
module _ {i} {A : Type i} where
  ua-equiv• : (A ≃ A , ide _) ≃• (A == A , idp)
  ua-equiv• = ((ua-equiv ⁻¹) , idp) ⁻¹•

-- *** Definition 4.1 ***
{- Pointed families.
   A pointed family over a pointed type is a family over the base
   together with a inhabitant of the family at the point.
   Note that pointed types are equivalent to pointed families
   over the pointed unit type (not shown here). -}
Fam• : ∀ {i} (X : Type• i) (j : ULevel) → Type (i ⊔ lsucc j)
Fam• X j = Σ (base X → Type j) (λ P → P (pt X))

-- We have fibered notions of the loop space contruction and n-truncatedness.
module _ {i} {X : Type• i} {j} where
  -- *** Definition 4.3 ***
  {- Note that the definition of the family of path types differs slightly from
     that of the article, which would correspond to transport P p x == x.
     We use dependent paths since this follows the design of the HoTT
     community's Agda library. Clearly, both types are equivalent. -}
  Ω̃ : Fam• X j → Fam• (Ω X) j
  Ω̃ (P , x) = ((λ p → x == x [ P ↓ p ]) , idp)

  fam-has-level : ℕ₋₂ → Fam• X j → Type (i ⊔ j)
  fam-has-level n Q = (a : base X) → has-level n (fst Q a)

{- == Pointed dependent sums ==
   Pointed families as defined above enable us to introduce a Σ-connective
   for pointed types. Because of the abstract nature of some of our lemmata, we
   give Σ• in its uncurried form and first define the type of its parameter. -}
Σ•-param : ∀ i j → Type (lsucc (i ⊔ j))
Σ•-param i j = Σ (Type• i) (λ X → Fam• X j)

module _ {i j} where
  Ω-Σ•-param : Σ•-param i j → Σ•-param i j
  Ω-Σ•-param (X , W) = (Ω X , Ω̃ W)

  -- *** Definition 4.4 ***
  Σ• : Σ•-param i j → Type• (i ⊔ j)
  Σ• (X , Q) = (Σ (base X) (fst Q) , (pt X , snd Q))

  -- *** Lemma 4.5 ***
  {- Commutativity of pointed dependent sums and the loop space construction
     will become an important technical tool, enabling us to work at a more
     abstract level later on. -}
  Ω-Σ•-comm : (R : Σ•-param i j) → Ω (Σ• R) ≃• Σ• (Ω-Σ•-param R)
  Ω-Σ•-comm _ = (=Σ-eqv _ _ , idp) ⁻¹•

{- Pointed dependent products.
   This is not quite the equivalent of Π for pointed types: the domain parameter
   is just an ordinary non-pointed type. However, to enable our goal of
   abstractly working with pointed types, defining this notion is useful. -}
Π•-param : ∀ i j → Type (lsucc (i ⊔ j))
Π•-param i j = Σ (Type i) (λ A → A → Type• j)

module _ {i j} where
  Ω-Π•-param : Π•-param i j → Π•-param i j
  Ω-Π•-param (A , F) = (A , Ω ∘ F)

  -- *** Definition 4.6 ***
  Π• : Π•-param i j → Type• (i ⊔ j)
  Π• (A , Y) = (Π A (base ∘ Y) , pt ∘ Y)

  -- *** Lemma 4.7 ***
  {- Pointed dependent products and loop space construction on
     its codomain parameter commute as well. -}
  Ω-Π•-comm : (R : Π•-param i j) → Ω (Π• R) ≃• Π• (Ω-Π•-param R)
  Ω-Π•-comm _ = (app=-equiv , idp)

  Ω^-Π•-comm : (C : Type i) (F : C → Type• j) (n : ℕ)
             → (Ω ^ n) (Π• (C , F)) ≃• Π• (C , Ω ^ n ∘ F)
  Ω^-Π•-comm C F 0     = ide• _
  Ω^-Π•-comm C F (S n) = Ω^-Π•-comm C _ n ∘e• equiv-Ω^ n (Ω-Π•-comm _)

equiv-Π• : ∀ {i₀ i₁ j₀ j₁} {R₀ : Π•-param i₀ j₀} {R₁ : Π•-param i₁ j₁}
           → Σ (fst R₀ ≃ fst R₁) (λ u → ∀ a → snd R₀ (<– u a) ≃• snd R₁ a)
           → Π• R₀ ≃• Π• R₁
equiv-Π• (u , v) = (equiv-Π u (fst ∘ v) , λ= (snd ∘ v))

-- *** Lemma 5.1 ***
-- In an n-th loop space, we can forget components of truncation level n.
forget-Ω^-Σ•₂ : ∀ {i j} {X : Type• i} (Q : Fam• X j) (n : ℕ)
                → fam-has-level (n -2) Q → (Ω ^ n) (Σ• (X , Q)) ≃• (Ω ^ n) X
forget-Ω^-Σ•₂     {X = X} Q    O  h = (Σ₂-contr h , idp)
forget-Ω^-Σ•₂ {i} {X = X} Q (S n) h =
  (Ω ^ (S n)) (Σ• (X , Q))  ≃•⟨ equiv-Ω^ n (Ω-Σ•-comm _) ⟩
  (Ω ^ n) (Σ• (Ω X , Ω̃ Q))  ≃•⟨ forget-Ω^-Σ•₂ {i} _ n (λ _ → =-[-↓-]-level h) ⟩
  (Ω ^ (S n)) X             ≃•∎

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for Vec-based tables
------------------------------------------------------------------------

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

module Text.Tabular.Vec where

open import Data.List.Base using (List)
open import Data.Product as Prod using (uncurry)
open import Data.String.Base using (String; rectangle; fromAlignment)
open import Data.Vec.Base
open import Function.Base

open import Text.Tabular.Base

display : ∀ {m n} → TabularConfig → Vec Alignment n → Vec (Vec String n) m →
          List String
display c a = unsafeDisplay c
            ∘ toList
            ∘ map toList
            ∘ transpose
            ∘ map (uncurry rectangle ∘ unzip)
            ∘ transpose
            ∘ map (zip (map fromAlignment a))


text:
open import Agda.Builtin.Equality

postulate
  A : Set

mutual
  F : ((@♭ _ : A) -> A) → A → A
  F f = _

  testF : {f : A -> A} → F f ≡ f
  testF = refl

max_forks_repo_name: shlevy/agda


text:
-- Concrete definition of variables, context maps, and map operations
module SOAS.Variable {T : Set} where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Sorting
open import SOAS.Families.Core {T}

-- Sorted family of variables, as typed, scoped de Bruijn indices
data ℐ : Familyₛ where
  new : {α   : T}{Γ : Ctx}          → ℐ α (α ∙ Γ)
  old : {α β : T}{Γ : Ctx} → ℐ β Γ → ℐ β (α ∙ Γ)

-- Explicitly specify the extra variable type
oldₑ : (α {β} : T)(Γ : Ctx) → ℐ β Γ → ℐ β (α ∙ Γ)
oldₑ α Γ = old {α}{_}{Γ}

open import Relation.Nullary

decEqℐ : ∀ {a b} (x y : ℐ a b) → Dec (x ≡ y)
decEqℐ new new = yes refl
decEqℐ new (old y) = no (λ ())
decEqℐ (old x) new = no (λ ())
decEqℐ (old x) (old y) with decEqℐ x y
... | yes refl = yes refl
... | no npf = no (λ { refl → npf refl })

-- | Context-family maps
-- Generalised transformations between 𝒳-terms in one context and 𝒴-terms in
-- another context. The special case of 𝒳 being the family of variables
-- gives the usual notion of an environment (Allais et al.) or "type preserving
-- map from variables over Γ to stuff over Δ" (McBride 2005), where "stuff" is a
-- sorted family.

-- Context-family map between two sorted families in different contexts.
-- The type is implicitly quantified over.
_~[_➔_]↝_ : Ctx → Familyₛ → Familyₛ → Ctx → Set
Γ ~[ 𝒳 ➔ 𝒴 ]↝ Δ = {τ : T} → 𝒳 τ Γ → 𝒴 τ Δ

-- 𝒳-valued context map, associating variables in context Γ with 𝒳-terms
-- in context Δ.
_~[_]↝_ : Ctx → Familyₛ → Ctx → Set
Γ ~[ 𝒳 ]↝ Δ = Γ ~[ ℐ ➔ 𝒳 ]↝ Δ
infix 10 _~[_]↝_

-- Renaming map, mapping variables to variables
_↝_ : Ctx → Ctx → Set
Γ ↝ Δ = Γ ~[ ℐ ]↝ Δ
infix 4 _↝_

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import Calf.CostMonoid

-- Upper bound on the cost of a computation.

module Calf.Types.Bounded (costMonoid : CostMonoid) where

open CostMonoid costMonoid

open import Calf.Prelude
open import Calf.Metalanguage
open import Calf.PhaseDistinction
open import Calf.Types.Eq
open import Calf.Step costMonoid

open import Calf.Types.Bool
open import Calf.Types.Sum

open import Relation.Binary.PropositionalEquality as Eq

record IsBounded (A : tp pos) (e : cmp (F A)) (c : cmp cost) : □ where
  constructor ⇓_withCost_[_,_]
  field
    result : val A
    c' : ℂ
    h-bounded : ◯ (c' ≤ c)
    h-≡ : cmp (F (eq (U (F A)) e (step (F A) c' (ret result))))

IsBounded⁻ : (A : tp pos) → cmp (F A) → cmp cost → tp neg
IsBounded⁻ A e p = meta (IsBounded A e p)

bound/relax : ∀ {A e p p'} → ◯ (p ≤ p') → IsBounded A e p → IsBounded A e p'
bound/relax h (⇓ result withCost c' [ h-bounded , h-≡ ]) = ⇓ result withCost c' [ (λ u → ≤-trans (h-bounded u) (h u)) , h-≡ ]

bound/circ : ∀ {A e} d {c} →
  IsBounded A e c →
  IsBounded A e (step (meta ℂ) d c)
bound/circ d {c} (⇓ a withCost c' [ h-bounded , h-≡ ]) =
  ⇓ a withCost c' [ (λ u → subst (c' ≤_) (sym (step/ext cost c d u)) (h-bounded u)) , h-≡ ]

bound/ret : {A : tp pos} {a : val A} → IsBounded A (ret {A} a) zero
bound/ret {a = a} = ⇓ a withCost zero [ (λ u → ≤-refl) , ret (eq/intro refl) ]

bound/step : ∀ {A e} (d c : ℂ) →
  IsBounded A e c →
  IsBounded A (step (F A) d e) (d + c)
bound/step d c (⇓ a withCost c' [ h-bounded , h-≡ ]) with eq/ref h-≡
... | refl = ⇓ a withCost d + c' [ (λ u → +-monoʳ-≤ d (h-bounded u)) , ret (eq/intro refl) ]

bound/bind : ∀ {A B : tp pos} {e : cmp (F A)} {f : val A → cmp (F B)}
  (c : ℂ) (d : val A → ℂ) →
  IsBounded A e c →
  ((a : val A) → IsBounded B (f a) (d a)) →
  IsBounded B (bind {A} (F B) e f)
              (bind {A} cost e (λ a → c + d a))
bound/bind {f = f} c d (⇓ a withCost c' [ h-bounded₁ , h-≡₁ ]) h with eq/ref h-≡₁
... | refl with h a
... | ⇓ b withCost d' [ h-bounded₂ , h-≡₂ ] with f a | eq/ref h-≡₂
... | _ | refl = bound/circ c' (⇓ b withCost c' + d' [ (λ u → +-mono-≤ (h-bounded₁ u) (h-bounded₂ u)) , ret (eq/intro refl) ])

bound/bind/const : ∀ {A B : tp pos} {e : cmp (F A)} {f : val A → cmp (F B)}
  (c d : ℂ) →
  IsBounded A e c →
  ((a : val A) → IsBounded B (f a) d) →
  IsBounded B (bind {A} (F B) e f) (c + d)
bound/bind/const c d (⇓ a withCost c' [ h-bounded , h-≡ ]) h with eq/ref h-≡
... | refl = bound/circ' c' (bound/bind c (λ _ → d) (⇓ a withCost c' [ h-bounded , h-≡ ]) h)
  where
    bound/circ' : ∀ {A e} d {c} →
      IsBounded A e (step (meta ℂ) d c) →
      IsBounded A e c
    bound/circ' d {c} (⇓ a withCost c' [ h-bounded , h-≡ ]) =
      ⇓ a withCost c' [ (λ u → subst (c' ≤_) (step/ext cost c d u) (h-bounded u)) , h-≡ ]

bound/bool : ∀ {A : tp pos} {e0 e1} {p : val bool → cmp cost} →
  (b : val bool) →
  IsBounded A e0 (p false) →
  IsBounded A e1 (p true ) →
  IsBounded A (if b then e1 else e0) (p b)
bound/bool false h0 h1 = h0
bound/bool true  h0 h1 = h1

bound/sum/case/const/const : ∀ A B (C : val (sum A B) → tp pos) →
  (s : val (sum A B)) →
  (e0 : (a : val A) → cmp (F (C (inj₁ a)))) →
  (e1 : (b : val B) → cmp (F (C (inj₂ b)))) →
  (p : ℂ) →
  ((a : val A) → IsBounded (C (inj₁ a)) (e0 a) p) →
  ((b : val B) → IsBounded (C (inj₂ b)) (e1 b) p) →
  IsBounded (C s) (sum/case A B (λ s → F (C s)) s e0 e1) p
bound/sum/case/const/const A B C s e0 e1 p h1 h2 = sum/case A B
  (λ s → meta (IsBounded (C s) (sum/case A B (λ s₁ → F (C s₁)) s e0 e1) p)) s h1 h2

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Allto where

f : Set → Set
f = {!!}

g : Set → Set
g x = f {!!}


text:
module FFI.Data.Maybe where

{-# FOREIGN GHC import qualified Data.Maybe #-}

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A
{-# COMPILE GHC Maybe = data Data.Maybe.Maybe (Data.Maybe.Nothing|Data.Maybe.Just) #-}

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
-- Andreas, 2017-07-28, issue #1077
-- Agda's reconstruction of the top-level module can be confusing
-- in case the user puts some illegal declarations before the
-- top level module in error.

foo = Set

module Issue1077 where

  bar = Set

-- WAS: accepted, creating modules Issue1077 and Issue1077.Issue1077
-- with Issue1077.foo and Issue1077.Issue1077.bar

-- NOW: Error
-- Illegal declarations before top-level module


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Matrix where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Functions.FunExtEquiv

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat hiding (_+_ ; _·_; +-comm ; +-assoc; ·-assoc)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.BigOps

open Iso

private
  variable
    ℓ : Level
    A : Type ℓ

-- Equivalence between Vec matrix and Fin function matrix

FinMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
FinMatrix A m n = FinVec (FinVec A n) m

VecMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
VecMatrix A m n = Vec (Vec A n) m

FinMatrix→VecMatrix : {m n : ℕ} → FinMatrix A m n → VecMatrix A m n
FinMatrix→VecMatrix M = FinVec→Vec (λ fm → FinVec→Vec (M fm))

VecMatrix→FinMatrix : {m n : ℕ} → VecMatrix A m n → FinMatrix A m n
VecMatrix→FinMatrix M fn fm = lookup fm (lookup fn M)

FinMatrix→VecMatrix→FinMatrix : {m n : ℕ} (M : FinMatrix A m n)
                              → VecMatrix→FinMatrix (FinMatrix→VecMatrix M) ≡ M
FinMatrix→VecMatrix→FinMatrix {m = zero} M = funExt (⊥.rec ∘ ¬Fin0)
FinMatrix→VecMatrix→FinMatrix {n = zero} M = funExt₂ (λ _ → ⊥.rec ∘ ¬Fin0)
FinMatrix→VecMatrix→FinMatrix {m = suc m} {n = suc n} M = funExt₂ goal
  where
  goal : (fm : Fin (suc m)) (fn : Fin (suc n))
       → VecMatrix→FinMatrix (_ ∷ FinMatrix→VecMatrix (M ∘ suc)) fm fn ≡ M fm fn
  goal zero zero       = refl
  goal zero (suc fn) i = FinVec→Vec→FinVec (M zero ∘ suc) i fn
  goal (suc fm) fn i   = FinMatrix→VecMatrix→FinMatrix (M ∘ suc) i fm fn

VecMatrix→FinMatrix→VecMatrix : {m n : ℕ} (M : VecMatrix A m n)
                              → FinMatrix→VecMatrix (VecMatrix→FinMatrix M) ≡ M
VecMatrix→FinMatrix→VecMatrix {m = zero} [] = refl
VecMatrix→FinMatrix→VecMatrix {m = suc m} (M ∷ MS) i =
  Vec→FinVec→Vec M i ∷ VecMatrix→FinMatrix→VecMatrix MS i

FinMatrixIsoVecMatrix : (A : Type ℓ) (m n : ℕ) → Iso (FinMatrix A m n) (VecMatrix A m n)
fun (FinMatrixIsoVecMatrix A m n)      = FinMatrix→VecMatrix
inv (FinMatrixIsoVecMatrix A m n)      = VecMatrix→FinMatrix
rightInv (FinMatrixIsoVecMatrix A m n) = VecMatrix→FinMatrix→VecMatrix
leftInv (FinMatrixIsoVecMatrix A m n)  = FinMatrix→VecMatrix→FinMatrix

FinMatrix≃VecMatrix : {m n : ℕ} → FinMatrix A m n ≃ VecMatrix A m n
FinMatrix≃VecMatrix {_} {A} {m} {n} = isoToEquiv (FinMatrixIsoVecMatrix A m n)

FinMatrix≡VecMatrix : (A : Type ℓ) (m n : ℕ) → FinMatrix A m n ≡ VecMatrix A m n
FinMatrix≡VecMatrix _ _ _ = ua FinMatrix≃VecMatrix

-- Define abelian group structure on matrices
module FinMatrixAbGroup (G' : AbGroup ℓ) where

  open AbGroupStr (snd G') renaming ( is-set to isSetG )
  private G = ⟨ G' ⟩

  zeroFinMatrix : ∀ {m n} → FinMatrix G m n
  zeroFinMatrix _ _ = 0g

  negFinMatrix : ∀ {m n} → FinMatrix G m n → FinMatrix G m n
  negFinMatrix M i j = - M i j

  addFinMatrix : ∀ {m n} → FinMatrix G m n → FinMatrix G m n → FinMatrix G m n
  addFinMatrix M N i j = M i j + N i j

  isSetFinMatrix : ∀ {m n} → isSet (FinMatrix G m n)
  isSetFinMatrix = isSetΠ2 λ _ _ → isSetG

  addFinMatrixAssoc : ∀ {m n} → (M N K : FinMatrix G m n)
                    → addFinMatrix M (addFinMatrix N K) ≡ addFinMatrix (addFinMatrix M N) K
  addFinMatrixAssoc M N K i j k = assoc (M j k) (N j k) (K j k) i

  addFinMatrix0r : ∀ {m n} → (M : FinMatrix G m n)
                 → addFinMatrix M zeroFinMatrix ≡ M
  addFinMatrix0r M i j k = rid (M j k) i

  addFinMatrix0l : ∀ {m n} → (M : FinMatrix G m n)
                 → addFinMatrix zeroFinMatrix M ≡ M
  addFinMatrix0l M i j k = lid (M j k) i

  addFinMatrixNegMatrixr : ∀ {m n} → (M : FinMatrix G m n)
                         → addFinMatrix M (negFinMatrix M) ≡ zeroFinMatrix
  addFinMatrixNegMatrixr M i j k = invr (M j k) i

  addFinMatrixNegMatrixl : ∀ {m n} → (M : FinMatrix G m n)
                         → addFinMatrix (negFinMatrix M) M ≡ zeroFinMatrix
  addFinMatrixNegMatrixl M i j k = invl (M j k) i

  addFinMatrixComm : ∀ {m n} → (M N : FinMatrix G m n)
                   → addFinMatrix M N ≡ addFinMatrix N M
  addFinMatrixComm M N i k l = comm (M k l) (N k l) i

  FinMatrixAbGroup : (m n : ℕ) → AbGroup ℓ
  FinMatrixAbGroup m n =
    makeAbGroup {G = FinMatrix G m n} zeroFinMatrix addFinMatrix negFinMatrix
                isSetFinMatrix addFinMatrixAssoc addFinMatrix0r
                addFinMatrixNegMatrixr addFinMatrixComm

-- Define a abelian group structure on vector matrices and prove that
-- it is equal to FinMatrixAbGroup using the SIP
module _ (G' : AbGroup ℓ) where

  open AbGroupStr (snd G')
  private G = ⟨ G' ⟩
  zeroVecMatrix : ∀ {m n} → VecMatrix G m n
  zeroVecMatrix = replicate (replicate 0g)

  negVecMatrix : ∀ {m n} → VecMatrix G m n → VecMatrix G m n
  negVecMatrix = map (map (λ x → - x))

  addVec : ∀ {m} → Vec G m → Vec G m → Vec G m
  addVec [] [] = []
  addVec (x ∷ xs) (y ∷ ys) = x + y ∷ addVec xs ys

  addVecMatrix : ∀ {m n} → VecMatrix G m n → VecMatrix G m n → VecMatrix G m n
  addVecMatrix [] [] = []
  addVecMatrix (M ∷ MS) (N ∷ NS) = addVec M N ∷ addVecMatrix MS NS

  open FinMatrixAbGroup

  -- Proof that FinMatrix→VecMatrix is a group homorphism
  FinMatrix→VecMatrixHomAdd : (m n : ℕ) (M N : FinMatrix G m n)
    → FinMatrix→VecMatrix (addFinMatrix G' M N) ≡
      addVecMatrix (FinMatrix→VecMatrix M) (FinMatrix→VecMatrix N)
  FinMatrix→VecMatrixHomAdd zero n M N = refl
  FinMatrix→VecMatrixHomAdd (suc m) n M N =
    λ i → lem n (M zero) (N zero) i
        ∷ FinMatrix→VecMatrixHomAdd m n (λ i j → M (suc i) j) (λ i j → N (suc i) j) i
     where
     lem : (n : ℕ) (V W : FinVec G n)
       → FinVec→Vec (λ j → V j + W j) ≡ addVec (FinVec→Vec V) (FinVec→Vec W)
     lem zero V W = refl
     lem (suc n) V W = λ i → V zero + W zero ∷ lem n (V ∘ suc) (W ∘ suc) i

  -- Combine everything to get an induced abelian group structure of
  -- VecMatrix that is equal to the one on FinMatrix
  VecMatrixAbGroup : (m n : ℕ) → AbGroup ℓ
  VecMatrixAbGroup m n =
    InducedAbGroup (FinMatrixAbGroup G' m n) addVecMatrix
      FinMatrix≃VecMatrix (FinMatrix→VecMatrixHomAdd m n)

  FinMatrixAbGroup≡VecMatrixAbGroup : (m n : ℕ) → FinMatrixAbGroup G' m n ≡ VecMatrixAbGroup m n
  FinMatrixAbGroup≡VecMatrixAbGroup m n =
    InducedAbGroupPath (FinMatrixAbGroup G' m n) addVecMatrix
      FinMatrix≃VecMatrix (FinMatrix→VecMatrixHomAdd m n)

-- Define identity matrix and matrix multiplication for FinMatrix and
-- prove that square matrices form a ring
module _ (R' : Ring ℓ) where

  open RingStr (snd R') renaming ( is-set to isSetR )
  open RingTheory R'
  open KroneckerDelta R'
  open Sum R'
  open FinMatrixAbGroup (_ , abgroupstr _ _ _ (snd R' .RingStr.+IsAbGroup))

  private R = ⟨ R' ⟩

  oneFinMatrix : ∀ {n} → FinMatrix R n n
  oneFinMatrix i j = δ i j

  mulFinMatrix : ∀ {m1 m2 m3} → FinMatrix R m1 m2 → FinMatrix R m2 m3 → FinMatrix R m1 m3
  mulFinMatrix M N i k = ∑ λ j → M i j · N j k

  ∑Exchange : ∀ {m n} → (M : FinMatrix R m n) → ∑ (λ i → ∑ (λ j → M i j)) ≡ ∑ (λ j → ∑ (λ i → M i j))
  ∑Exchange {m = zero}  {n = n}     M = sym (∑0r n)
  ∑Exchange {m = suc m} {n = zero}  M = cong (λ x → 0r + x) (∑0r m) ∙ +Rid 0r
  ∑Exchange {m = suc m} {n = suc n} M =
     let a  = M zero zero
         L  = ∑ λ j → M zero (suc j)
         C  = ∑ λ i → M (suc i) zero
         N  = ∑ λ i → ∑ λ j → M (suc i) (suc j)
         -- N reindexed
         N' = ∑ λ j → ∑ λ i → M (suc i) (suc j)
     in a + L + ∑ (λ i → ∑ (λ j → M (suc i) j)) ≡⟨ (λ k → a + L + ∑Split (λ i → M (suc i) zero) (λ i → ∑ (λ j → M (suc i) (suc j))) k) ⟩
        a + L + (C + N)                         ≡⟨ (λ k → a + L + (C + ∑Exchange (λ i j → M (suc i) (suc j)) k)) ⟩
        a + L + (C + N')                        ≡⟨ sym (+Assoc _ _ _) ⟩
        a + (L + (C + N'))                      ≡⟨ (λ k → a + +Assoc-comm1 L C N' k) ⟩
        a + (C + (L + N'))                      ≡⟨ +Assoc _ _ _ ⟩
        a + C + (L + N')                        ≡⟨ (λ k → a + C + ∑Split (λ j → M zero (suc j)) (λ j → ∑ (λ i → M (suc i) (suc j))) (~ k)) ⟩
        a + C + ∑ (λ j → ∑ (λ i → M i (suc j))) ∎

  mulFinMatrixAssoc : ∀ {m n k l} → (M : FinMatrix R m n) → (N : FinMatrix R n k) → (K : FinMatrix R k l)
                   → mulFinMatrix M (mulFinMatrix N K) ≡ mulFinMatrix (mulFinMatrix M N) K
  mulFinMatrixAssoc M N K = funExt₂ λ i j →
    ∑ (λ k → M i k · ∑ (λ l → N k l · K l j))   ≡⟨ ∑Ext (λ k → ∑Mulrdist (M i k) (λ l → N k l · K l j)) ⟩
    ∑ (λ k → ∑ (λ l → M i k · (N k l · K l j))) ≡⟨ ∑Ext (λ k → ∑Ext (λ l → ·Assoc (M i k) (N k l) (K l j))) ⟩
    ∑ (λ k → ∑ (λ l → M i k · N k l · K l j))   ≡⟨ ∑Exchange (λ k l → M i k · N k l · K l j) ⟩
    ∑ (λ l → ∑ (λ k → M i k · N k l · K l j))   ≡⟨ ∑Ext (λ l → sym (∑Mulldist (K l j) (λ k → M i k · N k l))) ⟩
    ∑ (λ l → ∑ (λ k → M i k · N k l) · K l j)   ∎

  mulFinMatrixr1 : ∀ {m n} → (M : FinMatrix R m n) → mulFinMatrix M oneFinMatrix ≡ M
  mulFinMatrixr1 M = funExt₂ λ i j → ∑Mulr1 _ (M i) j

  mulFinMatrix1r : ∀ {m n} → (M : FinMatrix R m n) → mulFinMatrix oneFinMatrix M ≡ M
  mulFinMatrix1r M = funExt₂ λ i j → ∑Mul1r _ (λ x → M x j) i

  mulFinMatrixrDistrAddFinMatrix : ∀ {n} (M N K : FinMatrix R n n)
                                 → mulFinMatrix M (addFinMatrix N K) ≡ addFinMatrix (mulFinMatrix M N) (mulFinMatrix M K)
  mulFinMatrixrDistrAddFinMatrix M N K = funExt₂ λ i j →
    ∑ (λ k → M i k · (N k j + K k j))                 ≡⟨ ∑Ext (λ k → ·Rdist+ (M i k) (N k j) (K k j)) ⟩
    ∑ (λ k → M i k · N k j + M i k · K k j)           ≡⟨ ∑Split (λ k → M i k · N k j) (λ k → M i k · K k j) ⟩
    ∑ (λ k → M i k · N k j) + ∑ (λ k → M i k · K k j) ∎

  mulFinMatrixlDistrAddFinMatrix : ∀ {n} (M N K : FinMatrix R n n)
                                 → mulFinMatrix (addFinMatrix M N) K ≡ addFinMatrix (mulFinMatrix M K) (mulFinMatrix N K)
  mulFinMatrixlDistrAddFinMatrix M N K = funExt₂ λ i j →
    ∑ (λ k → (M i k + N i k) · K k j)                 ≡⟨ ∑Ext (λ k → ·Ldist+ (M i k) (N i k) (K k j)) ⟩
    ∑ (λ k → M i k · K k j + N i k · K k j)           ≡⟨ ∑Split (λ k → M i k · K k j) (λ k → N i k · K k j) ⟩
    ∑ (λ k → M i k · K k j) + ∑ (λ k → N i k · K k j) ∎

  FinMatrixRing : (n : ℕ) → Ring ℓ
  FinMatrixRing n =
    makeRing {R = FinMatrix R n n} zeroFinMatrix oneFinMatrix addFinMatrix
             mulFinMatrix negFinMatrix isSetFinMatrix addFinMatrixAssoc
             addFinMatrix0r addFinMatrixNegMatrixr addFinMatrixComm
             mulFinMatrixAssoc mulFinMatrixr1 mulFinMatrix1r
             mulFinMatrixrDistrAddFinMatrix mulFinMatrixlDistrAddFinMatrix

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
open import Common.IO
open import Common.Nat
open import Common.String
open import Common.Unit

private
  n : Nat
  n = 7

{-# COMPILE OCaml n as val n : Z.t #-}

main : IO Unit
main = do
          putStrLn (natToString n)

max_stars_repo_name: xekoukou/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


text:
-- Minimal implicational logic, PHOAS approach, final encoding

module Pf.ArrMp where

-- Types

infixr 0 _=>_
data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty

-- Context and truth judgement

Cx : Set1
Cx = Ty -> Set

isTrue : Ty -> Cx -> Set
isTrue a tc = tc a

-- Terms

TmRepr : Set1
TmRepr = Cx -> Ty -> Set

module ArrMp where
  record Tm (tr : TmRepr) : Set1 where
    infixl 1 _$_
    field
      var  : forall {tc a}   -> isTrue a tc               -> tr tc a
      lam' : forall {tc a b} -> (isTrue a tc -> tr tc b)  -> tr tc (a => b)
      _$_  : forall {tc a b} -> tr tc (a => b) -> tr tc a -> tr tc b

    lam'' : forall {tc a b} -> (tr tc a -> tr tc b) -> tr tc (a => b)
    lam'' f = lam' \x -> f (var x)

    syntax lam'' (\a -> b) = lam a => b
  open Tm {{...}} public

  Thm : Ty -> Set1
  Thm a = forall {tr tc} {{_ : Tm tr}} -> tr tc a
open ArrMp public

-- Example theorems

aI : forall {a} -> Thm (a => a)
aI =
  lam x => x

aK : forall {a b} -> Thm (a => b => a)
aK =
  lam x =>
    lam _ => x

aS : forall {a b c} -> Thm ((a => b => c) => (a => b) => a => c)
aS =
  lam f =>
    lam g =>
      lam x => f $ x $ (g $ x)

tSKK : forall {a} -> Thm (a => a)
tSKK {a = a} =
  aS {b = a => a} $ aK $ aK

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
{-# OPTIONS --prop #-}

postulate
  P : Prop
  p : P

-- C-c C-n should print `p` as `_`

record Box (X : Prop) : Set where
  constructor box
  field unbox : X
open Box

test : P → Box P
test = λ x → box x

-- C-c C-n should print `test` as `λ x → box _`

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2017-01-21, issue #2424

-- {-# OPTIONS -v tc.cover:40 #-}
-- {-# OPTIONS -v interaction.case:40 #-}

postulate Nat : Set

data List : Set₁ where
  _∷_ : (x : Set) (xs : List) → List

test : (As : List) (x : Nat) → Set
test As x = {!As!} -- C-c C-c

-- Expected output:
--   test (x₁ ∷ As) x = {!!}