text:
-- Step-indexed logical relations based on functional big-step semantics.
--
-- Goal for now: just prove the fundamental theorem of logical relations,
-- relating a term to itself in a different environments.
--
-- But to betray the eventual goal, I can also relate integer values with a
-- change in the relation witness. That was a completely local change. But that
-- might also be because we only have few primitives.
--
-- Because of closures, we need relations across different terms with different
-- contexts and environments.
--
-- This development is strongly inspired by "Imperative self-adjusting
-- computation" (ISAC below), POPL'08, in preference to Dargaye and Leroy (2010), "A verified
-- framework for higher-order uncurrying optimizations", but I deviate
-- somewhere, especially to try following "Functional Big-Step Semantics"),
-- though I deviate somewhere.

-- In fact, this development is typed, hence some parts of the model are closer
-- to Ahmed (ESOP 2006), "Step-Indexed Syntactic Logical Relations for Recursive
-- and Quantified Types". But for many relevant aspects, the two papers are
-- interchangeable.
--
-- The main insight from the ISAC paper missing from the other one is how to
-- step-index a big-step semantics correctly: just ensure that the steps in the
-- big-step semantics agree with the ones in the small-step semantics. *Then*
-- everything just works with big-step semantics. Quite a few other details are
-- fiddly, but those are the same in small-step semantics.
--
-- CHEATS:
-- "Fuctional big-step semantics" requires an external termination proof for the
-- semantics. There it is also mechanized, here it isn't. Worse, the same
-- termination problem affects some lemmas about the semantics.

module Thesis.FunBigStepSILR2 where

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

data Type : Set where
  _⇒_ : (σ τ : Type) → Type
  nat : Type
infixr 20 _⇒_

⟦_⟧Type : Type → Set
⟦ σ ⇒ τ ⟧Type = ⟦ σ ⟧Type → ⟦ τ ⟧Type
⟦ nat ⟧Type = ℕ

open import Base.Syntax.Context Type public
open import Base.Syntax.Vars Type public

data Const : (τ : Type) → Set where
  lit : ℕ → Const nat
  -- succ : Const (int ⇒ int)

data Term (Γ : Context) :
  (τ : Type) → Set where
  -- constants aka. primitives
  const : ∀ {τ} →
    (c : Const τ) →
    Term Γ τ
  var : ∀ {τ} →
    (x : Var Γ τ) →
    Term Γ τ
  app : ∀ {σ τ}
    (s : Term Γ (σ ⇒ τ)) →
    (t : Term Γ σ) →
    Term Γ τ
  -- we use de Bruijn indices, so we don't need binding occurrences.
  abs : ∀ {σ τ}
    (t : Term (σ • Γ) τ) →
    Term Γ (σ ⇒ τ)

weaken : ∀ {Γ₁ Γ₂ τ} →
  (Γ₁≼Γ₂ : Γ₁ ≼ Γ₂) →
  Term Γ₁ τ →
  Term Γ₂ τ
weaken Γ₁≼Γ₂ (const c) = const c
weaken Γ₁≼Γ₂ (var x) = var (weaken-var Γ₁≼Γ₂ x)
weaken Γ₁≼Γ₂ (app s t) = app (weaken Γ₁≼Γ₂ s) (weaken Γ₁≼Γ₂ t)
weaken Γ₁≼Γ₂ (abs {σ} t) = abs (weaken (keep σ • Γ₁≼Γ₂) t)

data Val : Type → Set
open import Base.Denotation.Environment Type Val public
open import Base.Data.DependentList public

data Val where
  closure : ∀ {Γ σ τ} → (t : Term (σ • Γ) τ) → (ρ : ⟦ Γ ⟧Context) → Val (σ ⇒ τ)
  intV : ∀ (n : ℕ) → Val nat

import Base.Denotation.Environment
-- Den stands for Denotational semantics.
module Den = Base.Denotation.Environment Type ⟦_⟧Type

--
-- Functional big-step semantics
--

-- Termination is far from obvious to Agda once we use closures. So we use
-- step-indexing with a fuel value.

-- WARNING: ISAC's big-step semantics produces a step count as "output". But
-- that would not help Agda establish termination. That's only a problem for a
-- functional big-step semantics, not for a relational semantics.
--
-- So, instead, I tried to use a sort of writer monad: the interpreter gets fuel
-- and returns the remaining fuel. That's the same trick as in "functional
-- big-step semantics". That *makes* the function terminating, even though Agda
-- cannot see this because it does not know that the returned fuel is no bigger.

-- Since we focus for now on STLC, unlike that
-- paper, we could avoid error values because we keep types.
--
-- One could drop types and add error values instead.

data ErrVal (τ : Type) : Set where
  Done : (v : Val τ) → (n1 : ℕ) → ErrVal τ
  Error : ErrVal τ
  TimeOut : ErrVal τ

Res : Type → Set
Res τ = (n : ℕ) → ErrVal τ

_>>=_ : ∀ {σ τ} → Res σ → (Val σ → Res τ) → Res τ
(s >>= t) n0 with s n0
... | Done v n1 = t v n1
... | Error = Error
... | TimeOut = TimeOut

evalConst : ∀ {τ} → Const τ → Res τ
evalConst (lit v) n = Done (intV v) n

{-# TERMINATING #-}
eval : ∀ {Γ τ} → Term Γ τ → ⟦ Γ ⟧Context → Res τ

apply : ∀ {σ τ} → Val (σ ⇒ τ) → Val σ → Res τ
apply (closure t ρ) a n = eval t (a • ρ) n

eval (var x) ρ n = Done (⟦ x ⟧Var ρ) n
eval (abs t) ρ n = Done (closure t ρ) n
eval (const c) ρ n = evalConst c n
eval _ ρ zero = TimeOut
eval (app s t) ρ (suc n) = (eval s ρ >>= (λ sv → eval t ρ >>= λ tv → apply sv tv)) n

eval-const-dec : ∀ {τ} → (c : Const τ) → ∀ {v} n0 n1 → evalConst c n0 ≡ Done v n1 →  n1 ≤ n0
eval-const-dec (lit v) n0 .n0 refl = ≤-refl

{-# TERMINATING #-}
eval-dec : ∀ {Γ τ} → (t : Term Γ τ) → ∀ ρ v n0 n1 → eval t ρ n0 ≡ Done v n1 → n1 ≤ n0
eval-dec (const c) ρ v n0 n1 eq = eval-const-dec c n0 n1 eq
eval-dec (var x) ρ .(⟦ x ⟧Var ρ) n0 .n0 refl = ≤-refl
eval-dec (abs t) ρ .(closure t ρ) n0 .n0 refl = ≤-refl
eval-dec (app s t) ρ v zero n1 ()
eval-dec (app s t) ρ v (suc n0) n3 eq  with eval s ρ n0 | inspect (eval s ρ) n0
eval-dec (app s t) ρ v (suc n0) n3 eq | Done sv sn1 | [ seq ] with eval t ρ sn1 | inspect (eval t ρ) sn1
eval-dec (app s t) ρ v (suc n0) n3 eq | Done sv@(closure st sρ) sn1 | [ seq ] | (Done tv tn2) | [ teq ] = ≤-step (≤-trans (≤-trans (eval-dec st _ _ _ _ eq) (eval-dec t _ _ _ _ teq)) (eval-dec s _ _ _ _ seq))
eval-dec (app s t) ρ v (suc n0) n3 () | Done sv sn1 | [ seq ] | Error | [ teq ]
eval-dec (app s t) ρ v (suc n0) n3 () | Done sv sn1 | [ seq ] | TimeOut | [ teq ]
eval-dec (app s t) ρ v (suc n0) n3 () | Error | [ seq ]
eval-dec (app s t) ρ v (suc n0) n3 () | TimeOut | [ seq ]

eval-const-mono : ∀ {τ} → (c : Const τ) → ∀ {v} n0 n1 → evalConst c n0 ≡ Done v n1 → evalConst c (suc n0) ≡ Done v (suc n1)
eval-const-mono (lit v) n0 .n0 refl = refl

-- ARGH
{-# TERMINATING #-}
eval-mono : ∀ {Γ τ} → (t : Term Γ τ) → ∀ ρ v n0 n1 → eval t ρ n0 ≡ Done v n1 → eval t ρ (suc n0) ≡ Done v (suc n1)
eval-mono (const c) ρ v n0 n1 eq = eval-const-mono c n0 n1 eq
eval-mono (var x) ρ .(⟦ x ⟧Var ρ) n0 .n0 refl = refl
eval-mono (abs t) ρ .(closure t ρ) n0 .n0 refl = refl
eval-mono (app s t) ρ v zero n1 ()
eval-mono (app s t) ρ v (suc n0) n1 eq with eval s ρ n0 | inspect (eval s ρ) n0
eval-mono (app s t) ρ v (suc n0) n2 eq | Done sv n1 | [ seq ] with eval s ρ (suc n0) | eval-mono s ρ sv n0 n1 seq
eval-mono (app s t) ρ v (suc n0) n2 eq | Done sv n1 | [ seq ] | .(Done sv (suc n1)) | refl with eval t ρ n1 | inspect (eval t ρ) n1
eval-mono (app s t) ρ v (suc n0) n3 eq | Done sv n1 | [ seq ] | .(Done sv (suc n1)) | refl | Done tv n2 | [ teq ] with eval t ρ (suc n1) | eval-mono t ρ tv n1 n2 teq
eval-mono (app s t) ρ v (suc n0) n3 eq | Done (closure t₁ ρ₁) n1 | [ seq ] | .(Done (closure {Γ = _} {σ = _} {τ = _} t₁ ρ₁) (suc n1)) | refl | (Done tv n2) | [ teq ] | .(Done tv (suc n2)) | refl = eval-mono t₁ (tv • ρ₁) v n2 n3 eq
eval-mono (app s t) ρ v (suc n0) n2 () | Done sv n1 | [ seq ] | .(Done sv (suc n1)) | refl | Error | [ teq ]
eval-mono (app s t) ρ v (suc n0) n2 () | Done sv n1 | [ seq ] | .(Done sv (suc n1)) | refl | TimeOut | [ teq ]
eval-mono (app s t) ρ v (suc n0) n1 () | Error | [ seq ]
eval-mono (app s t) ρ v (suc n0) n1 () | TimeOut | [ seq ]

eval-adjust-plus : ∀ d {Γ τ} → (t : Term Γ τ) → ∀ ρ v n0 n1 → eval t ρ n0 ≡ Done v n1 → eval t ρ (d + n0) ≡ Done v (d + n1)
eval-adjust-plus zero t ρ v n0 n1 eq = eq
eval-adjust-plus (suc d) t ρ v n0 n1 eq = eval-mono t ρ v (d + n0) (d + n1) (eval-adjust-plus d t ρ v n0 n1 eq)

eval-const-strengthen : ∀ {τ} → (c : Const τ) → ∀ {v} n0 n1 → evalConst c (suc n0) ≡ Done v (suc n1) → evalConst c n0 ≡ Done v n1
eval-const-strengthen (lit v) n0 .n0 refl = refl

-- I started trying to prove eval-strengthen, which I appeal to informally
-- below, but I gave up. I still guess the lemma is true but proving it looks
-- too painful to bother.

-- Without this lemma, I can't fully prove that this logical relation is
-- equivalent to the original one.
-- But this one works (well, at least up to the fundamental theorem, haven't
-- attempted other lemmas), so it should be good enough.

-- eval-mono-err : ∀ {Γ τ} → (t : Term Γ τ) → ∀ ρ n → eval t ρ n ≡ Error → eval t ρ (suc n) ≡ Error
-- eval-mono-err (const (lit x)) ρ zero eq = {!!}
-- eval-mono-err (const (lit x)) ρ (suc n) eq = {!!}
-- eval-mono-err (var x) ρ n eq = {!!}
-- eval-mono-err (app t t₁) ρ n eq = {!!}
-- eval-mono-err (abs t) ρ n eq = {!!}

-- -- eval t ρ (suc n0) ≡ Done v (suc n1) → eval t ρ n0 ≡ Done v n
-- eval-aux : ∀ {Γ τ} → (t : Term Γ τ) → ∀ ρ n → (Σ[ res0 ∈ ErrVal τ ] eval t ρ n ≡ res0) × (Σ[ resS ∈ ErrVal τ ] eval t ρ n ≡ resS)
-- eval-aux t ρ n with
--   eval t ρ n | inspect (eval t ρ) n |
--   eval t ρ (suc n) | inspect (eval t ρ) (suc n)
-- eval-aux t ρ n | res0 | [ eq0 ] | (Done v1 n1) | [ eq1 ] = {!!}
-- eval-aux t ρ n | res0 | [ eq0 ] | Error | [ eq1 ] = {!!}
-- eval-aux t ρ n | Done v n1 | [ eq0 ] | TimeOut | [ eq1 ] = {!!}
-- eval-aux t ρ n | Error | [ eq0 ] | TimeOut | [ eq1 ] = {!!}
-- eval-aux t ρ n | TimeOut | [ eq0 ] | TimeOut | [ eq1 ] = (TimeOut , refl) , (TimeOut , refl)

-- {-# TERMINATING #-}
-- eval-strengthen : ∀ {Γ τ} → (t : Term Γ τ) → ∀ ρ v n0 n1 → eval t ρ (suc n0) ≡ Done v (suc n1) → eval t ρ n0 ≡ Done v n1
-- eval-strengthen (const c) ρ v n0 n1 eq = eval-const-strengthen c n0 n1 eq
-- eval-strengthen (var x) ρ .(⟦ x ⟧Var ρ) n0 .n0 refl = refl
-- eval-strengthen (abs t) ρ .(closure t ρ) n0 .n0 refl = refl
-- eval-strengthen (app s t) ρ v zero n1 eq with eval s ρ 0 | inspect (eval s ρ) 0
-- eval-strengthen (app s t) ρ v zero n1 eq | Done sv sn1 | [ seq ] with eval-dec s ρ sv 0 sn1 seq
-- eval-strengthen (app s t) ρ v zero n1 eq | Done sv .0 | [ seq ] | z≤n with eval t ρ 0 | inspect (eval t ρ) 0
-- eval-strengthen (app s t) ρ v zero n1 eq | Done sv _ | [ seq ] | z≤n | Done tv tn1 | [ teq ]  with eval-dec t ρ tv 0 tn1 teq
-- eval-strengthen (app s t) ρ v zero n1 eq | Done (closure st sρ) _ | [ seq ] | z≤n | (Done tv .0) | [ teq ] | z≤n with eval-dec st _ v 0 (suc n1) eq
-- eval-strengthen (app s t) ρ v zero n1 eq | Done (closure st sρ) _ | [ seq ] | z≤n | (Done tv _) | [ teq ] | z≤n | ()
-- eval-strengthen (app s t) ρ v zero n1 () | Done sv _ | [ seq ] | z≤n | Error | [ teq ]
-- eval-strengthen (app s t) ρ v zero n1 () | Done sv _ | [ seq ] | z≤n | TimeOut | [ teq ]
-- eval-strengthen (app s t) ρ v zero n1 () | Error | [ seq ]
-- eval-strengthen (app s t) ρ v zero n1 () | TimeOut | [ seq ]
-- -- eval-dec s ρ
-- --  {!eval-dec s ρ ? (suc zero) (suc n1) !}
-- -- eval-strengthen (app s t) ρ v (suc n0) n1 eq with eval s ρ (suc n0) | inspect (eval s ρ) (suc n0)
-- -- eval-strengthen (app s t) ρ v₁ (suc n0) n2 eq | Done sv n1 | [ seq ] with eval s ρ n0 = {!eval-strengthen s ρ v n0 n1 seq !}
-- -- eval-strengthen (app s t) ρ v (suc n0) n1 () | Error | [ seq ]
-- -- eval-strengthen (app s t) ρ v (suc n0) n1 () | TimeOut | [ seq ]
-- eval-strengthen (app s t) ρ v (suc n0) n1 eq with eval s ρ n0 | inspect (eval s ρ) n0
-- eval-strengthen (app s t) ρ v (suc n0) n2 eq | Done sv n1 | [ seq ] with eval s ρ (suc n0) | eval-mono s ρ sv n0 n1 seq
-- eval-strengthen (app s t) ρ v (suc n0) n2 eq | Done sv n1 | [ seq ] | .(Done sv (suc n1)) | refl with eval t ρ n1 | inspect (eval t ρ) n1
-- eval-strengthen (app s t) ρ v (suc n0) n3 eq | Done sv n1 | [ seq ] | .(Done sv (suc n1)) | refl | Done tv n2 | [ teq ] with eval t ρ (suc n1) | eval-mono t ρ tv n1 n2 teq
-- eval-strengthen (app s t) ρ v (suc n0) n3 eq | Done (closure t₁ ρ₁) n1 | [ seq ] | .(Done (closure {Γ = _} {σ = _} {τ = _} t₁ ρ₁) (suc n1)) | refl | (Done tv n2) | [ teq ] | .(Done tv (suc n2)) | refl = eval-strengthen t₁ (tv • ρ₁) v n2 n3 eq
-- eval-strengthen (app s t) ρ v (suc n0) n2 eq | Done sv n1 | [ seq ] | .(Done sv (suc n1)) | refl | Error | [ teq ] = {!!}
-- eval-strengthen (app s t) ρ v (suc n0) n2 eq | Done sv n1 | [ seq ] | .(Done sv (suc n1)) | refl | TimeOut | [ teq ] = {!!}
-- eval-strengthen (app s t) ρ v (suc n0) n1 eq | Error | [ seq ] = {!!}
-- eval-strengthen (app s t) ρ v (suc n0) n1 eq | TimeOut | [ seq ] = {!!}

-- eval-adjust-minus : ∀ d {Γ τ} → (t : Term Γ τ) → ∀ {ρ v} n0 n1 → eval t ρ (d + n0) ≡ Done v (d + n1) → eval t ρ n0 ≡ Done v n1
-- eval-adjust-minus zero t n0 n1 eq = eq
-- eval-adjust-minus (suc d) t n0 n1 eq = eval-adjust-minus d t n0 n1 (eval-strengthen t _ _ (d + n0) (d + n1) eq)

import Data.Integer as I
open I using (ℤ)
mutual
  -- Warning: compared to Ahmed's papers, this definition for relT also requires
  -- t1 to be well-typed, not just t2.
  --
  -- This difference might affect the status of some proofs in Ahmed's papers,
  -- but that's not a problem here.

  -- Also: can't confirm this in any of the papers I'm using, but I'd guess that
  -- all papers using environments allow to relate closures with different
  -- implementations and different hidden environments.
  --
  -- To check if the proof goes through with equal context, I changed the proof.
  -- Now a proof that two closures are equivalent contains a proof that their
  -- typing contexts are equivalent. The changes were limited softawre
  -- engineering, the same proofs go through.

  -- This is not the same definition of relT, but it is equivalent.
  relT : ∀ {τ Γ} (t1 : Term Γ τ) (t2 : Term Γ τ) (ρ1 : ⟦ Γ ⟧Context) (ρ2 : ⟦ Γ ⟧Context) → ℕ → Set
  -- This equation is a lemma in the original definition.
  relT t1 t2 ρ1 ρ2 zero = ⊤
  -- To compare this definition, note that the original k is suc n here.
  relT {τ} t1 t2 ρ1 ρ2 (suc n) =
    (v1 : Val τ) →
    -- Originally we have 0 ≤ j < k, so j < suc n, so k - j = suc n - j.
    -- It follows that 0 < k - j ≤ k, hence suc n - j ≤ suc n, or n - j ≤ n.
    -- Here, instead of binding j we bind n-j = n - j, require n - j ≤ n, and
    -- use suc n-j instead of k - j.
    ∀ n-j (n-j≤n : n-j ≤ n) →
    -- The next assumption is important. This still says that evaluation consumes j steps.
    -- Since j ≤ n, it is OK to start evaluation with n steps.
    -- Starting with (suc n) and getting suc n-j is equivalent, per eval-mono
    -- and eval-strengthen. But in practice this version is easier to use.
    (eq : eval t1 ρ1 n ≡ Done v1 n-j) →
    Σ[ v2 ∈ Val τ ] Σ[ n2 ∈ ℕ ] eval t2 ρ2 n2 ≡ Done v2 0 × relV τ v1 v2 (suc n-j)
    -- Here, computing t2 is allowed to take an unbounded number of steps. Having to write a number at all is annoying.

  relV : ∀ τ (v1 v2 : Val τ) → ℕ → Set
  -- Show the proof still goes through if we relate clearly different values by
  -- inserting changes in the relation.
  -- There's no syntax to produce such changes, but you can add changes to the
  -- environment.
  relV nat (intV v1) (intV v2) n = Σ[ dv ∈ ℤ ] dv I.+ (I.+ v1) ≡ (I.+ v2)
  relV (σ ⇒ τ) (closure {Γ1} t1 ρ1) (closure {Γ2} t2 ρ2) n =
    Σ (Γ1 ≡ Γ2) λ { refl →
      ∀ (k : ℕ) (k≤n : k < n) v1 v2 →
      relV σ v1 v2 k →
      relT t1 t2 (v1 • ρ1) (v2 • ρ2) k
    }
  -- Above, in the conclusion, I'm not relating app (closure t1 ρ1) v1 with app
  -- (closure t2 ρ2) v2 (or some encoding of that that actually works), but the
  -- result of taking a step from that configuration. That is important, because
  -- both Pitts' "Step-Indexed Biorthogonality: a Tutorial Example" and
  -- "Imperative Self-Adjusting Computation" do the same thing (and point out it's
  -- important).

Δτ : Type → Type
Δτ (σ ⇒ τ) = σ ⇒ (Δτ σ) ⇒ Δτ τ
Δτ nat = nat

mutual
  -- The original relation allows unrelated environments. However, while that is
  -- fine as a logical relation, it's not OK if we want to prove that validity
  -- agrees with oplus. We want a finer relation.
  -- Also: we still need to demand the actual environments to be related, and
  -- the bodies to match. Haven't done that yet. On the other hand, since we do want
  -- to allow for replacement changes, that would probably complicate the proof
  -- elsewhere.
  relT3 : ∀ {τ Γ ΔΓ} (t1 : Term Γ τ) (dt : Term ΔΓ (Δτ τ)) (t2 : Term Γ τ) (ρ1 : ⟦ Γ ⟧Context) (dρ : ⟦ ΔΓ ⟧Context) (ρ2 : ⟦ Γ ⟧Context) → ℕ → Set
  relT3 t1 dt t2 ρ1 dρ ρ2 zero = ⊤
  relT3 {τ} t1 dt t2 ρ1 dρ ρ2 (suc n) =
    (v1 : Val τ) →
    ∀ n-j (n-j≤n : n-j ≤ n) →
    (eq : eval t1 ρ1 n ≡ Done v1 n-j) →
    Σ[ v2 ∈ Val τ ] Σ[ n2 ∈ ℕ ] eval t2 ρ2 n2 ≡ Done v2 0 ×
    Σ[ dv ∈ Val (Δτ τ) ] Σ[ dn ∈ ℕ ] eval dt dρ dn ≡ Done dv 0 ×
    relV3 τ v1 dv v2 (suc n-j)

  -- Weakening in this definition is going to be annoying to use. And having to
  -- construct terms is ugly.
  -- Worse, evaluating the application consumes computation steps.

  -- Weakening could be avoided if we use a separate language of change terms
  -- with two environments, and with a dclosure binding two variables at once,
  -- and so on.
  relV3 : ∀ τ (v1 : Val τ) (dv : Val (Δτ τ)) (v2 : Val τ) → ℕ → Set
  relV3 nat (intV v1) (intV dv) (intV v2) n = dv + v1 ≡ v2
  relV3 (σ ⇒ τ) (closure {Γ1} t1 ρ1) (closure dt dρ) (closure {Γ2} t2 ρ2) n =
    Σ (Γ1 ≡ Γ2) λ { refl →
      ∀ (k : ℕ) (k<n : k < n) v1 dv v2 →
      relV3 σ v1 dv v2 k →
      relT3 t1 (app (weaken (drop (Δτ σ) • ≼-refl) dt) (var this)) t2 (v1 • ρ1) (dv • v1 • dρ) (v2 • ρ2) k
    }

  -- Relate λ x → 0 and λ x → 1 at any step count.
  example1 : ∀ n → relV (nat ⇒ nat) (closure (const (lit 0)) ∅) (closure (const (lit 1)) ∅) n
  example1 n = refl ,
    λ { zero k<n v1 v2 x → tt
      ; (suc k) k<n v1 v2 x .(intV 0) .k n-j≤n refl → intV 1 , 0 , refl , (I.+ 1 , refl)
      }

  -- Relate λ x → 0 and λ x → x at any step count.
  example2 : ∀ n → relV (nat ⇒ nat) (closure (const (lit 0)) ∅) (closure (var this) ∅) n
  example2 n = refl ,
    λ { zero k<n v1 v2 x → tt
      ; (suc k) k<n (intV v1) (intV v2) x .(intV 0) .k n-j≤n refl → intV v2 , 0 , refl , (I.+ v2 , cong I.+_ (+-identityʳ v2))
      }

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

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

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

fundamentalV : ∀ {Γ τ} (x : Var Γ τ) → (n : ℕ) → (ρ1 ρ2 : ⟦ Γ ⟧Context) (ρρ : relρ Γ ρ1 ρ2 n) → relT (var x) (var x) ρ1 ρ2 n
fundamentalV x zero ρ1 ρ2 ρρ = tt
fundamentalV this (suc n) (v1 • ρ1) (v2 • ρ2) (vv , ρρ) .v1 .n n-j≤n refl = v2 , zero , refl , vv
fundamentalV (that x) (suc n) (v1 • ρ1) (v2 • ρ2) (vv , ρρ) = fundamentalV x (suc n) ρ1 ρ2 ρρ

lt1 : ∀ {k n} → k < n → k ≤ n
lt1 (s≤s p) = ≤-step p

fundamental : ∀ {Γ τ} (t : Term Γ τ) → (n : ℕ) → (ρ1 ρ2 : ⟦ Γ ⟧Context) (ρρ : relρ Γ ρ1 ρ2 n) → relT t t ρ1 ρ2 n
fundamental t zero ρ1 ρ2 ρρ = tt
fundamental (var x) (suc n) ρ1 ρ2 ρρ = fundamentalV x (suc n) ρ1 ρ2 ρρ
fundamental (const (lit v)) (suc n) ρ1 ρ2 ρρ .(intV v) .n n-j≤n refl = intV v , zero , refl , I.+ zero , refl
fundamental (abs t) (suc n) ρ1 ρ2 ρρ .(closure t ρ1) .n n-j≤n refl =  closure t ρ2 , zero , refl , refl , λ k k<n v1 v2 vv → fundamental t k (v1 • ρ1) (v2 • ρ2) (vv , relρ-mono k (suc n) (lt1 k<n) _ _ _ ρρ)
fundamental (app s t) (suc zero) ρ1 ρ2 ρρ v1 n-j n-j≤n ()
fundamental (app s t) (suc (suc n)) ρ1 ρ2 ρρ v1 n-j n-j≤n eq with eval s ρ1 n | inspect (eval s ρ1) n
fundamental (app s t) (suc (suc n)) ρ1 ρ2 ρρ v1 n-j n-j≤n eq | Done sv1 n1 | [ s1eq ] with eval-dec s _ _ n n1 s1eq | eval t ρ1 n1 | inspect (eval t ρ1) n1
fundamental (app s t) (suc (suc n)) ρ1 ρ2 ρρ v1 n-j n-j≤n eq | Done (closure st1 sρ1) n1 | [ s1eq ] | n1≤n | Done tv1 n2 | [ t1eq ] with eval-dec t _ _ n1 n2 t1eq
... | n2≤n1 with fundamental s (suc (suc n)) ρ1 ρ2 ρρ (closure st1 sρ1) (suc n1) (s≤s n1≤n) (eval-mono s ρ1 (closure st1 sρ1) n n1 s1eq)
  | fundamental t (suc (suc n1)) ρ1 ρ2 (relρ-mono (suc (suc n1)) (suc (suc n)) (s≤s (s≤s n1≤n)) _ _ _ ρρ) tv1 (suc n2) (s≤s n2≤n1) (eval-mono t ρ1 tv1 n1 n2 t1eq)
... | sv2@(closure st2 sρ2) , sn3 , s2eq , refl , svv | tv2 , tn3 , t2eq , tvv with svv (suc n2) (s≤s (s≤s n2≤n1)) tv1 tv2 (relV-mono (suc n2) (suc (suc n2)) (s≤s (n≤1+n n2)) _ tv1 tv2 tvv) v1 n-j (eval-dec st1 _ _ _ _ eq) eq
... | v2 , n3 , eq2 , vv = v2 , suc (sn3 + (tn3 + n3)) , comp , vv
  where
    s2eq-adj : eval s ρ2 (sn3 + (tn3 + n3)) ≡ Done (closure st2 sρ2) (tn3 + n3)
    s2eq-adj rewrite +-comm sn3 (tn3 + n3)| cong (Done (closure st2 sρ2)) (sym (+-identityʳ (tn3 + n3))) = eval-adjust-plus (tn3 + n3) s _ sv2 _ _ s2eq
    t2eq-adj : eval t ρ2 (tn3 + n3) ≡ Done tv2 n3
    t2eq-adj rewrite +-comm tn3 n3 | cong (Done tv2) (sym (+-identityʳ n3)) = eval-adjust-plus n3 t _ tv2 _ _ t2eq

    comp : (eval s ρ2 >>= (λ sv → eval t ρ2 >>= apply sv))
      (sn3 + (tn3 + n3))
      ≡ Done v2 0
    comp rewrite s2eq-adj | t2eq-adj = eq2

fundamental (app s t) (suc (suc n)) ρ1 ρ2 ρρ v1 n-j n-j≤n () | Done sv1 n1 | [ s1eq ] | n1≤n | Error | [ t1eq ]
fundamental (app s t) (suc (suc n)) ρ1 ρ2 ρρ v1 n-j n-j≤n () | Done sv1 n1 | [ s1eq ] | n1≤n | TimeOut | [ t1eq ]
fundamental (app s t) (suc (suc n)) ρ1 ρ2 ρρ v1 n-j n-j≤n () | Error | [ s1eq ]
fundamental (app s t) (suc (suc n)) ρ1 ρ2 ρρ v1 n-j n-j≤n () | TimeOut | [ s1eq ]

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-

Automatically generating proofs of UnivalentStr for records

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.List as List
open import Cubical.Data.Vec as Vec
open import Cubical.Data.Bool
open import Cubical.Data.Maybe
open import Cubical.Data.Sum
open import Cubical.Structures.Auto
import Cubical.Structures.Macro as M
import Agda.Builtin.Reflection as R
open import Cubical.Reflection.Base

-- Magic number
private
  FUEL = 10000

-- Types for specifying inputs to the tactics

data AutoFieldSpec : Typeω where
  autoFieldSpec : ∀ {ℓ ℓ₁ ℓ₂} (R : Type ℓ → Type ℓ₁) {S : Type ℓ → Type ℓ₂}
    → ({X : Type ℓ} → R X → S X)
    → AutoFieldSpec

module _ {ℓ ℓ₁ ℓ₁'} where
  mutual
    data AutoFields (R : Type ℓ → Type ℓ₁) (ι : StrEquiv R ℓ₁') : Typeω
      where
      fields: : AutoFields R ι
      _data[_∣_] : (fs : AutoFields R ι)
        → ∀ {ℓ₂ ℓ₂'} {S : Type ℓ → Type ℓ₂} {ι' : StrEquiv S ℓ₂'}
        → (f : {X : Type ℓ} → R X → S X)
        → ({A B : TypeWithStr ℓ R} {e : typ A ≃ typ B} → ι A B e → ι' (map-snd f A) (map-snd f B) e)
        → AutoFields R ι
      _prop[_∣_] : (fs : AutoFields R ι)
        → ∀ {ℓ₂} {P : (X : Type ℓ) → GatherFields fs X → Type ℓ₂}
        → ({X : Type ℓ} (r : R X) → P X (projectFields fs r))
        → isPropProperty R ι fs P
        → AutoFields R ι

    GatherFieldsLevel : {R : Type ℓ → Type ℓ₁} {ι : StrEquiv R ℓ₁'}
      → AutoFields R ι
      → Level
    GatherFieldsLevel fields: = ℓ-zero
    GatherFieldsLevel (_data[_∣_] fs {ℓ₂ = ℓ₂} _ _) = ℓ-max (GatherFieldsLevel fs) ℓ₂
    GatherFieldsLevel (_prop[_∣_] fs {ℓ₂ = ℓ₂} _ _) = ℓ-max (GatherFieldsLevel fs) ℓ₂

    GatherFields : {R : Type ℓ → Type ℓ₁} {ι : StrEquiv R ℓ₁'}
      (dat : AutoFields R ι)
      → Type ℓ → Type (GatherFieldsLevel dat)
    GatherFields fields: X = Unit
    GatherFields (_data[_∣_] fs {S = S} _ _) X = GatherFields fs X × S X
    GatherFields (_prop[_∣_] fs {P = P} _ _) X =
      Σ[ s ∈ GatherFields fs X ] (P X s)

    projectFields : {R : Type ℓ → Type ℓ₁} {ι : StrEquiv R ℓ₁'}
      (fs : AutoFields R ι)
      → {X : Type ℓ} → R X → GatherFields fs X
    projectFields fields: = _
    projectFields (fs data[ f ∣ _ ]) r = projectFields fs r , f r
    projectFields (fs prop[ f ∣ _ ]) r = projectFields fs r , f r

    isPropProperty : ∀ {ℓ₂} (R : Type ℓ → Type ℓ₁)
      (ι : StrEquiv R ℓ₁')
      (fs : AutoFields R ι)
      (P : (X : Type ℓ) → GatherFields fs X → Type ℓ₂)
      → Type (ℓ-max (ℓ-suc ℓ) (ℓ-max ℓ₁ ℓ₂))
    isPropProperty R ι fs P =
      {X : Type ℓ} (r  : R X) → isProp (P X (projectFields fs r))

  data AutoRecordSpec : Typeω where
    autoRecordSpec : (R : Type ℓ → Type ℓ₁) (ι : StrEquiv R ℓ₁')
      → AutoFields R ι
      → AutoRecordSpec

-- Some reflection utilities
private
  tApply : R.Term → List (R.Arg R.Term) → R.Term
  tApply t l = R.def (quote idfun) (R.unknown v∷ t v∷ l)

  tStrMap : R.Term → R.Term → R.Term
  tStrMap A f = R.def (quote map-snd) (f v∷ A v∷ [])

  tStrProj : R.Term → R.Name → R.Term
  tStrProj A sfield = tStrMap A (R.def sfield [])

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

-- Helper functions used in the generated univalence proof
private
  pathMap : ∀ {ℓ ℓ'} {S : I → Type ℓ} {T : I → Type ℓ'} (f : {i : I} → S i → T i)
    {x : S i0} {y : S i1} → PathP S x y → PathP T (f x) (f y)
  pathMap f p i = f (p i)

  -- Property field helper functions
  module _
    {ℓ ℓ₁ ℓ₁' ℓ₂}
    (R : Type ℓ → Type ℓ₁) -- Structure record
    (ι : StrEquiv R ℓ₁') -- Equivalence record
    (fs : AutoFields R ι) -- Prior fields
    (P : (X : Type ℓ) → GatherFields fs X → Type ℓ₂) -- Property type
    (f : {X : Type ℓ} (r : R X) → P X (projectFields fs r)) -- Property projection
    where

    prev = projectFields fs
    Prev = GatherFields fs

    PropHelperCenterType : Type _
    PropHelperCenterType =
      (A B : TypeWithStr ℓ R) (e : A .fst ≃ B .fst)
      (p : PathP (λ i → Prev (ua e i)) (prev (A .snd)) (prev (B .snd)))
      → PathP (λ i → P (ua e i) (p i)) (f (A .snd)) (f (B .snd))

    PropHelperContractType : PropHelperCenterType → Type _
    PropHelperContractType c =
      (A B : TypeWithStr ℓ R) (e : A .fst ≃ B .fst)
      {p₀ : PathP (λ i → Prev (ua e i)) (prev (A .snd)) (prev (B .snd))}
      (q : PathP (λ i → R (ua e i)) (A .snd) (B .snd))
      (p : p₀ ≡ (λ i → prev (q i)))
      → PathP (λ k → PathP (λ i → P (ua e i) (p k i)) (f (A .snd)) (f (B .snd)))
        (c A B e p₀)
        (λ i → f (q i))

    PropHelperType : Type _
    PropHelperType =
      Σ PropHelperCenterType PropHelperContractType

    derivePropHelper : isPropProperty R ι fs P → PropHelperType
    derivePropHelper propP .fst A B e p =
      isOfHLevelPathP' 0 (propP _) (f (A .snd)) (f (B .snd)) .fst
    derivePropHelper propP .snd A B e q p =
      isOfHLevelPathP' 0 (isOfHLevelPathP 1 (propP _) _ _) _ _ .fst

  -- Build proof of univalence from an isomorphism
  module _ {ℓ ℓ₁ ℓ₁'} (S : Type ℓ → Type ℓ₁) (ι : StrEquiv S ℓ₁') where

    fwdShape : Type _
    fwdShape =
      (A B : TypeWithStr ℓ S) (e : typ A ≃ typ B) → ι A B e → PathP (λ i → S (ua e i)) (str A) (str B)

    bwdShape : Type _
    bwdShape =
      (A B : TypeWithStr ℓ S) (e : typ A ≃ typ B) → PathP (λ i → S (ua e i)) (str A) (str B) → ι A B e

    fwdBwdShape : fwdShape → bwdShape → Type _
    fwdBwdShape fwd bwd =
      (A B : TypeWithStr ℓ S) (e : typ A ≃ typ B) → ∀ p → fwd A B e (bwd A B e p) ≡ p

    bwdFwdShape : fwdShape → bwdShape → Type _
    bwdFwdShape fwd bwd =
      (A B : TypeWithStr ℓ S) (e : typ A ≃ typ B) → ∀ r → bwd A B e (fwd A B e r) ≡ r

    -- The implicit arguments A,B in UnivalentStr make some things annoying so let's avoid them
    ExplicitUnivalentStr : Type _
    ExplicitUnivalentStr =
      (A B : TypeWithStr _ S) (e : typ A ≃ typ B) → ι A B e ≃ PathP (λ i → S (ua e i)) (str A) (str B)

    explicitUnivalentStr : (fwd : fwdShape) (bwd : bwdShape)
      → fwdBwdShape fwd bwd → bwdFwdShape fwd bwd
      → ExplicitUnivalentStr
    explicitUnivalentStr fwd bwd fwdBwd bwdFwd A B e = isoToEquiv isom
      where
      open Iso
      isom : Iso _ _
      isom .fun = fwd A B e
      isom .inv = bwd A B e
      isom .rightInv = fwdBwd A B e
      isom .leftInv = bwdFwd A B e

  ExplicitUnivalentDesc : ∀ ℓ → (d : M.Desc ℓ) → Type _
  ExplicitUnivalentDesc _ d =
    ExplicitUnivalentStr (M.MacroStructure d) (M.MacroEquivStr d)

  explicitUnivalentDesc : ∀ ℓ → (d : M.Desc ℓ) → ExplicitUnivalentDesc ℓ d
  explicitUnivalentDesc _ d A B e = M.MacroUnivalentStr d e

-- Internal record specification type
private
  record TypedTerm : Type where
    field
      type : R.Term
      term : R.Term

  record InternalDatumField : Type where
    field
      sfield : R.Name -- name of structure field
      efield : R.Name -- name of equivalence field

  record InternalPropField : Type where
    field
      sfield : R.Name -- name of structure field

  InternalField : Type
  InternalField = InternalDatumField ⊎ InternalPropField

  record InternalSpec (A : Type) : Type where
    field
      srec : R.Term -- structure record type
      erec : R.Term -- equivalence record type
      fields : List (InternalField × A) -- in reverse order

  open TypedTerm
  open InternalDatumField
  open InternalPropField

-- Parse a field and record specifications
private
  findName : R.Term → R.TC R.Name
  findName (R.def name _) = R.returnTC name
  findName (R.lam R.hidden (R.abs _ t)) = findName t
  findName t = R.typeError (R.strErr "Not a name + spine: " ∷ R.termErr t ∷ [])

  parseFieldSpec : R.Term → R.TC (R.Term × R.Term × R.Term × R.Term)
  parseFieldSpec (R.con (quote autoFieldSpec) (ℓ h∷ ℓ₁ h∷ ℓ₂ h∷ R v∷ S h∷ f v∷ [])) =
    R.reduce ℓ >>= λ ℓ →
    R.returnTC (ℓ , ℓ₂ , S , f)
  parseFieldSpec t =
    R.typeError (R.strErr "Malformed field specification: " ∷ R.termErr t ∷ [])

  parseSpec : R.Term → R.TC (InternalSpec TypedTerm)
  parseSpec (R.con (quote autoRecordSpec) (ℓ h∷ ℓ₁ h∷ ℓ₁' h∷ srecTerm v∷ erecTerm v∷ fs v∷ [])) =
    parseFields fs >>= λ fs' →
    R.returnTC λ { .srec → srecTerm ; .erec → erecTerm ; .fields → fs'}
    where
    open InternalSpec

    parseFields : R.Term → R.TC (List (InternalField × TypedTerm))
    parseFields (R.con (quote fields:) _) = R.returnTC []
    parseFields (R.con (quote _data[_∣_])
      (ℓ h∷ ℓ₁ h∷ ℓ₁' h∷ R h∷ ι h∷ fs v∷ ℓ₂ h∷ ℓ₂' h∷ S h∷ ι' h∷ sfieldTerm v∷ efieldTerm v∷ []))
      =
      R.reduce ℓ >>= λ ℓ →
      findName sfieldTerm >>= λ sfieldName →
      findName efieldTerm >>= λ efieldName →
      buildDesc FUEL ℓ ℓ₂ S >>= λ d →
      let
        f : InternalField × TypedTerm
        f = λ
          { .fst → inl λ { .sfield → sfieldName ; .efield → efieldName }
          ; .snd .type → R.def (quote ExplicitUnivalentDesc) (ℓ v∷ d v∷ [])
          ; .snd .term → R.def (quote explicitUnivalentDesc) (ℓ v∷ d v∷ [])
          }
      in
      liftTC (f ∷_) (parseFields fs)
    parseFields (R.con (quote _prop[_∣_])
      (ℓ h∷ ℓ₁ h∷ ℓ₁' h∷ R h∷ ι h∷ fs v∷ ℓ₂ h∷ P h∷ fieldTerm v∷ prop v∷ []))
      =
      findName fieldTerm >>= λ fieldName →
      let
        p : InternalField × TypedTerm
        p = λ
          { .fst → inr λ { .sfield → fieldName }
          ; .snd .type →
            R.def (quote PropHelperType) (srecTerm v∷ erecTerm v∷ fs v∷ P v∷ fieldTerm v∷ [])
          ; .snd .term →
            R.def (quote derivePropHelper) (srecTerm v∷ erecTerm v∷ fs v∷ P v∷ fieldTerm v∷ prop v∷ [])
          }
      in
      liftTC (p ∷_) (parseFields fs)

    parseFields t = R.typeError (R.strErr "Malformed autoRecord specification (1): " ∷ R.termErr t ∷ [])

  parseSpec t = R.typeError (R.strErr "Malformed autoRecord specification (2): " ∷ R.termErr t ∷ [])

-- Build a proof of univalence from an InternalSpec
module _ (spec : InternalSpec ℕ) where
  open InternalSpec spec
  private

    fwdDatum : Vec R.Term 4 → R.Term → InternalDatumField × ℕ → R.Term
    fwdDatum (A ∷ B ∷ e ∷ streq ∷ _) i (dat , n) =
      R.def (quote equivFun)
        (tApply (v n) (tStrProj A (dat .sfield) v∷ tStrProj B (dat .sfield) v∷ e v∷ [])
          v∷ R.def (dat .efield) (streq v∷ [])
          v∷ i
          v∷ [])

    fwdProperty : Vec R.Term 4 → R.Term → R.Term → InternalPropField × ℕ → R.Term
    fwdProperty (A ∷ B ∷ e ∷ streq ∷ _) i prevPath prop =
      R.def (quote fst) (v (prop .snd) v∷ A v∷ B v∷ e v∷ prevPath v∷ i v∷ [])

    bwdClause : Vec R.Term 4 → InternalDatumField × ℕ → R.Clause
    bwdClause (A ∷ B ∷ e ∷ q ∷ _) (dat , n) =
      R.clause [] (R.proj (dat .efield) v∷ [])
        (R.def (quote invEq)
          (tApply
            (v n)
            (tStrProj A (dat .sfield) v∷ tStrProj B (dat .sfield) v∷ e v∷ [])
            v∷ R.def (quote pathMap) (R.def (dat .sfield) [] v∷ q v∷ [])
            v∷ []))

    fwdBwdDatum : Vec R.Term 4 → R.Term → R.Term → InternalDatumField × ℕ → R.Term
    fwdBwdDatum (A ∷ B ∷ e ∷ q ∷ _) j i (dat , n) =
      R.def (quote retEq)
        (tApply
          (v n)
          (tStrProj A (dat .sfield) v∷ tStrProj B (dat .sfield) v∷ e v∷ [])
          v∷ R.def (quote pathMap) (R.def (dat .sfield) [] v∷ q v∷ [])
          v∷ j v∷ i
          v∷ [])

    fwdBwdProperty : Vec R.Term 4 → (j i prevPath : R.Term) → InternalPropField × ℕ → R.Term
    fwdBwdProperty (A ∷ B ∷ e ∷ q ∷ _) j i prevPath prop =
      R.def (quote snd) (v (prop .snd) v∷ A v∷ B v∷ e v∷ q v∷ prevPath v∷ j v∷ i v∷ [])

    bwdFwdClause : Vec R.Term 4 → R.Term → InternalDatumField × ℕ → R.Clause
    bwdFwdClause (A ∷ B ∷ e ∷ streq ∷ _) j (dat , n) =
      R.clause [] (R.proj (dat .efield) v∷ [])
        (R.def (quote secEq)
          (tApply
            (v n)
            (tStrProj A (dat .sfield) v∷ tStrProj B (dat .sfield) v∷ e v∷ [])
            v∷ R.def (dat .efield) (streq v∷ [])
            v∷ j
            v∷ []))

    makeVarsFrom : {n : ℕ} → ℕ → Vec R.Term n
    makeVarsFrom {zero} k = []
    makeVarsFrom {suc n} k = v (n + k) ∷ (makeVarsFrom k)

    fwd : R.Term
    fwd =
      vlam "A" (vlam "B" (vlam "e" (vlam "streq" (vlam "i" (R.pat-lam body [])))))
      where
      -- input list is in reverse order
      fwdClauses : ℕ → List (InternalField × ℕ) → List (R.Name × R.Term)
      fwdClauses k [] = []
      fwdClauses k ((inl f , n) ∷ fs) =
        fwdClauses k fs
        ∷ʳ (f .sfield , fwdDatum (makeVarsFrom k) (v 0) (map-snd (4 + k +_) (f , n)))
      fwdClauses k ((inr p , n) ∷ fs) =
        fwdClauses k fs
        ∷ʳ (p .sfield , fwdProperty (makeVarsFrom k) (v 0) prevPath (map-snd (4 + k +_) (p , n)))
        where
        prevPath =
          vlam "i"
            (List.foldl
              (λ t (_ , t') → R.con (quote _,_) (t v∷ t' v∷ []))
              (R.con (quote tt) [])
              (fwdClauses (suc k) fs))

      body =
        List.map (λ (n , t) → R.clause [] [ varg (R.proj n) ] t) (fwdClauses 1 fields)

    bwd : R.Term
    bwd =
      vlam "A" (vlam "B" (vlam "e" (vlam "q" (R.pat-lam (bwdClauses fields) []))))
      where
      -- input is in reverse order
      bwdClauses : List (InternalField × ℕ) → List R.Clause
      bwdClauses [] = []
      bwdClauses ((inl f , n) ∷ fs) =
        bwdClauses fs
        ∷ʳ bwdClause (makeVarsFrom 0) (map-snd (4 +_) (f , n))
      bwdClauses ((inr p , n) ∷ fs) = bwdClauses fs

    fwdBwd : R.Term
    fwdBwd =
      vlam "A" (vlam "B" (vlam "e" (vlam "q" (vlam "j" (vlam "i" (R.pat-lam body []))))))
      where
      -- input is in reverse order
      fwdBwdClauses : ℕ →  List (InternalField × ℕ) → List (R.Name × R.Term)
      fwdBwdClauses k [] = []
      fwdBwdClauses k ((inl f , n) ∷ fs) =
        fwdBwdClauses k fs
        ∷ʳ (f .sfield , fwdBwdDatum (makeVarsFrom k) (v 1) (v 0) (map-snd (4 + k +_) (f , n)))
      fwdBwdClauses k ((inr p , n) ∷ fs) =
        fwdBwdClauses k fs
        ∷ʳ ((p .sfield , fwdBwdProperty (makeVarsFrom k) (v 1) (v 0) prevPath (map-snd (4 + k +_) (p , n))))
        where
        prevPath =
          vlam "j"
            (vlam "i"
              (List.foldl
                (λ t (_ , t') → R.con (quote _,_) (t v∷ t' v∷ []))
                (R.con (quote tt) [])
                (fwdBwdClauses (2 + k) fs)))

      body = List.map (λ (n , t) → R.clause [] [ varg (R.proj n) ] t) (fwdBwdClauses 2 fields)

    bwdFwd : R.Term
    bwdFwd =
      vlam "A" (vlam "B" (vlam "e" (vlam "streq" (vlam "j" (R.pat-lam (bwdFwdClauses fields) [])))))
      where
      bwdFwdClauses : List (InternalField × ℕ) → List R.Clause
      bwdFwdClauses [] = []
      bwdFwdClauses ((inl f , n) ∷ fs) =
        bwdFwdClauses fs
        ∷ʳ bwdFwdClause (makeVarsFrom 1) (v 0) (map-snd (5 +_) (f , n))
      bwdFwdClauses ((inr _ , n) ∷ fs) = bwdFwdClauses fs

  univalentRecord : R.Term
  univalentRecord =
    R.def (quote explicitUnivalentStr)
      (R.unknown v∷ R.unknown v∷ fwd v∷ bwd v∷ fwdBwd v∷ bwdFwd v∷ [])

macro
  autoFieldEquiv : R.Term → R.Term → R.Term → R.Term → R.TC Unit
  autoFieldEquiv spec A B hole =
    (R.reduce spec >>= parseFieldSpec) >>= λ (ℓ , ℓ₂ , S , f) →
    buildDesc FUEL ℓ ℓ₂ S >>= λ d →
    R.unify hole (R.def (quote M.MacroEquivStr) (d v∷ tStrMap A f v∷ tStrMap B f v∷ []))

  autoUnivalentRecord : R.Term → R.Term → R.TC Unit
  autoUnivalentRecord t hole =
    (R.reduce t >>= parseSpec) >>= λ spec →
    -- R.typeError (R.strErr "WOW: " ∷ R.termErr (main spec) ∷ [])
    R.unify (main spec) hole
    where
    module _ (spec : InternalSpec TypedTerm) where
      open InternalSpec spec

      mapUp : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (ℕ → A → B) → ℕ → List A → List B
      mapUp f _ [] = []
      mapUp f n (x ∷ xs) = f n x ∷ mapUp f (suc n) xs

      closureSpec : InternalSpec ℕ
      closureSpec .InternalSpec.srec = srec
      closureSpec .InternalSpec.erec = erec
      closureSpec .InternalSpec.fields = mapUp (λ n → map-snd (λ _ → n)) 0 fields

      closure : R.Term
      closure =
        iter (List.length fields) (vlam "") (univalentRecord closureSpec)

      env : List (R.Arg R.Term)
      env = List.map (varg ∘ term ∘ snd) (List.rev fields)

      closureTy : R.Term
      closureTy =
        List.foldr
          (λ ty cod → R.def (quote Fun) (ty v∷ cod v∷ []))
          (R.def (quote ExplicitUnivalentStr) (srec v∷ erec v∷ []))
          (List.map (type ∘ snd) (List.rev fields))

      main : R.Term
      main = R.def (quote idfun) (closureTy v∷ closure v∷ env)

ext: agda

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Record where

module M where

  record A
    : Set
    where

    constructor

      a

open M

record B
  : Set
  where

record C
  : Set
  where

  constructor

    c

x
  : A
x
  = a

y
  : C
y
  = record {}

record D
  (E : Set)
  : Set
  where

record F
  : Set₁
  where

  field

    G
      : Set

    z
      : G

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
{-# OPTIONS --cubical --safe #-}
module JustBeInjective where

open import Cubical.Core.Everything
open import Cubical.Data.Unit
data maybe (A : Set) : Set where
  just : A -> maybe A
  nothing : maybe A

variable A : Set

unwrap : A → (a : maybe A) → A
unwrap _ (just x) = x
unwrap a nothing = a

just-injective : ∀ {A : Set} (a b : A) → just a ≡ just b → a ≡ b
just-injective a b p i = unwrap a (p i)

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
{-# OPTIONS --cubical #-}
module LaterPrims where

open import Agda.Primitive
open import Agda.Primitive.Cubical renaming (itIsOne to 1=1)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to outS)

module Prims where
  primitive
    primLockUniv : Set₁

open Prims renaming (primLockUniv to LockU) public

private
  variable
    l : Level
    A B : Set l

-- We postulate Tick as it is supposed to be an abstract sort.
postulate
  Tick : LockU

▹_ : ∀ {l} → Set l → Set l
▹_ A = (@tick x : Tick) -> A

▸_ : ∀ {l} → ▹ Set l → Set l
▸ A = (@tick x : Tick) → A x

next : A → ▹ A
next x _ = x

_⊛_ : ▹ (A → B) → ▹ A → ▹ B
_⊛_ f x a = f a (x a)

map▹ : (f : A → B) → ▹ A → ▹ B
map▹ f x α = f (x α)

transpLater : ∀ (A : I → ▹ Set) → ▸ (A i0) → ▸ (A i1)
transpLater A u0 a = primTransp (\ i → A i a) i0 (u0 a)

transpLater-prim : (A : I → ▹ Set) → (x : ▸ (A i0)) → ▸ (A i1)
transpLater-prim A x = primTransp (\ i → ▸ (A i)) i0 x

transpLater-test : ∀ (A : I → ▹ Set) → (x : ▸ (A i0)) → transpLater-prim A x ≡ transpLater A x
transpLater-test A x = \ _ → transpLater-prim A x

hcompLater-prim : ∀ (A : ▹ Set) φ (u : I → Partial φ (▸ A)) → (u0 : (▸ A) [ φ ↦ u i0 ]) → ▸ A
hcompLater-prim A φ u u0 a = primHComp (\ { i (φ = i1) → u i 1=1 a }) (outS u0 a)

hcompLater : ∀ (A : ▹ Set) φ (u : I → Partial φ (▸ A)) → (u0 : (▸ A) [ φ ↦ u i0 ]) → ▸ A
hcompLater A φ u u0 = primHComp (\ { i (φ = i1) → u i 1=1 }) (outS u0)

hcompLater-test : ∀ (A : ▹ Set) φ (u : I → Partial φ (▸ A)) → (u0 : (▸ A) [ φ ↦ u i0 ]) → hcompLater A φ u u0 ≡ hcompLater-prim A φ u u0
hcompLater-test A φ u x = \ _ → hcompLater-prim A φ u x

ap : ∀ {A B : Set} (f : A → B) → ∀ {x y} → x ≡ y → f x ≡ f y
ap f eq = \ i → f (eq i)

_$>_ : ∀ {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
eq $> x = \ i → eq i x
later-ext : ∀ {A : Set} → {f g : ▹ A} → (▸ \ α → f α ≡ g α) → f ≡ g
later-ext eq = \ i α → eq α i

postulate
  dfix : ∀ {l} {A : Set l} → (▹ A → A) → ▹ A
  pfix : ∀ {l} {A : Set l} (f : ▹ A → A) → dfix f ≡ (\ _ → f (dfix f))

pfix' : ∀ {l} {A : Set l} (f : ▹ A → A) → ▸ \ α → dfix f α ≡ f (dfix f)
pfix' f α i = pfix f i α

fix : ∀ {l} {A : Set l} → (▹ A → A) → A
fix f = f (dfix f)

data gStream (A : Set) : Set where
  cons : (x : A) (xs : ▹ gStream A) → gStream A

repeat : ∀ {A : Set} → A → gStream A
repeat a = fix \ repeat▹ → cons a repeat▹

repeat-eq : ∀ {A : Set} (a : A) → repeat a ≡ cons a (\ α → repeat a)
repeat-eq a = ap (cons a) (pfix (cons a))

map : ∀ {A B : Set} → (A → B) → gStream A → gStream B
map f = fix \ map▹ → \ { (cons a as) → cons (f a) \ α → map▹ α (as α) }

map-eq : ∀ {A B : Set} → (f : A → B) → ∀ a as → map f (cons a as) ≡ cons (f a) (\ α → map f (as α))
map-eq f a b = ap (cons _) (later-ext \ α → pfix' _ α $> b α)

_∙_ : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {x = x} p q i = primHComp (\ j → \ { (i = i0) → x; (i = i1) → q j}) (p i)

map-repeat : ∀ {A B : Set} → (a : A) → (f : A → B) → map f (repeat a) ≡ repeat (f a)
map-repeat a f = fix \ prf▹ → ap (map f) (repeat-eq a) ∙ (map-eq f a _ ∙ ap (cons (f a)) (later-ext prf▹ ∙ later-ext \ α → \ i → pfix' (cons (f a)) α (primINeg i) ))

max_stars_repo_name: rwe/agda

max_issues_repo_name: rwe/agda

max_forks_repo_name: rwe/agda


text:
module 120-natural-induction-necessary where

open import 010-false-true
open import 020-equivalence
open import 100-natural

-- We prove that the induction axiom is necessary.

-- Peano axioms without induction.

record NaturalWithoutInduction
  {M : Set}
  (zero : M)
  (suc : M -> M)
  (_==_ : M -> M -> Set)
  : Set1 where

  -- axioms
  field
    equiv : Equivalence _==_
    sucn!=zero : ∀ {r} -> suc r == zero -> False
    sucinjective : ∀ {r s} -> suc r == suc s -> r == s
    cong : ∀ {r s} -> r == s -> suc r == suc s
    not-induction :
      ((p : M -> Set) -> p zero -> (∀ n -> p n -> p (suc n)) -> ∀ n -> p n)
      -> False

  open Equivalence equiv public

-- Construct a model, and prove it satisfies NaturalWithoutInduction
-- but not Natural. To do this, we add an extra zero.

data M : Set where
  zero1 : M
  zero2 : M
  suc : M -> M

thm-M-is-natural-without-induction : NaturalWithoutInduction zero1 suc _≡_
thm-M-is-natural-without-induction = record {
  equiv = thm-≡-is-equivalence;
  sucn!=zero = sucn!=zero;
  sucinjective = sucinjective;
  cong = cong;
  not-induction = not-induction
  }
  where
    sucn!=zero : ∀ {r} -> suc r ≡ zero1 -> False
    sucn!=zero ()
    sucinjective : ∀ {r s} -> suc r ≡ suc s -> r ≡ s
    sucinjective refl = refl
    cong : ∀ {r s} -> r ≡ s -> suc r ≡ suc s
    cong refl = refl
    -- To prove that induction fails, we test the property "is a
    -- successor of zero1 but not of zero2". This holds for zero1 (the
    -- base case), and it also holds for every successor of n if it
    -- holds for n, but it does not hold for zero2 (or for any of its
    -- successors).
    not-induction :
      ((p : M -> Set) -> p zero1 -> (∀ n -> p n -> p (suc n)) -> ∀ n -> p n)
      -> False
    not-induction induction = induction p base hypothesis zero2
      where
        -- Property "is a successor of zero1 but not a successor of zero2".
        p : M -> Set
        p zero1 = True  -- true for zero1
        p zero2 = False -- false (no proof) for zero2
        p (suc n) = p n -- true for successor of n if and only if true for n

        -- Base case is trivial.
        base : p zero1
        base = trivial

        -- Induction hypothesis follows by application of "p n" itself
        -- due to the recursive definition of p.
        hypothesis : ∀ n -> p n -> p (suc n)
        hypothesis n pn = pn

-- To round this off, we explicitly prove that M is not natural.

thm-M-is-not-natural : (Natural zero1 suc _≡_) -> False
thm-M-is-not-natural nat =
  (NaturalWithoutInduction.not-induction thm-M-is-natural-without-induction)
  (Natural.induction nat)

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


text:
module Issue468 where

data Unit : Set where
 nothing : Unit

data Maybe (A : Set) : Set where
 nothing : Maybe A
 just    : A → Maybe A

data P : (R : Set) → Maybe R → Set₁ where
 p : (R : Set) (x : R) → P R (just x)

works : P Unit (just _)
works = p _ nothing

fails : Unit → P Unit (just _)
fails x = p _ nothing

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Setoids.Setoids
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Groups.Definition
open import Groups.Homomorphisms.Definition

module Groups.Isomorphisms.Definition where

record GroupIso {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) (f : A → B) : Set (m ⊔ n ⊔ o ⊔ p) where
  open Setoid S renaming (_∼_ to _∼G_)
  open Setoid T renaming (_∼_ to _∼H_)
  field
    groupHom : GroupHom G H f
    bij : SetoidBijection S T f

record GroupsIsomorphic {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·A_ : A → A → A} {B : Set n} {T : Setoid {n} {p} B} {_·B_ : B → B → B} (G : Group S _·A_) (H : Group T _·B_) : Set (m ⊔ n ⊔ o ⊔ p) where
  field
    isomorphism : A → B
    proof : GroupIso G H isomorphism


text:
module Lib.Vec where

open import Lib.Prelude
open import Lib.Nat
open import Lib.Fin

infixr 40 _::_ _++_

data Vec (A : Set) : Nat -> Set where
  []   : Vec A 0
  _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)

_++_ : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
[]        ++ ys = ys
(x :: xs) ++ ys = x :: xs ++ ys

_!_ : forall {A n} -> Vec A n -> Fin n -> A
[]      ! ()
x :: xs ! zero  = x
x :: xs ! suc i = xs ! i

tabulate : forall {A n} -> (Fin n -> A) -> Vec A n
tabulate {n = zero}  f = []
tabulate {n = suc n} f = f zero :: tabulate (f ∘ suc)

vec : forall {A n} -> A -> Vec A n
vec x = tabulate (\_ -> x)

infixl 30 _<*>_

_<*>_ : forall {A B n} -> Vec (A -> B) n -> Vec A n -> Vec B n
[]      <*> []      = []
f :: fs <*> x :: xs = f x :: (fs <*> xs)

map : forall {A B n} -> (A -> B) -> Vec A n -> Vec B n
map f xs = vec f <*> xs

zip : forall {A B C n} -> (A -> B -> C) -> Vec A n -> Vec B n -> Vec C n
zip f xs ys = vec f <*> xs <*> ys

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Instances.Unit where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Unit

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

private
  variable
    ℓ : Level

open CommRingStr

UnitCommRing : ∀ {ℓ} → CommRing ℓ
fst UnitCommRing = Unit*
0r (snd UnitCommRing) = tt*
1r (snd UnitCommRing) = tt*
_+_ (snd UnitCommRing) = λ _ _ → tt*
_·_ (snd UnitCommRing) = λ _ _ → tt*
- snd UnitCommRing = λ _ → tt*
isCommRing (snd UnitCommRing) =
  makeIsCommRing isSetUnit* (λ _ _ _ → refl) (λ { tt* → refl }) (λ _ → refl)
                 (λ _ _ → refl) (λ _ _ _ → refl) (λ { tt* → refl })
                 (λ _ _ _ → refl) (λ _ _ → refl)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Prelude.String where

open import Prelude.Bool
open import Prelude.Char
open import Prelude.List
open import Prelude.Nat

postulate
  String : Set
  nil : String
  primStringToNat : String → Nat
  charToString : Char -> String

{-# BUILTIN STRING String #-}

primitive
  primStringAppend   : String → String → String
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringEquality : String → String → Bool

{-# COMPILED_EPIC nil () -> String = "" #-}
{-# COMPILED_EPIC primStringToNat (s : String) -> BigInt = foreign BigInt "strToBigInt" (s : String) #-}
-- {-# COMPILED_EPIC charToString (c : Int) -> String = charToString(c) #-}

strEq : (x y : String) -> Bool
strEq = primStringEquality

infixr 30 _+S+_

_+S+_ : (x y : String) -> String
_+S+_ = primStringAppend

fromList : List Char -> String
fromList = primStringFromList

fromString : String -> List Char
fromString = primStringToList


text:
module Everything where

import Library
import Syntax
import RenamingAndSubstitution
import EquationalTheory

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
-- TODO: Unfinished
open import Logic
open import Type
open import Structure.Relator
open import Structure.Setoid

module Geometry.HilbertAxioms
  {ℓₚ ℓₗ ℓₚₑ ℓₗₑ ℓₚₗ ℓₚₚₚ}
  (Point : Type{ℓₚ}) ⦃ equiv-point : Equiv{ℓₚₑ}(Point) ⦄ -- The type of points on a plane.
  (Line : Type{ℓₗ}) ⦃ equiv-line : Equiv{ℓₗₑ}(Line) ⦄    -- The type of lines on a plane.
  (Distance : Type{ℓₗ}) ⦃ equiv-distance : Equiv{ℓₗₑ}(Distance) ⦄
  (Angle : Type{ℓₗ}) ⦃ equiv-angle : Equiv{ℓₗₑ}(Angle) ⦄
  (_∈ₚₗ_ : Point → Line → Stmt{ℓₚₗ})                     -- `p ∈ₚₗ l` means that the point `p` lies on the line `l`.
  (_―_―_ : Point → Point → Point → Stmt{ℓₚₚₚ})           -- `p₁ ― p₂ ― p₃` means that the second point `p₂` lies between `p₁` and `p₃` in some line.
  ⦃ incidence-relator : BinaryRelator(_∈ₚₗ_) ⦄
  ⦃ betweenness-relator : TrinaryRelator(_―_―_) ⦄
  where

open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Functional.Combinations
import      Lvl
open import Logic.Predicate
open import Logic.Propositional
open import Logic.Propositional.Xor
open import Sets.ExtensionalPredicateSet renaming (_≡_ to _≡ₛ_)
open import Structure.Relator.Properties
open import Structure.Setoid.Uniqueness
open import Syntax.Function

private variable p p₁ p₂ p₃ p₄ q q₁ q₂ q₃ q₄ : Point
private variable l l₁ l₂ : Line

module _ where
  -- An open line segment.
  -- The set of points strictly between two points in a line.
  -- Also called:
  -- • Open interval in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
  betweens : Point → Point → PredSet(Point)
  betweens a b ∋ p = a ― p ― b
  PredSet.preserve-equiv (betweens a b) = TrinaryRelator.unary₂ betweenness-relator

  extensionPoints : Point → Point → PredSet(Point)
  extensionPoints a b ∋ p = a ― b ― p
  PredSet.preserve-equiv (extensionPoints a b) = TrinaryRelator.unary₃ betweenness-relator

  -- A line segment.
  -- The set of points between two points in a line including the endpoints.
  segment : Point → Point → PredSet(Point)
  segment a b = (• a) ∪ (• b) ∪ (betweens a b)

  -- A ray.
  -- The set of points between starting from `a` in the direction of `b` in a line.
  ray : Point → Point → PredSet(Point)
  ray a b = (• a) ∪ (• b) ∪ (extensionPoints a b)

  angle : Point → Point → Point → PredSet(PredSet(Point))
  angle p₁ p₂ p₃ = (• ray p₁ p₂) ∪ (• ray p₁ p₃)

Distinct₃ : Point → Point → Point → Stmt
Distinct₃ = combine₃Fn₂Op₂(_≢_)(_∧_)

Collinear₃ : Point → Point → Point → Stmt
Collinear₃ p₁ p₂ p₃ = ∃(l ↦ all₃Fn₁Op₂(_∈ₚₗ l)(_∧_) p₁ p₂ p₃)

record Axioms : Type{ℓₚ Lvl.⊔ ℓₗ Lvl.⊔ ℓₚₑ Lvl.⊔ ℓₗₑ Lvl.⊔ ℓₚₗ Lvl.⊔ ℓₚₚₚ} where
  field
    -- There is an unique line for every unordered distinct pair of points.
    -- Also called:
    -- • I1 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
    -- • I.1 and I.2 in Project Gutenberg’s The Foundations of Geometry by David Hilbert.
    -- • I1 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
    line-construction : (p₁ ≢ p₂) → ∃!(l ↦ (p₁ ∈ₚₗ l) ∧ (p₂ ∈ₚₗ l))

    -- There are two distinct points on every line.
    -- Also called:
    -- • I2 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
    -- • I.7 in Project Gutenberg’s The Foundations of Geometry by David Hilbert.
    -- • I2 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
    line-deconstruction : ∃{Obj = Point ⨯ Point}(\{(p₁ , p₂) → (p₁ ≢ p₂) ∧ (p₁ ∈ₚₗ l) ∧ (p₂ ∈ₚₗ l)})

    -- There exists three points that constructs a triangle (not all on the same line).
    -- • I3 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
    -- • I3 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
    triangle-existence : ∃{Obj = Point ⨯ Point ⨯ Point}(\{(p₁ , p₂ , p₃) → ¬(Collinear₃ p₁ p₂ p₃)})

    -- The betweenness relation is strict (pairwise irreflexive).
    -- There are no points between a single point.
    betweenness-strictness : ¬(p₁ ― p₂ ― p₁)

    -- The betweenness relation is symmetric.
    -- Also called:
    -- • B1 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
    -- • II.1 in Project Gutenberg’s The Foundations of Geometry by David Hilbert.
    -- • B1 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
    betweenness-symmetry : (p₁ ― p₂ ― p₃) → (p₃ ― p₂ ― p₁)

    -- A line segment can be extended to a third point.
    -- • Part of II.2 in Project Gutenberg’s The Foundations of Geometry by David Hilbert.
    -- • B2 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
    -- • B2 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
    betweenness-extensionᵣ : (p₁ ≢ p₂) → ∃(p₃ ↦ (p₁ ― p₂ ― p₃))

    -- Three points are always between each other in a certain order.
    betweenness-antisymmetryₗ : (p₁ ― p₂ ― p₃) → (p₂ ― p₁ ― p₃) → ⊥

    -- Three distinct points on a line are always between each other in a certain order.
    -- Also called:
    -- • Part of B3 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
    -- • Part of II.3 in Project Gutenberg’s The Foundations of Geometry by David Hilbert.
    -- • Part of B3 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
    betweenness-cases : (Distinct₃ p₁ p₂ p₃) → (Collinear₃ p₁ p₂ p₃) → (rotate₃Fn₃Op₂(_―_―_)(_∨_) p₁ p₂ p₃)

    -- For three points that forms a triangle, and a line not intersecting the triangle's vertices, but intersecting one of its edges. Such a line intersects exactly one of the other edges of the triangle.
    -- Also called:
    -- • Pasch's axiom
    -- • B4 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
    -- • II.5 in Project Gutenberg’s The Foundations of Geometry by David Hilbert.
    -- • B4 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
    line-triangle-intersection : ¬(Collinear₃ p₁ p₂ p₃) → (all₃Fn₁Op₂(¬_ ∘ (_∈ₚₗ l))(_∧_) p₁ p₂ p₃) → ((p ∈ₚₗ l) ∧ (p₁ ― p ― p₂)) → (∃(p ↦ (p ∈ₚₗ l) ∧ (p₁ ― p ― p₃)) ⊕ ∃(p ↦ (p ∈ₚₗ l) ∧ (p₂ ― p ― p₃)))

    -- TODO: The rest of the axioms are not yet formulated because I am not sure what the best way to express them is
    ray-segment : ∃!(p ↦ (p ∈ ray p₁ p₂) ∧ (segment q₁ q₂ ≡ₛ segment p₁ p))
    segment-concat : (p₁ ― p₂ ― p₃) → (q₁ ― q₂ ― q₃) → (segment p₁ p₂ ≡ₛ segment q₁ q₂) → (segment p₂ p₃ ≡ₛ segment q₂ q₃) → (segment p₁ p₃ ≡ₛ segment q₁ q₃)

  -- A pair of points constructs a line.
  line : (a : Point) → (b : Point) → (a ≢ b) → Line
  line a b nab = [∃!]-witness(line-construction nab)

  -- A line can be deconstructed to two points.
  linePoints : Line → (Point ⨯ Point)
  linePoints l = [∃]-witness(line-deconstruction{l})

  -- The point to the left in the construction of a line is in the line.
  line-construction-pointₗ : (np12 : p₁ ≢ p₂) → (p₁ ∈ₚₗ line p₁ p₂ np12)
  line-construction-pointₗ np12 = [∧]-elimₗ([∃!]-proof (line-construction np12))

  -- The point to the right in the construction of a line is in the line.
  line-construction-pointᵣ : (np12 : p₁ ≢ p₂) → (p₂ ∈ₚₗ line p₁ p₂ np12)
  line-construction-pointᵣ np12 = [∧]-elimᵣ([∃!]-proof (line-construction np12))

  -- Two lines having a pair of common points are the same line..
  line-uniqueness : (p₁ ≢ p₂) → (p₁ ∈ₚₗ l₁) → (p₂ ∈ₚₗ l₁) → (p₁ ∈ₚₗ l₂) → (p₂ ∈ₚₗ l₂) → (l₁ ≡ l₂)
  line-uniqueness np12 p1l1 p2l1 p1l2 p2l2 = [∃!]-uniqueness (line-construction np12) ([∧]-intro p1l1 p2l1) ([∧]-intro p1l2 p2l2)

  -- The deconstructed points of a line are distinct.
  linePoints-distinct : let (a , b) = linePoints(l) in (a ≢ b)
  linePoints-distinct = [∧]-elimₗ([∧]-elimₗ([∃]-proof(line-deconstruction)))

  -- The left deconstructed point of a line is in the line.
  linePoints-pointₗ : Tuple.left(linePoints(l)) ∈ₚₗ l
  linePoints-pointₗ = [∧]-elimᵣ([∧]-elimₗ([∃]-proof(line-deconstruction)))

  -- The right deconstructed point of a line is in the line.
  linePoints-pointᵣ : Tuple.right(linePoints(l)) ∈ₚₗ l
  linePoints-pointᵣ = [∧]-elimᵣ([∃]-proof(line-deconstruction))

  -- The line of the deconstructed points of a line is the same line.
  line-linePoints-inverseᵣ : let (a , b) = linePoints(l) in (line a b linePoints-distinct ≡ l)
  line-linePoints-inverseᵣ = line-uniqueness
    linePoints-distinct (line-construction-pointₗ linePoints-distinct) (line-construction-pointᵣ linePoints-distinct) linePoints-pointₗ linePoints-pointᵣ

  betweenness-antisymmetryᵣ : (p₁ ― p₂ ― p₃) → (p₁ ― p₃ ― p₂) → ⊥
  betweenness-antisymmetryᵣ p123 p132 = betweenness-antisymmetryₗ (betweenness-symmetry p123) (betweenness-symmetry p132)

  betweenness-irreflexivityₗ : ¬(p₁ ― p₁ ― p₂)
  betweenness-irreflexivityₗ p112 = betweenness-antisymmetryₗ p112 p112

  betweenness-irreflexivityᵣ : ¬(p₁ ― p₂ ― p₂)
  betweenness-irreflexivityᵣ p122 = betweenness-irreflexivityₗ (betweenness-symmetry p122)

  -- Also called:
  -- • B1 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
  -- • B1 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
  betweenness-distinct : (p₁ ― p₂ ― p₃) → (Distinct₃ p₁ p₂ p₃)
  Tuple.left              (betweenness-distinct p123)  p12 = betweenness-irreflexivityₗ(substitute₃-unary₁(_―_―_) p12 p123)
  Tuple.left (Tuple.right (betweenness-distinct p123)) p13 = betweenness-strictness(substitute₃-unary₁(_―_―_) p13 p123)
  Tuple.right(Tuple.right (betweenness-distinct p123)) p23 = betweenness-irreflexivityᵣ(substitute₃-unary₂(_―_―_) p23 p123)

  betweenness-extensionₗ : (p₂ ≢ p₃) → ∃(p₁ ↦ (p₁ ― p₂ ― p₃))
  betweenness-extensionₗ np23 = [∃]-map-proof betweenness-symmetry (betweenness-extensionᵣ (np23 ∘ symmetry(_≡_)))

  -- Three points are always between each other in a certain order.
    -- Also called:
    -- • B3 in Hilbert’s Axiom System for Plane Geometry, A Short Introduction by Bjørn Jahren.
    -- • II.3 in Project Gutenberg’s The Foundations of Geometry by David Hilbert.
    -- • B3 in A Minimal Version of Hilbert's Axioms for Plane Geometry by William Richter.
  betweenness-distinct-cases : (Distinct₃ p₁ p₂ p₃) → (Collinear₃ p₁ p₂ p₃) → ((p₁ ― p₂ ― p₃) ⊕₃ (p₂ ― p₃ ― p₁) ⊕₃ (p₃ ― p₁ ― p₂))
  betweenness-distinct-cases pd pl with betweenness-cases pd pl
  ... | [∨]-introₗ             p123  = [⊕₃]-intro₁ p123 (betweenness-antisymmetryₗ (betweenness-symmetry p123)) (betweenness-antisymmetryᵣ (betweenness-symmetry p123))
  ... | [∨]-introᵣ ([∨]-introₗ p231) = [⊕₃]-intro₂ (betweenness-antisymmetryᵣ ((betweenness-symmetry p231))) p231 (betweenness-antisymmetryₗ ((betweenness-symmetry p231)))
  ... | [∨]-introᵣ ([∨]-introᵣ p312) = [⊕₃]-intro₃ (betweenness-antisymmetryₗ (betweenness-symmetry p312)) (betweenness-antisymmetryᵣ (betweenness-symmetry p312)) p312

  --betweenness-between : (p₁ ≢ p₂) → (p₁ ∈ₚₗ l) → (p₂ ∈ₚₗ l) → ∃(p ↦ p₁ ― p ― p₂)
  --betweenness-between np12 p1l p2l = {!!}

  --betweenness-collinnear : (p₁ ― p₂ ― p₃) → (Collinear₃ p₁ p₂ p₃)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --sized-types #-}
module GiveSize where

postulate Size : Set
{-# BUILTIN SIZE Size #-}

id : Size → Size
id i = {!i!}

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Syntax.NegativeTranslations (𝔏 : Signature) where
open Signature(𝔏)

open import Data.ListSized
import      Lvl
open import Formalization.PredicateLogic.Syntax (𝔏)
open import Functional using (_∘_ ; _∘₂_ ; swap)
open import Numeral.Finite
open import Numeral.Natural
open import Sets.PredicateSet using (PredSet)
open import Type

private variable ℓ : Lvl.Level
private variable args vars : ℕ

-- Also called: Gödel-Gentzen's negative translation.
-- 2.3.3
ggTrans : Formula(vars) → Formula(vars)
ggTrans (P $ x) = ¬¬(P $ x)
ggTrans ⊤       = ⊤
ggTrans ⊥       = ⊥
ggTrans (φ ∧ ψ) = (ggTrans φ) ∧ (ggTrans ψ)
ggTrans (φ ∨ ψ) = ¬(¬(ggTrans φ) ∧ ¬(ggTrans ψ))
ggTrans (φ ⟶ ψ) = (ggTrans φ) ⟶ (ggTrans ψ)
ggTrans (Ɐ φ)   = Ɐ(ggTrans φ)
ggTrans (∃ φ)   = ¬ Ɐ(¬(ggTrans φ))

-- Also called: Kolmogorov's negative translation.
-- 2.3.7A
koTrans : Formula(vars) → Formula(vars)
koTrans (P $ x) = ¬¬(P $ x)
koTrans ⊤       = ⊤
koTrans ⊥       = ⊥
koTrans (φ ∧ ψ) = ¬¬((koTrans φ) ∧ (koTrans ψ))
koTrans (φ ∨ ψ) = ¬¬((koTrans φ) ∨ (koTrans ψ))
koTrans (φ ⟶ ψ) = ¬¬((koTrans φ) ⟶ (koTrans ψ))
koTrans (Ɐ φ)   = ¬¬ Ɐ(koTrans φ)
koTrans (∃ φ)   = ¬¬ ∃(koTrans φ)

-- Also called: Kuroda's negative translation.
-- 2.3.7B
kuTrans : Formula(vars) → Formula(vars)
kuTrans (P $ x) = P $ x
kuTrans ⊤       = ⊤
kuTrans ⊥       = ⊥
kuTrans (φ ∧ ψ) = ((koTrans φ) ∧ (koTrans ψ))
kuTrans (φ ∨ ψ) = ((koTrans φ) ∨ (koTrans ψ))
kuTrans (φ ⟶ ψ) = ((koTrans φ) ⟶ (koTrans ψ))
kuTrans (Ɐ φ)   = Ɐ(¬¬(koTrans φ))
kuTrans (∃ φ)   = ∃(koTrans φ)


text:
module Lawvere where

open import Library
open import Data.Sum
open import Categories
open import Categories.Sets
open import Categories.Initial
open import Categories.PushOuts
open import Categories.Products hiding (_×_)
open import Categories.CoProducts
open import Categories.Terminal

open import Functors
open import Functors.Fin

record Lawvere {a}{b} : Set (lsuc (a ⊔ b)) where
  constructor lawvere
  field T  : Cat {a}{b}
        L  : Fun (Nats Op) T
        L0 : Term T (Fun.OMap L zero)
        LP : ∀ m n → Prod T (Fun.OMap L m) (Fun.OMap L n)

-- it's not the identity, it switches some implicit in fid and fcomp I think
FunOp : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}} →
        Fun C D → Fun (C Op) (D Op)
FunOp (functor OMap HMap fid fcomp) = functor OMap HMap fid fcomp

LSet : Lawvere
LSet = lawvere
  (Sets Op)
  (FunOp FinF)
  (term (λ ()) (ext λ ()))
  λ m n → prod
    (Fin m ⊎ Fin n)
    inj₁
    inj₂
    [_,_]′
    refl
    refl
    λ p q → ext (λ{ (inj₁ a) -> fcong a p; (inj₂ b) -> fcong b q})

open import RMonads
open import RMonads.RKleisli
open import RMonads.RKleisli.Functors

lem : RMonad FinF → Lawvere {lzero}{lzero}
lem M = lawvere
  (Kl M Op)
  (FunOp (RKlL M) )
  (term (λ ()) (ext λ ()))
  λ m n → prod
    (m + n)
    (η ∘ extend)
    (η ∘ lift m)
    (case m)
    (ext λ i → trans (fcong (extend i) law2) (lem1 m _ _ i))
    (ext λ i → trans (fcong (lift m i) law2) (lem2 m _ _ i))
    λ {o} {f} {g} {h} p q → ext (lem3
      m
      f
      g
      h
      (trans (ext λ i → sym (fcong (extend i) law2)) p)
      (trans (ext λ i → sym (fcong (lift m i) law2)) q))
    where open RMonad M

lem-1 : Lawvere {lzero}{lzero} → RMonad FinF
lem-1 LT = rmonad
  (λ n → Cat.Hom (Lawvere.T LT) (Fun.OMap (Lawvere.L LT) 1) (Fun.OMap (Lawvere.L LT) n))
  {!!}
  {!!}
  {!!}
  {!!}
  {!!}

open import Categories.Products

record Model {a}{b}{c}{d} (Law : Lawvere {a}{b}) : Set (lsuc (a ⊔ b ⊔ c ⊔ d))
  where
  open Lawvere Law
  field C : Cat {c}{d}
        F : Fun T C
        F0 : Term C (Fun.OMap F (Fun.OMap L zero))
        FP : ∀ m n → Prod C (Fun.OMap F (Fun.OMap L m))
                            (Fun.OMap F (Fun.OMap L n))
open import RMonads.REM
open import RMonads.CatofRAdj.InitRAdj
open import RMonads.CatofRAdj.TermRAdjObj
open import RMonads.REM.Functors

model : (T : RMonad FinF) → Model (lem T)
model T = record {
  C  = EM T Op ;
  F  = FunOp (K' T (EMObj T));
  F0 = term (λ{alg} → ralgmorph (RAlg.astr alg {0} (λ ()))
                               (λ {n}{f} →
                                 sym $ RAlg.alaw2 alg {n}{zero}{f}{λ ()} ))
           (λ{alg}{f} → RAlgMorphEq T (ext (λ t → trans
             (trans (cong (λ f₁ → RAlg.astr alg f₁ t) (ext (λ ())))
                    (sym (fcong t (RAlgMorph.ahom f {0}{RMonad.η T}))))
             (cong (RAlgMorph.amor f) (fcong t (RMonad.law1 T))))));
  FP = λ m n → prod
    (Fun.OMap (REML FinF T) (m + n) )
    (Fun.HMap (REML FinF T) extend)
    (Fun.HMap (REML FinF T) (lift m))
    (λ{alg} f g → ralgmorph
      (RAlg.astr alg
                 (case m (RAlgMorph.amor f ∘ RMonad.η T)
                         (RAlgMorph.amor g ∘ RMonad.η T)))
      (sym (RAlg.alaw2 alg)))
    (λ {alg}{f}{g} → RAlgMorphEq T (trans
      (sym (RAlg.alaw2 alg))
      (trans (cong (RAlg.astr alg)
                   (ext λ i → trans (fcong (extend i) (sym (RAlg.alaw1 alg)))
                                    (lem1 m _ _ i)))
             (trans (sym (RAlgMorph.ahom f))
                    (ext λ i → cong (RAlgMorph.amor f)
                                    (fcong i (RMonad.law1 T)))))))
    (λ {alg}{f}{g} → RAlgMorphEq T (trans
      (sym (RAlg.alaw2 alg))
      (trans (cong (RAlg.astr alg)
                   (ext λ i → trans (fcong (lift m i) (sym (RAlg.alaw1 alg)))
                                    (lem2 m _ _ i)))
             (trans (sym (RAlgMorph.ahom g))
                    (ext λ i → cong (RAlgMorph.amor g)
                                    (fcong i (RMonad.law1 T)))))))
    λ{alg}{f}{g}{h} p q → RAlgMorphEq T (trans
      (trans (ext λ i → cong (RAlgMorph.amor h)
                             (sym (fcong i (RMonad.law1 T))))
             (RAlgMorph.ahom h))
      (cong (RAlg.astr alg) (ext (lem3
        m
        (RAlgMorph.amor f ∘ RMonad.η T)
        (RAlgMorph.amor g ∘ RMonad.η T)
        (RAlgMorph.amor h ∘ RMonad.η T)
        (ext λ i → trans
          (cong (RAlgMorph.amor h) (sym (fcong i (RMonad.law2 T))))
          (fcong (RMonad.η T i) (cong RAlgMorph.amor p)))
        (ext λ i → trans
          (cong (RAlgMorph.amor h) (sym (fcong i (RMonad.law2 T))))
          (fcong (RMonad.η T i) (cong RAlgMorph.amor q)))))))}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module UniDB.Subst.Core where

open import UniDB.Spec public
open import UniDB.Morph.Unit

record Ap (T X : STX) : Set₁ where
  field
    ap : {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
      {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (x : X γ₁) → X γ₂
open Ap {{...}} public

record ApVr (T : STX) {{vrT : Vr T}} {{apTT : Ap T T}} : Set₁ where
  field
    ap-vr :
      {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
      {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) →
      (i : Ix γ₁) → ap {T} ξ (vr i) ≡ lk {T} ξ i
open ApVr {{...}} public

record LkCompAp
  (T : STX) {{vrT : Vr T}} {{apTT : Ap T T}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{compΞ : Comp Ξ}} : Set₁ where
  field
    lk-⊙-ap : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Ξ γ₁ γ₂) (ξ₂ : Ξ γ₂ γ₃)
      (i : Ix γ₁) → lk {T} (ξ₁ ⊙ ξ₂) i ≡ ap {T} ξ₂ (lk ξ₁ i)
open LkCompAp {{...}} public

record ApIdm
  (T : STX) {{vrT : Vr T}}
  (X : STX) {{apTX : Ap T X}} : Set₁ where
  field
    ap-idm :
      {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{idmΞ : Idm Ξ}}
      {{lkIdmTΞ : LkIdm T Ξ}} {{upIdmΞ : UpIdm Ξ}}
      {γ : Dom} (x : X γ) →
      ap {T} (idm {Ξ} γ) x ≡ x
open ApIdm {{...}} public

record ApRel
  (T : STX) {{vrT : Vr T}}
  (X : STX) {{apTX : Ap T X}} : Set₁ where
  field
    ap-rel≅ :
      {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
      {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}}
      {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂} (hyp : [ T ] ξ ≅ ζ)
      (x : X γ₁) → ap {T} ξ x ≡ ap {T} ζ x

  ap-rel≃ :  {{wkT : Wk T}}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{lkUpTΞ : LkUp T Ξ}}
    {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} {{lkUpTΖ : LkUp T Ζ}}
    {γ₁ γ₂ : Dom} {ξ : Ξ γ₁ γ₂} {ζ : Ζ γ₁ γ₂} (hyp : [ T ] ξ ≃ ζ)
    (x : X γ₁) → ap {T} ξ x ≡ ap {T} ζ x
  ap-rel≃ hyp = ap-rel≅ (≃-to-≅` (≃-↑ hyp))
open ApRel {{...}} public

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}}
  (X : STX) {{wkX : Wk X}} {{apTX : Ap T X}}
  where

  record ApWkmWk : Set₁ where
    field
      ap-wkm-wk₁ :
        {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{wkmΞ : Wkm Ξ}}
        {{lkUpTΞ : LkUp T Ξ}} {{lkWkmTΞ : LkWkm T Ξ}}
        {γ : Dom} (x : X γ) →
        ap {T} (wkm {Ξ} 1) x ≡ wk₁ x
      ap-wkm-wk :
        {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{wkmΞ : Wkm Ξ}}
        {{lkUpTΞ : LkUp T Ξ}} {{lkWkmTΞ : LkWkm T Ξ}}
        {γ : Dom} (δ : Dom) (x : X γ) →
        ap {T} (wkm {Ξ} δ) x ≡ wk δ x

  open ApWkmWk {{...}} public

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}}
  (X : STX) {{wkX : Wk X}} {{apTX : Ap T X}}
  where

  record ApWk : Set₁ where
    field
      ap-wk₁ :
        {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
        {{lkUpTΞ : LkUp T Ξ}}
        {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (x : X γ₁) →
        ap {T} (ξ ↑₁) (wk₁ x) ≡ wk₁ (ap {T} ξ x)
  open ApWk {{...}} public

module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  (X : STX) {{apTX : Ap T X}}
  where

  record ApComp : Set₁ where
    field
      ap-⊙ :
        {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{compΞ : Comp Ξ}}
        {{upCompΞ : UpComp Ξ}} {{lkCompTΞ : LkCompAp T Ξ}}
        {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Ξ γ₁ γ₂) (ξ₂ : Ξ γ₂ γ₃) →
          (x : X γ₁) → ap {T} (ξ₁ ⊙ ξ₂) x ≡ ap {T} ξ₂ (ap {T} ξ₁ x)
  open ApComp {{...}} public

instance
  iApIx : Ap Ix Ix
  ap {{iApIx}} = lk

  iApVrIx : ApVr Ix
  ap-vr {{iApVrIx}} ξ i = refl

  iApIdmIxIx : ApIdm Ix Ix
  ap-idm {{iApIdmIxIx}} {Ξ} = lk-idm {Ix} {Ξ}

  iApWkmWkIxIx : ApWkmWk Ix Ix
  ap-wkm-wk₁ {{iApWkmWkIxIx}} {Ξ} = lk-wkm {Ix} {Ξ} 1
  ap-wkm-wk {{iApWkmWkIxIx}} {Ξ} = lk-wkm {Ix} {Ξ}

  iApRelIxIx : ApRel Ix Ix
  ap-rel≅ {{iApRelIxIx}} = lk≃ ∘ ≅-to-≃

  iApWkIxIx : ApWk Ix Ix
  ap-wk₁ {{iApWkIxIx}} {Ξ} ξ i = lk-↑₁-suc {Ix} {Ξ} ξ i

-- TODO: Remove
module _
  (T : STX) {{vrT : Vr T}} {{apTT : Ap T T}}
  (Ξ : MOR) {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
  (Ζ : MOR) {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}}
  (Θ : MOR) {{lkTΘ : Lk T Θ}} {{upΘ : Up Θ}}
  {{hcompΞΖΘ : HComp Ξ Ζ Θ}}
  where

  record LkHCompAp : Set₁ where
    field
      lk-⊡-ap : {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₂ γ₃)
        (i : Ix γ₁) → lk {T} {Θ} (ξ ⊡ ζ) i ≡ ap {T} ζ (lk ξ i)
  open LkHCompAp {{...}} public

-- TODO: Remove
module _
  (T : STX) {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}}
  (X : STX) {{apTX : Ap T X}}
  where

  record ApHComp : Set₁ where
    field
      ap-⊡ :
        {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}}
        {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}}
        {Θ : MOR} {{lkTΘ : Lk T Θ}} {{upΘ : Up Θ}}
        {{hcompΞΖΘ : HComp Ξ Ζ Θ}} {{upHCompΞ : UpHComp Ξ Ζ Θ}}
        {{lkHCompTΞΖΘ : LkHCompAp T Ξ Ζ Θ}}
        {γ₁ γ₂ γ₃ : Dom} (ξ : Ξ γ₁ γ₂) (ζ : Ζ γ₂ γ₃) →
          (x : X γ₁) → ap {T} {X} {Θ} (ξ ⊡ ζ) x ≡ ap {T} ζ (ap {T} ξ x)
  open ApHComp {{...}} public

-- TODO: Move
module _
  {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{wkVrT : WkVr T}}
  {X : STX} {{wkX : Wk X}} {{apTX : Ap T X}} {{apRelTX : ApRel T X}} {{apIdmTX : ApIdm T X}}
  {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{idmΞ : Idm Ξ}} {{lkIdmTΞ : LkIdm T Ξ}}
  {{lkUpTΞ : LkUp T Ξ}}
  where

  ap-idm` : {γ : Dom} (x : X γ) → ap {T} (idm {Ξ} γ) x ≡ x
  ap-idm` {γ} x = begin
    ap {T} (idm {Ξ} γ) x    ≡⟨ ap-rel≃ {T} lem x ⟩
    ap {T} (idm {Unit} γ) x ≡⟨ ap-idm {T} x ⟩
    x ∎
    where
      lem : [ T ] idm {Ξ} γ ≃ unit
      lk≃ lem = lk-idm {T} {Ξ}

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

infixr 6 _∷_

data List (A : Set) : Set where
  [] : List A
  _∷_ : A -> List A -> List A

postulate
  Bool : Set
  t : Bool

long : List Bool
long =
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷ t ∷
 []

meta : Set
meta = _

max_stars_repo_name: larrytheliquid/agda


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

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.HITs.Sn
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₋₁ ; ∣_∣ to ∣_∣₋₁)
open import Cubical.HITs.Nullification
open import Cubical.Data.Int hiding (_+_ ; +-comm)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation
open import Cubical.Homotopy.Connected
open import Cubical.Data.Unit
open import Cubical.Algebra.Group

-- H⁰(Unit)
open GroupHom
open GroupIso
private
  H⁰-Unit≅ℤ' : GroupIso (coHomGr 0 Unit) intGroup
  fun (GroupIso.map H⁰-Unit≅ℤ') = sRec isSetInt (λ f → f tt)
  isHom (GroupIso.map H⁰-Unit≅ℤ') = sElim2 (λ _ _ → isOfHLevelPath 2 isSetInt _ _) λ a b → addLemma (a tt) (b tt)
  inv H⁰-Unit≅ℤ' a = ∣ (λ _ → a) ∣₂
  rightInv H⁰-Unit≅ℤ' _ = refl
  leftInv H⁰-Unit≅ℤ' = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _) λ a → refl

H⁰-Unit≅ℤ : GroupEquiv (coHomGr 0 Unit) intGroup
H⁰-Unit≅ℤ = GrIsoToGrEquiv H⁰-Unit≅ℤ'

{- Hⁿ(Unit) for n ≥ 1 -}
isContrHⁿ-Unit : (n : ℕ) → isContr (coHom (suc n) Unit)
isContrHⁿ-Unit n = subst isContr (λ i → ∥ UnitToTypePath (coHomK (suc n)) (~ i) ∥₂) (helper' n)
  where
  helper' : (n : ℕ) → isContr (∥ coHomK (suc n) ∥₂)
  helper' n =
    subst isContr
      ((isoToPath (truncOfTruncIso {A = S₊ (1 + n)} 2 (1 + n)))
         ∙∙ sym propTrunc≡Trunc2
         ∙∙ λ i → ∥ hLevelTrunc (suc (+-comm n 2 i)) (S₊ (1 + n)) ∥₂)
      (isConnectedSubtr 2 (helper2 n .fst)
        (subst (λ x → isConnected x (S₊ (suc n))) (sym (helper2 n .snd)) (sphereConnected (suc n))) )
    where
    helper2 : (n : ℕ) → Σ[ m ∈ ℕ ] m + 2  ≡ 2 + n
    helper2 zero = 0 , refl
    helper2 (suc n) = (suc n) , λ i → suc (+-comm n 2 i)

Hⁿ-Unit≅0' : (n : ℕ) → GroupIso (coHomGr (suc n) Unit) trivialGroup
GroupHom.fun (GroupIso.map (Hⁿ-Unit≅0' n)) _ = _
GroupHom.isHom (GroupIso.map (Hⁿ-Unit≅0' n)) _ _ = refl
GroupIso.inv (Hⁿ-Unit≅0' n) _ = 0ₕ
GroupIso.rightInv (Hⁿ-Unit≅0' n) _ = refl
GroupIso.leftInv (Hⁿ-Unit≅0' n) _ = isOfHLevelSuc 0 (isContrHⁿ-Unit n) _ _

Hⁿ-Unit≅0 : (n : ℕ) → GroupEquiv (coHomGr (suc n) Unit) trivialGroup
Hⁿ-Unit≅0 n = GrIsoToGrEquiv (Hⁿ-Unit≅0' n)

{- Hⁿ for arbitrary contractible types -}
private
  Hⁿ-contrTypeIso : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isContr A
                   → Iso (coHom (suc n) A) (coHom (suc n) Unit)
  Hⁿ-contrTypeIso n contr = compIso (setTruncIso (isContr→Iso2 contr))
                                    (setTruncIso (invIso (isContr→Iso2 isContrUnit)))

  Hⁿ-contrType≅0' : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isContr A
                → GroupIso (coHomGr (suc n) A) trivialGroup
  fun (GroupIso.map (Hⁿ-contrType≅0' _ _)) _ = _
  isHom (GroupIso.map (Hⁿ-contrType≅0' _ _)) _ _ = refl
  inv (Hⁿ-contrType≅0' _ _) _ = 0ₕ
  rightInv (Hⁿ-contrType≅0' _ _) _ = refl
  leftInv (Hⁿ-contrType≅0' {A = A} n contr) _ = isOfHLevelSuc 0 helper _ _
    where
    helper : isContr (coHom (suc n) A)
    helper = (Iso.inv (Hⁿ-contrTypeIso n contr) 0ₕ)
            , λ y →  cong (Iso.inv (Hⁿ-contrTypeIso n contr))
                           (isOfHLevelSuc 0 (isContrHⁿ-Unit n) 0ₕ (Iso.fun (Hⁿ-contrTypeIso n contr) y))
                    ∙ Iso.leftInv (Hⁿ-contrTypeIso n contr) y

Hⁿ-contrType≅0 : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isContr A
              → GroupEquiv (coHomGr (suc n) A) trivialGroup
Hⁿ-contrType≅0 n contr = GrIsoToGrEquiv (Hⁿ-contrType≅0' n contr)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Instances.FreeAbGroup where

open import Cubical.Foundations.Prelude
open import Cubical.HITs.FreeAbGroup
open import Cubical.Algebra.AbGroup

private variable
  ℓ : Level

module _ {A : Type ℓ} where

  FAGAbGroup : AbGroup ℓ
  FAGAbGroup = makeAbGroup {G = FreeAbGroup A} ε _·_ _⁻¹ trunc assoc identityᵣ invᵣ comm