text:
open import SOAS.Common
open import SOAS.Families.Core
open import Categories.Object.Initial
open import SOAS.Coalgebraic.Strength
import SOAS.Metatheory.MetaAlgebra

-- Renaming structure by initiality
module SOAS.Metatheory.Renaming {T : Set}
  (⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ) (⅀:Str : Strength ⅀F)
  (𝔛 : Familyₛ) (open SOAS.Metatheory.MetaAlgebra ⅀F 𝔛)
  (𝕋:Init : Initial 𝕄etaAlgebras)
  where

open import SOAS.Context
open import SOAS.Variable
open import SOAS.Abstract.Hom
import SOAS.Abstract.Coalgebra as →□ ; open →□.Sorted
import SOAS.Abstract.Box as □ ; open □.Sorted

open import SOAS.Coalgebraic.Map

open import SOAS.Metatheory.Algebra {T} ⅀F
open import SOAS.Metatheory.Semantics ⅀F ⅀:Str 𝔛 𝕋:Init
open import SOAS.Metatheory.Traversal ⅀F ⅀:Str 𝔛 𝕋:Init

open Strength ⅀:Str

-- Renaming is a ℐ-parametrised traversal into 𝕋
module Renaming = □Traversal 𝕋ᵃ

𝕣𝕖𝕟 : 𝕋 ⇾̣ □ 𝕋
𝕣𝕖𝕟 = Renaming.𝕥𝕣𝕒𝕧

𝕨𝕜 : {α τ : T}{Γ : Ctx} → 𝕋 α Γ → 𝕋 α (τ ∙ Γ)
𝕨𝕜 t = 𝕣𝕖𝕟 t old

-- Comultiplication law
𝕣𝕖𝕟-comp : MapEq₂ ℐᴮ ℐᴮ 𝕒𝕝𝕘 (λ t ρ ϱ → 𝕣𝕖𝕟 t (ϱ ∘ ρ))
                           (λ t ρ ϱ → 𝕣𝕖𝕟 (𝕣𝕖𝕟 t ρ) ϱ)
𝕣𝕖𝕟-comp = record
  { φ = 𝕧𝕒𝕣
  ; ϕ = λ x ρ → 𝕧𝕒𝕣 (ρ x)
  ; χ = 𝕞𝕧𝕒𝕣
  ; f⟨𝑣⟩ = 𝕥⟨𝕧⟩
  ; f⟨𝑚⟩ = 𝕥⟨𝕞⟩
  ; f⟨𝑎⟩ = λ{ {σ = ρ}{ϱ}{t} → begin
        𝕣𝕖𝕟 (𝕒𝕝𝕘 t) (ϱ ∘ ρ)
    ≡⟨ 𝕥⟨𝕒⟩ ⟩
        𝕒𝕝𝕘 (str ℐᴮ 𝕋 (⅀₁ 𝕣𝕖𝕟 t) (ϱ ∘ ρ))
    ≡⟨ cong 𝕒𝕝𝕘 (str-dist 𝕋 (jᶜ ℐᴮ) (⅀₁ 𝕣𝕖𝕟 t) ρ ϱ) ⟩
        𝕒𝕝𝕘 (str ℐᴮ 𝕋 (str ℐᴮ (□ 𝕋) (⅀₁ (precomp 𝕋 (j ℐ)) (⅀₁ 𝕣𝕖𝕟 t)) ρ) ϱ)
    ≡˘⟨ congr ⅀.homomorphism (λ - → 𝕒𝕝𝕘 (str ℐᴮ 𝕋 (str ℐᴮ (□ 𝕋) - ρ) ϱ)) ⟩
        𝕒𝕝𝕘 (str ℐᴮ 𝕋 (str ℐᴮ (□ 𝕋) (⅀₁ (λ{ t ρ ϱ → 𝕣𝕖𝕟 t (ϱ ∘ ρ)}) t) ρ) ϱ)
    ∎ }
  ; g⟨𝑣⟩ = trans (𝕥≈₁ 𝕥⟨𝕧⟩) 𝕥⟨𝕧⟩
  ; g⟨𝑚⟩ = trans (𝕥≈₁ 𝕥⟨𝕞⟩) 𝕥⟨𝕞⟩
  ; g⟨𝑎⟩ = λ{ {σ = ρ}{ϱ}{t} → begin
        𝕣𝕖𝕟 (𝕣𝕖𝕟 (𝕒𝕝𝕘 t) ρ) ϱ
    ≡⟨ 𝕥≈₁ 𝕥⟨𝕒⟩ ⟩
        𝕣𝕖𝕟 (𝕒𝕝𝕘 (str ℐᴮ 𝕋 (⅀₁ 𝕣𝕖𝕟 t) ρ)) ϱ
    ≡⟨ 𝕥⟨𝕒⟩ ⟩
        𝕒𝕝𝕘 (str ℐᴮ 𝕋 (⅀₁ 𝕣𝕖𝕟 (str ℐᴮ 𝕋 (⅀₁ 𝕣𝕖𝕟 t) ρ)) ϱ)
    ≡˘⟨ congr (str-nat₂ 𝕣𝕖𝕟 (⅀₁ 𝕣𝕖𝕟 t) ρ) (λ - → 𝕒𝕝𝕘 (str ℐᴮ 𝕋 - ϱ)) ⟩
        𝕒𝕝𝕘 (str ℐᴮ 𝕋 (str ℐᴮ (□ 𝕋) (⅀.F₁ (λ { h′ ς → 𝕣𝕖𝕟 (h′ ς) }) (⅀₁ 𝕣𝕖𝕟 t)) ρ) ϱ)
    ≡˘⟨ congr ⅀.homomorphism (λ - → 𝕒𝕝𝕘 (str ℐᴮ 𝕋 (str ℐᴮ (□ 𝕋) - ρ) ϱ)) ⟩
        𝕒𝕝𝕘 (str ℐᴮ 𝕋 (str ℐᴮ (□ 𝕋) (⅀₁ (λ{ t ρ ϱ → 𝕣𝕖𝕟 (𝕣𝕖𝕟 t ρ) ϱ}) t) ρ) ϱ)
    ∎ }
  }
  where
  open ≡-Reasoning
  open Renaming

-- Pointed □-coalgebra structure for 𝕋
𝕋ᵇ : Coalg 𝕋
𝕋ᵇ = record { r = 𝕣𝕖𝕟 ; counit = □𝕥𝕣𝕒𝕧-id≈id
            ; comult = λ{ {t = t} → MapEq₂.≈ 𝕣𝕖𝕟-comp t } }

𝕋ᴮ : Coalgₚ 𝕋
𝕋ᴮ = record { ᵇ = 𝕋ᵇ ; η = 𝕧𝕒𝕣 ; r∘η = Renaming.𝕥⟨𝕧⟩ }

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
open import Common.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Strict

data ∋⋆ : Set where
  Z : ∋⋆

data ⊢⋆ : Set where
  size⋆ : Nat → ⊢⋆

⋆Sub : Set
⋆Sub = ∋⋆ → ⊢⋆

data TermCon : ⊢⋆ → Set where
  integer : (s : Nat) → TermCon (size⋆ s)

data ⊢_ : ⊢⋆ → Set where
  con : ∀ {s} → TermCon (size⋆ s) → ⊢ size⋆ s

data Value : {A : ⊢⋆} → ⊢ A → Set where
  V-con : ∀ {n} → (cn : TermCon (size⋆ n)) → Value (con cn)

notErased : Nat → Bool
notErased n = primForce n λ _ → true

BUILTIN : (σ : ⋆Sub) (vtel : Σ (⊢ σ Z) Value) → Bool
BUILTIN σ vtel with σ Z
BUILTIN σ (_ , V-con (integer s)) | _ = notErased s
-- Either of these work:
-- BUILTIN σ (_ , V-con (integer s)) | size⋆ s = notErased s
-- BUILTIN σ (con (integer s) , V-con (integer s)) | _ = notErased s

con2 : ⊢ size⋆ 8
con2 = con (integer 8)

vcon2 : Value con2
vcon2 = V-con (integer 8)

builtin2plus2 : Bool
builtin2plus2 = BUILTIN (λ _ → size⋆ 8) (con2 , vcon2)

help : Bool → String
help true  = "4"
help false = "something went wrong"

check : "4" ≡ help builtin2plus2
check = refl

main : IO ⊤
main = putStrLn (help builtin2plus2)

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Common.Reflection
open import Common.Prelude
open import Common.Equality
open import Agda.Builtin.Sigma

pattern `Nat = def (quote Nat) []
pattern _`→_ a b = pi (vArg a) (abs "_" b)
pattern `Set     = sort (lit 0)
pattern `⊥       = def (quote ⊥) []

pattern `zero  = con (quote zero) []
pattern `suc n = con (quote suc) (vArg n ∷ [])

prDef : FunDef
prDef =
  funDef (`Nat `→ `Nat)
       ( clause [] [] (extLam ( clause [] (vArg `zero ∷ []) `zero
                              ∷ clause (("x" , vArg `Nat) ∷ []) (vArg (`suc (var 0)) ∷ []) (var 0 [])
                              ∷ []) [])
       ∷ [] )

magicDef : FunDef
magicDef =
  funDef (pi (hArg `Set) (abs "A" (`⊥ `→ var 1 [])))
       ( clause [] [] (extLam ( absurdClause (("()" , vArg `⊥) ∷ []) (vArg absurd ∷ [])
                              ∷ []) [])
       ∷ [] )

unquoteDecl magic = define (vArg magic) magicDef

checkMagic : {A : Set} → ⊥ → A
checkMagic = magic

unquoteDecl pr = define (vArg pr) prDef

magic′ : {A : Set} → ⊥ → A
magic′ = unquote (give (extLam (absurdClause (("()" , vArg `⊥) ∷ []) (vArg absurd ∷ []) ∷ []) []))

module Pred (A : Set) where
  unquoteDecl pr′ = define (vArg pr′) prDef

check : pr 10 ≡ 9
check = refl

check′ : Pred.pr′ ⊥ 10 ≡ 9
check′ = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

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

open import LibraBFT.ImplShared.Base.Types

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochDep
open import Util.PKCS
open import Util.Prelude
open import Yasm.Base

-- This module collects in one place the obligations an
-- implementation must meet in order to enjoy the properties
-- proved in Abstract.Properties.

module LibraBFT.Concrete.Obligations (iiah : SystemInitAndHandlers ℓ-RoundManager ConcSysParms) (𝓔 : EpochConfig) where
  import      LibraBFT.Concrete.Properties.PreferredRound iiah as PR
  import      LibraBFT.Concrete.Properties.VotesOnce      iiah as VO
  import      LibraBFT.Concrete.Properties.Common         iiah as Common

  open        SystemTypeParameters ConcSysParms
  open        SystemInitAndHandlers iiah
  open        ParamsWithInitAndHandlers iiah
  open import Yasm.Yasm ℓ-RoundManager ℓ-VSFP ConcSysParms iiah
                        PeerCanSignForPK PeerCanSignForPK-stable

  record ImplObligations : Set (ℓ+1 ℓ-RoundManager) where
    field
      -- Structural obligations:
      sps-cor : StepPeerState-AllValidParts

      -- Semantic obligations:
      --
      -- VotesOnce:
      bsvc : Common.ImplObl-bootstrapVotesConsistent 𝓔
      bsvr : Common.ImplObl-bootstrapVotesRound≡0 𝓔
      v≢0  : Common.ImplObl-NewVoteRound≢0 𝓔
      ∈BI? : (sig : Signature) → Dec (∈BootstrapInfo bootstrapInfo sig)
      v4rc : PR.ImplObligation-RC 𝓔
      iro  : Common.IncreasingRoundObligation 𝓔
      vo₂  : VO.ImplObligation₂ 𝓔

      -- PreferredRound:
      pr₁  : PR.ImplObligation₁ 𝓔
      pr₂  : PR.ImplObligation₂ 𝓔


text:
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality

infix 0 case_of_
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

blockOnFresh : TC ⊤
blockOnFresh =
  checkType unknown unknown >>= λ
  { (meta m _) → blockOnMeta m
  ; _ → typeError (strErr "impossible" ∷ []) }

macro
  shouldNotCrash : Tactic
  shouldNotCrash hole = blockOnFresh

-- Should leave some yellow and a constraint 'unquote shouldNotCrash : Nat'
n : Nat
n = shouldNotCrash


text:
-- There was a bug with the open M es syntax.
module Issue31 where

record M : Set1 where
  field
    A : Set

module MOps (m : M) where
  open M m public

postulate m : M

open MOps m hiding (A)
open MOps m using (A)

postulate foo : A -> Set

module AnotherBug where

  postulate Z : Set

  module A (X : Set) where
    postulate H : Set
  module B (Y : Set) where

  module C where
    open A Z
    open B Z public

  postulate H : Set
  open C

  X = H


text:
module Control.Monad.Reader where

open import Prelude
open import Control.Monad.Zero
open import Control.Monad.Identity
open import Control.Monad.Transformer

record ReaderT {a} (R : Set a) (M : Set a → Set a) (A : Set a) : Set a where
  no-eta-equality
  constructor readerT
  field runReaderT : R → M A

open ReaderT public

module _ {a} {R : Set a} {M : Set a → Set a} where

  instance
    FunctorReaderT : {{_ : Functor M}} → Functor {a = a} (ReaderT R M)
    runReaderT (fmap {{ FunctorReaderT }} f m) r = f <$> runReaderT m r

    FunctorZeroReaderT : {{_ : FunctorZero M}} → FunctorZero {a = a} (ReaderT R M)
    runReaderT (empty {{FunctorZeroReaderT}}) r = empty

    AlternativeReaderT : {{_ : Alternative M}} → Alternative {a = a} (ReaderT R M)
    runReaderT (_<|>_ {{AlternativeReaderT}} x y) r = runReaderT x r <|> runReaderT y r

  module _ {{_ : Monad M}} where

    private
      bindReaderT : ∀ {A B} → ReaderT R M A → (A → ReaderT R M B) → ReaderT R M B
      runReaderT (bindReaderT m f) r = runReaderT m r >>= λ x → runReaderT (f x) r

    instance
      ApplicativeReaderT : Applicative {a = a} (ReaderT R M)
      runReaderT (pure {{ApplicativeReaderT}} x) r = pure x
      _<*>_ {{ApplicativeReaderT}} = monadAp bindReaderT

      MonadReaderT : Monad {a = a} (ReaderT R M)
      _>>=_  {{MonadReaderT}} = bindReaderT

    liftReaderT : {A : Set a} → M A → ReaderT R M A
    runReaderT (liftReaderT m) r = m

    asks : {A : Set a} → (R → A) → ReaderT R M A
    runReaderT (asks f) r = return (f r)

    ask : ReaderT R M R
    ask = asks id

    local : {A : Set a} → (R → R) → ReaderT R M A → ReaderT R M A
    runReaderT (local f m) r = runReaderT m (f r)

instance
  TransformerReaderT : ∀ {a} {R : Set a} → Transformer (ReaderT R)
  lift {{TransformerReaderT}} = liftReaderT

Reader : ∀ {a} (R : Set a) (A : Set a) → Set a
Reader R = ReaderT R Identity

runReader : ∀ {a} {R : Set a} {A : Set a} → Reader R A → R → A
runReader m r = runIdentity (runReaderT m r)

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 BasicT.Metatheory.GentzenNormalForm-Unknown where

open import BasicT.Syntax.GentzenNormalForm public

-- Forcing.  (In a particular model?)

infix 3 _⊩_
_⊩_ : Cx Ty → Ty → Set
Γ ⊩ α P   = Γ ⊢ⁿᶠ α P
Γ ⊩ A ▻ B = Γ ⊢ⁿᵉ A ▻ B ⊎ ∀ {Γ′} → Γ ⊆ Γ′ → Γ′ ⊩ A → Γ′ ⊩ B
Γ ⊩ A ∧ B = Γ ⊢ⁿᵉ A ∧ B ⊎ Γ ⊩ A × Γ ⊩ B
Γ ⊩ ⊤    = Γ ⊢ⁿᶠ ⊤
Γ ⊩ BOOL  = Γ ⊢ⁿᶠ BOOL
Γ ⊩ NAT   = Γ ⊢ⁿᶠ NAT

infix 3 _⊩⋆_
_⊩⋆_ : Cx Ty → Cx Ty → Set
Γ ⊩⋆ ∅     = 𝟙
Γ ⊩⋆ Ξ , A = Γ ⊩⋆ Ξ × Γ ⊩ A

-- Monotonicity with respect to context inclusion.

mono⊩ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩ A → Γ′ ⊩ A
mono⊩ {α P}   η t      = mono⊢ⁿᶠ η t
mono⊩ {A ▻ B} η (ι₁ t) = ι₁ (mono⊢ⁿᵉ η t)
mono⊩ {A ▻ B} η (ι₂ s) = ι₂ (λ η′ a → s (trans⊆ η η′) a)
mono⊩ {A ∧ B} η (ι₁ t) = ι₁ (mono⊢ⁿᵉ η t)
mono⊩ {A ∧ B} η (ι₂ s) = ι₂ (mono⊩ {A} η (π₁ s) , mono⊩ {B} η (π₂ s))
mono⊩ {⊤}    η t      = mono⊢ⁿᶠ η t
mono⊩ {BOOL}  η t      = mono⊢ⁿᶠ η t
mono⊩ {NAT}   η t      = mono⊢ⁿᶠ η t

mono⊩⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩⋆ Ξ → Γ′ ⊩⋆ Ξ
mono⊩⋆ {∅}     η ∙       = ∙
mono⊩⋆ {Ξ , A} η (γ , a) = mono⊩⋆ {Ξ} η γ , mono⊩ {A} η a

-- Soundness and completeness.  (With respect to a particular model?)

reflect : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊩ A
reflect {α P}   t = neⁿᶠ t
reflect {A ▻ B} t = ι₁ t
reflect {A ∧ B} t = ι₁ t
reflect {⊤}    t = neⁿᶠ t
reflect {BOOL}  t = neⁿᶠ t
reflect {NAT}   t = neⁿᶠ t

reify : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ⁿᶠ A
reify {α P}   t      = t
reify {A ▻ B} (ι₁ t) = neⁿᶠ t
reify {A ▻ B} (ι₂ s) = lamⁿᶠ (reify (s weak⊆ (reflect {A} (varⁿᵉ top))))
reify {A ∧ B} (ι₁ t) = neⁿᶠ t
reify {A ∧ B} (ι₂ s) = pairⁿᶠ (reify (π₁ s)) (reify (π₂ s))
reify {⊤}    t      = t
reify {BOOL}  t      = t
reify {NAT}   t      = t

reflect⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ⁿᵉ Ξ → Γ ⊩⋆ Ξ
reflect⋆ {∅}     ∙        = ∙
reflect⋆ {Ξ , A} (ts , t) = reflect⋆ ts , reflect t

reify⋆ : ∀ {Ξ Γ} → Γ ⊩⋆ Ξ → Γ ⊢⋆ⁿᶠ Ξ
reify⋆ {∅}     ∙        = ∙
reify⋆ {Ξ , A} (ts , t) = reify⋆ ts , reify t

-- Additional useful equipment.

_⟪$⟫_ : ∀ {A B w} → w ⊩ A ▻ B → w ⊩ A → w ⊩ B
ι₁ t ⟪$⟫ a = reflect (appⁿᵉ t (reify a))
ι₂ s ⟪$⟫ a = s refl⊆ a

⟪π₁⟫ : ∀ {A B w} → w ⊩ A ∧ B → w ⊩ A
⟪π₁⟫ (ι₁ t) = reflect (fstⁿᵉ t)
⟪π₁⟫ (ι₂ s) = π₁ s

⟪π₂⟫ : ∀ {A B w} → w ⊩ A ∧ B → w ⊩ B
⟪π₂⟫ (ι₁ t) = reflect (sndⁿᵉ t)
⟪π₂⟫ (ι₂ s) = π₂ s

⟪if⟫ : ∀ {C w} → w ⊩ BOOL → w ⊩ C → w ⊩ C → w ⊩ C
⟪if⟫ {C} (neⁿᶠ t) s₂ s₃ = reflect {C} (ifⁿᵉ t (reify s₂) (reify s₃))
⟪if⟫ {C} trueⁿᶠ   s₂ s₃ = s₂
⟪if⟫ {C} falseⁿᶠ  s₂ s₃ = s₃

⟪it⟫ : ∀ {C w} → w ⊩ NAT → w ⊩ C ▻ C → w ⊩ C → w ⊩ C
⟪it⟫ {C} (neⁿᶠ t)  s₂ s₃ = reflect {C} (itⁿᵉ t (reify s₂) (reify s₃))
⟪it⟫ {C} zeroⁿᶠ    s₂ s₃ = s₃
⟪it⟫ {C} (sucⁿᶠ t) s₂ s₃ = s₂ ⟪$⟫ ⟪it⟫ t s₂ s₃

⟪rec⟫ : ∀ {C w} → w ⊩ NAT → w ⊩ NAT ▻ C ▻ C → w ⊩ C → w ⊩ C
⟪rec⟫ {C} (neⁿᶠ t)  s₂ s₃ = reflect {C} (recⁿᵉ t (reify s₂) (reify s₃))
⟪rec⟫ {C} zeroⁿᶠ    s₂ s₃ = s₃
⟪rec⟫ {C} (sucⁿᶠ t) s₂ s₃ = (s₂ ⟪$⟫ t) ⟪$⟫ ⟪rec⟫ t s₂ s₃

-- Forcing for sequents.  (In a particular world of a particular model?)

infix 3 _⊩_⇒_
_⊩_⇒_ : Cx Ty → Cx Ty → Ty → Set
w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

infix 3 _⊩_⇒⋆_
_⊩_⇒⋆_ : Cx Ty → Cx Ty → Cx Ty → Set
w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

-- Entailment.  (Forcing in all worlds of all models, for sequents?)

infix 3 _⊨_
_⊨_ : Cx Ty → Ty → Set
Γ ⊨ A = ∀ {w : Cx Ty} → w ⊩ Γ ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty → Cx Ty → Set
Γ ⊨⋆ Ξ = ∀ {w : Cx Ty} → w ⊩ Γ ⇒⋆ Ξ

-- Additional useful equipment, for sequents.

lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
lookup top     (γ , a) = a
lookup (pop i) (γ , b) = lookup i γ

-- Evaluation.  (Soundness with respect to all models?)

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)         γ = lookup i γ
eval (lam t)         γ = ι₂ (λ η a → eval t (mono⊩⋆ η γ , a))
eval (app t u)       γ = eval t γ ⟪$⟫ eval u γ
eval (pair t u)      γ = ι₂ (eval t γ , eval u γ)
eval (fst t)         γ = ⟪π₁⟫ (eval t γ)
eval (snd t)         γ = ⟪π₂⟫ (eval t γ)
eval unit            γ = unitⁿᶠ
eval true            γ = trueⁿᶠ
eval false           γ = trueⁿᶠ
eval (if {C} t u v)  γ = ⟪if⟫ {C} (eval t γ) (eval u γ) (eval v γ)
eval zero            γ = zeroⁿᶠ
eval (suc t)         γ = sucⁿᶠ (eval t γ)
eval (it {C} t u v)  γ = ⟪it⟫ {C} (eval t γ) (eval u γ) (eval v γ)
eval (rec {C} t u v) γ = ⟪rec⟫ {C} (eval t γ) (eval u γ) (eval v γ)

eval⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ Ξ → Γ ⊨⋆ Ξ
eval⋆ {∅}     ∙        γ = ∙
eval⋆ {Ξ , A} (ts , t) γ = eval⋆ ts γ , eval t γ

-- Reflexivity and transitivity.

refl⊩⋆ : ∀ {Γ} → Γ ⊩⋆ Γ
refl⊩⋆ = reflect⋆ refl⊢⋆ⁿᵉ

trans⊩⋆ : ∀ {Γ Γ′ Γ″} → Γ ⊩⋆ Γ′ → Γ′ ⊩⋆ Γ″ → Γ ⊩⋆ Γ″
trans⊩⋆ ts us = eval⋆ (trans⊢⋆ (nf→tm⋆ (reify⋆ ts)) (nf→tm⋆ (reify⋆ us))) refl⊩⋆

-- Quotation.  (Completeness with respect to all models?)

quot : ∀ {A Γ} → Γ ⊨ A → Γ ⊢ A
quot s = nf→tm (reify (s refl⊩⋆))

-- Normalisation by evaluation.

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

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

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Logics.And where

open import Function

------------------------------------------------------------------------
-- definitions

infixl 5 _∧_
infixl 4 _⇔_

data _∧_ (P Q : Set) : Set where
  ∧-intro : P → Q → P ∧ Q

_⇔_ : (P Q : Set) → Set
p ⇔ q = (p → q) ∧ (q → p)

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

private

  ∧-comm′ : ∀ {P Q} → (P ∧ Q) → (Q ∧ P)
  ∧-comm′ (∧-intro p q) = ∧-intro q p

  ∧-assoc₀ : ∀ {P Q R} → ((P ∧ Q) ∧ R) → (P ∧ (Q ∧ R))
  ∧-assoc₀ (∧-intro (∧-intro p q) r) = ∧-intro p $ ∧-intro q r

  ∧-assoc₁ : ∀ {P Q R} → (P ∧ (Q ∧ R)) → ((P ∧ Q) ∧ R)
  ∧-assoc₁ (∧-intro p (∧-intro q r)) = ∧-intro (∧-intro p q) r

  ∧-comm : ∀ {P Q} → (P ∧ Q) ⇔ (Q ∧ P)
  ∧-comm = ∧-intro ∧-comm′ ∧-comm′

  ∧-assoc : ∀ {P Q R} → (P ∧ (Q ∧ R)) ⇔ ((P ∧ Q) ∧ R)
  ∧-assoc = ∧-intro ∧-assoc₁ ∧-assoc₀

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

and-comm : ∀ {P Q} → (P ∧ Q) ⇔ (Q ∧ P)
and-comm = ∧-comm

and-assoc : ∀ {P Q R} → (P ∧ (Q ∧ R)) ⇔ ((P ∧ Q) ∧ R)
and-assoc = ∧-assoc


text:
module NoQualifiedInstances.ParameterizedImport.A (T : Set) where

record I : Set where

postulate instance i : I


text:
module Data.Tuple.List{ℓ} where

import      Lvl
open import Data using (Unit ; <>)
open import Data.Tuple using (_⨯_ ; _,_)
import      Data.List
open        Data.List using (List)
open import Type{ℓ}

-- Constructs a tuple from a list
Tuple : List(Type) → Type
Tuple(List.∅)          = Unit
Tuple(T List.⊰ List.∅) = T
Tuple(T List.⊰ L)      = (T ⨯ Tuple(L))

pattern ∅        = <>
pattern _⊰∅ a    = a
pattern _⊰+_ a l = (a , l)

import Data.List.Functions as List

_⊰_ : ∀{T}{L} → T → Tuple(L) → Tuple(T List.⊰ L)
_⊰_ {_}{List.∅}     a _ = a
_⊰_ {_}{_ List.⊰ _} a l = (a , l)

head : ∀{T}{L} → Tuple(T List.⊰ L) → T
head{_}{List.∅}    (a ⊰∅)   = a
head{_}{_ List.⊰ _}(a ⊰+ _) = a

tail : ∀{T}{L} → Tuple(T List.⊰ L) → Tuple(L)
tail{_}{List.∅}    (_ ⊰∅)   = ∅
tail{_}{_ List.⊰ _}(_ ⊰+ l) = l

module _ where
  open import Data.List.Equiv.Id
  open import Data.List.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs
  open import Structure.Relator
  open import Structure.Operator.Properties

  _++_ : ∀{L₁ L₂} → Tuple(L₁) → Tuple(L₂) → Tuple(L₁ List.++ L₂)
  _++_{L}                   {List.∅} (l)(_)         = substitute₁ₗ(Tuple) {y = L} (identityᵣ(List._++_)(List.∅)) l
  _++_{List.∅}              {_}      (_)(l)         = l
  _++_{A List.⊰ List.∅}     {L₂}     (a ⊰∅)   (l₂) = _⊰_ {A}{L₂} (a) (l₂)
  _++_{A List.⊰ B List.⊰ L₁}{L₂}     (a ⊰+ l₁)(l₂) = _⊰_ {A}{(B Data.List.⊰ L₁) List.++ L₂} (a) (_++_ {B Data.List.⊰ L₁}{L₂} l₁ l₂)

module _ where
  open import Numeral.Natural

  length : ∀{L} → Tuple(L) → ℕ
  length{L} (_) = List.length(L)

-- TODO: TupleRaise : Tuple(repeat(n)(T)) ≡ T ^ n

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:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Empty.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty.Base

isProp⊥ : isProp ⊥
isProp⊥ ()

isContr⊥→A : ∀ {ℓ} {A : Type ℓ} → isContr (⊥ → A)
fst isContr⊥→A ()
snd isContr⊥→A f i ()

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


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
-}

open import LibraBFT.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.Consensus.ConsensusProvider as ConsensusProvider
import      LibraBFT.Impl.IO.OBM.GenKeyFile           as GenKeyFile
import      LibraBFT.Impl.IO.OBM.ObmNeedFetch         as ObmNeedFetch
import      LibraBFT.Impl.Types.ValidatorSigner       as ValidatorSigner
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.Prelude
open import Optics.All

module LibraBFT.Impl.IO.OBM.Start where

{-
This only does the initialization steps from the Haskell version.
If initialization succeeds, it returns
- the EpochManager (for all epochs)
  - note: this contains the initialized RoundManager for the current epoch (i.e., Epoch 0)
- any output from the RoundManager produced during initialization

The only output is (with info logging removed):

-- only the leader of round 1 will broadcast a proposal
BroadcastProposal; [ ... peer addresses ... ];
                   (ProposalMsg
                     (B 7194dca (BD 1 1 (Prop ("TX/1/1")) ...)) -- proposed block
                     (SI (hqc c66a132) (hcc N) (htc (TC N))))   -- SyncInfo

The Haskell code, after initialization, hooks up the communication channels and sockets
and starts threads that handle them.  One of the threads is given to
EpochManager.obmStartLoop to get input and pass it through the EpochManager
and then (usually) on to the RoundMnager.

TODO-3: Replace 'Handle.initRM' with the initialized RoundManager obtained
through the following 'startViaConsensusProvider'.
TODO-3: Figure out how to handle the initial BroadcastProposal.
-}
startViaConsensusProvider
  : Instant
  → GenKeyFile.NfLiwsVsVvPe
  → TxTypeDependentStuffForNetwork
  → Either ErrLog (EpochManager × List Output)
startViaConsensusProvider now (nf , liws , vs , vv , pe) txTDS = do
  (nc , occp , _liws , sk , _pe) ← ConsensusProvider.obmInitialData (nf , liws , vs , vv , pe)
  ConsensusProvider.startConsensus
    nc now occp liws sk
    (ObmNeedFetch∙new {- newNetwork -stps'-})
    (txTDS ^∙ ttdsnProposalGenerator) (txTDS ^∙ ttdsnStateComputer)

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 --without-K --safe #-}

module Dodo.Unary.Intersection where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (refl; _≡_)
open import Level using (Level; _⊔_)
open import Function using (_∘₂_)
open import Data.Product using (_×_; _,_; swap; proj₁; proj₂)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel; REL)
-- Local imports
open import Dodo.Unary.Equality
open import Dodo.Unary.Unique

-- # Definitions

infixr 30 _∩₁_

_∩₁_ : {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → Pred A ℓ₁
  → Pred A ℓ₂
  → Pred A (ℓ₁ ⊔ ℓ₂)
_∩₁_ p q x = p x × q x

-- # Properties

module _ {a ℓ : Level} {A : Set a} {P : Pred A ℓ} where

  ∩₁-idem : (P ∩₁ P) ⇔₁ P
  ∩₁-idem = ⇔: (λ _ → proj₁) ⊇-proof
    where
    ⊇-proof : P ⊆₁' (P ∩₁ P)
    ⊇-proof _ Px = (Px , Px)

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

  ∩₁-comm : (P ∩₁ Q) ⇔₁ (Q ∩₁ P)
  ∩₁-comm = ⇔: (λ _ → swap) (λ _ → swap)

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

  ∩₁-assoc : P ∩₁ (Q ∩₁ R) ⇔₁ (P ∩₁ Q) ∩₁ R
  ∩₁-assoc = ⇔: ⊆-proof ⊇-proof
    where
    ⊆-proof : P ∩₁ (Q ∩₁ R) ⊆₁' (P ∩₁ Q) ∩₁ R
    ⊆-proof _ (Px , Qx , Rx) = ((Px , Qx) , Rx)
    ⊇-proof : (P ∩₁ Q) ∩₁ R ⊆₁' P ∩₁ (Q ∩₁ R)
    ⊇-proof _ ((Px , Qx) , Rx) = (Px , Qx , Rx)

-- # Operations

-- ## Operations: General

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

  ∩₁-unique-pred :
      UniquePred P
    → UniquePred Q
    → UniquePred (P ∩₁ Q)
  ∩₁-unique-pred uniqueP uniqueQ x (Px₁ , Qx₁) (Px₂ , Qx₂)
    with uniqueP x Px₁ Px₂ | uniqueQ x Qx₁ Qx₂
  ... | refl | refl = refl

-- ## Operations: ⊆₁

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

  ∩₁-combine-⊆₁ : P ⊆₁ Q → P ⊆₁ R → P ⊆₁ (Q ∩₁ R)
  ∩₁-combine-⊆₁ (⊆: P⊆Q) (⊆: P⊆R) = ⊆: (λ x Px → (P⊆Q x Px , P⊆R x Px))

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

  ∩₁-introˡ-⊆₁ : (P ∩₁ Q) ⊆₁ P
  ∩₁-introˡ-⊆₁ = ⊆: (λ _ → proj₁)

  ∩₁-introʳ-⊆₁ : (P ∩₁ Q) ⊆₁ Q
  ∩₁-introʳ-⊆₁ = ⊆: (λ _ → proj₂)

  ∩₁-elimˡ-⊆₁ : P ⊆₁ (Q ∩₁ R) → P ⊆₁ R
  ∩₁-elimˡ-⊆₁ (⊆: P⊆[Q∩R]) = ⊆: (λ x Px → proj₂ (P⊆[Q∩R] x Px))

  ∩₁-elimʳ-⊆₁ : P ⊆₁ (Q ∩₁ R) → P ⊆₁ Q
  ∩₁-elimʳ-⊆₁ (⊆: P⊆[Q∩R]) = ⊆: (λ x Px → proj₁ (P⊆[Q∩R] x Px))

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

  ∩₁-substˡ-⊆₁ : P ⊆₁ Q → (P ∩₁ R) ⊆₁ (Q ∩₁ R)
  ∩₁-substˡ-⊆₁ (⊆: P⊆Q) = ⊆: lemma
    where
    lemma : (P ∩₁ R) ⊆₁' (Q ∩₁ R)
    lemma x (Px , Rx) = (P⊆Q x Px , Rx)

  ∩₁-substʳ-⊆₁ : P ⊆₁ Q → (R ∩₁ P) ⊆₁ (R ∩₁ Q)
  ∩₁-substʳ-⊆₁ (⊆: P⊆Q) = ⊆: lemma
    where
    lemma : (R ∩₁ P) ⊆₁' (R ∩₁ Q)
    lemma x (Rx , Px) = (Rx , P⊆Q x Px)

-- ## Operations: ⇔₂

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

  ∩₁-substˡ : P ⇔₁ Q → (P ∩₁ R) ⇔₁ (Q ∩₁ R)
  ∩₁-substˡ = ⇔₁-compose ∩₁-substˡ-⊆₁ ∩₁-substˡ-⊆₁

  ∩₁-substʳ : P ⇔₁ Q → (R ∩₁ P) ⇔₁ (R ∩₁ Q)
  ∩₁-substʳ = ⇔₁-compose ∩₁-substʳ-⊆₁ ∩₁-substʳ-⊆₁

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Unit

data S : Set where
  base : S

foo : ∀ i j k → Partial _ S
foo i j k (i = i0)(k = i1) = base
foo i j k (j = i1)         = base

-- Testing that fallthrough patterns get expanded when compiling the
-- clauses of foo.
-- Just because (i = i0) matches the first clause doesn't mean we commit to it.
-- `foo i0 i1 k o` should still compute to base by the second clause.
testf : ∀ k (o : IsOne i1) → foo i0 i1 k o ≡ base
testf k o i = base

max_forks_repo_name: Agda-zh/agda


text:
module Relation.Unary.Membership {a} (A : Set a) where

open import Level
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Unary
open import Relation.Binary

infixl 4 _≋_
_≋_ : Rel (Pred A a) _
P ≋ Q = P ⊆′ Q × Q ⊆′ P

⊆-refl : Reflexive (_⊆′_ {a} {A} {a})
⊆-refl {pred} x P = P

≋-refl : Reflexive _≋_
≋-refl {pred} = (⊆-refl {pred}) , (⊆-refl {pred})

≋-sym : Symmetric _≋_
≋-sym x = (proj₂ x) , (proj₁ x)

≋-trans : Transitive _≋_
≋-trans f≋g g≋h =
    (λ x z → proj₁ g≋h x (proj₁ f≋g x z)) , (λ x z → proj₂ f≋g x (proj₂ g≋h x z))

≋-isEquivalence : IsEquivalence _≋_
≋-isEquivalence = record
    { refl = ≋-refl
    ; sym = ≋-sym
    ; trans = ≋-trans
    }

⊆-trans : Transitive (_⊆′_ {a} {A} {a})
⊆-trans A⊆B B⊆C x x∈A = B⊆C x (A⊆B x x∈A)

⊆-preorder : IsPreorder _≋_ _⊆′_
⊆-preorder = record
    { isEquivalence = ≋-isEquivalence
    ; reflexive = proj₁
    ; trans = ⊆-trans
    }

⊆-partialOrder : IsPartialOrder _≋_ _⊆′_
⊆-partialOrder = record
    { isPreorder = ⊆-preorder
    ; antisym = λ A⊆B B⊆A → A⊆B , B⊆A
    }

⊆-poset : Poset (suc a) a a
⊆-poset = record
    { Carrier = Pred A a
    ; _≈_ = _≋_
    ; _≤_ = _⊆′_
    ; isPartialOrder = ⊆-partialOrder
    }

module ⊆-Reasoning where
    import Relation.Binary.PartialOrderReasoning as PosetR
    open PosetR ⊆-poset public
        renaming (_≤⟨_⟩_ to _⊆⟨_⟩_)

    infix 1 _∈⟨_⟩_
    infixr 2 _→⟨_⟩_

    _∈⟨_⟩_ : ∀ x {xs ys} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys
    x ∈⟨ x∈xs ⟩ xs⊆ys = begin_ xs⊆ys x x∈xs

    _→⟨_⟩_ : ∀ A {B C} → (A ⊆ B) → B IsRelatedTo C → A IsRelatedTo C
    A →⟨ f ⟩ B∼C = A ⊆⟨ (λ x x∈A → f x∈A) ⟩ B∼C
    -- A ⊆[ f ] relTo B∼C = A ⊆⟨ f ⟩ relTo B∼C
    --

        --(begin xs⊆ys) x∈xs

max_stars_repo_name: banacorn/formal-language

max_issues_repo_name: banacorn/formal-language

max_forks_repo_name: banacorn/formal-language


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums of binary relations
------------------------------------------------------------------------

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

module Data.Sum.Relation.Binary.LeftOrder where

open import Data.Sum as Sum
open import Data.Sum.Relation.Binary.Pointwise as PW
  using (Pointwise; inj₁; inj₂)
open import Data.Product
open import Data.Empty
open import Function
open import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

----------------------------------------------------------------------
-- Definition

infixr 1 _⊎-<_

data _⊎-<_ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
           {ℓ₁ ℓ₂} (_∼₁_ : Rel A₁ ℓ₁) (_∼₂_ : Rel A₂ ℓ₂) :
           Rel (A₁ ⊎ A₂) (a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂) where
  ₁∼₂ : ∀ {x y}                 → (_∼₁_ ⊎-< _∼₂_) (inj₁ x) (inj₂ y)
  ₁∼₁ : ∀ {x y} (x∼₁y : x ∼₁ y) → (_∼₁_ ⊎-< _∼₂_) (inj₁ x) (inj₁ y)
  ₂∼₂ : ∀ {x y} (x∼₂y : x ∼₂ y) → (_∼₁_ ⊎-< _∼₂_) (inj₂ x) (inj₂ y)

----------------------------------------------------------------------
-- Some properties which are preserved by _⊎-<_

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂}
         where

  drop-inj₁ : ∀ {x y} → (∼₁ ⊎-< ∼₂) (inj₁ x) (inj₁ y) → ∼₁ x y
  drop-inj₁ (₁∼₁ x∼₁y) = x∼₁y

  drop-inj₂ : ∀ {x y} → (∼₁ ⊎-< ∼₂) (inj₂ x) (inj₂ y) → ∼₂ x y
  drop-inj₂ (₂∼₂ x∼₂y) = x∼₂y

  ⊎-<-refl : Reflexive ∼₁ → Reflexive ∼₂ →
             Reflexive (∼₁ ⊎-< ∼₂)
  ⊎-<-refl refl₁ refl₂ {inj₁ x} = ₁∼₁ refl₁
  ⊎-<-refl refl₁ refl₂ {inj₂ y} = ₂∼₂ refl₂

  ⊎-<-transitive : Transitive ∼₁ → Transitive ∼₂ →
                   Transitive (∼₁ ⊎-< ∼₂)
  ⊎-<-transitive trans₁ trans₂ ₁∼₂        (₂∼₂ x∼₂y)  = ₁∼₂
  ⊎-<-transitive trans₁ trans₂ (₁∼₁ x∼₁y) ₁∼₂         = ₁∼₂
  ⊎-<-transitive trans₁ trans₂ (₁∼₁ x∼₁y) (₁∼₁ x∼₁y₁) = ₁∼₁ (trans₁ x∼₁y x∼₁y₁)
  ⊎-<-transitive trans₁ trans₂ (₂∼₂ x∼₂y) (₂∼₂ x∼₂y₁) = ₂∼₂ (trans₂ x∼₂y x∼₂y₁)

  ⊎-<-asymmetric : Asymmetric ∼₁ → Asymmetric ∼₂ →
                   Asymmetric (∼₁ ⊎-< ∼₂)
  ⊎-<-asymmetric asym₁ asym₂ ₁∼₂ ()
  ⊎-<-asymmetric asym₁ asym₂ (₁∼₁ x∼₁y) (₁∼₁ x∼₁y₁) = asym₁ x∼₁y x∼₁y₁
  ⊎-<-asymmetric asym₁ asym₂ (₂∼₂ x∼₂y) (₂∼₂ x∼₂y₁) = asym₂ x∼₂y x∼₂y₁

  ⊎-<-total : Total ∼₁ → Total ∼₂ → Total (∼₁ ⊎-< ∼₂)
  ⊎-<-total total₁ total₂ = total
    where
    total : Total (_ ⊎-< _)
    total (inj₁ x) (inj₁ y) = Sum.map ₁∼₁ ₁∼₁ $ total₁ x y
    total (inj₁ x) (inj₂ y) = inj₁ ₁∼₂
    total (inj₂ x) (inj₁ y) = inj₂ ₁∼₂
    total (inj₂ x) (inj₂ y) = Sum.map ₂∼₂ ₂∼₂ $ total₂ x y

  ⊎-<-decidable : Decidable ∼₁ → Decidable ∼₂ →
                  Decidable (∼₁ ⊎-< ∼₂)
  ⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₁ y) = Dec.map′ ₁∼₁ drop-inj₁ (dec₁ x y)
  ⊎-<-decidable dec₁ dec₂ (inj₁ x) (inj₂ y) = yes ₁∼₂
  ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₁ y) = no λ()
  ⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = Dec.map′ ₂∼₂ drop-inj₂ (dec₂ x y)

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂}
         {ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄}
         where

  ⊎-<-reflexive : ≈₁ ⇒ ∼₁ → ≈₂ ⇒ ∼₂ →
                  (Pointwise ≈₁ ≈₂) ⇒ (∼₁ ⊎-< ∼₂)
  ⊎-<-reflexive refl₁ refl₂ (inj₁ x) = ₁∼₁ (refl₁ x)
  ⊎-<-reflexive refl₁ refl₂ (inj₂ x) = ₂∼₂ (refl₂ x)

  ⊎-<-irreflexive : Irreflexive ≈₁ ∼₁ → Irreflexive ≈₂ ∼₂ →
                    Irreflexive (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-irreflexive irrefl₁ irrefl₂ (inj₁ x) (₁∼₁ x∼₁y) = irrefl₁ x x∼₁y
  ⊎-<-irreflexive irrefl₁ irrefl₂ (inj₂ x) (₂∼₂ x∼₂y) = irrefl₂ x x∼₂y

  ⊎-<-antisymmetric : Antisymmetric ≈₁ ∼₁ → Antisymmetric ≈₂ ∼₂ →
                      Antisymmetric (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-antisymmetric antisym₁ antisym₂ (₁∼₁ x∼₁y) (₁∼₁ x∼₁y₁) = inj₁ (antisym₁ x∼₁y x∼₁y₁)
  ⊎-<-antisymmetric antisym₁ antisym₂ (₂∼₂ x∼₂y) (₂∼₂ x∼₂y₁) = inj₂ (antisym₂ x∼₂y x∼₂y₁)
  -- Remove in Agda 2.6.0?
  ⊎-<-antisymmetric antisym₁ antisym₂ ₁∼₂ ()

  ⊎-<-respectsʳ : ∼₁ Respectsʳ ≈₁ → ∼₂ Respectsʳ ≈₂ →
                  (∼₁ ⊎-< ∼₂) Respectsʳ (Pointwise ≈₁ ≈₂)
  ⊎-<-respectsʳ resp₁ resp₂ (inj₁ x₁) (₁∼₁ x∼₁y) = ₁∼₁ (resp₁ x₁ x∼₁y)
  ⊎-<-respectsʳ resp₁ resp₂ (inj₂ x₁) ₁∼₂        = ₁∼₂
  ⊎-<-respectsʳ resp₁ resp₂ (inj₂ x₁) (₂∼₂ x∼₂y) = ₂∼₂ (resp₂ x₁ x∼₂y)

  ⊎-<-respectsˡ : ∼₁ Respectsˡ ≈₁ → ∼₂ Respectsˡ ≈₂ →
                  (∼₁ ⊎-< ∼₂) Respectsˡ (Pointwise ≈₁ ≈₂)
  ⊎-<-respectsˡ resp₁ resp₂ (inj₁ x) ₁∼₂        = ₁∼₂
  ⊎-<-respectsˡ resp₁ resp₂ (inj₁ x) (₁∼₁ x∼₁y) = ₁∼₁ (resp₁ x x∼₁y)
  ⊎-<-respectsˡ resp₁ resp₂ (inj₂ x) (₂∼₂ x∼₂y) = ₂∼₂ (resp₂ x x∼₂y)

  ⊎-<-respects₂ : ∼₁ Respects₂ ≈₁ → ∼₂ Respects₂ ≈₂ →
                  (∼₁ ⊎-< ∼₂) Respects₂ (Pointwise ≈₁ ≈₂)
  ⊎-<-respects₂ (r₁ , l₁) (r₂ , l₂) = ⊎-<-respectsʳ r₁ r₂ , ⊎-<-respectsˡ l₁ l₂

  ⊎-<-trichotomous : Trichotomous ≈₁ ∼₁ → Trichotomous ≈₂ ∼₂ →
                     Trichotomous (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-trichotomous tri₁ tri₂ (inj₁ x) (inj₂ y) = tri< ₁∼₂ (λ()) (λ())
  ⊎-<-trichotomous tri₁ tri₂ (inj₂ x) (inj₁ y) = tri> (λ()) (λ()) ₁∼₂
  ⊎-<-trichotomous tri₁ tri₂ (inj₁ x) (inj₁ y) with tri₁ x y
  ... | tri< x<y x≉y x≯y = tri< (₁∼₁ x<y) (x≉y ∘ PW.drop-inj₁) (x≯y ∘ drop-inj₁)
  ... | tri≈ x≮y x≈y x≯y = tri≈ (x≮y ∘ drop-inj₁) (inj₁ x≈y) (x≯y ∘ drop-inj₁)
  ... | tri> x≮y x≉y x>y = tri> (x≮y ∘ drop-inj₁) (x≉y ∘ PW.drop-inj₁) (₁∼₁ x>y)
  ⊎-<-trichotomous tri₁ tri₂ (inj₂ x) (inj₂ y) with tri₂ x y
  ... | tri< x<y x≉y x≯y = tri< (₂∼₂ x<y) (x≉y ∘ PW.drop-inj₂) (x≯y ∘ drop-inj₂)
  ... | tri≈ x≮y x≈y x≯y = tri≈ (x≮y ∘ drop-inj₂) (inj₂ x≈y) (x≯y ∘ drop-inj₂)
  ... | tri> x≮y x≉y x>y = tri> (x≮y ∘ drop-inj₂) (x≉y ∘ PW.drop-inj₂) (₂∼₂ x>y)

----------------------------------------------------------------------
-- Some collections of properties which are preserved

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₂}
         {ℓ₃ ℓ₄} {≈₂ : Rel A₂ ℓ₃} {∼₂ : Rel A₂ ℓ₄} where

  ⊎-<-isPreorder : IsPreorder ≈₁ ∼₁ → IsPreorder ≈₂ ∼₂ →
                   IsPreorder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-isPreorder pre₁ pre₂ = record
    { isEquivalence = PW.⊎-isEquivalence (isEquivalence pre₁) (isEquivalence pre₂)
    ; reflexive     = ⊎-<-reflexive (reflexive pre₁) (reflexive pre₂)
    ; trans         = ⊎-<-transitive (trans pre₁) (trans pre₂)
    }
    where open IsPreorder

  ⊎-<-isPartialOrder : IsPartialOrder ≈₁ ∼₁ →
                       IsPartialOrder ≈₂ ∼₂ →
                       IsPartialOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-isPartialOrder po₁ po₂ = record
    { isPreorder = ⊎-<-isPreorder (isPreorder po₁) (isPreorder po₂)
    ; antisym    = ⊎-<-antisymmetric (antisym po₁) (antisym    po₂)
    }
    where open IsPartialOrder

  ⊎-<-isStrictPartialOrder : IsStrictPartialOrder ≈₁ ∼₁ →
                             IsStrictPartialOrder ≈₂ ∼₂ →
                             IsStrictPartialOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-isStrictPartialOrder spo₁ spo₂ = record
    { isEquivalence = PW.⊎-isEquivalence (isEquivalence spo₁) (isEquivalence spo₂)
    ; irrefl        = ⊎-<-irreflexive   (irrefl spo₁) (irrefl   spo₂)
    ; trans         = ⊎-<-transitive    (trans spo₁)  (trans    spo₂)
    ; <-resp-≈      = ⊎-<-respects₂   (<-resp-≈ spo₁) (<-resp-≈ spo₂)
    }
    where open IsStrictPartialOrder

  ⊎-<-isTotalOrder : IsTotalOrder ≈₁ ∼₁ →
                     IsTotalOrder ≈₂ ∼₂ →
                     IsTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-isTotalOrder to₁ to₂ = record
    { isPartialOrder = ⊎-<-isPartialOrder (isPartialOrder to₁) (isPartialOrder to₂)
    ; total          = ⊎-<-total (total to₁) (total to₂)
    }
    where open IsTotalOrder

  ⊎-<-isDecTotalOrder : IsDecTotalOrder ≈₁ ∼₁ →
                        IsDecTotalOrder ≈₂ ∼₂ →
                        IsDecTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-isDecTotalOrder to₁ to₂ = record
    { isTotalOrder = ⊎-<-isTotalOrder (isTotalOrder to₁) (isTotalOrder to₂)
    ; _≟_          = PW.⊎-decidable (_≟_  to₁) (_≟_  to₂)
    ; _≤?_         = ⊎-<-decidable (_≤?_ to₁) (_≤?_ to₂)
    }
    where open IsDecTotalOrder

  ⊎-<-isStrictTotalOrder : IsStrictTotalOrder ≈₁ ∼₁ →
                           IsStrictTotalOrder ≈₂ ∼₂ →
                           IsStrictTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
  ⊎-<-isStrictTotalOrder sto₁ sto₂ = record
    { isEquivalence = PW.⊎-isEquivalence (isEquivalence sto₁) (isEquivalence sto₂)
    ; trans         = ⊎-<-transitive (trans sto₁) (trans sto₂)
    ; compare       = ⊎-<-trichotomous (compare sto₁) (compare sto₂)
    }
    where open IsStrictTotalOrder

------------------------------------------------------------------------
-- "Packages" can also be combined.

module _ {a b c d e f} where

  ⊎-<-preorder : Preorder a b c →
                 Preorder d e f →
                 Preorder _ _ _
  ⊎-<-preorder p₁ p₂ = record
    { isPreorder   =
        ⊎-<-isPreorder (isPreorder p₁) (isPreorder p₂)
    } where open Preorder

  ⊎-<-poset : Poset a b c →
              Poset a b c →
              Poset _ _ _
  ⊎-<-poset po₁ po₂ = record
    { isPartialOrder =
        ⊎-<-isPartialOrder (isPartialOrder po₁) (isPartialOrder po₂)
    } where open Poset

  ⊎-<-strictPartialOrder : StrictPartialOrder a b c →
                           StrictPartialOrder d e f →
                           StrictPartialOrder _ _ _
  ⊎-<-strictPartialOrder spo₁ spo₂ = record
    { isStrictPartialOrder =
      ⊎-<-isStrictPartialOrder (isStrictPartialOrder spo₁) (isStrictPartialOrder spo₂)
    } where open StrictPartialOrder

  ⊎-<-totalOrder : TotalOrder a b c →
                   TotalOrder d e f →
                   TotalOrder _ _ _
  ⊎-<-totalOrder to₁ to₂ = record
    { isTotalOrder = ⊎-<-isTotalOrder (isTotalOrder to₁) (isTotalOrder to₂)
    } where open TotalOrder

  ⊎-<-decTotalOrder : DecTotalOrder a b c →
                      DecTotalOrder d e f →
                      DecTotalOrder _ _ _
  ⊎-<-decTotalOrder to₁ to₂ = record
    { isDecTotalOrder = ⊎-<-isDecTotalOrder (isDecTotalOrder to₁) (isDecTotalOrder to₂)
    } where open DecTotalOrder

  ⊎-<-strictTotalOrder : StrictTotalOrder a b c →
                         StrictTotalOrder a b c →
                         StrictTotalOrder _ _ _
  ⊎-<-strictTotalOrder sto₁ sto₂ = record
    { isStrictTotalOrder = ⊎-<-isStrictTotalOrder (isStrictTotalOrder sto₁) (isStrictTotalOrder sto₂)
    } where open StrictTotalOrder


text:
module Golden where

open import Basics
open import Vec
open import Ix
open import Cutting
open import Interior
open import Tensor
open RECTANGLE
open INTERIOR RectCut

ind : (n : Nat)(P : Nat -> Set) -> P zero ->
         ((k : Nat) -> P k -> P (suc k)) -> P n
ind zero P pz ps = pz
ind (suc n) P pz ps = ps n (ind n P pz ps)

+N-zero : (x : Nat) -> (x +N zero) == x
+N-zero x = ind x (\ x -> (x +N zero) == x) (refl _) (\ _ h -> refl suc =$= h)

+N-suc : (x y : Nat) -> (x +N suc y) == suc (x +N y)
+N-suc x y = ind x (\ x -> (x +N suc y) == suc (x +N y))
             (refl _) (\ _ h -> refl suc =$= h)

comm-+N : (x y : Nat) -> (x +N y) == (y +N x)
comm-+N x zero = +N-zero x
comm-+N x (suc y) rewrite +N-suc x y = refl suc =$= comm-+N x y

clockwise90 : {P : Nat * Nat -> Set}{w h : Nat} ->
  ({w h : Nat} -> P (w , h) -> P (h , w)) ->
  Interior P (w , h) -> Interior P (h , w)
clockwise90 pc90 (tile p) = tile (pc90 p)
clockwise90 pc90 < inl (l , r , refl _) 8>< (il , ir , <>) >
  = < inr (l , r , refl _) 8><
      clockwise90 pc90 il , clockwise90 pc90 ir , <> >
clockwise90 pc90 < inr (t , b , refl _) 8>< it , ib , <> >
  = < (inl (b , t , comm-+N b t)) 8><
      clockwise90 pc90 ib , clockwise90 pc90 it , <> >

Square : Nat * Nat -> Set
Square (w , h) = w == h

c90Sq : {w h : Nat} -> Square (w , h) -> Square (h , w)
c90Sq (refl _) = refl _

golden : (n : Nat) -> Sg Nat \ w -> Sg Nat \ h -> Interior Square (w , h)
golden zero = 1 , 1 , tile (refl 1)
golden (suc n) with golden n
... | w , h , i = (w +N h) , w , < (inl (w , h , refl _)) 8><
                  tile (refl w) , clockwise90 c90Sq i , <> >

fill : {n : Nat}{X : Set} -> X -> X -> X -> Vec X (suc (suc n))
fill {n} first midst last rewrite comm-+N 1 (suc n) = first ,- (pure midst +V (last ,- []))
  where open Applicative (VecAppl n)

border : {w h : Nat} -> Matrix Char (w , h)
border {w} {zero} = []
border {zero} {h} = pure [] where open Applicative (VecAppl _)
border {suc zero} {suc zero} = ('O' ,- []) ,- []
border {suc (suc w)} {suc zero} = fill '<' '-' '>' ,- []
border {suc zero} {suc (suc h)} = fill ('^' ,- []) ('|' ,- []) ('v' ,- [])
border {suc (suc w)} {suc (suc h)} =
  fill (fill '/' '-' '\\')
       (fill '|' ' ' '|')
       (fill '\\' '-' '/')

goldenInterior :  (n : Nat) -> Sg Nat \ w -> Sg Nat \ h -> Interior (Matrix Char) (w , h)
goldenInterior n with golden n
... | w , h , sqi = w , h , ifold (\ _ _ -> tile border) (\ _ -> <_>) (w , h) sqi

picture : [ Interior (Matrix Char) -:> Matrix Char ]
picture = ifold (\ _ -> id) NatCut2DMatAlg

goldenPicture : (n : Nat) -> Sg Nat \ w -> Sg Nat \ h -> Matrix Char (w , h)
goldenPicture n with goldenInterior n
... | w , h , mi = w , h , picture _ mi

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


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

module Experiment.Categories.Category.Monoidal.Strict where


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

open import common

open import syntx as N
open import derivability as N2
open import typingrules
open import structuralrules
open import typetheories
open import examples

open import traditional as T

Σ : Signature
Σ = TTSig ΠUEl-TT

{- Maps between expressions -}

T→N : {n : ℕ} {k : SyntaxSort} → T.Expr k n → N.Expr Σ n k
T→N uu = sym 1 []
T→N (el v) = sym 0 ([] , T→N v)
T→N (pi A B) = sym 4 ([] , T→N A , T→N B)
T→N (var x) = var x
T→N (lam A B u) = sym 3 ([] , T→N A , T→N B , T→N u)
T→N (app A B f a) = sym 2 ([] , T→N A , T→N B , T→N f , T→N a)

N→T : {n : ℕ} {k : SyntaxSort} → N.Expr Σ n k → T.Expr k n
N→T (var x) = var x
N→T (sym (prev (prev (prev (prev new)))) ([] , A , B)) = pi (N→T A) (N→T B)
N→T (sym (prev (prev (prev new))) ([] , A , B , u)) = lam (N→T A) (N→T B) (N→T u)
N→T (sym (prev (prev new)) ([] , A , B , f , a)) = app (N→T A) (N→T B) (N→T f) (N→T a)
N→T (sym (prev new) []) = uu
N→T (sym new ([] , v)) = el (N→T v)

{- Equalities -}

TNT : {n : ℕ} {k : SyntaxSort} (e : N.Expr Σ n k) → T→N (N→T e) ≡ e
TNT (var x) = refl
TNT (sym (prev (prev (prev (prev new)))) ([] , A , B)) = ap2 (λ x y → sym 4 ([] , x , y)) (TNT A) (TNT B)
TNT (sym (prev (prev (prev new))) ([] , A , B , u)) = ap3 (λ x y z → sym 3 ([] , x , y , z)) (TNT A) (TNT B) (TNT u)
TNT (sym (prev (prev new)) ([] , A , B , f , a)) = ap4 (λ x y z t → sym 2 ([] , x , y , z , t)) (TNT A) (TNT B) (TNT f) (TNT a)
TNT (sym (prev new) []) = refl
TNT (sym new ([] , v)) = ap (λ v → sym 0 ([] , v)) (TNT v)

NTN : {n : ℕ} {k : SyntaxSort} (e : T.Expr k n) → N→T (T→N e) ≡ e
NTN uu = refl
NTN (el v) = ap el (NTN v)
NTN (pi A B) = ap2 pi (NTN A) (NTN B)
NTN (var x) = refl
NTN (lam A B u) = ap3 lam (NTN A) (NTN B) (NTN u)
NTN (app A B f a) = ap4 app (NTN A) (NTN B) (NTN f) (NTN a)

{- Derivability -}

data NJudgment : Set where
  njudgment : {n : ℕ} (Γ : N.Ctx Σ n) {k : JudgmentSort} → N2.Judgment Σ Γ 0 k → NJudgment

NDerivable : NJudgment → Prop
NDerivable (njudgment Γ j) = N2.Derivable (TTDer ΠUEl-TT) j

-- record NJudgment : Set where
--   constructor njudgment
--   field
--     {NJn} : ℕ
--     NJΓ : N.Ctx (TTSig ΠUEl-TT4)  NJn
--     {NJk} : JudgmentSort
--     NJj : N2.Judgment (TTSig ΠUEl-TT4) NJΓ 0 NJk

-- open NJudgment

-- record NDerivable (j : NJudgment) : Prop where
--   constructor ´_

--   field
--     `_ : N2.Derivable (TTDer ΠUEl-TT4) (NJj j)

-- open NDerivable

--   -- `_ : NDerivable (njudgment Γ j) → N2.Derivable (TTDer ΠUEl-TT) j
--   -- `_ d = d

--   -- ´_ : {n : ℕ} {Γ : N.Ctx Σ n} {k : JudgmentSort} {j : N2.Judgment Σ Γ 0 k} → N2.Derivable (TTDer ΠUEl-TT) j → NDerivable (njudgment Γ j)
--   -- ´_ d = d

NDerivable= : {j j' : NJudgment} (j= : j ≡ j') → NDerivable j' → NDerivable j
NDerivable= refl x = x

NDerivable=! : {j j' : NJudgment} (j= : j ≡ j') → NDerivable j → NDerivable j'
NDerivable=! refl x = x

T→NCtx : {n : ℕ} → T.Ctx n → N.Ctx Σ n
T→NCtx ◇ = ◇
T→NCtx (Γ , A) = (T→NCtx Γ , T→N A)

T→NJ : T.Judgment → NJudgment
T→NJ (Γ ⊢ A) = njudgment (T→NCtx Γ) (◇ ⊢ T→N A)
T→NJ (Γ ⊢ u :> A) = njudgment (T→NCtx Γ) (◇ ⊢ T→N u :> T→N A)
T→NJ (Γ ⊢ A == B) = njudgment (T→NCtx Γ) (◇ ⊢ T→N A == T→N B)
T→NJ (Γ ⊢ u == v :> A) = njudgment (T→NCtx Γ) (◇ ⊢ T→N u == T→N v :> T→N A)

weaken-comm : {k : SyntaxSort} {n : ℕ} {A : T.Expr k n} (p : WeakPos n) → N.weaken p (T→N A) ≡ T→N (T.weaken p A)
weaken-comm {A = uu} p = refl
weaken-comm {A = el v} p = ap (λ z → sym new ([] , z)) (weaken-comm p)
weaken-comm {A = pi A B} p = ap2 (λ z z' → sym (prev (prev (prev (prev new)))) ([] , z , z')) (weaken-comm p) (weaken-comm (prev p))
weaken-comm {A = var x} p = refl --ap var (weakenV-comm p x)
weaken-comm {A = lam A B u} p = ap3 (λ z z' z'' → sym (prev (prev (prev new))) ([] , z , z' , z'')) (weaken-comm p) (weaken-comm (prev p)) (weaken-comm (prev p))
weaken-comm {A = app A B f a} p = ap4 (λ z z' z'' z''' → sym (prev (prev new)) ([] , z , z' , z'' , z''')) (weaken-comm p) (weaken-comm (prev p)) (weaken-comm p) (weaken-comm p)

VarPos→ℕ : {n : ℕ} → VarPos n → ℕ
VarPos→ℕ last = 0
VarPos→ℕ (prev k) = suc (VarPos→ℕ k)

fst-VarPos→ℕ : {Σ : Signature} {n : ℕ} (k : VarPos n) (Γ : N.Ctx Σ n) {def : _} → fst (N.get (VarPos→ℕ k) Γ $ def) ≡ k
fst-VarPos→ℕ last (Γ , A) = refl
fst-VarPos→ℕ (prev k) (Γ , A) = ap prev (fst-VarPos→ℕ k Γ)

snd-VarPos→ℕ : {n : ℕ} (k : VarPos n) (Γ : T.Ctx n) {def : _} → snd (N.get (VarPos→ℕ k) (T→NCtx Γ) $ def) ≡ T→N (T.get k Γ)
snd-VarPos→ℕ last (Γ , A) = weaken-comm last
snd-VarPos→ℕ (prev k) (Γ , A) = ap (N.weaken last) (snd-VarPos→ℕ k Γ) ∙ weaken-comm last

get-def : {n : ℕ} (k : VarPos n) (Γ : T.Ctx n) → isDefined (N.get (VarPos→ℕ k) (T→NCtx Γ))
get-def last (Γ , A) = tt
get-def (prev k) (Γ , A) = (get-def k Γ , tt)

MorInsert : {Σ : Signature} (x : WeakPos m) (δ : N.Mor Σ n m) (u : N.TmExpr Σ n) → N.Mor Σ n (suc m)
MorInsert last δ u = (δ , u)
MorInsert (prev x) (δ , v) u = (MorInsert x δ u , v)

{-# REWRITE +O-rewrite #-}
{-# REWRITE +S-rewrite #-}
{-# REWRITE assoc #-}

weaken-MorInsert : {Σ : Signature} {n k : ℕ} {x : WeakPos n} {δ : N.Mor Σ k n} {u : N.TmExpr Σ k}
                 → N.weakenMor (MorInsert x δ u) ≡ MorInsert x (N.weakenMor δ) (N.weaken last u)
weaken-MorInsert {x = last} = refl
weaken-MorInsert {x = prev x} {δ , u} = ap2 _,_ weaken-MorInsert refl

Impossible : {n k : ℕ} {A : Prop} → suc (n + k) ≤ n → A
Impossible {suc n} {k = zero} (≤S p) = Impossible p
Impossible {suc n} {k = suc k} p = Impossible (≤P p)

weakenV-η : (x : WeakPos n) (y : VarPos n) {p : n ≤ n} → y ≡ weakenV {{p}} x y
weakenV-η x y {≤r} = ! weakenV≤r
weakenV-η x y {≤S p} = Impossible p

weaken-η  : {Σ : Signature} {k : _} {x : _} {p : n ≤ n} {u : N.Expr Σ n k} → u ≡ N.weaken {{p}} x u
weakenA-η : {Σ : Signature} {k : _} {x : _} {p : n ≤ n} {u : N.Args Σ n k} → u ≡ N.weakenA {{p}} x u

weaken-η {x = x} {u = var y} = ap var (weakenV-η x y)
weaken-η {u = sym s us} = ap (sym s) weakenA-η

weakenA-η {u = []} = refl
weakenA-η {u = u , x} = ap2 _,_ weakenA-η weaken-η

WeakPosIncl : {n m : ℕ} {{_ : n ≤ m}} → WeakPos n → WeakPos m
WeakPosIncl last = last
WeakPosIncl {m = suc m} {{p}} (prev x) = prev (WeakPosIncl {{≤P p}} x)

≤P-≤SS : {n m : ℕ} (p : n ≤ m) → p ≡ ≤P (≤SS {{p}})
≤P-≤SS ≤r = refl
≤P-≤SS (≤S p) = ap ≤S (≤P-≤SS _)

WeakPosIncl-comm : {n m k : ℕ} {{p : n ≤ m}} {x : WeakPos n} → weakenPos (≤-+ {m = k}) (WeakPosIncl {{p}} x) ≡ WeakPosIncl {{≤+ k {{p}}}} (weakenPos ≤-+ x)
WeakPosIncl-comm {k = zero} {x = last} = refl
WeakPosIncl-comm {k = suc k} {x = last} = ap prev (WeakPosIncl-comm {k = k} {x = last} ∙ ap (λ z → WeakPosIncl {{z}} (weakenPos ≤-+ last)) (≤P-≤SS _))
WeakPosIncl-comm {m = suc m} {zero} {x = prev x} = refl
WeakPosIncl-comm {m = suc m} {suc k} {x = prev x} = ap prev (WeakPosIncl-comm {m = suc m} {k = k} {x = prev x} ∙ ap (λ z → WeakPosIncl {{z}} (weakenPos ≤-+ (prev x))) (≤P-≤SS _))

≤-ishProp : {n m : ℕ} (p q : n ≤ m) → p ≡ q
≤-ishProp ≤r ≤r = refl
≤-ishProp ≤r (≤S q) = Impossible q
≤-ishProp (≤S p) ≤r = Impossible p
≤-ishProp (≤S p) (≤S q) = ap ≤S (≤-ishProp p q)

weakenV-μ : {n m k : ℕ} {{p : n ≤ m}} {{q : m ≤ k}} {{r : n ≤ k}} {x : VarPos n} {y : WeakPos n}
            → weakenV {{q}} (WeakPosIncl y) (weakenV {{p}} y x) ≡ weakenV {{r}} y x
weakenV-μ ⦃ p = ≤r ⦄ ⦃ ≤r ⦄ ⦃ ≤r ⦄ = weakenV≤r
weakenV-μ ⦃ p = ≤r ⦄ ⦃ ≤r ⦄ ⦃ ≤S r ⦄ = Impossible r
weakenV-μ ⦃ p = ≤r ⦄ ⦃ ≤S q ⦄ ⦃ ≤r ⦄ = Impossible q
weakenV-μ ⦃ p = ≤r ⦄ ⦃ ≤S q ⦄ ⦃ ≤S r ⦄ {x} {y = last} = ap2 (λ z z' → prev (weakenV ⦃ z ⦄ last z')) (≤-ishProp _ _) weakenV≤r
weakenV-μ ⦃ p = ≤r ⦄ ⦃ ≤S q ⦄ ⦃ ≤S r ⦄ {last} {y = prev y} = refl
weakenV-μ ⦃ p = ≤r ⦄ ⦃ ≤S q ⦄ ⦃ ≤S r ⦄ {prev x} {y = prev y} = ap prev (ap (weakenV {{≤P (≤S q)}} (WeakPosIncl y)) (! weakenV≤r) ∙ weakenV-μ {{≤r}} {{≤P (≤S q)}} {{≤P (≤S r)}} {x = x} {y})
weakenV-μ ⦃ p = ≤S p ⦄ ⦃ ≤r ⦄ ⦃ ≤r ⦄ = Impossible p
weakenV-μ ⦃ p = ≤S p ⦄ ⦃ ≤r ⦄ ⦃ ≤S r ⦄ {x} {y} = weakenV≤r {p = WeakPosIncl {{≤S p}} y} {v = weakenV {{≤S p}} y x} ∙ ap (λ z → weakenV ⦃ z ⦄ y x) (≤-ishProp _ _) --
weakenV-μ ⦃ p = ≤S p ⦄ ⦃ ≤S q ⦄ ⦃ ≤r ⦄ = Impossible (≤tr {{≤S p}} {{q}})
weakenV-μ ⦃ p = ≤S p ⦄ ⦃ ≤S q ⦄ ⦃ ≤S ≤r ⦄ = Impossible (≤tr {{q}} {{p}})
weakenV-μ ⦃ p = ≤S p ⦄ ⦃ ≤S q ⦄ ⦃ ≤S (≤S r) ⦄ {x} {y = last} = ap prev (weakenV-μ {{≤S p}} {{q}} {{≤S r}} {x} {last})
weakenV-μ ⦃ p = ≤S p ⦄ ⦃ ≤S q ⦄ ⦃ ≤S (≤S r) ⦄ {last} {y = prev y} = refl
weakenV-μ ⦃ p = ≤S p ⦄ ⦃ ≤S q ⦄ ⦃ ≤S (≤S r) ⦄ {prev x} {y = prev y} = ap prev (weakenV-μ {{≤P (≤S p)}} {{≤P (≤S q)}} {{≤P (≤S (≤S r))}} {x} {y})

weaken-μ  : {Σ : Signature} {k : _} {x : WeakPos n} {q : n ≤ m} {r : _} {u : N.Expr Σ n k} → N.weaken  {{≤S ≤r}} (WeakPosIncl {{q}} x) (N.weaken  {{q}} x u) ≡ N.weaken  {{r}} x u
weakenA-μ : {Σ : Signature} {k : _} {x : WeakPos n} {q : n ≤ m} {r : _} {u : N.Args Σ n k} → N.weakenA {{≤S ≤r}} (WeakPosIncl {{q}} x) (N.weakenA {{q}} x u) ≡ N.weakenA {{r}} x u

weaken-μ {x = y} {q = p} {u = var x} = ap var ((weakenV-μ {{p}} {{≤S ≤r}} {{_}} {x = x} {y = y}))
weaken-μ {u = sym s x} = ap (sym s) weakenA-μ

weakenA-μ {u = []} = refl
weakenA-μ {q = q} {u = u , x} = ap2 _,_ weakenA-μ (ap2 (λ z z' → N.weaken {{z}} z' (N.weaken {{≤+ _ {{q}}}} _ x))
                                                       (≤-ishProp _ _)
                                                       (WeakPosIncl-comm {{q}})
                                                   ∙ weaken-μ {q = ≤+ _ {{q}}})

weaken+-MorInsert : {Σ : Signature} (m : ℕ) {n k : ℕ} {x : WeakPos n} {δ : N.Mor Σ k n} {u : N.TmExpr Σ k}
                    → N.weakenMor+ m (MorInsert x δ u) ≡ MorInsert (weakenPos ≤-+ x) (N.weakenMor+ m δ) (N.weaken last u)
weaken+-MorInsert zero = ap (MorInsert _ _) weaken-η
weaken+-MorInsert (suc m) = ap2 _,_ (ap N.weakenMor (weaken+-MorInsert m) ∙ weaken-MorInsert ∙ ap (MorInsert _ _) weaken-μ) refl

SubstV-insert : {n m : ℕ} {y : VarPos n} {x : WeakPos n} {u : N.TmExpr Σ m} {δ : N.Mor Σ m n} {p : n ≤ suc n}
                → SubstMor (var (weakenV {{p}} x y)) (MorInsert x δ u) ≡ SubstMor (var y) δ
SubstV-insert {x = last} {δ = δ} {p = ≤S ≤r} = ap (λ z → SubstMor (var z) δ) weakenV≤r
SubstV-insert {y = last} {x = prev x} {δ = δ , v} {p = ≤S ≤r} = refl
SubstV-insert {y = prev y} {x = prev x} {u} {δ = δ , v} {p = ≤S ≤r} = SubstV-insert {y = y} {x = x} {u = u} {δ = δ} {p = ≤S ≤r}
SubstV-insert {p = ≤S (≤S p)} = Impossible p

Subst-insert  : {k : SyntaxSort} {n m : ℕ} {e : N.Expr Σ n k} {x : WeakPos n} {u : N.TmExpr Σ m} {δ : N.Mor Σ m n} {p : _}
                → SubstMor (N.weaken {{p}} x e) (MorInsert x δ u) ≡ SubstMor e δ
SubstA-insert : {args : SyntaxArityArgs} {n m : ℕ} {es : N.Args Σ n args} {x : WeakPos n} {u : N.TmExpr Σ m} {δ : N.Mor Σ m n} {p : _}
                → SubstAMor (N.weakenA {{p}} x es) (MorInsert x δ u) ≡ SubstAMor es δ

Subst-insert {e = var x} {x = x'} {u} {p = p} = SubstV-insert {x = x'} {u} {p = p}
Subst-insert {e = sym s x} = ap (sym s) SubstA-insert

SubstA-insert {es = []} = refl
SubstA-insert {args} {n} {es = _,_ {m = m} es e} {x = x} {u = u} {p = p} =
  ap2 _,_ SubstA-insert (ap (SubstMor (N.weaken {{≤+ m {n} {suc n} {{p}}}} (weakenPos ≤-+ x) e)) (weaken+-MorInsert m) ∙ Subst-insert {e = e} {x = weakenPos ≤-+ x})

weakenMor+-idMor : {n : ℕ} (m : ℕ) → N.weakenMor+ m (N.idMor {Σ = Σ} {n = n}) ≡ N.idMor
weakenMor+-idMor zero = refl
weakenMor+-idMor (suc m) = ap2 _,_ (ap N.weakenMor (weakenMor+-idMor m)) refl

SubstMor-weakenMor : {x : VarPos n} {δ : N.Mor Σ m n} → SubstMor (var x) (N.weakenMor δ) ≡ N.weaken last (SubstMor (var x) δ)
SubstMor-weakenMor {x = last} {δ , u} = refl
SubstMor-weakenMor {x = prev x} {δ , u} = SubstMor-weakenMor {x = x} {δ}

SubstMor-idMor  : {n : ℕ} {k : _} (e  : N.Expr Σ n k) → SubstMor e N.idMor ≡ e
SubstAMor-idMor : {n : ℕ} {k : _} (es : N.Args Σ n k) → SubstAMor es N.idMor ≡ es

SubstMor-idMor (var last) = refl
SubstMor-idMor (var (prev x)) = SubstMor-weakenMor {x = x} {δ = N.idMor} ∙ ap (N.weaken last) (SubstMor-idMor (var x)) ∙ ap var (ap prev weakenV≤r)
SubstMor-idMor (sym s es) = ap (sym s) (SubstAMor-idMor es)

SubstAMor-idMor [] = refl
SubstAMor-idMor (_,_ {m = m} es x) = ap2 _,_ (SubstAMor-idMor es) (ap (SubstMor x) (weakenMor+-idMor m) ∙ SubstMor-idMor x)

Subst-insert-idMor : {k : SyntaxSort} {e : N.Expr Σ n k} {x : WeakPos n} {u : N.TmExpr Σ n} {p : _}
                    → SubstMor (N.weaken {{p}} x e) (MorInsert x N.idMor u) ≡ e
Subst-insert-idMor {e = e} {x} {u} {p} = Subst-insert {e = e} {x} {u} {N.idMor} {p} ∙ SubstMor-idMor e

inj : WeakPos n → WeakPos (suc n)
inj last = last
inj (prev x) = prev (inj x)

weakenPos-inj : {m : ℕ} (x : WeakPos n) → weakenPos (≤-+ {m = m}) (inj x) ≡ inj (weakenPos ≤-+ x)
weakenPos-inj {m = zero} x = refl
weakenPos-inj {m = suc m} last = ap prev (weakenPos-inj last)
weakenPos-inj {m = suc m} (prev x) = ap prev (weakenPos-inj (prev x))

SubstV-insert2 : {n m : ℕ} {y : VarPos n} {x : WeakPos n} {u : N.TmExpr Σ (suc m)} {δ : N.Mor Σ (suc m) (suc n)} {p : _}
                → SubstMor (var (weakenV {{≤S p}} x y)) (MorInsert (inj x) δ u) ≡ SubstMor (var (weakenV {{p}} x y)) δ
SubstV-insert2 {y = last} {last} = refl
SubstV-insert2 {y = prev y} {last} = refl
SubstV-insert2 {y = last} {prev x} {δ = δ , u} = refl
SubstV-insert2 {y = prev y} {prev x} {δ = δ , u} {≤S ≤r} = SubstV-insert2 {y = y} {x = x} {δ = δ}
SubstV-insert2 {y = prev y} {prev x} {δ = δ , u} {≤S (≤S p)} = Impossible p

Subst-insert2  : {k : SyntaxSort} {n m : ℕ} {e : N.Expr Σ n k} {x : WeakPos n} {u : N.TmExpr Σ (suc m)} {δ : N.Mor Σ (suc m) (suc n)} {p : _}
                 → SubstMor (N.weaken {{≤S p}} x e) (MorInsert (inj x) δ u) ≡ SubstMor (N.weaken {{p}} x e) δ
SubstA-insert2  : {args : SyntaxArityArgs} {n m : ℕ} {es : N.Args Σ n args} {x : WeakPos n} {u : N.TmExpr Σ (suc m)} {δ : N.Mor Σ (suc m) (suc n)} {p : _}
                 → SubstAMor (N.weakenA {{≤S p}} x es) (MorInsert (inj x) δ u) ≡ SubstAMor (N.weakenA {{p}} x es) δ

Subst-insert2 {e = var y} {x = x} = SubstV-insert2 {y = y} {x = x}
Subst-insert2 {e = sym s es} = ap (sym s) SubstA-insert2

SubstA-insert2 {es = []} = refl
SubstA-insert2 {n = n} {m = m'} {es = _,_ {m = m} es e} {x = x} {u = u} =
  ap2 _,_ SubstA-insert2 ((ap (SubstMor (N.weaken {{_}} (weakenPos ≤-+ x) e)) (weaken+-MorInsert m ∙ ap3 MorInsert (weakenPos-inj x) refl refl)
                          ∙ ap
                              (λ z →
                                 SubstMor (N.weaken ⦃ z ⦄ (weakenPos ≤-+ x) e)
                                 (MorInsert (inj (weakenPos ≤-+ x)) (N.weakenMor+ m {n = suc n} {m = suc m'} _)
                                  (N.weaken last u)))
                              (≤-ishProp _ _) ∙ Subst-insert2 {e = e} {x = weakenPos ≤-+ x} {u = N.weaken last u}))

Subst-insert-idMor2 : {k : SyntaxSort} {e : N.Expr Σ n k} {x : WeakPos n} {u : N.TmExpr Σ (suc n)}
                    → SubstMor (N.weaken x e) (MorInsert (inj x) (N.idMor {n = suc n}) u) ≡ N.weaken {{≤S ≤r}} x e
Subst-insert-idMor2 {e = e} {x} {u} = Subst-insert2 {e = e} {x} {u} {N.idMor} ∙ SubstMor-idMor _

T→NMor : T.Mor n m → N.Mor Σ n m
T→NMor ◇ = ◇
T→NMor (δ , u) = (T→NMor δ , T→N u)

weakenMor-comm : {δ : T.Mor n m} → N.weakenMor (T→NMor δ) ≡ T→NMor (T.weakenMor δ)
weakenMor-comm {δ = ◇} = refl
weakenMor-comm {δ = δ , u} = ap2 _,_ weakenMor-comm (weaken-comm last)

substV-lemma : (x : VarPos n) {δ : T.Mor m n} → SubstMor (var x) (T→NMor δ) ≡ T→N (var x [ δ ])
substV-lemma last {δ , u} = refl
substV-lemma (prev x) {δ , u} = substV-lemma x

subst-lemma : {k : _} (B : T.Expr k n) {δ : T.Mor m n} → SubstMor (T→N B) (T→NMor δ) ≡ T→N (B [ δ ])
subst-lemma uu = refl
subst-lemma (el v) = ap (λ z → sym new ([] , z)) (subst-lemma v)
subst-lemma (pi A B) = ap2 (λ z z' → sym (prev (prev (prev (prev new)))) ([] , z , z')) (subst-lemma A) (ap (SubstMor (T→N B)) (ap2 _,_ weakenMor-comm refl) ∙ subst-lemma B)
subst-lemma (var x) = substV-lemma x
subst-lemma (lam A B u) = ap3 (λ z z' z'' → sym (prev (prev (prev new))) ([] , z , z' , z''))
                            (subst-lemma A) (ap (SubstMor (T→N B)) (ap2 _,_ weakenMor-comm refl) ∙ subst-lemma B) (ap (SubstMor (T→N u)) (ap2 _,_ weakenMor-comm refl) ∙ subst-lemma u)
subst-lemma (app A B f a) = ap4
                              (λ z z' z'' z''' →
                                 sym (prev (prev new)) ([] , z , z' , z'' , z'''))
                              (subst-lemma A) (ap (SubstMor (T→N B)) (ap2 _,_ weakenMor-comm refl) ∙ subst-lemma B) (subst-lemma f) (subst-lemma a)

idMor-lemma : {n : ℕ} → N.idMor {n = n} ≡ T→NMor T.idMor
idMor-lemma {zero} = refl
idMor-lemma {suc n} = ap2 _,_ (ap N.weakenMor idMor-lemma ∙ weakenMor-comm) refl

Subst-T→N : {k : _} (B : T.Expr k (suc n)) (a : T.TmExpr n) → N.SubstMor (T→N B) (N.idMor , T→N a) ≡ T→N (T.subst B a)
Subst-T→N B a = ap (λ z → SubstMor (T→N B) (z , T→N a)) idMor-lemma ∙ subst-lemma B

-- T→NDer : {j : T.Judgment} → T.Derivable j → NDerivable (T→NJ j)
-- T→NDer (Var {Γ = Γ} k dA) = NDerivable=! (ap (λ x → njudgment (T→NCtx Γ) (◇ ⊢ var x :> T→N (T.get k Γ))) (fst-VarPos→ℕ k (T→NCtx Γ))) (´ apr S (var (VarPos→ℕ k)) ([] ,0Ty ` T→NDer dA) {{get-def k Γ , (snd-VarPos→ℕ k Γ , tt)}})
-- T→NDer (TyRefl dA) = ´ apr S tyRefl ([] , ` T→NDer dA)
-- T→NDer (TySymm dA=) = ´ apr S tySymm ([] , ` T→NDer dA=)
-- T→NDer (TyTran dA= dB=) = ´ apr S tyTran ([] , ` T→NDer dA= , ` T→NDer dB=)
-- T→NDer (TmRefl du) = ´ apr S tmRefl ([] , ` T→NDer du)
-- T→NDer (TmSymm du=) = ´ apr S tmSymm ([] , ` T→NDer du=)
-- -- T→NDer (TmTran du= dv=) = apr S tmTran ([] , T→NDer du= , T→NDer dv=)
-- -- T→NDer (Conv du dA=) = apr S conv ([] , T→NDer du , T→NDer dA=)
-- -- T→NDer (ConvEq du= dA=) = apr S convEq ([] , T→NDer du= , T→NDer dA=)
-- -- T→NDer UU = apr T 1 []
-- -- T→NDer UUCong = apr C 1 []
-- -- T→NDer (El dv) = apr T 0 ([] ,0Tm T→NDer dv)
-- -- T→NDer (ElCong dv=) = apr C 0 ([] ,0Tm= T→NDer dv=)
-- -- T→NDer (Pi dA dB) = apr T 4 ([] ,0Ty T→NDer dA ,1Ty T→NDer dB)
-- -- T→NDer (PiCong dA= dB=) = apr C 4 ([] ,0Ty= T→NDer dA= ,1Ty= T→NDer dB=)
-- -- T→NDer (Lam {A = A} {B = B} {u = u} dA dB du) =
-- --   NDerivable=! (ap (λ z → njudgment _ (◇ ⊢ sym (prev (prev (prev new))) ([] , T→N _ , T→N _ , T→N _) :> sym (prev (prev (prev (prev new)))) ([] , T→N _ , z))) Subst-insert-idMor)
-- --                (apr T 3 ([] ,0Ty T→NDer dA ,1Ty T→NDer dB ,1Tm NDerivable= (ap (λ z → njudgment _ (◇ ⊢ T→N _ :> z)) Subst-insert-idMor) (T→NDer du)))
-- -- T→NDer (LamCong dA= dB= du=) =
-- --   NDerivable=! (ap (λ z → njudgment _ (◇ ⊢ sym (prev (prev (prev new))) ([] , T→N _ , T→N _ , T→N _) == sym (prev (prev (prev new))) ([] , T→N _ , T→N _ , T→N _) :> sym (prev (prev (prev (prev new)))) ([] , T→N _ , z)))
-- --                    Subst-insert-idMor)
-- --     (apr C 3 ([] ,0Ty= T→NDer dA= ,1Ty= T→NDer dB= ,1Tm= NDerivable= (ap (λ z → njudgment _ (◇ ⊢ T→N _ == T→N _ :> z)) Subst-insert-idMor) (T→NDer du=)))
-- -- T→NDer (App {A = A} {B} {f} {a} dA dB df da) =
-- --   NDerivable=! (ap (λ z → njudgment _ (◇ ⊢ sym (prev (prev new)) ([] , T→N A , T→N B , T→N f , T→N a) :> z)) (Subst-T→N B a))
-- --     (apr T 2 ([] ,0Ty T→NDer dA
-- --                  ,1Ty T→NDer dB
-- --                  ,0Tm NDerivable= (ap (λ z → njudgment _ (◇ ⊢ T→N f :> sym (prev (prev (prev (prev new)))) ([] , T→N A , z))) Subst-insert-idMor) (T→NDer df)
-- --                  ,0Tm T→NDer da))
-- -- T→NDer (AppCong {A = A} {A' = A'} {B = B} {B' = B'} {f = f} {f' = f'} {a = a} {a' = a'} dA= dB= df= da=) =
-- --   NDerivable=! (ap (λ z → njudgment _ (◇ ⊢ sym (prev (prev new)) ([] , T→N A , T→N B , T→N f , T→N a) == sym (prev (prev new)) ([] , T→N A' , T→N B' , T→N f' , T→N a') :> z)) (Subst-T→N B a))
-- --     (apr C 2 ([] ,0Ty= T→NDer dA=
-- --                  ,1Ty= T→NDer dB=
-- --                  ,0Tm= NDerivable= (ap (λ z → njudgment _ (◇ ⊢ T→N f == T→N f' :> sym (prev (prev (prev (prev new)))) ([] , T→N A , z))) Subst-insert-idMor)
-- --                                    (T→NDer df=)
-- --                  ,0Tm= T→NDer da=))
-- -- T→NDer (BetaPi {A = A} {B = B} {u = u} {a = a} dA dB du da) =
-- --   NDerivable=! (ap4
-- --                   (λ z z' z'' z''' →
-- --                      njudgment _
-- --                      (◇ ⊢
-- --                       sym (prev (prev new))
-- --                       ([] , T→N A , z ,
-- --                        sym (prev (prev (prev new))) ([] , T→N A , z , z')
-- --                        , T→N a)
-- --                       == z'' :> z'''))
-- --                   Subst-insert-idMor Subst-insert-idMor (Subst-T→N u a) (Subst-T→N B a))
-- --                (apr Eq 1 ([] ,0Ty T→NDer dA ,1Ty T→NDer dB ,1Tm NDerivable= (ap (λ z → njudgment _ (◇ ⊢ T→N u :> z)) Subst-insert-idMor) (T→NDer du) ,0Tm T→NDer da))
-- -- T→NDer (EtaPi {n = n} {A = A} {B = B} {f = f} dA dB df) =
-- --   NDerivable=! (ap4
-- --                   (λ z z' z'' z''' →
-- --                      njudgment _
-- --                      (◇ ⊢ T→N f ==
-- --                       sym (prev (prev (prev new)))
-- --                       ([] , T→N A , z ,
-- --                        sym (prev (prev new)) ([] , z' , z'' , z''' , var last))
-- --                       :> sym (prev (prev (prev (prev new)))) ([] , T→N A , z)))
-- --                   Subst-insert-idMor (weaken-comm last) (Subst-insert-idMor2 ∙ weaken-comm (prev last)) (weaken-comm last))
-- --                (apr Eq 0 ([] ,0Ty T→NDer dA
-- --                              ,1Ty T→NDer dB
-- --                              ,0Tm NDerivable= (ap (λ z → njudgment _ (◇ ⊢ T→N f :> sym (prev (prev (prev (prev new)))) ([] , T→N A , z))) Subst-insert-idMor) (T→NDer df)))

N→TCtx : {n : ℕ} → N.Ctx Σ n → T.Ctx n
N→TCtx ◇ = ◇
N→TCtx (Γ , A) = (N→TCtx Γ , N→T A)

N→TMor : {n m : ℕ} → N.Mor Σ n m → T.Mor n m
N→TMor ◇ = ◇
N→TMor (δ , u) = (N→TMor δ , N→T u)

weaken-comm' : {k : SyntaxSort} {n : ℕ} {A : N.Expr Σ n k} (p : WeakPos n) → N→T (N.weaken p A) ≡ T.weaken p (N→T A)
weaken-comm' p = ap N→T (ap (N.weaken p) (! (TNT _))) ∙ ap N→T (weaken-comm p) ∙ NTN _

get-eq : {n : ℕ} (k : ℕ) (Γ : N.Ctx Σ n) {def : _} → N→T (snd (N.get k Γ $ def)) ≡ T.get (fst (N.get k Γ $ def)) (N→TCtx Γ)
get-eq zero (Γ , A) = weaken-comm' last
get-eq (suc k) (Γ , A) = weaken-comm' last ∙ ap (T.weaken last) (get-eq k Γ)

N→TJ : NJudgment → T.Judgment
N→TJ (njudgment Γ (◇ ⊢ A)) = N→TCtx Γ ⊢ N→T A
N→TJ (njudgment Γ (◇ ⊢ u :> A)) = N→TCtx Γ ⊢ N→T u :> N→T A
N→TJ (njudgment Γ (◇ ⊢ A == B)) = N→TCtx Γ ⊢ N→T A == N→T B
N→TJ (njudgment Γ (◇ ⊢ u == v :> A)) = N→TCtx Γ ⊢ N→T u == N→T v :> N→T A

congTy : {Γ : T.Ctx n} {A A' : T.TyExpr n} → A ≡ A' → T.Derivable (Γ ⊢ A) → T.Derivable (Γ ⊢ A')
congTy refl d = d

congTmTy : {Γ : T.Ctx n} {u : T.TmExpr n} {A A' : T.TyExpr n} → A ≡ A' → T.Derivable (Γ ⊢ u :> A) → T.Derivable (Γ ⊢ u :> A')
congTmTy refl d = d

congTmTy! : {Γ : T.Ctx n} {u : T.TmExpr n} {A A' : T.TyExpr n} → A' ≡ A → T.Derivable (Γ ⊢ u :> A) → T.Derivable (Γ ⊢ u :> A')
congTmTy! refl d = d

congTmEqTy : {Γ : T.Ctx n} {u u' : T.TmExpr n} {A A' : T.TyExpr n} → A ≡ A' → T.Derivable (Γ ⊢ u == u' :> A) → T.Derivable (Γ ⊢ u == u' :> A')
congTmEqTy refl d = d

congTmEqTy! : {Γ : T.Ctx n} {u u' : T.TmExpr n} {A A' : T.TyExpr n} → A' ≡ A → T.Derivable (Γ ⊢ u == u' :> A) → T.Derivable (Γ ⊢ u == u' :> A')
congTmEqTy! refl d = d

congTmEq : {Γ : T.Ctx n} {u u' v v' : T.TmExpr n} {A A' : T.TyExpr n} → A ≡ A' → u ≡ u' → v ≡ v' → T.Derivable (Γ ⊢ u == v :> A) → T.Derivable (Γ ⊢ u' == v' :> A')
congTmEq refl refl refl d = d

congTmEq! : {Γ : T.Ctx n} {u u' v v' : T.TmExpr n} {A A' : T.TyExpr n} → A' ≡ A → u' ≡ u → v' ≡ v → T.Derivable (Γ ⊢ u == v :> A) → T.Derivable (Γ ⊢ u' == v' :> A')
congTmEq! refl refl refl d = d

N→T-Subst : {k : _} (B : N.Expr Σ (suc n) k) (a : N.TmExpr Σ n) → N→T (SubstMor B (N.idMor , a)) ≡ T.subst (N→T B) (N→T a)
N→T-Subst B a = ap N→T (! (ap2 SubstMor (TNT B) (ap2 _,_ refl (TNT a))) ∙ Subst-T→N (N→T B) (N→T a)) ∙ NTN _

N→TDer : {j : NJudgment} → NDerivable j → T.Derivable (N→TJ j)

-- N→TDer {njudgment Γ _} (apr S (var k) {js = [] , ◇ ⊢ A} ([] , dA) {{xᵈ , (refl , tt)}}) = congTmTy! (get-eq k Γ) (Var (fst (N.get k Γ $ xᵈ)) (congTy (get-eq k Γ) (N→TDer dA)))
-- N→TDer {njudgment Γ _} (apr S conv {js = [] , ◇ ⊢ u :> A , ◇ ⊢ A == B} ([] , du , dA=) {{refl , tt}}) = Conv (N→TDer du) (N→TDer dA=)
-- N→TDer {njudgment Γ _} (apr S convEq {js = [] , ◇ ⊢ u == v :> A , ◇ ⊢ A == B} ([] , du= , dA=) {{refl , tt}}) = ConvEq (N→TDer du=) (N→TDer dA=)
-- N→TDer {njudgment Γ _} (apr S tyRefl {js = [] , ◇ ⊢ A} ([] , dA)) = TyRefl (N→TDer dA)
-- N→TDer {njudgment Γ _} (apr S tySymm {js = [] , ◇ ⊢ A == B} ([] , dA=)) = TySymm (N→TDer dA=)
-- N→TDer {njudgment Γ _} (apr S tyTran {js = [] , ◇ ⊢ A == B , ◇ ⊢ B == D} ([] , dA= , dB=) {{refl , tt}}) = TyTran (N→TDer dA=) (N→TDer dB=)
-- N→TDer {njudgment Γ _} (apr S tmRefl {js = [] , ◇ ⊢ u :> A} ([] , du)) = TmRefl (N→TDer du)
-- N→TDer {njudgment Γ _} (apr S tmSymm {js = [] , ◇ ⊢ u == v :> A} ([] , du=)) = TmSymm (N→TDer du=)
-- N→TDer {njudgment Γ _} (apr S tmTran {js = [] , ◇ ⊢ u == v :> A , ◇ ⊢ v == w :> A} ([] , du= , dv=) {{refl , (refl , tt)}}) = TmTran (N→TDer du=) (N→TDer dv=)
-- N→TDer {njudgment Γ _} (apr T typingrule {js = [] , (◇ ⊢ v :> _)} ([] , dv) {{(tt , (tt , (refl , tt))) , tt}}) = El (N→TDer dv)
-- N→TDer {njudgment Γ _} (apr T (prev typingrule) []) = UU
-- N→TDer {njudgment Γ _} (apr T (prev (prev typingrule)) {js = [] , ◇ ⊢ A , (◇ , _) ⊢ B , (◇ ⊢ f :> _) , (◇ ⊢ a :> _)} ([] , dA , dB , df , da)
--                            {{(((((tt , (tt , tt)) , ((tt , refl) , tt)) , (tt , (refl , tt))) , (tt , (refl , tt))) , tt)}}) = congTmTy! (N→T-Subst B a) (App (N→TDer dA) (N→TDer dB) (congTmTy (ap (pi (N→T A)) (ap N→T Subst-insert-idMor)) (N→TDer df)) (N→TDer da))
-- N→TDer {njudgment Γ _} (apr T (prev (prev (prev typingrule))) {js = [] , ◇ ⊢ A , ((◇ , A) ⊢ B) , ((◇ , A) ⊢ u :> B')} ([] , dA , dB , du) {{(((tt , (tt , tt)) , ((tt , refl) , tt)) , ((tt , refl) , (refl , tt)) ) , tt}})
--   = congTmTy! (ap (pi (N→T A)) (ap N→T Subst-insert-idMor)) (Lam (N→TDer dA) (N→TDer dB) (congTmTy (ap N→T Subst-insert-idMor) (N→TDer du)))
-- N→TDer {njudgment Γ _} (apr T (prev (prev (prev (prev typingrule)))) {js = [] , ◇ ⊢ A , (◇ , ._) ⊢ B} ([] , dA , dB) {{((tt , (tt , tt)) , ((tt , refl) , tt)) , tt}}) = Pi (N→TDer dA) (N→TDer dB)
-- N→TDer {njudgment Γ _} (apr C congruencerule {js = [] , ◇ ⊢ v == v' :> _} ([] , dv=) {{((tt , (tt , (refl , tt))) , tt)}}) = ElCong (N→TDer dv=)
-- N→TDer {njudgment Γ _} (apr C (prev congruencerule) []) = UUCong
-- N→TDer {njudgment Γ _} (apr C (prev (prev congruencerule)) {js = [] , ◇ ⊢ A == A' , (◇ , _) ⊢ B == B' , (◇ ⊢ f == f' :> _) , (◇ ⊢ a == a' :> _)} ([] , dA= , dB= , df= , da=)
--   {{(((((tt , (tt , tt)) , ((tt , refl) , tt)) , (tt , (refl , tt))) , (tt , (refl , tt))) , tt)}})
--    = congTmEqTy! (N→T-Subst B a) (AppCong (N→TDer dA=) (N→TDer dB=) (congTmEqTy (ap (pi (N→T A)) (ap N→T Subst-insert-idMor)) (N→TDer df=)) (N→TDer da=))
-- N→TDer {njudgment Γ _} (apr C (prev (prev (prev congruencerule))) {js = [] , ◇ ⊢ A == A' , ((◇ , A) ⊢ B == B') , ((◇ , A) ⊢ u == u' :> B'')} ([] , dA= , dB= , du=) {{(((tt , (tt , tt)) , ((tt , refl) , tt)) , ((tt , refl) , (refl , tt)) ) , tt}}) = congTmEqTy! (ap (pi (N→T A)) (ap N→T Subst-insert-idMor)) (LamCong (N→TDer dA=) (N→TDer dB=) (congTmEqTy (ap N→T Subst-insert-idMor) (N→TDer du=)))
-- N→TDer {njudgment Γ _} (apr C (prev (prev (prev (prev congruencerule)))) {js = [] , ◇ ⊢ A == A' , (◇ , ._) ⊢ B == B'} ([] , dA= , dB=) {{(((tt , (tt , tt)) , ((tt , refl) , tt)) , tt)}}) = PiCong (N→TDer dA=) (N→TDer dB=)
-- N→TDer {njudgment Γ _} (apr Eq equalityrule js-der) = {!Eta!}
N→TDer {njudgment Γ _} (apr Eq (prev equalityrule) {js = [] , (◇ ⊢ A) , ((◇ , _) ⊢ B) , ((◇ , _) ⊢ u :> _) , (◇ ⊢ a :> _)} ([] , dA , dB , du , da)
  {{(((((tt , (tt , tt)) , ((tt , refl) , tt)) , ((tt , refl) , (refl , tt))) , (tt , (refl , tt))) , tt)}})
   = {!da --jdef --congTmEq! ? ? ? (BetaPi (N→TDer dA) (N→TDer dB) (congTmTy (ap N→T Subst-insert-idMor) (N→TDer du)) (N→TDer da))!}

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


text:
{-# OPTIONS --rewriting --confluence-check #-}

open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

variable
  A B : Set
  x y z : A
  xs ys zs : List A
  f : A → B
  m n : Nat

cong : (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

trans : x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

+zero : m + zero ≡ m
+zero {zero} = refl
+zero {suc m} = cong suc +zero

suc+zero : suc m + zero ≡ suc m
suc+zero = +zero

+suc : m + (suc n) ≡ suc (m + n)
+suc {zero} = refl
+suc {suc m} = cong suc +suc

zero+suc : zero + (suc n) ≡ suc n
zero+suc = refl

suc+suc : (suc m) + (suc n) ≡ suc (suc (m + n))
suc+suc = cong suc +suc

{-# REWRITE +zero +suc suc+zero zero+suc suc+suc #-}

map : (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = (f x) ∷ (map f xs)

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

++-[] : xs ++ [] ≡ xs
++-[] {xs = []} = refl
++-[] {xs = x ∷ xs} = cong (_∷_ x) ++-[]

∷-++-[] : (x ∷ xs) ++ [] ≡ x ∷ xs
∷-++-[] = ++-[]

map-id : map (λ x → x) xs ≡ xs
map-id {xs = []} = refl
map-id {xs = x ∷ xs} = cong (_∷_ x) map-id

map-id-∷ : map (λ x → x) (x ∷ xs) ≡ x ∷ xs
map-id-∷ = map-id

{-# REWRITE ++-[] ∷-++-[] #-}
{-# REWRITE map-id map-id-∷ #-}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Luau.Var.ToString where

open import Agda.Builtin.String using (String)
open import Luau.Var using (Var)

varToString : Var → String
varToString x = x

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
module Issue739 where

record ⊤ : Set where
  constructor tt

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

uncurry : {A : Set} {B : A → Set} →
          ((x : A) → B x → Set) →
          Σ A B → Set
uncurry f (x , y) = f x y

data U : Set₁

El : U → Set

infixl 5 _▻_

data U where
  ε   : U
  _▻_ : (u : U) → (El u → Set) → U

El ε       = ⊤
El (u ▻ P) = Σ (El u) P

Id : ∀ u → (El u → Set) → El u → Set
Id u P = P

-- Type-checks:

works : U
works =
  ε
  ▻ (λ _ → ⊤)
  ▻ (λ { (_ , _) → ⊤ })

-- Type-checks:

works′ : U
works′ =
  ε
  ▻ (λ _ → ⊤)
  ▻ Id (_ ▻ _) (λ { (_ , _) → ⊤ })

-- Type-checks:

works″ : U
works″ =
  ε
  ▻ (λ _ → ⊤)
  ▻ Id _ (uncurry λ _ _ → ⊤)

-- Type-checks:

works‴ : U
works‴ =
  ε
  ▻ (λ _ → ⊤)
  ▻ Id _ const-⊤
  where
  const-⊤ : _ → _
  const-⊤ (_ , _) = ⊤

-- Type-checks:

works⁗ : U
works⁗ =
  ε
  ▻ (λ _ → ⊤)
  ▻ Id _ const-⊤
  where
  const-⊤ : _ → _
  const-⊤ = λ { (_ , _) → ⊤ }

-- Type-checks:

works′́ : U
works′́ =
  ε
  ▻ (λ _ → ⊤)
  ▻ Id _ (λ { _ → ⊤ })

-- Doesn't type-check (but I want to write something like this):

fails : U
fails =
  ε
  ▻ (λ _ → ⊤)
  ▻ Id _ (λ { (_ , _) → ⊤ })

-- Given all the working examples I'm led to believe that there is
-- something wrong with pattern-matching lambdas. Please correct me if
-- I'm wrong.

-- Andreas, 2012-10-29 should work now.

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import LogicalFormulae
open import Setoids.Setoids
open import Groups.Definition
open import Sets.EquivalenceRelations
open import Groups.Abelian.Definition
open import Groups.Homomorphisms.Definition
open import Groups.DirectSum.Definition
open import Groups.Isomorphisms.Definition

module Groups.Abelian.Lemmas where

directSumAbelianGroup : {m n o p : _} → {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} {underG : Group S _·A_} {underH : Group T _·B_} (G : AbelianGroup underG) (h : AbelianGroup underH) → (AbelianGroup (directSumGroup underG underH))
AbelianGroup.commutative (directSumAbelianGroup {A = A} {B} G H) = AbelianGroup.commutative G ,, AbelianGroup.commutative H

subgroupOfAbelianIsAbelian : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : B → A} {fHom : GroupHom H G f} → SetoidInjection T S f → AbelianGroup G → AbelianGroup H
AbelianGroup.commutative (subgroupOfAbelianIsAbelian {S = S} {_+B_ = _+B_} {fHom = fHom} fInj record { commutative = commutative }) {x} {y} = SetoidInjection.injective fInj (transitive (GroupHom.groupHom fHom) (transitive commutative (symmetric (GroupHom.groupHom fHom))))
  where
    open Setoid S
    open Equivalence eq

abelianIsGroupProperty : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} → GroupsIsomorphic G H → AbelianGroup H → AbelianGroup G
abelianIsGroupProperty iso abH = subgroupOfAbelianIsAbelian {fHom = GroupIso.groupHom (GroupsIsomorphic.proof iso)} (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof iso))) abH


text:
open import Agda.Primitive

variable
  a : Level

postulate
  works : Set a → {a : Set} → a
  fails : Set a → {a : Set} → {!a!}

module _ (A : Set a) (a : A) where
  x : A
  x = a


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

open import Cubical.ZCohomology.Base
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Hopf
open import Cubical.Homotopy.Freudenthal hiding (encode)
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Truncation renaming (elim to trElim ; rec to trRec ; map to trMap)

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv.HalfAdjoint

open import Cubical.Data.Int renaming (_+_ to +Int)
open import Cubical.Data.Nat

open import Cubical.HITs.Susp
open import Cubical.HITs.Nullification
open import Cubical.Data.Prod.Base
open import Cubical.Homotopy.Loopspace
open import Cubical.Data.Bool
open import Cubical.Data.Sum.Base
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.HITs.S3

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

{- We want to prove that Kn≃ΩKn+1. For this we use the map ϕ-}

ϕ : (pt a : A) → typ (Ω (Susp A , north))
ϕ pt a = (merid a) ∙ sym (merid pt)

  {- To define the map for n=0 we use the λ k → loopᵏ map for S₊ 1. The loop is given by ϕ north south -}

loop* : Path (S₊ 1) north north
loop* = ϕ north south

looper : Int → Path (S₊ 1) north north
looper (pos zero) = refl
looper (pos (suc n)) = looper (pos n) ∙ loop*
looper (negsuc zero) = sym loop*
looper (negsuc (suc n)) = looper (negsuc n) ∙ sym loop*

private

  {- The map of Kn≃ΩKn+1 is given as follows. -}
  Kn→ΩKn+1 : (n : ℕ) → coHomK n → typ (Ω (coHomK-ptd (suc n)))
  Kn→ΩKn+1 zero x = cong ∣_∣ (looper x)
  Kn→ΩKn+1 (suc n) = trRec (isOfHLevelTrunc (2 + (suc (suc n))) ∣ north ∣ ∣ north ∣)
                             λ a → cong ∣_∣ ((merid a) ∙ (sym (merid north)))

  {- We show that looper is a composition of intLoop with two other maps, all three being isos -}
  sndcomp : ΩS¹ → Path (Susp Bool) north north
  sndcomp = cong S¹→SuspBool

  thrdcomp : Path (Susp Bool) north north → Path (S₊ 1) north north
  thrdcomp = cong SuspBool→S1

looper2 : Int → Path (S₊ 1) north north
looper2 a = thrdcomp (sndcomp (intLoop a))

looper≡looper2 : (x : Int) → looper x ≡ looper2 x
looper≡looper2 (pos zero) = refl
looper≡looper2 (pos (suc n)) =
       looper (pos n) ∙ loop*                                       ≡⟨ (λ i → looper≡looper2 (pos n) i ∙ congFunct SuspBool→S1 (merid false)  (sym (merid true)) (~ i)) ⟩
       looper2 (pos n) ∙ cong SuspBool→S1 (ϕ true false)           ≡⟨ sym (congFunct SuspBool→S1 (sndcomp (intLoop (pos n))) (ϕ true false)) ⟩
       cong SuspBool→S1 (sndcomp (intLoop (pos n)) ∙ ϕ true false) ≡⟨ cong thrdcomp (sym (congFunct S¹→SuspBool (intLoop (pos n)) loop)) ⟩
       looper2 (pos (suc n)) ∎
looper≡looper2 (negsuc zero) =
       sym loop*                                                    ≡⟨ symDistr (merid south) (sym (merid north)) ⟩
       merid north ∙ sym (merid south)                              ≡⟨ sym (congFunct SuspBool→S1 (merid true) (sym (merid false))) ⟩
       cong SuspBool→S1 (merid true ∙ sym (merid false))           ≡⟨ cong thrdcomp (sym (symDistr (merid false) (sym (merid true)))) ⟩
       looper2 (negsuc zero) ∎
looper≡looper2 (negsuc (suc n)) =
       looper (negsuc n) ∙ sym loop*                                                    ≡⟨ ((λ i → looper≡looper2 (negsuc n) i ∙ symDistr (merid south) (sym (merid north)) i)) ⟩
       looper2 (negsuc n) ∙ merid north ∙ sym (merid south)                             ≡⟨ cong (λ x → looper2 (negsuc n) ∙ x) (sym (congFunct SuspBool→S1 (merid true) (sym (merid false)))) ⟩
       looper2 (negsuc n) ∙ cong SuspBool→S1 (ϕ false true)                            ≡⟨ cong (λ x → looper2 (negsuc n) ∙ x) (cong thrdcomp (sym (symDistr (merid false) (sym (merid true))))) ⟩
       looper2 (negsuc n) ∙ cong SuspBool→S1 (sym (ϕ true false))                      ≡⟨ sym (congFunct SuspBool→S1 (sndcomp (intLoop (negsuc n))) (sym (ϕ true false))) ⟩
       thrdcomp (cong S¹→SuspBool (intLoop (negsuc n)) ∙ cong S¹→SuspBool (sym loop)) ≡⟨ cong thrdcomp (sym (congFunct S¹→SuspBool (intLoop (negsuc n)) (sym loop))) ⟩
       looper2 (negsuc (suc n)) ∎

private
  isolooper2 : Iso Int (Path (S₊ 1) north north)
  isolooper2 = compIso (invIso ΩS¹IsoInt) (compIso iso2 iso1)
    where
    iso1 : Iso (Path (Susp Bool) north north) (Path (S₊ 1) north north)
    iso1 = congIso SuspBoolIsoS1

    iso2 : Iso ΩS¹ (Path (Susp Bool) north north)
    iso2 = congIso S¹IsoSuspBool

  isolooper : Iso Int (Path (S₊ 1) north north)
  Iso.fun isolooper = looper
  Iso.inv isolooper = Iso.inv isolooper2
  Iso.rightInv isolooper a = (looper≡looper2 (Iso.inv isolooper2 a)) ∙ Iso.rightInv isolooper2 a
  Iso.leftInv isolooper a = cong (Iso.inv isolooper2) (looper≡looper2 a) ∙ Iso.leftInv isolooper2 a

  {- We want to show that this map is an equivalence. n ≥ 2 follows from Freudenthal, and  -}

  {-
  We want to show that the function (looper : Int → S₊ 1) defined by λ k → loopᵏ is an equivalece. We already know that the corresponding function (intLoop : Int → S¹ is) an equivalence,
  so the idea is to show that when intLoop is transported along a suitable path S₊ 1 ≡ S¹ we get looper. Instead of using S₊ 1 straight away, we begin by showing this for the equivalent Susp Bool.
  -}

  ----------------------------------- n = 1 -----------------------------------------------------

  {- We begin by stating some useful lemmas -}

  S³≡SuspSuspS¹ : S³ ≡ Susp (Susp S¹)
  S³≡SuspSuspS¹ = S³≡SuspS² ∙ λ i → Susp (S²≡SuspS¹ i)

  S3≡SuspSuspS¹ : S₊ 3 ≡ Susp (Susp S¹)
  S3≡SuspSuspS¹ = (λ i → Susp (Susp (Susp (ua Bool≃Susp⊥ (~ i))))) ∙ λ i → Susp (Susp (S¹≡SuspBool (~ i)))

  sphereConnectedSpecCase : isConnected 4 (Susp (Susp S¹))
  sphereConnectedSpecCase = transport (λ i → isConnected 4 (S3≡SuspSuspS¹ i)) (sphereConnected 3)

  {- We give the following map and show that its truncation is an equivalence -}

  d-map : typ (Ω ((Susp S¹) , north)) → S¹
  d-map p = subst HopfSuspS¹ p base

  d-mapId : (r : S¹) → d-map (ϕ base r) ≡ r
  d-mapId r = substComposite HopfSuspS¹ (merid r) (sym (merid base)) base ∙
              rotLemma r
    where
    rotLemma : (r : S¹) → rot r base ≡ r
    rotLemma base = refl
    rotLemma (loop i) = refl

  d-mapComp : fiber d-map base ≡ Path (Susp (Susp S¹)) north north
  d-mapComp = ΣPathTransport≡PathΣ {B = HopfSuspS¹} _ _ ∙ helper
    where
    helper : Path (Σ (Susp S¹) λ x → HopfSuspS¹ x) (north , base) (north , base) ≡ Path (Susp (Susp S¹)) north north
    helper = (λ i → (Path (S³≡TotalHopf (~ i))
                          (transp (λ j → S³≡TotalHopf (~ i ∨ ~ j)) (~ i) (north , base))
                          ((transp (λ j → S³≡TotalHopf (~ i ∨ ~ j)) (~ i) (north , base))))) ∙
             (λ i → Path (S³≡SuspSuspS¹ i) (transp (λ j → S³≡SuspSuspS¹ (i ∧ j)) (~ i) base) ((transp (λ j → S³≡SuspSuspS¹ (i ∧ j)) (~ i) base)))

  is1Connected-dmap : isConnectedFun 3 d-map
  is1Connected-dmap = toPropElim (λ s → isPropIsOfHLevel 0) (transport (λ j → isContr (∥ d-mapComp (~ j) ∥ 3))
                                      (transport (λ i →  isContr (PathΩ {A = Susp (Susp S¹)} {a = north} 3 i))
                                                 (refl , isOfHLevelSuc 1 (isOfHLevelSuc 0 sphereConnectedSpecCase) ∣ north ∣ ∣ north ∣ (λ _ → ∣ north ∣))))

  d-iso2 : Iso (hLevelTrunc 3 (typ (Ω (Susp S¹ , north)))) (hLevelTrunc 3 S¹)
  d-iso2 = connectedTruncIso _ d-map is1Connected-dmap

  {- We show that composing (λ a → ∣ ϕ base a ∣) and (λ x → ∣ d-map x ∣) gives us the identity function.  -}

  d-mapId2 : Iso.fun d-iso2 ∘ trMap (ϕ base) ≡ idfun (hLevelTrunc 3 S¹)
  d-mapId2 = funExt (trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) (λ a → cong ∣_∣ (d-mapId a)))

  {- This means that (λ a → ∣ ϕ base a ∣) is an equivalence -}

  Iso∣ϕ-base∣ : Iso (hLevelTrunc 3 S¹) (hLevelTrunc 3 (typ (Ω (Susp S¹ , north))))
  Iso∣ϕ-base∣ = composesToId→Iso d-iso2 (trMap (ϕ base)) d-mapId2

  ---------------------------------
  -- We cheat when n = 1 and use J to prove the following lemmma.  There is an obvious dependent path between ϕ base and ϕ north. Since the first one is an iso, so is the other.
  -- So far this hasn't been an issue.

  pointFunIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ} {C : (A : Type ℓ) (a1 : A) → Type ℓ'} (p : A ≡ B) (a : A) (b : B) →
              (transport p a ≡ b) →
              (f : (A : Type ℓ) →
              (a1 : A) (a2 : hLevelTrunc 3 A)  → C A a1) →
              isIso (f A a) →
              isIso (f B b)
  pointFunIso {ℓ = ℓ}{A = A} {B = B} {C = C} =
           J (λ B p → (a : A) (b : B) →
                        (transport p a ≡ b) →
                        (f : (A : Type ℓ) →
                        (a1 : A) (a2 : hLevelTrunc 3 A)  → C A a1) →
                        isIso (f A a) →
                        isIso (f B b))
             λ a b trefl f is → transport (λ i → isIso (f A ((sym (transportRefl a) ∙ trefl) i))) is

  {- By pointFunIso, this gives that λ a → ∣ ϕ north a ∣ is an iso -}

  isIso∣ϕ∣ : isIso {A = hLevelTrunc 3 (S₊ 1)} {B = hLevelTrunc 3 (typ (Ω (S₊ 2 , north)))} (trMap (ϕ north))
  isIso∣ϕ∣ = pointFunIso {A = S¹} (λ i → S¹≡S1 (~ i)) base north refl (λ A a1 → trMap (ϕ a1)) ((Iso.inv Iso∣ϕ-base∣) , ((Iso.rightInv Iso∣ϕ-base∣) , (Iso.leftInv Iso∣ϕ-base∣)))

  Iso∣ϕ∣ : Iso (hLevelTrunc 3 (S₊ 1)) (hLevelTrunc 3 (typ (Ω (S₊ 2 , north))))
  Iso.fun Iso∣ϕ∣ = trMap (ϕ north)
  Iso.inv Iso∣ϕ∣ = isIso∣ϕ∣ .fst
  Iso.rightInv Iso∣ϕ∣ = isIso∣ϕ∣ .snd .fst
  Iso.leftInv Iso∣ϕ∣ = isIso∣ϕ∣ .snd .snd

---------------------------------------------------- Finishing up ---------------------------------

-- We need ΩTrunc. It appears to compute better when restated for this particular case --

decode-fun2 : (n : HLevel) → (x : A) → hLevelTrunc n (x ≡ x) → Path (hLevelTrunc (suc n) A) ∣ x ∣ ∣ x ∣
decode-fun2 zero x = trElim (λ _ → isOfHLevelPath 0 (∣ x ∣ , isOfHLevelTrunc 1 ∣ x ∣) ∣ x ∣ ∣ x ∣) (λ p i → ∣ p i ∣)
decode-fun2 (suc n) x = trElim (λ _ → isOfHLevelPath' (suc n) (isOfHLevelTrunc (suc (suc n))) ∣ x ∣ ∣ x ∣) (cong ∣_∣)

funsAreSame : (n : HLevel) (x : A) (b : hLevelTrunc n (x ≡ x)) → (decode-fun2 n x b) ≡ (ΩTrunc.decode-fun ∣ x ∣ ∣ x ∣ b)
funsAreSame zero x = trElim (λ a → isOfHLevelPath 0 (refl , (isOfHLevelSuc 1 (isOfHLevelTrunc 1) ∣ x ∣ ∣ x ∣ refl)) _ _) λ a → refl
funsAreSame (suc n) x = trElim (λ a → isOfHLevelPath _ (isOfHLevelPath' (suc n) (isOfHLevelTrunc (suc (suc n))) ∣ x ∣ ∣ x ∣) _ _) λ a → refl

decodeIso : (n : HLevel) (x : A) → Iso (hLevelTrunc n (x ≡ x)) (Path (hLevelTrunc (suc n) A) ∣ x ∣ ∣ x ∣)
Iso.fun (decodeIso n x) = decode-fun2 n x
Iso.inv (decodeIso n x) = ΩTrunc.encode-fun ∣ x ∣ ∣ x ∣
Iso.rightInv (decodeIso n x) b = funsAreSame n x (ΩTrunc.encode-fun ∣ x ∣ ∣ x ∣ b) ∙ ΩTrunc.P-rinv ∣ x ∣ ∣ x ∣ b
Iso.leftInv (decodeIso n x) b = cong (ΩTrunc.encode-fun ∣ x ∣ ∣ x ∣) (funsAreSame n x b) ∙ ΩTrunc.P-linv ∣ x ∣ ∣ x ∣ b

Iso-Kn-ΩKn+1 : (n : HLevel) → Iso (coHomK n) (typ (Ω (coHomK-ptd (suc n))))
Iso-Kn-ΩKn+1 zero = compIso isolooper (congIso (truncIdempotentIso _ isOfHLevelS1))
Iso-Kn-ΩKn+1 (suc zero) = compIso Iso∣ϕ∣ (decodeIso _ north)
Iso-Kn-ΩKn+1 (suc (suc n)) = compIso (connectedTruncIso2 (4 + n) _ (ϕ north) (n , helper)
                                                                             (isConnectedσ (suc n) (sphereConnected _)))
                                     (decodeIso _ north)
  where
  helper : n + (4 + n) ≡ 2 + (n + (2 + n))
  helper = +-suc n (3 + n) ∙ (λ i → suc (+-suc n (2 + n) i))

mapId2 : (n : ℕ) →  Kn→ΩKn+1 n ≡ Iso.fun (Iso-Kn-ΩKn+1 n)
mapId2 zero = refl
mapId2 (suc zero) = funExt (trElim (λ x → isOfHLevelPath 3 (isOfHLevelTrunc 4 ∣ north ∣ ∣ north ∣) _ _) λ a → refl)
mapId2 (suc (suc n)) = funExt (trElim (λ x → isOfHLevelPath (4 + n) (isOfHLevelTrunc (5 + n) ∣ north ∣ ∣ north ∣) _ _) λ a → refl)

-- Experiments with abstract definitions

Iso2-Kn-ΩKn+1 : (n : ℕ) → Iso (coHomK n) (typ (Ω (coHomK-ptd (suc n))))
Iso.fun (Iso2-Kn-ΩKn+1 n) = Kn→ΩKn+1 n
Iso.inv (Iso2-Kn-ΩKn+1 n) = Iso.inv (Iso-Kn-ΩKn+1 n)
Iso.rightInv (Iso2-Kn-ΩKn+1 n) a = rinv
  where
  abstract
    rinv : Kn→ΩKn+1 n (Iso.inv (Iso-Kn-ΩKn+1 n) a) ≡ a
    rinv = funExt⁻ (mapId2 n) _ ∙ Iso.rightInv (Iso-Kn-ΩKn+1 n) a
Iso.leftInv (Iso2-Kn-ΩKn+1 n) a = linv
  where
  abstract
    linv : Iso.inv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n a) ≡ a
    linv = cong (Iso.inv (Iso-Kn-ΩKn+1 n)) (funExt⁻ (mapId2 n) a) ∙ Iso.leftInv (Iso-Kn-ΩKn+1 n) a

--- even more abstract

abstract
  absInv' : (n : ℕ) → typ (Ω (coHomK-ptd (2 + n))) → coHomK (1 + n)
  absInv' n = Iso.inv (Iso-Kn-ΩKn+1 (1 + n))

  absSect' : (n : ℕ) (a : typ (Ω (coHomK-ptd (2 + n)))) → Kn→ΩKn+1 (1 + n) (absInv' n a) ≡ a
  absSect' n a = funExt⁻ (mapId2 (1 + n)) _ ∙ Iso.rightInv (Iso-Kn-ΩKn+1 (1 + n)) a

  absRetr' : (n : ℕ) (a : coHomK (1 + n)) → absInv' n (Kn→ΩKn+1 (1 + n) a) ≡ a
  absRetr' n a = cong (Iso.inv (Iso-Kn-ΩKn+1 (1 + n))) (funExt⁻ (mapId2 (1 + n)) a) ∙ Iso.leftInv (Iso-Kn-ΩKn+1 (1 + n)) a

absInv : (n : ℕ) → typ (Ω (coHomK-ptd (1 + n))) → coHomK n
absInv zero = Iso.inv (Iso-Kn-ΩKn+1 zero)
absInv (suc n) = absInv' n

absSect : (n : ℕ) → section (Kn→ΩKn+1 n) (absInv n)
absSect zero a = funExt⁻ (mapId2 zero) (Iso.inv isolooper2 (Iso.inv (congIso (truncIdempotentIso _ isOfHLevelS1)) a)) ∙ Iso.rightInv (Iso-Kn-ΩKn+1 zero) a
absSect (suc n) = absSect' n

absRetr : (n : ℕ) → retract (Kn→ΩKn+1 n) (absInv n)
absRetr zero a = cong (Iso.inv (Iso-Kn-ΩKn+1 zero)) (funExt⁻ (mapId2 zero) a) ∙ Iso.leftInv (Iso-Kn-ΩKn+1 zero) a
absRetr (suc n) = absRetr' n

Iso3-Kn-ΩKn+1 : (n : ℕ) → Iso (coHomK n) (typ (Ω (coHomK-ptd (suc n))))
Iso.fun (Iso3-Kn-ΩKn+1 n) = Kn→ΩKn+1 n
Iso.inv (Iso3-Kn-ΩKn+1 n) = absInv n
Iso.rightInv (Iso3-Kn-ΩKn+1 n) = absSect n
Iso.leftInv (Iso3-Kn-ΩKn+1 n) = absRetr n

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


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

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Bool
open import lib.types.Int

module lib.types.List where

infixr 60 _::_

data List {i} (A : Type i) : Type i where
  nil : List A
  _::_ : A → List A → List A

module _ {i} {A : Type i} where
  infixr 80 _++_
  _++_ : List A → List A → List A
  nil ++ l = l
  (x :: l₁) ++ l₂ = x :: (l₁ ++ l₂)

  snoc : List A → A → List A
  snoc l a = l ++ (a :: nil)

  ++-unit-r : ∀ l → l ++ nil == l
  ++-unit-r nil      = idp
  ++-unit-r (a :: l) = ap (a ::_) $ ++-unit-r l

  ++-assoc : ∀ l₁ l₂ l₃ → (l₁ ++ l₂) ++ l₃ == l₁ ++ (l₂ ++ l₃)
  ++-assoc nil l₂ l₃ = idp
  ++-assoc (x :: l₁) l₂ l₃ = ap (x ::_) (++-assoc l₁ l₂ l₃)

  -- properties
  module _ {j} (P : A → Type j) where
    data Any : List A → Type (lmax i j) where
      here : ∀ {a} {l} → P a → Any (a :: l)
      there : ∀ {a} {l} → Any l → Any (a :: l)

    data All : List A → Type (lmax i j) where
      nil : All nil
      _::_ : ∀ {a} {l} → P a → All l → All (a :: l)

    Any-dec : (∀ a → Dec (P a)) → (∀ l → Dec (Any l))
    Any-dec _   nil       = inr λ{()}
    Any-dec dec (a :: l) with dec a
    ... | inl p = inl $ here p
    ... | inr ¬p with Any-dec dec l
    ...   | inl ∃p = inl $ there ∃p
    ...   | inr ¬∃p = inr λ{(here p) → ¬p p; (there ∃p) → ¬∃p ∃p}

    Any-++-l : ∀ l₁ l₂ → Any l₁ → Any (l₁ ++ l₂)
    Any-++-l _ _ (here p)   = here p
    Any-++-l _ _ (there ∃p) = there (Any-++-l _ _ ∃p)

    Any-++-r : ∀ l₁ l₂ → Any l₂ → Any (l₁ ++ l₂)
    Any-++-r nil      _ ∃p = ∃p
    Any-++-r (a :: l) _ ∃p = there (Any-++-r l _ ∃p)

    Any-++ : ∀ l₁ l₂ → Any (l₁ ++ l₂) → Any l₁ ⊔ Any l₂
    Any-++ nil       l₂ ∃p         = inr ∃p
    Any-++ (a :: l₁) l₂ (here p)   = inl (here p)
    Any-++ (a :: l₁) l₂ (there ∃p) with Any-++ l₁ l₂ ∃p
    ... | inl ∃p₁ = inl (there ∃p₁)
    ... | inr ∃p₂ = inr ∃p₂

  infix 80 _∈_
  _∈_ : A → List A → Type i
  a ∈ l = Any (_== a) l

  ∈-dec : has-dec-eq A → ∀ a l → Dec (a ∈ l)
  ∈-dec dec a l = Any-dec (_== a) (λ a' → dec a' a) l

  ∈-++-l : ∀ a l₁ l₂ → a ∈ l₁ → a ∈ (l₁ ++ l₂)
  ∈-++-l a = Any-++-l (_== a)

  ∈-++-r : ∀ a l₁ l₂ → a ∈ l₂ → a ∈ (l₁ ++ l₂)
  ∈-++-r a = Any-++-r (_== a)

  ∈-++ : ∀ a l₁ l₂ → a ∈ (l₁ ++ l₂) → (a ∈ l₁) ⊔ (a ∈ l₂)
  ∈-++ a = Any-++ (_== a)

  -- [foldr] in Haskell
  foldr : ∀ {j} {B : Type j} → (A → B → B) → B → List A → B
  foldr f b nil = b
  foldr f b (a :: l) = f a (foldr f b l)

  -- [length] in Haskell
  length : List A → ℕ
  length = foldr (λ _ n → S n) 0

  -- [filter] in Haskell
  -- Note that [Bool] is currently defined as a coproduct.
  filter : ∀ {j k} {Keep : A → Type j} {Drop : A → Type k}
    → ((a : A) → Keep a ⊔ Drop a) → List A → List A
  filter p nil = nil
  filter p (a :: l) with p a
  ... | inl _ = a :: filter p l
  ... | inr _ = filter p l

  -- [reverse] in Haskell
  reverse : List A → List A
  reverse nil = nil
  reverse (x :: l) = snoc (reverse l) x

  reverse-snoc : ∀ a l → reverse (snoc l a) == a :: reverse l
  reverse-snoc a nil = idp
  reverse-snoc a (b :: l) = ap (λ l → snoc l b) (reverse-snoc a l)

  reverse-reverse : ∀ l → reverse (reverse l) == l
  reverse-reverse nil = idp
  reverse-reverse (a :: l) = reverse-snoc a (reverse l) ∙ ap  (a ::_) (reverse-reverse l)

  -- Reasoning about identifications
  List= : ∀ (l₁ l₂ : List A) → Type i
  List= nil       nil       = Lift ⊤
  List= nil       (y :: l₂) = Lift ⊥
  List= (x :: l₁) nil       = Lift ⊥
  List= (x :: l₁) (y :: l₂) = (x == y) × (l₁ == l₂)

  List=-in : ∀ {l₁ l₂ : List A} → l₁ == l₂ → List= l₁ l₂
  List=-in {l₁ = nil} idp = lift unit
  List=-in {l₁ = x :: l} idp = idp , idp

  List=-out : ∀ {l₁ l₂ : List A} → List= l₁ l₂ → l₁ == l₂
  List=-out {l₁ = nil} {l₂ = nil} _ = idp
  List=-out {l₁ = nil} {l₂ = y :: l₂} (lift ())
  List=-out {l₁ = x :: l₁} {l₂ = nil} (lift ())
  List=-out {l₁ = x :: l₁} {l₂ = y :: l₂} (x=y , l₁=l₂) = ap2 _::_ x=y l₁=l₂

module _ {i j} {A : Type i} {B : Type j} (f : A → B) where

  -- [map] in Haskell
  map : List A → List B
  map nil = nil
  map (a :: l) = f a :: map l

  map-++ : ∀ l₁ l₂ → map (l₁ ++ l₂) == map l₁ ++ map l₂
  map-++ nil l₂ = idp
  map-++ (x :: l₁) l₂ = ap (f x ::_) (map-++ l₁ l₂)
{-
  reverse-map : ∀ l → reverse (map l) == map (reverse l)
  reverse-map nil = idp
  reverse-map (x :: l) = {! ! (map-++ (reverse l) (x :: nil)) !}
-}
-- These functions use different [A], [B] or [f].
module _ {i} {A : Type i} where
  -- [concat] in Haskell
  concat : List (List A) → List A
  concat l = foldr _++_ nil l

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- Andreas, 2016-01-18, Issue1778, reported by mechvel
-- record pattern elimination must preserve hiding information

-- {-# OPTIONS --show-implicit #-}

open import Common.Prelude using (⊤)
open import Common.Equality
open import Common.Product
-- assuming _×_ is a record type (not data type)

module _ (A : Set) (let T = ⊤ → {p : A × A} → A) (f : T) where

swap : T → T
swap f _ {x , y} = f _ {y , x}
-- becomes by record pattern elimination
-- WAS: swap f _ xy   = f _ {proj₂ xy , proj₁ xy}
-- NOW: swap f _ {xy} = f _ {proj₂ xy , proj₁ xy}

test : f ≡ swap (swap f)
test with Set -- trigers internal checking of type
test | _ = refl

-- WAS:
-- Expected a hidden argument, but found a visible argument
-- when checking that the type
-- (w : Set₁) → f ≡ (λ _ xy → f (record {}))
-- of the generated with function is well-formed

-- NOW:
-- should succeed


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

-- Given a predicate on the objects of a Category C, build another category
-- with just those that satisfy a pr

module Categories.Category.Construction.ObjectRestriction where

open import Level
open import Data.Product using (Σ; proj₁)
open import Relation.Unary using (Pred)
open import Function using (_on_) renaming (id to id→)

open import Categories.Category.Core

private
  variable
    o ℓ e ℓ′ : Level

ObjectRestriction : (C : Category o ℓ e) → Pred (Category.Obj C) ℓ′ → Category (o ⊔ ℓ′) ℓ e
ObjectRestriction C R = record
  { Obj = Σ Obj R
  ; _⇒_ = _⇒_ on proj₁
  ; _≈_ = _≈_
  ; id = id
  ; _∘_ = _∘_
  ; assoc = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv = equiv
  ; ∘-resp-≈ = ∘-resp-≈
  }
  where open Category C

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 Cats.Category.Setoids.Facts.Terminal where

open import Data.Unit using (⊤)
open import Level

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

module Build {l} {l≈} where

  open Category (Setoids l l≈)

  One : Obj
  One = record
      { Carrier = Lift l ⊤
      ; _≈_ = λ _ _ → Lift l≈ ⊤
      }

  isTerminal : IsTerminal One
  isTerminal X = ∃!-intro _ _ _

open Build

instance
  hasTerminal : ∀ l l≈ → HasTerminal (Setoids l l≈)
  hasTerminal l l≈ = record
      { One = One
      ; isTerminal = isTerminal
      }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats