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
-}
{-# OPTIONS --allow-unsolved-metas #-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types.EpochIndep
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open        WithAbsVote

-- Here we have the abstraction functions that connect
-- the datatypes defined in LibraBFT.Impl.Consensus.Types
-- to the abstract records from LibraBFT.Abstract.Records
-- for a given EpochConfig.
--
module LibraBFT.Concrete.Records (𝓔 : EpochConfig) where
 open import LibraBFT.Impl.Consensus.Types.EpochDep 𝓔
 open import LibraBFT.Abstract.Abstract UID _≟UID_ NodeId 𝓔 ConcreteVoteEvidence as Abs hiding (bId; qcVotes; Block)
 open        EpochConfig 𝓔
 --------------------------------
 -- Abstracting Blocks and QCs --
 --------------------------------

 α-Block : Block → Abs.Block
 α-Block b with ₋bdBlockType (₋bBlockData b)
 ...| NilBlock = record
      { bId     = ₋bId b
      ; bPrevQC = just (b ^∙ (bBlockData ∙ bdQuorumCert ∙ qcVoteData ∙  vdParent ∙ biId))
      ; bRound  = b ^∙ bBlockData ∙ bdRound
      }
 ...| Genesis = record
      { bId     = b ^∙ bId
      ; bPrevQC = nothing
      ; bRound  = b ^∙ bBlockData ∙ bdRound
      }
 ...| Proposal cmd α = record
      { bId     = b ^∙ bId
      ; bPrevQC = just (b ^∙ bBlockData ∙ bdQuorumCert ∙ qcVoteData ∙ vdParent ∙ biId)
      ; bRound  = b ^∙ bBlockData ∙ bdRound
      }

 α-VoteData-Block : VoteData → Abs.Block
 α-VoteData-Block vd = record
      { bId     = vd ^∙ vdProposed ∙ biId
      ; bPrevQC = just (vd ^∙ vdParent ∙ biId)
      ; bRound  = vd ^∙ vdProposed ∙ biRound
      }

 α-Vote : (qc : QuorumCert)(valid : MetaIsValidQC qc) → ∀ {as} → as ∈ qcVotes qc → Abs.Vote
 α-Vote qc v {as} as∈QC = α-ValidVote (rebuildVote qc as)
                                      (₋ivvMember (All-lookup (₋ivqcMetaVotesValid v) as∈QC))

 -- Abstraction of votes produce votes that carry evidence
 -- they have been cast.
 α-Vote-evidence : (qc : QuorumCert)(valid : MetaIsValidQC qc)
                 → ∀{vs} (prf : vs ∈ qcVotes qc)
                 → ConcreteVoteEvidence (α-Vote qc valid prf)
 α-Vote-evidence qc valid {as} v∈qc
   = record { ₋cveVote        = rebuildVote qc as
            ; ₋cveIsValidVote = All-lookup (₋ivqcMetaVotesValid valid) v∈qc
            ; ₋cveIsAbs       = refl
            }

 α-QC : Σ QuorumCert MetaIsValidQC → Abs.QC
 α-QC (qc , valid) = record
   { qCertBlockId = qc ^∙ qcVoteData ∙ vdProposed ∙ biId
   ; qRound       = qc ^∙ qcVoteData ∙ vdProposed ∙ biRound
   ; qVotes       = All-reduce (α-Vote qc valid) All-self
   ; qVotes-C1    = {! MetaIsValidQC.₋ivqcMetaIsQuorum valid!}
   ; qVotes-C2    = All-reduce⁺ (α-Vote qc valid) (λ _ → refl) All-self
   ; qVotes-C3    = All-reduce⁺ (α-Vote qc valid) (λ _ → refl) All-self
   ; qVotes-C4    = All-reduce⁺ (α-Vote qc valid) (α-Vote-evidence qc valid) All-self
   }

 -- What does it mean for an (abstract) Block or QC to be represented in a NetworkMsg?
 data _α-∈NM_ : Abs.Record → NetworkMsg → Set where
   qc∈NM : ∀ {cqc q nm}
         → (valid : MetaIsValidQC cqc)
         → cqc QC∈NM nm
         → q ≡ α-QC (cqc , valid)
         → Abs.Q q α-∈NM nm
   b∈NM  : ∀ {cb pm nm}
         → nm ≡ P pm
         → pm ^∙ pmProposal ≡ cb
         → Abs.B (α-Block cb) α-∈NM nm

 -- Our system model contains a message pool, which is a list of NodeId-NetworkMsg pairs.  The
 -- following relation expresses that an abstract record r is represented in a given message pool
 -- sm.
 data _α-Sent_ (r : Abs.Record) (sm : List (NodeId × NetworkMsg)) : Set where
   ws : ∀ {p nm} → getEpoch nm ≡ epoch → (p , nm) ∈ sm → r α-∈NM nm → r α-Sent sm

ext: agda

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module Selective.Examples.TestAO where

open import Selective.ActorMonad
open import Prelude
open import Selective.Libraries.Call2
open import Selective.Libraries.ActiveObjects

open import Debug
open import Data.Nat.Show using (show)

ℕ-ReplyMessage : MessageType
ℕ-ReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ

ℕ-Reply : InboxShape
ℕ-Reply = [ ℕ-ReplyMessage ]ˡ

ℕ×ℕ→ℕ-Message : MessageType
ℕ×ℕ→ℕ-Message = ValueType UniqueTag ∷ ReferenceType ℕ-Reply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ

Calculate : InboxShape
Calculate = [ ℕ×ℕ→ℕ-Message ]ˡ

CalculateProtocol : ChannelInitiation
CalculateProtocol = record
                       { request = Calculate
                       ; response = record {
                         channel-shape = ℕ-Reply
                         ; all-tagged = (HasTag _) ∷ []
                         }
                       ; request-tagged = [ HasTag+Ref _ ]ᵃ
                       }

ℕ×ℕ→ℕ-ci : ChannelInitiation
ℕ×ℕ→ℕ-ci = record {
  request = Calculate
  ; response = record { channel-shape = ℕ-Reply ; all-tagged = (HasTag _) ∷ [] }
  ; request-tagged = (HasTag+Ref _) ∷ [] }

add-method-header = ResponseMethod ℕ×ℕ→ℕ-ci
multiply-method-header = ResponseMethod ℕ×ℕ→ℕ-ci

calculator-methods : List ActiveMethod
calculator-methods = add-method-header ∷ multiply-method-header ∷ []

calculator-inbox = methods-shape calculator-methods

calculator-state-vars : ⊤₁ → TypingContext
calculator-state-vars _ = []

add : (active-method calculator-inbox ⊤₁ calculator-state-vars add-method-header)
add _ (_ sent Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z  [ lift (n + m)]ᵃ })
add _ (_ sent Msg (S ()) _) _

multiply : (active-method calculator-inbox ⊤₁ (λ _ → []) multiply-method-header)
multiply _ (_ sent Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n * m)]ᵃ })
multiply _ (_ sent Msg (S ()) _) _

calculator : ActiveObject
calculator = record {
  state-type = ⊤₁
  ; vars = calculator-state-vars
  ; methods = calculator-methods
  ; extra-messages = []
  ; handlers = add ∷ multiply ∷ []
  }

calculator-actor = run-active-object calculator _

TestBox : InboxShape
TestBox = ℕ-Reply

-- import Selective.Examples.CalculatorProtocol as CP
-- calculator-test-actor = CP.calculator-test-actor calculator-actor

calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift (lsuc lzero) ℕ) [] (λ _ → [])
calculator-test-actor = do
  spawn∞ calculator-actor
  Msg Z (_ ∷ n ∷ []) ← call CalculateProtocol (record {
    var = Z
    ; chosen-field = Z
    ; fields = lift 32 ∷ [ lift 10 ]ᵃ
    ; session = record {
      can-request = [ Z ]ᵐ -- Pick add method
      ; response-session = record {
        can-receive = [ Z ]ᵐ
        ; tag = 0
        }
      }
    })
    where
      Msg (S ()) _
  Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculateProtocol (record {
    var = Z
    ; chosen-field = Z
    ; fields = lift n ∷ [ lift 10 ]ᵃ
    ; session = record {
      can-request = [ S Z ]ᵐ -- Pick multiply method
      ; response-session = record {
        can-receive = [ Z ]ᵐ
        ; tag = 1
        }
      }
    }))
    where
      Msg (S ()) _
  debug (show m) (strengthen [])
  return m

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
module Everything where
open import Pi.Everything       -- Formalization for Π
open import RevMachine          -- Formalization of reversible machine and partial reversible machine
open import RevNoRepeat         -- Non-repeating theorem for reversible machine
open import PartialRevNoRepeat  -- Non-repeating theorem for partial reversible machine
open import TimeSpace           -- Time space trade-off
open import Pi-.Everything      -- Formalization for Π⁻
open import PiFrac.Everything   -- Formalization for Π/
open import PiQ.Everything      -- Formalization for Π^ℚ


text:
module RecordUpdateSyntax where

open import Common.Prelude
open import Common.Equality

data Param : Nat → Set where
  param : ∀ n → Param (suc n)

record R : Set where
  field
    {i} : Nat
    p : Param i
    s : Nat

old : R
old = record { p = param 0; s = 1 }

-- Simple update, it should be able to infer the type and the implicit.
new : _
new = record old { p = param 1 }

new′ : R
new′ = record { i = 2; p = param 1; s = 1 }

-- Here's a needlessly complex update.
upd-p-s : Nat → _ → _ → R
upd-p-s zero s r = record r { p = param zero; s = s }
upd-p-s (suc n) s r = record (upd-p-s n 0 r) { p = param n; s = s }

eq₁ : new ≡ new′
eq₁ = refl

eq₂ : upd-p-s zero 1 (record new { s = 0 }) ≡ old
eq₂ = refl

-- Check that instance arguments are handled properly
postulate
  T : Nat → Set
  instance
    t0 : T 0
    t1 : T 1

record Instance : Set where
  field
    n : Nat
    {{t}} : T n

r0 : Instance
r0 = record { n = 0 }

r1 : Instance
r1 = record r0 { n = 1 }

check : Instance.t r1 ≡ t1
check = refl

-- Andreas, 2020-03-27, issue #3684
-- warn only if there are invalid or duplicate fields

_ = record old { invalidField = 1 }
_ = record old { s = 1; s = 0 }
_ = record old { foo = 1; bar = 0; s = 1; s = 0 }

-- The record type R does not have the field invalidField but it would
-- have the fields i, p, s
-- when checking that the expression record old { invalidField = 1 }
-- has type R

-- Duplicate field s in record
-- when checking that the expression record old { s = 1 ; s = 0 } has
-- type R

-- /Users/abel/agda-erasure/test/Succeed/RecordUpdateSyntax.agda:59,5-50
-- The record type R does not have the fields foo, bar but it would
-- have the fields i, p
-- when checking that the expression
-- record old { foo = 1 ; bar = 0 ; s = 1 ; s = 0 } has type R

-- Duplicate field s in record
-- when checking that the expression
-- record old { foo = 1 ; bar = 0 ; s = 1 ; s = 0 } has type R

max_stars_repo_name: alexarice/agda

max_issues_repo_name: alexarice/agda

max_forks_repo_name: alexarice/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Empty type
------------------------------------------------------------------------

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

module Data.Empty where

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

-- Note that by default the empty type is not universe polymorphic as it
-- often results in unsolved metas. See `Data.Empty.Polymorphic` for a
-- universe polymorphic variant.

data ⊥ : Set where

------------------------------------------------------------------------
-- Functions

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()


text:
module StateSized.GUI.SpaceShipSimpleVar where

open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent

open import Data.Bool.Base
open import Data.List.Base
open import Data.Integer

open import Data.Product hiding (map)
open import SizedIO.Object
open import SizedIO.IOObject

open import NativeIO

open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.VariableList

open import StateSizedIO.GUI.WxGraphicsLib

open import StateSized.GUI.BitMaps

VarType : Set
VarType = ℤ

varInit : VarType
varInit = (+ 150)

onPaint  : ∀{i} → VarType   → DC → Rect → IO GuiLev1Interface i VarType
onPaint  z dc rect = exec (drawBitmap dc ship (z , (+ 150)) true) λ _ →
                     return z

moveSpaceShip : ∀{i} → Frame → VarType  → IO GuiLev1Interface i VarType
moveSpaceShip fra z   = return (z + + 20)

callRepaint : ∀{i} → Frame → VarType  → IO GuiLev1Interface i VarType
callRepaint fra z   = exec (repaint fra) λ _  →
                       return z

program : ∀{i} → IOˢ GuiLev2Interface i (λ _ → Unit) []
program =  execˢ (level1C makeFrame)           λ fra →
           execˢ (level1C (makeButton fra))    λ bt →
           execˢ (level1C (addButton fra bt))  λ _ →
           execˢ (createVar varInit)           λ _ →
           execˢ (setButtonHandler bt (moveSpaceShip fra
                                     ∷ [ callRepaint fra ])) λ _ →
           execˢ (setOnPaint fra [ onPaint  ])
           returnˢ

main : NativeIO Unit
main = start (translateLev2 program)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 24-sequences where

import 23-id-pushout
open 23-id-pushout public

{- We introduce two types of sequences: one with the arrows going up and one
   with the arrows going down. -}

Sequence :
  ( l : Level) → UU (lsuc l)
Sequence l = Σ (ℕ → UU l) (λ A → (n : ℕ) → A n → A (succ-ℕ n))

type-seq :
  { l : Level} (A : Sequence l) → (n : ℕ) → UU l
type-seq A = pr1 A

map-seq :
  { l : Level} (A : Sequence l) →
  ( n : ℕ) → (type-seq A n) → (type-seq A (succ-ℕ n))
map-seq A = pr2 A

Sequence' :
  ( l : Level) → UU (lsuc l)
Sequence' l = Σ (ℕ → UU l) (λ A → (n : ℕ) → A (succ-ℕ n) → A n)

type-seq' :
  { l : Level} (A : Sequence' l) → (n : ℕ) → UU l
type-seq' A = pr1 A

map-seq' :
  { l : Level} (A : Sequence' l) →
  (n : ℕ) → (type-seq' A (succ-ℕ n)) → (type-seq' A n)
map-seq' A = pr2 A

{- We characterize the identity type of Sequence l. -}

naturality-hom-Seq :
  { l1 l2 : Level} (A : Sequence l1) (B : Sequence l2)
  ( h : (n : ℕ) → type-seq A n → type-seq B n) (n : ℕ) → UU (l1 ⊔ l2)
naturality-hom-Seq A B h n =
  ((map-seq B n) ∘ (h n)) ~ ((h (succ-ℕ n)) ∘ (map-seq A n))

equiv-Seq :
  { l1 l2 : Level} (A : Sequence l1) (B : Sequence l2) → UU (l1 ⊔ l2)
equiv-Seq A B =
  Σ ( (n : ℕ) → (type-seq A n) ≃ (type-seq B n))
    ( λ e → (n : ℕ) →
      naturality-hom-Seq A B (λ n → map-equiv (e n)) n)

reflexive-equiv-Seq :
  { l1 : Level} (A : Sequence l1) → equiv-Seq A A
reflexive-equiv-Seq A =
  pair
    ( λ n → equiv-id (type-seq A n))
    ( λ n → htpy-refl)

equiv-eq-Seq :
  { l1 : Level} (A B : Sequence l1) → Id A B → equiv-Seq A B
equiv-eq-Seq A .A refl = reflexive-equiv-Seq A

is-contr-total-equiv-Seq :
  { l1 : Level} (A : Sequence l1) →
  is-contr (Σ (Sequence l1) (equiv-Seq A))
is-contr-total-equiv-Seq A =
  is-contr-total-Eq-structure
    ( λ B g (e : (n : ℕ) → (type-seq A n) ≃ B n) →
      (n : ℕ) → naturality-hom-Seq A (pair B g) (λ n → map-equiv (e n)) n)
    ( is-contr-total-Eq-Π
      ( λ n X → type-seq A n ≃ X)
      ( λ n → is-contr-total-equiv (type-seq A n))
      ( type-seq A))
    ( pair (type-seq A) (λ n → equiv-id (type-seq A n)))
    ( is-contr-total-Eq-Π
      ( λ n h → h ~ (map-seq A n))
      ( λ n → is-contr-total-htpy' (map-seq A n))
      ( map-seq A))

is-equiv-equiv-eq-Seq :
  { l1 : Level} (A B : Sequence l1) → is-equiv (equiv-eq-Seq A B)
is-equiv-equiv-eq-Seq A =
  fundamental-theorem-id A
    ( reflexive-equiv-Seq A)
    ( is-contr-total-equiv-Seq A)
    ( equiv-eq-Seq A)

eq-equiv-Seq :
  { l1 : Level} {A B : Sequence l1} → equiv-Seq A B → Id A B
eq-equiv-Seq {A = A} {B} =
  inv-is-equiv (is-equiv-equiv-eq-Seq A B)

{- We characterize the identity type of Sequence' l. -}

equiv-Seq' :
  { l1 l2 : Level} (A : Sequence' l1) (B : Sequence' l2) → UU (l1 ⊔ l2)
equiv-Seq' A B =
  Σ ( (n : ℕ) → (type-seq' A n) ≃ (type-seq' B n)) (λ e →
    ( n : ℕ) →
      ( (map-seq' B n) ∘ (map-equiv (e (succ-ℕ n)))) ~
      ( (map-equiv (e n)) ∘ (map-seq' A n)))

reflexive-equiv-Seq' :
  { l1 : Level} (A : Sequence' l1) → equiv-Seq' A A
reflexive-equiv-Seq' A =
  pair
    ( λ n → equiv-id (type-seq' A n))
    ( λ n → htpy-refl)

equiv-eq-Seq' :
  { l1 : Level} (A B : Sequence' l1) → Id A B → equiv-Seq' A B
equiv-eq-Seq' A .A refl = reflexive-equiv-Seq' A

is-contr-total-equiv-Seq' :
  { l1 : Level} (A : Sequence' l1) →
  is-contr (Σ (Sequence' l1) (equiv-Seq' A))
is-contr-total-equiv-Seq' A =
  is-contr-total-Eq-structure
    ( λ B g (e : (n : ℕ) → (type-seq' A n) ≃ (B n)) → (n : ℕ) →
      ( (g n) ∘ (map-equiv (e (succ-ℕ n)))) ~
      ( (map-equiv (e n)) ∘ (map-seq' A n)))
    ( is-contr-total-Eq-Π
      ( λ n B → (type-seq' A n) ≃ B)
      ( λ n → is-contr-total-equiv (type-seq' A n))
      ( type-seq' A))
    ( pair (type-seq' A) (λ n → equiv-id (type-seq' A n)))
    ( is-contr-total-Eq-Π
      ( λ n g → g ~ (map-seq' A n))
      ( λ n → is-contr-total-htpy' (map-seq' A n))
      ( map-seq' A))

is-equiv-equiv-eq-Seq' :
  { l1 : Level} (A B : Sequence' l1) → is-equiv (equiv-eq-Seq' A B)
is-equiv-equiv-eq-Seq' A =
  fundamental-theorem-id A
    ( reflexive-equiv-Seq' A)
    ( is-contr-total-equiv-Seq' A)
    ( equiv-eq-Seq' A)

eq-equiv-Seq' :
  { l1 : Level} (A B : Sequence' l1) → equiv-Seq' A B → Id A B
eq-equiv-Seq' A B = inv-is-equiv (is-equiv-equiv-eq-Seq' A B)

{- We introduce cones on a type sequence. -}

cone-sequence :
  { l1 l2 : Level} (A : Sequence' l1) (X : UU l2) → UU (l1 ⊔ l2)
cone-sequence A X =
  Σ ( (n : ℕ) → X → type-seq' A n)
    ( λ p → (n : ℕ) → ((map-seq' A n) ∘ (p (succ-ℕ n))) ~ (p n))

map-cone-sequence :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( n : ℕ) → X → type-seq' A n
map-cone-sequence A c = pr1 c

triangle-cone-sequence :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( n : ℕ) →
  ( (map-seq' A n) ∘ (map-cone-sequence A c (succ-ℕ n))) ~
  ( map-cone-sequence A c n)
triangle-cone-sequence A c = pr2 c

{- We characterize the identity type of cone-sequence. -}

naturality-htpy-cone-sequence :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c c' : cone-sequence A X) →
  ( H : (n : ℕ) → (map-cone-sequence A c n) ~ (map-cone-sequence A c' n)) →
  ( n : ℕ) → UU (l1 ⊔ l2)
naturality-htpy-cone-sequence A c c' H n =
  ( ((map-seq' A n) ·l (H (succ-ℕ n))) ∙h (triangle-cone-sequence A c' n)) ~
  ( (triangle-cone-sequence A c n) ∙h (H n))

htpy-cone-sequence :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} →
  ( c c' : cone-sequence A X) → UU (l1 ⊔ l2)
htpy-cone-sequence A c c' =
  Σ ( (n : ℕ) → (map-cone-sequence A c n) ~ (map-cone-sequence A c' n)) (λ H →
    (n : ℕ) → naturality-htpy-cone-sequence A c c' H n)

reflexive-htpy-cone-sequence :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  htpy-cone-sequence A c c
reflexive-htpy-cone-sequence A c =
  pair
    ( λ n → htpy-refl)
    ( λ n → htpy-inv htpy-right-unit)

htpy-cone-sequence-eq :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c c' : cone-sequence A X) →
  Id c c' → htpy-cone-sequence A c c'
htpy-cone-sequence-eq A c .c refl = reflexive-htpy-cone-sequence A c

is-contr-total-htpy-cone-sequence :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  is-contr (Σ (cone-sequence A X) (htpy-cone-sequence A c))
is-contr-total-htpy-cone-sequence A c =
  is-contr-total-Eq-structure
    ( λ p t H → (n : ℕ) → naturality-htpy-cone-sequence A c (pair p t) H n)
    ( is-contr-total-Eq-Π
      ( λ n pn → (map-cone-sequence A c n) ~ pn)
      ( λ n → is-contr-total-htpy (map-cone-sequence A c n))
      ( map-cone-sequence A c))
    ( pair (map-cone-sequence A c) (λ n → htpy-refl))
    ( is-contr-total-Eq-Π
      ( λ n H → H ~ ((triangle-cone-sequence A c n) ∙h htpy-refl))
      ( λ n →
        is-contr-total-htpy' ((triangle-cone-sequence A c n) ∙h htpy-refl))
      ( triangle-cone-sequence A c))

is-equiv-htpy-cone-sequence-eq :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c c' : cone-sequence A X) →
  is-equiv (htpy-cone-sequence-eq A c c')
is-equiv-htpy-cone-sequence-eq A c =
  fundamental-theorem-id c
    ( reflexive-htpy-cone-sequence A c)
    ( is-contr-total-htpy-cone-sequence A c)
    ( htpy-cone-sequence-eq A c)

eq-htpy-cone-sequence :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c c' : cone-sequence A X) →
  htpy-cone-sequence A c c' → Id c c'
eq-htpy-cone-sequence A {X} c c' =
  inv-is-equiv (is-equiv-htpy-cone-sequence-eq A c c')

equiv-htpy-cone-sequence-eq :
  { l1 l2 : Level} (A : Sequence' l1) {X : UU l2} (c c' : cone-sequence A X) →
  Id c c' ≃ (htpy-cone-sequence A c c')
equiv-htpy-cone-sequence-eq A c c' =
  pair
    ( htpy-cone-sequence-eq A c c')
    ( is-equiv-htpy-cone-sequence-eq A c c')

{- We introduce sequential limits. -}

cone-sequence-map :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( Y : UU l3) → (Y → X) → cone-sequence A Y
cone-sequence-map A c Y h =
  pair
    ( λ n → (map-cone-sequence A c n) ∘ h)
    ( λ n → (triangle-cone-sequence A c n) ·r h)

universal-property-sequential-limit :
  ( l : Level) {l1 l2 : Level} (A : Sequence' l1) {X : UU l2}
  ( c : cone-sequence A X) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-sequential-limit l A c =
  (Y : UU l) → is-equiv (cone-sequence-map A c Y)

{- We introduce the canonical sequential limit. -}

canonical-sequential-limit :
  { l1 : Level} (A : Sequence' l1) → UU l1
canonical-sequential-limit A =
  Σ ( (n : ℕ) → type-seq' A n)
    ( λ a → (n : ℕ) → Id (map-seq' A n (a (succ-ℕ n))) (a n))

{- We characterize the identity type of the canonical sequential limit. -}

Eq-canonical-sequential-limit :
  { l1 : Level} (A : Sequence' l1) (x y : canonical-sequential-limit A) → UU l1
Eq-canonical-sequential-limit A x y =
  Σ ( (pr1 x) ~ (pr1 y)) (λ H →
    (n : ℕ) →
    Id ((ap (map-seq' A n) (H (succ-ℕ n))) ∙ (pr2 y n)) ((pr2 x n) ∙ (H n)))

reflexive-Eq-canonical-sequential-limit :
  { l1 : Level} (A : Sequence' l1) (x : canonical-sequential-limit A) →
  Eq-canonical-sequential-limit A x x
reflexive-Eq-canonical-sequential-limit A x =
  pair htpy-refl (htpy-inv htpy-right-unit)

Eq-canonical-sequential-limit-eq :
  { l1 : Level} (A : Sequence' l1) (x y : canonical-sequential-limit A) →
  Id x y → Eq-canonical-sequential-limit A x y
Eq-canonical-sequential-limit-eq A x .x refl =
  reflexive-Eq-canonical-sequential-limit A x

is-contr-total-Eq-canonical-sequential-limit :
  { l1 : Level} (A : Sequence' l1) (x : canonical-sequential-limit A) →
  is-contr
    ( Σ (canonical-sequential-limit A) (Eq-canonical-sequential-limit A x))
is-contr-total-Eq-canonical-sequential-limit A x =
  is-contr-total-Eq-structure
    ( λ y q (H : (n : ℕ) → Id (pr1 x n) (y n)) →
      (n : ℕ) →
        Id ((ap (map-seq' A n) (H (succ-ℕ n))) ∙ (q n)) ((pr2 x n) ∙ (H n)))
    ( is-contr-total-Eq-Π
      ( λ n yn → Id (pr1 x n) yn)
      ( λ n → is-contr-total-path (pr1 x n))
      ( pr1 x))
    ( pair (pr1 x) htpy-refl)
    ( is-contr-total-Eq-Π
      ( λ n q → Id q ((pr2 x n) ∙ refl))
      ( λ n → is-contr-total-path' ((pr2 x n) ∙ refl))
      ( pr2 x))

is-equiv-Eq-canonical-sequential-limit :
  { l1 : Level} (A : Sequence' l1) (x y : canonical-sequential-limit A) →
  is-equiv (Eq-canonical-sequential-limit-eq A x y)
is-equiv-Eq-canonical-sequential-limit A x =
  fundamental-theorem-id x
    ( reflexive-Eq-canonical-sequential-limit A x)
    ( is-contr-total-Eq-canonical-sequential-limit A x)
    ( Eq-canonical-sequential-limit-eq A x)

eq-Eq-canonical-sequential-limit :
  { l1 : Level} (A : Sequence' l1) {x y : canonical-sequential-limit A} →
  Eq-canonical-sequential-limit A x y → Id x y
eq-Eq-canonical-sequential-limit A {x} {y} =
  inv-is-equiv (is-equiv-Eq-canonical-sequential-limit A x y)

{- We equip the canonical sequential limit with the structure of a cone. -}

cone-canonical-sequential-limit :
  { l1 : Level} (A : Sequence' l1) →
  cone-sequence A (canonical-sequential-limit A)
cone-canonical-sequential-limit A =
  pair
    ( λ n a → pr1 a n)
    ( λ n a → pr2 a n)

{- We show that the canonical sequential limit satisfies the universal property
   of sequential limits. -}

inv-canonical-cone-sequence-map :
  { l1 l2 : Level} (A : Sequence' l1) (Y : UU l2) →
  cone-sequence A Y → (Y → canonical-sequential-limit A)
inv-canonical-cone-sequence-map A Y c y =
  pair
    ( λ n → map-cone-sequence A c n y)
    ( λ n → triangle-cone-sequence A c n y)

issec-inv-canonical-cone-sequence-map :
  { l1 l2 : Level} (A : Sequence' l1) (Y : UU l2) →
  ( ( cone-sequence-map A (cone-canonical-sequential-limit A) Y) ∘
    ( inv-canonical-cone-sequence-map A Y)) ~ id
issec-inv-canonical-cone-sequence-map A Y c =
  eq-htpy-cone-sequence A
    ( cone-sequence-map A
      ( cone-canonical-sequential-limit A)
      ( Y)
      ( inv-canonical-cone-sequence-map A Y c))
    ( c)
    ( reflexive-htpy-cone-sequence A c)

isretr-inv-canonical-cone-sequence-map :
  { l1 l2 : Level} (A : Sequence' l1) (Y : UU l2) →
  ( ( inv-canonical-cone-sequence-map A Y) ∘
    ( cone-sequence-map A (cone-canonical-sequential-limit A) Y)) ~ id
isretr-inv-canonical-cone-sequence-map A Y h =
  eq-htpy (λ y →
    eq-Eq-canonical-sequential-limit A
      ( reflexive-Eq-canonical-sequential-limit A (h y)))

universal-property-canonical-sequential-limit :
  ( l : Level) {l1 : Level} (A : Sequence' l1) →
  universal-property-sequential-limit l A (cone-canonical-sequential-limit A)
universal-property-canonical-sequential-limit l A Y =
  is-equiv-has-inverse
    ( inv-canonical-cone-sequence-map A Y)
    ( issec-inv-canonical-cone-sequence-map A Y)
    ( isretr-inv-canonical-cone-sequence-map A Y)

{- Unique mapping property for sequential limits. -}

unique-mapping-property-sequential-limit' :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( up-X : (l : Level) → universal-property-sequential-limit l A c)
  { Y : UU l3} (c' : cone-sequence A Y) →
  is-contr (fib (cone-sequence-map A c Y) c')
unique-mapping-property-sequential-limit' {l3 = l3} A c up-X {Y} =
  is-contr-map-is-equiv (up-X l3 Y)

map-universal-property-sequential-limit :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( up-X : (l : Level) → universal-property-sequential-limit l A c) →
  { Y : UU l3} (c' : cone-sequence A Y) → Y → X
map-universal-property-sequential-limit A c up-X c' =
  pr1 (center (unique-mapping-property-sequential-limit' A c up-X c'))

path-universal-property-sequential-limit :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( up-X : (l : Level) → universal-property-sequential-limit l A c) →
  { Y : UU l3} (c' : cone-sequence A Y) →
  Id ( cone-sequence-map A c Y
       ( map-universal-property-sequential-limit A c up-X c'))
     ( c')
path-universal-property-sequential-limit A c up-X c' =
  pr2 (center (unique-mapping-property-sequential-limit' A c up-X c'))

unique-mapping-property-sequential-limit :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( up-X : (l : Level) → universal-property-sequential-limit l A c) →
  { Y : UU l3} (c' : cone-sequence A Y) →
  is-contr
    ( Σ ( Y → X)
        ( λ h → htpy-cone-sequence A (cone-sequence-map A c Y h) c'))
unique-mapping-property-sequential-limit {l3 = l3} A c up-X {Y} c' =
  is-contr-equiv'
    ( fib (cone-sequence-map A c Y) c')
    ( equiv-tot
      ( λ h → equiv-htpy-cone-sequence-eq A (cone-sequence-map A c Y h) c'))
    ( unique-mapping-property-sequential-limit' A c up-X c')

htpy-universal-property-sequential-limit :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( up-X : (l : Level) → universal-property-sequential-limit l A c) →
  { Y : UU l3} (c' : cone-sequence A Y) →
  htpy-cone-sequence A
    ( cone-sequence-map A c Y
      ( map-universal-property-sequential-limit A c up-X c'))
    ( c')
htpy-universal-property-sequential-limit A c up-X {Y} c' =
  htpy-cone-sequence-eq A
    ( cone-sequence-map A c Y
      ( map-universal-property-sequential-limit A c up-X c'))
    ( c')
    ( path-universal-property-sequential-limit A c up-X c')

uniqueness-map-sequential-limit' :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( up-X : (l : Level) → universal-property-sequential-limit l A c)
  { Y : UU l3} (c' : cone-sequence A Y) →
  ( h : Y → X) (H : Id (cone-sequence-map A c Y h) c')
  ( h' : Y → X) (H' : Id (cone-sequence-map A c Y h') c') →
  h ~ h'
uniqueness-map-sequential-limit' A c up-X c' h H h' H' =
  htpy-eq
    ( ap pr1
      ( is-prop-is-contr'
        ( unique-mapping-property-sequential-limit' A c up-X c')
          ( pair h H)
          ( pair h' H')))

uniqueness-map-sequential-limit :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( up-X : (l : Level) → universal-property-sequential-limit l A c) →
  { Y : UU l3} (c' : cone-sequence A Y)
  ( h : Y → X) (H : htpy-cone-sequence A (cone-sequence-map A c Y h) c')
  ( h' : Y → X) (H' : htpy-cone-sequence A (cone-sequence-map A c Y h') c') →
  h ~ h'
uniqueness-map-sequential-limit A c up-X c' h H h' H' =
  htpy-eq
    ( ap pr1
      ( is-prop-is-contr'
        ( unique-mapping-property-sequential-limit A c up-X c')
        ( pair h H)
        ( pair h' H')))

{- We show a 3-for-2 property of sequential limits. -}

compose-cone-sequence-map :
  { l1 l2 l3 l4 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X)
  { Y : UU l3} {Z : UU l4} (h : Y → X) (k : Z → Y) →
  Id ( cone-sequence-map A (cone-sequence-map A c Y h) Z k)
     ( cone-sequence-map A c Z (h ∘ k))
compose-cone-sequence-map A c h k = refl

module 3-for-2-sequential-limit
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} {Y : UU l3}
  ( c : cone-sequence A X) (c' : cone-sequence A Y) (h : Y → X)
  ( e : htpy-cone-sequence A (cone-sequence-map A c Y h) c')
  where

  triangle-cone-cone-sequence :
    {l4 : Level} (Z : UU  l4) →
      ( cone-sequence-map A c' Z) ~
      ( ( cone-sequence-map A c Z) ∘ (λ (k : Z → Y) → h ∘ k))
  triangle-cone-cone-sequence Z k =
    ap (λ t → cone-sequence-map A t Z k)
      (inv (eq-htpy-cone-sequence A (cone-sequence-map A c Y h) c' e))

  is-equiv-universal-property-sequential-limit :
    ((l : Level) → universal-property-sequential-limit l A c) →
    ((l : Level) → universal-property-sequential-limit l A c') →
    is-equiv h
  is-equiv-universal-property-sequential-limit up-X up-Y =
    is-equiv-is-equiv-postcomp h (λ {l} Z →
      is-equiv-right-factor
        ( cone-sequence-map A c' Z)
        ( cone-sequence-map A c Z)
        ( λ k → h ∘ k)
        ( triangle-cone-cone-sequence Z)
        ( up-X l Z)
        ( up-Y l Z))

  universal-property-sequential-limit-is-equiv' :
    ((l : Level) → universal-property-sequential-limit l A c) →
    is-equiv h →
    ((l : Level) → universal-property-sequential-limit l A c')
  universal-property-sequential-limit-is-equiv' up-X is-equiv-h l Z =
    is-equiv-comp
      ( cone-sequence-map A c' Z)
      ( cone-sequence-map A c Z)
      ( λ k → h ∘ k)
      ( triangle-cone-cone-sequence Z)
      ( is-equiv-postcomp-is-equiv h is-equiv-h Z)
      ( up-X l Z)

  universal-property-sequential-limit-is-equiv :
    ((l : Level) → universal-property-sequential-limit l A c') →
    is-equiv h →
    ((l : Level) → universal-property-sequential-limit l A c)
  universal-property-sequential-limit-is-equiv up-Y is-equiv-h l Z =
    is-equiv-left-factor
      ( cone-sequence-map A c' Z)
      ( cone-sequence-map A c Z)
      ( λ k → h ∘ k)
      ( triangle-cone-cone-sequence Z)
      ( up-Y l Z)
      ( is-equiv-postcomp-is-equiv h is-equiv-h Z)

open 3-for-2-sequential-limit public

{- We prove the uniquely uniqueness of sequential limits. -}

uniquely-uniqueness-sequential-limit :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} {Y : UU l3} →
  ( c : cone-sequence A X) (c' : cone-sequence A Y) →
  ( (l : Level) → universal-property-sequential-limit l A c) →
  ( (l : Level) → universal-property-sequential-limit l A c') →
  is-contr (Σ (Y ≃ X)
    (λ e → htpy-cone-sequence A (cone-sequence-map A c Y (map-equiv e)) c'))
uniquely-uniqueness-sequential-limit A {X} {Y} c c' up-X up-Y =
  is-contr-total-Eq-substructure
    ( unique-mapping-property-sequential-limit A c up-X c')
    ( is-subtype-is-equiv)
    ( map-universal-property-sequential-limit A c up-X c')
    ( htpy-universal-property-sequential-limit A c up-X c')
    ( is-equiv-universal-property-sequential-limit A c c'
      ( map-universal-property-sequential-limit A c up-X c')
      ( htpy-universal-property-sequential-limit A c up-X c')
      ( up-X)
      ( up-Y))

{- We introduce the sequence of function types. -}

mapping-sequence :
  { l1 l2 : Level} (A : Sequence' l1) (X : UU l2) → Sequence' (l1 ⊔ l2)
mapping-sequence A X =
  pair
    ( λ n → X → type-seq' A n)
    ( λ n h → (map-seq' A n) ∘ h)

cone-mapping-sequence :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( Y : UU l3) → cone-sequence (mapping-sequence A Y) (Y → X)
cone-mapping-sequence A c Y =
  pair
    ( λ n h → (map-cone-sequence A c n) ∘ h)
    ( λ n h → eq-htpy ((triangle-cone-sequence A c n) ·r h))

universal-property-sequential-limit-cone-mapping-sequence :
  { l1 l2 l3 : Level} (A : Sequence' l1) {X : UU l2} (c : cone-sequence A X) →
  ( up-X : (l : Level) → universal-property-sequential-limit l A c) →
  ( Y : UU l3) (l : Level) →
  universal-property-sequential-limit l
    ( mapping-sequence A Y)
    ( cone-mapping-sequence A c Y)
universal-property-sequential-limit-cone-mapping-sequence A c up-X Y l Z =
  {!!}

{- We introduce cocones on a type sequence. -}

cocone-sequence :
  { l1 l2 : Level} (A : Sequence l1) (X : UU l2) → UU (l1 ⊔ l2)
cocone-sequence A X =
  Σ ( (n : ℕ) → type-seq A n → X) (λ i →
    (n : ℕ) → (i n) ~ ((i (succ-ℕ n)) ∘ (map-seq A n)))

map-cocone-sequence :
  { l1 l2 : Level} (A : Sequence l1) {X : UU l2} (c : cocone-sequence A X) →
  ( n : ℕ) → type-seq A n → X
map-cocone-sequence A c = pr1 c

triangle-cocone-sequence :
  { l1 l2 : Level} (A : Sequence l1) {X : UU l2} (c : cocone-sequence A X) →
  ( n : ℕ) →
  ( map-cocone-sequence A c n) ~
  ( (map-cocone-sequence A c (succ-ℕ n)) ∘ (map-seq A n))
triangle-cocone-sequence A c = pr2 c

{- We characterize the identity type of cocone-sequence. -}

naturality-htpy-cocone-sequence :
  { l1 l2 : Level} (A : Sequence l1) {X : UU l2} (c c' : cocone-sequence A X) →
  ( H : (n : ℕ) →
    (map-cocone-sequence A c n) ~ (map-cocone-sequence A c' n)) →
  ( n : ℕ) → UU (l1 ⊔ l2)
naturality-htpy-cocone-sequence A c c' H n =
  ( (H n) ∙h (triangle-cocone-sequence A c' n)) ~
      ( ( triangle-cocone-sequence A c n) ∙h
        ( (H (succ-ℕ n)) ·r (map-seq A n)))

htpy-cocone-sequence :
  { l1 l2 : Level} (A : Sequence l1) {X : UU l2}
  ( c c' : cocone-sequence A X) → UU (l1 ⊔ l2)
htpy-cocone-sequence A c c' =
  Σ ( (n : ℕ) → (map-cocone-sequence A c n) ~ (map-cocone-sequence A c' n))
    ( λ H → (n : ℕ) → naturality-htpy-cocone-sequence A c c' H n)

reflexive-htpy-cocone-sequence :
  { l1 l2 : Level} (A : Sequence l1) {X : UU l2} →
  ( c : cocone-sequence A X) → htpy-cocone-sequence A c c
reflexive-htpy-cocone-sequence A c =
  pair
    ( λ n → htpy-refl)
    ( λ n → htpy-inv htpy-right-unit)

htpy-cocone-sequence-eq :
  { l1 l2 : Level} (A : Sequence l1) {X : UU l2} →
  ( c c' : cocone-sequence A X) → Id c c' → htpy-cocone-sequence A c c'
htpy-cocone-sequence-eq A c .c refl =
  reflexive-htpy-cocone-sequence A c

is-contr-total-htpy-cocone-sequence :
  { l1 l2 : Level} (A : Sequence l1) {X : UU l2} (c : cocone-sequence A X) →
  is-contr (Σ (cocone-sequence A X) (htpy-cocone-sequence A c))
is-contr-total-htpy-cocone-sequence A c =
  is-contr-total-Eq-structure
    ( λ j t H →
      (n : ℕ) → naturality-htpy-cocone-sequence A c (pair j t) H n)
    ( is-contr-total-Eq-Π
      ( λ n j → map-cocone-sequence A c n ~ j)
      ( λ n → is-contr-total-htpy (map-cocone-sequence A c n))
      ( map-cocone-sequence A c))
    ( pair
      ( map-cocone-sequence A c)
      ( λ n → htpy-refl))
    ( is-contr-total-Eq-Π
      ( λ n H → H ~ ((triangle-cocone-sequence A c n) ∙h htpy-refl))
      ( λ n → is-contr-total-htpy'
        ( (triangle-cocone-sequence A c n) ∙h htpy-refl))
      ( triangle-cocone-sequence A c))

is-equiv-htpy-cocone-sequence-eq :
  { l1 l2 : Level} (A : Sequence l1) {X : UU l2} (c c' : cocone-sequence A X) →
  is-equiv (htpy-cocone-sequence-eq A c c')
is-equiv-htpy-cocone-sequence-eq A c =
  fundamental-theorem-id c
    ( reflexive-htpy-cocone-sequence A c)
    ( is-contr-total-htpy-cocone-sequence A c)
    ( htpy-cocone-sequence-eq A c)

{- We introduce the universal property of sequential colimits. -}

cocone-sequence-map :
  { l1 l2 l3 : Level} (A : Sequence l1)
  {X : UU l2} → cocone-sequence A X →
  (Y : UU l3) → (X → Y) → cocone-sequence A Y
cocone-sequence-map A c Y h =
  pair
    ( λ n → h ∘ (map-cocone-sequence A c n))
    ( λ n → h ·l (triangle-cocone-sequence A c n))

universal-property-sequential-colimit :
  ( l : Level) {l1 l2 : Level} (A : Sequence l1) {X : UU l2}
  ( c : cocone-sequence A X) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-sequential-colimit l A c =
  (Y : UU l) → is-equiv (cocone-sequence-map A c Y)

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
module Container.Traversable where

open import Prelude

record Traversable {a} (T : Set a → Set a) : Set (lsuc a) where
  field
    traverse : ∀ {F : Set a → Set a} {A B} {{AppF : Applicative F}} → (A → F B) → T A → F (T B)
    overlap {{super}} : Functor T

open Traversable {{...}} public

record Traversable′ {a b} (T : ∀ {a} → Set a → Set a) : Set (lsuc (a ⊔ b)) where
  field
    traverse′ : ∀ {F : Set b → Set b} {A : Set a} {B : Set b}
                  {{AppF : Applicative F}} → (A → F B) → T A → F (T B)
    overlap {{super}} : Functor′ {a} {b} T

open Traversable′ {{...}} public

{-# DISPLAY Traversable.traverse   _ = traverse #-}
{-# DISPLAY Traversable′.traverse′ _ = traverse′ #-}

--- Instances ---

instance
  TraversableMaybe : ∀ {a} → Traversable {a} Maybe
  traverse {{TraversableMaybe}} f m = maybe (pure nothing) (λ x -> pure just <*> f x) m

  TraversableList : ∀ {a} → Traversable {a} List
  traverse {{TraversableList}} f xs = foldr (λ x fxs → pure _∷_ <*> f x <*> fxs) (pure []) xs

  TraversableVec : ∀ {a n} → Traversable {a} (λ A → Vec A n)
  traverse {{TraversableVec}} f []       = pure []
  traverse {{TraversableVec}} f (x ∷ xs) = ⦇ f x ∷ traverse f xs ⦈

  Traversable′Maybe : ∀ {a b} → Traversable′ {a} {b} Maybe
  traverse′ {{Traversable′Maybe}} f m = maybe (pure nothing) (λ x -> pure just <*> f x) m

  Traversable′List : ∀ {a b} → Traversable′ {a} {b} List
  traverse′ {{Traversable′List}} f xs = foldr (λ x fxs → pure _∷_ <*> f x <*> fxs) (pure []) xs

  Traversable′Vec : ∀ {a b n} → Traversable′ {a} {b} (λ A → Vec A n)
  traverse′ {{Traversable′Vec}} f []       = pure []
  traverse′ {{Traversable′Vec}} f (x ∷ xs) = ⦇ f x ∷ traverse′ f xs ⦈

mapM : ∀ {a b} {F : Set b → Set b} {A : Set a} {B : Set b} {{AppF : Applicative F}} →
         (A → F B) → List A → F (List B)
mapM = traverse′

mapM! : ∀ {a} {F : Set → Set} {A : Set a} {{AppF : Applicative F}} →
          (A → F ⊤) → List A → F ⊤
mapM! f xs = _ <$ mapM f xs

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:
-- This file tests that implicit record fields are not printed out (by
-- default).

module ImplicitRecordFields where

record R : Set₁ where
  field
    {A}         : Set
    f           : A → A
    {B C} D {E} : Set
    g           : B → C → E

postulate
  A  : Set
  r₁ : R

r₂ : R
r₂ = record
  { A = A
  ; f = λ x → x
  ; B = A
  ; C = A
  ; D = A
  ; g = λ x _ → x
  }

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

foo : r₁ ≡ r₂
foo = refl

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Data.Maybe where

open import Data.Maybe.Base public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Equivalence (coinhabitance)
------------------------------------------------------------------------

module Function.Equivalence where

open import Function using (flip)
open import Function.Equality as F
  using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
open import Level
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

-- Setoid equivalence.

record Equivalence {f₁ f₂ t₁ t₂}
                   (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
                   Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    to   : From ⟶ To
    from : To ⟶ From

-- Set equivalence.

infix 3 _⇔_

_⇔_ : ∀ {f t} → Set f → Set t → Set _
From ⇔ To = Equivalence (P.setoid From) (P.setoid To)

equivalence : ∀ {f t} {From : Set f} {To : Set t} →
              (From → To) → (To → From) → From ⇔ To
equivalence to from = record { to = P.→-to-⟶ to; from = P.→-to-⟶ from }

------------------------------------------------------------------------
-- Map and zip

map : ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
        {f₁′ f₂′ t₁′ t₂′}
        {From′ : Setoid f₁′ f₂′} {To′ : Setoid t₁′ t₂′} →
      ((From ⟶ To) → (From′ ⟶ To′)) →
      ((To ⟶ From) → (To′ ⟶ From′)) →
      Equivalence From To → Equivalence From′ To′
map t f eq = record { to = t to; from = f from }
  where open Equivalence eq

zip : ∀ {f₁₁ f₂₁ t₁₁ t₂₁}
        {From₁ : Setoid f₁₁ f₂₁} {To₁ : Setoid t₁₁ t₂₁}
        {f₁₂ f₂₂ t₁₂ t₂₂}
        {From₂ : Setoid f₁₂ f₂₂} {To₂ : Setoid t₁₂ t₂₂}
        {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
      ((From₁ ⟶ To₁) → (From₂ ⟶ To₂) → (From ⟶ To)) →
      ((To₁ ⟶ From₁) → (To₂ ⟶ From₂) → (To ⟶ From)) →
      Equivalence From₁ To₁ → Equivalence From₂ To₂ →
      Equivalence From To
zip t f eq₁ eq₂ =
  record { to = t (to eq₁) (to eq₂); from = f (from eq₁) (from eq₂) }
  where open Equivalence

------------------------------------------------------------------------
-- Equivalence is an equivalence relation

-- Identity and composition (reflexivity and transitivity).

id : ∀ {s₁ s₂} → Reflexive (Equivalence {s₁} {s₂})
id {x = S} = record
  { to   = F.id
  ; from = F.id
  }

infixr 9 _∘_

_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂} →
      TransFlip (Equivalence {f₁} {f₂} {m₁} {m₂})
                (Equivalence {m₁} {m₂} {t₁} {t₂})
                (Equivalence {f₁} {f₂} {t₁} {t₂})
f ∘ g = record
  { to   = to   f ⟪∘⟫ to   g
  ; from = from g ⟪∘⟫ from f
  } where open Equivalence

-- Symmetry.

sym : ∀ {f₁ f₂ t₁ t₂} →
      Sym (Equivalence {f₁} {f₂} {t₁} {t₂})
          (Equivalence {t₁} {t₂} {f₁} {f₂})
sym eq = record
  { from       = to
  ; to         = from
  } where open Equivalence eq

-- For fixed universe levels we can construct setoids.

setoid : (s₁ s₂ : Level) → Setoid (suc (s₁ ⊔ s₂)) (s₁ ⊔ s₂)
setoid s₁ s₂ = record
  { Carrier       = Setoid s₁ s₂
  ; _≈_           = Equivalence
  ; isEquivalence = record {refl = id; sym = sym; trans = flip _∘_}
  }

⇔-setoid : (ℓ : Level) → Setoid (suc ℓ) ℓ
⇔-setoid ℓ = record
  { Carrier       = Set ℓ
  ; _≈_           = _⇔_
  ; isEquivalence = record {refl = id; sym = sym; trans = flip _∘_}
  }


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.Span

module lib.types.PushoutFlip where

module _ {i j k} {d : Span {i} {j} {k}} where

  module PushoutFlip = PushoutRec
    (right {d = Span-flip d})
    (left {d = Span-flip d})
    (λ z → ! (glue {d = Span-flip d} z))

  Pushout-flip : Pushout d → Pushout (Span-flip d)
  Pushout-flip = PushoutFlip.f

Pushout-flip-involutive : ∀ {i j k} (d : Span {i} {j} {k})
  (s : Pushout d) → Pushout-flip (Pushout-flip s) == s
Pushout-flip-involutive d = Pushout-elim
  (λ a → idp)
  (λ b → idp)
  (λ c → ↓-∘=idf-in' Pushout-flip Pushout-flip $
     ap Pushout-flip (ap Pushout-flip (glue c))
       =⟨ ap (ap Pushout-flip) (PushoutFlip.glue-β c) ⟩
     ap Pushout-flip (! (glue c))
       =⟨ ap-! Pushout-flip (glue c) ⟩
     ! (ap Pushout-flip (glue c))
       =⟨ ap ! (PushoutFlip.glue-β c) ⟩
     ! (! (glue c))
       =⟨ !-! (glue c) ⟩
     glue c
       =∎)

{- Equivalence for spans with proofs that the equivalence swaps the
 - injections -}
Pushout-flip-equiv : ∀ {i j k} (d : Span {i} {j} {k})
  → Pushout d ≃ Pushout (Span-flip d)
Pushout-flip-equiv d =
  equiv Pushout-flip Pushout-flip
    (Pushout-flip-involutive (Span-flip d))
    (Pushout-flip-involutive d)
  where open Span d

module _ {i j k} (ps : ⊙Span {i} {j} {k}) where

  open ⊙Span ps

  private
    s = ⊙Span-to-Span ps

    preserves : –> (Pushout-flip-equiv s) (left (pt X)) == left (pt Y)
    preserves = snd (⊙right (⊙Span-flip ps))

  ⊙Pushout-flip : ⊙Pushout ps ⊙→ ⊙Pushout (⊙Span-flip ps)
  ⊙Pushout-flip = (PushoutFlip.f , preserves)

  {- action of [Pushout-flip] on [snd ⊙right] -}
  ap-Pushout-flip-right-pt : ap Pushout-flip (snd (⊙right ps))
          == ! (snd (⊙right (⊙Span-flip ps)))
  ap-Pushout-flip-right-pt = lemma f g
    where
    lemma : {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
            (f : Z ⊙→ X) (g : Z ⊙→ Y)
          → ap (Pushout-flip {d = ⊙Span-to-Span (⊙span X Y Z f g)})
              (ap right (! (snd g)) ∙ ! (glue (pt Z)) ∙' ap left (snd f))
         == ! (ap right (! (snd f)) ∙ ! (glue (pt Z)) ∙' ap left (snd g))
    lemma {Z = Z} (f , idp) (g , idp) =
      ap Pushout-flip (! (glue (pt Z)))
        =⟨ ap-! Pushout-flip (glue (pt Z)) ⟩
      ! (ap Pushout-flip (glue (pt Z)))
        =⟨ PushoutFlip.glue-β (pt Z) |in-ctx ! ⟩
      ! (! (glue (pt Z)))
        =∎

module _ {i j k} (ps : ⊙Span {i} {j} {k}) where

  open ⊙Span ps

  ⊙Pushout-flip-involutive : ∀ {i j k} (ps : ⊙Span {i} {j} {k})
    → ⊙Pushout-flip (⊙Span-flip ps) ⊙∘ ⊙Pushout-flip ps == ⊙idf _
  ⊙Pushout-flip-involutive ps =
    ⊙λ= (Pushout-flip-involutive _) lemma
    where
    lemma :
      ap Pushout-flip (snd (⊙right (⊙Span-flip ps))) ∙ snd (⊙right ps)
      == idp
    lemma =
      ap Pushout-flip (snd (⊙right (⊙Span-flip ps))) ∙ snd (⊙right ps)
        =⟨ ap-Pushout-flip-right-pt (⊙Span-flip ps) |in-ctx _∙ snd (⊙right ps) ⟩
      ! (snd (⊙right ps)) ∙ snd (⊙right ps)
        =⟨ !-inv-l (snd (⊙right ps)) ⟩
      idp
        =∎

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Numeral.Natural.Prime where

import Lvl
open import Data.Boolean.Stmt
open import Logic
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Relator.Equals

PrimeProof : {_ : ℕ} → Stmt{Lvl.𝟎}
PrimeProof{n} = (∀{x} → (𝐒(x) ∣ 𝐒(𝐒(n))) → ((x ≡ 𝟎) ∨ (x ≡ 𝐒(n))))

-- A prime number is a number `n` in which its only divisors are `{1,n}`.
data Prime : ℕ → Stmt{Lvl.𝟎} where
  intro : ∀{n} → PrimeProof{n} → Prime(𝐒(𝐒(n)))

-- A composite number is a number which are the product of two numbers greater than or equals 2.
data Composite : ℕ → Stmt{Lvl.𝟎} where
  intro : (a b : ℕ) → Composite(𝐒(𝐒(a)) ⋅ 𝐒(𝐒(b)))

Composite-intro : (a b : ℕ) → ⦃ _ : IsTrue(a ≥? 2) ⦄ ⦃ _ : IsTrue(b ≥? 2) ⦄ → Composite(a ⋅ b)
Composite-intro (𝐒(𝐒 a)) (𝐒(𝐒 b)) = intro a b

-- PrimeFactor(n)(p) means that `p` is a prime factor of `n`.
-- A prime factor `p` of `n` is a prime number that divides `n`.
record PrimeFactor(n : ℕ) (p : ℕ) : Stmt{Lvl.𝟎} where
  constructor intro
  field
    ⦃ prime ⦄  : Prime(p)
    ⦃ factor ⦄ : (p ∣ n)

-- greater-prime-existence : ∀{p} → Prime(p) → ∃(p₂ ↦ Prime(p₂) ∧ (p₂ > p))

-- TODO: https://math.stackexchange.com/questions/2786458/a-formal-statement-of-the-fundamental-theorem-of-arithmetic
-- TODO: Needs to be a finite multiset of primes.
-- PrimeMultiset = Type{Lvl.𝟎}
-- PrimeMultiSet = ((p : ℕ) → ⦃ _ : Prime(p) ⦄ → ℕ)

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:
------------------------------------------------------------------------
-- Some simple binary relations
------------------------------------------------------------------------

module Relation.Binary.Simple where

open import Relation.Binary
open import Data.Unit
open import Data.Empty

-- Constant relations.

Const : ∀ {a} → Set → Rel a
Const I = λ _ _ → I

-- The universally true relation.

Always : ∀ {a} → Rel a
Always = Const ⊤

-- The universally false relation.

Never : ∀ {a} → Rel a
Never = Const ⊥

-- Always is an equivalence.

Always-isEquivalence : ∀ {a} → IsEquivalence (Always {a})
Always-isEquivalence = record {}

max_issues_repo_name: larrytheliquid/Lemmachine


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

-- This file contains some core definitions which are reexported by
-- Relation.Binary.PropositionalEquality.

module Relation.Binary.PropositionalEquality.Core where

open import Relation.Binary.Core
open import Relation.Binary.Consequences.Core

------------------------------------------------------------------------
-- Some properties

sym : {a : Set} → Symmetric {a} _≡_
sym refl = refl

trans : {a : Set} → Transitive {a} _≡_
trans refl refl = refl

subst : {a : Set} → Substitutive {a} _≡_
subst P refl p = p

resp₂ : ∀ {a} (∼ : Rel a) → ∼ Respects₂ _≡_
resp₂ _∼_ = subst⟶resp₂ _∼_ subst

isEquivalence : ∀ {a} → IsEquivalence {a} _≡_
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }


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

open import Cubical.HITs.S3.Base public

-- open import Cubical.HITs.S3.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K #-}
module container.m.from-nat.core where

open import level
open import sum
open import equality
open import function
open import container.core
open import sets.nat.core
open import sets.nat.struct
open import sets.unit
open import hott.level

-- Definition 9 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
module Limit {i} (X : ℕ → Set i)
                 (π : (n : ℕ) → X (suc n) → X n) where
  L : Set _
  L = Σ ((n : ℕ) → X n) λ x
    → (∀ n → π n (x (suc n)) ≡ x n)

  p : (n : ℕ) → L → X n
  p n (x , q) = x n

  β : (n : ℕ) → ∀ x → π n (p (suc n) x) ≡ p n x
  β n (x , q) = q n

module Limit-univ {i j}{Z : Set i}
                  (X : Z → ℕ → Set j)
                  (π : (z : Z)(n : ℕ) → X z (suc n) → X z n) where
  open module WithZ (z : Z) = Limit (X z) (π z)

  -- Lemma 10 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  univ-iso : ( Σ ((n : ℕ)(z : Z) → X z n) λ u
             → ∀ n z → π z n (u (suc n) z) ≡ u n z )
           ≅ ((z : Z) → L z)
  univ-iso = record
    { to = λ { (u , q) z → (λ n → u n z) , (λ n → q n z) }
    ; from = λ f → (λ n z → p z n (f z)) , (λ n z → β z n (f z))
    ; iso₁ = λ { (u , q) → refl }
    ; iso₂ = λ f → refl }

module Limit-op {i} (X : ℕ → Set i)
                    (ρ : (n : ℕ) → X n → X (suc n)) where
  L : Set _
  L = Σ ((n : ℕ) → X n) λ x
    → (∀ n → x (suc n) ≡ ρ n (x n))

  module _ (χ : (x₀ : X 0)
              → contr ( Σ ((n : ℕ) → X n) λ x
              → (x₀ ≡ x 0)
              × (∀ n → ρ n (x n) ≡ x (suc n)) ) ) where
    lim-contr' : L ≅ X 0
    lim-contr' = begin
        L
      ≅⟨ sym≅ ( Σ-ap-iso refl≅ λ x → Π-ap-iso refl≅ λ n → sym≡-iso _ _ ) ⟩
        ( Σ ((n : ℕ) → X n) λ x
        → (∀ n → ρ n (x n) ≡ x (suc n)) )
      ≅⟨ sym≅ ( Σ-ap-iso refl≅ λ x → ×-left-unit ) ⟩
        ( Σ ((n : ℕ) → X n) λ x
        → Σ ⊤ λ _
        → (∀ n → ρ n (x n) ≡ x (suc n)) )
      ≅⟨ sym≅ ( Σ-ap-iso refl≅ λ x
              → Σ-ap-iso (contr-⊤-iso (singl-contr' (x 0))) λ _
              → refl≅ ) ⟩
        ( Σ ((n : ℕ) → X n) λ x
        → Σ (singleton' (x 0)) λ _
        → (∀ n → ρ n (x n) ≡ x (suc n)) )
      ≅⟨ record
          { to = λ { (x , (z , p) , q) → (z , x , p , q) }
          ; from = λ { (z , x , p , q) → (x , (z , p) , q) }
          ; iso₁ = λ { (x , (z , p) , q) → refl }
          ; iso₂ = λ { (z , x , p , q) → refl } } ⟩
        ( Σ (X 0) λ z
        → Σ ((n : ℕ) → X n) λ x
        → Σ (z ≡ x 0) λ _
        → (∀ n → ρ n (x n) ≡ x (suc n)) )
      ≅⟨ (Σ-ap-iso refl≅ λ z → contr-⊤-iso (χ z)) ·≅ ×-right-unit ⟩
        X 0
      ∎
      where
        open ≅-Reasoning

-- Lemma 11 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  lim-contr : L ≅ X 0
  lim-contr = lim-contr' (λ z → ℕ-initial X z ρ)

module Limit-op-simple {i} (X : Set i) where
  module L = Limit-op (λ _ → X) (λ _ x → x)

  lim-contr : L.L ≅ X
  lim-contr = L.lim-contr' ℕ-initial-simple

module Limit-univⁱ
         {ℓ li}(I : Set li)
         (X : ℕ → I → Set ℓ)
         (π : ∀ n → X (suc n) →ⁱ X n) where

  open module WithI (i : I) = Limit (λ n → X n i) (λ n → π n i)

  module _ {ℓ'}{Z : I → Set ℓ'} where
    private
      IZ = Σ I Z

      XZ : IZ → ℕ → Set _
      XZ (i , _) n = X n i

      πZ : (iz : IZ)(n : ℕ) → XZ iz (suc n) → XZ iz n
      πZ (i , _) n = π n i

  -- Lemma 10 (indexed version) in Ahrens, Capriotti and Spadotti
    univ-iso : ( Σ ((n : ℕ) → Z →ⁱ X n) λ f
               → (∀ n → π n ∘ⁱ f (suc n) ≡ f n) )
             ≅ (Z →ⁱ L)
    univ-iso = begin
       ( Σ ((n : ℕ)(i : I) → Z i → X n i) λ f
       → ∀ n → (λ i z → π n i (f (suc n) i z)) ≡ f n )
     ≅⟨ sym≅ ( Σ-ap-iso refl≅ λ f → Π-ap-iso refl≅ λ n → funext-isoⁱ ) ⟩
        ( Σ ((n : ℕ)(i : I) → Z i → X n i) λ f
        → ∀ n i z → π n i (f (suc n) i z) ≡ f n i z )
     ≅⟨ record { to = λ { (u , q) → (λ { n (i , z) → u n i z })
                                  , (λ { n (i , z) → q n i z }) }
               ; from = λ { (u , q) → (λ { n i z → u n (i , z) })
                                    , (λ { n i z → q n (i , z) }) }
               ; iso₁ = λ { (u , q) → refl }
               ; iso₂ = λ { (u , q) → refl } } ⟩
        ( Σ ((n : ℕ)(iz : IZ) → XZ iz n) λ f
        → (∀ n iz → πZ iz n (f (suc n) iz) ≡ f n iz) )
     ≅⟨ Limit-univ.univ-iso XZ πZ ⟩
       ((iz : IZ) → L (proj₁ iz))
     ≅⟨ curry-iso (λ i z → L i) ⟩
       (Z →ⁱ L)
     ∎
     where
       open ≅-Reasoning

module F-Limit {ℓ li la lb} (c : Container li la lb)
               (X : Container.I c → ℕ → Set ℓ)
               (π : ∀ i → (n : ℕ) → X i (suc n) → X i n) where
  open Container c
  private
    open module WithI (i : I) = Limit (X i) (π i)

    X' : I → ℕ → Set _
    X' i n = F (λ i → X i n) i

    π' : ∀ i n → X' i (suc n) → X' i n
    π' i n = imap (λ i → π i n) i

    open module WithI' (i : I) = Limit (X' i) (π' i)
      using () renaming ( L to L'
                        ; p to p'
                        ; β to β' )

  -- Lemma 13 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  lim-iso : ∀ i → F L i ≅ L' i
  lim-iso i = begin
      F L i
    ≅⟨ ( Σ-ap-iso refl≅ λ a
       → sym≅ (Limit-univ.univ-iso (λ b n → X (r b) n) (λ b n → π (r b) n)) ) ⟩
      ( Σ (A i) λ a
      → Σ ((n : ℕ) → (b : B a) → X (r b) n) λ u
      → ∀ n b → π (r b) n (u (suc n) b) ≡ u n b )
    ≅⟨ ( Σ-ap-iso refl≅ λ a
        → Σ-ap-iso refl≅ λ u
        → Π-ap-iso refl≅ λ n
        → strong-funext-iso ) ⟩
      ( Σ (A i) λ a
      → Σ ((n : ℕ) → (b : B a) → X (r b) n) λ u
      → ∀ n → (λ b → π (r b) n (u (suc n) b)) ≡ u n )
    ≅⟨ ( Σ-ap-iso (sym≅ (Limit-op-simple.lim-contr (A i))) λ a → refl≅ ) ⟩
      ( Σ (Σ (ℕ → A i) λ a → ∀ n → a (suc n) ≡ a n) λ { (a , q)
      → Σ ((n : ℕ) → (b : B (a n)) → X (r b) n) λ u
      → ∀ n → subst (λ a → (b : B a) → X (r b) n) (q n)
                (λ b → π (r b) n (u (suc n) b)) ≡ u n } )
    ≅⟨ record
         { to = λ { ((a , q) , u , z) → ((a , u) , q , z) }
         ; from = λ { ((a , u) , q , z) → ((a , q) , u , z) }
         ; iso₁ = λ { ((a , q) , u , z) → refl }
         ; iso₂ = λ { ((a , u) , q , z) → refl } } ⟩
      ( Σ (Σ (ℕ → A i) λ a → ((n : ℕ) → (b : B (a n)) → X (r b) n)) λ { (a , u)
      → Σ (∀ n → a (suc n) ≡ a n) λ q
      → ∀ n → subst (λ a → (b : B a) → X (r b) n) (q n)
                (λ b → π (r b) n (u (suc n) b)) ≡ u n } )
    ≅⟨ ( Σ-ap-iso refl≅ λ { (a , u) → sym≅ ΠΣ-swap-iso } ) ⟩
      ( Σ (Σ (ℕ → A i) λ a → ((n : ℕ) → (b : B (a n)) → X (r b) n)) λ { (a , u)
      → ∀ n
      → Σ (a (suc n) ≡ a n) λ q
      → subst (λ a → (b : B a) → X (r b) n) q
              (λ b → π (r b) n (u (suc n) b)) ≡ u n } )
    ≅⟨ ( Σ-ap-iso refl≅ λ { (a , u)
            → Π-ap-iso refl≅ λ n
            → Σ-split-iso } ) ⟩
      ( Σ (Σ (ℕ → A i) λ a → ((n : ℕ) → (b : B (a n)) → X (r b) n)) λ { (a , u)
      → ∀ n
      → _≡_ { A = Σ (A i) λ a → (b : B a) → X (r b) n }
             (a (suc n) , λ b → π (r b) n (u (suc n) b))
             (a n , u n) } )
    ≅⟨ ( Σ-ap-iso (sym≅ ΠΣ-swap-iso) λ w → Π-ap-iso refl≅ λ n → refl≅ ) ⟩
      ( Σ ((n : ℕ) → F (λ i → X i n) i) λ w
      → (∀ n → imap (λ i → π i n) i (w (suc n)) ≡ w n) )
    ∎
    where
      open ≅-Reasoning

module Limit-shift {ℓ} (X : ℕ → Set ℓ)
                       (π : (n : ℕ) → X (suc n) → X n) where
  open Limit X π

  X' : ℕ → Set ℓ
  X' n = X (suc n)

  π' : (n : ℕ) → X' (suc n) → X' n
  π' n = π (suc n)

  open Limit X' π' using ()
    renaming (L to L' ; p to p' ; β to β')

  -- Lemma 12 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  shift-iso : L' ≅ L
  shift-iso = begin
      ( Σ ((n : ℕ) → X (suc n)) λ x
      → ∀ n → π (suc n) (x (suc n)) ≡ x n )
    ≅⟨ ( Σ-ap-iso refl≅ λ y
       → sym≅ ×-left-unit
       ·≅ (Σ-ap-iso (sym≅ (contr-⊤-iso (singl-contr _))) λ _ → refl≅) ) ⟩
      ( Σ ((n : ℕ) → X (suc n)) λ y
      → Σ (singleton (π 0 (y 0))) λ _
      → (∀ n → π (suc n) (y (suc n)) ≡ y n) )
    ≅⟨ record
         { to = λ { (y , (x₀ , q₀) , q) → ((x₀ , y) , (q₀ , q)) }
         ; from = λ { ((x₀ , y) , (q₀ , q)) → (y , (x₀ , q₀) , q) }
         ; iso₁ = λ { (y , (x₀ , q₀) , q) → refl }
         ; iso₂ = λ { ((x₀ , y) , (q₀ , q)) → refl } } ⟩
      ( Σ (X 0 × ((n : ℕ) → X (suc n))) λ { (x₀ , y)
      → ((π 0 (y 0) ≡ x₀) × (∀ n → π (suc n) (y (suc n)) ≡ y n)) } )
    ≅⟨ (Σ-ap-iso (sym≅ ℕ-elim-shift) λ _ → (sym≅ ℕ-elim-shift)) ⟩
      ( Σ ((n : ℕ) → X n) λ x
      → ∀ n → π n (x (suc n)) ≡ x n )
    ∎
    where
      open ≅-Reasoning

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of the identity function
------------------------------------------------------------------------

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

module Function.Identity.Categorical {ℓ} where

open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Category.Comonad
open import Function

Identity : Set ℓ → Set ℓ
Identity A = A

functor : RawFunctor Identity
functor = record
  { _<$>_ = id
  }

applicative : RawApplicative Identity
applicative = record
  { pure = id
  ; _⊛_  = id
  }

monad : RawMonad Identity
monad = record
  { return = id
  ; _>>=_  = _|>′_
  }

comonad : RawComonad Identity
comonad = record
  { extract = id
  ; extend  = id
  }


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Environments (heterogeneous collections)
------------------------------------------------------------------------

module Data.Star.Environment (Ty : Set) where

open import Data.Star
open import Data.Star.List
open import Data.Star.Decoration
open import Data.Star.Pointer as Pointer hiding (lookup)
open import Data.Unit
open import Relation.Binary.PropositionalEquality

-- Contexts, listing the types of all the elements in an environment.

Ctxt : Set
Ctxt = List Ty

-- Variables (de Bruijn indices); pointers into environments.

infix 4 _∋_

_∋_ : Ctxt → Ty → Set
Γ ∋ σ = Any (λ _ → ⊤) (_≡_ σ) Γ

vz : ∀ {Γ σ} → Γ ▻ σ ∋ σ
vz = this refl

vs : ∀ {Γ σ τ} → Γ ∋ τ → Γ ▻ σ ∋ τ
vs = that tt

-- Environments. The T function maps types to element types.

Env : (Ty → Set) → Ctxt → Set
Env T Γ = All T Γ

-- A safe lookup function for environments.

lookup : ∀ {Γ σ} {T : Ty → Set} → Γ ∋ σ → Env T Γ → T σ
lookup i ρ with Pointer.lookup i ρ
... | result refl x = x


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Congruence of application.
--
-- If f ≡ g and x ≡ y, then (f x) ≡ (g y).
------------------------------------------------------------------------

module Theorem.CongApp where

open import Relation.Binary.PropositionalEquality public

infixl 0 _⟨$⟩_

_⟨$⟩_ : ∀ {a b} {A : Set a} {B : Set b}
  {f g : A → B} {x y : A} →
  f ≡ g → x ≡ y → f x ≡ g y

_⟨$⟩_ = cong₂ (λ x y → x y)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
-- Andreas, 2017-09-09
-- Builtin constructors may be ambiguous / overloaded.

data Semmel : Set where
  false : Semmel

data Bool : Set where
  true  : Bool
  false : Bool

{-# BUILTIN BOOL  Bool #-}
{-# BUILTIN TRUE  true #-}
{-# BUILTIN FALSE false  #-}  -- This is accepted.

data Brezel A : Set where
  _∷_ : (x : A) (xs : Brezel A) → Brezel A

data List₀ A : Set where
  []  : List₀ A
  _∷_ : (x : A) (xs : List₀ A) → List₀ A

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

{-# BUILTIN LIST List₀ #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Test where

data _∨_ (A B : Set) : Set where
  inj₁ : A → A ∨ B
  inj₂ : B → A ∨ B

postulate
  A B    : Set
  ∨-comm : A ∨ B → B ∨ A
{-# ATP prove ∨-comm #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax Prod | P

type
  _⊗_ : 2-ary | l40

term
  pair : α  β  ->  α ⊗ β | ⟨_,_⟩
  fst  : α ⊗ β  ->  α
  snd  : α ⊗ β  ->  β

theory
  (fβ) a : α  b : β |> fst (pair(a, b))      = a
  (sβ) a : α  b : β |> snd (pair(a, b))      = b
  (pη) p : α ⊗ β    |> pair (fst(p), snd(p)) = p
-}

module Prod.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Prod.Signature

private
  variable
    Γ Δ Π : Ctx
    α β : PT
    𝔛 : Familyₛ

-- Inductive term declaration
module P:Terms (𝔛 : Familyₛ) where

  data P : Familyₛ where
    var  : ℐ ⇾̣ P
    mvar : 𝔛 α Π → Sub P Π Γ → P α Γ

    ⟨_,_⟩ : P α Γ → P β Γ → P (α ⊗ β) Γ
    fst   : P (α ⊗ β) Γ → P α Γ
    snd   : P (α ⊗ β) Γ → P β Γ

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Pᵃ : MetaAlg P
  Pᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (pairₒ ⋮ a , b) → ⟨_,_⟩ a b
      (fstₒ  ⋮ a)     → fst   a
      (sndₒ  ⋮ a)     → snd   a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Pᵃ = MetaAlg Pᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : P ⇾̣ 𝒜
    𝕊 : Sub P Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (⟨_,_⟩ a b) = 𝑎𝑙𝑔 (pairₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (fst   a)   = 𝑎𝑙𝑔 (fstₒ  ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (snd   a)   = 𝑎𝑙𝑔 (sndₒ  ⋮ 𝕤𝕖𝕞 a)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Pᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ P α Γ) → 𝕤𝕖𝕞 (Pᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (pairₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (fstₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (sndₒ  ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ P ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : P ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ Pᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : P α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub P Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (⟨_,_⟩ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (fst a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (snd a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
P:Syn : Syntax
P:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = P:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open P:Terms 𝔛 in record
    { ⊥ = P ⋉ Pᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax P:Syn public
open P:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Pᵃ public
open import SOAS.Metatheory P:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Issue363 where

infixl 0 _>>=_

postulate
  A     : Set
  x     : A
  _>>=_ : A → (A → A) → A
  P     : A → Set

lemma : P ((x >>= λ x → x) >>= λ x → x)
lemma = {!!}

-- The type of the goal above was printed as follows:
--
--   P (x >>= λ x' → x' >>= λ x' → x')
--
-- This is not correct.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2014-04-11, issue reported by James Chapman
-- {-# OPTIONS -v tc.decl.ax:100 #-}
-- {-# OPTIONS -v tc.polarity:100 #-}
{-# OPTIONS --copatterns --sized-types #-}
module _ where

open import Common.Size

module Works where
  mutual
    data Delay i (A : Set) : Set where
      now   : A → Delay i A
      later : ∞Delay i A → Delay i A

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

  mutual
    _=<<_ : ∀{i A B} → Delay i A → (A → Delay i B) → Delay i B
    now x   =<< f = f x
    later x =<< f = later (x ∞=<< f)

    _∞=<<_ : ∀{i A B} → ∞Delay i A → (A → Delay i B) → ∞Delay i B
    force (c ∞=<< f) = force c =<< f

-- Polarity of Issue1099.Delay from positivity: [Contravariant,Covariant]
-- Refining polarity with type  Size → Set → Set
-- Polarity of Issue1099.Delay: [Contravariant,Covariant]

module Fails where
  mutual
    data Delay i A : Set where
      now   : A → Delay i A
      later : ∞Delay i A → Delay i A

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

  mutual
    _=<<_ : ∀{i A B} → Delay i A → (A → Delay i B) → Delay i B
    now x   =<< f = f x
    later x =<< f = later (x ∞=<< f)

    _∞=<<_ : ∀{i A B} → ∞Delay i A → (A → Delay i B) → ∞Delay i B
    force (c ∞=<< f) = force c =<< f

-- Polarity of Issue1099.Delay from positivity: [Contravariant,Covariant]
-- Refining polarity with type  (i₁ : Size) → Set → Set
-- WAS: Polarity of Issue1099.Delay: [Invariant,Covariant]
-- NOW: Polarity of Issue1099.Delay: [Contravariant,Covariant]

-- Polarity refinement calls free variable analysis, which is not in the
-- monad.  Thus, need to instantiate metas before polarity refinement.


text:
{-# OPTIONS --safe #-}
module Issue2728-3 where
foo = Set -- something to cache
postulate B : Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties

open import Cubical.ZCohomology.S1.S1

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
open import Level hiding ( suc ; zero )
open import Algebra
module Gutil {n m : Level} (G : Group n m ) where

open import Data.Unit
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
open import Function
open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
open import Relation.Nullary
open import Data.Empty
open import Data.Product
open import  Relation.Binary.PropositionalEquality hiding ( [_] )

open Group G

import Relation.Binary.Reasoning.Setoid as EqReasoning

gsym = Algebra.Group.sym G
grefl = Algebra.Group.refl G
gtrans = Algebra.Group.trans G

lemma3 : ε ≈ ε ⁻¹
lemma3 = begin
     ε          ≈⟨ gsym (proj₁ inverse _) ⟩
     ε ⁻¹ ∙ ε   ≈⟨ proj₂ identity _ ⟩
     ε ⁻¹
   ∎ where open EqReasoning (Algebra.Group.setoid G)

lemma6 : {f : Carrier } →  ( f ⁻¹ ) ⁻¹  ≈ f
lemma6 {f} = begin
     ( f ⁻¹ ) ⁻¹   ≈⟨ gsym ( proj₁ identity _) ⟩
      ε  ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩
     (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹   ≈⟨ assoc _ _ _ ⟩
     f ∙ ( f ⁻¹  ∙ ( f ⁻¹ ) ⁻¹ )  ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩
     f ∙ ε  ≈⟨ proj₂ identity _ ⟩
     f
   ∎ where open EqReasoning (Algebra.Group.setoid G)

≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g
≡→≈ refl = grefl

---
-- to avoid assoc storm, flatten multiplication according to the template
--

data MP  : Carrier → Set (Level.suc n) where
    am  : (x : Carrier )   →  MP  x
    _o_ : {x y : Carrier } →  MP  x →  MP  y → MP  ( x ∙ y )

mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier
mpf (am x) y = x ∙ y
mpf (m o m₁) y = mpf m ( mpf m₁ y )

mp-flatten : {x : Carrier } → (m : MP x ) → Carrier
mp-flatten  m = mpf m ε

mpl1 : Carrier → {x : Carrier } → MP x → Carrier
mpl1 x (am y) = x ∙ y
mpl1 x (y o y1) = mpl1 ( mpl1 x y ) y1

mpl : {x z : Carrier } → MP x → MP z  → Carrier
mpl (am x)  m = mpl1 x m
mpl (m o m1) m2 = mpl m (m1 o m2)

mp-flattenl : {x : Carrier } → (m : MP x ) → Carrier
mp-flattenl m = mpl m (am ε)

test1 : ( f g : Carrier ) → Carrier
test1 f g = mp-flattenl ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))

test2 : ( f g : Carrier ) → test1 f g ≡  g ⁻¹ ∙ f ⁻¹ ∙ f ∙ g ∙  (f ∙ g) ⁻¹  ∙ ε
test2 f g = _≡_.refl

test3 : ( f g : Carrier ) → Carrier
test3 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))

test4 : ( f g : Carrier ) → test3 f g ≡ g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))
test4 f g = _≡_.refl

∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m
∙-flatten {x} (am x) = gsym (proj₂ identity _)
∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q )
∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ ( ∙-flatten {x ∙ y } (p o q )) ( ∙-flatten {z} r ) where
   mp-cong : {p q r : Carrier} → (P : MP p)  → q ≈ r → mpf P q ≈ mpf P r
   mp-cong (am x) q=r = ∙-cong grefl q=r
   mp-cong (P o P₁) q=r = mp-cong P ( mp-cong P₁ q=r )
   mp-assoc : {p q r : Carrier} → (P : MP p)  → mpf P q ∙ r ≈ mpf P (q ∙ r )
   mp-assoc (am x) = assoc _ _ _
   mp-assoc {p} {q} {r} (P o P₁) = begin
       mpf P (mpf  P₁ q) ∙ r      ≈⟨ mp-assoc P ⟩
       mpf P (mpf P₁ q ∙ r)       ≈⟨ mp-cong P (mp-assoc P₁)  ⟩ mpf P ((mpf  P₁) (q ∙ r))
    ∎ where open EqReasoning (Algebra.Group.setoid G)
   lemma9 : (x y z : Carrier) →  x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε →  x ∙ y ∙ z ≈ mp-flatten ((p o q) o r)
   lemma9 x y z t s = begin
       x ∙ y ∙ z                    ≈⟨ ∙-cong t grefl  ⟩
       mpf p (mpf q ε) ∙ z          ≈⟨ mp-assoc p ⟩
       mpf p (mpf q ε ∙ z)          ≈⟨ mp-cong p (mp-assoc q ) ⟩
       mpf p (mpf q (ε ∙ z))        ≈⟨ mp-cong p (mp-cong q (proj₁ identity _  )) ⟩
       mpf p (mpf q z)              ≈⟨ mp-cong p (mp-cong q s) ⟩
       mpf p (mpf q (mpf r ε))
    ∎ where open EqReasoning (Algebra.Group.setoid G)

grepl : { x y0 y1 z  : Carrier } → x ∙ y0 ≈ y1  → x ∙ ( y0 ∙ z ) ≈ y1 ∙ z
grepl eq = gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )

grm : { x y0 y1 z  : Carrier } → x ∙ y0 ≈ ε  → x ∙ ( y0 ∙ z ) ≈  z
grm eq = gtrans ( gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )) ( proj₁ identity _ )

-- ∙-flattenl : {x : Carrier } → (m : MP x ) → x ≈ mp-flattenl m
-- ∙-flattenl (am x) = gsym (proj₂ identity _)
-- ∙-flattenl (q o am x) with ∙-flattenl q    -- x₁ ∙ x ≈ mpl q (am x o am ε) ,  t : x₁ ≈ mpl q (am ε)
-- ... | t = {!!}
-- ∙-flattenl (q o (x o y )) with ∙-flattenl q
-- ... | t = gtrans (gsym (assoc _ _ _ )) {!!}

lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
lemma5 f g = begin
     g ⁻¹ ∙ f ⁻¹                                     ≈⟨ gsym (proj₂ identity _) ⟩
     g ⁻¹ ∙ f ⁻¹  ∙ ε                                ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )         ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))  ⟩
     g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))))    ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩
     g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))    ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
     g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))                   ≈⟨ gsym (assoc _ _ _) ⟩
     (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε)                  ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
     (f ∙ g) ⁻¹ ∙ ε                                  ≈⟨ proj₂ identity _ ⟩
     (f ∙ g) ⁻¹
     ∎ where open EqReasoning (Algebra.Group.setoid G)

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


text:
{-

Generate univalent reflexive graph characterizations for record types from
characterizations of the field types using reflection.

See end of file for an example.

-}
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Displayed.Record where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Data.Sigma
open import Cubical.Data.List as List
open import Cubical.Data.Unit
open import Cubical.Data.Bool
open import Cubical.Data.Maybe as Maybe

open import Cubical.Displayed.Base
open import Cubical.Displayed.Properties
open import Cubical.Displayed.Prop
open import Cubical.Displayed.Sigma
open import Cubical.Displayed.Unit
open import Cubical.Displayed.Universe
open import Cubical.Displayed.Auto

import Agda.Builtin.Reflection as R
open import Cubical.Reflection.Base
import Cubical.Reflection.RecordEquiv as RE

{-
  `DUAFields`
  A collection of DURG characterizations for fields of a record is described by an element of this inductive
  family. If you just want to see how to use it, have a look at the end of the file first.

  An element of `DUAFields 𝒮-A R _≅R⟨_⟩_ πS 𝒮ᴰ-S πS≅` describes a mapping
  - from a structure `R : A → Type _` and notion of structured equivalence `_≅R⟨_⟩_`,
    which are meant to be defined as parameterized record types,
  - to a DURG `𝒮ᴰ-S`,
    the underlying structure of which will be an iterated Σ-type,
  - via projections `πS` and `πS≅`.

  `𝒮-A`, `R`, and `_≅R⟨_⟩_` are parameters, while `πS`, `𝒮ᴰ-S`, and `πS≅` are indices;
  the user builds up the Σ-type representation of the record using the DUAFields constructors.

  A DUAFields representation is _total_ when the projections `πS` and `πS≅` are equivalences, in which case we
  obtain a DURG on `R` with `_≅R⟨_⟩_` as the notion of structured equivalence---see `𝒮ᴰ-Fields` below.

  When `R`, and `_≅R⟨_⟩_` are defined by record types, we can use reflection to automatically generate proofs
  `πS` and `πS≅` are equivalences---see `𝒮ᴰ-Record` below.

-}
data DUAFields {ℓA ℓ≅A ℓR ℓ≅R} {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
  (R : A → Type ℓR) (_≅R⟨_⟩_ : {a a' : A} → R a → UARel._≅_ 𝒮-A a a' → R a' → Type ℓ≅R)
  : ∀ {ℓS ℓ≅S} {S : A → Type ℓS}
    (πS : ∀ {a} → R a → S a) (𝒮ᴰ-S : DUARel 𝒮-A S ℓ≅S)
    (πS≅ : ∀ {a} {r : R a} {e} {r' : R a} → r ≅R⟨ e ⟩ r' → DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-S (πS r) e (πS r'))
    → Typeω
  where

  -- `fields:`
  -- Base case, no fields yet recorded in `𝒮ᴰ-S`.
  fields: : DUAFields 𝒮-A R _≅R⟨_⟩_ (λ _ → tt) (𝒮ᴰ-Unit 𝒮-A) (λ _ → tt)

  -- `… data[ πF ∣ 𝒮ᴰ-F ∣ πF≅ ]`
  -- Add a new field with a DURG. `πF` should be the name of the field in the structure record `R` and `πF≅`
  -- the name of the corresponding field in the equivalence record `_≅R⟨_⟩_`, while `𝒮ᴰ-F` is a DURG for the
  -- field's type over `𝒮-A`. Data fields that depend on previous fields of the record are not currently
  -- supported.
  _data[_∣_∣_] : ∀ {ℓS ℓ≅S} {S : A → Type ℓS}
    {πS : ∀ {a} → R a → S a} {𝒮ᴰ-S : DUARel 𝒮-A S ℓ≅S}
    {πS≅ : ∀ {a} {r : R a} {e} {r' : R a} → r ≅R⟨ e ⟩ r' → DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-S (πS r) e (πS r')}
    → DUAFields 𝒮-A R _≅R⟨_⟩_ πS 𝒮ᴰ-S πS≅
    → ∀ {ℓF ℓ≅F} {F : A → Type ℓF}
    (πF : ∀ {a} → (r : R a) → F a)
    (𝒮ᴰ-F : DUARel 𝒮-A F ℓ≅F)
    (πF≅ : ∀ {a} {r : R a} {e} {r' : R a} (p : r ≅R⟨ e ⟩ r') → DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-F (πF r) e (πF r'))
    → DUAFields 𝒮-A R _≅R⟨_⟩_ (λ r → πS r , πF r) (𝒮ᴰ-S ×𝒮ᴰ 𝒮ᴰ-F) (λ p → πS≅ p , πF≅ p)

  -- `… prop[ πF ∣ propF ]`
  -- Add a new propositional field. `πF` should be the name of the field in the structure record `R`, while
  -- propF is a proof that this field is a proposition.
  _prop[_∣_] : ∀ {ℓS ℓ≅S} {S : A → Type ℓS}
    {πS : ∀ {a} → R a → S a} {𝒮ᴰ-S : DUARel 𝒮-A S ℓ≅S}
    {πS≅ : ∀ {a} {r : R a} {e} {r' : R a} → r ≅R⟨ e ⟩ r' → DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-S (πS r) e (πS r')}
    → DUAFields 𝒮-A R _≅R⟨_⟩_ πS 𝒮ᴰ-S πS≅
    → ∀ {ℓF} {F : (a : A) → S a → Type ℓF}
    (πF : ∀ {a} → (r : R a) → F a (πS r))
    (propF : ∀ a s → isProp (F a s))
    → DUAFields 𝒮-A R _≅R⟨_⟩_ (λ r → πS r , πF r) (𝒮ᴰ-subtype 𝒮ᴰ-S propF) (λ p → πS≅ p)

module _ {ℓA ℓ≅A} {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {ℓR ℓ≅R} {R : A → Type ℓR} (_≅R⟨_⟩_ : {a a' : A} → R a → UARel._≅_ 𝒮-A a a' → R a' → Type ℓ≅R)
  {ℓS ℓ≅S} {S : A → Type ℓS}
  {πS : ∀ {a} → R a → S a} {𝒮ᴰ-S : DUARel 𝒮-A S ℓ≅S}
  {πS≅ : ∀ {a} {r : R a} {e} {r' : R a} → r ≅R⟨ e ⟩ r' → DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-S (πS r) e (πS r')}
  (fs : DUAFields 𝒮-A R _≅R⟨_⟩_ πS 𝒮ᴰ-S πS≅)
  where

  open UARel 𝒮-A
  open DUARel 𝒮ᴰ-S

  𝒮ᴰ-Fields :
    (e : ∀ a → Iso (R a) (S a))
    (e≅ : ∀ a a' (r : R a) p (r' : R a') → Iso (r ≅R⟨ p ⟩ r') ((e a .Iso.fun r ≅ᴰ⟨ p ⟩ e a' .Iso.fun r')))
    → DUARel 𝒮-A R ℓ≅R
  DUARel._≅ᴰ⟨_⟩_ (𝒮ᴰ-Fields e e≅) r p r' = r ≅R⟨ p ⟩ r'
  DUARel.uaᴰ (𝒮ᴰ-Fields e e≅) r p r' =
    isoToEquiv
      (compIso
        (e≅ _ _ r p r')
        (compIso
          (equivToIso (uaᴰ (e _ .Iso.fun r) p (e _ .Iso.fun r')))
          (invIso (congPathIso λ i → isoToEquiv (e _)))))

module DisplayedRecordMacro where

  -- Extract a name from a term
  findName : R.Term → R.TC R.Name
  findName t =
    Maybe.rec
      (R.typeError (R.strErr "Not a name: " ∷ R.termErr t ∷ []))
      (λ s → s)
      (go t)
    where
    go : R.Term → Maybe (R.TC R.Name)
    go (R.meta x _) = just (R.blockOnMeta x)
    go (R.def name _) = just (R.returnTC name)
    go (R.lam _ (R.abs _ t)) = go t
    go t = nothing

  -- ℓA ℓ≅A ℓR ℓ≅R A 𝒮-A R _≅R⟨_⟩_
  pattern family∷ hole = _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ hole

  -- ℓS ℓ≅S S πS 𝒮ᴰ-S πS≅
  pattern indices∷ hole = _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ _ h∷ hole

  {-
    Takes a reflected DUAFields term as input and collects lists of structure field names and equivalence
    field names. (These are returned in reverse order.
  -}
  parseFields : R.Term → R.TC (List R.Name × List R.Name)
  parseFields (R.con (quote fields:) _) = R.returnTC ([] , [])
  parseFields (R.con (quote _data[_∣_∣_]) (family∷ (indices∷ (fs v∷ ℓF h∷ ℓ≅F h∷ F h∷ πF v∷ 𝒮ᴰ-F v∷ πF≅ v∷ _)))) =
    parseFields fs >>= λ (fs , f≅s) →
    findName πF >>= λ f →
    findName πF≅ >>= λ f≅ →
    R.returnTC (f ∷ fs , f≅ ∷ f≅s)
  parseFields (R.con (quote _prop[_∣_]) (family∷ (indices∷ (fs v∷ ℓF h∷ F h∷ πF v∷ _)))) =
    parseFields fs >>= λ (fs , f≅s) →
    findName πF >>= λ f →
    R.returnTC (f ∷ fs , f≅s)
  parseFields (R.meta x _) = R.blockOnMeta x
  parseFields t = R.typeError (R.strErr "Malformed specification: " ∷ R.termErr t ∷ [])

  {-
    Given a list of record field names (in reverse order), generates a ΣFormat (in the sense of
    Cubical.Reflection.RecordEquiv) associating the record fields with the fields of a left-associated
    iterated Σ-type
  -}
  List→LeftAssoc : List R.Name → RE.ΣFormat
  List→LeftAssoc [] = RE.unit
  List→LeftAssoc (x ∷ xs) = List→LeftAssoc xs RE., RE.leaf x

  module _ {ℓA ℓ≅A} {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
    {ℓR ℓ≅R} {R : A → Type ℓR} (≅R : {a a' : A} → R a → UARel._≅_ 𝒮-A a a' → R a' → Type ℓ≅R)
    {ℓS ℓ≅S} {S : A → Type ℓS}
    {πS : ∀ {a} → R a → S a} {𝒮ᴰ-S : DUARel 𝒮-A S ℓ≅S}
    {πS≅ : ∀ {a} {r : R a} {e} {r' : R a} → ≅R r e r' → DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-S (πS r) e (πS r')}
    where

    {-
      "𝒮ᴰ-Record ... : DUARel 𝒮-A R ℓ≅R"
      Requires that `R` and `_≅R⟨_⟩_` are defined by records and `πS` and `πS≅` are equivalences.
      The proofs of equivalence are generated using Cubical.Reflection.RecordEquiv and then
      `𝒮ᴰ-Fields` is applied.
    -}
    𝒮ᴰ-Record : DUAFields 𝒮-A R ≅R πS 𝒮ᴰ-S πS≅ → R.Term → R.TC Unit
    𝒮ᴰ-Record fs hole =
      R.quoteTC (DUARel 𝒮-A R ℓ≅R) >>= R.checkType hole >>= λ hole →
      R.quoteωTC fs >>= λ `fs` →
      parseFields `fs` >>= λ (fields , ≅fields) →
      R.freshName "fieldsIso" >>= λ fieldsIso →
      R.freshName "≅fieldsIso" >>= λ ≅fieldsIso →
      R.quoteTC R >>= R.normalise >>= λ `R` →
      R.quoteTC {A = {a a' : A} → R a → UARel._≅_ 𝒮-A a a' → R a' → Type ℓ≅R} ≅R >>= R.normalise >>= λ `≅R` →
      findName `R` >>= RE.declareRecordIsoΣ' fieldsIso (List→LeftAssoc fields) >>
      findName `≅R` >>= RE.declareRecordIsoΣ' ≅fieldsIso (List→LeftAssoc ≅fields) >>
      R.unify hole
        (R.def (quote 𝒮ᴰ-Fields)
          (`≅R` v∷ `fs` v∷
            vlam "_" (R.def fieldsIso []) v∷
            vlam "a" (vlam "a'" (vlam "r" (vlam "p" (vlam "r'" (R.def ≅fieldsIso []))))) v∷
            []))

macro
  𝒮ᴰ-Record = DisplayedRecordMacro.𝒮ᴰ-Record

-- Example

private
  module Example where

    record Example (A : Type) : Type where
      no-eta-equality -- works with or without eta equality
      field
        dog : A → A → A
        cat : A → A → A
        mouse : Unit

    open Example

    record ExampleEquiv {A B : Type} (x : Example A) (e : A ≃ B) (y : Example B) : Type where
      no-eta-equality -- works with or without eta equality
      field
        dogEq : ∀ a a' → e .fst (x .dog a a') ≡ y .dog (e .fst a) (e .fst a')
        catEq : ∀ a a' → e .fst (x .cat a a') ≡ y .cat (e .fst a) (e .fst a')

    open ExampleEquiv

    example : DUARel (𝒮-Univ ℓ-zero) Example ℓ-zero
    example =
      𝒮ᴰ-Record (𝒮-Univ ℓ-zero) ExampleEquiv
        (fields:
          data[ dog ∣ autoDUARel _ _ ∣ dogEq ]
          data[ cat ∣ autoDUARel _ _ ∣ catEq ]
          prop[ mouse ∣ (λ _ _ → isPropUnit) ])

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module Pi.Eval where
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Data.List as L hiding (_∷_)
open import Relation.Binary.PropositionalEquality
open import Pi.Syntax
open import Pi.Opsem
open import Pi.NoRepeat

-- Stuck states must be of the form ［ c ∣ v ∣ ☐ ］
Stuck : ∀ {st} → is-stuck st
      → (Σ[ A ∈ 𝕌 ] Σ[ B ∈ 𝕌 ] Σ[ c ∈ A ↔ B ] Σ[ v ∈ ⟦ B ⟧ ] st ≡ ［ c ∣ v ∣ ☐ ］)
Stuck {⟨ unite₊l  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ uniti₊l  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ swap₊    ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ assocl₊  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ assocr₊  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ unite⋆l  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ uniti⋆l  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ swap⋆    ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ assocl⋆  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ assocr⋆  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ dist     ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ factor   ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ absorbr  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ factorzl ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₁))
Stuck {⟨ id↔      ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₂))
Stuck {⟨ c₁ ⨾ c₂  ∣ v       ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₃))
Stuck {⟨ c₁ ⊕ c₂  ∣ inj₁ x  ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₄))
Stuck {⟨ c₁ ⊕ c₂  ∣ inj₂ y  ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₅))
Stuck {⟨ c₁ ⊗ c₂  ∣ (x , y) ∣ κ ⟩} stuck = ⊥-elim (stuck (_ , ↦₆))
Stuck {［ c ∣ v ∣ ☐               ］} stuck = _ , _ , _ , _ , refl
Stuck {［ c ∣ v ∣ ☐⨾ c₂ • κ       ］} stuck = ⊥-elim (stuck (_ , ↦₇))
Stuck {［ c ∣ v ∣ c₁ ⨾☐• κ        ］} stuck = ⊥-elim (stuck (_ , ↦₁₀))
Stuck {［ c ∣ v ∣ ☐⊕ c₂ • κ       ］} stuck = ⊥-elim (stuck (_ , ↦₁₁))
Stuck {［ c ∣ v ∣ c₁ ⊕☐• κ        ］} stuck = ⊥-elim (stuck (_ , ↦₁₂))
Stuck {［ c ∣ v ∣ ☐⊗[ c₂ , y ]• κ ］} stuck = ⊥-elim (stuck (_ , ↦₈))
Stuck {［ c ∣ v ∣ [ c₁ , x ]⊗☐• κ ］} stuck = ⊥-elim (stuck (_ , ↦₉))

-- Auxiliary function for forward evaluator
ev : ∀ {A B κ} → (c : A ↔ B) (v : ⟦ A ⟧) → Σ[ v' ∈ ⟦ B ⟧ ] ⟨ c ∣ v ∣ κ ⟩ ↦* ［ c ∣ v' ∣ κ ］
ev unite₊l (inj₂ v) = v , (↦₁ ∷ ◾)
ev uniti₊l v = inj₂ v , (↦₁ ∷ ◾)
ev swap₊ (inj₁ v) = inj₂ v , (↦₁ ∷ ◾)
ev swap₊ (inj₂ v) = inj₁ v , (↦₁ ∷ ◾)
ev assocl₊ (inj₁ v) = inj₁ (inj₁ v) , (↦₁ ∷ ◾)
ev assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v) , (↦₁ ∷ ◾)
ev assocl₊ (inj₂ (inj₂ v)) = inj₂ v , (↦₁ ∷ ◾)
ev assocr₊ (inj₁ (inj₁ v)) = inj₁ v , (↦₁ ∷ ◾)
ev assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v) , (↦₁ ∷ ◾)
ev assocr₊ (inj₂ v) = inj₂ (inj₂ v) , (↦₁ ∷ ◾)
ev unite⋆l (tt , v) = v , (↦₁ ∷ ◾)
ev uniti⋆l v = (tt , v) , (↦₁ ∷ ◾)
ev swap⋆ (x , y) = (y , x) , (↦₁ ∷ ◾)
ev assocl⋆ (x , (y , z)) = ((x , y) , z) , (↦₁ ∷ ◾)
ev assocr⋆ ((x , y) , z) = (x , (y , z)) , (↦₁ ∷ ◾)
ev dist (inj₁ x , z) = inj₁ (x , z) , (↦₁ ∷ ◾)
ev dist (inj₂ y , z) = inj₂ (y , z) , (↦₁ ∷ ◾)
ev factor (inj₁ (x , z)) = (inj₁ x , z) , (↦₁ ∷ ◾)
ev factor (inj₂ (y , z)) = (inj₂ y , z) , (↦₁ ∷ ◾)
ev id↔ v = v , (↦₂ ∷ ◾)
ev {κ = κ} (c₁ ⨾ c₂) v₁ with ev {κ = ☐⨾ c₂ • κ} c₁ v₁
... | (v₂ , c₁↦*) with ev {κ = c₁ ⨾☐• κ} c₂ v₂
... | (v₃ , c₂↦*) = v₃ , ((↦₃ ∷ c₁↦* ++↦ (↦₇ ∷ ◾)) ++↦ (c₂↦* ++↦ (↦₁₀ ∷ ◾)))
ev {κ = κ} (c₁ ⊕ c₂) (inj₁ x) with ev {κ = ☐⊕ c₂ • κ} c₁ x
... | x' , c₁↦* = inj₁ x' , ↦₄ ∷ c₁↦* ++↦ (↦₁₁ ∷ ◾)
ev {κ = κ} (c₁ ⊕ c₂) (inj₂ y) with ev {κ = c₁ ⊕☐• κ} c₂ y
... | y' , c₂↦* = inj₂ y' , ↦₅ ∷ c₂↦* ++↦ (↦₁₂ ∷ ◾)
ev {κ = κ} (c₁ ⊗ c₂) (x , y) with ev {κ = ☐⊗[ c₂ , y ]• κ} c₁ x
... | x' , c₁↦* with ev {κ = [ c₁ , x' ]⊗☐• κ} c₂ y
... | y' , c₂↦* = (x' , y') , ((↦₆ ∷ c₁↦*) ++↦ ((↦₈ ∷ c₂↦*) ++↦ (↦₉ ∷ ◾)))

-- Forward evaluator for Pi
eval : ∀ {A B} → (c : A ↔ B) → ⟦ A ⟧ → ⟦ B ⟧
eval c v = proj₁ (ev {κ = ☐} c v)

-- Forward evaluator which returns execution trace
evalₜᵣ : ∀ {A B} → (c : A ↔ B) → ⟦ A ⟧ → List State
evalₜᵣ c v = convert (proj₂ (ev {κ = ☐} c v))
  where
    convert : ∀ {st st'} → st ↦* st' → List State
    convert (◾ {st}) = st L.∷ []
    convert (_∷_ {st} r rs) = st L.∷ convert rs

-- Auxiliary function for backward evaluator
evᵣₑᵥ : ∀ {A B κ} → (c : A ↔ B) (v' : ⟦ B ⟧) → Σ[ v ∈ ⟦ A ⟧ ] ［ c ∣ v' ∣ κ ］ ↦ᵣₑᵥ* ⟨ c ∣ v ∣ κ ⟩
evᵣₑᵥ unite₊l v' = inj₂ v' , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ uniti₊l (inj₂ v') = v' , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ swap₊ (inj₁ v') = inj₂ v' , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ swap₊ (inj₂ v') = inj₁ v' , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocl₊ (inj₁ (inj₁ v')) = inj₁ v' , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocl₊ (inj₁ (inj₂ v')) = inj₂ (inj₁ v') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocl₊ (inj₂ v') = inj₂ (inj₂ v') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocr₊ (inj₁ v') = inj₁ (inj₁ v') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocr₊ (inj₂ (inj₁ v')) = inj₁ (inj₂ v') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocr₊ (inj₂ (inj₂ v')) = inj₂ v' , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ unite⋆l v' = (tt , v') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ uniti⋆l (tt , v') = v' , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ swap⋆ (x' , y') = (y' , x') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocl⋆ ((x' , y') , z') = (x' , (y' , z')) , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ assocr⋆ (x' , (y' , z')) = ((x' , y') , z') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ dist (inj₁ (x' , z')) = (inj₁ x' , z') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ dist (inj₂ (y' , z')) = (inj₂ y' , z') , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ factor (inj₁ x' , z') = (inj₁ (x' , z')) , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ factor (inj₂ y' , z') = (inj₂ (y' , z')) , ((↦₁ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ id↔ v' = v' , ((↦₂ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ {κ = κ} (c₁ ⨾ c₂) v₃ with evᵣₑᵥ {κ = c₁ ⨾☐• κ} c₂ v₃
... | (v₂ , c₂↦ᵣₑᵥ*) with evᵣₑᵥ {κ = ☐⨾ c₂ • κ} c₁ v₂
... | (v₁ , c₁↦ᵣₑᵥ*) = v₁ , ((↦₁₀ ᵣₑᵥ) ∷ c₂↦ᵣₑᵥ*) ++↦ᵣₑᵥ ((↦₇ ᵣₑᵥ) ∷ (c₁↦ᵣₑᵥ* ++↦ᵣₑᵥ ((↦₃ ᵣₑᵥ) ∷ ◾)))
evᵣₑᵥ {κ = κ} (c₁ ⊕ c₂) (inj₁ v') with evᵣₑᵥ {κ = ☐⊕ c₂ • κ} c₁ v'
... | v , c₁↦ᵣₑᵥ* = inj₁ v , ((↦₁₁ ᵣₑᵥ) ∷ c₁↦ᵣₑᵥ*) ++↦ᵣₑᵥ ((↦₄ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ {κ = κ} (c₁ ⊕ c₂) (inj₂ v') with evᵣₑᵥ {κ = c₁ ⊕☐• κ} c₂ v'
... | v , c₂↦ᵣₑᵥ* = inj₂ v , ((↦₁₂ ᵣₑᵥ) ∷ c₂↦ᵣₑᵥ*) ++↦ᵣₑᵥ ((↦₅ ᵣₑᵥ) ∷ ◾)
evᵣₑᵥ {κ = κ} (c₁ ⊗ c₂) (x' , y') with evᵣₑᵥ {κ = [ c₁ , x' ]⊗☐• κ} c₂ y'
... | y , c₂↦ᵣₑᵥ* with evᵣₑᵥ {κ = ☐⊗[ c₂ , y ]• κ} c₁ x'
... | x , c₁↦ᵣₑᵥ* = (x , y) , ((↦₉ ᵣₑᵥ) ∷ c₂↦ᵣₑᵥ*) ++↦ᵣₑᵥ (((↦₈ ᵣₑᵥ) ∷ c₁↦ᵣₑᵥ*) ++↦ᵣₑᵥ ((↦₆ ᵣₑᵥ) ∷ ◾))

-- Backward evaluator for Pi
evalᵣₑᵥ : ∀ {A B} → (c : A ↔ B) → ⟦ B ⟧ → ⟦ A ⟧
evalᵣₑᵥ c v' = proj₁ (evᵣₑᵥ {κ = ☐} c v')


text:
{-# OPTIONS --no-termination-check #-}

module Pi where

open import Data.Empty
open import Data.Unit
open import Data.Sum hiding (map)
open import Data.Product hiding (map)

open import Relation.Binary.PropositionalEquality hiding (sym; [_])

infixr 30 _⟷_
infixr 30 _⟺_
infixr 20 _◎_

------------------------------------------------------------------------------
-- A universe of our value types

data B : Set where
  ZERO  : B
  ONE   : B
  PLUS  : B → B → B
  TIMES : B → B → B

⟦_⟧ : B → Set
⟦ ZERO ⟧         = ⊥
⟦ ONE ⟧          = ⊤
⟦ PLUS b1 b2 ⟧   = ⟦ b1 ⟧ ⊎ ⟦ b2 ⟧
⟦ TIMES b1 b2 ⟧  = ⟦ b1 ⟧ × ⟦ b2 ⟧

------------------------------------------------------------------------------
-- Primitive isomorphisms

data _⟷_ : B → B → Set where
  -- (+,0) commutative monoid
  unite₊  : { b : B } → PLUS ZERO b ⟷ b
  uniti₊  : { b : B } → b ⟷ PLUS ZERO b
  swap₊   : { b₁ b₂ : B } → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  -- (*,1) commutative monoid
  unite⋆  : { b : B } → TIMES ONE b ⟷ b
  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
  swap⋆   : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  -- * distributes over +
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
  -- id
  id⟷   : { b : B } → b ⟷ b

adjointP : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
adjointP unite₊    = uniti₊
adjointP uniti₊    = unite₊
adjointP swap₊     = swap₊
adjointP assocl₊   = assocr₊
adjointP assocr₊   = assocl₊
adjointP unite⋆    = uniti⋆
adjointP uniti⋆    = unite⋆
adjointP swap⋆     = swap⋆
adjointP assocl⋆   = assocr⋆
adjointP assocr⋆   = assocl⋆
adjointP dist      = factor
adjointP factor    = dist
adjointP id⟷      = id⟷

evalP : { b₁ b₂ : B } → (b₁ ⟷ b₂) → ⟦ b₁ ⟧ → ⟦ b₂ ⟧
evalP unite₊ (inj₁ ())
evalP unite₊ (inj₂ v) = v
evalP uniti₊ v = inj₂ v
evalP swap₊ (inj₁ v) = inj₂ v
evalP swap₊ (inj₂ v) = inj₁ v
evalP assocl₊ (inj₁ v) = inj₁ (inj₁ v)
evalP assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
evalP assocl₊ (inj₂ (inj₂ v)) = inj₂ v
evalP assocr₊ (inj₁ (inj₁ v)) = inj₁ v
evalP assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
evalP assocr₊ (inj₂ v) = inj₂ (inj₂ v)
evalP unite⋆ (tt , v) = v
evalP uniti⋆ v = (tt , v)
evalP swap⋆ (v₁ , v₂) = (v₂ , v₁)
evalP assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
evalP assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
evalP dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
evalP dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
evalP factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
evalP factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
evalP id⟷ v = v

-- Backwards evaluator

bevalP : { b₁ b₂ : B } → (b₁ ⟷ b₂) → ⟦ b₂ ⟧ → ⟦ b₁ ⟧
bevalP c v = evalP (adjointP c) v

------------------------------------------------------------------------------
-- Closure combinators

data _⟺_ : B → B → Set where
  iso    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₁ ⟺ b₂)
  sym    : { b₁ b₂ : B } → (b₁ ⟺ b₂) → (b₂ ⟺ b₁)
  _◎_    : { b₁ b₂ b₃ : B } → (b₁ ⟺ b₂) → (b₂ ⟺ b₃) → (b₁ ⟺ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟺ b₃) → (b₂ ⟺ b₄) → (PLUS b₁ b₂ ⟺ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟺ b₃) → (b₂ ⟺ b₄) → (TIMES b₁ b₂ ⟺ TIMES b₃ b₄)

--

adjoint : { b₁ b₂ : B } → (b₁ ⟺ b₂) → (b₂ ⟺ b₁)
adjoint (iso c) = iso (adjointP c)
adjoint (sym c)   = c
adjoint (c₁ ◎ c₂) = adjoint c₂ ◎ adjoint c₁
adjoint (c₁ ⊕ c₂) = adjoint c₁ ⊕ adjoint c₂
adjoint (c₁ ⊗ c₂) = adjoint c₁ ⊗ adjoint c₂

--

-- (Context a b c d) represents a combinator (c <-> d) with a hole
-- requiring something of type (a <-> b). When we use these contexts,
-- it is always the case that the (c <-> a) part of the computation
-- has ALREADY been done and that we are about to evaluate (a <-> b)
-- using a given 'a'. The continuation takes the output 'b' and
-- produces a 'd'.

data Context : B → B → B → B → Set where
  emptyC : {a b : B} → Context a b a b
  seqC₁ : {a b c i o : B} → (b ⟺ c) → Context a c i o → Context a b i o
  seqC₂ : {a b c i o : B} → (a ⟺ b) → Context a c i o → Context b c i o
  leftC : {a b c d i o : B} →
          (c ⟺ d) → Context (PLUS a c) (PLUS b d) i o → Context a b i o
  rightC : {a b c d i o : B} →
           (a ⟺ b) → Context (PLUS a c) (PLUS b d) i o → Context c d i o
  -- the (i <-> a) part of the computation is completely done; so we must store
  -- the value of type [[ c ]] as part of the context
  fstC : {a b c d i o : B} →
         ⟦ c ⟧ → (c ⟺ d) → Context (TIMES a c) (TIMES b d) i o → Context a b i o
  -- the (i <-> c) part of the computation and the (a <-> b) part of
  -- the computation are completely done; so we must store the value
  -- of type [[ b ]] as part of the context
  sndC : {a b c d i o : B} →
         (a ⟺ b) → ⟦ b ⟧ → Context (TIMES a c) (TIMES b d) i o → Context c d i o

-- Evaluation

mutual

  -- The (c <-> a) part of the computation has been done.
  -- We have an 'a' and we are about to do the (a <-> b) computation.
  -- We get a 'b' and examine the context to get the 'd'
  eval_c : { a b c d : B } → (a ⟺ b) → ⟦ a ⟧ → Context a b c d → ⟦ d ⟧
  eval_c (iso f) v C = eval_k (iso f) (evalP f v) C
  eval_c (sym c) v C = eval_c (adjoint c) v C
  eval_c (f ◎ g) v C = eval_c f v (seqC₁ g C)
  eval_c (f ⊕ g) (inj₁ v) C = eval_c f v (leftC g C)
  eval_c (f ⊕ g) (inj₂ v) C = eval_c g v (rightC f C)
  eval_c (f ⊗ g) (v₁ , v₂) C = eval_c f v₁ (fstC v₂ g C)

  -- The (c <-> a) part of the computation has been done.
  -- The (a <-> b) part of the computation has been done.
  -- We need to examine the context to get the 'd'.
  -- We rebuild the combinator on the way out.
  eval_k : { a b c d : B } → (a ⟺ b) → ⟦ b ⟧ → Context a b c d → ⟦ d ⟧
  eval_k f v emptyC = v
  eval_k f v (seqC₁ g C) = eval_c g v (seqC₂ f C)
  eval_k g v (seqC₂ f C) = eval_k (f ◎ g) v C
  eval_k f v (leftC g C) = eval_k (f ⊕ g) (inj₁ v) C
  eval_k g v (rightC f C) = eval_k (f ⊕ g) (inj₂ v) C
  eval_k f v₁ (fstC v₂ g C) = eval_c g v₂ (sndC f v₁ C)
  eval_k g v₂ (sndC f v₁ C) = eval_k (f ⊗ g) (v₁ , v₂) C

-- Backwards evaluator

mutual

  -- The (d <-> b) part of the computation has been done.
  -- We have a 'b' and we are about to do the (a <-> b) computation backwards.
  -- We get an 'a' and examine the context to get the 'c'
  beval_c : { a b c d : B } → (a ⟺ b) → ⟦ b ⟧ → Context a b c d → ⟦ c ⟧
  beval_c (iso f) v C = beval_k (iso f) (bevalP f v) C
  beval_c (sym c) v C = beval_c (adjoint c) v C
  beval_c (f ◎ g) v C = beval_c g v (seqC₂ f C)
  beval_c (f ⊕ g) (inj₁ v) C = beval_c f v (leftC g C)
  beval_c (f ⊕ g) (inj₂ v) C = beval_c g v (rightC f C)
  beval_c (f ⊗ g) (v₁ , v₂) C = beval_c g v₂ (sndC f v₁ C)

  -- The (d <-> b) part of the computation has been done.
  -- The (a <-> b) backwards computation has been done.
  -- We have an 'a' and examine the context to get the 'c'
  beval_k : { a b c d : B } → (a ⟺ b) → ⟦ a ⟧ → Context a b c d → ⟦ c ⟧
  beval_k f v emptyC = v
  beval_k g v (seqC₂ f C) = beval_c f v (seqC₁ g C)
  beval_k f v (seqC₁ g C) = beval_k (f ◎ g) v C
  beval_k f v (leftC g C) = beval_k (f ⊕ g) (inj₁ v) C
  beval_k g v (rightC f C) = beval_k (f ⊕ g) (inj₂ v) C
  beval_k g v₂ (sndC f v₁ C) = beval_c f v₁ (fstC v₂ g C)
  beval_k f v₁ (fstC v₂ g C) = beval_k (f ⊗ g) (v₁ , v₂) C

------------------------------------------------------------------------------
-- Proposition 'Reversible'

-- eval_c : { a b c d : B } → (a ⟺ b) → ⟦ a ⟧ → Context a b c d → ⟦ d ⟧
-- eval_k : { a b c d : B } → (a ⟺ b) → ⟦ b ⟧ → Context a b c d → ⟦ d ⟧
-- beval_c : { a b c d : B } → (a ⟺ b) → ⟦ b ⟧ → Context a b c d → ⟦ c ⟧
-- beval_k : { a b c d : B } → (a ⟺ b) → ⟦ a ⟧ → Context a b c d → ⟦ c ⟧

-- Prop. 2.2
{-
logical-reversibility : {a b : B} {f : a ⟺ b} {va : ⟦ a ⟧} {vb : ⟦ b ⟧} →
  eval_c f va emptyC ≡ eval_k f vb emptyC →
  eval_c (adjoint f) vb emptyC ≡ eval_k (adjoint f) va emptyC
logical-reversibility = λ fwd≡bwd → {!!}
-}
------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- {-# OPTIONS -v scope:20 #-}

module _ (X : Set) where

postulate
  X₁ X₂ : Set

data D : Set where
  d : D

module Q (x : D) where
    module M1 (z : X₁) where
      g = x
    module M2 (y : D) (z : X₂) where
      h = y
      open M1 public

-- module Qd = Q d

-- This fails to apply g to d!
module QM2d = Q.M2 d d

module QM2p (x : D) = Q.M2 x x

test-h : X₂ → D
test-h = QM2d.h

test-g₁ : X₁ → D
test-g₁ = QM2d.g

test-g₂ : D → X₁ → D
test-g₂ = QM2p.g

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

postulate
  Lift : Nat → Set
  mkLift : ∀ n → Lift n

module TS (T : Nat) where
  module Lifted (lift : Lift T) where
    postulate f : Nat

record Bla (T : Nat) : Set₁ where

  module TST = TS T
  module LT = TST.Lifted (mkLift T)

  Z : Nat
  Z = LT.f

postulate
  A : Set

module C (X : Set) where
  postulate cA : X

module C′  = C
module C′A = C′ A

dA' : A → A
dA' x = C′A.cA

postulate
  B : Set

module TermSubst (X : Set) where
  module Lifted (Y : Set) where
    f : Set
    f = Y

record TermLemmas (Z : Set) : Set₁ where
  module TZ  = TermSubst A
  module TZL = TZ.Lifted B
  foo : Set
  foo = TZL.f
  field Y : Set

module NatCore where
  module NatT (X Y : Set) where
    Z : Set
    Z = X → Y

module NatTrans (Y : Set) where
  open NatCore public

module NT = NatTrans

foo : Set → Set
foo X = Eta.Z
  module Local where
    module Eta = NT.NatT X X