text:
module DFA where

open import Level
open import Data.Unit
open import Data.List using (List; []; _∷_)
open import Data.Bool using (Bool; true; false; _∧_; _∨_; T; not)
open import Function
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary

open DecSetoid

String : (Σ : Set) → Set
String Σ = List Σ

-- A deterministic finite automaton is a 5-tuple, (Q, Σ, δ, q0, F)
record DFA (Q : DecSetoid zero zero) (Σ : Set): Set₁ where
    constructor dfa
    field
        δ : Carrier Q → Σ → Carrier Q
        initial : Carrier Q
        accepts : Carrier Q → Bool

open DFA

-- eats a character
step : ∀ {Q Σ} → DFA Q Σ → Σ → DFA Q Σ
step (dfa δ initial accept) char = dfa δ (δ initial char) accept

-- eats a lot of characters
steps : ∀ {Q Σ} → DFA Q Σ → String Σ → DFA Q Σ
steps machine []       = machine
steps machine (x ∷ xs) = steps (step machine x) xs

-- a machine M is acceptable if its initial state is in the accept states
acceptable : ∀ {Q Σ} → DFA Q Σ → Bool
acceptable (dfa δ initial accepts) = accepts initial

--------------------------------------------------------------------------------
--  language and automaton
--------------------------------------------------------------------------------

open import Relation.Unary hiding (Decidable)

Language : (Σ : Set) → Set _
Language Σ = Pred (String Σ) zero

-- machine ⇒ language
⟦_⟧ : ∀ {P Σ} → DFA P Σ → Language Σ
⟦ machine ⟧ = λ string → T (acceptable (steps machine string))

_∈?_ : ∀ {P Σ} → (string : String Σ) → (M : DFA P Σ) → Dec (string ∈ ⟦ M ⟧)
string ∈? machine with acceptable (steps machine string)
string ∈? machine | false = no id
string ∈? machine | true = yes tt

--------------------------------------------------------------------------------
--  product and sum
--------------------------------------------------------------------------------

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

-- a helper function for constructing a transition function with product states
product-δ : ∀ {P Q Σ} → DFA P Σ → DFA Q Σ → Carrier P × Carrier Q → Σ → Carrier P × Carrier Q
product-δ A B (p , q) c = δ A p c , δ B q c

-- intersection
infixl 30 _∩ᴹ_
_∩ᴹ_ : ∀ {P Q Σ} → DFA P Σ → DFA Q Σ → DFA (P ×-decSetoid Q) Σ
A ∩ᴹ B = dfa
    (product-δ A B)
    (initial A , initial B)
    (uncurry (λ p q → accepts A p ∧ accepts B q))

-- union
infixl 29 _∪ᴹ_
_∪ᴹ_ : ∀ {P Q Σ} → DFA P Σ → DFA Q Σ → DFA (P ×-decSetoid Q) Σ
A ∪ᴹ B = dfa
    (product-δ A B)
    (initial A , initial B)
    (uncurry (λ p q → accepts A p ∨ accepts B q))

-- negation
infixl 31 Cᴹ_
Cᴹ_ : ∀ {P Σ} → DFA P Σ → DFA P Σ
Cᴹ dfa δ initial accepts = dfa δ initial (not ∘ accepts)

--------------------------------------------------------------------------------
--  concatenation
--------------------------------------------------------------------------------

open import Data.Sum
open import Relation.Binary.Sum
open import Data.Empty

module Pointwise where
    -- _⊎-decSetoid_ : ∀ {d₁ d₂ d₃ d₄}
    --     → DecSetoid d₁ d₂
    --     → DecSetoid d₃ d₄
    --     → DecSetoid _ _
    -- _⊎-decSetoid_ {d₁} {d₂} {d₃} {d₄} s₁ s₂ = record
    --     { Carrier = Carrier s₁ ⊎ Carrier s₂
    --     ; _≈_ = _⊎-≈_
    --     ; isDecEquivalence = record
    --         { isEquivalence = ⊎-≈-isEquivalence
    --         ; _≟_ = ⊎-≈-decidable
    --         }
    --     }
    --     where
    --
    --         open DecSetoid
    --         _⊎-≈_ : Carrier s₁ ⊎ Carrier s₂
    --             → Carrier s₁ ⊎ Carrier s₂
    --             → Set (d₂ ⊔ d₄)
    --         _⊎-≈_ (inj₁ x) (inj₁ y) = Lift {d₂} {d₄} (_≈_ s₁ x y)  -- (_≈_ s₁ x y)
    --         _⊎-≈_ (inj₁ x) (inj₂ y) = Lift ⊥
    --         _⊎-≈_ (inj₂ x) (inj₁ y) = Lift ⊥
    --         _⊎-≈_ (inj₂ x) (inj₂ y) = Lift {d₄} {d₂} (_≈_ s₂ x y)
    --
    --         open IsEquivalence
    --         module S₁ = IsDecEquivalence (isDecEquivalence s₁)
    --         module S₂ = IsDecEquivalence (isDecEquivalence s₂)
    --
    --         ⊎-≈-refl : Reflexive _⊎-≈_
    --         ⊎-≈-refl {inj₁ x} = lift (refl S₁.isEquivalence)
    --         ⊎-≈-refl {inj₂ y} = lift (refl S₂.isEquivalence)
    --
    --         ⊎-≈-sym : Symmetric _⊎-≈_
    --         ⊎-≈-sym {inj₁ x} {inj₁ y} (lift eq) = lift (sym S₁.isEquivalence eq)
    --         ⊎-≈-sym {inj₁ x} {inj₂ y} (lift ())
    --         ⊎-≈-sym {inj₂ x} {inj₁ y} (lift ())
    --         ⊎-≈-sym {inj₂ x} {inj₂ y} (lift eq) = lift (sym S₂.isEquivalence eq)
    --
    --         ⊎-≈-trans : Transitive _⊎-≈_
    --         ⊎-≈-trans {inj₁ x} {inj₁ y} {inj₁ z} (lift p) (lift q) = lift (trans S₁.isEquivalence p q)
    --         ⊎-≈-trans {inj₁ x} {inj₁ y} {inj₂ z} p        (lift ())
    --         ⊎-≈-trans {inj₁ x} {inj₂ y} {_}      (lift ()) q
    --         ⊎-≈-trans {inj₂ x} {inj₁ y} {_}      (lift ()) q
    --         ⊎-≈-trans {inj₂ x} {inj₂ y} {inj₁ z} p        (lift ())
    --         ⊎-≈-trans {inj₂ x} {inj₂ y} {inj₂ z} (lift p) (lift q) = lift (trans S₂.isEquivalence p q)
    --
    --         ⊎-≈-isEquivalence : IsEquivalence _⊎-≈_
    --         ⊎-≈-isEquivalence = record
    --             { refl = λ {x} → ⊎-≈-refl {x}
    --             ; sym = λ {x} {y} eq → ⊎-≈-sym {x} {y} eq
    --             ; trans = λ {x} {y} {z} p q → ⊎-≈-trans {x} {y} {z} p q
    --             }
    --
    --         lift-dec : ∀ {a} {b} {P : Set a} → Dec P → Dec (Lift {a} {b} P)
    --         lift-dec (yes p) = yes (lift p)
    --         lift-dec (no ¬p) = no (λ p → contradiction (lower p) ¬p)
    --
    --         ⊎-≈-decidable : Decidable _⊎-≈_
    --         ⊎-≈-decidable (inj₁ x) (inj₁ y) = lift-dec (S₁._≟_ x y)
    --         ⊎-≈-decidable (inj₁ x) (inj₂ y) = no lower
    --         ⊎-≈-decidable (inj₂ x) (inj₁ y) = no lower
    --         ⊎-≈-decidable (inj₂ x) (inj₂ y) = lift-dec (S₂._≟_ x y)

infixl 28 _++_
_++_ : ∀ {P Q Σ} → DFA P Σ → DFA Q Σ → DFA (P ⊎-decSetoid Q) Σ
_++_ {P} {Q} {Σ} A B = dfa
    δ'
    (inj₁ (initial A))
    accepts'
    where
        δ' : Carrier (P ⊎-decSetoid Q) → Σ → Carrier (P ⊎-decSetoid Q)
        δ' (inj₁ state) character with acceptable (step A character)
        δ' (inj₁ state) character | false = inj₁ (δ A state character)
        δ' (inj₁ state) character | true = inj₂ (initial B)
        δ' (inj₂ state) character = inj₂ (δ B state character)

        accepts' : Carrier (P ⊎-decSetoid Q) → Bool
        accepts' (inj₁ state) = false
        accepts' (inj₂ state) = accepts B state

-- -- ++-right-identity : {P Q Σ : Set}
-- --     → (A : DFA P Σ) → (B : DFA Q Σ)
-- --     → Empty B
-- --     → DFA (P ⊎ Q) Σ
--
--------------------------------------------------------------------------------
--  Kleene closure
--------------------------------------------------------------------------------

-- 1. make the initial state the accept state
-- 2. wire all of the transitions that would've gone to the original accept
--    states to the initial state (which is the new accept state)
infixl 32 _*
_* : ∀ {Q Σ} → DFA Q Σ → DFA Q Σ
_* {Q} {Σ} M = dfa δ' (initial M) accepts'
    where

        δ' : Carrier Q → Σ → Carrier Q
        δ' state character with acceptable (step M character)
        δ' state character | false = δ M state character
        δ' state character | true = initial M

        open IsDecEquivalence (isDecEquivalence Q) renaming (_≟_ to _≟s_)
        open import Relation.Nullary.Decidable
        accepts' : Carrier Q → Bool
        accepts' state = ⌊ state ≟s initial M ⌋

--------------------------------------------------------------------------------
--  Properties
--------------------------------------------------------------------------------

module Properties (Σ : Set) where

    open import Function.Equality using (Π)
    open Π
    open import Function.Equivalence using (_⇔_; Equivalence)
    open import Data.Bool.Properties as BoolProp
    open import Relation.Nullary.Negation
    -- extracting one direction of a function equivalence
    ⟦_⟧→ : {A B : Set} → A ⇔ B → A → B
    ⟦ A⇔B ⟧→ A = Equivalence.to A⇔B ⟨$⟩ A

    ←⟦_⟧ : {A B : Set} → A ⇔ B → B → A
    ←⟦ A⇔B ⟧ B = Equivalence.from A⇔B ⟨$⟩ B

    open import Relation.Unary.Membership (String Σ)
    open ⊆-Reasoning

    ∩-homo⇒ : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ∩ᴹ B ⟧ ⊆′ ⟦ A ⟧ ∩ ⟦ B ⟧
    ∩-homo⇒ A B []       = ⟦ BoolProp.T-∧ ⟧→
    ∩-homo⇒ A B (x ∷ xs) = ∩-homo⇒ (step A x) (step B x) xs

    ∩-homo⇐ : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ⟧ ∩ ⟦ B ⟧ ⊆′ ⟦ A ∩ᴹ B ⟧
    ∩-homo⇐ A B []       = ←⟦ BoolProp.T-∧ ⟧
    ∩-homo⇐ A B (x ∷ xs) = ∩-homo⇐ (step A x) (step B x) xs

    ∩-homo : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ∩ᴹ B ⟧ ≋ ⟦ A ⟧ ∩ ⟦ B ⟧
    ∩-homo A B = (∩-homo⇒ A B) , (∩-homo⇐ A B)

    ∩-sym⇒ : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ∩ᴹ B ⟧ ⊆′ ⟦ B ∩ᴹ A ⟧
    ∩-sym⇒ A B xs P =
            xs
        ∈⟨ P ⟩
            ⟦ A ∩ᴹ B ⟧
        ⊆⟨ ∩-homo⇒ A B ⟩
            ⟦ A ⟧ ∩ ⟦ B ⟧
        →⟨ swap ⟩
            ⟦ B ⟧ ∩ ⟦ A ⟧
        ⊆⟨ ∩-homo⇐ B A ⟩
            ⟦ B ∩ᴹ A ⟧
        ∎

    ∩-sym : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ∩ᴹ B ⟧ ≋ ⟦ B ∩ᴹ A ⟧
    ∩-sym A B = (∩-sym⇒ A B) , (∩-sym⇒ B A)

    ∪-homo⇒ : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ∪ᴹ B ⟧ ⊆′ ⟦ A ⟧ ∪ ⟦ B ⟧
    ∪-homo⇒ A B []       P = ⟦ BoolProp.T-∨ ⟧→ P
    ∪-homo⇒ A B (x ∷ xs) P = ∪-homo⇒ (step A x) (step B x) xs P

    ∪-homo⇐ : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ⟧ ∪ ⟦ B ⟧ ⊆′ ⟦ A ∪ᴹ B ⟧
    ∪-homo⇐ A B []       P = ←⟦ BoolProp.T-∨ ⟧ P
    ∪-homo⇐ A B (x ∷ xs) P = ∪-homo⇐ (step A x) (step B x) xs P

    ∪-homo : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ∪ᴹ B ⟧ ≋ ⟦ A ⟧ ∪ ⟦ B ⟧
    ∪-homo A B = (∪-homo⇒ A B) , (∪-homo⇐ A B)

    ∪-sym⇒ : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ∪ᴹ B ⟧ ⊆′ ⟦ B ∪ᴹ A ⟧
    ∪-sym⇒ A B xs P =
            xs
        ∈⟨ P ⟩
            ⟦ A ∪ᴹ B ⟧
        ⊆⟨ ∪-homo⇒ A B ⟩
            ⟦ A ⟧ ∪ ⟦ B ⟧
        →⟨ ⊎-swap ⟩
            ⟦ B ⟧ ∪ ⟦ A ⟧
        ⊆⟨ ∪-homo⇐ B A ⟩
            ⟦ B ∪ᴹ A ⟧
        ∎
        where
            ⊎-swap : ∀ {a b} {A : Set a} {B : Set b} → A ⊎ B → B ⊎ A
            ⊎-swap (inj₁ x) = inj₂ x
            ⊎-swap (inj₂ y) = inj₁ y

    ∪-sym : ∀ {P Q} → (A : DFA P Σ) → (B : DFA Q Σ)
        → ⟦ A ∪ᴹ B ⟧ ≋ ⟦ B ∪ᴹ A ⟧
    ∪-sym A B = (∪-sym⇒ A B) , (∪-sym⇒ B A)

    T-not-¬ : {b : Bool} → T (not b) → ¬ (T b)
    T-not-¬ {false} P Q = Q
    T-not-¬ {true}  P Q = P

    T-¬-not : {b : Bool} → ¬ (T b) → T (not b)
    T-¬-not {false} P = tt
    T-¬-not {true}  P = P tt

    C⇒ : ∀ {P} → (M : DFA P Σ)
        → ∁ ⟦ M ⟧ ⊆ ⟦ Cᴹ M ⟧
    C⇒ M {[]}     = T-¬-not
    C⇒ M {x ∷ xs} = C⇒ (step M x) {xs}

    C⇐ : ∀ {P} → (M : DFA P Σ)
        → ⟦ Cᴹ M ⟧ ⊆ ∁ ⟦ M ⟧
    C⇐ M {[]}     = T-not-¬
    C⇐ M {x ∷ xs} = C⇐ (step M x) {xs}

    C-∩-∅⇒ : ∀ {P} → (M : DFA P Σ) → ⟦ M ∩ᴹ Cᴹ M ⟧ ⊆ ∅
    C-∩-∅⇒ M {[]} P =
        let
            Q , ¬Q = ∩-homo⇒ M (Cᴹ M) [] P
        in contradiction Q (C⇐ M {[]} ¬Q)
    C-∩-∅⇒ M {x ∷ xs} = C-∩-∅⇒ (step M x) {xs}

    C-∩-∅⇐ : ∀ {P} → (M : DFA P Σ) → ∅ ⊆ ⟦ M ∩ᴹ Cᴹ M ⟧
    C-∩-∅⇐ M {[]} ()
    C-∩-∅⇐ M {x ∷ xs} = C-∩-∅⇐ (step M x) {xs}

    C-∪-U⇒ : ∀ {P} → (M : DFA P Σ) → ⟦ M ∪ᴹ Cᴹ M ⟧ ⊆ U
    C-∪-U⇒ M {[]} P = tt
    C-∪-U⇒ M {x ∷ xs} = C-∪-U⇒ (step M x) {xs}

    C-∪-U⇐ : ∀ {P} → (M : DFA P Σ) → U ⊆ ⟦ M ∪ᴹ Cᴹ M ⟧
    C-∪-U⇐ M {[]} P with [] ∈? M
    C-∪-U⇐ M {[]} P | yes p = ←⟦ T-∨ ⟧ (inj₁ p)
    C-∪-U⇐ M {[]} P | no ¬p = ←⟦ T-∨
            {accepts M (initial M)}
            {not (accepts M (initial M))}
        ⟧ (inj₂ (T-¬-not ¬p))
    C-∪-U⇐ M {x ∷ xs} = C-∪-U⇐ (step M x) {xs}

max_stars_repo_name: banacorn/formal-language

max_issues_repo_name: banacorn/formal-language

max_forks_repo_name: banacorn/formal-language


text:
{-# OPTIONS --safe --no-qualified-instances #-}
module CF.Transform.Compile.Expressions where

open import Function using (_∘_)
open import Level
open import Data.Unit
open import Data.Bool
open import Data.Product as P
open import Data.List as L hiding (null; [_])
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.All
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Unary hiding (_∈_)
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Monad
open import Relation.Ternary.Construct.Bag.Properties

private
  module Src where
    open import CF.Syntax.DeBruijn public
    open import CF.Types public
    open import CF.Contexts.Lexical using (module DeBruijn) public; open DeBruijn public

  module Tgt where
    open import JVM.Types public
    open import JVM.Model StackTy public
    open import JVM.Syntax.Values public
    open import JVM.Syntax.Instructions public

open Src
open Tgt

open import JVM.Compiler
open import CF.Transform.Compile.ToJVM

-- Compilation of CF expressions
compileₑₛ : ∀ {as ψ Γ} → Exps as Γ → ε[ Compiler ⟦ Γ ⟧ ψ (⟦ as ⟧ ++ ψ) Emp ]

compileₑ  : ∀ {a ψ Γ}  → Exp a Γ   → ε[ Compiler ⟦ Γ ⟧ ψ (⟦ a ⟧ ∷ ψ) Emp ]

compileₑ (unit) = do
  code (push (bool true))

compileₑ (num x) = do
  code (push (num x))

compileₑ (bool b) = do
  code (push (bool b))

compileₑ (var' x) = do
  code (load ⟦ x ⟧)

compileₑ (bop f e₁ e₂) = do
  compileₑ e₁
  compileₑ e₂
  compile-bop f

  where

    -- a < b compiles to (assume a and b on stack):
    --
    --     if_icmplt l⁻
    --     iconst_1
    --     goto e⁻
    -- l⁺: iconst_0
    -- e⁺: nop
    --
    -- Other comparisons go similar
    compile-comp : ∀ {Γ as} → Comparator as → ε[ Compiler Γ (as ++ ψ) (boolean ∷ ψ) Emp ]
    compile-comp cmp = do
      ↓ lfalse⁻ ∙⟨ σ ⟩ lfalse⁺ ← ✴-swap ⟨$⟩ freshLabel
      lfalse⁺                  ← ✴-id⁻ˡ ⟨$⟩ (code (if cmp lfalse⁻) ⟨ Up _  # σ ⟩& lfalse⁺)
      lfalse⁺                  ← ✴-id⁻ˡ ⟨$⟩ (code (push (bool false)) ⟨ Up _  # ∙-idˡ ⟩& lfalse⁺)
      ↓ lend⁻ ∙⟨ σ ⟩ labels    ← (✴-rotateₗ ∘ ✴-assocᵣ) ⟨$⟩ (freshLabel ⟨ Up _  # ∙-idˡ ⟩& lfalse⁺)
      lfalse⁺ ∙⟨ σ ⟩ lend⁺     ← ✴-id⁻ˡ ⟨$⟩ (code (goto lend⁻) ⟨ _ ✴ _ # σ ⟩& labels)
      lend⁺                    ← ✴-id⁻ˡ ⟨$⟩ (attach lfalse⁺ ⟨ Up _ # σ ⟩& lend⁺)
      code (push (bool true))
      attach lend⁺

    -- Compile comparisons and other binary operations
    compile-bop : ∀ {Γ a b c} → BinOp a b c → ε[ Compiler Γ (⟦ b ⟧ ∷ ⟦ a ⟧ ∷ ψ) (⟦ c ⟧ ∷ ψ) Emp ]
    compile-bop add = code (bop add)
    compile-bop sub = code (bop sub)
    compile-bop mul = code (bop mul)
    compile-bop div = code (bop div)
    compile-bop xor = code (bop xor)
    compile-bop eq  = compile-comp icmpeq
    compile-bop ne  = compile-comp icmpne
    compile-bop lt  = compile-comp icmplt
    compile-bop ge  = compile-comp icmpge
    compile-bop gt  = compile-comp icmpgt
    compile-bop le  = compile-comp icmplt

compileₑ (ifthenelse c e₁ e₂) = do
  -- condition
  compileₑ c
  lthen+ ∙⟨ σ ⟩ ↓ lthen-  ← freshLabel
  lthen+                  ← ✴-id⁻ˡ ⟨$⟩ (code (if ne lthen-) ⟨ Up _  # ∙-comm σ     ⟩& lthen+)

  -- else
  compileₑ e₂
  ↓ lend- ∙⟨ σ ⟩ labels   ← (✴-rotateₗ ∘ ✴-assocᵣ) ⟨$⟩ (freshLabel ⟨ Up _  # ∙-idˡ        ⟩& lthen+)

  -- then
  lthen+ ∙⟨ σ ⟩ lend+     ← ✴-id⁻ˡ ⟨$⟩ (code (goto lend-) ⟨ _ ✴ _ # σ ⟩& labels)
  lend+                   ← ✴-id⁻ˡ ⟨$⟩ (attach lthen+ ⟨ Up _  # σ ⟩& lend+)
  compileₑ e₁

  -- label the end
  attach lend+

compileₑₛ [] = return refl
compileₑₛ (e ∷ es) = do
  compileₑₛ es
  compileₑ e

ext: agda


text:
module _ where

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

open _×_

partial : ∀ {A B} → A → A × B
partial x .fst = x

open import Agda.Builtin.Equality

theorem : ∀ {A} (x : A) → partial x .snd ≡ x
theorem x = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

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

module Categories.Adjoint.Construction.Kleisli {o ℓ e} {C : Category o ℓ e} (M : Monad C) where

open import Categories.Category.Construction.Kleisli using (Kleisli)
open import Categories.Adjoint using (_⊣_)
open import Categories.Functor using (Functor; _∘F_)
open import Categories.Morphism using (Iso)
open import Categories.Functor.Properties using ([_]-resp-square)
open import Categories.NaturalTransformation.Core using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Morphism.Reasoning C

private
  module C = Category C
  module M = Monad M
  open M.F
  open M using (module μ; module η)
  open C using (Obj; _⇒_; _∘_; _≈_; ∘-resp-≈ʳ; ∘-resp-≈ˡ; assoc; sym-assoc; identityˡ)
  open C.HomReasoning
  open C.Equiv

Forgetful : Functor (Kleisli M) C
Forgetful = record
  { F₀           = λ X → F₀ X
  ; F₁           = λ f → μ.η _ ∘ F₁ f
  ; identity     = M.identityˡ
  ; homomorphism = λ {X Y Z} {f g} → begin
    μ.η Z ∘ F₁ ((μ.η Z ∘ F₁ g) ∘ f)         ≈⟨ refl⟩∘⟨ homomorphism ⟩
    μ.η Z ∘ F₁ (μ.η Z ∘ F₁ g) ∘ F₁ f        ≈⟨ refl⟩∘⟨ homomorphism ⟩∘⟨refl ⟩
    μ.η Z ∘ (F₁ (μ.η Z) ∘ F₁ (F₁ g)) ∘ F₁ f ≈⟨ pull-first M.assoc ⟩
    (μ.η Z ∘ μ.η (F₀ Z)) ∘ F₁ (F₁ g) ∘ F₁ f ≈⟨ center (μ.commute g) ⟩
    μ.η Z ∘ (F₁ g ∘ μ.η Y) ∘ F₁ f           ≈⟨ pull-first refl ⟩
    (μ.η Z ∘ F₁ g) ∘ μ.η Y ∘ F₁ f           ∎
  ; F-resp-≈     = λ eq → ∘-resp-≈ʳ (F-resp-≈ eq)
  }

Free : Functor C (Kleisli M)
Free = record
  { F₀           = λ X → X
  ; F₁           = λ f → η.η _ ∘ f
  ; identity     = C.identityʳ
  ; homomorphism = λ {X Y Z} {f g} → begin
    η.η Z ∘ g ∘ f                             ≈⟨ sym-assoc ○ ⟺ identityˡ ⟩
    C.id ∘ (η.η Z ∘ g) ∘ f                    ≈˘⟨ pull-first M.identityˡ ⟩
    μ.η Z ∘ (F₁ (η.η Z) ∘ η.η Z ∘ g) ∘ f      ≈⟨ refl⟩∘⟨ pushʳ (η.commute g) ⟩∘⟨refl ⟩
    μ.η Z ∘ ((F₁ (η.η Z) ∘ F₁ g) ∘ η.η Y) ∘ f ≈˘⟨ center (∘-resp-≈ˡ homomorphism) ⟩
    (μ.η Z ∘ F₁ (η.η Z ∘ g)) ∘ η.η Y ∘ f      ∎
  ; F-resp-≈     = ∘-resp-≈ʳ
  }

FF≃F : Forgetful ∘F Free ≃ M.F
FF≃F = record
  { F⇒G = ntHelper record
    { η       = λ X → F₁ C.id
    ; commute = λ {X Y} f → begin
      F₁ C.id ∘ μ.η Y ∘ F₁ (η.η Y ∘ f)      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ homomorphism ⟩
      F₁ C.id ∘ μ.η Y ∘ F₁ (η.η Y) ∘ F₁ f   ≈⟨ refl⟩∘⟨ cancelˡ M.identityˡ ⟩
      F₁ C.id ∘ F₁ f                        ≈⟨ [ M.F ]-resp-square id-comm-sym ⟩
      F₁ f ∘ F₁ C.id                        ∎
    }
  ; F⇐G = ntHelper record
    { η       = λ X → F₁ C.id
    ; commute = λ {X Y} f → begin
      F₁ C.id ∘ F₁ f                         ≈⟨ [ M.F ]-resp-square id-comm-sym ⟩
      F₁ f ∘ F₁ C.id                         ≈˘⟨ cancelˡ M.identityˡ ⟩∘⟨refl ⟩
      (μ.η Y ∘ F₁ (η.η Y) ∘ F₁ f) ∘ F₁ C.id  ≈˘⟨ ∘-resp-≈ʳ homomorphism ⟩∘⟨refl ⟩
      (μ.η Y ∘ F₁ (η.η Y ∘ f)) ∘ F₁ C.id     ∎
    }
  ; iso = λ X → record
    { isoˡ = elimˡ identity ○ identity
    ; isoʳ = elimˡ identity ○ identity
    }
  }

Free⊣Forgetful : Free ⊣ Forgetful
Free⊣Forgetful = record
  { unit   = ntHelper record
    { η       = η.η
    ; commute = λ {X Y} f → begin
      η.η Y ∘ f                            ≈⟨ η.commute f ⟩
      F₁ f ∘ η.η X                         ≈˘⟨ cancelˡ M.identityˡ ⟩∘⟨refl ⟩
      (μ.η Y ∘ F₁ (η.η Y) ∘ F₁ f) ∘ η.η X  ≈˘⟨ ∘-resp-≈ʳ homomorphism ⟩∘⟨refl ⟩
      (μ.η Y ∘ F₁ (η.η Y ∘ f)) ∘ η.η X     ∎
    }
  ; counit = ntHelper record
    { η       = λ X → F₁ C.id
    ; commute = λ {X Y} f → begin
      (μ.η Y ∘ F₁ (F₁ C.id)) ∘ η.η (F₀ Y) ∘ μ.η Y ∘ F₁ f  ≈⟨ elimʳ (F-resp-≈ identity ○ identity) ⟩∘⟨refl ⟩
      μ.η Y ∘ η.η (F₀ Y) ∘ μ.η Y ∘ F₁ f                   ≈⟨ cancelˡ M.identityʳ ⟩
      μ.η Y ∘ F₁ f                                        ≈⟨ introʳ identity ⟩
      (μ.η Y ∘ F₁ f) ∘ F₁ C.id                            ∎
    }
  ; zig    = λ {A} → begin
    (μ.η A ∘ F₁ (F₁ C.id)) ∘ η.η (F₀ A) ∘ η.η A  ≈⟨ elimʳ (F-resp-≈ identity ○ identity) ⟩∘⟨refl ⟩
    μ.η A ∘ η.η (F₀ A) ∘ η.η A                   ≈⟨ cancelˡ M.identityʳ ⟩
    η.η A                                        ∎
  ; zag    = λ {B} → begin
    (μ.η B ∘ F₁ (F₁ C.id)) ∘ η.η (F₀ B)  ≈⟨ elimʳ (F-resp-≈ identity ○ identity) ⟩∘⟨refl ⟩
    μ.η B ∘ η.η (F₀ B)                   ≈⟨ M.identityʳ ⟩
    C.id                                 ∎
  }

module KleisliExtension where

  κ : {A B : Obj} → (f : A ⇒ F₀ B) → F₀ A ⇒ F₀ B
  κ {_} {B} f = μ.η B ∘ F₁ f

  f-iso⇒Klf-iso : ∀ {A B : Obj} → (f : A ⇒ F₀ B) → (g : B ⇒ F₀ A) → Iso (Kleisli M) g f → Iso C (κ f) (κ g)
  f-iso⇒Klf-iso {A} {B} f g (record { isoˡ = isoˡ ; isoʳ = isoʳ }) = record
    { isoˡ = begin
       (μ.η A ∘ F₁ g) ∘ μ.η B ∘ F₁ f           ≈⟨ center (sym (μ.commute g)) ⟩
       μ.η A ∘ (μ.η (F₀ A) ∘ F₁ (F₁ g)) ∘ F₁ f ≈⟨ assoc²'' ○ pushˡ M.sym-assoc ⟩
       μ.η A ∘ F₁ (μ.η A) ∘ F₁ (F₁ g) ∘ F₁ f   ≈⟨ refl⟩∘⟨ sym trihom ⟩
       μ.η A ∘ F₁ (μ.η A ∘ F₁ g ∘ f)           ≈⟨ refl⟩∘⟨ F-resp-≈ sym-assoc ⟩
       μ.η A ∘ F₁ ((μ.η A ∘ F₁ g) ∘ f)         ≈⟨ refl⟩∘⟨ F-resp-≈ isoʳ ○ M.identityˡ ⟩
       C.id                                        ∎
    ; isoʳ = begin
       (μ.η B ∘ F₁ f) ∘ μ.η A ∘ F₁ g           ≈⟨ center (sym (μ.commute f)) ⟩
       μ.η B ∘ (μ.η (F₀ B) ∘ F₁ (F₁ f)) ∘ F₁ g ≈⟨ assoc²'' ○ pushˡ M.sym-assoc ⟩
       μ.η B ∘ F₁ (μ.η B) ∘ F₁ (F₁ f) ∘ F₁ g   ≈⟨ refl⟩∘⟨ sym trihom ⟩
       μ.η B ∘ F₁ (μ.η B ∘ F₁ f ∘ g)           ≈⟨ refl⟩∘⟨ F-resp-≈ sym-assoc ⟩
       μ.η B ∘ F₁ ((μ.η B ∘ F₁ f) ∘ g)         ≈⟨ refl⟩∘⟨ F-resp-≈ isoˡ ○ M.identityˡ ⟩
       C.id                                        ∎
    }
    where
    trihom : {X Y Z W : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} {h : Z ⇒ W} → F₁ (h ∘ g ∘ f) ≈ F₁ h ∘ F₁ g ∘ F₁ f
    trihom {X} {Y} {Z} {W} {f} {g} {h} = begin
      F₁ (h ∘ g ∘ f)     ≈⟨ homomorphism ⟩
      F₁ h ∘ F₁ (g ∘ f)  ≈⟨ refl⟩∘⟨ homomorphism ⟩
      F₁ h ∘ F₁ g ∘ F₁ f ∎

  Klf-iso⇒f-iso : ∀ {A B : Obj} → (f : A ⇒ F₀ B) → (g : B ⇒ F₀ A) → Iso C (κ f) (κ g) → Iso (Kleisli M) g f
  Klf-iso⇒f-iso {A} {B} f g record { isoˡ = isoˡ ; isoʳ = isoʳ } = record
    { isoˡ = begin
      (μ.η B ∘ F₁ f) ∘ g                          ≈⟨ introʳ M.identityʳ ⟩∘⟨refl ⟩
      ((μ.η B ∘ F₁ f) ∘ (μ.η A ∘ η.η (F₀ A))) ∘ g ≈⟨ assoc ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ assoc ○ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
      μ.η B ∘ F₁ f ∘ (μ.η A) ∘ (η.η (F₀ A) ∘ g)   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ η.commute g ⟩
      μ.η B ∘ F₁ f ∘ μ.η A ∘ (F₁ g ∘ η.η B)       ≈˘⟨ assoc ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ assoc ○ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
      ((μ.η B ∘ F₁ f) ∘ μ.η A ∘ F₁ g) ∘ η.η B     ≈⟨ elimˡ isoʳ ⟩
      η.η B                                           ∎
    ; isoʳ = begin
      (μ.η A ∘ F₁ g) ∘ f                          ≈⟨ introʳ M.identityʳ ⟩∘⟨refl ⟩
      ((μ.η A ∘ F₁ g) ∘ (μ.η B ∘ η.η (F₀ B))) ∘ f ≈⟨ assoc ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ assoc ○ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
      μ.η A ∘ F₁ g ∘ (μ.η B) ∘ (η.η (F₀ B) ∘ f)   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ η.commute f ⟩
      μ.η A ∘ F₁ g ∘ μ.η B ∘ (F₁ f ∘ η.η A)       ≈˘⟨ assoc ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ assoc ○ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
      ((μ.η A ∘ F₁ g) ∘ μ.η B ∘ F₁ f) ∘ η.η A     ≈⟨ elimˡ isoˡ ⟩
      η.η A                                       ∎
    }

  kl-ext-compat : ∀ {A B X : Obj} → (f : A ⇒ F₀ B) → (g : B ⇒ F₀ X) → κ ((κ g) ∘ f) ≈ κ g ∘ κ f
  kl-ext-compat {A} {B} {X} f g = begin
    μ.η X ∘ F₁ ((μ.η X ∘ F₁ g) ∘ f)         ≈⟨ refl⟩∘⟨ F-resp-≈ assoc ○ refl⟩∘⟨ trihom ⟩
    μ.η X ∘ (F₁ (μ.η X) ∘ F₁ (F₁ g) ∘ F₁ f) ≈⟨ sym-assoc ⟩
    (μ.η X ∘ F₁ (μ.η X)) ∘ F₁ (F₁ g) ∘ F₁ f ≈⟨ M.assoc ⟩∘⟨refl ⟩
    (μ.η X ∘ μ.η (F₀ X)) ∘ F₁ (F₁ g) ∘ F₁ f ≈⟨ center (μ.commute g) ⟩
    μ.η X ∘ (F₁ g ∘ μ.η B) ∘ F₁ f           ≈⟨ sym-assoc ○ (sym-assoc ⟩∘⟨refl) ○ assoc ⟩
    (μ.η X ∘ F₁ g) ∘ μ.η B ∘ F₁ f           ∎
    where
    trihom : {X Y Z W : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} {h : Z ⇒ W} → F₁ (h ∘ g ∘ f) ≈ F₁ h ∘ F₁ g ∘ F₁ f
    trihom {X} {Y} {Z} {W} {f} {g} {h} = begin
      F₁ (h ∘ g ∘ f)     ≈⟨ homomorphism ⟩
      F₁ h ∘ F₁ (g ∘ f)  ≈⟨ refl⟩∘⟨ homomorphism ⟩
      F₁ h ∘ F₁ g ∘ F₁ f ∎

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

-- see also https://lists.chalmers.se/pipermail/agda-dev/2015-January/000041.html

open import Common.IO
open import Common.Unit
open import Common.Nat

f : (m : Nat) {l : Nat} -> Nat
f zero {l = l} = l
f (suc y) = y

main : IO Unit
main = printNat (f 0 {1}) ,,
  putStr "\n" ,,
  printNat (f 30 {1})

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Prelude
open import Level using (Level; _⊔_; Lift) renaming (zero to lz; suc to ls)
open import Data.Maybe using (Maybe; nothing; just)

module RW.Utils.Monads where

  ---------------------
  -- Monad Typeclass --
  ---------------------

  record Monad {a}(M : Set a → Set a) : Set (ls a) where
    infixl 1 _>>=_
    field
      return : {A : Set a} → A → M A
      _>>=_  : {A B : Set a} → M A → (A → M B) → M B

  open Monad {{...}}

  mapM : ∀{a}{M : Set a → Set a}{{ m : Monad M}}{A B : Set a}
       → (A → M B) → List A → M (List B)
  mapM f []       = return []
  mapM f (x ∷ la) = f x >>= (λ x' → mapM f la >>= return ∘ _∷_ x')

  _>>_ : ∀{a}{M : Set a → Set a}{{ m : Monad M }}{A B : Set a}
       → M A → M B → M B
  f >> g = f >>= λ _ → g

  -- Binds the side-effects of the second computation,
  -- returning the value of the first.
  _<>=_ : ∀{a}{M : Set a → Set a}{{ m : Monad M }}{A B : Set a}
        → M A → (A → M B) → M A
  f <>= x = f >>= λ r → x r >> return r

  {-
  _<$>_ : ∀{a}{A B : Set a}{M : Set a → Set a}{{ m : Monad M }}
        → (A → B) → M A → M B
  f <$> x = ?
  -}

  -----------------
  -- Maybe Monad --
  -----------------

  _<$>+1_ : ∀{a}{A B : Set a} → (A → B) → Maybe A → Maybe B
  f <$>+1 x with x
  ...| nothing = nothing
  ...| just x' = just (f x')

  instance
    MonadMaybe : ∀{a} → Monad {a} Maybe
    MonadMaybe = record
      { return = just
      ; _>>=_  = λ { nothing  _ → nothing
                   ; (just x) f → f x
                   }
      }

  -----------------
  -- State Monad --
  -----------------

  record ST (s a : Set) : Set where
    field run : s → (a × s)

  evalST : ∀{a s} → ST s a → s → a
  evalST s = p1 ∘ (ST.run s)

  get : ∀{s} → ST s s
  get = record { run = λ s → (s , s) }

  put : ∀{s} → s → ST s Unit
  put s = record { run = λ _ → (unit , s) }

  instance
    MonadState : ∀{s} → Monad (ST s)
    MonadState = record
      { return = λ a → record { run = λ s → a , s }
      ; _>>=_  = λ x f → record { run =
                 λ s → let y = ST.run x s
                       in ST.run (f (p1 y)) (p2 y)
                }
      }

  -- Universe Polymorphic version of the state monad.
  record STₐ {a b}(s : Set a)(o : Set b) : Set (a ⊔ b) where
    field run : s → (o × s)

  evalSTₐ : ∀{a b}{s : Set a}{o : Set b} → STₐ s o → s → o
  evalSTₐ s = p1 ∘ (STₐ.run s)

  getₐ : ∀{a}{s : Set a} → STₐ s s
  getₐ = record { run = λ s → (s , s) }

  putₐ : ∀{a}{s : Set a} → s → STₐ s Unit
  putₐ s = record { run = λ _ → (unit , s) }

  instance
    MonadStateₐ : ∀{a b}{s : Set a} → Monad {a ⊔ b} (STₐ s)
    MonadStateₐ = record
      { return = λ x → record { run = λ s → x , s }
      ; _>>=_  = λ x f → record { run =
                 λ s → let y = STₐ.run x s
                       in STₐ.run (f (p1 y)) (p2 y)
                }
      }

  -------------
  -- Fresh ℕ --
  -------------

  Freshℕ : Set → Set
  Freshℕ A = ST ℕ A

  runFresh : ∀{A} → Freshℕ A → A
  runFresh f = evalST f 0

  runFresh-n : ∀{A} → Freshℕ A → ℕ → A
  runFresh-n = evalST

  inc : Freshℕ Unit
  inc = get >>= (put ∘ suc)

  ----------------
  -- List Monad --
  ----------------

  NonDet : ∀{a} → Set a → Set a
  NonDet A = List A

  NonDetBind : ∀{a}{A B : Set a} → NonDet A → (A → NonDet B) → NonDet B
  NonDetBind x f = concat (map f x)

  NonDetRet : ∀{a}{A : Set a} → A → NonDet A
  NonDetRet x = x ∷ []

  instance
    MonadNonDet : Monad {lz} NonDet
    MonadNonDet = record
      { return = NonDetRet
      ; _>>=_  = NonDetBind
      }

  ------------------
  -- Reader Monad --
  ------------------

  Reader : ∀{a b} → Set a → Set b → Set (a ⊔ b)
  Reader R A = R → A

  reader-bind : ∀{a b}{R : Set a}{A B : Set b}
              → Reader R A → (A → Reader R B) → Reader R B
  reader-bind ra rb = λ r → rb (ra r) r

  reader-return : ∀{a b}{R : Set a}{A : Set b}
                → A → Reader R A
  reader-return a = λ _ → a

  reader-local : ∀{a b}{R : Set a}{A : Set b}
               → (R → R) → Reader R A → Reader R A
  reader-local f ra = ra ∘ f

  reader-ask : ∀{a}{R : Set a} → Reader R R
  reader-ask = id

  instance
    MonadReader : ∀{a b}{R : Set a} → Monad {b ⊔ a} (Reader {b = b ⊔ a} R)
    MonadReader = record
      { return = reader-return
      ; _>>=_  = reader-bind
      }

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
module FStream.FVec where

------------------------------------------------------------------------
-- Dissecting effectful streams
------------------------------------------------------------------------

open import Library
open import FStream.Core
open import Data.Fin

infixr 5 _▻_
infix 6 ⟨_▻⋯
infix 7 _⟩

data FVec {ℓ₁ ℓ₂} (C : Container ℓ₁) (A : Set ℓ₂) : (n : ℕ) → Set (ℓ₁ ⊔ ℓ₂) where
  FNil : FVec C A 0
  FCons : ∀ {n} → ⟦ C ⟧ (A × FVec C A n) → FVec C A (suc n)

-- TODO Syntactic sugar for these as well
data FVec' {ℓ₁ ℓ₂} (C : Container ℓ₁) (A : Set ℓ₂) : (n : ℕ) → Set (ℓ₁ ⊔ ℓ₂) where
  FNil' : FVec' C A 0
  FCons' : ∀ {n} → A → ⟦ C ⟧ (FVec' C A n) → FVec' C A (suc n)

_▻'_ : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {n} →
  A → ⟦ C ⟧ (FVec' C A n) → FVec' C A (suc n)
_▻'_ = FCons'

fVec'ToFVec : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {n} →
  FVec' C A n → FVec C A n
fVec'ToFVec FNil' = FNil
fVec'ToFVec (FCons' a v) = FCons (fmap (λ x → a , fVec'ToFVec x) v)

nest : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {n} →
  Vec (⟦ C ⟧ A) n → FVec C A n
nest [] = FNil
nest (a ∷ as) = FCons (fmap (_, nest as) a)

_▻_ :  ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {n} →
  ⟦ C ⟧ A → (FVec C A n) → FVec C A (suc n)
a ▻ v = FCons (fmap (λ x → x , v) a)

_⟩ : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} → ⟦ C ⟧ A → FVec C A 1
a ⟩ = a ▻ FNil

mutual
  vmap : ∀ {ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂} {B : Set ℓ₃} {n} →
    (f : A → B) → FVec C A n → FVec C B n
  vmap _ FNil = FNil
  vmap f (FCons x) = FCons (fmap (vmap' f) x)

  vmap' : ∀ {ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂} {B : Set ℓ₃} {n} →
    (f : A → B) → A × FVec C A n → B × FVec C B n
  vmap' f (a , v) = f a , vmap f v

mutual
  take : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} →
    (n : ℕ) → FStream C A → FVec C A n
  take ℕ.zero as = FNil
  take (ℕ.suc n) as = FCons (fmap (take' n) (inF as))

  take' : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} →
    (n : ℕ) → FStream' C A → A × FVec C A n
  proj₁ (take' n as) = head as
  proj₂ (take' n as) = take n (tail as)

take'' : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} →
  (n : ℕ) → FStream' C A → FVec' C A n
take'' zero as = FNil'
take'' (suc n) as = FCons' (head as) (fmap (take'' n) (inF (tail as)))

_pre⟨_▻⋯' : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {m n}
     → FVec' C A m → FVec' C A (suc n) → FStream' {i} C A
head (FNil' pre⟨ FCons' a _ ▻⋯') = a
inF (tail (FNil' pre⟨ FCons' a v ▻⋯')) = fmap (_pre⟨ (FCons' a v) ▻⋯') v
head (FCons' x _ pre⟨ v' ▻⋯') = x
inF (tail (FCons' _ v pre⟨ v' ▻⋯')) = fmap (_pre⟨ v' ▻⋯') v

⟨_▻⋯' : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {n : ℕ}
     → FVec' C A (suc n) → FStream' {i} C A
⟨ v ▻⋯' = FNil' pre⟨ v ▻⋯'

mutual
  _pre⟨_▻⋯ : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {m n}
       → FVec C A m → FVec C A (suc n) → FStream {i} C A
  inF (FCons x pre⟨ keep ▻⋯) = fmap (_aux keep) x
  inF (FNil pre⟨ FCons x ▻⋯) = fmap (_aux (FCons x)) x
  _aux_ : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {n m : ℕ}
    → A × FVec C A m → FVec C A (suc n) → FStream' {i} C A
  head ((a , _ ) aux v) = a
  tail ((_ , v') aux v) = v' pre⟨ v ▻⋯

⟨_▻⋯ : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {A : Set ℓ₂} {n : ℕ}
     → FVec C A (suc n) → FStream {i} C A
⟨ as ▻⋯ = FNil pre⟨ as ▻⋯

data _[_]=_ {a} {A : Set a} {ℓ} {C : Container ℓ} : {n : ℕ} → FVec C A n → Fin n → ⟦ C ⟧ A → Set (a ⊔ ℓ) where
  here : ∀ {n} {x : ⟦ C ⟧ A} {xs : FVec C A n} → (x ▻ xs) [ zero ]= x
  there : ∀ {n} {k} {x y} {xs : FVec C A n} → xs [ k ]= x → (y ▻ xs) [ suc k ]= x

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Integers
------------------------------------------------------------------------

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

module Data.Integer where

import Data.Nat.Show as ℕ
open import Data.Sign as Sign using (Sign)
open import Data.String.Base using (String; _++_)

------------------------------------------------------------------------
-- Integers, basic types and operations

open import Data.Integer.Base public

------------------------------------------------------------------------
-- Re-export queries from the properties modules

open import Data.Integer.Properties public
  using (_≟_; _≤?_)

------------------------------------------------------------------------
-- Conversions

show : ℤ → String
show i = showSign (sign i) ++ ℕ.show ∣ i ∣
  where
  showSign : Sign → String
  showSign Sign.- = "-"
  showSign Sign.+ = ""

------------------------------------------------------------------------
-- Deprecated

-- Version 0.17

open import Data.Integer.Properties public
  using (◃-cong; drop‿+≤+; drop‿-≤-)
  renaming (◃-inverse to ◃-left-inverse)


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

open import LogicalFormulae
open import Lists.Lists
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.BinaryNaturals.Definition
open import Semirings.Definition
open import Orders.Total.Definition

module Numbers.BinaryNaturals.Addition where

-- Define the monoid structure, and show that it's the same as ℕ's

_+Binherit_ : BinNat → BinNat → BinNat
a +Binherit b = NToBinNat (binNatToN a +N binNatToN b)

_+B_ : BinNat → BinNat → BinNat
[] +B b = b
(x :: a) +B [] = x :: a
(zero :: xs) +B (y :: ys) = y :: (xs +B ys)
(one :: xs) +B (zero :: ys) = one :: (xs +B ys)
(one :: xs) +B (one :: ys) = zero :: incr (xs +B ys)

+BCommutative : (a b : BinNat) → a +B b ≡ b +B a
+BCommutative [] [] = refl
+BCommutative [] (x :: b) = refl
+BCommutative (x :: a) [] = refl
+BCommutative (zero :: as) (zero :: bs) rewrite +BCommutative as bs = refl
+BCommutative (zero :: as) (one :: bs) rewrite +BCommutative as bs = refl
+BCommutative (one :: as) (zero :: bs) rewrite +BCommutative as bs = refl
+BCommutative (one :: as) (one :: bs) rewrite +BCommutative as bs = refl

private
  +BIsInherited[] : (b : BinNat) (prB : b ≡ canonical b) → [] +Binherit b ≡ [] +B b
  +BIsInherited[] [] prB = refl
  +BIsInherited[] (zero :: b) prB = t
    where
      refine : (b : BinNat) → zero :: b ≡ canonical (zero :: b) → b ≡ canonical b
      refine b pr with canonical b
      refine b pr | x :: bl = ::Inj pr
      t : NToBinNat (0 +N binNatToN (zero :: b)) ≡ zero :: b
      t with TotalOrder.totality ℕTotalOrder 0 (binNatToN b)
      t | inl (inl pos) = transitivity (doubleIsBitShift (binNatToN b) pos) (applyEquality (zero ::_) (transitivity (binToBin b) (equalityCommutative (refine b prB))))
      t | inl (inr ())
      ... | inr eq with binNatToNZero b (equalityCommutative eq)
      ... | u with canonical b
      t | inr eq | u | [] = exFalso (bad b prB)
        where
          bad : (c : BinNat) → zero :: c ≡ [] → False
          bad c ()
      t | inr eq | () | x :: bl
  +BIsInherited[] (one :: b) prB = ans
    where
      ans : NToBinNat (binNatToN (one :: b)) ≡ one :: b
      ans = transitivity (binToBin (one :: b)) (equalityCommutative prB)

-- Show that the monoid structure of ℕ is the same as that of BinNat

+BIsInherited : (a b : BinNat) (prA : a ≡ canonical a) (prB : b ≡ canonical b) → a +Binherit b ≡ a +B b
+BinheritLemma : (a : BinNat) (b : BinNat) (prA : a ≡ canonical a) (prB : b ≡ canonical b) → incr (NToBinNat ((binNatToN a +N binNatToN b) +N ((binNatToN a +N binNatToN b) +N zero))) ≡ one :: (a +B b)

+BIsInherited' : (a b : BinNat) → a +Binherit b ≡ canonical (a +B b)

+BinheritLemma a b prA prB with TotalOrder.totality ℕTotalOrder 0 (binNatToN a +N binNatToN b)
+BinheritLemma a b prA prB | inl (inl x) rewrite doubleIsBitShift (binNatToN a +N binNatToN b) x = applyEquality (one ::_) (+BIsInherited a b prA prB)
+BinheritLemma a b prA prB | inr x with sumZeroImpliesSummandsZero (equalityCommutative x)
+BinheritLemma a b prA prB | inr x | fst ,, snd = ans2
  where
    bad : b ≡ []
    bad = transitivity prB (binNatToNZero b snd)
    bad2 : a ≡ []
    bad2 = transitivity prA (binNatToNZero a fst)
    ans2 : incr (NToBinNat ((binNatToN a +N binNatToN b) +N ((binNatToN a +N binNatToN b) +N zero))) ≡ one :: (a +B b)
    ans2 rewrite bad | bad2 = refl

+BIsInherited [] b _ prB = +BIsInherited[] b prB
+BIsInherited (x :: a) [] prA _ = transitivity (applyEquality NToBinNat (Semiring.commutative ℕSemiring (binNatToN (x :: a)) 0)) (transitivity (binToBin (x :: a)) (equalityCommutative prA))
+BIsInherited (zero :: as) (zero :: b) prA prB with TotalOrder.totality ℕTotalOrder 0 (binNatToN as +N binNatToN b)
... | inl (inl 0<) rewrite Semiring.commutative ℕSemiring (binNatToN as) 0 | Semiring.commutative ℕSemiring (binNatToN b) 0 | Semiring.+Associative ℕSemiring (binNatToN as +N binNatToN as) (binNatToN b) (binNatToN b) | equalityCommutative (Semiring.+Associative ℕSemiring (binNatToN as) (binNatToN as) (binNatToN b)) | Semiring.commutative ℕSemiring (binNatToN as) (binNatToN b) | Semiring.+Associative ℕSemiring (binNatToN as) (binNatToN b) (binNatToN as) | equalityCommutative (Semiring.+Associative ℕSemiring (binNatToN as +N binNatToN b) (binNatToN as) (binNatToN b)) | Semiring.commutative ℕSemiring 0 ((binNatToN as +N binNatToN b) +N (binNatToN as +N binNatToN b)) | equalityCommutative (Semiring.+Associative ℕSemiring (binNatToN as +N binNatToN b) (binNatToN as +N binNatToN b) 0) = transitivity (doubleIsBitShift (binNatToN as +N binNatToN b) (identityOfIndiscernablesRight _<N_ 0< (Semiring.commutative ℕSemiring (binNatToN b) _))) (applyEquality (zero ::_) (+BIsInherited as b (canonicalDescends as prA) (canonicalDescends b prB)))
+BIsInherited (zero :: as) (zero :: b) prA prB | inl (inr ())
... | inr p with sumZeroImpliesSummandsZero {binNatToN as} (equalityCommutative p)
+BIsInherited (zero :: as) (zero :: b) prA prB | inr p | as=0 ,, b=0 rewrite as=0 | b=0 = exFalso ans
  where
    bad : (b : BinNat) → (pr : b ≡ canonical b) → (pr2 : binNatToN b ≡ 0) → b ≡ []
    bad b pr pr2 = transitivity pr (binNatToNZero b pr2)
    t : b ≡ canonical b
    t with canonical b
    t | x :: bl = ::Inj prB
    u : b ≡ []
    u = bad b t b=0
    nono : {A : Set} → {a : A} → {as : List A} → a :: as ≡ [] → False
    nono ()
    ans : False
    ans with inspect (canonical b)
    ans | [] with≡ x rewrite x = nono prB
    ans | (x₁ :: y) with≡ x = nono (transitivity (equalityCommutative x) (transitivity (equalityCommutative t) u))
+BIsInherited (zero :: as) (one :: b) prA prB rewrite Semiring.commutative ℕSemiring (binNatToN as +N (binNatToN as +N zero)) (succ (binNatToN b +N (binNatToN b +N zero))) | Semiring.commutative ℕSemiring (binNatToN b +N (binNatToN b +N zero)) (binNatToN as +N (binNatToN as +N zero)) | equalityCommutative (Semiring.+DistributesOver* ℕSemiring 2 (binNatToN as) (binNatToN b)) = +BinheritLemma as b (canonicalDescends as prA) (canonicalDescends b prB)
+BIsInherited (one :: as) (zero :: bs) prA prB rewrite equalityCommutative (Semiring.+DistributesOver* ℕSemiring 2 (binNatToN as) (binNatToN bs)) = +BinheritLemma as bs (canonicalDescends as prA) (canonicalDescends bs prB)
+BIsInherited (one :: as) (one :: bs) prA prB rewrite Semiring.commutative ℕSemiring (binNatToN as +N (binNatToN as +N zero)) (succ (binNatToN bs +N (binNatToN bs +N zero))) | Semiring.commutative ℕSemiring (binNatToN bs +N (binNatToN bs +N zero)) (2 *N binNatToN as) | equalityCommutative (Semiring.+DistributesOver* ℕSemiring 2 (binNatToN as) (binNatToN bs)) | +BinheritLemma as bs (canonicalDescends as prA) (canonicalDescends bs prB) = refl

+BIsInherited'[] : (b : BinNat) → [] +Binherit b ≡ canonical ([] +B b)
+BIsInherited'[] [] = refl
+BIsInherited'[] (zero :: b) with inspect (canonical b)
+BIsInherited'[] (zero :: b) | [] with≡ pr rewrite binNatToNZero' b pr | pr = refl
+BIsInherited'[] (zero :: b) | (x :: bl) with≡ pr rewrite pr = ans
  where
    contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
    contr {l1 = []} p1 ()
    contr {l1 = x :: l1} () p2
    ans : NToBinNat (binNatToN b +N (binNatToN b +N zero)) ≡ zero :: x :: bl
    ans with inspect (binNatToN b)
    ans | zero with≡ th rewrite th = exFalso (contr (binNatToNZero b th) pr)
    ans | succ th with≡ blah rewrite blah | doubleIsBitShift' th = applyEquality (zero ::_) (transitivity (equalityCommutative u) pr)
      where
        u : canonical b ≡ incr (NToBinNat th)
        u = transitivity (equalityCommutative (binToBin b)) (applyEquality NToBinNat blah)
+BIsInherited'[] (one :: b) with inspect (binNatToN b)
... | zero with≡ pr rewrite pr = applyEquality (one ::_) (equalityCommutative (binNatToNZero b pr))
... | (succ bl) with≡ pr = ans
  where
    u : NToBinNat (2 *N binNatToN b) ≡ zero :: canonical b
    u with doubleIsBitShift' bl
    ... | t = transitivity (identityOfIndiscernablesLeft _≡_ t (applyEquality (λ i → NToBinNat (2 *N i)) (equalityCommutative pr))) (applyEquality (zero ::_) (transitivity (applyEquality NToBinNat (equalityCommutative pr)) (binToBin b)))
    ans : incr (NToBinNat (binNatToN b +N (binNatToN b +N zero))) ≡ one :: canonical b
    ans = applyEquality incr u

+BIsInherited' [] b = +BIsInherited'[] b
+BIsInherited' (zero :: a) [] with inspect (binNatToN a)
+BIsInherited' (zero :: a) [] | zero with≡ x rewrite x | binNatToNZero a x = refl
+BIsInherited' (zero :: a) [] | succ y with≡ x rewrite x | Semiring.commutative ℕSemiring (y +N succ (y +N 0)) 0 = transitivity (doubleIsBitShift' y) (transitivity (applyEquality (λ i → (zero :: NToBinNat i)) (equalityCommutative x)) (transitivity (applyEquality (λ i → zero :: i) (binToBin a)) (canonicalAscends' {zero} a bad)))
  where
    bad : canonical a ≡ [] → False
    bad pr with transitivity (equalityCommutative x) (transitivity (equalityCommutative (binNatToNIsCanonical a)) (applyEquality binNatToN pr))
    bad pr | ()
+BIsInherited' (one :: a) [] with inspect (binNatToN a)
+BIsInherited' (one :: a) [] | 0 with≡ x rewrite x | binNatToNZero a x = refl
+BIsInherited' (one :: a) [] | succ n with≡ x rewrite x | doubleIsBitShift' n = applyEquality incr {_} {zero :: canonical a} (transitivity {x = _} {NToBinNat (2 *N succ n)} bl (transitivity (doubleIsBitShift' n) (applyEquality (zero ::_) (transitivity (applyEquality NToBinNat (equalityCommutative x)) (binToBin a)))))
  where
    bl : incr (NToBinNat ((n +N succ (n +N 0)) +N 0)) ≡ NToBinNat (succ (n +N succ (n +N 0)))
    bl rewrite equalityCommutative x | Semiring.commutative ℕSemiring (n +N succ (n +N 0)) 0 = refl
+BIsInherited' (zero :: as) (zero :: bs) rewrite equalityCommutative (Semiring.+DistributesOver* ℕSemiring 2 (binNatToN as) (binNatToN bs)) = ans
  where
    ans : NToBinNat (2 *N (binNatToN as +N binNatToN bs)) ≡ canonical (zero :: (as +B bs))
    ans with inspect (binNatToN as +N binNatToN bs)
    ans | zero with≡ x with sumZeroImpliesSummandsZero {binNatToN as} x
    ... | as=0 ,, bs=0 rewrite as=0 | bs=0 = foo
      where
        u : canonical (as +Binherit bs) ≡ []
        u rewrite as=0 | bs=0 = refl
        foo : [] ≡ canonical (zero :: (as +B bs))
        foo = transitivity (transitivity b (applyEquality (λ i → canonical (zero :: i)) (+BIsInherited' as bs))) (canonicalAscends'' {zero} (as +B bs))
          where
            b : [] ≡ canonical (zero :: (as +Binherit bs))
            b rewrite u = refl
    ans | succ y with≡ x rewrite x | doubleIsBitShift' y = transitivity (applyEquality (λ i → zero :: NToBinNat i) (equalityCommutative x)) ans2
      where
        u : 0 <N binNatToN (as +B bs)
        u rewrite equalityCommutative (binNatToNIsCanonical (as +B bs)) | equalityCommutative (+BIsInherited' as bs) | x | nToN (succ y) = succIsPositive y
        ans2 : zero :: NToBinNat (binNatToN as +N binNatToN bs) ≡ canonical (zero :: (as +B bs))
        ans2 rewrite +BIsInherited' as bs = canonicalAscends (as +B bs) u
+BIsInherited' (zero :: as) (one :: bs) rewrite Semiring.commutative ℕSemiring (2 *N binNatToN as) (succ (2 *N binNatToN bs)) | Semiring.commutative ℕSemiring (2 *N binNatToN bs) (2 *N binNatToN as) | equalityCommutative (Semiring.+DistributesOver* ℕSemiring 2 (binNatToN as) (binNatToN bs)) = ans2
  where
    ans2 : incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs))) ≡ one :: canonical (as +B bs)
    ans2 with inspect (binNatToN as +N binNatToN bs)
    ans2 | zero with≡ x with sumZeroImpliesSummandsZero {binNatToN as} x
    ans2 | zero with≡ x | as=0 ,, bs=0 rewrite as=0 | bs=0 = applyEquality (one ::_) (transitivity t (+BIsInherited' as bs))
      where
        t : [] ≡ as +Binherit bs
        t rewrite as=0 | bs=0 = refl
    ans2 | succ y with≡ x rewrite x | doubleIsBitShift' y = applyEquality (one ::_) (transitivity (applyEquality NToBinNat (equalityCommutative x)) (+BIsInherited' as bs))
+BIsInherited' (one :: as) (zero :: bs) rewrite equalityCommutative (Semiring.+DistributesOver* ℕSemiring 2 (binNatToN as) (binNatToN bs)) = ans
  where
    ans : incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs))) ≡ one :: canonical (as +B bs)
    ans with inspect (binNatToN as +N binNatToN bs)
    ans | zero with≡ x with sumZeroImpliesSummandsZero {binNatToN as} x
    ... | as=0 ,, bs=0 rewrite as=0 | bs=0 = applyEquality (one ::_) (transitivity t (+BIsInherited' as bs))
      where
        t : [] ≡ NToBinNat (binNatToN as +N binNatToN bs)
        t rewrite as=0 | bs=0 = refl
    ans | succ y with≡ x rewrite x | doubleIsBitShift' y = applyEquality (one ::_) (transitivity (applyEquality NToBinNat (equalityCommutative x)) (+BIsInherited' as bs))
+BIsInherited' (one :: as) (one :: bs) rewrite Semiring.commutative ℕSemiring (2 *N binNatToN as) (succ (2 *N binNatToN bs)) | Semiring.commutative ℕSemiring (2 *N binNatToN bs) (2 *N binNatToN as) | equalityCommutative (Semiring.+DistributesOver* ℕSemiring 2 (binNatToN as) (binNatToN bs)) = ans
  where
    ans : incr (incr (NToBinNat (2 *N (binNatToN as +N binNatToN bs)))) ≡ canonical (zero :: incr (as +B bs))
    ans with inspect (binNatToN as +N binNatToN bs)
    ... | zero with≡ x with sumZeroImpliesSummandsZero {binNatToN as} x
    ans | zero with≡ x | as=0 ,, bs=0 rewrite as=0 | bs=0 = bar
      where
        u' : canonical (as +Binherit bs) ≡ []
        u' rewrite as=0 | bs=0 = refl
        u : canonical (as +B bs) ≡ []
        u rewrite equalityCommutative (+BIsInherited' as bs) = transitivity (NToBinNatIsCanonical (binNatToN as +N binNatToN bs)) u'
        t : canonical (incr (as +B bs)) ≡ one :: []
        t rewrite incrPreservesCanonical' (as +B bs) | u = refl
        bar : zero :: one :: [] ≡ canonical (zero :: incr (as +B bs))
        bar rewrite t = refl
    ans | succ y with≡ x rewrite x | doubleIsBitShift' y = transitivity (applyEquality (λ i → zero :: incr (NToBinNat i)) (equalityCommutative x)) ans2
      where
        ans2 : zero :: incr (as +Binherit bs) ≡ canonical (zero :: incr (as +B bs))
        ans2 rewrite +BIsInherited' as bs | equalityCommutative (incrPreservesCanonical' (as +B bs)) | canonicalAscends' {zero} (incr (as +B bs)) (incrNonzero (as +B bs)) = refl

+BIsHom : (a b : BinNat) → binNatToN (a +B b) ≡ (binNatToN a) +N (binNatToN b)
+BIsHom a b = transitivity (equalityCommutative (binNatToNIsCanonical (a +B b))) (transitivity (equalityCommutative (applyEquality binNatToN (+BIsInherited' a b))) (nToN _))

sumCanonical : (a b : BinNat) → canonical a ≡ a → canonical b ≡ b → canonical (a +B b) ≡ a +B b
sumCanonical a b a=a b=b = transitivity (equalityCommutative (+BIsInherited' a b)) (+BIsInherited a b (equalityCommutative a=a) (equalityCommutative b=b))


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

open import Level
open import Data.Quiver using (Quiver)

-- The Category of (free) paths over a Quiver
module Categories.Category.Construction.PathCategory {o ℓ e} (G : Quiver o ℓ e) where

open import Function.Base using (_$_)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties hiding (trans)
open import Data.Quiver.Paths

open import Categories.Category.Core using (Category)

open Quiver G
private module P = Paths G
open P

PathCategory : Category o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)
PathCategory = record
  { Obj       = Obj
  ; _⇒_       = Star _⇒_
  ; _≈_       = _≈*_
  ; id        = ε
  ; _∘_       = _▻▻_
  ; assoc     = λ {_ _ _ _} {f g h} → sym $ ≡⇒≈* $ ◅◅-assoc f g h
  ; sym-assoc = λ {_ _ _ _} {f g h} → ≡⇒≈* $ ◅◅-assoc f g h
  ; identityˡ = λ {_ _ f} → ◅◅-identityʳ f
  ; identityʳ = refl
  ; identity² = refl
  ; equiv     = isEquivalence
  ; ∘-resp-≈  = resp
  }
  where
  resp : ∀ {A B C} {f h : Star _⇒_ B C} {g i : Star _⇒_ A B} →
           f ≈* h → g ≈* i → (f ▻▻ g) ≈* (h ▻▻ i)
  resp eq ε = eq
  resp eq (eq₁ ◅ eq₂) = eq₁ ◅ (resp eq eq₂)


text:
-- Andreas, 2019-02-03, issue #3541:
-- Treat indices like parameters in positivity check.

data Works (A : Set) : Set where
  nest : Works (Works A) → Works A

data Foo : Set → Set where
  foo : ∀{A} → Foo (Foo A) → Foo A

-- Should pass.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


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

open import Categories.Category.Core
open import Categories.Object.Terminal hiding (up-to-iso)

module Categories.Object.NaturalNumber {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Terminal : Terminal 𝒞) where

open import Level

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open HomReasoning
open Equiv

open Terminal 𝒞-Terminal

private
  variable
    A B C D X Y Z : Obj
    h i j : A ⇒ B

record IsNaturalNumber (N : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    z : ⊤ ⇒ N
    s : N ⇒ N
    universal : ∀ {A} → ⊤ ⇒ A → A ⇒ A → N ⇒ A
    z-commute : ∀ {A} {q : ⊤ ⇒ A} {f : A ⇒ A} → q ≈ universal q f ∘ z
    s-commute : ∀ {A} {q : ⊤ ⇒ A} {f : A ⇒ A} → f ∘ universal q f ≈ universal q f ∘ s
    unique    : ∀ {A} {q : ⊤ ⇒ A} {f : A ⇒ A} {u : N ⇒ A} → q ≈ u ∘ z → f ∘ u ≈ u ∘ s → u ≈ universal q f

  η : universal z s ≈ id
  η = ⟺ (unique (⟺ identityˡ) id-comm)

  universal-cong : ∀ {A} → {f f′ : ⊤ ⇒ A} → {g g′ : A ⇒ A} → f ≈ f′ → g ≈ g′ → universal f g ≈ universal f′ g′
  universal-cong f≈f′ g≈g′ = unique (⟺ f≈f′ ○  z-commute) (∘-resp-≈ˡ (⟺ g≈g′) ○ s-commute)

record NaturalNumber : Set (o ⊔ ℓ ⊔ e) where
  field
    N : Obj
    isNaturalNumber : IsNaturalNumber N

  open IsNaturalNumber isNaturalNumber public

open NaturalNumber

module _ (N : NaturalNumber) (N′ : NaturalNumber) where
  private
    module N = NaturalNumber N
    module N′ = NaturalNumber N′

  up-to-iso : N.N ≅ N′.N
  up-to-iso = record
    { from = N.universal N′.z N′.s
    ; to = N′.universal N.z N.s
    ; iso = record
      { isoˡ = universal-∘ N N′
      ; isoʳ = universal-∘ N′ N
      }
    }
    where
      universal-∘ : ∀ (N N′ : NaturalNumber) → universal N′ (z N) (s N) ∘ universal N (z N′) (s N′) ≈ id
      universal-∘ N N′ = unique N (z-commute N′ ○ pushʳ (z-commute N)) (pullˡ (s-commute N′) ○ assoc ○ ∘-resp-≈ʳ (s-commute N) ○ ⟺ assoc) ○ (η N)


text:
-- A Beth model of normal forms

open import Library

module NfModelCaseTreeConv (Base : Set) where

import Formulas   ; open module Form = Formulas    Base
import Derivations; open module Der  = Derivations Base

-- Beth model

data Cover (P : Cxt → Set) (Γ : Cxt) : Set where
  returnC : (p : P Γ) → Cover P Γ
  falseC  : (t : Ne Γ False) → Cover P Γ
  orC     : ∀{C D} (t : Ne Γ (C ∨ D))
              (c : Cover P (Γ ∙ C))
              (d : Cover P (Γ ∙ D)) → Cover P Γ

-- Syntactic paste

pasteNf : ∀{A} → Cover (Nf' A) →̇ Nf' A
pasteNf (returnC p) = p
pasteNf (falseC t)  = falseE t
pasteNf (orC t c d) = orE t (pasteNf c) (pasteNf d)

-- Weakening covers:  A case tree in Γ can be transported to a thinning Δ
-- by weakening all the scrutinees.

monC : ∀{P} → (monP : Mon P) → Mon (Cover P)
monC monP τ (returnC p) = returnC (monP τ p)
monC monP τ (falseC t)  = falseC (monNe τ t)
monC monP τ (orC t c d) = orC (monNe τ t) (monC monP (lift τ) c)
                                          (monC monP (lift τ) d)

-- Monad

mapC : ∀{P Q} → (P →̇ Q) → (Cover P →̇ Cover Q)
mapC f (returnC p) = returnC (f p)
mapC f (falseC t)  = falseC t
mapC f (orC t c d) = orC t (mapC f c) (mapC f d)

joinC : ∀{P} → Cover (Cover P) →̇ Cover P
joinC (returnC p) = p
joinC (falseC t)  = falseC t
joinC (orC t c d) = orC t (joinC c) (joinC d)

-- Version of mapC with f relativized to subcontexts of Γ

mapC' : ∀{P Q Γ} → KFun P Q Γ → Cover P Γ → Cover Q Γ
mapC' f (returnC p) = returnC (f id≤ p)
mapC' f (falseC t)  = falseC t
mapC' f (orC t c d) = orC t (mapC' (λ τ → f (τ • weak id≤)) c)
                            (mapC' (λ τ → f (τ • weak id≤)) d)

Conv : (Δ₀ : Cxt) (P Q : Cxt → Set) → Set
Conv Δ₀ P Q = ∀{Γ Δ} (δ : Δ ≤ Δ₀) (τ : Δ ≤ Γ) → P Γ → Q Δ

convC : ∀{Δ₀} {P Q}
  → Conv Δ₀ P Q
  → Conv Δ₀ (Cover P) (Cover Q)
convC {Δ₀} {P} {Q} f {Γ} {Δ} δ τ (returnC p) = returnC (f δ τ p)
convC {Δ₀} {P} {Q} f {Γ} {Δ} δ τ (falseC t) = falseC (monNe τ t)
convC {Δ₀} {P} {Q} f {Γ} {Δ} δ τ (orC t c d) = orC (monNe τ t)
  (convC {Δ₀} f (weak δ) (lift τ) c)
  (convC {Δ₀} f (weak δ) (lift τ) d)

-- The syntactic Beth model.

-- We interpret base propositions  Atom P  by their normal deriviations.
-- ("Normal" is important; "neutral is not sufficient since we need case trees here.)

-- The negative connectives True, ∧, and ⇒ are explained as usual by η-expansion
-- and the meta-level connective.

-- The positive connectives False and ∨ are inhabited by case trees.
-- In case False, the tree has no leaves.
-- In case A ∨ B, each leaf must be in the semantics of either A or B.

T⟦_⟧ : (A : Form) (Γ : Cxt) → Set
T⟦ Atom P ⟧ = Nf' (Atom P)
T⟦ True   ⟧ Γ = ⊤
T⟦ False  ⟧ = Cover λ Δ → ⊥
T⟦ A ∨ B  ⟧ = Cover λ Δ → T⟦ A ⟧ Δ ⊎ T⟦ B ⟧ Δ
T⟦ A ∧ B  ⟧ Γ = T⟦ A ⟧ Γ × T⟦ B ⟧ Γ
T⟦ A ⇒ B  ⟧ Γ = ∀{Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Δ → T⟦ B ⟧ Δ

-- Monotonicity of the model is proven by induction on the proposition,
-- using monotonicity of covers and the built-in monotonicity at implication.

-- monT : ∀ A {Γ Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Γ → T⟦ A ⟧ Δ

monT : ∀ A → Mon T⟦ A ⟧
monT (Atom P) = monNf
monT True     = _
monT False    = monC λ τ ()
monT (A ∨ B)  = monC λ τ → map-⊎ (monT A τ) (monT B τ)
monT (A ∧ B) τ (a , b) = monT A τ a , monT B τ b
monT (A ⇒ B) τ f σ = f (σ • τ)

-- Reflection / reification, proven simultaneously by induction on the proposition.

-- Reflection is η-expansion (and recursively reflection);
-- at positive connections we build a case tree with a single scrutinee: the neutral
-- we are reflecting.

-- At implication, we need reification, which produces introductions
-- and reifies the stored case trees.

mutual

  fresh : ∀ {Γ} A → T⟦ A ⟧ (Γ ∙ A)
  fresh A = reflect A (hyp top)

  reflect : ∀ A → Ne' A →̇ T⟦ A ⟧
  reflect (Atom P) t = ne t
  reflect True     t = _
  reflect False    t = falseC t
  reflect (A ∨ B)  t = orC t (returnC (inj₁ (fresh A)))
                             (returnC (inj₂ (fresh B)))
  reflect (A ∧ B)  t = reflect A (andE₁ t) , reflect B (andE₂ t)
  reflect (A ⇒ B)  t τ a = reflect B (impE (monNe τ t) (reify A a))

  reify : ∀ A → T⟦ A ⟧ →̇ Nf' A
  reify (Atom P) t      = t
  reify True _          = trueI
  reify False           = pasteNf ∘  mapC ⊥-elim
  reify (A ∨ B)         = pasteNf ∘  mapC [ orI₁ ∘ reify A , orI₂ ∘ reify B ]
  reify (A ∧ B) (a , b) = andI (reify A a) (reify B b)
  reify (A ⇒ B) ⟦f⟧     = impI (reify B (⟦f⟧ (weak id≤) (fresh A)))

-- Semantic paste.

paste : ∀ A → Cover T⟦ A ⟧ →̇ T⟦ A ⟧
paste (Atom P) = pasteNf
paste True     = _
paste False    = joinC
paste (A ∨ B)  = joinC
paste (A ∧ B)  = < paste A ∘ mapC proj₁ , paste B ∘ mapC proj₂  >
paste (A ⇒ B) c τ a = paste B (convC (λ δ τ' f → f τ' (monT A δ a)) id≤ τ c)

-- Fundamental theorem
-- Extension of T⟦_⟧ to contexts

G⟦_⟧ : ∀ (Γ Δ : Cxt) → Set
G⟦ ε     ⟧ Δ = ⊤
G⟦ Γ ∙ A ⟧ Δ = G⟦ Γ ⟧ Δ × T⟦ A ⟧ Δ

-- monG : ∀{Γ Δ Φ} (τ : Φ ≤ Δ) → G⟦ Γ ⟧ Δ → G⟦ Γ ⟧ Φ

monG : ∀{Γ} → Mon G⟦ Γ ⟧
monG {ε} τ _ = _
monG {Γ ∙ A} τ (γ , a) = monG τ γ , monT A τ a

-- Variable case.

lookup : ∀{Γ A} (x : Hyp A Γ) → G⟦ Γ ⟧ →̇ T⟦ A ⟧
lookup top     = proj₂
lookup (pop x) = lookup x ∘ proj₁

-- A lemma for the orE case.

orElim : ∀ A B C {Γ} → T⟦ A ∨ B ⟧ Γ → T⟦ A ⇒ C ⟧ Γ → T⟦ B ⇒ C ⟧ Γ → T⟦ C ⟧ Γ
orElim A B C c g h = paste C (mapC' (λ τ → [ g τ , h τ ]) c)

-- A lemma for the falseE case.

-- Casts an empty cover into any semantic value (by contradiction).

falseElim : ∀ C → T⟦ False ⟧ →̇ T⟦ C ⟧
falseElim C = paste C ∘ mapC ⊥-elim

-- The fundamental theorem

eval :  ∀{A Γ} (t : Γ ⊢ A) → G⟦ Γ ⟧ →̇ T⟦ A ⟧
eval (hyp x)           = lookup x
eval (impI t)    γ τ a = eval t (monG τ γ , a)
eval (impE t u)  γ     = eval t γ id≤ (eval u γ)
eval (andI t u)  γ     = eval t γ , eval u γ
eval (andE₁ t)         = proj₁ ∘ eval t
eval (andE₂ t)         = proj₂ ∘ eval t
eval (orI₁ t)    γ     = returnC (inj₁ (eval t γ))
eval (orI₂ t)    γ     = returnC (inj₂ (eval t γ))
eval (orE {A = A} {B} {C} t u v) γ = orElim A B C (eval t γ)
  (λ τ a → eval u (monG τ γ , a))
  (λ τ b → eval v (monG τ γ , b))
eval {C} (falseE t) γ  = falseElim C (eval t γ)
eval trueI       γ     = _

-- Identity environment

ide : ∀ Γ → G⟦ Γ ⟧ Γ
ide ε = _
ide (Γ ∙ A) = monG (weak id≤) (ide Γ) , reflect A (hyp top)

-- Normalization

norm : ∀{A} → Tm A →̇ Nf' A
norm t = reify _ (eval t (ide _))

-- Q.E.D. -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
------------------------------------------------------------------------
-- Compatibility lemmas
------------------------------------------------------------------------

open import Atom

module Compatibility (atoms : χ-atoms) where

open import Bag-equivalence hiding (trans)
open import Equality.Propositional
open import Prelude hiding (const)
open import Tactic.By

open import List equality-with-J using (map)

open import Chi       atoms
open import Constants atoms
open import Reasoning atoms
open import Values    atoms

open χ-atoms atoms

-- A compatibility lemma that does not hold.

¬-⇓-[←]-right :
  ¬ (∀ {e′ v′} e x {v} →
     e′ ⇓ v′ → e [ x ← v′ ] ⇓ v → e [ x ← e′ ] ⇓ v)
¬-⇓-[←]-right hyp = ¬e[x←e′]⇓v (hyp e x e′⇓v′ e[x←v′]⇓v)
  where
  x : Var
  x = v-x

  e′ v′ e v : Exp
  e′ = apply (lambda v-x (var v-x)) (const c-true [])
  v′ = const c-true []
  e  = lambda v-y (var v-x)
  v  = lambda v-y (const c-true [])

  e′⇓v′ : e′ ⇓ v′
  e′⇓v′ = apply lambda (const [])
            (case v-x V.≟ v-x
             return (λ b → if b then const c-true []
                                else var v-x ⇓ v′) of (λ where
               (yes _)   → const []
               (no  x≢x) → ⊥-elim (x≢x refl)))

  lemma : ∀ v → e [ x ← v ] ≡ lambda v-y v
  lemma _ with v-x V.≟ v-y
  ... | yes x≡y = ⊥-elim (V.distinct-codes→distinct-names (λ ()) x≡y)
  ... | no  _   with v-x V.≟ v-x
  ...   | yes _   = refl
  ...   | no  x≢x = ⊥-elim (x≢x refl)

  e[x←v′]⇓v : e [ x ← v′ ] ⇓ v
  e[x←v′]⇓v =
    e [ x ← v′ ]   ≡⟨ lemma _ ⟩⟶
    lambda v-y v′  ⇓⟨ lambda ⟩■
    v

  ¬e[x←e′]⇓v : ¬ e [ x ← e′ ] ⇓ v
  ¬e[x←e′]⇓v p with _[_←_] e x e′ | lemma e′
  ¬e[x←e′]⇓v () | ._ | refl

mutual

  -- Contexts.

  data Context : Type where
    ∙       : Context
    apply←_ : Context → {e : Exp} → Context
    apply→_ : {e : Exp} → Context → Context
    const   : {c : Const} → Context⋆ → Context
    case    : Context → {bs : List Br} → Context

  data Context⋆ : Type where
    here  : Context → {es : List Exp} → Context⋆
    there : {e : Exp} → Context⋆ → Context⋆

mutual

  -- Filling a context's hole (∙) with an expression.

  infix 6 _[_] _[_]⋆

  _[_] : Context → Exp → Exp
  ∙                  [ e ] = e
  apply←_ c {e = e′} [ e ] = apply (c [ e ]) e′
  apply→_ {e = e′} c [ e ] = apply e′ (c [ e ])
  const {c = c′} c   [ e ] = const c′ (c [ e ]⋆)
  case c {bs = bs}   [ e ] = case (c [ e ]) bs

  _[_]⋆ : Context⋆ → Exp → List Exp
  here c {es = es} [ e ]⋆ = (c [ e ]) ∷ es
  there {e = e′} c [ e ]⋆ = e′ ∷ (c [ e ]⋆)

mutual

  -- If e₁ terminates with v₁ and c [ v₁ ] terminates with v₂, then
  -- c [ e₁ ] also terminates with v₂.

  []⇓ :
    ∀ c {e₁ v₁ v₂} →
    e₁ ⇓ v₁ → c [ v₁ ] ⇓ v₂ → c [ e₁ ] ⇓ v₂
  []⇓ ∙ {e₁} {v₁} {v₂} p q =
    e₁  ⇓⟨ p ⟩
    v₁  ⇓⟨ q ⟩■
    v₂

  []⇓ (apply← c) p (apply q r s)  = apply ([]⇓ c p q) r s
  []⇓ (apply→ c) p (apply q r s)  = apply q ([]⇓ c p r) s
  []⇓ (const c)  p (const ps)     = const ([]⇓⋆ c p ps)
  []⇓ (case c)   p (case q r s t) = case ([]⇓ c p q) r s t

  []⇓⋆ :
    ∀ c {e v vs} →
    e ⇓ v → c [ v ]⋆ ⇓⋆ vs → c [ e ]⋆ ⇓⋆ vs
  []⇓⋆ (here  c) p (q ∷ qs) = []⇓ c p q ∷ qs
  []⇓⋆ (there c) p (q ∷ qs) = q ∷ []⇓⋆ c p qs

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


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

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
{-# OPTIONS --allow-unsolved-metas #-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Hash
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS

open import LibraBFT.Abstract.Types

open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Handle sha256 sha256-cr

open import LibraBFT.Concrete.System.Parameters

open import LibraBFT.Yasm.Base
open import LibraBFT.Yasm.AvailableEpochs using (AvailableEpochs ; lookup'; lookup'')
open import LibraBFT.Yasm.System     ConcSysParms
open import LibraBFT.Yasm.Properties ConcSysParms

-- This module defines an abstract system state given a reachable
-- concrete system state.

-- An implementation must prove that, if one of its handlers sends a
-- message that contains a vote and is signed by a public key pk, then
-- either the vote's author is the peer executing the handler, the
-- epochId is in range, the peer is a member of the epoch, and its key
-- in that epoch is pk; or, a message with the same signature has been
-- sent before.  This is represented by StepPeerState-AllValidParts.
module LibraBFT.Concrete.System (sps-corr : StepPeerState-AllValidParts) where

 -- Bring in 'unwind', 'ext-unforgeability' and friends
 open Structural sps-corr

 -- TODO-1: refactor this somewhere else?  Maybe something like
 -- LibraBFT.Impl.Consensus.Types.Properties?
 sameHonestSig⇒sameVoteData : ∀ {v1 v2 : Vote} {pk}
                            → Meta-Honest-PK pk
                            → WithVerSig pk v1
                            → WithVerSig pk v2
                            → v1 ^∙ vSignature ≡ v2 ^∙ vSignature
                            → NonInjective-≡ sha256 ⊎ v2 ^∙ vVoteData ≡ v1 ^∙ vVoteData
 sameHonestSig⇒sameVoteData {v1} {v2} hpk wvs1 wvs2 refl
    with verify-bs-inj (verified wvs1) (verified wvs2)
      -- The signable fields of the votes must be the same (we do not model signature collisions)
 ...| bs≡
      -- Therefore the LedgerInfo is the same for the new vote as for the previous vote
      = sym <⊎$> (hashVote-inj1 {v1} {v2} (sameBS⇒sameHash bs≡))

 honestVoteProps : ∀ {e st} → ReachableSystemState {e} st → ∀ {pk nm v sender}
                    → Meta-Honest-PK pk
                    → v ⊂Msg nm
                    → (sender , nm) ∈ msgPool st
                    → WithVerSig pk v
                    → NonInjective-≡ sha256 ⊎ v ^∙ vEpoch < e
 honestVoteProps r hpk v⊂m m∈pool ver
   with honestPartValid r hpk v⊂m m∈pool ver
 ...| msg , valid
   =  ⊎-map id (λ { refl → vp-epoch valid })
               (sameHonestSig⇒sameVoteData hpk ver (msgSigned msg)
                                           (sym (msgSameSig msg)))

 -- We are now ready to define an 'AbsSystemState' view for a concrete
 -- reachable state.  We will do so by fixing an epoch that exists in
 -- the system, which will enable us to define the abstract
 -- properties. The culminaton of this 'PerEpoch' module is seen in
 -- the 'ConcSysState' "function" at the bottom, which probably the
 -- best place to start uynderstanding this.  Longer term, we will
 -- also need higher-level, cross-epoch properties.
 module PerState {e}(st : SystemState e)(r : ReachableSystemState st) where

  -- TODO-3: Remove this postulate when we are satisfied with the
  -- "hash-collision-tracking" solution. For example, when proving voo
  -- (in LibraBFT.LibraBFT.Concrete.Properties.VotesOnce), we
  -- currently use this postulate to eliminate the possibility of two
  -- votes that have the same signature but different VoteData
  -- whenever we use sameHonestSig⇒sameVoteData.  To eliminate the
  -- postulate, we need to refine the properties we prove to enable
  -- the possibility of a hash collision, in which case the required
  -- property might not hold.  However, it is not sufficient to simply
  -- prove that a hash collision *exists* (which is obvious,
  -- regardless of the LibraBFT implementation).  Rather, we
  -- ultimately need to produce a specific hash collision and relate
  -- it to the data in the system, so that we can prove that the
  -- desired properties hold *unless* an actual hash collision is
  -- found by the implementation given the data in the system.  In
  -- the meantime, we simply require that the collision identifies a
  -- reachable state; later "collision tracking" will require proof
  -- that the colliding values actually exist in that state.
  postulate  -- temporary
    meta-sha256-cr : ¬ (NonInjective-≡ sha256)

  module PerEpoch (eid : Fin e) where

   open import LibraBFT.Yasm.AvailableEpochs

   𝓔 : EpochConfig
   𝓔 = lookup' (availEpochs st) eid
   open EpochConfig

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

   -- * Auxiliary definitions;
   -- TODO-1: simplify and cleanup
   record QcPair  (q : Abs.QC) : Set where
     constructor mkQcPair
     field
       cqc    : QuorumCert
       isv    : IsValidQC 𝓔 cqc
       q≡αcqc : q ≡ α-QC (cqc , isv)
   open QcPair

   qc-α-Sent⇒ : ∀ {st q} → (Abs.Q q) α-Sent st
             → QcPair q
   qc-α-Sent⇒ (ws _ _ (qc∈NM {cqc} isv _ q≡)) = mkQcPair cqc isv q≡

   record ConcBits {q α} (va∈q : α Abs.∈QC q) (qcp : QcPair q) : Set where
     constructor mkConcBits
     field
       as     : Author × Signature
       as∈cqc : as ∈ qcVotes (cqc qcp)
       αVote≡ : Any-lookup va∈q ≡ α-Vote (cqc qcp) (isv qcp) as∈cqc
   open ConcBits

   qcp⇒concBits : ∀ {q α}
            → (qcp : QcPair q)
            → (va∈q : α Abs.∈QC q)
            → ConcBits va∈q qcp
   qcp⇒concBits qcp va∈q
     with All-reduce⁻ {vdq = Any-lookup va∈q} (α-Vote (cqc qcp) (isv qcp)) All-self
                       (subst (Any-lookup va∈q ∈_) (cong Abs.qVotes (q≡αcqc qcp)) (Any-lookup-correctP va∈q))
   ...| as , as∈cqc , α≡ = mkConcBits as as∈cqc α≡

   -- This record is highly duplicated; but it does provide a simple way to access
   -- all the properties from an /honest vote/
   record Vote∈QcProps {q} (qcp : QcPair q) {α} (α∈q : α Abs.∈QC q) : Set₁ where
     constructor mkV∈QcP
     field
       ev    : ConcreteVoteEvidence 𝓔 (Abs.∈QC-Vote q α∈q)
       as    : Author × Signature
       as∈qc : as ∈ qcVotes (cqc qcp)
       rbld  : ₋cveVote ev ≈Vote rebuildVote (cqc qcp) as

   vote∈QcProps : ∀ {q α st} → (αSent : Abs.Q q α-Sent st) → (α∈q : α Abs.∈QC q)
                → Vote∈QcProps {q} (qc-α-Sent⇒ αSent) α∈q
   vote∈QcProps {q} {α} αSent va∈q
      with  All-lookup (Abs.qVotes-C5 q)  (Abs.∈QC-Vote-correct q va∈q)
   ...| ev
      with qc-α-Sent⇒ αSent
   ...| qcp
      with qcp⇒concBits qcp va∈q
   ...| mkConcBits as' as∈cqc αVote≡'
               = mkV∈QcP ev as' as∈cqc
                    (voteInEvidence≈rebuiltVote {valid = isv qcp} as∈cqc ev αVote≡')

   -- Here we capture the idea that there exists a vote message that
   -- witnesses the existence of a given Abs.Vote
   record ∃VoteMsgFor (v : Abs.Vote) : Set where
     constructor mk∃VoteMsgFor
     field
       -- A message that was actually sent
       nm            : NetworkMsg
       cv            : Vote
       cv∈nm         : cv ⊂Msg nm
       -- And contained a valid vote that, once abstracted, yeilds v.
       vmsgMember    : Member 𝓔
       vmsgSigned    : WithVerSig (getPubKey 𝓔 vmsgMember) cv
       vmsg≈v        : α-ValidVote 𝓔 cv vmsgMember ≡ v
       vmsgEpoch     : cv ^∙ vEpoch ≡ epochId 𝓔
   open ∃VoteMsgFor public

   record ∃VoteMsgSentFor (sm : SentMessages)(v : Abs.Vote) : Set where
     constructor mk∃VoteMsgSentFor
     field
       vmFor        : ∃VoteMsgFor v
       vmSender     : NodeId
       nmSentByAuth : (vmSender , (nm vmFor)) ∈ sm
   open ∃VoteMsgSentFor public

   ∃VoteMsgSentFor-stable : ∀ {e e'} {pre : SystemState e} {post : SystemState e'} {v}
                          → Step pre post
                          → ∃VoteMsgSentFor (msgPool pre) v
                          → ∃VoteMsgSentFor (msgPool post) v
   ∃VoteMsgSentFor-stable theStep (mk∃VoteMsgSentFor sndr vmFor sba) =
                                   mk∃VoteMsgSentFor sndr vmFor (msgs-stable theStep sba)

   record ∃VoteMsgInFor (outs : List NetworkMsg)(v : Abs.Vote) : Set where
     constructor mk∃VoteMsgInFor
     field
       vmFor    : ∃VoteMsgFor v
       nmInOuts : nm vmFor ∈ outs
   open ∃VoteMsgInFor public

   ∈QC⇒sent : ∀{e} {st : SystemState e} {q α}
            → Abs.Q q α-Sent (msgPool st)
            → Meta-Honest-Member 𝓔 α
            → (vα : α Abs.∈QC q)
            → ∃VoteMsgSentFor (msgPool st) (Abs.∈QC-Vote q vα)

   ∈QC⇒sent {e} {st} {α = α} vsent@(ws {sender} {nm} e≡ nm∈st (qc∈NM {cqc} {q} .{nm} valid cqc∈nm cqc≡)) ha va
      with vote∈QcProps vsent va
   ...| mkV∈QcP ev _ as∈qc rbld
      with vote∈qc as∈qc rbld cqc∈nm
   ...| v∈nm = mk∃VoteMsgSentFor
                 (mk∃VoteMsgFor nm (₋cveVote ev) v∈nm
                                (₋ivvMember (₋cveIsValidVote ev))
                                (₋ivvSigned (₋cveIsValidVote ev)) (₋cveIsAbs ev)
                                (₋ivvEpoch (₋cveIsValidVote ev)))
                 sender
                 nm∈st

   -- Finally, we can define the abstract system state corresponding to the concrete state st
   ConcSystemState : AbsSystemState ℓ0
   ConcSystemState = record
     { InSys           = λ { r → r α-Sent (msgPool st) }
     ; HasBeenSent     = λ { v → ∃VoteMsgSentFor (msgPool st) v }
     ; ∈QC⇒HasBeenSent = ∈QC⇒sent {st = st}
     }


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

module Categories.Morphism.Properties {o ℓ e} (𝒞 : Category o ℓ e) where

open import Data.Product using (_,_; _×_)

open Category 𝒞
open HomReasoning

import Categories.Morphism as M
open M 𝒞
open import Categories.Morphism.Reasoning 𝒞

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

module _ (iso : Iso f g) where

  open Iso iso

  Iso-resp-≈ : f ≈ h → g ≈ i → Iso h i
  Iso-resp-≈ {h = h} {i = i} eq₁ eq₂ = record
    { isoˡ = begin
      i ∘ h ≈˘⟨ eq₂ ⟩∘⟨ eq₁ ⟩
      g ∘ f ≈⟨ isoˡ ⟩
      id    ∎
    ; isoʳ = begin
      h ∘ i ≈˘⟨ eq₁ ⟩∘⟨ eq₂ ⟩
      f ∘ g ≈⟨ isoʳ ⟩
      id    ∎
    }

  Iso-swap : Iso g f
  Iso-swap = record
    { isoˡ = isoʳ
    ; isoʳ = isoˡ
    }

  Iso⇒Mono : Mono f
  Iso⇒Mono h i eq = begin
    h           ≈⟨ introˡ isoˡ ⟩
    (g ∘ f) ∘ h ≈⟨ pullʳ eq ⟩
    g ∘ f ∘ i   ≈⟨ cancelˡ isoˡ ⟩
    i           ∎

  Iso⇒Epi : Epi f
  Iso⇒Epi h i eq = begin
    h           ≈⟨ introʳ isoʳ ⟩
    h ∘ f ∘ g   ≈⟨ pullˡ eq ⟩
    (i ∘ f) ∘ g ≈⟨ cancelʳ isoʳ ⟩
    i           ∎

Iso-∘ : Iso f g → Iso h i → Iso (h ∘ f) (g ∘ i)
Iso-∘ {f = f} {g = g} {h = h} {i = i} iso iso′ = record
  { isoˡ = begin
    (g ∘ i) ∘ h ∘ f ≈⟨ cancelInner (isoˡ iso′) ⟩
    g ∘ f           ≈⟨ isoˡ iso ⟩
    id              ∎
  ; isoʳ = begin
    (h ∘ f) ∘ g ∘ i ≈⟨ cancelInner (isoʳ iso) ⟩
    h ∘ i           ≈⟨ isoʳ iso′ ⟩
    id              ∎
  }
  where open Iso

Iso-≈ : f ≈ h → Iso f g → Iso h i → g ≈ i
Iso-≈ {f = f} {h = h} {g = g} {i = i} eq iso iso′ = begin
  g           ≈⟨ introˡ (isoˡ iso′) ⟩
  (i ∘ h) ∘ g ≈˘⟨ (refl ⟩∘⟨ eq) ⟩∘⟨refl ⟩
  (i ∘ f) ∘ g ≈⟨ cancelʳ (isoʳ iso) ⟩
  i           ∎
  where open Iso

module _ where
  open _≅_

  isos×≈⇒≈ : ∀ {f g : A ⇒ B} → h ≈ i → (iso₁ : A ≅ C) → (iso₂ : B ≅ D) →
               CommutativeSquare f (from iso₁) (from iso₂) h →
               CommutativeSquare g (from iso₁) (from iso₂) i →
               f ≈ g
  isos×≈⇒≈ {h = h} {i = i} {f = f} {g = g} eq iso₁ iso₂ sq₁ sq₂ = begin
    f ≈⟨ switch-fromtoˡ iso₂ sq₁ ⟩
    to iso₂ ∘ h ∘ from iso₁ ≈⟨ refl⟩∘⟨ (eq ⟩∘⟨refl ) ⟩
    to iso₂ ∘ i ∘ from iso₁ ≈˘⟨ switch-fromtoˡ iso₂ sq₂ ⟩
    g ∎

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2016-07-26, issue 2215, reported by effectfully

data Term : Set where
  abs : Term → Term

Type = Term

f : Type → Term
f (abs b@(abs _)) = b

-- WAS: Panic: Pattern match failure in AsPatterns.conPattern
-- due to a missing reduce

-- Should work.


text:
-- Andreas, 2016-10-01, issue #2231
-- The termination checker should not always see through abstract definitions.

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

  -- abstract hides constructor nature of zero and suc.
  zero = zero'
  suc  = suc'

data D : Nat → Set where
  c1 : ∀ n → D n → D (suc n)
  c2 : ∀ n → D n → D n

-- To see that this is terminating the termination checker has to look at the
-- natural number index, which is in a dot pattern.
f : ∀ n → D n → Nat
f .(suc n) (c1  n d) = f n (c2 n (c2 n d))
f n        (c2 .n d) = f n d

-- Termination checking based on dot patterns should fail,
-- since suc is abstract.


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

open import HoTT
open import homotopy.Bouquet
open import homotopy.FinWedge
open import cohomology.Theory

module cohomology.SubFinBouquet (OT : OrdinaryTheory lzero) where

open OrdinaryTheory OT
open import cohomology.Sphere OT
open import cohomology.SubFinWedge cohomology-theory
open import cohomology.Bouquet OT

C-SubFinBouquet-diag : ∀ n {A B : Type₀} (B-ac : has-choice 0 B lzero) {I} (p : Fin I → Coprod A B)
  → C (ℕ-to-ℤ n) (⊙Bouquet B n) ≃ᴳ Πᴳ B (λ _ → C2 0)
C-SubFinBouquet-diag n {B = B} B-ac p = C-Bouquet-diag n B B-ac

C-FinBouquet-diag : ∀ n I → C (ℕ-to-ℤ n) (⊙FinBouquet I n) ≃ᴳ Πᴳ (Fin I) (λ _ → C2 0)
C-FinBouquet-diag n I = C-SubFinBouquet-diag n {A = Empty} {B = Fin I} (Fin-has-choice 0 lzero) inr

abstract
  C-SubFinBouquet-diag-β : ∀ n {A B : Type₀} (B-ac : has-choice 0 B lzero) {I} (p : Fin I → Coprod A B) g b
    →  GroupIso.f (C-FinBouquet-diag n I) g b
    == GroupIso.f (C-Sphere-diag n)
        (CEl-fmap (ℕ-to-ℤ n) ⊙lower
          (CEl-fmap (ℕ-to-ℤ n) (⊙bwin b) g))
  C-SubFinBouquet-diag-β n B-ac p g b =
    GroupIso.f (C-Sphere-diag n)
      (CEl-fmap (ℕ-to-ℤ n) (⊙bwin b)
        (CEl-fmap (ℕ-to-ℤ n) (⊙–> (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv))) g))
      =⟨ ap (GroupIso.f (C-Sphere-diag n)) $
            ∘-CEl-fmap (ℕ-to-ℤ n) (⊙bwin b) (⊙–> (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv))) g
          ∙ CEl-fmap-base-indep (ℕ-to-ℤ n) (λ _ → idp) g
          ∙ CEl-fmap-∘ (ℕ-to-ℤ n) (⊙bwin b) ⊙lower g ⟩
    GroupIso.f (C-Sphere-diag n) (CEl-fmap (ℕ-to-ℤ n) ⊙lower (CEl-fmap (ℕ-to-ℤ n) (⊙bwin b) g))
      =∎

  C-FinBouquet-diag-β : ∀ n I g <I
    →  GroupIso.f (C-FinBouquet-diag n I) g <I
    == GroupIso.f (C-Sphere-diag n)
        (CEl-fmap (ℕ-to-ℤ n) ⊙lower
          (CEl-fmap (ℕ-to-ℤ n) (⊙bwin <I) g))
  C-FinBouquet-diag-β n I =
    C-SubFinBouquet-diag-β n {A = Empty} {B = Fin I}
      (Fin-has-choice 0 lzero) inr

  inverse-C-SubFinBouquet-diag-β : ∀ n
    {A B : Type₀} (B-ac : has-choice 0 B lzero) (B-dec : has-dec-eq B) {I} (p : Fin I ≃ Coprod A B) g
    →  GroupIso.g (C-SubFinBouquet-diag n B-ac (–> p)) g
    == Group.subsum-r (C (ℕ-to-ℤ n) (⊙Bouquet B n)) (–> p)
        (λ b → CEl-fmap (ℕ-to-ℤ n) (⊙bwproj B-dec b)
          (CEl-fmap (ℕ-to-ℤ n) ⊙lift
            (GroupIso.g (C-Sphere-diag n) (g b))))
  inverse-C-SubFinBouquet-diag-β n {B = B} B-ac B-dec p g =
    CEl-fmap (ℕ-to-ℤ n) (⊙<– (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv)))
      (GroupIso.g (C-subfinite-additive-iso (ℕ-to-ℤ n) (–> p) (⊙Lift (⊙Sphere n)) B-ac)
        (GroupIso.g (C-Sphere-diag n) ∘ g))
      =⟨ ap (CEl-fmap (ℕ-to-ℤ n) (⊙<– (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv)))) $
          inverse-C-subfinite-additive-β (ℕ-to-ℤ n) B-ac B-dec p (GroupIso.g (C-Sphere-diag n) ∘ g) ⟩
    CEl-fmap (ℕ-to-ℤ n) (⊙<– (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv)))
      (Group.subsum-r (C (ℕ-to-ℤ n) (⊙BouquetLift B n)) (–> p)
        (λ b → CEl-fmap (ℕ-to-ℤ n) (⊙bwproj B-dec b) (GroupIso.g (C-Sphere-diag n) (g b))))
      =⟨ GroupHom.pres-subsum-r (C-fmap (ℕ-to-ℤ n) (⊙<– (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv)))) (–> p) $
          (λ b → CEl-fmap (ℕ-to-ℤ n) (⊙bwproj B-dec b) (GroupIso.g (C-Sphere-diag n) (g b))) ⟩
    Group.subsum-r (C (ℕ-to-ℤ n) (⊙Bouquet B n)) (–> p)
      (λ b →
        CEl-fmap (ℕ-to-ℤ n) (⊙<– (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv)))
          (CEl-fmap (ℕ-to-ℤ n) (⊙bwproj B-dec b) (GroupIso.g (C-Sphere-diag n) (g b))))
      =⟨ ap (Group.subsum-r (C (ℕ-to-ℤ n) (⊙Bouquet B n)) (–> p))
          (λ= λ b →
              ∘-CEl-fmap (ℕ-to-ℤ n)
                (⊙<– (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv))) (⊙bwproj B-dec b)
                (GroupIso.g (C-Sphere-diag n) (g b))
            ∙ CEl-fmap-base-indep (ℕ-to-ℤ n)
                (bwproj-BigWedge-emap-r-lift B-dec b)
                (GroupIso.g (C-Sphere-diag n) (g b))
            ∙ CEl-fmap-∘ (ℕ-to-ℤ n) ⊙lift (⊙bwproj B-dec b)
                (GroupIso.g (C-Sphere-diag n) (g b))) ⟩
    Group.subsum-r (C (ℕ-to-ℤ n) (⊙Bouquet B n)) (–> p)
      (λ b →
        CEl-fmap (ℕ-to-ℤ n) (⊙bwproj B-dec b)
          (CEl-fmap (ℕ-to-ℤ n) ⊙lift
            (GroupIso.g (C-Sphere-diag n) (g b))))
      =∎

  inverse-C-FinBouquet-diag-β : ∀ n I g
    →  GroupIso.g (C-FinBouquet-diag n I) g
    == Group.sum (C (ℕ-to-ℤ n) (⊙FinBouquet I n))
        (λ <I → CEl-fmap (ℕ-to-ℤ n) (⊙fwproj <I)
          (CEl-fmap (ℕ-to-ℤ n) ⊙lift
            (GroupIso.g (C-Sphere-diag n) (g <I))))
  inverse-C-FinBouquet-diag-β n I =
    inverse-C-SubFinBouquet-diag-β n {A = Empty} {B = Fin I}
      (Fin-has-choice 0 lzero) Fin-has-dec-eq (⊔₁-Empty (Fin I) ⁻¹)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import FRP.LTL.RSet.Core using ( RSet )
open import FRP.LTL.Time using ( _+_ )

module FRP.LTL.RSet.Next where

○ : RSet → RSet
○ A t = A (t + 1)

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
module Issue1436-2 where

module A where

  infixl 19 _↑_
  infixl  1 _↓_

  data D : Set where
    ●       : D
    _↓_ _↑_ : D → D → D

module B where

  infix -1000000 _↓_

  data D : Set where
    _↓_ : D → D → D

open A
open B

rejected = ● ↑ ● ↓ ● ↑ ● ↓ ● ↑ ●


text:
-- Andreas, 2017-05-17, issue #2574 reported by G. Allais

-- This file is intentionally without module header.

private
  postulate A : Set


text:
open import Prelude
open import Nat
open import Agda.Primitive using (Level; lzero; lsuc) renaming (_⊔_ to lmax)

module List where

  -- definitions

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

  _++_ : {A : Set} → List A → List A → List A
  [] ++ l₂ = l₂
  (h :: l₁) ++ l₂ = h :: (l₁ ++ l₂)

  infixl 50 _++_

  ∥_∥ : {A : Set} → List A → Nat
  ∥ [] ∥ = Z
  ∥ a :: as ∥ = 1+ ∥ as ∥

  _⟦_⟧ : {A : Set} → List A → Nat → Maybe A
  [] ⟦ i ⟧ = None
  (a :: as) ⟦ Z ⟧ = Some a
  (a :: as) ⟦ 1+ i ⟧ = as ⟦ i ⟧

  map : {A B : Set} → (A → B) → List A → List B
  map f [] = []
  map f (a :: as) = f a :: map f as

  foldl : {A B : Set} → (B → A → B) → B → List A → B
  foldl f b [] = b
  foldl f b (a :: as) = foldl f (f b a) as

  concat : {A : Set} → List (List A) → List A
  concat [] = []
  concat (l1 :: rest) = l1 ++ (concat rest)

  -- if the lists aren't the same length,
  -- the extra elements of the longer list are ignored
  zip : {A B : Set} → List A → List B → List (A ∧ B)
  zip []        _         = []
  zip (a :: as) []        = []
  zip (a :: as) (b :: bs) = (a , b) :: zip as bs

  unzip : {A B : Set} → List (A ∧ B) → (List A ∧ List B)
  unzip [] = ([] , [])
  unzip ((a , b) :: rest)
    with unzip rest
  ... | (as , bs) = (a :: as , b :: bs)

  reverse : {A : Set} → List A → List A
  reverse [] = []
  reverse (a :: as) = reverse as ++ (a :: [])

  -- theorems

  list-==-dec :  {A : Set} →
                 (l1 l2 : List A) →
                 ((a1 a2 : A) → a1 == a2 ∨ a1 ≠ a2) →
                 l1 == l2 ∨ l1 ≠ l2
  list-==-dec [] [] A-==-dec       = Inl refl
  list-==-dec [] (_ :: _) A-==-dec = Inr (λ ())
  list-==-dec (_ :: _) [] A-==-dec = Inr (λ ())
  list-==-dec (h1 :: t1) (h2 :: t2) A-==-dec
    with A-==-dec h1 h2
  ... | Inr ne = Inr (λ where refl → ne refl)
  ... | Inl refl
    with list-==-dec t1 t2 A-==-dec
  ... | Inr ne = Inr (λ where refl → ne refl)
  ... | Inl refl = Inl refl

  -- if the items of two lists are equal, then the lists are equal
  ==-per-elem : {A : Set} → {l1 l2 : List A} →
                 ((i : Nat) → l1 ⟦ i ⟧ == l2 ⟦ i ⟧) →
                 l1 == l2
  ==-per-elem {l1 = []} {[]} items== = refl
  ==-per-elem {l1 = []} {h2 :: t2} items== = abort (somenotnone (! (items== Z)))
  ==-per-elem {l1 = h1 :: t1} {[]} items== = abort (somenotnone (items== Z))
  ==-per-elem {l1 = h1 :: t1} {h2 :: t2} items==
    rewrite someinj (items== Z) | ==-per-elem {l1 = t1} {t2} (λ i → items== (1+ i))
      = refl

  -- _++_ theorems
  ++assc : ∀{A a1 a2 a3} → (_++_ {A} a1 a2) ++ a3 == a1 ++ (a2 ++ a3)
  ++assc {A} {[]} {a2} {a3} = refl
  ++assc {A} {x :: a1} {a2} {a3} with a1 ++ a2 ++ a3 | ++assc {A} {a1} {a2} {a3}
  ++assc {A} {x :: a1} {a2} {a3} | _ | refl = refl

  l++[]==l : {A : Set} (l : List A) →
              l ++ [] == l
  l++[]==l [] = refl
  l++[]==l (a :: as)
    rewrite l++[]==l as
      = refl

  -- ∥_∥ theorem
  ∥-++-comm : ∀{A a1 a2} → ∥ a1 ∥ + (∥_∥ {A} a2) == ∥ a1 ++ a2 ∥
  ∥-++-comm {A} {[]} {a2} = refl
  ∥-++-comm {A} {a :: a1} {a2} = 1+ap (∥-++-comm {A} {a1})

  -- _⟦_⟧ and ++ theorem
  ⦇l1++[a]++l2⦈⟦∥l1∥⟧==a : {A : Set} {l1 l2 : List A} {a : A} →
                             (h : ∥ l1 ∥ < ∥ l1 ++ (a :: []) ++ l2 ∥) →
                             ((l1 ++ (a :: []) ++ l2) ⟦ ∥ l1 ∥ ⟧ == Some a)
  ⦇l1++[a]++l2⦈⟦∥l1∥⟧==a {l1 = []} h = refl
  ⦇l1++[a]++l2⦈⟦∥l1∥⟧==a {l1 = a1 :: l1rest} {l2} {a} h = ⦇l1++[a]++l2⦈⟦∥l1∥⟧==a {l1 = l1rest} {l2} {a} (1+n<1+m→n<m h)

  -- packaging of list indexing results
  list-index-dec : {A : Set} (l : List A) (i : Nat) →
                    l ⟦ i ⟧ == None ∨ Σ[ a ∈ A ] (l ⟦ i ⟧ == Some a)
  list-index-dec l i
    with l ⟦ i ⟧
  ... | None   = Inl refl
  ... | Some a = Inr (a , refl)

  -- theorems characterizing the partiality of list indexing
  list-index-some : {A : Set} {l : List A} {i : Nat} →
                     i < ∥ l ∥ →
                     Σ[ a ∈ A ] (l ⟦ i ⟧ == Some a)
  list-index-some {l = []}      {Z}    i<∥l∥ = abort (n≮0 i<∥l∥)
  list-index-some {l = a :: as} {Z}    i<∥l∥ = _ , refl
  list-index-some {l = a :: as} {1+ i} i<∥l∥ = list-index-some (1+n<1+m→n<m i<∥l∥)

  list-index-none : {A : Set} {l : List A} {i : Nat} →
                     ∥ l ∥ ≤ i →
                     l ⟦ i ⟧ == None
  list-index-none {l = []}             i≥∥l∥ = refl
  list-index-none {l = a :: as} {1+ i} i≥∥l∥ = list-index-none (1+n≤1+m→n≤m i≥∥l∥)

  list-index-some-conv : {A : Set} {l : List A} {i : Nat} {a : A} →
                          l ⟦ i ⟧ == Some a →
                          i < ∥ l ∥
  list-index-some-conv {l = l} {i} i≥∥l∥
    with <dec ∥ l ∥ i
  ... | Inr (Inr i<∥l∥) = i<∥l∥
  ... | Inr (Inl refl)
    rewrite list-index-none {l = l} {∥ l ∥} ≤refl
      = abort (somenotnone (! i≥∥l∥))
  ... | Inl ∥l∥<i
    rewrite list-index-none (n<m→n≤m ∥l∥<i)
      = abort (somenotnone (! i≥∥l∥))

  list-index-none-conv : {A : Set} {l : List A} {i : Nat} →
                          l ⟦ i ⟧ == None →
                          ∥ l ∥ ≤ i
  list-index-none-conv {l = l} {i} i≥∥l∥
    with <dec ∥ l ∥ i
  ... | Inl ∥l∥<i       = n<m→n≤m ∥l∥<i
  ... | Inr (Inl refl) = ≤refl
  ... | Inr (Inr i<∥l∥)
    with list-index-some i<∥l∥
  ... | _ , i≱∥l∥ rewrite i≥∥l∥ = abort (somenotnone (! i≱∥l∥))

  ∥l1∥==∥l2∥→l1[i]→l2[i] : {A B : Set} {la : List A} {lb : List B} {i : Nat} {a : A} →
                             ∥ la ∥ == ∥ lb ∥ →
                             la ⟦ i ⟧ == Some a →
                             Σ[ b ∈ B ] (lb ⟦ i ⟧ == Some b)
  ∥l1∥==∥l2∥→l1[i]→l2[i] {i = i} ∥la∥==∥lb∥ la[i]==a
    = list-index-some (tr (λ y → i < y) ∥la∥==∥lb∥ (list-index-some-conv la[i]==a))

  ∥l1∥==∥l2∥→¬l1[i]→¬l2[i] : {A B : Set} {la : List A} {lb : List B} {i : Nat} →
                                ∥ la ∥ == ∥ lb ∥ →
                                la ⟦ i ⟧ == None →
                                lb ⟦ i ⟧ == None
  ∥l1∥==∥l2∥→¬l1[i]→¬l2[i] {i = i} ∥la∥==∥lb∥ la[i]==None
    = list-index-none (tr (λ y → y ≤ i) ∥la∥==∥lb∥ (list-index-none-conv la[i]==None))

  -- map theorem
  map-++-comm : ∀{A B f a b} → map f a ++ map f b == map {A} {B} f (a ++ b)
  map-++-comm {a = []} = refl
  map-++-comm {A} {B} {f} {h :: t} {b} with map f (t ++ b) | map-++-comm {A} {B} {f} {t} {b}
  map-++-comm {A} {B} {f} {h :: t} {b} | _ | refl = refl

  -- foldl theorem
  foldl-++ : {A B : Set} {l1 l2 : List A} {f : B → A → B} {b0 : B} →
              foldl f b0 (l1 ++ l2) == foldl f (foldl f b0 l1) l2
  foldl-++ {l1 = []} = refl
  foldl-++ {l1 = a1 :: l1rest} = foldl-++ {l1 = l1rest}

  -- zip/unzip theorems
  unzip-inv : {A B : Set} {l : List (A ∧ B)} {la : List A} {lb : List B} →
               unzip l == (la , lb) →
               l == zip la lb
  unzip-inv {l = []} form
    with form
  ... | refl = refl
  unzip-inv {l = (a' , b') :: rest} {a :: as} {b :: bs} form
    with unzip rest  | unzip-inv {l = rest} refl | form
  ...  | (as' , bs') | refl                      | refl = refl

  zip-inv : {A B : Set} {la : List A} {lb : List B} →
             ∥ la ∥ == ∥ lb ∥ →
             unzip (zip la lb) == (la , lb)
  zip-inv {la = []}      {[]}      len-eq = refl
  zip-inv {la = a :: as} {b :: bs} len-eq
    with unzip (zip as bs) | zip-inv (1+inj len-eq)
  ...  | (as' , bs')       | refl                   = refl

  -- reverse theorems
  reverse-single : {A : Set} {a : A} → reverse (a :: []) == a :: []
  reverse-single = refl

  reverse-++ : {A : Set} {l1 l2 : List A} →
                reverse (l1 ++ l2) == reverse l2 ++ reverse l1
  reverse-++ {l1 = []} {l2}
    rewrite l++[]==l (reverse l2)
      = refl
  reverse-++ {l1 = a1 :: as1} {l2}
    rewrite reverse-++ {l1 = as1} {l2}
      = ++assc {a1 = reverse l2}

  reverse-inv : {A : Set} {l : List A} → reverse (reverse l) == l
  reverse-inv {l = []} = refl
  reverse-inv {l = a :: as}
    rewrite reverse-++ {l1 = reverse as} {a :: []} | reverse-inv {l = as}
      = refl

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


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

open import HoTT

module homotopy.3x3.PushoutPushout where

-- Numbering is in row/column form
-- A span^2 is a 5 × 5 table (numbered from 0 to 4) where
-- * the even/even cells are types
-- * the odd/even and even/odd cells are functions
-- * the odd/odd cells are equalities between functions
record Span^2 {i} : Type (lsucc i) where
  constructor span^2
  field
    A₀₀ A₀₂ A₀₄ A₂₀ A₂₂ A₂₄ A₄₀ A₄₂ A₄₄ : Type i
    f₀₁ : A₀₂ → A₀₀
    f₀₃ : A₀₂ → A₀₄
    f₂₁ : A₂₂ → A₂₀
    f₂₃ : A₂₂ → A₂₄
    f₄₁ : A₄₂ → A₄₀
    f₄₃ : A₄₂ → A₄₄
    f₁₀ : A₂₀ → A₀₀
    f₃₀ : A₂₀ → A₄₀
    f₁₂ : A₂₂ → A₀₂
    f₃₂ : A₂₂ → A₄₂
    f₁₄ : A₂₄ → A₀₄
    f₃₄ : A₂₄ → A₄₄
    H₁₁ : (x : A₂₂) → f₁₀ (f₂₁ x) == f₀₁ (f₁₂ x)
    H₁₃ : (x : A₂₂) → f₀₃ (f₁₂ x) == f₁₄ (f₂₃ x)
    H₃₁ : (x : A₂₂) → f₃₀ (f₂₁ x) == f₄₁ (f₃₂ x)
    H₃₃ : (x : A₂₂) → f₄₃ (f₃₂ x) == f₃₄ (f₂₃ x)

record SquareFunc {i} : Type (lsucc i) where
  constructor square
  field
    {A B₁ B₂ C} : Type i
    f₁ : A  → B₁
    f₂ : A  → B₂
    g₁ : B₁ → C
    g₂ : B₂ → C

module _ {i} where

  square=-raw :
    {A A' : Type i} (eq-A : A == A')
    {B₁ B₁' : Type i} (eq-B₁ : B₁ == B₁')
    {B₂ B₂' : Type i} (eq-B₂ : B₂ == B₂')
    {C C' : Type i} (eq-C : C == C')
    {f₁ : A → B₁} {f₁' : A' → B₁'} (eq-f₁ : f₁ == f₁' [ (λ u → fst u → snd u) ↓ pair×= eq-A eq-B₁ ])
    {f₂ : A → B₂} {f₂' : A' → B₂'} (eq-f₂ : f₂ == f₂' [ (λ u → fst u → snd u) ↓ pair×= eq-A eq-B₂ ])
    {g₁ : B₁ → C} {g₁' : B₁' → C'} (eq-g₁ : g₁ == g₁' [ (λ u → fst u → snd u) ↓ pair×= eq-B₁ eq-C ])
    {g₂ : B₂ → C} {g₂' : B₂' → C'} (eq-g₂ : g₂ == g₂' [ (λ u → fst u → snd u) ↓ pair×= eq-B₂ eq-C ])
    → square f₁ f₂ g₁ g₂ == square f₁' f₂' g₁' g₂'
  square=-raw idp idp idp idp idp idp idp idp = idp

  square-thing :
    {A A' : Type i} (eq-A : A == A')
    {B₁ B₁' : Type i} (eq-B₁ : B₁ == B₁')
    {B₂ B₂' : Type i} (eq-B₂ : B₂ == B₂')
    {C C' : Type i} (eq-C : C == C')
    {f₁ : A → B₁} {f₁' : A' → B₁'} (eq-f₁ : f₁ == f₁' [ (λ u → fst u → snd u) ↓ pair×= eq-A eq-B₁ ])
    {f₂ : A → B₂} {f₂' : A' → B₂'} (eq-f₂ : f₂ == f₂' [ (λ u → fst u → snd u) ↓ pair×= eq-A eq-B₂ ])
    {g₁ : B₁ → C} {g₁' : B₁' → C'} (eq-g₁ : g₁ == g₁' [ (λ u → fst u → snd u) ↓ pair×= eq-B₁ eq-C ])
    {g₂ : B₂ → C} {g₂' : B₂' → C'} (eq-g₂ : g₂ == g₂' [ (λ u → fst u → snd u) ↓ pair×= eq-B₂ eq-C ])
    {a : _} {b : _}
    → a == b [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₂ u (SquareFunc.f₂ u x) == SquareFunc.g₁ u (SquareFunc.f₁ u x))) ↓ (square=-raw eq-A eq-B₂ eq-B₁ eq-C eq-f₂ eq-f₁ eq-g₂ eq-g₁) ]
    → a == b [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x))) ↓ (square=-raw eq-A eq-B₁ eq-B₂ eq-C eq-f₁ eq-f₂ eq-g₁ eq-g₂) ]
  square-thing idp idp idp idp idp idp idp idp α = α

  span^2=-raw :
    {A₀₀ A₀₀' : Type i} (eq-A₀₀ : A₀₀ == A₀₀')
    {A₀₂ A₀₂' : Type i} (eq-A₀₂ : A₀₂ == A₀₂')
    {A₀₄ A₀₄' : Type i} (eq-A₀₄ : A₀₄ == A₀₄')
    {A₂₀ A₂₀' : Type i} (eq-A₂₀ : A₂₀ == A₂₀')
    {A₂₂ A₂₂' : Type i} (eq-A₂₂ : A₂₂ == A₂₂')
    {A₂₄ A₂₄' : Type i} (eq-A₂₄ : A₂₄ == A₂₄')
    {A₄₀ A₄₀' : Type i} (eq-A₄₀ : A₄₀ == A₄₀')
    {A₄₂ A₄₂' : Type i} (eq-A₄₂ : A₄₂ == A₄₂')
    {A₄₄ A₄₄' : Type i} (eq-A₄₄ : A₄₄ == A₄₄')
    {f₀₁ : A₀₂ → A₀₀} {f₀₁' : A₀₂' → A₀₀'} (eq-f₀₁ : f₀₁ == f₀₁' [ (λ u → fst u → snd u) ↓ pair×= eq-A₀₂ eq-A₀₀ ])
    {f₀₃ : A₀₂ → A₀₄} {f₀₃' : A₀₂' → A₀₄'} (eq-f₀₃ : f₀₃ == f₀₃' [ (λ u → fst u → snd u) ↓ pair×= eq-A₀₂ eq-A₀₄ ])
    {f₂₁ : A₂₂ → A₂₀} {f₂₁' : A₂₂' → A₂₀'} (eq-f₂₁ : f₂₁ == f₂₁' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₂ eq-A₂₀ ])
    {f₂₃ : A₂₂ → A₂₄} {f₂₃' : A₂₂' → A₂₄'} (eq-f₂₃ : f₂₃ == f₂₃' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₂ eq-A₂₄ ])
    {f₄₁ : A₄₂ → A₄₀} {f₄₁' : A₄₂' → A₄₀'} (eq-f₄₁ : f₄₁ == f₄₁' [ (λ u → fst u → snd u) ↓ pair×= eq-A₄₂ eq-A₄₀ ])
    {f₄₃ : A₄₂ → A₄₄} {f₄₃' : A₄₂' → A₄₄'} (eq-f₄₃ : f₄₃ == f₄₃' [ (λ u → fst u → snd u) ↓ pair×= eq-A₄₂ eq-A₄₄ ])
    {f₁₀ : A₂₀ → A₀₀} {f₁₀' : A₂₀' → A₀₀'} (eq-f₁₀ : f₁₀ == f₁₀' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₀ eq-A₀₀ ])
    {f₃₀ : A₂₀ → A₄₀} {f₃₀' : A₂₀' → A₄₀'} (eq-f₃₀ : f₃₀ == f₃₀' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₀ eq-A₄₀ ])
    {f₁₂ : A₂₂ → A₀₂} {f₁₂' : A₂₂' → A₀₂'} (eq-f₁₂ : f₁₂ == f₁₂' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₂ eq-A₀₂ ])
    {f₃₂ : A₂₂ → A₄₂} {f₃₂' : A₂₂' → A₄₂'} (eq-f₃₂ : f₃₂ == f₃₂' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₂ eq-A₄₂ ])
    {f₁₄ : A₂₄ → A₀₄} {f₁₄' : A₂₄' → A₀₄'} (eq-f₁₄ : f₁₄ == f₁₄' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₄ eq-A₀₄ ])
    {f₃₄ : A₂₄ → A₄₄} {f₃₄' : A₂₄' → A₄₄'} (eq-f₃₄ : f₃₄ == f₃₄' [ (λ u → fst u → snd u) ↓ pair×= eq-A₂₄ eq-A₄₄ ])
    {H₁₁ : (x : A₂₂) → f₁₀ (f₂₁ x) == f₀₁ (f₁₂ x)} {H₁₁' : (x : A₂₂') → f₁₀' (f₂₁' x) == f₀₁' (f₁₂' x)}
    (eq-H₁₁ : H₁₁ == H₁₁' [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x)))
                          ↓ square=-raw eq-A₂₂ eq-A₂₀ eq-A₀₂ eq-A₀₀ eq-f₂₁ eq-f₁₂ eq-f₁₀ eq-f₀₁ ])
    {H₁₃ : (x : A₂₂) → f₀₃ (f₁₂ x) == f₁₄ (f₂₃ x)} {H₁₃' : (x : A₂₂') → f₀₃' (f₁₂' x) == f₁₄' (f₂₃' x)}
    (eq-H₁₃ : H₁₃ == H₁₃' [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x)))
                          ↓ square=-raw eq-A₂₂ eq-A₀₂ eq-A₂₄ eq-A₀₄ eq-f₁₂ eq-f₂₃ eq-f₀₃ eq-f₁₄ ])
    {H₃₁ : (x : A₂₂) → f₃₀ (f₂₁ x) == f₄₁ (f₃₂ x)} {H₃₁' : (x : A₂₂') → f₃₀' (f₂₁' x) == f₄₁' (f₃₂' x)}
    (eq-H₃₁ : H₃₁ == H₃₁' [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x)))
                          ↓ square=-raw eq-A₂₂ eq-A₂₀ eq-A₄₂ eq-A₄₀ eq-f₂₁ eq-f₃₂ eq-f₃₀ eq-f₄₁ ])
    {H₃₃ : (x : A₂₂) → f₄₃ (f₃₂ x) == f₃₄ (f₂₃ x)} {H₃₃' : (x : A₂₂') → f₄₃' (f₃₂' x) == f₃₄' (f₂₃' x)}
    (eq-H₃₃ : H₃₃ == H₃₃' [ (λ u → ((x : SquareFunc.A u) → SquareFunc.g₁ u (SquareFunc.f₁ u x) == SquareFunc.g₂ u (SquareFunc.f₂ u x)))
                          ↓ square=-raw eq-A₂₂ eq-A₄₂ eq-A₂₄ eq-A₄₄ eq-f₃₂ eq-f₂₃ eq-f₄₃ eq-f₃₄ ])
     → span^2 A₀₀  A₀₂  A₀₄  A₂₀  A₂₂  A₂₄  A₄₀  A₄₂  A₄₄  f₀₁  f₀₃  f₂₁  f₂₃  f₄₁  f₄₃  f₁₀  f₃₀  f₁₂  f₃₂  f₁₄  f₃₄  H₁₁  H₁₃  H₃₁  H₃₃
    == span^2 A₀₀' A₀₂' A₀₄' A₂₀' A₂₂' A₂₄' A₄₀' A₄₂' A₄₄' f₀₁' f₀₃' f₂₁' f₂₃' f₄₁' f₄₃' f₁₀' f₃₀' f₁₂' f₃₂' f₁₄' f₃₄' H₁₁' H₁₃' H₃₁' H₃₃'
  span^2=-raw idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp idp = idp

module M {i} (d : Span^2 {i}) where

  open Span^2 d

  A₀∙ : Type i
  A₀∙ = Pushout (span A₀₀ A₀₄ A₀₂ f₀₁ f₀₃)

  A₂∙ : Type i
  A₂∙ = Pushout (span A₂₀ A₂₄ A₂₂ f₂₁ f₂₃)

  A₄∙ : Type i
  A₄∙ = Pushout (span A₄₀ A₄₄ A₄₂ f₄₁ f₄₃)

  module F₁∙ = PushoutRec {D = A₀∙}
                          (left ∘ f₁₀) (right ∘ f₁₄)
                          (λ c → ap left (H₁₁ c)
                                 ∙ glue (f₁₂ c)
                                 ∙ ap right (H₁₃ c))

  f₁∙ : A₂∙ → A₀∙
  f₁∙ = F₁∙.f

  module F₃∙ = PushoutRec {D = A₄∙}
                          (left ∘ f₃₀) (right ∘ f₃₄)
                          (λ c → ap left (H₃₁ c)
                                 ∙ glue (f₃₂ c)
                                 ∙ ap right (H₃₃ c))

  f₃∙ : A₂∙ → A₄∙
  f₃∙ = F₃∙.f

  -- Span obtained after taking horizontal pushouts
  v-h-span : Span
  v-h-span = span A₀∙ A₄∙ A₂∙ f₁∙ f₃∙

  Pushout^2 : Type i
  Pushout^2 = Pushout v-h-span

  {-
  Definition of [f₁∙] and [f₃∙] in ∞TT:

  f₁∙ : A₂∙ → A₀∙
  f₁∙ (left a) = left (f₁₀ a)
  f₁∙ (right c) = right (f₁₄ c)
  ap f₁∙ (glue b) = ap left (H₁₁ c) ∙ glue (f₁₂ c) ∙ ap right (H₁₃ c)

  f₃∙ : A₂∙ → A₄∙
  f₃∙ (left a) = left (f₃₀ a)
  f₃∙ (right c) = right (f₃₄ c)
  ap f₃∙ (glue b) = ap left (H₃₁ c) ∙ glue (f₃₂ c) ∙ ap right (H₃₃ c)
  -}

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

-- This module packages up all the stuff that's passed to the other
-- modules in a convenient form.
module Polynomial.Parameters where

open import Function
open import Algebra
open import Relation.Unary
open import Level
open import Algebra.Solver.Ring.AlmostCommutativeRing
open import Data.Bool using (Bool; T)

-- This record stores all the stuff we need for the coefficients:
--
--  * A raw ring
--  * A (decidable) predicate on "zeroeness"
--
-- It's used for defining the operations on the horner normal form.
record RawCoeff c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    coeffs  : RawRing c ℓ
    Zero-C  : RawRing.Carrier coeffs → Bool

  open RawRing coeffs public

-- This record stores the full information we need for converting
-- to the final ring.
record Homomorphism c ℓ₁ ℓ₂ ℓ₃ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  field
    coeffs : RawCoeff c ℓ₁
  module Raw = RawCoeff coeffs
  field
    ring     : AlmostCommutativeRing ℓ₂ ℓ₃
    morphism : Raw.coeffs -Raw-AlmostCommutative⟶ ring
  open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧ᵣ) public
  open AlmostCommutativeRing ring public
  field
    Zero-C⟶Zero-R : ∀ x → T (Raw.Zero-C x) → 0# ≈  ⟦ x ⟧ᵣ

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
module Prelude.Erased where

data [erased]-is-only-for-printing : Set where
  [erased] : [erased]-is-only-for-printing

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
module Common.ContextPair where

open import Common.Context public

-- Context pairs.

infix 4 _⁏_
record Cx² (U V : Set) : Set where
  constructor _⁏_
  field
    int : Cx U
    mod : Cx V

open Cx² public

∅² : ∀ {U V} → Cx² U V
∅² = ∅ ⁏ ∅

-- Context inclusion.

module _ {U V : Set} where
  infix 3 _⊆²_
  _⊆²_ : Cx² U V → Cx² U V → Set
  Γ ⁏ Δ ⊆² Γ′ ⁏ Δ′ = Γ ⊆ Γ′ × Δ ⊆ Δ′

  refl⊆² : ∀ {Π} → Π ⊆² Π
  refl⊆² = refl⊆ , refl⊆

  trans⊆² : ∀ {Π Π′ Π″} → Π ⊆² Π′ → Π′ ⊆² Π″ → Π ⊆² Π″
  trans⊆² (η , θ) (η′ , θ′) = trans⊆ η η′ , trans⊆ θ θ′

  weak⊆²₁ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊆² Γ , A ⁏ Δ
  weak⊆²₁ = weak⊆ , refl⊆

  weak⊆²₂ : ∀ {A Γ Δ} → Γ ⁏ Δ ⊆² Γ ⁏ Δ , A
  weak⊆²₂ = refl⊆ , weak⊆

  bot⊆² : ∀ {Π} → ∅² ⊆² Π
  bot⊆² = bot⊆ , bot⊆

-- Context concatenation.

module _ {U V : Set} where
  _⧺²_ : Cx² U V → Cx² U V → Cx² U V
  (Γ ⁏ Δ) ⧺² (Γ′ ⁏ Δ′) = Γ ⧺ Γ′ ⁏ Δ ⧺ Δ′

  weak⊆²⧺₁ : ∀ {Π} Π′ → Π ⊆² Π ⧺² Π′
  weak⊆²⧺₁ (Γ′ ⁏ Δ′) = weak⊆⧺₁ Γ′ , weak⊆⧺₁ Δ′

  weak⊆²⧺₂ : ∀ {Π Π′} → Π′ ⊆² Π ⧺² Π′
  weak⊆²⧺₂ = weak⊆⧺₂ , weak⊆⧺₂

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.ZCohomology.S1.S1 where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.HITs.S1
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.Nullification
open import Cubical.Data.Int
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation

----  H⁰(S¹) = ℤ  ----

coHom0-S1 : coHom zero S¹ ≡ Int
coHom0-S1 = (λ i → ∥ helpLemma i ∥₀ ) ∙ setId isSetInt
  where
  helpLemma : (S¹ → Int) ≡ Int
  helpLemma = isoToPath (iso fun funinv (λ _ → refl) (λ f → funExt (rinvLemma f)))
    where
    fun : (S¹ → Int) → Int
    fun f = f base

    funinv : Int → (S¹ → Int)
    funinv a base = a
    funinv a (loop i) = a

    rinvLemma : (f : S¹ → Int) → (x : S¹) → funinv (fun f) x ≡ f x
    rinvLemma f  base = refl
    rinvLemma f  (loop i) j = isSetInt (f base) (f base) (λ k → f (loop k)) refl (~ j) i

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

{- TODO : give Hᵏ(S¹) for all k -}

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical