text:
open import Nat
open import Prelude

module Hazelnut-core where
  -- types
  data τ̇ : Set where
    num  : τ̇
    <||> : τ̇
    _==>_ : τ̇ → τ̇ → τ̇

  -- expressions, prefixed with a · to distinguish name clashes with agda
  -- built-ins
  data ė : Set where
    _·:_  : ė → τ̇ → ė
    X     : Nat → ė
    ·λ    : Nat → ė → ė
    N     : Nat → ė
    _·+_  : ė → ė → ė
    <||>  : ė
    <|_|> : ė → ė
    _∘_   : ė → ė → ė

  ---- contexts and some operations on them

  -- variables are named with naturals in ė. therefore we represent
  -- contexts as functions from names for variables (nats) to possible
  -- bindings.
  ·ctx : Set
  ·ctx = Nat → Maybe τ̇ -- todo: (Σ[ n : Nat ] (y : Nat) → y ∈ Γ → x > y)?

  -- convenient shorthand for the (unique up to fun. ext.) empty context
  ∅ : ·ctx
  ∅ _ = None

  -- add a new binding to the context, clobbering anything that might have
  -- been there before.
  _,,_ : ·ctx → (Nat × τ̇) → ·ctx
  (Γ ,, (x , t)) y with natEQ x y
  (Γ ,, (x , t)) .x | Inl refl = Some t
  (Γ ,, (x , t)) y  | Inr neq  = Γ y

  -- membership, or presence, in a context
    -- todo: not sure if this should take a pair
  _∈_ : (p : Nat × τ̇) → (Γ : ·ctx) → Set
  (x , t) ∈ Γ = (Γ x) == Some t

  -- apartness for contexts, so that we can follow barendregt's convention
  _#_ : (n : Nat) → (Γ : ·ctx) → Set
  x # Γ = (Γ x) == None

  -- without: remove a variable from a context
  _/_ : ·ctx → Nat → ·ctx
  (Γ / x) y with natEQ x y
  (Γ / x) .x | Inl refl = None
  (Γ / x) y  | Inr neq  = Γ y

  -- the type compatability judgement
  data _~_ : (t1 : τ̇) → (t2 : τ̇) → Set where
    TCRefl : {t : τ̇} → t ~ t
    TCHole1 : {t : τ̇} → t ~ <||>
    TCHole2 : {t : τ̇} → <||> ~ t
    TCArr : {t1 t2 t1' t2' : τ̇} →
               t1 ~ t1' →
               t2 ~ t2' →
               (t1 ==> t2) ~ (t1' ==> t2')

  -- type incompatability. rather than enumerate the types which aren't
  -- compatible, we encode this judgement immediately as the complement of
  -- compatability. this simplifies a few proofs later.
  _~̸_ : τ̇ → τ̇ → Set
  t1 ~̸ t2 = (t1 ~ t2) → ⊥

  -- bidirectional type checking judgements for ė
  mutual
    -- synthesis
    data _⊢_=>_ : (Γ : ·ctx) → (e : ė) → (t : τ̇) → Set where
      SAsc    : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 Γ ⊢ e <= t →
                 Γ ⊢ (e ·: t) => t
      SVar    : {Γ : ·ctx} {t : τ̇} {n : Nat} →
                 (n , t) ∈ Γ →
                 Γ ⊢ X n => t
      SAp     : {Γ : ·ctx} {e1 e2 : ė} {t t2 : τ̇} →
                 Γ ⊢ e1 => (t2 ==> t) →
                 Γ ⊢ e2 <= t2 →
                 Γ ⊢ (e1 ∘ e2) => t
      SNum    :  {Γ : ·ctx} {n : Nat} →
                 Γ ⊢ N n => num
      SPlus   : {Γ : ·ctx} {e1 e2 : ė}  →
                 Γ ⊢ e1 <= num →
                 Γ ⊢ e2 <= num →
                 Γ ⊢ (e1 ·+ e2) => num
      SEHole  : {Γ : ·ctx} → Γ ⊢ <||> => <||>
      SFHole  : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 Γ ⊢ e => t →
                 Γ ⊢ <| e |> => <||>
      SApHole : {Γ : ·ctx} {e1 e2 : ė} →
                 Γ ⊢ e1 => <||> →
                 Γ ⊢ e2 <= <||> →
                 Γ ⊢ (e1 ∘ e2) => <||>

    -- analysis
    data _⊢_<=_ : (Γ : ·ctx) → (e : ė) → (t : τ̇) → Set where
      ASubsume : {Γ : ·ctx} {e : ė} {t t' : τ̇} →
                 Γ ⊢ e => t' →
                 t ~ t' →
                 Γ ⊢ e <= t
      ALam : {Γ : ·ctx} {e : ė} {t1 t2 : τ̇} {n : Nat} →
                 n # Γ →
                 (Γ ,, (n , t1)) ⊢ e <= t2 →
                 Γ ⊢ (·λ n e) <= (t1 ==> t2)

  ----- a couple of exmaples to demonstrate how the encoding above works

  -- the function (λx. x + 0) where x is named "0".
  add0 : ė
  add0 = ·λ 0 (X 0 ·+ N 0)

  -- this is the derivation that fn has type num ==> num
  ex1 : ∅ ⊢ ·λ 0 (X 0 ·+ N 0) <= (num ==> num)
  ex1 = ALam refl
         (ASubsume
          (SPlus (ASubsume (SVar refl) TCRefl) (ASubsume SNum TCRefl))
          TCRefl)

  -- the derivation that when applied to the numeric argument 10 add0
  -- produces a num.
  ex2 : ∅ ⊢ (add0 ·: (num ==> num)) ∘ (N 10) => num
  ex2 = SAp (SAsc ex1) (ASubsume SNum TCRefl)

  -- the slightly longer derivation that argues that add0 applied to a
  -- variable that's known to be a num produces a num
  ex2b : (∅ ,, (1 , num)) ⊢ (add0 ·: (num ==> num)) ∘ (X 1) => num
  ex2b = SAp (SAsc
                (ALam refl
                 (ASubsume
                  (SPlus (ASubsume (SVar refl) TCRefl) (ASubsume SNum TCRefl))
                  TCRefl)))
              (ASubsume (SVar refl) TCRefl)

  -- eta-expanding addition to curry it gets num → num → num
  ex3 : ∅ ⊢ ·λ 0 ( (·λ 1 (X 0 ·+ X 1)) ·: (num ==> num)  )
               <= (num ==> (num ==> num))
  ex3 = ALam refl (ASubsume (SAsc (ALam refl
                                    (ASubsume
                                      (SPlus (ASubsume (SVar refl) TCRefl)
                                             (ASubsume (SVar refl) TCRefl))
                                          TCRefl))) TCRefl)

  ----- some theorems about the rules and judgement presented so far.

  -- thrm: a variable is apart from any context from which it is removed
  aar : (Γ : ·ctx) (x : Nat) → x # (Γ / x)
  aar Γ x with natEQ x x
  aar Γ x | Inl refl = refl
  aar Γ x | Inr x≠x  = abort (x≠x refl)

  -- contexts give at most one binding for each variable
  ctxunicity : {Γ : ·ctx} {n : Nat} {t t' : τ̇} →
               (n , t) ∈ Γ →
               (n , t') ∈ Γ →
               t == t'
  ctxunicity {n = n} p q with natEQ n n
  ctxunicity p q | Inl refl = someinj (! p · q)
  ctxunicity _ _ | Inr x≠x = abort (x≠x refl)

  -- type compatablity is symmetric
  ~sym : {t1 t2 : τ̇} → t1 ~ t2 → t2 ~ t1
  ~sym TCRefl = TCRefl
  ~sym TCHole1 = TCHole2
  ~sym TCHole2 = TCHole1
  ~sym (TCArr p1 p2) = TCArr (~sym p1) (~sym p2)

  -- if the domain or codomain of a pair of arrows isn't compatable, the
  -- whole arrow isn't compatible.
  lemarr1 : {t1 t2 t3 t4 : τ̇} → (t1 ~ t3 → ⊥) → (t1 ==> t2) ~ (t3 ==> t4)  → ⊥
  lemarr1 v TCRefl = v TCRefl
  lemarr1 v (TCArr p _) = v p

  lemarr2 : {t1 t2 t3 t4 : τ̇} → (t2 ~ t4 → ⊥) → (t1 ==> t2) ~ (t3 ==> t4) →  ⊥
  lemarr2 v TCRefl = v TCRefl
  lemarr2 v (TCArr _ p) = v p

  --  every pair of types is either compatable or not compatable
  ~dec : (t1 t2 : τ̇) → ((t1 ~ t2) + (t1 ~̸ t2))
    -- this takes care of all hole cases, so we don't consider them below
  ~dec _ <||> = Inl TCHole1
  ~dec <||> _ = Inl TCHole2
    -- num cases
  ~dec num num = Inl TCRefl
  ~dec num (t2 ==> t3) = Inr (λ ())
    -- arrow cases
  ~dec (t1 ==> t2) num = Inr (λ ())
  ~dec (t1 ==> t2) (t3 ==> t4) with ~dec t1 t3 | ~dec t2 t4
  ... | Inl x | Inl y = Inl (TCArr x y)
  ... | Inl _ | Inr y = Inr (lemarr2 y)
  ... | Inr x | _     = Inr (lemarr1 x)

  -- theorem: no pair of types is both compatable and not compatable. this
  -- is immediate from our encoding of the ~̸ judgement in the formalism
  -- here; in the exact mathematics presented in the paper, this would
  -- require induction to relate the two judgements.
  ~apart : {t1 t2 : τ̇} → (t1 ~̸ t2) → (t1 ~ t2) → ⊥
  ~apart v p = v p

  -- synthesis only produces equal types. note that there is no need for an
  -- analagous theorem for analytic positions because we think of
  -- the type as an input
  synthunicity : {Γ : ·ctx} {e : ė} {t t' : τ̇} →
                  (Γ ⊢ e => t)
                → (Γ ⊢ e => t')
                → t == t'
  synthunicity (SAsc _) (SAsc _) = refl
  synthunicity {Γ = G} (SVar in1) (SVar in2) = ctxunicity {Γ = G} in1 in2
  synthunicity (SAp D1 _) (SAp D2 _) with synthunicity D1 D2
  ... | refl = refl
  synthunicity (SAp D1 _) (SApHole D2 _) with synthunicity D1 D2
  ... | ()
  synthunicity SNum SNum = refl
  synthunicity (SPlus _ _ ) (SPlus _ _ ) = refl
  synthunicity SEHole SEHole = refl
  synthunicity (SFHole _) (SFHole _) = refl
  synthunicity (SApHole D1 _) (SAp D2 _) with synthunicity D1 D2
  ... | ()
  synthunicity (SApHole _ _) (SApHole _ _) = refl

  ----- the zippered form of the forms above and the rules for actions on them

  -- those types without holes anywhere
  tcomplete : τ̇ → Set
  tcomplete num         = ⊤
  tcomplete <||>        = ⊥
  tcomplete (t1 ==> t2) = (tcomplete t1) × (tcomplete t2)

  -- similarly to the complete types, the complete expressions
  ecomplete : ė → Set
  ecomplete (e1 ·: t)  = ecomplete e1 × tcomplete t
  ecomplete (X _)      = ⊤
  ecomplete (·λ _ e1)  = ecomplete e1
  ecomplete (N x)      = ⊤
  ecomplete (e1 ·+ e2) = ecomplete e1 × ecomplete e2
  ecomplete <||>       = ⊥
  ecomplete <| e1 |>   = ⊥
  ecomplete (e1 ∘ e2)  = ecomplete e1 × ecomplete e2

  -- zippered form of types
  data τ̂ : Set where
    ▹_◃  : τ̇ → τ̂
    _==>₁_ : τ̂ → τ̇ → τ̂
    _==>₂_ : τ̇ → τ̂ → τ̂

  -- zippered form of expressions
  data ê : Set where
    ▹_◃   : ė → ê
    _·:₁_ : ê → τ̇ → ê
    _·:₂_ : ė → τ̂ → ê
    ·λ    : Nat → ê → ê
    _∘₁_  : ê → ė → ê
    _∘₂_  : ė → ê → ê
    _·+₁_ : ê → ė → ê
    _·+₂_ : ė → ê → ê
    <|_|> : ê → ê

  --focus erasure for types
  _◆t : τ̂ → τ̇
  ▹ t ◃ ◆t =  t
  (t1 ==>₁ t2) ◆t = (t1 ◆t) ==> t2
  (t1 ==>₂ t2) ◆t = t1 ==> (t2 ◆t)

  --focus erasure for expressions
  _◆e : ê → ė
  ▹ x ◃ ◆e       = x
  (e ·:₁ t) ◆e   = (e ◆e) ·: t
  (e ·:₂ t) ◆e   = e      ·: (t ◆t)
  ·λ x e ◆e      = ·λ x (e ◆e)
  (e1 ∘₁ e2) ◆e  = (e1 ◆e) ∘ e2
  (e1 ∘₂ e2) ◆e  = e1      ∘ (e2 ◆e)
  (e1 ·+₁ e2) ◆e = (e1 ◆e) ·+ e2
  (e1 ·+₂ e2) ◆e = e1      ·+ (e2 ◆e)
  <| e |> ◆e     = <| e ◆e |>

  -- the three grammars that define actions
  data direction : Set where
    firstChild : direction
    parent : direction
    nextSib : direction
    prevSib : direction

  data shape : Set where
    arrow : shape
    num   : shape
    asc   : shape
    var   : Nat → shape
    lam   : Nat → shape
    ap    : shape
    arg   : shape
    numlit : Nat → shape
    plus  : shape

  data action : Set where
    move : direction → action
    del : action
    construct : shape → action
    finish : action

  -- type movement
  data _+_+>_ : (t : τ̂) → (α : action) → (t' : τ̂) → Set where
    TMFirstChild : {t1 t2 : τ̇} →
               ▹ t1 ==> t2 ◃ + move firstChild +> (▹ t1 ◃ ==>₁ t2)
    TMParent1 : {t1 t2 : τ̇} →
               (▹ t1 ◃ ==>₁ t2) + move parent +> ▹ t1 ==> t2 ◃
    TMParent2 : {t1 t2 : τ̇} →
               (t1 ==>₂ ▹ t2 ◃) + move parent +> ▹ t1 ==> t2 ◃
    TMNextSib : {t1 t2 : τ̇} →
               (▹ t1 ◃ ==>₁ t2) + move nextSib +> (t1 ==>₂ ▹ t2 ◃)
    TMPrevSib : {t1 t2 : τ̇} →
               (t1 ==>₂ ▹ t2 ◃) + move prevSib +> (▹ t1 ◃ ==>₁ t2)
    TMDel     : {t : τ̇} →
                (▹ t ◃) + del +> (▹ <||> ◃)
    TMConArrow  : {t : τ̇} →
                (▹ t ◃) + construct arrow +> (t ==>₂ ▹ <||> ◃)
    TMConNum  : (▹ <||> ◃) + construct num +> (▹ num ◃)
    TMZip1 : {t1 t1' : τ̂} {t2 : τ̇} {α : action} →
                (t1 + α +> t1') →
                ((t1 ==>₁ t2) + α +> (t1' ==>₁ t2))
    TMZip2 : {t2 t2' : τ̂} {t1 : τ̇} {α : action} →
                (t2 + α +> t2') →
                ((t1 ==>₂ t2) + α +> (t1 ==>₂ t2'))

  -- expression movement
  -- todo: want this action to be direction, since they're all move?
  data _+_+>e_ : (e : ê) → (α : action) → (e' : ê) → Set where
    -- rules for ascriptions
    EMAscFirstChild : {e : ė} {t : τ̇} →
              (▹ e ·: t ◃) + move firstChild +>e (▹ e ◃ ·:₁ t)
    EMAscParent1 : {e : ė} {t : τ̇} →
              (▹ e ◃ ·:₁ t) + move parent +>e (▹ e ·: t ◃)
    EMAscParent2 : {e : ė} {t : τ̇} →
              (e ·:₂ ▹ t ◃) + move parent +>e (▹ e ·: t ◃)
    EMAscNextSib : {e : ė} {t : τ̇} →
              (▹ e ◃ ·:₁ t) + move nextSib +>e (e ·:₂ ▹ t ◃)
    EMAscPrevSib : {e : ė} {t : τ̇} →
              (e ·:₂ ▹ t ◃) + move prevSib +>e (▹ e ◃ ·:₁ t)
    -- rules for lambdas
    EMLamFirstChild : {e : ė} {x : Nat} →
              ▹ (·λ x e) ◃ + move firstChild +>e ·λ x (▹ e ◃)
    EMLamParent : {e : ė} {x : Nat} →
               ·λ x (▹ e ◃) + move parent +>e ▹ (·λ x e) ◃
    -- rules for 2-ary constructors
    EMPlusFirstChild : {e1 e2 : ė} →
               (▹ e1 ·+ e2 ◃) + move firstChild +>e (▹ e1 ◃ ·+₁ e2)
    EMPlusParent1 : {e1 e2 : ė} →
               (▹ e1 ◃ ·+₁ e2) + move parent +>e (▹ e1 ·+ e2 ◃)
    EMPlusParent2 : {e1 e2 : ė} →
               (e1 ·+₂ ▹ e2 ◃) + move parent +>e (▹ e1 ·+ e2 ◃)
    EMPlusNextSib : {e1 e2 : ė} →
               (▹ e1 ◃ ·+₁ e2) + move nextSib +>e (e1 ·+₂ ▹ e2 ◃)
    EMPlusPrevSib : {e1 e2 : ė} →
               (e1 ·+₂ ▹ e2 ◃) + move prevSib +>e (▹ e1 ◃ ·+₁ e2)

    EMApFirstChild : {e1 e2 : ė} →
               (▹ e1 ∘ e2 ◃) + move firstChild +>e (▹ e1 ◃ ∘₁ e2)
    EMApParent1 : {e1 e2 : ė} →
               (▹ e1 ◃ ∘₁ e2) + move parent +>e (▹ e1 ∘ e2 ◃)
    EMApParent2 : {e1 e2 : ė} →
               (e1 ∘₂ ▹ e2 ◃) + move parent +>e (▹ e1 ∘ e2 ◃)
    EMApNextSib : {e1 e2 : ė} →
               (▹ e1 ◃ ∘₁ e2) + move nextSib +>e (e1 ∘₂ ▹ e2 ◃)
    EMApPrevSib : {e1 e2 : ė} →
               (e1 ∘₂ ▹ e2 ◃) + move prevSib +>e (▹ e1 ◃ ∘₁ e2)

    -- rules for non-empty holes
    EMFHoleFirstChild : {e : ė} →
               (▹ <| e |> ◃) + move firstChild +>e <| ▹ e ◃ |>
    EMFHoleParent : {e : ė} →
                <| ▹ e ◃ |> + move parent +>e (▹ <| e |> ◃)

  mutual
  -- synthetic action expressions
    data _⊢_=>_~_~>_=>_ : (Γ : ·ctx) → (e1 : ê) → (t1 : τ̇)
                        → (α : action) → (e2 : ê) → (t2 : τ̇) → Set where
      SAMove : {δ : direction} {e e' : ê} {Γ : ·ctx} {t : τ̇} →
                (e + move δ +>e e') →
                Γ ⊢ e => t ~ move δ ~> e' => t
      SADel : {Γ : ·ctx} {e : ė} {t : τ̇} →
                Γ ⊢ ▹ e ◃ => t ~ del ~> ▹ <||> ◃ => <||>
      SAConAsc : {Γ : ·ctx} {e : ė} {t : τ̇} →
                Γ ⊢ ▹ e ◃ => t ~ construct asc ~> (e ·:₂ ▹ t ◃ ) => t
      SAConVar : {Γ : ·ctx} {x : Nat} {t : τ̇} →
                (p : (x , t) ∈ Γ) → -- todo: is this right?
                Γ ⊢ ▹ <||> ◃ => <||> ~ construct (var x) ~> ▹ X x ◃ => t
      SAConLam : {Γ : ·ctx} {x : Nat} →
               (x # Γ) → -- todo: i added this; it doesn't appear in the text
                Γ ⊢ ▹ <||> ◃ => <||> ~ construct (lam x) ~>
                   ((·λ x <||>) ·:₂ (▹ <||> ◃ ==>₁ <||>)) => (<||> ==> <||>)
      SAConAp1 : {Γ : ·ctx} {t1 t2 : τ̇} {e : ė} →
                Γ ⊢ ▹ e ◃ => (t1 ==> t2) ~ construct ap ~> e ∘₂ ▹ <||> ◃ => t2
      SAConAp2 : {Γ : ·ctx} {e : ė} →
                Γ ⊢ ▹ e ◃ => <||> ~ construct ap ~>  e ∘₂ ▹ <||> ◃ => <||>
      SAConAp3 : {Γ : ·ctx} {t : τ̇} {e : ė} →
                (t ~̸ (<||> ==> <||>)) →
                Γ ⊢ ▹ e ◃ => t ~ construct ap ~> <| e |> ∘₂ ▹ <||> ◃ => <||>
      SAConArg : {Γ : ·ctx} {e : ė} {t : τ̇} →
                Γ ⊢ ▹ e ◃ => t ~ construct arg ~> ▹ <||> ◃ ∘₁ e => <||>
      SAConNumlit : {Γ : ·ctx} {e : ė} {n : Nat} →
                Γ ⊢ ▹ <||> ◃ => <||> ~ construct (numlit n) ~> ▹ N n ◃ => num
      -- todo: these ought to look like ap, no? why are there two here and
      -- three there? probably because of the induced type
      -- structure. otherwise i would try to abstract this..
      SAConPlus1 : {Γ : ·ctx} {e : ė} {t : τ̇} →
                (t ~ num) →
                Γ ⊢ ▹ e ◃ => t ~ construct plus ~> e ·+₂ ▹ <||> ◃  => num
      SAConPlus2 : {Γ : ·ctx} {e : ė} {t : τ̇} →
                (t ~̸ num) →
                Γ ⊢ ▹ e ◃ => t ~ construct plus ~> <| e |> ·+₂ ▹ <||> ◃  => num
      SAFinish : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 (Γ ⊢ e => t) →
                 Γ ⊢ ▹ <| e |> ◃ => <||> ~ finish ~> ▹ e ◃ => t
      SAZipAsc1 : {Γ : ·ctx} {e e' : ê} {α : action} {t : τ̇} →
                  (Γ ⊢ e ~ α ~> e' ⇐ t) →
                  Γ ⊢ (e ·:₁ t) => t ~ α ~> (e' ·:₁ t) => t
      SAZipAsc2 : {Γ : ·ctx} {e : ė} {α : action} {t t' : τ̂} →
                  (t + α +> t') →
                  (Γ ⊢ e <= (t' ◆t)) → -- todo: this rule seems weirdly asymmetrical
                  Γ ⊢ (e ·:₂ t) => (t ◆t) ~ α ~> (e ·:₂ t') => (t' ◆t)
      SAZipAp1 : {Γ : ·ctx} {t1 t2 t3 t4 : τ̇} {α : action} {eh eh' : ê} {e : ė} →
                 (Γ ⊢ (eh ◆e) => t2) →
                 (Γ ⊢ eh => t2 ~ α ~> eh' => (t3 ==> t4)) →
                 (Γ ⊢ e <= t3) →
                 Γ ⊢ (eh ∘₁ e) => t1 ~ α ~> (eh' ∘₁ e) => t4
      SAZipAp2 : {Γ : ·ctx} {t1 t2 : τ̇} {α : action} {eh eh' : ê} {e : ė} →
                 (Γ ⊢ (eh ◆e) => t2) →
                 (Γ ⊢ eh => t2 ~ α ~> eh' => <||>) →
                 (Γ ⊢ e <= <||>) →
                 Γ ⊢ (eh ∘₁ e) => t1 ~ α ~> (eh' ∘₁ e) => <||>
      SAZipAp3 : {Γ : ·ctx} {t2 t : τ̇} {e : ė} {eh eh' : ê} {α : action} →
                 (Γ ⊢ e => (t2 ==> t)) →
                 (Γ ⊢ eh ~ α ~> eh' ⇐ t2) →
                 Γ ⊢ (e ∘₂ eh) => t ~ α ~> (e ∘₂ eh') => t
      SAZipAp4 : {Γ : ·ctx} {e : ė} {eh eh' : ê} {α : action} →
                 (Γ ⊢ e => <||>) →
                 (Γ ⊢ eh ~ α ~> eh' ⇐ <||>) →
                 Γ ⊢ (e ∘₂ eh) => <||> ~ α ~> (e ∘₂ eh') => <||>
      SAZipPlus1 : {Γ : ·ctx} {e : ė} {eh eh' : ê} {α : action} →
                   (Γ ⊢ eh ~ α ~> eh' ⇐ num) →
                   Γ ⊢ (eh ·+₁ e) => num ~ α ~> (eh' ·+₁ e) => num
      SAZipPlus2 : {Γ : ·ctx} {e : ė} {eh eh' : ê} {α : action} →
                   (Γ ⊢ eh ~ α ~> eh' ⇐ num) →
                   Γ ⊢ (e ·+₂ eh) => num ~ α ~> (e ·+₂ eh') => num
      SAZipHole1 : {Γ : ·ctx} {e e' : ê} {t t' : τ̇} {α : action} →
                   (Γ ⊢ (e ◆e) => t) →
                   (Γ ⊢ e => t ~ α ~> e' => t') →
                   ((e' == ▹ <||> ◃) → ⊥) →
                   Γ ⊢ <| e |> => <||> ~ α ~>  <| e' |> => <||>
      SAZipHole2 : {Γ : ·ctx} {e : ê} {t : τ̇} {α : action} →
                   (Γ ⊢ (e ◆e) => t) →
                   (Γ ⊢ e => t ~ α ~> ▹ <||> ◃ => <||>) →
                   Γ ⊢ <| e |> => <||> ~ α ~> ▹ <||> ◃ => <||>

    -- analytic action expressions
    data _⊢_~_~>_⇐_ : (Γ : ·ctx) → (e : ê) → (α : action) →
                      (e' : ê) → (t : τ̇) → Set where
      AASubsume : {Γ : ·ctx} {e e' : ê} {t t' t'' : τ̇} {α : action} → -- troublemaker
                  {p : (α == construct asc → ⊥) × -- cyrus's proposed fix for two cases
                       ((x : Nat) → (α == construct (lam x) → ⊥))} →
                  (Γ ⊢ (e ◆e) => t') →
                  (Γ ⊢ e => t' ~ α ~> e' => t'') →
                  (t ~ t'') →
                  Γ ⊢ e ~ α ~> e' ⇐ t
      AAMove : {e e' : ê} {δ : direction} {Γ : ·ctx} {t : τ̇} →
                  (e + move δ +>e e') →
                  Γ ⊢ e ~ move δ ~> e' ⇐ t
      AADel : {e : ė} {Γ : ·ctx} {t : τ̇} →
                 Γ ⊢ ▹ e ◃ ~ del ~> ▹ <||> ◃ ⇐ t
      AAConAsc : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 Γ ⊢ ▹ e ◃ ~ construct asc ~> (e ·:₂ ▹ t ◃) ⇐ t
      AAConVar : {Γ : ·ctx} {t t' : τ̇} {x : Nat} →
                 (t ~̸ t') →           -- todo: i don't understand this
                 (p : (x , t') ∈ Γ) → -- todo: is this right?
                 Γ ⊢ ▹ <||> ◃ ~ construct (var x) ~> <| ▹ X x ◃ |> ⇐ t
      AAConLam1 : {Γ : ·ctx} {x : Nat} {t1 t2 : τ̇} →
                  (x # Γ) → -- todo: i added this
                  Γ ⊢ ▹ <||> ◃ ~ construct (lam x) ~>
                      ·λ x (▹ <||> ◃) ⇐ (t1 ==> t2)
      AAConLam2 : {Γ : ·ctx} {x : Nat} {t : τ̇} →
                  (x # Γ) → -- todo: i added this
                  (t ~̸ (<||> ==> <||>)) →
                  Γ ⊢ ▹ <||> ◃ ~ construct (lam x) ~>
                      <| ·λ x <||> ·:₂ (▹ <||> ◃ ==>₁ <||>) |> ⇐ t
      AAConNumlit : {Γ : ·ctx} {t : τ̇} {n : Nat} →
                    (t ~̸ num) →
                    Γ ⊢ ▹ <||> ◃ ~ construct (numlit n) ~> <| ▹ (N n) ◃ |> ⇐ t
      AAFinish : {Γ : ·ctx} {e : ė} {t : τ̇} →
                 (Γ ⊢ e <= t) →
                 Γ ⊢ ▹ <| e |> ◃ ~ finish ~> ▹ e ◃ ⇐ t
      AAZipLam : {Γ : ·ctx} {x : Nat} {t1 t2 : τ̇} {e e' : ê} {α : action} →
                 (x # Γ) →
                 ((Γ ,, (x , t1)) ⊢ e ~ α ~> e' ⇐ t2) →
                 Γ ⊢ (·λ x e) ~ α ~> (·λ x e') ⇐ (t1 ==> t2)


text:
module Issue259b where

postulate
 R : Set
 T : R → Set

I : Set
I = {x : R} → T x  -- The code type checks if this Π is explicit.

data P : Set where
 c : I → P

data D : P → Set where
 c : (i : I) → D (c i)

-- When pattern matching we do want to eta contract implicit lambdas.
Foo : (i : I) → D (c i) → Set₁
Foo i (c .i) = Set

postulate
  A : Set
  B : A → Set
  b : ({x : A} → B x) → A
  C : A → Set
  d : {x : A} → B x

e : A
e = b (λ {x} → d {x})

F : C e → Set₁
F _ with Set
F _ | _ = Set

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import PathInduction
open import Pushout

module JamesContractibility {i} (A : Type i) (⋆A : A) where

open import JamesTwoMaps A ⋆A public

-- We do not prove the flattening lemma here, we only prove that the following pushout is contractible

T : Type i
T = Pushout (span JA JA (A × JA) snd (uncurry αJ))

⋆T : T
⋆T = inl εJ

T-contr-inl-ε : inl εJ == ⋆T
T-contr-inl-ε = idp

T-contr-inl-α : (a : A) (x : JA) → inl x == ⋆T → inl (αJ a x) == ⋆T
T-contr-inl-α a x y = push (⋆A , αJ a x) ∙ ! (ap inr (δJ (αJ a x))) ∙ ! (push (a , x)) ∙ y

T-contr-inl-δ : (x : JA) (y : inl x == ⋆T) → Square (ap inl (δJ x)) y (T-contr-inl-α ⋆A x y) idp
T-contr-inl-δ x y = & coh (ap-square inr (& cη (ηJ x))) (natural-square (λ z → push (⋆A , z)) (δJ x) idp (ap-∘ inr (αJ ⋆A) (δJ x)))  where

  coh : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q q' : c == b} (q= : Square q q' idp idp)
             {d : A} {r : d == c} {e : A} {s : d == e} {t : d == a} (sq : Square r t q p)
      → Square t s (p ∙ ! q' ∙ ! r ∙ s) idp)
  coh = path-induction

  cη : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : a == c} {r : b == c} (ηJ : ! p ∙ q == r) → Square p q r idp)
  cη = path-induction

T-contr-inl : (x : JA) → inl x == ⋆T
T-contr-inl = JA-elim T-contr-inl-ε T-contr-inl-α (λ x y → ↓-='-from-square idp (ap-cst ⋆T (δJ x)) (square-symmetry (T-contr-inl-δ x y)))

T-contr-inr : (x : JA) → inr x == ⋆T
T-contr-inr x = ap inr (δJ x) ∙ ! (push (⋆A , x)) ∙ T-contr-inl x

T-contr-push : (a : A) (x : JA) → Square (T-contr-inl x) (push (a , x)) idp (T-contr-inr (αJ a x))
T-contr-push a x = & coh  where

  coh : Coh ({A : Type i} {a b : A} {r : a == b} {c : A} {p : c == b} {d : A} {q : d == c} {e : A} {y : d == e}
            → Square y q idp (p ∙ ! r ∙ (r ∙ ! p ∙ ! q ∙ y)))
  coh = path-induction

T-contr : (x : T) → x == ⋆T
T-contr = Pushout-elim T-contr-inl T-contr-inr (λ {(a , x) → ↓-='-from-square (ap-idf (push (a , x))) (ap-cst ⋆T (push (a , x))) (T-contr-push a x)})

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text:
module FFI.Data.Scientific where

open import Agda.Builtin.Float using (Float)
open import FFI.Data.String using (String)
open import FFI.Data.HaskellString using (HaskellString; pack; unpack)

{-# FOREIGN GHC import qualified Data.Scientific #-}
{-# FOREIGN GHC import qualified Text.Show #-}

postulate Scientific : Set
{-# COMPILE GHC Scientific = type Data.Scientific.Scientific #-}

postulate
  showHaskell : Scientific → HaskellString
  toFloat : Scientific → Float

{-# COMPILE GHC showHaskell = \x -> Text.Show.show x #-}
{-# COMPILE GHC toFloat = \x -> Data.Scientific.toRealFloat x #-}

show : Scientific → String
show x = pack (showHaskell x)

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
{-

This file document and export the main primitives of Cubical Agda. It
also defines some basic derived operations (composition and filling).

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Core.Primitives where

open import Agda.Builtin.Cubical.Path public
open import Agda.Builtin.Cubical.Sub public
  renaming ( inc to inS
           ; primSubOut to outS
           )
open import Agda.Primitive.Cubical public
  renaming ( primIMin       to _∧_  -- I → I → I
           ; primIMax       to _∨_  -- I → I → I
           ; primINeg       to ~_   -- I → I
           ; isOneEmpty     to empty
           ; primComp       to comp
           ; primHComp      to hcomp
           ; primTransp     to transp
           ; itIsOne        to 1=1 )
open import Agda.Primitive public
  using    ( Level )
  renaming ( lzero to ℓ-zero
           ; lsuc  to ℓ-suc
           ; _⊔_   to ℓ-max
           ; Setω  to Typeω )
open import Agda.Builtin.Sigma public

Type : (ℓ : Level) → Set (ℓ-suc ℓ)
Type ℓ = Set ℓ

Type₀ : Type (ℓ-suc ℓ-zero)
Type₀ = Type ℓ-zero

Type₁ : Type (ℓ-suc (ℓ-suc ℓ-zero))
Type₁ = Type (ℓ-suc ℓ-zero)

-- This file document the Cubical Agda primitives. The primitives
-- themselves are bound by the Agda files imported above.

-- * The Interval
-- I : Typeω

-- Endpoints, Connections, Reversal
-- i0 i1   : I
-- _∧_ _∨_ : I → I → I
-- ~_      : I → I

-- * Dependent path type. (Path over Path)

-- Introduced with lambda abstraction and eliminated with application,
-- just like function types.

-- PathP : ∀ {ℓ} (A : I → Type ℓ) → A i0 → A i1 → Type ℓ

infix 4 _[_≡_]

_[_≡_] : ∀ {ℓ} (A : I → Type ℓ) → A i0 → A i1 → Type ℓ
_[_≡_] = PathP

-- Non dependent path types

Path : ∀ {ℓ} (A : Type ℓ) → A → A → Type ℓ
Path A a b = PathP (λ _ → A) a b

-- PathP (λ i → A) x y gets printed as x ≡ y when A does not mention i.
--  _≡_ : ∀ {ℓ} {A : Type ℓ} → A → A → Type ℓ
--  _≡_ {A = A} = PathP (λ _ → A)

-- * @IsOne r@ represents the constraint "r = i1".
-- Often we will use "φ" for elements of I, when we intend to use them
-- with IsOne (or Partial[P]).
-- IsOne : I → Typeω

-- i1 is indeed equal to i1.
-- 1=1 : IsOne i1

-- * Types of partial elements, and their dependent version.

-- "Partial φ A" is a special version of "IsOne φ → A" with a more
-- extensional judgmental equality.
-- "PartialP φ A" allows "A" to be defined only on "φ".

-- Partial : ∀ {ℓ} → I → Type ℓ → Typeω
-- PartialP : ∀ {ℓ} → (φ : I) → Partial φ (Type ℓ) → Typeω

-- Partial elements are introduced by pattern matching with (r = i0)
-- or (r = i1) constraints, like so:

private
  sys : ∀ i → Partial (i ∨ ~ i) Type₁
  sys i (i = i0) = Type₀
  sys i (i = i1) = Type₀ → Type₀

  -- It also works with pattern matching lambdas:
  --  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatchingLambdas
  sys' : ∀ i → Partial (i ∨ ~ i) Type₁
  sys' i = λ { (i = i0) → Type₀
             ; (i = i1) → Type₀ → Type₀
             }

  -- When the cases overlap they must agree.
  sys2 : ∀ i j → Partial (i ∨ (i ∧ j)) Type₁
  sys2 i j = λ { (i = i1)          → Type₀
               ; (i = i1) (j = i1) → Type₀
               }

  -- (i0 = i1) is actually absurd.
  sys3 : Partial i0 Type₁
  sys3 = λ { () }

-- * There are cubical subtypes as in CCHM. Note that these are not
-- fibrant (hence in Typeω):

_[_↦_] : ∀ {ℓ} (A : Type ℓ) (φ : I) (u : Partial φ A) → Typeω
A [ φ ↦ u ] = Sub A φ u

infix 4 _[_↦_]

-- Any element u : A can be seen as an element of A [ φ ↦ u ] which
-- agrees with u on φ:

-- inS : ∀ {ℓ} {A : Type ℓ} {φ} (u : A) → A [ φ ↦ (λ _ → u) ]

-- One can also forget that an element agrees with u on φ:

-- outS : ∀ {ℓ} {A : Type ℓ} {φ : I} {u : Partial φ A} → A [ φ ↦ u ] → A

-- * Composition operation according to [CCHM 18].
-- When calling "comp A φ u a" Agda makes sure that "a" agrees with "u i0" on "φ".
-- compCCHM : ∀ {ℓ} (A : (i : I) → Type ℓ) (φ : I) (u : ∀ i → Partial φ (A i)) (a : A i0) → A i1

-- Note: this is not recommended to use, instead use the CHM
-- primitives! The reason is that these work with HITs and produce
-- fewer empty systems.

-- * Generalized transport and homogeneous composition [CHM 18].

-- When calling "transp A φ a" Agda makes sure that "A" is constant on "φ".
-- transp : ∀ {ℓ} (A : I → Type ℓ) (φ : I) (a : A i0) → A i1

-- When calling "hcomp A φ u a" Agda makes sure that "a" agrees with "u i0" on "φ".
-- hcomp : ∀ {ℓ} {A : Type ℓ} {φ : I} (u : I → Partial φ A) (a : A) → A

private
  variable
    ℓ  : Level
    ℓ′ : I → Level

-- Homogeneous filling
hfill : {A : Type ℓ}
        {φ : I}
        (u : ∀ i → Partial φ A)
        (u0 : A [ φ ↦ u i0 ])
        -----------------------
        (i : I) → A
hfill {φ = φ} u u0 i =
  hcomp (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
                 ; (i = i0) → outS u0 })
        (outS u0)

-- Heterogeneous composition can defined as in CHM, however we use the
-- builtin one as it doesn't require u0 to be a cubical subtype. This
-- reduces the number of inS's a lot.
-- comp : (A : ∀ i → Type (ℓ′ i))
--        {φ : I}
--        (u : ∀ i → Partial φ (A i))
--        (u0 : A i0 [ φ ↦ u i0 ])
--      → ---------------------------
--        A i1
-- comp A {φ = φ} u u0 =
--   hcomp (λ i → λ { (φ = i1) → transp (λ j → A (i ∨ j)) i (u _ 1=1) })
--         (transp A i0 (outS u0))

-- Heterogeneous filling defined using comp
fill : (A : ∀ i → Type (ℓ′ i))
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (u0 : A i0 [ φ ↦ u i0 ])
       ---------------------------
       (i : I) → A i
fill A {φ = φ} u u0 i =
  comp (λ j → A (i ∧ j))
       (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
                ; (i = i0) → outS u0 })
       (outS u0)

-- Σ-types
infix 2 Σ-syntax

Σ-syntax : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module lambda.system-f where

open import Data.Nat
open import Data.Fin hiding (lift)
open import lambda.vec
open import lambda.untyped hiding (lift; subst; ↑; subst₁)

infixr 22 _⇒_
infix 20 ∀'_

data type (n : ℕ) : Set where
  var : Fin n → type n
  ∀'_ : type (suc n) → type n
  _⇒_ : type n → type n → type n

type₀ : Set
type₀ = type 0

context : ℕ → ℕ → Set
context n = vec (type n)

lift : ∀ {n} → type n → type (suc n)
lift (var i) = var (suc i)
lift (∀' x) = ∀' (lift x)
lift (x ⇒ y) = lift x ⇒ lift y

↑ : ∀ {n m} → (Fin n → type m) → Fin (suc n) → type (suc m)
↑ ρ zero = var zero
↑ ρ (suc i) = lift (ρ i)

subst : ∀ {n m} → type n → (Fin n → type m) → type m
subst (var x) ρ = ρ x
subst (∀' x) ρ = ∀' (subst x (↑ ρ))
subst (x ⇒ y) ρ = (subst x ρ) ⇒ (subst y ρ)

idˢ : ∀ {n} → Fin n → type n
idˢ i = var i

_∘ˢ_ : ∀ {n m p} → (Fin m → type p) → (Fin n → type m) → (Fin n → type p)
(ρ ∘ˢ μ) i = subst (μ i) ρ

1ˢ : ∀ {n} → type n → Fin (suc n) → type n
1ˢ x zero = x
1ˢ x (suc i) = var i

_∷ˢ_ : ∀ {n m} → type m → (Fin n → type m) → Fin (suc n) → type m
(e ∷ˢ ρ) zero = e
(e ∷ˢ ρ) (suc i) = ρ i

subst₁ : ∀ {n} → type (suc n) → type n → type n
subst₁ x y = subst x (1ˢ y)

lift-c : ∀ {n m} → context n m → context (suc n) m
lift-c ε = ε
lift-c (Γ ▸ x) = lift-c Γ ▸ lift x

infix 10 _⊢_∶_

data _⊢_∶_ {n m : ℕ} (Γ : context n m) : term m → type n → Set where
  ax : ∀ {i} → Γ ⊢ var i ∶ lookup i Γ
  lam : ∀ {B x} → (A : type n) → Γ ▸ A ⊢ x ∶ B → Γ ⊢ lam x ∶ A ⇒ B
  app : ∀ {A B x y} → Γ ⊢ x ∶ A ⇒ B → Γ ⊢ y ∶ A → Γ ⊢ app x y ∶ B
  gen : ∀ {A x} → lift-c Γ ⊢ x ∶ A → Γ ⊢ x ∶ ∀' A
  sub : ∀ {A x} → (B : type n) → Γ ⊢ x ∶ ∀' A → Γ ⊢ x ∶ subst₁ A B

⊢_∶_ : ∀ {n} → term 0 → type n → Set
⊢ x ∶ t = ε ⊢ x ∶ t


text:
open import TypeTheory.Nat.Mono.Structure

module TypeTheory.Nat.Mono.Properties (nat : Nat) where

open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Empty using (⊥)
open import Data.Product using (Σ; _×_; _,_)
open import Data.Sum
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_)
open import Function.Base

open Nat nat

+-suc : ∀ m n → suc m + n ≡ suc (m + n)
+-suc m n = rec-suc _ _ _

+-identityˡ : ∀ n → zero + n ≡ n
+-identityˡ n = rec-zero _ _

+-identityʳ : ∀ n → n + zero ≡ n
+-identityʳ n = ind (λ k → k + zero ≡ k) (+-identityˡ zero)
                    (λ k k+z≡k → trans (+-suc k zero) (cong suc k+z≡k) )
                    n

1N+n≡sn : ∀ n → 1N + n ≡ suc n
1N+n≡sn n = begin
  suc zero + n   ≡⟨ +-suc zero n ⟩
  suc (zero + n) ≡⟨ cong suc (+-identityˡ n) ⟩
  suc n          ∎
  where open ≡-Reasoning

+-suc-comm : ∀ m n → suc m + n ≡ m + suc n
+-suc-comm m n =
  ind
    (λ o → suc o + n ≡ o + suc n)
    (begin
      suc zero + n ≡⟨ 1N+n≡sn n ⟩
      suc n        ≡⟨ sym $ +-identityˡ (suc n) ⟩
      zero + suc n ∎)
    (λ o so+n≡o+sn → begin
      suc (suc o) + n ≡⟨ +-suc (suc o) n ⟩
      suc (suc o + n) ≡⟨ cong suc so+n≡o+sn ⟩
      suc (o + suc n) ≡⟨ sym $ +-suc o (suc n) ⟩
      suc o + suc n   ∎)
    m
  where open ≡-Reasoning

z≤n : ∀ n → zero ≤ n
z≤n n = n , +-identityˡ n

≤-step : ∀ {m n} → m ≤ n → m ≤ suc n
≤-step {m} {n} (o , m+o≡n) = suc o , (begin
  m + suc o   ≡⟨ sym $ +-suc-comm m o ⟩
  suc m + o   ≡⟨ +-suc m o ⟩
  suc (m + o) ≡⟨ cong suc m+o≡n ⟩
  suc n       ∎)
  where open ≡-Reasoning

≤-refl : ∀ {n} → n ≤ n
≤-refl {n} = zero , +-identityʳ n

s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n
s≤s {m} {n} (o , m+o≡n) = o , trans (+-suc m o) (cong suc m+o≡n)

s<s : ∀ {m n} → m < n → suc m < suc n
s<s = s≤s

z<s : ∀ n → zero < suc n
z<s n = s≤s (z≤n n)

n<sn : ∀ n → n < suc n
n<sn n = ≤-refl {suc n}

≤⇒<∨≡ : ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
≤⇒<∨≡ {m} {n} (o , m+o≡n) =
  ind (λ k → m + k ≡ n → m < n ⊎ m ≡ n)
      (λ m+z≡n → inj₂ (trans (sym $ +-identityʳ m) m+z≡n))
      (λ k _ m+sk≡n → inj₁ (k , (trans (+-suc-comm m k) m+sk≡n)))
      o
      m+o≡n

data Order (m n : N) : Set where
  less    : (m<n : m < n) → Order m n
  equal   : (m≡n : m ≡ n) → Order m n
  greater : (m>n : m > n) → Order m n

order? : ∀ m n → Order m n
order? m₀ n₀ = ind (λ m → Order m n₀) order?-zero order?-suc m₀
  where
  order?-zero : Order zero n₀
  order?-zero = ind (Order zero) (equal refl) (λ _ _ → less (z<s _)) n₀

  order?-suc : ∀ m → Order m n₀ → Order (suc m) n₀
  order?-suc m (less sm≤n) with ≤⇒<∨≡ sm≤n
  ... | inj₁ sm<n = less sm<n
  ... | inj₂ sm≡n = equal sm≡n
  order?-suc m (equal refl)  = greater (n<sn _)
  order?-suc m (greater m>n) = greater (≤-step m>n)

-- indΔ :
module _ (P : N → N → Set) where
  indΔ : P zero zero →
         (∀ n → P zero (suc n)) →
         (∀ m → P (suc m) zero) →
         (∀ m n → P m n → P (suc m) (suc n)) →
         ∀ m n → P m n
  indΔ Pzz Pzs Psz Pss m n with order? m n
  ... | less    m<n = {!   !}
  ... | equal   m≡n = {!   !}
  ... | greater m>n = {!   !}


text:
module _ where

infixr 5 _⇒_
infixl 6 _▻_
infix  3 _⊢_ _∈_
infixr 5 vs_
infixr 4 ƛ_
infixl 6 _·_

data Type : Set where
  ι   : Type
  _⇒_ : Type → Type → Type

data Con : Set where
  ε   : Con
  _▻_ : Con → Type → Con

data _∈_ σ : Con → Set where
  vz  : ∀ {Γ}   → σ ∈ Γ ▻ σ
  vs_ : ∀ {Γ τ} → σ ∈ Γ     → σ ∈ Γ ▻ τ

data _⊢_ Γ : Type → Set where
  var : ∀ {σ}   → σ ∈ Γ     → Γ ⊢ σ
  ƛ_  : ∀ {σ τ} → Γ ▻ σ ⊢ τ → Γ ⊢ σ ⇒ τ
  _·_ : ∀ {σ τ} → Γ ⊢ σ ⇒ τ → Γ ⊢ σ     → Γ ⊢ τ

Term : Type → Set
Term σ = ε ⊢ σ

postulate
  _extends_ : Con → Con → Set

  instance
    extends-stop : ∀ {Γ} → Γ extends Γ
    extends-skip : ∀ {Γ Δ σ} {{_ : Δ extends Γ}} → (Δ ▻ σ) extends Γ

  lam : ∀ {Γ σ τ} → ((∀ {Δ} {{_ : Δ extends (Γ ▻ σ)}} → Δ ⊢ σ) → Γ ▻ σ ⊢ τ) → Γ ⊢ σ ⇒ τ

I : Term (ι ⇒ ι)
I = lam λ x → x

K : Term (ι ⇒ ι ⇒ ι)
K = lam λ x → lam λ y → x

A : Term ((ι ⇒ ι) ⇒ ι ⇒ ι)
A = lam λ f → lam λ x → f {{extends-skip {{extends-stop}}}} · x
                            {{extends-stop}}

loop : Term ((ι ⇒ ι) ⇒ ι ⇒ ι)
loop = lam λ f → lam λ x → f · x

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- TODO: use StrictTotalOrder for QName representation

module Syntax (QName : Set) where

open import Data.Nat.Base
open import Data.Nat.Properties using (+-suc; +-identityʳ)
open import Data.List.Base hiding (_∷ʳ_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans)

-- Well-scoped de Bruijn indices
-- n is the length of the context

data Var : ℕ → Set where
  vzero : ∀{n} → Var (suc n)
  vsuc  : ∀{n} (x : Var n) → Var (suc n)

-- Example: in context x,y,z (so n = 3)
-- x  is  vsuc (vsuc vzero) : Var 3
-- y  is      vsuc vzero  : Var 3
-- z  is         vzero  : Var 3

-- Qualified names

DRName   = QName  -- datatype / record name
FuncName = QName  -- function name
ProjName = QName  -- projection name (overloaded)
ConsName = QName  -- datatype / record constructor name (overloaded)

-- Data or record constructors

data ConHead : Set where
  dataCon : DRName → ConHead
  recCon  : DRName → (fs : List ProjName) → ConHead

-- Sorts are Set₀, Set₁, ...

data Sort : Set where
  uni : (ℓ : ℕ) → Sort

-- In the following definition of well-scoped syntax,
-- n is always the length of the context.

mutual

  data Term (n : ℕ) : Set where
    var : (x : Var n) (es : Elims n) → Term n
    def : (f : FuncName) (es : Elims n) → Term n
    con : (c : ConHead) (vs : Args n) → Term n     -- Fully applied
    lam : (v : Term (suc n)) → Term n
    -- Types
    dat  : (d : DRName) (vs : Args n) → Term n     -- Fully applied
    sort : (s : Sort) → Term n
    pi   : (u : Term n) (v : Term (suc n)) → Term n

  data Elim (n : ℕ) : Set where
    apply : (u : Term n)   → Elim n
    proj  : (π : ProjName) → Elim n

  Elims : (n : ℕ) → Set
  Elims n = List (Elim n)

  Args : (n : ℕ) → Set
  Args n = List (Term n)

-- Example: (A : Set) (x : A) → A
-- is represented by

exTyId : Term 0
exTyId = pi (sort (uni 0)) (pi (var vzero []) (var (vsuc vzero) []))

-- Looking up a field in a field-value collection

-- TODO: Do we want to ensure |fs| = |vs| ?
data LookupField {a} {A : Set a} : (fs : List ProjName) (vs : List A) (f : ProjName) (v : A) → Set where

  here : ∀{f fs v vs}
    → LookupField (f ∷ fs) (v ∷ vs) f v

  there : ∀{f f' fs v v' vs}
    → LookupField fs vs f v
    → LookupField (f' ∷ fs) (v' ∷ vs) f v

-- Renamings represented as functions

Renaming : (Γ Δ : ℕ) → Set
Renaming Γ Δ = Var Δ → Var Γ

weak : ∀{Γ} → Renaming (suc Γ) Γ
weak x = vsuc x

-- If    Γ   ⊢ ρ         : Δ
-- then  Γ,x ⊢ liftRen ρ : Δ,x.

liftRen : ∀{Γ Δ} → Renaming Γ Δ → Renaming (suc Γ) (suc Δ)
liftRen ρ vzero    = vzero
liftRen ρ (vsuc x) = vsuc (ρ x)

-- We need sized types to show termination of rename.
{-# TERMINATING #-}

mutual
  rename : ∀{Γ Δ} (ρ : Renaming Γ Δ) (t : Term Δ) → Term Γ
  rename ρ (var x es) = var (ρ x) (map (renameElim ρ) es)
  rename ρ (def f es) = def f (map (renameElim ρ) es)
  rename ρ (con c vs) = con c (map (rename ρ) vs)
  rename ρ (lam t)    = lam (rename (liftRen ρ) t)
  rename ρ (dat d vs) = dat d (map (rename ρ) vs)
  rename ρ (sort s)   = sort s
  rename ρ (pi u v)   = pi (rename ρ u) (rename (liftRen ρ) v)

  renameElim : ∀{Γ Δ} (ρ : Renaming Γ Δ) (e : Elim Δ) → Elim Γ
  renameElim ρ (apply u) = apply (rename ρ u)
  renameElim ρ (proj π)  = proj π

-- Substitutions represented as functions

-- σ : Subst Γ Δ  applies to a term living in context Δ
-- and turns it into a term living in context Γ

Substitution : (Γ Δ : ℕ) → Set
Substitution Γ Δ = Var Δ → Term Γ

liftSub : ∀{Γ Δ} (σ : Substitution Γ Δ) → Substitution (suc Γ) (suc Δ)
liftSub σ vzero    = var vzero []
liftSub σ (vsuc x) = rename weak (σ x)

-- Substitute for the last variable (vzero)

sg : ∀{Γ} (u : Term Γ) → Substitution Γ (suc Γ)
sg {Γ} u vzero    = u
sg {Γ} u (vsuc x) = var x []

data All₂ {A B : Set} (R : A → B → Set) : List A → List B → Set where
  nil  : All₂ R [] []
  cons : ∀{x y xs ys}
    → R x y
    → All₂ R xs ys
    → All₂ R (x ∷ xs) (y ∷ ys)

mutual

  data Apply {Γ} : (t : Term Γ) (es : Elims Γ) (v : Term Γ) → Set where

    empty : ∀{t}
      → Apply t [] t

    var : ∀{x es es'}
      → Apply (var x es) es' (var x (es ++ es'))

    def : ∀{f es es'}
      → Apply (def f es) es' (def f (es ++ es'))

    proj : ∀{ c πs vs π es u v}
      → LookupField πs vs π u
      → Apply u es v
      → Apply (con (recCon c πs) vs) (proj π ∷ es) v

    lam : ∀{t t' u v es}
      → SubstTerm (sg u) t t'
      → Apply t' es v
      → Apply (lam t) (apply u ∷ es) v

  data SubstTerm {Γ Δ} (σ : Substitution Γ Δ) : Term Δ → Term Γ → Set where

    var : ∀{x : Var Δ} {es : Elims Δ} {v : Term Γ} {es' : Elims Γ}
      → All₂ (SubstElim σ) es es'
      → Apply (σ x) es' v
      → SubstTerm σ (var x es) v

    def : ∀{f : FuncName} {es : Elims Δ} {es' : Elims Γ}
      → All₂ (SubstElim σ) es es'
      → SubstTerm σ (def f es) (def f es')

    con : ∀{c : ConHead} {vs : Args Δ} {vs' : Args Γ}
      → All₂ (SubstTerm σ) vs vs'
      → SubstTerm σ (con c vs) (con c vs')

    lam : ∀{v : Term (suc Δ)} {v'}
      → SubstTerm (liftSub σ) v v'
      → SubstTerm σ (lam v) (lam v')

    dat : ∀{d : DRName} {vs : Args Δ} {vs' : Args Γ}
      → All₂ (SubstTerm σ) vs vs'
      → SubstTerm σ (dat d vs) (dat d vs')

    pi : ∀{U V U' V'}
      → SubstTerm σ U U'
      → SubstTerm (liftSub σ) V V'
      → SubstTerm σ (pi U V) (pi U' V')

    sort : ∀{s : Sort}
      → SubstTerm σ (sort s) (sort s)

  data SubstElim {Γ Δ} (σ : Substitution Γ Δ) : Elim Δ → Elim Γ → Set where

    apply : ∀{u u'}
      → SubstTerm σ u u'
      → SubstElim σ (apply u) (apply u')

    proj : ∀{π}
      → SubstElim σ (proj π) (proj π)

data FunctionApply {Γ} : (T : Term Γ) (us : Args Γ) (U : Term Γ) → Set where

  empty : ∀{T}
    → FunctionApply T [] T

  pi : ∀{u us T U V V'}
    → SubstTerm (sg u) V V'
    → FunctionApply V' us T
    → FunctionApply (pi U V) (u ∷ us) T

-- n is the length of the context
data Context : (n : ℕ) → Set where
  []   : Context zero
  _∷ʳ_ : ∀{n} → Context n → Term n → Context (suc n)

-- n is the size of the outer context; m is the size of the telescope
data Telescope (n : ℕ) : (m : ℕ) →  Set where
  []  : Telescope n zero
  _∷_ : ∀{m} → Term n → Telescope (suc n) m → Telescope n (suc m)

telescopeSize : ∀{n m} → Telescope n m → ℕ
telescopeSize {m = m} _ = m

suc-move : (m n : ℕ) → m + suc n ≡ suc m + n
suc-move zero    n = refl
suc-move (suc m) n = cong suc (+-suc m n)

-- Add a telescope to a compatible outer context.
addToContext : ∀{n m}  → Context n → Telescope n m → Context (n + m)
addToContext {n}            Γ []                rewrite +-identityʳ n = Γ
addToContext {n} {.(suc m)} Γ (_∷_ {m = m} x t) rewrite suc-move n m       = addToContext (Γ ∷ʳ x) t

expandTelescope : ∀ {n m} → Telescope n m → Term (n + m) → Term n
expandTelescope {n} [] T rewrite +-identityʳ n = T
expandTelescope {n} {suc m} (U ∷ Δ) T rewrite suc-move n m =
  pi U (expandTelescope Δ T)

data Pattern (n : ℕ) : Set where
  pvariable      : Var n → Pattern n
  pconstructor   : ConsName → List (Pattern n) → Pattern n
  pinaccesssible : Term n → Pattern n

data Copattern (n : ℕ) : Set where
  capply : Pattern n → Copattern n
  cproj  : ProjName  → Copattern n

record ConsDeclaration (n : ℕ) : Set where
  constructor mkConsDeclaration
  field
    consName : ConsName
    consType : Term n

record ProjDeclaration (n : ℕ) : Set where
  constructor mkProjDeclaration
  field
    projName : ProjName
    projType : Term n

record DataSignature : Set where
  constructor mkDataSignature
  field
    name         : DRName
    {numParams}  : ℕ
    {numIndices} : ℕ
    params       : Telescope zero      numParams
    indices      : Telescope numParams numIndices
    dsort        : Sort

record DataDefinition : Set where
  field
    name         : DRName
    {numParams}  : ℕ
    params       : Telescope zero numParams
    constructors : List (ConsDeclaration numParams)

record RecordSignature : Set where
  constructor mkRecordSignature
  field
    name        : DRName
    {numParams} : ℕ
    params      : Telescope zero numParams
    dsort       : Sort

record RecordDefinition : Set where
  field
    name         : DRName
    {numParams}  : ℕ
    params       : Telescope zero numParams
    fconstructor : ConsName
    fields       : List (ProjDeclaration numParams)

-- TODO: Update spec
record FuncClause : Set where
   field
     ctxSize : ℕ
     ctx   : Context ctxSize
     name  : FuncName
     spine : List (Copattern ctxSize)
     rhs   : Term ctxSize

-- TODO: How to represent pattern variables?
data Declaration : Set where
  typeSignature    : FuncName → Term zero → Declaration
  functionClause   : FuncClause → Declaration
  dataSignature    : DataSignature    → Declaration
  dataDefinition   : DataDefinition   → Declaration
  recordSignature  : RecordSignature  → Declaration
  recordDefinition : RecordDefinition → Declaration

-- TODO: Update signature declarations
data SignatureDeclaration : Set where
  dataSig     : (D : DataSignature) → List (ConsDeclaration (DataSignature.numParams D)) →
                SignatureDeclaration
  recordSig   : (R : RecordSignature) → ConsDeclaration (RecordSignature.numParams R) →
                List (ProjDeclaration (RecordSignature.numParams R)) → SignatureDeclaration
  functionSig : FuncName → Term zero → List FuncClause → SignatureDeclaration

Signature : Set
Signature = List SignatureDeclaration

data LookupSig : Signature → SignatureDeclaration → Set where

  here : ∀{sd sds}
    → LookupSig (sd ∷ sds) sd

  there : ∀{sd sd' sds}
    → LookupSig sds sd
    → LookupSig (sd' ∷ sds) sd

data LookupCons : ∀{m} → List (ConsDeclaration m) → ConsName → Term m → Set where

  here : ∀{c m} {T : Term m} {cs : List (ConsDeclaration m)}
    → LookupCons {m} (mkConsDeclaration c T ∷ cs) c T

  there : ∀{c c' m} {T : Term m} {T' : Term m} {cs : List (ConsDeclaration m)}
    → LookupCons cs c T
    → LookupCons (mkConsDeclaration c' T' ∷ cs) c T

data LookupProj : ∀{m} → List (ProjDeclaration m) → ProjName → Term m → Set where

  here : ∀{π m} {T : Term m} {πs : List (ProjDeclaration m)}
    → LookupProj (mkProjDeclaration π T ∷ πs) π T

  there : ∀ {π π' m} {πs : List (ProjDeclaration m)} {T : Term m} {T' : Term m}
    → LookupProj πs π T
    → LookupProj (mkProjDeclaration π' T' ∷ πs) π T

data SigLookup : ∀{m} → Signature → QName → Term m → Set where
  func : ∀{Σ f T cls} → LookupSig Σ (functionSig f T cls) → SigLookup Σ f T
  dat : ∀{Σ D m m' s cs} {Δ : Telescope zero m} {Δ' : Telescope m m'} →
        LookupSig Σ (dataSig (mkDataSignature D {m} {m'} Δ Δ' s) cs) →
        SigLookup Σ D (expandTelescope Δ (expandTelescope Δ' (sort s)))
  con : ∀{Σ D m m' s cs c T} {Δ : Telescope zero m} {Δ' : Telescope m m'} →
        LookupSig Σ (dataSig (mkDataSignature D {m} {m'} Δ Δ' s) cs) →
        LookupCons cs c T →
        SigLookup Σ c (expandTelescope Δ T)
  rec : ∀{Σ R m s c ps} {Δ : Telescope zero m} →
        LookupSig Σ (recordSig (mkRecordSignature R Δ s) c ps) →
        SigLookup Σ R (expandTelescope Δ (sort s))
  rcon : ∀{Σ R m s c T πs} {Δ : Telescope zero m} →
         LookupSig Σ (recordSig (mkRecordSignature R Δ s) (mkConsDeclaration c T) πs) →
         SigLookup Σ c (expandTelescope Δ T)
  rproj : ∀{Σ R m s c π T πs} {Δ : Telescope zero m} →
          LookupSig Σ (recordSig (mkRecordSignature R Δ s) (mkConsDeclaration c T) πs) →
          LookupProj πs π T →
          SigLookup Σ π (expandTelescope Δ T)

max_stars_repo_name: agda/agda-spec

max_issues_repo_name: agda/agda-spec

max_forks_repo_name: agda/agda-spec


text:
open import Data.Product using ( _×_ ; _,_ )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ ; ⊨a-resp-≲ )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; ⌊_⌋ )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _≃_ ; ≃⌊_⌋ ; ≃-impl-≲ )
open import Web.Semantic.DL.KB using ( KB ; tbox ; abox )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Model using ( _⊨t_ ; ⊨t-resp-≃ )

module Web.Semantic.DL.KB.Model {Σ : Signature} {X : Set} where

infixr 2 _⊨_

_⊨_ : Interp Σ X → KB Σ X → Set
I ⊨ K = (⌊ I ⌋ ⊨t tbox K) × (I ⊨a abox K)

Interps : KB Σ X → Interp Σ X → Set
Interps K I = I ⊨ K

⊨-resp-≃ : ∀ {I J} → (I ≃ J) → ∀ K → (I ⊨ K) → (J ⊨ K)
⊨-resp-≃ I≃J K (I⊨T , I⊨A) =
  (⊨t-resp-≃ ≃⌊ I≃J ⌋ (tbox K) I⊨T , ⊨a-resp-≲ (≃-impl-≲ I≃J) (abox K) I⊨A)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


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

{- The type of all types in some universe with a fixed truncation level
   behaves almost like a universe itself. In this utility module, we develop
   some notation for efficiently working with this pseudo-universe.
   It will lead to considerably more briefer and more comprehensible proofs. -}
module Universe.Utility.TruncUniverse where

open import lib.Basics
open import lib.NType2
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.TLevel
open import lib.types.Unit

open import Universe.Utility.General

module _ {n : ℕ₋₂} where
  ⟦_⟧ : ∀ {i} → n -Type i → Type i
  ⟦ (B , _) ⟧ = B

module _ {n : ℕ₋₂} where
  Lift-≤ : ∀ {i j} → n -Type i → n -Type (i ⊔ j)
  Lift-≤ {i} {j} (A , h) = (Lift {j = j} A , equiv-preserves-level (lift-equiv ⁻¹) h)

  raise : ∀ {i} → n -Type i → S n -Type i
  raise (A , h) = (A , raise-level n h)

  raise-≤T : ∀ {i} {m n : ℕ₋₂} → m ≤T n → m -Type i → n -Type i
  raise-≤T p (A , h) = (A , raise-level-≤T p h)

  ⊤-≤ : n -Type lzero
  ⊤-≤ = (⊤ , raise-level-≤T (-2≤T n) Unit-is-contr)

  Π-≤ : ∀ {i j} (A : Type i) → (A → n -Type j) → n -Type (i ⊔ j)
  Π-≤ A B = (Π A (fst ∘ B) , Π-level (snd ∘ B))

  infixr 2 _→-≤_

  _→-≤_ : ∀ {i j} → Type i → n -Type j → n -Type (i ⊔ j)
  A →-≤ B = Π-≤ A (λ _ → B)

  Σ-≤ : ∀ {i j} (A : n -Type i) → (⟦ A ⟧ → n -Type j) → n -Type (i ⊔ j)
  Σ-≤ A B = (Σ ⟦ A ⟧ (λ a → ⟦ B a ⟧) , Σ-level (snd A) (snd ∘ B))

  infixr 4 _×-≤_

  _×-≤_ : ∀ {i j} → n -Type i → n -Type j → n -Type (i ⊔ j)
  A ×-≤ B = Σ-≤ A (λ _ → B)

  Path-< : ∀ {i} (A : S n -Type i) (x y : ⟦ A ⟧) → n -Type i
  Path-< A x y = (x == y , snd A _ _)

  Path-≤ : ∀ {i} (A : n -Type i) (x y : ⟦ A ⟧) → n -Type i
  Path-≤ A x y = Path-< (raise A) x y

  _≃-≤_ : ∀ {i j} (A : n -Type i) (B : n -Type j) → n -Type (i ⊔ j)
  A ≃-≤ B = (⟦ A ⟧ ≃ ⟦ B ⟧ , ≃-level (snd A) (snd B))

_-Type-≤_ : (n : ℕ₋₂) (i : ULevel) → S n -Type lsucc i
n -Type-≤ i = (n -Type i , n -Type-level i)

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
module plfa-code.Induction where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
open import Function

open import plfa-code.Reasoning-legacy

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5
  ≡⟨⟩
    7 + 5
  ≡⟨⟩
    12
  ≡⟨⟩
    3 + 9
  ≡⟨⟩
    3 + (4 + 5)
  ∎

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m)⟩
    suc m
  ∎

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm zero n =
  begin
    zero + n
  ≡⟨⟩
    n
  ≡⟨ sym (+-identityʳ n) ⟩
    n + zero
  ∎
+-comm (suc m) n =
  begin
    suc m + n
  ≡⟨⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨ sym (+-suc n m) ⟩
    n + suc m
  ∎

+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ +-assoc m n (p + q) ⟩
    m + (n + (p + q))
  ≡⟨ cong (m +_) (sym (+-assoc n p q)) ⟩
    m + ((n + p) + q)
  ≡⟨ sym (+-assoc m (n + p) q) ⟩
    (m + (n + p)) + q
  ∎

+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc′ zero n p = refl
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl

-- practice

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m zero p = refl
+-swap m (suc n) p
  rewrite +-suc m (n + p)
  | sym (+-assoc m n p)
  | +-comm m n
  | +-assoc n m p = refl

*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p = refl
*-distrib-+ (suc m) n p rewrite *-distrib-+ m n p
                                | sym (+-assoc p (m * p) (n * p)) = refl

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p = refl
*-assoc (suc m) n p rewrite *-distrib-+ n (m * n) p | *-assoc m n p = refl

*-zeroʳ : ∀ (n : ℕ) → n * zero ≡ zero
*-zeroʳ zero = refl
*-zeroʳ (suc n) rewrite *-zeroʳ n = refl

*-suc : ∀ (m n : ℕ) → m * suc n ≡ m * n + m
*-suc zero n = refl
*-suc (suc m) n =
  begin
    (suc m) * (suc n)
  ≡⟨⟩
    (suc n) + m * (suc n)
  ≡⟨ cong ((suc n) +_) (*-suc m n) ⟩
    suc n + (m * n + m)
  ≡⟨ +-swap (suc n) (m * n) m ⟩
    m * n + (suc n + m)
  ≡⟨ cong ((m * n) +_) (sym (+-suc n m)) ⟩
    m * n + (n + suc m)
  ≡⟨ sym (+-assoc (m * n) n (suc m)) ⟩
    m * n + n + suc m
  ≡⟨ cong (_+ (suc m)) (+-comm (m * n) n) ⟩
    (suc m) * n + (suc m)
  ∎

*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm zero n rewrite *-zeroʳ n = refl
*-comm (suc m) n =
  begin
    suc m * n
  ≡⟨⟩
    n + m * n
  ≡⟨ +-comm n (m * n) ⟩
    m * n + n
  ≡⟨ cong (_+ n) (*-comm m n) ⟩
    n * m + n
  ≡⟨ sym (*-suc n m) ⟩
    n * suc m
  ∎

z∸n≡z : ∀ (n : ℕ) → zero ∸ n ≡ zero
z∸n≡z zero = refl
z∸n≡z (suc n) = refl

∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc zero n p rewrite z∸n≡z n | z∸n≡z p | z∸n≡z (n + p) = refl
∸-+-assoc (suc m) zero p = refl
∸-+-assoc (suc m) (suc n) p rewrite ∸-+-assoc m n p = refl

---------- Bin ----------
data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil    = x1 nil
inc (x0 t) = x1 t
inc (x1 t) = x0 (inc t)

to : ℕ → Bin
to zero    = x0 nil
to (suc n) = inc (to n)

from : Bin → ℕ
from nil      = 0
from (x0 t)   = 2 * (from t)
from (x1 t)   = suc (2 * (from t))
--------------------------------------

+1≡suc : ∀ {n : ℕ} → n + 1 ≡ suc n
+1≡suc {zero}   = refl
+1≡suc {suc n}  = cong suc +1≡suc

suc-from-inc : ∀ (x : Bin) → from (inc x) ≡ suc (from x)
suc-from-inc nil                                                        = refl
suc-from-inc (x0 x) rewrite +1≡suc {from x * 2}                         = refl
suc-from-inc (x1 x) rewrite suc-from-inc x | +-suc (from x) (from x + 0) = refl

-- t4 is ⊥ , because `to (from nil) ≡ x0 nil ≢ nil`
-- t4 : ∀ (x : Bin) → to (from x) ≡ x

from-to-const : ∀ (n : ℕ) → from (to n) ≡ n
from-to-const zero                                                  = refl
from-to-const (suc n) rewrite suc-from-inc (to n) | from-to-const n = refl

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category where

open import Level

-- The main definitions are in:
open import Categories.Category.Core public

-- Convenience functions for working over mupliple categories at once:
-- C [ x , y ] (for x y objects of C) - Hom_C(x , y)
-- C [ f ≈ g ] (for f g arrows of C)  - that f and g are equivalent arrows
-- C [ f ∘ g ] (for f g composables arrows of C) - composition in C
infix 10  _[_,_] _[_≈_] _[_∘_]

_[_,_] : ∀ {o ℓ e} → (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ
_[_,_] = Category._⇒_

_[_≈_] : ∀ {o ℓ e} → (C : Category o ℓ e) → ∀ {X Y} (f g : C [ X , Y ]) → Set e
_[_≈_] = Category._≈_

_[_∘_] : ∀ {o ℓ e} → (C : Category o ℓ e) → ∀ {X Y Z} (f : C [ Y , Z ]) → (g : C [ X , Y ]) → C [ X , Z ]
_[_∘_] = Category._∘_

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module UselessPrivatePrivate where

private
  private
    postulate
      A : Set

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module NoBindingForBuiltin where

foo = 42

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --universe-polymorphism #-}

module TrustMe-with-doubly-indexed-equality where

open import Common.Level

infix 4 _≡_

data _≡_ {a} {A : Set a} : A → A → Set a where
  refl : ∀ {x} → x ≡ x

{-# BUILTIN EQUALITY _≡_  #-}
{-# BUILTIN REFL     refl #-}

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

primitive
  primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y

postulate
  A : Set
  x : A

eq : x ≡ x
eq = primTrustMe

evaluates-to-refl : sym (sym eq) ≡ eq
evaluates-to-refl = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Primality
------------------------------------------------------------------------

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

module Data.Nat.Primality where

open import Data.Empty using (⊥)
open import Data.Fin using (Fin; toℕ)
open import Data.Fin.Properties using (all?)
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Nat.Divisibility using (_∤_; _∣?_)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (from-yes)
open import Relation.Nullary.Negation using (¬?)
open import Relation.Unary using (Decidable)

-- Definition of primality.

Prime : ℕ → Set
Prime 0             = ⊥
Prime 1             = ⊥
Prime (suc (suc n)) = (i : Fin n) → 2 + toℕ i ∤ 2 + n

-- Decision procedure for primality.

prime? : Decidable Prime
prime? 0             = no λ()
prime? 1             = no λ()
prime? (suc (suc n)) = all? (λ _ → ¬? (_ ∣? _))

private

  -- Example: 2 is prime.

  2-is-prime : Prime 2
  2-is-prime = from-yes (prime? 2)


text:
module TestNat where
import PreludeNatType
import AlonzoPrelude
import PreludeNat
import PreludeString
import PreludeShow
import RTP
import PreludeList

open AlonzoPrelude
open PreludeShow
open PreludeNatType
open PreludeString
open PreludeNat
open PreludeList hiding(_++_)
one = suc zero
two = suc one

lines : (List String) -> String
lines [] = ""
lines (l :: []) = l
lines (l :: ls) = l ++ "\n" ++ (lines ls)

mainS = (id ○ lines) ((showNat 42) :: (showBool (2007 == 2007)) :: [])


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

-- Multicategories but over an 'index' type, rather than forcing Fin n
module Categories.Multi.Category.Indexed where

open import Level
open import Data.Fin.Base using (Fin)
open import Data.Product using (Σ; uncurry; curry; _×_; _,_; proj₁; proj₂)
open import Data.Product.Properties
open import Data.Unit.Polymorphic using (⊤; tt)
open import Data.Vec.Functional
open import Function.Base using (const) renaming (_∘_ to _●_; id to id→)
open import Function.Equality using (_⟨$⟩_)
-- note how this is Function.Inverse instead of the one from Function.
open import Function.Inverse as Inv renaming (id to id↔; _∘_ to trans)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- any point can be lifted to a function from ⊤
pointed : {s t : Level} {S : Set s} (x : S) → ⊤ {t} → S
pointed x _ = x

-- the standard library doesn't seem to have the 'right' version of these.
⊤×K↔K : {t k : Level} {K : Set k} → (⊤ {t} × K) ↔ K
⊤×K↔K = inverse proj₂ (tt ,_) (λ _ → refl) λ _ → refl

K×⊤↔K : {t k : Level} {K : Set k} → (K × ⊤ {t}) ↔ K
K×⊤↔K = inverse proj₁ (_, tt) (λ _ → refl) λ _ → refl

⊤×⊤↔⊤ : {t : Level} → (⊤ {t} × ⊤) ↔ ⊤
⊤×⊤↔⊤ = inverse proj₁ (λ x → x , x) (λ _ → refl) λ _ → refl

Σ-assoc : {a b c : Level} {I : Set a} {J : I → Set b} {K : Σ I J → Set c} →
  Σ (Σ I J) K ↔ Σ I (λ i → Σ (J i) (curry K i))
Σ-assoc {I = I} {J} {K} = inverse g f (λ _ → refl) λ _ → refl
  where
  f : Σ I (λ i → Σ (J i) (λ j → K (i , j))) → Σ (Σ I J) K
  f (i , j , k) = (i , j) , k
  g : Σ (Σ I J) K → Σ I (λ i → Σ (J i) (λ j → K (i , j)))
  g ((i , j) , k) = i , j , k

-- the ι level is for the 'index' (and to not steal 'i')

-- The important part is that in _∘_, there is no flattening of the
-- index set. But also _≈[_]_ builds in an explicit equivalence
-- that allows one to properly re-index things. The classical view
-- of MultiCategory sweeps all of that under the rug, which gives
-- Agda conniptions (and rightfully so). The advantage of doing it
-- this way makes it clear that the 3 laws are based on the underlying
-- 3 laws that hold for (dependent!) product.

-- The upshot is that this version of MultiCategory makes no finiteness
-- assumption whatsoever.  The index sets involved could be huge,
-- without any issues.

-- Note that this still isn't Symmetric Multicategory. The renaming that
-- happens on indices say nothing about the relation to the contents
-- of the other Hom set.
record MultiCategory {o ℓ e ı : Level} : Set (suc (o ⊔ ℓ ⊔ e ⊔ ı)) where
  infix  4 _≈[_]_
  infixr 9 _∘_

  field
    Obj : Set o
    Hom : {I : Set ı} → (I → Obj) → Obj → Set ℓ
    id : (o : Obj) → Hom {⊤} (pointed o) o
    _∘_ : {I : Set ı} {aₙ : I → Obj} {a : Obj} {J : I → Set ı}
          {v : (i : I) → J i → Obj} {b : I → Obj} →
          Hom {I} aₙ a → ((i : I) → Hom (v i) (b i)) → Hom {Σ I J} (uncurry v) a
    _≈[_]_ : {I J : Set ı} {aₙ : I → Obj} {a : Obj} →
          Hom {I} aₙ a → (σ : I ↔ J) → Hom {J} (aₙ ● ( Inverse.from σ ⟨$⟩_ )) a → Set e

    identityˡ : {K : Set ı} {aₖ : K → Obj} {a : Obj} {f : Hom aₖ a} →
              id a ∘ pointed f ≈[ ⊤×K↔K ]  f
    identityʳ : {K : Set ı} {aₖ : K → Obj} {a : Obj} {f : Hom aₖ a} →
              f ∘ (id ● aₖ) ≈[ K×⊤↔K ] f

    identity² : {a : Obj} → id a ∘ pointed (id a) ≈[ ⊤×⊤↔⊤ ] id a

    assoc : -- the 3 index sets
            {I : Set ı} {J : I → Set ı} {K : Σ I J → Set ı}
            -- the 3 sets of (indexed) objects
            {vh : I → Obj} {bh : Obj}
            {vg : (i : I) → J i → Obj} {bg : I → Obj}
            {vf : (h : Σ I J) → K h → Obj} {bf : Σ I J → Obj}
            -- the 3 Homs
            {h : Hom vh bh}
            {g : (i : I) → Hom (vg i) (bg i)}
            {f : (k : Σ I J) → Hom (vf k) (bf k)} →
            -- and their relation under composition
            (h ∘ g) ∘ f ≈[ Σ-assoc ] h ∘ (λ i → g i ∘ curry f i)

    -- we also need that _≈[_]_ is, in an appropriate sense, an equivalence relation, which in this case
    -- means that _≈[ id↔ ]_ is.  In other words, we don't care when transport is over 'something else'.
    refl≈ : {I : Set ı} {aₙ : I → Obj} {a : Obj} →
            {h : Hom {I} aₙ a} → h ≈[ id↔ ] h
    sym≈ : {I : Set ı} {aₙ : I → Obj} {a : Obj} →
           {g h : Hom {I} aₙ a} → g ≈[ id↔ ] h → h ≈[ id↔ ] g
    trans≈ : {I : Set ı} {aₙ : I → Obj} {a : Obj} →
           {f g h : Hom {I} aₙ a} → f ≈[ id↔ ] g → g ≈[ id↔ ] h → f ≈[ id↔ ] h

    -- we probably need ∘-resp-≈ too.

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


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

open import HoTT
open import cohomology.FunctionOver
open import cohomology.FlipPushout

module cohomology.CofiberSequence {i} where

{- Lemma: pushing flip-susp through susp-fmap -}
⊙flip-susp-fmap : {X Y : Ptd i} (f : fst (X ⊙→ Y))
  → ⊙flip-susp Y ⊙∘ ⊙susp-fmap f == ⊙susp-fmap f ⊙∘ ⊙flip-susp X
⊙flip-susp-fmap {X = X} (f , idp) = ⊙λ= lemma-fst lemma-snd
  where
  lemma-fst : ∀ σ →
    flip-susp (susp-fmap f σ) == susp-fmap f (flip-susp σ)
  lemma-fst = Suspension-elim _ idp idp $ λ y → ↓-='-in $
    ap-∘ (susp-fmap f) flip-susp (merid _ y)
    ∙ ap (ap (susp-fmap f)) (FlipSusp.glue-β y)
    ∙ ap-! (susp-fmap f) (merid _ y)
    ∙ ap ! (SuspFmap.glue-β f y)
    ∙ ! (FlipSusp.glue-β (f y))
    ∙ ! (ap (ap flip-susp) (SuspFmap.glue-β f y))
    ∙ ∘-ap flip-susp (susp-fmap f) (merid _ y)

  lemma-snd :
    ! (merid _ (f (snd X))) == ap (susp-fmap f) (! (merid _ (snd X))) ∙ idp
  lemma-snd =
     ap ! (! (SuspFmap.glue-β f (snd X)))
     ∙ !-ap (susp-fmap f) (merid _ (snd X))
     ∙ ! (∙-unit-r _)

{- Useful abbreviations -}
module _ {X Y : Ptd i} (f : fst (X ⊙→ Y)) where

  ⊙Cof² = ⊙Cof (⊙cfcod f)
  ⊙cfcod² = ⊙cfcod (⊙cfcod f)
  ⊙Cof³ = ⊙Cof ⊙cfcod²
  ⊙cfcod³ = ⊙cfcod ⊙cfcod²
  ⊙Cof⁴ = ⊙Cof ⊙cfcod³
  ⊙cfcod⁴ = ⊙cfcod ⊙cfcod³

{- For [f : X → Y], the cofiber space [Cof(cfcod f)] is equivalent to
 - [Suspension X]. This is essentially an application of the two pushouts
 - lemma:
 -
 -       f
 -   X ––––> Y ––––––––––––––> ∙
 -   |       |                 |
 -   |       |cfcod f          |
 -   v       v                 v
 -   ∙ ––> Cof f ––––––––––> Cof² f
 -                cfcod² f
 -
 - The map [cfcod² f : Cof f → Cof² f] becomes [ext-glue : Cof f → ΣX],
 - and the map [ext-glue : Cof² f → ΣY] becomes [susp-fmap f : ΣX → ΣY].
 -}
module Cof² {X Y : Ptd i} (f : fst (X ⊙→ Y)) where

  module Equiv {X Y : Ptd i} (f : fst (X ⊙→ Y)) where

    module Into = CofiberRec (cfcod (fst f)) {C = fst (⊙Susp X)}
      (south _) ext-glue (λ _ → idp)

    into = Into.f

    module Out = SuspensionRec (fst X) {C = fst (⊙Cof² f)}
      (cfcod _ (cfbase _)) (cfbase _)
      (λ x → ap (cfcod _) (cfglue _ x) ∙ ! (cfglue _ (fst f x)))

    out = Out.f

    into-out : ∀ σ → into (out σ) == σ
    into-out = Suspension-elim (fst X) idp idp
      (λ x → ↓-∘=idf-in into out $
        ap (ap into) (Out.glue-β x)
        ∙ ap-∙ into (ap (cfcod _) (cfglue _ x)) (! (cfglue _ (fst f x)))
        ∙ ap (λ w → ap into (ap (cfcod _) (cfglue _ x)) ∙ w)
             (ap-! into (cfglue _ (fst f x)) ∙ ap ! (Into.glue-β (fst f x)))
        ∙ ∙-unit-r _
        ∙ ∘-ap into (cfcod _) (cfglue _ x) ∙ ExtGlue.glue-β x)

    out-into : ∀ κ → out (into κ) == κ
    out-into = Cofiber-elim (cfcod (fst f))
      idp
      (Cofiber-elim (fst f) idp (cfglue _)
        (λ x → ↓-='-from-square $
          (ap-∘ out ext-glue (cfglue _ x)
           ∙ ap (ap out) (ExtGlue.glue-β x) ∙ Out.glue-β x)
          ∙v⊡ (vid-square {p = ap (cfcod _) (cfglue _ x)}
               ⊡h rt-square (cfglue _ (fst f x)))
          ⊡v∙ ∙-unit-r _))
      (λ y → ↓-∘=idf-from-square out into $
         ap (ap out) (Into.glue-β y) ∙v⊡ connection)

    eq = equiv into out into-out out-into

    space-path : ⊙Cof² f == ⊙Susp X
    space-path = ⊙ua eq (! (merid _ (snd X)))

  cfcod²-over : ⊙cfcod² f == ⊙ext-glue
                [ (λ U → fst (⊙Cof f ⊙→ U)) ↓ Equiv.space-path f ]
  cfcod²-over = ind-lemma f
    where
    {- is there a better way to handle this? -}
    ind-lemma : {X Y : Ptd i} (f : fst (X ⊙→ Y))
      → ⊙cfcod² f == ⊙ext-glue
        [ (λ U → fst (⊙Cof f ⊙→ U)) ↓ Equiv.space-path f ]
    ind-lemma {X = X} (f , idp) =
      codomain-over-⊙equiv (⊙cfcod² (f , idp)) _ _
      ▹ pair= idp (l snd-lemma)
      where
      x₀ = snd X; y₀ = f (snd X); F = (f , idp {a = y₀})

      snd-lemma : ap (Equiv.into F)
                     (ap (cfcod (cfcod f)) (! (! (cfglue _ x₀)))
                      ∙ ! (cfglue _ y₀))
                  == merid _ x₀
      snd-lemma =
        ap (Equiv.into F)
           (ap (cfcod (cfcod f)) (! (! (cfglue _ x₀))) ∙ ! (cfglue _ y₀))
          =⟨ !-! (cfglue _ x₀) |in-ctx (λ w →
               ap (Equiv.into F) (ap (cfcod (cfcod f)) w ∙ ! (cfglue _ y₀))) ⟩
        ap (Equiv.into F)
           (ap (cfcod (cfcod f)) (cfglue _ x₀) ∙ ! (cfglue _ y₀))
          =⟨ ap-∙ (Equiv.into F)
               (ap (cfcod (cfcod f)) (cfglue _ x₀)) (! (cfglue _ y₀)) ⟩
        ap (Equiv.into F) (ap (cfcod (cfcod f)) (cfglue _ x₀))
        ∙ ap (Equiv.into F) (! (cfglue _ y₀))
          =⟨ ∘-ap (Equiv.into F) (cfcod (cfcod f)) (cfglue _ x₀)
             |in-ctx (λ w → w ∙ ap (Equiv.into F) (! (cfglue _ y₀))) ⟩
        ap ext-glue (cfglue _ x₀) ∙ ap (Equiv.into F) (! (cfglue _ y₀))
          =⟨ ExtGlue.glue-β x₀
             |in-ctx (λ w → w ∙ ap (Equiv.into F) (! (cfglue _ y₀))) ⟩
        merid _ x₀ ∙ ap (Equiv.into F) (! (cfglue _ y₀))
          =⟨ ap-! (Equiv.into F) (cfglue _ y₀) |in-ctx (λ w → merid _ x₀ ∙ w) ⟩
        merid _ x₀ ∙ ! (ap (Equiv.into F) (cfglue _ y₀))
          =⟨ Equiv.Into.glue-β F y₀ |in-ctx (λ w → merid _ x₀ ∙ ! w) ⟩
        merid _ x₀ ∙ idp
          =⟨ ∙-unit-r _ ⟩
        merid _ x₀ ∎

      l : ∀ {i} {A : Type i} {x y : A} {p q : x == y}
        → p == q → p ∙ ! q == idp
      l {p = p} {q = q} α = ap (λ r → r ∙ ! q) α ∙ !-inv-r q

  cfcod³-over :
    ⊙ext-glue == ⊙flip-susp Y ⊙∘ ⊙susp-fmap f
    [ (λ U → fst (U ⊙→ ⊙Susp Y)) ↓ Equiv.space-path f ]
  cfcod³-over =
    ⊙λ= fst-lemma (l snd-lemma)
    ◃ domain-over-⊙equiv (⊙flip-susp Y ⊙∘ ⊙susp-fmap f) _ _
    where
    fst-lemma : (κ : fst (⊙Cof² f))
      → ext-glue κ == flip-pushout (susp-fmap (fst f) (Equiv.into f κ))
    fst-lemma = Cofiber-elim (cfcod (fst f))
      idp
      (Cofiber-elim (fst f)
        idp
        (! ∘ merid (fst Y))
        (λ x → ↓-='-from-square $
          ap-cst (south _) (cfglue _ x) ∙v⊡
            connection
          ⊡v∙ ! (ap-∘ (flip-pushout ∘ susp-fmap (fst f)) ext-glue (cfglue _ x)
                 ∙ ap (ap (flip-pushout ∘ susp-fmap (fst f))) (ExtGlue.glue-β x)
                 ∙ ap-∘ flip-pushout (susp-fmap (fst f)) (merid _ x)
                 ∙ ap (ap flip-pushout) (SuspFmap.glue-β (fst f) x)
                 ∙ FlipPushout.glue-β (fst f x))))
      (λ y → ↓-='-from-square $
        ExtGlue.glue-β y ∙v⊡
          tr-square (merid _ y)
        ⊡v∙ ! (ap-∘ (flip-pushout ∘ susp-fmap (fst f)) (Equiv.into f)
                    (cfglue _ y)
               ∙ ap (ap (flip-pushout ∘ susp-fmap (fst f)))
                    (Equiv.Into.glue-β f y)))

    snd-lemma : ap (flip-pushout ∘ susp-fmap (fst f)) (! (merid _ (snd X)))
                == merid _ (snd Y)
    snd-lemma =
      ap (flip-pushout ∘ susp-fmap (fst f)) (! (merid _ (snd X)))
        =⟨ ap-! (flip-pushout ∘ susp-fmap (fst f)) (merid _ (snd X)) ⟩
      ! (ap (flip-pushout ∘ susp-fmap (fst f)) (merid _ (snd X)))
        =⟨ ap ! (ap-∘ flip-pushout (susp-fmap (fst f)) (merid _ (snd X))) ⟩
      ! (ap flip-pushout (ap (susp-fmap (fst f)) (merid _ (snd X))))
        =⟨ ap (! ∘ ap flip-pushout) (SuspFmap.glue-β (fst f) (snd X)) ⟩
      ! (ap flip-pushout (merid _ (fst f (snd X))))
        =⟨ ap ! (FlipPushout.glue-β (fst f (snd X))) ⟩
      ! (! (merid _ (fst f (snd X))))
        =⟨ !-! (merid _ (fst f (snd X))) ⟩
      merid _ (fst f (snd X))
        =⟨ ap (merid _) (snd f) ⟩
      merid _ (snd Y) ∎

    l : ∀ {i} {A : Type i} {x y : A} {p q : x == y}
      → p == q → idp == p ∙ ! q
    l {p = p} {q = q} α = ! (!-inv-r p) ∙ ap (λ w → p ∙ ! w) α

  open Equiv f public

  full-path : Path
    {A = Σ (Ptd i) (λ U → fst (⊙Cof f ⊙→ U) × fst (U ⊙→ ⊙Susp Y))}
    (_ , ⊙cfcod² f , ⊙ext-glue)
    (_ , ⊙ext-glue , ⊙flip-susp Y ⊙∘ ⊙susp-fmap f)
  full-path = pair= space-path (↓-×-in cfcod²-over cfcod³-over)

cofiber-sequence : {X Y : Ptd i} (f : fst (X ⊙→ Y)) → Path
  {A = Σ (Ptd i × Ptd i × Ptd i)
         (λ {(U , V , W) → fst (⊙Cof f ⊙→ U) × fst (U ⊙→ V) × fst (V ⊙→ W)})}
  (_ , ⊙cfcod² f , ⊙cfcod³ f , ⊙cfcod⁴ f)
  (_ , ⊙ext-glue , ⊙susp-fmap f , ⊙susp-fmap (⊙cfcod f))
cofiber-sequence {Y = Y} f =
    ap (λ {(_ , g , _) → (_ , ⊙cfcod² f , ⊙cfcod³ f , g)})
       (Cof².full-path (⊙cfcod² f))
  ∙ ap (λ {(_ , g , h) → (_ , ⊙cfcod² f , g , h)})
       (Cof².full-path (⊙cfcod f))
  ∙ ap (λ {(_ , g , h) → (_ , g , h , ⊙flip-susp (⊙Cof f) ⊙∘
                                      ⊙susp-fmap (⊙cfcod f))})
       (Cof².full-path f)
  ∙ ap (λ g → (_ , ⊙ext-glue , ⊙flip-susp Y ⊙∘ ⊙susp-fmap f , g))
       (⊙flip-susp-fmap (⊙cfcod f))
  ∙ ap (λ {(_ , g , h) → (_ , ⊙ext-glue , g , h)})
       (pair= (flip-⊙pushout-path (suspension-⊙span Y))
          (↓-×-in (codomain-over-⊙equiv
                    (⊙flip-susp Y ⊙∘ ⊙susp-fmap f) _ _
                   ▹ lemma)
                  (domain-over-⊙equiv (⊙susp-fmap (⊙cfcod f)) _ _)))
  where
  lemma : ⊙flip-susp Y ⊙∘ ⊙flip-susp Y ⊙∘ ⊙susp-fmap f
       == ⊙susp-fmap f
  lemma = ! (⊙∘-assoc (⊙flip-susp Y) (⊙flip-susp Y) (⊙susp-fmap f))
          ∙ ap (λ w → w ⊙∘ ⊙susp-fmap f)
               (flip-⊙pushout-involutive (suspension-⊙span Y))
          ∙ ⊙∘-unit-l (⊙susp-fmap f)

suspend-cofiber : {X Y : Ptd i} (f : fst (X ⊙→ Y)) → Path
  {A = Σ _ (λ {(U , V , W) → fst (U ⊙→ V) × fst (V ⊙→ W)})}
  (_ , ⊙susp-fmap f , ⊙cfcod (⊙susp-fmap f))
  (_ , ⊙susp-fmap f , ⊙susp-fmap (⊙cfcod f))
suspend-cofiber f =
  ap (λ {((U , V , W) , _ , g , _) → ((U , V , ⊙Cof g) , g , ⊙cfcod g)})
     (! (cofiber-sequence f))
  ∙ ap (λ {(_ , _ , g , h) → (_ , g , h)}) (cofiber-sequence f)

suspend^-cof= : {X Y Z : Ptd i} (m : ℕ) (f : fst (X ⊙→ Y)) (g : fst (Y ⊙→ Z))
  (p : Path {A = Σ _ (λ U → fst (Y ⊙→ U))} (⊙Cof f , ⊙cfcod f) (Z , g))
  → Path {A = Σ _ (λ {(U , V , W) → fst (U ⊙→ V) × fst (V ⊙→ W)})}
    (_ , ⊙susp^-fmap m f , ⊙cfcod (⊙susp^-fmap m f))
    (_ , ⊙susp^-fmap m f , ⊙susp^-fmap m g)
suspend^-cof= O f g p = ap (λ {(_ , h) → (_ , f , h)}) p
suspend^-cof= (S m) f g p =
  suspend-cofiber (⊙susp^-fmap m f)
  ∙ ap (λ {(_ , h , k) → (_ , ⊙susp-fmap h , ⊙susp-fmap k)})
       (suspend^-cof= m f g p)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


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

open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Fields.Fields
open import Rings.Orders.Total.Definition
open import Rings.Orders.Total.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Orders.LeastUpperBounds.Definition
open import Fields.Orders.Total.Definition

module Numbers.ClassicalReals.RealField where

record RealField : Agda.Primitive.Setω where
  field
    a b c : _
    A : Set a
    S : Setoid {_} {b} A
    _+_ : A → A → A
    _*_ : A → A → A
    R : Ring S _+_ _*_
    F : Field R
    _<_ : Rel {_} {c} A
    pOrder : SetoidPartialOrder S _<_
    pOrderedRing : PartiallyOrderedRing R pOrder
    orderedRing : TotallyOrderedRing pOrderedRing
    lub : {d : _} → {pred : A → Set d} → (sub : subset S pred) → (nonempty : Sg A pred) → (boundedAbove : Sg A (UpperBound pOrder sub)) → Sg A (LeastUpperBound pOrder sub)
  open Setoid S
  open Field F
  charNot2 : (Ring.1R R + Ring.1R R) ∼ Ring.0R R → False
  charNot2 = orderedImpliesCharNot2 orderedRing nontrivial
  oField : TotallyOrderedField F pOrderedRing
  oField = record { oRing = orderedRing }


text:
{-# OPTIONS --cubical-compatible --show-implicit #-}
-- {-# OPTIONS -v tc.lhs.split.well-formed:100 #-}
-- Andreas, adapted from Andres Sicard, 2013-05-29
module WithoutKRestrictive where

open import Common.Level
open import Common.Equality
open import Common.Product

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n} → zero ≤ n
  s≤s : ∀ {n m} → n ≤ m → suc n ≤ suc m

_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

refl≤ : ∀ (n : ℕ) → n ≤ n
refl≤ zero    = z≤n
refl≤ (suc n) = s≤s (refl≤ n)

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

length : {A : Set} → List A → ℕ
length []       = zero
length (x ∷ xs) = suc (length xs)

P : {A : Set} → List A → List A → Set
P xs ys = Σ _ (λ x → ys ≡ (x ∷ xs))

Q : {A : Set} → List A → List A → Set
Q xs ys = (length xs) < (length ys)

helper : {A : Set}(y : A)(xs : List A) → (length xs) < (length (y ∷ xs))
helper y []       = s≤s z≤n
helper y (x ∷ xs) = s≤s (refl≤ _)

-- Why the --cubical-compatible option rejects the following proof

foo : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
foo xs .(x ∷ xs) (x , refl) = helper x xs

-- if I can prove foo using only subst

foo' : {A : Set}(xs ys : List A) → P xs ys → Q xs ys
foo' xs ys (x , h) =
  subst (λ ys' → length xs < length ys') (sym h) (helper x xs)


text:
-- Run this test case in safe mode
-- {-# OPTIONS --safe #-} -- does not parse (2012-03-12 Andreas)
module Issue586 where

Foo : Set1
Foo = Set


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

open import Prelude
open import Algebra

module Data.FingerTree {ℓ} (mon : Monoid ℓ) where

open Monoid mon

record Measured {a} (A : Type a) : Type (a ℓ⊔ ℓ) where
  constructor measured
  field μ : A → 𝑆

open Measured ⦃ ... ⦄ public

data Digit {a} (A : Type a) : Type a where
  D₁ : A → Digit A
  D₂ : A → A → Digit A
  D₃ : A → A → A → Digit A

data Node {a} (A : Type a) : Type a where
  N₂ : A → A → Node A
  N₃ : A → A → A → Node A

instance
  measuredDigit : ⦃ _ : Measured A ⦄ → Measured (Digit A)
  measuredDigit =
    measured λ { (D₁ x) → μ x
               ; (D₂ x x₁) → μ x ∙ μ x₁
               ; (D₃ x x₁ x₂) → μ x ∙ μ x₁ ∙ μ x₂
               }

instance
  measuredNode : ⦃ _ : Measured A ⦄ → Measured (Node A)
  measuredNode =
    measured λ { (N₂ x x₁) → μ x ∙ μ x₁
               ; (N₃ x x₁ x₂) → μ x ∙ μ x₁ ∙ μ x₂
               }

record ⟪_⟫ (A : Type a) ⦃ _ : Measured A ⦄ : Type (a ℓ⊔ ℓ) where
  constructor recd
  field
    val : A
    mem : 𝑆
    prf : μ val ≡ mem
open ⟪_⟫ public

memo : ⦃ _ : Measured A ⦄ → A → ⟪ A ⟫
memo x = recd x (μ x) refl

instance
  measuredMemo : ⦃ _ : Measured A ⦄ → Measured ⟪ A ⟫
  measuredMemo = measured mem

mutual
  record Deep {a} (A : Type a) ⦃ _ : Measured A ⦄ : Type (a ℓ⊔ ℓ) where
    pattern
    constructor more
    inductive
    field
      lbuff : Digit A
      tree  : Tree ⟪ Node A ⟫
      rbuff : Digit A

  data Tree {a} (A : Type a) ⦃ _ : Measured A ⦄ : Type (a ℓ⊔ ℓ) where
    empty : Tree A
    single : A → Tree A
    deep : ⟪ Deep A ⟫  → Tree A

  μ-deep : ∀ {a} {A : Type a} ⦃ _ : Measured A ⦄ → Deep A → 𝑆
  μ-deep (more l x r) = μ l ∙ (μ-tree x ∙ μ r)

  μ-tree : ∀ {a} {A : Type a} ⦃ _ : Measured A ⦄ → Tree A → 𝑆
  μ-tree empty = ε
  μ-tree (single x) = μ x
  μ-tree (deep xs) = xs .mem

  instance
    Measured-Deep : ∀ {a} {A : Type a} → ⦃ _ : Measured A ⦄ → Measured (Deep A)
    Measured-Deep = measured μ-deep

  instance
    Measured-Tree : ∀ {a} {A : Type a} → ⦃ _ : Measured A ⦄ → Measured (Tree A)
    Measured-Tree = measured μ-tree
open Deep

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

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

open import LibraBFT.Abstract.Types

-- This module defines the types used to define a SystemModel.

module LibraBFT.Yasm.Base where

 -- Our system is configured through a value of type
 -- SystemParameters where we specify:
 record SystemParameters : Set₁ where
  constructor mkSysParms
  field
    PeerState : Set
    Msg       : Set
    Part      : Set -- Types of interest that can be represented in Msgs

    -- The messages must be able to carry signatures
    instance Part-sig : WithSig Part

    -- A relation specifying what Parts are included in a Msg.
    _⊂Msg_       : Part → Msg → Set

    -- Finally, messages must carry an epoch id and might have an author
    part-epoch  : Part → EpochId

    -- Initializes a potentially-empty state with an EpochConfig
    init : NodeId → EpochConfig → Maybe PeerState → PeerState × List Msg

    -- Handles a message on a previously initialized peer.
    handle : NodeId → Msg → PeerState → PeerState × List Msg

    -- TODO-3?: So far, handlers only produce messages to be sent.
    -- It would be reasonable to generalize this to something like
    --
    --   data Action = Send Msg | Crash CrashMsg | Log LogMsg | ...
    --
    -- on the system level, and have the handlers return List Action,
    -- rather than just ListMsg.  For example, if an assertion fires, this
    -- could "kill the process" and make it not send any messages in the future.
    -- We could also then prove that the handlers do not crash, certain
    -- messages are logged under certain circumstances, etc.
    --
    -- Alternatively, we could keep this outside the system model by
    -- defining an application-specific peerState type, for example:
    --
    -- > libraHandle : Msg → Status × Log × LState → Status × LState × List Action
    -- > libraHandle _ (Crashed , l , s) = Crashed , s , [] -- i.e., crashed peers never send messages
    -- >
    -- > handle = filter isSend ∘ libraHandle

 -- We also require a standard key-value store interface, along with its
 -- functionality and various properties about it.  Most of the properties
 -- are not currently used, but they are included here based on our
 -- experience in other work, as we think many of them will be needed when
 -- reasoning about an actual LibraBFT implementation.

 -- Although we believe the assumptions here are reasonable, it is always
 -- possible that we made a mistake in postulating one of the properties,
 -- making it impossible to implement.  Thus, it would a useful contribution
 -- to:
 --
 -- TODO-1: construct an actual implementation and provide and prove the
 -- necessary properties to satisfy the requirements of this module
 --
 -- Note that this would require some work, but should be relatively
 -- straightforward and requires only "local" changes.

 postulate
   Map        : Set → Set → Set
   Map-empty  : ∀{k v} → Map k v
   Map-lookup : ∀{k v} → k → Map k v → Maybe v
   Map-insert : ∀{k v} → k → v → Map k v → Map k v
   Map-set    : ∀{k v} → k → Maybe v → Map k v → Map k v

   -- It must satisfy the following properties
   Map-insert-correct  : ∀ {K V : Set}{k : K}{v : V}{m : Map K V}
                       → Map-lookup k (Map-insert k v m) ≡ just v

   Map-insert-target-≢ : ∀ {K V : Set}{k k' : K}{v : V}{m}
                       → k' ≢ k
                       → Map-lookup k' m ≡ Map-lookup k' (Map-insert k v m)

   Map-set-correct     : ∀ {K V : Set}{k : K}{mv : Maybe V}{m : Map K V}
                       → Map-lookup k (Map-set k mv m) ≡ mv

   Map-set-target-≢    : ∀ {K V : Set}{k k' : K}{mv : Maybe V}{m}
                       → k' ≢ k
                       → Map-lookup k' m ≡ Map-lookup k' (Map-set k mv m)

   Map-set-≡-correct   : ∀ {K V : Set}{k : K}{m : Map K V}
                       → Map-set k (Map-lookup k m) m ≡ m


text:
{-# OPTIONS --universe-polymorphism #-}

open import Categories.Category

module Categories.Object.Products {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level

import Categories.Object.Terminal as Terminal
import Categories.Object.BinaryProducts as BinaryProducts

open Terminal C
open BinaryProducts C

-- this should really be 'FiniteProducts', no?
record Products : Set (o ⊔ ℓ ⊔ e) where
  field
    terminal : Terminal
    binary : BinaryProducts

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --without-K #-}
module Relation.Path.Operation where

open import Basics
open import Relation.Equality
open import Data.Product

infixr 4 _∙_
infix 9 _⁻¹

-- Path inversion
_⁻¹ : ∀ {a}{A : Set a}{x y : A} → (x ≡ y) → (y ≡ x)
_⁻¹ = ind₌ (λ x y _ → y ≡ x) (λ _ → refl) _ _

-- Composition of paths
_∙_ : ∀ {a}{A : Set a}{x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_∙_ {z = z} = ind₌ (λ x y _ → y ≡ z → x ≡ z) (λ _ p → p) _ _

-- Unit laws for Composition

rup : ∀ {i}{A : Set i}{a b : A} → (p : a ≡ b) → (p ∙ refl) ≡ p
rup = ind₌ (λ _ _ p → (p ∙ refl) ≡ p) (λ _ → refl) _ _

lup : ∀ {i}{A : Set i}{a b : A} → (p : a ≡ b) → (refl ∙ p) ≡ p
lup _ = refl

-- Associativity of path composition
assoc : ∀ {i}{A : Set i}{a b c d : A} → (p : a ≡ b) (q : b ≡ c) (r : c ≡ d) → (p ∙ (q ∙ r)) ≡ ((p ∙ q) ∙ r)
assoc {c = c} {d = d} = ind₌
  (λ _ b p → (q : b ≡ c) (r : c ≡ d) → (p ∙ q ∙ r) ≡ ((p ∙ q) ∙ r))
  (λ b → ind₌
    (λ _ c q → (r : c ≡ d) → (refl ∙ q ∙ r) ≡ ((refl ∙ q) ∙ r))
    (λ _ _ → refl) _ _)
    _ _

-- It is a familiar fact in topology that when we concatenate a path p with the
-- reversed path p ⁻¹, we don’t literally obtain a constant path (which
-- corresponds to the equality refl in type theory) — instead we have a
-- homotopy, or higher path, from p ∙ p ⁻¹ to the constant path.

there-and-back-again : ∀ {i} {A : Set i}{x y : A}{p : x ≡ y} → (p ∙ p ⁻¹) ≡ refl
there-and-back-again {i} {A} {x}{y} {p} = ind₌ D d _ _ p where
  D : (x y : A) → (x ≡ y) → Set i
  D x y p = (p ∙ p ⁻¹) ≡ refl

  d : (x₁ : A) → D x₁ x₁ refl
  d = λ x → refl

back-and-there-again : ∀ {i}{A : Set i}{x y : A}{p : x ≡ y} → (p ⁻¹ ∙ p) ≡ refl
back-and-there-again {i} {A} {x}{y} {p} = ind₌ D d _ _ p where
  D : (x y : A) → (p : x ≡ y) → Set i
  D x y p = (p ⁻¹ ∙ p) ≡ refl

  d : (x₁ : A) → D x₁ x₁ refl
  d = λ x → refl

-- Paths are functor looking things.
ap : ∀ {i j} {A : Set i}{B : Set j}{x y : A}{f : A → B} → (x ≡ y) → (f x ≡ f y)
ap {i}{j} {A}{B} {x}{y}{f} p = ind₌ D d x y p where
  D : (x y : A) → (p : x ≡ y) → Set j
  D x y p = f x ≡ f y

  d : (x : A) → D x x refl
  d = λ x → refl

--
ap₂ : ∀ {i j k} {A : Set i}{B : Set j}{C : Set k}{x x′ : A}{y y′ : B}(f : A → B → C) → (x ≡ x′) → (y ≡ y′) → (f x y ≡ f x′ y′)
ap₂ f p q = ap {f = λ _ → f _ _} p ∙ ap {f = f _} q

-- The dependently typed version of `ap` takes a type family and relates its instantiations with p
transport : ∀ {i j} {A : Set i}{P : A → Set j}{x y : A} → (p : x ≡ y) → P x → P y
transport {i}{j} {A}{P} {x}{y} p = ind₌ D d x y p where
    D : (x y : A) → (p : x ≡ y) → Set j
    D x y p = P x → P y

    d : (x : A) → D x x refl
    d = λ x → id

2-11-2 : ∀ {i} {A : Set i} → (a : A) {x₁ x₂ : A} (p : x₁ ≡ x₂) (q : a ≡ x₁) → (transport p q) ≡ (q ∙ p)
2-11-2 a = ind₌
  (λ x _ p → (q : a ≡ x) → (transport {P = (λ x → a ≡ x)} p q) ≡ (q ∙ p))
  (λ _ q → rup q ⁻¹)
  _ _

-- Basically, P respects equality
path-lifting : ∀ {a p}{A : Set a}{x y : A}{P : A → Set p} → (u : P x) → (p : x ≡ y) → (x , u) ≡ (y , u)
path-lifting u = cong (λ z → z , u)

-- Look, transport works in the "upper" space too!
apd : ∀ {i} {A : Set i}{P : A → Set i}{f : (x : A) → P x}{x y : A} → (p : x ≡ y) → (transport p (f x) ≡ f y)
apd {i} {A}{P} {f}{x}{y} p = ind₌ D d x y p where
  D : (x y : A) → (p : x ≡ y) → Set i
  D x y p = transport p (f x) ≡ f y

  d : (x : A) → D x x refl
  d = λ x → refl

-- We can also fix B and make transport work like fmap with equalities.
transportconst : ∀ {i} {A : Set i}{B : Set i}{P : A → B}{x y : A} → (p : x ≡ y) → (b : B) → transport p b ≡ b
transportconst {i} {A}{B}{P} {x}{y} p b = ind₌ D d x y p where
  D : (x y : A) → (x ≡ y) → Set i
  D x y p = transport p b ≡ b

  d : (x : A) → D x x refl
  d = λ x → refl

-- Path Structure for Product Types
split-path₌ : ∀ {a b}{A : Set a}{B : Set b} → (x y : (A × B)) → (x ≡ y) → (proj₁ x ≡ proj₁ y) × (proj₂ x ≡ proj₂ y)
split-path₌ xs ys p = ap {f = proj₁} p , ap {f = proj₂} p

{-
pair₌ : ∀ {a b}{A : Set a}{B : Set b} → (x y : (A × B)) → (proj₁ x ≡ proj₁ y) × (proj₂ x ≡ proj₂ y) → (x ≡ y)
pair₌ (a₁ , b₁) (a₂ , b₂) (p , q) = {!!}
-}

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A solver for proving that one list is a sublist of the other for types
-- which enjoy decidable equalities.
------------------------------------------------------------------------

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

open import Relation.Binary using (Decidable)
open import Agda.Builtin.Equality using (_≡_)

module Data.List.Relation.Binary.Sublist.DecPropositional.Solver
       {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
       where

import Relation.Binary.PropositionalEquality as P

open import Data.List.Relation.Binary.Sublist.DecSetoid.Solver (P.decSetoid _≟_) public


text:
open import Agda.Primitive

record R (a : Level) : Set (lsuc a) where
  field
    A : Set a

_ : ∀ a → R {!a!} → Set a
_ = λ _ → R.A

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --cubical --no-import-sorts #-}

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

module MoreNatProperties where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)

open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
open import Function.Base using (_$_)

open import Cubical.Data.Nat hiding (min)
-- open import Cubical.Data.Nat.Properties hiding (min)
open import Cubical.Data.Nat.Order renaming (zero-≤ to z≤n; suc-≤-suc to s≤s)

min : ℕ → ℕ → ℕ
min a b with a ≟ b
... | lt a<b = a
... | eq a≡b = a
... | gt b<a = b

max : ℕ → ℕ → ℕ
max a b with a ≟ b
... | lt a<b = b
... | eq a≡b = a
... | gt b<a = a

-- to make use of `it` to find proofs for `Fin k`:
module FinInstances where
  open import Function.Base using (it) public
  instance
    z≤n' : ∀ {n}                 → zero  ≤ n
    z≤n' {n} = z≤n
    s≤s' : ∀ {m n} {{m≤n : m ≤ n}} → suc m ≤ suc n
    s≤s' {m} {n} {{m≤n}} = s≤s m≤n

¬1<0 : ¬(1 < 0)
¬1<0 (k , p) = snotz (sym (+-suc k 1) ∙ p)

suc-preserves-< : ∀{x y} → x < y → suc x < suc y
suc-preserves-< {x} {y} p = s≤s p
suc-reflects-< : ∀{x y} → suc x < suc y → x < y
suc-reflects-< {x} {y} (k , p) = k , (injSuc (sym (+-suc k (suc x)) ∙ p))

¬[k+x<k] : ∀ k x → ¬(k + x < k)
¬[k+x<k] k x (z , p) = snotz $ sym $ inj-m+ {k} {0} (+-zero k ∙ sym p ∙ +-suc z (k + x) ∙ (λ i → suc (+-comm z (k + x) i)) ∙ (λ i → suc (+-assoc k x z (~ i))) ∙ sym (+-suc k (x + z)))

-- import MoreLogic
open import MoreLogic.Reasoning

<-asymʷ : ∀ a b → a < b → ¬(b < a)
<-asymʷ a b a<b = ¬m<m ∘ <-trans a<b

{-
<-asym : ∀ a b → a < b → ¬(b < a)
<-asym a b (k , p) (l , q) = snotz $ inj-m+ {a} ((sym γ ∙ transport (λ i → l + suc (p (~ i)) ≡ a) q) ∙ sym (+-zero a))
  where
    γ = (
      l + suc (k + suc a)   ≡⟨ ( λ i → l + suc (+-suc k a i)) ⟩
      l + suc (suc (k + a)) ≡⟨ ( λ i → l + suc (suc (+-comm k a i)) ) ⟩
      l + suc (suc (a + k)) ≡⟨ ( λ i → l + suc (+-suc a k (~ i))) ⟩
      l + suc (a + suc k)   ≡⟨ ( λ i → l + (+-suc a (suc k) (~ i))) ⟩
      l + (a + suc (suc k)) ≡⟨ +-assoc l a (suc (suc k)) ⟩
      (l + a) + suc (suc k) ≡⟨ (λ i → +-comm l a i + suc (suc k) ) ⟩
      (a + l) + suc (suc k) ≡⟨ sym $ +-assoc a l (suc (suc k)) ⟩
      a + (l + suc (suc k)) ≡⟨ (λ i → a + +-suc l (suc k) i) ⟩
      a + suc (l + suc k)   ∎)
-}

<>-implies-≡ : ∀ a b → a ≤ b → b ≤ a → a ≡ b
<>-implies-≡ a b (n , p) (m , q) with m+n≡0→m≡0×n≡0 {m} {n} (m+n≡n→m≡0 γ)
  where γ = sym (+-assoc m n a) ∙ (λ i → m + p i) ∙ q
... | m≡0 , n≡0 = (λ i → n≡0 (~ i) + a) ∙ p

≟-sym : ∀ a b → Trichotomy a b → Trichotomy b a
≟-sym a b (lt x) = gt x
≟-sym a b (eq x) = eq (sym x)
≟-sym a b (gt x) = lt x

-- NOTE: this is an ingedience to disprove
--         isComplex ≤ₙₗ isRat
--       which normalizes to
--         Σ[ k ∈ ℕ ] k + 4 ≡ 2
--       and is the same as
--         4 ≤ 2
--       so more elegantly would be
--         ∀ x k → x < x + suc k
--       and turn this into
--         ∀ x k → ¬ (x + suc k ≤ x)
k+x+sy≢x : ∀ k x y → ¬(k + (x + suc y) ≡ x)
k+x+sy≢x k x y p = snotz $ sym (+-suc k y) ∙ inj-m+ {x} (+-assoc x k (suc y) ∙ (λ i → (+-comm x k) i + (suc y)) ∙ sym (+-assoc k x (suc y)) ∙ p ∙ sym (+-zero x))

0≤x : ∀ x → 0 ≤ x
0≤x zero =  0 , refl
0≤x (suc x) =  suc x , (λ i → suc (+-zero x i)) ∙ refl {x = suc x}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on the Stream type
------------------------------------------------------------------------

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

module Codata.Stream.Properties where

open import Size
open import Codata.Thunk using (Thunk; force)
open import Codata.Stream
open import Codata.Stream.Bisimilarity

open import Data.Nat.Base
open import Data.Nat.GeneralisedArithmetic using (fold; fold-pull)

import Data.Vec as Vec
import Data.Product as Prod

open import Function
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)

------------------------------------------------------------------------
-- repeat

module _ {a} {A : Set a} where

 lookup-repeat-identity : (n : ℕ) (a : A) → lookup n (repeat a) ≡ a
 lookup-repeat-identity zero    a = Eq.refl
 lookup-repeat-identity (suc n) a = lookup-repeat-identity n a

 take-repeat-identity : (n : ℕ) (a : A) → take n (repeat a) ≡ Vec.replicate a
 take-repeat-identity zero    a = Eq.refl
 take-repeat-identity (suc n) a = Eq.cong (a Vec.∷_) (take-repeat-identity n a)

module _ {a b} {A : Set a} {B : Set b} where

 map-repeat-commute : ∀ (f : A → B) a {i} → i ⊢ map f (repeat a) ≈ repeat (f a)
 map-repeat-commute f a = Eq.refl ∷ λ where .force → map-repeat-commute f a

 repeat-ap-identity : ∀ (f : A → B) as {i} → i ⊢ ap (repeat f) as ≈ map f as
 repeat-ap-identity f (a ∷ as) = Eq.refl ∷ λ where .force → repeat-ap-identity f (as .force)

 ap-repeat-identity : ∀ (fs : Stream (A → B) ∞) (a : A) {i} → i ⊢ ap fs (repeat a) ≈ map (_$ a) fs
 ap-repeat-identity (f ∷ fs) a = Eq.refl ∷ λ where .force → ap-repeat-identity (fs .force) a

 ap-repeat-commute : ∀ (f : A → B) a {i} → i ⊢ ap (repeat f) (repeat a) ≈ repeat (f a)
 ap-repeat-commute f a = Eq.refl ∷ λ where .force → ap-repeat-commute f a

------------------------------------------------------------------------
-- Functor laws

module _ {a} {A : Set a} where

 map-identity : ∀ (as : Stream A ∞) {i} → i ⊢ map id as ≈ as
 map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

 map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} → i ⊢ map g (map f as) ≈ map (g ∘ f) as
 map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)

------------------------------------------------------------------------
-- splitAt

module _ {a b} {A : Set a} {B : Set b} where

  splitAt-map : ∀ n (f : A → B) xs →
    splitAt n (map f xs) ≡ Prod.map (Vec.map f) (map f) (splitAt n xs)
  splitAt-map zero    f xs       = Eq.refl
  splitAt-map (suc n) f (x ∷ xs) =
    Eq.cong (Prod.map₁ (f x Vec.∷_)) (splitAt-map n f (xs .force))

------------------------------------------------------------------------
-- iterate

module _ {a} {A : Set a} where

  lookup-iterate-identity : ∀ n f (a : A) → lookup n (iterate f a) ≡ fold a f n
  lookup-iterate-identity zero     f a = Eq.refl
  lookup-iterate-identity (suc n)  f a = begin
    lookup (suc n) (iterate f a) ≡⟨⟩
    lookup n (iterate f (f a))   ≡⟨ lookup-iterate-identity n f (f a) ⟩
    fold (f a) f n               ≡⟨ fold-pull (const ∘′ f) (f a) Eq.refl (λ _ → Eq.refl) n ⟩
    f (fold a f n)               ≡⟨⟩
    fold a f (suc n)             ∎ where open Eq.≡-Reasoning