text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.List.Base where

open import Agda.Builtin.List        public
open import Cubical.Core.Everything

module _ {ℓ} {A : Type ℓ} where

  infixr 5 _++_

  [_] : A → List A
  [ a ] = a ∷ []

  _++_ : List A → List A → List A
  [] ++ ys = ys
  (x ∷ xs) ++ ys = x ∷ xs ++ ys

  rev : List A → List A
  rev [] = []
  rev (x ∷ xs) = rev xs ++ [ x ]

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Structure.Function.Proofs where

import      Lvl
open import Functional
open import Structure.Function
open import Structure.Operator
open import Structure.Operator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ : Lvl.Level
private variable T A B C D : Type{ℓ}

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-C : Equiv{ℓₑ₃}(C) ⦄
  ⦃ equiv-D : Equiv{ℓₑ₄}(D) ⦄
  {f : C → D} ⦃ func : Function(f) ⦄
  {_▫_ : A → B → C} ⦃ oper : BinaryOperator(_▫_) ⦄
  where

  [∘₂]-function : BinaryOperator(f ∘₂ (_▫_))
  BinaryOperator.congruence [∘₂]-function = congruence₁(f) ∘₂ congruence₂(_▫_)

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-C : Equiv{ℓₑ₃}(C) ⦄
  {_▫_ : A → B → C}
  ⦃ funcₗ : ∀{x} → Function(x ▫_) ⦄
  ⦃ funcᵣ : ∀{y} → Function(_▫ y) ⦄
  where

  binaryOperator-from-function : BinaryOperator(_▫_)
  BinaryOperator.congruence binaryOperator-from-function xy1 xy2 = congruence₁(_▫ _) xy1 🝖 congruence₁(_ ▫_) xy2

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {_▫_ : A → A → B}
  ⦃ funcᵣ : ∀{y} → Function(_▫ y) ⦄
  ⦃ comm : Commutativity(_▫_) ⦄
  where

  functionₗ-from-commutative-functionᵣ : ∀{x} → Function(x ▫_)
  Function.congruence (functionₗ-from-commutative-functionᵣ{a}) {x}{y} xy = commutativity(_▫_) {a}{x} 🝖 congruence₁(_▫ a) xy 🝖 commutativity(_▫_) {y}{a}

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  {_▫_ : A → A → B}
  ⦃ funcᵣ : ∀{x} → Function(x ▫_) ⦄
  ⦃ comm : Commutativity(_▫_) ⦄
  where

  functionᵣ-from-commutative-functionₗ : ∀{y} → Function(_▫ y)
  Function.congruence (functionᵣ-from-commutative-functionₗ{a}) {x}{y} xy = commutativity(_▫_) {x}{a} 🝖 congruence₁(a ▫_) xy 🝖 commutativity(_▫_) {a}{y}

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module PredicateLifting where

import Level
open import Data.Empty
open import Data.Unit as Unit
open import Data.Nat
open import Data.List as List renaming ([] to Ø; [_] to [_]L)
open import NonEmptyList as NList
open import Data.Fin hiding (_+_)
open import Data.Vec as Vec renaming ([_] to [_]V; _++_ to _++V_)
open import Data.Product as Prod
open import Function

open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open import Relation.Binary
open ≡-Reasoning

open import Common.Context as Context

open import Algebra
open Monoid {{ ... }} hiding (refl)

open import SyntaxRaw
open import Syntax

-- | Extend the parameter context of each type variable in the given
-- type context by one extra variable. We need this to specify the new
-- type variable context, in which the predicate lifting of a type lives.
-- See predL below for the correspond typing rule.
liftTyCtx : ∀ {Θ} → TyCtxMorP Ø Θ → TyCtx
liftTyCtx {Ø}     f       = Ø
liftTyCtx {Γ ∷ Θ} (A , f) = (∗ ∷ Γ) ∷ liftTyCtx f

-- | Extend a parameter context by a variable of the given type.
extTyVarParams : (Γ₂ : RawCtx) → PreType Ø Ø Γ₂ → RawCtx
extTyVarParams Γ₂ A = ∗ ∷ Γ₂

-- | Get the Yᵢ : (Γᵢ, xᵢ : Bᵢ) ⊸ ∗ corresponding to Xᵢ : Γᵢ ⊸ ∗ in
-- the lifted context, c.f. the typing rule for predL below.
liftTyVar : ∀{Θ Γ₂} → (f : TyCtxMorP Ø Θ) (X : TyVar Θ Γ₂) →
            TyVar (liftTyCtx f) (extTyVarParams Γ₂ (getTy f X))
liftTyVar f       zero       = zero
liftTyVar (A , f) (succ Γ X) =
  succ (extTyVarParams Γ (getTy f X)) (liftTyVar f X)

-- | Turn an instantiation into a substitution.
instToSubst : ∀{Γ₁} (A : U) (Γ₂ : RawCtx) → PreTerm Γ₁ Ø →
              CtxMorP (∗ ∷ Γ₂ ++ Γ₁) (∗ ∷ (Γ₂ ↑ A) ++ Γ₁)
instToSubst {Γ₁} A Γ₂ t =
  let f = weakenPO' (∗ ∷ Γ₂) t ∷ ctxProjP Γ₁ (∗ ∷ Γ₂)
  in subst (CtxMorP (∗ ∷ Γ₂ ++ Γ₁))
           (PE.sym (cong (_∷_ ∗ ) (assoc Γ₂ (A ∷ Ø) Γ₁)))
           (extendProj (∗ ∷ Γ₂) Ø f)

-- | Auxiliary function to define predL below.
predL₀ : ∀ {Θ Γ₁ Γ₂} →
         (A : Raw Θ Γ₁ Γ₂) → DecentType A → (f : TyCtxMorP Ø Θ) →
         liftTyCtx f ∣ ∗ ∷ Γ₂ ++ Γ₁ / Ø ⊸Ty
predL₀ ._ (DT-⊤ Θ Γ)                                 f =
  ⊤-PT (liftTyCtx f) (∗ ∷ Ø ++ Γ)
predL₀ ._ (DT-tyVar Γ₁ X)                            f =
  tyVarPT _ (liftTyVar f X) §ₜ ctxProjP' Ø _ Γ₁
predL₀ ._ (DT-inst {Γ₂ = Γ₂} B t B-dec t-dec)        f =
  let B' = predL₀ B B-dec f
  in substPT B' (instToSubst _ Γ₂ (mkPreTerm t-dec))
predL₀ ._ (DT-paramAbstr {Γ₂ = Γ₂} {B = B} Γ₁ A-dec) f =
  subst (λ u → PreType (liftTyCtx f) u Ø)
        (cong (_∷_ ∗) (PE.sym (assoc Γ₂ (B ∷ Ø) Γ₁)))
        (predL₀ _ A-dec f)
predL₀ {Θ} {.Γ₁} {Γ₂} ._ (DT-fp Γ₁ ρ D p)            f =
  fpPT (∗ ∷ Γ₂ ++ Γ₁) ρ (mkD' D p 0) §ₜ f'
  where
    f' : CtxMorP (∗ ∷ Γ₂ ++ Γ₁) (∗ ∷ Γ₂)
    f' = extendP ∗ (ctxProjP' Ø Γ₂ Γ₁)

    mkD' : (D : FpData Raw Θ Γ₂) → DecentFpData D → ℕ →
           FpDataP (liftTyCtx f) (∗ ∷ Γ₂)
    mkD' [ Γ , g , A ] (g-dec , A-dec) k =
      let A' = predL₀ A A-dec (substTy (fpPT Ø ρ (mkFpDataP {D = D} p)) f , f)
      in
        [ ( (∗ ∷ Γ)
          , (α (∗ ∷ Γ) Γ ∗ k §ₘ ctxidP (∗ ∷ Γ))
            ∷ (mkCtxMorP {Γ} {Γ₂} {g} g-dec • ctxProjP Γ (∗ ∷ Ø))
          , A' ) ]
    mkD' ((Γ , g , A) ∷ D₁) ((g-dec , A-dec) , q) k =
      let A' = predL₀ A A-dec (substTy (fpPT Ø ρ (mkFpDataP {D = D} p)) f , f)
      in ( ∗ ∷ Γ
          , (α (∗ ∷ Γ) Γ ∗ k §ₘ ctxidP (∗ ∷ Γ))
            ∷ (mkCtxMorP {Γ} {Γ₂} {g} g-dec • ctxProjP Γ (∗ ∷ Ø))
          , A' )
         ∷ mkD' D₁ q (suc k)

-- | Lift an open type A to predicates. More specifically, predL
-- implements the following rule, in which we write Ā for predL A.
--   X₁ : Δ₁ ⊸ Ty, ..., Xₙ : Δₙ ⊸ Ty | Γ₁ ⊢ A : Γ₂ ⊸ Ty
--   B₁ : Δ₁ ⊸ Ty
--   ...
--   Bₙ : Δ₁ ⊸ Ty
--  ================================================================= (predL)
--   Y₁ : (Δ₁, x₁ : B₁ ⊙ id) ⊸ Ty, ..., (Yₙ : Δₙ, xₙ : Bₙ ⊙ id) ⊸ Ty
--     | Γ₁, Γ₂, z : A[B₁/X₁, ..., Bₙ/Xₙ] ⊙ id
--     ⊢ Ā : Ty
predL : ∀ {Θ Γ₁ Γ₂} →
        PreType Θ Γ₁ Γ₂ →
        (f : TyCtxMorP Ø Θ) →
--      ===========================================================
        liftTyCtx f ∣ ∗ ∷ Γ₂ ++ Γ₁ / Ø ⊸Ty
predL (A , A-dec) = predL₀ A A-dec

-- | Special instance of the predicate lifting for types with one
-- free variable and no parameters.
--           X : Δ ⊸ Ty | Γ ⊢ A : Ty           B : Δ ⊸ Ty
--  =============================================================== (predL₁)
--     Y : (Δ, x : B ⊙ id) ⊸ ∗ | Γ, z : A[B/X] ⊢ Ā : Ty
predL₁ : ∀ {Δ Γ} →
        ((Δ ∷ Ø) ∣ Γ / Ø ⊸Ty) → (Ø ∣ Ø / Δ ⊸Ty) →
--      ===========================================================
        ((∗ ∷ Δ) ∷ Ø) ∣ ∗ ∷ Γ / Ø ⊸Ty
predL₁ A B = predL A (B , tt)

max_stars_repo_name: StillerHarpo/CoindDepTypes

max_issues_repo_name: StillerHarpo/CoindDepTypes

max_forks_repo_name: StillerHarpo/CoindDepTypes


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

-- Universes
open import Agda.Primitive

module main where

-- I don't really understand exactly which equality gets imported in agda if
-- I try to import the builtin, so define the sane MLTT one here.

infixl 4 _≡_
data _≡_ {n : Level} {A : Set n} : A → A → Set n where
  refl : {a : A} → a ≡ a
{-# BUILTIN EQUALITY _≡_ #-}

-- Lemma 2.1.1 all paths have inverses
inv : ∀ {n} {A : Set n} {a b : A} → a ≡ b → b ≡ a
inv refl = refl

-- This is painful to type so I'll just stick with inv most of the time
_⁻¹ = inv

-- Lemma 2.1.2 any two paths with connecting endpoint compose
trans : ∀ {n} {A : Set n} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl p = p

_∙_ = trans
infixl 50 _∙_

-- Lemma 2.1.4 types are groupoids
-- (i) left and right identity laws
left-id : ∀ {n} {A : Set n} {a b : A} → (p : a ≡ b) → refl ∙ p ≡ p
left-id refl = refl

right-id : ∀ {n} {A : Set n} {a b : A} → (p : a ≡ b) → p ∙ refl ≡ p
right-id refl = refl

-- (ii) inverses compose to identity
left-inv : ∀ {n} {A : Set n} {a b : A} → (p : a ≡ b) → (inv p) ∙ p ≡ refl
left-inv refl = refl

right-inv : ∀ {n} {A : Set n} {a b : A} → (p : a ≡ b) → p ∙ (inv p) ≡ refl
right-inv refl = refl

-- (iii) inverse of inverse gives an equal path
inv-inv : ∀ {n} {A : Set n} {a b : A} → (p : a ≡ b) → inv (inv p) ≡ p
inv-inv refl = refl

-- (iv) associativity of path composition
assoc :
  ∀ {n} {A : Set n} {a b c d : A} →
  (p : a ≡ b) (q : b ≡ c) (r : c ≡ d) →
  p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
assoc refl q r = refl

-- Theorem 2.1.6 Eckmann-Hilton
loop-space : (A : Set) (a : A) → Set
loop-space A a = a ≡ a

Ω = loop-space

loop-space-2d : (A : Set) (a : A) → Set
loop-space-2d A a = loop-space (a ≡ a) (refl {a = a})

Ω² = loop-space-2d

_∙ᵣ_ :
  ∀ {n} {A : Set n} {a b c : A} {p q : a ≡ b} →
  (α : p ≡ q) (r : b ≡ c) →
  (p ∙ r ≡ q ∙ r)
α ∙ᵣ refl = (right-id _) ∙ α ∙ (inv (right-id _))

-- My emacs setup doesn't show subscript l for some reason, or I typed it wrong
_∙ₗ_ :
  ∀ {n} {A : Set n} {a b c : A} {r s : b ≡ c} →
  (q : a ≡ b) (β : r ≡ s) →
  (q ∙ r ≡ q ∙ s)
refl ∙ₗ β = β

horizontal-comp : ∀ {n} {A : Set n} {a b c : A} →
  {p q : a ≡ b} {r s : b ≡ c} →
  (α : p ≡ q) (β : r ≡ s) →
  (p ∙ r ≡ q ∙ s)
horizontal-comp {q = q} {r = r} α β = (α ∙ᵣ r) ∙ (q ∙ₗ β)

_⋆_ = horizontal-comp

horizontal-comp' : ∀ {n} {A : Set n} {a b c : A}
  {p q : a ≡ b} {r s : b ≡ c} →
  (α : p ≡ q) (β : r ≡ s) →
  (p ∙ r ≡ q ∙ s)
horizontal-comp' {p = p} {s = s} α β = (p ∙ₗ β) ∙ (α ∙ᵣ s)

_⋆'_ = horizontal-comp'

-- two compositions agree
comp-agree : {A : Set} {a : A} → (α β : loop-space-2d A a) → α ⋆ β ≡ α ⋆' β
comp-agree α β = comp-agree' α β
  where
    -- (more generally at two free endpoints, or we won't get path induction)
    comp-agree' : {A : Set} {a : A} {p r : a ≡ a} → (α : p ≡ refl) (β : refl ≡ r) → α ⋆ β ≡ α ⋆' β
    comp-agree' refl refl = refl

eckmann-hilton : {A : Set} {a : A} → (α β : loop-space-2d A a) → α ∙ β ≡ β ∙ α
eckmann-hilton α β = (inv horizontal-comp-simp) ∙ (comp-agree α β) ∙ horizontal-comp-simp'
  where
    horizontal-comp-simp : α ⋆ β ≡ α ∙ β
    horizontal-comp-simp = remove α β
      where
        -- not hard, just annoying to do directly.
        remove :
          {A : Set} {a b c : A} (p : a ≡ b) (q : b ≡ c) → (p ∙ refl) ∙ q ≡ p ∙ q
        remove refl refl = refl

    horizontal-comp-simp' : α ⋆' β ≡ β ∙ α
    horizontal-comp-simp' = remove β α
      where
        remove :
          {A : Set} {a b c : A} (p : a ≡ b) (q : b ≡ c) → p ∙ (q ∙ refl) ≡ p ∙ q
        remove refl refl = refl

-- Lemma 2.2.1 action on paths preserve path equality
ap :
  ∀ {n m} {A : Set n} {B : Set m} {x y : A} →
  (f : A → B) (p : x ≡ y) → f x ≡ f y
ap f refl = refl

-- Lemma 2.2.2 functions are functors
-- (i) functions preserves composition
ap-preserves-composition :
  ∀ {n m} {A : Set n} {B : Set m} {x y z : A} {f : A → B} →
  (p : x ≡ y) (q : y ≡ z) →
  ap f (p ∙ q) ≡ (ap f p) ∙ (ap f q)
ap-preserves-composition refl q = refl

-- (ii) functions preserves inverses
ap-preserves-inverses :
  ∀ {n m} {A : Set n} {B : Set m} {x y z : A} {f : A → B} →
  (p : x ≡ y) →
  ap f (inv p) ≡ inv (ap f p)
ap-preserves-inverses refl = refl

-- (iii) functors compose
_∘_ :
  ∀ {n m p} {A : Set n} {B : A → Set m} {C : (x : A) → B x → Set p} →
  (g : {x : A} → (y : B x) → C x y) (f : (x : A) → B x) →
  (x : A) → C x (f x)
(g ∘ f) x = g (f x)

ap-preserves-function-composition :
  ∀ {n} {A B C : Set n} {x y z : A} {f : A → B} {g : B → C} →
  (p : x ≡ y) →
  ap g (ap f p) ≡ ap (g ∘ f) p
ap-preserves-function-composition refl = refl

-- (iv) identity maps to identity
ap-identity-map :
  ∀ {n} {A : Set n} {x y : A} →
  (p : x ≡ y) →
  ap (λ x → x) p ≡ p
ap-identity-map refl = refl

-- Lemma 2.3.1 transport
transport :
  ∀ {n m} {A : Set n} {x y : A} →
  (P : A → Set m) (p : x ≡ y) →
  P x → P y
transport _ refl x = x

-- Lemma 2.3.4 dependent action on paths
apd :
  ∀ {n m} {A : Set n} {B : A → Set m} {x y : A} →
  (f : (x : A) → B x) →
  (p : x ≡ y) →
  transport B p (f x) ≡ f y
apd f refl = refl

-- Lemma 2.3.5 non-dependent transport moves around ap path
transport-const :
  ∀ {n} {A B : Set n} {x y : A} →
  (p : x ≡ y) (b : B) →
  transport (λ _ → B) p b ≡ b
transport-const refl b = refl

-- Lemma 2.3.8 relation between dependent and nondependent transport
apd-ap :
  ∀ {n} {A B : Set n} {x y : A} →
  (f : A → B) (p : x ≡ y) →
  apd f p ≡ (transport-const p (f x)) ∙ (ap f p)
apd-ap f refl = refl

-- Lemma 2.3.9 transport unrolling
transport-unroll :
  ∀ {n m} {A : Set n} {P : A → Set m} {x y z : A} →
  (p : x ≡ y) (q : y ≡ z) →
  {u : P x} → transport P q (transport P p u) ≡ transport P (p ∙ q) u
transport-unroll refl refl = refl

-- Lemma 2.3.10 transport over ap
transport-ap :
  ∀ {n m} {A B : Set n} {P : B → Set m} {x y : A} →
  (f : A → B) (p : x ≡ y) →
  {u : P (f x)} → transport (P ∘ f) p u ≡ transport P (ap f p) u
transport-ap f refl = refl

-- Lemma 2.3.11 transport naturality
transport-natural :
  ∀ {n m} {A : Set n} {P Q : A → Set m} {x y : A} →
  (f : (x : A) → P x → Q x) (p : x ≡ y) →
  {u : P x} → transport Q p (f x u) ≡ f y (transport P p u)
transport-natural f refl = refl

-- Definition 2.4.1 homotopy between functions
homotopy : ∀ {n m} {A : Set n} {P : A → Set m} → (f g : (x : A) → P x) → Set (n ⊔ m)
homotopy {A = A} f g = (x : A) → f x ≡ g x

_~_ = homotopy
infixl 10 _~_

-- Lemma 2.4.2 homotopy is an equivalence relation
homotopy-refl :
  ∀ {n m} {A : Set n} {P : A → Set m} →
  (f : (x : A) → P x) → f ~ f
homotopy-refl f x = refl

homotopy-sym :
  ∀ {n m} {A : Set n} {P : A → Set m} →
  (f g : (x : A) → P x) → f ~ g → g ~ f
homotopy-sym f g f-g-hom x = inv (f-g-hom x)

homotopy-trans :
  ∀ {n m} {A : Set n} {P : A → Set m} →
  (f g h : (x : A) → P x) → f ~ g → g ~ h → f ~ h
homotopy-trans f g h f-g-hom g-h-hom x = (f-g-hom x) ∙ (g-h-hom x)

-- Lemma 2.4.3 homotopies are natural transformations between functions
homotopy-natural :
  ∀ {n} {A B : Set n} {x y : A} {p : x ≡ y} →
  (f g : A → B) (H : f ~ g) →
  (H x) ∙ (ap g p) ≡ (ap f p) ∙ (H y)
homotopy-natural {x = x} {p = refl} f g h = right-id (h x)

-- Corollary 2.4.4 naturality over identity
homotopy-natural-id :
  ∀ {n} {A : Set n} →
  (f : A → A) (H : f ~ (λ x → x)) →
  {x : A} → H (f x) ≡ ap f (H x)
homotopy-natural-id f H {x = x} = remove-ends (H x) (inv commute-square)
  where
    f-x-path : f x ≡ x
    f-x-path = H x

    -- annoying to reason about, not hard
    replace-inline :
      ∀ {n} {A : Set n} {x y z : A} →
      {p : x ≡ y} {q q' : y ≡ z} {r : x ≡ z} →
      p ∙ q ≡ r → q ≡ q' → p ∙ q' ≡ r
    replace-inline {p = refl} q-r q-q' = (inv q-q') ∙ q-r

    commute-square : (ap f (H x)) ∙ (H x) ≡ (H (f x)) ∙ (H x)
    commute-square = inv
      (replace-inline
      (homotopy-natural {p = f-x-path} f (λ x → x) H)
      (ap-identity-map (H x)))

    -- annoying to reason about, not hard
    remove-ends :
      ∀ {n} {A : Set n} {x y z : A} →
      {p p' : x ≡ y} → (q : y ≡ z) →
      p ∙ q ≡ p' ∙ q → p ≡ p'
    remove-ends {p = p} {p' = p'} refl p-q-eq-p'-eq =
      (inv (right-id p)) ∙ p-q-eq-p'-eq ∙ (right-id p')

-- Definition 2.4.6 quasi-inverse
record qinv {n m : Level} {A : Set n} {B : Set m} (f : A → B) : Set (n ⊔ m) where
  constructor _st_and_
  field
    g : B → A
    α : f ∘ g ~ λ x → x
    β : g ∘ f ~ λ x → x

-- Example 2.4.7 the identity function is a quasi-inverse
id-qinv : ∀ {n} {A : Set n} → qinv {A = A} {B = A} (λ x → x)
id-qinv = (λ x → x) st (λ x → refl) and (λ x → refl)

-- Example 2.4.8 path concats are quasi-inverses
preconcat-qinv :
  ∀ {n} {A : Set n} {x y z : A} →
  (p : x ≡ y) → qinv (λ (q : y ≡ z) → p ∙ q)
preconcat-qinv {x = x} {y = y} {z = z} p =
  g st α and β
  where
    f : y ≡ z → x ≡ z
    f q = p ∙ q

    g : x ≡ z → y ≡ z
    g pq = (inv p) ∙ pq

    α : (f ∘ g) ~ λ x → x
    α refl = simpl p
      where
        simpl : ∀ {n} {A : Set n} {x y : A} → (p : x ≡ y) → p ∙ ((inv p) ∙ refl) ≡ refl
        simpl refl = refl

    β : (g ∘ f) ~ λ x → x
    β refl = simpl p
      where
        simpl : ∀ {n} {A : Set n} {x y : A} → (p : x ≡ y) → (inv p) ∙ (p ∙ refl) ≡ refl
        simpl refl = refl

postconcat-qinv :
  ∀ {n} {A : Set n} {x y z : A} →
  (p : x ≡ y) → qinv (λ (q : z ≡ x) → q ∙ p)
postconcat-qinv {x = x} {y = y} {z = z} p =
  g st α and β
  where
    f : z ≡ x → z ≡ y
    f q = q ∙ p

    g : z ≡ y → z ≡ x
    g qp = qp ∙ (inv p)

    α : (f ∘ g) ~ λ x → x
    α refl = left-inv p

    β : (g ∘ f) ~ λ x → x
    β refl = right-inv p

-- Example 2.4.9 transport over paths induces a quasi-inverse over the inverse path
transport-qinv :
  ∀ {n m} {A : Set n} {x y : A} →
  (P : A → Set m) (p : x ≡ y) →
  qinv (transport P p)
transport-qinv {x = x} {y = y} P p =
  g st α and β
    where
      f : P x → P y
      f = transport P p

      g : P y → P x
      g = transport P (inv p)

      transport-equiv-paths :
        ∀ {n m} {A : Set n} {x y : A} →
        (P : A → Set m) (p q : x ≡ y) →
        p ≡ q → {n : P x} → transport P p n ≡ transport P q n
      transport-equiv-paths P p .p refl = refl

      transport-refl-paths :
        ∀ {n m} {A : Set n} {x : A} →
        (P : A → Set m) (p : x ≡ x) →
        p ≡ refl → {n : P x} → transport P p n ≡ n
      transport-refl-paths P p p-refl {n = n} =
        transport-equiv-paths P p refl p-refl {n = n}

      α : (f ∘ g) ~ λ x → x
      α x =
        (transport-unroll {P = P} (inv p) p) ∙
        (transport-refl-paths P ((inv p) ∙ p) (left-inv p) {n = x})

      β : (g ∘ f) ~ λ x → x
      β x =
        (transport-unroll {P = P} p (inv p)) ∙
        (transport-refl-paths P _ (right-inv p))

-- 2.4.10 a specific definition of equivalence
record isequiv {n m : Level} {A : Set n} {B : Set m} (f : A → B) : Set (n ⊔ m) where
  constructor _st_also_st_
  field
    g : B → A
    α : f ∘ g ~ λ x → x
    h : B → A
    β : h ∘ f ~ λ x → x

-- (i) quasi-inverses induce equivalences
qinv-to-isequiv :
  ∀ {n m} {A : Set n} {B : Set m} → (f : A → B) → qinv f → isequiv f
qinv-to-isequiv f (g st α and β) = g st α also g st β

-- (ii) equivalences induce quasi-inverses
isequiv-to-qinv :
  ∀ {n m} {A : Set n} {B : Set m} → (f : A → B) → isequiv f → qinv f
isequiv-to-qinv {A} {B} f (g st α also h st β) = g st α and β'
  where
    g~h∘f∘g : g ~ (h ∘ (f ∘ g))
    g~h∘f∘g x = inv (β (g x))

    h∘f∘g~h : (h ∘ (f ∘ g)) ~ h
    h∘f∘g~h x = ap h (α x)

    g~h : g ~ h
    g~h = homotopy-trans _ _ _ g~h∘f∘g h∘f∘g~h

    β' : g ∘ f ~ λ x → x
    β' x = g~h (f x) ∙ (β x)

-- Definition 2.4.11 equivalence between types
record _≃_ {n : Level} (A B : Set n) : Set n where
  constructor _withequiv_
  field
    f : A → B
    e : isequiv f

-- Lemma 2.4.12 type equivalence is a equivalence relation
equiv-refl : ∀ {n} {A : Set n} → A ≃ A
equiv-refl =
  (λ x → x) withequiv
  (qinv-to-isequiv (λ x → x) ((λ x → x) st (λ x → refl) and (λ x → refl)))

equiv-sym : ∀ {n} {A B : Set n} → A ≃ B → B ≃ A
equiv-sym (f withequiv equiv) with (isequiv-to-qinv f equiv)
... | g st α and β = g withequiv qinv-to-isequiv g (f st β and α)

equiv-trans : ∀ {n} {A B C : Set n} → A ≃ B → B ≃ C → A ≃ C
equiv-trans (fab withequiv equivab) (fbc withequiv equivbc)
  with (isequiv-to-qinv fab equivab) | (isequiv-to-qinv fbc equivbc)
... | gab st αab and βab | gbc st αbc and βbc =
      (fbc ∘ fab) withequiv
      (qinv-to-isequiv (fbc ∘ fab) ((gab ∘ gbc)
        st (λ x → ap fbc (αab (gbc x)) ∙ (αbc x))
        and λ x → ap gab (βbc (fab x)) ∙ (βab x)))

record _×_ {n m : Level} (A : Set n) (B : Set m) : Set (n ⊔ m) where
  constructor _,,_
  field
    fst : A
    snd : B

fst : ∀ {n m} {A : Set n} {B : Set m} → A × B → A
fst (fst ,, snd) = fst

snd : ∀ {n m} {A : Set n} {B : Set m} → A × B → B
snd (fst ,, snd) = snd

-- Function 2.6.1 a path between products induces a pair of paths between elements
product-path-to-elem-path :
  ∀ {n m} {A : Set n} {B : Set m} {x y : A × B} →
  x ≡ y → (fst x ≡ fst y) × (snd x ≡ snd y)
product-path-to-elem-path refl = refl ,, refl

-- Theorem 2.6.2 product path to element paths is an equivalence
product-path-to-elem-path-equiv :
  ∀ {n m} {A : Set n} {B : Set m} {x y : A × B} →
  isequiv (product-path-to-elem-path {A = A} {B = B} {x = x} {y = y})
product-path-to-elem-path-equiv {A = A} {B = B} {x = x} {y = y} =
  qinv-to-isequiv product-path-to-elem-path (g st α and β)
    where
      f = product-path-to-elem-path

      g : (fst x ≡ fst y) × (snd x ≡ snd y) → x ≡ y
      g = g' x y
        where
          g' : (x y : A × B) → (fst x ≡ fst y) × (snd x ≡ snd y) → x ≡ y
          g' (fst₁ ,, snd₁) (.fst₁ ,, .snd₁) (refl ,, refl) = refl

      α : f ∘ g ~ λ x → x
      α (refl ,, refl) = refl

      β : g ∘ f ~ λ x → x
      β refl = refl

-- Theorem 2.6.4 transport over a path to a product fiber is a product of fibers over a path
product-transport :
  ∀ {n m} {Z : Set n} {A B : Z → Set m} {z w : Z} →
  (p : z ≡ w) (x : (A z) × (B z))  →
  transport (λ z → (A z) × (B z)) p x ≡ (transport A p (fst x) ,, transport B p (snd x))
product-transport refl (fst ,, snd) = refl

-- Definition of pair⁼
pair⁼ :
  ∀ {n m} {A : Set n} {B : Set m} {x y : A × B} →
  (fst x ≡ fst y) × (snd x ≡ snd y) →
  x ≡ y
pair⁼ {A = A} {B = B} {x = x} {y = y} =
  isequiv.g (product-path-to-elem-path-equiv {A = A} {B = B} {x = x} {y = y})

-- Theorem 2.6.5 functions are functors over products
function-functor-pair :
  {A B A' B' : Set} →
  (g : A → A') (h : B → B') →
  {x y : A × B} {p : fst x ≡ fst y} {q : snd x ≡ snd y} →
  ap (λ x → (g (fst x) ,, h (snd x))) (pair⁼ (p ,, q)) ≡ pair⁼ (ap g p ,, ap h q)
function-functor-pair g h {x = fstx ,, sndx} {y = .fstx ,, .sndx} {p = refl} {q = refl} = refl

-- Theorem 2.7.2 dependent functions are fibrations over Σ-types
record Sigma (A : Set) (B : A → Set) : Set where
  constructor _,,_
  field
    pr1 : A
    pr2 : B pr1

syntax Sigma A (λ x → y) = Σ x of A , y

pr1 : {A : Set} {B : A → Set} → Σ x of A , B x → A
pr1 (left ,, right) = left

pr2 : {A : Set} {B : A → Set} → (v : Σ x of A , B x) → B (pr1 {A} {B} v)
pr2 (left ,, right) = right

-- Theorem 2.7.2 dependent functions are functors over fibrations
function-fibration-product :
  {A : Set} {P : A → Set} {w w' : Σ x of A , P x} →
  (w ≡ w') ≃ (Σ p of (pr1 w ≡ pr1 w') , (transport P p (pr2 w) ≡ pr2 w'))
function-fibration-product {A = A} {P = P} {w = w} {w' = w'} =
  f withequiv qinv-to-isequiv f (g st α and β)
  where
    f :
      {w w' : Σ x of A , P x} →
      (w ≡ w') → (Σ p of (pr1 w ≡ pr1 w') , (transport P p (pr2 w) ≡ pr2 w'))
    f refl = refl ,, refl

    g :
      {w w' : Σ x of A , P x} →
      (Σ p of (pr1 w ≡ pr1 w') , (transport P p (pr2 w) ≡ pr2 w')) → (w ≡ w')
    g {w = w1 ,, w2} {w' = .w1 ,, .w2} (refl ,, refl) = refl

    α : f ∘ g ~ λ x → x
    α (refl ,, refl) = refl

    β : g ∘ f ~ λ x → x
    β refl = refl

-- Corollary 2.7.3 computation rule for Σ types
computation-sigma :
  {A : Set} {P : A → Set} →
  (z : Σ x of A , P x) → z ≡ (pr1 z ,, pr2 z)
computation-sigma z =
  isequiv.g (_≃_.e function-fibration-product)
  (refl ,, refl)

-- Theorem 2.8.1 : only one path between unit elements
record Unit : Set where
  constructor unit

single-path-between-unit : {x y : Unit} → (x ≡ y) ≃ Unit
single-path-between-unit {x = x} {y = y} =
  f withequiv qinv-to-isequiv f
  (g st α and β)
  where
    f : x ≡ y → Unit
    f _ = unit

    g : {x y : Unit} → Unit → x ≡ y
    g {x = unit} {y = unit} _ = refl

    α : f ∘ g ~ λ x → x
    α unit = refl

    β : g ∘ f ~ λ x → x
    β refl = refl

-- Theorem 2.9.2 path between functions are homotopies
happly :
  ∀ {n m} {A : Set n} {B : A → Set m} {f g : (x : A) → B x} →
  (f ≡ g) → f ~ g
happly refl x = refl

-- Axiom 2.9.3 function extensionality
postulate
  funext-equiv : ∀ {n m} {A : Set n} {B : A → Set m} {f g : (x : A) → B x} →
    isequiv (happly {A = A} {B = B} {f = f} {g = g})

funext :
  ∀ {n m} {A : Set n} {B : A → Set m} {f g : (x : A) → B x} →
  f ~ g → f ≡ g
funext = isequiv.g funext-equiv

-- Lemma 2.9.6
function-path-transport-equiv :
  ∀ {n m} {X : Set n} {A B : X → Set m} {x y : X} →
  {p : x ≡ y} (f : A x → B x) (g : A y → B y) →
  (transport (λ x → A x → B x) p f ≡ g) ≃
    ((a : A x) → (transport B p (f a) ≡ g (transport A p a)))
function-path-transport-equiv {p = refl} f g = happly withequiv funext-equiv

-- Lemma 2.10.1 paths between types are equivalences.
id-to-equiv : ∀ {n} {A B : Set n} → A ≡ B → A ≃ B
id-to-equiv refl = equiv-refl

-- Axiom 2.10.3 univalence axiom.
postulate univalence-equiv : ∀ {n} {A B : Set n} → isequiv (id-to-equiv {A = A} {B = B})

max_stars_repo_name: haoxuany/hott-practice

max_issues_repo_name: haoxuany/hott-practice

max_forks_repo_name: haoxuany/hott-practice


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

open import HoTT

module stash.modalities.FiberedPushout {i j k} {X : Type i} {Y : Type j} where

  {-
     X ---glue-left--- P ---glue-right--- Y
  -}

  module _ (P : X → Y → Type k) where
    fibered-pushout-span : Span
    fibered-pushout-span = record
      { A = Σ X λ x → Σ Y λ y → P x y
      ; B = Coprod X Y
      ; C = Coprod (Σ X λ x → Σ Y λ y → P x y) (Σ X λ x → Σ Y λ y → P x y)
      ; f = λ{ (inl p) → p ; (inr p) → p}
      ; g = λ{ (inl p) → inl (fst p) ; (inr p) → inr (fst (snd p))}
      }

    FiberedPushout : Type (lmax (lmax i j) k)
    FiberedPushout = Pushout fibered-pushout-span

  module _ {P : X → Y → Type k} where
    in-left : X → FiberedPushout P
    in-left = right ∘ inl

    in-right : Y → FiberedPushout P
    in-right = right ∘ inr

    in-mid : ∀ {x y} → P x y → FiberedPushout P
    in-mid p = left (_ , _ , p)

    glue-left : ∀ {x y} (p : P x y) → in-mid p == in-left x
    glue-left p = glue (inl (_ , _ , p))

    glue-right : ∀ {x y} (p : P x y) → in-mid p == in-right y
    glue-right p = glue (inr (_ , _ , p))

    module FiberedPushoutElim {l}
      (C : FiberedPushout P → Type l)
      (b1 : (x : X) → C (in-left x))
      (b2 : (x : X) (y : Y) (p : P x y) → C (in-mid p))
      (b3 : (y : Y) → C (in-right y))
      (glue-left' : (x : X) (y : Y) (p : P x y) → b2 x y p == b1 x [ C ↓ glue-left p ])
      (glue-right' : (x : X) (y : Y) (p : P x y) → b2 x y p == b3 y [ C ↓ glue-right p ])
      where

      private
        module PElim = PushoutElim {d = fibered-pushout-span P} {P = C}
          (λ{(x , y , p) → b2 x y p})
          (λ{(inl x) → b1 x ; (inr y) → b3 y})
          (λ{(inl (_ , _ , p)) → glue-left'  _ _ p
           ; (inr (_ , _ , p)) → glue-right' _ _ p})

      f = PElim.f

      glue-left-β : ∀ {x y} (p : P x y) → apd f (glue-left p) == glue-left' x y p
      glue-left-β p = PElim.glue-β (inl (_ , _ , p))

      glue-right-β : ∀ {x y} (p : P x y) → apd f (glue-right p) == glue-right' x y p
      glue-right-β p = PElim.glue-β (inr (_ , _ , p))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A Categorical view of the Sum type (Right-biased)
------------------------------------------------------------------------

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

open import Level

module Data.Sum.Categorical.Right (a : Level) {b} (B : Set b) where

open import Data.Sum.Base
open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Function
import Function.Identity.Categorical as Id

Sumᵣ : Set (a ⊔ b) → Set (a ⊔ b)
Sumᵣ A = A ⊎ B

functor : RawFunctor Sumᵣ
functor = record { _<$>_ = map₁ }

applicative : RawApplicative Sumᵣ
applicative = record
  { pure = inj₁
  ; _⊛_ = [ map₁ , const ∘ inj₂ ]′
  }

monadT : RawMonadT (_∘′ Sumᵣ)
monadT M = record
  { return = M.pure ∘′ inj₁
  ; _>>=_  = λ ma f → ma M.>>= [ f , M.pure ∘′ inj₂ ]′
  } where module M = RawMonad M

monad : RawMonad Sumᵣ
monad = monadT Id.monad

------------------------------------------------------------------------
-- Get access to other monadic functions

module TraversableA {F} (App : RawApplicative {a ⊔ b} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → Sumᵣ (F A) → F (Sumᵣ A)
  sequenceA (inj₂ a) = pure (inj₂ a)
  sequenceA (inj₁ x) = inj₁ <$> x

  mapA : ∀ {A B} → (A → F B) → Sumᵣ A → F (Sumᵣ B)
  mapA f = sequenceA ∘ map₁ f

  forA : ∀ {A B} → Sumᵣ A → (A → F B) → F (Sumᵣ B)
  forA = flip mapA

module TraversableM {M} (Mon : RawMonad {a ⊔ b} M) where

  open RawMonad Mon

  open TraversableA rawIApplicative public
    renaming
    ( sequenceA to sequenceM
    ; mapA      to mapM
    ; forA      to forM
    )


text:
module MJ.Syntax.Scoped where

open import Prelude
open import Data.Maybe as Maybe using (Maybe; just)
open import Data.Maybe.All as MayAll
open import Data.Vec as Vec hiding (_∈_)
open import Data.Star.Indexed
open import Data.List
open import Data.List.Properties.Extra
open import Data.List.Prefix
open import Data.List.Any
open import Data.List.All as List∀ hiding (lookup)
open import Data.List.All.Properties.Extra
open import Relation.Binary.PropositionalEquality

import Data.Vec.All as Vec∀
open Membership-≡

open import MJ.Types

NativeBinOp = ℕ → ℕ → ℕ

data Expr {n : ℕ} (Γ : Ctx c n) : Ty c → Set where
  new  : (C : Fin c) → All (Expr Γ) (Class.constr (clookup C)) → Expr Γ (ref C)
  unit : Expr Γ void
  num  : ℕ → Expr Γ int
  iop  : NativeBinOp → (l r : Expr Γ int) → Expr Γ int
  call : ∀ {cid as b} →
        Expr Γ (ref cid) → Member Σ cid MTH (as , b) → All (Expr Γ) as →
        Expr Γ b
  var  : (i : Fin n) → Expr Γ (lookup i Γ)
  get  : ∀ {cid ty} → Expr Γ (ref cid) → Member Σ cid FLD ty → Expr Γ ty
  upcast : ∀ {c c'} → Σ ⊢ c <: c' → Expr Γ (ref c) → Expr Γ (ref c')

data Cmd {n}(I : Ctx c n)(r : Ty c) : ∀ {m} → (O : Ctx c m) → Set where
  loc  : ∀ a → Expr I a → Cmd I r (a ∷ I)
  asgn : ∀ (i : Fin n) → Expr I (lookup i I) → Cmd I r I
  set  : ∀ {C a} → Expr I (ref C) →
          Member Σ C FLD a → Expr I a → Cmd I r I
  do   : ∀ {a} → Expr I a → Cmd I r I
  ret  : Expr I r → Cmd I r I

Stmts : ∀ {n m}→ (Ctx c n) → Ty c → (Ctx c m) → Set
Stmts I r O = Star ℕ (λ n m (I : Ctx c n) (O : Ctx c m) → Cmd I r O) I O

data Body {n}(I : Ctx c n) : Ty c → Set where
  body : ∀ {m r}{O : Ctx c m} → Stmts I r O → Expr O r → Body I r

-- mapping of namespace typings to the type of their implementation
Def : ∀ {ns} → Fin c → typing ns c → Set
-- methods have bodies
Def {MTH} C (as , b) = Body (ref C ∷ (fromList as)) b
-- fields have initializers
Def {FLD} C a = Body (fromList (Class.constr (clookup C))) a

record Implementation (cid : Fin c) : Set where
  constructor impl
  open Class (clookup cid) public
  field
    -- mapping construct arguments to super constructor arguments
    super-args :
      Maybe.All
        (λ p → All (Expr (fromList constr)) (Class.constr (clookup p)))
        parent

    -- definitions for all local members
    defs : ∀ ns → All (Def cid) (decls ns)

-- implementation of a classtable
record Impl : Set where
  field
    bodies : ∀ (cid : Fin c) → Implementation cid

-- get member definition from a class
getDef : ∀ {ns ty}→ (cid : Fin c) → (m : Member Σ cid ns ty) → Impl → Def (proj₁ m) ty
getDef {ns = ns} cid (_ , refl , def) I with clookup cid | inspect clookup cid
... | C@(class parent constr decls) | [ refl ] with Impl.bodies I cid
... | impl _ defs = ∈-all def (defs ns)
getDef cid (P' , super {pid = pid} p P<:P' , def) I = getDef pid (P' , P<:P' , def) I

Prog : Ty c → Set
Prog a = Impl × (Body [] a)


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

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

import      LibraBFT.Base.KVMap                            as Map
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.Prelude
open import Optics.All

module LibraBFT.Impl.Consensus.TestUtils.MockSharedStorage where

new : ValidatorSet → MockSharedStorage
new = mkMockSharedStorage
  Map.empty
  Map.empty
  Map.empty
  nothing
  nothing

newObmWithLIWS : ValidatorSet → LedgerInfoWithSignatures → MockSharedStorage
newObmWithLIWS vs obmLIWS =
  new vs & mssLis ∙~ Map.singleton (obmLIWS ^∙ liwsVersion) obmLIWS

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
{-# OPTIONS --allow-unsolved-metas #-} -- FIXME

open import Everything

module Test.Test1 where

  test-functor-transextensionality : ∀
    {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂}
    ⦃ functor : Functor 𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂ ⦄
    (open Functor functor)
    → {!Transextensionality!.type _∼₁_ _∼̇₁_!}
  test-functor-transextensionality = transextensionality
  -- test-functor-transextensionality ⦃ functor ⦄ = let open Functor ⦃ … ⦄ in transextensionality1


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Ways to give instances of certain structures where some fields can
-- be given in terms of others
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)

module Algebra.Structures.Biased
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where

open import Algebra.Core
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
import Algebra.Consequences.Setoid as Consequences
open import Data.Product using (_,_; proj₁; proj₂)
open import Level using (_⊔_)

------------------------------------------------------------------------
-- IsCommutativeMonoid

record IsCommutativeMonoidˡ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identityˡ   : LeftIdentity ε ∙
    comm        : Commutative ∙

  open IsSemigroup isSemigroup

  private

    identityʳ : RightIdentity ε ∙
    identityʳ = Consequences.comm+idˡ⇒idʳ setoid comm identityˡ

    identity : Identity ε ∙
    identity = (identityˡ , identityʳ)

  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
  isCommutativeMonoid = record
    { isMonoid = record
      { isSemigroup = isSemigroup
      ; identity    = identity
      }
    ; comm = comm
    }

open IsCommutativeMonoidˡ public
  using () renaming (isCommutativeMonoid to isCommutativeMonoidˡ)

record IsCommutativeMonoidʳ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identityʳ   : RightIdentity ε ∙
    comm        : Commutative ∙

  open IsSemigroup isSemigroup

  private

    identityˡ : LeftIdentity ε ∙
    identityˡ = Consequences.comm+idʳ⇒idˡ setoid comm identityʳ

    identity : Identity ε ∙
    identity = (identityˡ , identityʳ)

  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
  isCommutativeMonoid = record
    { isMonoid = record
      { isSemigroup = isSemigroup
      ; identity    = identity
      }
    ; comm = comm
    }

open IsCommutativeMonoidʳ public
  using () renaming (isCommutativeMonoid to isCommutativeMonoidʳ)

------------------------------------------------------------------------
-- IsCommutativeSemiring

record IsCommutativeSemiringˡ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isCommutativeMonoid : IsCommutativeMonoid * 1#
    distribʳ              : * DistributesOverʳ +
    zeroˡ                 : LeftZero 0# *

  private
    module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
    open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
           using () renaming (comm to *-comm)

    distribˡ : * DistributesOverˡ +
    distribˡ = Consequences.comm+distrʳ⇒distrˡ
                +-CM.setoid +-CM.∙-cong *-comm distribʳ

    distrib : * DistributesOver +
    distrib = (distribˡ , distribʳ)

    zeroʳ : RightZero 0# *
    zeroʳ = Consequences.comm+zeˡ⇒zeʳ +-CM.setoid *-comm zeroˡ

    zero : Zero 0# *
    zero = (zeroˡ , zeroʳ)

  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
  isCommutativeSemiring = record
    { isSemiring = record
      { isSemiringWithoutAnnihilatingZero = record
        { +-isCommutativeMonoid = +-isCommutativeMonoid
        ; *-isMonoid = *-CM.isMonoid
        ; distrib = distrib
        }
      ; zero = zero
      }
    ; *-comm = *-comm
    }

open IsCommutativeSemiringˡ public
  using () renaming (isCommutativeSemiring to isCommutativeSemiringˡ)

record IsCommutativeSemiringʳ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isCommutativeMonoid : IsCommutativeMonoid * 1#
    distribˡ              : * DistributesOverˡ +
    zeroʳ                 : RightZero 0# *

  private
    module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
    open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
           using () renaming (comm to *-comm)

    distribʳ : * DistributesOverʳ +
    distribʳ = Consequences.comm+distrˡ⇒distrʳ
                +-CM.setoid +-CM.∙-cong *-comm distribˡ

    distrib : * DistributesOver +
    distrib = (distribˡ , distribʳ)

    zeroˡ : LeftZero 0# *
    zeroˡ = Consequences.comm+zeʳ⇒zeˡ +-CM.setoid *-comm zeroʳ

    zero : Zero 0# *
    zero = (zeroˡ , zeroʳ)

  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
  isCommutativeSemiring = record
    { isSemiring = record
      { isSemiringWithoutAnnihilatingZero = record
        { +-isCommutativeMonoid = +-isCommutativeMonoid
        ; *-isMonoid = *-CM.isMonoid
        ; distrib = distrib
        }
      ; zero = zero
      }
    ; *-comm = *-comm
    }

open IsCommutativeSemiringʳ public
  using () renaming (isCommutativeSemiring to isCommutativeSemiringʳ)

------------------------------------------------------------------------
-- IsRing

-- We can recover a ring without proving that 0# annihilates *.
record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
                                     : Set (a ⊔ ℓ) where
  field
    +-isAbelianGroup : IsAbelianGroup + 0# -_
    *-isMonoid       : IsMonoid * 1#
    distrib          : * DistributesOver +

  private

    module + = IsAbelianGroup +-isAbelianGroup
    module * = IsMonoid *-isMonoid

    open + using (setoid) renaming (∙-cong to +-cong)
    open * using ()       renaming (∙-cong to *-cong)

    zeroˡ : LeftZero 0# *
    zeroˡ = Consequences.assoc+distribʳ+idʳ+invʳ⇒zeˡ setoid
             +-cong *-cong +.assoc (proj₂ distrib) +.identityʳ +.inverseʳ

    zeroʳ : RightZero 0# *
    zeroʳ = Consequences.assoc+distribˡ+idʳ+invʳ⇒zeʳ setoid
             +-cong *-cong +.assoc (proj₁ distrib) +.identityʳ +.inverseʳ

    zero : Zero 0# *
    zero = (zeroˡ , zeroʳ)

  isRing : IsRing + * -_ 0# 1#
  isRing = record
    { +-isAbelianGroup = +-isAbelianGroup
    ; *-isMonoid = *-isMonoid
    ; distrib = distrib
    ; zero = zero
    }

open IsRingWithoutAnnihilatingZero public
  using () renaming (isRing to isRingWithoutAnnihilatingZero)


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

module Data.Unit.Properties where

open import Data.Unit
open import Level
open import HLevels

isProp⊤ : isProp ⊤
isProp⊤ _ _ i = tt

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module ExtendedLambdaCase where

data Bool : Set where
  true false : Bool

data Void : Set where

foo : Bool -> Bool -> Bool -> Bool
foo = λ { x → λ { y z → {!!} } }

data Bar : (Bool -> Bool) -> Set where
  baz : (t : Void) -> Bar λ { x → {!!} }

-- with hidden argument
data Bar' : (Bool -> Bool) -> Set where
  baz' : {t : Void} -> Bar' λ { x' → {!!} }

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
{-# OPTIONS --without-K #-}
-- Expose all the core types and theorems.
module hott.core.theorems where

open import hott.core                   public
open import hott.core.equality.theorems public

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bounded vectors, basic types and operations
------------------------------------------------------------------------

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

module Data.Vec.Bounded.Base where

open import Level using (Level)
open import Data.Nat.Base
import Data.Nat.Properties as ℕₚ
open import Data.List.Base as List using (List)
open import Data.List.Extrema ℕₚ.≤-totalOrder
open import Data.List.Relation.Unary.All as All using (All)
import Data.List.Relation.Unary.All.Properties as Allₚ
open import Data.List.Membership.Propositional using (mapWith∈)
open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Vec.Base as Vec using (Vec)
open import Data.These.Base as These using (These)
open import Function
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

private
  variable
    a b c p : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Types

infix 4 _,_
record Vec≤ (A : Set a) (n : ℕ) : Set a where
  constructor _,_
  field {length} : ℕ
        vec      : Vec A length
        .bound   : length ≤ n

------------------------------------------------------------------------
-- Conversion functions

fromVec : ∀ {n} → Vec A n → Vec≤ A n
fromVec v = v , ℕₚ.≤-refl

padRight : ∀ {n} → A → Vec≤ A n → Vec A n
padRight a (vs , m≤n)
  with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n)
... | less-than-or-equal refl = vs Vec.++ Vec.replicate a

padLeft : ∀ {n} → A → Vec≤ A n → Vec A n
padLeft a as@(vs , m≤n)
  with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n)
... | less-than-or-equal {k} ∣as∣+k≡n
  with P.trans (ℕₚ.+-comm k (Vec≤.length as)) ∣as∣+k≡n
... | refl = Vec.replicate a Vec.++ vs

private
  split : ∀ {m n} k → m + k ≡ n → ⌊ k /2⌋ + (m + ⌈ k /2⌉) ≡ n
  split {m} {n} k eq = begin
    ⌊ k /2⌋ + (m + ⌈ k /2⌉) ≡⟨ ℕₚ.+-comm ⌊ k /2⌋ _ ⟩
    m + ⌈ k /2⌉ + ⌊ k /2⌋   ≡⟨ ℕₚ.+-assoc m ⌈ k /2⌉ ⌊ k /2⌋ ⟩
    m + (⌈ k /2⌉ + ⌊ k /2⌋) ≡⟨ P.cong (m +_) (ℕₚ.+-comm ⌈ k /2⌉ ⌊ k /2⌋) ⟩
    m + (⌊ k /2⌋ + ⌈ k /2⌉) ≡⟨ P.cong (m +_) (ℕₚ.⌊n/2⌋+⌈n/2⌉≡n k) ⟩
    m + k                   ≡⟨ eq ⟩
    n                       ∎ where open P.≡-Reasoning

padBoth : ∀ {n} → A → A → Vec≤ A n → Vec A n
padBoth aₗ aᵣ as@(vs , m≤n)
  with recompute (_ ℕₚ.≤″? _) (ℕₚ.≤⇒≤″ m≤n)
... | less-than-or-equal {k} ∣as∣+k≡n
  with split k ∣as∣+k≡n
... | refl = Vec.replicate {n = ⌊ k /2⌋} aₗ
      Vec.++ vs
      Vec.++ Vec.replicate {n = ⌈ k /2⌉} aᵣ

fromList : (as : List A) → Vec≤ A (List.length as)
fromList = fromVec ∘ Vec.fromList

toList : ∀ {n} → Vec≤ A n → List A
toList = Vec.toList ∘ Vec≤.vec

------------------------------------------------------------------------
-- Creating new Vec≤ vectors

replicate : ∀ {m n} .(m≤n : m ≤ n) → A → Vec≤ A n
replicate m≤n a = Vec.replicate a , m≤n

[] : ∀ {n} → Vec≤ A n
[] = Vec.[] , z≤n

infixr 5 _∷_
_∷_ : ∀ {n} → A → Vec≤ A n → Vec≤ A (suc n)
a ∷ (as , p) = a Vec.∷ as , s≤s p

------------------------------------------------------------------------
-- Modifying Vec≤ vectors

≤-cast : ∀ {m n} → .(m≤n : m ≤ n) → Vec≤ A m → Vec≤ A n
≤-cast m≤n (v , p) = v , ℕₚ.≤-trans p m≤n

≡-cast : ∀ {m n} → .(eq : m ≡ n) → Vec≤ A m → Vec≤ A n
≡-cast m≡n = ≤-cast (ℕₚ.≤-reflexive m≡n)

map : (A → B) → ∀ {n} → Vec≤ A n → Vec≤ B n
map f (v , p) = Vec.map f v , p

reverse : ∀ {n} → Vec≤ A n → Vec≤ A n
reverse (v , p) = Vec.reverse v , p

-- Align and Zip.

alignWith : (These A B → C) → ∀ {n} → Vec≤ A n → Vec≤ B n → Vec≤ C n
alignWith f (as , p) (bs , q) = Vec.alignWith f as bs , ℕₚ.⊔-least p q

zipWith : (A → B → C) → ∀ {n} → Vec≤ A n → Vec≤ B n → Vec≤ C n
zipWith f (as , p) (bs , q) = Vec.restrictWith f as bs , ℕₚ.m≤n⇒m⊓o≤n _ p

zip : ∀ {n} → Vec≤ A n → Vec≤ B n → Vec≤ (A × B) n
zip = zipWith _,_

align : ∀ {n} → Vec≤ A n → Vec≤ B n → Vec≤ (These A B) n
align = alignWith id

-- take and drop

take : ∀ {m} n → Vec≤ A m → Vec≤ A (n ⊓ m)
take             zero    _                = []
take             (suc n) (Vec.[] , p)     = []
take {m = suc m} (suc n) (a Vec.∷ as , p) = a ∷ take n (as , ℕₚ.≤-pred p)

drop : ∀ {m} n → Vec≤ A m → Vec≤ A (m ∸ n)
drop             zero    v                = v
drop             (suc n) (Vec.[] , p)     = []
drop {m = suc m} (suc n) (a Vec.∷ as , p) = drop n (as , ℕₚ.≤-pred p)

------------------------------------------------------------------------
-- Lifting a collection of bounded vectors to the same size

rectangle : List (∃ (Vec≤ A)) → ∃ (List ∘ Vec≤ A)
rectangle {A = A} rows = width , padded where

  sizes = List.map proj₁ rows
  width = max 0 sizes

  all≤ : All (λ v → proj₁ v ≤ width) rows
  all≤ = Allₚ.map⁻ (xs≤max 0 sizes)

  padded : List (Vec≤ A width)
  padded = mapWith∈ rows $ λ {x} x∈rows →
    ≤-cast (All.lookup all≤ x∈rows) (proj₂ x)


text:
{-# OPTIONS --erased-cubical --no-main --save-metas #-}

open import Agda.Builtin.Bool

open import Erased-cubical-Cubical

postulate
  f : Not-compiled → Bool

-- It is at the time of writing not possible to give a COMPILE GHC
-- pragma for f, because Not-compiled is not compiled.

{-# COMPILE GHC f = \_ -> True #-}


text:
{-# OPTIONS --copatterns --sized-types --without-K #-}
module PolyFinalCoalg where

open import Data.Product
open import Data.Nat
open import Data.Fin
open import Data.Unit as Unit
open import Data.Empty
open import Data.Vec hiding (_∈_; [_])
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Sum as Sum
open import Size

open import Poly

-- | Indexed product
_×ᵢ_ : {I : Set} → Fam I → Fam I → Fam I
(A ×ᵢ B) i = A i × B i

-- | Product of indexed functors
_×ᵢ'_ : {I J K : Set} →
        (Fam K → Fam I) → (Fam J → Fam I) → (Fam K × Fam J → Fam I)
(F ×ᵢ' G) (X , Y) = F X ×ᵢ G Y

record Isomorphic (A B : Set) : Set where
--  constructor isIso
  field
    f : A → B
    f⃖ : B → A
    is-invˡ : (a : A) → f⃖ (f a) ≡ a
    is-invʳ : (b : B) → f (f⃖ b) ≡ b

_≃_ = Isomorphic

_≃'_ : {I : Set} → Fam I → Fam I → Set
_≃'_ {I} A B = (i : I) → A i ≃ B i

-- | Avoid setoids for now
postulate
  Π'-ext : {I J : Set} {u : I → J} {P : Fam I} →
           (j : J) (f g : Π' u P j) →
           ((i : I) → (p : u i ≡ j) → f (i , p) ≡ g (i , p)) → f ≡ g
  Π'-ext' : {I J : Set} {u : I → J} {P : Fam I} →
           (f g : (i : I) → Π' u P (u i)) →
           ((i : I) → app i (f i) ≡ app i (g i)) → (i : I) → f i ≡ g i

-- | Dependent polynomials
record ParamPoly {I J : Set}  : Set₁ where
  constructor ppoly
  field
    -- J ←t- B -p→ A -s→ I
    A : Set  -- ^ Labels
    s : A → I
    B : Set
    p₁ p₂ : B → A
    t₁ : B → J
    t₂ : B → I

first : {I J : Set} → ParamPoly {I} {J} → DPoly {I} {J}
first (ppoly A s B p₁ p₂ t₁ t₂) = dpoly A s B p₁ t₁

second : {I J : Set} → ParamPoly {I} {J} → DPoly {I} {I}
second (ppoly A s B p₁ p₂ t₁ t₂) = dpoly A s B p₂ t₂

R : {I J : Set} → ParamPoly {I} {J} →
    (X : Fam J) → (Y : Fam I) → Fam I
R (ppoly A s B p₁ p₂ t₁ t₂) X Y =
  Σ' s (Π' p₁ ((t₁ *) X) ×ᵢ Π' p₂ ((t₂ *) Y))

data ⊤' (I : Set) : I → Set where
  tt : (i : I) → ⊤' I i

⊤'-unique : {I : Set} {i : I} → (x y : ⊤' I i) → x ≡ y
⊤'-unique (tt i) (tt .i) = refl

triv-param : {I J : Set} → (P : ParamPoly {I} {J}) →
             (Y : Fam I) → R P (⊤' J) Y ≃' T (second P) Y
triv-param {I} {J} (ppoly A s B p₁ p₂ t₁ t₂) Y i =
  record
  { f = f i
  ; f⃖ = g i
  ; is-invˡ = is-invˡ i
  ; is-invʳ = is-invʳ i
  }
  where
    P = ppoly A s B p₁ p₂ t₁ t₂

    f : (i : I) → R P (⊤' J) Y i → T (second P) Y i
    f ._ (ins a (v₁ , v₂)) = ins a v₂

    triv : (a : A) → Π' p₁ ((t₁ *) (⊤' J)) a
    triv a = abs (λ b → tt (t₁ b)) a

    g : (i : I) → T (second P) Y i → R P (⊤' J) Y i
    g ._ (ins a v) = ins a (triv a , v)

    is-invˡ : (i : I) → (x : R P (⊤' J) Y i) → g i (f i x) ≡ x
    is-invˡ ._ (ins a (v₁ , v₂)) =
      Σ'-eq a a (triv a , v₂) (v₁ , v₂)
      refl
      (×-eq (triv a) v₁ v₂ v₂
        (Π'-ext a (triv a) v₁ (lem a v₁))
        refl)
      where
        lem : (a : A) (v₁ :  Π' p₁ ((t₁ *) (⊤' J)) a)
              (i₁ : B) (p : p₁ i₁ ≡ a) →
              triv a (i₁ , p) ≡ v₁ (i₁ , p)
        lem ._ v₁ i₁ refl = ⊤'-unique (tt (t₁ i₁)) (app i₁ v₁)

    is-invʳ : (i : I) → (x : T (second P) Y i) → f i (g i x) ≡ x
    is-invʳ ._ (ins a x) = refl

triv : {I J : Set} (P : DPoly {I} {J}) → T P (⊤' J) ≃' toFam (DPoly.s P)
triv {I} {J} (dpoly A s E p t) i =
  record
  { f = f i
  ; f⃖ = g i
  ; is-invˡ = p₁ i
  ; is-invʳ = p₂ i
  }
  where
    P = dpoly A s E p t

    f : (i : I) → T P (⊤' J) i → toFam s i
    f ._ (ins a v) = (a , refl)

    g : (i : I) → toFam s i → T P (⊤' J) i
    g ._ (a , refl) = ins a (abs'' a v)
      where
        v : (b : E) → p b ≡ a → ⊤' J (t b)
        v b _ = tt (t b)

    p₁ : (i : I) → (x : T (dpoly A s E p t) (⊤' J) i) → g i (f i x) ≡ x
    p₁ ._ (ins a v) =
      Σ'-eq a a (abs'' a (λ b _ → tt (t b))) v
            refl
            (Π'-ext a (abs'' a (λ b _ → tt (t b))) v
                    (λ b p₂ → ⊤'-unique (tt (t b)) (v (b , p₂))))

    p₂ : (i : I) (b : toFam s i) → f i (g i b) ≡ b
    p₂ ._ (a , refl) = refl

foo : {A C P : Set} (B : Fam A) (D : Fam C) (Q : Fam P) (X : Set) →
      Σ (A × C) (λ {(a , c) → (B a → X) × (D c → Σ P (λ p → Q p → X)) })
      ≃
      Σ (A × Σ C (λ c → D c → P))
        (λ {(a , c , t) → ((B a → X) × ((Σ (D c) ((t *) Q)) → X))})
foo {A} {C} {P} B D Q X =
  record
  { f = f
  ; f⃖ = g
  ; is-invˡ = {!!}
  ; is-invʳ = {!!}
  }
  where
    f : Σ (A × C) (λ {(a , c) → (B a → X) × (D c → Σ P (λ p → Q p → X)) }) →
        Σ (A × Σ C (λ c → D c → P))
          (λ {(a , c , t) → ((B a → X) × ((Σ (D c) ((t *) Q)) → X))})
    f ((a , c) , t) =
      ((a , c , (λ d → proj₁ (proj₂ t d) ))
      , ((proj₁ t) , (λ { (d , q) → proj₂ (proj₂ t d) q})))

    g : Σ (A × Σ C (λ c → D c → P))
          (λ {(a , c , t) → ((B a → X) × ((Σ (D c) ((t *) Q)) → X))}) →
        Σ (A × C) (λ {(a , c) → (B a → X) × (D c → Σ P (λ p → Q p → X)) })
    g ((a , c , t₁) , t₂) =
      ((a , c)
      , (proj₁ t₂)
      , (λ d → (t₁ d , (λ q → proj₂ t₂ (d , q)))))

δ : {I : Set} → I → I × I
δ i = (i , i)

bar : {I K L : Set} (t : K → I) (v : L → I) (A : Fam K) (B : Fam L) →
      (Σ' t A ×ᵢ Σ' v B) ≃' (δ *) (Σ' (t ⊗ v) ((proj₁ *) A ×ᵢ (proj₂ *) B))
bar {I} {K} {L} t v A B i =
  record
  { f = f i
  ; f⃖ = g i
  ; is-invˡ = {!!}
  ; is-invʳ = {!!}
  }
  where
    f : (i : I) →
        (Σ' t A ×ᵢ Σ' v B) i → (Σ' (t ⊗ v) ((proj₁ *) A ×ᵢ (proj₂ *) B)) (i , i)
    f .(t k) (ins k x , y) = h k x (t k) refl y
      where
        h : (k : K) (x : A k) (i : I) (p : t k ≡ i) →
            (Σ' v B) i → (Σ' (t ⊗ v) ((proj₁ *) A ×ᵢ (proj₂ *) B)) (i , i)
        h k x ._ p (ins l y) =
          ins' (k , l)
               ((v l) , (v l))
               (⊗-eq {f = t} {v} k l p)
               (x , y)

    g : (i : I) →
        (Σ' (t ⊗ v) ((proj₁ *) A ×ᵢ (proj₂ *) B)) (i , i) → (Σ' t A ×ᵢ Σ' v B) i
    g i x =
      let
        k = proj₁ (p₁' x)
        l = proj₂ (p₁' x)

        q₁ : t k ≡ i
        q₁ = ×-eqˡ (p₌' x)

        q₂ : v l ≡ i
        q₂ = ×-eqʳ (p₌' x)

        u : A k × B l
        u = p₂' x
      in (ins' k i q₁ (proj₁ u) , ins' l i q₂ (proj₂ u))

_∣_ : {I J : Set} → Fam I → Fam J → Fam (I ⊎ J)
X ∣ Y = [ X , Y ]′

PB : {A₁ A₂ I : Set} → (A₁ → I) → (A₂ → I) → Set
PB {A₁} {A₂} f g = Σ[ x ∈ A₁ × A₂ ] (f (proj₁ x) ≡ g (proj₂ x))

PB-idx : {A₁ A₂ I : Set} → (f : A₁ → I) → (g : A₂ → I) → (PB f g → I)
PB-idx f _ ((x₁ , x₂) , _) = f x₁

_⊎'_ : {I J K : Set} → DPoly {I} {J} → DPoly {I} {K} → DPoly {I} {J ⊎ K}
(dpoly A₁ s₁ B₁ p₁ t₁) ⊎' (dpoly A₂ s₂ B₂ p₂ t₂)
  = dpoly A (PB-idx s₁ s₂) (U₁ ⊎ U₂) [ q₁ , q₂ ]′ (Sum.map (t₁ ∘ r₁) (t₂ ∘ r₂))
  where
    A = PB s₁ s₂
    U₁ = PB {A} (proj₁ ∘ proj₁) p₁
    U₂ = PB {A} (proj₂ ∘ proj₁) p₂
    q₁ : U₁ → A
    q₁ = proj₁ ∘ proj₁
    q₂ : U₂ → A
    q₂ = proj₁ ∘ proj₁
    r₁ : U₁ → B₁
    r₁ = proj₂ ∘ proj₁
    r₂ : U₂ → B₂
    r₂ = proj₂ ∘ proj₁

parametric-poly-by-sum : {I J K : Set} →
  (P : DPoly {I} {J}) → (Q : DPoly {I} {K}) →
  ∀ X Y → (T P ×ᵢ' T Q)(X , Y) ≃' T (P ⊎' Q) (X ∣ Y)
parametric-poly-by-sum {I} {J} P Q X Y i =
  record
  { f = f i
  ; f⃖ = g i
  ; is-invˡ = {!!}
  ; is-invʳ = {!!}
  }

  where

  f : (i : I) → (T P ×ᵢ' T Q) (X , Y) i → T (P ⊎' Q) (X ∣ Y) i
  f ._ (ins a v , y) = h a v (DPoly.s P a) refl y
    where
      h : (a : DPoly.A P)
          (v : Π' (DPoly.p P) (λ e → X (DPoly.t P e)) a)
          (i : I)
          (p : DPoly.s P a ≡ i) →
          T Q Y i → T (P ⊎' Q) (X ∣ Y) i
      h a₁ v₁ ._ p (ins a₂ v₂) = ins' a₃ (DPoly.s Q a₂) p₃ v₃
        where
          a₃ : DPoly.A (P ⊎' Q)
          a₃ = (a₁ , a₂) , p

          p₃ : DPoly.s (P ⊎' Q) a₃ ≡ DPoly.s Q a₂
          p₃ = trans refl p

          v₃ : Π' (DPoly.p (P ⊎' Q)) (λ e → (X ∣ Y) (DPoly.t (P ⊎' Q) e)) a₃
          v₃ = abs'' a₃ (v' a₃ refl)
            where
            v' : (u : DPoly.A (P ⊎' Q)) →
                 (a₁ , a₂) ≡ proj₁ u →
                 (i₁ : DPoly.E (P ⊎' Q)) →
                 DPoly.p (P ⊎' Q) i₁ ≡ u →
                 ((X ∣ Y) (DPoly.t (P ⊎' Q) i₁))
            v' u r (inj₁ ((.u , b) , q)) refl = v₁ (b , sym (trans (×-eqˡ r) q))
            v' u r (inj₂ ((.u , b) , q)) refl = v₂ (b , sym (trans (×-eqʳ r) q))

  g :  (i : I) → T (P ⊎' Q) (X ∣ Y) i → (T P ×ᵢ' T Q) (X , Y) i
  g ._ (ins x v) =
    (ins (proj₁ (proj₁ x)) v₁
    , ins' a₂ (DPoly.s P a₁) (sym (proj₂ x)) v₂)
    where
      a₁ = proj₁ (proj₁ x)
      a₂ = proj₂ (proj₁ x)

      v₁ : Π' (DPoly.p P) (((DPoly.t P) *) X) a₁
      v₁ = abs'' a₁ (v₁' a₁ refl)
        where
          v₁' : (a : DPoly.A P) (p : a₁ ≡ a) (b : DPoly.E P) →
                DPoly.p P b ≡ a → X (DPoly.t P b)
          v₁' ._ p b refl = v ((inj₁ ((x , b) , p)) , refl)

      v₂ : Π' (DPoly.p Q) (((DPoly.t Q) *) Y) a₂
      v₂ = abs'' a₂ (v₂' a₂ refl)
        where
          v₂' : (a : DPoly.A Q) (p : a₂ ≡ a) (b : DPoly.E Q) →
                DPoly.p Q b ≡ a → Y (DPoly.t Q b)
          v₂' ._ p b refl = v ((inj₂ ((x , b) , p)) , refl)

{-
 : {I J : Set} → (P : DPoly {I} {J}) → (Q : DPoly {I} {J}) →
       let H = λ X Y → ⟦ P ⟧ X ×ᵢ ⟦ Q ⟧
       in
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------------
--  Properties related with lists (using induction on the FOTC lists type)
------------------------------------------------------------------------------

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

module FOTC.Data.List.PropertiesByInductionI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Data.List
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Congruence properties

++-leftCong : ∀ {xs ys zs} → xs ≡ ys → xs ++ zs ≡ ys ++ zs
++-leftCong refl = refl

------------------------------------------------------------------------------
-- Totality properties

lengthList-N : ∀ {xs} → List xs → N (length xs)
lengthList-N = List-ind A A[] h
  where
  A : D → Set
  A ds = N (length ds)

  A[] : A []
  A[] = subst N (sym length-[]) nzero

  h : ∀ a {as} → A as → A (a ∷ as)
  h a {as} Aas = subst N (sym (length-∷ a as)) (nsucc Aas)

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

++-leftIdentity : ∀ xs → [] ++ xs ≡ xs
++-leftIdentity = ++-[]

++-assoc : ∀ {xs} → List xs → ∀ ys zs → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
++-assoc Lxs ys zs = List-ind A A[] h Lxs
  where
  A : D → Set
  A as = (as ++ ys) ++ zs ≡ as ++ ys ++ zs

  A[] : A []
  A[] = ([] ++ ys) ++ zs ≡⟨ ++-leftCong (++-leftIdentity ys) ⟩
        ys ++ zs         ≡⟨ sym (++-leftIdentity (ys ++ zs)) ⟩
        [] ++ ys ++ zs   ∎

  h : ∀ a {as} → A as → A (a ∷ as)
  h a {as} Aas =
    ((a ∷ as) ++ ys) ++ zs ≡⟨ ++-leftCong (++-∷ a as ys) ⟩
    (a ∷ (as ++ ys)) ++ zs ≡⟨ ++-∷ a (as ++ ys) zs ⟩
    a ∷ ((as ++ ys) ++ zs) ≡⟨ ∷-rightCong Aas ⟩
    a ∷ (as ++ ys ++ zs)   ≡⟨ sym (++-∷ a as (ys ++ zs)) ⟩
    (a ∷ as) ++ ys ++ zs   ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Thesis.BigStepSILR2 where

open import Data.Empty
open import Data.Unit.Base hiding (_≤_)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Binary hiding (_⇒_)
open import Data.Nat -- using (ℕ; zero; suc; decTotalOrder; _<_; _≤_)
open import Data.Nat.Properties
open import Thesis.FunBigStepSILR2

-- Standard relational big-step semantics, with step-indexes matching a small-step semantics.
-- Protip: doing this on ANF terms would be much easier.
data _⊢_↓[_]_ {Γ} (ρ : ⟦ Γ ⟧Context) : ∀ {τ} → Term Γ τ → ℕ → Val τ → Set where
  abs : ∀ {τ₁ τ₂} {t : Term (τ₁ • Γ) τ₂} →
    ρ ⊢ abs t ↓[ 0 ] closure t ρ
  app : ∀ n1 n2 n3 {Γ′ τ₁ τ₂ ρ′ v₂ v′} {t₁ : Term Γ (τ₁ ⇒ τ₂)} {t₂ : Term Γ τ₁} {t′ : Term (τ₁ • Γ′) τ₂} →
    ρ ⊢ t₁ ↓[ n1 ] closure t′ ρ′ →
    ρ ⊢ t₂ ↓[ n2 ] v₂ →
    (v₂ • ρ′) ⊢ t′ ↓[ n3 ] v′ →
    ρ ⊢ app t₁ t₂ ↓[ suc n1 + n2 + n3 ] v′
  var : ∀ {τ} (x : Var Γ τ) →
    ρ ⊢ var x ↓[ 0 ] (⟦ x ⟧Var ρ)
  lit : ∀ n →
    ρ ⊢ const (lit n) ↓[ 0 ] intV n

-- Silly lemmas for eval-dec-sound
module _ where
  Done-inj : ∀ {τ} m n {v1 v2 : Val τ} → Done v1 m ≡ Done v2 n → m ≡ n
  Done-inj _ _ refl = refl

  lem1 : ∀ n d → d ≢ suc (n + d)
  lem1 n d eq rewrite +-comm n d = m≢1+m+n d eq

  subd : ∀ n d → n + d ≡ d → n ≡ 0
  subd zero d eq = refl
  subd (suc n) d eq = ⊥-elim (lem1 n d (sym eq))

  comp∸ : ∀ a b → b ≤ a → suc a ∸ b ≡ suc (a ∸ b)
  comp∸ a zero le = refl
  comp∸ zero (suc b) ()
  comp∸ (suc a) (suc b) (s≤s le) = comp∸ a b le

  rearr∸ : ∀ a b c → c ≤ b → a + (b ∸ c) ≡ (a + b) ∸ c
  rearr∸ a b zero c≤b = refl
  rearr∸ a zero (suc c) ()
  rearr∸ a (suc b) (suc c) (s≤s c≤b) rewrite +-suc a b = rearr∸ a b c c≤b

  cancel∸ : ∀ a b → b ≤ a → a ∸ b + b ≡ a
  cancel∸ a zero b≤a = +-identityʳ a
  cancel∸ zero (suc b) ()
  cancel∸ (suc a) (suc b) (s≤s b≤a) rewrite +-suc (a ∸ b) b = cong suc (cancel∸ a b b≤a)

  lemR : ∀ {τ} n m {v1 v2 : Val τ} → Done v1 m ≡ Done v2 n → m ≡ n
  lemR n .n refl = refl

  lem2 : ∀ n n3 r → n3 ≤ n → n + n3 ≡ suc r → ∃ λ s → (n ≡ suc s)
  lem2 zero .0 r z≤n ()
  lem2 (suc n) n3 .(n + n3) le refl = n , refl

{-# TERMINATING #-}
eval-dec-sound : ∀ {Γ τ} → (t : Term Γ τ) → ∀ ρ v m n → eval t ρ m ≡ Done v n → ρ ⊢ t ↓[ m ∸ n ] v
eval-dec-sound (const (lit x)) ρ (intV v) m n eq with lemR n m eq
eval-dec-sound (const (lit x)) ρ (intV .x) m .m refl | refl rewrite n∸n≡0 m = lit x
eval-dec-sound (var x) ρ v m n eq with lemR n m eq
eval-dec-sound (var x) ρ .(⟦ x ⟧Var ρ) m .m refl | refl rewrite n∸n≡0 m  = var x
eval-dec-sound (abs t) ρ v m n eq with lemR n m eq
eval-dec-sound (abs t) ρ .(closure t ρ) m .m refl | refl rewrite n∸n≡0 m  = abs
eval-dec-sound (app s t) ρ v zero n ()
eval-dec-sound (app s t) ρ v (suc r) n eq with eval s ρ r | inspect (eval s ρ) r
eval-dec-sound (app s t) ρ v (suc r) n eq | (Done sv n1) | [ seq ] with eval t ρ n1 | inspect (eval t ρ) n1
eval-dec-sound (app s t) ρ v (suc r) n eq | (Done (closure st sρ) n1) | [ seq ] | (Done tv n2) | [ teq ] with eval st (tv • sρ) n2 | inspect (eval st (tv • sρ)) n2
eval-dec-sound (app s t) ρ .v (suc r) .n3 refl | (Done sv@(closure st sρ) n1) | [ seq ] | (Done tv n2) | [ teq ] | (Done v n3) | [ veq ] = body
  where
    n1≤r : n1 ≤ r
    n1≤r = eval-dec s ρ sv r n1 seq
    n2≤n1 : n2 ≤ n1
    n2≤n1 = eval-dec t ρ tv n1 n2 teq
    n3≤n2 : n3 ≤ n2
    n3≤n2 = eval-dec st (tv • sρ) v n2 n3 veq
    eval1 = eval-dec-sound s ρ sv r n1 seq
    eval2 = eval-dec-sound t ρ tv n1 n2 teq
    eval3 = eval-dec-sound st (tv • sρ) v n2 n3 veq
    l1 : suc r ∸ n3 ≡ suc (r ∸ n3)
    l1 = comp∸ r n3 (≤-trans n3≤n2 (≤-trans n2≤n1 n1≤r))
    l2 : suc r ∸ n3 ≡ suc (((r ∸ n1) + (n1 ∸ n2)) + (n2 ∸ n3))
    l2
      rewrite rearr∸ (r ∸ n1) n1 n2 n2≤n1 | cancel∸ r n1 n1≤r
      | rearr∸ (r ∸ n2) n2 n3 n3≤n2 | cancel∸ r n2 (≤-trans n2≤n1 n1≤r) = l1
    foo : ρ ⊢ app s t ↓[ suc (r ∸ n1 + (n1 ∸ n2) + (n2 ∸ n3)) ] v
    foo = app (r ∸ n1) (n1 ∸ n2) (n2 ∸ n3) {t₁ = s} {t₂ = t} {t′ = st} eval1 eval2 eval3
    body : ρ ⊢ app s t ↓[ suc r ∸ n3 ] v
    body rewrite l2 = foo
eval-dec-sound (app s t) ρ v (suc r) n () | (Done (closure st sρ) n1) | [ seq ] | (Done tv n2) | [ teq ] | Error | [ veq ]
eval-dec-sound (app s t) ρ v (suc r) n () | (Done (closure st sρ) n1) | [ seq ] | (Done tv n2) | [ teq ] | TimeOut | [ veq ]
eval-dec-sound (app s t) ρ v (suc r) n () | (Done sv n1) | [ seq ] | Error | [ teq ]
eval-dec-sound (app s t) ρ v (suc r) n () | (Done sv n1) | [ seq ] | TimeOut | [ teq ]
eval-dec-sound (app s t) ρ v (suc r) n () | Error | [ seq ]
eval-dec-sound (app s t) ρ v (suc r) n () | TimeOut | [ seq ]
-- ↦-sound : ∀ {Γ τ} ρ (x : Var Γ τ) →
--   ((Den.⟦ x ⟧Var) (⟦ ρ ⟧Context)) ≡ (⟦ (⟦ x ⟧Var) ρ ⟧Val)
-- ↦-sound (px • ρ) this = refl
-- ↦-sound (px • ρ) (that x) = ↦-sound ρ x

-- ↓-sound : ∀ {Γ τ ρ v} {t : Term Γ τ} →
--   ρ ⊢ t ↓ v →
--   ⟦ t ⟧Term ⟦ ρ ⟧Env ≡ ⟦ v ⟧Val
-- ↓-sound abs = refl
-- ↓-sound (app ↓₁ ↓₂ ↓′) rewrite ↓-sound ↓₁ | ↓-sound ↓₂ | ↓-sound ↓′ = refl
-- ↓-sound (var x) = ↦-sound _ x
-- ↓-sound (lit n) = refl

import Data.Integer as I
open I using (ℤ)

-- The extra "r" stands for "relational", because unlike relT and relV, rrelV
-- and rrelT are based on a *relational* big-step semantics.
mutual
  rrelT : ∀ {τ Γ} (t1 : Term Γ τ) (t2 : Term Γ τ) (ρ1 : ⟦ Γ ⟧Context) (ρ2 : ⟦ Γ ⟧Context) → ℕ → Set
  rrelT {τ} t1 t2 ρ1 ρ2 k =
    (v1 : Val τ) →
    ∀ j (j<k : j < k) →
    (ρ1⊢t1↓[j]v1 : ρ1 ⊢ t1 ↓[ j ] v1) →
    Σ[ v2 ∈ Val τ ] Σ[ n2 ∈ ℕ ] ρ2 ⊢ t2 ↓[ n2 ] v2 × rrelV τ v1 v2 (k ∸ j)

  rrelV : ∀ τ (v1 v2 : Val τ) → ℕ → Set
  rrelV nat (intV v1) (intV v2) n = Σ[ dv ∈ ℤ ] dv I.+ (I.+ v1) ≡ (I.+ v2)
  rrelV (σ ⇒ τ) (closure {Γ1} t1 ρ1) (closure {Γ2} t2 ρ2) n =
    Σ (Γ1 ≡ Γ2) λ { refl →
      ∀ (k : ℕ) (k<n : k < n) v1 v2 →
      (vv : rrelV σ v1 v2 k) →
      rrelT t1 t2 (v1 • ρ1) (v2 • ρ2) k
    }

rrelρ : ∀ Γ (ρ1 ρ2 : ⟦ Γ ⟧Context) → ℕ → Set
rrelρ ∅ ∅ ∅ n = ⊤
rrelρ (τ • Γ) (v1 • ρ1) (v2 • ρ2) n = rrelV τ v1 v2 n × rrelρ Γ ρ1 ρ2 n

⟦_⟧RelVar : ∀ {Γ τ n} (x : Var Γ τ) {ρ1 ρ2 : ⟦ Γ ⟧Context} →
  rrelρ Γ ρ1 ρ2 n →
  rrelV τ (⟦ x ⟧Var ρ1) (⟦ x ⟧Var ρ2) n
⟦ this ⟧RelVar {v1 • ρ1} {v2 • ρ2} (vv , ρρ) = vv
⟦ that x ⟧RelVar {v1 • ρ1} {v2 • ρ2} (vv , ρρ) = ⟦ x ⟧RelVar ρρ

rrelV-mono : ∀ m n → m ≤ n → ∀ τ v1 v2 → rrelV τ v1 v2 n → rrelV τ v1 v2 m
rrelV-mono m n m≤n nat (intV v1) (intV v2) vv = vv
rrelV-mono m n m≤n (σ ⇒ τ) (closure t1 ρ1) (closure t2 ρ2) (refl , ff) = refl , λ k k≤m → ff k (≤-trans k≤m m≤n)

rrelρ-mono : ∀ m n → m ≤ n → ∀ Γ ρ1 ρ2 → rrelρ Γ ρ1 ρ2 n → rrelρ Γ ρ1 ρ2 m
rrelρ-mono m n m≤n ∅ ∅ ∅ tt = tt
rrelρ-mono m n m≤n (τ • Γ) (v1 • ρ1) (v2 • ρ2) (vv , ρρ) = rrelV-mono m n m≤n _ v1 v2 vv , rrelρ-mono m n m≤n Γ ρ1 ρ2 ρρ

rfundamentalV : ∀ {Γ τ} (x : Var Γ τ) → (n : ℕ) → (ρ1 ρ2 : ⟦ Γ ⟧Context) (ρρ : rrelρ Γ ρ1 ρ2 n) → rrelT (var x) (var x) ρ1 ρ2 n
rfundamentalV x n ρ1 ρ2 ρρ .(⟦ x ⟧Var ρ1) .0 j<n (var .x) = ⟦ x ⟧Var ρ2 , 0 , (var x) , ⟦ x ⟧RelVar ρρ

bar : ∀ m {n o} → o ≤ n → m ≤ (m + n) ∸ o
bar m {n} {o} o≤n rewrite +-∸-assoc m o≤n = m≤m+n m (n ∸ o)

suc∸ : ∀ m n → n ≤ m → suc (m ∸ n) ≡ suc m ∸ n
suc∸ m zero z≤n = refl
suc∸ (suc m) (suc n) (s≤s n≤m) = suc∸ m n n≤m

suc∸suc : ∀ m n → n < m → suc (m ∸ suc n) ≡ m ∸ n
suc∸suc (suc m) zero (s≤s n<m) = refl
suc∸suc (suc m) (suc n) (s≤s n<m) = suc∸suc m n n<m

m≡m∸1+1 : ∀ m {n} → n < m → m ≡ suc (m ∸ 1)
m≡m∸1+1 (suc m) (s≤s n<m) = refl

m∸[n+1]<m : ∀ m n → n < m → m ∸ suc n < m
m∸[n+1]<m (suc m) zero (s≤s n<m) = s≤s ≤-refl
m∸[n+1]<m (suc m) (suc n) (s≤s n<m) rewrite sym (suc∸suc m n n<m) = ≤-step (m∸[n+1]<m m n n<m)

sub∸ : ∀ m n o → m + n ≤ o → n ≤ o ∸ m
sub∸ m n o n+m≤o rewrite +-comm m n | cong (_≤ o ∸ m) (sym (m+n∸n≡m n m)) = ∸-mono n+m≤o (≤-refl {m})

rfundamental : ∀ {Γ τ} (t : Term Γ τ) → (n : ℕ) → (ρ1 ρ2 : ⟦ Γ ⟧Context) (ρρ : rrelρ Γ ρ1 ρ2 n) → rrelT t t ρ1 ρ2 n
rfundamental (var x) n ρ1 ρ2 ρρ = rfundamentalV x n ρ1 ρ2 ρρ
rfundamental (const (lit x)) n ρ1 ρ2 ρρ .(intV x) .0 j<n (lit .x) = intV x , 0 , lit x , I.+ 0 , refl
rfundamental (abs t) n ρ1 ρ2 ρρ .(closure t ρ1) .0 j<n abs = closure t ρ2 , 0 , abs , refl , (λ k k<n v1 v2 vv v3 j j<k ρ1⊢t1↓[j]v1 → rfundamental t k (v1 • ρ1) (v2 • ρ2) (vv , rrelρ-mono k n (lt1 k<n) _ _ _ ρρ) v3 j j<k ρ1⊢t1↓[j]v1 )
rfundamental (app s t) n ρ1 ρ2 ρρ v1 .(suc (n1 + n2 + n3)) 1+n1+n2+n3<n (app n1 n2 n3 ρ1⊢t1↓[j]v1 ρ1⊢t1↓[j]v2 ρ1⊢t1↓[j]v3) = body
  where
    open ≤-Reasoning
    n1≤sum : n1 ≤ n1 + n2 + n3
    n1≤sum rewrite +-assoc n1 n2 n3 = m≤m+n n1 (n2 + n3)
    n1<n : n1 < n
    n1<n = ≤-trans (s≤s (≤-step n1≤sum)) 1+n1+n2+n3<n

    n2≤sum : n2 ≤ n1 + n2 + n3
    n2≤sum rewrite +-assoc n1 n2 n3 = ≤-steps {n2} {n2 + n3} n1 (m≤m+n n2 n3)
    n2<n : n2 < n
    n2<n = ≤-trans (s≤s (≤-step n2≤sum)) 1+n1+n2+n3<n
    n1+n2<n : n1 + n2 < n
    n1+n2<n = ≤-trans (s≤s (≤-step (m≤m+n (n1 + n2) n3))) 1+n1+n2+n3<n
    n2+n1<n : n2 + n1 < n
    n2+n1<n rewrite +-comm n2 n1 = n1+n2<n

    n1+n3≤sum : n1 + n3 ≤ (n1 + n2) + n3
    n1+n3≤sum = m≤m+n n1 n2 +-mono (≤-refl {n3})
    foo : suc n2 ≡ suc (n1 + n2 + n3) ∸ (n1 + n3)
    foo rewrite cong suc (sym (m+n∸n≡m n2 (n1 + n3))) | sym (+-assoc n2 n1 n3) | +-comm n2 n1 = suc∸ (n1 + n2 + n3) (n1 + n3) n1+n3≤sum
    n2<n∸n1 : n2 < n ∸ n1
    n2<n∸n1 rewrite foo = ∸-mono {suc (n1 + n2 + n3)} {n} {n1 + n3} {n1} (lt1 1+n1+n2+n3<n) (m≤m+n n1 n3)
    n-[1+n1+n2]<n-n1 : n ∸ n1 ∸ suc n2 < n ∸ n1
    n-[1+n1+n2]<n-n1 = m∸[n+1]<m (n ∸ n1) n2 n2<n∸n1

    n-[1+n1+n2]<n-n2 : n ∸ n1 ∸ suc n2 < n ∸ n2
    n-[1+n1+n2]<n-n2 rewrite ∸-+-assoc n n1 (suc n2) | +-suc n1 n2 | +-comm n1 n2 | suc∸suc n (n2 + n1) n2+n1<n | sym (∸-+-assoc n n2 n1) = n∸m≤n n1 (n ∸ n2)

    baz : n1 + suc (n2 + suc n3) ≤ n
    baz rewrite +-suc n2 n3 | +-suc n1 (suc (n2 + n3)) | +-suc n1 (n2 + n3) | +-assoc n1 n2 n3 = 1+n1+n2+n3<n
    n3<n-n1-[1+n2] : n3 < n ∸ n1 ∸ suc n2
    n3<n-n1-[1+n2] = sub∸ (suc n2) (suc n3) (n ∸ n1) (sub∸ n1 (suc (n2 + suc n3)) n baz)

    l1 : suc (n1 + n2 + n3) ≡ n1 + suc n2 + n3
    l1 = cong (_+ n3) (sym (+-suc n1 n2))
    n-1+sum≡alt : n ∸ suc (n1 + n2 + n3) ≡ n ∸ n1 ∸ suc n2 ∸ n3
    n-1+sum≡alt rewrite l1 | sym (∸-+-assoc n (n1 + suc n2) n3) | sym (∸-+-assoc n n1 (suc n2)) = refl

    body : Σ[ v2 ∈ Val _ ] Σ[ tn ∈ ℕ ] ρ2 ⊢ app s t ↓[ tn ] v2 × rrelV _ v1 v2 (n ∸ suc (n1 + n2 + n3))
    body with rfundamental s n ρ1 ρ2 ρρ _ n1 n1<n ρ1⊢t1↓[j]v1 | rfundamental t n ρ1 ρ2 ρρ _ n2 n2<n ρ1⊢t1↓[j]v2
    ... | sv2@(closure st2 sρ2) , sn2 , ρ2⊢s↓ , refl , sv1v2 | tv2 , tn2 , ρ2⊢t↓ , tv1v2 with sv1v2 (n ∸ n1 ∸ suc n2) n-[1+n1+n2]<n-n1 _ tv2 (rrelV-mono (n ∸ n1 ∸ suc n2) (n ∸ n2) (lt1 n-[1+n1+n2]<n-n2) _ _ tv2 tv1v2) v1 n3 n3<n-n1-[1+n2]  ρ1⊢t1↓[j]v3
    ... | v2 , stn , ρ2⊢st2↓ , vv rewrite n-1+sum≡alt = v2 , suc (sn2 + tn2 + stn) , app _ _ _ ρ2⊢s↓ ρ2⊢t↓  ρ2⊢st2↓ , vv

mutual
  rrelT3 : ∀ {τ Γ ΔΓ} (t1 : Term Γ τ) (dt : Term ΔΓ (Δτ τ)) (t2 : Term Γ τ) (ρ1 : ⟦ Γ ⟧Context) (dρ : ⟦ ΔΓ ⟧Context) (ρ2 : ⟦ Γ ⟧Context) → ℕ → Set
  rrelT3 {τ} t1 dt t2 ρ1 dρ ρ2 k =
    (v1 v2 : Val τ) →
    ∀ j n2 (j<k : j < k) →
    (ρ1⊢t1↓[j]v1 : ρ1 ⊢ t1 ↓[ j ] v1) →
    (ρ2⊢t2↓[n2]v2 : ρ2 ⊢ t2 ↓[ n2 ] v2) →
    Σ[ dv ∈ Val (Δτ τ) ] Σ[ dn ∈ ℕ ]
    dρ ⊢ dt ↓[ dn ] dv ×
    rrelV3 τ v1 dv v2 (k ∸ j)

  rrelV3 : ∀ τ (v1 : Val τ) (dv : Val (Δτ τ)) (v2 : Val τ) → ℕ → Set
  rrelV3 nat (intV v1) (intV dv) (intV v2) n = dv + v1 ≡ v2

  -- XXX What we want for rrelV3:
  -- rrelV3 (σ ⇒ τ) (closure {Γ1} t1 ρ1) (dclosure dt dρ) (closure {Γ2} t2 ρ2) n =
  --     Σ (Γ1 ≡ Γ2) λ { refl →
  --       ∀ (k : ℕ) (k<n : k < n) v1 dv v2 →
  --       rrelV3 σ v1 dv v2 k →
  --       rrelT3
  --         t1
  --         dt
  --         t2
  --         (v1 • ρ1)
  --         (dv • v1 • dρ)
  --         (v2 • ρ2) k
  --     }

  -- However, we don't have separate change values, so we write:

  rrelV3 (σ ⇒ τ) (closure {Γ1} t1 ρ1) (closure dt' dρ) (closure {Γ2} t2 ρ2) n =
      -- Require a proof that the two contexts match:
      Σ (Γ1 ≡ Γ2) λ { refl →
        ∀ (k : ℕ) (k<n : k < n) v1 dv v2 →
        rrelV3 σ v1 dv v2 k →
        rrelT3
          t1
          -- XXX The next expression is wrong.
          -- rrelV3 should require dv to be a change closure,
          -- (λ x dx . dt , dρ) or (dclosure dt dρ).
          -- Then, here we could write as conclusion.
          -- rrelT3 t1 dt t2 (v1 • ρ1) (dv • v1 • dρ) (v2 • ρ2) k

          -- Instead, with this syntax I can just match dv as a normal closure,
          -- closure dt' dρ or (λ x . dt', dρ), where we hope that dt' evaluates
          -- to λ dx. dt. So, instead of writing dt, I must write dt' dx where
          -- dx is a newly bound variable (hence, var this), and dt' must be
          -- weakened once. Hence, we write instead:
          (app (weaken (drop (Δτ σ) • ≼-refl) dt') (var this))
          t2
          (v1 • ρ1)
          (dv • v1 • dρ)
          (v2 • ρ2)
          k
      }

ΔΓ : Context → Context
ΔΓ ∅ = ∅
ΔΓ (τ • Γ) = Δτ τ • ΔΓ Γ

rrelρ3 : ∀ Γ (ρ1 : ⟦ Γ ⟧Context) (dρ : ⟦ ΔΓ Γ ⟧Context) (ρ2 : ⟦ Γ ⟧Context) → ℕ → Set
rrelρ3 ∅ ∅ ∅ ∅ n = ⊤
rrelρ3 (τ • Γ) (v1 • ρ1) (dv • dρ) (v2 • ρ2) n = rrelV3 τ v1 dv v2 n × rrelρ3 Γ ρ1 dρ ρ2 n

derive-var : ∀ {Γ τ} → Var Γ τ → Var (ΔΓ Γ) (Δτ τ)
derive-var this = this
derive-var (that x) = that (derive-var x)

⟦_⟧RelVar3 : ∀ {Γ τ n} (x : Var Γ τ)
  {ρ1 : ⟦ Γ ⟧Context} {dρ : ⟦ ΔΓ Γ ⟧Context} {ρ2 : ⟦ Γ ⟧Context} →
  rrelρ3 Γ ρ1 dρ ρ2 n →
  rrelV3 τ (⟦ x ⟧Var ρ1) (⟦ derive-var x ⟧Var dρ) (⟦ x ⟧Var ρ2) n
⟦ this ⟧RelVar3 {v1 • ρ1} {dv • dρ} {v2 • ρ2} (vv , ρρ) = vv
⟦ that x ⟧RelVar3 {v1 • ρ1} {dv • dρ} {v2 • ρ2} (vv , ρρ) = ⟦ x ⟧RelVar3 ρρ

rfundamentalV3 : ∀ {Γ τ} (x : Var Γ τ) → (n : ℕ) → (ρ1 : ⟦ Γ ⟧Context) (dρ : ⟦ ΔΓ Γ ⟧Context) (ρ2 : ⟦ Γ ⟧Context) (ρρ : rrelρ3 Γ ρ1 dρ ρ2 n) → rrelT3 (var x) (var (derive-var x)) (var x) ρ1 dρ ρ2 n
rfundamentalV3 x n ρ1 dρ ρ2 ρρ .(⟦ x ⟧Var ρ1) .(⟦ x ⟧Var ρ2) .0 .0 j<n (var .x) (var .x) = ⟦ derive-var x ⟧Var dρ , 0 , (var (derive-var x)) , ⟦ x ⟧RelVar3 ρρ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import LogicalFormulae
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Subgroups.Definition
open import Rings.Cosets
open import Groups.Lemmas
open import Setoids.Functions.Lemmas
open import Rings.Ideals.Definition

module Rings.Ideals.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open import Rings.Divisible.Definition R

idealPredForKernel : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → A → Set d
idealPredForKernel {T = T} R2 {f} fHom a = Setoid._∼_ T (f a) (Ring.0R R2)

idealPredForKernelWellDefined : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → {x y : A} → (Setoid._∼_ S x y) → (idealPredForKernel R2 fHom x → idealPredForKernel R2 fHom y)
idealPredForKernelWellDefined {T = T} R2 {f} fHom a x=0 = Equivalence.transitive (Setoid.eq T) (GroupHom.wellDefined (RingHom.groupHom fHom) (Equivalence.symmetric (Setoid.eq S) a)) x=0

kernelIdealIsIdeal : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} {R2 : Ring T _+2_ _*2_} {f : A → C} (fHom : RingHom R R2 f) → Ideal R (idealPredForKernel R2 fHom)
Subgroup.isSubset (Ideal.isSubgroup (kernelIdealIsIdeal {R2 = R2} fHom)) = idealPredForKernelWellDefined R2 fHom
Subgroup.closedUnderPlus (Ideal.isSubgroup (kernelIdealIsIdeal {T = T} {R2 = R2} fHom)) {x} {y} fx=0 fy=0 = transitive (transitive (GroupHom.groupHom (RingHom.groupHom fHom)) (+WellDefined fx=0 fy=0)) identLeft
  where
    open Ring R2
    open Group (Ring.additiveGroup R2)
    open Setoid T
    open Equivalence eq
Subgroup.containsIdentity (Ideal.isSubgroup (kernelIdealIsIdeal fHom)) = imageOfIdentityIsIdentity (RingHom.groupHom fHom)
Subgroup.closedUnderInverse (Ideal.isSubgroup (kernelIdealIsIdeal {T = T} {R2 = R2} fHom)) {x} fx=0 = zeroImpliesInverseZero (RingHom.groupHom fHom) fx=0
  where
    open Ring R2
    open Group (Ring.additiveGroup R2)
    open Setoid T
    open Equivalence eq
Ideal.accumulatesTimes (kernelIdealIsIdeal {T = T} {R2 = R2} {f = f} fHom) {x} {y} fx=0 = transitive (RingHom.ringHom fHom) (transitive (Ring.*WellDefined R2 fx=0 reflexive) (transitive (Ring.*Commutative R2) (Ring.timesZero R2 {f y})))
  where
    open Setoid T
    open Equivalence eq

open Ring R
open Group additiveGroup
open Setoid S
open Equivalence eq

translate : {c : _} {pred : A → Set c} → (i : Ideal R pred) → {a : A} → pred a → pred (inverse (Ring.0R (cosetRing R i)) + a)
translate {a} i predA = Ideal.isSubset i (transitive (symmetric identLeft) (+WellDefined (symmetric (invIdent additiveGroup)) reflexive)) predA
translate' : {c : _} {pred : A → Set c} → (i : Ideal R pred) → {a : A} → pred (inverse (Ring.0R (cosetRing R i)) + a) → pred a
translate' i = Ideal.isSubset i (transitive (+WellDefined (invIdent additiveGroup) reflexive) identLeft)

inverseImageIsIdeal : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} {R2 : Ring T _+2_ _*2_} {f : C → A} (fHom : RingHom R2 R f) → {e : _} {pred : A → Set e} → (i : Ideal R pred) → Ideal R2 (inverseImagePred {S = T} {S} {f} (GroupHom.wellDefined (RingHom.groupHom fHom)) (Ideal.isSubset i))
Subgroup.isSubset (Ideal.isSubgroup (inverseImageIsIdeal {T = T} fHom i)) = inverseImageWellDefined {S = T} {S} (GroupHom.wellDefined (RingHom.groupHom fHom)) (Ideal.isSubset i)
Subgroup.closedUnderPlus (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) {g} {h} (c , (prC ,, fg=c)) (d , (prD ,, fh=d)) = (c + d) , (Ideal.closedUnderPlus i prC prD ,, transitive (GroupHom.groupHom (RingHom.groupHom fHom)) (+WellDefined fg=c fh=d))
Subgroup.containsIdentity (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) = 0G , (Ideal.containsIdentity i ,, imageOfIdentityIsIdentity (RingHom.groupHom fHom))
Subgroup.closedUnderInverse (Ideal.isSubgroup (inverseImageIsIdeal fHom i)) (a , (prA ,, fg=a)) = inverse a , (Ideal.closedUnderInverse i prA ,, transitive (homRespectsInverse (RingHom.groupHom fHom)) (inverseWellDefined additiveGroup fg=a))
Ideal.accumulatesTimes (inverseImageIsIdeal {_*2_ = _*2_} {f = f} fHom i) {g} {h} (a , (prA ,, fg=a)) = (a * f h) , (Ideal.accumulatesTimes i prA ,, transitive (RingHom.ringHom fHom) (*WellDefined fg=a reflexive))

memberDividesImpliesMember : {a b : A} → {c : _} → {pred : A → Set c} → (i : Ideal R pred) → pred a → a ∣ b → pred b
memberDividesImpliesMember {a} {b} i pA (s , as=b) = Ideal.isSubset i as=b (Ideal.accumulatesTimes i pA)

generatorZeroImpliesMembersZero : {x : A} → generatedIdealPred R 0R x → x ∼ 0R
generatorZeroImpliesMembersZero {x} (a , b) = transitive (symmetric b) (transitive *Commutative timesZero)


text:
------------------------------------------------------------------------------
-- Propositional equality
------------------------------------------------------------------------------

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

-- Tested with the development version of Agda on 15 June 2012.

module FOT.Agsy.NoStd.MyPropositionalEquality where

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Relation/Binary/Core.agda).
infix 7 _≡_

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

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

-- Identity properties

sym : ∀ {A} → {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {A} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl y≡z = y≡z

cong : {A B : Set} (f : A → B) → ∀ {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

module ≡-Reasoning where
  -- We add 3 to the fixities of the Agda standard library 0.8.1 (see
  -- Relation/Binary/PreorderReasoning.agda).
  infix  7 _≃_
  infix  4 begin_
  infixr 5 _≡⟨_⟩_
  infix  6 _∎

  ----------------------------------------------------------------------------
  -- Adapted from the Agda standard library 0.8.1 (see
  -- Relation/Binary/PreorderReasoning.agda).
  private
    data _≃_ {A : Set}(x y : A) : Set where
      prf : x ≡ y → x ≃ y

  begin_ : {A : Set}{x y : A} → x ≃ y → x ≡ y
  begin prf x≡y = x≡y

  _≡⟨_⟩_ : {A : Set}(x : A){y z : A} → x ≡ y → y ≃ z → x ≃ z
  _ ≡⟨ x≡y ⟩ prf y≡z = prf (trans x≡y y≡z)

  _∎ : {A : Set}(x : A) → x ≃ x
  _∎ _ = prf refl


text:
{-

  Importing and re-exporting this module allows for (constrained) natural number
   and negative integer literals for any type (e.g. Int, ℕ₋₁, ℕ₋₂, ℕ₊₁).

-}
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.Nat.Literals where

open import Agda.Builtin.FromNat public
  renaming (Number to HasFromNat)
open import Agda.Builtin.FromNeg public
  renaming (Negative to HasFromNeg)
open import Cubical.Data.Unit.Base public

-- Natural number literals for ℕ

open import Agda.Builtin.Nat renaming (Nat to ℕ)

instance
  fromNatℕ : HasFromNat ℕ
  fromNatℕ = record { Constraint = λ _ → Unit ; fromNat = λ n → n }

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import HoTT
open import homotopy.LoopSpaceCircle

-- This file is temporarily put in the cw/ directory for
-- development, but it actually belongs to somewhere else.

module homotopy.SphereEndomorphism where

  ⊙SphereS-endo-out : ∀ n
    → Trunc 0 (⊙Sphere (S n) ⊙→ ⊙Sphere (S n))
    → Trunc 0 ( Sphere (S n)  →  Sphere (S n))
  ⊙SphereS-endo-out n = Trunc-rec Trunc-level ([_] ∘ fst)

  -- For [S¹], the pointedness is free because of the commutativity of its loop space.

  -- favonia: maybe one can simplify the proofs through
  --          an intermediate type [Σ S¹ (λ x → x == x)]?

  private
    ⊙S¹-endo-in'' : (base* : S¹) (loop* : base* == base*) → (⊙S¹ ⊙→ ⊙S¹)
    ⊙S¹-endo-in'' = S¹-elim
      (λ loop* → S¹-rec base loop* , idp)
      (↓-app→cst-in λ r → ap (λ loop* → (S¹-rec base loop* , idp)) (lemma₀ r)) where
      abstract
        lemma₀ : ∀ {loop₁ loop₂}
          → loop₁ == loop₂ [ (λ x → x == x) ↓ loop ]
          → loop₁ == loop₂
        lemma₀ {loop₁} {loop₂} p = anti-whisker-right loop $
          loop₁ ∙ loop
            =⟨ ↓-idf=idf-out' p ⟩
          loop ∙' loop₂
            =⟨ ∙'=∙ loop loop₂ ⟩
          loop ∙ loop₂
            =⟨ ΩS¹-is-abelian loop loop₂ ⟩
          loop₂ ∙ loop
            =∎

    ⊙S¹-endo-in' : (S¹ → S¹) → (⊙S¹ ⊙→ ⊙S¹)
    ⊙S¹-endo-in' f = ⊙S¹-endo-in'' (f base) (ap f loop)

  ⊙S¹-endo-in : Trunc 0 (S¹ → S¹) → Trunc 0 (⊙S¹ ⊙→ ⊙S¹)
  ⊙S¹-endo-in = Trunc-fmap ⊙S¹-endo-in'

  abstract
    ⊙S¹-endo-in-η : ∀ f → ⊙S¹-endo-in (⊙SphereS-endo-out 0 f) == f
    ⊙S¹-endo-in-η = Trunc-elim (λ _ → =-preserves-set Trunc-level)
      λ{(f , pt) → ap [_] $
        ⊙S¹-endo-in''-shifted pt (ap f loop) ∙ ⊙λ= (S¹-rec-η f) idp}
      where
      -- free one end to apply identification elimination
      ⊙S¹-endo-in''-shifted : {base* : S¹}
        (shift : base* == base) (loop* : base* == base*)
        → ⊙S¹-endo-in'' base* loop* == (S¹-rec base* loop* , shift)
      ⊙S¹-endo-in''-shifted idp _ = idp

    ⊙S¹-endo-out-β : ∀ f → ⊙SphereS-endo-out 0 (⊙S¹-endo-in f) == f
    ⊙S¹-endo-out-β = Trunc-elim (λ _ → =-preserves-level Trunc-level)
      λ f → ! (ap (λ f → [ fst (⊙S¹-endo-in' f) ]) (λ= $ S¹-rec-η f))
          ∙ ⊙S¹-endo-out'-β (f base) (ap f loop)
          ∙ ap [_] (λ= $ S¹-rec-η f)
      where
        -- free [base*] to apply circle elimination
        ⊙S¹-endo-out'-β : (base* : S¹) (loop* : base* == base*)
          →  [ fst (⊙S¹-endo-in' (S¹-rec base* loop*)) ]
          == [ S¹-rec base* loop* ] :> Trunc 0 (S¹ → S¹)
        ⊙S¹-endo-out'-β = S¹-elim
          (λ loop* → ap (λ loop* → [ S¹-rec base loop* ]) (S¹Rec.loop-β base loop*))
          (prop-has-all-paths-↓ $ Π-is-prop λ loop* → Trunc-level {n = 0} _ _)

  ⊙S¹-endo-out-is-equiv : is-equiv (⊙SphereS-endo-out 0)
  ⊙S¹-endo-out-is-equiv = is-eq _ ⊙S¹-endo-in ⊙S¹-endo-out-β ⊙S¹-endo-in-η

  -- For [Sphere (S (S n))], the pointedness is free because of its connectivity.

  private
    SphereSS-conn : ∀ n → is-connected 1 (Sphere (S (S n)))
    SphereSS-conn n = connected-≤T (≤T-+2+-l 1 (-2≤T ⟨ n ⟩₋₂)) (Sphere-conn (S (S n)))

    SphereSS-conn-path : ∀ n (x y : Sphere (S (S n))) → is-connected 0 (x == y)
    SphereSS-conn-path n x y = path-conn (SphereSS-conn n)

    SphereSS-has-all-trunc-paths : ∀ n (x y : Sphere (S (S n))) → Trunc 0 (x == y)
    SphereSS-has-all-trunc-paths n x y = –> (Trunc=-equiv [ x ] [ y ])
      (contr-has-all-paths (SphereSS-conn n) [ x ] [ y ])

  ⊙SphereSS-endo-in : ∀ n
    → Trunc 0 ( Sphere (S (S n))  →  Sphere (S (S n)))
    → Trunc 0 (⊙Sphere (S (S n)) ⊙→ ⊙Sphere (S (S n)))
  ⊙SphereSS-endo-in n = Trunc-rec Trunc-level λ f →
    Trunc-rec Trunc-level (λ pt → [ f , pt ])
      (SphereSS-has-all-trunc-paths n (f north) north)

  abstract
    ⊙SphereSS-endo-in-η : ∀ n f → ⊙SphereSS-endo-in n (⊙SphereS-endo-out (S n) f) == f
    ⊙SphereSS-endo-in-η n = Trunc-elim (λ _ → =-preserves-set Trunc-level)
      λ{(f , pt) → ap (Trunc-rec Trunc-level (λ pt → [ f , pt ]))
        (contr-has-all-paths (SphereSS-conn-path n (f north) north)
          (SphereSS-has-all-trunc-paths n (f north) north) [ pt ])}

    ⊙SphereSS-endo-out-β : ∀ n f → ⊙SphereS-endo-out (S n) (⊙SphereSS-endo-in n f) == f
    ⊙SphereSS-endo-out-β n = Trunc-elim (λ _ → =-preserves-set Trunc-level)
      λ f → Trunc-elim
        {P = λ pt → ⊙SphereS-endo-out (S n) (Trunc-rec Trunc-level (λ pt → [ f , pt ]) pt) == [ f ]}
        (λ _ → =-preserves-set Trunc-level)
        (λ pt → idp) (SphereSS-has-all-trunc-paths n (f north) north)

  ⊙SphereSS-endo-out-is-equiv : ∀ n → is-equiv (⊙SphereS-endo-out (S n))
  ⊙SphereSS-endo-out-is-equiv n = is-eq
    (⊙SphereS-endo-out (S n)) (⊙SphereSS-endo-in n)
    (⊙SphereSS-endo-out-β n) (⊙SphereSS-endo-in-η n)

  -- the unified interface

  ⊙SphereS-endo-out-is-equiv : ∀ n → is-equiv (⊙SphereS-endo-out n)
  ⊙SphereS-endo-out-is-equiv 0 = ⊙S¹-endo-out-is-equiv
  ⊙SphereS-endo-out-is-equiv (S n) = ⊙SphereSS-endo-out-is-equiv n

  ⊙SphereS-endo-in : ∀ n
    → Trunc 0 ( Sphere (S n)  →  Sphere (S n))
    → Trunc 0 (⊙Sphere (S n) ⊙→ ⊙Sphere (S n))
  ⊙SphereS-endo-in n = is-equiv.g (⊙SphereS-endo-out-is-equiv n)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
open import Common.Prelude
open import Common.Reflect
open import Common.Equality

postulate
  trustme : ∀ {a} {A : Set a} {x y : A} → x ≡ y

magic : Term → Term
magic _ = def (quote trustme) []

id : ∀ {a} {A : Set a} → A → A
id x = x

science : Term → Term
science _ = def (quote id) []

by-magic : ∀ n → n + 4 ≡ 3
by-magic n = tactic magic

by-science : ∀ n → 0 + n ≡ n
by-science n = tactic science | refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
-- 2010-09-06 Andreas

module IrrelevantApplication where

-- an unknown function that does not use its second argument

postulate
  f : {A B : Set} -> A -> .B -> A

data _==_ {A : Set}(a : A) : A -> Set where
  refl : a == a

-- the second argument is irrelevant for equality

proofIrr : {A : Set}{x y z : A} -> f x y == f x z
proofIrr = refl

-- irrelevant arguments (like x) may appear as arguments to irrelevant func.s

id : {A B : Set} -> (.A -> B) -> .A -> B
id g x = g x

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

-- t = pId id

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

-- matching an irrelevant record is ok as long as fields are use irrelevantly
irrElim : {A B C : Set} → .(Prod A B) → (.A → .B → C) → C
irrElim (a , b) f = f a b

lemma : {A B C : Set}(a : A)(b : B)(f : .A -> .B -> C) -> irrElim (a , b) f == f a b
lemma a b f = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas, 2017-10-08, issue #2594, reported by gallais

-- Incomplete pattern matching should be reported as such,
-- rather than crashing on a split error.

-- {-# OPTIONS -v tc.cover:10 #-}

open import Agda.Builtin.Bool

dispatch : Bool → Set
dispatch true  = Bool
dispatch false = Bool

argh : (b : Bool) → dispatch b → Bool
argh false false = true
argh false true  = false

-- Error was: Cannot split on non-datatype

-- Expected error:
-- Incomplete pattern matching

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda