ice1000

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat using (Nat; suc; zero)

cong : (f : Nat → Nat) → ∀ {a b} → a ≡ b → f a ≡ f b
cong f refl = refl
trans : ∀ {a b c : Nat} → a ≡ b → b ≡ c → a ≡ c
trans refl p = p
sym : ∀ {a b : Nat} → a ≡ b → b ≡ a
sym refl = refl

ice1000

\import Data.Bool
\import Data.List
\import Logic.Meta
\import Paths

\func CoNat =>
  \Sigma (f : Nat -> Bool)
         (\Pi (i : _) -> f i = false -> f (suc i) = false)
  \where {
    \func blt (n m : Nat) : Bool

ice1000

module PSet3 where

record TermStructure : Set₁ where
  field
    Term : Set

module QPER (TS TS' : TermStructure) where
  open TermStructure TS
  open TermStructure TS'
    renaming (Term to Term')

ice1000

Definition lemma {n m : nat} (p : n = m) : pred n = pred m := f_equal pred p.
Definition lemma2 {n m : nat} (p : n = m) : S n = S m := f_equal S p.
Definition lemma3 {n m : nat} (p : S n = S m) : lemma2 (lemma p) = p
  := match p with | eq_refl => eq_refl end.

(* Definition bruh {n} (a : nat) (p : S n = a) : Prop.
Proof.
  destruct a.
  - exact True.
  - exact (@lemma2 n a (@lemma (S n) (S a) p) = p).

ice1000

Inductive nat: Type :=
| S (n: nat)
| O.

Inductive even: nat -> Prop :=
| Base: even O
| Ind: forall n, even n -> even (S (S n)).

Inductive ev: nat -> Prop :=
| ev_Base: ev O

ice1000

variable
  A B : Set
postulate
  Eq : A → A → Set
  refl : (a : A) → Eq a a
  rw : {x y : A} → Eq x y → (B : A → Set) → B x → B y
  -- UIP missing but not needed
  N : Set
  Z : N
  S : N → N

ice1000

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Data.List

private variable X : Type

rev-ind : (P : List X → Type)
  → P []
  → (∀ x xs → P xs → P (xs ∷ʳ x))

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Data.Int
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.SetTruncation

-- Maps out of a set-truncated int can only target sets,
-- yet it's equivalent to the normal int

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Data.List
open import Cubical.Data.Nat.Base
open import Cubical.Data.Equality hiding (map)

variable
  A : Type
  B : Type
  n : ℕ

ice1000

{-# OPTIONS --cubical #-}

open import Cubical.Data.Vec
open import Cubical.Data.Nat.Base
open import Cubical.Data.Equality hiding (map)

variable
  A : Type
  B : Type
  n : ℕ